Merge pull request #540 from FissoreD/class-declare-TC-command

Locality can be charged to coq.elpi.add-predicate

Author: gares

Changelog.md

@@ -1,5 +1,20 @@
 # Changelog
 
+## Unreleased - 09/11/2023
+
+### API
+- Change `coq.elpi.add-predicate` now locality can be changed
+- Experimental `coq.toposort` returns a valid topological ordering of the nodes 
+  of a graph
+- Change `coq.TC.db-for`, now instances are returned sorted wrt their priority
+- New `tc-priority`, contains the priority of an instance and if the priority
+  has been given by the user or computed by `coq`
+- Change `tc-instance`, now the type is `gref -> tc-priority -> tc-instance` i.e. the priority is not an integer anymore
+
+### Apps 
+- New `tc` app providing an implementation of a type class solver written in elpi.
+  This app is experimental
+
 ## [1.19.3] - 12/10/2023
 
 Requires Elpi 1.16.5 and Coq 8.18.

apps/tc/elpi/create_tc_predicate.elpi

@@ -25,15 +25,21 @@ modes-of-class ClassGr Modes :-
   N is {coq.count-prods ClassTy} + 1, % + 1 for the solution
   list-init N (x\r\ r = (pr out "term")) Modes.
 
+pred get-class-locality o:list prop. 
+get-class-locality [@local!] :- coq.env.current-section-path [_ | _], !.
+get-class-locality [@global!].
+
 pred add-class-gr i:search-mode, i:gref.
 add-class-gr SearchMode ClassGR :-
   std.assert! (coq.TC.class? ClassGR) "Only gref of type classes can be added as new predicates",
   if (class ClassGR _ _) true 
     (modes-of-class ClassGR Modes, 
       gref->pred-name ClassGR PredName,
-      coq.elpi.add-predicate "tc.db" _ PredName Modes,
-      add-tc-db _ _ (tc-mode ClassGR Modes),
-      @global! => add-tc-db _ _ (class ClassGR PredName SearchMode)).
+      get-class-locality Locality, 
+      Locality => (
+        add-tc-db _ _ (tc-mode ClassGR Modes),
+        coq.elpi.add-predicate "tc.db" _ PredName Modes,
+        add-tc-db _ _ (class ClassGR PredName SearchMode))).
 
 pred add-class-str i:search-mode, i:string.
 add-class-str SearchMode ClassStr :-
@@ -42,9 +48,9 @@ add-class-str SearchMode ClassStr :-
 
 % Following are predicates for TC.declare
 
-pred attr->deterministic o:search-mode. 
-attr->deterministic deterministic :- get-option "deterministic" tt, !.
-attr->deterministic classic.
+pred attr->search-mode o:search-mode. 
+attr->search-mode deterministic :- get-option "deterministic" tt, !.
+attr->search-mode classic.
 
 pred attr->modes o:list hint-mode.
 attr->modes CoqModes :- 
@@ -63,14 +69,15 @@ pred declare-class-in-coq i:gref.
 declare-class-in-coq ClassGR :- 
   attr->modes CoqModes,
   if (CoqModes = []) true 
-    (@global! => coq.hints.add-mode ClassGR "typeclass_instances" CoqModes),
+    (coq.hints.add-mode ClassGR "typeclass_instances" CoqModes),
   % CAVEAT: this triggers the observer
   coq.TC.declare-class ClassGR,
-  attr->deterministic SearchMode, 
+  attr->search-mode SearchMode, 
   gref->pred-name ClassGR PredName,
   % HACK: we override the clauses added by the observer, since it does not know
   % the SearchMode.
-  @global! => add-tc-db _ (after "0") (class ClassGR PredName SearchMode :- !).
+  get-class-locality Locality, 
+  Locality => add-tc-db _ (after "0") (class ClassGR PredName SearchMode :- !).
 
 pred declare-class i:indt-decl. 
 declare-class D :- !, 

apps/tc/src/coq_elpi_tc_register.ml

@@ -51,16 +51,22 @@ let observer_instance ({locality; instance; info; class_name} : instance) : Coq_
 
 let inObservation =
   Libobject.declare_object @@
-    Libobject.local_object "TC_HACK_OBSERVER2"
+    Libobject.local_object "TC_HACK_OBSERVER_CLASSES"
+      ~cache:(fun (run,cl) -> run @@ observer_class cl)
+      ~discharge:(fun x -> Some x)
+
+let inObservation1 =
+  Libobject.declare_object @@
+    Libobject.local_object "TC_HACK_OBSERVER_INSTANCE"
       ~cache:(fun (run,inst) -> run @@ observer_instance inst)
       ~discharge:(fun (_,inst as x) -> if inst.locality = 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))
+  | Event.NewClass cl -> Lib.add_leaf (inObservation (run_program,cl)) 
+  | Event.NewInstance inst -> Lib.add_leaf (inObservation1 (run_program,inst))
 
 module StringMap = Map.Make(String)
 

apps/tc/tests/section_in_out.v

@@ -52,5 +52,12 @@ End A.
 
 Elpi len_test 4.
 
-
-
+Section ClassPersistence.
+  Section S1.
+    Context (X : Type) (A : X).
+    Class class (A : X).
+    Definition x : class A. apply Build_class. Qed.
+    Elpi TC.AddInstances x.
+    Goal exists x, class x. eexists. apply _. Qed.
+  End S1.
+End ClassPersistence.

coq-builtin.elpi

@@ -1739,10 +1739,13 @@ type in argument_mode.
 type out argument_mode.
 
 % [coq.elpi.add-predicate Db Indexing PredName Spec] Declares a new
-% predicate PredName in the data base Db. Indexing can be left unspecified.
-% Spec gathers a mode and a type for each argument. CAVEAT: types and
-% indexing are strings instead of proper data types; beware parsing errors
-% are fatal
+% predicate PredName in the data base Db.
+% Indexing can be left unspecified. Spec gathers a mode and a
+% type for each argument. CAVEAT: types and indexing are strings
+% instead of proper data types; beware parsing errors are fatal.
+% Supported attributes:
+% - @local! (default: false, discard at the end of section or module)
+% - @global! (default: false, always active
 external pred coq.elpi.add-predicate i:string, i:string, i:string, 
                                      i:list (pair argument_mode string).
 

src/coq_elpi_builtins.ml

@@ -604,7 +604,7 @@ let argument_mode = let open Conv in let open API.AlgebraicData in declare {
 
 
 let set_accumulate_text_to_db, get_accumulate_text_to_db =
-  let f = ref (fun _ _ -> assert false) in
+  let f = ref (fun _ _ _ -> assert false) in
   (fun x -> f := x),
   (fun () -> !f)
 
@@ -4084,10 +4084,19 @@ Supported attributes:
     In(B.unspec B.string,"Indexing",
     In(B.string,"PredName",
     In(B.list (B.pair argument_mode B.string),"Spec",
-    Full(global,"Declares a new predicate PredName in the data base Db. Indexing can be left unspecified. Spec gathers a mode and a type for each argument. CAVEAT: types and indexing are strings instead of proper data types; beware parsing errors are fatal"))))),
-    (fun dbname indexing predname spec ~depth _ _ state ->
+    Full(global,{|Declares a new predicate PredName in the data base Db.
+Indexing can be left unspecified. Spec gathers a mode and a
+type for each argument. CAVEAT: types and indexing are strings
+instead of proper data types; beware parsing errors are fatal.
+Supported attributes:
+- @local! (default: false, discard at the end of section or module)
+- @global! (default: false, always active|}))))),
+    (fun dbname indexing predname spec ~depth ctx _ state ->
       let dbname = Coq_elpi_utils.string_split_on_char '.' dbname in
       let f = get_accumulate_text_to_db () in
+      let local = ctx.options.local = Some true in
+      let super_global = ctx.options.local = Some false in
+      if local && super_global then CErrors.user_err Pp.(str "coq.elpi.add-predicate: @global! incompatible with @local!");
       let indexing =
         match indexing with
         | B.Given str -> ":index ("^str^") "
@@ -4100,7 +4109,8 @@ Supported attributes:
         mode ^ "(" ^ ty ^ ")") in
       let spec = String.concat ", " spec in
       let text = indexing ^ "pred " ^ predname ^ " " ^ spec ^ "." in
-      f dbname text;
+      let scope = if local then Local else if super_global then SuperGlobal else Regular in 
+      f dbname text scope;
       state, (), []
       )),
   DocAbove);

src/coq_elpi_builtins.mli

@@ -13,7 +13,7 @@ val clauses_for_later :
   (qualified_name * Ast.program * Names.Id.t list * Coq_elpi_utils.clause_scope) list State.component
 val set_accumulate_to_db :
   (((qualified_name * Ast.program * Names.Id.t list * Coq_elpi_utils.clause_scope) list -> unit)) -> unit
-val set_accumulate_text_to_db : ((string list -> string -> unit)) -> unit
+val set_accumulate_text_to_db : ((string list -> string -> Coq_elpi_utils.clause_scope -> unit)) -> unit
 
 type attribute_data =
   | AttributeString of string

src/coq_elpi_programs.ml

@@ -629,8 +629,8 @@ let () = Coq_elpi_builtins.set_accumulate_to_db (fun clauses_to_add ->
   clauses_to_add |> List.iter (fun (dbname,units,vs,scope) ->
     accumulate_to_db dbname units vs ~scope))
 
-let () = Coq_elpi_builtins.set_accumulate_text_to_db (fun n txt ->
+let () = Coq_elpi_builtins.set_accumulate_text_to_db (fun n txt scope ->
   let elpi = ensure_initialized () in
   let loc = API.Ast.Loc.initial "(elpi.add_predicate)" in
   let u = unit_from_string ~elpi loc txt in
-  accumulate_to_db n [u] [] ~scope:Regular)
+  accumulate_to_db n [u] [] ~scope)