patch cs hook

Author: Tragicus

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,36 +44,38 @@ 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
            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
-		 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

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:{{
 

apps/cs/theories/cs.v

@@ -3,25 +3,26 @@ 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,
   % 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.