From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 6 Oct 2015 19:09:10 +0200 Subject: Splitting kernel universe code in two modules. 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity. --- kernel/term.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/term.mli') diff --git a/kernel/term.mli b/kernel/term.mli index 501aaf741e..f8badb0ddc 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -427,11 +427,11 @@ val eq_constr : constr -> constr -> bool (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [u]. *) -val eq_constr_univs : constr Univ.check_function +val eq_constr_univs : constr UGraph.check_function (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo alpha, casts, application grouping and the universe constraints in [u]. *) -val leq_constr_univs : constr Univ.check_function +val leq_constr_univs : constr UGraph.check_function (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and ignoring universe instances. *) -- cgit v1.2.3 From 14edc57ac5ad75bbc4ea8559111606aea8978f48 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 18 Oct 2015 19:35:57 +0200 Subject: Adding a function to mirror decompose_prod_n_assum in that it counts let-ins, to compensate decompose_lam_n_assum which does not count let-ins. Any idea on a uniform and clear naming scheme for this kind of decomposition functions? --- kernel/term.mli | 31 ++++++++++++++++++++----------- 1 file changed, 20 insertions(+), 11 deletions(-) (limited to 'kernel/term.mli') diff --git a/kernel/term.mli b/kernel/term.mli index 501aaf741e..d60716410c 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -281,13 +281,15 @@ val decompose_prod : constr -> (Name.t*constr) list * constr {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a lambda. *) val decompose_lam : constr -> (Name.t*constr) list * constr -(** Given a positive integer n, transforms a product term +(** Given a positive integer n, decompose a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} - into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. *) + into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. + Raise a user error if not enough products. *) val decompose_prod_n : int -> constr -> (Name.t * constr) list * constr -(** Given a positive integer {% $ %}n{% $ %}, transforms a lambda term - {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %} *) +(** Given a positive integer {% $ %}n{% $ %}, decompose a lambda term + {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}. + Raise a user error if not enough lambdas. *) val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr (** Extract the premisses and the conclusion of a term of the form @@ -297,10 +299,15 @@ val decompose_prod_assum : types -> rel_context * types (** Idem with lambda's *) val decompose_lam_assum : constr -> rel_context * constr -(** Idem but extract the first [n] premisses *) +(** Idem but extract the first [n] premisses, counting let-ins. *) val decompose_prod_n_assum : int -> types -> rel_context * types + +(** Idem for lambdas, _not_ counting let-ins *) val decompose_lam_n_assum : int -> constr -> rel_context * constr +(** Idem, counting let-ins *) +val decompose_lam_n_decls : int -> constr -> rel_context * constr + (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction gives {% $ %}n{% $ %} (casts are ignored) *) val nb_lam : constr -> int @@ -308,12 +315,14 @@ val nb_lam : constr -> int (** Similar to [nb_lam], but gives the number of products instead *) val nb_prod : constr -> int -(** Returns the premisses/parameters of a type/term (let-in included) *) +(** Return the premisses/parameters of a type/term (let-in included) *) val prod_assum : types -> rel_context val lam_assum : constr -> rel_context -(** Returns the first n-th premisses/parameters of a type/term (let included)*) +(** Return the first n-th premisses/parameters of a type (let included and counted) *) val prod_n_assum : int -> types -> rel_context + +(** Return the first n-th premisses/parameters of a term (let included but not counted) *) val lam_n_assum : int -> constr -> rel_context (** Remove the premisses/parameters of a type/term *) @@ -328,11 +337,11 @@ val strip_lam_n : int -> constr -> constr val strip_prod_assum : types -> types val strip_lam_assum : constr -> constr -(** flattens application lists *) +(** Flattens application lists *) val collapse_appl : constr -> constr -(** Removes recursively the casts around a term i.e. +(** Remove recursively the casts around a term i.e. [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) val strip_outer_cast : constr -> constr @@ -352,10 +361,10 @@ type arity = rel_context * sorts (** Build an "arity" from its canonical form *) val mkArity : arity -> types -(** Destructs an "arity" into its canonical form *) +(** Destruct an "arity" into its canonical form *) val destArity : types -> arity -(** Tells if a term has the form of an arity *) +(** Tell if a term has the form of an arity *) val isArity : types -> bool (** {5 Kind of type} *) -- cgit v1.2.3 From 2e3ee15b03cf4b7428e1a7453385d79f434ec4a7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 8 Nov 2015 09:54:42 +0100 Subject: Moving three related small half-general half-ad-hoc utility functions next to each other, waiting for possible integration into a more uniform API. --- kernel/term.mli | 7 ------- 1 file changed, 7 deletions(-) (limited to 'kernel/term.mli') diff --git a/kernel/term.mli b/kernel/term.mli index 2bb8110608..69adb517a0 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -308,13 +308,6 @@ val decompose_lam_n_assum : int -> constr -> rel_context * constr (** Idem, counting let-ins *) val decompose_lam_n_decls : int -> constr -> rel_context * constr -(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction - gives {% $ %}n{% $ %} (casts are ignored) *) -val nb_lam : constr -> int - -(** Similar to [nb_lam], but gives the number of products instead *) -val nb_prod : constr -> int - (** Return the premisses/parameters of a type/term (let-in included) *) val prod_assum : types -> rel_context val lam_assum : constr -> rel_context -- cgit v1.2.3 From e8c47b652a0b53f8d3f7eaa877e81910c8de55d0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Nov 2015 17:11:39 +0100 Subject: Unifying betazeta_applist and prod_applist into a clearer interface. - prod_applist - prod_applist_assum - lambda_applist - lambda_applist_assum expect an instance matching the quantified context. They are now in term.ml, with "list" being possibly "vect". Names are a bit arbitrary. Better propositions are welcome. They are put in term.ml in that reduction is after all not needed, because the intent is not to do β or ι on the fly but rather to substitute a λΓ.c or ∀Γ.c (seen as internalization of a Γ⊢c) into one step, independently of the idea of reducing. On the other side: - beta_applist - beta_appvect are seen as optimizations of application doing reduction on the fly only if possible. They are then kept as functions relevant for reduction.ml. --- kernel/term.mli | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) (limited to 'kernel/term.mli') diff --git a/kernel/term.mli b/kernel/term.mli index 69adb517a0..972a67ebed 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -262,14 +262,34 @@ val to_lambda : int -> constr -> constr where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *) val to_prod : int -> constr -> constr +val it_mkLambda_or_LetIn : constr -> rel_context -> constr +val it_mkProd_or_LetIn : types -> rel_context -> types + +(** In [lambda_applist c args], [c] is supposed to have the form + [λΓ.c] with [Γ] without let-in; it returns [c] with the variables + of [Γ] instantiated by [args]. *) +val lambda_applist : constr -> constr list -> constr +val lambda_appvect : constr -> constr array -> constr + +(** In [lambda_applist_assum n c args], [c] is supposed to have the + form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it + returns [c] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val lambda_applist_assum : int -> constr -> constr list -> constr +val lambda_appvect_assum : int -> constr -> constr array -> constr + (** pseudo-reduction rule *) (** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *) val prod_appvect : constr -> constr array -> constr val prod_applist : constr -> constr list -> constr -val it_mkLambda_or_LetIn : constr -> rel_context -> constr -val it_mkProd_or_LetIn : types -> rel_context -> types +(** In [prod_appvect_assum n c args], [c] is supposed to have the + form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it + returns [c] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val prod_appvect_assum : int -> constr -> constr array -> constr +val prod_applist_assum : int -> constr -> constr list -> constr (** {5 Other term destructors. } *) -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- kernel/term.mli | 37 ++++++++++++++++++------------------- 1 file changed, 18 insertions(+), 19 deletions(-) (limited to 'kernel/term.mli') diff --git a/kernel/term.mli b/kernel/term.mli index 972a67ebed..c45e043386 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Context (** {5 Redeclaration of types from module Constr and Sorts} @@ -213,14 +212,14 @@ val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr val mkNamedProd : Id.t -> types -> types -> types (** Constructs either [(x:t)c] or [[x=b:t]c] *) -val mkProd_or_LetIn : rel_declaration -> types -> types -val mkProd_wo_LetIn : rel_declaration -> types -> types -val mkNamedProd_or_LetIn : named_declaration -> types -> types -val mkNamedProd_wo_LetIn : named_declaration -> types -> types +val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types +val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types +val mkNamedProd_or_LetIn : Context.Named.Declaration.t -> types -> types +val mkNamedProd_wo_LetIn : Context.Named.Declaration.t -> types -> types (** Constructs either [[x:t]c] or [[x=b:t]c] *) -val mkLambda_or_LetIn : rel_declaration -> constr -> constr -val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr +val mkLambda_or_LetIn : Context.Rel.Declaration.t -> constr -> constr +val mkNamedLambda_or_LetIn : Context.Named.Declaration.t -> constr -> constr (** {5 Other term constructors. } *) @@ -262,8 +261,8 @@ val to_lambda : int -> constr -> constr where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *) val to_prod : int -> constr -> constr -val it_mkLambda_or_LetIn : constr -> rel_context -> constr -val it_mkProd_or_LetIn : types -> rel_context -> types +val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr +val it_mkProd_or_LetIn : types -> Context.Rel.t -> types (** In [lambda_applist c args], [c] is supposed to have the form [λΓ.c] with [Γ] without let-in; it returns [c] with the variables @@ -314,29 +313,29 @@ val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr (** Extract the premisses and the conclusion of a term of the form "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *) -val decompose_prod_assum : types -> rel_context * types +val decompose_prod_assum : types -> Context.Rel.t * types (** Idem with lambda's *) -val decompose_lam_assum : constr -> rel_context * constr +val decompose_lam_assum : constr -> Context.Rel.t * constr (** Idem but extract the first [n] premisses, counting let-ins. *) -val decompose_prod_n_assum : int -> types -> rel_context * types +val decompose_prod_n_assum : int -> types -> Context.Rel.t * types (** Idem for lambdas, _not_ counting let-ins *) -val decompose_lam_n_assum : int -> constr -> rel_context * constr +val decompose_lam_n_assum : int -> constr -> Context.Rel.t * constr (** Idem, counting let-ins *) -val decompose_lam_n_decls : int -> constr -> rel_context * constr +val decompose_lam_n_decls : int -> constr -> Context.Rel.t * constr (** Return the premisses/parameters of a type/term (let-in included) *) -val prod_assum : types -> rel_context -val lam_assum : constr -> rel_context +val prod_assum : types -> Context.Rel.t +val lam_assum : constr -> Context.Rel.t (** Return the first n-th premisses/parameters of a type (let included and counted) *) -val prod_n_assum : int -> types -> rel_context +val prod_n_assum : int -> types -> Context.Rel.t (** Return the first n-th premisses/parameters of a term (let included but not counted) *) -val lam_n_assum : int -> constr -> rel_context +val lam_n_assum : int -> constr -> Context.Rel.t (** Remove the premisses/parameters of a type/term *) val strip_prod : types -> types @@ -369,7 +368,7 @@ val under_outer_cast : (constr -> constr) -> constr -> constr Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = rel_context * sorts +type arity = Context.Rel.t * sorts (** Build an "arity" from its canonical form *) val mkArity : arity -> types -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/term.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/term.mli') diff --git a/kernel/term.mli b/kernel/term.mli index d60716410c..14c20a2054 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* cofixpoint (** non-dependent product [t1 -> t2], an alias for [forall (_:t1), t2]. Beware [t_2] is NOT lifted. - Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 0) (mkRel 1))] + Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 1) (mkRel 2))] *) val mkArrow : types -> types -> constr -- cgit v1.2.3