Cswb

README.md

@@ -175,8 +175,8 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
   [elpi-command](elpi/elpi-command-template.elpi).
 - `Elpi Tactic <qname>` creates a tactic `<qname>` containing the preamble
   [elpi-tactic](elpi/elpi-tactic-template.elpi).
-- `Elpi Db <dbname> <code>` creates a Db (a program that is accumulated into
-  other programs). `<code>` is the initial contents of the Db, including the
+- `Elpi Db <dbname> [<code>]` creates a Db (a program that is accumulated into
+  other programs). The optional `<code>` is the initial contents of the Db, including the
   type declaration of its constituting predicates.
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands).
 - `Elpi Program <qname> <code>` lower level primitive letting one crate a

_CoqProject.test

@@ -55,4 +55,5 @@ tests/test_link_order_import3.v
 tests/test_query_extra_dep.v
 tests/test_toposort.v
 tests/test_synterp.v
+tests/test_grafting.v
 tests/test_checker.v

apps/coercion/src/coq_elpi_coercion_hook.mlg

@@ -11,6 +11,13 @@ open Coq_elpi_vernacular
 let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
   let loc = API.Ast.Loc.initial "(unknown)" in
   let atts = [] in
+  let (env, sigma, expected, retype) =
+    match expected with
+    | Coercion.Type t -> (env, sigma, t, false)
+    | Coercion.Product -> begin let (sigma, (source, _)) = Evarutil.new_type_evar env sigma Evd.univ_flexible in
+      let (sigma, (target, _)) = let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (Context.annotR (Names.Name (Namegen.default_dependent_ident)) , source)) env in Evarutil.new_type_evar env sigma Evd.univ_flexible in
+      (env, sigma, EConstr.mkProd (Context.annotR (Names.Name (Namegen.default_type_ident)), source, target), true) end
+  | Coercion.Sort -> let (sigma, t) = Evarutil.new_Type sigma in (env, sigma, t, true) in
   let sigma, goal = Evarutil.new_evar env sigma expected in
   let goal_evar, _ = EConstr.destEvar sigma goal in
   let query ~depth state =
@@ -28,7 +35,9 @@ let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
     | API.Execute.Success solution ->
       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 Some (sigma, goal) else None
+      if Evd.is_defined sigma goal_evar
+        then let t = if retype then Retyping.get_type_of env sigma goal else expected in Some (sigma, goal, t)
+		  else None
     | API.Execute.NoMoreSteps
     | API.Execute.Failure -> None
     | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None
@@ -57,4 +66,4 @@ VERNAC COMMAND EXTEND ElpiCoercion CLASSIFIED AS SIDEFF
      let () = ignore_unknown_attributes atts in
      add_coercion_hook (snd p) }
 
-END
+END

apps/coercion/tests/test_coercion.v

@@ -32,3 +32,20 @@ Check natmul R n : ringType_sort R.
 Check n : ringType_sort R.
 
 End TestNatMul.
+
+Elpi Accumulate coercion.db lp:{{
+
+coercion _ V T E {{ Nat.mul lp:V }} :-
+  coq.unify-eq T {{ nat }} ok,
+  coq.unify-eq E {{ nat -> nat }} ok.
+
+coercion _ V T E {{ { m : nat | m < lp:V } }} :-
+  coq.unify-eq T {{ nat }} ok,
+  coq.unify-eq E {{ Type }} ok.
+
+}}.
+Elpi Typecheck coercion.
+
+Check 3 2.
+Check forall (x : 3), proj1_sig x < 3.
+

apps/cs/src/coq_elpi_cs_hook.mlg

@@ -10,48 +10,70 @@ 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 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
 	  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.whd_all env sigma (EConstr.mkApp (EConstr.mkConstU (proji, EConstr.EInstance.empty), Array.of_list (params1 @ [goal]))) in
+			  let h, sk1 = EConstr.decompose_app 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, (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
-  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 +82,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 | exception Not_found -> 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,19 +3,21 @@ 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:{{
 
-cs _ {{ sort lp:Sol }} {{ nat }} :-
-  Sol = {{ Build_S nat }}.
+cs _ A B :- coq.say "cs" A B, fail.
+cs _ {{ sort lp:T lp:Sol }} {{ @id lp:T }} :-
+  Sol = {{ 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.