From 533ef5ae923a89bed4b5a1af4a5a039d9a35142e Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Sun, 15 Oct 2023 23:55:33 +0200 Subject: [PATCH 01/20] inst&classes auto inserted in db of elpi --- apps/tc/_CoqProject | 1 + apps/tc/_CoqProject.test | 2 + apps/tc/src/.gitignore | 1 + apps/tc/src/coq_elpi_class_tactics_hacked.ml | 9 ---- apps/tc/src/coq_elpi_tc_hook.ml | 30 +++++++++---- apps/tc/src/coq_elpi_tc_hook.mlg | 5 +++ apps/tc/src/coq_elpi_tc_register.ml | 29 +++++++++++++ apps/tc/src/elpi_tc_plugin.mlpack | 1 + apps/tc/tests/auto_compile.v | 44 ++++++++++++++++++++ 9 files changed, 105 insertions(+), 17 deletions(-) create mode 100644 apps/tc/src/.gitignore create mode 100644 apps/tc/src/coq_elpi_tc_register.ml create mode 100644 apps/tc/tests/auto_compile.v diff --git a/apps/tc/_CoqProject b/apps/tc/_CoqProject index 1e009a732..5d380e185 100644 --- a/apps/tc/_CoqProject +++ b/apps/tc/_CoqProject @@ -6,6 +6,7 @@ -R theories elpi.apps -R elpi elpi.apps.tc +src/coq_elpi_tc_register.ml src/coq_elpi_tc_hook.mlg src/coq_elpi_class_tactics_hacked.ml src/elpi_tc_plugin.mlpack diff --git a/apps/tc/_CoqProject.test b/apps/tc/_CoqProject.test index 5eab1487e..7d8dc9874 100644 --- a/apps/tc/_CoqProject.test +++ b/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 diff --git a/apps/tc/src/.gitignore b/apps/tc/src/.gitignore new file mode 100644 index 000000000..aa3ca7354 --- /dev/null +++ b/apps/tc/src/.gitignore @@ -0,0 +1 @@ +coq_elpi_tc_hook.ml \ No newline at end of file diff --git a/apps/tc/src/coq_elpi_class_tactics_hacked.ml b/apps/tc/src/coq_elpi_class_tactics_hacked.ml index ea19c0e63..a4b59f9b0 100644 --- a/apps/tc/src/coq_elpi_class_tactics_hacked.ml +++ b/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) diff --git a/apps/tc/src/coq_elpi_tc_hook.ml b/apps/tc/src/coq_elpi_tc_hook.ml index a4dc4187e..5459f7840 100644 --- a/apps/tc/src/coq_elpi_tc_hook.ml +++ b/apps/tc/src/coq_elpi_tc_hook.ml @@ -5,10 +5,9 @@ let _ = Mltop.add_known_module "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 -module M = Coq_elpi_vernacular - let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-elpi-tc.plugin") ~command:"ElpiTypeclasses" ~classifier:(fun _ -> Vernacextend.classify_as_sideeff) ?entry:None @@ -20,7 +19,7 @@ let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-elpi-tc.plugin") ~ Vernacextend.TyNil))))), (let coqpp_body p atts = Vernacextend.vtdefault (fun () -> -# 15 "src/coq_elpi_tc_hook.mlg" +# 14 "src/coq_elpi_tc_hook.mlg" let () = ignore_unknown_attributes atts in takeover false [] (snd p) @@ -34,7 +33,7 @@ let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-elpi-tc.plugin") ~ Vernacextend.TyNil))))), (let coqpp_body p atts = Vernacextend.vtdefault (fun () -> -# 18 "src/coq_elpi_tc_hook.mlg" +# 17 "src/coq_elpi_tc_hook.mlg" let () = ignore_unknown_attributes atts in takeover true [] (snd p) @@ -51,7 +50,7 @@ let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-elpi-tc.plugin") ~ Vernacextend.TyNil)))))), (let coqpp_body p cs atts = Vernacextend.vtdefault (fun () -> -# 23 "src/coq_elpi_tc_hook.mlg" +# 22 "src/coq_elpi_tc_hook.mlg" let () = ignore_unknown_attributes atts in takeover false cs (snd p) @@ -67,7 +66,7 @@ let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-elpi-tc.plugin") ~ Vernacextend.TyNil))))), (let coqpp_body cs atts = Vernacextend.vtdefault (fun () -> -# 26 "src/coq_elpi_tc_hook.mlg" +# 25 "src/coq_elpi_tc_hook.mlg" let () = ignore_unknown_attributes atts in takeover_add cs @@ -83,11 +82,26 @@ let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-elpi-tc.plugin") ~ Vernacextend.TyNil))))), (let coqpp_body cs atts = Vernacextend.vtdefault (fun () -> -# 29 "src/coq_elpi_tc_hook.mlg" +# 28 "src/coq_elpi_tc_hook.mlg" let () = ignore_unknown_attributes atts in takeover_rm cs ) in fun cs ?loc ~atts () -> coqpp_body cs - (Attributes.parse any_attribute atts)), None))] + (Attributes.parse any_attribute atts)), None)); + (Vernacextend.TyML (false, Vernacextend.TyTerminal ("Elpi", + Vernacextend.TyTerminal ("Override", + Vernacextend.TyTerminal ("Register", + Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_qualified_name), + Vernacextend.TyNil)))), (let coqpp_body p + atts = Vernacextend.vtdefault (fun () -> + +# 32 "src/coq_elpi_tc_hook.mlg" + + let () = ignore_unknown_attributes atts in + register_observer (fst p, snd p, atts) + ) in fun p + ?loc ~atts () + -> coqpp_body p + (Attributes.parse any_attribute atts)), None))] diff --git a/apps/tc/src/coq_elpi_tc_hook.mlg b/apps/tc/src/coq_elpi_tc_hook.mlg index 09ec0faae..23c145756 100644 --- a/apps/tc/src/coq_elpi_tc_hook.mlg +++ b/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" "Register" qualified_name(p) ] -> { + let () = ignore_unknown_attributes atts in + register_observer (fst p, snd p, atts) } + END \ No newline at end of file diff --git a/apps/tc/src/coq_elpi_tc_register.ml b/apps/tc/src/coq_elpi_tc_register.ml new file mode 100644 index 000000000..020314f3e --- /dev/null +++ b/apps/tc/src/coq_elpi_tc_register.ml @@ -0,0 +1,29 @@ +open Elpi_plugin + +type qualified_name = Coq_elpi_utils.qualified_name + +type solver = (Loc.t * qualified_name * Attributes.vernac_flags) +let solvers : solver list ref = ref [] + +let observer (x : Classes.Event.t) ((loc, name, atts) : solver) = + let open Coq_elpi_vernacular in + let open Coq_elpi_arg_HOAS in + let run_program e = run_program loc name ~atts [e] in + let gref_2_string gref = Pp.string_of_ppcmds (Names.GlobRef.print gref) in + let normalize_string s = + let s = List.hd (String.split_on_char ',' s) in + let s = if String.starts_with ~prefix:"(" s then + String.sub s 1 (String.length s - 1) else s in + Cmd.String s in + let add_aux gref = run_program (normalize_string (gref_2_string gref)) in + add_aux @@ match x with + | Classes.Event.NewClass x -> x.cl_impl + | Classes.Event.NewInstance x -> x.instance + +let observer (x : Classes.Event.t) = + List.iter (observer x) !solvers + +let register_observer (loc, name, atts : solver) = + solvers := (loc, name, atts) :: !solvers; + let observer = Classes.register_observer ~name:(String.concat "." name) observer in + Classes.activate_observer observer \ No newline at end of file diff --git a/apps/tc/src/elpi_tc_plugin.mlpack b/apps/tc/src/elpi_tc_plugin.mlpack index 8aed0b167..1e62bcd54 100644 --- a/apps/tc/src/elpi_tc_plugin.mlpack +++ b/apps/tc/src/elpi_tc_plugin.mlpack @@ -1,2 +1,3 @@ +Coq_elpi_tc_register Coq_elpi_class_tactics_hacked Coq_elpi_tc_hook \ No newline at end of file diff --git a/apps/tc/tests/auto_compile.v b/apps/tc/tests/auto_compile.v new file mode 100644 index 000000000..a5a9da06a --- /dev/null +++ b/apps/tc/tests/auto_compile.v @@ -0,0 +1,44 @@ +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 [str A] :- + coq.locate A GR, + coq.say {attributes}, + coq.say "Adding :" GR, + if (coq.TC.class? GR) (add-class-gr classic GR) + (add-inst->db [] ff GR). +}}. +Elpi Typecheck. +Elpi Override Register add_instance. +Elpi Override TC TC_solver All. + +Require Import Bool. + +(* TODO: How to add the #[deterministic] pragma in front of the class? *) +(* #[deterministic] Class A (T : Type) := {succ : T -> T}. *) +Class A (T : Type) := {succ : T -> T}. +#[local] Instance B : A nat := {succ n := S n}. +Instance C : A bool := {succ b := negb b}. +Instance Prod (X Y: Type) `(A X, A Y) : A (X * Y) := + {succ b := match b with (a, b) => (succ a, succ b) end}. + +Elpi Accumulate TC_solver lp:{{ + :after "firstHook" + solve _ _ :- coq.say "Solving in ELPI!", fail. +}}. +Elpi Typecheck. + +Goal A (nat * (nat * bool)). apply _. Qed. + + From 657ddf51261e2f4ab29e16151cc0e93066c13302 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Mon, 16 Oct 2023 17:56:17 +0200 Subject: [PATCH 02/20] move comment --- apps/tc/elpi/compiler.elpi | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi index 5302000a2..ceae7e129 100644 --- a/apps/tc/elpi/compiler.elpi +++ b/apps/tc/elpi/compiler.elpi @@ -145,9 +145,6 @@ 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" _). @@ -157,6 +154,9 @@ make-inst-graft Inst _NoPremises (after Grafting) :- % if (NoPremises = tt) (Grafting = RawGrafting) (Grafting is RawGrafting ^ "_complex"). Grafting = RawGrafting. +% [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 :- From 3b11dfbd729ace42be492ce00fe9091211787337 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Tue, 17 Oct 2023 17:36:56 +0200 Subject: [PATCH 03/20] Update get_instances order --- coq-builtin.elpi | 3 +++ src/coq_elpi_builtins.ml | 31 ++++++++++++++++++++++++++++++- 2 files changed, 33 insertions(+), 1 deletion(-) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index fa4f798d4..b581dc22d 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -1144,6 +1144,9 @@ external pred coq.TC.db-tc o:list gref. % [coq.TC.db-for GR Db] reads all instances of the given class GR external pred coq.TC.db-for i:gref, o:list tc-instance. +% [coq.TC.db-for2 GR List Db] reads all instances of the given class GR +external pred coq.TC.db-for2 i:gref, o:list gref. + % [coq.TC.class? GR] checks if GR is a class external pred coq.TC.class? i:gref. diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index ebb75198c..ec28f0cf1 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -1234,7 +1234,29 @@ let eta_contract env sigma t = (*Printf.eprintf "------------- %s\n" Pp.(string_of_ppcmds @@ Printer.pr_econstr_env env sigma t);*) map env t - +let get_instances tc = + let hint_db = Hints.searchtable_map "typeclass_instances" in + let secvars : Names.Id.Pred.t = Names.Id.Pred.full in + let full_hints = Hints.Hint_db.map_all ~secvars:secvars tc hint_db in + let hint_asts = List.map Hints.FullHint.repr full_hints in + let hints = List.filter_map (function + | Hints.Res_pf a -> Some a + | ERes_pf a -> Some a + | Extern (a, b) -> None + | Give_exact a -> Some a + | Res_pf_THEN_trivial_fail e -> Some e + | Unfold_nth e -> None) hint_asts in + let sigma, _ = + let env = Global.env () in Evd.(from_env env, env) in + let constrs = List.map (fun a -> Hints.hint_as_term a |> snd) hints in + (* Printer.pr_global tc |> Pp.string_of_ppcmds |> Printf.printf "%s\n"; *) + let instances_grefs = List.filter_map (fun e -> + match EConstr.kind sigma e with + | Constr.Ind (a, _) -> Some (Names.GlobRef.IndRef a) + | Constr.Const (a, _) -> Some (Names.GlobRef.ConstRef a) + | Constr.Construct (a, _) -> Some (Names.GlobRef.ConstructRef a) + | _ -> None) constrs in + instances_grefs (*****************************************************************************) @@ -2727,6 +2749,13 @@ Supported attributes: !: (Typeclasses.instances_exn env (get_sigma state) gr))), DocAbove); + MLCode(Pred("coq.TC.db-for2", + In(gref, "GR", + Out(B.list gref, "List Db", + Easy {|reads all instances of the given class GR|})), + (fun s _ ~depth:_ -> !: (get_instances s))), + DocAbove); + MLCode(Pred("coq.TC.class?", In(gref, "GR", Easy "checks if GR is a class"), From 22a6c2d4b6dcf56f1014dbfadc70ecdd1da8adc7 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Tue, 17 Oct 2023 17:37:27 +0200 Subject: [PATCH 04/20] Persistent register --- apps/tc/src/coq_elpi_tc_register.ml | 56 +++++++++++++++++++++-------- apps/tc/tests/auto_compile.v | 2 +- apps/tc/theories/tc.v | 13 +++---- 3 files changed, 50 insertions(+), 21 deletions(-) diff --git a/apps/tc/src/coq_elpi_tc_register.ml b/apps/tc/src/coq_elpi_tc_register.ml index 020314f3e..404c59f5d 100644 --- a/apps/tc/src/coq_elpi_tc_register.ml +++ b/apps/tc/src/coq_elpi_tc_register.ml @@ -1,29 +1,57 @@ open Elpi_plugin +open Classes type qualified_name = Coq_elpi_utils.qualified_name -type solver = (Loc.t * qualified_name * Attributes.vernac_flags) -let solvers : solver list ref = ref [] +type loc_name_atts = (Loc.t * qualified_name * Attributes.vernac_flags) -let observer (x : Classes.Event.t) ((loc, name, atts) : solver) = +let observer_evt ((loc, name, atts) : loc_name_atts) (x : Event.t) = let open Coq_elpi_vernacular in let open Coq_elpi_arg_HOAS in let run_program e = run_program loc name ~atts [e] in let gref_2_string gref = Pp.string_of_ppcmds (Names.GlobRef.print gref) in let normalize_string s = - let s = List.hd (String.split_on_char ',' s) in - let s = if String.starts_with ~prefix:"(" s then - String.sub s 1 (String.length s - 1) else s in + Printf.printf "Adding : %s\n" s; + let s = String.split_on_char '.' s |> List.rev |> List.hd in + let s = String.split_on_char ',' s |> List.hd in Cmd.String s in let add_aux gref = run_program (normalize_string (gref_2_string gref)) in add_aux @@ match x with - | Classes.Event.NewClass x -> x.cl_impl - | Classes.Event.NewInstance x -> x.instance + | Event.NewClass x -> x.cl_impl + | Event.NewInstance x -> x.instance -let observer (x : Classes.Event.t) = - List.iter (observer x) !solvers +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 (loc, name, atts : solver) = - solvers := (loc, name, atts) :: !solvers; - let observer = Classes.register_observer ~name:(String.concat "." name) observer in - Classes.activate_observer observer \ No newline at end of file +let register_observer (x : loc_name_atts) = + Lib.add_leaf (inTakeover x) + +(* type hint_term = + | IsGlobRef of Names.GlobRef.t + | IsConstr of Constr.t * Univ.ContextSet.t option (* None if monomorphic *) + +let hack : Hints.hint_term -> hint_term = fun x -> + ( + assert (Coq_config.version = "8.18.0"); + Obj.magic x + ) *) + + (* EConstr.kind x + | Constr.Constant + | Constr.Contructor + | Constr.Inductive + | Constr..... *) + +(* let _ = + let sigma, env = + let env = Global.env () in Evd.(from_env env, env) in + Hints.pr_hint_db_by_name env sigma "typeclass_instances" |> ignore; + Printer.pr_constr_env env sigma |> ignore *) \ No newline at end of file diff --git a/apps/tc/tests/auto_compile.v b/apps/tc/tests/auto_compile.v index a5a9da06a..cae9eace4 100644 --- a/apps/tc/tests/auto_compile.v +++ b/apps/tc/tests/auto_compile.v @@ -14,7 +14,7 @@ Elpi Accumulate File compiler. Elpi Accumulate lp:{{ main [str A] :- coq.locate A GR, - coq.say {attributes}, + % coq.say {attributes}, coq.say "Adding :" GR, if (coq.TC.class? GR) (add-class-gr classic GR) (add-inst->db [] ff GR). diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v index 157eb4f91..be43387ac 100644 --- a/apps/tc/theories/tc.v +++ b/apps/tc/theories/tc.v @@ -61,22 +61,23 @@ Elpi Accumulate lp:{{ Elpi Command MySectionEnd. Elpi Accumulate Db tc.db. -Elpi Accumulate File tc_aux. Elpi Accumulate File base. +Elpi Accumulate File tc_aux. Elpi Accumulate File modes. Elpi Accumulate File compiler. Elpi Accumulate lp:{{ main _ :- - instances-of-current-section InstsFiltered, - coq.env.end-section, - std.forall {std.rev InstsFiltered} (add-inst->db [] tt). + % true. + % instances-of-current-section InstsFiltered, + coq.env.end-section. + % std.forall {std.rev InstsFiltered} (add-inst->db [] tt). }}. (* Elpi Typecheck. *) Elpi Command AddAllInstances. Elpi Accumulate Db tc.db. -Elpi Accumulate File tc_aux. Elpi Accumulate File base. +Elpi Accumulate File tc_aux. Elpi Accumulate File modes. Elpi Accumulate File compiler. Elpi Accumulate lp:{{ @@ -156,8 +157,8 @@ Elpi Accumulate lp:{{ Elpi Tactic TC_solver. Elpi Accumulate Db tc.db. -Elpi Accumulate File rforward. Elpi Accumulate File base. +Elpi Accumulate File rforward. Elpi Accumulate File tc_aux. Elpi Accumulate File modes. Elpi Accumulate File alias. From 9873ccb55d5ba298ceac0cfec4c99e7f4f948e16 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 22 Oct 2023 16:03:08 +0100 Subject: [PATCH 05/20] rm generated file --- apps/tc/src/.gitignore | 1 - apps/tc/src/coq_elpi_tc_hook.ml | 107 -------------------------------- 2 files changed, 108 deletions(-) delete mode 100644 apps/tc/src/.gitignore delete mode 100644 apps/tc/src/coq_elpi_tc_hook.ml diff --git a/apps/tc/src/.gitignore b/apps/tc/src/.gitignore deleted file mode 100644 index aa3ca7354..000000000 --- a/apps/tc/src/.gitignore +++ /dev/null @@ -1 +0,0 @@ -coq_elpi_tc_hook.ml \ No newline at end of file diff --git a/apps/tc/src/coq_elpi_tc_hook.ml b/apps/tc/src/coq_elpi_tc_hook.ml deleted file mode 100644 index 5459f7840..000000000 --- a/apps/tc/src/coq_elpi_tc_hook.ml +++ /dev/null @@ -1,107 +0,0 @@ -let _ = Mltop.add_known_module "coq-elpi-tc.plugin" - -# 3 "src/coq_elpi_tc_hook.mlg" - -open Stdarg -open Elpi_plugin -open Coq_elpi_arg_syntax -open Coq_elpi_tc_register -open Coq_elpi_class_tactics_hacked - - - -let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-elpi-tc.plugin") ~command:"ElpiTypeclasses" ~classifier:(fun _ -> Vernacextend.classify_as_sideeff) ?entry:None - [(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Elpi", - Vernacextend.TyTerminal ("Override", - Vernacextend.TyTerminal ("TC", Vernacextend.TyNonTerminal ( - Extend.TUentry (Genarg.get_arg_tag wit_qualified_name), - Vernacextend.TyTerminal ("All", - Vernacextend.TyNil))))), - (let coqpp_body p - atts = Vernacextend.vtdefault (fun () -> -# 14 "src/coq_elpi_tc_hook.mlg" - - let () = ignore_unknown_attributes atts in - takeover false [] (snd p) - ) in fun p - ?loc ~atts () -> coqpp_body p (Attributes.parse any_attribute atts)), None)); - (Vernacextend.TyML (false, Vernacextend.TyTerminal ("Elpi", - Vernacextend.TyTerminal ("Override", - Vernacextend.TyTerminal ("TC", Vernacextend.TyNonTerminal ( - Extend.TUentry (Genarg.get_arg_tag wit_qualified_name), - Vernacextend.TyTerminal ("None", - Vernacextend.TyNil))))), - (let coqpp_body p - atts = Vernacextend.vtdefault (fun () -> -# 17 "src/coq_elpi_tc_hook.mlg" - - let () = ignore_unknown_attributes atts in - takeover true [] (snd p) - ) in fun p - ?loc ~atts () -> coqpp_body p (Attributes.parse any_attribute atts)), None)); - (Vernacextend.TyML (false, Vernacextend.TyTerminal ("Elpi", - Vernacextend.TyTerminal ("Override", - Vernacextend.TyTerminal ("TC", Vernacextend.TyNonTerminal ( - Extend.TUentry (Genarg.get_arg_tag wit_qualified_name), - Vernacextend.TyTerminal ("Only", - Vernacextend.TyNonTerminal ( - Extend.TUlist1 ( - Extend.TUentry (Genarg.get_arg_tag wit_reference)), - Vernacextend.TyNil)))))), - (let coqpp_body p cs - atts = Vernacextend.vtdefault (fun () -> -# 22 "src/coq_elpi_tc_hook.mlg" - - let () = ignore_unknown_attributes atts in - takeover false cs (snd p) - ) in fun p - cs ?loc ~atts () -> coqpp_body p cs - (Attributes.parse any_attribute atts)), None)); - (Vernacextend.TyML (false, Vernacextend.TyTerminal ("Elpi", - Vernacextend.TyTerminal ("Override", - Vernacextend.TyTerminal ("TC", Vernacextend.TyTerminal ("+", - Vernacextend.TyNonTerminal ( - Extend.TUlist0 ( - Extend.TUentry (Genarg.get_arg_tag wit_reference)), - Vernacextend.TyNil))))), - (let coqpp_body cs - atts = Vernacextend.vtdefault (fun () -> -# 25 "src/coq_elpi_tc_hook.mlg" - - let () = ignore_unknown_attributes atts in - takeover_add cs - ) in fun cs - ?loc ~atts () -> coqpp_body cs - (Attributes.parse any_attribute atts)), None)); - (Vernacextend.TyML (false, Vernacextend.TyTerminal ("Elpi", - Vernacextend.TyTerminal ("Override", - Vernacextend.TyTerminal ("TC", Vernacextend.TyTerminal ("-", - Vernacextend.TyNonTerminal ( - Extend.TUlist0 ( - Extend.TUentry (Genarg.get_arg_tag wit_reference)), - Vernacextend.TyNil))))), - (let coqpp_body cs - atts = Vernacextend.vtdefault (fun () -> -# 28 "src/coq_elpi_tc_hook.mlg" - - let () = ignore_unknown_attributes atts in - takeover_rm cs - ) in fun cs - ?loc ~atts () -> coqpp_body cs - (Attributes.parse any_attribute atts)), None)); - (Vernacextend.TyML (false, Vernacextend.TyTerminal ("Elpi", - Vernacextend.TyTerminal ("Override", - Vernacextend.TyTerminal ("Register", - Vernacextend.TyNonTerminal (Extend.TUentry (Genarg.get_arg_tag wit_qualified_name), - Vernacextend.TyNil)))), (let coqpp_body p - atts = Vernacextend.vtdefault (fun () -> - -# 32 "src/coq_elpi_tc_hook.mlg" - - let () = ignore_unknown_attributes atts in - register_observer (fst p, snd p, atts) - ) in fun p - ?loc ~atts () - -> coqpp_body p - (Attributes.parse any_attribute atts)), None))] - From 42253d30abe5ee5502bd50bd655c1a2162ccdd25 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 22 Oct 2023 16:18:25 +0100 Subject: [PATCH 06/20] pass a term --- apps/tc/src/coq_elpi_tc_register.ml | 4 ++-- apps/tc/tests/auto_compile.v | 3 +-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/apps/tc/src/coq_elpi_tc_register.ml b/apps/tc/src/coq_elpi_tc_register.ml index 404c59f5d..db9c58c16 100644 --- a/apps/tc/src/coq_elpi_tc_register.ml +++ b/apps/tc/src/coq_elpi_tc_register.ml @@ -14,8 +14,8 @@ let observer_evt ((loc, name, atts) : loc_name_atts) (x : Event.t) = Printf.printf "Adding : %s\n" s; let s = String.split_on_char '.' s |> List.rev |> List.hd in let s = String.split_on_char ',' s |> List.hd in - Cmd.String s in - let add_aux gref = run_program (normalize_string (gref_2_string gref)) in + s in + let add_aux x = run_program (Cmd.Term (CAst.make @@ Constrexpr.CRef(Libnames.qualid_of_string @@ normalize_string @@ gref_2_string x,None))) in add_aux @@ match x with | Event.NewClass x -> x.cl_impl | Event.NewInstance x -> x.instance diff --git a/apps/tc/tests/auto_compile.v b/apps/tc/tests/auto_compile.v index cae9eace4..f21b15c85 100644 --- a/apps/tc/tests/auto_compile.v +++ b/apps/tc/tests/auto_compile.v @@ -12,8 +12,7 @@ Elpi Accumulate Db tc.db. Elpi Accumulate File create_tc_predicate. Elpi Accumulate File compiler. Elpi Accumulate lp:{{ - main [str A] :- - coq.locate A GR, + main [trm (global GR)] :- % coq.say {attributes}, coq.say "Adding :" GR, if (coq.TC.class? GR) (add-class-gr classic GR) From b80a6597dd133bdd0f7f3fdf9e56218961324db4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 22 Oct 2023 16:19:18 +0100 Subject: [PATCH 07/20] ignore generated file --- .gitignore | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index a8d712e50..c9d2ab4b9 100644 --- a/.gitignore +++ b/.gitignore @@ -46,4 +46,5 @@ META *.cache apps/coercion/src/coq_elpi_coercion_hook.ml -.filestoinstall \ No newline at end of file +.filestoinstall +apps/tc/src/coq_elpi_tc_hook.ml From 5090547c1a61cdbced1b6f20a2c15005313fd33c Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Sun, 22 Oct 2023 20:21:30 +0200 Subject: [PATCH 08/20] Refactor instance/class observer --- apps/tc/elpi/compiler.elpi | 12 ++++ apps/tc/src/coq_elpi_tc_register.ml | 68 ++++++++++---------- apps/tc/tests/auto_compile.v | 8 +-- apps/tc/tests/importOrder/sameOrderCommand.v | 38 ++++++++--- apps/tc/tests/importOrder/tc_same_order.elpi | 24 +++++++ 5 files changed, 101 insertions(+), 49 deletions(-) create mode 100644 apps/tc/tests/importOrder/tc_same_order.elpi diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi index ceae7e129..fbb533a06 100644 --- a/apps/tc/elpi/compiler.elpi +++ b/apps/tc/elpi/compiler.elpi @@ -154,6 +154,18 @@ make-inst-graft Inst _NoPremises (after Grafting) :- % if (NoPremises = tt) (Grafting = RawGrafting) (Grafting is RawGrafting ^ "_complex"). Grafting = RawGrafting. +pred add-inst i:gref, i:gref, i:string, i:int. +add-inst Inst TC Locality Prio :- + compile Inst _ TC Clause, + % TODO: a clause is flexible if an instance is polimorphic (pglobal) + not (var Clause), + Graft is after (int_to_string Prio), + get-full-path Inst ClauseName, + if (Locality = "Local") (Visibility = [@local!]) (Visibility = [@global!]), + Visibility => (add-tc-db ClauseName Graft Clause, add-tc-db _ Graft (instance [] 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 diff --git a/apps/tc/src/coq_elpi_tc_register.ml b/apps/tc/src/coq_elpi_tc_register.ml index db9c58c16..6330944cc 100644 --- a/apps/tc/src/coq_elpi_tc_register.ml +++ b/apps/tc/src/coq_elpi_tc_register.ml @@ -1,24 +1,44 @@ 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] + +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 | SuperGlobal -> "Global" in + Cmd.String (hint2string loc) in + let prio2elpi_int (prio: Typeclasses.hint_info) = + Cmd.Int (Option.default 0 prio.hint_priority) in + [ + gref2elpi_term instance; + gref2elpi_term class_name; + locality2elpi_string locality; + prio2elpi_int info + ] + let observer_evt ((loc, name, atts) : loc_name_atts) (x : Event.t) = let open Coq_elpi_vernacular in - let open Coq_elpi_arg_HOAS in - let run_program e = run_program loc name ~atts [e] in - let gref_2_string gref = Pp.string_of_ppcmds (Names.GlobRef.print gref) in - let normalize_string s = - Printf.printf "Adding : %s\n" s; - let s = String.split_on_char '.' s |> List.rev |> List.hd in - let s = String.split_on_char ',' s |> List.hd in - s in - let add_aux x = run_program (Cmd.Term (CAst.make @@ Constrexpr.CRef(Libnames.qualid_of_string @@ normalize_string @@ gref_2_string x,None))) in - add_aux @@ match x with - | Event.NewClass x -> x.cl_impl - | Event.NewInstance x -> x.instance + let run_program e = run_program loc name ~atts e in + run_program @@ match x with + | Event.NewClass cl -> observer_class cl + | Event.NewInstance inst -> observer_instance inst let inTakeover = let cache (loc, name, atts) = @@ -32,26 +52,4 @@ let inTakeover = (superglobal_object_nodischarge "TC_HACK_OBSERVER" ~cache ~subst:None)) let register_observer (x : loc_name_atts) = - Lib.add_leaf (inTakeover x) - -(* type hint_term = - | IsGlobRef of Names.GlobRef.t - | IsConstr of Constr.t * Univ.ContextSet.t option (* None if monomorphic *) - -let hack : Hints.hint_term -> hint_term = fun x -> - ( - assert (Coq_config.version = "8.18.0"); - Obj.magic x - ) *) - - (* EConstr.kind x - | Constr.Constant - | Constr.Contructor - | Constr.Inductive - | Constr..... *) - -(* let _ = - let sigma, env = - let env = Global.env () in Evd.(from_env env, env) in - Hints.pr_hint_db_by_name env sigma "typeclass_instances" |> ignore; - Printer.pr_constr_env env sigma |> ignore *) \ No newline at end of file + Lib.add_leaf (inTakeover x) \ No newline at end of file diff --git a/apps/tc/tests/auto_compile.v b/apps/tc/tests/auto_compile.v index f21b15c85..8c5b47adf 100644 --- a/apps/tc/tests/auto_compile.v +++ b/apps/tc/tests/auto_compile.v @@ -12,11 +12,11 @@ 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)] :- - % coq.say {attributes}, - coq.say "Adding :" GR, - if (coq.TC.class? GR) (add-class-gr classic GR) - (add-inst->db [] ff GR). + add-class-gr classic GR. }}. Elpi Typecheck. Elpi Override Register add_instance. diff --git a/apps/tc/tests/importOrder/sameOrderCommand.v b/apps/tc/tests/importOrder/sameOrderCommand.v index 1e7980554..30685d60e 100644 --- a/apps/tc/tests/importOrder/sameOrderCommand.v +++ b/apps/tc/tests/importOrder/sameOrderCommand.v @@ -1,14 +1,32 @@ From elpi Require Export tc. -Elpi Command SameOrderImport. +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 _ :- - std.findall (instance _ _ _) RulesInst, - coq.TC.db DB_tc-inst, - std.map RulesInst (x\inst\ instance _Path inst _TC = x) RulesElpi, - std.map DB_tc-inst (x\inst\ tc-instance inst _ = x) RulesCoq, - if (RulesElpi = RulesCoq) true ( - coq.error "Error in import order\n" - "Expected :" RulesCoq "\nFound :" RulesElpi). -}}. \ No newline at end of file + 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. diff --git a/apps/tc/tests/importOrder/tc_same_order.elpi b/apps/tc/tests/importOrder/tc_same_order.elpi new file mode 100644 index 000000000..f5f7dc4d9 --- /dev/null +++ b/apps/tc/tests/importOrder/tc_same_order.elpi @@ -0,0 +1,24 @@ +% [Typeclass, Coq Instances, Elpi Instances] +% the instances of the given typeclass should be in the same order as Coq +pred correct_instance_order_aux i:gref, i:(list gref), i:(list gref). +:name "tc-correct-instance-order-aux" +correct_instance_order_aux _ [] []. +correct_instance_order_aux TC [I1 | TL1] [I1 | TL2] :- + correct_instance_order_aux TC TL1 TL2. + +% [Typeclasses of Coq, Elpi Instances] +pred correct_instance_order i:(list gref), i:(list prop). +:name "tc-correct-instance-order" +correct_instance_order [] _. +correct_instance_order [TC | TL] ElpiInst :- + coq.TC.db-for2 TC CoqInst, + std.map-filter ElpiInst (x\r\ sigma I\ x = instance _ I TC, r = I) ElpiInstTC, + if (correct_instance_order_aux TC CoqInst ElpiInstTC) + (correct_instance_order TL ElpiInst) + (coq.error "Error in import order\n" + "Expected :" CoqInst "\nFound :" ElpiInstTC). + +:name "tc-same-order-main" +main _ :- + std.findall (instance _ _ _) ElpiInst, + correct_instance_order {coq.TC.db-tc} ElpiInst. \ No newline at end of file From 3aa61b060cdf82635b377bdbceae29b379240c86 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Sun, 22 Oct 2023 21:07:56 +0200 Subject: [PATCH 09/20] Ok all tests + correct instance insertion order --- apps/tc/_CoqProject.test | 15 +++++++-------- apps/tc/elpi/compiler.elpi | 5 ++++- apps/tc/elpi/tc_aux.elpi | 4 +++- apps/tc/src/coq_elpi_tc_register.ml | 11 ++++++++++- apps/tc/tests/eqSimpl.v | 1 - apps/tc/tests/importOrder/f1.v | 2 -- apps/tc/tests/importOrder/f2a.v | 3 +-- apps/tc/tests/importOrder/f2b.v | 2 +- apps/tc/tests/importOrder/f3a.v | 3 --- apps/tc/tests/importOrder/f3b.v | 3 --- apps/tc/tests/importOrder/f3c.v | 22 ++++++++++++++-------- apps/tc/tests/importOrder/f3d.v | 19 ++++++++++--------- apps/tc/tests/importOrder/f3e.v | 15 +++++++-------- apps/tc/tests/importOrder/f3f.v | 8 ++++---- apps/tc/tests/importOrder/f3g.v | 2 -- apps/tc/tests/importOrder/f4.v | 9 ++++++++- apps/tc/tests/patternFragmentBug.v | 2 +- apps/tc/tests/section_in_out.v | 6 ++++-- apps/tc/theories/tc.v | 7 +++---- 19 files changed, 77 insertions(+), 62 deletions(-) diff --git a/apps/tc/_CoqProject.test b/apps/tc/_CoqProject.test index 7d8dc9874..905583fe0 100644 --- a/apps/tc/_CoqProject.test +++ b/apps/tc/_CoqProject.test @@ -22,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 diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi index fbb533a06..7ec533927 100644 --- a/apps/tc/elpi/compiler.elpi +++ b/apps/tc/elpi/compiler.elpi @@ -159,7 +159,10 @@ add-inst Inst TC Locality Prio :- compile Inst _ TC Clause, % TODO: a clause is flexible if an instance is polimorphic (pglobal) not (var Clause), - Graft is after (int_to_string Prio), + if (Prio = -1) + (coq.env.typeof Inst InstTy, get-inst-prio-coq InstTy [] Prio1) + (Prio1 = Prio), + Graft is after (int_to_string Prio1), get-full-path Inst ClauseName, if (Locality = "Local") (Visibility = [@local!]) (Visibility = [@global!]), Visibility => (add-tc-db ClauseName Graft Clause, add-tc-db _ Graft (instance [] Inst TC)). diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi index b4d3ffac8..9a864ecc1 100644 --- a/apps/tc/elpi/tc_aux.elpi +++ b/apps/tc/elpi/tc_aux.elpi @@ -106,7 +106,9 @@ make-tc _IsHead Ty Inst Hyp Clause :- (Hyp = [Hd]) (Clause = (Q :- Hd)) (Clause = (Q :- Hyp)). - +% This predicate wants to campute the priority of an instance as Coq would do +% This computation of the priority of an instance is shown here +% https://github.com/coq/coq/blob/f022d5d194cb42c2321ea91cecbcce703a9bcad3/tactics/hints.ml#L841 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. diff --git a/apps/tc/src/coq_elpi_tc_register.ml b/apps/tc/src/coq_elpi_tc_register.ml index 6330944cc..9002ebe08 100644 --- a/apps/tc/src/coq_elpi_tc_register.ml +++ b/apps/tc/src/coq_elpi_tc_register.ml @@ -17,6 +17,15 @@ let gref2elpi_term (gref: Names.GlobRef.t) : Cmd.raw = 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 @@ -24,7 +33,7 @@ let observer_instance ({locality; instance; info; class_name} : instance) : Coq_ | Export | SuperGlobal -> "Global" in Cmd.String (hint2string loc) in let prio2elpi_int (prio: Typeclasses.hint_info) = - Cmd.Int (Option.default 0 prio.hint_priority) in + Cmd.Int (Option.default (-1) prio.hint_priority) in [ gref2elpi_term instance; gref2elpi_term class_name; diff --git a/apps/tc/tests/eqSimpl.v b/apps/tc/tests/eqSimpl.v index 07948357e..ff08779e1 100644 --- a/apps/tc/tests/eqSimpl.v +++ b/apps/tc/tests/eqSimpl.v @@ -12,7 +12,6 @@ Elpi AddInstances Eqb. Elpi Override TC TC_solver All. Fail Check (fun n m : _ => eqb n m). -Elpi Trace Browser. Goal (tt, (tt, true)) == (tt, (tt, true)) = true. easy. Qed. diff --git a/apps/tc/tests/importOrder/f1.v b/apps/tc/tests/importOrder/f1.v index a2b17d269..70c4c1c1c 100644 --- a/apps/tc/tests/importOrder/f1.v +++ b/apps/tc/tests/importOrder/f1.v @@ -2,6 +2,4 @@ From elpi.apps.tc.tests.importOrder Require Export sameOrderCommand. Class A (T : Set) := f : T -> T. -Elpi AddClasses A. - Elpi SameOrderImport. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f2a.v b/apps/tc/tests/importOrder/f2a.v index 0fcf326c3..9c3839098 100644 --- a/apps/tc/tests/importOrder/f2a.v +++ b/apps/tc/tests/importOrder/f2a.v @@ -7,5 +7,4 @@ Global Instance f2ab : A nat := {f x := x}. Global Instance f2ac : A nat := {f x := x}. Global Instance f2ad : A nat := {f x := x}. -Elpi AddInstances A. -(* Elpi SameOrderImport. *) \ No newline at end of file +Elpi SameOrderImport. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f2b.v b/apps/tc/tests/importOrder/f2b.v index 2f87a80aa..b7ec3d03e 100644 --- a/apps/tc/tests/importOrder/f2b.v +++ b/apps/tc/tests/importOrder/f2b.v @@ -5,5 +5,5 @@ Global Instance f2bb : A nat := {f x := x}. Global Instance f2bc : A nat := {f x := x}. Global Instance f2bd : A nat := {f x := x}. -Elpi AddInstances A. + (* Elpi SameOrderImport. *) diff --git a/apps/tc/tests/importOrder/f3a.v b/apps/tc/tests/importOrder/f3a.v index c32eac7c1..58d5444fd 100644 --- a/apps/tc/tests/importOrder/f3a.v +++ b/apps/tc/tests/importOrder/f3a.v @@ -1,7 +1,4 @@ From elpi.apps.tc.tests.importOrder Require Import f2a. From elpi.apps.tc.tests.importOrder Require Import f2b. -(* Elpi AddAllInstances. *) -Print HintDb typeclass_instances. -Elpi Print TC_solver "tests/f3a". Elpi SameOrderImport. diff --git a/apps/tc/tests/importOrder/f3b.v b/apps/tc/tests/importOrder/f3b.v index dce7ecc47..41f84e7aa 100644 --- a/apps/tc/tests/importOrder/f3b.v +++ b/apps/tc/tests/importOrder/f3b.v @@ -1,7 +1,4 @@ From elpi.apps.tc.tests.importOrder Require Import f2b. From elpi.apps.tc.tests.importOrder Require Import f2a. -(* Elpi AddAllInstances. *) -Print HintDb typeclass_instances. -Elpi Print TC_solver "tests/f3b". Elpi SameOrderImport. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f3c.v b/apps/tc/tests/importOrder/f3c.v index 1027dcd20..27df693ea 100644 --- a/apps/tc/tests/importOrder/f3c.v +++ b/apps/tc/tests/importOrder/f3c.v @@ -3,24 +3,31 @@ From elpi.apps.tc.tests.importOrder Require Export f1. Global Instance f3a : A nat := {f x := x}. Global Instance f3b : A nat := {f x := x}. Global Instance f3c : A nat := {f x := x}. -Elpi AddAllInstances. + Elpi SameOrderImport. Section S1. - Global Instance f3d : A nat := {f x := x}. + Local Instance f3d : A nat := {f x := x}. Global Instance f3e : A nat := {f x := x}. Global Instance f3f : A nat := {f x := x}. - Elpi AddAllInstances. + Elpi SameOrderImport. -MySectionEnd. +End S1. Elpi SameOrderImport. Section S2. Context (T : Set). Global Instance f3g : A T := {f x := x}. - Elpi AddAllInstances. + Elpi SameOrderImport. -MySectionEnd. +End S2. + +Elpi Query add_instance lp:{{ + coq.warning "elpi.todo" "todo" "On section end, instances depending on + context variables should create an Event so that they are recompiled in elpi" +}}. + +(* TODO: Here the instance f3g should be readded... *) Elpi SameOrderImport. Section S3. @@ -32,8 +39,7 @@ Section S3. Global Instance f3g3 : A (T: Set) := {f x := x}. Global Instance f3g4 : A (T: Set) | 10 := {f x := x}. - Elpi AddAllInstances. Elpi SameOrderImport. -MySectionEnd. +End S3. Elpi SameOrderImport. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f3d.v b/apps/tc/tests/importOrder/f3d.v index 4b1a9bdcb..0566660a4 100644 --- a/apps/tc/tests/importOrder/f3d.v +++ b/apps/tc/tests/importOrder/f3d.v @@ -3,7 +3,7 @@ From elpi.apps.tc.tests.importOrder Require Import f2b. Elpi SameOrderImport. Global Instance f3a' T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}. -Elpi AddInstances A. + Elpi SameOrderImport. Module M4'. @@ -11,21 +11,22 @@ Module M4'. Elpi SameOrderImport. Global Instance f3a : A nat := {f x := x}. - Elpi AddInstances f3a. + Section S1. Global Instance f3b : A nat := {f x := x}. - Elpi AddInstances f3b. + Section S1'. Global Instance f3c : A nat := {f x := x}. - Elpi AddInstances f3c. - MySectionEnd. - MySectionEnd. + + End S1'. + End S1. Elpi SameOrderImport. Section S2. Global Instance f3h T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}. - Elpi AddInstances f3h. - MySectionEnd. -End M4'. \ No newline at end of file + End S2. +End M4'. + +Elpi SameOrderImport. diff --git a/apps/tc/tests/importOrder/f3e.v b/apps/tc/tests/importOrder/f3e.v index fbffe2a68..842bc909e 100644 --- a/apps/tc/tests/importOrder/f3e.v +++ b/apps/tc/tests/importOrder/f3e.v @@ -1,25 +1,24 @@ From elpi.apps.tc.tests.importOrder Require Export f1. From elpi.apps.tc.tests.importOrder Require Import f2b. +From elpi.apps.tc.tests.importOrder Require Import f2a. Global Instance f3a' T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}. -Elpi AddAllInstances. + Elpi SameOrderImport. Module M4'. - From elpi.apps.tc.tests.importOrder Require Import f2a. - Global Instance f3a : A nat := {f x := x}. Section S1. Global Instance f3b : A nat := {f x := x}. Section S1'. Global Instance f3c : A nat := {f x := x}. - MySectionEnd. - MySectionEnd. + End S1'. + End S1. Section S2. - Global Instance f3h T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}. - MySectionEnd. + Global Instance f3h T1 T2 `(A T1, A T2) : A (T1 * T2) | 100 := {f x := x}. + End S2. End M4'. -Elpi AddAllInstances. + Elpi SameOrderImport. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f3f.v b/apps/tc/tests/importOrder/f3f.v index d183876c1..2b0db45ee 100644 --- a/apps/tc/tests/importOrder/f3f.v +++ b/apps/tc/tests/importOrder/f3f.v @@ -3,15 +3,15 @@ From elpi.apps.tc.tests.importOrder Require Import f1. Section S1. Context (T : Set). Global Instance f3a : A T := {f x := x}. - Elpi AddInstances f3a. + Elpi SameOrderImport. Section S2. Context (T1 : Set). Global Instance f3b : A T1 := {f x := x}. - Elpi AddInstances f3b. - MySectionEnd. + + End S2. Elpi SameOrderImport. -MySectionEnd. +End S1. Elpi SameOrderImport. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f3g.v b/apps/tc/tests/importOrder/f3g.v index 1650e3416..608efd7f1 100644 --- a/apps/tc/tests/importOrder/f3g.v +++ b/apps/tc/tests/importOrder/f3g.v @@ -2,10 +2,8 @@ From elpi.apps.tc.tests.importOrder Require Export f1. Module M8. Class Classe (A: Type) (B: Type). - Elpi AddClasses Classe. Global Instance I (a b c d: Type): Classe a a -> Classe b c. Admitted. - Elpi AddAllInstances. Elpi SameOrderImport. End M8. diff --git a/apps/tc/tests/importOrder/f4.v b/apps/tc/tests/importOrder/f4.v index 62681ca25..0d73340cd 100644 --- a/apps/tc/tests/importOrder/f4.v +++ b/apps/tc/tests/importOrder/f4.v @@ -1 +1,8 @@ -From elpi.apps.tc.tests.importOrder Require Import f3f. \ No newline at end of file +From elpi.apps.tc.tests.importOrder Require Import f3f. +From elpi.apps.tc.tests.importOrder Require Import f2a. +From elpi.apps.tc.tests.importOrder Require Import f2b. +From elpi.apps.tc.tests.importOrder Require Import f3c. +From elpi.apps.tc.tests.importOrder Require Import f3d. +From elpi.apps.tc.tests.importOrder Require Import f3g. + +Elpi SameOrderImport. \ No newline at end of file diff --git a/apps/tc/tests/patternFragmentBug.v b/apps/tc/tests/patternFragmentBug.v index 8570fd7fc..31174df32 100644 --- a/apps/tc/tests/patternFragmentBug.v +++ b/apps/tc/tests/patternFragmentBug.v @@ -48,7 +48,7 @@ Unset Typeclass Resolution For Conversion. Goal Z bool. intros. (* TODO: here Elpi Trace Fails... *) -Elpi Trace Browser. +(* Elpi Trace Browser. *) (* Elpi Override TC TC_solver Only Z. *) (* Elpi Override TC - Z. *) diff --git a/apps/tc/tests/section_in_out.v b/apps/tc/tests/section_in_out.v index e643d2d09..fa484adbe 100644 --- a/apps/tc/tests/section_in_out.v +++ b/apps/tc/tests/section_in_out.v @@ -1,13 +1,16 @@ From elpi.apps Require Import tc. From elpi.apps.tc Extra Dependency "base.elpi" as base. +Elpi Accumulate tc.db lp:{{ + pred origial_tc o:int. +}}. + Elpi Command len_test. Elpi Accumulate Db tc.db. Elpi Accumulate File base. Elpi Accumulate lp:{{ % contains the number of instances that are not % imported from other files - pred origial_tc o:int. main [int Len] :- std.findall (instance _ _ _) Insts, std.map Insts (x\r\ instance _ r _ = x) R, @@ -17,7 +20,6 @@ Elpi Accumulate lp:{{ std.forall R (x\ sigma L\ std.assert! (count R x L, L = 1) "Duplicates in instances"). }}. -(* Elpi Typecheck. *) Elpi Query TC_solver lp:{{ std.findall (instance _ _ _) Rules, diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v index be43387ac..144da73bd 100644 --- a/apps/tc/theories/tc.v +++ b/apps/tc/theories/tc.v @@ -67,10 +67,9 @@ Elpi Accumulate File modes. Elpi Accumulate File compiler. Elpi Accumulate lp:{{ main _ :- - % true. - % instances-of-current-section InstsFiltered, - coq.env.end-section. - % std.forall {std.rev InstsFiltered} (add-inst->db [] tt). + instances-of-current-section InstsFiltered, + coq.env.end-section, + std.forall {std.rev InstsFiltered} (add-inst->db [] tt). }}. (* Elpi Typecheck. *) From bc3090b3251eb5a4c4d47c79b8adadcbae9815ef Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Mon, 23 Oct 2023 18:05:05 +0200 Subject: [PATCH 10/20] WIP: tc-for2 returns tc-instnce --- apps/tc/tests/importOrder/tc_same_order.elpi | 4 ++-- coq-builtin.elpi | 2 +- src/coq_elpi_builtins.ml | 14 +++++++++----- 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/apps/tc/tests/importOrder/tc_same_order.elpi b/apps/tc/tests/importOrder/tc_same_order.elpi index f5f7dc4d9..bd1662ece 100644 --- a/apps/tc/tests/importOrder/tc_same_order.elpi +++ b/apps/tc/tests/importOrder/tc_same_order.elpi @@ -1,9 +1,9 @@ % [Typeclass, Coq Instances, Elpi Instances] % the instances of the given typeclass should be in the same order as Coq -pred correct_instance_order_aux i:gref, i:(list gref), i:(list gref). +pred correct_instance_order_aux i:gref, i:(list tc-instance), i:(list gref). :name "tc-correct-instance-order-aux" correct_instance_order_aux _ [] []. -correct_instance_order_aux TC [I1 | TL1] [I1 | TL2] :- +correct_instance_order_aux TC [tc-instance I1 _ | TL1] [I1 | TL2] :- correct_instance_order_aux TC TL1 TL2. % [Typeclasses of Coq, Elpi Instances] diff --git a/coq-builtin.elpi b/coq-builtin.elpi index b581dc22d..a9b4559d0 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -1145,7 +1145,7 @@ external pred coq.TC.db-tc o:list gref. external pred coq.TC.db-for i:gref, o:list tc-instance. % [coq.TC.db-for2 GR List Db] reads all instances of the given class GR -external pred coq.TC.db-for2 i:gref, o:list gref. +external pred coq.TC.db-for2 i:gref, o:list tc-instance. % [coq.TC.class? GR] checks if GR is a class external pred coq.TC.class? i:gref. diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index ec28f0cf1..f5444d86e 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -1234,7 +1234,7 @@ let eta_contract env sigma t = (*Printf.eprintf "------------- %s\n" Pp.(string_of_ppcmds @@ Printer.pr_econstr_env env sigma t);*) map env t -let get_instances tc = +let get_instances (env: Environ.env) (emap: Evd.evar_map) tc = let hint_db = Hints.searchtable_map "typeclass_instances" in let secvars : Names.Id.Pred.t = Names.Id.Pred.full in let full_hints = Hints.Hint_db.map_all ~secvars:secvars tc hint_db in @@ -1256,7 +1256,11 @@ let get_instances tc = | Constr.Const (a, _) -> Some (Names.GlobRef.ConstRef a) | Constr.Construct (a, _) -> Some (Names.GlobRef.ConstructRef a) | _ -> None) constrs in - instances_grefs + let instances_grefs2istance x = + let open Typeclasses in + let inst_of_tc = instances_exn env emap tc in + List.find (fun (e: instance) -> e.is_impl = x) inst_of_tc in + List.map instances_grefs2istance instances_grefs (*****************************************************************************) @@ -2751,9 +2755,9 @@ Supported attributes: MLCode(Pred("coq.TC.db-for2", In(gref, "GR", - Out(B.list gref, "List Db", - Easy {|reads all instances of the given class GR|})), - (fun s _ ~depth:_ -> !: (get_instances s))), + Out(list tc_instance, "List Db", + Read (global, "reads all instances of the given class GR"))), + (fun gr _ ~depth { env } _ state -> !: (get_instances env (get_sigma state) gr))), DocAbove); MLCode(Pred("coq.TC.class?", From f1526afba3021f5ff94340002a36d4b53bb8f0a5 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Mon, 23 Oct 2023 18:48:54 +0200 Subject: [PATCH 11/20] fun to get prio of an inst --- src/coq_elpi_builtins.ml | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index f5444d86e..e3e284a94 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -1234,6 +1234,30 @@ let eta_contract env sigma t = (*Printf.eprintf "------------- %s\n" Pp.(string_of_ppcmds @@ Printer.pr_econstr_env env sigma t);*) map env t +let get_term_prio gr env sigma (info : 'a Typeclasses.hint_info_gen) : int = + let rec nb_hyp sigma c = match EConstr.kind sigma c with + | Prod(_,_,c2) -> if EConstr.Vars.noccurn sigma 1 c2 then 1+(nb_hyp sigma c2) else nb_hyp sigma c2 + | _ -> 0 in + let merge_context_set_opt sigma ctx = + match ctx with + | None -> sigma + | Some ctx -> Evd.merge_context_set Evd.univ_flexible sigma ctx + in + let fresh_global_or_constr env sigma = + let (c, ctx) = UnivGen.fresh_global_instance env gr in + let ctx = if Environ.is_polymorphic env gr then Some ctx else None in + (EConstr.of_constr c, ctx) in + let c, ctx = fresh_global_or_constr env sigma in + let cty = Retyping.get_type_of env sigma c in + let cty = Reductionops.nf_betaiota env sigma cty in + let sigma' = merge_context_set_opt sigma ctx in + let ce = Clenv.mk_clenv_from env sigma' (c,cty) in + let miss = Clenv.clenv_missing ce in + let nmiss = List.length miss in + let hyps = nb_hyp sigma' cty in + let pri = match info.hint_priority with None -> hyps + nmiss | Some p -> p in + pri + let get_instances (env: Environ.env) (emap: Evd.evar_map) tc = let hint_db = Hints.searchtable_map "typeclass_instances" in let secvars : Names.Id.Pred.t = Names.Id.Pred.full in @@ -1259,7 +1283,9 @@ let get_instances (env: Environ.env) (emap: Evd.evar_map) tc = let instances_grefs2istance x = let open Typeclasses in let inst_of_tc = instances_exn env emap tc in - List.find (fun (e: instance) -> e.is_impl = x) inst_of_tc in + let inst = List.find (fun (e: instance) -> e.is_impl = x) inst_of_tc in + let inst_prio = get_term_prio x env sigma inst.is_info in + {inst with is_info = { inst.is_info with hint_priority = Some inst_prio}} in List.map instances_grefs2istance instances_grefs From 95a2c1fb0462a27c503da8e745f7257aa6055256 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Mon, 23 Oct 2023 18:53:01 +0200 Subject: [PATCH 12/20] function rename --- src/coq_elpi_builtins.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index e3e284a94..2d1f16d43 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -1234,7 +1234,7 @@ let eta_contract env sigma t = (*Printf.eprintf "------------- %s\n" Pp.(string_of_ppcmds @@ Printer.pr_econstr_env env sigma t);*) map env t -let get_term_prio gr env sigma (info : 'a Typeclasses.hint_info_gen) : int = +let get_instance_prio gr env sigma (info : 'a Typeclasses.hint_info_gen) : int = let rec nb_hyp sigma c = match EConstr.kind sigma c with | Prod(_,_,c2) -> if EConstr.Vars.noccurn sigma 1 c2 then 1+(nb_hyp sigma c2) else nb_hyp sigma c2 | _ -> 0 in @@ -1284,7 +1284,7 @@ let get_instances (env: Environ.env) (emap: Evd.evar_map) tc = let open Typeclasses in let inst_of_tc = instances_exn env emap tc in let inst = List.find (fun (e: instance) -> e.is_impl = x) inst_of_tc in - let inst_prio = get_term_prio x env sigma inst.is_info in + let inst_prio = get_instance_prio x env sigma inst.is_info in {inst with is_info = { inst.is_info with hint_priority = Some inst_prio}} in List.map instances_grefs2istance instances_grefs From f95c7d833aa95ce158a6f4d0b6cd0e10980f0b47 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Tue, 24 Oct 2023 14:46:17 +0200 Subject: [PATCH 13/20] Small correction for no-argument classes --- apps/tc/elpi/solver.elpi | 2 +- apps/tc/elpi/tc_aux.elpi | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi index 64f7f9bf0..c08472d4f 100644 --- a/apps/tc/elpi/solver.elpi +++ b/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. diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi index 9a864ecc1..629ea809e 100644 --- a/apps/tc/elpi/tc_aux.elpi +++ b/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, @@ -114,6 +114,7 @@ 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 (global _) _ 0. get-inst-prio-coq A _ _ :- coq.error "Invalid case for" A. % returns the priority of an instance from the gref of an instance From b9f994ea1c0825c867ccb13d365be0759bcedee4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 25 Oct 2023 15:58:29 +0200 Subject: [PATCH 14/20] uniform API --- apps/tc/elpi/compiler.elpi | 2 +- apps/tc/elpi/tc_aux.elpi | 16 +- apps/tc/tests/importOrder/tc_same_order.elpi | 2 +- coq-builtin.elpi | 13 +- src/coq_elpi_builtins.ml | 165 +++++++++++-------- 5 files changed, 106 insertions(+), 92 deletions(-) diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi index 7ec533927..70c37511a 100644 --- a/apps/tc/elpi/compiler.elpi +++ b/apps/tc/elpi/compiler.elpi @@ -160,7 +160,7 @@ add-inst Inst TC Locality Prio :- % TODO: a clause is flexible if an instance is polimorphic (pglobal) not (var Clause), if (Prio = -1) - (coq.env.typeof Inst InstTy, get-inst-prio-coq InstTy [] Prio1) + (get-inst-prio Inst Prio1) (Prio1 = Prio), Graft is after (int_to_string Prio1), get-full-path Inst ClauseName, diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi index 629ea809e..abea7e6f0 100644 --- a/apps/tc/elpi/tc_aux.elpi +++ b/apps/tc/elpi/tc_aux.elpi @@ -106,25 +106,15 @@ make-tc _IsHead Ty Inst Hyp Clause :- (Hyp = [Hd]) (Clause = (Q :- Hd)) (Clause = (Q :- Hyp)). -% This predicate wants to campute the priority of an instance as Coq would do -% This computation of the priority of an instance is shown here -% https://github.com/coq/coq/blob/f022d5d194cb42c2321ea91cecbcce703a9bcad3/tactics/hints.ml#L841 -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 (global _) _ 0. -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 diff --git a/apps/tc/tests/importOrder/tc_same_order.elpi b/apps/tc/tests/importOrder/tc_same_order.elpi index bd1662ece..4d4607123 100644 --- a/apps/tc/tests/importOrder/tc_same_order.elpi +++ b/apps/tc/tests/importOrder/tc_same_order.elpi @@ -11,7 +11,7 @@ pred correct_instance_order i:(list gref), i:(list prop). :name "tc-correct-instance-order" correct_instance_order [] _. correct_instance_order [TC | TL] ElpiInst :- - coq.TC.db-for2 TC CoqInst, + coq.TC.db-for TC CoqInst, std.map-filter ElpiInst (x\r\ sigma I\ x = instance _ I TC, r = I) ElpiInstTC, if (correct_instance_order_aux TC CoqInst ElpiInstTC) (correct_instance_order TL ElpiInst) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index a9b4559d0..da1556585 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -1125,9 +1125,14 @@ external pred coq.CS.db-for i:gref, i:cs-pattern, o:list cs-instance. % [coq.TC.declare-class GR] Declare GR as a type class external pred coq.TC.declare-class i:gref. +% Type class instance priority +kind tc-priority type. +type tc-priority-given int -> tc-priority. % User given priority +type tc-priority-computed int -> tc-priority. % Coq computed priority + % Type class instance with priority kind tc-instance type. -type tc-instance gref -> int -> tc-instance. +type tc-instance gref -> tc-priority -> tc-instance. % [coq.TC.declare-instance GR Priority] Declare GR as a Global type class % instance with Priority. @@ -1141,12 +1146,10 @@ external pred coq.TC.db o:list tc-instance. % [coq.TC.db-tc TypeClasses] reads all type classes external pred coq.TC.db-tc o:list gref. -% [coq.TC.db-for GR Db] reads all instances of the given class GR +% [coq.TC.db-for GR InstanceList] reads all instances of the given class GR. +% Instances are in their precedence order. external pred coq.TC.db-for i:gref, o:list tc-instance. -% [coq.TC.db-for2 GR List Db] reads all instances of the given class GR -external pred coq.TC.db-for2 i:gref, o:list tc-instance. - % [coq.TC.class? GR] checks if GR is a class external pred coq.TC.class? i:gref. diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 2d1f16d43..259af19df 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -442,17 +442,95 @@ let cs_instance = let open Conv in let open API.AlgebraicData in let open Struct ] } |> CConv.(!<) -let tc_instance = let open Conv in let open API.AlgebraicData in let open Typeclasses in declare { + +type tc_priority = Computed of int | UserGiven of int + +let tc_priority = let open Conv in let open API.AlgebraicData in declare { + ty = TyName "tc-priority"; + doc = "Type class instance priority"; + pp = (fun fmt _ -> Format.fprintf fmt ""); + constructors = [ + K("tc-priority-given","User given priority",A(int,N), + B (fun i -> UserGiven i), + M (fun ~ok ~ko -> function UserGiven i -> ok i | _ -> ko ())); + K("tc-priority-computed","Coq computed priority", A(int,N), + B (fun i -> Computed i), + M (fun ~ok ~ko -> function Computed i -> ok i | _ -> ko ())); +]} |> CConv.(!<) + +type type_class_instance = { + implementation : GlobRef.t; + priority : tc_priority; +} + +let tc_instance = let open Conv in let open API.AlgebraicData in declare { ty = TyName "tc-instance"; doc = "Type class instance with priority"; pp = (fun fmt _ -> Format.fprintf fmt ""); constructors = [ - K("tc-instance","",A(gref,A(int,N)), - B (fun g p -> nYI "lp2instance"), - M (fun ~ok ~ko i -> - ok (instance_impl i) (Option.default 0 (hint_priority i)))); + K("tc-instance","",A(gref,A(tc_priority,N)), + B (fun implementation priority -> { implementation; priority }), + M (fun ~ok ~ko { implementation; priority } -> ok implementation priority)); ]} |> CConv.(!<) +let get_instance_prio gr env sigma (info : 'a Typeclasses.hint_info_gen) : tc_priority = + match info.hint_priority with + | Some p -> UserGiven p + | None -> + let rec nb_hyp sigma c = match EConstr.kind sigma c with + | Prod(_,_,c2) -> if EConstr.Vars.noccurn sigma 1 c2 then 1+(nb_hyp sigma c2) else nb_hyp sigma c2 + | _ -> 0 in + let merge_context_set_opt sigma ctx = + match ctx with + | None -> sigma + | Some ctx -> Evd.merge_context_set Evd.univ_flexible sigma ctx + in + let fresh_global_or_constr env sigma = + let (c, ctx) = UnivGen.fresh_global_instance env gr in + let ctx = if Environ.is_polymorphic env gr then Some ctx else None in + (EConstr.of_constr c, ctx) in + let c, ctx = fresh_global_or_constr env sigma in + let cty = Retyping.get_type_of env sigma c in + let cty = Reductionops.nf_betaiota env sigma cty in + let sigma' = merge_context_set_opt sigma ctx in + let ce = Clenv.mk_clenv_from env sigma' (c,cty) in + let miss = Clenv.clenv_missing ce in + let nmiss = List.length miss in + let hyps = nb_hyp sigma' cty in + Computed (hyps + nmiss) + +let get_instances (env: Environ.env) (emap: Evd.evar_map) tc : type_class_instance list = + let hint_db = Hints.searchtable_map "typeclass_instances" in + let secvars : Names.Id.Pred.t = Names.Id.Pred.full in + let full_hints = Hints.Hint_db.map_all ~secvars:secvars tc hint_db in + let hint_asts = List.map Hints.FullHint.repr full_hints in + let hints = List.filter_map (function + | Hints.Res_pf a -> Some a + | ERes_pf a -> Some a + | Extern (a, b) -> None + | Give_exact a -> Some a + | Res_pf_THEN_trivial_fail e -> Some e + | Unfold_nth e -> None) hint_asts in + let sigma, _ = + let env = Global.env () in Evd.(from_env env, env) in + let constrs = List.map (fun a -> Hints.hint_as_term a |> snd) hints in + (* Printer.pr_global tc |> Pp.string_of_ppcmds |> Printf.printf "%s\n"; *) + let instances_grefs = List.filter_map (fun e -> + match EConstr.kind sigma e with + | Constr.Ind (a, _) -> Some (Names.GlobRef.IndRef a) + | Constr.Const (a, _) -> Some (Names.GlobRef.ConstRef a) + | Constr.Construct (a, _) -> Some (Names.GlobRef.ConstructRef a) + | _ -> None) constrs in + let inst_of_tc = + Typeclasses.instances_exn env emap tc |> + List.fold_left (fun m i -> GlobRef.Map.add i.Typeclasses.is_impl i m) GlobRef.Map.empty in + let instances_grefs2istance x = + let open Typeclasses in + let inst = GlobRef.Map.find x inst_of_tc in + let priority = get_instance_prio x env sigma inst.is_info in + { implementation = x; priority } in + List.map instances_grefs2istance instances_grefs + type scope = ExecutionSite | CurrentModule | Library let scope = let open Conv in let open API.AlgebraicData in declare { @@ -1234,60 +1312,6 @@ let eta_contract env sigma t = (*Printf.eprintf "------------- %s\n" Pp.(string_of_ppcmds @@ Printer.pr_econstr_env env sigma t);*) map env t -let get_instance_prio gr env sigma (info : 'a Typeclasses.hint_info_gen) : int = - let rec nb_hyp sigma c = match EConstr.kind sigma c with - | Prod(_,_,c2) -> if EConstr.Vars.noccurn sigma 1 c2 then 1+(nb_hyp sigma c2) else nb_hyp sigma c2 - | _ -> 0 in - let merge_context_set_opt sigma ctx = - match ctx with - | None -> sigma - | Some ctx -> Evd.merge_context_set Evd.univ_flexible sigma ctx - in - let fresh_global_or_constr env sigma = - let (c, ctx) = UnivGen.fresh_global_instance env gr in - let ctx = if Environ.is_polymorphic env gr then Some ctx else None in - (EConstr.of_constr c, ctx) in - let c, ctx = fresh_global_or_constr env sigma in - let cty = Retyping.get_type_of env sigma c in - let cty = Reductionops.nf_betaiota env sigma cty in - let sigma' = merge_context_set_opt sigma ctx in - let ce = Clenv.mk_clenv_from env sigma' (c,cty) in - let miss = Clenv.clenv_missing ce in - let nmiss = List.length miss in - let hyps = nb_hyp sigma' cty in - let pri = match info.hint_priority with None -> hyps + nmiss | Some p -> p in - pri - -let get_instances (env: Environ.env) (emap: Evd.evar_map) tc = - let hint_db = Hints.searchtable_map "typeclass_instances" in - let secvars : Names.Id.Pred.t = Names.Id.Pred.full in - let full_hints = Hints.Hint_db.map_all ~secvars:secvars tc hint_db in - let hint_asts = List.map Hints.FullHint.repr full_hints in - let hints = List.filter_map (function - | Hints.Res_pf a -> Some a - | ERes_pf a -> Some a - | Extern (a, b) -> None - | Give_exact a -> Some a - | Res_pf_THEN_trivial_fail e -> Some e - | Unfold_nth e -> None) hint_asts in - let sigma, _ = - let env = Global.env () in Evd.(from_env env, env) in - let constrs = List.map (fun a -> Hints.hint_as_term a |> snd) hints in - (* Printer.pr_global tc |> Pp.string_of_ppcmds |> Printf.printf "%s\n"; *) - let instances_grefs = List.filter_map (fun e -> - match EConstr.kind sigma e with - | Constr.Ind (a, _) -> Some (Names.GlobRef.IndRef a) - | Constr.Const (a, _) -> Some (Names.GlobRef.ConstRef a) - | Constr.Construct (a, _) -> Some (Names.GlobRef.ConstructRef a) - | _ -> None) constrs in - let instances_grefs2istance x = - let open Typeclasses in - let inst_of_tc = instances_exn env emap tc in - let inst = List.find (fun (e: instance) -> e.is_impl = x) inst_of_tc in - let inst_prio = get_instance_prio x env sigma inst.is_info in - {inst with is_info = { inst.is_info with hint_priority = Some inst_prio}} in - List.map instances_grefs2istance instances_grefs - (*****************************************************************************) (*****************************************************************************) @@ -2740,6 +2764,7 @@ Supported attributes: state, (), []))), DocAbove); + MLData tc_priority; MLData tc_instance; MLCode(Pred("coq.TC.declare-instance", @@ -2758,8 +2783,12 @@ Supported attributes: MLCode(Pred("coq.TC.db", Out(list tc_instance, "Instances", - Easy "reads all type class instances"), - (fun _ ~depth -> !: (Typeclasses.all_instances ()))), + Read(global, "reads all type class instances")), + (fun _ ~depth { env } _ state -> + let sigma = get_sigma state in + let x = Typeclasses.typeclasses () in + let classes = List.map (fun x -> x.Typeclasses.cl_impl) x in + !: (classes |> List.map (get_instances env sigma) |> List.concat))), DocAbove); MLCode(Pred("coq.TC.db-tc", @@ -2771,18 +2800,10 @@ Supported attributes: l))), DocAbove); - MLCode(Pred("coq.TC.db-for", - In(gref, "GR", - Out(list tc_instance, "Db", - Read(global,"reads all instances of the given class GR"))), - (fun gr _ ~depth { env } _ state -> - !: (Typeclasses.instances_exn env (get_sigma state) gr))), - DocAbove); - - MLCode(Pred("coq.TC.db-for2", + MLCode(Pred("coq.TC.db-for", In(gref, "GR", - Out(list tc_instance, "List Db", - Read (global, "reads all instances of the given class GR"))), + Out(list tc_instance, "InstanceList", + Read (global, "reads all instances of the given class GR. Instances are in their precedence order."))), (fun gr _ ~depth { env } _ state -> !: (get_instances env (get_sigma state) gr))), DocAbove); From dfde18949d324fe45dc6f04adb939efc32dc9b2e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 25 Oct 2023 16:17:44 +0200 Subject: [PATCH 15/20] fix paths for vscoq --- apps/tc/_CoqProject | 1 + 1 file changed, 1 insertion(+) diff --git a/apps/tc/_CoqProject b/apps/tc/_CoqProject index 5d380e185..50c6dbae3 100644 --- a/apps/tc/_CoqProject +++ b/apps/tc/_CoqProject @@ -5,6 +5,7 @@ -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 From a50f1048874e8d6043ab92032862f606232de39b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 25 Oct 2023 16:54:22 +0200 Subject: [PATCH 16/20] wip section ending --- apps/tc/elpi/compiler.elpi | 9 +++++---- apps/tc/elpi/tc_aux.elpi | 6 ++---- apps/tc/src/coq_elpi_tc_register.ml | 11 ++++++++--- apps/tc/tests/importOrder/f3c.v | 4 +++- apps/tc/tests/importOrder/f3d.v | 6 +++--- apps/tc/tests/importOrder/f3e.v | 6 +++--- apps/tc/theories/tc.v | 5 +++-- 7 files changed, 27 insertions(+), 20 deletions(-) diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi index 70c37511a..c13df14e1 100644 --- a/apps/tc/elpi/compiler.elpi +++ b/apps/tc/elpi/compiler.elpi @@ -156,6 +156,7 @@ make-inst-graft Inst _NoPremises (after Grafting) :- pred add-inst i:gref, i:gref, i:string, i:int. add-inst Inst TC Locality Prio :- + coq.env.section SectionVars, compile Inst _ TC Clause, % TODO: a clause is flexible if an instance is polimorphic (pglobal) not (var Clause), @@ -165,7 +166,7 @@ add-inst Inst TC Locality Prio :- Graft is after (int_to_string Prio1), get-full-path Inst ClauseName, if (Locality = "Local") (Visibility = [@local!]) (Visibility = [@global!]), - Visibility => (add-tc-db ClauseName Graft Clause, add-tc-db _ Graft (instance [] Inst TC)). + Visibility => (add-tc-db ClauseName Graft Clause, add-tc-db _ Graft (instance SectionVars Inst TC)). add-inst Inst _ _ _ :- coq.warning "Not-added" "TC_solver" "Warning : Cannot compile " Inst "since it is pglobal". @@ -175,7 +176,7 @@ add-inst Inst _ _ _ :- pred add-inst->db i:list gref, i:bool, i:gref. :name "add-inst->db:start" add-inst->db IgnoreClassDepL ForceAdd Inst :- - coq.env.current-section-path SectionPath, + coq.env.section SectionVars, get-sub-classes Inst Dep, warn-multiple-deps Inst Dep, if ((ForceAdd = tt; not (instance _ Inst _)), @@ -188,8 +189,8 @@ add-inst->db IgnoreClassDepL ForceAdd Inst :- get-full-path Inst ClauseName, if (is-local) (Visibility = [@local!]) (if (has-context-deps Inst) - (@local! => add-tc-db _ Graft (instance SectionPath Inst TC-of-Inst)) - (@global! => add-tc-db _ Graft (instance [] Inst TC-of-Inst)), Visibility = [@global!]), + (@local! => add-tc-db _ Graft (instance SectionVars Inst TC-of-Inst)) + (@global! => add-tc-db _ Graft (instance SectionVars Inst TC-of-Inst)), Visibility = [@global!]), Visibility => add-tc-db ClauseName Graft Clause ) true; @global! => add-tc-db _ _ (banned Inst), diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi index abea7e6f0..4af76b19c 100644 --- a/apps/tc/elpi/tc_aux.elpi +++ b/apps/tc/elpi/tc_aux.elpi @@ -34,10 +34,8 @@ remove-eta2 A B :- !, pred instances-of-current-section o:list gref. :name "MySectionEndHook" instances-of-current-section InstsFiltered :- - coq.env.current-section-path SectionPath, - std.findall (instance SectionPath _ _) Insts, - coq.env.section SectionVars, - std.map-filter Insts (x\r\ sigma X\ instance _ r _ = x, const X = r, not(std.mem SectionVars X)) InstsFiltered. + std.findall (instance _ _ _) Insts, + std.map-filter Insts (x\r\ sigma X\ instance _ r _ = x, const X = r) InstsFiltered. pred is-instance-gr i:gref. is-instance-gr GR :- diff --git a/apps/tc/src/coq_elpi_tc_register.ml b/apps/tc/src/coq_elpi_tc_register.ml index 9002ebe08..ae36db698 100644 --- a/apps/tc/src/coq_elpi_tc_register.ml +++ b/apps/tc/src/coq_elpi_tc_register.ml @@ -41,13 +41,18 @@ let observer_instance ({locality; instance; info; class_name} : instance) : Coq_ 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 - run_program @@ match x with - | Event.NewClass cl -> observer_class cl - | Event.NewInstance inst -> observer_instance inst + 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) = diff --git a/apps/tc/tests/importOrder/f3c.v b/apps/tc/tests/importOrder/f3c.v index 27df693ea..ecd6e7899 100644 --- a/apps/tc/tests/importOrder/f3c.v +++ b/apps/tc/tests/importOrder/f3c.v @@ -6,13 +6,15 @@ Global Instance f3c : A nat := {f x := x}. Elpi SameOrderImport. -Section S1. +Section S1. Variable X : Type. Local Instance f3d : A nat := {f x := x}. Global Instance f3e : A nat := {f x := x}. Global Instance f3f : A nat := {f x := x}. Elpi SameOrderImport. End S1. + + Elpi SameOrderImport. Section S2. diff --git a/apps/tc/tests/importOrder/f3d.v b/apps/tc/tests/importOrder/f3d.v index 0566660a4..84c4b3b45 100644 --- a/apps/tc/tests/importOrder/f3d.v +++ b/apps/tc/tests/importOrder/f3d.v @@ -13,10 +13,10 @@ Module M4'. Global Instance f3a : A nat := {f x := x}. - Section S1. + Section S1. Variable X : Type. Global Instance f3b : A nat := {f x := x}. - Section S1'. + Section S1'. Variable Y : Type. Global Instance f3c : A nat := {f x := x}. End S1'. @@ -24,7 +24,7 @@ Module M4'. Elpi SameOrderImport. - Section S2. + Section S2. Variable X : Type. Global Instance f3h T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}. End S2. End M4'. diff --git a/apps/tc/tests/importOrder/f3e.v b/apps/tc/tests/importOrder/f3e.v index 842bc909e..0de8467ce 100644 --- a/apps/tc/tests/importOrder/f3e.v +++ b/apps/tc/tests/importOrder/f3e.v @@ -8,14 +8,14 @@ Elpi SameOrderImport. Module M4'. Global Instance f3a : A nat := {f x := x}. - Section S1. + Section S1. Variable X : Type. Global Instance f3b : A nat := {f x := x}. - Section S1'. + Section S1'. Variable Y : Type. Global Instance f3c : A nat := {f x := x}. End S1'. End S1. - Section S2. + Section S2. Variable X : Type. Global Instance f3h T1 T2 `(A T1, A T2) : A (T1 * T2) | 100 := {f x := x}. End S2. End M4'. diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v index 144da73bd..eebeefc25 100644 --- a/apps/tc/theories/tc.v +++ b/apps/tc/theories/tc.v @@ -22,9 +22,10 @@ Elpi Db tc.db lp:{{ type classic search-mode. % contains the instances added to the DB - % associated to the list of sections they belong to + % associated to the list of sections variables (so that the clause is dropped + % when any goes out of scope) % :index (1) - pred instance o:list string, o:gref, o:gref. + pred instance o:list constant, o:gref, o:gref. % contains the typeclasses added to the DB :index (3) From 1cc9d669ce59961245666976fab70b5a3c88b7ed Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Wed, 25 Oct 2023 18:39:45 +0200 Subject: [PATCH 17/20] OK for Instances recompilation on section end --- apps/tc/elpi/compiler.elpi | 16 ++++++++------ apps/tc/elpi/tc_aux.elpi | 6 ++++-- apps/tc/tests/auto_compile.v | 37 +++++++++++++++++++++++++++++++++ apps/tc/tests/eqSimplDef.v | 11 +--------- apps/tc/tests/importOrder/f3c.v | 6 ------ apps/tc/tests/test.v | 1 + apps/tc/theories/tc.v | 5 ++--- 7 files changed, 55 insertions(+), 27 deletions(-) diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi index c13df14e1..59d0dc476 100644 --- a/apps/tc/elpi/compiler.elpi +++ b/apps/tc/elpi/compiler.elpi @@ -154,9 +154,13 @@ make-inst-graft Inst _NoPremises (after Grafting) :- % if (NoPremises = tt) (Grafting = RawGrafting) (Grafting is RawGrafting ^ "_complex"). Grafting = RawGrafting. +pred is_local i:string. +is_local "Local". +is_local _ :- coq.env.current-section-path [_ | _]. + pred add-inst i:gref, i:gref, i:string, i:int. add-inst Inst TC Locality Prio :- - coq.env.section SectionVars, + coq.env.current-section-path SectionPath, compile Inst _ TC Clause, % TODO: a clause is flexible if an instance is polimorphic (pglobal) not (var Clause), @@ -165,8 +169,8 @@ add-inst Inst TC Locality Prio :- (Prio1 = Prio), Graft is after (int_to_string Prio1), get-full-path Inst ClauseName, - if (Locality = "Local") (Visibility = [@local!]) (Visibility = [@global!]), - Visibility => (add-tc-db ClauseName Graft Clause, add-tc-db _ Graft (instance SectionVars Inst TC)). + if (is_local Locality) (Visibility = [@local!]) (Visibility = [@global!]), + Visibility => (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". @@ -176,7 +180,7 @@ add-inst Inst _ _ _ :- pred add-inst->db i:list gref, i:bool, i:gref. :name "add-inst->db:start" add-inst->db IgnoreClassDepL ForceAdd Inst :- - coq.env.section SectionVars, + coq.env.current-section-path SectionPath, get-sub-classes Inst Dep, warn-multiple-deps Inst Dep, if ((ForceAdd = tt; not (instance _ Inst _)), @@ -189,8 +193,8 @@ add-inst->db IgnoreClassDepL ForceAdd Inst :- get-full-path Inst ClauseName, if (is-local) (Visibility = [@local!]) (if (has-context-deps Inst) - (@local! => add-tc-db _ Graft (instance SectionVars Inst TC-of-Inst)) - (@global! => add-tc-db _ Graft (instance SectionVars Inst TC-of-Inst)), Visibility = [@global!]), + (@local! => add-tc-db _ Graft (instance SectionPath Inst TC-of-Inst)) + (@global! => add-tc-db _ Graft (instance [] Inst TC-of-Inst)), Visibility = [@global!]), Visibility => add-tc-db ClauseName Graft Clause ) true; @global! => add-tc-db _ _ (banned Inst), diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi index 4af76b19c..abea7e6f0 100644 --- a/apps/tc/elpi/tc_aux.elpi +++ b/apps/tc/elpi/tc_aux.elpi @@ -34,8 +34,10 @@ remove-eta2 A B :- !, pred instances-of-current-section o:list gref. :name "MySectionEndHook" instances-of-current-section InstsFiltered :- - std.findall (instance _ _ _) Insts, - std.map-filter Insts (x\r\ sigma X\ instance _ r _ = x, const X = r) InstsFiltered. + coq.env.current-section-path SectionPath, + std.findall (instance SectionPath _ _) Insts, + coq.env.section SectionVars, + std.map-filter Insts (x\r\ sigma X\ instance _ r _ = x, const X = r, not(std.mem SectionVars X)) InstsFiltered. pred is-instance-gr i:gref. is-instance-gr GR :- diff --git a/apps/tc/tests/auto_compile.v b/apps/tc/tests/auto_compile.v index 8c5b47adf..53b835fe8 100644 --- a/apps/tc/tests/auto_compile.v +++ b/apps/tc/tests/auto_compile.v @@ -40,4 +40,41 @@ Elpi Typecheck. Goal A (nat * (nat * bool)). apply _. Qed. +Module M. + Class B (T : nat). + Section A. + Instance X : B 1. Qed. + Goal B 1. apply _. Qed. + Global Instance Y : B 2. Qed. + Goal B 2. apply _. Qed. + End A. + Goal B 1. Proof. Fail apply _. Abort. + Goal B 2. Proof. apply _. Qed. + + Section B. + Variable V : nat. + Global Instance Z : `(B 0) -> B V. Qed. + Global Instance W : B 0. Qed. + End B. + + Goal B 0. apply _. Qed. + Goal B 10. apply _. Qed. +End M. + +Goal M.B 1. apply M.X. Qed. +Goal M.B 0. apply _. Qed. +Goal M.B 10. apply _. Qed. + +(* + TODO: @gares @FissoreD we have an unwanted warning: + constant tc-elpi.apps.tc.tests.auto_compile.M.tc-B has no declared type + since the considered instances come from a module. +*) +Elpi Query TC_solver lp:{{ + % Small test for instance order + sigma I L\ + std.findall (instance _ _ _) I, + std.map-filter I (x\y\ x = instance _ y {{:gref M.B}}) + [{{:gref M.W}}, {{:gref M.Y}}, {{:gref M.Z}}]. +}}. \ No newline at end of file diff --git a/apps/tc/tests/eqSimplDef.v b/apps/tc/tests/eqSimplDef.v index c2e1854d8..916cde199 100644 --- a/apps/tc/tests/eqSimplDef.v +++ b/apps/tc/tests/eqSimplDef.v @@ -8,13 +8,4 @@ Notation " x == y " := (eqb x y) (no associativity, at level 70). Global Instance eqU : Eqb unit := { eqb x y := true }. Global Instance eqB : Eqb bool := { eqb x y := if x then y else negb y }. Global Instance eqP {A B} `{Eqb A} `{Eqb B} : Eqb (A * B) := { - eqb x y := (fst x == fst y) && (snd x == snd y) }. -(* Global Instance eqN : Eqb nat := { - eqb := fix add (a: nat) b := match a, b with - | 0, 0 => true - | S a, S b => add a b - | _, _ => false - end }. - - -Check (forall n, n + n == 2 * n = true). *) \ No newline at end of file + eqb x y := (fst x == fst y) && (snd x == snd y) }. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f3c.v b/apps/tc/tests/importOrder/f3c.v index ecd6e7899..2c94dfcb2 100644 --- a/apps/tc/tests/importOrder/f3c.v +++ b/apps/tc/tests/importOrder/f3c.v @@ -24,12 +24,6 @@ Section S2. Elpi SameOrderImport. End S2. -Elpi Query add_instance lp:{{ - coq.warning "elpi.todo" "todo" "On section end, instances depending on - context variables should create an Event so that they are recompiled in elpi" -}}. - -(* TODO: Here the instance f3g should be readded... *) Elpi SameOrderImport. Section S3. diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v index e15c7603f..d95a858ce 100644 --- a/apps/tc/tests/test.v +++ b/apps/tc/tests/test.v @@ -1,6 +1,7 @@ From elpi.apps.tc.tests Require Import stdppInj. Elpi TC_solver. Set TimeRefine. Set TimeTC. Set Debug "elpitime". Elpi Accumulate TC_solver lp:{{ + shorten tc-elpi.apps.tc.tests.stdppInj.{tc-Inj}. :after "firstHook" tc-Inj A B RA RB {{@compose lp:A lp:A lp:A lp:FL lp:FL}} Sol :- !, tc-Inj A B RA RB FL Sol1, diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v index eebeefc25..144da73bd 100644 --- a/apps/tc/theories/tc.v +++ b/apps/tc/theories/tc.v @@ -22,10 +22,9 @@ Elpi Db tc.db lp:{{ type classic search-mode. % contains the instances added to the DB - % associated to the list of sections variables (so that the clause is dropped - % when any goes out of scope) + % associated to the list of sections they belong to % :index (1) - pred instance o:list constant, o:gref, o:gref. + pred instance o:list string, o:gref, o:gref. % contains the typeclasses added to the DB :index (3) From c2519802ef3710f353596fc28e2ba66262948376 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Thu, 26 Oct 2023 09:57:35 +0200 Subject: [PATCH 18/20] small test for locality in #[...] style --- apps/tc/tests/auto_compile.v | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/apps/tc/tests/auto_compile.v b/apps/tc/tests/auto_compile.v index 53b835fe8..178130b89 100644 --- a/apps/tc/tests/auto_compile.v +++ b/apps/tc/tests/auto_compile.v @@ -77,4 +77,16 @@ Elpi Query TC_solver lp:{{ std.findall (instance _ _ _) I, std.map-filter I (x\y\ x = instance _ y {{:gref M.B}}) [{{:gref M.W}}, {{:gref M.Y}}, {{:gref M.Z}}]. -}}. \ No newline at end of file +}}. + +Module S. + Class Cl (i: nat). + #[local] Instance Cl1 : Cl 1. Qed. + #[global] Instance Cl2 : Cl 2. Qed. + #[export] Instance Cl3 : Cl 3. Qed. +End S. + +Goal S.Cl 1 /\ S.Cl 2 /\ S.Cl 3. + split. all:cycle 1. split; apply _. + Fail apply _. +Abort. \ No newline at end of file From 4af2a2e8e4721a21d0d1e99c08e4c94ef1fc0818 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Thu, 26 Oct 2023 10:47:46 +0200 Subject: [PATCH 19/20] Correct behavior of #{export] --- apps/tc/elpi/compiler.elpi | 12 +++++++----- apps/tc/src/coq_elpi_tc_register.ml | 3 ++- apps/tc/tests/auto_compile.v | 9 ++++++++- 3 files changed, 17 insertions(+), 7 deletions(-) diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi index 59d0dc476..7bd7bd75a 100644 --- a/apps/tc/elpi/compiler.elpi +++ b/apps/tc/elpi/compiler.elpi @@ -154,9 +154,11 @@ make-inst-graft Inst _NoPremises (after Grafting) :- % if (NoPremises = tt) (Grafting = RawGrafting) (Grafting is RawGrafting ^ "_complex"). Grafting = RawGrafting. -pred is_local i:string. -is_local "Local". -is_local _ :- coq.env.current-section-path [_ | _]. +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 :- @@ -169,8 +171,8 @@ add-inst Inst TC Locality Prio :- (Prio1 = Prio), Graft is after (int_to_string Prio1), get-full-path Inst ClauseName, - if (is_local Locality) (Visibility = [@local!]) (Visibility = [@global!]), - Visibility => (add-tc-db ClauseName Graft Clause, add-tc-db _ Graft (instance SectionPath Inst TC)). + 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". diff --git a/apps/tc/src/coq_elpi_tc_register.ml b/apps/tc/src/coq_elpi_tc_register.ml index ae36db698..651270a29 100644 --- a/apps/tc/src/coq_elpi_tc_register.ml +++ b/apps/tc/src/coq_elpi_tc_register.ml @@ -30,7 +30,8 @@ let observer_instance ({locality; instance; info; class_name} : instance) : Coq_ let locality2elpi_string loc = let hint2string = function | Hints.Local -> "Local" - | Export | SuperGlobal -> "Global" in + | 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 diff --git a/apps/tc/tests/auto_compile.v b/apps/tc/tests/auto_compile.v index 178130b89..ccafa5eb7 100644 --- a/apps/tc/tests/auto_compile.v +++ b/apps/tc/tests/auto_compile.v @@ -86,7 +86,14 @@ Module S. #[export] Instance Cl3 : Cl 3. Qed. End S. +Elpi Override TC TC_solver None. Goal S.Cl 1 /\ S.Cl 2 /\ S.Cl 3. - split. all:cycle 1. split; apply _. +Proof. + split. all:cycle 1. + split. + apply _. + Fail apply _. + Import S. + apply _. Fail apply _. Abort. \ No newline at end of file From 6905031a62e673291f4a10b382afe053649c4cd3 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Thu, 26 Oct 2023 11:09:12 +0200 Subject: [PATCH 20/20] auto_compiler in tc.v --- apps/tc/elpi/compiler.elpi | 14 +++------- apps/tc/src/coq_elpi_tc_hook.mlg | 2 +- apps/tc/tests/auto_compile.v | 22 +--------------- apps/tc/tests/importOrder/sameOrderCommand.v | 27 +++----------------- apps/tc/theories/tc.v | 15 +++++++++++ 5 files changed, 24 insertions(+), 56 deletions(-) diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi index 7bd7bd75a..c1155c94a 100644 --- a/apps/tc/elpi/compiler.elpi +++ b/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) diff --git a/apps/tc/src/coq_elpi_tc_hook.mlg b/apps/tc/src/coq_elpi_tc_hook.mlg index 23c145756..cc621e5c4 100644 --- a/apps/tc/src/coq_elpi_tc_hook.mlg +++ b/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) } diff --git a/apps/tc/tests/auto_compile.v b/apps/tc/tests/auto_compile.v index ccafa5eb7..3ea473912 100644 --- a/apps/tc/tests/auto_compile.v +++ b/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. diff --git a/apps/tc/tests/importOrder/sameOrderCommand.v b/apps/tc/tests/importOrder/sameOrderCommand.v index 30685d60e..fb4770c1f 100644 --- a/apps/tc/tests/importOrder/sameOrderCommand.v +++ b/apps/tc/tests/importOrder/sameOrderCommand.v @@ -1,28 +1,6 @@ -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. @@ -30,3 +8,6 @@ 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. \ No newline at end of file diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v index 144da73bd..473945124 100644 --- a/apps/tc/theories/tc.v +++ b/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. \ No newline at end of file