Merge pull request #522 from FissoreD/origin/master-tc

TC solver 1

.gitignore

@@ -46,4 +46,5 @@ META
 *.cache
 
 apps/coercion/src/coq_elpi_coercion_hook.ml
-.filestoinstall
+.filestoinstall
+apps/tc/src/coq_elpi_tc_hook.ml

apps/tc/_CoqProject

@@ -5,7 +5,9 @@
 
 -R theories   elpi.apps
 -R elpi       elpi.apps.tc
+-R tests    elpi.apps.tc.tests
 
+src/coq_elpi_tc_register.ml
 src/coq_elpi_tc_hook.mlg
 src/coq_elpi_class_tactics_hacked.ml
 src/elpi_tc_plugin.mlpack

apps/tc/_CoqProject.test

@@ -7,6 +7,8 @@
 -R tests    elpi.apps.tc.tests
 -I src
 
+tests/auto_compile.v
+
 tests/premisesSort/sortCode.v
 tests/premisesSort/sort1.v
 # tests/premisesSort/sort2.v
@@ -20,16 +22,15 @@ tests/importOrder/sameOrderCommand.v
 tests/importOrder/f1.v
 tests/importOrder/f2a.v
 tests/importOrder/f2b.v
-# tests/importOrder/f3a.v
-# tests/importOrder/f3b.v
-# tests/importOrder/f3c.v
-# tests/importOrder/f3d.v
-# tests/importOrder/f3e.v
-# tests/importOrder/f3f.v
-# tests/importOrder/f3g.v
+tests/importOrder/f3a.v
+tests/importOrder/f3b.v
+tests/importOrder/f3c.v
+tests/importOrder/f3d.v
+tests/importOrder/f3e.v
+tests/importOrder/f3f.v
+tests/importOrder/f3g.v
 
 tests/nobacktrack.v
-tests/removeEta.v
 tests/patternFragment.v
 tests/contextDeepHierarchy.v
 tests/mode_no_repetion.v

apps/tc/elpi/compiler.elpi

@@ -145,18 +145,32 @@ has-context-deps GR :-
   coq.env.dependencies GR _ Deps, 
   std.exists SectionVars (x\ coq.gref.set.mem (const x) Deps).
 
-% [add-inst->db IgnoreClassDepL Inst] add the Inst to
-% the database except those depending on at least one 
-% inside IgnoreClassDepL
 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 [_ | _].
+get-locality "Global" [@global!].
+get-locality "Export" [].
 
+pred add-inst i:gref, i:gref, i:string, i:int.
+add-inst Inst TC Locality Prio :-
+  coq.env.current-section-path SectionPath,
+  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),
+  Graft is after (int_to_string Prio1),
+  get-full-path Inst ClauseName,
+  get-locality Locality LocalityProp,
+  LocalityProp => (add-tc-db ClauseName Graft Clause, add-tc-db _ Graft (instance SectionPath Inst TC)).
+add-inst Inst _ _ _ :- 
+  coq.warning "Not-added" "TC_solver" "Warning : Cannot compile " Inst "since it is pglobal".
+
+% [add-inst->db IgnoreClassDepL ForceAdd Inst] add the Inst to
+% the database except those depending on at least one 
+% inside IgnoreClassDepL
 pred add-inst->db i:list gref, i:bool, i:gref.
 :name "add-inst->db:start"
 add-inst->db IgnoreClassDepL ForceAdd Inst :-
@@ -166,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/elpi/solver.elpi

@@ -25,7 +25,7 @@ build-context-clauses Ctx Clauses :-
 
 pred tc i:term, o:term.
 tc Ty Sol :- 
-  Ty = app [global TC | TL'],
+  coq.safe-dest-app Ty (global TC) TL',
   std.append TL' [Sol] TL,
   % replace-with-alias T T' A, !, 
   % A = tt, tc Gref T' Sol.

apps/tc/elpi/tc_aux.elpi

@@ -97,7 +97,7 @@ no-backtrack [X | XS] [std.do! [X | XS']] :- !, no-backtrack XS XS'.
 
 pred make-tc i:prop, i:term, i:term, i:list prop, o:prop.
 make-tc _IsHead Ty Inst Hyp Clause :-
-  app [global TC | TL] = Ty,
+  coq.safe-dest-app Ty (global TC) TL,
   gref->string-no-path TC TC_Str,
   std.append TL [Inst] Args, 
   coq.elpi.predicate TC_Str Args Q,
@@ -106,22 +106,15 @@ make-tc _IsHead Ty Inst Hyp Clause :-
       (Hyp = [Hd]) (Clause = (Q :- Hd)) 
       (Clause = (Q :- Hyp)).
 
-
-pred get-inst-prio-coq i:term, i:list term, o:int.
-get-inst-prio-coq (prod _ _ A) L Prio :-
-  pi x\ get-inst-prio-coq (A x) [x | L] Prio.
-get-inst-prio-coq (app _ as App) L Prio :-
-  std.fold L 0 (T\acc\r\ if (not(occurs T App)) (r is acc + 1) (r = acc)) Prio.
-get-inst-prio-coq A _ _ :- coq.error "Invalid case for" A.
-
 % returns the priority of an instance from the gref of an instance
 pred get-inst-prio i:gref, o:int.
 get-inst-prio InstGr Prio :-
   coq.env.typeof InstGr InstTy,
   get-TC-of-inst-type InstTy TC,
   find-opt {coq.TC.db-for TC} 
-    (x\ tc-instance InstGr Prio' = x) (some _), !,
-  if (Prio' = 0) (get-inst-prio-coq InstTy [] Prio) (Prio = Prio').
+    (x\ tc-instance InstGr (tc-priority-given Prio) = x ;
+        tc-instance InstGr (tc-priority-computed Prio) = x)
+      (some _), !.
 get-inst-prio _ 0.
 
 % TODO: @FissoreD improve this method complexity

apps/tc/src/coq_elpi_class_tactics_hacked.ml

@@ -27,14 +27,6 @@ open Elpi
 open Elpi_plugin
 open Coq_elpi_utils
 
-let handle_event = function
- | Classes.Event.NewClass _ -> assert false
- | Classes.Event.NewInstance _ -> assert false
-
-let this_observer =
-  Classes.register_observer ~name:"elpi.tc" handle_event
-
-
 module NamedDecl = Context.Named.Declaration
 
 (** Hint database named "typeclass_instances", created in prelude *)
@@ -1181,7 +1173,6 @@ let elpi_solver = Summary.ref ~name:"tc_takeover" None
 
 let takeover action =
   let open Names.GlobRef in
-  Classes.activate_observer this_observer;
   match !elpi_solver, action with
   | _, Set(solver,mode) ->
     elpi_solver := Some (mode,solver)

apps/tc/src/coq_elpi_tc_hook.mlg

@@ -4,6 +4,7 @@ DECLARE PLUGIN "coq-elpi-tc.plugin"
 open Stdarg
 open Elpi_plugin
 open Coq_elpi_arg_syntax
+open Coq_elpi_tc_register
 open Coq_elpi_class_tactics_hacked
 
 }
@@ -28,4 +29,8 @@ VERNAC COMMAND EXTEND ElpiTypeclasses CLASSIFIED AS SIDEFF
      let () = ignore_unknown_attributes atts in
      takeover_rm cs }
 
+| #[ atts = any_attribute ] [ "Elpi" "Override" "TC_Register" qualified_name(p) ] -> {
+     let () = ignore_unknown_attributes atts in
+     register_observer (fst p, snd p, atts) }
+
 END

apps/tc/src/coq_elpi_tc_register.ml

@@ -0,0 +1,70 @@
+open Elpi_plugin
+open Classes
+open Coq_elpi_arg_HOAS
+
+type qualified_name = Coq_elpi_utils.qualified_name
+
+type loc_name_atts = (Loc.t * qualified_name * Attributes.vernac_flags)
+
+let gref2elpi_term (gref: Names.GlobRef.t) : Cmd.raw = 
+  let gref_2_string gref = Pp.string_of_ppcmds (Names.GlobRef.print gref) in
+  let normalize_string s = 
+    String.split_on_char '.' s |> List.rev |> List.hd |>
+    String.split_on_char ',' |> List.hd  in
+  Cmd.Term (CAst.make @@ Constrexpr.CRef(
+    Libnames.qualid_of_string @@ normalize_string @@ gref_2_string gref,None))
+
+let observer_class (x : Typeclasses.typeclass) : Coq_elpi_arg_HOAS.Cmd.raw list = 
+  [gref2elpi_term x.cl_impl]
+
+(* 
+  The elpi arguments passed to the elpi program are [Inst, TC, Locality, Prio] where: 
+  - Inst     : is the elpi Term for the current instance 
+  - TC       : is the elpi Term for the type classes implemented by Inst
+  - Locality : is the elpi String [Local|Global] depending on the locality of Inst 
+  - Prio     : is the elpi Int X representing the priority of the instance
+               in particular if the priority is defined by the user, X is that priority
+               otherwise, X is -1
+*)
+let observer_instance ({locality; instance; info; class_name} : instance) : Coq_elpi_arg_HOAS.Cmd.raw list = 
+  let locality2elpi_string loc = 
+    let hint2string = function 
+    | Hints.Local -> "Local"
+    | Export -> "Export"
+    | SuperGlobal -> "Global" in
+    Cmd.String (hint2string loc) in 
+  let prio2elpi_int (prio: Typeclasses.hint_info) = 
+    Cmd.Int (Option.default (-1) prio.hint_priority) in 
+  [
+    gref2elpi_term instance; 
+    gref2elpi_term class_name;
+    locality2elpi_string locality;
+    prio2elpi_int info
+  ]
+
+let inObservation =
+  Libobject.declare_object @@
+    Libobject.local_object "TC_HACK_OBSERVER2"
+      ~cache:(fun (run,inst) -> run @@ observer_instance inst)
+      ~discharge:(fun (_,inst as x) -> if inst.locality = Hints.Local then None else Some x)
+
+let observer_evt ((loc, name, atts) : loc_name_atts) (x : Event.t) = 
+  let open Coq_elpi_vernacular in
+  let run_program e = run_program loc name ~atts e in 
+  match x with  
+  | Event.NewClass cl -> run_program @@ observer_class cl
+  | Event.NewInstance inst -> Lib.add_leaf (inObservation (run_program,inst))
+
+let inTakeover =
+  let cache (loc, name, atts) = 
+    let observer1 = Classes.register_observer 
+                    ~name:(String.concat "." name) 
+                    (observer_evt (loc, name, atts))
+    in
+    Classes.activate_observer observer1
+  in
+  Libobject.(declare_object 
+    (superglobal_object_nodischarge "TC_HACK_OBSERVER" ~cache ~subst:None))
+
+let register_observer (x : loc_name_atts) = 
+  Lib.add_leaf (inTakeover x)

apps/tc/src/elpi_tc_plugin.mlpack

@@ -1,2 +1,3 @@
+Coq_elpi_tc_register
 Coq_elpi_class_tactics_hacked
 Coq_elpi_tc_hook