From ef7254792cd9f325f4785278ca37f95c0c2e9ba0 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 8 Feb 2024 17:35:17 +0100 Subject: [PATCH 1/5] fix reduction bug --- apps/cs/src/coq_elpi_cs_hook.mlg | 12 ++++++++++-- apps/cs/tests/test_cs.v | 8 ++++---- apps/cs/theories/cs.v | 6 +++--- 3 files changed, 17 insertions(+), 9 deletions(-) diff --git a/apps/cs/src/coq_elpi_cs_hook.mlg b/apps/cs/src/coq_elpi_cs_hook.mlg index 7d7a65c12..2c29bafc6 100644 --- a/apps/cs/src/coq_elpi_cs_hook.mlg +++ b/apps/cs/src/coq_elpi_cs_hook.mlg @@ -40,8 +40,16 @@ 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.Stack.zip sigma (EConstr.mkConstU (proji, EConstr.EInstance.empty), Reductionops.Stack.append_app_list (params1 @ [goal]) Reductionops.Stack.empty) in + let lhs = Reductionops.whd_const proji env sigma lhs in + let lhs = Reductionops.whd_betaiotazeta env sigma lhs in + let hh, sk1 = EConstr.decompose_app sigma lhs in + let () = Feedback.msg_info Pp.(str "aha" ++ Printer.pr_econstr_env env 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, (hh, 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 diff --git a/apps/cs/tests/test_cs.v b/apps/cs/tests/test_cs.v index 5cf69a562..628b49159 100644 --- a/apps/cs/tests/test_cs.v +++ b/apps/cs/tests/test_cs.v @@ -6,16 +6,16 @@ Elpi Override CS All. Structure S : Type := { sort :> Type }. -Elpi Accumulate cs.db lp:{{ +Elpi Accumulate canonical_solution lp:{{ -cs _ {{ sort lp:Sol }} {{ nat }} :- - Sol = {{ Build_S nat }}. +cs _ {{ sort lp:T }} {{ @id lp:T }} {{ 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. diff --git a/apps/cs/theories/cs.v b/apps/cs/theories/cs.v index 0d38897a9..8bb1bdaf3 100644 --- a/apps/cs/theories/cs.v +++ b/apps/cs/theories/cs.v @@ -16,9 +16,9 @@ pred cs i:goal-ctx, o:term, o:term. Elpi Tactic canonical_solution. Elpi Accumulate 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. }}. From 5af360081951256a71bbc5e5cd3eb2190b5caafe Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 9 Feb 2024 17:05:42 +0100 Subject: [PATCH 2/5] fixed tests & bugs, removed debug msgs --- apps/cs/src/coq_elpi_cs_hook.mlg | 37 ++++++++++++++++++++++---------- apps/cs/tests/test_cs.v | 19 +++++----------- 2 files changed, 31 insertions(+), 25 deletions(-) diff --git a/apps/cs/src/coq_elpi_cs_hook.mlg b/apps/cs/src/coq_elpi_cs_hook.mlg index 2c29bafc6..f4e5daa14 100644 --- a/apps/cs/src/coq_elpi_cs_hook.mlg +++ b/apps/cs/src/coq_elpi_cs_hook.mlg @@ -18,12 +18,30 @@ let elpi_cs_hook program env sigma lhs rhs = then begin 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 + | (proji, _), _ -> 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 Reductionops.Stack.args_size sk2 = Reductionops.Stack.args_size extra_args1 then [], sk2 + else match Reductionops.Stack.strip_n_app (Reductionops.Stack.args_size sk2 - Reductionops.Stack.args_size 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 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 = @@ -36,7 +54,7 @@ let elpi_cs_hook program env sigma lhs rhs = match Interp.get_and_compile program with | None -> None | Some (cprogram, _) -> - match Interp.run ~static_check:false cprogram (`Fun query) with + begin 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 @@ -45,16 +63,13 @@ let elpi_cs_hook program env sigma lhs rhs = let lhs = Reductionops.whd_const proji env sigma lhs in let lhs = Reductionops.whd_betaiotazeta env sigma lhs in let hh, sk1 = EConstr.decompose_app sigma lhs in - let () = Feedback.msg_info Pp.(str "aha" ++ Printer.pr_econstr_env env 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, (hh, 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 + end let add_cs_hook = let cs_hook_program = Summary.ref ~name:"elpi-cs" None in diff --git a/apps/cs/tests/test_cs.v b/apps/cs/tests/test_cs.v index 628b49159..f81b0377f 100644 --- a/apps/cs/tests/test_cs.v +++ b/apps/cs/tests/test_cs.v @@ -15,24 +15,15 @@ Elpi Typecheck canonical_solution. Check 1. Check eq_refl _ : (sort nat _) = @id nat. +Check 11. Check eq_refl _ : (sort nat _) 1 = @id nat 1. -Definition nat1 := nat. +Definition id1 := id. Check 2. -Check eq_refl _ : (sort _) = nat1. +Check eq_refl _ : (sort nat _) = @id1 nat. Definition sort1 := sort. Check 3. -Check eq_refl _ : (sort1 _) = nat. +Check eq_refl _ : (sort1 nat _) = @id nat. Check 4. -Check eq_refl _ : (sort1 _) = nat1. - - -Elpi Accumulate cs.db lp:{{ - -cs _ {{ sort lp:Sol }} {{ bool }} :- - % typing is wired in, do we want this? - std.spy(Sol = {{ Prop }}). - -}}. -Elpi Typecheck canonical_solution. +Check eq_refl _ : (sort1 nat _) = @id1 nat. From 40e73791819f20a0194e1a36745702c58d336c6e Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 12 Feb 2024 15:20:20 +0100 Subject: [PATCH 3/5] patch evarconv --- apps/cs/src/evarconv_hacked.ml | 104 ++++++++++++++++++++++++++------- 1 file changed, 82 insertions(+), 22 deletions(-) diff --git a/apps/cs/src/evarconv_hacked.ml b/apps/cs/src/evarconv_hacked.ml index 79f8ce536..a36878385 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 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 i 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 i 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,32 @@ 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 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 + | 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 (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 +1338,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) = From ae5b0a6c03396e8639a75508cead4d0a49d882cb Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 12 Feb 2024 16:02:09 +0100 Subject: [PATCH 4/5] patch cs hook --- apps/cs/src/coq_elpi_cs_hook.mlg | 31 +++++++++++++++---------------- apps/cs/tests/test_cs.v | 4 ++-- apps/cs/theories/cs.v | 13 +++++++------ 3 files changed, 24 insertions(+), 24 deletions(-) diff --git a/apps/cs/src/coq_elpi_cs_hook.mlg b/apps/cs/src/coq_elpi_cs_hook.mlg index f4e5daa14..e0badf337 100644 --- a/apps/cs/src/coq_elpi_cs_hook.mlg +++ b/apps/cs/src/coq_elpi_cs_hook.mlg @@ -10,19 +10,17 @@ 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 () = 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 - | (proji, _), _ -> 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 *) @@ -35,6 +33,7 @@ let elpi_cs_hook program env sigma lhs rhs = 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 Reductionops.Stack.args_size sk2 = Reductionops.Stack.args_size extra_args1 then [], sk2 else match Reductionops.Stack.strip_n_app (Reductionops.Stack.args_size sk2 - Reductionops.Stack.args_size extra_args1 - 1) sk2 with @@ -45,17 +44,18 @@ let elpi_cs_hook program env sigma lhs rhs = 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 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, _) -> - begin 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 @@ -63,18 +63,19 @@ let elpi_cs_hook program env sigma lhs rhs = let lhs = Reductionops.whd_const proji env sigma lhs in let lhs = Reductionops.whd_betaiotazeta env sigma lhs in let hh, sk1 = EConstr.decompose_app sigma lhs in + let () = Feedback.msg_info Pp.(str "aha" ++ Printer.pr_econstr_env env 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, (hh, 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 - end + | 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 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 @@ -83,8 +84,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/tests/test_cs.v b/apps/cs/tests/test_cs.v index f81b0377f..48f0ea15f 100644 --- a/apps/cs/tests/test_cs.v +++ b/apps/cs/tests/test_cs.v @@ -3,8 +3,8 @@ From Coq Require Import Bool. Elpi Override CS All. -Structure S : Type := - { sort :> Type }. +Structure S (T : Type) : Type := + { sort :> T -> T }. Elpi Accumulate canonical_solution lp:{{ diff --git a/apps/cs/theories/cs.v b/apps/cs/theories/cs.v index 8bb1bdaf3..f7f04660a 100644 --- a/apps/cs/theories/cs.v +++ b/apps/cs/theories/cs.v @@ -3,18 +3,20 @@ From elpi Require Import elpi. Elpi Db cs.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 cs.db. +Elpi Accumulate canonical_solution lp:{{ solve (goal Ctx _ _Ty Sol [trm Proj, trm Rhs]) _ :- cs Ctx Proj Rhs Sol, @@ -22,6 +24,5 @@ solve (goal Ctx _ _Ty Sol [trm Proj, trm Rhs]) _ :- true. }}. -Elpi Accumulate Db cs.db. -Elpi Typecheck. +Elpi Typecheck canonical_solution. Elpi CSFallbackTactic canonical_solution. From b4660ad3543cd90fb6feae5441068c705e4ccdc9 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 12 Feb 2024 16:35:41 +0100 Subject: [PATCH 5/5] changelog --- Changelog.md | 1 + 1 file changed, 1 insertion(+) diff --git a/Changelog.md b/Changelog.md index fc7f2cef4..7c514f5ec 100644 --- a/Changelog.md +++ b/Changelog.md @@ -23,6 +23,7 @@ Requires Elpi 1.18.2 and Coq 8.19. ### Apps - TC: avoid declaring options twice (could make vscoq2 fail) +- CS: `cs` now takes a context, a term that is the projection of some structure applied to the parameters of the structure, a term to put a structure on and the solution to return ## [2.0.1] - 29/12/2023