new cs hook

LPCIC · Feb 8, 2024 · 1d39142 · 1d39142
1 parent 402b410
commit 1d39142
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 18 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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]) _ :-