Imported Upstream version 8.5~beta1+dfsg

1 files changed, 138 insertions, 124 deletions

diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index f8c1db27..4b94f420 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -1,29 +1,24 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*)
+(*i camlp4deps: "grammar/grammar.cma grammar/q_constr.cmo" i*)
 
 open Pp
+open Errors
 open Util
 open Names
-open Nameops
 open Term
-open Sign
 open Termops
-open Reductionops
 open Inductiveops
-open Evd
-open Environ
-open Clenv
-open Pattern
-open Matching
+open Constr_matching
 open Coqlib
 open Declarations
+open Tacmach.New
 
 (* I implemented the following functions which test whether a term t
    is an inductive but non-recursive type, a general conjuction, a
@@ -52,8 +47,8 @@ let match_with_non_recursive_type t =
     | App _ ->
         let (hdapp,args) = decompose_app t in
         (match kind_of_term hdapp with
-           | Ind ind ->
-               if not (Global.lookup_mind (fst ind)).mind_finite then
+           | Ind (ind,u) ->
+               if (Global.lookup_mind (fst ind)).mind_finite == Decl_kinds.CoFinite then
 		 Some (hdapp,args)
 	       else
 		 None
@@ -83,55 +78,67 @@ let has_nodep_prod = has_nodep_prod_after 0
 
 (* style: None = record; Some false = conjunction; Some true = strict conj *)
 
-let match_with_one_constructor style allow_rec t =
+let is_strict_conjunction = function
+| Some true -> true
+| _ -> false
+
+let is_lax_conjunction = function
+| Some false -> true
+| _ -> false
+
+let match_with_one_constructor style onlybinary allow_rec t =
   let (hdapp,args) = decompose_app t in
-  match kind_of_term hdapp with
+  let res = match kind_of_term hdapp with
   | Ind ind ->
-      let (mib,mip) = Global.lookup_inductive ind in
-      if (Array.length mip.mind_consnames = 1)
-	&& (allow_rec or not (mis_is_recursive (ind,mib,mip)))
-        && (mip.mind_nrealargs = 0)
+      let (mib,mip) = Global.lookup_inductive (fst ind) in
+      if Int.equal (Array.length mip.mind_consnames) 1
+	&& (allow_rec || not (mis_is_recursive (fst ind,mib,mip)))
+        && (Int.equal mip.mind_nrealargs 0)
       then
-	if style = Some true (* strict conjunction *) 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
 	  if
 	    List.for_all
-	      (fun (_,b,c) -> b=None && isRel c && destRel c = mib.mind_nparams) ctx
+	      (fun (_,b,c) -> Option.is_empty b && isRel c && Int.equal (destRel c) mib.mind_nparams) ctx
 	  then
 	    Some (hdapp,args)
 	  else None
 	else
 	  let ctyp = prod_applist mip.mind_nf_lc.(0) args in
 	  let cargs = List.map pi3 ((prod_assum ctyp)) in
-	  if style <> Some false || has_nodep_prod ctyp then
+	  if not (is_lax_conjunction style) || has_nodep_prod ctyp then
 	    (* Record or non strict conjunction *)
 	    Some (hdapp,List.rev cargs)
 	  else
 	      None
       else
 	None
+  | _ -> None in
+  match res with
+  | Some (hdapp, args) when not onlybinary -> res
+  | Some (hdapp, [_; _]) -> res
   | _ -> None
 
-let match_with_conjunction ?(strict=false) t =
-  match_with_one_constructor (Some strict) false t
+let match_with_conjunction ?(strict=false) ?(onlybinary=false) t =
+  match_with_one_constructor (Some strict) onlybinary false t
 
 let match_with_record t =
-  match_with_one_constructor None false t
+  match_with_one_constructor None false false t
 
-let is_conjunction ?(strict=false) t =
-  op2bool (match_with_conjunction ~strict t)
+let is_conjunction ?(strict=false) ?(onlybinary=false) t =
+  op2bool (match_with_conjunction ~strict ~onlybinary t)
 
 let is_record t =
   op2bool (match_with_record t)
 
 let match_with_tuple t =
-  let t = match_with_one_constructor None true t in
+  let t = match_with_one_constructor None false true t in
   Option.map (fun (hd,l) ->
     let ind = destInd hd in
-    let (mib,mip) = Global.lookup_inductive ind in
-    let isrec = mis_is_recursive (ind,mib,mip) in
+    let (mib,mip) = Global.lookup_pinductive ind in
+    let isrec = mis_is_recursive (fst ind,mib,mip) in
     (hd,l,isrec)) t
 
 let is_tuple t =
@@ -143,20 +150,20 @@ let is_tuple t =
    "Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *)
 
 let test_strict_disjunction n lc =
-  array_for_all_i (fun i c ->
+  Array.for_all_i (fun i c ->
     match (prod_assum (snd (decompose_prod_n_assum n c))) with
-    | [_,None,c] -> isRel c && destRel c = (n - i)
+    | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
     | _ -> false) 0 lc
 
-let match_with_disjunction ?(strict=false) t =
+let match_with_disjunction ?(strict=false) ?(onlybinary=false) t =
   let (hdapp,args) = decompose_app t in
-  match kind_of_term hdapp with
-  | Ind ind  ->
-      let car = mis_constr_nargs ind in
+  let res = match kind_of_term hdapp with
+  | Ind (ind,u)  ->
+      let car = constructors_nrealargs ind in
       let (mib,mip) = Global.lookup_inductive ind in
-      if array_for_all (fun ar -> ar = 1) car
-        && not (mis_is_recursive (ind,mib,mip))
-        && (mip.mind_nrealargs = 0)
+      if Array.for_all (fun ar -> Int.equal ar 1) car
+	&& not (mis_is_recursive (ind,mib,mip))
+        && (Int.equal mip.mind_nrealargs 0)
       then
 	if strict then
 	  if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then
@@ -170,10 +177,14 @@ let match_with_disjunction ?(strict=false) t =
 	  Some (hdapp,Array.to_list cargs)
       else
 	None
+  | _ -> None in
+  match res with
+  | Some (hdapp,args) when not onlybinary -> res
+  | Some (hdapp,[_; _]) -> res
   | _ -> None
 
-let is_disjunction ?(strict=false) t =
-  op2bool (match_with_disjunction ~strict t)
+let is_disjunction ?(strict=false) ?(onlybinary=false) t =
+  op2bool (match_with_disjunction ~strict ~onlybinary t)
 
 (* An empty type is an inductive type, possible with indices, that has no
    constructors *)
@@ -182,9 +193,9 @@ let match_with_empty_type t =
   let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
     | Ind ind ->
-        let (mib,mip) = Global.lookup_inductive ind in
+        let (mib,mip) = Global.lookup_pinductive ind in
         let nconstr = Array.length mip.mind_consnames in
-	if nconstr = 0 then Some hdapp else None
+	if Int.equal nconstr 0 then Some hdapp else None
     | _ ->  None
 
 let is_empty_type t = op2bool (match_with_empty_type t)
@@ -196,11 +207,11 @@ let match_with_unit_or_eq_type t =
   let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
     | Ind ind  ->
-        let (mib,mip) = Global.lookup_inductive ind in
+        let (mib,mip) = Global.lookup_pinductive ind in
         let constr_types = mip.mind_nf_lc in
         let nconstr = Array.length mip.mind_consnames in
-        let zero_args c = nb_prod c = mib.mind_nparams in
-	if nconstr = 1 && zero_args constr_types.(0) then
+        let zero_args c = Int.equal (nb_prod c) mib.mind_nparams in
+	if Int.equal nconstr 1 && zero_args constr_types.(0) then
 	  Some hdapp
 	else
 	  None
@@ -214,7 +225,7 @@ let is_unit_or_eq_type t = op2bool (match_with_unit_or_eq_type t)
 
 let is_unit_type t =
   match match_with_conjunction t with
-  | Some (_,t) when List.length t = 0 -> true
+  | Some (_,[]) -> true
   | _ -> false
 
 (* Checks if a given term is an application of an
@@ -232,27 +243,30 @@ let coq_refl_leibniz1_pattern = PATTERN [ forall x:_, _ x x ]
 let coq_refl_leibniz2_pattern = PATTERN [ forall A:_, forall x:A, _ A x x ]
 let coq_refl_jm_pattern       = PATTERN [ forall A:_, forall x:A, _ A x A x ]
 
-open Libnames
+open Globnames
+
+let is_matching x y = is_matching (Global.env ()) Evd.empty x y
+let matches x y = matches (Global.env ()) Evd.empty 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
-  | Ind ind ->
-      if IndRef ind = glob_eq then
+  | Ind (ind,u) ->
+      if eq_gr (IndRef ind) glob_eq then
 	Some (build_coq_eq_data()),hdapp,
 	PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
-      else if IndRef ind = glob_identity then
+      else if eq_gr (IndRef ind) glob_identity then
 	Some (build_coq_identity_data()),hdapp,
 	PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
-      else if IndRef ind = glob_jmeq then
+      else if eq_gr (IndRef ind) glob_jmeq then
 	Some (build_coq_jmeq_data()),hdapp,
 	HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
       else
         let (mib,mip) = Global.lookup_inductive ind in
         let constr_types = mip.mind_nf_lc in
         let nconstr = Array.length mip.mind_consnames in
-	if nconstr = 1 then
+	if Int.equal nconstr 1 then
           if is_matching coq_refl_leibniz1_pattern constr_types.(0) then
 	    None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
 	  else if is_matching coq_refl_leibniz2_pattern constr_types.(0) then
@@ -263,25 +277,41 @@ let match_with_equation t =
         else raise NoEquationFound
     | _ -> raise NoEquationFound
 
+(* Note: An "equality type" is any type with a single argument-free
+   constructor: it captures eq, eq_dep, JMeq, eq_true, etc. but also
+   True/unit which is the degenerate equality type (isomorphic to ()=());
+   in particular, True/unit are provable by "reflexivity" *)
+
 let is_inductive_equality ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let nconstr = Array.length mip.mind_consnames in
-  nconstr = 1 && constructor_nrealargs (Global.env()) (ind,1) = 0
+  Int.equal nconstr 1 && Int.equal (constructor_nrealargs (ind,1)) 0
 
 let match_with_equality_type t =
   let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
-  | Ind ind when is_inductive_equality ind -> Some (hdapp,args)
+  | Ind (ind,_) when is_inductive_equality ind -> Some (hdapp,args)
   | _ -> None
 
 let is_equality_type t = op2bool (match_with_equality_type t)
 
+(* Arrows/Implication/Negation *)
+
 let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ]
 
 let match_arrow_pattern t =
-  match matches coq_arrow_pattern t with
-    | [(m1,arg);(m2,mind)] -> assert (m1=meta1 & m2=meta2); (arg, mind)
-    | _ -> anomaly "Incorrect pattern matching"
+  let result = matches 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 c=
+  match kind_of_term c with
+    | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b)
+    | _              -> None
+
+let is_imp_term c = op2bool (match_with_imp_term c)
 
 let match_with_nottype t =
   try
@@ -291,6 +321,8 @@ let match_with_nottype t =
 
 let is_nottype t = op2bool (match_with_nottype t)
 
+(* Forall *)
+
 let match_with_forall_term c=
   match kind_of_term c with
     | Prod (nam,a,b) -> Some (nam,a,b)
@@ -298,24 +330,17 @@ let match_with_forall_term c=
 
 let is_forall_term c = op2bool (match_with_forall_term c)
 
-let match_with_imp_term c=
-  match kind_of_term c with
-    | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b)
-    | _              -> None
-
-let is_imp_term c = op2bool (match_with_imp_term c)
-
 let match_with_nodep_ind t =
   let (hdapp,args) = decompose_app t in
     match (kind_of_term hdapp) with
       | Ind ind  ->
-          let (mib,mip) = Global.lookup_inductive ind in
+          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 in
-		if array_for_all nodep_constr mip.mind_nf_lc then
+		if Array.for_all nodep_constr mip.mind_nf_lc then
 		  let params=
-		    if mip.mind_nrealargs=0 then args else
-		      fst (list_chop mib.mind_nparams args) in
+		    if Int.equal mip.mind_nrealargs 0 then args else
+		      fst (List.chop mib.mind_nparams args) in
 		    Some (hdapp,params,mip.mind_nrealargs)
 		else
 		  None
@@ -327,10 +352,10 @@ let match_with_sigma_type t=
   let (hdapp,args) = decompose_app t in
   match (kind_of_term hdapp) with
     | Ind ind  ->
-        let (mib,mip) = Global.lookup_inductive ind in
-          if (Array.length (mib.mind_packets)=1) &&
-	    (mip.mind_nrealargs=0) &&
-	    (Array.length mip.mind_consnames=1) &&
+        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) mip.mind_nf_lc.(0) then
 	      (*allowing only 1 existential*)
 	      Some (hdapp,args)
@@ -344,9 +369,10 @@ let is_sigma_type t=op2bool (match_with_sigma_type t)
 
 let rec first_match matcher = function
   | [] -> raise PatternMatchingFailure
-  | (pat,build_set)::l ->
-      try (build_set (),matcher pat)
-      with PatternMatchingFailure -> first_match matcher l
+  | (pat,check,build_set)::l when check () ->
+      (try (build_set (),matcher pat)
+       with PatternMatchingFailure -> first_match matcher l)
+  | _::l -> first_match matcher l
 
 (*** Equality *)
 
@@ -355,50 +381,48 @@ let coq_eq_pattern_gen eq = lazy PATTERN [ %eq ?X1 ?X2 ?X3 ]
 let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
 let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref
 let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ]
-let coq_eq_true_pattern = lazy PATTERN [ %coq_eq_true_ref ?X1 ]
 
 let match_eq eqn eq_pat =
   let pat =
     try Lazy.force eq_pat
     with e when Errors.noncritical e -> raise PatternMatchingFailure
   in
-  match matches pat eqn with
+  match Id.Map.bindings (matches pat eqn) with
     | [(m1,t);(m2,x);(m3,y)] ->
-	assert (m1 = meta1 & m2 = meta2 & m3 = meta3);
-	PolymorphicLeibnizEq (t,x,y)
+	assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
+        PolymorphicLeibnizEq (t,x,y)
     | [(m1,t);(m2,x);(m3,t');(m4,x')] ->
-	assert (m1 = meta1 & m2 = meta2 & m3 = meta3 & m4 = meta4);
+        assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3 && Id.equal m4 meta4);
 	HeterogenousEq (t,x,t',x')
-    | _ -> anomaly "match_eq: an eq pattern should match 3 or 4 terms"
+    | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 or 4 terms")
+
+let no_check () = true
+let check_jmeq_loaded () = Library.library_is_loaded Coqlib.jmeq_module
 
 let equalities =
-  [coq_eq_pattern, build_coq_eq_data;
-   coq_jmeq_pattern, build_coq_jmeq_data;
-   coq_identity_pattern, build_coq_identity_data]
+  [coq_eq_pattern, no_check, build_coq_eq_data;
+   coq_jmeq_pattern, check_jmeq_loaded, build_coq_jmeq_data;
+   coq_identity_pattern, no_check, build_coq_identity_data]
 
 let find_eq_data eqn = (* fails with PatternMatchingFailure *)
-  first_match (match_eq eqn) equalities
+  let d,k = first_match (match_eq eqn) equalities in
+  let hd,u = destInd (fst (destApp eqn)) in
+    d,u,k
 
 let extract_eq_args gl = function
   | MonomorphicLeibnizEq (e1,e2) ->
-      let t = Tacmach.pf_type_of gl e1 in (t,e1,e2)
+      let t = pf_type_of gl e1 in (t,e1,e2)
   | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
   | HeterogenousEq (t1,e1,t2,e2) ->
-      if Tacmach.pf_conv_x gl t1 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,eq_args) = find_eq_data eqn in
-  (lbeq,extract_eq_args gl eq_args)
-
-let inversible_equalities =
-  [coq_eq_pattern, build_coq_inversion_eq_data;
-   coq_jmeq_pattern, build_coq_inversion_jmeq_data;
-   coq_identity_pattern, build_coq_inversion_identity_data;
-   coq_eq_true_pattern, build_coq_inversion_eq_true_data]
+  let (lbeq,u,eq_args) = find_eq_data eqn in
+  (lbeq,u,extract_eq_args gl eq_args)
 
 let find_this_eq_data_decompose gl eqn =
-  let (lbeq,eq_args) =
+  let (lbeq,u,eq_args) =
     try (*first_match (match_eq eqn) inversible_equalities*)
       find_eq_data eqn
     with PatternMatchingFailure ->
@@ -407,17 +431,14 @@ let find_this_eq_data_decompose gl eqn =
     try extract_eq_args gl eq_args
     with PatternMatchingFailure ->
       error "Don't know what to do with JMeq on arguments not of same type." in
-  (lbeq,eq_args)
-
-open Tacmach
-open Tacticals
+  (lbeq,u,eq_args)
 
 let match_eq_nf gls eqn eq_pat =
-  match pf_matches gls (Lazy.force eq_pat) eqn with
+  match Id.Map.bindings (pf_matches gls (Lazy.force eq_pat) eqn) with
     | [(m1,t);(m2,x);(m3,y)] ->
-	assert (m1 = meta1 & m2 = meta2 & m3 = meta3);
+        assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
 	(t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y)
-    | _ -> anomaly "match_eq: an eq pattern should match 3 terms"
+    | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms")
 
 let dest_nf_eq gls eqn =
   try
@@ -427,31 +448,24 @@ let dest_nf_eq gls eqn =
 
 (*** Sigma-types *)
 
-(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *)
-let coq_ex_pattern_gen ex = lazy PATTERN [ %ex ?X1 ?X2 ?X3 ?X4 ]
-let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
-let coq_exist_pattern = coq_ex_pattern_gen coq_exist_ref
-
-let match_sigma ex ex_pat =
-  match matches (Lazy.force ex_pat) ex with
-    | [(m1,a);(m2,p);(m3,car);(m4,cdr)] ->
-	assert (m1=meta1 & m2=meta2 & m3=meta3 & m4=meta4);
-	(a,p,car,cdr)
-    | _ ->
-	anomaly "match_sigma: a successful sigma pattern should match 4 terms"
-
+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)
+  | _ -> raise PatternMatchingFailure
+    
 let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
-  first_match (match_sigma ex)
-    [coq_existT_pattern, build_sigma_type;
-     coq_exist_pattern, build_sigma]
+  match_sigma ex
 
 (* Pattern "(sig ?1 ?2)" *)
 let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ]
 
 let match_sigma t =
-  match matches (Lazy.force coq_sig_pattern) t with
+  match Id.Map.bindings (matches (Lazy.force coq_sig_pattern) t) with
     | [(_,a); (_,p)] -> (a,p)
-    | _ -> anomaly "Unexpected pattern"
+    | _ -> anomaly (Pp.str "Unexpected pattern")
 
 let is_matching_sigma t = is_matching (Lazy.force coq_sig_pattern) t
 
@@ -486,10 +500,10 @@ let match_eqdec t =
     try true,op_or,matches (Lazy.force coq_eqdec_pattern) t
     with PatternMatchingFailure ->
         false,op_or,matches (Lazy.force coq_eqdec_rev_pattern) t in
-  match subst with
+  match Id.Map.bindings subst with
   | [(_,typ);(_,c1);(_,c2)] ->
-      eqonleft, Libnames.constr_of_global (Lazy.force op), c1, c2, typ
-  | _ -> anomaly "Unexpected pattern"
+      eqonleft, Universes.constr_of_global (Lazy.force op), c1, c2, typ
+  | _ -> anomaly (Pp.str "Unexpected pattern")
 
 (* Patterns "~ ?" and "? -> False" *)
 let coq_not_pattern = lazy PATTERN [ ~ _ ]