diff options
Diffstat (limited to 'pretyping/rawterm.ml')
-rw-r--r-- | pretyping/rawterm.ml | 156 |
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 |