From 6899d3aa567436784a08af4e179c2ef1fa504a02 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 21 Nov 2015 00:17:21 +0100 Subject: Moving extended_rel_vect/extended_rel_list to the kernel. It will later be used to fix a bug and improve some code. Interestingly, there were a redundant semantic equivalent to extended_rel_list in the kernel called local_rels, and another private copy of extended_rel_list in exactly the same file. --- kernel/context.mli | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'kernel/context.mli') diff --git a/kernel/context.mli b/kernel/context.mli index 5279aefb6b..7354677474 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -82,8 +82,21 @@ val fold_named_context_reverse : ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a (** {6 Section-related auxiliary functions } *) + +(** [instance_from_named_context Ω] builds an instance [args] such + that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local + definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it + gives [Var id1, Var id3]. All [idj] are supposed distinct. *) val instance_from_named_context : named_context -> Constr.t list +(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] + with n = |Δ| and with the local definitions of [Γ] skipped in + [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) +val extended_rel_list : int -> rel_context -> Constr.t list + +(** [extended_rel_vect n Γ] does the same, returning instead an array. *) +val extended_rel_vect : int -> rel_context -> Constr.t array + (** {6 ... } *) (** Signatures of ordered optionally named variables, intended to be accessed by de Bruijn indices *) @@ -120,3 +133,4 @@ val rel_context_length : rel_context -> int val rel_context_nhyps : rel_context -> int (** Indicates whether a LetIn or a Lambda, starting from oldest declaration *) val rel_context_tags : rel_context -> bool list + -- 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/context.mli | 243 ++++++++++++++++++++++++++++++++--------------------- 1 file changed, 149 insertions(+), 94 deletions(-) (limited to 'kernel/context.mli') diff --git a/kernel/context.mli b/kernel/context.mli index 7354677474..0db82beb57 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -6,131 +6,186 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** The modules defined below represent a {e local context} + as defined by Chapter 4 in the Reference Manual: + + A {e local context} is an ordered list of of {e local declarations} + of names that we call {e variables}. + + A {e local declaration} of some variable can be either: + - a {e local assumption}, or + - a {e local definition}. + + {e Local assumptions} are denoted in the Reference Manual as [(name : typ)] and + {e local definitions} are there denoted as [(name := value : typ)]. +*) + open Names -(** TODO: cleanup *) +(** Representation of contexts that can capture anonymous as well as non-anonymous variables. + Individual declarations are then designated by de Bruijn indexes. *) +module Rel : +sig + (** Representation of {e local declarations}. + + [(name, None, typ)] represents a {e local assumption}. + + [(name, Some value, typ)] represents a {e local definition}. + *) + module Declaration : + sig + type t = Name.t * Constr.t option * Constr.t + + (** Map all terms in a given declaration. *) + val map : (Constr.t -> Constr.t) -> t -> t + + (** Reduce all terms in a given declaration to a single value. *) + val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + + (** Check whether any term in a given declaration satisfies a given predicate. *) + val exists : (Constr.t -> bool) -> t -> bool + + (** Check whether all terms in a given declaration satisfy a given predicate. *) + val for_all : (Constr.t -> bool) -> t -> bool + + (** Check whether the two given declarations are equal. *) + val equal : t -> t -> bool + end + + (** Rel-context is represented as a list of declarations. + Inner-most declarations are at the beginning of the list. + Outer-most declarations are at the end of the list. *) + type t = Declaration.t list + + (** empty rel-context *) + val empty : t + + (** Return a new rel-context enriched by with a given inner-most declaration. *) + val add : Declaration.t -> t -> t + + (** Return a declaration designated by a given de Bruijn index. + @raise Not_found if the designated de Bruijn index outside the range. *) + val lookup : int -> t -> Declaration.t + + (** Map all terms in a given rel-context. *) + val map : (Constr.t -> Constr.t) -> t -> t -(** {6 Declarations} *) -(** A {e declaration} has the form [(name,body,type)]. It is either an - {e assumption} if [body=None] or a {e definition} if - [body=Some actualbody]. It is referred by {e name} if [na] is an - identifier or by {e relative index} if [na] is not an identifier - (in the latter case, [na] is of type [name] but just for printing - purpose) *) + (** Reduce all terms in a given rel-context to a single value. + Innermost declarations are processed first. *) + val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a -type named_declaration = Id.t * Constr.t option * Constr.t -type named_list_declaration = Id.t list * Constr.t option * Constr.t -type rel_declaration = Name.t * Constr.t option * Constr.t + (** Reduce all terms in a given rel-context to a single value. + Outermost declarations are processed first. *) + val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a -val map_named_declaration : - (Constr.t -> Constr.t) -> named_declaration -> named_declaration -val map_named_list_declaration : - (Constr.t -> Constr.t) -> named_list_declaration -> named_list_declaration -val map_rel_declaration : - (Constr.t -> Constr.t) -> rel_declaration -> rel_declaration + (** Perform a given action on every declaration in a given rel-context. *) + val iter : (Constr.t -> unit) -> t -> unit -val fold_named_declaration : - (Constr.t -> 'a -> 'a) -> named_declaration -> 'a -> 'a -val fold_rel_declaration : - (Constr.t -> 'a -> 'a) -> rel_declaration -> 'a -> 'a + (** Return the number of {e local declarations} in a given context. *) + val length : t -> int -val exists_named_declaration : - (Constr.t -> bool) -> named_declaration -> bool -val exists_rel_declaration : - (Constr.t -> bool) -> rel_declaration -> bool + (** Return the number of {e local assumptions} in a given rel-context. *) + val nhyps : t -> int -val for_all_named_declaration : - (Constr.t -> bool) -> named_declaration -> bool -val for_all_rel_declaration : - (Constr.t -> bool) -> rel_declaration -> bool + (** Map a given rel-context to a list where each {e local assumption} is mapped to [true] + and each {e local definition} is mapped to [false]. *) + val to_tags : t -> bool list -val eq_named_declaration : - named_declaration -> named_declaration -> bool + (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] + with n = |Δ| and with the {e local definitions} of [Γ] skipped in + [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) + val to_extended_list : int -> t -> Constr.t list -val eq_rel_declaration : - rel_declaration -> rel_declaration -> bool + (** [extended_vect n Γ] does the same, returning instead an array. *) + val to_extended_vect : int -> t -> Constr.t array +end -(** {6 Signatures of ordered named declarations } *) +(** This module represents contexts that can capture non-anonymous variables. + Individual declarations are then designated by the identifiers they bind. *) +module Named : +sig + (** Representation of {e local declarations}. -type named_context = named_declaration list -type section_context = named_context -type named_list_context = named_list_declaration list -type rel_context = rel_declaration list -(** In [rel_context], more recent declaration is on top *) + [(id, None, typ)] represents a {e local assumption}. -val empty_named_context : named_context -val add_named_decl : named_declaration -> named_context -> named_context -val vars_of_named_context : named_context -> Id.Set.t + [(id, Some value, typ)] represents a {e local definition}. + *) + module Declaration : + sig + type t = Id.t * Constr.t option * Constr.t -val lookup_named : Id.t -> named_context -> named_declaration + (** Map all terms in a given declaration. *) + val map : (Constr.t -> Constr.t) -> t -> t -(** number of declarations *) -val named_context_length : named_context -> int + (** Reduce all terms in a given declaration to a single value. *) + val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a -(** named context equality *) -val named_context_equal : named_context -> named_context -> bool + (** Check whether any term in a given declaration satisfies a given predicate. *) + val exists : (Constr.t -> bool) -> t -> bool -(** {6 Recurrence on [named_context]: older declarations processed first } *) -val fold_named_context : - (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a + (** Check whether all terms in a given declaration satisfy a given predicate. *) + val for_all : (Constr.t -> bool) -> t -> bool -val fold_named_list_context : - (named_list_declaration -> 'a -> 'a) -> named_list_context -> init:'a -> 'a + (** Check whether the two given declarations are equal. *) + val equal : t -> t -> bool + end -(** newer declarations first *) -val fold_named_context_reverse : - ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a + (** Rel-context is represented as a list of declarations. + Inner-most declarations are at the beginning of the list. + Outer-most declarations are at the end of the list. *) + type t = Declaration.t list -(** {6 Section-related auxiliary functions } *) + (** empty named-context *) + val empty : t -(** [instance_from_named_context Ω] builds an instance [args] such - that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local - definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it - gives [Var id1, Var id3]. All [idj] are supposed distinct. *) -val instance_from_named_context : named_context -> Constr.t list + (** Return a new rel-context enriched by with a given inner-most declaration. *) + val add : Declaration.t -> t -> t -(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] - with n = |Δ| and with the local definitions of [Γ] skipped in - [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) -val extended_rel_list : int -> rel_context -> Constr.t list + (** Return a declaration designated by an identifier of the variable bound in that declaration. + @raise Not_found if the designated identifier is not bound in a given named-context. *) + val lookup : Id.t -> t -> Declaration.t -(** [extended_rel_vect n Γ] does the same, returning instead an array. *) -val extended_rel_vect : int -> rel_context -> Constr.t array + (** Map all terms in a given named-context. *) + val map : (Constr.t -> Constr.t) -> t -> t -(** {6 ... } *) -(** Signatures of ordered optionally named variables, intended to be - accessed by de Bruijn indices *) + (** Reduce all terms in a given named-context to a single value. + Innermost declarations are processed first. *) + val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a -(** {6 Recurrence on [rel_context]: older declarations processed first } *) -val fold_rel_context : - (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a + (** Reduce all terms in a given named-context to a single value. + Outermost declarations are processed first. *) + val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a -(** newer declarations first *) -val fold_rel_context_reverse : - ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a + (** Perform a given action on every declaration in a given named-context. *) + val iter : (Constr.t -> unit) -> t -> unit -(** {6 Map function of [rel_context] } *) -val map_rel_context : (Constr.t -> Constr.t) -> rel_context -> rel_context + (** Return the number of {e local declarations} in a given named-context. *) + val length : t -> int -(** {6 Map function of [named_context] } *) -val map_named_context : (Constr.t -> Constr.t) -> named_context -> named_context + (** Check whether given two named-contexts are equal. *) + val equal : t -> t -> bool -(** {6 Map function of [rel_context] } *) -val iter_rel_context : (Constr.t -> unit) -> rel_context -> unit + (** Return the set of all identifiers bound in a given named-context. *) + val to_vars : t -> Id.Set.t -(** {6 Map function of [named_context] } *) -val iter_named_context : (Constr.t -> unit) -> named_context -> unit + (** [instance_from_named_context Ω] builds an instance [args] such + that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local + definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it + gives [Var id1, Var id3]. All [idj] are supposed distinct. *) + val to_instance : t -> Constr.t list +end -(** {6 Contexts of declarations referred to by de Bruijn indices } *) +module NamedList : +sig + module Declaration : + sig + type t = Id.t list * Constr.t option * Constr.t + val map : (Constr.t -> Constr.t) -> t -> t + end -val empty_rel_context : rel_context -val add_rel_decl : rel_declaration -> rel_context -> rel_context + type t = Declaration.t list -val lookup_rel : int -> rel_context -> rel_declaration -(** Size of the [rel_context] including LetIns *) -val rel_context_length : rel_context -> int -(** Size of the [rel_context] without LetIns *) -val rel_context_nhyps : rel_context -> int -(** Indicates whether a LetIn or a Lambda, starting from oldest declaration *) -val rel_context_tags : rel_context -> bool list + val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a +end +type section_context = Named.t -- 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/context.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/context.mli') diff --git a/kernel/context.mli b/kernel/context.mli index 5279aefb6b..b78bbb03e6 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- kernel/context.mli | 151 ++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 110 insertions(+), 41 deletions(-) (limited to 'kernel/context.mli') diff --git a/kernel/context.mli b/kernel/context.mli index 1976e46d33..a69754cc29 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -26,21 +26,32 @@ open Names Individual declarations are then designated by de Bruijn indexes. *) module Rel : sig - (** Representation of {e local declarations}. - - [(name, None, typ)] represents a {e local assumption}. - - [(name, Some value, typ)] represents a {e local definition}. - *) module Declaration : sig - type t = Name.t * Constr.t option * Constr.t + (* local declaration *) + type t = LocalAssum of Name.t * Constr.t (* local assumption *) + | LocalDef of Name.t * Constr.t * Constr.t (* local definition *) - (** Map all terms in a given declaration. *) - val map : (Constr.t -> Constr.t) -> t -> t + (** Return the name bound by a given declaration. *) + val get_name : t -> Name.t - (** Reduce all terms in a given declaration to a single value. *) - val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + (** Return [Some value] for local-declarations and [None] for local-assumptions. *) + val get_value : t -> Constr.t option + + (** Return the type of the name bound by a given declaration. *) + val get_type : t -> Constr.t + + (** Set the name that is bound by a given declaration. *) + val set_name : Name.t -> t -> t + + (** Set the type of the bound variable in a given declaration. *) + val set_type : Constr.t -> t -> t + + (** Return [true] iff a given declaration is a local assumption. *) + val is_local_assum : t -> bool + + (** Return [true] iff a given declaration is a local definition. *) + val is_local_def : t -> bool (** Check whether any term in a given declaration satisfies a given predicate. *) val exists : (Constr.t -> bool) -> t -> bool @@ -50,6 +61,28 @@ sig (** Check whether the two given declarations are equal. *) val equal : t -> t -> bool + + (** Map the name bound by a given declaration. *) + val map_name : (Name.t -> Name.t) -> t -> t + + (** For local assumptions, this function returns the original local assumptions. + For local definitions, this function maps the value in the local definition. *) + val map_value : (Constr.t -> Constr.t) -> t -> t + + (** Map the type of the name bound by a given declaration. *) + val map_type : (Constr.t -> Constr.t) -> t -> t + + (** Map all terms in a given declaration. *) + val map_constr : (Constr.t -> Constr.t) -> t -> t + + (** Perform a given action on all terms in a given declaration. *) + val iter_constr : (Constr.t -> unit) -> t -> unit + + (** Reduce all terms in a given declaration to a single value. *) + val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + + val to_tuple : t -> Name.t * Constr.t option * Constr.t + val of_tuple : Name.t * Constr.t option * Constr.t -> t end (** Rel-context is represented as a list of declarations. @@ -63,6 +96,15 @@ sig (** Return a new rel-context enriched by with a given inner-most declaration. *) val add : Declaration.t -> t -> t + (** Return the number of {e local declarations} in a given context. *) + val length : t -> int + + (** Check whether given two rel-contexts are equal. *) + val equal : t -> t -> bool + + (** Return the number of {e local assumptions} in a given rel-context. *) + val nhyps : t -> int + (** Return a declaration designated by a given de Bruijn index. @raise Not_found if the designated de Bruijn index outside the range. *) val lookup : int -> t -> Declaration.t @@ -70,6 +112,9 @@ sig (** Map all terms in a given rel-context. *) val map : (Constr.t -> Constr.t) -> t -> t + (** Perform a given action on every declaration in a given rel-context. *) + val iter : (Constr.t -> unit) -> t -> unit + (** Reduce all terms in a given rel-context to a single value. Innermost declarations are processed first. *) val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a @@ -78,15 +123,6 @@ sig Outermost declarations are processed first. *) val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a - (** Perform a given action on every declaration in a given rel-context. *) - val iter : (Constr.t -> unit) -> t -> unit - - (** Return the number of {e local declarations} in a given context. *) - val length : t -> int - - (** Return the number of {e local assumptions} in a given rel-context. *) - val nhyps : t -> int - (** Map a given rel-context to a list where each {e local assumption} is mapped to [true] and each {e local definition} is mapped to [false]. *) val to_tags : t -> bool list @@ -104,21 +140,32 @@ end Individual declarations are then designated by the identifiers they bind. *) module Named : sig - (** Representation of {e local declarations}. - - [(id, None, typ)] represents a {e local assumption}. - - [(id, Some value, typ)] represents a {e local definition}. - *) + (** Representation of {e local declarations}. *) module Declaration : sig - type t = Id.t * Constr.t option * Constr.t + type t = LocalAssum of Id.t * Constr.t + | LocalDef of Id.t * Constr.t * Constr.t - (** Map all terms in a given declaration. *) - val map : (Constr.t -> Constr.t) -> t -> t + (** Return the identifier bound by a given declaration. *) + val get_id : t -> Id.t - (** Reduce all terms in a given declaration to a single value. *) - val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + (** Return [Some value] for local-declarations and [None] for local-assumptions. *) + val get_value : t -> Constr.t option + + (** Return the type of the name bound by a given declaration. *) + val get_type : t -> Constr.t + + (** Set the identifier that is bound by a given declaration. *) + val set_id : Id.t -> t -> t + + (** Set the type of the bound variable in a given declaration. *) + val set_type : Constr.t -> t -> t + + (** Return [true] iff a given declaration is a local assumption. *) + val is_local_assum : t -> bool + + (** Return [true] iff a given declaration is a local definition. *) + val is_local_def : t -> bool (** Check whether any term in a given declaration satisfies a given predicate. *) val exists : (Constr.t -> bool) -> t -> bool @@ -128,6 +175,28 @@ sig (** Check whether the two given declarations are equal. *) val equal : t -> t -> bool + + (** Map the identifier bound by a given declaration. *) + val map_id : (Id.t -> Id.t) -> t -> t + + (** For local assumptions, this function returns the original local assumptions. + For local definitions, this function maps the value in the local definition. *) + val map_value : (Constr.t -> Constr.t) -> t -> t + + (** Map the type of the name bound by a given declaration. *) + val map_type : (Constr.t -> Constr.t) -> t -> t + + (** Map all terms in a given declaration. *) + val map_constr : (Constr.t -> Constr.t) -> t -> t + + (** Perform a given action on all terms in a given declaration. *) + val iter_constr : (Constr.t -> unit) -> t -> unit + + (** Reduce all terms in a given declaration to a single value. *) + val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + + val to_tuple : t -> Id.t * Constr.t option * Constr.t + val of_tuple : Id.t * Constr.t option * Constr.t -> t end (** Rel-context is represented as a list of declarations. @@ -141,13 +210,22 @@ sig (** Return a new rel-context enriched by with a given inner-most declaration. *) val add : Declaration.t -> t -> t + (** Return the number of {e local declarations} in a given named-context. *) + val length : t -> int + (** Return a declaration designated by an identifier of the variable bound in that declaration. @raise Not_found if the designated identifier is not bound in a given named-context. *) val lookup : Id.t -> t -> Declaration.t + (** Check whether given two rel-contexts are equal. *) + val equal : t -> t -> bool + (** Map all terms in a given named-context. *) val map : (Constr.t -> Constr.t) -> t -> t + (** Perform a given action on every declaration in a given named-context. *) + val iter : (Constr.t -> unit) -> t -> unit + (** Reduce all terms in a given named-context to a single value. Innermost declarations are processed first. *) val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a @@ -156,15 +234,6 @@ sig Outermost declarations are processed first. *) val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a - (** Perform a given action on every declaration in a given named-context. *) - val iter : (Constr.t -> unit) -> t -> unit - - (** Return the number of {e local declarations} in a given named-context. *) - val length : t -> int - - (** Check whether given two named-contexts are equal. *) - val equal : t -> t -> bool - (** Return the set of all identifiers bound in a given named-context. *) val to_vars : t -> Id.Set.t @@ -180,7 +249,7 @@ sig module Declaration : sig type t = Id.t list * Constr.t option * Constr.t - val map : (Constr.t -> Constr.t) -> t -> t + val map_constr : (Constr.t -> Constr.t) -> t -> t end type t = Declaration.t list -- cgit v1.2.3 From 5dfb5d5e48c86dabd17ee2167c6fd5304c788474 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 9 Feb 2016 18:07:53 +0100 Subject: REFORMATTING: kernel/context.ml{,i} --- kernel/context.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/context.mli') diff --git a/kernel/context.mli b/kernel/context.mli index a69754cc29..b5f3904d22 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -29,8 +29,8 @@ sig module Declaration : sig (* local declaration *) - type t = LocalAssum of Name.t * Constr.t (* local assumption *) - | LocalDef of Name.t * Constr.t * Constr.t (* local definition *) + type t = LocalAssum of Name.t * Constr.t (** name, type *) + | LocalDef of Name.t * Constr.t * Constr.t (** name, value, type *) (** Return the name bound by a given declaration. *) val get_name : t -> Name.t @@ -143,8 +143,8 @@ sig (** Representation of {e local declarations}. *) module Declaration : sig - type t = LocalAssum of Id.t * Constr.t - | LocalDef of Id.t * Constr.t * Constr.t + type t = LocalAssum of Id.t * Constr.t (** identifier, type *) + | LocalDef of Id.t * Constr.t * Constr.t (** identifier, value, type *) (** Return the identifier bound by a given declaration. *) val get_id : t -> Id.t -- cgit v1.2.3