diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-09-26 23:57:40 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-26 23:57:40 +0200 |
commit | b9740771e8113cb9e607793887be7a12587d0326 (patch) | |
tree | f69105ad9813738abd10ae824756947940a7dc6d /pretyping | |
parent | 4b6383889d4d38de4c9a28bee960b30114a51b16 (diff) | |
parent | 3c964a60d698134c21adc77cbb69ce1528350682 (diff) |
Merge PR #688: Binding universe constraints in Definition/Inductive/etc...
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/pretyping.mllib | 1 | ||||
-rw-r--r-- | pretyping/univdecls.ml | 64 | ||||
-rw-r--r-- | pretyping/univdecls.mli | 19 |
3 files changed, 84 insertions, 0 deletions
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index c8b3307d7..d04dcb8e3 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -29,3 +29,4 @@ Indrec Cases Pretyping Unification +Univdecls diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml new file mode 100644 index 000000000..d7c42d03a --- /dev/null +++ b/pretyping/univdecls.ml @@ -0,0 +1,64 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Nameops +open CErrors +open Pp + +(** Local universes and constraints declarations *) +type universe_decl = + (Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +let default_univ_decl = + let open Misctypes in + { univdecl_instance = []; + univdecl_extensible_instance = true; + univdecl_constraints = Univ.Constraint.empty; + univdecl_extensible_constraints = true } + +let interp_univ_constraints env evd cstrs = + let open Misctypes in + let u_of_id x = + match x with + | Misctypes.GProp -> Loc.tag Univ.Level.prop + | GSet -> Loc.tag Univ.Level.set + | GType None | GType (Some (_, Anonymous)) -> + user_err ~hdr:"interp_constraint" + (str "Cannot declare constraints on anonymous universes") + | GType (Some (loc, Name id)) -> + try loc, Evd.universe_of_name evd (Id.to_string id) + with Not_found -> + user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ pr_id id) + in + let interp (evd,cstrs) (u, d, u') = + let lloc, ul = u_of_id u and rloc, u'l = u_of_id 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 + evd, cstrs' + with Univ.UniverseInconsistency e -> + user_err ~hdr:"interp_constraint" (str "Universe inconsistency" (* TODO *)) + in + List.fold_left interp (evd,Univ.Constraint.empty) cstrs + +let interp_univ_decl env decl = + let open Misctypes in + let pl = decl.univdecl_instance in + let evd = Evd.from_ctx (Evd.make_evar_universe_context env (Some pl)) in + let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in + let decl = { univdecl_instance = pl; + univdecl_extensible_instance = decl.univdecl_extensible_instance; + univdecl_constraints = cstrs; + univdecl_extensible_constraints = decl.univdecl_extensible_constraints } + in evd, decl + +let interp_univ_decl_opt env l = + match l with + | None -> Evd.from_env env, default_univ_decl + | Some decl -> interp_univ_decl env decl diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli new file mode 100644 index 000000000..0c3b749cb --- /dev/null +++ b/pretyping/univdecls.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Local universe and constraint declarations. *) +type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +val default_univ_decl : universe_decl + +val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr -> + Evd.evar_map * universe_decl + +val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option -> + Evd.evar_map * universe_decl |