Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 115 insertions, 90 deletions

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 83bfe9ea..65f342d8 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -1,19 +1,17 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pattern.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Names
 open Libnames
 open Nameops
 open Term
-open Rawterm
+open Glob_term
 open Environ
 open Nametab
 open Pp
@@ -28,6 +26,12 @@ type extended_patvar_map = (patvar * constr_under_binders) list
 
 (* Patterns *)
 
+type case_info_pattern =
+    { cip_style : case_style;
+      cip_ind : inductive option;
+      cip_ind_args : (int * int) option; (** number of params and args *)
+      cip_extensible : bool (** does this match end with _ => _ ? *) }
+
 type constr_pattern =
   | PRef of global_reference
   | PVar of identifier
@@ -38,11 +42,11 @@ type constr_pattern =
   | PLambda of name * constr_pattern * constr_pattern
   | PProd of name * constr_pattern * constr_pattern
   | PLetIn of name * constr_pattern * constr_pattern
-  | PSort of rawsort
+  | PSort of glob_sort
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
-  | PCase of (case_style * int array * inductive option * (int * int) option)
-      * constr_pattern * constr_pattern * constr_pattern array
+  | PCase of case_info_pattern * constr_pattern * constr_pattern *
+      (int * int * constr_pattern) list (** constructor index, nb of args *)
   | PFix of fixpoint
   | PCoFix of cofixpoint
 
@@ -57,16 +61,11 @@ let rec occur_meta_pattern = function
       (occur_meta_pattern c1) or (occur_meta_pattern c2)
   | PCase(_,p,c,br) ->
       (occur_meta_pattern p) or
-      (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
+      (occur_meta_pattern c) or
+      (List.exists (fun (_,_,p) -> occur_meta_pattern p) br)
   | PMeta _ | PSoApp _ -> true
   | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
 
-type constr_label =
-  | ConstNode of constant
-  | IndNode of inductive
-  | CstrNode of constructor
-  | VarNode of identifier
-
 exception BoundPattern;;
 
 let rec head_pattern_bound t =
@@ -100,8 +99,8 @@ let pattern_of_constr sigma t =
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n)))
     | Var id -> PVar id
-    | Sort (Prop c) -> PSort (RProp c)
-    | Sort (Type _) -> PSort (RType None)
+    | Sort (Prop c) -> PSort (GProp c)
+    | Sort (Type _) -> PSort (GType None)
     | Cast (c,_,_)      -> pattern_of_constr c
     | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
@@ -130,11 +129,17 @@ let pattern_of_constr sigma t =
           | GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
           | _ -> PMeta None)
     | Case (ci,p,a,br) ->
-	let cip = ci.ci_pp_info in
-	let no = Some (ci.ci_npar,cip.ind_nargs) in
-	PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,no),
-	       pattern_of_constr p,pattern_of_constr a,
-	       Array.map pattern_of_constr br)
+        let cip =
+	  { cip_style = ci.ci_pp_info.style;
+	    cip_ind = Some ci.ci_ind;
+	    cip_ind_args = Some (ci.ci_npar, ci.ci_pp_info.ind_nargs);
+	    cip_extensible = false }
+	in
+	let branch_of_constr i c =
+	  (i, ci.ci_cstr_ndecls.(i), pattern_of_constr c)
+	in
+	PCase (cip, pattern_of_constr p, pattern_of_constr a,
+	       Array.to_list (Array.mapi branch_of_constr br))
     | Fix f -> PFix f
     | CoFix f -> PCoFix f in
   let p = pattern_of_constr t in
@@ -151,14 +156,13 @@ let map_pattern_with_binders g f l = function
   | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b)
   | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g n l) b)
   | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
-  | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p,Array.map (f l) pl)
+  | PCase (ci,po,p,pl) ->
+    PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl)
   (* Non recursive *)
   | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _
   (* Bound to terms *)
   | PFix _ | PCoFix _ as x) -> x
 
-let map_pattern f = map_pattern_with_binders (fun _ () -> ()) (fun () -> f) ()
-
 let error_instantiate_pattern id l =
   let is = if List.length l = 1 then "is" else "are" in
   errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id
@@ -235,14 +239,20 @@ let rec subst_pattern subst pat =
       let c2' = subst_pattern subst c2 in
 	if c' == c && c1' == c1 && c2' == c2 then pat else
 	  PIf (c',c1',c2')
-  | PCase ((a,b,ind,n as cs),typ,c,branches) ->
+  | PCase (cip,typ,c,branches) ->
+      let ind = cip.cip_ind in
       let ind' = Option.smartmap (Inductiveops.subst_inductive subst) ind in
+      let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in
       let typ' = subst_pattern subst typ in
       let c' = subst_pattern subst c in
-      let branches' = array_smartmap (subst_pattern subst) branches in
-      let cs' = if ind == ind' then cs else (a,b,ind',n) in
-	if typ' == typ && c' == c && branches' == branches then pat else
-	  PCase(cs',typ', c', branches')
+      let subst_branch ((i,n,c) as br) =
+	let c' = subst_pattern subst c in
+	if c' == c then br else (i,n,c')
+      in
+      let branches' = list_smartmap subst_branch branches in
+      if cip' == cip && typ' == typ && c' == c && branches' == branches
+      then pat
+      else PCase(cip', typ', c', branches')
   | PFix fixpoint ->
       let cstr = mkFix fixpoint in
       let fixpoint' = destFix (subst_mps subst cstr) in
@@ -257,94 +267,109 @@ let rec subst_pattern subst pat =
 let mkPLambda na b = PLambda(na,PMeta None,b)
 let rev_it_mkPLambda = List.fold_right mkPLambda
 
+let err loc pp = user_err_loc (loc,"pattern_of_glob_constr", pp)
+
 let rec pat_of_raw metas vars = function
-  | RVar (_,id) ->
+  | GVar (_,id) ->
       (try PRel (list_index (Name id) vars)
        with Not_found -> PVar id)
-  | RPatVar (_,(false,n)) ->
+  | GPatVar (_,(false,n)) ->
       metas := n::!metas; PMeta (Some n)
-  | RRef (_,gr) ->
+  | GRef (_,gr) ->
       PRef (canonical_gr gr)
   (* Hack pour ne pas réécrire une interprétation complète des patterns*)
-  | RApp (_, RPatVar (_,(true,n)), cl) ->
+  | GApp (_, GPatVar (_,(true,n)), cl) ->
       metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
-  | RApp (_,c,cl) ->
+  | GApp (_,c,cl) ->
       PApp (pat_of_raw metas vars c,
 	    Array.of_list (List.map (pat_of_raw metas vars) cl))
-  | RLambda (_,na,bk,c1,c2) ->
+  | GLambda (_,na,bk,c1,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PLambda (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | RProd (_,na,bk,c1,c2) ->
+  | GProd (_,na,bk,c1,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PProd (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | RLetIn (_,na,c1,c2) ->
+  | GLetIn (_,na,c1,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PLetIn (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | RSort (_,s) ->
+  | GSort (_,s) ->
       PSort s
-  | RHole _ ->
+  | GHole _ ->
       PMeta None
-  | RCast (_,c,_) ->
-      Flags.if_verbose
-        Pp.warning "Cast not taken into account in constr pattern";
+  | GCast (_,c,_) ->
+      Flags.if_warn
+        Pp.msg_warning (str "Cast not taken into account in constr pattern");
       pat_of_raw metas vars c
-  | RIf (_,c,(_,None),b1,b2) ->
+  | GIf (_,c,(_,None),b1,b2) ->
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
-  | RLetTuple (loc,nal,(_,None),b,c) ->
-      let mkRLambda c na = RLambda (loc,na,Explicit,RHole (loc,Evd.InternalHole),c) in
-      let c = List.fold_left mkRLambda c nal in
-      PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b,
-             [|pat_of_raw metas vars c|])
-  | RCases (loc,sty,p,[c,(na,indnames)],brs) ->
-      let pred,ind_nargs, ind = match p,indnames with
-	| Some p, Some (_,ind,n,nal) ->
-	    rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
-	    Some (n,List.length nal),Some ind
-	| _ -> PMeta None, None, None in
-      let ind = match ind with Some _ -> ind | None ->
-	match brs with
-	  | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
-	  | _ -> None in
-      let cbrs =
-	Array.init (List.length brs) (pat_of_raw_branch loc metas vars ind brs)
+  | GLetTuple (loc,nal,(_,None),b,c) ->
+      let mkGLambda c na = GLambda (loc,na,Explicit,GHole (loc,Evd.InternalHole),c) in
+      let c = List.fold_left mkGLambda c nal in
+      let cip =
+	{ cip_style = LetStyle;
+	  cip_ind = None;
+	  cip_ind_args = None;
+	  cip_extensible = false }
+      in
+      PCase (cip, PMeta None, pat_of_raw metas vars b,
+             [0,1,pat_of_raw metas vars c])
+  | GCases (loc,sty,p,[c,(na,indnames)],brs) ->
+      let get_ind = function
+	| (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
+	| _ -> None
+      in
+      let ind_nargs,ind = match indnames with
+	| Some (_,ind,n,nal) -> Some (n,List.length nal), Some ind
+	| None -> None, get_ind brs
+      in
+      let ext,brs = pats_of_glob_branches loc metas vars ind brs
+      in
+      let pred = match p,indnames with
+	| Some p, Some (_,_,_,nal) ->
+	  rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p))
+	| _ -> PMeta None
+      in
+      let info =
+	{ cip_style = sty;
+	  cip_ind = ind;
+	  cip_ind_args = ind_nargs;
+	  cip_extensible = ext }
       in
-      let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in
-      PCase ((sty,cstr_nargs,ind,ind_nargs), pred,
-             pat_of_raw metas vars c, brs)
+      (* Nota : when we have a non-trivial predicate,
+	 the inductive type is known. Same when we have at least
+	 one non-trivial branch. These facts are used in [Constrextern]. *)
+      PCase (info, pred, pat_of_raw metas vars c, brs)
 
-  | r ->
-      let loc = loc_of_rawconstr r in
-      user_err_loc (loc,"pattern_of_rawconstr", Pp.str"Non supported pattern.")
+  | r -> err (loc_of_glob_constr r) (Pp.str "Non supported pattern.")
 
-and pat_of_raw_branch loc metas vars ind brs i =
-  let bri = List.filter
-    (function
-        (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1
-      | (loc,_,_,_) ->
-          user_err_loc (loc,"pattern_of_rawconstr",
-                        Pp.str "Non supported pattern.")) brs in
-  match bri with
-    | [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
-	if ind <> None & ind <> Some indsp then
-          user_err_loc (loc,"pattern_of_rawconstr",
-            Pp.str "All constructors must be in the same inductive type.");
-        let lna =
-          List.map
-            (function PatVar(_,na) -> na
-              | PatCstr(loc,_,_,_) ->
-                  user_err_loc (loc,"pattern_of_rawconstr",
-                                Pp.str "Non supported pattern.")) lv in
-        let vars' = List.rev lna @ vars in
-	List.length lv, rev_it_mkPLambda lna (pat_of_raw metas vars' br)
-    | _ -> user_err_loc (loc,"pattern_of_rawconstr",
-                         str "No unique branch for " ++ int (i+1) ++
-                         str"-th constructor.")
+and pats_of_glob_branches loc metas vars ind brs =
+  let get_arg = function
+    | PatVar(_,na) -> na
+    | PatCstr(loc,_,_,_) -> err loc (Pp.str "Non supported pattern.")
+  in
+  let rec get_pat indexes = function
+    | [] -> false, []
+    | [(_,_,[PatVar(_,Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *)
+    | (_,_,[PatCstr(_,(indsp,j),lv,_)],br) :: brs ->
+      if ind <> None && ind <> Some indsp then
+        err loc (Pp.str "All constructors must be in the same inductive type.");
+      if Intset.mem (j-1) indexes then
+	err loc
+          (str "No unique branch for " ++ int j ++ str"-th constructor.");
+      let lna = List.map get_arg lv in
+      let vars' = List.rev lna @ vars in
+      let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in
+      let ext,pats = get_pat (Intset.add (j-1) indexes) brs in
+      ext, ((j-1, List.length lv, pat) :: pats)
+    | (loc,_,_,_) :: _ -> err loc (Pp.str "Non supported pattern.")
+  in
+  get_pat Intset.empty brs
 
-let pattern_of_rawconstr c =
+let pattern_of_glob_constr c =
   let metas = ref [] in
   let p = pat_of_raw metas [] c in	
   (!metas,p)