Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * 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 rebuilding of Coq around a purely functional abstract type-checker, Aug 1999 *)(* Miscellaneous extensions, restructurations and bug-fixes by Hugo Herbelin and Bruno Barras *)
(* This file defines types and combinators regarding indexes-based and names-based contexts *)
(** The modules defined below represent a {e local context} as defined by Chapter 4 in the Reference Manual:
A {e local context} is an ordered list of of {e local declarations} of names that we call {e variables}.
A {e local declaration} of some variable can be either: - a {e local assumption}, or - a {e local definition}.*)
open Utilopen Names
type ('a,'r) pbinder_annot = { binder_name : 'a; binder_relevance : 'r }
let eq_annot eq eqr {binder_name=na1;binder_relevance=r1} {binder_name=na2;binder_relevance=r2} = eq na1 na2 && eqr r1 r2
let hash_annot h {binder_name=n;binder_relevance=r} = Hashset.Combine.combinesmall (Sorts.relevance_hash r) (h n)
let map_annot f {binder_name=na;binder_relevance} = let na' = f na in {binder_name=na';binder_relevance}
let map_annot_relevance fr ({binder_name=na;binder_relevance=r} as a) = let r' = fr r in if r == r' then a else {binder_name=na;binder_relevance=r'}
let map_annot_relevance_het fr {binder_name=na;binder_relevance=r} = let r' = fr r in {binder_name=na;binder_relevance=r'}
let make_annot x r = {binder_name=x;binder_relevance=r}
let binder_name x = x.binder_namelet binder_relevance x = x.binder_relevance
let annotR x = make_annot x Sorts.Relevant
let nameR x = annotR (Name x)let anonR = annotR Anonymous
(** 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 ('constr, 'types, 'r) pt = | LocalAssum of (Name.t,'r) pbinder_annot * 'types (** name, type *) | LocalDef of (Name.t,'r) pbinder_annot * 'constr * 'types (** name, value, type *)
let get_annot = function | LocalAssum (na,_) | LocalDef (na,_,_) -> na
(** Return the name bound by a given declaration. *) let get_name x = (get_annot x).binder_name
(** 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
let get_relevance x = (get_annot x).binder_relevance
let set_annot x d = if get_annot d == x then d else match d with | LocalAssum (_,ty) -> LocalAssum (x, ty) | LocalDef (_,v,ty) -> LocalDef (x, v, ty)
(** Set the name that is bound by a given declaration. *) let set_name na = function | LocalAssum (x,ty) -> LocalAssum ({x with binder_name=na}, ty) | LocalDef (x,v,ty) -> LocalDef ({x with binder_name=na}, v, ty)
let set_relevance r = function | LocalAssum (x,ty) -> LocalAssum ({x with binder_relevance=r}, ty) | LocalDef (x,v,ty) -> LocalDef ({x with binder_relevance=r}, 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 eqr eq decl1 decl2 = match decl1, decl2 with | LocalAssum (n1,ty1), LocalAssum (n2, ty2) -> eq_annot Name.equal eqr n1 n2 && eq ty1 ty2 | LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) -> eq_annot Name.equal eqr n1 n2 && eq v1 v2 && eq ty1 ty2 | _ -> false
(** Map the name bound by a given declaration. *) let map_name f x = let na = get_name x in let na' = f na in if na == na' then x else set_name na' x
let map_relevance f x = let r = get_relevance x in let r' = f r in if r == r' then x else set_relevance r' x
(** 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')
(** Map all terms in a given declaration. *) let map_constr_with_relevance g f = function | LocalAssum (na, ty) as decl -> let na' = map_annot_relevance g na in let ty' = f ty in if na == na' && ty == ty' then decl else LocalAssum (na', ty') | LocalDef (na, v, ty) as decl -> let na' = map_annot_relevance g na in let v' = f v in let ty' = f ty in if na == na' && v == v' && ty == ty' then decl else LocalDef (na', v', ty')
let map_constr_het fr f = function | LocalAssum (na, ty) -> let ty' = f ty in LocalAssum (map_annot_relevance_het fr na, ty') | LocalDef (na, v, ty) -> let v' = f v in let ty' = f ty in LocalDef (map_annot_relevance_het fr 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_constr 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 drop_body = function | LocalAssum _ as d -> d | LocalDef (na, _v, ty) -> LocalAssum (na, 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, 'r) pt = ('constr, 'types, 'r) Declaration.pt 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 rel-context. *) let length = List.length
(** Return the number of {e local assumptions} in a given rel-context. *) 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 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
(** Check whether given two rel-contexts are equal. *) let equal eqr eq l = List.equal (fun c -> Declaration.equal eqr eq c) l
(** Map all terms in a given rel-context. *) let map f = List.Smart.map (Declaration.map_constr f)
let map_with_relevance g f = List.Smart.map (Declaration.map_constr_with_relevance g f)
let map_het fr f = List.map (Declaration.map_constr_het fr f)
(** Map all terms in a given rel-context. *) let map_with_binders f ctx = let rec aux k = function | decl :: ctx as l -> let decl' = Declaration.map_constr (f k) decl in let ctx' = aux (k-1) ctx in if decl == decl' && ctx == ctx' then l else decl' :: ctx' | [] -> [] in aux (length ctx) ctx
(** 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
(** Return the set of all named variables bound in a given rel-context. *) let to_vars l = List.fold_left (fun accu decl -> match Declaration.get_name decl with | Name id -> Id.Set.add id accu | Anonymous -> accu) Id.Set.empty l
(** Map a given rel-context to a list where each {e local definition} is mapped to [true] and each {e local assumption} is mapped to [false]. *) 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 [] l
let drop_bodies l = List.Smart.map Declaration.drop_body l
(** Split a context so that the second part contains [n] [LocalAssum], keeping all [LocalDef] in the middle in the first part *) let chop_nhyps n l = let rec aux l' = function | (0, l) -> (List.rev l', l) | (n, (Declaration.LocalDef _ as h) :: l) -> aux (h::l') (n, l) | (n, (Declaration.LocalAssum _ as h) :: l) -> aux (h::l') (n-1, l) | (_, []) -> CErrors.anomaly (Pp.str "chop_nhyps: not enough hypotheses.") in aux [] (n,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 mk n l = let rec reln l p = function | Declaration.LocalAssum _ :: hyps -> reln (mk (n+p) :: l) (p+1) hyps | Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps | [] -> l in reln [] 1 l
(** [extended_vect n Γ] does the same, returning instead an array. *) let to_extended_vect mk n hyps = Array.of_list (to_extended_list mk n hyps)
(** Consistency with terminology in Named *) let instance = to_extended_vect let instance_list = to_extended_listend
(** 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 ('constr, 'types, 'r) pt = | LocalAssum of (Id.t,'r) pbinder_annot * 'types (** identifier, type *) | LocalDef of (Id.t,'r) pbinder_annot * 'constr * 'types (** identifier, value, type *)
let get_annot = function | LocalAssum (na,_) | LocalDef (na,_,_) -> na
(** Return the identifier bound by a given declaration. *) let get_id x = (get_annot x).binder_name
(** 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
let get_relevance x = (get_annot x).binder_relevance
(** Set the identifier that is bound by a given declaration. *) let set_id id = let set x = {x with binder_name = id} in function | LocalAssum (x,ty) -> LocalAssum (set x, ty) | LocalDef (x, v, ty) -> LocalDef (set x, 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 eqr eq decl1 decl2 = match decl1, decl2 with | LocalAssum (id1, ty1), LocalAssum (id2, ty2) -> eq_annot Id.equal eqr id1 id2 && eq ty1 ty2 | LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) -> eq_annot Id.equal eqr id1 id2 && eq v1 v2 && eq ty1 ty2 | _ -> false
(** Map the identifier bound by a given declaration. *) let map_id f x = let id = get_id x in let id' = f id in if id == id' then x else set_id id' x
(** 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')
(** Map all terms in a given declaration. *) let map_constr_with_relevance g f = function | LocalAssum (id, ty) as decl -> let id' = map_annot_relevance g id in let ty' = f ty in if id == id' && ty == ty' then decl else LocalAssum (id', ty') | LocalDef (id, v, ty) as decl -> let id' = map_annot_relevance g id in let v' = f v in let ty' = f ty in if id == id' && v == v' && ty == ty' then decl else LocalDef (id', v', ty')
let map_constr_het fr f = function | LocalAssum (id, ty) -> let ty' = f ty in LocalAssum (map_annot_relevance_het fr id, ty') | LocalDef (id, v, ty) -> let v' = f v in let ty' = f ty in LocalDef (map_annot_relevance_het fr 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_constr 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)
let drop_body = function | LocalAssum _ as d -> d | LocalDef (id, _v, ty) -> LocalAssum (id, ty)
let of_rel_decl f = function | Rel.Declaration.LocalAssum (na,t) -> LocalAssum (map_annot f na, t) | Rel.Declaration.LocalDef (na,v,t) -> LocalDef (map_annot f na, v, t)
let to_rel_decl = let name x = {binder_name=Name x.binder_name;binder_relevance=x.binder_relevance} in 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, 'r) pt = ('constr, 'types, 'r) Declaration.pt list
(** empty named-context *) let empty = []
(** Return a new named-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 named-context. *) let length = List.length
(** 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 eqr eq l = List.equal (fun c -> Declaration.equal eqr eq c) l
(** Map all terms in a given named-context. *) let map f = List.Smart.map (Declaration.map_constr f)
let map_with_relevance g f = List.Smart.map (Declaration.map_constr_with_relevance g f)
let map_het fr f = List.map (Declaration.map_constr_het fr 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 l = List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty l
let drop_bodies l = List.Smart.map Declaration.drop_body l
(** [to_instance Ω] builds an instance [args] in reverse order 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 mk l = let filter = function | Declaration.LocalAssum (id, _) -> Some (mk id.binder_name) | _ -> None in List.map_filter filter l
(** [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 gives [Var id1, Var id3]. All [idj] are supposed distinct. *) let instance_list mk l = let filter = function | Declaration.LocalAssum (id, _) -> Some (mk id.binder_name) | _ -> None in List.rev (List.map_filter filter l)
let instance mk l = Array.of_list (instance_list mk l)end