Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2

5 files changed, 72 insertions, 42 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index daa57b77..570d113d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 8831 2006-05-19 09:29:54Z herbelin $ *)
+(* $Id: constrextern.ml 8997 2006-07-03 16:40:20Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -186,7 +186,7 @@ let rec check_same_type ty1 ty2 =
   | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) ->
       List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2;
       List.iter2 (fun (_,pl1,r1) (_,pl2,r2) ->
-        List.iter2 check_same_pattern pl1 pl2;
+        List.iter2 (List.iter2 check_same_pattern) pl1 pl2;
         check_same_type r1 r2) brl1 brl2
   | CHole _, CHole _ -> ()
   | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> ()
@@ -797,7 +797,7 @@ and extern_local_binder scopes vars = function
              LocalRawAssum([(dummy_loc,na)],ty) :: l))
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
-  (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl,
+  (loc,[List.map (extern_cases_pattern_in_scope scopes vars) pl],
    extern inctx scopes vars c)
 
 and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
@@ -843,6 +843,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 and extern_recursion_order scopes vars = function
     RStructRec -> CStructRec
   | RWfRec c -> CWfRec (extern true scopes vars c)
+  | RMeasureRec c -> CMeasureRec (extern true scopes vars c)
 
 
 let extern_rawconstr vars c =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 678fb87b..355bac1d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 8924 2006-06-08 17:49:01Z notin $ *)
+(* $Id: constrintern.ml 8997 2006-07-03 16:40:20Z herbelin $ *)
 
 open Pp
 open Util
@@ -81,9 +81,8 @@ let explain_non_linear_pattern id =
   str "The variable " ++ pr_id id ++ str " is bound several times in pattern"
 
 let explain_bad_patterns_number n1 n2 =
-  let s = if n1 > 1 then "s" else "" in
-  str "Expecting " ++ int n1 ++ str " pattern" ++ str s ++ str " but found "
-    ++ int n2
+  str "Expecting " ++ int n1 ++ str (plural n1 " pattern") ++
+  str " but found " ++ int n2
 
 let explain_bad_explicitation_number n po =
   match n with
@@ -357,7 +356,8 @@ let rec has_duplicate = function
   | x::l -> if List.mem x l then (Some x) else has_duplicate l
 
 let loc_of_lhs lhs = 
- join_loc (cases_pattern_loc (List.hd lhs)) (cases_pattern_loc (list_last lhs))
+ join_loc (cases_pattern_loc (List.hd (List.hd lhs)))
+          (cases_pattern_loc (list_last (list_last lhs)))
 
 let check_linearity lhs ids =
   match has_duplicate ids with
@@ -775,17 +775,22 @@ let internalise sigma globalenv env allow_soapp lvar c =
 	in
         let idl = Array.map
           (fun (id,(n,order),bl,ty,bd) ->
-	    let ro, ((ids',_,_),rbl) =
-	      (match order with
-		   CStructRec -> 
-		     RStructRec,
-		     List.fold_left intern_local_binder (env,[]) bl
-		 | CWfRec c -> 
-		     let before, after = list_chop (succ (out_some n)) bl in
-		     let ((ids',_,_),rafter) =
-		       List.fold_left intern_local_binder (env,[]) after in
-		     let ro = RWfRec (intern (ids', tmp_scope, scopes) c) in
-		       ro, List.fold_left intern_local_binder (env,rafter) before)
+	     let intern_ro_arg c f =
+	       let before, after = list_chop (succ (out_some n)) bl in
+	       let ((ids',_,_),rafter) =
+		 List.fold_left intern_local_binder (env,[]) after in
+	       let ro = (intern (ids', tmp_scope, scopes) c) in
+		 f ro, List.fold_left intern_local_binder (env,rafter) before
+	     in
+	     let ro, ((ids',_,_),rbl) =
+	       (match order with
+		    CStructRec -> 
+		      RStructRec,
+		      List.fold_left intern_local_binder (env,[]) bl
+		  | CWfRec c ->
+		      intern_ro_arg c (fun r -> RWfRec r)
+		  | CMeasureRec c ->
+		      intern_ro_arg c (fun r -> RMeasureRec r))
 	    in
 	    let ids'' = List.fold_right Idset.add lf ids' in
 	     ((n, ro), List.rev rbl, 
@@ -924,11 +929,24 @@ let internalise sigma globalenv env allow_soapp lvar c =
         ((name_fold Idset.add na ids,ts,sc),
          (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
 
-  and intern_eqn n (ids,tmp_scope,scopes as _env) (loc,lhs,rhs) =
+  (* Expands a multiple pattern into a disjunction of multiple patterns *)
+  and intern_multiple_pattern scopes pl =
     let idsl_pll = 
-      List.map (intern_cases_pattern globalenv scopes ([],[]) None) lhs in
-
-    let eqn_ids,pll = product_of_cases_patterns [] idsl_pll in
+      List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in
+    product_of_cases_patterns [] idsl_pll
+
+  (* Expands a disjunction of multiple pattern *)
+  and intern_disjunctive_multiple_pattern scopes loc mpl =
+    assert (mpl <> []);
+    let mpl' = List.map (intern_multiple_pattern scopes) mpl in
+    let (idsl,mpl') = List.split mpl' in
+    let ids = List.hd idsl in
+    check_or_pat_variables loc ids (List.tl idsl);
+    (ids,List.flatten mpl')
+
+  (* Expands a pattern-matching clause [lhs => rhs] *)
+  and intern_eqn n (ids,tmp_scope,scopes) (loc,lhs,rhs) =
+    let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc lhs in
     (* Linearity implies the order in ids is irrelevant *)
     check_linearity lhs eqn_ids;
     check_number_of_pattern loc n (snd (List.hd pll));
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 37b30927..c4275589 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: genarg.mli 8926 2006-06-08 20:23:17Z herbelin $ i*)
+(*i $Id: genarg.mli 8983 2006-06-23 13:21:49Z herbelin $ i*)
 
 open Util
 open Names
@@ -60,20 +60,21 @@ Transformation for each type :
 \begin{verbatim}
 tag                            raw open type            cooked closed type
 
-BoolArgType                    bool                     bool
-IntArgType                     int                      int
-IntOrVarArgType                int or_var               int
-StringArgType                  string (parsed w/ "")    string
-PreIdentArgType                string (parsed w/o "")   (vernac only)
-IdentArgType                   identifier               identifier
-IntroPatternArgType            intro_pattern_expr       intro_pattern_expr
-VarArgType                     identifier               constr
-RefArgType                     reference                global_reference
-ConstrArgType                  constr_expr              constr
-ConstrMayEvalArgType           constr_expr may_eval     constr
-QuantHypArgType                quantified_hypothesis    quantified_hypothesis
-OpenConstrArgType              constr_expr              open_constr
-ConstrBindingsArgType      constr_expr with_bindings constr with_bindings
+BoolArgType                    bool                      bool
+IntArgType                     int                       int
+IntOrVarArgType                int or_var                int
+StringArgType                  string (parsed w/ "")     string
+PreIdentArgType                string (parsed w/o "")    (vernac only)
+IdentArgType                   identifier                identifier
+IntroPatternArgType            intro_pattern_expr        intro_pattern_expr
+VarArgType                     identifier located        identifier
+RefArgType                     reference                 global_reference
+QuantHypArgType                quantified_hypothesis     quantified_hypothesis
+ConstrArgType                  constr_expr               constr
+ConstrMayEvalArgType           constr_expr may_eval      constr
+OpenConstrArgType              open_constr_expr          open_constr
+ConstrWithBindingsArgType      constr_expr with_bindings constr with_bindings
+BindingsArgType                constr_expr bindings      constr bindings
 List0ArgType of argument_type
 List1ArgType of argument_type
 OptArgType of argument_type
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index f7256026..f3099346 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: topconstr.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: topconstr.ml 9032 2006-07-07 16:30:34Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -515,7 +515,7 @@ type constr_expr =
       (constr_expr * explicitation located option) list
   | CCases of loc * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
-      (loc * cases_pattern_expr list * constr_expr) list
+      (loc * cases_pattern_expr list list * constr_expr) list
   | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
@@ -544,6 +544,7 @@ and cofixpoint_expr =
 and recursion_order_expr = 
   | CStructRec
   | CWfRec of constr_expr
+  | CMeasureRec of constr_expr
 
 (***********************)
 (* For binders parsing *)
@@ -553,6 +554,11 @@ let rec local_binders_length = function
   | LocalRawDef _::bl -> 1 + local_binders_length bl
   | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
 
+let rec local_assums_length = function
+  | [] -> 0
+  | LocalRawDef _::bl -> local_binders_length bl
+  | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
+
 let names_of_local_assums bl =
   List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 8305ea54..51853089 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: topconstr.mli 8875 2006-05-29 19:59:11Z msozeau $ i*)
+(*i $Id: topconstr.mli 9032 2006-07-07 16:30:34Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -98,7 +98,7 @@ type constr_expr =
         (constr_expr * explicitation located option) list
   | CCases of loc * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
-      (loc * cases_pattern_expr list * constr_expr) list
+      (loc * cases_pattern_expr list list * constr_expr) list
   | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
@@ -122,6 +122,7 @@ and cofixpoint_expr =
 and recursion_order_expr = 
   | CStructRec
   | CWfRec of constr_expr
+  | CMeasureRec of constr_expr
 
 and local_binder =
   | LocalRawDef of name located * constr_expr
@@ -158,6 +159,9 @@ val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
 (* Includes let binders *)
 val local_binders_length : local_binder list -> int
 
+(* Excludes let binders *)
+val local_assums_length : local_binder list -> int
+
 (* Does not take let binders into account *)
 val names_of_local_assums : local_binder list -> name located list