Tactic_matching API using EConstr.

5 files changed, 30 insertions, 23 deletions

diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml
index df38a42cb..288e12d0b 100644
--- a/ltac/taccoerce.ml
+++ b/ltac/taccoerce.ml
@@ -17,7 +17,7 @@ open Geninterp
 
 exception CannotCoerceTo of string
 
-let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
+let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type) =
   let wit = Genarg.create_arg "constr_context" in
   let () = register_val0 wit None in
   wit
@@ -64,7 +64,7 @@ let to_constr v =
     Some c
   else if has_type v (topwit wit_constr_under_binders) then
     let vars, c = out_gen (topwit wit_constr_under_binders) v in
-    match vars with [] -> Some c | _ -> None
+    match vars with [] -> Some (EConstr.Unsafe.to_constr c) | _ -> None
   else None
 
 let of_uconstr c = in_gen (topwit wit_uconstr) c
@@ -96,7 +96,7 @@ let is_variable env id =
 
 (* Transforms an id into a constr if possible, or fails with Not_found *)
 let constr_of_id env id =
-  Term.mkVar (let _ = Environ.lookup_named id env in id)
+  EConstr.mkVar (let _ = Environ.lookup_named id env in id)
 
 (* Gives the constr corresponding to a Constr_context tactic_arg *)
 let coerce_to_constr_context v =
@@ -212,7 +212,7 @@ let coerce_to_constr env v =
     | _ -> fail ()
   else if has_type v (topwit wit_constr) then
     let c = out_gen (topwit wit_constr) v in
-    ([], c)
+    ([], EConstr.of_constr c)
   else if has_type v (topwit wit_constr_under_binders) then
     out_gen (topwit wit_constr_under_binders) v
   else if has_type v (topwit wit_var) then
@@ -229,6 +229,7 @@ let coerce_to_uconstr env v =
 
 let coerce_to_closed_constr env v =
   let ids,c = coerce_to_constr env v in
+  let c = EConstr.Unsafe.to_constr c in
   let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in
   c
 
diff --git a/ltac/taccoerce.mli b/ltac/taccoerce.mli
index 0b67f8726..3049aff7e 100644
--- a/ltac/taccoerce.mli
+++ b/ltac/taccoerce.mli
@@ -48,7 +48,7 @@ end
 
 (** {5 Coercion functions} *)
 
-val coerce_to_constr_context : Value.t -> constr
+val coerce_to_constr_context : Value.t -> EConstr.constr
 
 val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t
 
@@ -91,6 +91,6 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list
 
 (** {5 Missing generic arguments} *)
 
-val wit_constr_context : (Empty.t, Empty.t, constr) genarg_type
+val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type
 
 val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 553565639..d2fb2614e 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -239,7 +239,7 @@ let pr_value env v =
   else if has_type v (topwit wit_constr_context) then
     let c = out_gen (topwit wit_constr_context) v in
     match env with
-    | Some (env,sigma) -> pr_lconstr_env env sigma c
+    | Some (env,sigma) -> pr_lconstr_env env sigma (EConstr.Unsafe.to_constr c)
     | _ -> str "a term"
   else if has_type v (topwit wit_constr) then
     let c = out_gen (topwit wit_constr) v in
@@ -334,7 +334,7 @@ let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2
 
 let extend_values_with_bindings (ln,lm) lfun =
   let of_cub c = match c with
-  | [], c -> Value.of_constr c
+  | [], c -> Value.of_constr (EConstr.Unsafe.to_constr c)
   | _ -> in_gen (topwit wit_constr_under_binders) c
   in
   (* For compatibility, bound variables are visible only if no other
@@ -790,6 +790,7 @@ let interp_may_eval f ist env sigma = function
       (try
 	let (sigma,ic) = f ist env sigma c in
 	let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
+	let ctxt = EConstr.Unsafe.to_constr ctxt in
 	let evdref = ref sigma in
 	let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
 	let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in
@@ -860,6 +861,7 @@ let rec message_of_value v =
     end }
   else if has_type v (topwit wit_constr_context) then
     let c = out_gen (topwit wit_constr_context) v in
+    let c = EConstr.Unsafe.to_constr c in
     Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (project gl) c) end }
   else if has_type v (topwit wit_uconstr) then
     let c = out_gen (topwit wit_uconstr) v in
@@ -1464,7 +1466,7 @@ and interp_letin ist llc u =
 and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
   let (>>=) = Ftactic.bind in
   let lctxt = Id.Map.map interp_context context in
-  let hyp_subst = Id.Map.map Value.of_constr terms in
+  let hyp_subst = Id.Map.map (EConstr.Unsafe.to_constr %> Value.of_constr) terms in
   let lfun = extend_values_with_bindings subst (lctxt +++ hyp_subst +++ ist.lfun) in
   let ist = { ist with lfun } in
   val_interp ist lhs >>= fun v ->
@@ -1518,6 +1520,7 @@ and interp_match ist lz constr lmr =
           Proofview.tclZERO ~info e
     end
   end >>= fun constr ->
+  let constr = EConstr.of_constr constr in
   Ftactic.enter { enter = begin fun gl ->
     let sigma = project gl in
     let env = Proofview.Goal.env gl in
@@ -1533,6 +1536,7 @@ and interp_match_goal ist lz lr lmr =
       let hyps = Proofview.Goal.hyps gl in
       let hyps = if lr then List.rev hyps else hyps in
       let concl = Proofview.Goal.concl gl in
+      let concl = EConstr.of_constr concl in
       let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
       interp_match_successes lz ist (Tactic_matching.match_goal env sigma hyps concl ilr)
     end }
@@ -1844,7 +1848,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         let c_interp patvars = { Sigma.run = begin fun sigma ->
 	  let lfun' = Id.Map.fold (fun id c lfun ->
-	    Id.Map.add id (Value.of_constr c) lfun) 
+	    Id.Map.add id (Value.of_constr (EConstr.Unsafe.to_constr c)) lfun) 
 	    patvars ist.lfun
 	  in
 	  let sigma = Sigma.to_evar_map sigma in
@@ -1871,7 +1875,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in
         let c_interp patvars = { Sigma.run = begin fun sigma ->
           let lfun' = Id.Map.fold (fun id c lfun ->
-            Id.Map.add id (Value.of_constr c) lfun) 
+            Id.Map.add id (Value.of_constr (EConstr.Unsafe.to_constr c)) lfun) 
             patvars ist.lfun
           in
           let ist = { ist with lfun = lfun' } in
diff --git a/ltac/tactic_matching.ml b/ltac/tactic_matching.ml
index 58998c96e..ac64f0bba 100644
--- a/ltac/tactic_matching.ml
+++ b/ltac/tactic_matching.ml
@@ -23,8 +23,8 @@ module NamedDecl = Context.Named.Declaration
     substitution mapping corresponding to matched hypotheses. *)
 type 'a t = {
   subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
-  context : Term.constr Id.Map.t;
-  terms : Term.constr Id.Map.t;
+  context : EConstr.constr Id.Map.t;
+  terms : EConstr.constr Id.Map.t;
   lhs : 'a;
 }
 
@@ -84,7 +84,7 @@ let equal_instances env sigma (ctx',c') (ctx,c) =
   (* How to compare instances? Do we want the terms to be convertible?
      unifiable? Do we want the universe levels to be relevant? 
      (historically, conv_x is used) *)
-  CList.equal Id.equal ctx ctx' && Reductionops.is_conv env sigma (EConstr.of_constr c') (EConstr.of_constr c)
+  CList.equal Id.equal ctx ctx' && Reductionops.is_conv env sigma c' c
 
 
 (** Merges two substitutions. Raises [Not_coherent_metas] when
@@ -233,7 +233,7 @@ module PatternMatching (E:StaticEnvironment) = struct
     | Term p ->
         begin 
           try
-            put_subst (Constr_matching.extended_matches E.env E.sigma p (EConstr.of_constr term)) <*>
+            put_subst (Constr_matching.extended_matches E.env E.sigma p term) <*>
             return lhs
           with Constr_matching.PatternMatchingFailure -> fail
         end
@@ -252,7 +252,7 @@ module PatternMatching (E:StaticEnvironment) = struct
             | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx)
         }
       in
-      map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p (EConstr.of_constr term)) imatching_error
+      map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error
 
 
   (** [rule_match_term term rule] matches the term [term] with the
@@ -284,8 +284,8 @@ module PatternMatching (E:StaticEnvironment) = struct
     pick hyps >>= fun decl ->
     let id = NamedDecl.get_id decl in
     let refresh = is_local_def decl in
-    pattern_match_term refresh pat (NamedDecl.get_type decl) () <*>
-    put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
+    pattern_match_term refresh pat (EConstr.of_constr (NamedDecl.get_type decl)) () <*>
+    put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*>
     return id
 
   (** [hyp_match_type hypname bodypat typepat hyps] matches a single
@@ -295,9 +295,11 @@ module PatternMatching (E:StaticEnvironment) = struct
   let hyp_match_body_and_type hypname bodypat typepat hyps =
     pick hyps >>= function
       | LocalDef (id,body,hyp) ->
+          let body = EConstr.of_constr body in
+          let hyp = EConstr.of_constr hyp in
           pattern_match_term false bodypat body () <*>
           pattern_match_term true typepat hyp () <*>
-          put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
+          put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*>
           return id
       | LocalAssum (id,hyp) -> fail
 
diff --git a/ltac/tactic_matching.mli b/ltac/tactic_matching.mli
index 090207bcc..d6f67d6c7 100644
--- a/ltac/tactic_matching.mli
+++ b/ltac/tactic_matching.mli
@@ -18,8 +18,8 @@
     substitution mapping corresponding to matched hypotheses. *)
 type 'a t = {
   subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
-  context : Term.constr Names.Id.Map.t;
-  terms : Term.constr Names.Id.Map.t;
+  context : EConstr.constr Names.Id.Map.t;
+  terms : EConstr.constr Names.Id.Map.t;
   lhs : 'a;
 }
 
@@ -31,7 +31,7 @@ type 'a t = {
 val match_term :
   Environ.env ->
   Evd.evar_map ->
-  Term.constr ->
+  EConstr.constr ->
   (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
   Tacexpr.glob_tactic_expr t Proofview.tactic
 
@@ -44,6 +44,6 @@ val match_goal:
   Environ.env ->
   Evd.evar_map ->
   Context.Named.t ->
-  Term.constr ->
+  EConstr.constr ->
   (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
   Tacexpr.glob_tactic_expr t Proofview.tactic