auto_compiler in tc.v

apps/tc/elpi/compiler.elpi

@@ -148,12 +148,6 @@ has-context-deps GR :-
 pred is-local.
 is-local :- std.mem {attributes} (attribute "local" _).
 
-pred make-inst-graft i:gref, i:bool, o:grafting.
-make-inst-graft Inst _NoPremises (after Grafting) :- 
-  RawGrafting is int_to_string {get-inst-prio Inst},
-  % if (NoPremises = tt) (Grafting = RawGrafting) (Grafting is RawGrafting ^ "_complex").
-  Grafting = RawGrafting.
-
 pred get-locality i:string, o:list prop.
 get-locality "Local" [@local!].
 get-locality _ [@local!] :- coq.env.current-section-path [_ | _].
@@ -166,9 +160,7 @@ add-inst Inst TC Locality Prio :-
   compile Inst _ TC Clause, 
   % TODO: a clause is flexible if an instance is polimorphic (pglobal)
   not (var Clause),
-  if (Prio = -1) 
-    (get-inst-prio Inst Prio1)
-    (Prio1 = Prio),
+  if (Prio = -1) (get-inst-prio Inst Prio1) (Prio1 = Prio),
   Graft is after (int_to_string Prio1),
   get-full-path Inst ClauseName,
   get-locality Locality LocalityProp,
@@ -188,10 +180,10 @@ add-inst->db IgnoreClassDepL ForceAdd Inst :-
   if ((ForceAdd = tt; not (instance _ Inst _)), 
     not (std.exists Dep (std.mem IgnoreClassDepL)), not (banned Inst)) 
   (
-    compile Inst IsLeaf TC-of-Inst Clause, 
+    compile Inst _IsLeaf TC-of-Inst Clause, 
     % TODO: a clause is flexible if an instance is polimorphic (pglobal)
     not (var Clause),
-    make-inst-graft Inst IsLeaf Graft,
+    Graft is after (int_to_string {get-inst-prio Inst}),
     get-full-path Inst ClauseName,
     if (is-local) (Visibility = [@local!])
       (if (has-context-deps Inst) 

apps/tc/src/coq_elpi_tc_hook.mlg

@@ -29,7 +29,7 @@ VERNAC COMMAND EXTEND ElpiTypeclasses CLASSIFIED AS SIDEFF
      let () = ignore_unknown_attributes atts in
      takeover_rm cs }
 
-| #[ atts = any_attribute ] [ "Elpi" "Override" "Register" qualified_name(p) ] -> {
+| #[ atts = any_attribute ] [ "Elpi" "Override" "TC_Register" qualified_name(p) ] -> {
      let () = ignore_unknown_attributes atts in
      register_observer (fst p, snd p, atts) }
 

apps/tc/tests/auto_compile.v

@@ -1,25 +1,6 @@
 From elpi.apps Require Import tc.
 
-From elpi.apps.tc Extra Dependency "base.elpi" as base.
-From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler.
-From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
-From elpi.apps.tc Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
-
-Elpi Command add_instance.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate Db tc.db.
-Elpi Accumulate File create_tc_predicate.
-Elpi Accumulate File compiler.
-Elpi Accumulate lp:{{
-  main [trm (global Inst), trm (global TC), str Locality, int Prio] :- 
-    add-inst Inst TC Locality Prio.
-
-  main [trm (global GR)] :- 
-    add-class-gr classic GR.
-}}.
-Elpi Typecheck.
-Elpi Override Register add_instance.
+Elpi Override TC_Register auto_compiler.
 Elpi Override TC TC_solver All.
 
 Require Import Bool.
@@ -36,7 +17,6 @@ Elpi Accumulate TC_solver lp:{{
   :after "firstHook"
   solve _ _ :- coq.say "Solving in ELPI!", fail.
 }}.
-Elpi Typecheck.
 
 Goal A (nat * (nat * bool)). apply _. Qed.
 

apps/tc/tests/importOrder/sameOrderCommand.v

@@ -1,32 +1,13 @@
-From elpi Require Export tc.
+From elpi.apps Require Export tc.
 
 From elpi.apps.tc Extra Dependency "base.elpi" as base.
-From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler.
-From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
-From elpi.apps.tc Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
-
-Elpi Command add_instance.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate Db tc.db.
-Elpi Accumulate File create_tc_predicate.
-Elpi Accumulate File compiler.
-Elpi Accumulate lp:{{
-  main [trm (global Inst), trm (global TC), str Locality, int Prio] :- 
-    add-inst Inst TC Locality Prio.
-
-  main [trm (global GR)] :- 
-    add-class-gr classic GR.
-}}.
-Elpi Typecheck.
-Elpi Override Register add_instance.
-Elpi Override TC TC_solver All.
-
-
 From elpi.apps.tc.tests.importOrder Extra Dependency "tc_same_order.elpi" as tc_same_order.
 
 Elpi Command SameOrderImport.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate File base.
 Elpi Accumulate File tc_same_order.
 Elpi Typecheck.
+
+Elpi Override TC_Register auto_compiler.
+Elpi Override TC TC_solver All.

apps/tc/theories/tc.v

@@ -210,3 +210,18 @@ Elpi Export MySectionEnd.
 
 Elpi AddAllClasses.
 Elpi AddAllInstances.
+
+Elpi Command auto_compiler.
+Elpi Accumulate File base.
+Elpi Accumulate File tc_aux.
+Elpi Accumulate Db tc.db.
+Elpi Accumulate File create_tc_predicate.
+Elpi Accumulate File compiler.
+Elpi Accumulate lp:{{
+  main [trm (global Inst), trm (global TC), str Locality, int Prio] :- 
+    add-inst Inst TC Locality Prio.
+
+  main [trm (global GR)] :- 
+    add-class-gr classic GR.
+}}.
+Elpi Typecheck.