summaryrefslogtreecommitdiff
path: root/pretyping/rawterm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/rawterm.ml')
-rw-r--r--pretyping/rawterm.ml156
1 files changed, 87 insertions, 69 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 30b62ea8..ba523402 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: rawterm.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id$ *)
(*i*)
open Util
@@ -42,7 +42,7 @@ type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list
-type 'a bindings =
+type 'a bindings =
| ImplicitBindings of 'a list
| ExplicitBindings of 'a explicit_bindings
| NoBindings
@@ -53,7 +53,7 @@ type 'a cast_type =
| CastConv of cast_kind * 'a
| CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
-type rawconstr =
+type rawconstr =
| RRef of (loc * global_reference)
| RVar of (loc * identifier)
| REvar of loc * existential_key * rawconstr list option
@@ -63,7 +63,7 @@ type rawconstr =
| RProd of loc * name * binding_kind * rawconstr * rawconstr
| RLetIn of loc * name * rawconstr * rawconstr
| RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
- | RLetTuple of loc * name list * (name * rawconstr option) *
+ | RLetTuple of loc * name list * (name * rawconstr option) *
rawconstr * rawconstr
| RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
| RRec of loc * fix_kind * identifier array * rawdecl list array *
@@ -75,7 +75,7 @@ type rawconstr =
and rawdecl = name * binding_kind * rawconstr option * rawconstr
-and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr
+and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr * rawconstr option
and fix_kind =
| RFix of ((int option * fix_recursion_order) array * int)
@@ -97,37 +97,55 @@ let cases_predicate_names tml =
| (tm,(na,None)) -> [na]
| (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
- arities incrementally lifted
-
- [On pourrait plutot mettre les arités aves le type qu'elles auront
- dans le contexte servant à typer les body ???]
-
- - boolean in POldCase means it is recursive
-i*)
-let map_rawdecl f (na,k,obd,ty) = (na,k,Option.map f obd,f ty)
-
-let map_rawconstr f = function
- | RVar (loc,id) -> RVar (loc,id)
- | RApp (loc,g,args) -> RApp (loc,f g, List.map f args)
- | RLambda (loc,na,bk,ty,c) -> RLambda (loc,na,bk,f ty,f c)
- | RProd (loc,na,bk,ty,c) -> RProd (loc,na,bk,f ty,f c)
- | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
+let map_rawdecl_left_to_right f (na,k,obd,ty) =
+ let comp1 = Option.map f obd in
+ let comp2 = f ty in
+ (na,k,comp1,comp2)
+
+let map_rawconstr_left_to_right f = function
+ | RApp (loc,g,args) ->
+ let comp1 = f g in
+ let comp2 = Util.list_map_left f args in
+ RApp (loc,comp1,comp2)
+ | RLambda (loc,na,bk,ty,c) ->
+ let comp1 = f ty in
+ let comp2 = f c in
+ RLambda (loc,na,bk,comp1,comp2)
+ | RProd (loc,na,bk,ty,c) ->
+ let comp1 = f ty in
+ let comp2 = f c in
+ RProd (loc,na,bk,comp1,comp2)
+ | RLetIn (loc,na,b,c) ->
+ let comp1 = f b in
+ let comp2 = f c in
+ RLetIn (loc,na,comp1,comp2)
| RCases (loc,sty,rtntypopt,tml,pl) ->
- RCases (loc,sty,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)
+ let comp1 = Option.map f rtntypopt in
+ let comp2 = Util.list_map_left (fun (tm,x) -> (f tm,x)) tml in
+ let comp3 = Util.list_map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in
+ RCases (loc,sty,comp1,comp2,comp3)
| RLetTuple (loc,nal,(na,po),b,c) ->
- RLetTuple (loc,nal,(na,Option.map f po),f b,f c)
+ let comp1 = Option.map f po in
+ let comp2 = f b in
+ let comp3 = f c in
+ RLetTuple (loc,nal,(na,comp1),comp2,comp3)
| RIf (loc,c,(na,po),b1,b2) ->
- RIf (loc,f c,(na,Option.map f po),f b1,f b2)
+ let comp1 = Option.map f po in
+ let comp2 = f b1 in
+ let comp3 = f b2 in
+ RIf (loc,f c,(na,comp1),comp2,comp3)
| 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)
- | RCast (loc,c,k) -> RCast (loc,f c, match k with CastConv (k,t) -> CastConv (k, f t) | x -> x)
- | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
-
+ let comp1 = Array.map (Util.list_map_left (map_rawdecl_left_to_right f)) bl in
+ let comp2 = Array.map f tyl in
+ let comp3 = Array.map f bv in
+ RRec (loc,fk,idl,comp1,comp2,comp3)
+ | RCast (loc,c,k) ->
+ let comp1 = f c in
+ let comp2 = match k with CastConv (k,t) -> CastConv (k, f t) | x -> x in
+ RCast (loc,comp1,comp2)
+ | (RVar _ | RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
+
+let map_rawconstr = map_rawconstr_left_to_right
(*
let name_app f e = function
@@ -178,10 +196,10 @@ let occur_rawconstr id =
(occur_option rtntypopt)
or (List.exists (fun (tm,_) -> occur tm) tml)
or (List.exists occur_pattern pl)
- | RLetTuple (loc,nal,rtntyp,b,c) ->
+ | RLetTuple (loc,nal,rtntyp,b,c) ->
occur_return_type rtntyp id
or (occur b) or (not (List.mem (Name id) nal) & (occur c))
- | RIf (loc,c,rtntyp,b1,b2) ->
+ | RIf (loc,c,rtntyp,b1,b2) ->
occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
| RRec (loc,fk,idl,bl,tyl,bv) ->
not (array_for_all4 (fun fid bl ty bd ->
@@ -207,67 +225,67 @@ let occur_rawconstr id =
in occur
-let add_name_to_ids set na =
- match na with
- | Anonymous -> set
- | Name id -> Idset.add id set
+let add_name_to_ids set na =
+ match na with
+ | Anonymous -> set
+ | Name id -> Idset.add id set
let free_rawvars =
let rec vars bounded vs = function
| RVar (loc,id') -> if Idset.mem id' bounded then vs else Idset.add id' vs
| RApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
- | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) ->
- let vs' = vars bounded vs ty in
- let bounded' = add_name_to_ids bounded na in
+ | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) ->
+ let vs' = vars bounded vs ty in
+ let bounded' = add_name_to_ids bounded na in
vars bounded' vs' c
| RCases (loc,sty,rtntypopt,tml,pl) ->
- let vs1 = vars_option bounded vs rtntypopt in
- let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in
+ let vs1 = vars_option bounded vs rtntypopt in
+ let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in
List.fold_left (vars_pattern bounded) vs2 pl
| RLetTuple (loc,nal,rtntyp,b,c) ->
- let vs1 = vars_return_type bounded vs rtntyp in
- let vs2 = vars bounded vs1 b in
+ let vs1 = vars_return_type bounded vs rtntyp in
+ let vs2 = vars bounded vs1 b in
let bounded' = List.fold_left add_name_to_ids bounded nal in
vars bounded' vs2 c
- | RIf (loc,c,rtntyp,b1,b2) ->
- let vs1 = vars_return_type bounded vs rtntyp in
- let vs2 = vars bounded vs1 c in
- let vs3 = vars bounded vs2 b1 in
+ | RIf (loc,c,rtntyp,b1,b2) ->
+ let vs1 = vars_return_type bounded vs rtntyp in
+ let vs2 = vars bounded vs1 c in
+ let vs3 = vars bounded vs2 b1 in
vars bounded vs3 b2
| RRec (loc,fk,idl,bl,tyl,bv) ->
- let bounded' = Array.fold_right Idset.add idl bounded in
- let vars_fix i vs fid =
- let vs1,bounded1 =
- List.fold_left
- (fun (vs,bounded) (na,k,bbd,bty) ->
- let vs' = vars_option bounded vs bbd in
+ let bounded' = Array.fold_right Idset.add idl bounded in
+ let vars_fix i vs fid =
+ let vs1,bounded1 =
+ List.fold_left
+ (fun (vs,bounded) (na,k,bbd,bty) ->
+ let vs' = vars_option bounded vs bbd in
let vs'' = vars bounded vs' bty in
- let bounded' = add_name_to_ids bounded na in
+ let bounded' = add_name_to_ids bounded na in
(vs'',bounded')
)
(vs,bounded')
bl.(i)
in
- let vs2 = vars bounded1 vs1 tyl.(i) in
+ let vs2 = vars bounded1 vs1 tyl.(i) in
vars bounded1 vs2 bv.(i)
in
array_fold_left_i vars_fix vs idl
- | RCast (loc,c,k) -> let v = vars bounded vs c in
+ | RCast (loc,c,k) -> let v = vars bounded vs c in
(match k with CastConv (_,t) -> vars bounded v t | _ -> v)
| (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs
- and vars_pattern bounded vs (loc,idl,p,c) =
- let bounded' = List.fold_right Idset.add idl bounded in
+ and vars_pattern bounded vs (loc,idl,p,c) =
+ let bounded' = List.fold_right Idset.add idl bounded in
vars bounded' vs c
and vars_option bounded vs = function None -> vs | Some p -> vars bounded vs p
- and vars_return_type bounded vs (na,tyopt) =
- let bounded' = add_name_to_ids bounded na in
+ and vars_return_type bounded vs (na,tyopt) =
+ let bounded' = add_name_to_ids bounded na in
vars_option bounded' vs tyopt
- in
- fun rt ->
- let vs = vars Idset.empty Idset.empty rt in
+ in
+ fun rt ->
+ let vs = vars Idset.empty Idset.empty rt in
Idset.elements vs
@@ -344,10 +362,10 @@ let no_occurrences_expr = (true,[])
type 'a with_occurrences = occurrences_expr * 'a
-type ('a,'b) red_expr_gen =
+type ('a,'b,'c) red_expr_gen =
| Red of bool
| Hnf
- | Simpl of 'a with_occurrences option
+ | Simpl of 'c with_occurrences option
| Cbv of 'b raw_red_flag
| Lazy of 'b raw_red_flag
| Unfold of 'b with_occurrences list
@@ -356,8 +374,8 @@ type ('a,'b) red_expr_gen =
| ExtraRedExpr of string
| CbvVm
-type ('a,'b) may_eval =
+type ('a,'b,'c) may_eval =
| ConstrTerm of 'a
- | ConstrEval of ('a,'b) red_expr_gen * 'a
+ | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
| ConstrContext of (loc * identifier) * 'a
| ConstrTypeOf of 'a
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 04:37:41 +0000