version3: add tests

LPCIC · Oct 8, 2023 · ae83724 · ae83724
1 parent 9dae1eb
commit ae83724
Show file tree

Hide file tree

Showing 47 changed files with 3,799 additions and 115 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -18,7 +18,9 @@
 -R apps/eltac/tests    elpi.apps.eltac.tests
 -R apps/eltac/examples elpi.apps.eltac.examples
 -R apps/coercion/theories elpi.apps.coercion
--R apps/tc/theories elpi.apps.tc
+-R apps/tc/theories       elpi.apps.tc
+-R apps/tc/tests          elpi.apps.tc.tests
+-R apps/tc/elpi           elpi.apps.tc
 
 theories/elpi.v
 theories/wip/memoization.v

diff --git a/apps/coercion/theories/coercion.v b/apps/coercion/theories/coercion.v
@@ -23,3 +23,7 @@ solve (goal Ctx _ Ty Sol [trm V, trm VTy]) _ :- coercion Ctx V VTy Ty Sol.
 Elpi Accumulate Db coercion.db.
 Elpi Typecheck.
 Elpi CoercionFallbackTactic coercion.
+
+Elpi Query lp:{{
+  coq.warning "A" "B" "C"
+}}.
diff --git a/apps/tc/_CoqProject.test b/apps/tc/_CoqProject.test
@@ -1,11 +1,48 @@
 # Hack to see Coq-Elpi even if it is not installed yet
 -Q ../../theories elpi
 -I ../../src
--docroot elpi.apps
 
+-Q elpi     elpi.apps.tc
 -R theories elpi.apps
 -R tests    elpi.apps.tc.tests
+-I src
 
-tests/test_tc.v
+tests/premisesSort/sortCode.v
+tests/premisesSort/sort1.v
+# tests/premisesSort/sort2.v
+# tests/premisesSort/sort3.v
+# tests/premisesSort/sort4.v
+tests/included_proof.v
+# tests/goalDispatch.v
 
--I src
+# Import order of instances
+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/nobacktrack.v
+tests/removeEta.v
+tests/patternFragment.v
+tests/contextDeepHierarchy.v
+tests/mode_no_repetion.v
+# tests/test_commands_API.v
+tests/section_in_out.v
+tests/eqSimplDef.v
+tests/eqSimpl.v
+
+tests/injTest.v
+# Test with light version of base.v of stdpp
+tests/stdppInj.v
+tests/stdppInjClassic.v
+tests/test.v
+
+# Test with base.v of stdpp
+# tests/bigTest.v
diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi
@@ -177,7 +177,8 @@ add-inst->db IgnoreClassDepL ForceAdd 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), coq.warning "Not-added" "TC_solver" "Cannot compile " Inst.
+  true; @global! => add-tc-db _ _ (banned Inst), 
+  coq.warning "Not-added" "TC_solver" "Warning : Cannot compile " Inst "since it is pglobal".
 
 pred add-tc i:list gref, i:list gref, i:gref.
 add-tc IgnoreDepClassGR IgnoreInstsGR GR:-

diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
@@ -4,9 +4,9 @@ msolve L N :- !,
 pred my-refine i:term, i:goal, o:(list sealed-goal).
 % :if "time-refine"
 my-refine T G GL :- !, std.time(
-    % coq.reduction.eta-contract T T-eta-red,
-    T-eta-red = T,
-    refine.no_check T-eta-red G GL) FF, 
+    coq.reduction.eta-contract T T-eta-red,
+    % T-eta-red = T,
+    refine T-eta-red G GL) FF, 
   if (coq.option.get ["TimeRefine"] (coq.option.bool tt)) (coq.say "Refine Time" FF) true.
 % my-refine T G GL :- refine T G GL.
 

diff --git a/apps/tc/src/coq_elpi_tc_hook.ml b/apps/tc/src/coq_elpi_tc_hook.ml
@@ -2,6 +2,7 @@ let _ = Mltop.add_known_module "coq-elpi-tc.plugin"
 
 # 3 "src/coq_elpi_tc_hook.mlg"
 
+open Stdarg
 open Elpi
 open Elpi_plugin
 open Coq_elpi_arg_syntax
@@ -1414,10 +1415,8 @@ let resolve_all_evars depth unique env p oevd do_split fail =
           (* Typeclass resolution failed *)
           raise (Unresolved evd))
       with Unresolved evd' ->
-        if fail && (not do_split || is_mandatory (p evd') comp evd')
+        if fail && is_mandatory (p evd') comp evd'
         then (* Unable to satisfy the constraints. *)
-          let comp = if do_split then Some comp else None in
-          match comp with None -> raise (Invalid_argument "ciao") | Some comp ->
           error_unresolvable env evd' comp
         else (* Best effort: use the best found solution on this component *)
           docomp evd' comps
@@ -1531,53 +1530,6 @@ let autoapply c i =
       Proofview.Unsafe.tclEVARS sigma) end
 
 
-open Elpi
-open Elpi_plugin
-open Coq_elpi_vernacular
-
-
-let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
-  let loc = API.Ast.Loc.initial "(unknown)" in
-  let atts = [] in
-  let sigma, goal = Evarutil.new_evar env sigma expected in
-  let goal_evar, _ = EConstr.destEvar sigma goal in
-  let query ~depth state =
-    let state, (loc, q), gls =
-      Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [v; inferred])
-        ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in
-    let state, qatts = atts2impl loc ~depth state atts q in
-    let state = API.State.set Coq_elpi_builtins.tactic_mode state true in
-    state, (loc, qatts), gls
-  in
-  let cprogram, _ = get_and_compile program in
-  match run ~static_check:false cprogram (`Fun query) with
-  | API.Execute.Success solution ->
-     let gls = Evar.Set.singleton goal_evar in
-     let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in
-     if Evd.is_defined sigma goal_evar then Some (sigma, goal) else None
-  | API.Execute.NoMoreSteps
-  | API.Execute.Failure -> None
-  | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None
-
-let add_coercion_hook =
-  let coercion_hook_program = Summary.ref ~name:"elpi-coercion" None in
-  let coercion_hook env sigma ~flags v ~inferred ~expected =
-    match !coercion_hook_program with
-    | None -> None
-    | Some h -> elpi_coercion_hook h env sigma ~flags v ~inferred ~expected in
-  let name = "elpi-coercion" in
-  Coercion.register_hook ~name coercion_hook;
-  let inCoercion =
-    let cache program =
-      coercion_hook_program := Some program;
-      Coercion.activate_hook ~name in
-    let open Libobject in
-    declare_object
-    @@ superglobal_object_nodischarge "ELPI-COERCION1" ~cache ~subst:None in
-  fun program -> Lib.add_leaf (inCoercion program)
-
-
-
 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", 
@@ -1587,7 +1539,7 @@ let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-elpi-tc.plugin") ~
                                                                     Vernacextend.TyNil))))), 
          (let coqpp_body p
          atts = Vernacextend.vtdefault (fun () -> 
-# 1582 "src/coq_elpi_tc_hook.mlg"
+# 1534 "src/coq_elpi_tc_hook.mlg"
 
      let () = ignore_unknown_attributes atts in
      takeover false [] (snd p) 
@@ -1601,10 +1553,60 @@ let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-elpi-tc.plugin") ~
                                                                    Vernacextend.TyNil))))), 
          (let coqpp_body p
          atts = Vernacextend.vtdefault (fun () -> 
-# 1585 "src/coq_elpi_tc_hook.mlg"
+# 1537 "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))]
+         ?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 () -> 
+# 1542 "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 () -> 
+# 1545 "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 () -> 
+# 1548 "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))]
 
diff --git a/apps/tc/src/coq_elpi_tc_hook.mlg b/apps/tc/src/coq_elpi_tc_hook.mlg
@@ -1,6 +1,7 @@
 DECLARE PLUGIN "coq-elpi-tc.plugin"
 
 {
+open Stdarg
 open Elpi
 open Elpi_plugin
 open Coq_elpi_arg_syntax
@@ -1413,10 +1414,8 @@ let resolve_all_evars depth unique env p oevd do_split fail =
           (* Typeclass resolution failed *)
           raise (Unresolved evd))
       with Unresolved evd' ->
-        if fail && (not do_split || is_mandatory (p evd') comp evd')
+        if fail && is_mandatory (p evd') comp evd'
         then (* Unable to satisfy the constraints. *)
-          let comp = if do_split then Some comp else None in
-          match comp with None -> raise (Invalid_argument "ciao") | Some comp ->
           error_unresolvable env evd' comp
         else (* Best effort: use the best found solution on this component *)
           docomp evd' comps
@@ -1528,53 +1527,6 @@ let autoapply c i =
       let sigma = Typeclasses.make_unresolvables
           (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.evar_source (Evd.find_undefined sigma ev))))) sigma in
       Proofview.Unsafe.tclEVARS sigma) end
-
-
-open Elpi
-open Elpi_plugin
-open Coq_elpi_vernacular
-
-
-let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
-  let loc = API.Ast.Loc.initial "(unknown)" in
-  let atts = [] in
-  let sigma, goal = Evarutil.new_evar env sigma expected in
-  let goal_evar, _ = EConstr.destEvar sigma goal in
-  let query ~depth state =
-    let state, (loc, q), gls =
-      Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [v; inferred])
-        ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in
-    let state, qatts = atts2impl loc ~depth state atts q in
-    let state = API.State.set Coq_elpi_builtins.tactic_mode state true in
-    state, (loc, qatts), gls
-  in
-  let cprogram, _ = get_and_compile program in
-  match run ~static_check:false cprogram (`Fun query) with
-  | API.Execute.Success solution ->
-     let gls = Evar.Set.singleton goal_evar in
-     let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in
-     if Evd.is_defined sigma goal_evar then Some (sigma, goal) else None
-  | API.Execute.NoMoreSteps
-  | API.Execute.Failure -> None
-  | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None
-
-let add_coercion_hook =
-  let coercion_hook_program = Summary.ref ~name:"elpi-coercion" None in
-  let coercion_hook env sigma ~flags v ~inferred ~expected =
-    match !coercion_hook_program with
-    | None -> None
-    | Some h -> elpi_coercion_hook h env sigma ~flags v ~inferred ~expected in
-  let name = "elpi-coercion" in
-  Coercion.register_hook ~name coercion_hook;
-  let inCoercion =
-    let cache program =
-      coercion_hook_program := Some program;
-      Coercion.activate_hook ~name in
-    let open Libobject in
-    declare_object
-    @@ superglobal_object_nodischarge "ELPI-COERCION1" ~cache ~subst:None in
-  fun program -> Lib.add_leaf (inCoercion program)
-
 }
 
 VERNAC COMMAND EXTEND ElpiTypeclasses CLASSIFIED AS SIDEFF
@@ -1586,4 +1538,15 @@ VERNAC COMMAND EXTEND ElpiTypeclasses CLASSIFIED AS SIDEFF
      let () = ignore_unknown_attributes atts in
      takeover true [] (snd p) }
 
+
+| #[ atts = any_attribute ] [ "Elpi" "Override" "TC" qualified_name(p) "Only" ne_reference_list(cs) ] -> {
+     let () = ignore_unknown_attributes atts in
+     takeover false cs (snd p) }
+| #[ atts = any_attribute ] [ "Elpi" "Override" "TC" "+" reference_list(cs) ] -> {
+     let () = ignore_unknown_attributes atts in
+     takeover_add cs }
+| #[ atts = any_attribute ] [ "Elpi" "Override" "TC" "-" reference_list(cs) ] -> {
+     let () = ignore_unknown_attributes atts in
+     takeover_rm cs }
+
 END
diff --git a/apps/tc/tests/add_alias.v b/apps/tc/tests/add_alias.v
@@ -0,0 +1,30 @@
+From elpi.apps Require Import tc.
+Elpi Override TC TC_solver All.
+Elpi Debug "use-alias".
+
+Class foo (A : Type) := f : Type.
+
+Global Instance fooNat : foo nat := {f := nat}.
+Global Instance fooBool : foo bool := {f := bool}.
+
+Elpi AddClasses foo.
+Elpi AddInstances foo.
+
+Definition nat' := nat.
+
+
+Goal foo nat. apply _. Qed.
+Goal foo bool. apply _. Qed.
+Goal foo nat'. Fail apply _. Abort.
+
+Module A.
+  Elpi Accumulate TC_solver lp:{{
+    alias {{nat'}} {{nat}}.
+  }}.
+  Goal foo nat'. apply _. Qed.
+End A.
+
+Definition nat'' := nat'.
+
+Elpi AddAlias (nat'') (nat').
+Goal foo nat''. apply _. Qed.