From 729a2163c7f29573eeb66a4806a1147a490c0b88 Mon Sep 17 00:00:00 2001 From: qvermande Date: Thu, 2 Nov 2023 10:45:06 +0100 Subject: [PATCH 01/14] update hook (due to hook call update in coq) --- apps/coercion/src/coq_elpi_coercion_hook.mlg | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/apps/coercion/src/coq_elpi_coercion_hook.mlg b/apps/coercion/src/coq_elpi_coercion_hook.mlg index db082bdb4..f19565ab6 100644 --- a/apps/coercion/src/coq_elpi_coercion_hook.mlg +++ b/apps/coercion/src/coq_elpi_coercion_hook.mlg @@ -11,6 +11,13 @@ 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 (env, (sigma, expected)) = + match expected with + | Coercion.Type t -> (env, (sigma, t)) + | Coercion.Product -> let (sigma, (source, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible in + let (sigma, (target, _)) = let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (Context.annotR (Names.Name (Names.Id.of_string "__whatever")) , source)) env in Evarutil.new_type_evar env sigma Evd.univ_flexible in + (env, (sigma, EConstr.mkProd (Context.annotR (Names.Name (Names.Id.of_string "__whateverx")), source, target))) + | Coercion.Sort -> (env, Evarutil.new_Type sigma) in let sigma, goal = Evarutil.new_evar env sigma expected in let goal_evar, _ = EConstr.destEvar sigma goal in let query ~depth state = @@ -57,4 +64,4 @@ VERNAC COMMAND EXTEND ElpiCoercion CLASSIFIED AS SIDEFF let () = ignore_unknown_attributes atts in add_coercion_hook (snd p) } -END \ No newline at end of file +END From edc76b4e1d99f0969bd5c09c377dc8271fe5180b Mon Sep 17 00:00:00 2001 From: qvermande Date: Thu, 2 Nov 2023 16:41:23 +0100 Subject: [PATCH 02/14] add retyping after coercion (due to a modification in coq) --- apps/coercion/src/coq_elpi_coercion_hook.mlg | 32 ++++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/apps/coercion/src/coq_elpi_coercion_hook.mlg b/apps/coercion/src/coq_elpi_coercion_hook.mlg index f19565ab6..1e763e415 100644 --- a/apps/coercion/src/coq_elpi_coercion_hook.mlg +++ b/apps/coercion/src/coq_elpi_coercion_hook.mlg @@ -11,13 +11,13 @@ 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 (env, (sigma, expected)) = + let (env, sigma, expected, retype) = match expected with - | Coercion.Type t -> (env, (sigma, t)) - | Coercion.Product -> let (sigma, (source, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible in + | Coercion.Type t -> (env, sigma, t, false) + | Coercion.Product -> begin let (sigma, (source, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible in let (sigma, (target, _)) = let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (Context.annotR (Names.Name (Names.Id.of_string "__whatever")) , source)) env in Evarutil.new_type_evar env sigma Evd.univ_flexible in - (env, (sigma, EConstr.mkProd (Context.annotR (Names.Name (Names.Id.of_string "__whateverx")), source, target))) - | Coercion.Sort -> (env, Evarutil.new_Type sigma) in + (env, sigma, EConstr.mkProd (Context.annotR (Names.Name (Names.Id.of_string "__whateverx")), source, target), true) end + | Coercion.Sort -> let (sigma, t) = Evarutil.new_Type sigma in (env, sigma, t, true) in let sigma, goal = Evarutil.new_evar env sigma expected in let goal_evar, _ = EConstr.destEvar sigma goal in let query ~depth state = @@ -28,17 +28,17 @@ let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected = let state = API.State.set Coq_elpi_builtins.tactic_mode state true in state, (loc, qatts), gls in - match Interp.get_and_compile program with - | None -> None - | Some (cprogram, _) -> - match Interp.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 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 let t = if retype then Retyping.get_type_of env sigma goal else expected in Some (sigma, goal, t) + 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 From b2043818146006c3679512d85746d90904d43860 Mon Sep 17 00:00:00 2001 From: qvermande Date: Thu, 2 Nov 2023 16:49:20 +0100 Subject: [PATCH 03/14] added tests --- apps/coercion/tests/test_coercion.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/apps/coercion/tests/test_coercion.v b/apps/coercion/tests/test_coercion.v index 932605cb2..6a929a121 100644 --- a/apps/coercion/tests/test_coercion.v +++ b/apps/coercion/tests/test_coercion.v @@ -32,3 +32,20 @@ Check natmul R n : ringType_sort R. Check n : ringType_sort R. End TestNatMul. + +Elpi Accumulate coercion.db lp:{{ + +coercion _ V T E {{ Nat.mul lp:V }} :- + coq.unify-eq T {{ nat }} ok, + coq.unify-eq E {{ nat -> nat }} ok. + +coercion _ V T E {{ { m : nat | m < lp:V } }} :- + coq.unify-eq T {{ nat }} ok, + coq.unify-eq E {{ Type }} ok. + +}}. +Elpi Typecheck coercion. + +Check 3 2. +Check forall (x : 3), proj1_sig x < 3. + From b333090eacc5d3e1533d6d02ede1c26a17f3e6ec Mon Sep 17 00:00:00 2001 From: qvermande Date: Mon, 13 Nov 2023 15:37:02 +0100 Subject: [PATCH 04/14] fixed naming --- apps/coercion/src/coq_elpi_coercion_hook.mlg | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/apps/coercion/src/coq_elpi_coercion_hook.mlg b/apps/coercion/src/coq_elpi_coercion_hook.mlg index 1e763e415..ac3e6e079 100644 --- a/apps/coercion/src/coq_elpi_coercion_hook.mlg +++ b/apps/coercion/src/coq_elpi_coercion_hook.mlg @@ -15,8 +15,8 @@ let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected = match expected with | Coercion.Type t -> (env, sigma, t, false) | Coercion.Product -> begin let (sigma, (source, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible in - let (sigma, (target, _)) = let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (Context.annotR (Names.Name (Names.Id.of_string "__whatever")) , source)) env in Evarutil.new_type_evar env sigma Evd.univ_flexible in - (env, sigma, EConstr.mkProd (Context.annotR (Names.Name (Names.Id.of_string "__whateverx")), source, target), true) end + let (sigma, (target, _)) = let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (Context.annotR (Names.Name (Namegen.default_dependent_ident)) , source)) env in Evarutil.new_type_evar env sigma Evd.univ_flexible in + (env, sigma, EConstr.mkProd (Context.annotR (Names.Name (Namegen.default_type_ident)), source, target), true) end | Coercion.Sort -> let (sigma, t) = Evarutil.new_Type sigma in (env, sigma, t, true) in let sigma, goal = Evarutil.new_evar env sigma expected in let goal_evar, _ = EConstr.destEvar sigma goal in From 44b52f3887d64a86abf34e1322d52c4c571e9506 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 9 Jan 2024 13:23:20 +0100 Subject: [PATCH 05/14] wip --- apps/coercion/src/coq_elpi_coercion_hook.mlg | 24 +++++++------ apps/tc/elpi/solver.elpi | 2 +- coq-builtin.elpi | 2 ++ src/coq_elpi_builtins.ml | 38 +++++++++++--------- 4 files changed, 37 insertions(+), 29 deletions(-) diff --git a/apps/coercion/src/coq_elpi_coercion_hook.mlg b/apps/coercion/src/coq_elpi_coercion_hook.mlg index ac3e6e079..5794d3492 100644 --- a/apps/coercion/src/coq_elpi_coercion_hook.mlg +++ b/apps/coercion/src/coq_elpi_coercion_hook.mlg @@ -28,17 +28,19 @@ let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected = 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 let t = if retype then Retyping.get_type_of env sigma goal else expected in Some (sigma, goal, t) - else None - | API.Execute.NoMoreSteps - | API.Execute.Failure -> None - | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None + match Interp.get_and_compile program with + | None -> None + | Some (cprogram, _) -> + match Interp.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 let t = if retype then Retyping.get_type_of env sigma goal else expected in Some (sigma, goal, t) + 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 diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi index 8c6453e49..922161010 100644 --- a/apps/tc/elpi/solver.elpi +++ b/apps/tc/elpi/solver.elpi @@ -90,4 +90,4 @@ solve-aux (goal Ctx _ Ty Sol _ as G) GL :- ) (GL = [seal G]). -main _. \ No newline at end of file +main _. diff --git a/coq-builtin.elpi b/coq-builtin.elpi index d5a2085af..f9d0eb8b8 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -1395,6 +1395,8 @@ external pred coq.sigma.print . % If Ty is provided, then % the inferred type is unified (see unify-leq) with it. % Universe constraints are put in the constraint store. +% Supported attributes: +% - @no-tc! (default false, do not infer typeclasses) external pred coq.typecheck i:term, o:term, o:diagnostic. % [coq.typecheck-ty Ty U Diagnostic] typchecks a type Ty returning its diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 042f1d276..fc8f4c4dd 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -90,17 +90,18 @@ let with_pp_options o f = Detyping.print_evar_arguments := print_evar_arguments; raise reraise -let with_no_tc ~no_tc f sigma = - if no_tc then - let typeclass_evars = Evd.get_typeclass_evars sigma in - let sigma = Evd.set_typeclass_evars sigma Evar.Set.empty in +let with_no_tc ~no_tc env f sigma = + let sigma, rc = if no_tc then + let typeclass_evars = Evd.get_typeclass_evars sigma in + let sigma = Evd.set_typeclass_evars sigma Evar.Set.empty in let sigma, rc = f sigma in let typeclass_evars = Evar.Set.filter (fun x -> - try ignore (Evd.find_undefined sigma x); true - with Not_found -> false) typeclass_evars in + try ignore (Evd.find_undefined sigma x); true + with Not_found -> false) typeclass_evars in let sigma = Evd.set_typeclass_evars sigma typeclass_evars in sigma, rc - else f sigma + else f sigma in + sigma, rc let pr_econstr_env options env sigma t = with_pp_options options.pp (fun () -> @@ -3149,21 +3150,24 @@ is equivalent to Elpi Export TacName.|})))), Full (proof_context, {|typchecks a term T returning its type Ty. If Ty is provided, then the inferred type is unified (see unify-leq) with it. -Universe constraints are put in the constraint store.|})))), +Universe constraints are put in the constraint store. +Supported attributes: +- @no-tc! (default false, do not infer typeclasses)|})))), (fun t ety diag ~depth proof_context _ state -> + let no_tc = if proof_context.options.no_tc = Some true then true else false in try let sigma = get_sigma state in - let sigma, ty = Typing.type_of proof_context.env sigma t in + let sigma, ty = with_no_tc ~no_tc proof_context.env (fun sigma -> Typing.type_of proof_context.env sigma t) sigma in match ety with | Data ety -> - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL ty ety in - let state, assignments = set_current_sigma ~depth state sigma in - state, ?: None +! B.mkOK, assignments + let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL ty ety in + let state, assignments = set_current_sigma ~depth state sigma in + (state, ?: None +! B.mkOK, assignments) | NoData -> - let flags = Evarconv.default_flags_of TransparentState.full in - let sigma = Evarconv.solve_unif_constraints_with_heuristics ~flags ~with_ho:true proof_context.env sigma in - let state, assignments = set_current_sigma ~depth state sigma in - state, !: ty +! B.mkOK, assignments + let flags = Evarconv.default_flags_of TransparentState.full in + let sigma = Evarconv.solve_unif_constraints_with_heuristics ~flags ~with_ho:true proof_context.env sigma in + let state, assignments = set_current_sigma ~depth state sigma in + (state, !: ty +! B.mkOK, assignments) with Pretype_errors.PretypeError (env, sigma, err) -> match diag with | Data B.OK -> @@ -3613,7 +3617,7 @@ Supported attributes: let open Proofview in let open Notations in let focused_tac = Unsafe.tclSETGOALS [with_empty_state goal] <*> tactic in - with_no_tc ~no_tc (fun sigma -> + with_no_tc ~no_tc proof_context.env (fun sigma -> let _, pv = init sigma [] in let (), pv, _, _ = let vernac_state = Vernacstate.freeze_full_state () in From 3725a992a14326157365d15f9f44ebdd54504a7b Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Wed, 17 Jan 2024 14:55:25 +0100 Subject: [PATCH 06/14] add no-tc attribute support for typecheck and unification --- coq-builtin.elpi | 8 +++++++- src/coq_elpi_builtins.ml | 27 +++++++++++++++++++-------- 2 files changed, 26 insertions(+), 9 deletions(-) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index f9d0eb8b8..9885a89ff 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -1403,13 +1403,19 @@ external pred coq.typecheck i:term, o:term, o:diagnostic. % universe U. If U is provided, then % the inferred universe is unified (see unify-leq) with it. % Universe constraints are put in the constraint store. +% Supported attributes: +% - @no-tc! (default false, do not infer typeclasses) external pred coq.typecheck-ty i:term, o:sort, o:diagnostic. -% [coq.unify-eq A B Diagnostic] unifies the two terms +% [coq.unify-eq A B Diagnostic] unifies the two terms. +% Supported attributes: +% - @no-tc! (default false, do not infer typeclasses) external pred coq.unify-eq i:term, i:term, o:diagnostic. % [coq.unify-leq A B Diagnostic] unifies the two terms (with cumulativity, % if they are types) +% Supported attributes: +% - @no-tc! (default false, do not infer typeclasses) external pred coq.unify-leq i:term, i:term, o:diagnostic. % [coq.elaborate-skeleton T ETy E Diagnostic] elabotares T against the diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index fc8f4c4dd..87b2be760 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -3160,7 +3160,7 @@ Supported attributes: let sigma, ty = with_no_tc ~no_tc proof_context.env (fun sigma -> Typing.type_of proof_context.env sigma t) sigma in match ety with | Data ety -> - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL ty ety in + let sigma, _ = with_no_tc ~no_tc proof_context.env (fun sigma -> Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL ty ety, ()) sigma in let state, assignments = set_current_sigma ~depth state sigma in (state, ?: None +! B.mkOK, assignments) | NoData -> @@ -3185,14 +3185,17 @@ Supported attributes: Full (proof_context, {|typchecks a type Ty returning its universe U. If U is provided, then the inferred universe is unified (see unify-leq) with it. -Universe constraints are put in the constraint store.|})))), +Universe constraints are put in the constraint store. +Supported attributes: +- @no-tc! (default false, do not infer typeclasses)|})))), (fun ty es diag ~depth proof_context _ state -> + let no_tc = if proof_context.options.no_tc = Some true then true else false in try let sigma = get_sigma state in - let sigma, s = Typing.sort_of proof_context.env sigma ty in + let sigma, s = with_no_tc ~no_tc proof_context.env (fun sigma -> Typing.sort_of proof_context.env sigma ty) sigma in match es with | Data es -> - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL (EConstr.mkSort s) (EConstr.mkSort (EConstr.ESorts.make es)) in + let sigma, _ = with_no_tc ~no_tc proof_context.env (fun sigma -> Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL (EConstr.mkSort s) (EConstr.mkSort (EConstr.ESorts.make es)), ()) sigma in let state, assignments = set_current_sigma ~depth state sigma in state, !: es +! B.mkOK, assignments | NoData -> @@ -3214,11 +3217,15 @@ Universe constraints are put in the constraint store.|})))), CIn(term, "A", CIn(term, "B", InOut(B.ioarg B.diagnostic, "Diagnostic", - Full (proof_context, "unifies the two terms")))), + Full (proof_context, +{|unifies the two terms. +Supported attributes: +- @no-tc! (default false, do not infer typeclasses)|})))), (fun a b diag ~depth proof_context _ state -> + let no_tc = if proof_context.options.no_tc = Some true then true else false in let sigma = get_sigma state in try - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CONV a b in + let sigma, _ = with_no_tc ~no_tc proof_context.env (fun sigma -> Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CONV a b, ()) sigma in let state, assignments = set_current_sigma ~depth state sigma in state, !: B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> @@ -3235,11 +3242,15 @@ Universe constraints are put in the constraint store.|})))), CIn(term, "A", CIn(term, "B", InOut(B.ioarg B.diagnostic, "Diagnostic", - Full (proof_context, "unifies the two terms (with cumulativity, if they are types)")))), + Full (proof_context, +{|unifies the two terms (with cumulativity, if they are types) +Supported attributes: +- @no-tc! (default false, do not infer typeclasses)|})))), (fun a b diag ~depth proof_context _ state -> + let no_tc = if proof_context.options.no_tc = Some true then true else false in let sigma = get_sigma state in try - let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL a b in + let sigma, _ = with_no_tc ~no_tc proof_context.env (fun sigma -> Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL a b, ()) sigma in let state, assignments = set_current_sigma ~depth state sigma in state, !: B.mkOK, assignments with Pretype_errors.PretypeError (env, sigma, err) -> From a58c201538507b8c549f902516f72f3d04c1e5e7 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Thu, 11 Jan 2024 16:43:40 +0100 Subject: [PATCH 07/14] Add of the expose grafting + test --- _CoqProject.test | 1 + tests/test_grafting.v | 37 +++++++++++++++++++++++++++++++++++++ 2 files changed, 38 insertions(+) create mode 100644 tests/test_grafting.v diff --git a/_CoqProject.test b/_CoqProject.test index 71e43c409..8510ba804 100644 --- a/_CoqProject.test +++ b/_CoqProject.test @@ -55,3 +55,4 @@ tests/test_link_order_import3.v tests/test_query_extra_dep.v tests/test_toposort.v tests/test_synterp.v +tests/test_grafting.v \ No newline at end of file diff --git a/tests/test_grafting.v b/tests/test_grafting.v new file mode 100644 index 000000000..4a536edb0 --- /dev/null +++ b/tests/test_grafting.v @@ -0,0 +1,37 @@ +From elpi Require Import elpi. + +Elpi Db my_db lp:{{ + pred graft_me o:int. + + :name "graft_me0" + graft_me 0. +}}. + +Elpi Command test_wanted_order. +Elpi Accumulate Db my_db. +Elpi Accumulate lp:{{ + main L1 :- + std.findall (graft_me _) L2, + std.forall2 L1 L2 (x\y\ sigma X\ graft_me X = y, int X = x). +}}. +Elpi Typecheck. + +Elpi test_wanted_order 0. + +Elpi Query lp:{{ + coq.elpi.accumulate _ "my_db" (clause "graft_me2" (after "graft_me0") (graft_me 2)). +}}. + +Elpi test_wanted_order 0 2. + +Elpi Query lp:{{ + coq.elpi.accumulate _ "my_db" (clause "graft_me1" (before "graft_me2") (graft_me 1)). +}}. + +Elpi test_wanted_order 0 1 2. + +Elpi Query lp:{{ + coq.elpi.accumulate _ "my_db" (clause _ (replace "graft_me2") (graft_me 3)). +}}. + +Elpi test_wanted_order 0 1 3. From 402b410425ffde786705ee8ee2a23d8a95d161e2 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 6 Feb 2024 14:12:15 +0100 Subject: [PATCH 08/14] complete and compiles --- apps/cs/src/coq_elpi_cs_hook.mlg | 53 ++++++++++------ apps/cs/src/evarconv_hacked.ml | 103 ++++++++++++++++++++++++------- apps/cs/tests/test_cs.v | 16 ++--- apps/cs/theories/cs.v | 23 +++---- 4 files changed, 135 insertions(+), 60 deletions(-) diff --git a/apps/cs/src/coq_elpi_cs_hook.mlg b/apps/cs/src/coq_elpi_cs_hook.mlg index 7d7a65c12..d25968d6e 100644 --- a/apps/cs/src/coq_elpi_cs_hook.mlg +++ b/apps/cs/src/coq_elpi_cs_hook.mlg @@ -10,24 +10,37 @@ module Evarconv = Evarconv module Evarconv_hacked = Evarconv_hacked -let elpi_cs_hook program env sigma lhs rhs = - let (lhead, largs) = EConstr.decompose_app sigma lhs in - let (rhead, rargs) = EConstr.decompose_app sigma rhs in - if (EConstr.isConst sigma lhead && Structures.Structure.is_projection (fst (EConstr.destConst sigma lhead))) || - (EConstr.isConst sigma rhead && Structures.Structure.is_projection (fst (EConstr.destConst sigma rhead))) - then begin +let elpi_cs_hook program env sigma (t1, sk1) (t2, sk2) = let loc = API.Ast.Loc.initial "(unknown)" in let atts = [] in - (*let sigma, ty = Typing.type_of env sigma lhs in*) - let sigma, (ty, _) = Evarutil.new_type_evar env sigma Evd.univ_flexible in - let { Coqlib.eq } = Coqlib.build_coq_eq_data () in - let sigma, eq = EConstr.fresh_global env sigma eq in - let t = EConstr.mkApp (eq,[|ty;lhs;rhs|]) in - let sigma, goal = Evarutil.new_evar env sigma t in + let (proji, u), arg = + match Termops.global_app_of_constr sigma t1 with + | (Names.GlobRef.ConstRef proji, u), arg -> (proji, u), arg + | _ -> raise Not_found in + let structure = Structures.Structure.find_from_projection proji in + let params1, c1, extra_args1 = + match arg with + | Some c -> (* A primitive projection applied to c *) + let ty = Retyping.get_type_of ~lax:true env sigma c in + let (i,u), ind_args = + (* Are we sure that ty is not an evar? *) + Inductiveops.find_mrectype env sigma ty + in ind_args, c, sk1 + | None -> + match Reductionops.Stack.strip_n_app structure.nparams sk1 with + | Some (params1, c1, extra_args1) -> (Option.get @@ Reductionops.Stack.list_of_app_stack params1), c1, extra_args1 + | _ -> raise Not_found in + let sk2, extra_args2 = + if List.length sk2 < List.length extra_args1 then raise Not_found + else match Reductionops.Stack.strip_n_app (List.length sk2 - List.length extra_args1) sk2 with + | None -> raise Not_found + | Some (l',el,s') -> ((Option.get @@ Reductionops.Stack.list_of_app_stack l') @ [el],s') in + let rhs = Reductionops.Stack.zip sigma (t2, Reductionops.Stack.append_app_list sk2 Reductionops.Stack.empty) in + let sigma, goal = Evarutil.new_evar env sigma (Retyping.get_type_of env sigma c1) 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 []) + Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [EConstr.mkApp (EConstr.mkConstU (proji, EConstr.EInstance.empty), Array.of_list params1); rhs]) ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in let state, qatts = atts2impl loc Summary.Stage.Interp ~depth state atts q in let state = API.State.set Coq_elpi_builtins.tactic_mode state true in @@ -40,18 +53,20 @@ let elpi_cs_hook program env sigma lhs rhs = | API.Execute.Success solution -> let gls = Evar.Set.singleton goal_evar in let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in - let ty_evar, _ = EConstr.destEvar sigma ty in - Some (Evd.remove (Evd.remove sigma ty_evar) goal_evar) + if Evd.is_defined sigma goal_evar then + let lhs = Reductionops.whd_all env sigma (EConstr.mkApp (EConstr.mkConstU (proji, EConstr.EInstance.empty), Array.of_list (params1 @ [goal]))) in + let h, sk1 = EConstr.decompose_app sigma lhs in + let h2, sk2 = EConstr.decompose_app sigma rhs in + let _, params = EConstr.decompose_app sigma (Retyping.get_type_of env sigma goal) in + Some (sigma, (h, h2), goal, [], (Array.to_list params, params1), (Array.to_list sk1, Array.to_list sk2), (extra_args1, extra_args2), c1, (None, rhs)) + else None | API.Execute.NoMoreSteps | API.Execute.Failure -> None | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None - end - else None let add_cs_hook = let cs_hook_program = Summary.ref ~name:"elpi-cs" None in let cs_hook env sigma proj pat = - Feedback.msg_info (Pp.str "run"); match !cs_hook_program with | None -> None | Some h -> elpi_cs_hook h env sigma proj pat in @@ -60,8 +75,6 @@ let add_cs_hook = let inCs = let cache program = cs_hook_program := Some program; - Feedback.msg_info (Pp.str "activate"); - Evarconv_hacked.activate_hook ~name in let open Libobject in declare_object diff --git a/apps/cs/src/evarconv_hacked.ml b/apps/cs/src/evarconv_hacked.ml index 79f8ce536..52f078665 100644 --- a/apps/cs/src/evarconv_hacked.ml +++ b/apps/cs/src/evarconv_hacked.ml @@ -488,7 +488,10 @@ let rec ise_stack2 no_app env evd f sk1 sk2 = |_, _ -> fail (UnifFailure (i,(* Maybe improve: *) NotSameHead)) in ise_rev_stack2 false evd (List.rev sk1) (List.rev sk2) -type hook = Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t -> Evd.evar_map option +type hook = Environ.env -> Evd.evar_map -> (EConstr.t * Reductionops.Stack.t) -> (EConstr.t * Reductionops.Stack.t) -> (Evd.evar_map * (EConstr.t * EConstr.t) * EConstr.t * EConstr.t list * +(EConstr.t list * EConstr.t list) * (EConstr.t list * EConstr.t list) * +(Reductionops.Stack.t * Reductionops.Stack.t) * EConstr.constr * +(int option * EConstr.constr)) option let all_hooks = ref (CString.Map.empty : hook CString.Map.t) @@ -591,6 +594,38 @@ let infer_conv_noticing_evars ~pb ~ts env sigma t1 t2 = if !has_evar then None else Some (UnifFailure (sigma, UnifUnivInconsistency e)) +let pr_econstr = ref (fun _ _ _ -> Pp.str "unable to print econstr") + +(* TODO: move to a proper place *) +let rec split_at n acc l = + if n = 0 then (List.rev acc, l) + else match l with + | [] -> (List.rev acc, l) + | h :: t -> split_at (n-1) (h :: acc) t +let split_at n l = split_at n [] l + +let try_simplify_proj_construct flags env evd v k sk = + match k with (* try unfolding an applied projection on the rhs *) + | Proj (p, _, c) -> begin + let c = whd_all env evd c in (* reduce argument *) + try let (hd, args) = destApp evd c in + if isConstruct evd hd then Some (whd_nored_state env evd (args.(Projection.npars p + Projection.arg p), sk)) + else None + with _ -> None + end + | Const (cn, _) when Structures.Structure.is_projection cn -> begin + match split_at (Structures.Structure.projection_nparams cn) (Option.default [] (Stack.list_of_app_stack sk)) with + | (_, []) -> None + | (_, c :: _) -> begin + let c = whd_all env evd c in + try let (hd, _) = destApp evd c in + if isConstruct evd hd then + Some (whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd (v,sk)) + else None + with _ -> None + end end + | _ -> None + let rec evar_conv_x flags env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in let term2 = whd_head_evar evd term2 in @@ -923,7 +958,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty flex_maybeflex false ev2 appr2 appr1 v1 | MaybeFlexible v1, MaybeFlexible v2 -> begin - match EConstr.kind evd term1, EConstr.kind evd term2 with + let k1 = EConstr.kind evd term1 in + let k2 = EConstr.kind evd term2 in + begin + match k1, k2 with | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) -> let f1 i = (* FO *) ise_and i @@ -996,16 +1034,22 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty | None -> UnifFailure (i,NotSameHead) and f2 i = - (try + (match try_simplify_proj_construct flags env evd v1 k1 sk1, try_simplify_proj_construct flags env evd v2 k2 sk2 with + | Some x1, Some x2 -> UnifFailure (i,NoCanonicalStructure) + | Some x1, None -> UnifFailure (i,NoCanonicalStructure) + | None, Some x2 -> UnifFailure (i,NoCanonicalStructure) + | _, _ -> (try if not flags.with_cs then raise Not_found else conv_record flags env (try check_conv_record env i appr1 appr2 - with Not_found -> check_conv_record env i appr2 appr1) - with Not_found -> - let sigma = i in - match apply_hooks env sigma (Stack.zip sigma appr1) (Stack.zip sigma appr2) with - | Some sigma -> Success sigma - | None -> UnifFailure (i,NoCanonicalStructure)) + with Not_found -> begin match (apply_hooks env evd appr1 appr2) with + | Some r -> r + | None -> begin try check_conv_record env i appr2 appr1 + with Not_found -> begin match (apply_hooks env evd appr2 appr1) with + | Some r -> r + | None -> raise Not_found + end end end) + with Not_found -> UnifFailure (i,NoCanonicalStructure))) and f3 i = (* heuristic: unfold second argument first, exception made if the first argument is a beta-redex (expand a constant @@ -1044,7 +1088,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty flags.open_ts env i (v2,sk2)) in ise_try evd [f1; f2; f3] - end + end end | Rigid, Rigid when EConstr.isLambda evd term1 && EConstr.isLambda evd term2 -> let (na1,c1,c'1) = EConstr.destLambda evd term1 in @@ -1062,14 +1106,21 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1 | MaybeFlexible v1, Rigid -> + let k1 = EConstr.kind evd term1 in begin + let () = debug_unification (fun () -> Pp.(v 0 (str "v1 maybeflexible against rigid" ++ !pr_econstr env evd v1 ++ cut ()))) in + match try_simplify_proj_construct flags env evd v1 k1 sk1 with + | Some x1 -> evar_eqappr_x flags env evd pbty x1 appr2 + | None -> let f3 i = (try if not flags.with_cs then raise Not_found - else conv_record flags env (check_conv_record env i appr1 appr2) - with Not_found -> let sigma = i in - match apply_hooks env sigma (Stack.zip sigma appr1) (Stack.zip sigma appr2) with - | Some sigma -> Success sigma - | None -> UnifFailure (i,NoCanonicalStructure)) + else conv_record flags env ( + try check_conv_record env i appr1 appr2 with + | Not_found -> begin match apply_hooks env evd appr1 appr2 with + | Some r -> r + | None -> raise Not_found + end) + with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f4 i = evar_eqappr_x flags env i pbty @@ -1078,22 +1129,31 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty appr2 in ise_try evd [f3; f4] + end | Rigid, MaybeFlexible v2 -> + let k2 = EConstr.kind evd term2 in begin + let () = debug_unification (fun () -> Pp.(v 0 (str "rigid against v2 maybeflexible" ++ !pr_econstr env evd v2 ++ cut ()))) in + match try_simplify_proj_construct flags env evd v2 k2 sk2 with + | Some x2 -> let () = debug_unification (fun () -> Pp.(v 0 (str "reduced to" ++ !pr_econstr env evd (let (x, _) = x2 in x)))) in evar_eqappr_x flags env evd pbty appr1 x2 + | None -> let f3 i = (try if not flags.with_cs then raise Not_found - else conv_record flags env (check_conv_record env i appr2 appr1) - with Not_found -> let sigma = i in - match apply_hooks env sigma (Stack.zip sigma appr1) (Stack.zip sigma appr2) with - | Some sigma -> Success sigma - | None -> UnifFailure (i,NoCanonicalStructure)) + else conv_record flags env ( + try check_conv_record env i appr2 appr1 with + | Not_found -> begin match apply_hooks env evd appr1 appr2 with + | Some r -> r + | None -> raise Not_found + end) + with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f4 i = evar_eqappr_x flags env i pbty appr1 (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (v2,sk2)) in ise_try evd [f3; f4] + end (* Eta-expansion *) | Rigid, _ when isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 -> @@ -1277,8 +1337,7 @@ and conv_record flags env (evd,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c (fun i -> evar_conv_x flags env i CONV c1 app); (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2); test; - (fun i -> evar_conv_x flags env i CONV h2 - (fst (decompose_app i (substl ks h))))] + (fun i -> evar_conv_x flags env i CONV h2 (fst (decompose_app i (substl ks h))))] else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor flags env evd ((ind, i), u) sk1 (term2,sk2) = diff --git a/apps/cs/tests/test_cs.v b/apps/cs/tests/test_cs.v index 5cf69a562..527abf45a 100644 --- a/apps/cs/tests/test_cs.v +++ b/apps/cs/tests/test_cs.v @@ -3,19 +3,21 @@ From Coq Require Import Bool. Elpi Override CS All. -Structure S : Type := - { sort :> Type }. +Structure S (T : Type) : Type := + { sort :> T -> T }. -Elpi Accumulate cs.db lp:{{ +Elpi Accumulate tc.db lp:{{ -cs _ {{ sort lp:Sol }} {{ nat }} :- - Sol = {{ Build_S nat }}. +cs _ A B :- coq.say "cs" A B, fail. +cs _ {{ sort lp:T lp:Sol }} {{ @id lp:T }} :- + Sol = {{ Build_S lp:T (@id lp:T) }}. }}. Elpi Typecheck canonical_solution. Check 1. -Check eq_refl _ : (sort _) = nat. +Check eq_refl _ : (sort nat _) = @id nat. +Check eq_refl _ : (sort nat _) 1 = @id nat 1. Definition nat1 := nat. Check 2. Check eq_refl _ : (sort _) = nat1. @@ -26,7 +28,7 @@ Check 4. Check eq_refl _ : (sort1 _) = nat1. -Elpi Accumulate cs.db lp:{{ +Elpi Accumulate tc.db lp:{{ cs _ {{ sort lp:Sol }} {{ bool }} :- % typing is wired in, do we want this? diff --git a/apps/cs/theories/cs.v b/apps/cs/theories/cs.v index 0d38897a9..33eb5af46 100644 --- a/apps/cs/theories/cs.v +++ b/apps/cs/theories/cs.v @@ -1,27 +1,28 @@ Declare ML Module "coq-elpi-cs.plugin". -From elpi Require Import elpi. +From elpi Require Import elpi tc. -Elpi Db cs.db lp:{{ +Elpi Accumulate tc.db lp:{{ - % predicate [canonical-solution Ctx Lhs Rhs] used to unify Lhs with Rhs, with +% predicate [cs Ctx Proj Rhs Sol] used to find Sol such that Proj Sol = Rhs, where % - [Ctx] is the context -% - [Lhs] and [Rhs] are the terms to unify +% - [Proj] is the projector of some structure, applied to the structure's parameters if any +% - [Rhs] the term to find a structure on. :index (0 6 6) -pred cs i:goal-ctx, o:term, o:term. +pred cs i:goal-ctx, i:term, i:term, o:term. }}. Elpi Tactic canonical_solution. -Elpi Accumulate lp:{{ +Elpi Accumulate Db tc.db. +Elpi Accumulate canonical_solution lp:{{ -solve (goal Ctx _ {{ @eq lp:T lp:Lhs lp:Rhs }} _P []) _ :- - cs Ctx Lhs Rhs, - % std.assert! (P = {{ eq_refl lp:Lhs }}) "cs: wrong solution". +solve (goal Ctx _ _Ty Sol [trm Proj, trm Rhs]) _ :- + cs Ctx Proj Rhs Sol, + % std.assert! (P = {{ eq_refl lp:Lhs }}) "cs: wrong solution". true. }}. -Elpi Accumulate Db cs.db. -Elpi Typecheck. +Elpi Typecheck canonical_solution. Elpi CSFallbackTactic canonical_solution. From 1d39142bc005299c5979201e5bdca9dbf191d876 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 8 Feb 2024 10:19:38 +0100 Subject: [PATCH 09/14] new cs hook --- apps/cs/src/coq_elpi_cs_hook.mlg | 23 +++++++++++++++-------- apps/cs/src/evarconv_hacked.ml | 11 ++++++----- apps/cs/tests/test_cs.v | 4 ++-- apps/cs/theories/cs.v | 6 +++--- 4 files changed, 26 insertions(+), 18 deletions(-) diff --git a/apps/cs/src/coq_elpi_cs_hook.mlg b/apps/cs/src/coq_elpi_cs_hook.mlg index d25968d6e..284952e3b 100644 --- a/apps/cs/src/coq_elpi_cs_hook.mlg +++ b/apps/cs/src/coq_elpi_cs_hook.mlg @@ -13,11 +13,14 @@ module Evarconv_hacked = Evarconv_hacked let elpi_cs_hook program env sigma (t1, sk1) (t2, sk2) = let loc = API.Ast.Loc.initial "(unknown)" in let atts = [] in + let () = Feedback.msg_info (Pp.str "cs hook start") in let (proji, u), arg = match Termops.global_app_of_constr sigma t1 with | (Names.GlobRef.ConstRef proji, u), arg -> (proji, u), arg - | _ -> raise Not_found in + | (proji, _), _ -> let () = Feedback.msg_info Pp.(str "proj is not const" ++ Names.GlobRef.print proji) in raise Not_found in + let () = Feedback.msg_info (Pp.str "cs hook got proj") in let structure = Structures.Structure.find_from_projection proji in + let () = Feedback.msg_info (Pp.str "cs hook got structure") in let params1, c1, extra_args1 = match arg with | Some c -> (* A primitive projection applied to c *) @@ -30,11 +33,13 @@ let elpi_cs_hook program env sigma (t1, sk1) (t2, sk2) = match Reductionops.Stack.strip_n_app structure.nparams sk1 with | Some (params1, c1, extra_args1) -> (Option.get @@ Reductionops.Stack.list_of_app_stack params1), c1, extra_args1 | _ -> raise Not_found in + let () = Feedback.msg_info Pp.(str "cs hook got params & arg " ++ int (List.length sk2) ++ str " " ++ int (List.length extra_args1)) in let sk2, extra_args2 = - if List.length sk2 < List.length extra_args1 then raise Not_found - else match Reductionops.Stack.strip_n_app (List.length sk2 - List.length extra_args1) sk2 with + if List.length sk2 = List.length extra_args1 then [], sk2 + else match Reductionops.Stack.strip_n_app (List.length sk2 - List.length extra_args1 - 1) sk2 with | None -> raise Not_found | Some (l',el,s') -> ((Option.get @@ Reductionops.Stack.list_of_app_stack l') @ [el],s') in + let () = Feedback.msg_info (Pp.str "cs hook split t2") in let rhs = Reductionops.Stack.zip sigma (t2, Reductionops.Stack.append_app_list sk2 Reductionops.Stack.empty) in let sigma, goal = Evarutil.new_evar env sigma (Retyping.get_type_of env sigma c1) in let goal_evar, _ = EConstr.destEvar sigma goal in @@ -45,12 +50,13 @@ let elpi_cs_hook program env sigma (t1, sk1) (t2, sk2) = let state, qatts = atts2impl loc Summary.Stage.Interp ~depth state atts q in let state = API.State.set Coq_elpi_builtins.tactic_mode state true in state, (loc, qatts), gls - in + in let () = Feedback.msg_info Pp.(str "compile solver") in match Interp.get_and_compile program with | None -> None | Some (cprogram, _) -> - match Interp.run ~static_check:false cprogram (`Fun query) with - | API.Execute.Success solution -> + let () = Feedback.msg_info Pp.(str "run solver\n") in + begin try match Interp.run ~static_check:false cprogram (`Fun query) with + | API.Execute.Success solution -> let () = Feedback.msg_info Pp.(str "found solution\n") in 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 @@ -61,8 +67,9 @@ let elpi_cs_hook program env sigma (t1, sk1) (t2, sk2) = Some (sigma, (h, h2), goal, [], (Array.to_list params, params1), (Array.to_list sk1, Array.to_list sk2), (extra_args1, extra_args2), c1, (None, rhs)) else None | API.Execute.NoMoreSteps - | API.Execute.Failure -> None - | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None + | API.Execute.Failure -> let () = Feedback.msg_info Pp.(str "solver failed\n") in None + with e -> let () = Feedback.msg_info Pp.(str "solver crashed\n") in raise e end + | exception e -> let () = Feedback.msg_info Pp.(str "compiler crashed\n") in raise e let add_cs_hook = let cs_hook_program = Summary.ref ~name:"elpi-cs" None in diff --git a/apps/cs/src/evarconv_hacked.ml b/apps/cs/src/evarconv_hacked.ml index 52f078665..a36878385 100644 --- a/apps/cs/src/evarconv_hacked.ml +++ b/apps/cs/src/evarconv_hacked.ml @@ -1042,10 +1042,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty if not flags.with_cs then raise Not_found else conv_record flags env (try check_conv_record env i appr1 appr2 - with Not_found -> begin match (apply_hooks env evd appr1 appr2) with + with Not_found -> begin match (apply_hooks env i appr1 appr2) with | Some r -> r | None -> begin try check_conv_record env i appr2 appr1 - with Not_found -> begin match (apply_hooks env evd appr2 appr1) with + with Not_found -> begin match (apply_hooks env i appr2 appr1) with | Some r -> r | None -> raise Not_found end end end) @@ -1116,7 +1116,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty if not flags.with_cs then raise Not_found else conv_record flags env ( try check_conv_record env i appr1 appr2 with - | Not_found -> begin match apply_hooks env evd appr1 appr2 with + | Not_found -> begin match apply_hooks env i appr1 appr2 with | Some r -> r | None -> raise Not_found end) @@ -1142,10 +1142,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty if not flags.with_cs then raise Not_found else conv_record flags env ( try check_conv_record env i appr2 appr1 with - | Not_found -> begin match apply_hooks env evd appr1 appr2 with + | Not_found -> begin let () = debug_unification (fun () -> Pp.(v 0 (str "ask cs hook"))) in match apply_hooks env i appr2 appr1 with | Some r -> r | None -> raise Not_found - end) + end + | e -> let () = Feedback.msg_info Pp.(str "cs hook crashed") in failwith "argh") with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f4 i = evar_eqappr_x flags env i pbty appr1 diff --git a/apps/cs/tests/test_cs.v b/apps/cs/tests/test_cs.v index 527abf45a..48ee53ba1 100644 --- a/apps/cs/tests/test_cs.v +++ b/apps/cs/tests/test_cs.v @@ -6,7 +6,7 @@ Elpi Override CS All. Structure S (T : Type) : Type := { sort :> T -> T }. -Elpi Accumulate tc.db lp:{{ +Elpi Accumulate cs.db lp:{{ cs _ A B :- coq.say "cs" A B, fail. cs _ {{ sort lp:T lp:Sol }} {{ @id lp:T }} :- @@ -28,7 +28,7 @@ Check 4. Check eq_refl _ : (sort1 _) = nat1. -Elpi Accumulate tc.db lp:{{ +Elpi Accumulate cs.db lp:{{ cs _ {{ sort lp:Sol }} {{ bool }} :- % typing is wired in, do we want this? diff --git a/apps/cs/theories/cs.v b/apps/cs/theories/cs.v index 33eb5af46..f7f04660a 100644 --- a/apps/cs/theories/cs.v +++ b/apps/cs/theories/cs.v @@ -1,7 +1,7 @@ Declare ML Module "coq-elpi-cs.plugin". -From elpi Require Import elpi tc. +From elpi Require Import elpi. -Elpi Accumulate tc.db lp:{{ +Elpi Db cs.db lp:{{ % predicate [cs Ctx Proj Rhs Sol] used to find Sol such that Proj Sol = Rhs, where % - [Ctx] is the context @@ -15,7 +15,7 @@ pred cs i:goal-ctx, i:term, i:term, o:term. Elpi Tactic canonical_solution. -Elpi Accumulate Db tc.db. +Elpi Accumulate Db cs.db. Elpi Accumulate canonical_solution lp:{{ solve (goal Ctx _ _Ty Sol [trm Proj, trm Rhs]) _ :- From ea4f6d3219d0237ff4d181f34874ae5d080c1f20 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 9 Jan 2024 10:36:24 +0100 Subject: [PATCH 10/14] fix Elpi Typecheck program --- _CoqProject.test | 3 ++- src/coq_elpi_vernacular.ml | 2 +- tests/test_checker.v | 19 +++++++++++++++++++ 3 files changed, 22 insertions(+), 2 deletions(-) create mode 100644 tests/test_checker.v diff --git a/_CoqProject.test b/_CoqProject.test index 8510ba804..266fcb992 100644 --- a/_CoqProject.test +++ b/_CoqProject.test @@ -55,4 +55,5 @@ tests/test_link_order_import3.v tests/test_query_extra_dep.v tests/test_toposort.v tests/test_synterp.v -tests/test_grafting.v \ No newline at end of file +tests/test_grafting.v +tests/test_checker.v diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index dc41a2119..ea578e236 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -286,7 +286,7 @@ let set_current_program n = current_program := Some n let typecheck_program ?program () = - match !current_program with + match Option.append program !current_program with | None -> () | Some program -> let elpi = P.ensure_initialized () in diff --git a/tests/test_checker.v b/tests/test_checker.v new file mode 100644 index 000000000..e39000196 --- /dev/null +++ b/tests/test_checker.v @@ -0,0 +1,19 @@ +From elpi Require Import elpi. + +Elpi Command foo. +Elpi Accumulate lp:{{ +pred p i:int. +p 0 0. + +}}. +Fail Elpi Typecheck. + +Elpi Command bar. +Elpi Accumulate lp:{{ +pred p i:int. +p 0. + +}}. +Elpi Typecheck. + +Fail Elpi Typecheck foo. From 2ce9d167e799e72ed6d35e10c2cd6afb6060bb79 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Wed, 21 Feb 2024 14:52:52 +0100 Subject: [PATCH 11/14] add coq.reduction.lazy.whd_betaiota_deltazeta_for_iota_state --- src/coq_elpi_builtins.ml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 87b2be760..764b397f0 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -3382,6 +3382,21 @@ Supported attributes: !: t)), DocAbove); + MLCode(Pred("coq.reduction.lazy.whd_betaiota_deltazeta_for_iota_state", + CIn(term,"T", + COut(term,"Tred", + Read(proof_context, {|Puts T in weak head normal form. +Supported attributes: +- @redflags! (default coq.redflags.all)|}))), + (fun t _ ~depth proof_context constraints state -> + let sigma = get_sigma state in + let flags = Option.default RedFlags.all proof_context.options.redflags in + let t, sk = EConstr.decompose_app sigma t in + let t, sk = Reductionops.whd_betaiota_deltazeta_for_iota_state (RedFlags.red_transparent flags) proof_context.env sigma (t, Reductionops.Stack.append_app sk Reductionops.Stack.empty) in + let t = Reductionops.Stack.zip sigma (t, sk) in + !: t)), + DocAbove); + MLCode(Pred("coq.reduction.lazy.norm", CIn(term,"T", COut(term,"Tred", From 0cda7be36ec0bc55904e2d82a6cdbe2f727eaa3e Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Wed, 21 Feb 2024 17:08:31 +0100 Subject: [PATCH 12/14] fix evarconv --- apps/cs/src/evarconv_hacked.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/apps/cs/src/evarconv_hacked.ml b/apps/cs/src/evarconv_hacked.ml index a36878385..4caca1400 100644 --- a/apps/cs/src/evarconv_hacked.ml +++ b/apps/cs/src/evarconv_hacked.ml @@ -1044,7 +1044,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (try check_conv_record env i appr1 appr2 with Not_found -> begin match (apply_hooks env i appr1 appr2) with | Some r -> r - | None -> begin try check_conv_record env i appr2 appr1 + | None | exception Not_found -> begin try check_conv_record env i appr2 appr1 with Not_found -> begin match (apply_hooks env i appr2 appr1) with | Some r -> r | None -> raise Not_found From bb0cd520d921cfb7c2dea9748905562bdca43b43 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 21 Feb 2024 13:33:31 +0100 Subject: [PATCH 13/14] Enable loading db from files --- src/coq_elpi_vernacular.ml | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index ea578e236..cb576757f 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -318,11 +318,15 @@ let run_in_program ?(program = current_program ()) ?(st_setup=fun x -> x) (loc, str" is unknown; please add a directive like 'From .. Extra Dependency .. as " ++ Names.Id.print id ++ str"'.")) in try - let new_src_ast = List.map (fun fname -> - File { - fname; - fast = P.unit_from_file ~elpi fname; - }) s in + let new_src_ast = List.map (fun fname -> P.unit_from_file ~elpi fname) s in + if P.db_exists program then + P.accumulate_to_db program new_src_ast [] ~scope:Coq_elpi_utils.Regular + else + let new_src_ast = List.map2 (fun fname funit -> + File { + fname; + fast = funit; + }) s new_src_ast in P.accumulate program new_src_ast with Failure s -> CErrors.user_err Pp.(str s) let accumulate_extra_deps ~atts:(only,ph) ?program ids = skip ~only ~ph (accumulate_extra_deps ?program) ids @@ -330,11 +334,15 @@ let run_in_program ?(program = current_program ()) ?(st_setup=fun x -> x) (loc, let accumulate_files ?(program=current_program()) s = let elpi = P.ensure_initialized () in try - let new_src_ast = List.map (fun fname -> - File { - fname; - fast = P.unit_from_file ~elpi fname; - }) s in + let new_src_ast = List.map (fun fname -> P.unit_from_file ~elpi fname) s in + if P.db_exists program then + P.accumulate_to_db program new_src_ast [] ~scope:Coq_elpi_utils.Regular + else + let new_src_ast = List.map2 (fun fname funit -> + File { + fname; + fast = funit; + }) s new_src_ast in P.accumulate program new_src_ast with Failure s -> CErrors.user_err Pp.(str s) let accumulate_files ~atts:(only,ph) ?program s = skip ~only ~ph (accumulate_files ?program) s From 38afaf32034d519cd90cca018db7a33d45174d86 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 21 Feb 2024 16:27:21 +0100 Subject: [PATCH 14/14] Enable creating Db without initial code --- README.md | 4 ++-- src/coq_elpi_vernacular.ml | 6 +++--- src/coq_elpi_vernacular.mli | 2 +- src/coq_elpi_vernacular_syntax.mlg | 6 +++--- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index d6620a80c..b54f96a8d 100644 --- a/README.md +++ b/README.md @@ -175,8 +175,8 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`. [elpi-command](elpi/elpi-command-template.elpi). - `Elpi Tactic ` creates a tactic `` containing the preamble [elpi-tactic](elpi/elpi-tactic-template.elpi). -- `Elpi Db ` creates a Db (a program that is accumulated into - other programs). `` is the initial contents of the Db, including the +- `Elpi Db []` creates a Db (a program that is accumulated into + other programs). The optional `` is the initial contents of the Db, including the type declaration of its constituting predicates. It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands). - `Elpi Program ` lower level primitive letting one crate a diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index cb576757f..f48917704 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -456,14 +456,14 @@ let run_in_program ?(program = current_program ()) ?(st_setup=fun x -> x) (loc, P.init_program n init; set_current_program (snd n) - let create_db ~atts n ~init:(loc,s) = + let create_db ~atts n ?init () = let do_init = match atts with | None -> same_phase Interp P.stage | Some phase -> same_phase phase P.stage in let elpi = P.ensure_initialized () in P.declare_db n; - if do_init then + match do_init, init with false, _ | _, None -> () | true, Some (loc, s) -> let unit = P.unit_from_string ~elpi loc s in P.init_db n unit @@ -511,7 +511,7 @@ module type Common = sig val create_program : atts:bool option -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit val create_command : atts:bool option -> program_name -> unit val create_tactic : program_name -> unit - val create_db : atts:phase option -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit + val create_db : atts:phase option -> program_name -> ?init:(Elpi.API.Ast.Loc.t * string) -> unit -> unit end diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli index 770a69ef4..9970b57ed 100644 --- a/src/coq_elpi_vernacular.mli +++ b/src/coq_elpi_vernacular.mli @@ -47,7 +47,7 @@ module type Common = sig val create_program : atts:bool option -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit val create_command : atts:bool option -> program_name -> unit val create_tactic : program_name -> unit - val create_db : atts:phase option -> program_name -> init:(Elpi.API.Ast.Loc.t * string) -> unit + val create_db : atts:phase option -> program_name -> ?init:(Elpi.API.Ast.Loc.t * string) -> unit -> unit end diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index 90bafb8dd..cc756d791 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/coq_elpi_vernacular_syntax.mlg @@ -283,13 +283,13 @@ VERNAC COMMAND EXTEND Elpi CLASSIFIED AS SIDEFF EV.Synterp.create_tactic p } -> { EV.Interp.create_tactic p } -| #[ atts = any_attribute ] [ "Elpi" "Db" qualified_name(d) elpi_string(s) ] SYNTERP AS atts +| #[ atts = any_attribute ] [ "Elpi" "Db" qualified_name(d) elpi_string_opt(s) ] SYNTERP AS atts { let atts = validate_attributes synterp_attribute atts in - EV.Synterp.create_db ~atts d ~init:s; + EV.Synterp.create_db ~atts d ?init:s (); atts } -> { - EV.Interp.create_db ~atts d ~init:s } + EV.Interp.create_db ~atts d ?init:s () } | #[ atts = any_attribute ] [ "Elpi" "Typecheck" ] SYNTERP AS _ {