diff options
| author | Gaëtan Gilbert | 2020-11-18 16:45:58 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-25 13:09:35 +0100 |
| commit | 81063864db93c3d736171147f0973249da85fd27 (patch) | |
| tree | e17375947229fce238158066e81b46d9efef790d | |
| parent | 2b80095f5dbfb996643309bfae6f45f62e2ecdb1 (diff) | |
Separate interning and pretyping of universes
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
64 files changed, 459 insertions, 317 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index a9438c4aca..4faa12af79 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -27,6 +27,11 @@ let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false +let with_env_evm f x = + let env = Global.env() in + let sigma = Evd.from_env env in + f env sigma x + (* std_ppcmds *) let pp x = Pp.pp_with !Topfmt.std_ft x @@ -75,7 +80,7 @@ let ppeconstr x = pp (pr_econstr x) let ppconstr_expr x = let sigma,env = get_current_context () in pp (Ppconstr.pr_constr_expr env sigma x) let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x -let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x)) +let ppglob_constr = (fun x -> pp(with_env_evm pr_lglob_constr_env x)) let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x)) let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e))) let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) @@ -130,7 +135,7 @@ let rec pr_closure {idents=idents;typed=typed;untyped=untyped} = and pr_closed_glob_constr_idmap x = pridmap (fun _ -> pr_closed_glob_constr) x and pr_closed_glob_constr {closure=closure;term=term} = - pr_closure closure ++ (pr_lglob_constr_env Global.(env ())) term + pr_closure closure ++ with_env_evm pr_lglob_constr_env term let ppclosure x = pp (pr_closure x) let ppclosedglobconstr x = pp (pr_closed_glob_constr x) @@ -212,7 +217,7 @@ let pproof p = pp(Proof.pr_proof p) let ppuni u = pp(Universe.pr u) let ppuni_level u = pp (Level.pr u) -let prlev = UnivNames.pr_with_global_universes +let prlev = UnivNames.pr_with_global_universes Id.Map.empty let ppuniverse_set l = pp (LSet.pr prlev l) let ppuniverse_instance l = pp (Instance.pr prlev l) let ppuniverse_context l = pp (pr_universe_context prlev l) diff --git a/engine/uState.ml b/engine/uState.ml index 103b552d86..0c994dfea0 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -341,12 +341,16 @@ let constrain_variables diff uctx = in { uctx with local = (univs, local); univ_variables = vars } -let qualid_of_level uctx = +let id_of_level uctx l = + try Some (Option.get (LMap.find l (snd uctx.names)).uname) + with Not_found | Option.IsNone -> + None + +let qualid_of_level uctx l = let map, map_rev = uctx.names in - fun l -> - try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname)) - with Not_found | Option.IsNone -> - UnivNames.qualid_of_level l + try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname)) + with Not_found | Option.IsNone -> + UnivNames.qualid_of_level map l let pr_uctx_level uctx l = match qualid_of_level uctx l with diff --git a/engine/uState.mli b/engine/uState.mli index bd3aac0d8b..442c29180c 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -209,4 +209,7 @@ val update_sigma_univs : t -> UGraph.t -> t val pr_uctx_level : t -> Univ.Level.t -> Pp.t val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option +(** Only looks in the local names, not in the nametab. *) +val id_of_level : t -> Univ.Level.t -> Id.t option + val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t diff --git a/engine/univNames.ml b/engine/univNames.ml index 2e15558db2..f5542cc0f7 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -12,15 +12,15 @@ open Names open Univ -let qualid_of_level l = +let qualid_of_level ctx l = match Level.name l with | Some qid -> - (try Some (Nametab.shortest_qualid_of_universe qid) + (try Some (Nametab.shortest_qualid_of_universe (Id.Map.domain ctx) qid) with Not_found -> None) | None -> None -let pr_with_global_universes l = - match qualid_of_level l with +let pr_with_global_universes ctx l = + match qualid_of_level ctx l with | Some qid -> Libnames.pr_qualid qid | None -> Level.pr l diff --git a/engine/univNames.mli b/engine/univNames.mli index 5f69d199b3..875c043032 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -10,9 +10,6 @@ open Univ -val pr_with_global_universes : Level.t -> Pp.t -val qualid_of_level : Level.t -> Libnames.qualid option - (** Local universe name <-> level mapping *) type universe_binders = Univ.Level.t Names.Id.Map.t @@ -20,3 +17,6 @@ type universe_binders = Univ.Level.t Names.Id.Map.t val empty_binders : universe_binders type univ_name_list = Names.lname list + +val pr_with_global_universes : universe_binders -> Level.t -> Pp.t +val qualid_of_level : universe_binders -> Level.t -> Libnames.qualid option diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index b3f06faa1c..b14c325f69 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -13,10 +13,23 @@ open Libnames (** {6 Concrete syntax for terms } *) -(** [constr_expr] is the abstract syntax tree produced by the parser *) -type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl +(** Universes *) +type sort_name_expr = + | CSProp | CProp | CSet + | CType of qualid + | CRawType of Univ.Level.t (** Universes like "foo.1" have no qualid form *) + +type univ_level_expr = sort_name_expr Glob_term.glob_sort_gen +type sort_expr = (sort_name_expr * int) list Glob_term.glob_sort_gen + +type instance_expr = univ_level_expr list + +(** Constraints don't have anonymous universes *) +type univ_constraint_expr = sort_name_expr * Univ.constraint_type * sort_name_expr + +type universe_decl_expr = (lident list, univ_constraint_expr list) UState.gen_universe_decl type cumul_univ_decl_expr = - ((lident * Univ.Variance.t option) list, Glob_term.glob_constraint list) UState.gen_universe_decl + ((lident * Univ.Variance.t option) list, univ_constraint_expr list) UState.gen_universe_decl type ident_decl = lident * universe_decl_expr option type cumul_ident_decl = lident * cumul_univ_decl_expr option @@ -64,8 +77,7 @@ type prim_token = | Number of NumTok.Signed.t | String of string -type instance_expr = Glob_term.glob_level list - +(** [constr_expr] is the abstract syntax tree produced by the parser *) type cases_pattern_expr_r = | CPatAlias of cases_pattern_expr * lname | CPatCstr of qualid @@ -114,7 +126,7 @@ and constr_expr_r = | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of Pattern.patvar | CEvar of Glob_term.existential_name CAst.t * (lident * constr_expr) list - | CSort of Glob_term.glob_sort + | CSort of sort_expr | CCast of constr_expr * constr_expr Glob_term.cast_type | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index a60dc11b57..f02874253e 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -18,6 +18,25 @@ open Glob_term open Notation open Constrexpr +(***********) +(* Universes *) + +let sort_name_expr_eq c1 c2 = match c1, c2 with + | CSProp, CSProp + | CProp, CProp + | CSet, CSet -> true + | CType q1, CType q2 -> Libnames.qualid_eq q1 q2 + | CRawType u1, CRawType u2 -> Univ.Level.equal u1 u2 + | (CSProp|CProp|CSet|CType _|CRawType _), _ -> false + +let univ_level_expr_eq u1 u2 = + Glob_ops.glob_sort_gen_eq sort_name_expr_eq u1 u2 + +let sort_expr_eq u1 u2 = + Glob_ops.glob_sort_gen_eq + (List.equal (fun (x,m) (y,n) -> sort_name_expr_eq x y && Int.equal m n)) + u1 u2 + (***********************) (* For binders parsing *) @@ -59,13 +78,11 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with Id.equal id1 id2 | _ -> false -let eq_ast f { CAst.v = x } { CAst.v = y } = f x y - let rec cases_pattern_expr_eq p1 p2 = if CAst.(p1.v == p2.v) then true else match CAst.(p1.v, p2.v) with | CPatAlias(a1,i1), CPatAlias(a2,i2) -> - eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2 + CAst.eq Name.equal i1 i2 && cases_pattern_expr_eq a1 a2 | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) -> qualid_eq c1 c2 && Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && @@ -108,10 +125,10 @@ let rec constr_expr_eq e1 e2 = else match CAst.(e1.v, e2.v) with | CRef (r1,u1), CRef (r2,u2) -> qualid_eq r1 r2 && eq_universes u1 u2 | CFix(id1,fl1), CFix(id2,fl2) -> - eq_ast Id.equal id1 id2 && + lident_eq id1 id2 && List.equal fix_expr_eq fl1 fl2 | CCoFix(id1,fl1), CCoFix(id2,fl2) -> - eq_ast Id.equal id1 id2 && + lident_eq id1 id2 && List.equal cofix_expr_eq fl1 fl2 | CProdN(bl1,a1), CProdN(bl2,a2) -> List.equal local_binder_eq bl1 bl2 && @@ -120,7 +137,7 @@ let rec constr_expr_eq e1 e2 = List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 | CLetIn(na1,a1,t1,b1), CLetIn(na2,a2,t2,b2) -> - eq_ast Name.equal na1 na2 && + CAst.eq Name.equal na1 na2 && constr_expr_eq a1 a2 && Option.equal constr_expr_eq t1 t2 && constr_expr_eq b1 b2 @@ -144,14 +161,14 @@ let rec constr_expr_eq e1 e2 = List.equal case_expr_eq a1 a2 && List.equal branch_expr_eq brl1 brl2 | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) -> - List.equal (eq_ast Name.equal) n1 n2 && - Option.equal (eq_ast Name.equal) m1 m2 && + List.equal (CAst.eq Name.equal) n1 n2 && + Option.equal (CAst.eq Name.equal) m1 m2 && Option.equal constr_expr_eq e1 e2 && constr_expr_eq t1 t2 && constr_expr_eq b1 b2 | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) -> constr_expr_eq e1 e2 && - Option.equal (eq_ast Name.equal) n1 n2 && + Option.equal (CAst.eq Name.equal) n1 n2 && Option.equal constr_expr_eq r1 r2 && constr_expr_eq t1 t2 && constr_expr_eq f1 f2 @@ -161,7 +178,7 @@ let rec constr_expr_eq e1 e2 = | CEvar (id1, c1), CEvar (id2, c2) -> Id.equal id1.CAst.v id2.CAst.v && List.equal instance_eq c1 c2 | CSort s1, CSort s2 -> - Glob_ops.glob_sort_eq s1 s2 + sort_expr_eq s1 s2 | CCast(t1,c1), CCast(t2,c2) -> constr_expr_eq t1 t2 && cast_expr_eq c1 c2 | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) -> @@ -187,12 +204,12 @@ let rec constr_expr_eq e1 e2 = | CGeneralization _ | CDelimiters _ | CArray _), _ -> false and args_eq (a1,e1) (a2,e2) = - Option.equal (eq_ast explicitation_eq) e1 e2 && + Option.equal (CAst.eq explicitation_eq) e1 e2 && constr_expr_eq a1 a2 and case_expr_eq (e1, n1, p1) (e2, n2, p2) = constr_expr_eq e1 e2 && - Option.equal (eq_ast Name.equal) n1 n2 && + Option.equal (CAst.eq Name.equal) n1 n2 && Option.equal cases_pattern_expr_eq p1 p2 and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = @@ -200,35 +217,35 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = constr_expr_eq e1 e2 and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) = - (eq_ast Id.equal id1 id2) && + (lident_eq id1 id2) && Option.equal recursion_order_expr_eq r1 r2 && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) = - (eq_ast Id.equal id1 id2) && + (lident_eq id1 id2) && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 and recursion_order_expr_eq_r r1 r2 = match r1, r2 with - | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2 + | CStructRec i1, CStructRec i2 -> lident_eq i1 i2 | CWfRec (i1,e1), CWfRec (i2,e2) -> constr_expr_eq e1 e2 | CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) -> - Option.equal (eq_ast Id.equal) i1 i2 && + Option.equal lident_eq i1 i2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 | _ -> false -and recursion_order_expr_eq r1 r2 = eq_ast recursion_order_expr_eq_r r1 r2 +and recursion_order_expr_eq r1 r2 = CAst.eq recursion_order_expr_eq_r r1 r2 and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> - eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 + CAst.eq Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> (* Don't care about the [binder_kind] *) - List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2 + List.equal (CAst.eq Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) = diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index dfa51918d1..ffa7c8ec10 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -16,6 +16,10 @@ open Constrexpr (** {6 Equalities on [constr_expr] related types} *) +val sort_name_expr_eq : sort_name_expr -> sort_name_expr -> bool +val univ_level_expr_eq : univ_level_expr -> univ_level_expr -> bool +val sort_expr_eq : sort_expr -> sort_expr -> bool + val explicitation_eq : explicitation -> explicitation -> bool (** Equality on [explicitation]. *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 378adb566c..3969c7ea1f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -923,22 +923,44 @@ let extern_float f scopes = (**********************************************************************) (* mapping glob_constr to constr_expr *) -let extern_glob_sort = function +type extern_env = Id.Set.t * UnivNames.universe_binders +let extern_env env sigma = vars_of_env env, Evd.universe_binders sigma +let empty_extern_env = Id.Set.empty, Id.Map.empty + +let extern_glob_sort_name uvars = function + | GSProp -> CSProp + | GProp -> CProp + | GSet -> CSet + | GLocalUniv u -> CType (qualid_of_lident u) + | GRawUniv u -> CRawType u + | GUniv u -> begin match UnivNames.qualid_of_level uvars u with + | Some qid -> CType qid + | None -> CRawType u + end + +let extern_glob_sort uvars = + map_glob_sort_gen (List.map (on_fst (extern_glob_sort_name uvars))) + +(** wrapper to handle print_universes: don't forget small univs *) +let extern_glob_sort uvars = function (* In case we print a glob_constr w/o having passed through detyping *) - | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u + | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> extern_glob_sort uvars u | UNamed _ when not !print_universes -> UAnonymous {rigid=true} - | UNamed _ | UAnonymous _ as u -> u + | UNamed _ | UAnonymous _ as u -> extern_glob_sort uvars u -let extern_universes = function - | Some _ as l when !print_universes -> l +let extern_instance uvars = function + | Some l when !print_universes -> + Some (List.map (map_glob_sort_gen (extern_glob_sort_name uvars)) l) | _ -> None -let extern_ref vars ref us = +let extern_ref (vars,uvars) ref us = extern_global (select_stronger_impargs (implicits_of_global ref)) - (extern_reference vars ref) (extern_universes us) + (extern_reference vars ref) (extern_instance uvars us) let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) +let add_vname (vars,uvars) na = add_vname vars na, uvars + let rec extern inctx ?impargs scopes vars r = match remove_one_coercion inctx (flatten_application r) with | Some (nargs,inctx,r') -> @@ -995,7 +1017,7 @@ let rec extern inctx ?impargs scopes vars r = (* Otherwise... *) extern_applied_ref inctx (select_stronger_impargs (implicits_of_global ref)) - (ref,extern_reference ?loc vars ref) (extern_universes us) args) + (ref,extern_reference ?loc (fst vars) ref) (extern_instance (snd vars) us) args) | _ -> let args = List.map (fun c -> (sub_extern true scopes vars c,None)) args in let head = sub_extern false scopes vars f in @@ -1015,7 +1037,8 @@ let rec extern inctx ?impargs scopes vars r = | GCases (sty,rtntypopt,tml,eqns) -> let vars' = List.fold_right (Name.fold_right Id.Set.add) - (cases_predicate_names tml) vars in + (cases_predicate_names tml) (fst vars) in + let vars' = vars', snd vars in let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> let na' = match na, DAst.get tm with @@ -1035,7 +1058,7 @@ let rec extern inctx ?impargs scopes vars r = Option.map (fun {CAst.loc;v=(ind,nal)} -> let args = List.map (fun x -> DAst.make @@ PatVar x) nal in let fullargs = add_cpatt_for_params ind args in - extern_ind_pattern_in_scope scopes vars ind fullargs + extern_ind_pattern_in_scope scopes (fst vars) ind fullargs ) x)) tml in @@ -1058,7 +1081,7 @@ let rec extern inctx ?impargs scopes vars r = sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2) | GRec (fk,idv,blv,tyv,bv) -> - let vars' = Array.fold_right Id.Set.add idv vars in + let vars' = on_fst (Array.fold_right Id.Set.add idv) vars in (match fk with | GFix (nv,n) -> let listdecl = @@ -1066,8 +1089,8 @@ let rec extern inctx ?impargs scopes vars r = let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in let (assums,ids,bl) = extern_local_binder scopes vars bl in - let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in - let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in + let vars0 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars in + let vars1 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars' in let n = match nv.(i) with | None -> None @@ -1082,14 +1105,14 @@ let rec extern inctx ?impargs scopes vars r = Array.mapi (fun i fi -> let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in let (_,ids,bl) = extern_local_binder scopes vars bl in - let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in - let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in + let vars0 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars in + let vars1 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars' in ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i), sub_extern true scopes vars1 bv.(i))) idv in CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl)) - | GSort s -> CSort (extern_glob_sort s) + | GSort s -> CSort (extern_glob_sort (snd vars) s) | GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *) @@ -1105,7 +1128,7 @@ let rec extern inctx ?impargs scopes vars r = | GFloat f -> extern_float f (snd scopes) | GArray(u,t,def,ty) -> - CArray(extern_universes u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty) + CArray(extern_instance (snd vars) u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty) in insert_entry_coercion coercion (CAst.make ?loc c) @@ -1127,7 +1150,7 @@ and factorize_prod ?impargs scopes vars na bk t c = let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = extern_typ scopes vars b in - let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in + let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes (fst vars)) disjpat) in let binder = CLocalPattern p in (match b.v with | CProdN (bl,b) -> CProdN (binder::bl,b) @@ -1168,7 +1191,7 @@ and factorize_lambda inctx scopes vars na bk t c = let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = sub_extern inctx scopes vars b in - let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in + let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes (fst vars)) disjpat) in let binder = CLocalPattern p in (match b.v with | CLambdaN (bl,b) -> CLambdaN (binder::bl,b) @@ -1196,7 +1219,7 @@ and extern_local_binder scopes vars = function match DAst.get b with | GLocalDef (na,bk,bd,ty) -> let (assums,ids,l) = - extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in + extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l in (assums,na::ids, CLocalDef(CAst.make na, extern false scopes vars bd, Option.map (extern_typ scopes vars) ty) :: l) @@ -1204,7 +1227,7 @@ and extern_local_binder scopes vars = function | GLocalAssum (na,bk,ty) -> let implicit_type = is_reserved_type na ty in let ty = extern_typ scopes vars ty in - (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with + (match extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) && match na with Name id -> not (occur_var_constr_expr id ty') @@ -1219,7 +1242,7 @@ and extern_local_binder scopes vars = function | GLocalPattern ((p,_),_,bk,ty) -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in - let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in + let p = mkCPatOr (List.map (extern_cases_pattern (fst vars)) p) in let (assums,ids,l) = extern_local_binder scopes vars l in let p = match ty with | None -> p @@ -1227,7 +1250,7 @@ and extern_local_binder scopes vars = function (assums,ids, CLocalPattern p :: l) and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = - let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in + let pll = List.map (List.map (extern_cases_pattern_in_scope scopes (fst vars))) pll in make ?loc (pll,extern inctx scopes vars c) and extern_notations inctx scopes vars nargs t = @@ -1277,6 +1300,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = end | AppBoundedNotation _ -> raise No_match in (* Try matching ... *) + let vars, uvars = vars in let terms,termlists,binders,binderlists = match_notation_constr ~print_univ:(!print_universes) t ~vars pat in (* Try availability of interpretation ... *) @@ -1300,35 +1324,43 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = let l = List.map (fun ((vars,c),(subentry,(scopt,scl))) -> extern (* assuming no overloading: *) true - (subentry,(scopt,scl@scopes')) vars c) - terms in + (subentry,(scopt,scl@scopes')) (vars,uvars) c) + terms + in let ll = List.map (fun ((vars,l),(subentry,(scopt,scl))) -> - List.map (extern true (subentry,(scopt,scl@scopes')) vars) l) - termlists in + List.map (extern true (subentry,(scopt,scl@scopes')) (vars,uvars)) l) + termlists + in let bl = List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> - (mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)), - Explicit) - binders in + (mkCPatOr (List.map + (extern_cases_pattern_in_scope + (subentry,(scopt,scl@scopes')) vars) + bl)), + Explicit) + binders + in let bll = List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> - pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) - binderlists in + pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) (vars,uvars) bl)) + binderlists + in let c = make_notation loc specific_ntn (l,ll,bl,bll) in let c = insert_entry_coercion coercion (insert_delimiters c key) in let args = fill_arg_scopes args argsscopes allscopes in - let args = extern_args (extern true) vars args in + let args = extern_args (extern true) (vars,uvars) args in CAst.make ?loc @@ extern_applied_notation inctx nallargs argsimpls c args) | SynDefRule kn -> let l = List.map (fun ((vars,c),(subentry,(scopt,scl))) -> - extern true (subentry,(scopt,scl@snd scopes)) vars c) - terms in + extern true (subentry,(scopt,scl@snd scopes)) (vars,uvars) c) + terms + in let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in let a = CRef (cf,None) in let args = fill_arg_scopes args argsscopes allscopes in - let args = extern_args (extern true) vars args in + let args = extern_args (extern true) (vars,uvars) args in let c = CAst.make ?loc @@ extern_applied_syntactic_definition inctx nallargs argsimpls (a,cf) l args in if isCRef_no_univ c.CAst.v && entry_has_global custom then c else match availability_of_entry_coercion custom InConstrEntrySomeLevel with @@ -1348,7 +1380,7 @@ let extern_glob_type ?impargs vars c = let extern_constr ?lax ?(inctx=false) ?scope env sigma t = let r = Detyping.detype Detyping.Later ?lax false Id.Set.empty env sigma t in - let vars = vars_of_env env in + let vars = extern_env env sigma in extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r let extern_constr_in_scope ?lax ?inctx scope env sigma t = @@ -1364,16 +1396,16 @@ let extern_type ?lax ?(goal_concl_style=false) env sigma ?impargs t = (* consideration; see namegen.ml for further details *) let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype Detyping.Later ?lax goal_concl_style avoid env sigma t in - extern_glob_type ?impargs (vars_of_env env) r + extern_glob_type ?impargs (extern_env env sigma) r -let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) +let extern_sort sigma s = extern_glob_sort (Evd.universe_binders sigma) (detype_sort sigma s) let extern_closed_glob ?lax ?(goal_concl_style=false) ?(inctx=false) ?scope env sigma t = let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t in - let vars = vars_of_env env in + let vars = extern_env env sigma in extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r (******************************************************************) @@ -1491,10 +1523,13 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with GArray (None, Array.map glob_of t, glob_of def, glob_of ty) let extern_constr_pattern env sigma pat = - extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat) + extern true (InConstrEntrySomeLevel,(None,[])) + (* XXX no vars? *) + (Id.Set.empty, Evd.universe_binders sigma) + (glob_of_pat Id.Set.empty env sigma pat) let extern_rel_context where env sigma sign = let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in - let vars = vars_of_env env in + let vars = extern_env env sigma in let a = List.map (extended_glob_local_binder_of_decl) a in pi3 (extern_local_binder (InConstrEntrySomeLevel,(None,[])) vars a) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index f85e49d2df..298b52f0be 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -23,9 +23,12 @@ open Ltac_pretype (** Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing *) +type extern_env = Id.Set.t * UnivNames.universe_binders +val extern_env : env -> Evd.evar_map -> extern_env + val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr -val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr -val extern_glob_type : ?impargs:Glob_term.binding_kind list -> Id.Set.t -> 'a glob_constr_g -> constr_expr +val extern_glob_constr : extern_env -> 'a glob_constr_g -> constr_expr +val extern_glob_type : ?impargs:Glob_term.binding_kind list -> extern_env -> 'a glob_constr_g -> constr_expr val extern_constr_pattern : names_context -> Evd.evar_map -> constr_pattern -> constr_expr val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> @@ -43,7 +46,7 @@ val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> types -> constr_expr -val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort +val extern_sort : Evd.evar_map -> Sorts.t -> sort_expr val extern_rel_context : constr option -> env -> Evd.evar_map -> rel_context -> local_binder_expr list @@ -96,3 +99,6 @@ val toggle_scope_printing : val toggle_notation_printing : ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit + +(** Probably shouldn't be used *) +val empty_extern_env : extern_env diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0645636255..cf2f333596 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -254,9 +254,12 @@ let contract_curly_brackets_pat ntn (l,ll) = (* side effect; don't inline *) (InConstrEntry,!ntn'),(l,ll) +type local_univs = { bound : Univ.Level.t Id.Map.t; unb_univs : bool } + type intern_env = { - ids: Names.Id.Set.t; + ids: Id.Set.t; unb: bool; + local_univs: local_univs; tmp_scope: Notation_term.tmp_scope_name option; scopes: Notation_term.scope_name list; impls: internalization_env; @@ -1160,6 +1163,32 @@ let glob_sort_of_level (level: glob_level) : glob_sort = | UAnonymous {rigid} -> UAnonymous {rigid} | UNamed id -> UNamed [id,0] +let intern_sort_name ~local_univs = function + | CSProp -> GSProp + | CProp -> GProp + | CSet -> GSet + | CRawType u -> GRawUniv u + | CType qid -> + let is_id = qualid_is_ident qid in + let local = if not is_id then None + else Id.Map.find_opt (qualid_basename qid) local_univs.bound + in + match local with + | Some u -> GUniv u + | None -> + try GUniv (Univ.Level.make (Nametab.locate_universe qid)) + with Not_found -> + if is_id && local_univs.unb_univs + then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid)) + else + CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".") + +let intern_sort ~local_univs s = + map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s + +let intern_instance ~local_univs us = + Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us + (* Is it a global reference or a syntactic definition? *) let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let loc = qid.loc in @@ -1225,6 +1254,7 @@ let check_applied_projection isproj realref qid = let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us args qid = let loc = qid.CAst.loc in + let us = intern_instance ~local_univs:env.local_univs us in if qualid_is_ident qid then try let res = intern_var env lvar namedctx loc (qualid_basename qid) us in @@ -1256,7 +1286,8 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us let interp_reference vars r = let (r,_,_),_ = intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None) - {ids = Id.Set.empty; unb = false ; + {ids = Id.Set.empty; unb = false; + local_univs = { bound=Id.Map.empty; unb_univs = false };(* <- doesn't matter here *) tmp_scope = None; scopes = []; impls = empty_internalization_env; binder_block_names = None} Environ.empty_named_context_val @@ -2269,12 +2300,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* end *) | CSort s -> DAst.make ?loc @@ - GSort s + GSort (intern_sort ~local_univs:env.local_univs s) | CCast (c1, c2) -> DAst.make ?loc @@ GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2) | CArray(u,t,def,ty) -> - DAst.make ?loc @@ GArray(u, Array.map (intern env) t, intern env def, intern env ty) + DAst.make ?loc @@ GArray(intern_instance ~local_univs:env.local_univs u, Array.map (intern env) t, intern env def, intern env ty) ) and intern_type env = intern (set_type_scope env) @@ -2446,6 +2477,8 @@ let extract_ids env = (Termops.ids_of_rel_context (Environ.rel_context env)) Id.Set.empty +let bound_univs sigma = Evd.universe_binders sigma + let scope_of_type_kind env sigma = function | IsType -> Notation.current_type_scope_name () | OfType typ -> compute_type_scope env sigma typ @@ -2468,8 +2501,9 @@ let intern_gen kind env sigma let tmp_scope = scope_of_type_kind env sigma kind in let k = allowed_binder_kind_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; - tmp_scope = tmp_scope; scopes = []; - impls; binder_block_names = Some (k,Id.Map.domain impls)} + local_univs = { bound = bound_univs sigma; unb_univs = true }; + tmp_scope = tmp_scope; scopes = []; + impls; binder_block_names = Some (k,Id.Map.domain impls)} pattern_mode (ltacvars, Id.Map.empty) c let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c @@ -2558,7 +2592,9 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) let impls = empty_internalization_env in let k = allowed_binder_kind_of_type_kind kind in internalize env - {ids; unb = false; tmp_scope; scopes = []; impls; + {ids; unb = false; + local_univs = { bound = bound_univs sigma; unb_univs = true }; + tmp_scope; scopes = []; impls; binder_block_names = Some (k,Id.Set.empty)} pattern_mode (ltacvars, vl) c @@ -2568,8 +2604,11 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in let c = internalize env - {ids; unb = false; tmp_scope = None; scopes = []; impls; binder_block_names = None} - false (empty_ltac_sign, vl) a in + {ids; unb = false; + local_univs = { bound = Id.Map.empty; unb_univs = false }; + tmp_scope = None; scopes = []; impls; binder_block_names = None} + false (empty_ltac_sign, vl) a + in (* Splits variables into those that are binding, bound, or both *) (* Translate and check that [c] has all its free variables bound in [vars] *) let a, reversible = notation_constr_of_glob_constr nenv c in @@ -2596,7 +2635,7 @@ let interp_binder_evars env sigma na t = let my_intern_constr env lvar acc c = internalize env acc false lvar c -let intern_context env impl_env binders = +let intern_context env ~bound_univs impl_env binders = let lvar = (empty_ltac_sign, Id.Map.empty) in let ids = (* We assume all ids around are parts of the prefix of the current @@ -2607,6 +2646,7 @@ let intern_context env impl_env binders = let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in (env, bl)) ({ids; unb = false; + local_univs = { bound = bound_univs; unb_univs = true }; tmp_scope = None; scopes = []; impls = impl_env; binder_block_names = Some (Some AbsPi,ids)}, []) binders in (lenv.impls, List.map glob_local_binder_of_extended bl) @@ -2643,17 +2683,21 @@ let interp_glob_context_evars ?(program_mode=false) env sigma bl = sigma, ((env, par), List.rev impls) let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) env sigma params = - let int_env,bl = intern_context env impl_env params in + let int_env,bl = intern_context env ~bound_univs:(bound_univs sigma) impl_env params in let sigma, x = interp_glob_context_evars ?program_mode env sigma bl in sigma, (int_env, x) (** Local universe and constraint declarations. *) +let interp_known_level evd u = + let u = intern_sort_name ~local_univs:{bound = bound_univs evd; unb_univs=false} u in + Pretyping.known_glob_level evd u + let interp_univ_constraints env evd cstrs = let interp (evd,cstrs) (u, d, u') = - let ul = Pretyping.interp_known_glob_level evd u in - let u'l = Pretyping.interp_known_glob_level evd u' in + let ul = interp_known_level evd u in + let u'l = interp_known_level evd u' in let cstr = (ul,d,u'l) in let cstrs' = Univ.Constraint.add cstr cstrs in try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 0de6c3e89d..f92a54e23f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -88,7 +88,8 @@ val intern_gen : typing_constraint -> env -> evar_map -> val intern_pattern : env -> cases_pattern_expr -> lident list * (Id.t Id.Map.t * cases_pattern) list -val intern_context : env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list +val intern_context : env -> bound_univs:UnivNames.universe_binders -> + internalization_env -> local_binder_expr list -> internalization_env * glob_decl list (** {6 Composing internalization with type inference (pretyping) } *) @@ -198,6 +199,8 @@ val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit (** Check that a list of record field definitions doesn't contain duplicates. *) +val interp_known_level : Evd.evar_map -> sort_name_expr -> Univ.Level.t + (** Local universe and constraint declarations. *) val interp_univ_decl : Environ.env -> universe_decl_expr -> Evd.evar_map * UState.universe_decl diff --git a/kernel/names.ml b/kernel/names.ml index 13761ca245..be65faf234 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1115,3 +1115,5 @@ let eq_egr e1 e2 = match e1, e2 with type lident = Id.t CAst.t type lname = Name.t CAst.t type lstring = string CAst.t + +let lident_eq = CAst.eq Id.equal diff --git a/kernel/names.mli b/kernel/names.mli index 74a4e6f7d0..747299bb12 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -727,3 +727,5 @@ val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool type lident = Id.t CAst.t type lname = Name.t CAst.t type lstring = string CAst.t + +val lident_eq : lident -> lident -> bool diff --git a/lib/cAst.ml b/lib/cAst.ml index 18fa1c9b0d..30b7fca587 100644 --- a/lib/cAst.ml +++ b/lib/cAst.ml @@ -24,3 +24,5 @@ let map_from_loc f l = let with_val f n = f n.v let with_loc_val f n = f ?loc:n.loc n.v + +let eq f x y = f x.v y.v diff --git a/lib/cAst.mli b/lib/cAst.mli index 2e07d1cd78..025bdf25ab 100644 --- a/lib/cAst.mli +++ b/lib/cAst.mli @@ -22,3 +22,5 @@ val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> 'b t val with_val : ('a -> 'b) -> 'a t -> 'b val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> 'a t -> 'b + +val eq : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool diff --git a/library/libnames.ml b/library/libnames.ml index 88b2e41855..ba1ef1e2f9 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -145,6 +145,8 @@ let qualid_of_dirpath ?loc dir = let (l,a) = split_dirpath dir in make_qualid ?loc l a +let qualid_of_lident lid = qualid_of_ident ?loc:lid.CAst.loc lid.CAst.v + let qualid_is_ident qid = DirPath.is_empty qid.CAst.v.dirpath diff --git a/library/libnames.mli b/library/libnames.mli index a384510879..65aca0c87d 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -77,6 +77,7 @@ val qualid_of_string : ?loc:Loc.t -> string -> qualid val qualid_of_path : ?loc:Loc.t -> full_path -> qualid val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid +val qualid_of_lident : lident -> qualid val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t diff --git a/library/nametab.ml b/library/nametab.ml index a51c281f2b..d5cc4f8ac5 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -562,9 +562,9 @@ let shortest_qualid_of_modtype ?loc kn = let sp = MPmap.find kn !the_modtyperevtab in MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab -let shortest_qualid_of_universe ?loc kn = +let shortest_qualid_of_universe ?loc ctx kn = let sp = UnivIdMap.find kn !the_univrevtab in - UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab + UnivTab.shortest_qualid ?loc ctx sp !the_univtab let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) diff --git a/library/nametab.mli b/library/nametab.mli index 8a8b59733c..fa27dcab9a 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -206,7 +206,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid -val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid +val shortest_qualid_of_universe : ?loc:Loc.t -> Id.Set.t -> Univ.Level.UGlobal.t -> qualid (** {5 Generic name handling} *) diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 68530178f8..efe4bfd7f6 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -106,9 +106,9 @@ GRAMMAR EXTEND Gram [ [ c = lconstr -> { c } ] ] ; sort: - [ [ "Set" -> { UNamed [GSet,0] } - | "Prop" -> { UNamed [GProp,0] } - | "SProp" -> { UNamed [GSProp,0] } + [ [ "Set" -> { UNamed [CSet,0] } + | "Prop" -> { UNamed [CProp,0] } + | "SProp" -> { UNamed [CSProp,0] } | "Type" -> { UAnonymous {rigid=true} } | "Type"; "@{"; "_"; "}" -> { UAnonymous {rigid=false} } | "Type"; "@{"; u = universe; "}" -> { UNamed u } ] ] @@ -124,9 +124,9 @@ GRAMMAR EXTEND Gram | -> { 0 } ] ] ; universe_name: - [ [ id = global -> { GType id } - | "Set" -> { GSet } - | "Prop" -> { GProp } ] ] + [ [ id = global -> { CType id } + | "Set" -> { CSet } + | "Prop" -> { CProp } ] ] ; universe_expr: [ [ id = universe_name; n = universe_increment -> { (id,n) } ] ] @@ -282,12 +282,12 @@ GRAMMAR EXTEND Gram | -> { None } ] ] ; universe_level: - [ [ "Set" -> { UNamed GSet } + [ [ "Set" -> { UNamed CSet } (* no parsing SProp as a level *) - | "Prop" -> { UNamed GProp } + | "Prop" -> { UNamed CProp } | "Type" -> { UAnonymous {rigid=true} } | "_" -> { UAnonymous {rigid=false} } - | id = global -> { UNamed (GType id) } ] ] + | id = global -> { UNamed (CType id) } ] ] ; fix_decls: [ [ dcl = fix_decl -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) } diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d0ae594db1..7cd73b4c24 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -190,9 +190,9 @@ module Constr : [@@deprecated "Deprecated in 8.13; use 'term' instead"] val ident : Id.t Entry.t val global : qualid Entry.t - val universe_name : Glob_term.glob_sort_name Entry.t - val universe_level : Glob_term.glob_level Entry.t - val sort : Glob_term.glob_sort Entry.t + val universe_name : sort_name_expr Entry.t + val universe_level : univ_level_expr Entry.t + val sort : sort_expr Entry.t val sort_family : Sorts.family Entry.t val pattern : cases_pattern_expr Entry.t val constr_pattern : constr_expr Entry.t diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index c485c38009..23a7b89d2c 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -443,7 +443,7 @@ let cc_tactic depth additionnal_terms = let pr_missing (c, missing) = let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in let holes = List.init missing (fun _ -> hole) in - Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes)) + Printer.pr_glob_constr_env env sigma (DAst.make @@ GApp (c, holes)) in let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing." ++ fnl () ++ diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 767a9ec39b..5bfb37f4cb 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -458,9 +458,11 @@ let rec pattern_to_term_and_type env typ = but only the value of the function *) +let pr_glob_constr_env env x = pr_glob_constr_env env (Evd.from_env env) x + let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_return = - observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); + observe (str " Entering : " ++ pr_glob_constr_env env rt); let open CAst in match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ @@ -638,9 +640,7 @@ let rec build_entry_lc env sigma funnames avoid rt : with Not_found -> user_err ( str "Cannot find the inductive associated to " - ++ Printer.pr_glob_constr_env env b - ++ str " in " - ++ Printer.pr_glob_constr_env env rt + ++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt ++ str ". try again with a cast" ) in let case_pats = build_constructors_of_type (fst ind) [] in @@ -662,9 +662,7 @@ let rec build_entry_lc env sigma funnames avoid rt : with Not_found -> user_err ( str "Cannot find the inductive associated to " - ++ Printer.pr_glob_constr_env env b - ++ str " in " - ++ Printer.pr_glob_constr_env env rt + ++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt ++ str ". try again with a cast" ) in let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in @@ -1321,11 +1319,11 @@ let do_build_inductive evd (funconstants : pconstant list) @@ Constrexpr.CLetIn ( CAst.make n , with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) t , Some (with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) typ) , acc ) | None -> @@ -1335,7 +1333,7 @@ let do_build_inductive evd (funconstants : pconstant list) ( [CAst.make n] , Constrexpr_ops.default_binder_kind , with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) t ) ] , acc )) rel_first_args @@ -1410,11 +1408,11 @@ let do_build_inductive evd (funconstants : pconstant list) @@ Constrexpr.CLetIn ( CAst.make n , with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) t , Some (with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) typ) , acc ) | None -> @@ -1424,7 +1422,7 @@ let do_build_inductive evd (funconstants : pconstant list) ( [CAst.make n] , Constrexpr_ops.default_binder_kind , with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) t ) ] , acc )) rel_first_args @@ -1448,16 +1446,16 @@ let do_build_inductive evd (funconstants : pconstant list) | Some typ -> Constrexpr.CLocalDef ( CAst.make n - , Constrextern.extern_glob_constr Id.Set.empty t + , Constrextern.(extern_glob_constr empty_extern_env) t , Some (with_full_print - (Constrextern.extern_glob_constr Id.Set.empty) + Constrextern.(extern_glob_constr empty_extern_env) typ) ) | None -> Constrexpr.CLocalAssum ( [CAst.make n] , Constrexpr_ops.default_binder_kind - , Constrextern.extern_glob_constr Id.Set.empty t )) + , Constrextern.(extern_glob_constr empty_extern_env) t )) rels_params in let ext_rels_constructors = @@ -1466,7 +1464,7 @@ let do_build_inductive evd (funconstants : pconstant list) ( false , ( CAst.make id , with_full_print - (Constrextern.extern_glob_type Id.Set.empty) + Constrextern.(extern_glob_type empty_extern_env) ((* zeta_normalize *) alpha_rt rel_params_ids t) ) ))) rel_constructors in diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index ff4a82f864..daed855600 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -150,7 +150,7 @@ let pr_occurrences = pr_occurrences () () () let pr_gen env sigma prc _prlc _prtac x = prc env sigma x let pr_globc env sigma _prc _prlc _prtac (_,glob) = - Printer.pr_glob_constr_env env glob + Printer.pr_glob_constr_env env sigma glob let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index eed9419946..069a342b2a 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -63,7 +63,7 @@ let eval_uconstrs ist cs = let pr_auto_using_raw env sigma _ _ _ = Pptactic.pr_auto_using @@ Ppconstr.pr_constr_expr env sigma let pr_auto_using_glob env sigma _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> - Printer.pr_glob_constr_env env c) + Printer.pr_glob_constr_env env sigma c) let pr_auto_using env sigma _ _ _ = Pptactic.pr_auto_using @@ Printer.pr_closed_glob_env env sigma diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index a3f03b5bb5..f12ca0685e 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -40,9 +40,9 @@ type glob_constr_with_bindings = glob_constr_and_expr with_bindings type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings let pr_glob_constr_with_bindings_sign env sigma _ _ _ (ge : glob_constr_with_bindings_sign) = - Printer.pr_glob_constr_env env (fst (fst (snd ge))) + Printer.pr_glob_constr_env env sigma (fst (fst (snd ge))) let pr_glob_constr_with_bindings env sigma _ _ _ (ge : glob_constr_with_bindings) = - Printer.pr_glob_constr_env env (fst (fst ge)) + Printer.pr_glob_constr_env env sigma (fst (fst ge)) let pr_constr_expr_with_bindings env sigma prc _ _ (ge : constr_expr_with_bindings) = prc env sigma (fst ge) let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c) let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index cd7b1f7f28..fa5bbf7676 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1130,12 +1130,12 @@ let pr_goal_selector ~toplevel s = let rec prtac n (t:glob_tactic_expr) = let pr = { pr_tactic = prtac; - pr_constr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)); - pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)); - pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env)); - pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env)); + pr_constr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma)); + pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma)); + pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma)); + pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env sigma)); pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env)); - pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env)); + pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env sigma)); pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant); pr_name = pr_lident; pr_generic = Pputils.pr_glb_generic; @@ -1166,7 +1166,7 @@ let pr_goal_selector ~toplevel s = let pr = { pr_tactic = (fun _ _ -> str "<tactic>"); pr_constr = pr_econstr_env; - pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)); + pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma)); pr_lconstr = pr_leconstr_env; pr_pattern = pr_constr_pattern_env; pr_lpattern = pr_lconstr_pattern_env; @@ -1189,7 +1189,7 @@ let pr_goal_selector ~toplevel s = let pr_raw_extend env sigma = pr_raw_extend_rec @@ pr_raw_tactic_level env sigma - let pr_glob_extend env sigma = pr_glob_extend_rec (pr_glob_tactic_level env) + let pr_glob_extend env = pr_glob_extend_rec (pr_glob_tactic_level env) let pr_alias pr lev key args = pr_alias_gen (fun _ arg -> pr arg) lev key args @@ -1212,8 +1212,8 @@ let declare_extra_genarg_pprule wit f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in let g x = Genprint.PrinterBasic (fun env sigma -> - g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)) - (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env)) + g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma)) + (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma)) (fun env sigma -> pr_glob_tactic_level env) x) in let h x = @@ -1242,8 +1242,8 @@ let declare_extra_genarg_pprule_with_level wit default_already_surrounded = default_surrounded; default_ensure_surrounded = default_non_surrounded; printer = (fun env sigma n -> - g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)) - (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env)) + g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma)) + (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma)) (fun env sigma -> pr_glob_tactic_level env) n x) } in let h x = @@ -1301,10 +1301,10 @@ let register_basic_print0 wit f g h = Genprint.register_print0 wit (lift f) (lift g) (lift_top h) let pr_glob_constr_pptac env sigma c = - pr_glob_constr_env env c + pr_glob_constr_env env sigma c let pr_lglob_constr_pptac env sigma c = - pr_lglob_constr_env env c + pr_lglob_constr_env env sigma c let pr_raw_intro_pattern = lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5e199dad62..79e0adf9f7 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -124,7 +124,7 @@ val pr_glb_generic : env -> Evd.evar_map -> glevel generic_argument -> Pp.t val pr_raw_extend: env -> Evd.evar_map -> int -> ml_tactic_entry -> raw_tactic_arg list -> Pp.t -val pr_glob_extend: env -> Evd.evar_map -> int -> +val pr_glob_extend: env -> int -> ml_tactic_entry -> glob_tactic_arg list -> Pp.t val pr_extend : diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 9c15d24dd3..aa2449d962 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -244,7 +244,8 @@ let string_of_call ck = (Pptactic.pr_glob_tactic (Global.env ()) (Tacexpr.TacAtom (CAst.make te))) | Tacexpr.LtacConstrInterp (c, _) -> - pr_glob_constr_env (Global.env ()) c + let env = Global.env () in + pr_glob_constr_env env (Evd.from_env env) c | Tacexpr.LtacMLCall te -> (Pptactic.pr_glob_tactic (Global.env ()) te) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 00ac155f0e..f2241e78d2 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -773,7 +773,7 @@ let interp_may_eval f ist env sigma = function function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> - str"interpretation of term " ++ pr_glob_constr_env env (fst c))); + str"interpretation of term " ++ pr_glob_constr_env env sigma (fst c))); Exninfo.iraise reraise (* Interprets a constr expression possibly to first evaluate *) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 5fbea4eeef..c4c528d373 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -16,11 +16,12 @@ open Tacexpr let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () let prtac x = - Pptactic.pr_glob_tactic (Global.env()) x + let env = Global.env () in + Pptactic.pr_glob_tactic env x let prmatchpatt env sigma hyp = Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp let prmatchrl env sigma rl = - Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env())) + Pptactic.pr_match_rule false prtac (fun (_,p) -> Printer.pr_constr_pattern_env env sigma p) rl (* This module intends to be a beginning of debugger for tactic expressions. @@ -366,24 +367,22 @@ let explain_ltac_call_trace last trace loc = | Tacexpr.LtacNotationCall kn -> quote (Pptactic.pr_alias_key kn) | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst) | Tacexpr.LtacMLCall t -> - quote (Pptactic.pr_glob_tactic (Global.env()) t) + quote (prtac t) | Tacexpr.LtacVarCall (id,t) -> quote (Id.print id) ++ strbrk " (bound to " ++ - Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" + prtac t ++ str ")" | Tacexpr.LtacAtomCall te -> - quote (Pptactic.pr_glob_tactic (Global.env()) - (Tacexpr.TacAtom (CAst.make te))) + quote (prtac (Tacexpr.TacAtom (CAst.make te))) | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) -> - quote (Printer.pr_glob_constr_env (Global.env()) c) ++ + (* XXX: This hooks into the CErrors's additional error info API so + it is tricky to provide the right env for now. *) + let env = Global.env() in + let sigma = Evd.from_env env in + quote (Printer.pr_glob_constr_env env sigma c) ++ (if not (Id.Map.is_empty vars) then strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - (* XXX: This hooks into the CErrors's additional error - info API so it is tricky to provide the right env for - now. *) - let env = Global.env () in - let sigma = Evd.from_env env in Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index 42b9248979..61643c2aa3 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -50,7 +50,7 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) = SsrHyp (Loc.tag ?loc id) :: clr', rcs' | _ -> clr', rcs' -let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl) +let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl) (project gl) let interp_nbargs ist gl rc = try diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index cb58b9bcb8..cd219838d5 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -895,7 +895,7 @@ open Constrexpr open Util (** Constructors for constr_expr *) -let mkCProp loc = CAst.make ?loc @@ CSort (UNamed [GProp,0]) +let mkCProp loc = CAst.make ?loc @@ CSort (UNamed [CProp,0]) let mkCType loc = CAst.make ?loc @@ CSort (UAnonymous {rigid=true}) let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None) let rec mkCHoles ?loc n = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index a7ebd5f9f5..fdfba48024 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -84,7 +84,7 @@ let interp_congrarg_at ist gl n rf ty m = if i + n > m then None else try let rt = mkRApp congrn (args1 @ mkRApp rf (mkRHoles i) :: args2) in - ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) rt)); + ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt)); Some (interp_refine ist gl rt) with _ -> loop (i + 1) in loop 0 diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index ab36d4fc7c..95c8024e89 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -57,17 +57,16 @@ let pr_guarded guard prc c = let s = Format.flush_str_formatter () ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c -let prl_constr_expr = +let with_global_env_evm f x = let env = Global.env () in let sigma = Evd.from_env env in - Ppconstr.pr_lconstr_expr env sigma -let pr_glob_constr c = Printer.pr_glob_constr_env (Global.env ()) c -let prl_glob_constr c = Printer.pr_lglob_constr_env (Global.env ()) c + f env sigma x + +let prl_constr_expr = with_global_env_evm Ppconstr.pr_lconstr_expr +let pr_glob_constr = with_global_env_evm Printer.pr_glob_constr_env +let prl_glob_constr = with_global_env_evm Printer.pr_lglob_constr_env let pr_glob_constr_and_expr = function - | _, Some c -> - let env = Global.env () in - let sigma = Evd.from_env env in - Ppconstr.pr_constr_expr env sigma c + | _, Some c -> with_global_env_evm Ppconstr.pr_constr_expr c | c, None -> pr_glob_constr c let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 99cf197b78..3e44bd4d3b 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -203,8 +203,8 @@ let pr_raw_ssrhintref env sigma prc _ _ = let open CAst in function let pr_rawhintref env sigma c = match DAst.get c with | GApp (f, args) when isRHoles args -> - pr_glob_constr_env env f ++ str "|" ++ int (List.length args) - | _ -> pr_glob_constr_env env c + pr_glob_constr_env env sigma f ++ str "|" ++ int (List.length args) + | _ -> pr_glob_constr_env env sigma c let pr_glob_ssrhintref env sigma _ _ _ (c, _) = pr_rawhintref env sigma c diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index d99ead139d..97926753f5 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -195,7 +195,7 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal -> let env = Goal.env goal in let sigma = Goal.sigma goal in Ssrprinters.ppdebug (lazy - Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env glob)); + Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env sigma glob)); try let sigma,term = Tacinterp.interp_open_constr ist env sigma (glob,None) in Ssrprinters.ppdebug (lazy @@ -205,7 +205,7 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal -> (* XXX this is another catch all! *) let e, info = Exninfo.capture e in Ssrprinters.ppdebug (lazy - Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob)); + Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env sigma glob)); tclZERO ~info e end diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index a4aa08300d..ea014250ca 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -88,8 +88,12 @@ let pr_guarded guard prc c = let s = Pp.string_of_ppcmds (prc c) ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c (* More sensible names for constr printers *) -let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c -let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c +let with_global_env_evm f x = + let env = Global.env () in + let sigma = Evd.from_env env in + f env sigma x +let prl_glob_constr = with_global_env_evm pr_lglob_constr_env +let pr_glob_constr = with_global_env_evm pr_glob_constr_env let prl_constr_expr = pr_lconstr_expr let pr_constr_expr = pr_constr_expr let prl_glob_constr_and_expr env sigma = function diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a12a832f76..402a6f6ed3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -648,26 +648,16 @@ let detype_cofix detype flags avoid env sigma n (names,tys,bodies) = Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) -(* TODO use some algebraic type with a case for unnamed univs so we - can cleanly detype them. NB: this corresponds to a hack in - Pretyping.interp_universe_level_name to convert Foo.xx strings into - universes. *) -let hack_qualid_of_univ_level sigma l = - match Termops.reference_of_level sigma l with - | Some qid -> qid - | None -> - let path = String.split_on_char '.' (Univ.Level.to_string l) in - let path = List.rev_map Id.of_string_soft path in - Libnames.qualid_of_dirpath (DirPath.make path) +let detype_level_name sigma l = + if Univ.Level.is_sprop l then GSProp else + if Univ.Level.is_prop l then GProp else + if Univ.Level.is_set l then GSet else + match UState.id_of_level (Evd.evar_universe_context sigma) l with + | Some id -> GLocalUniv (CAst.make id) + | None -> GUniv l let detype_universe sigma u = - let fn (l, n) = - let s = - if Univ.Level.is_prop l then GProp else - if Univ.Level.is_set l then GSet else - GType (hack_qualid_of_univ_level sigma l) in - (s, n) in - List.map fn (Univ.Universe.repr u) + List.map (on_fst (detype_level_name sigma)) (Univ.Universe.repr u) let detype_sort sigma = function | SProp -> UNamed [GSProp,0] @@ -684,8 +674,7 @@ type binder_kind = BProd | BLambda | BLetIn (* Main detyping function *) let detype_level sigma l = - let l = hack_qualid_of_univ_level sigma l in - UNamed (GType l) + UNamed (detype_level_name sigma l) let detype_instance sigma l = let l = EInstance.kind sigma l in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index d631be18b8..86d2cc78e0 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -48,8 +48,10 @@ let glob_sort_name_eq g1 g2 = match g1, g2 with | GSProp, GSProp | GProp, GProp | GSet, GSet -> true - | GType u1, GType u2 -> Libnames.qualid_eq u1 u2 - | (GSProp|GProp|GSet|GType _), _ -> false + | GUniv u1, GUniv u2 -> Univ.Level.equal u1 u2 + | GLocalUniv u1, GLocalUniv u2 -> lident_eq u1 u2 + | GRawUniv u1, GRawUniv u2 -> Univ.Level.equal u1 u2 + | (GSProp|GProp|GSet|GUniv _|GLocalUniv _|GRawUniv _), _ -> false exception ComplexSort @@ -60,6 +62,10 @@ let glob_sort_family = let open Sorts in function | UNamed [GSet,0] -> InSet | _ -> raise ComplexSort +let map_glob_sort_gen f = function + | UNamed l -> UNamed (f l) + | UAnonymous _ as x -> x + let glob_sort_gen_eq f u1 u2 = match u1, u2 with | UAnonymous {rigid=r1}, UAnonymous {rigid=r2} -> r1 = r2 diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 6da8173dce..5ad1a207f3 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -11,8 +11,12 @@ open Names open Glob_term +val map_glob_sort_gen : ('a -> 'b) -> 'a glob_sort_gen -> 'b glob_sort_gen + (** Equalities *) +val glob_sort_gen_eq : ('a -> 'a -> bool) -> 'a glob_sort_gen -> 'a glob_sort_gen -> bool + val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool val glob_level_eq : Glob_term.glob_level -> Glob_term.glob_level -> bool diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 0b4eab1475..a957bc0fcd 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -26,7 +26,13 @@ type glob_sort_name = | GSProp (** representation of [SProp] literal *) | GProp (** representation of [Prop] level *) | GSet (** representation of [Set] level *) - | GType of Libnames.qualid (** representation of a [Type] level *) + | GUniv of Univ.Level.t + | GLocalUniv of lident (** Locally bound universes (may also be nonstrict declaration) *) + | GRawUniv of Univ.Level.t + (** Hack for funind, DO NOT USE + + Note that producing the similar Constrexpr.CRawType for printing + is OK, just don't try to reinterp it. *) type 'a glob_sort_gen = | UAnonymous of { rigid : bool } (** not rigid = unifiable by minimization *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b70ff20e32..65950edb81 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -130,53 +130,32 @@ let is_strict_universe_declarations = (** Miscellaneous interpretation functions *) -let interp_known_universe_level_name evd qid = - try - let open Libnames in - if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid - else raise Not_found +let universe_level_name evd ({CAst.v=id} as lid) = + try evd, Evd.universe_of_name evd id with Not_found -> - let qid = Nametab.locate_universe qid in - Univ.Level.make qid + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc:lid.CAst.loc ~name:id univ_rigid evd + else user_err ?loc:lid.CAst.loc ~hdr:"universe_level_name" + (Pp.(str "Undeclared universe: " ++ Id.print id)) -let interp_universe_level_name evd qid = - try evd, interp_known_universe_level_name evd qid - with Not_found -> - if Libnames.qualid_is_ident qid then (* Undeclared *) - let id = Libnames.qualid_basename qid in - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd - else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ Id.print id)) - else - let dp, i = Libnames.repr_qualid qid in - let num = - try int_of_string (Id.to_string i) - with Failure _ -> - user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid)) - in - let level = Univ.Level.(make (UGlobal.make dp num)) in - let evd = - try Evd.add_global_univ evd level - with UGraph.AlreadyDeclared -> evd - in evd, level - -let interp_sort_name sigma = function +let sort_name sigma = function | GSProp -> sigma, Univ.Level.sprop | GProp -> sigma, Univ.Level.prop | GSet -> sigma, Univ.Level.set - | GType l -> interp_universe_level_name sigma l + | GUniv u -> sigma, u + | GRawUniv u -> + (try Evd.add_global_univ sigma u with UGraph.AlreadyDeclared -> sigma), u + | GLocalUniv l -> universe_level_name sigma l -let interp_sort_info ?loc evd l = +let sort_info ?loc evd l = List.fold_left (fun (evd, u) (l,n) -> - let evd', u' = interp_sort_name evd l in + let evd', u' = sort_name evd l in let u' = Univ.Universe.make u' in let u' = match n with | 0 -> u' | 1 -> Univ.Universe.super u' | n -> - user_err ?loc ~hdr:"interp_universe" + user_err ?loc ~hdr:"sort_info" (Pp.(str "Cannot interpret universe increment +" ++ int n)) in (evd', Univ.sup u u')) (evd, Univ.Universe.type0m) l @@ -393,24 +372,33 @@ let pretype_id pretype loc env sigma id = (*************************************************************************) (* Main pretyping function *) -let interp_known_glob_level ?loc evd = function +let known_universe_level_name evd lid = + try Evd.universe_of_name evd lid.CAst.v + with Not_found -> + let u = Nametab.locate_universe (Libnames.qualid_of_lident lid) in + Univ.Level.make u + +let known_glob_level evd = function | GSProp -> Univ.Level.sprop | GProp -> Univ.Level.prop | GSet -> Univ.Level.set - | GType qid -> - try interp_known_universe_level_name evd qid + | GUniv u -> u + | GRawUniv u -> anomaly Pp.(str "Raw universe in known_glob_level.") + | GLocalUniv lid -> + try known_universe_level_name evd lid with Not_found -> - user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid) + user_err ?loc:lid.CAst.loc ~hdr:"known_level_info" + (str "Undeclared universe " ++ Id.print lid.CAst.v) -let interp_glob_level ?loc evd : glob_level -> _ = function +let glob_level ?loc evd : glob_level -> _ = function | UAnonymous {rigid} -> new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd - | UNamed s -> interp_sort_name evd s + | UNamed s -> sort_name evd s -let interp_instance ?loc evd l = +let instance ?loc evd l = let evd, l' = List.fold_left (fun (evd, univs) l -> - let evd, l = interp_glob_level ?loc evd l in + let evd, l = glob_level ?loc evd l in (evd, l :: univs)) (evd, []) l in @@ -424,7 +412,7 @@ let pretype_global ?loc rigid env evd gr us = let evd, instance = match us with | None -> evd, None - | Some l -> interp_instance ?loc evd l + | Some l -> instance ?loc evd l in Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr @@ -451,11 +439,11 @@ let pretype_ref ?loc sigma env ref us = let sigma, ty = type_of !!env sigma c in sigma, make_judge c ty -let interp_sort ?loc evd : glob_sort -> _ = function +let sort ?loc evd : glob_sort -> _ = function | UAnonymous {rigid} -> let evd, l = new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd in evd, Univ.Universe.make l - | UNamed l -> interp_sort_info ?loc evd l + | UNamed l -> sort_info ?loc evd l let judge_of_sort ?loc evd s = let judge = @@ -469,7 +457,7 @@ let pretype_sort ?loc sigma s = | UNamed [GProp,0] -> sigma, judge_of_prop | UNamed [GSet,0] -> sigma, judge_of_set | _ -> - let sigma, s = interp_sort ?loc sigma s in + let sigma, s = sort ?loc sigma s in judge_of_sort ?loc sigma s let new_type_evar env sigma loc = diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 7bb4a6e273..5668098fe6 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -30,8 +30,7 @@ val get_bidirectionality_hint : GlobRef.t -> int option val clear_bidirectionality_hint : GlobRef.t -> unit -val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> - glob_sort_name -> Univ.Level.t +val known_glob_level : Evd.evar_map -> glob_sort_name -> Univ.Level.t (** An auxiliary function for searching for fixpoint guard indexes *) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 8942bc7805..4c410c3170 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -152,14 +152,15 @@ let tag_var = tag Tag.variable let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c) - let pr_glob_sort_name = function - | GSProp -> str "SProp" - | GProp -> str "Prop" - | GSet -> str "Set" - | GType qid -> pr_qualid qid + let pr_sort_name_expr = function + | CSProp -> str "SProp" + | CProp -> str "Prop" + | CSet -> str "Set" + | CType qid -> pr_qualid qid + | CRawType s -> Univ.Level.pr s let pr_univ_expr (u,n) = - pr_glob_sort_name u ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) + pr_sort_name_expr u ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) let pr_univ l = match l with @@ -168,21 +169,22 @@ let tag_var = tag Tag.variable let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" - let pr_glob_sort = let open Glob_term in function - | UNamed [GSProp,0] -> tag_type (str "SProp") - | UNamed [GProp,0] -> tag_type (str "Prop") - | UNamed [GSet,0] -> tag_type (str "Set") + let pr_sort_expr = function + | UNamed [CSProp,0] -> tag_type (str "SProp") + | UNamed [CProp,0] -> tag_type (str "Prop") + | UNamed [CSet,0] -> tag_type (str "Set") | UAnonymous {rigid=true} -> tag_type (str "Type") | UAnonymous {rigid=false} -> tag_type (str "Type") ++ pr_univ_annot (fun _ -> str "_") () | UNamed u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u) - let pr_glob_level = let open Glob_term in function - | UNamed GSProp -> tag_type (str "SProp") - | UNamed GProp -> tag_type (str "Prop") - | UNamed GSet -> tag_type (str "Set") + let pr_univ_level_expr = function + | UNamed CSProp -> tag_type (str "SProp") + | UNamed CProp -> tag_type (str "Prop") + | UNamed CSet -> tag_type (str "Set") | UAnonymous {rigid=true} -> tag_type (str "Type") | UAnonymous {rigid=false} -> tag_type (str "_") - | UNamed (GType u) -> tag_type (pr_qualid u) + | UNamed (CType u) -> tag_type (pr_qualid u) + | UNamed (CRawType s) -> tag_type (Univ.Level.pr s) let pr_qualid sp = let (sl, id) = repr_qualid sp in @@ -200,7 +202,7 @@ let tag_var = tag Tag.variable let pr_patvar = pr_id let pr_universe_instance l = - pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_level)) l + pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_univ_level_expr)) l let pr_reference qid = if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid) @@ -664,7 +666,7 @@ let tag_var = tag Tag.variable | CPatVar p -> return (str "@?" ++ pr_patvar p, latom) | CSort s -> - return (pr_glob_sort s, latom) + return (pr_sort_expr s, latom) | CCast (a,b) -> return ( hv 0 (pr mt (LevelLt lcast) a ++ spc () ++ @@ -717,7 +719,7 @@ let tag_var = tag Tag.variable let transf env sigma c = if !Flags.beautify_file then let r = Constrintern.for_grammar (Constrintern.intern_constr env sigma) c in - Constrextern.extern_glob_constr (Termops.vars_of_env env) r + Constrextern.(extern_glob_constr (extern_env env sigma)) r else c let pr_expr env sigma prec c = diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 02e04573f8..d66b77efb2 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -32,9 +32,9 @@ val pr_id : Id.t -> Pp.t val pr_qualid : qualid -> Pp.t val pr_patvar : Pattern.patvar -> Pp.t -val pr_glob_sort_name : Glob_term.glob_sort_name -> Pp.t -val pr_glob_level : Glob_term.glob_level -> Pp.t -val pr_glob_sort : Glob_term.glob_sort -> Pp.t +val pr_sort_name_expr : sort_name_expr -> Pp.t +val pr_univ_level_expr : univ_level_expr -> Pp.t +val pr_sort_expr : sort_expr -> Pp.t val pr_guard_annot : (constr_expr -> Pp.t) -> local_binder_expr list diff --git a/printing/printer.ml b/printing/printer.ml index ea718526de..1425cebafc 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -97,10 +97,10 @@ let pr_ltype_env ?lax ?goal_concl_style env sigma ?impargs c = let pr_ljudge_env env sigma j = (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) -let pr_lglob_constr_env env c = - pr_lconstr_expr env (Evd.from_env env) (extern_glob_constr (Termops.vars_of_env env) c) -let pr_glob_constr_env env c = - pr_constr_expr env (Evd.from_env env) (extern_glob_constr (Termops.vars_of_env env) c) +let pr_lglob_constr_env env sigma c = + pr_lconstr_expr env sigma (extern_glob_constr (extern_env env sigma) c) +let pr_glob_constr_env env sigma c = + pr_constr_expr env sigma (extern_glob_constr (extern_env env sigma) c) let pr_closed_glob_n_env ?lax ?goal_concl_style ?inctx ?scope env sigma n c = pr_constr_expr_n env sigma n (extern_closed_glob ?lax ?goal_concl_style ?inctx ?scope env sigma c) @@ -115,7 +115,7 @@ let pr_constr_pattern_env env sigma c = let pr_cases_pattern t = pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t) -let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) +let pr_sort sigma s = pr_sort_expr (extern_sort sigma s) let () = Termops.Internal.set_print_constr (fun env sigma t -> pr_lconstr_expr env sigma (extern_constr ~lax:true env sigma t)) diff --git a/printing/printer.mli b/printing/printer.mli index ea388ae57e..732af5570d 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -107,9 +107,9 @@ val pr_closed_glob_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t -val pr_lglob_constr_env : env -> 'a glob_constr_g -> Pp.t +val pr_lglob_constr_env : env -> evar_map -> 'a glob_constr_g -> Pp.t -val pr_glob_constr_env : env -> 'a glob_constr_g -> Pp.t +val pr_glob_constr_env : env -> evar_map -> 'a glob_constr_g -> Pp.t val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t diff --git a/tactics/declareUctx.ml b/tactics/declareUctx.ml index 3f67ff20a4..bca43697cb 100644 --- a/tactics/declareUctx.ml +++ b/tactics/declareUctx.ml @@ -16,7 +16,7 @@ let name_instance inst = assert false | Some na -> try - let qid = Nametab.shortest_qualid_of_universe na in + let qid = Nametab.shortest_qualid_of_universe Names.Id.Set.empty na in Names.Name (Libnames.qualid_basename qid) with Not_found -> (* Best-effort naming from the string representation of the level. diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg index ba0bcb1b3c..0f843b3b14 100644 --- a/test-suite/misc/quotation_token/src/quotation.mlg +++ b/test-suite/misc/quotation_token/src/quotation.mlg @@ -7,6 +7,6 @@ GRAMMAR EXTEND Gram term: LEVEL "0" [ [ s = QUOTATION "foobar:" -> { - CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ] + CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [CProp,0])) } ] ] ; END diff --git a/test-suite/misc/side-eff-leak-univs/src/evil.mlg b/test-suite/misc/side-eff-leak-univs/src/evil.mlg index d89ab887a8..bb6eaff409 100644 --- a/test-suite/misc/side-eff-leak-univs/src/evil.mlg +++ b/test-suite/misc/side-eff-leak-univs/src/evil.mlg @@ -7,7 +7,7 @@ open Stdarg TACTIC EXTEND magic | [ "magic" ident(i) ident(j) ] -> { - let open Glob_term in - DeclareUniv.do_constraint ~poly:false [ GType (Libnames.qualid_of_ident i), Univ.Lt, GType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT() + let open Constrexpr in + DeclareUniv.do_constraint ~poly:false [ CType (Libnames.qualid_of_ident i), Univ.Lt, CType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT() } END diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 5d49d1635c..01b1025da1 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1100,7 +1100,7 @@ let interp_constr flags ist c = let () = let intern = intern_constr in let interp ist c = interp_constr constr_flags ist c in - let print env c = str "constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in + let print env sigma c = str "constr:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in let obj = { ml_intern = intern; @@ -1113,7 +1113,7 @@ let () = let () = let intern = intern_constr in let interp ist c = interp_constr open_constr_no_classes_flags ist c in - let print env c = str "open_constr:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in + let print env sigma c = str "open_constr:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in let obj = { ml_intern = intern; @@ -1125,7 +1125,7 @@ let () = let () = let interp _ id = return (Value.of_ident id) in - let print _ id = str "ident:(" ++ Id.print id ++ str ")" in + let print _ _ id = str "ident:(" ++ Id.print id ++ str ")" in let obj = { ml_intern = (fun _ _ id -> GlbVal id, gtypref t_ident); ml_interp = interp; @@ -1147,7 +1147,7 @@ let () = let sigma = Evd.from_env env in Patternops.subst_pattern env sigma subst c in - let print env pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env Evd.empty pat ++ str ")" in + let print env sigma pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env sigma pat ++ str ")" in let interp _ c = return (Value.of_pattern c) in let obj = { ml_intern = intern; @@ -1169,7 +1169,7 @@ let () = return (Value.of_ext val_preterm c) in let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in - let print env c = str "preterm:(" ++ Printer.pr_lglob_constr_env env c ++ str ")" in + let print env sigma c = str "preterm:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in let obj = { ml_intern = (fun _ _ e -> Empty.abort e); ml_interp = interp; @@ -1193,7 +1193,7 @@ let () = in let subst s c = Globnames.subst_global_reference s c in let interp _ gr = return (Value.of_reference gr) in - let print _ = function + let print _ _ = function | GlobRef.VarRef id -> str "reference:(" ++ str "&" ++ Id.print id ++ str ")" | r -> str "reference:(" ++ Printer.pr_global r ++ str ")" in @@ -1241,7 +1241,7 @@ let () = return (Tac2ffi.of_closure (Tac2ffi.abstract len clos)) in let subst s (ids, tac) = (ids, Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac) in - let print env (ids, tac) = + let print env sigma (ids, tac) = let ids = if List.is_empty ids then mt () else pr_sequence Id.print ids ++ spc () ++ str "|-" ++ spc () @@ -1290,7 +1290,7 @@ let () = return (Tac2ffi.of_closure (Tac2ffi.abstract len clos)) in let subst s (ids, tac) = (ids, Genintern.substitute Tacarg.wit_tactic s tac) in - let print env (ids, tac) = + let print env sigma (ids, tac) = let ids = if List.is_empty ids then mt () else pr_sequence Id.print ids ++ str " |- " diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index eebd6635fa..d0655890a7 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -853,8 +853,10 @@ let pr_frame = function str "Prim <" ++ str ml.mltac_plugin ++ str ":" ++ str ml.mltac_tactic ++ str ">" | FrExtn (tag, arg) -> let obj = Tac2env.interp_ml_object tag in + let env = Global.env () in + let sigma = Evd.from_env env in str "Extn " ++ str (Tac2dyn.Arg.repr tag) ++ str ":" ++ spc () ++ - obj.Tac2env.ml_print (Global.env ()) arg + obj.Tac2env.ml_print env sigma arg let () = register_handler begin function | Tac2interp.LtacError (kn, args) -> diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml index 6c2133f8f2..f6d07e484b 100644 --- a/user-contrib/Ltac2/tac2env.ml +++ b/user-contrib/Ltac2/tac2env.ml @@ -253,7 +253,7 @@ type ('a, 'b) ml_object = { ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun; ml_subst : Mod_subst.substitution -> 'b -> 'b; ml_interp : environment -> 'b -> valexpr Proofview.tactic; - ml_print : Environ.env -> 'b -> Pp.t; + ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t; } module MLTypeObj = diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli index 2468959810..af1197c24c 100644 --- a/user-contrib/Ltac2/tac2env.mli +++ b/user-contrib/Ltac2/tac2env.mli @@ -122,7 +122,7 @@ type ('a, 'b) ml_object = { ml_intern : 'r. (raw_tacexpr, glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun; ml_subst : Mod_subst.substitution -> 'b -> 'b; ml_interp : environment -> 'b -> valexpr Proofview.tactic; - ml_print : Environ.env -> 'b -> Pp.t; + ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t; } val define_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object -> unit diff --git a/user-contrib/Ltac2/tac2print.ml b/user-contrib/Ltac2/tac2print.ml index a37fe2f7a5..fe62de1fb3 100644 --- a/user-contrib/Ltac2/tac2print.ml +++ b/user-contrib/Ltac2/tac2print.ml @@ -274,7 +274,9 @@ let pr_glbexpr_gen lvl c = paren (hov 0 (c ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl))) | GTacExt (tag, arg) -> let tpe = interp_ml_object tag in - hov 0 (tpe.ml_print (Global.env ()) arg) (* FIXME *) + let env = Global.env() in + let sigma = Evd.from_env env in + hov 0 (tpe.ml_print env sigma arg) (* FIXME *) | GTacPrm (prm, args) -> let args = match args with | [] -> mt () diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml index 1705915e70..1987d48e0f 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -109,9 +109,8 @@ let do_universe ~poly l = let do_constraint ~poly l = let open Univ in - let u_of_id x = - Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x - in + let evd = Evd.from_env (Global.env ()) in + let u_of_id x = Constrintern.interp_known_level evd x in let constraints = List.fold_left (fun acc (l, d, r) -> let lu = u_of_id l and ru = u_of_id r in Constraint.add (lu, d, ru) acc) diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli index e4d1d5dc65..ca990a58eb 100644 --- a/vernac/declareUniv.mli +++ b/vernac/declareUniv.mli @@ -17,4 +17,4 @@ exception AlreadyDeclared of (string option * Id.t) val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit val do_universe : poly:bool -> lident list -> unit -val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit +val do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 9d86ea90e6..f35c77ec3b 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -961,7 +961,7 @@ let explain_not_match_error = function status (not b) ++ str" declaration was found" | IncompatibleUniverses incon -> str"the universe constraints are inconsistent: " ++ - Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon + Univ.explain_universe_inconsistency UnivNames.(pr_with_global_universes empty_binders) incon | IncompatiblePolymorphism (env, t1, t2) -> str "conversion of polymorphic values generates additional constraints: " ++ quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t1) ++ spc () ++ @@ -1218,7 +1218,7 @@ let error_large_non_prop_inductive_not_in_type () = str "Large non-propositional inductive types must be in Type." let error_inductive_missing_constraints (us,ind_univ) = - let pr_u = Univ.Universe.pr_with UnivNames.pr_with_global_universes in + let pr_u = Univ.Universe.pr_with UnivNames.(pr_with_global_universes empty_binders) in str "Missing universe constraint declared for inductive type:" ++ spc() ++ v 0 (prlist_with_sep spc (fun u -> hov 0 (pr_u u ++ str " <= " ++ pr_u ind_univ)) @@ -1406,7 +1406,7 @@ let _ = CErrors.register_handler (wrap_unhandled explain_exn_default) let rec vernac_interp_error_handler = function | Univ.UniverseInconsistency i -> str "Universe inconsistency." ++ spc() ++ - Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i ++ str "." + Univ.explain_universe_inconsistency UnivNames.(pr_with_global_universes empty_binders) i ++ str "." | TypeError(ctx,te) -> let te = map_ptype_error EConstr.of_constr te in explain_type_error ctx Evd.empty te diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 01873918aa..ff4365c8d3 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -60,8 +60,8 @@ let pr_red_expr = keyword let pr_uconstraint (l, d, r) = - pr_glob_sort_name l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ - pr_glob_sort_name r + pr_sort_name_expr l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ + pr_sort_name_expr r let pr_univ_name_list = function | None -> mt () diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 840754ccc6..0fc6c7f87b 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -206,7 +206,7 @@ let print_if_is_coercion ref = let pr_template_variables = function | [] -> mt () - | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars + | vars -> str "on " ++ prlist_with_sep spc UnivNames.(pr_with_global_universes empty_binders) vars let print_polymorphism ref = let poly = Global.is_polymorphic ref in @@ -668,7 +668,7 @@ let gallina_print_syntactic_def env kn = spc () ++ str ":=") ++ spc () ++ Constrextern.without_specific_symbols - [Notation.SynDefRule kn] (pr_glob_constr_env env) c) + [Notation.SynDefRule kn] (pr_glob_constr_env env (Evd.from_env env)) c) module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> Pp.t option end) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0f63dfe5ce..57b264bbc2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -353,9 +353,9 @@ let universe_subgraph ?loc kept univ = let open Univ in let sigma = Evd.from_env (Global.env()) in let parse q = - let q = Glob_term.(GType q) in + let q = Constrexpr.CType q in (* this function has a nice error message for not found univs *) - Pretyping.interp_known_glob_level ?loc sigma q + Constrintern.interp_known_level sigma q in let kept = List.fold_left (fun kept q -> LSet.add (parse q) kept) LSet.empty kept in let csts = UGraph.constraints_for ~kept univ in @@ -377,7 +377,7 @@ let print_universes ?loc ~sort ~subgraph dst = if Global.is_joined_environment () then mt () else str"There may remain asynchronous universe constraints" in - let prl = UnivNames.pr_with_global_universes in + let prl = UnivNames.(pr_with_global_universes empty_binders) in begin match dst with | None -> UGraph.pr_universes prl univ ++ pr_remaining | Some s -> dump_universes_gen (fun u -> Pp.string_of_ppcmds (prl u)) univ s @@ -1829,11 +1829,11 @@ let vernac_print ~pstate = | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s | PrintHintDb -> Hints.pr_searchtable env sigma | PrintScopes -> - Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env)) + Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env sigma)) | PrintScope s -> - Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env)) s + Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env sigma)) s | PrintVisibility s -> - Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env)) s + Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env sigma)) s | PrintAbout (ref_or_by_not,udecl,glnumopt) -> print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt | PrintImplicit qid -> @@ -1867,9 +1867,9 @@ let vernac_locate ~pstate = let open Constrexpr in function | LocateTerm {v=AN qid} -> Prettyp.print_located_term qid | LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *) | LocateTerm {v=ByNotation (ntn, sc)} -> - let _, env = get_current_or_global_context ~pstate in + let sigma, env = get_current_or_global_context ~pstate in Notation.locate_notation - (Constrextern.without_symbols (pr_glob_constr_env env)) ntn sc + (Constrextern.without_symbols (pr_glob_constr_env env sigma)) ntn sc | LocateLibrary qid -> print_located_library qid | LocateModule qid -> Prettyp.print_located_module qid | LocateOther (s, qid) -> Prettyp.print_located_other s qid diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 89c09bb169..2e360cf969 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -339,7 +339,7 @@ type nonrec vernac_expr = | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list - | VernacConstraint of Glob_term.glob_constraint list + | VernacConstraint of univ_constraint_expr list (* Gallina extensions *) | VernacBeginSection of lident |