diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 9 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 215 | ||||
| -rw-r--r-- | pretyping/glob_ops.mli | 1 | ||||
| -rw-r--r-- | pretyping/miscops.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 62 |
5 files changed, 100 insertions, 189 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 483e2b4320..0d798b4d94 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -422,7 +422,9 @@ let detype_sort sigma = function | Type u -> GType (if !print_universes - then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)] + then + let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in + [dl, Name.mk_name (Id.of_string_soft u)] else []) type binder_kind = BProd | BLambda | BLetIn @@ -434,7 +436,8 @@ let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = - GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l))) + let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in + GType (Some (dl, Name.mk_name (Id.of_string_soft l))) let detype_instance sigma l = let l = EInstance.kind sigma l in @@ -695,7 +698,7 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = let c = detype (lax,false) avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in - let t = if s != InProp then None else Some (detype (lax,false) avoid env sigma ty) in + let t = if s != InProp && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in GLetIn (dl, na', c, t, r) let detype_rel_context ?(lax=false) where avoid env sigma sign = diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index ebbfa195f0..6509aaac3d 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -214,120 +214,62 @@ let fold_glob_constr f acc = function f acc c | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc -let iter_glob_constr f = fold_glob_constr (fun () -> f) () +let fold_return_type_with_binders f g v acc (na,tyopt) = + Option.fold_left (f (name_fold g na v)) acc tyopt -let same_id na id = match na with -| Anonymous -> false -| Name id' -> Id.equal id id' +let fold_glob_constr_with_binders g f v acc = function + | GVar _ -> acc + | GApp (_,c,args) -> List.fold_left (f v) (f v acc c) args + | GLambda (_,na,_,b,c) | GProd (_,na,_,b,c) -> + f (name_fold g na v) (f v acc b) c + | GLetIn (_,na,b,t,c) -> + f (name_fold g na v) (Option.fold_left (f v) (f v acc b) t) c + | GCases (_,_,rtntypopt,tml,pl) -> + let fold_pattern acc (_,idl,p,c) = f (List.fold_right g idl v) acc c in + let fold_tomatch (v',acc) (tm,(na,onal)) = + (Option.fold_left (fun v'' (_,_,nal) -> List.fold_right (name_fold g) nal v'') + (name_fold g na v') onal, + f v acc tm) in + let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in + let acc = Option.fold_left (f v') acc rtntypopt in + List.fold_left fold_pattern acc pl + | GLetTuple (_,nal,rtntyp,b,c) -> + f v (f v (fold_return_type_with_binders f g v acc rtntyp) b) c + | GIf (_,c,rtntyp,b1,b2) -> + f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2 + | GRec (_,_,idl,bll,tyl,bv) -> + let f' i acc fid = + let v,acc = + List.fold_left + (fun (v,acc) (na,k,bbd,bty) -> + (name_fold g na v, f v (Option.fold_left (f v) acc bbd) bty)) + (v,acc) + bll.(i) in + f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in + Array.fold_left_i f' acc idl + | GCast (_,c,k) -> + let acc = match k with + | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in + f v acc c + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc + +let iter_glob_constr f = fold_glob_constr (fun () -> f) () let occur_glob_constr id = - let rec occur = function + let rec occur barred acc = function | GVar (loc,id') -> Id.equal id id' - | GApp (loc,f,args) -> (occur f) || (List.exists occur args) - | GLambda (loc,na,bk,ty,c) -> - (occur ty) || (not (same_id na id) && (occur c)) - | GProd (loc,na,bk,ty,c) -> - (occur ty) || (not (same_id na id) && (occur c)) - | GLetIn (loc,na,b,t,c) -> - (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c)) - | GCases (loc,sty,rtntypopt,tml,pl) -> - (occur_option rtntypopt) - || (List.exists (fun (tm,_) -> occur tm) tml) - || (List.exists occur_pattern pl) - | GLetTuple (loc,nal,rtntyp,b,c) -> - occur_return_type rtntyp id - || (occur b) || (not (List.mem_f Name.equal (Name id) nal) && (occur c)) - | GIf (loc,c,rtntyp,b1,b2) -> - occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2) - | GRec (loc,fk,idl,bl,tyl,bv) -> - not (Array.for_all4 (fun fid bl ty bd -> - let rec occur_fix = function - [] -> not (occur ty) && (Id.equal fid id || not(occur bd)) - | (na,k,bbd,bty)::bl -> - not (occur bty) && - (match bbd with - Some bd -> not (occur bd) - | _ -> true) && - (match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in - occur_fix bl) - idl bl tyl bv) - | GCast (loc,c,k) -> (occur c) || (match k with CastConv t - | CastVM t | CastNative t -> occur t | CastCoerce -> false) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false - - and occur_pattern (loc,idl,p,c) = not (Id.List.mem id idl) && (occur c) - - and occur_option = function None -> false | Some p -> occur p - - and occur_return_type (na,tyopt) id = not (same_id na id) && occur_option tyopt - - in occur - - -let add_name_to_ids set na = - match na with - | Anonymous -> set - | Name id -> Id.Set.add id set + | c -> + (* [g] looks if [id] appears in a binding position, in which + case, we don't have to look in the corresponding subterm *) + let g id' barred = barred || Id.equal id id' in + let f barred acc c = acc || not barred && occur false acc c in + fold_glob_constr_with_binders g f barred acc c in + occur false false let free_glob_vars = - let rec vars bounded vs = function - | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.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) -> - let vs' = vars bounded vs ty in - let bounded' = add_name_to_ids bounded na in - vars bounded' vs' c - | GLetIn (loc,na,b,ty,c) -> - let vs' = vars bounded vs b in - let vs'' = Option.fold_left (vars bounded) vs' ty in - let bounded' = add_name_to_ids bounded na in - vars bounded' vs'' c - | 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 - | 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 - | 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 - | GRec (loc,fk,idl,bl,tyl,bv) -> - let bounded' = Array.fold_right Id.Set.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 - (vs'',bounded') - ) - (vs,bounded') - bl.(i) - in - let vs2 = vars bounded1 vs1 tyl.(i) in - vars bounded1 vs2 bv.(i) - in - Array.fold_left_i vars_fix vs idl - | GCast (loc,c,k) -> let v = vars bounded vs c in - (match k with CastConv t | CastVM t | CastNative t -> vars bounded v t | _ -> v) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs - - and vars_pattern bounded vs (loc,idl,p,c) = - let bounded' = List.fold_right Id.Set.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 - vars_option bounded' vs tyopt - in + let rec vars bound vs = function + | GVar (loc,id') -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs + | c -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in fun rt -> let vs = vars Id.Set.empty Id.Set.empty rt in Id.Set.elements vs @@ -353,57 +295,16 @@ let add_and_check_ident id set = Id.Set.add id set let bound_glob_vars = - let rec vars bound = function - | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c -> - let bound = name_fold add_and_check_ident na bound in - fold_glob_constr vars bound c - | GCases (loc,sty,rtntypopt,tml,pl) -> - let bound = vars_option bound rtntypopt in - let bound = - List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in - List.fold_left vars_pattern bound pl - | GLetTuple (loc,nal,rtntyp,b,c) -> - let bound = vars_return_type bound rtntyp in - let bound = vars bound b in - let bound = List.fold_right (name_fold add_and_check_ident) nal bound in - vars bound c - | GIf (loc,c,rtntyp,b1,b2) -> - let bound = vars_return_type bound rtntyp in - let bound = vars bound c in - let bound = vars bound b1 in - vars bound b2 - | GRec (loc,fk,idl,bl,tyl,bv) -> - let bound = Array.fold_right Id.Set.add idl bound in - let vars_fix i bound fid = - let bound = - List.fold_left - (fun bound (na,k,bbd,bty) -> - let bound = vars_option bound bbd in - let bound = vars bound bty in - name_fold add_and_check_ident na bound - ) - bound - bl.(i) - in - let bound = vars bound tyl.(i) in - vars bound bv.(i) - in - Array.fold_left_i vars_fix bound idl - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound - | GApp _ | GCast _ as c -> fold_glob_constr vars bound c - - and vars_pattern bound (loc,idl,p,c) = - let bound = List.fold_right add_and_check_ident idl bound in - vars bound c - - and vars_option bound = function None -> bound | Some p -> vars bound p - - and vars_return_type bound (na,tyopt) = - let bound = name_fold add_and_check_ident na bound in - vars_option bound tyopt + let rec vars bound = + fold_glob_constr_with_binders + (fun id () -> bound := add_and_check_ident id !bound) + (fun () () -> vars bound) + () () in fun rt -> - vars Id.Set.empty rt + let bound = ref Id.Set.empty in + vars bound rt; + !bound (** Mapping of names in binders *) diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 55e6b6533f..af2834e498 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -37,6 +37,7 @@ val map_glob_constr_left_to_right : val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a +val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit val occur_glob_constr : Id.t -> glob_constr -> bool val free_glob_vars : glob_constr -> Id.t list diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 7fe81c9a43..1669f8334b 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -30,7 +30,7 @@ let smartmap_cast_type f c = let glob_sort_eq g1 g2 = match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true -| GType l1, GType l2 -> List.equal (fun x y -> CString.equal (snd x) (snd y)) l1 l2 +| GType l1, GType l2 -> List.equal (fun x y -> Names.Name.equal (snd x) (snd y)) l1 l2 | _ -> false let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 68ef976592..4886423bd0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -192,45 +192,51 @@ let _ = optwrite = (:=) Universes.set_minimization }) (** Miscellaneous interpretation functions *) -let interp_universe_level_name evd (loc,s) = - let names, _ = Global.global_universe_names () in - if CString.string_contains ~where:s ~what:"." then - match List.rev (CString.split '.' s) with - | [] -> anomaly (str"Invalid universe name " ++ str s) - | n :: dp -> - let num = int_of_string n in - let dp = DirPath.make (List.map Id.of_string dp) in - let level = Univ.Level.make dp num in - let evd = - try Evd.add_global_univ evd level - with UGraph.AlreadyDeclared -> evd - in evd, level - else - try - let level = Evd.universe_of_name evd s in - evd, level - with Not_found -> - try - let id = try Id.of_string s with _ -> raise Not_found in - evd, snd (Idmap.find id names) - with Not_found -> - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ~loc ~name:s univ_rigid evd - else user_err ~loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ str s)) +let interp_universe_level_name ~anon_rigidity evd (loc,s) = + match s with + | Anonymous -> + new_univ_level_variable ~loc anon_rigidity evd + | Name s -> + let s = Id.to_string s in + let names, _ = Global.global_universe_names () in + if CString.string_contains ~where:s ~what:"." then + match List.rev (CString.split '.' s) with + | [] -> anomaly (str"Invalid universe name " ++ str s) + | n :: dp -> + let num = int_of_string n in + let dp = DirPath.make (List.map Id.of_string dp) in + let level = Univ.Level.make dp num in + let evd = + try Evd.add_global_univ evd level + with UGraph.AlreadyDeclared -> evd + in evd, level + else + try + let level = Evd.universe_of_name evd s in + evd, level + with Not_found -> + try + let id = try Id.of_string s with _ -> raise Not_found in + evd, snd (Idmap.find id names) + with Not_found -> + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ~loc ~name:s univ_rigid evd + else user_err ~loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ str s)) let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in evd, Univ.Universe.make l | l -> List.fold_left (fun (evd, u) l -> - let evd', l = interp_universe_level_name evd l in + (* [univ_flexible_alg] can produce algebraic universes in terms *) + let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible evd l in (evd', Univ.sup u (Univ.Universe.make l))) (evd, Univ.Universe.type0m) l let interp_level_info loc evd : Misctypes.level_info -> _ = function | None -> new_univ_level_variable ~loc univ_rigid evd - | Some (loc,s) -> interp_universe_level_name evd (loc,s) + | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (loc,s) let interp_sort ?loc evd = function | GProp -> evd, Prop Null |