From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:11:47 +0200 Subject: Remove unused [open] statements --- pretyping/detyping.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'pretyping/detyping.ml') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 8ba408679..483e2b432 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -13,7 +13,6 @@ open CErrors open Util open Names open Term -open Environ open EConstr open Vars open Inductiveops -- cgit v1.2.3 From dba083b267a2aede3654dcebaab0013d284d32c7 Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (@brixpro-home)" Date: Sun, 22 Jan 2017 11:59:22 -0500 Subject: applied the patch for printing types of let bindings by @herbelin --- pretyping/detyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/detyping.ml') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 483e2b432..1eec85f45 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -695,7 +695,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 = -- cgit v1.2.3 From e9b745af47ba3386724b874e3fd74b6dad33b015 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Thu, 6 Apr 2017 22:48:32 +0200 Subject: Allow flexible anonymous universes in instances and sorts. The addition to the test suite showcases the usage. --- intf/misctypes.mli | 4 +-- library/declare.ml | 5 ++-- parsing/g_constr.ml4 | 8 ++--- pretyping/detyping.ml | 7 +++-- pretyping/miscops.ml | 2 +- pretyping/pretyping.ml | 61 +++++++++++++++++++++------------------ printing/ppconstr.ml | 8 ++--- test-suite/success/polymorphism.v | 32 +++++++++++++++++++- 8 files changed, 82 insertions(+), 45 deletions(-) (limited to 'pretyping/detyping.ml') diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 33dc2a335..7c2dc5177 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -48,8 +48,8 @@ type 'a glob_sort_gen = | GProp (** representation of [Prop] literal *) | GSet (** representation of [Set] literal *) | GType of 'a (** representation of [Type] literal *) -type sort_info = string Loc.located list -type level_info = string Loc.located option +type sort_info = Name.t Loc.located list +type level_info = Name.t Loc.located option type glob_sort = sort_info glob_sort_gen type glob_level = level_info glob_sort_gen diff --git a/library/declare.ml b/library/declare.ml index 31c9c24bc..91e0cb44b 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -514,11 +514,10 @@ let do_constraint poly l = match x with | GProp -> Loc.dummy_loc, (false, Univ.Level.prop) | GSet -> Loc.dummy_loc, (false, Univ.Level.set) - | GType None -> + | GType None | GType (Some (_, Anonymous)) -> user_err ~hdr:"Constraint" (str "Cannot declare constraints on anonymous universes") - | GType (Some (loc, id)) -> - let id = Id.of_string id in + | GType (Some (loc, Name id)) -> let names, _ = Global.global_universe_names () in try loc, Idmap.find id names with Not_found -> diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 0f2ed88fe..15f100c3b 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -146,12 +146,12 @@ GEXTEND Gram [ [ "Set" -> GSet | "Prop" -> GProp | "Type" -> GType [] - | "Type"; "@{"; u = universe; "}" -> GType (List.map (fun (loc,x) -> (loc, Id.to_string x)) u) + | "Type"; "@{"; u = universe; "}" -> GType u ] ] ; universe: - [ [ IDENT "max"; "("; ids = LIST1 identref SEP ","; ")" -> ids - | id = identref -> [id] + [ [ IDENT "max"; "("; ids = LIST1 name SEP ","; ")" -> ids + | id = name -> [id] ] ] ; lconstr: @@ -298,7 +298,7 @@ GEXTEND Gram [ [ "Set" -> GSet | "Prop" -> GProp | "Type" -> GType None - | id = identref -> GType (Some (fst id, Id.to_string (snd id))) + | id = name -> GType (Some id) ] ] ; fix_constr: diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 483e2b432..8a90a3f9b 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 diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 7fe81c9a4..1669f8334 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 68ef97659..767e4be35 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -192,45 +192,50 @@ 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 + let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible_alg 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 diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 3041ac259..b546c39ae 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -151,8 +151,8 @@ let tag_var = tag Tag.variable let pr_univ l = match l with - | [_,x] -> str x - | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")" + | [_,x] -> pr_name x + | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> pr_name (snd x)) l ++ str")" let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" @@ -166,7 +166,7 @@ let tag_var = tag Tag.variable | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") | GType None -> tag_type (str "Type") - | GType (Some (_, u)) -> tag_type (str u) + | GType (Some (_, u)) -> tag_type (pr_name u) let pr_qualid sp = let (sl, id) = repr_qualid sp in @@ -191,7 +191,7 @@ let tag_var = tag Tag.variable tag_type (str "Set") | GType u -> (match u with - | Some (_,u) -> str u + | Some (_,u) -> pr_name u | None -> tag_type (str "Type")) let pr_universe_instance l = diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 878875bd9..0a58fe89a 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -321,4 +321,34 @@ Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw. Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ Type)) eq_refl. -End Hurkens'. \ No newline at end of file +End Hurkens'. + +Module Anonymous. + Set Universe Polymorphism. + + Definition defaultid := (fun x => x) : Type -> Type. + Definition collapseid := defaultid@{_ _}. + Check collapseid@{_}. + + Definition anonid := (fun x => x) : Type -> Type@{_}. + Check anonid@{_}. + + Definition defaultalg := Type : Type. + Definition usedefaultalg := defaultalg@{_ _}. + Check usedefaultalg@{_ _}. + + Definition anonalg := (fun x => x) (Type : Type@{_}). + Check anonalg@{_}. + + Definition unrelated@{i j} := nat. + Definition useunrelated := unrelated@{_ _}. + Check useunrelated@{_ _}. + + Definition inthemiddle@{i j k} := + let _ := defaultid@{i j} in + defaultalg@{k j}. + (* i <= j < k *) + Definition collapsethemiddle := inthemiddle@{i _ j}. + Check collapsethemiddle@{_ _}. + +End Anonymous. -- cgit v1.2.3