From a42795cc1c2a8ed3efa9960af920ff7b16d928f0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 1 Sep 2016 17:52:44 +0200 Subject: Introducing a new EConstr.t type to perform the nf_evar operation on demand. --- engine/eConstr.mli | 183 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 183 insertions(+) create mode 100644 engine/eConstr.mli (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli new file mode 100644 index 0000000000..03e2d4ffcc --- /dev/null +++ b/engine/eConstr.mli @@ -0,0 +1,183 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t -> (t, t) Constr.kind_of_term +(** Same as {!Constr.kind} except that it expands evars and normalizes + universes on the fly. *) + +val to_constr : Evd.evar_map -> t -> Constr.t +(** Returns the evar-normal form of the argument. See {!Evarutil.nf_evar}. *) + +(** {5 Constructors} *) + +val of_kind : (t, t) Constr.kind_of_term -> t +(** Construct a term from a view. *) + +val of_constr : Constr.t -> t +(** Translate a kernel term into an incomplete term in O(1). *) + +(** {5 Insensitive primitives} + + Evar-insensitive versions of the corresponding functions. See the {!Constr} + module for more information. + +*) + +(** {6 Constructors} *) + +val mkRel : int -> t +val mkVar : Id.t -> t +val mkMeta : metavariable -> t +val mkEvar : t pexistential -> t +val mkSort : Sorts.t -> t +val mkProp : t +val mkSet : t +val mkType : Univ.universe -> t +val mkCast : t * cast_kind * t -> t +val mkProd : Name.t * t * t -> t +val mkLambda : Name.t * t * t -> t +val mkLetIn : Name.t * t * t * t -> t +val mkApp : t * t array -> t +(* val mkConst : constant -> t *) +val mkConstU : pconstant -> t +val mkProj : (projection * t) -> t +(* val mkInd : inductive -> t *) +val mkIndU : pinductive -> t +(* val mkConstruct : constructor -> t *) +val mkConstructU : pconstructor -> t +(* val mkConstructUi : pinductive * int -> t *) +val mkCase : case_info * t * t * t array -> t +val mkFix : (t, t) pfixpoint -> t +val mkCoFix : (t, t) pcofixpoint -> t + +val applist : t * t list -> t + +val mkProd_or_LetIn : Rel.Declaration.t -> t -> t +val mkLambda_or_LetIn : Rel.Declaration.t -> t -> t +val it_mkProd_or_LetIn : t -> Rel.t -> t +val it_mkLambda_or_LetIn : t -> Rel.t -> t + +(** {6 Simple case analysis} *) + +val isRel : Evd.evar_map -> t -> bool +val isVar : Evd.evar_map -> t -> bool +val isInd : Evd.evar_map -> t -> bool +val isEvar : Evd.evar_map -> t -> bool +val isMeta : Evd.evar_map -> t -> bool +val isSort : Evd.evar_map -> t -> bool +val isCast : Evd.evar_map -> t -> bool +val isApp : Evd.evar_map -> t -> bool +val isLambda : Evd.evar_map -> t -> bool +val isLetIn : Evd.evar_map -> t -> bool +val isProd : Evd.evar_map -> t -> bool +val isConst : Evd.evar_map -> t -> bool +val isConstruct : Evd.evar_map -> t -> bool +val isFix : Evd.evar_map -> t -> bool +val isCoFix : Evd.evar_map -> t -> bool +val isCase : Evd.evar_map -> t -> bool +val isProj : Evd.evar_map -> t -> bool +val isArity : Evd.evar_map -> t -> bool +val isVarId : Evd.evar_map -> Id.t -> t -> bool + +val destRel : Evd.evar_map -> t -> int +val destMeta : Evd.evar_map -> t -> metavariable +val destVar : Evd.evar_map -> t -> Id.t +val destSort : Evd.evar_map -> t -> Sorts.t +val destCast : Evd.evar_map -> t -> t * cast_kind * t +val destProd : Evd.evar_map -> t -> Name.t * types * types +val destLambda : Evd.evar_map -> t -> Name.t * types * t +val destLetIn : Evd.evar_map -> t -> Name.t * t * types * t +val destApp : Evd.evar_map -> t -> t * t array +val destConst : Evd.evar_map -> t -> constant puniverses +val destEvar : Evd.evar_map -> t -> t pexistential +val destInd : Evd.evar_map -> t -> inductive puniverses +val destConstruct : Evd.evar_map -> t -> constructor puniverses +val destCase : Evd.evar_map -> t -> case_info * t * t * t array +val destProj : Evd.evar_map -> t -> projection * t +val destFix : Evd.evar_map -> t -> (t, t) pfixpoint +val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint + +val decompose_app : Evd.evar_map -> t -> t * t list + +val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t +val decompose_lam_assum : Evd.evar_map -> t -> Context.Rel.t * t +val decompose_lam_n_assum : Evd.evar_map -> int -> t -> Context.Rel.t * t +val decompose_lam_n_decls : Evd.evar_map -> int -> t -> Context.Rel.t * t + +val decompose_prod : Evd.evar_map -> t -> (Name.t * t) list * t +val decompose_prod_assum : Evd.evar_map -> t -> Context.Rel.t * t +val decompose_prod_n_assum : Evd.evar_map -> int -> t -> Context.Rel.t * t + +val existential_type : Evd.evar_map -> existential -> types + +(** {6 Equality} *) + +val eq_constr : Evd.evar_map -> t -> t -> bool +val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool +val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option +val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option +val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.universe_constraints option + +(** {6 Iterators} *) + +val map : Evd.evar_map -> (t -> t) -> t -> t +val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t +val iter : Evd.evar_map -> (t -> unit) -> t -> unit +val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit +val iter_with_full_binders : Evd.evar_map -> (Rel.Declaration.t -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit +val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a + +(** {6 Substitutions} *) + +module Vars : +sig +val lift : int -> t -> t +val liftn : int -> int -> t -> t +val substnl : t list -> int -> t -> t +val substl : t list -> t -> t +val subst1 : t -> t -> t + +val replace_vars : (Id.t * t) list -> t -> t +val substn_vars : int -> Id.t list -> t -> t +val subst_vars : Id.t list -> t -> t +val subst_var : Id.t -> t -> t + +val noccurn : Evd.evar_map -> int -> t -> bool +val noccur_between : Evd.evar_map -> int -> int -> t -> bool + +val closedn : Evd.evar_map -> int -> t -> bool +val closed0 : Evd.evar_map -> t -> bool +end + +(** {5 Unsafe operations} *) + +module Unsafe : +sig + val to_constr : t -> Constr.t + (** Physical identity. Does not care for defined evars. *) + + val eq : (t, Constr.t) eq + (** Use for transparent cast between types. *) +end -- cgit v1.2.3 From ca993b9e7765ac58f70740818758457c9367b0da Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 00:29:02 +0100 Subject: Making judgment type generic over the type of inner constrs. This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules. --- engine/eConstr.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 03e2d4ffcc..10eb064a3c 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -20,6 +20,8 @@ type constr = t type existential = t pexistential type fixpoint = (t, t) pfixpoint type cofixpoint = (t, t) pcofixpoint +type unsafe_judgment = (constr, types) Environ.punsafe_judgment +type unsafe_type_judgment = types Environ.punsafe_type_judgment (** {5 Destructors} *) -- cgit v1.2.3 From 0489e8b56d7e10f7111c0171960e25d32201b963 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 21:55:33 +0100 Subject: Clenv API using EConstr. --- engine/eConstr.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 10eb064a3c..e4136a6122 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -171,6 +171,9 @@ val noccur_between : Evd.evar_map -> int -> int -> t -> bool val closedn : Evd.evar_map -> int -> t -> bool val closed0 : Evd.evar_map -> t -> bool + +val subst_univs_level_constr : Univ.universe_level_subst -> t -> t + end (** {5 Unsafe operations} *) -- cgit v1.2.3 From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 13 Nov 2016 20:38:41 +0100 Subject: Tactics API using EConstr. --- engine/eConstr.mli | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e4136a6122..15463a8f68 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -73,6 +73,7 @@ val mkConstructU : pconstructor -> t val mkCase : case_info * t * t * t array -> t val mkFix : (t, t) pfixpoint -> t val mkCoFix : (t, t) pcofixpoint -> t +val mkArrow : t -> t -> t val applist : t * t list -> t @@ -81,6 +82,12 @@ val mkLambda_or_LetIn : Rel.Declaration.t -> t -> t val it_mkProd_or_LetIn : t -> Rel.t -> t val it_mkLambda_or_LetIn : t -> Rel.t -> t +val mkNamedLambda : Id.t -> types -> constr -> constr +val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr +val mkNamedProd : Id.t -> types -> types -> types +val mkNamedLambda_or_LetIn : Named.Declaration.t -> types -> types +val mkNamedProd_or_LetIn : Named.Declaration.t -> types -> types + (** {6 Simple case analysis} *) val isRel : Evd.evar_map -> t -> bool @@ -141,6 +148,7 @@ val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool val eq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.universe_constraints option +val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool (** {6 Iterators} *) -- cgit v1.2.3 From 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Nov 2016 20:35:01 +0100 Subject: Equality API using EConstr. --- engine/eConstr.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 15463a8f68..e6270fa78f 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -62,12 +62,12 @@ val mkProd : Name.t * t * t -> t val mkLambda : Name.t * t * t -> t val mkLetIn : Name.t * t * t * t -> t val mkApp : t * t array -> t -(* val mkConst : constant -> t *) +val mkConst : constant -> t val mkConstU : pconstant -> t val mkProj : (projection * t) -> t -(* val mkInd : inductive -> t *) +val mkInd : inductive -> t val mkIndU : pinductive -> t -(* val mkConstruct : constructor -> t *) +val mkConstruct : constructor -> t val mkConstructU : pconstructor -> t (* val mkConstructUi : pinductive * int -> t *) val mkCase : case_info * t * t * t array -> t -- cgit v1.2.3 From 118ae18590dbc7d01cf34e0cd6133b1e34ef9090 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Nov 2016 00:20:30 +0100 Subject: Contradiction API using EConstr. --- engine/eConstr.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e6270fa78f..cb671154c6 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -69,7 +69,7 @@ val mkInd : inductive -> t val mkIndU : pinductive -> t val mkConstruct : constructor -> t val mkConstructU : pconstructor -> t -(* val mkConstructUi : pinductive * int -> t *) +val mkConstructUi : pinductive * int -> t val mkCase : case_info * t * t * t array -> t val mkFix : (t, t) pfixpoint -> t val mkCoFix : (t, t) pcofixpoint -> t -- cgit v1.2.3 From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- engine/eConstr.mli | 48 ++++++++++++++++++++++++++++++++++++------------ 1 file changed, 36 insertions(+), 12 deletions(-) (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli index cb671154c6..d6b2113d2c 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -10,6 +10,7 @@ open CSig open Names open Constr open Context +open Environ type t (** Type of incomplete terms. Essentially a wrapper around {!Constr.t} ensuring @@ -22,6 +23,10 @@ type fixpoint = (t, t) pfixpoint type cofixpoint = (t, t) pcofixpoint type unsafe_judgment = (constr, types) Environ.punsafe_judgment type unsafe_type_judgment = types Environ.punsafe_type_judgment +type named_declaration = (constr, types) Context.Named.Declaration.pt +type rel_declaration = (constr, types) Context.Rel.Declaration.pt +type named_context = (constr, types) Context.Named.pt +type rel_context = (constr, types) Context.Rel.pt (** {5 Destructors} *) @@ -77,16 +82,16 @@ val mkArrow : t -> t -> t val applist : t * t list -> t -val mkProd_or_LetIn : Rel.Declaration.t -> t -> t -val mkLambda_or_LetIn : Rel.Declaration.t -> t -> t -val it_mkProd_or_LetIn : t -> Rel.t -> t -val it_mkLambda_or_LetIn : t -> Rel.t -> t +val mkProd_or_LetIn : rel_declaration -> t -> t +val mkLambda_or_LetIn : rel_declaration -> t -> t +val it_mkProd_or_LetIn : t -> rel_context -> t +val it_mkLambda_or_LetIn : t -> rel_context -> t val mkNamedLambda : Id.t -> types -> constr -> constr val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr val mkNamedProd : Id.t -> types -> types -> types -val mkNamedLambda_or_LetIn : Named.Declaration.t -> types -> types -val mkNamedProd_or_LetIn : Named.Declaration.t -> types -> types +val mkNamedLambda_or_LetIn : named_declaration -> types -> types +val mkNamedProd_or_LetIn : named_declaration -> types -> types (** {6 Simple case analysis} *) @@ -131,13 +136,13 @@ val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint val decompose_app : Evd.evar_map -> t -> t * t list val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t -val decompose_lam_assum : Evd.evar_map -> t -> Context.Rel.t * t -val decompose_lam_n_assum : Evd.evar_map -> int -> t -> Context.Rel.t * t -val decompose_lam_n_decls : Evd.evar_map -> int -> t -> Context.Rel.t * t +val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t +val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t +val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t val decompose_prod : Evd.evar_map -> t -> (Name.t * t) list * t -val decompose_prod_assum : Evd.evar_map -> t -> Context.Rel.t * t -val decompose_prod_n_assum : Evd.evar_map -> int -> t -> Context.Rel.t * t +val decompose_prod_assum : Evd.evar_map -> t -> rel_context * t +val decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t val existential_type : Evd.evar_map -> existential -> types @@ -156,7 +161,7 @@ val map : Evd.evar_map -> (t -> t) -> t -> t val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t val iter : Evd.evar_map -> (t -> unit) -> t -> unit val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit -val iter_with_full_binders : Evd.evar_map -> (Rel.Declaration.t -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit +val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a (** {6 Substitutions} *) @@ -184,6 +189,25 @@ val subst_univs_level_constr : Univ.universe_level_subst -> t -> t end +(** {5 Environment handling} *) + +val push_rel : rel_declaration -> env -> env +val push_rel_context : rel_context -> env -> env + +val push_named : named_declaration -> env -> env +val push_named_context : named_context -> env -> env +val push_named_context_val : named_declaration -> named_context_val -> named_context_val + +val rel_context : env -> rel_context +val named_context : env -> named_context + +val val_of_named_context : named_context -> named_context_val +val named_context_of_val : named_context_val -> named_context + +val lookup_rel : int -> env -> rel_declaration +val lookup_named : variable -> env -> named_declaration +val lookup_named_val : variable -> named_context_val -> named_declaration + (** {5 Unsafe operations} *) module Unsafe : -- cgit v1.2.3 From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Nov 2016 00:41:31 +0100 Subject: Namegen primitives now apply on evar constrs. Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough. --- engine/eConstr.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli index d6b2113d2c..83536d6f8a 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -114,6 +114,7 @@ val isCase : Evd.evar_map -> t -> bool val isProj : Evd.evar_map -> t -> bool val isArity : Evd.evar_map -> t -> bool val isVarId : Evd.evar_map -> Id.t -> t -> bool +val isRelN : Evd.evar_map -> int -> t -> bool val destRel : Evd.evar_map -> t -> int val destMeta : Evd.evar_map -> t -> metavariable -- cgit v1.2.3 From 4f66c854956bd05a24fd55c3d52fb669dbbb65e6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Nov 2016 15:06:42 +0100 Subject: Moving evar-normalization functions to EConstr. This removes code duplication between Evarutil and EConstr. --- engine/eConstr.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 83536d6f8a..7992c0633a 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -34,6 +34,8 @@ val kind : Evd.evar_map -> t -> (t, t) Constr.kind_of_term (** Same as {!Constr.kind} except that it expands evars and normalizes universes on the fly. *) +val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t) Constr.kind_of_term + val to_constr : Evd.evar_map -> t -> Constr.t (** Returns the evar-normal form of the argument. See {!Evarutil.nf_evar}. *) @@ -146,6 +148,7 @@ val decompose_prod_assum : Evd.evar_map -> t -> rel_context * t val decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t val existential_type : Evd.evar_map -> existential -> types +val whd_evar : Evd.evar_map -> constr -> constr (** {6 Equality} *) -- cgit v1.2.3 From 1523276aedcde1c79aff899ec87f05f3a708d13b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 9 Feb 2017 18:53:53 +0100 Subject: Missing API in EConstr. --- engine/eConstr.mli | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 7992c0633a..3b479a64d9 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -39,6 +39,8 @@ val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t) Constr.kind_of_ val to_constr : Evd.evar_map -> t -> Constr.t (** Returns the evar-normal form of the argument. See {!Evarutil.nf_evar}. *) +val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type + (** {5 Constructors} *) val of_kind : (t, t) Constr.kind_of_term -> t @@ -143,6 +145,9 @@ val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t +val compose_lam : (Name.t * t) list -> t -> t +val to_lambda : Evd.evar_map -> int -> t -> t + val decompose_prod : Evd.evar_map -> t -> (Name.t * t) list * t val decompose_prod_assum : Evd.evar_map -> t -> rel_context * t val decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t @@ -212,6 +217,16 @@ val lookup_rel : int -> env -> rel_declaration val lookup_named : variable -> env -> named_declaration val lookup_named_val : variable -> named_context_val -> named_declaration +(* XXX Missing Sigma proxy *) +val fresh_global : + ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> + 'r Sigma.t -> Globnames.global_reference -> (t, 'r) Sigma.sigma + +(** {5 Extra} *) + +val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt +val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, types) Context.Rel.Declaration.pt + (** {5 Unsafe operations} *) module Unsafe : @@ -219,6 +234,12 @@ sig val to_constr : t -> Constr.t (** Physical identity. Does not care for defined evars. *) + val to_rel_decl : (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt + (** Physical identity. Does not care for defined evars. *) + + val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt + (** Physical identity. Does not care for defined evars. *) + val eq : (t, Constr.t) eq (** Use for transparent cast between types. *) end -- cgit v1.2.3 From ce029533a1f0fc6ac9e28d162350a64446522246 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 31 Mar 2017 23:05:17 +0200 Subject: Make the Constr.kind_of_term type parametric in sorts and universes. --- engine/eConstr.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 1ae71216f1..e7287fc06c 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -30,11 +30,11 @@ type rel_context = (constr, types) Context.Rel.pt (** {5 Destructors} *) -val kind : Evd.evar_map -> t -> (t, t) Constr.kind_of_term +val kind : Evd.evar_map -> t -> (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term (** Same as {!Constr.kind} except that it expands evars and normalizes universes on the fly. *) -val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t) Constr.kind_of_term +val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, Univ.Instance.t) Constr.kind_of_term val to_constr : Evd.evar_map -> t -> Constr.t (** Returns the evar-normal form of the argument. See {!Evarutil.nf_evar}. *) @@ -43,7 +43,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type (** {5 Constructors} *) -val of_kind : (t, t) Constr.kind_of_term -> t +val of_kind : (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -> t (** Construct a term from a view. *) val of_constr : Constr.t -> t -- cgit v1.2.3 From 3df2431a80f9817ce051334cb9c3b1f465bffb60 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 31 Mar 2017 23:20:25 +0200 Subject: Actually exporting delayed universes in the EConstr implementation. For now we only normalize sorts, and we leave instances for the next commit. --- engine/eConstr.mli | 26 +++++++++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e7287fc06c..db10fbf424 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -28,9 +28,26 @@ type rel_declaration = (constr, types) Context.Rel.Declaration.pt type named_context = (constr, types) Context.Named.pt type rel_context = (constr, types) Context.Rel.pt +(** {5 Universe variables} *) + +module ESorts : +sig + type t + (** Type of sorts up-to universe unification. Essentially a wrapper around + Sorts.t so that normalization is ensured statically. *) + + val make : Sorts.t -> t + (** Turn a sort into an up-to sort. *) + + val kind : Evd.evar_map -> t -> Sorts.t + (** Returns the view into the current sort. Note that the kind of a variable + may change if the unification state of the evar map changes. *) + +end + (** {5 Destructors} *) -val kind : Evd.evar_map -> t -> (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term +val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term (** Same as {!Constr.kind} except that it expands evars and normalizes universes on the fly. *) @@ -43,7 +60,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type (** {5 Constructors} *) -val of_kind : (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -> t +val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t (** Construct a term from a view. *) val of_constr : Constr.t -> t @@ -123,7 +140,7 @@ val isRelN : Evd.evar_map -> int -> t -> bool val destRel : Evd.evar_map -> t -> int val destMeta : Evd.evar_map -> t -> metavariable val destVar : Evd.evar_map -> t -> Id.t -val destSort : Evd.evar_map -> t -> Sorts.t +val destSort : Evd.evar_map -> t -> ESorts.t val destCast : Evd.evar_map -> t -> t * cast_kind * t val destProd : Evd.evar_map -> t -> Name.t * types * types val destLambda : Evd.evar_map -> t -> Name.t * types * t @@ -242,6 +259,9 @@ sig val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt (** Physical identity. Does not care for defined evars. *) + val to_sorts : ESorts.t -> Sorts.t + (** Physical identity. Does not care for normalization. *) + val eq : (t, Constr.t) eq (** Use for transparent cast between types. *) end -- cgit v1.2.3 From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 1 Apr 2017 02:36:16 +0200 Subject: Using delayed universe instances in EConstr. The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. --- engine/eConstr.mli | 33 ++++++++++++++++++++++++--------- 1 file changed, 24 insertions(+), 9 deletions(-) (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli index db10fbf424..3a9469e55a 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -45,9 +45,21 @@ sig end +module EInstance : +sig + type t + (** Type of universe instances up-to universe unification. Similar to + {ESorts.t} for {Univ.Instance.t}. *) + + val make : Univ.Instance.t -> t + val kind : Evd.evar_map -> t -> Univ.Instance.t + val empty : t + val is_empty : t -> bool +end + (** {5 Destructors} *) -val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term +val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term (** Same as {!Constr.kind} except that it expands evars and normalizes universes on the fly. *) @@ -60,7 +72,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type (** {5 Constructors} *) -val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t +val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t (** Construct a term from a view. *) val of_constr : Constr.t -> t @@ -89,13 +101,13 @@ val mkLambda : Name.t * t * t -> t val mkLetIn : Name.t * t * t * t -> t val mkApp : t * t array -> t val mkConst : constant -> t -val mkConstU : pconstant -> t +val mkConstU : constant * EInstance.t -> t val mkProj : (projection * t) -> t val mkInd : inductive -> t -val mkIndU : pinductive -> t +val mkIndU : inductive * EInstance.t -> t val mkConstruct : constructor -> t -val mkConstructU : pconstructor -> t -val mkConstructUi : pinductive * int -> t +val mkConstructU : constructor * EInstance.t -> t +val mkConstructUi : (inductive * EInstance.t) * int -> t val mkCase : case_info * t * t * t array -> t val mkFix : (t, t) pfixpoint -> t val mkCoFix : (t, t) pcofixpoint -> t @@ -146,10 +158,10 @@ val destProd : Evd.evar_map -> t -> Name.t * types * types val destLambda : Evd.evar_map -> t -> Name.t * types * t val destLetIn : Evd.evar_map -> t -> Name.t * t * types * t val destApp : Evd.evar_map -> t -> t * t array -val destConst : Evd.evar_map -> t -> constant puniverses +val destConst : Evd.evar_map -> t -> constant * EInstance.t val destEvar : Evd.evar_map -> t -> t pexistential -val destInd : Evd.evar_map -> t -> inductive puniverses -val destConstruct : Evd.evar_map -> t -> constructor puniverses +val destInd : Evd.evar_map -> t -> inductive * EInstance.t +val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t val destCase : Evd.evar_map -> t -> case_info * t * t * t array val destProj : Evd.evar_map -> t -> projection * t val destFix : Evd.evar_map -> t -> (t, t) pfixpoint @@ -262,6 +274,9 @@ sig val to_sorts : ESorts.t -> Sorts.t (** Physical identity. Does not care for normalization. *) + val to_instance : EInstance.t -> Univ.Instance.t + (** Physical identity. Does not care for normalization. *) + val eq : (t, Constr.t) eq (** Use for transparent cast between types. *) end -- cgit v1.2.3