diff options
Diffstat (limited to 'kernel/context.mli')
| -rw-r--r-- | kernel/context.mli | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/kernel/context.mli b/kernel/context.mli index c97db434..2b0d36cb 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -35,8 +35,6 @@ sig | LocalAssum of Name.t * 'types (** name, type *) | LocalDef of Name.t * 'constr * 'types (** name, value, type *) - type t = (Constr.constr, Constr.types) pt - (** Return the name bound by a given declaration. *) val get_name : ('c, 't) pt -> Name.t @@ -87,13 +85,15 @@ sig val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a val to_tuple : ('c, 't) pt -> Name.t * 'c option * 't + + (** Turn [LocalDef] into [LocalAssum], identity otherwise. *) + val drop_body : ('c, 't) pt -> ('c, 't) pt 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 ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list (** empty rel-context *) val empty : ('c, 't) pt @@ -132,6 +132,9 @@ sig and each {e local definition} is mapped to [false]. *) val to_tags : ('c, 't) pt -> bool list + (** Turn all [LocalDef] into [LocalAssum], leave [LocalAssum] unchanged. *) + val drop_bodies : ('c, 't) pt -> ('c, 't) pt + (** [extended_list mk n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] with n = |Δ| and with the {e local definitions} of [Γ] skipped in [args] where [mk] is used to build the corresponding variables. @@ -153,8 +156,6 @@ sig | LocalAssum of Id.t * 'types (** identifier, type *) | LocalDef of Id.t * 'constr * 'types (** identifier, value, type *) - type t = (Constr.constr, Constr.types) pt - (** Return the identifier bound by a given declaration. *) val get_id : ('c, 't) pt -> Id.t @@ -207,6 +208,9 @@ sig val to_tuple : ('c, 't) pt -> Id.t * 'c option * 't val of_tuple : Id.t * 'c option * 't -> ('c, 't) pt + (** Turn [LocalDef] into [LocalAssum], identity otherwise. *) + val drop_body : ('c, 't) pt -> ('c, 't) pt + (** Convert [Rel.Declaration.t] value to the corresponding [Named.Declaration.t] value. The function provided as the first parameter determines how to translate "names" to "ids". *) val of_rel_decl : (Name.t -> Id.t) -> ('c, 't) Rel.Declaration.pt -> ('c, 't) pt @@ -220,7 +224,6 @@ sig Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list (** empty named-context *) val empty : ('c, 't) pt @@ -255,6 +258,9 @@ sig (** Return the set of all identifiers bound in a given named-context. *) val to_vars : ('c, 't) pt -> Id.Set.t + (** Turn all [LocalDef] into [LocalAssum], leave [LocalAssum] unchanged. *) + val drop_bodies : ('c, 't) pt -> ('c, 't) pt + (** [to_instance Ω] 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 @@ -270,15 +276,12 @@ sig | LocalAssum of Id.t list * 'types | LocalDef of Id.t list * 'constr * 'types - type t = (Constr.constr, Constr.types) pt - val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt val of_named_decl : ('c, 't) Named.Declaration.pt -> ('c, 't) pt val to_named_context : ('c, 't) pt -> ('c, 't) Named.pt end type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list val fold : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a end |