diff options
Diffstat (limited to 'kernel/context.ml')
| -rw-r--r-- | kernel/context.ml | 133 |
1 files changed, 85 insertions, 48 deletions
diff --git a/kernel/context.ml b/kernel/context.ml index 4e53b73a..4f3f649c 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Jean-Christophe Filliâtre out of names.ml as part of the @@ -37,9 +39,11 @@ struct module Declaration = struct (* local declaration *) - type t = - | LocalAssum of Name.t * Constr.t (** name, type *) - | LocalDef of Name.t * Constr.t * Constr.t (** name, value, type *) + type ('constr, 'types) pt = + | 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. *) let get_name = function @@ -87,12 +91,12 @@ struct | LocalDef (_, v, ty) -> f v && f ty (** Check whether the two given declarations are equal. *) - let equal decl1 decl2 = + let equal eq decl1 decl2 = match decl1, decl2 with | LocalAssum (n1,ty1), LocalAssum (n2, ty2) -> - Name.equal n1 n2 && Constr.equal ty1 ty2 + Name.equal n1 n2 && eq ty1 ty2 | LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) -> - Name.equal n1 n2 && Constr.equal v1 v2 && Constr.equal ty1 ty2 + Name.equal n1 n2 && eq v1 v2 && eq ty1 ty2 | _ -> false @@ -138,7 +142,7 @@ struct | LocalDef (_,v,ty) -> f v; f ty (** Reduce all terms in a given declaration to a single value. *) - let fold f decl acc = + let fold_constr f decl acc = match decl with | LocalAssum (n,ty) -> f ty acc | LocalDef (n,v,ty) -> f ty (f v acc) @@ -147,14 +151,12 @@ struct | LocalAssum (na, ty) -> na, None, ty | LocalDef (na, v, ty) -> na, Some v, ty - let of_tuple = function - | n, None, ty -> LocalAssum (n,ty) - | n, Some v, ty -> LocalDef (n,v,ty) 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 *) @@ -169,14 +171,14 @@ struct (** [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]. *) - let nhyps = + let nhyps ctx = let open Declaration in let rec nhyps acc = function | [] -> acc | LocalAssum _ :: hyps -> nhyps (succ acc) hyps | LocalDef _ :: hyps -> nhyps acc hyps in - nhyps 0 + nhyps 0 ctx (** Return a declaration designated by a given de Bruijn index. @raise Not_found if the designated de Bruijn index is not present in the designated rel-context. *) @@ -187,7 +189,7 @@ struct | _, [] -> raise Not_found (** Check whether given two rel-contexts are equal. *) - let equal = List.equal Declaration.equal + let equal eq l = List.equal (fun c -> Declaration.equal eq c) l (** Map all terms in a given rel-context. *) let map f = List.smartmap (Declaration.map_constr f) @@ -205,26 +207,26 @@ struct (** 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]. *) - let to_tags = + let to_tags l = let rec aux l = function | [] -> l | Declaration.LocalDef _ :: ctx -> aux (true::l) ctx | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx - in aux [] + in aux [] l (** [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]. *) - let to_extended_list n = + let to_extended_list mk n l = let rec reln l p = function - | Declaration.LocalAssum _ :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps + | Declaration.LocalAssum _ :: hyps -> reln (mk (n+p) :: l) (p+1) hyps | Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps | [] -> l in - reln [] 1 + reln [] 1 l (** [extended_vect n Γ] does the same, returning instead an array. *) - let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps) + let to_extended_vect mk n hyps = Array.of_list (to_extended_list mk n hyps) end (** This module represents contexts that can capture non-anonymous variables. @@ -235,9 +237,11 @@ struct module Declaration = struct (** local declaration *) - type t = - | LocalAssum of Id.t * Constr.t (** identifier, type *) - | LocalDef of Id.t * Constr.t * Constr.t (** identifier, value, type *) + type ('constr, 'types) pt = + | 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. *) let get_id = function @@ -285,12 +289,12 @@ struct | LocalDef (_, v, ty) -> f v && f ty (** Check whether the two given declarations are equal. *) - let equal decl1 decl2 = + let equal eq decl1 decl2 = match decl1, decl2 with | LocalAssum (id1, ty1), LocalAssum (id2, ty2) -> - Id.equal id1 id2 && Constr.equal ty1 ty2 + Id.equal id1 id2 && eq ty1 ty2 | LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) -> - Id.equal id1 id2 && Constr.equal v1 v2 && Constr.equal ty1 ty2 + Id.equal id1 id2 && eq v1 v2 && eq ty1 ty2 | _ -> false @@ -336,7 +340,7 @@ struct | LocalDef (_, v, ty) -> f v; f ty (** Reduce all terms in a given declaration to a single value. *) - let fold f decl a = + let fold_constr f decl a = match decl with | LocalAssum (_, ty) -> f ty a | LocalDef (_, v, ty) -> a |> f v |> f ty @@ -348,11 +352,24 @@ struct let of_tuple = function | id, None, ty -> LocalAssum (id, ty) | id, Some v, ty -> LocalDef (id, v, ty) + + let of_rel_decl f = function + | Rel.Declaration.LocalAssum (na,t) -> + LocalAssum (f na, t) + | Rel.Declaration.LocalDef (na,v,t) -> + LocalDef (f na, v, t) + + let to_rel_decl = function + | LocalAssum (id,t) -> + Rel.Declaration.LocalAssum (Name id, t) + | LocalDef (id,v,t) -> + Rel.Declaration.LocalDef (Name id,v,t) end (** Named-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 named-context *) @@ -364,14 +381,15 @@ struct (** Return the number of {e local declarations} in a given named-context. *) let length = List.length -(** Return a declaration designated by a given de Bruijn index. - @raise Not_found if the designated identifier is not present in the designated named-context. *) let rec lookup id = function +(** Return a declaration designated by a given identifier + @raise Not_found if the designated identifier is not present in the designated named-context. *) + let rec lookup id = function | decl :: _ when Id.equal id (Declaration.get_id decl) -> decl | _ :: sign -> lookup id sign | [] -> raise Not_found (** Check whether given two named-contexts are equal. *) - let equal = List.equal Declaration.equal + let equal eq l = List.equal (fun c -> Declaration.equal eq c) l (** Map all terms in a given named-context. *) let map f = List.smartmap (Declaration.map_constr f) @@ -388,36 +406,55 @@ struct let fold_outside f l ~init = List.fold_right f l init (** Return the set of all identifiers bound in a given named-context. *) - let to_vars = - List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty + let to_vars l = + List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty l (** [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. *) - let to_instance = + let to_instance mk l = let filter = function - | Declaration.LocalAssum (id, _) -> Some (Constr.mkVar id) + | Declaration.LocalAssum (id, _) -> Some (mk id) | _ -> None in - List.map_filter filter - end + List.map_filter filter l +end -module NamedList = +module Compacted = struct module Declaration = struct - type t = Id.t list * Constr.t option * Constr.t - - let map_constr f (ids, copt, ty as decl) = - let copt' = Option.map f copt in - let ty' = f ty in - if copt == copt' && ty == ty' then decl else (ids, copt', ty') + type ('constr, 'types) pt = + | LocalAssum of Id.t list * 'types + | LocalDef of Id.t list * 'constr * 'types + + type t = (Constr.constr, Constr.types) pt + + let map_constr f = function + | LocalAssum (ids, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalAssum (ids, ty') + | LocalDef (ids, c, ty) as decl -> + let ty' = f ty in + let c' = f c in + if c == c' && ty == ty' then decl else LocalDef (ids,c',ty') + + let of_named_decl = function + | Named.Declaration.LocalAssum (id,t) -> + LocalAssum ([id],t) + | Named.Declaration.LocalDef (id,v,t) -> + LocalDef ([id],v,t) + + let to_named_context = function + | LocalAssum (ids, t) -> + List.map (fun id -> Named.Declaration.LocalAssum (id,t)) ids + | LocalDef (ids, v, t) -> + List.map (fun id -> Named.Declaration.LocalDef (id,v,t)) ids end + type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list type t = Declaration.t list let fold f l ~init = List.fold_right f l init end - -type section_context = Named.t |