From 45352e43db4c67eab23517f13e94ba1b5cc11808 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 13 Nov 2018 15:42:02 +0100 Subject: Towards unifying parsing/printing for universe instances and Type's argument. We consistently use: - UUnknown: to mean a rigid anonymous universe (written Type in instances and Type as a sort) [was formerly encoded as [] in Type's argument] - UAnonymous: to mean a flexible anonymous universe (written _ in instances and Type@{_} as a sort) [was formerly encoded as [None] in Type's argument] - UNamed: to mean a named universe or universe expression (written id or qualid in instances and Type@{id} or Type@{qualid} or more generally Type@{id+n}, Type@{qualid+n}, Type@{max(...)} as a sort) There is a little change of syntax: "_" in a "max" list of universes (e.g. "Type@{max(_,id+1)}" is not anymore allowed. But it was trivially satisfiable by unifying the flexible universe with a neighbor of the list and the syntax is anyway not documented. There is a little change of semantics: if I do id@{Type} for an abbreviation "id := Type", it will consider a rigid variable rather than a flexible variable as before. --- interp/constrextern.ml | 10 ++++------ interp/constrintern.ml | 12 ++++++------ 2 files changed, 10 insertions(+), 12 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index fe50bd4b08..c05af8be45 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -757,11 +757,9 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo (* mapping glob_constr to constr_expr *) let extern_glob_sort = function - | GSProp -> GSProp - | GProp -> GProp - | GSet -> GSet - | GType _ as s when !print_universes -> s - | GType _ -> GType [] + (* In case we print a glob_constr w/o having passed through detyping *) + | GType _ when not !print_universes -> GType UUnknown + | u -> u let extern_universes = function | Some _ as l when !print_universes -> l @@ -1315,7 +1313,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | PSort Sorts.InSProp -> GSort GSProp | PSort Sorts.InProp -> GSort GProp | PSort Sorts.InSet -> GSort GSet - | PSort Sorts.InType -> GSort (GType []) + | PSort Sorts.InType -> GSort (GType UUnknown) | PInt i -> GInt i let extern_constr_pattern env sigma pat = diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1dd68f2abf..b4294b4ff8 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -998,18 +998,18 @@ let intern_reference qid = in Smartlocate.global_of_extended_global r -let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option = +let sort_info_of_level_info (info: level_info) : sort_info = match info with - | UAnonymous -> None - | UUnknown -> None - | UNamed id -> Some (id, 0) + | UAnonymous -> UAnonymous + | UUnknown -> UUnknown + | UNamed id -> UNamed [id,0] let glob_sort_of_level (level: glob_level) : glob_sort = match level with | GSProp -> GSProp | GProp -> GProp | GSet -> GSet - | GType info -> GType [sort_info_of_level_info info] + | GType info -> GType (sort_info_of_level_info info) (* Is it a global reference or a syntactic definition? *) let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = @@ -1045,7 +1045,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) | _ -> err () end - | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) + | Some [s], GSort (GType UUnknown) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) | Some [_old_level], GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *) user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid) -- cgit v1.2.3 From 460bf801123d13e8c82503a2fc491892f8eed6d5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 14 Nov 2018 10:10:39 +0100 Subject: Allowing Set to be part of universe expressions. Conversely, Type existential variables now (explicitly) cover the Set case. Similarly for Prop and SProp. --- interp/constrextern.ml | 13 +++++++------ interp/constrintern.ml | 14 +++----------- interp/declare.mli | 3 +-- interp/notation_ops.ml | 6 +++++- 4 files changed, 16 insertions(+), 20 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index c05af8be45..701c07dc8d 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -758,8 +758,9 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo let extern_glob_sort = function (* In case we print a glob_constr w/o having passed through detyping *) - | GType _ when not !print_universes -> GType UUnknown - | u -> u + | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u + | UNamed _ when not !print_universes -> UAnonymous {rigid=true} + | UNamed _ | UAnonymous _ as u -> u let extern_universes = function | Some _ as l when !print_universes -> l @@ -1310,10 +1311,10 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) - | PSort Sorts.InSProp -> GSort GSProp - | PSort Sorts.InProp -> GSort GProp - | PSort Sorts.InSet -> GSort GSet - | PSort Sorts.InType -> GSort (GType UUnknown) + | PSort Sorts.InSProp -> GSort (UNamed [GSProp,0]) + | PSort Sorts.InProp -> GSort (UNamed [GProp,0]) + | PSort Sorts.InSet -> GSort (UNamed [GSet,0]) + | PSort Sorts.InType -> GSort (UAnonymous {rigid=true}) | PInt i -> GInt i let extern_constr_pattern env sigma pat = diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b4294b4ff8..1a81dc41a1 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -998,18 +998,10 @@ let intern_reference qid = in Smartlocate.global_of_extended_global r -let sort_info_of_level_info (info: level_info) : sort_info = - match info with - | UAnonymous -> UAnonymous - | UUnknown -> UUnknown - | UNamed id -> UNamed [id,0] - let glob_sort_of_level (level: glob_level) : glob_sort = match level with - | GSProp -> GSProp - | GProp -> GProp - | GSet -> GSet - | GType info -> GType (sort_info_of_level_info info) + | UAnonymous {rigid} -> UAnonymous {rigid} + | UNamed id -> UNamed [id,0] (* Is it a global reference or a syntactic definition? *) let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = @@ -1045,7 +1037,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) | _ -> err () end - | Some [s], GSort (GType UUnknown) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) + | Some [s], GSort (UAnonymous {rigid=true}) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) | Some [_old_level], GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *) user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid) diff --git a/interp/declare.mli b/interp/declare.mli index 795d9a767d..0b1a396a34 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -90,5 +90,4 @@ val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit val do_universe : polymorphic -> lident list -> unit -val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list -> - unit +val do_constraint : polymorphic -> Glob_term.glob_constraint list -> unit diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7f084fffdd..08619d912e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1190,7 +1190,11 @@ let rec match_ inner u alp metas sigma a1 a2 = Array.fold_left2 (match_in u alp metas) sigma bl1 bl2 | GCast(t1, c1), NCast(t2, c2) -> match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2 - | GSort (GType _), NSort (GType _) when not u -> sigma + + (* Next pair of lines useful only if not coming from detyping *) + | GSort (UNamed [(GProp|GSet),0]), NSort (UAnonymous _) -> raise No_match + | GSort _, NSort (UAnonymous _) when not u -> sigma + | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma | GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match -- cgit v1.2.3