From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 pretyping/rawterm.ml | 48 +++++++++++++++++++++++++++++++-----------------
 1 file changed, 31 insertions(+), 17 deletions(-)

(limited to 'pretyping/rawterm.ml')

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 5d177326..e61bf2c3 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: rawterm.ml 8624 2006-03-13 17:38:17Z msozeau $ *)
+(* $Id: rawterm.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
 
 (*i*)
 open Util
@@ -47,6 +47,10 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
+type cast_type =
+  | CastConv of cast_kind
+  | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
+
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -56,9 +60,7 @@ type rawconstr =
   | RLambda of loc * name * rawconstr * rawconstr
   | RProd of loc * name * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option *
-      (rawconstr * (name * (loc * inductive * name list) option)) list * 
-      (loc * identifier list * cases_pattern list * rawconstr) list
+  | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
@@ -66,19 +68,29 @@ type rawconstr =
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
   | RHole of (loc * hole_kind)
-  | RCast of loc * rawconstr * cast_kind * rawconstr
+  | RCast of loc * rawconstr * cast_type * rawconstr
   | RDynamic of loc * Dyn.t
 
 and rawdecl = name * rawconstr option * rawconstr
 
 and fix_recursion_order = RStructRec | RWfRec of rawconstr
 
-and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int
+and fix_kind =
+  | RFix of ((int option * fix_recursion_order) array * int)
+  | RCoFix of int
+
+and predicate_pattern =
+    name * (loc * inductive * int * name list) option
+
+and tomatch_tuple = (rawconstr * predicate_pattern) list
+
+and cases_clauses =
+    (loc * identifier list * cases_pattern list * rawconstr) list
 
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,(na,None)) -> [na]
-    | (tm,(na,Some (_,_,nal))) -> na::nal) tml)
+    | (tm,(na,Some (_,_,_,nal))) -> na::nal) tml)
 
 (*i - if PRec (_, names, arities, bodies) is in env then arities are
    typed in env too and bodies are typed in env enriched by the
@@ -89,7 +101,7 @@ let cases_predicate_names tml =
 
    - boolean in POldCase means it is recursive
 i*)
-let map_rawdecl f (na,obd,ty) = (na,option_app f obd,f ty)
+let map_rawdecl f (na,obd,ty) = (na,option_map f obd,f ty)
 
 let map_rawconstr f = function
   | RVar (loc,id) -> RVar (loc,id)
@@ -98,13 +110,13 @@ let map_rawconstr f = function
   | RProd (loc,na,ty,c) -> RProd (loc,na,f ty,f c)
   | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
   | RCases (loc,rtntypopt,tml,pl) ->
-      RCases (loc,option_app f rtntypopt,
+      RCases (loc,option_map f rtntypopt,
         List.map (fun (tm,x) -> (f tm,x)) tml,
         List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl)
   | RLetTuple (loc,nal,(na,po),b,c) ->
-      RLetTuple (loc,nal,(na,option_app f po),f b,f c)
+      RLetTuple (loc,nal,(na,option_map f po),f b,f c)
   | RIf (loc,c,(na,po),b1,b2) ->
-      RIf (loc,f c,(na,option_app f po),f b1,f b2)
+      RIf (loc,f c,(na,option_map f po),f b1,f b2)
   | RRec (loc,fk,idl,bl,tyl,bv) ->
       RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl,
             Array.map f tyl,Array.map f bv)
@@ -137,7 +149,7 @@ let map_rawconstr_with_binders_loc loc g f e = function
       let g' id e = snd (g id e) in
       let h (_,idl,p,c) = (loc,idl,p,f (List.fold_right g' idl e) c) in
       RCases
-	(loc,option_app (f e) tyopt,List.map (f e) tml, List.map h pl)
+	(loc,option_map (f e) tyopt,List.map (f e) tml, List.map h pl)
   | RRec (_,fk,idl,tyl,bv) ->
       let idl',e' = fold_ident g idl e in
       RRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv)
@@ -251,22 +263,24 @@ type 'a raw_red_flag = {
 let all_flags =
   {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []}
 
-type 'a occurrences = int list * 'a
+type 'a or_var = ArgArg of 'a | ArgVar of identifier located
+
+type 'a with_occurrences = int or_var list * 'a
 
 type ('a,'b) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl of 'a occurrences option
+  | Simpl of 'a with_occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
-  | Unfold of 'b occurrences list
+  | Unfold of 'b with_occurrences list
   | Fold of 'a list
-  | Pattern of 'a occurrences list
+  | Pattern of 'a with_occurrences list
   | ExtraRedExpr of string
   | CbvVm
 
 type ('a,'b) may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a, 'b) red_expr_gen * 'a
+  | ConstrEval of ('a,'b) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a
-- 
cgit v1.2.3