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.ml | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'kernel/context.ml') diff --git a/kernel/context.ml b/kernel/context.ml index 796f06d37e..5923048fa4 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -111,6 +111,20 @@ let instance_from_named_context sign = in List.map_filter filter sign +(** [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 extended_rel_list n hyps = + let rec reln l p = function + | (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps + | (_, Some _, _) :: hyps -> reln l (p+1) hyps + | [] -> l + in + reln [] 1 hyps + +let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps) + let fold_named_context f l ~init = List.fold_right f l init let fold_named_list_context f l ~init = List.fold_right f l init let fold_named_context_reverse f ~init l = List.fold_left f init l -- 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.ml | 356 ++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 226 insertions(+), 130 deletions(-) (limited to 'kernel/context.ml') diff --git a/kernel/context.ml b/kernel/context.ml index 5923048fa4..372f16a8d5 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -15,137 +15,233 @@ (* This file defines types and combinators regarding indexes-based and names-based contexts *) -open Util -open Names - -(***************************************************************************) -(* Type of assumptions *) -(***************************************************************************) - -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 - -let map_named_declaration_skel f (id, (v : Constr.t option), ty) = - (id, Option.map f v, f ty) -let map_named_list_declaration = map_named_declaration_skel -let map_named_declaration = map_named_declaration_skel - -let map_rel_declaration = map_named_declaration - -let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a) -let fold_rel_declaration = fold_named_declaration - -let exists_named_declaration f (_, v, ty) = Option.cata f false v || f ty -let exists_rel_declaration f (_, v, ty) = Option.cata f false v || f ty - -let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty -let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty - -let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = - Id.equal i1 i2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2 - -let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) = - Name.equal n1 n2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2 - -(***************************************************************************) -(* Type of local contexts (telescopes) *) -(***************************************************************************) - -(*s Signatures of ordered optionally named variables, intended to be - accessed by de Bruijn indices (to represent bound variables) *) - -type rel_context = rel_declaration list - -let empty_rel_context = [] - -let add_rel_decl d ctxt = d::ctxt - -let rec lookup_rel n sign = - match n, sign with - | 1, decl :: _ -> decl - | n, _ :: sign -> lookup_rel (n-1) sign - | _, [] -> raise Not_found - -let rel_context_length = List.length +(** The modules defined below represent a {e local context} + as defined by Chapter 4 in the Reference Manual: -let rel_context_nhyps hyps = - let rec nhyps acc = function - | [] -> acc - | (_,None,_)::hyps -> nhyps (1+acc) hyps - | (_,Some _,_)::hyps -> nhyps acc hyps in - nhyps 0 hyps + A {e local context} is an ordered list of of {e local declarations} + of names that we call {e variables}. -let rel_context_tags ctx = - let rec aux l = function - | [] -> l - | (_,Some _,_)::ctx -> aux (true::l) ctx - | (_,None,_)::ctx -> aux (false::l) ctx - in aux [] ctx + A {e local declaration} of some variable can be either: + - a {e local assumption}, or + - a {e local definition}. +*) -(*s Signatures of named hypotheses. Used for section variables and - goal assumptions. *) - -type named_context = named_declaration list -type named_list_context = named_list_declaration list - -let empty_named_context = [] - -let add_named_decl d sign = d::sign - -let rec lookup_named id = function - | (id',_,_ as decl) :: _ when Id.equal id id' -> decl - | _ :: sign -> lookup_named id sign - | [] -> raise Not_found - -let named_context_length = List.length -let named_context_equal = List.equal eq_named_declaration - -let vars_of_named_context ctx = - List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty ctx - -let instance_from_named_context sign = - let filter = function - | (id, None, _) -> Some (Constr.mkVar id) - | (_, Some _, _) -> None - in - List.map_filter filter sign - -(** [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 extended_rel_list n hyps = - let rec reln l p = function - | (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps - | (_, Some _, _) :: hyps -> reln l (p+1) hyps - | [] -> l - in - reln [] 1 hyps - -let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps) - -let fold_named_context f l ~init = List.fold_right f l init -let fold_named_list_context f l ~init = List.fold_right f l init -let fold_named_context_reverse f ~init l = List.fold_left f init l - -(*s Signatures of ordered section variables *) -type section_context = named_context - -let fold_rel_context f l ~init:x = List.fold_right f l x -let fold_rel_context_reverse f ~init:x l = List.fold_left f x l - -let map_context f l = - let map_decl (n, body_o, typ as decl) = - let body_o' = Option.smartmap f body_o in - let typ' = f typ in - if body_o' == body_o && typ' == typ then decl else - (n, body_o', typ') - in - List.smartmap map_decl l - -let map_rel_context = map_context -let map_named_context = map_context +open Util +open Names -let iter_rel_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b) -let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b) +(** Representation of contexts that can capture anonymous as well as non-anonymous variables. + Individual declarations are then designated by de Bruijn indexes. *) +module Rel = + struct + (** Representation of {e local declarations}. + + [(name, None, typ)] represents a {e local assumption}. + In the Reference Manual we denote them as [(name:typ)]. + + [(name, Some value, typ)] represents a {e local definition}. + In the Reference Manual we denote them as [(name := value : typ)]. + *) + module Declaration = + struct + type t = Name.t * Constr.t option * Constr.t + + (** Map all terms in a given declaration. *) + let map f (n, v, ty) = (n, Option.map f v, f ty) + + (** Reduce all terms in a given declaration to a single value. *) + let fold f (_, v, ty) a = f ty (Option.fold_right f v a) + + (** Check whether any term in a given declaration satisfies a given predicate. *) + let exists f (_, v, ty) = Option.cata f false v || f ty + + (** Check whether all terms in a given declaration satisfy a given predicate. *) + let for_all f (_, v, ty) = Option.cata f true v && f ty + + (** Check whether the two given declarations are equal. *) + let equal (n1, v1, ty1) (n2, v2, ty2) = + Name.equal n1 n2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2 + 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 *) + let empty = [] + + (** Return a new rel-context enriched by with a given inner-most declaration. *) + let add d ctx = d :: 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. *) + let rec lookup n ctx = + match n, ctx with + | 1, decl :: _ -> decl + | n, _ :: sign -> lookup (n-1) sign + | _, [] -> raise Not_found + + (** Map all terms in a given rel-context. *) + let map f = + let map_decl (n, body_o, typ as decl) = + let body_o' = Option.smartmap f body_o in + let typ' = f typ in + if body_o' == body_o && typ' == typ then decl else + (n, body_o', typ') + in + List.smartmap map_decl + + (** Reduce all terms in a given rel-context to a single value. + Innermost declarations are processed first. *) + let fold_inside f ~init = List.fold_left f init + + (** Reduce all terms in a given rel-context to a single value. + Outermost declarations are processed first. *) + let fold_outside f l ~init = List.fold_right f l init + + (** Perform a given action on every declaration in a given rel-context. *) + let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b) + + (** Return the number of {e local declarations} in a given context. *) + let length = List.length + + (** [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 rec nhyps acc = function + | [] -> acc + | (_,None,_)::hyps -> nhyps (1+acc) hyps + | (_,Some _,_)::hyps -> nhyps acc hyps in + nhyps 0 + + (** 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 rec aux l = function + | [] -> l + | (_,Some _,_)::ctx -> aux (true::l) ctx + | (_,None,_)::ctx -> aux (false::l) ctx + in aux [] + + (** [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 rec reln l p = function + | (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps + | (_, Some _, _) :: hyps -> reln l (p+1) hyps + | [] -> l + in + reln [] 1 + + (** [extended_vect n Γ] does the same, returning instead an array. *) + let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps) + end + +(** This module represents contexts that can capture non-anonymous variables. + Individual declarations are then designated by the identifiers they bind. *) +module Named = + struct + (** Representation of {e local declarations}. + + [(id, None, typ)] represents a {e local assumption}. + In the Reference Manual we denote them as [(name:typ)]. + + [(id, Some value, typ)] represents a {e local definition}. + In the Reference Manual we denote them as [(name := value : typ)]. + *) + module Declaration = + struct + (** 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 t = Id.t * Constr.t option * Constr.t + + (** Map all terms in a given declaration. *) + let map = Rel.Declaration.map + + (** Reduce all terms in a given declaration to a single value. *) + let fold f (_, v, ty) a = f ty (Option.fold_right f v a) + + (** Check whether any term in a given declaration satisfies a given predicate. *) + let exists f (_, v, ty) = Option.cata f false v || f ty + + (** Check whether all terms in a given declaration satisfy a given predicate. *) + let for_all f (_, v, ty) = Option.cata f true v && f ty + + (** Check whether the two given declarations are equal. *) + let equal (i1, v1, ty1) (i2, v2, ty2) = + Id.equal i1 i2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2 + end + + type t = Declaration.t list + + (** empty named-context *) + let empty = [] + + (** empty named-context *) + let add d ctx = d :: ctx + + (** 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 + | (id',_,_ as decl) :: _ when Id.equal id id' -> decl + | _ :: sign -> lookup id sign + | [] -> raise Not_found + + (** Map all terms in a given named-context. *) + let map f = + let map_decl (n, body_o, typ as decl) = + let body_o' = Option.smartmap f body_o in + let typ' = f typ in + if body_o' == body_o && typ' == typ then decl else + (n, body_o', typ') + in + List.smartmap map_decl + + (** Reduce all terms in a given named-context to a single value. + Innermost declarations are processed first. *) + let fold_inside f ~init = List.fold_left f init + + (** Reduce all terms in a given named-context to a single value. + Outermost declarations are processed first. *) + let fold_outside f l ~init = List.fold_right f l init + + (** Perform a given action on every declaration in a given named-context. *) + let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b) + + (** Return the number of {e local declarations} in a given named-context. *) + let length = List.length + + (** Check whether given two named-contexts are equal. *) + let equal = List.equal Declaration.equal + + (** Return the set of all identifiers bound in a given named-context. *) + let to_vars = + List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty + + (** [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 filter = function + | (id, None, _) -> Some (Constr.mkVar id) + | (_, Some _, _) -> None + in + List.map_filter filter + end + +module NamedList = + struct + module Declaration = + struct + type t = Id.t list * Constr.t option * Constr.t + let map = Named.Declaration.map + end + type t = Declaration.t list + let fold f l ~init = List.fold_right f l init + 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.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/context.ml') diff --git a/kernel/context.ml b/kernel/context.ml index 796f06d37e..454d4f252d 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -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.ml | 364 ++++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 269 insertions(+), 95 deletions(-) (limited to 'kernel/context.ml') diff --git a/kernel/context.ml b/kernel/context.ml index 3be1e83230..cc1e6f1762 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -33,33 +33,122 @@ open Names Individual declarations are then designated by de Bruijn indexes. *) module Rel = struct - (** Representation of {e local declarations}. - - [(name, None, typ)] represents a {e local assumption}. - In the Reference Manual we denote them as [(name:typ)]. - - [(name, Some value, typ)] represents a {e local definition}. - In the Reference Manual we denote them as [(name := value : typ)]. - *) + (** Representation of {e local declarations}. *) module Declaration = struct - type t = Name.t * Constr.t option * Constr.t - - (** Map all terms in a given declaration. *) - let map f (n, v, ty) = (n, Option.map f v, f ty) - - (** Reduce all terms in a given declaration to a single value. *) - let fold f (_, v, ty) a = f ty (Option.fold_right f v a) + (* local declaration *) + type t = LocalAssum of Name.t * Constr.t (* local assumption *) + | LocalDef of Name.t * Constr.t * Constr.t (* local definition *) + + (** Return the name bound by a given declaration. *) + let get_name = function + | LocalAssum (na,_) + | LocalDef (na,_,_) -> na + + (** Return [Some value] for local-declarations and [None] for local-assumptions. *) + let get_value = function + | LocalAssum _ -> None + | LocalDef (_,v,_) -> Some v + + (** Return the type of the name bound by a given declaration. *) + let get_type = function + | LocalAssum (_,ty) + | LocalDef (_,_,ty) -> ty + + (** Set the name that is bound by a given declaration. *) + let set_name na = function + | LocalAssum (_,ty) -> LocalAssum (na, ty) + | LocalDef (_,v,ty) -> LocalDef (na, v, ty) + + (** Set the type of the bound variable in a given declaration. *) + let set_type ty = function + | LocalAssum (na,_) -> LocalAssum (na, ty) + | LocalDef (na,v,_) -> LocalDef (na, v, ty) + + (** Return [true] iff a given declaration is a local assumption. *) + let is_local_assum = function + | LocalAssum _ -> true + | LocalDef _ -> false + + (** Return [true] iff a given declaration is a local definition. *) + let is_local_def = function + | LocalAssum _ -> false + | LocalDef _ -> true (** Check whether any term in a given declaration satisfies a given predicate. *) - let exists f (_, v, ty) = Option.cata f false v || f ty + let exists f = function + | LocalAssum (_, ty) -> f ty + | LocalDef (_, v, ty) -> f v || f ty (** Check whether all terms in a given declaration satisfy a given predicate. *) - let for_all f (_, v, ty) = Option.cata f true v && f ty + let for_all f = function + | LocalAssum (_, ty) -> f ty + | LocalDef (_, v, ty) -> f v && f ty (** Check whether the two given declarations are equal. *) - let equal (n1, v1, ty1) (n2, v2, ty2) = - Name.equal n1 n2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2 + let equal decl1 decl2 = + match decl1, decl2 with + | LocalAssum (n1,ty1), LocalAssum (n2, ty2) -> + Name.equal n1 n2 && Constr.equal ty1 ty2 + | LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) -> + Name.equal n1 n2 && Constr.equal v1 v2 && Constr.equal ty1 ty2 + | _ -> + false + + (** Map the name bound by a given declaration. *) + let map_name f = function + | LocalAssum (na, ty) as decl -> + let na' = f na in + if na == na' then decl else LocalAssum (na', ty) + | LocalDef (na, v, ty) as decl -> + let na' = f na in + if na == na' then decl else LocalDef (na', v, ty) + + (** For local assumptions, this function returns the original local assumptions. + For local definitions, this function maps the value in the local definition. *) + let map_value f = function + | LocalAssum _ as decl -> decl + | LocalDef (na, v, t) as decl -> + let v' = f v in + if v == v' then decl else LocalDef (na, v', t) + + (** Map the type of the name bound by a given declaration. *) + let map_type f = function + | LocalAssum (na, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalAssum (na, ty') + | LocalDef (na, v, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalDef (na, v, ty') + + (** Map all terms in a given declaration. *) + let map_constr f = function + | LocalAssum (na, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalAssum (na, ty') + | LocalDef (na, v, ty) as decl -> + let v' = f v in + let ty' = f ty in + if v == v' && ty == ty' then decl else LocalDef (na, v', ty') + + (** Perform a given action on all terms in a given declaration. *) + let iter_constr f = function + | LocalAssum (_,ty) -> f ty + | LocalDef (_,v,ty) -> f v; f ty + + (** Reduce all terms in a given declaration to a single value. *) + let fold f decl acc = + match decl with + | LocalAssum (n,ty) -> f ty acc + | LocalDef (n,v,ty) -> f ty (f v acc) + + let to_tuple = function + | 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. @@ -73,6 +162,21 @@ module Rel = (** Return a new rel-context enriched by with a given inner-most declaration. *) let add d ctx = d :: ctx + (** Return the number of {e local declarations} in a given context. *) + let length = List.length + + (** [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 open Declaration in + let rec nhyps acc = function + | [] -> acc + | LocalAssum _ :: hyps -> nhyps (succ acc) hyps + | LocalDef _ :: hyps -> nhyps acc hyps + in + nhyps 0 + (** 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. *) let rec lookup n ctx = @@ -81,15 +185,14 @@ module Rel = | n, _ :: sign -> lookup (n-1) sign | _, [] -> raise Not_found + (** Check whether given two rel-contexts are equal. *) + let equal = List.equal Declaration.equal + (** Map all terms in a given rel-context. *) - let map f = - let map_decl (n, body_o, typ as decl) = - let body_o' = Option.smartmap f body_o in - let typ' = f typ in - if body_o' == body_o && typ' == typ then decl else - (n, body_o', typ') - in - List.smartmap map_decl + let map f = List.smartmap (Declaration.map_constr f) + + (** Perform a given action on every declaration in a given rel-context. *) + let iter f = List.iter (Declaration.iter_constr f) (** Reduce all terms in a given rel-context to a single value. Innermost declarations are processed first. *) @@ -99,29 +202,13 @@ module Rel = Outermost declarations are processed first. *) let fold_outside f l ~init = List.fold_right f l init - (** Perform a given action on every declaration in a given rel-context. *) - let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b) - - (** Return the number of {e local declarations} in a given context. *) - let length = List.length - - (** [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 rec nhyps acc = function - | [] -> acc - | (_,None,_)::hyps -> nhyps (1+acc) hyps - | (_,Some _,_)::hyps -> nhyps acc hyps in - nhyps 0 - (** 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 rec aux l = function | [] -> l - | (_,Some _,_)::ctx -> aux (true::l) ctx - | (_,None,_)::ctx -> aux (false::l) ctx + | Declaration.LocalDef _ :: ctx -> aux (true::l) ctx + | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx in aux [] (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] @@ -129,8 +216,8 @@ module Rel = [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) let to_extended_list n = let rec reln l p = function - | (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps - | (_, Some _, _) :: hyps -> reln l (p+1) hyps + | Declaration.LocalAssum _ :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps + | Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps | [] -> l in reln [] 1 @@ -143,38 +230,127 @@ module Rel = Individual declarations are then designated by the identifiers they bind. *) module Named = struct - (** Representation of {e local declarations}. - - [(id, None, typ)] represents a {e local assumption}. - In the Reference Manual we denote them as [(name:typ)]. - - [(id, Some value, typ)] represents a {e local definition}. - In the Reference Manual we denote them as [(name := value : typ)]. - *) + (** Representation of {e local declarations}. *) module Declaration = struct - (** 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 t = Id.t * Constr.t option * Constr.t - - (** Map all terms in a given declaration. *) - let map = Rel.Declaration.map - - (** Reduce all terms in a given declaration to a single value. *) - let fold f (_, v, ty) a = f ty (Option.fold_right f v a) + (** local declaration *) + type t = LocalAssum of Id.t * Constr.t + | LocalDef of Id.t * Constr.t * Constr.t + + (** Return the identifier bound by a given declaration. *) + let get_id = function + | LocalAssum (id,_) -> id + | LocalDef (id,_,_) -> id + + (** Return [Some value] for local-declarations and [None] for local-assumptions. *) + let get_value = function + | LocalAssum _ -> None + | LocalDef (_,v,_) -> Some v + + (** Return the type of the name bound by a given declaration. *) + let get_type = function + | LocalAssum (_,ty) + | LocalDef (_,_,ty) -> ty + + (** Set the identifier that is bound by a given declaration. *) + let set_id id = function + | LocalAssum (_,ty) -> LocalAssum (id, ty) + | LocalDef (_, v, ty) -> LocalDef (id, v, ty) + + (** Set the type of the bound variable in a given declaration. *) + let set_type ty = function + | LocalAssum (id,_) -> LocalAssum (id, ty) + | LocalDef (id,v,_) -> LocalDef (id, v, ty) + + (** Return [true] iff a given declaration is a local assumption. *) + let is_local_assum = function + | LocalAssum _ -> true + | LocalDef _ -> false + + (** Return [true] iff a given declaration is a local definition. *) + let is_local_def = function + | LocalDef _ -> true + | LocalAssum _ -> false (** Check whether any term in a given declaration satisfies a given predicate. *) - let exists f (_, v, ty) = Option.cata f false v || f ty + let exists f = function + | LocalAssum (_, ty) -> f ty + | LocalDef (_, v, ty) -> f v || f ty (** Check whether all terms in a given declaration satisfy a given predicate. *) - let for_all f (_, v, ty) = Option.cata f true v && f ty + let for_all f = function + | LocalAssum (_, ty) -> f ty + | LocalDef (_, v, ty) -> f v && f ty (** Check whether the two given declarations are equal. *) - let equal (i1, v1, ty1) (i2, v2, ty2) = - Id.equal i1 i2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2 + let equal decl1 decl2 = + match decl1, decl2 with + | LocalAssum (id1, ty1), LocalAssum (id2, ty2) -> + Id.equal id1 id2 && Constr.equal ty1 ty2 + | LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) -> + Id.equal id1 id2 && Constr.equal v1 v2 && Constr.equal ty1 ty2 + | _ -> + false + + (** Map the identifier bound by a given declaration. *) + let map_id f = function + | LocalAssum (id, ty) as decl -> + let id' = f id in + if id == id' then decl else LocalAssum (id', ty) + | LocalDef (id, v, ty) as decl -> + let id' = f id in + if id == id' then decl else LocalDef (id', v, ty) + + (** For local assumptions, this function returns the original local assumptions. + For local definitions, this function maps the value in the local definition. *) + let map_value f = function + | LocalAssum _ as decl -> decl + | LocalDef (na, v, t) as decl -> + let v' = f v in + if v == v' then decl else LocalDef (na, v', t) + + (** Map the type of the name bound by a given declaration. *) + let map_type f = function + | LocalAssum (id, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalAssum (id, ty') + | LocalDef (id, v, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalDef (id, v, ty') + + (** Map all terms in a given declaration. *) + let map_constr f = function + | LocalAssum (id, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalAssum (id, ty') + | LocalDef (id, v, ty) as decl -> + let v' = f v in + let ty' = f ty in + if v == v' && ty == ty' then decl else LocalDef (id, v', ty') + + (** Perform a given action on all terms in a given declaration. *) + let iter_constr f = function + | LocalAssum (_, ty) -> f ty + | LocalDef (_, v, ty) -> f v; f ty + + (** Reduce all terms in a given declaration to a single value. *) + let fold f decl a = + match decl with + | LocalAssum (_, ty) -> f ty a + | LocalDef (_, v, ty) -> a |> f v |> f ty + + let to_tuple = function + | LocalAssum (id, ty) -> id, None, ty + | LocalDef (id, v, ty) -> id, Some v, ty + + let of_tuple = function + | id, None, ty -> LocalAssum (id, ty) + | id, Some v, ty -> LocalDef (id, v, ty) 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 t = Declaration.t list (** empty named-context *) @@ -183,22 +359,23 @@ module Named = (** empty named-context *) let add d ctx = d :: ctx + (** 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 - | (id',_,_ as decl) :: _ when Id.equal id id' -> decl - | _ :: sign -> lookup id sign - | [] -> raise Not_found + @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 (** Map all terms in a given named-context. *) - let map f = - let map_decl (n, body_o, typ as decl) = - let body_o' = Option.smartmap f body_o in - let typ' = f typ in - if body_o' == body_o && typ' == typ then decl else - (n, body_o', typ') - in - List.smartmap map_decl + let map f = List.smartmap (Declaration.map_constr f) + + (** Perform a given action on every declaration in a given named-context. *) + let iter f = List.iter (Declaration.iter_constr f) (** Reduce all terms in a given named-context to a single value. Innermost declarations are processed first. *) @@ -208,18 +385,9 @@ module Named = Outermost declarations are processed first. *) let fold_outside f l ~init = List.fold_right f l init - (** Perform a given action on every declaration in a given named-context. *) - let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b) - - (** Return the number of {e local declarations} in a given named-context. *) - let length = List.length - - (** Check whether given two named-contexts are equal. *) - let equal = List.equal Declaration.equal - (** Return the set of all identifiers bound in a given named-context. *) let to_vars = - List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty + List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty (** [instance_from_named_context Ω] builds an instance [args] such that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local @@ -227,8 +395,8 @@ module Named = gives [Var id1, Var id3]. All [idj] are supposed distinct. *) let to_instance = let filter = function - | (id, None, _) -> Some (Constr.mkVar id) - | (_, Some _, _) -> None + | Declaration.LocalAssum (id, _) -> Some (Constr.mkVar id) + | _ -> None in List.map_filter filter end @@ -238,9 +406,15 @@ module NamedList = module Declaration = struct type t = Id.t list * Constr.t option * Constr.t - let map = Named.Declaration.map + + 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') end + type t = Declaration.t list + let fold f l ~init = List.fold_right f l init end -- 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.ml | 718 +++++++++++++++++++++++++++--------------------------- 1 file changed, 360 insertions(+), 358 deletions(-) (limited to 'kernel/context.ml') diff --git a/kernel/context.ml b/kernel/context.ml index cc1e6f1762..4e53b73a28 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -32,380 +32,382 @@ open Names (** Representation of contexts that can capture anonymous as well as non-anonymous variables. Individual declarations are then designated by de Bruijn indexes. *) module Rel = +struct + (** Representation of {e local declarations}. *) + module Declaration = struct - (** Representation of {e local declarations}. *) - module Declaration = - struct - (* local declaration *) - type t = LocalAssum of Name.t * Constr.t (* local assumption *) - | LocalDef of Name.t * Constr.t * Constr.t (* local definition *) - - (** Return the name bound by a given declaration. *) - let get_name = function - | LocalAssum (na,_) - | LocalDef (na,_,_) -> na - - (** Return [Some value] for local-declarations and [None] for local-assumptions. *) - let get_value = function - | LocalAssum _ -> None - | LocalDef (_,v,_) -> Some v - - (** Return the type of the name bound by a given declaration. *) - let get_type = function - | LocalAssum (_,ty) - | LocalDef (_,_,ty) -> ty - - (** Set the name that is bound by a given declaration. *) - let set_name na = function - | LocalAssum (_,ty) -> LocalAssum (na, ty) - | LocalDef (_,v,ty) -> LocalDef (na, v, ty) - - (** Set the type of the bound variable in a given declaration. *) - let set_type ty = function - | LocalAssum (na,_) -> LocalAssum (na, ty) - | LocalDef (na,v,_) -> LocalDef (na, v, ty) - - (** Return [true] iff a given declaration is a local assumption. *) - let is_local_assum = function - | LocalAssum _ -> true - | LocalDef _ -> false - - (** Return [true] iff a given declaration is a local definition. *) - let is_local_def = function - | LocalAssum _ -> false - | LocalDef _ -> true - - (** Check whether any term in a given declaration satisfies a given predicate. *) - let exists f = function - | LocalAssum (_, ty) -> f ty - | LocalDef (_, v, ty) -> f v || f ty - - (** Check whether all terms in a given declaration satisfy a given predicate. *) - let for_all f = function - | LocalAssum (_, ty) -> f ty - | LocalDef (_, v, ty) -> f v && f ty - - (** Check whether the two given declarations are equal. *) - let equal decl1 decl2 = - match decl1, decl2 with - | LocalAssum (n1,ty1), LocalAssum (n2, ty2) -> - Name.equal n1 n2 && Constr.equal ty1 ty2 - | LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) -> - Name.equal n1 n2 && Constr.equal v1 v2 && Constr.equal ty1 ty2 - | _ -> - false - - (** Map the name bound by a given declaration. *) - let map_name f = function - | LocalAssum (na, ty) as decl -> - let na' = f na in - if na == na' then decl else LocalAssum (na', ty) - | LocalDef (na, v, ty) as decl -> - let na' = f na in - if na == na' then decl else LocalDef (na', v, ty) - - (** For local assumptions, this function returns the original local assumptions. - For local definitions, this function maps the value in the local definition. *) - let map_value f = function - | LocalAssum _ as decl -> decl - | LocalDef (na, v, t) as decl -> - let v' = f v in - if v == v' then decl else LocalDef (na, v', t) - - (** Map the type of the name bound by a given declaration. *) - let map_type f = function - | LocalAssum (na, ty) as decl -> - let ty' = f ty in - if ty == ty' then decl else LocalAssum (na, ty') - | LocalDef (na, v, ty) as decl -> - let ty' = f ty in - if ty == ty' then decl else LocalDef (na, v, ty') - - (** Map all terms in a given declaration. *) - let map_constr f = function - | LocalAssum (na, ty) as decl -> - let ty' = f ty in - if ty == ty' then decl else LocalAssum (na, ty') - | LocalDef (na, v, ty) as decl -> - let v' = f v in - let ty' = f ty in - if v == v' && ty == ty' then decl else LocalDef (na, v', ty') - - (** Perform a given action on all terms in a given declaration. *) - let iter_constr f = function - | LocalAssum (_,ty) -> f ty - | LocalDef (_,v,ty) -> f v; f ty - - (** Reduce all terms in a given declaration to a single value. *) - let fold f decl acc = - match decl with - | LocalAssum (n,ty) -> f ty acc - | LocalDef (n,v,ty) -> f ty (f v acc) - - let to_tuple = function - | 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 t = Declaration.t list + (* local declaration *) + 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. *) + let get_name = function + | LocalAssum (na,_) + | LocalDef (na,_,_) -> na + + (** Return [Some value] for local-declarations and [None] for local-assumptions. *) + let get_value = function + | LocalAssum _ -> None + | LocalDef (_,v,_) -> Some v + + (** Return the type of the name bound by a given declaration. *) + let get_type = function + | LocalAssum (_,ty) + | LocalDef (_,_,ty) -> ty + + (** Set the name that is bound by a given declaration. *) + let set_name na = function + | LocalAssum (_,ty) -> LocalAssum (na, ty) + | LocalDef (_,v,ty) -> LocalDef (na, v, ty) + + (** Set the type of the bound variable in a given declaration. *) + let set_type ty = function + | LocalAssum (na,_) -> LocalAssum (na, ty) + | LocalDef (na,v,_) -> LocalDef (na, v, ty) + + (** Return [true] iff a given declaration is a local assumption. *) + let is_local_assum = function + | LocalAssum _ -> true + | LocalDef _ -> false + + (** Return [true] iff a given declaration is a local definition. *) + let is_local_def = function + | LocalAssum _ -> false + | LocalDef _ -> true + + (** Check whether any term in a given declaration satisfies a given predicate. *) + let exists f = function + | LocalAssum (_, ty) -> f ty + | LocalDef (_, v, ty) -> f v || f ty + + (** Check whether all terms in a given declaration satisfy a given predicate. *) + let for_all f = function + | LocalAssum (_, ty) -> f ty + | LocalDef (_, v, ty) -> f v && f ty + + (** Check whether the two given declarations are equal. *) + let equal decl1 decl2 = + match decl1, decl2 with + | LocalAssum (n1,ty1), LocalAssum (n2, ty2) -> + Name.equal n1 n2 && Constr.equal ty1 ty2 + | LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) -> + Name.equal n1 n2 && Constr.equal v1 v2 && Constr.equal ty1 ty2 + | _ -> + false + + (** Map the name bound by a given declaration. *) + let map_name f = function + | LocalAssum (na, ty) as decl -> + let na' = f na in + if na == na' then decl else LocalAssum (na', ty) + | LocalDef (na, v, ty) as decl -> + let na' = f na in + if na == na' then decl else LocalDef (na', v, ty) + + (** For local assumptions, this function returns the original local assumptions. + For local definitions, this function maps the value in the local definition. *) + let map_value f = function + | LocalAssum _ as decl -> decl + | LocalDef (na, v, t) as decl -> + let v' = f v in + if v == v' then decl else LocalDef (na, v', t) + + (** Map the type of the name bound by a given declaration. *) + let map_type f = function + | LocalAssum (na, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalAssum (na, ty') + | LocalDef (na, v, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalDef (na, v, ty') - (** empty rel-context *) - let empty = [] - - (** Return a new rel-context enriched by with a given inner-most declaration. *) - let add d ctx = d :: ctx - - (** Return the number of {e local declarations} in a given context. *) - let length = List.length - - (** [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 open Declaration in - let rec nhyps acc = function - | [] -> acc - | LocalAssum _ :: hyps -> nhyps (succ acc) hyps - | LocalDef _ :: hyps -> nhyps acc hyps - in - nhyps 0 - - (** 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. *) - let rec lookup n ctx = - match n, ctx with - | 1, decl :: _ -> decl - | n, _ :: sign -> lookup (n-1) sign - | _, [] -> raise Not_found - - (** Check whether given two rel-contexts are equal. *) - let equal = List.equal Declaration.equal - - (** Map all terms in a given rel-context. *) - let map f = List.smartmap (Declaration.map_constr f) - - (** Perform a given action on every declaration in a given rel-context. *) - let iter f = List.iter (Declaration.iter_constr f) - - (** Reduce all terms in a given rel-context to a single value. - Innermost declarations are processed first. *) - let fold_inside f ~init = List.fold_left f init - - (** Reduce all terms in a given rel-context to a single value. - Outermost declarations are processed first. *) - let fold_outside f l ~init = List.fold_right f l init - - (** 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 rec aux l = function - | [] -> l - | Declaration.LocalDef _ :: ctx -> aux (true::l) ctx - | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx - in aux [] - - (** [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 rec reln l p = function - | Declaration.LocalAssum _ :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps - | Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps - | [] -> l - in - reln [] 1 - - (** [extended_vect n Γ] does the same, returning instead an array. *) - let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps) + (** Map all terms in a given declaration. *) + let map_constr f = function + | LocalAssum (na, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalAssum (na, ty') + | LocalDef (na, v, ty) as decl -> + let v' = f v in + let ty' = f ty in + if v == v' && ty == ty' then decl else LocalDef (na, v', ty') + + (** Perform a given action on all terms in a given declaration. *) + let iter_constr f = function + | LocalAssum (_,ty) -> f ty + | LocalDef (_,v,ty) -> f v; f ty + + (** Reduce all terms in a given declaration to a single value. *) + let fold f decl acc = + match decl with + | LocalAssum (n,ty) -> f ty acc + | LocalDef (n,v,ty) -> f ty (f v acc) + + let to_tuple = function + | 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 t = Declaration.t list + + (** empty rel-context *) + let empty = [] + + (** Return a new rel-context enriched by with a given inner-most declaration. *) + let add d ctx = d :: ctx + + (** Return the number of {e local declarations} in a given context. *) + let length = List.length + + (** [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 open Declaration in + let rec nhyps acc = function + | [] -> acc + | LocalAssum _ :: hyps -> nhyps (succ acc) hyps + | LocalDef _ :: hyps -> nhyps acc hyps + in + nhyps 0 + + (** 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. *) + let rec lookup n ctx = + match n, ctx with + | 1, decl :: _ -> decl + | n, _ :: sign -> lookup (n-1) sign + | _, [] -> raise Not_found + + (** Check whether given two rel-contexts are equal. *) + let equal = List.equal Declaration.equal + + (** Map all terms in a given rel-context. *) + let map f = List.smartmap (Declaration.map_constr f) + + (** Perform a given action on every declaration in a given rel-context. *) + let iter f = List.iter (Declaration.iter_constr f) + + (** Reduce all terms in a given rel-context to a single value. + Innermost declarations are processed first. *) + let fold_inside f ~init = List.fold_left f init + + (** Reduce all terms in a given rel-context to a single value. + Outermost declarations are processed first. *) + let fold_outside f l ~init = List.fold_right f l init + + (** 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 rec aux l = function + | [] -> l + | Declaration.LocalDef _ :: ctx -> aux (true::l) ctx + | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx + in aux [] + + (** [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 rec reln l p = function + | Declaration.LocalAssum _ :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps + | Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps + | [] -> l + in + reln [] 1 + + (** [extended_vect n Γ] does the same, returning instead an array. *) + let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps) +end + (** This module represents contexts that can capture non-anonymous variables. Individual declarations are then designated by the identifiers they bind. *) module Named = +struct + (** Representation of {e local declarations}. *) + module Declaration = struct - (** Representation of {e local declarations}. *) - module Declaration = - struct - (** local declaration *) - type t = LocalAssum of Id.t * Constr.t - | LocalDef of Id.t * Constr.t * Constr.t - - (** Return the identifier bound by a given declaration. *) - let get_id = function - | LocalAssum (id,_) -> id - | LocalDef (id,_,_) -> id - - (** Return [Some value] for local-declarations and [None] for local-assumptions. *) - let get_value = function - | LocalAssum _ -> None - | LocalDef (_,v,_) -> Some v - - (** Return the type of the name bound by a given declaration. *) - let get_type = function - | LocalAssum (_,ty) - | LocalDef (_,_,ty) -> ty - - (** Set the identifier that is bound by a given declaration. *) - let set_id id = function - | LocalAssum (_,ty) -> LocalAssum (id, ty) - | LocalDef (_, v, ty) -> LocalDef (id, v, ty) - - (** Set the type of the bound variable in a given declaration. *) - let set_type ty = function - | LocalAssum (id,_) -> LocalAssum (id, ty) - | LocalDef (id,v,_) -> LocalDef (id, v, ty) - - (** Return [true] iff a given declaration is a local assumption. *) - let is_local_assum = function - | LocalAssum _ -> true - | LocalDef _ -> false - - (** Return [true] iff a given declaration is a local definition. *) - let is_local_def = function - | LocalDef _ -> true - | LocalAssum _ -> false - - (** Check whether any term in a given declaration satisfies a given predicate. *) - let exists f = function - | LocalAssum (_, ty) -> f ty - | LocalDef (_, v, ty) -> f v || f ty - - (** Check whether all terms in a given declaration satisfy a given predicate. *) - let for_all f = function - | LocalAssum (_, ty) -> f ty - | LocalDef (_, v, ty) -> f v && f ty - - (** Check whether the two given declarations are equal. *) - let equal decl1 decl2 = - match decl1, decl2 with - | LocalAssum (id1, ty1), LocalAssum (id2, ty2) -> - Id.equal id1 id2 && Constr.equal ty1 ty2 - | LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) -> - Id.equal id1 id2 && Constr.equal v1 v2 && Constr.equal ty1 ty2 - | _ -> - false - - (** Map the identifier bound by a given declaration. *) - let map_id f = function - | LocalAssum (id, ty) as decl -> - let id' = f id in - if id == id' then decl else LocalAssum (id', ty) - | LocalDef (id, v, ty) as decl -> - let id' = f id in - if id == id' then decl else LocalDef (id', v, ty) - - (** For local assumptions, this function returns the original local assumptions. - For local definitions, this function maps the value in the local definition. *) - let map_value f = function - | LocalAssum _ as decl -> decl - | LocalDef (na, v, t) as decl -> - let v' = f v in - if v == v' then decl else LocalDef (na, v', t) - - (** Map the type of the name bound by a given declaration. *) - let map_type f = function - | LocalAssum (id, ty) as decl -> - let ty' = f ty in - if ty == ty' then decl else LocalAssum (id, ty') - | LocalDef (id, v, ty) as decl -> - let ty' = f ty in - if ty == ty' then decl else LocalDef (id, v, ty') - - (** Map all terms in a given declaration. *) - let map_constr f = function - | LocalAssum (id, ty) as decl -> - let ty' = f ty in - if ty == ty' then decl else LocalAssum (id, ty') - | LocalDef (id, v, ty) as decl -> - let v' = f v in - let ty' = f ty in - if v == v' && ty == ty' then decl else LocalDef (id, v', ty') - - (** Perform a given action on all terms in a given declaration. *) - let iter_constr f = function - | LocalAssum (_, ty) -> f ty - | LocalDef (_, v, ty) -> f v; f ty - - (** Reduce all terms in a given declaration to a single value. *) - let fold f decl a = - match decl with - | LocalAssum (_, ty) -> f ty a - | LocalDef (_, v, ty) -> a |> f v |> f ty - - let to_tuple = function - | LocalAssum (id, ty) -> id, None, ty - | LocalDef (id, v, ty) -> id, Some v, ty - - let of_tuple = function - | id, None, ty -> LocalAssum (id, ty) - | id, Some v, ty -> LocalDef (id, v, ty) - 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 t = Declaration.t list - - (** empty named-context *) - let empty = [] - - (** empty named-context *) - let add d ctx = d :: ctx - - (** 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 - | 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 - - (** Map all terms in a given named-context. *) - let map f = List.smartmap (Declaration.map_constr f) - - (** Perform a given action on every declaration in a given named-context. *) - let iter f = List.iter (Declaration.iter_constr f) - - (** Reduce all terms in a given named-context to a single value. - Innermost declarations are processed first. *) - let fold_inside f ~init = List.fold_left f init - - (** Reduce all terms in a given named-context to a single value. - Outermost declarations are processed first. *) - let fold_outside f l ~init = List.fold_right f l init + (** local declaration *) + 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. *) + let get_id = function + | LocalAssum (id,_) -> id + | LocalDef (id,_,_) -> id + + (** Return [Some value] for local-declarations and [None] for local-assumptions. *) + let get_value = function + | LocalAssum _ -> None + | LocalDef (_,v,_) -> Some v + + (** Return the type of the name bound by a given declaration. *) + let get_type = function + | LocalAssum (_,ty) + | LocalDef (_,_,ty) -> ty + + (** Set the identifier that is bound by a given declaration. *) + let set_id id = function + | LocalAssum (_,ty) -> LocalAssum (id, ty) + | LocalDef (_, v, ty) -> LocalDef (id, v, ty) + + (** Set the type of the bound variable in a given declaration. *) + let set_type ty = function + | LocalAssum (id,_) -> LocalAssum (id, ty) + | LocalDef (id,v,_) -> LocalDef (id, v, ty) + + (** Return [true] iff a given declaration is a local assumption. *) + let is_local_assum = function + | LocalAssum _ -> true + | LocalDef _ -> false + + (** Return [true] iff a given declaration is a local definition. *) + let is_local_def = function + | LocalDef _ -> true + | LocalAssum _ -> false + + (** Check whether any term in a given declaration satisfies a given predicate. *) + let exists f = function + | LocalAssum (_, ty) -> f ty + | LocalDef (_, v, ty) -> f v || f ty + + (** Check whether all terms in a given declaration satisfy a given predicate. *) + let for_all f = function + | LocalAssum (_, ty) -> f ty + | LocalDef (_, v, ty) -> f v && f ty + + (** Check whether the two given declarations are equal. *) + let equal decl1 decl2 = + match decl1, decl2 with + | LocalAssum (id1, ty1), LocalAssum (id2, ty2) -> + Id.equal id1 id2 && Constr.equal ty1 ty2 + | LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) -> + Id.equal id1 id2 && Constr.equal v1 v2 && Constr.equal ty1 ty2 + | _ -> + false + + (** Map the identifier bound by a given declaration. *) + let map_id f = function + | LocalAssum (id, ty) as decl -> + let id' = f id in + if id == id' then decl else LocalAssum (id', ty) + | LocalDef (id, v, ty) as decl -> + let id' = f id in + if id == id' then decl else LocalDef (id', v, ty) + + (** For local assumptions, this function returns the original local assumptions. + For local definitions, this function maps the value in the local definition. *) + let map_value f = function + | LocalAssum _ as decl -> decl + | LocalDef (na, v, t) as decl -> + let v' = f v in + if v == v' then decl else LocalDef (na, v', t) + + (** Map the type of the name bound by a given declaration. *) + let map_type f = function + | LocalAssum (id, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalAssum (id, ty') + | LocalDef (id, v, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalDef (id, v, ty') - (** 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 + (** Map all terms in a given declaration. *) + let map_constr f = function + | LocalAssum (id, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalAssum (id, ty') + | LocalDef (id, v, ty) as decl -> + let v' = f v in + let ty' = f ty in + if v == v' && ty == ty' then decl else LocalDef (id, v', ty') + + (** Perform a given action on all terms in a given declaration. *) + let iter_constr f = function + | LocalAssum (_, ty) -> f ty + | LocalDef (_, v, ty) -> f v; f ty + + (** Reduce all terms in a given declaration to a single value. *) + let fold f decl a = + match decl with + | LocalAssum (_, ty) -> f ty a + | LocalDef (_, v, ty) -> a |> f v |> f ty + + let to_tuple = function + | LocalAssum (id, ty) -> id, None, ty + | LocalDef (id, v, ty) -> id, Some v, ty + + let of_tuple = function + | id, None, ty -> LocalAssum (id, ty) + | id, Some v, ty -> LocalDef (id, v, ty) + end - (** [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 filter = function - | Declaration.LocalAssum (id, _) -> Some (Constr.mkVar id) - | _ -> None - in - List.map_filter filter + (** 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 t = Declaration.t list + + (** empty named-context *) + let empty = [] + + (** empty named-context *) + let add d ctx = d :: ctx + + (** 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 + | 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 + + (** Map all terms in a given named-context. *) + let map f = List.smartmap (Declaration.map_constr f) + + (** Perform a given action on every declaration in a given named-context. *) + let iter f = List.iter (Declaration.iter_constr f) + + (** Reduce all terms in a given named-context to a single value. + Innermost declarations are processed first. *) + let fold_inside f ~init = List.fold_left f init + + (** Reduce all terms in a given named-context to a single value. + Outermost declarations are processed first. *) + 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 + + (** [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 filter = function + | Declaration.LocalAssum (id, _) -> Some (Constr.mkVar id) + | _ -> None + in + List.map_filter filter end module NamedList = struct module Declaration = struct - type t = Id.t list * Constr.t option * Constr.t + 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 -- cgit v1.2.3