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]) _ :-