Hipattern API using EConstr.

1 files changed, 81 insertions, 75 deletions

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 5d78fd585..6681e5e49 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Term
 open Termops
+open EConstr
 open Inductiveops
 open Constr_matching
 open Coqlib
@@ -31,9 +32,9 @@ module RelDecl = Context.Rel.Declaration
 
   -- Eduardo (6/8/97). *)
 
-type 'a matching_function = Evd.evar_map -> constr -> 'a option
+type 'a matching_function = Evd.evar_map -> EConstr.constr -> 'a option
 
-type testing_function  = Evd.evar_map -> constr -> bool
+type testing_function  = Evd.evar_map -> EConstr.constr -> bool
 
 let mkmeta n = Nameops.make_ident "X" (Some n)
 let meta1 = mkmeta 1
@@ -44,10 +45,10 @@ let meta4 = mkmeta 4
 let op2bool = function Some _ -> true | None -> false
 
 let match_with_non_recursive_type sigma t =
-  match kind_of_term t with
+  match EConstr.kind sigma t with
     | App _ ->
-        let (hdapp,args) = decompose_app t in
-        (match kind_of_term hdapp with
+        let (hdapp,args) = decompose_app sigma t in
+        (match EConstr.kind sigma hdapp with
            | Ind (ind,u) ->
                if (Global.lookup_mind (fst ind)).mind_finite == Decl_kinds.CoFinite then
 		 Some (hdapp,args)
@@ -64,9 +65,9 @@ let is_non_recursive_type sigma t = op2bool (match_with_non_recursive_type sigma
    since they may appear in types of inductive constructors (see #2629) *)
 
 let rec has_nodep_prod_after n sigma c =
-  match kind_of_term c with
+  match EConstr.kind sigma c with
     | Prod (_,_,b) | LetIn (_,_,_,b) ->
-	( n>0 || EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b))
+	( n>0 || Vars.noccurn sigma 1 b)
 	&& (has_nodep_prod_after (n-1) sigma b)
     | _            -> true
 
@@ -87,9 +88,11 @@ let is_lax_conjunction = function
 | Some false -> true
 | _ -> false
 
+let prod_assum sigma t = fst (decompose_prod_assum sigma t)
+
 let match_with_one_constructor sigma style onlybinary allow_rec t =
-  let (hdapp,args) = decompose_app t in
-  let res = match kind_of_term hdapp with
+  let (hdapp,args) = decompose_app sigma t in
+  let res = match EConstr.kind sigma hdapp with
   | Ind ind ->
       let (mib,mip) = Global.lookup_inductive (fst ind) in
       if Int.equal (Array.length mip.mind_consnames) 1
@@ -98,22 +101,23 @@ let match_with_one_constructor sigma style onlybinary allow_rec t =
       then
 	if is_strict_conjunction style (* strict conjunction *) then
 	  let ctx =
-	    (prod_assum (snd
-	      (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))) in
+	    (prod_assum sigma (snd
+	      (decompose_prod_n_assum sigma mib.mind_nparams (EConstr.of_constr mip.mind_nf_lc.(0))))) in
 	  if
 	    List.for_all
 	      (fun decl -> let c = RelDecl.get_type decl in
 	                   is_local_assum decl &&
-			   isRel c &&
-                           Int.equal (destRel c) mib.mind_nparams) ctx
+			   Term.isRel c &&
+                           Int.equal (Term.destRel c) mib.mind_nparams) ctx
 	  then
 	    Some (hdapp,args)
 	  else None
 	else
-	  let ctyp = Term.prod_applist mip.mind_nf_lc.(0) args in
-	  let cargs = List.map RelDecl.get_type (prod_assum ctyp) in
+	  let ctyp = Termops.prod_applist sigma (EConstr.of_constr mip.mind_nf_lc.(0)) args in
+	  let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in
 	  if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then
 	    (* Record or non strict conjunction *)
+	    let cargs = List.map EConstr.of_constr cargs in
 	    Some (hdapp,List.rev cargs)
 	  else
 	      None
@@ -140,7 +144,7 @@ let is_record sigma t =
 let match_with_tuple sigma t =
   let t = match_with_one_constructor sigma None false true t in
   Option.map (fun (hd,l) ->
-    let ind = destInd hd in
+    let ind = destInd sigma hd in
     let (mib,mip) = Global.lookup_pinductive ind in
     let isrec = mis_is_recursive (fst ind,mib,mip) in
     (hd,l,isrec)) t
@@ -154,14 +158,15 @@ let is_tuple sigma t =
    "Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *)
 
 let test_strict_disjunction n lc =
+  let open Term in
   Array.for_all_i (fun i c ->
     match (prod_assum (snd (decompose_prod_n_assum n c))) with
     | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
     | _ -> false) 0 lc
 
 let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
-  let (hdapp,args) = decompose_app t in
-  let res = match kind_of_term hdapp with
+  let (hdapp,args) = decompose_app sigma t in
+  let res = match EConstr.kind sigma hdapp with
   | Ind (ind,u)  ->
       let car = constructors_nrealargs ind in
       let (mib,mip) = Global.lookup_inductive ind in
@@ -176,7 +181,7 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
 	    None
 	else
 	  let cargs =
-	    Array.map (fun ar -> pi2 (destProd (Term.prod_applist ar args)))
+	    Array.map (fun ar -> pi2 (destProd sigma (prod_applist sigma (EConstr.of_constr ar) args)))
 	      mip.mind_nf_lc in
 	  Some (hdapp,Array.to_list cargs)
       else
@@ -194,8 +199,8 @@ let is_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
    constructors *)
 
 let match_with_empty_type sigma t =
-  let (hdapp,args) = decompose_app t in
-  match (kind_of_term hdapp) with
+  let (hdapp,args) = decompose_app sigma t in
+  match EConstr.kind sigma hdapp with
     | Ind ind ->
         let (mib,mip) = Global.lookup_pinductive ind in
         let nconstr = Array.length mip.mind_consnames in
@@ -208,8 +213,8 @@ let is_empty_type sigma t = op2bool (match_with_empty_type sigma t)
    Parameters and indices are allowed *)
 
 let match_with_unit_or_eq_type sigma t =
-  let (hdapp,args) = decompose_app t in
-  match (kind_of_term hdapp) with
+  let (hdapp,args) = decompose_app sigma t in
+  match EConstr.kind sigma hdapp with
     | Ind ind  ->
         let (mib,mip) = Global.lookup_pinductive ind in
         let constr_types = mip.mind_nf_lc in
@@ -276,13 +281,13 @@ let coq_refl_jm_pattern       =
 
 open Globnames
 
-let is_matching x y = is_matching (Global.env ()) Evd.empty x (EConstr.of_constr y)
-let matches x y = matches (Global.env ()) Evd.empty x (EConstr.of_constr y)
+let is_matching sigma x y = is_matching (Global.env ()) sigma x y
+let matches sigma x y = matches (Global.env ()) sigma x y
 
-let match_with_equation t =
-  if not (isApp t) then raise NoEquationFound;
-  let (hdapp,args) = destApp t in
-  match kind_of_term hdapp with
+let match_with_equation sigma t =
+  if not (isApp sigma t) then raise NoEquationFound;
+  let (hdapp,args) = destApp sigma t in
+  match EConstr.kind sigma hdapp with
   | Ind (ind,u) ->
       if eq_gr (IndRef ind) glob_eq then
 	Some (build_coq_eq_data()),hdapp,
@@ -298,11 +303,11 @@ let match_with_equation t =
         let constr_types = mip.mind_nf_lc in
         let nconstr = Array.length mip.mind_consnames in
 	if Int.equal nconstr 1 then
-          if is_matching coq_refl_leibniz1_pattern constr_types.(0) then
+          if is_matching sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then
 	    None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
-	  else if is_matching coq_refl_leibniz2_pattern constr_types.(0) then
+	  else if is_matching sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then
 	    None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
-	  else if is_matching coq_refl_jm_pattern constr_types.(0) then
+	  else if is_matching sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then
 	    None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
 	  else raise NoEquationFound
         else raise NoEquationFound
@@ -319,8 +324,8 @@ let is_inductive_equality ind =
   Int.equal nconstr 1 && Int.equal (constructor_nrealargs (ind,1)) 0
 
 let match_with_equality_type sigma t =
-  let (hdapp,args) = decompose_app t in
-  match (kind_of_term hdapp) with
+  let (hdapp,args) = decompose_app sigma t in
+  match EConstr.kind sigma hdapp with
   | Ind (ind,_) when is_inductive_equality ind -> Some (hdapp,args)
   | _ -> None
 
@@ -331,23 +336,25 @@ let is_equality_type sigma t = op2bool (match_with_equality_type sigma t)
 (** X1 -> X2 **)
 let coq_arrow_pattern = mkPattern (mkGArrow (mkGPatVar "X1") (mkGPatVar "X2"))
 
-let match_arrow_pattern t =
-  let result = matches coq_arrow_pattern t in
+let match_arrow_pattern sigma t =
+  let result = matches sigma coq_arrow_pattern t in
   match Id.Map.bindings result with
     | [(m1,arg);(m2,mind)] ->
       assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind)
     | _ -> anomaly (Pp.str "Incorrect pattern matching")
 
 let match_with_imp_term sigma c =
-  match kind_of_term c with
-    | Prod (_,a,b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) -> Some (a,b)
+  match EConstr.kind sigma c with
+    | Prod (_,a,b) when Vars.noccurn sigma 1 b -> Some (a,b)
     | _              -> None
 
 let is_imp_term sigma c = op2bool (match_with_imp_term sigma c)
 
 let match_with_nottype sigma t =
   try
-    let (arg,mind) = match_arrow_pattern t in
+    let (arg,mind) = match_arrow_pattern sigma t in
+    let arg = EConstr.of_constr arg in
+    let mind = EConstr.of_constr mind in
     if is_empty_type sigma mind then Some (mind,arg) else None
   with PatternMatchingFailure -> None
 
@@ -356,19 +363,19 @@ let is_nottype sigma t = op2bool (match_with_nottype sigma t)
 (* Forall *)
 
 let match_with_forall_term sigma c=
-  match kind_of_term c with
+  match EConstr.kind sigma c with
     | Prod (nam,a,b) -> Some (nam,a,b)
     | _            -> None
 
 let is_forall_term sigma c = op2bool (match_with_forall_term sigma c)
 
 let match_with_nodep_ind sigma t =
-  let (hdapp,args) = decompose_app t in
-    match (kind_of_term hdapp) with
+  let (hdapp,args) = decompose_app sigma t in
+    match EConstr.kind sigma hdapp with
       | Ind ind  ->
           let (mib,mip) = Global.lookup_pinductive ind in
 	    if Array.length (mib.mind_packets)>1 then None else
-	      let nodep_constr = has_nodep_prod_after mib.mind_nparams sigma in
+	      let nodep_constr c = has_nodep_prod_after mib.mind_nparams sigma (EConstr.of_constr c) in
 		if Array.for_all nodep_constr mip.mind_nf_lc then
 		  let params=
 		    if Int.equal mip.mind_nrealargs 0 then args else
@@ -381,14 +388,14 @@ let match_with_nodep_ind sigma t =
 let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t)
 
 let match_with_sigma_type sigma t =
-  let (hdapp,args) = decompose_app t in
-  match (kind_of_term hdapp) with
+  let (hdapp,args) = decompose_app sigma t in
+  match EConstr.kind sigma hdapp with
     | Ind ind  ->
         let (mib,mip) = Global.lookup_pinductive ind in
           if Int.equal (Array.length (mib.mind_packets)) 1 &&
 	    (Int.equal mip.mind_nrealargs 0) &&
 	    (Int.equal (Array.length mip.mind_consnames)1) &&
-	    has_nodep_prod_after (mib.mind_nparams+1) sigma mip.mind_nf_lc.(0) then
+	    has_nodep_prod_after (mib.mind_nparams+1) sigma (EConstr.of_constr mip.mind_nf_lc.(0)) then
 	      (*allowing only 1 existential*)
 	      Some (hdapp,args)
 	  else
@@ -408,17 +415,17 @@ let rec first_match matcher = function
 
 (*** Equality *)
 
-let match_eq eqn (ref, hetero) =
+let match_eq sigma eqn (ref, hetero) =
   let ref =
     try Lazy.force ref
     with e when CErrors.noncritical e -> raise PatternMatchingFailure
   in
-  match kind_of_term eqn with
+  match EConstr.kind sigma eqn with
   | App (c, [|t; x; y|]) ->
-    if not hetero && is_global ref c then PolymorphicLeibnizEq (t, x, y)
+    if not hetero && Termops.is_global sigma ref c then PolymorphicLeibnizEq (t, x, y)
     else raise PatternMatchingFailure
   | App (c, [|t; x; t'; x'|]) ->
-    if hetero && is_global ref c then HeterogenousEq (t, x, t', x')
+    if hetero && Termops.is_global sigma ref c then HeterogenousEq (t, x, t', x')
     else raise PatternMatchingFailure
   | _ -> raise PatternMatchingFailure
 
@@ -430,27 +437,27 @@ let equalities =
    (coq_jmeq_ref, true), check_jmeq_loaded, build_coq_jmeq_data;
    (coq_identity_ref, false), no_check, build_coq_identity_data]
 
-let find_eq_data eqn = (* fails with PatternMatchingFailure *)
-  let d,k = first_match (match_eq eqn) equalities in
-  let hd,u = destInd (fst (destApp eqn)) in
+let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *)
+  let d,k = first_match (match_eq sigma eqn) equalities in
+  let hd,u = destInd sigma (fst (destApp sigma eqn)) in
     d,u,k
 
 let extract_eq_args gl = function
   | MonomorphicLeibnizEq (e1,e2) ->
-      let t = pf_unsafe_type_of gl (EConstr.of_constr e1) in (t,e1,e2)
+      let t = pf_unsafe_type_of gl e1 in (EConstr.of_constr t,e1,e2)
   | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
   | HeterogenousEq (t1,e1,t2,e2) ->
-      if pf_conv_x gl (EConstr.of_constr t1) (EConstr.of_constr t2) then (t1,e1,e2)
+      if pf_conv_x gl t1 t2 then (t1,e1,e2)
       else raise PatternMatchingFailure
 
 let find_eq_data_decompose gl eqn =
-  let (lbeq,u,eq_args) = find_eq_data eqn in
+  let (lbeq,u,eq_args) = find_eq_data (project gl) eqn in
   (lbeq,u,extract_eq_args gl eq_args)
 
 let find_this_eq_data_decompose gl eqn =
   let (lbeq,u,eq_args) =
     try (*first_match (match_eq eqn) inversible_equalities*)
-      find_eq_data eqn
+      find_eq_data (project gl) eqn
     with PatternMatchingFailure ->
       user_err  (str "No primitive equality found.") in
   let eq_args =
@@ -463,7 +470,6 @@ let match_eq_nf gls eqn (ref, hetero) =
   let n = if hetero then 4 else 3 in
   let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in
   let pat = mkPattern (mkGAppRef ref args) in
-  let eqn = EConstr.of_constr eqn in
   match Id.Map.bindings (pf_matches gls pat eqn) with
     | [(m1,t);(m2,x);(m3,y)] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
@@ -478,12 +484,12 @@ let dest_nf_eq gls eqn =
 
 (*** Sigma-types *)
 
-let match_sigma ex =
-  match kind_of_term ex with
-  | App (f, [| a; p; car; cdr |]) when is_global (Lazy.force coq_exist_ref) f -> 
-      build_sigma (), (snd (destConstruct f), a, p, car, cdr)
-  | App (f, [| a; p; car; cdr |]) when is_global (Lazy.force coq_existT_ref) f -> 
-    build_sigma_type (), (snd (destConstruct f), a, p, car, cdr)
+let match_sigma sigma ex =
+  match EConstr.kind sigma ex with
+  | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (Lazy.force coq_exist_ref) f -> 
+      build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr)
+  | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (Lazy.force coq_existT_ref) f -> 
+    build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr)
   | _ -> raise PatternMatchingFailure
     
 let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
@@ -493,12 +499,12 @@ let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
 let coq_sig_pattern =
   lazy (mkPattern (mkGAppRef coq_sig_ref [mkGPatVar "X1"; mkGPatVar "X2"]))
 
-let match_sigma t =
-  match Id.Map.bindings (matches (Lazy.force coq_sig_pattern) t) with
-    | [(_,a); (_,p)] -> (a,p)
+let match_sigma sigma t =
+  match Id.Map.bindings (matches sigma (Lazy.force coq_sig_pattern) t) with
+    | [(_,a); (_,p)] -> (EConstr.of_constr a,EConstr.of_constr p)
     | _ -> anomaly (Pp.str "Unexpected pattern")
 
-let is_matching_sigma t = is_matching (Lazy.force coq_sig_pattern) t
+let is_matching_sigma sigma t = is_matching sigma (Lazy.force coq_sig_pattern) t
 
 (*** Decidable equalities *)
 
@@ -530,15 +536,15 @@ let coq_eqdec_rev_pattern = coq_eqdec ~sum:coq_or_ref ~rev:true
 let op_or = coq_or_ref
 let op_sum = coq_sumbool_ref
 
-let match_eqdec t =
+let match_eqdec sigma t =
   let eqonleft,op,subst =
-    try true,op_sum,matches (Lazy.force coq_eqdec_inf_pattern) t
+    try true,op_sum,matches sigma (Lazy.force coq_eqdec_inf_pattern) t
     with PatternMatchingFailure ->
-    try false,op_sum,matches (Lazy.force coq_eqdec_inf_rev_pattern) t
+    try false,op_sum,matches sigma (Lazy.force coq_eqdec_inf_rev_pattern) t
     with PatternMatchingFailure ->
-    try true,op_or,matches (Lazy.force coq_eqdec_pattern) t
+    try true,op_or,matches sigma (Lazy.force coq_eqdec_pattern) t
     with PatternMatchingFailure ->
-        false,op_or,matches (Lazy.force coq_eqdec_rev_pattern) t in
+        false,op_or,matches sigma (Lazy.force coq_eqdec_rev_pattern) t in
   match Id.Map.bindings subst with
   | [(_,typ);(_,c1);(_,c2)] ->
       eqonleft, Universes.constr_of_global (Lazy.force op), c1, c2, typ
@@ -548,8 +554,8 @@ let match_eqdec t =
 let coq_not_pattern = lazy (mkPattern (mkGAppRef coq_not_ref [mkGHole]))
 let coq_imp_False_pattern = lazy (mkPattern (mkGArrow mkGHole (mkGRef coq_False_ref)))
 
-let is_matching_not t = is_matching (Lazy.force coq_not_pattern) t
-let is_matching_imp_False t = is_matching (Lazy.force coq_imp_False_pattern) t
+let is_matching_not sigma t = is_matching sigma (Lazy.force coq_not_pattern) t
+let is_matching_imp_False sigma t = is_matching sigma (Lazy.force coq_imp_False_pattern) t
 
 (* Remark: patterns that have references to the standard library must
    be evaluated lazily (i.e. at the time they are used, not a the time