diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 8 | ||||
| -rw-r--r-- | pretyping/cases.mli | 4 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 164 | ||||
| -rw-r--r-- | pretyping/detyping.mli | 22 | ||||
| -rw-r--r-- | pretyping/pattern.ml | 44 | ||||
| -rw-r--r-- | pretyping/pattern.mli | 4 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 82 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 36 | ||||
| -rw-r--r-- | pretyping/rawterm.ml | 266 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 76 |
10 files changed, 353 insertions, 353 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c61edbc55e..5115b3e3b7 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -66,9 +66,9 @@ let error_needs_inversion env x t = module type S = sig val compile_cases : loc -> case_style -> - (type_constraint -> env -> evar_map ref -> rawconstr -> unsafe_judgment) * evar_map ref -> + (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> type_constraint -> - env -> rawconstr option * tomatch_tuples * cases_clauses -> + env -> glob_constr option * tomatch_tuples * cases_clauses -> unsafe_judgment end @@ -348,7 +348,7 @@ let find_tomatch_tycon evdref env loc = function empty_tycon,None let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) = - let loc = Some (loc_of_rawconstr tomatch) in + let loc = Some (loc_of_glob_constr tomatch) in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in let j = typing_fun tycon env evdref tomatch in let typ = nf_evar !evdref j.uj_type in @@ -1228,7 +1228,7 @@ let matx_of_eqns env tomatchl eqns = let initial_rhs = rhs in let rhs = { rhs_env = env; - rhs_vars = free_rawvars initial_rhs; + rhs_vars = free_glob_vars initial_rhs; avoid_ids = ids@(ids_of_named_context (named_context env)); it = Some initial_rhs } in { patterns = initial_lpat; diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 2facf8696f..015b386a55 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -61,9 +61,9 @@ type tomatch_status = module type S = sig val compile_cases : loc -> case_style -> - (type_constraint -> env -> evar_map ref -> rawconstr -> unsafe_judgment) * evar_map ref -> + (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> type_constraint -> - env -> rawconstr option * tomatch_tuples * cases_clauses -> + env -> glob_constr option * tomatch_tuples * cases_clauses -> unsafe_judgment end diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 04dc132903..7469111bfc 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -275,30 +275,30 @@ let is_nondep_branch c n = let extract_nondep_branches test c b n = let rec strip n r = if n=0 then r else match r with - | RLambda (_,_,_,_,t) -> strip (n-1) t - | RLetIn (_,_,_,t) -> strip (n-1) t + | GLambda (_,_,_,_,t) -> strip (n-1) t + | GLetIn (_,_,_,t) -> strip (n-1) t | _ -> assert false in if test c n then Some (strip n b) else None let it_destRLambda_or_LetIn_names n c = let rec aux n nal c = if n=0 then (List.rev nal,c) else match c with - | RLambda (_,na,_,_,c) -> aux (n-1) (na::nal) c - | RLetIn (_,na,_,c) -> aux (n-1) (na::nal) c + | GLambda (_,na,_,_,c) -> aux (n-1) (na::nal) c + | GLetIn (_,na,_,c) -> aux (n-1) (na::nal) c | _ -> (* eta-expansion *) let rec next l = let x = next_ident_away (id_of_string "x") l in - (* Not efficient but unusual and no function to get free rawvars *) -(* if occur_rawconstr x c then next (x::l) else x in *) + (* Not efficient but unusual and no function to get free glob_vars *) +(* if occur_glob_constr x c then next (x::l) else x in *) x in - let x = next (free_rawvars c) in - let a = RVar (dl,x) in + let x = next (free_glob_vars c) in + let a = GVar (dl,x) in aux (n-1) (Name x :: nal) (match c with - | RApp (loc,p,l) -> RApp (loc,c,l@[a]) - | _ -> (RApp (dl,c,[a]))) + | GApp (loc,p,l) -> GApp (loc,c,l@[a]) + | _ -> (GApp (dl,c,[a]))) in aux n [] c let detype_case computable detype detype_eqns testdep avoid data p c bl = @@ -315,7 +315,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | Some p -> let nl,typ = it_destRLambda_or_LetIn_names k p in let n,typ = match typ with - | RLambda (_,x,_,t,c) -> x, c + | GLambda (_,x,_,t,c) -> x, c | _ -> Anonymous, typ in let aliastyp = if List.for_all ((=) Anonymous) nl then None @@ -341,20 +341,20 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | LetStyle when aliastyp = None -> let bl' = Array.map detype bl in let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in - RLetTuple (dl,nal,(alias,pred),tomatch,d) + GLetTuple (dl,nal,(alias,pred),tomatch,d) | IfStyle when aliastyp = None -> let bl' = Array.map detype bl in let nondepbrs = array_map3 (extract_nondep_branches testdep) bl bl' consnargsl in if array_for_all ((<>) None) nondepbrs then - RIf (dl,tomatch,(alias,pred), + GIf (dl,tomatch,(alias,pred), Option.get nondepbrs.(0),Option.get nondepbrs.(1)) else let eqnl = detype_eqns constructs consnargsl bl in - RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) + GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) | _ -> let eqnl = detype_eqns constructs consnargsl bl in - RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) + GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) let detype_sort = function | Prop c -> RProp c @@ -372,36 +372,36 @@ let rec detype (isgoal:bool) avoid env t = match kind_of_term (collapse_appl t) with | Rel n -> (try match lookup_name_of_rel n env with - | Name id -> RVar (dl, id) + | Name id -> GVar (dl, id) | Anonymous -> !detype_anonymous dl n with Not_found -> let s = "_UNBOUND_REL_"^(string_of_int n) - in RVar (dl, id_of_string s)) + in GVar (dl, id_of_string s)) | Meta n -> (* Meta in constr are not user-parsable and are mapped to Evar *) - REvar (dl, n, None) + GEvar (dl, n, None) | Var id -> (try - let _ = Global.lookup_named id in RRef (dl, VarRef id) + let _ = Global.lookup_named id in GRef (dl, VarRef id) with _ -> - RVar (dl, id)) - | Sort s -> RSort (dl,detype_sort s) + GVar (dl, id)) + | Sort s -> GSort (dl,detype_sort s) | Cast (c1,k,c2) -> - RCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2)) + GCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2)) | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c | App (f,args) -> - RApp (dl,detype isgoal avoid env f, + GApp (dl,detype isgoal avoid env f, array_map_to_list (detype isgoal avoid env) args) - | Const sp -> RRef (dl, ConstRef sp) + | Const sp -> GRef (dl, ConstRef sp) | Evar (ev,cl) -> - REvar (dl, ev, + GEvar (dl, ev, Some (List.map (detype isgoal avoid env) (Array.to_list cl))) | Ind ind_sp -> - RRef (dl, IndRef ind_sp) + GRef (dl, IndRef ind_sp) | Construct cstr_sp -> - RRef (dl, ConstructRef cstr_sp) + GRef (dl, ConstructRef cstr_sp) | Case (ci,p,c,bl) -> let comp = computable p (ci.ci_pp_info.ind_nargs) in detype_case comp (detype isgoal avoid env) @@ -424,7 +424,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) = let v = array_map3 (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t)) bodies tys vn in - RRec(dl,RFix (Array.map (fun i -> Some i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), + GRec(dl,RFix (Array.map (fun i -> Some i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) @@ -440,7 +440,7 @@ and detype_cofix isgoal avoid env n (names,tys,bodies) = let v = array_map2 (fun c t -> share_names isgoal 0 [] def_avoid def_env c (lift ntys t)) bodies tys in - RRec(dl,RCoFix n,Array.of_list (List.rev lfi), + GRec(dl,RCoFix n,Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) @@ -535,9 +535,9 @@ and detype_binder isgoal bk avoid env na ty c = else compute_displayed_name_in flag avoid na c in let r = detype isgoal avoid' (add_name na' env) c in match bk with - | BProd -> RProd (dl, na',Explicit,detype false avoid env ty, r) - | BLambda -> RLambda (dl, na',Explicit,detype false avoid env ty, r) - | BLetIn -> RLetIn (dl, na',detype false avoid env ty, r) + | BProd -> GProd (dl, na',Explicit,detype false avoid env ty, r) + | BLambda -> GLambda (dl, na',Explicit,detype false avoid env ty, r) + | BLetIn -> GLetIn (dl, na',detype false avoid env ty, r) let rec detype_rel_context where avoid env sign = let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in @@ -569,42 +569,42 @@ let rec subst_cases_pattern subst pat = if kn' == kn && cpl' == cpl then pat else PatCstr (loc,((kn',i),j),cpl',n) -let rec subst_rawconstr subst raw = +let rec subst_glob_constr subst raw = match raw with - | RRef (loc,ref) -> + | GRef (loc,ref) -> let ref',t = subst_global subst ref in if ref' == ref then raw else detype false [] [] t - | RVar _ -> raw - | REvar _ -> raw - | RPatVar _ -> raw + | GVar _ -> raw + | GEvar _ -> raw + | GPatVar _ -> raw - | RApp (loc,r,rl) -> - let r' = subst_rawconstr subst r - and rl' = list_smartmap (subst_rawconstr subst) rl in + | GApp (loc,r,rl) -> + let r' = subst_glob_constr subst r + and rl' = list_smartmap (subst_glob_constr subst) rl in if r' == r && rl' == rl then raw else - RApp(loc,r',rl') + GApp(loc,r',rl') - | RLambda (loc,n,bk,r1,r2) -> - let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in + | GLambda (loc,n,bk,r1,r2) -> + let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in if r1' == r1 && r2' == r2 then raw else - RLambda (loc,n,bk,r1',r2') + GLambda (loc,n,bk,r1',r2') - | RProd (loc,n,bk,r1,r2) -> - let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in + | GProd (loc,n,bk,r1,r2) -> + let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in if r1' == r1 && r2' == r2 then raw else - RProd (loc,n,bk,r1',r2') + GProd (loc,n,bk,r1',r2') - | RLetIn (loc,n,r1,r2) -> - let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in + | GLetIn (loc,n,r1,r2) -> + let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in if r1' == r1 && r2' == r2 then raw else - RLetIn (loc,n,r1',r2') + GLetIn (loc,n,r1',r2') - | RCases (loc,sty,rtno,rl,branches) -> - let rtno' = Option.smartmap (subst_rawconstr subst) rtno + | GCases (loc,sty,rtno,rl,branches) -> + let rtno' = Option.smartmap (subst_glob_constr subst) rtno and rl' = list_smartmap (fun (a,x as y) -> - let a' = subst_rawconstr subst a in + let a' = subst_glob_constr subst a in let (n,topt) = x in let topt' = Option.smartmap (fun (loc,(sp,i),x,y as t) -> @@ -615,61 +615,61 @@ let rec subst_rawconstr subst raw = (fun (loc,idl,cpl,r as branch) -> let cpl' = list_smartmap (subst_cases_pattern subst) cpl - and r' = subst_rawconstr subst r in + and r' = subst_glob_constr subst r in if cpl' == cpl && r' == r then branch else (loc,idl,cpl',r')) branches in if rtno' == rtno && rl' == rl && branches' == branches then raw else - RCases (loc,sty,rtno',rl',branches') + GCases (loc,sty,rtno',rl',branches') - | RLetTuple (loc,nal,(na,po),b,c) -> - let po' = Option.smartmap (subst_rawconstr subst) po - and b' = subst_rawconstr subst b - and c' = subst_rawconstr subst c in + | GLetTuple (loc,nal,(na,po),b,c) -> + let po' = Option.smartmap (subst_glob_constr subst) po + and b' = subst_glob_constr subst b + and c' = subst_glob_constr subst c in if po' == po && b' == b && c' == c then raw else - RLetTuple (loc,nal,(na,po'),b',c') + GLetTuple (loc,nal,(na,po'),b',c') - | RIf (loc,c,(na,po),b1,b2) -> - let po' = Option.smartmap (subst_rawconstr subst) po - and b1' = subst_rawconstr subst b1 - and b2' = subst_rawconstr subst b2 - and c' = subst_rawconstr subst c in + | GIf (loc,c,(na,po),b1,b2) -> + let po' = Option.smartmap (subst_glob_constr subst) po + and b1' = subst_glob_constr subst b1 + and b2' = subst_glob_constr subst b2 + and c' = subst_glob_constr subst c in if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else - RIf (loc,c',(na,po'),b1',b2') + GIf (loc,c',(na,po'),b1',b2') - | RRec (loc,fix,ida,bl,ra1,ra2) -> - let ra1' = array_smartmap (subst_rawconstr subst) ra1 - and ra2' = array_smartmap (subst_rawconstr subst) ra2 in + | GRec (loc,fix,ida,bl,ra1,ra2) -> + let ra1' = array_smartmap (subst_glob_constr subst) ra1 + and ra2' = array_smartmap (subst_glob_constr subst) ra2 in let bl' = array_smartmap (list_smartmap (fun (na,k,obd,ty as dcl) -> - let ty' = subst_rawconstr subst ty in - let obd' = Option.smartmap (subst_rawconstr subst) obd in + let ty' = subst_glob_constr subst ty in + let obd' = Option.smartmap (subst_glob_constr subst) obd in if ty'==ty & obd'==obd then dcl else (na,k,obd',ty'))) bl in if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else - RRec (loc,fix,ida,bl',ra1',ra2') + GRec (loc,fix,ida,bl',ra1',ra2') - | RSort _ -> raw + | GSort _ -> raw - | RHole (loc,ImplicitArg (ref,i,b)) -> + | GHole (loc,ImplicitArg (ref,i,b)) -> let ref',_ = subst_global subst ref in if ref' == ref then raw else - RHole (loc,InternalHole) - | RHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole | + GHole (loc,InternalHole) + | GHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole | TomatchTypeParameter _ | GoalEvar | ImpossibleCase | MatchingVar _)) -> raw - | RCast (loc,r1,k) -> + | GCast (loc,r1,k) -> (match k with CastConv (k,r2) -> - let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in + let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in if r1' == r1 && r2' == r2 then raw else - RCast (loc,r1', CastConv (k,r2')) + GCast (loc,r1', CastConv (k,r2')) | CastCoerce -> - let r1' = subst_rawconstr subst r1 in - if r1' == r1 then raw else RCast (loc,r1',k)) - | RDynamic _ -> raw + let r1' = subst_glob_constr subst r1 in + if r1' == r1 then raw else GCast (loc,r1',k)) + | GDynamic _ -> raw (* Utilities to transform kernel cases to simple pattern-matching problem *) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index e178a4ca3f..e2644592cb 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -17,40 +17,40 @@ open Mod_subst val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern -val subst_rawconstr : substitution -> rawconstr -> rawconstr +val subst_glob_constr : substitution -> glob_constr -> glob_constr -(** [detype isgoal avoid ctx c] turns a closed [c], into a rawconstr +(** [detype isgoal avoid ctx c] turns a closed [c], into a glob_constr de Bruijn indexes are turned to bound names, avoiding names in [avoid] [isgoal] tells if naming must avoid global-level synonyms as intro does [ctx] gives the names of the free variables *) -val detype : bool -> identifier list -> names_context -> constr -> rawconstr +val detype : bool -> identifier list -> names_context -> constr -> glob_constr val detype_case : - bool -> ('a -> rawconstr) -> + bool -> ('a -> glob_constr) -> (constructor array -> int array -> 'a array -> - (loc * identifier list * cases_pattern list * rawconstr) list) -> + (loc * identifier list * cases_pattern list * glob_constr) list) -> ('a -> int -> bool) -> identifier list -> inductive * case_style * int * int array * int -> - 'a option -> 'a -> 'a array -> rawconstr + 'a option -> 'a -> 'a array -> glob_constr val detype_sort : sorts -> rawsort val detype_rel_context : constr option -> identifier list -> names_context -> - rel_context -> rawdecl list + rel_context -> glob_decl list (** look for the index of a named var or a nondep var as it is renamed *) val lookup_name_as_displayed : env -> constr -> identifier -> int option val lookup_index_as_renamed : env -> constr -> int -> int option -val set_detype_anonymous : (loc -> int -> rawconstr) -> unit +val set_detype_anonymous : (loc -> int -> glob_constr) -> unit val force_wildcard : unit -> bool val synthetize_type : unit -> bool (** Utilities to transform kernel cases to simple pattern-matching problem *) -val it_destRLambda_or_LetIn_names : int -> rawconstr -> name list * rawconstr +val it_destRLambda_or_LetIn_names : int -> glob_constr -> name list * glob_constr val simple_cases_matrix_of_branches : - inductive -> int list -> rawconstr list -> cases_clauses + inductive -> int list -> glob_constr list -> cases_clauses val return_type_of_predicate : - inductive -> int -> int -> rawconstr -> predicate_pattern * rawconstr option + inductive -> int -> int -> glob_constr -> predicate_pattern * glob_constr option diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 15bc06e025..2217074fe4 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -248,48 +248,48 @@ let mkPLambda na b = PLambda(na,PMeta None,b) let rev_it_mkPLambda = List.fold_right mkPLambda 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,_) -> + | GCast (_,c,_) -> Flags.if_verbose Pp.warning "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 + | GLetTuple (loc,nal,(_,None),b,c) -> + let mkRLambda c na = GLambda (loc,na,Explicit,GHole (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) -> + | GCases (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)), @@ -307,34 +307,34 @@ let rec pat_of_raw metas vars = function 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.") + let loc = loc_of_glob_constr r in + user_err_loc (loc,"pattern_of_glob_constr", 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", + user_err_loc (loc,"pattern_of_glob_constr", 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", + user_err_loc (loc,"pattern_of_glob_constr", 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", + user_err_loc (loc,"pattern_of_glob_constr", 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", + | _ -> user_err_loc (loc,"pattern_of_glob_constr", str "No unique branch for " ++ int (i+1) ++ str"-th constructor.") -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) diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 7dadb78f30..a739a28887 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -103,11 +103,11 @@ val head_of_constr_reference : Term.constr -> global_reference val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern -(** [pattern_of_rawconstr l c] translates a term [c] with metavariables into +(** [pattern_of_glob_constr l c] translates a term [c] with metavariables into a pattern; variables bound in [l] are replaced by the pattern to which they are bound *) -val pattern_of_rawconstr : rawconstr -> +val pattern_of_glob_constr : glob_constr -> patvar list * constr_pattern val instantiate_pattern : diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7017edaf28..bc80296d57 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -48,7 +48,7 @@ type typing_constraint = OfType of types option | IsType type var_map = (identifier * constr_under_binders) list type unbound_ltac_var_map = (identifier * identifier option) list type ltac_var_map = var_map * unbound_ltac_var_map -type rawconstr_ltac_closure = ltac_var_map * rawconstr +type glob_constr_ltac_closure = ltac_var_map * glob_constr (************************************************************************) (* This concerns Cases *) @@ -86,7 +86,7 @@ let search_guard loc env possible_indexes fixdefs = user_err_loc (loc,"search_guard", Pp.str errmsg) with Found indexes -> indexes) -(* To embed constr in rawconstr *) +(* To embed constr in glob_constr *) let ((constr_in : constr -> Dyn.t), (constr_out : Dyn.t -> constr)) = Dyn.create "constr" @@ -109,19 +109,19 @@ sig (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) val allow_anonymous_refs : bool ref - (* Generic call to the interpreter from rawconstr to open_constr, leaving + (* Generic call to the interpreter from glob_constr to open_constr, leaving unresolved holes as evars and returning the typing contexts of these evars. Work as [understand_gen] for the rest. *) val understand_tcc : ?resolve_classes:bool -> - evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr + evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool -> - evar_map ref -> env -> typing_constraint -> rawconstr -> constr + evar_map ref -> env -> typing_constraint -> glob_constr -> constr (* More general entry point with evars from ltac *) - (* Generic call to the interpreter from rawconstr to constr, failing + (* Generic call to the interpreter from glob_constr to constr, failing unresolved holes in the rawterm cannot be instantiated. In [understand_ltac expand_evars sigma env ltac_env constraint c], @@ -134,29 +134,29 @@ sig val understand_ltac : bool -> evar_map -> env -> ltac_var_map -> - typing_constraint -> rawconstr -> evar_map * constr + typing_constraint -> glob_constr -> evar_map * constr - (* Standard call to get a constr from a rawconstr, resolving implicit args *) + (* Standard call to get a constr from a glob_constr, resolving implicit args *) val understand : evar_map -> env -> ?expected_type:Term.types -> - rawconstr -> constr + glob_constr -> constr - (* Idem but the rawconstr is intended to be a type *) + (* Idem but the glob_constr is intended to be a type *) - val understand_type : evar_map -> env -> rawconstr -> constr + val understand_type : evar_map -> env -> glob_constr -> constr (* A generalization of the two previous case *) val understand_gen : typing_constraint -> evar_map -> env -> - rawconstr -> constr + glob_constr -> constr (* Idem but returns the judgment of the understood term *) - val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment + val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment (* Idem but do not fail on unresolved evars *) - val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment + val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment (*i*) (* Internal of Pretyping... @@ -164,15 +164,15 @@ sig *) val pretype : type_constraint -> env -> evar_map ref -> - ltac_var_map -> rawconstr -> unsafe_judgment + ltac_var_map -> glob_constr -> unsafe_judgment val pretype_type : val_constraint -> env -> evar_map ref -> - ltac_var_map -> rawconstr -> unsafe_type_judgment + ltac_var_map -> glob_constr -> unsafe_type_judgment val pretype_gen : bool -> bool -> bool -> evar_map ref -> env -> - ltac_var_map -> typing_constraint -> rawconstr -> constr + ltac_var_map -> typing_constraint -> glob_constr -> constr (*i*) end @@ -302,17 +302,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) let rec pretype (tycon : type_constraint) env evdref lvar = function - | RRef (loc,ref) -> + | GRef (loc,ref) -> inh_conv_coerce_to_tycon loc env evdref (pretype_ref evdref env ref) tycon - | RVar (loc, id) -> + | GVar (loc, id) -> inh_conv_coerce_to_tycon loc env evdref (pretype_id loc env !evdref lvar id) tycon - | REvar (loc, evk, instopt) -> + | GEvar (loc, evk, instopt) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) let hyps = evar_filtered_context (Evd.find !evdref evk) in @@ -323,7 +323,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let j = (Retyping.get_judgment_of env !evdref c) in inh_conv_coerce_to_tycon loc env evdref j tycon - | RPatVar (loc,(someta,n)) -> + | GPatVar (loc,(someta,n)) -> let ty = match tycon with | Some (None, ty) -> ty @@ -332,7 +332,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let k = MatchingVar (someta,n) in { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } - | RHole (loc,k) -> + | GHole (loc,k) -> let ty = match tycon with | Some (None, ty) -> ty @@ -340,7 +340,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } - | RRec (loc,fixkind,names,bl,lar,vdef) -> + | GRec (loc,fixkind,names,bl,lar,vdef) -> let rec type_bl env ctxt = function [] -> ctxt | (na,bk,None,ty)::bl -> @@ -403,16 +403,16 @@ module Pretyping_F (Coercion : Coercion.S) = struct make_judge (mkCoFix cofix) ftys.(i) in inh_conv_coerce_to_tycon loc env evdref fixj tycon - | RSort (loc,s) -> + | GSort (loc,s) -> inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon - | RApp (loc,f,args) -> + | GApp (loc,f,args) -> let fj = pretype empty_tycon env evdref lvar f in - let floc = loc_of_rawconstr f in + let floc = loc_of_glob_constr f in let rec apply_rec env n resj = function | [] -> resj | c::rest -> - let argloc = loc_of_rawconstr c in + let argloc = loc_of_glob_constr c in let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in let resty = whd_betadeltaiota env !evdref resj.uj_type in match kind_of_term resty with @@ -446,7 +446,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | _ -> resj in inh_conv_coerce_to_tycon loc env evdref resj tycon - | RLambda(loc,name,bk,c1,c2) -> + | GLambda(loc,name,bk,c1,c2) -> let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env evdref lvar c1 in @@ -454,7 +454,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let j' = pretype rng (push_rel var env) evdref lvar c2 in judge_of_abstraction env (orelse_name name name') j j' - | RProd(loc,name,bk,c1,c2) -> + | GProd(loc,name,bk,c1,c2) -> let j = pretype_type empty_valcon env evdref lvar c1 in let j' = if name = Anonymous then @@ -470,10 +470,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct with TypeError _ as e -> Loc.raise loc e in inh_conv_coerce_to_tycon loc env evdref resj tycon - | RLetIn(loc,name,c1,c2) -> + | GLetIn(loc,name,c1,c2) -> let j = match c1 with - | RCast (loc, c, CastConv (DEFAULTcast, t)) -> + | GCast (loc, c, CastConv (DEFAULTcast, t)) -> let tj = pretype_type empty_valcon env evdref lvar t in pretype (mk_tycon tj.utj_val) env evdref lvar c | _ -> pretype empty_tycon env evdref lvar c1 @@ -485,12 +485,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; uj_type = subst1 j.uj_val j'.uj_type } - | RLetTuple (loc,nal,(na,po),c,d) -> + | GLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = try find_rectype env !evdref cj.uj_type with Not_found -> - let cloc = loc_of_rawconstr c in + let cloc = loc_of_glob_constr c in error_case_not_inductive_loc cloc env !evdref cj in let cstrs = get_constructors env indf in @@ -551,12 +551,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct in { uj_val = v; uj_type = ccl }) - | RIf (loc,c,(na,po),b1,b2) -> + | GIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = try find_rectype env !evdref cj.uj_type with Not_found -> - let cloc = loc_of_rawconstr c in + let cloc = loc_of_glob_constr c in error_case_not_inductive_loc cloc env !evdref cj in let cstrs = get_constructors env indf in if Array.length cstrs <> 2 then @@ -619,12 +619,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct in { uj_val = v; uj_type = p } - | RCases (loc,sty,po,tml,eqns) -> + | GCases (loc,sty,po,tml,eqns) -> Cases.compile_cases loc sty ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) tycon env (* loc *) (po,tml,eqns) - | RCast (loc,c,k) -> + | GCast (loc,c,k) -> let cj = match k with CastCoerce -> @@ -643,7 +643,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct { uj_val = v; uj_type = tval } in inh_conv_coerce_to_tycon loc env evdref cj tycon - | RDynamic (loc,d) -> + | GDynamic (loc,d) -> if (Dyn.tag d) = "constr" then let c = constr_out d in let j = (Retyping.get_judgment_of env !evdref c) in @@ -654,7 +654,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type valcon env evdref lvar = function - | RHole loc -> + | GHole loc -> (match valcon with | Some v -> let s = @@ -674,7 +674,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct utj_type = s}) | c -> let j = pretype empty_tycon env evdref lvar c in - let loc = loc_of_rawconstr c in + let loc = loc_of_glob_constr c in let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in match valcon with | None -> tj @@ -682,7 +682,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct if e_cumul env evdref v tj.utj_val then tj else error_unexpected_type_loc - (loc_of_rawconstr c) env !evdref tj.utj_val v + (loc_of_glob_constr c) env !evdref tj.utj_val v let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c = let c' = match kind with diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 7f707de3d2..8c02707436 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** This file implements type inference. It maps [rawconstr] +(** This file implements type inference. It maps [glob_constr] (i.e. untyped terms whose names are located) to [constr]. In particular, it drives complex pattern-matching problems ("match") into elementary ones, insertion of coercions and resolution of @@ -30,7 +30,7 @@ type typing_constraint = OfType of types option | IsType type var_map = (identifier * Pattern.constr_under_binders) list type unbound_ltac_var_map = (identifier * identifier option) list type ltac_var_map = var_map * unbound_ltac_var_map -type rawconstr_ltac_closure = ltac_var_map * rawconstr +type glob_constr_ltac_closure = ltac_var_map * glob_constr module type S = sig @@ -40,19 +40,19 @@ sig (** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) val allow_anonymous_refs : bool ref - (** Generic call to the interpreter from rawconstr to open_constr, leaving + (** Generic call to the interpreter from glob_constr to open_constr, leaving unresolved holes as evars and returning the typing contexts of these evars. Work as [understand_gen] for the rest. *) val understand_tcc : ?resolve_classes:bool -> - evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr + evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool -> - evar_map ref -> env -> typing_constraint -> rawconstr -> constr + evar_map ref -> env -> typing_constraint -> glob_constr -> constr (** More general entry point with evars from ltac *) - (** Generic call to the interpreter from rawconstr to constr, failing + (** Generic call to the interpreter from glob_constr to constr, failing unresolved holes in the rawterm cannot be instantiated. In [understand_ltac expand_evars sigma env ltac_env constraint c], @@ -65,42 +65,42 @@ sig val understand_ltac : bool -> evar_map -> env -> ltac_var_map -> - typing_constraint -> rawconstr -> evar_map * constr + typing_constraint -> glob_constr -> evar_map * constr - (** Standard call to get a constr from a rawconstr, resolving implicit args *) + (** Standard call to get a constr from a glob_constr, resolving implicit args *) val understand : evar_map -> env -> ?expected_type:Term.types -> - rawconstr -> constr + glob_constr -> constr - (** Idem but the rawconstr is intended to be a type *) + (** Idem but the glob_constr is intended to be a type *) - val understand_type : evar_map -> env -> rawconstr -> constr + val understand_type : evar_map -> env -> glob_constr -> constr (** A generalization of the two previous case *) val understand_gen : typing_constraint -> evar_map -> env -> - rawconstr -> constr + glob_constr -> constr (** Idem but returns the judgment of the understood term *) - val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment + val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment (** Idem but do not fail on unresolved evars *) - val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment + val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment (**/**) (** Internal of Pretyping... *) val pretype : type_constraint -> env -> evar_map ref -> - ltac_var_map -> rawconstr -> unsafe_judgment + ltac_var_map -> glob_constr -> unsafe_judgment val pretype_type : val_constraint -> env -> evar_map ref -> - ltac_var_map -> rawconstr -> unsafe_type_judgment + ltac_var_map -> glob_constr -> unsafe_type_judgment val pretype_gen : bool -> bool -> bool -> evar_map ref -> env -> - ltac_var_map -> typing_constraint -> rawconstr -> constr + ltac_var_map -> typing_constraint -> glob_constr -> constr (**/**) @@ -109,7 +109,7 @@ end module Pretyping_F (C : Coercion.S) : S module Default : S -(** To embed constr in rawconstr *) +(** To embed constr in glob_constr *) val constr_in : constr -> Dyn.t val constr_out : Dyn.t -> constr diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 88dc5db42f..deba9a257a 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -49,29 +49,29 @@ type 'a cast_type = | CastConv of cast_kind * 'a | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *) -type rawconstr = - | RRef of (loc * global_reference) - | RVar of (loc * identifier) - | REvar of loc * existential_key * rawconstr list option - | RPatVar of loc * (bool * patvar) (* Used for patterns only *) - | RApp of loc * rawconstr * rawconstr list - | RLambda of loc * name * binding_kind * rawconstr * 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) * - rawconstr * rawconstr - | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr - | RRec of loc * fix_kind * identifier array * rawdecl list array * - rawconstr array * rawconstr array - | RSort of loc * rawsort - | RHole of (loc * hole_kind) - | RCast of loc * rawconstr * rawconstr cast_type - | RDynamic of loc * Dyn.t - -and rawdecl = name * binding_kind * rawconstr option * rawconstr - -and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr * rawconstr option +type glob_constr = + | GRef of (loc * global_reference) + | GVar of (loc * identifier) + | GEvar of loc * existential_key * glob_constr list option + | GPatVar of loc * (bool * patvar) (* Used for patterns only *) + | GApp of loc * glob_constr * glob_constr list + | GLambda of loc * name * binding_kind * glob_constr * glob_constr + | GProd of loc * name * binding_kind * glob_constr * glob_constr + | GLetIn of loc * name * glob_constr * glob_constr + | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses + | GLetTuple of loc * name list * (name * glob_constr option) * + glob_constr * glob_constr + | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr + | GRec of loc * fix_kind * identifier array * glob_decl list array * + glob_constr array * glob_constr array + | GSort of loc * rawsort + | GHole of (loc * hole_kind) + | GCast of loc * glob_constr * glob_constr cast_type + | GDynamic of loc * Dyn.t + +and glob_decl = name * binding_kind * glob_constr option * glob_constr + +and fix_recursion_order = RStructRec | RWfRec of glob_constr | RMeasureRec of glob_constr * glob_constr option and fix_kind = | RFix of ((int option * fix_recursion_order) array * int) @@ -80,11 +80,11 @@ and fix_kind = and predicate_pattern = name * (loc * inductive * int * name list) option -and tomatch_tuple = (rawconstr * predicate_pattern) +and tomatch_tuple = (glob_constr * predicate_pattern) and tomatch_tuples = tomatch_tuple list -and cases_clause = (loc * identifier list * cases_pattern list * rawconstr) +and cases_clause = (loc * identifier list * cases_pattern list * glob_constr) and cases_clauses = cases_clause list @@ -93,55 +93,55 @@ let cases_predicate_names tml = | (tm,(na,None)) -> [na] | (tm,(na,Some (_,_,_,nal))) -> na::nal) tml) -let map_rawdecl_left_to_right f (na,k,obd,ty) = +let map_glob_decl_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 map_glob_constr_left_to_right f = function + | GApp (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) -> + GApp (loc,comp1,comp2) + | GLambda (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) -> + GLambda (loc,na,bk,comp1,comp2) + | GProd (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) -> + GProd (loc,na,bk,comp1,comp2) + | GLetIn (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) -> + GLetIn (loc,na,comp1,comp2) + | GCases (loc,sty,rtntypopt,tml,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) -> + GCases (loc,sty,comp1,comp2,comp3) + | GLetTuple (loc,nal,(na,po),b,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) -> + GLetTuple (loc,nal,(na,comp1),comp2,comp3) + | GIf (loc,c,(na,po),b1,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) -> - let comp1 = Array.map (Util.list_map_left (map_rawdecl_left_to_right f)) bl in + GIf (loc,f c,(na,comp1),comp2,comp3) + | GRec (loc,fk,idl,bl,tyl,bv) -> + let comp1 = Array.map (Util.list_map_left (map_glob_decl_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) -> + GRec (loc,fk,idl,comp1,comp2,comp3) + | GCast (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 + GCast (loc,comp1,comp2) + | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) as x -> x -let map_rawconstr = map_rawconstr_left_to_right +let map_glob_constr = map_glob_constr_left_to_right (* let name_app f e = function @@ -154,54 +154,54 @@ let fold_ident g idl e = (fun id (idl,e) -> let id,e = g id e in (id::idl,e)) idl ([],e) in (Array.of_list idl,e) -let map_rawconstr_with_binders_loc loc g f e = function - | RVar (_,id) -> RVar (loc,id) - | RApp (_,a,args) -> RApp (loc,f e a, List.map (f e) args) - | RLambda (_,na,ty,c) -> - let na,e = name_app g e na in RLambda (loc,na,f e ty,f e c) - | RProd (_,na,ty,c) -> - let na,e = name_app g e na in RProd (loc,na,f e ty,f e c) - | RLetIn (_,na,b,c) -> - let na,e = name_app g e na in RLetIn (loc,na,f e b,f e c) - | RCases (_,tyopt,tml,pl) -> +let map_glob_constr_with_binders_loc loc g f e = function + | GVar (_,id) -> GVar (loc,id) + | GApp (_,a,args) -> GApp (loc,f e a, List.map (f e) args) + | GLambda (_,na,ty,c) -> + let na,e = name_app g e na in GLambda (loc,na,f e ty,f e c) + | GProd (_,na,ty,c) -> + let na,e = name_app g e na in GProd (loc,na,f e ty,f e c) + | GLetIn (_,na,b,c) -> + let na,e = name_app g e na in GLetIn (loc,na,f e b,f e c) + | GCases (_,tyopt,tml,pl) -> (* We don't modify pattern variable since we don't traverse patterns *) 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 + GCases (loc,Option.map (f e) tyopt,List.map (f e) tml, List.map h pl) - | RRec (_,fk,idl,tyl,bv) -> + | GRec (_,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) - | RCast (_,c,t) -> RCast (loc,f e c,f e t) - | RSort (_,x) -> RSort (loc,x) - | RHole (_,x) -> RHole (loc,x) - | RRef (_,x) -> RRef (loc,x) - | REvar (_,x,l) -> REvar (loc,x,l) - | RPatVar (_,x) -> RPatVar (loc,x) - | RDynamic (_,x) -> RDynamic (loc,x) + GRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv) + | GCast (_,c,t) -> GCast (loc,f e c,f e t) + | GSort (_,x) -> GSort (loc,x) + | GHole (_,x) -> GHole (loc,x) + | GRef (_,x) -> GRef (loc,x) + | GEvar (_,x,l) -> GEvar (loc,x,l) + | GPatVar (_,x) -> GPatVar (loc,x) + | GDynamic (_,x) -> GDynamic (loc,x) *) -let fold_rawconstr f acc = +let fold_glob_constr f acc = let rec fold acc = function - | RVar _ -> acc - | RApp (_,c,args) -> List.fold_left fold (fold acc c) args - | RLambda (_,_,_,b,c) | RProd (_,_,_,b,c) | RLetIn (_,_,b,c) -> + | GVar _ -> acc + | GApp (_,c,args) -> List.fold_left fold (fold acc c) args + | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) -> fold (fold acc b) c - | RCases (_,_,rtntypopt,tml,pl) -> + | GCases (_,_,rtntypopt,tml,pl) -> List.fold_left fold_pattern (List.fold_left fold (Option.fold_left fold acc rtntypopt) (List.map fst tml)) pl - | RLetTuple (_,_,rtntyp,b,c) -> + | GLetTuple (_,_,rtntyp,b,c) -> fold (fold (fold_return_type acc rtntyp) b) c - | RIf (_,c,rtntyp,b1,b2) -> + | GIf (_,c,rtntyp,b1,b2) -> fold (fold (fold (fold_return_type acc rtntyp) c) b1) b2 - | RRec (_,_,_,bl,tyl,bv) -> + | GRec (_,_,_,bl,tyl,bv) -> let acc = Array.fold_left (List.fold_left (fun acc (na,k,bbd,bty) -> fold (Option.fold_left fold acc bbd) bty)) acc bl in Array.fold_left fold (Array.fold_left fold acc tyl) bv - | RCast (_,c,k) -> fold (match k with CastConv (_, t) -> fold acc t | CastCoerce -> acc) c - | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> acc + | GCast (_,c,k) -> fold (match k with CastConv (_, t) -> fold acc t | CastCoerce -> acc) c + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> acc and fold_pattern acc (_,idl,p,c) = fold acc c @@ -209,25 +209,25 @@ let fold_rawconstr f acc = in fold acc -let iter_rawconstr f = fold_rawconstr (fun () -> f) () +let iter_glob_constr f = fold_glob_constr (fun () -> f) () -let occur_rawconstr id = +let occur_glob_constr id = let rec occur = function - | RVar (loc,id') -> id = id' - | RApp (loc,f,args) -> (occur f) or (List.exists occur args) - | RLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) - | RProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) - | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c)) - | RCases (loc,sty,rtntypopt,tml,pl) -> + | GVar (loc,id') -> id = id' + | GApp (loc,f,args) -> (occur f) or (List.exists occur args) + | GLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) + | GProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) + | GLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c)) + | GCases (loc,sty,rtntypopt,tml,pl) -> (occur_option rtntypopt) or (List.exists (fun (tm,_) -> occur tm) tml) or (List.exists occur_pattern pl) - | RLetTuple (loc,nal,rtntyp,b,c) -> + | GLetTuple (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) -> + | GIf (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) -> + | GRec (loc,fk,idl,bl,tyl,bv) -> not (array_for_all4 (fun fid bl ty bd -> let rec occur_fix = function [] -> not (occur ty) && (fid=id or not(occur bd)) @@ -239,8 +239,8 @@ let occur_rawconstr id = (na=Name id or not(occur_fix bl)) in occur_fix bl) idl bl tyl bv) - | RCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false) - | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false + | GCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false) + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> false and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c) @@ -256,29 +256,29 @@ let add_name_to_ids set na = | Anonymous -> set | Name id -> Idset.add id set -let free_rawvars = +let free_glob_vars = 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) -> + | GVar (loc,id') -> if Idset.mem id' bounded then vs else Idset.add id' vs + | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args) + | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (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) -> + | GCases (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 List.fold_left (vars_pattern bounded) vs2 pl - | RLetTuple (loc,nal,rtntyp,b,c) -> + | GLetTuple (loc,nal,rtntyp,b,c) -> 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) -> + | GIf (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) -> + | GRec (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 = @@ -296,9 +296,9 @@ let free_rawvars = 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 + | GCast (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 + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> vs and vars_pattern bounded vs (loc,idl,p,c) = let bounded' = List.fold_right Idset.add idl bounded in @@ -315,51 +315,51 @@ let free_rawvars = Idset.elements vs -let loc_of_rawconstr = function - | RRef (loc,_) -> loc - | RVar (loc,_) -> loc - | REvar (loc,_,_) -> loc - | RPatVar (loc,_) -> loc - | RApp (loc,_,_) -> loc - | RLambda (loc,_,_,_,_) -> loc - | RProd (loc,_,_,_,_) -> loc - | RLetIn (loc,_,_,_) -> loc - | RCases (loc,_,_,_,_) -> loc - | RLetTuple (loc,_,_,_,_) -> loc - | RIf (loc,_,_,_,_) -> loc - | RRec (loc,_,_,_,_,_) -> loc - | RSort (loc,_) -> loc - | RHole (loc,_) -> loc - | RCast (loc,_,_) -> loc - | RDynamic (loc,_) -> loc +let loc_of_glob_constr = function + | GRef (loc,_) -> loc + | GVar (loc,_) -> loc + | GEvar (loc,_,_) -> loc + | GPatVar (loc,_) -> loc + | GApp (loc,_,_) -> loc + | GLambda (loc,_,_,_,_) -> loc + | GProd (loc,_,_,_,_) -> loc + | GLetIn (loc,_,_,_) -> loc + | GCases (loc,_,_,_,_) -> loc + | GLetTuple (loc,_,_,_,_) -> loc + | GIf (loc,_,_,_,_) -> loc + | GRec (loc,_,_,_,_,_) -> loc + | GSort (loc,_) -> loc + | GHole (loc,_) -> loc + | GCast (loc,_,_) -> loc + | GDynamic (loc,_) -> loc (**********************************************************************) -(* Conversion from rawconstr to cases pattern, if possible *) +(* Conversion from glob_constr to cases pattern, if possible *) -let rec cases_pattern_of_rawconstr na = function - | RVar (loc,id) when na<>Anonymous -> +let rec cases_pattern_of_glob_constr na = function + | GVar (loc,id) when na<>Anonymous -> (* Unable to manage the presence of both an alias and a variable *) raise Not_found - | RVar (loc,id) -> PatVar (loc,Name id) - | RHole (loc,_) -> PatVar (loc,na) - | RRef (loc,ConstructRef cstr) -> + | GVar (loc,id) -> PatVar (loc,Name id) + | GHole (loc,_) -> PatVar (loc,na) + | GRef (loc,ConstructRef cstr) -> PatCstr (loc,cstr,[],na) - | RApp (loc,RRef (_,ConstructRef cstr),l) -> - PatCstr (loc,cstr,List.map (cases_pattern_of_rawconstr Anonymous) l,na) + | GApp (loc,GRef (_,ConstructRef cstr),l) -> + PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) | _ -> raise Not_found -(* Turn a closed cases pattern into a rawconstr *) -let rec rawconstr_of_closed_cases_pattern_aux = function +(* Turn a closed cases pattern into a glob_constr *) +let rec glob_constr_of_closed_cases_pattern_aux = function | PatCstr (loc,cstr,[],Anonymous) -> - RRef (loc,ConstructRef cstr) + GRef (loc,ConstructRef cstr) | PatCstr (loc,cstr,l,Anonymous) -> - let ref = RRef (loc,ConstructRef cstr) in - RApp (loc,ref, List.map rawconstr_of_closed_cases_pattern_aux l) + let ref = GRef (loc,ConstructRef cstr) in + GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l) | _ -> raise Not_found -let rawconstr_of_closed_cases_pattern = function +let glob_constr_of_closed_cases_pattern = function | PatCstr (loc,cstr,l,na) -> - na,rawconstr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous)) + na,glob_constr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous)) | _ -> raise Not_found diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 1ab5ee7a55..95305d58c2 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -50,29 +50,29 @@ type 'a cast_type = | CastConv of cast_kind * 'a | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) -type rawconstr = - | RRef of (loc * global_reference) - | RVar of (loc * identifier) - | REvar of loc * existential_key * rawconstr list option - | RPatVar of loc * (bool * patvar) (** Used for patterns only *) - | RApp of loc * rawconstr * rawconstr list - | RLambda of loc * name * binding_kind * rawconstr * 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) * - rawconstr * rawconstr - | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr - | RRec of loc * fix_kind * identifier array * rawdecl list array * - rawconstr array * rawconstr array - | RSort of loc * rawsort - | RHole of (loc * Evd.hole_kind) - | RCast of loc * rawconstr * rawconstr cast_type - | RDynamic of loc * Dyn.t - -and rawdecl = name * binding_kind * rawconstr option * rawconstr - -and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr * rawconstr option +type glob_constr = + | GRef of (loc * global_reference) + | GVar of (loc * identifier) + | GEvar of loc * existential_key * glob_constr list option + | GPatVar of loc * (bool * patvar) (** Used for patterns only *) + | GApp of loc * glob_constr * glob_constr list + | GLambda of loc * name * binding_kind * glob_constr * glob_constr + | GProd of loc * name * binding_kind * glob_constr * glob_constr + | GLetIn of loc * name * glob_constr * glob_constr + | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses + | GLetTuple of loc * name list * (name * glob_constr option) * + glob_constr * glob_constr + | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr + | GRec of loc * fix_kind * identifier array * glob_decl list array * + glob_constr array * glob_constr array + | GSort of loc * rawsort + | GHole of (loc * Evd.hole_kind) + | GCast of loc * glob_constr * glob_constr cast_type + | GDynamic of loc * Dyn.t + +and glob_decl = name * binding_kind * glob_constr option * glob_constr + +and fix_recursion_order = RStructRec | RWfRec of glob_constr | RMeasureRec of glob_constr * glob_constr option and fix_kind = | RFix of ((int option * fix_recursion_order) array * int) @@ -81,42 +81,42 @@ and fix_kind = and predicate_pattern = name * (loc * inductive * int * name list) option -and tomatch_tuple = (rawconstr * predicate_pattern) +and tomatch_tuple = (glob_constr * predicate_pattern) and tomatch_tuples = tomatch_tuple list -and cases_clause = (loc * identifier list * cases_pattern list * rawconstr) +and cases_clause = (loc * identifier list * cases_pattern list * glob_constr) and cases_clauses = cases_clause list val cases_predicate_names : tomatch_tuples -> name list -val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr +val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr (* Ensure traversal from left to right *) -val map_rawconstr_left_to_right : - (rawconstr -> rawconstr) -> rawconstr -> rawconstr +val map_glob_constr_left_to_right : + (glob_constr -> glob_constr) -> glob_constr -> glob_constr (* -val map_rawconstr_with_binders_loc : loc -> +val map_glob_constr_with_binders_loc : loc -> (identifier -> 'a -> identifier * 'a) -> - ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr + ('a -> glob_constr -> glob_constr) -> 'a -> glob_constr -> glob_constr *) -val fold_rawconstr : ('a -> rawconstr -> 'a) -> 'a -> rawconstr -> 'a -val iter_rawconstr : (rawconstr -> unit) -> rawconstr -> unit -val occur_rawconstr : identifier -> rawconstr -> bool -val free_rawvars : rawconstr -> identifier list -val loc_of_rawconstr : rawconstr -> loc +val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a +val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit +val occur_glob_constr : identifier -> glob_constr -> bool +val free_glob_vars : glob_constr -> identifier list +val loc_of_glob_constr : glob_constr -> loc -(** Conversion from rawconstr to cases pattern, if possible +(** Conversion from glob_constr to cases pattern, if possible Take the current alias as parameter, @raise Not_found if translation is impossible *) -val cases_pattern_of_rawconstr : name -> rawconstr -> cases_pattern +val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern -val rawconstr_of_closed_cases_pattern : cases_pattern -> name * rawconstr +val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr (** {6 Reduction expressions} *) |