diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 12 | ||||
| -rw-r--r-- | pretyping/miscops.ml | 3 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 96 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 50 | ||||
| -rw-r--r-- | pretyping/retyping.mli | 5 |
5 files changed, 95 insertions, 71 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0d1e401d98..6527ba9355 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -414,15 +414,17 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let eqnl = detype_eqns constructs constagsl bl in GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) +let detype_universe sigma u = + let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in + Univ.Universe.map fn u + let detype_sort sigma = function | Prop Null -> GProp | Prop Pos -> GSet | Type u -> GType (if !print_universes - then - let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in - [Loc.tag @@ Name.mk_name (Id.of_string_soft u)] + then detype_universe sigma u else []) type binder_kind = BProd | BLambda | BLetIn @@ -434,8 +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 = - let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in - GType (Some (Loc.tag @@ Name.mk_name (Id.of_string_soft l))) + let l = Termops.reference_of_level sigma l in + GType (UNamed l) let detype_instance sigma l = let l = EInstance.kind sigma l in diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index bc563b46dc..f0cb8fd1f2 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -30,7 +30,8 @@ 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 -> Names.Name.equal (snd x) (snd y)) l1 l2 +| GType l1, GType l2 -> + List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) 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 00c254dbe2..b930c5db83 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -177,61 +177,77 @@ let _ = optwrite = (:=) Universes.set_minimization }) (** Miscellaneous interpretation functions *) -let interp_known_universe_level evd id = + +let interp_known_universe_level evd r = + let loc, qid = Libnames.qualid_of_reference r in try - let level = Evd.universe_of_name evd id in - level + match r with + | Libnames.Ident (loc, id) -> Evd.universe_of_name evd id + | Libnames.Qualid _ -> raise Not_found with Not_found -> - let names, _ = Global.global_universe_names () in - snd (Id.Map.find id names) - -let interp_universe_level_name ~anon_rigidity evd (loc, s) = - match s with - | Anonymous -> - new_univ_level_variable ?loc anon_rigidity evd - | Name id -> - let s = Id.to_string id in - if CString.string_contains ~where:s ~what:"." then - match List.rev (CString.split '.' s) with - | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".") - | 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 evd, interp_known_universe_level evd id - with Not_found -> - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ?loc ~name:id univ_rigid evd - else user_err ?loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ str s)) + let univ, k = Nametab.locate_universe qid in + Univ.Level.make univ k + +let interp_universe_level_name ~anon_rigidity evd r = + try evd, interp_known_universe_level evd r + with Not_found -> + match r with (* Qualified generated name *) + | Libnames.Qualid (loc, qid) -> + let dp, i = Libnames.repr_qualid qid in + let num = + try int_of_string (Id.to_string i) + with Failure _ -> + user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r)) + 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 + | Libnames.Ident (loc, id) -> (* Undeclared *) + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc ~name:id univ_rigid evd + else user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ Id.print id)) 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 -> - (* [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))) + List.fold_left (fun (evd, u) l -> + let evd', u' = + match l with + | Some (l,n) -> + (* [univ_flexible_alg] can produce algebraic universes in terms *) + let anon_rigidity = univ_flexible in + let evd', l = interp_universe_level_name ~anon_rigidity evd l in + let u' = Univ.Universe.make l in + (match n with + | 0 -> evd', u' + | 1 -> evd', Univ.Universe.super u' + | _ -> + user_err ?loc ~hdr:"interp_universe" + (Pp.(str "Cannot interpret universe increment +" ++ int n))) + | None -> + let evd, l = new_univ_level_variable ?loc univ_flexible evd in + evd, Univ.Universe.make l + in (evd', Univ.sup u u')) (evd, Univ.Universe.type0m) l let interp_known_level_info ?loc evd = function - | None | Some (_, Anonymous) -> + | UUnknown | UAnonymous -> user_err ?loc ~hdr:"interp_known_level_info" (str "Anonymous universes not allowed here.") - | Some (loc, Name id) -> - try interp_known_universe_level evd id + | UNamed ref -> + try interp_known_universe_level evd ref with Not_found -> - user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Id.print id) + user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref) 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 ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s) + | UUnknown -> new_univ_level_variable ?loc univ_rigid evd + | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd + | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 5dd6879d39..f8f086fad3 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -166,23 +166,6 @@ let retype ?(polyprop=true) sigma = | Lambda _ | Fix _ | Construct _ -> retype_error NotAType | _ -> decomp_sort env sigma (type_of env t) - and sort_family_of env t = - match EConstr.kind sigma t with - | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s) - | Sort _ -> InType - | Prod (name,t,c2) -> - let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in - if not (is_impredicative_set env) && - s2 == InSet && sort_family_of env t == InType then InType else s2 - | App(f,args) when is_template_polymorphic env sigma f -> - let t = type_of_global_reference_knowing_parameters env f args in - Sorts.family (sort_of_atomic_type env sigma t args) - | App(f,args) -> - Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) - | Lambda _ | Fix _ | Construct _ -> retype_error NotAType - | _ -> - Sorts.family (decomp_sort env sigma (type_of env t)) - and type_of_global_reference_knowing_parameters env c args = let argtyps = Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in @@ -198,15 +181,34 @@ let retype ?(polyprop=true) sigma = EConstr.of_constr (type_of_constructor env (cstr, u)) | _ -> assert false - in type_of, sort_of, sort_family_of, - type_of_global_reference_knowing_parameters + in type_of, sort_of, type_of_global_reference_knowing_parameters + +let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t = + let type_of,_,type_of_global_reference_knowing_parameters = retype ~polyprop sigma in + let rec sort_family_of env t = + match EConstr.kind sigma t with + | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s) + | Sort _ -> InType + | Prod (name,t,c2) -> + let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in + if not (is_impredicative_set env) && + s2 == InSet && sort_family_of env t == InType then InType else s2 + | App(f,args) when is_template_polymorphic env sigma f -> + if truncation_style then InType else + let t = type_of_global_reference_knowing_parameters env f args in + Sorts.family (sort_of_atomic_type env sigma t args) + | App(f,args) -> + Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) + | Lambda _ | Fix _ | Construct _ -> retype_error NotAType + | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType + | _ -> + Sorts.family (decomp_sort env sigma (type_of env t)) + in sort_family_of env t let get_sort_of ?(polyprop=true) env sigma t = - let _,f,_,_ = retype ~polyprop sigma in anomaly_on_error (f env) t -let get_sort_family_of ?(polyprop=true) env sigma c = - let _,_,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) c + let _,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) t let type_of_global_reference_knowing_parameters env sigma c args = - let _,_,_,f = retype sigma in anomaly_on_error (f env c) args + let _,_,f = retype sigma in anomaly_on_error (f env c) args let type_of_global_reference_knowing_conclusion env sigma c conclty = match EConstr.kind sigma c with @@ -232,7 +234,7 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = (* get_type_of polyprop lax env sigma c *) let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = - let f,_,_,_ = retype ~polyprop sigma in + let f,_,_ = retype ~polyprop sigma in if lax then f env c else anomaly_on_error (f env) c (* Makes an unsafe judgment from a constr *) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index af86df499c..6fdde90463 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -31,8 +31,11 @@ val get_type_of : val get_sort_of : ?polyprop:bool -> env -> evar_map -> types -> Sorts.t +(* When [truncation_style] is [true], tells if the type has been explicitly + truncated to Prop or (impredicative) Set; in particular, singleton type and + small inductive types, which have all eliminations to Type, are in Type *) val get_sort_family_of : - ?polyprop:bool -> env -> evar_map -> types -> Sorts.family + ?truncation_style:bool -> ?polyprop:bool -> env -> evar_map -> types -> Sorts.family (** Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment |