Merge pull request #593 from Tragicus/cspr

Update cs hook

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
 

apps/cs/src/coq_elpi_cs_hook.mlg

@@ -10,48 +10,72 @@ 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 () = 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, _), _ -> 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 *)
+			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 () = 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
+        | 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
 		 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
-			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
-  end
-  else 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
   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 +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/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) =

apps/cs/tests/test_cs.v

@@ -3,36 +3,27 @@ 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 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.
-Definition nat1 := nat.
+Check eq_refl _ : (sort nat _) = @id nat.
+Check 11.
+Check eq_refl _ : (sort nat _) 1 = @id nat 1.
+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.
 
 

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 _ {{ @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.