diff options
Diffstat (limited to 'kernel/context.ml')
| -rw-r--r-- | kernel/context.ml | 518 |
1 files changed, 402 insertions, 116 deletions
diff --git a/kernel/context.ml b/kernel/context.ml index 454d4f25..4e53b73a 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -15,123 +15,409 @@ (* 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 +(** The modules defined below represent a {e local context} + as defined by Chapter 4 in the Reference Manual: -let rec lookup_rel n sign = - match n, sign with - | 1, decl :: _ -> decl - | n, _ :: sign -> lookup_rel (n-1) sign - | _, [] -> raise Not_found + A {e local context} is an ordered list of of {e local declarations} + of names that we call {e variables}. -let rel_context_length = List.length + A {e local declaration} of some variable can be either: + - a {e local assumption}, or + - a {e local definition}. +*) -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 - -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 - -(*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 - -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}. *) + 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 *) + + (** 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 + + (** 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 + (** 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') + + (** 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 + + (** 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 + + 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 + +type section_context = Named.t |