Tactics API using EConstr.

7 files changed, 58 insertions, 21 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 7bd708e31..9e0a55a0d 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -98,6 +98,7 @@ let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
 let mkFix f = of_kind (Fix f)
 let mkCoFix f = of_kind (CoFix f)
 let mkProj (p, c) = of_kind (Proj (p, c))
+let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2))
 
 let applist (f, arg) = mkApp (f, Array.of_list arg)
 
@@ -466,6 +467,11 @@ let eq_constr_nounivs sigma c1 c2 =
   in
   eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2)
 
+let compare_constr sigma cmp c1 c2 =
+  let kind c = kind_upto sigma c in
+  let cmp c1 c2 = cmp (of_constr c1) (of_constr c2) in
+  compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal cmp (unsafe_to_constr c1) (unsafe_to_constr c2)
+
 (** TODO: factorize with universes.ml *)
 let test_constr_universes sigma leq m n =
   let open Universes in
@@ -608,6 +614,22 @@ let mkLambda_or_LetIn decl c =
   | LocalAssum (na,t) -> mkLambda (na, of_constr t, c)
   | LocalDef (na,b,t) -> mkLetIn (na, of_constr b, of_constr t, c)
 
+let mkNamedProd id typ c = mkProd (Name id, typ, Vars.subst_var id c)
+let mkNamedLambda id typ c = mkLambda (Name id, typ, Vars.subst_var id c)
+let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, Vars.subst_var id c2)
+
+let mkNamedProd_or_LetIn decl c =
+  let open Context.Named.Declaration in
+  match decl with
+    | LocalAssum (id,t) -> mkNamedProd id (of_constr t) c
+    | LocalDef (id,b,t) -> mkNamedLetIn id (of_constr b) (of_constr t) c
+
+let mkNamedLambda_or_LetIn decl c =
+  let open Context.Named.Declaration in
+  match decl with
+    | LocalAssum (id,t) -> mkNamedLambda id (of_constr t) c
+    | LocalDef (id,b,t) -> mkNamedLetIn id (of_constr b) (of_constr t) c
+
 let it_mkProd_or_LetIn t ctx = List.fold_left (fun c d -> mkProd_or_LetIn d c) t ctx
 let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d c) t ctx
 
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e4136a612..15463a8f6 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -73,6 +73,7 @@ val mkConstructU : pconstructor -> t
 val mkCase : case_info * t * t * t array -> t
 val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
+val mkArrow : t -> t -> t
 
 val applist : t * t list -> t
 
@@ -81,6 +82,12 @@ val mkLambda_or_LetIn : Rel.Declaration.t -> t -> t
 val it_mkProd_or_LetIn : t -> Rel.t -> t
 val it_mkLambda_or_LetIn : t -> Rel.t -> t
 
+val mkNamedLambda : Id.t -> types -> constr -> constr
+val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
+val mkNamedProd : Id.t -> types -> types -> types
+val mkNamedLambda_or_LetIn : Named.Declaration.t -> types -> types
+val mkNamedProd_or_LetIn : Named.Declaration.t -> types -> types
+
 (** {6 Simple case analysis} *)
 
 val isRel  : Evd.evar_map -> t -> bool
@@ -141,6 +148,7 @@ val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
 val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option
 val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option
 val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.universe_constraints option
+val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
 
 (** {6 Iterators} *)
 
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 7ccf9d810..4f40499d0 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -367,6 +367,7 @@ let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
 let push_rel_context_to_named_context env typ =
   (* compute the instances relative to the named context and rel_context *)
   let open Context.Named.Declaration in
+  let open EConstr in
   let ids = List.map get_id (named_context env) in
   let inst_vars = List.map mkVar ids in
   if List.is_empty (Environ.rel_context env) then
@@ -421,6 +422,7 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca
   Sigma.Unsafe.of_pair (newevk, evd)
 
 let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance =
+  let open EConstr in
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
   let Sigma (newevk, evd, p) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 431d98083..6620bbaed 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -24,7 +24,7 @@ val new_evar :
   env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> EConstr.types -> (constr, 'r) Sigma.sigma
+  ?principal:bool -> EConstr.types -> (EConstr.constr, 'r) Sigma.sigma
 
 val new_pure_evar :
   named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
@@ -39,18 +39,18 @@ val e_new_evar :
   env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> EConstr.types -> constr
+  ?principal:bool -> EConstr.types -> EConstr.constr
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
   env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
-  (constr * sorts, 'r) Sigma.sigma
+  (EConstr.constr * sorts, 'r) Sigma.sigma
 
 val e_new_type_evar : env -> evar_map ref ->
   ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
+  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> EConstr.constr * sorts
 
 val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
@@ -74,7 +74,7 @@ val new_evar_instance :
   ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
   ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool ->
-  constr list -> (constr, 'r) Sigma.sigma
+  EConstr.constr list -> (EConstr.constr, 'r) Sigma.sigma
 
 val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list
 
@@ -218,7 +218,7 @@ val push_rel_decl_to_named_context :
   Context.Rel.Declaration.t -> ext_named_context -> ext_named_context
 
 val push_rel_context_to_named_context : Environ.env -> EConstr.types ->
-  named_context_val * EConstr.types * constr list * csubst * (identifier*EConstr.constr) list
+  named_context_val * EConstr.types * EConstr.constr list * csubst * (identifier*EConstr.constr) list
 
 val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index b0f6d463b..9adf94744 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -72,6 +72,7 @@ let dependent_init =
   | TCons (env, sigma, typ, t) ->
     let sigma = Sigma.Unsafe.of_evar_map sigma in
     let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store (EConstr.of_constr typ) in
+    let econstr = EConstr.Unsafe.to_constr econstr in
     let sigma = Sigma.to_evar_map sigma in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let (gl, _) = Term.destEvar econstr in
diff --git a/engine/termops.ml b/engine/termops.ml
index 59dbb73f5..b7932665a 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -159,6 +159,7 @@ let print_env env =
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
 
 let rel_list n m =
+  let open EConstr in
   let rec reln l p =
     if p>m then l else reln (mkRel(n+p)::l) (p+1)
   in
@@ -857,16 +858,18 @@ let base_sort_cmp pb s0 s1 =
     | _ -> false
 
 (* eq_constr extended with universe erasure *)
-let compare_constr_univ f cv_pb t1 t2 =
-  match kind_of_term t1, kind_of_term t2 with
+let compare_constr_univ sigma f cv_pb t1 t2 =
+  match EConstr.kind sigma t1, EConstr.kind sigma t2 with
       Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
     | Prod (_,t1,c1), Prod (_,t2,c2) ->
 	f Reduction.CONV t1 t2 && f cv_pb c1 c2
-    | _ -> compare_constr (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
+    | _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
 
-let rec constr_cmp cv_pb t1 t2 = compare_constr_univ constr_cmp cv_pb t1 t2
+let constr_cmp sigma cv_pb t1 t2 =
+  let rec compare cv_pb t1 t2 = compare_constr_univ sigma compare cv_pb t1 t2 in
+  compare cv_pb t1 t2
 
-let eq_constr t1 t2 = constr_cmp Reduction.CONV t1 t2
+let eq_constr sigma t1 t2 = constr_cmp sigma Reduction.CONV t1 t2
 
 (* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn)
    App(c,[||]) -> ([],c) *)
@@ -883,12 +886,12 @@ type subst = (Context.Rel.t * constr) Evar.Map.t
 
 exception CannotFilter
 
-let filtering env cv_pb c1 c2 =
+let filtering sigma env cv_pb c1 c2 =
   let evm = ref Evar.Map.empty in
   let define cv_pb e1 ev c1 =
     try let (e2,c2) = Evar.Map.find ev !evm in
     let shift = List.length e1 - List.length e2 in
-    if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter
+    if constr_cmp sigma cv_pb (EConstr.of_constr c1) (EConstr.of_constr (lift shift c2)) then () else raise CannotFilter
     with Not_found ->
       evm := Evar.Map.add ev (e1,c1) !evm
   in
@@ -909,8 +912,9 @@ let filtering env cv_pb c1 c2 =
       | _, Evar (ev,_) -> define cv_pb env ev c1
       | Evar (ev,_), _ -> define cv_pb env ev c2
       | _ ->
-	  if compare_constr_univ
-	  (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
+          let inj = EConstr.Unsafe.to_constr in
+	  if compare_constr_univ sigma
+	  (fun pb c1 c2 -> aux env pb (inj c1) (inj c2); true) cv_pb (EConstr.of_constr c1) (EConstr.of_constr c2) then ()
 	  else raise CannotFilter
 	  (* TODO: le reste des binders *)
   in
diff --git a/engine/termops.mli b/engine/termops.mli
index abc9caa98..7758a57ee 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -41,7 +41,7 @@ val lookup_rel_id : Id.t -> Context.Rel.t -> int * constr option * types
     [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|]
 *)
 val rel_vect : int -> int -> constr array
-val rel_list : int -> int -> constr list
+val rel_list : int -> int -> EConstr.constr list
 
 (** iterators/destructors on terms *)
 val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
@@ -160,10 +160,10 @@ val replace_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.t -> constr
 
 (** Alternative term equalities *)
 val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
-val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) ->
-  Reduction.conv_pb -> constr -> constr -> bool
-val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool
-val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*)
+val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool) ->
+  Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool
+val constr_cmp : Evd.evar_map -> Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool
+val eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool (* FIXME rename: erases universes*)
 
 val eta_reduce_head : constr -> constr
 
@@ -185,7 +185,7 @@ exception CannotFilter
    Warning: Outer-kernel sort subtyping are taken into account: c1 has
    to be smaller than c2 wrt. sorts. *)
 type subst = (Context.Rel.t * constr) Evar.Map.t
-val filtering : Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst
+val filtering : Evd.evar_map -> Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst
 
 val decompose_prod_letin : Evd.evar_map -> EConstr.t -> int * Context.Rel.t * constr
 val align_prod_letin : Evd.evar_map -> EConstr.t -> EConstr.t -> Context.Rel.t * constr