diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 18 | ||||
| -rw-r--r-- | kernel/constr.mli | 26 | ||||
| -rw-r--r-- | kernel/context.ml | 69 | ||||
| -rw-r--r-- | kernel/context.mli | 160 | ||||
| -rw-r--r-- | kernel/environ.ml | 16 | ||||
| -rw-r--r-- | kernel/environ.mli | 19 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 2 | ||||
| -rw-r--r-- | kernel/inductive.ml | 4 | ||||
| -rw-r--r-- | kernel/term.ml | 13 | ||||
| -rw-r--r-- | kernel/term.mli | 14 | ||||
| -rw-r--r-- | kernel/type_errors.ml | 58 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 58 | ||||
| -rw-r--r-- | kernel/vars.mli | 2 |
13 files changed, 255 insertions, 204 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index ce20751abc..5a7561bf50 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -81,27 +81,27 @@ type pconstructor = constructor puniverses (* [Var] is used for named variables and [Rel] for variables as de Bruijn indices. *) -type ('constr, 'types) kind_of_term = +type ('constr, 'types, 'sort, 'univs) kind_of_term = | Rel of int | Var of Id.t | Meta of metavariable | Evar of 'constr pexistential - | Sort of Sorts.t + | Sort of 'sort | Cast of 'constr * cast_kind * 'types | Prod of Name.t * 'types * 'types | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of pconstant - | Ind of pinductive - | Construct of pconstructor + | Const of (constant * 'univs) + | Ind of (inductive * 'univs) + | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint | Proj of projection * 'constr (* constr is the fixpoint of the previous type. Requires option -rectypes of the Caml compiler to be set *) -type t = (t,t) kind_of_term +type t = (t, t, Sorts.t, Instance.t) kind_of_term type constr = t type existential = existential_key * constr array @@ -235,6 +235,12 @@ let mkVar id = Var id let kind c = c +(* The other way around. We treat specifically smart constructors *) +let of_kind = function +| App (f, a) -> mkApp (f, a) +| Cast (c, knd, t) -> mkCast (c, knd, t) +| k -> k + (****************************************************************************) (* Functions to recur through subterms *) (****************************************************************************) diff --git a/kernel/constr.mli b/kernel/constr.mli index 7095dbe6f9..700c235e6a 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -188,7 +188,7 @@ type ('constr, 'types) pfixpoint = type ('constr, 'types) pcofixpoint = int * ('constr, 'types) prec_declaration -type ('constr, 'types) kind_of_term = +type ('constr, 'types, 'sort, 'univs) kind_of_term = | Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *) | Var of Id.t (** Gallina-variable that was introduced by Vernacular-command that extends @@ -197,7 +197,7 @@ type ('constr, 'types) kind_of_term = | Meta of metavariable | Evar of 'constr pexistential - | Sort of Sorts.t + | Sort of 'sort | Cast of 'constr * cast_kind * 'types | Prod of Name.t * 'types * 'types (** Concrete syntax ["forall A:B,C"] is represented as [Prod (A,B,C)]. *) | Lambda of Name.t * 'types * 'constr (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)]. *) @@ -208,11 +208,11 @@ type ('constr, 'types) kind_of_term = - [F] itself is not {!App} - and [[|P1;..;Pn|]] is not empty. *) - | Const of constant puniverses (** Gallina-variable that was introduced by Vernacular-command that extends the global environment + | Const of (constant * 'univs) (** Gallina-variable that was introduced by Vernacular-command that extends the global environment (i.e. [Parameter], or [Axiom], or [Definition], or [Theorem] etc.) *) - | Ind of inductive puniverses (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) - | Construct of constructor puniverses (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) + | Ind of (inductive * 'univs) (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) + | Construct of (constructor * 'univs) (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint @@ -222,7 +222,8 @@ type ('constr, 'types) kind_of_term = least one argument and the function is not itself an applicative term *) -val kind : constr -> (constr, types) kind_of_term +val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term +val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr (** [equal a b] is true if [a] equals [b] modulo alpha, casts, and application grouping *) @@ -310,13 +311,22 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> (constr -> constr -> bool) -> constr -> constr -> bool +val compare_head_gen_leq_with : + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> + (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> + (Sorts.t -> Sorts.t -> bool) -> + (constr -> constr -> bool) -> + (constr -> constr -> bool) -> + constr -> constr -> bool + (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2] like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2]) is used,rather than {!kind}, to expose the immediate subterms of [c1] (resp. [c2]). *) val compare_head_gen_with : - (constr -> (constr,types) kind_of_term) -> - (constr -> (constr,types) kind_of_term) -> + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> (Sorts.t -> Sorts.t -> bool) -> (constr -> constr -> bool) -> diff --git a/kernel/context.ml b/kernel/context.ml index ae0388003d..abb284f226 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -37,9 +37,11 @@ struct module Declaration = struct (* local declaration *) - type t = - | LocalAssum of Name.t * Constr.t (** name, type *) - | LocalDef of Name.t * Constr.t * Constr.t (** name, value, type *) + type ('constr, 'types) pt = + | LocalAssum of Name.t * 'types (** name, type *) + | LocalDef of Name.t * 'constr * 'types (** name, value, type *) + + type t = (Constr.constr, Constr.types) pt (** Return the name bound by a given declaration. *) let get_name = function @@ -87,12 +89,12 @@ struct | LocalDef (_, v, ty) -> f v && f ty (** Check whether the two given declarations are equal. *) - let equal decl1 decl2 = + let equal eq decl1 decl2 = match decl1, decl2 with | LocalAssum (n1,ty1), LocalAssum (n2, ty2) -> - Name.equal n1 n2 && Constr.equal ty1 ty2 + Name.equal n1 n2 && eq ty1 ty2 | LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) -> - Name.equal n1 n2 && Constr.equal v1 v2 && Constr.equal ty1 ty2 + Name.equal n1 n2 && eq v1 v2 && eq ty1 ty2 | _ -> false @@ -152,6 +154,7 @@ struct (** Rel-context is represented as a list of declarations. Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) + type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list type t = Declaration.t list (** empty rel-context *) @@ -166,14 +169,14 @@ struct (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] with n = |Δ| and with the local definitions of [Γ] skipped in [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) - let nhyps = + let nhyps ctx = let open Declaration in let rec nhyps acc = function | [] -> acc | LocalAssum _ :: hyps -> nhyps (succ acc) hyps | LocalDef _ :: hyps -> nhyps acc hyps in - nhyps 0 + nhyps 0 ctx (** Return a declaration designated by a given de Bruijn index. @raise Not_found if the designated de Bruijn index is not present in the designated rel-context. *) @@ -184,7 +187,7 @@ struct | _, [] -> raise Not_found (** Check whether given two rel-contexts are equal. *) - let equal = List.equal Declaration.equal + let equal eq l = List.equal (fun c -> Declaration.equal eq c) l (** Map all terms in a given rel-context. *) let map f = List.smartmap (Declaration.map_constr f) @@ -202,26 +205,26 @@ struct (** Map a given rel-context to a list where each {e local assumption} is mapped to [true] and each {e local definition} is mapped to [false]. *) - let to_tags = + let to_tags l = let rec aux l = function | [] -> l | Declaration.LocalDef _ :: ctx -> aux (true::l) ctx | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx - in aux [] + in aux [] l (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] with n = |Δ| and with the {e local definitions} of [Γ] skipped in [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *) - let to_extended_list n = + let to_extended_list mk n l = let rec reln l p = function - | Declaration.LocalAssum _ :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps + | Declaration.LocalAssum _ :: hyps -> reln (mk (n+p) :: l) (p+1) hyps | Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps | [] -> l in - reln [] 1 + reln [] 1 l (** [extended_vect n Γ] does the same, returning instead an array. *) - let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps) + let to_extended_vect mk n hyps = Array.of_list (to_extended_list mk n hyps) end (** This module represents contexts that can capture non-anonymous variables. @@ -232,9 +235,11 @@ struct module Declaration = struct (** local declaration *) - type t = - | LocalAssum of Id.t * Constr.t (** identifier, type *) - | LocalDef of Id.t * Constr.t * Constr.t (** identifier, value, type *) + type ('constr, 'types) pt = + | LocalAssum of Id.t * 'types (** identifier, type *) + | LocalDef of Id.t * 'constr * 'types (** identifier, value, type *) + + type t = (Constr.constr, Constr.types) pt (** Return the identifier bound by a given declaration. *) let get_id = function @@ -282,12 +287,12 @@ struct | LocalDef (_, v, ty) -> f v && f ty (** Check whether the two given declarations are equal. *) - let equal decl1 decl2 = + let equal eq decl1 decl2 = match decl1, decl2 with | LocalAssum (id1, ty1), LocalAssum (id2, ty2) -> - Id.equal id1 id2 && Constr.equal ty1 ty2 + Id.equal id1 id2 && eq ty1 ty2 | LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) -> - Id.equal id1 id2 && Constr.equal v1 v2 && Constr.equal ty1 ty2 + Id.equal id1 id2 && eq v1 v2 && eq ty1 ty2 | _ -> false @@ -362,6 +367,7 @@ 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 ('constr, 'types) pt = ('constr, 'types) Declaration.pt list type t = Declaration.t list (** empty named-context *) @@ -380,7 +386,7 @@ struct | [] -> raise Not_found (** Check whether given two named-contexts are equal. *) - let equal = List.equal Declaration.equal + let equal eq l = List.equal (fun c -> Declaration.equal eq c) l (** Map all terms in a given named-context. *) let map f = List.smartmap (Declaration.map_constr f) @@ -397,28 +403,30 @@ struct let fold_outside f l ~init = List.fold_right f l init (** Return the set of all identifiers bound in a given named-context. *) - let to_vars = - List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty + let to_vars l = + List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty l (** [instance_from_named_context Ω] builds an instance [args] such that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it gives [Var id1, Var id3]. All [idj] are supposed distinct. *) - let to_instance = + let to_instance mk l = let filter = function - | Declaration.LocalAssum (id, _) -> Some (Constr.mkVar id) + | Declaration.LocalAssum (id, _) -> Some (mk id) | _ -> None in - List.map_filter filter + List.map_filter filter l end module Compacted = struct module Declaration = struct - type t = - | LocalAssum of Id.t list * Constr.t - | LocalDef of Id.t list * Constr.t * Constr.t + type ('constr, 'types) pt = + | LocalAssum of Id.t list * 'types + | LocalDef of Id.t list * 'constr * 'types + + type t = (Constr.constr, Constr.types) pt let map_constr f = function | LocalAssum (ids, ty) as decl -> @@ -442,6 +450,7 @@ module Compacted = List.map (fun id -> Named.Declaration.LocalDef (id,v,t)) ids end + type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list type t = Declaration.t list let fold f l ~init = List.fold_right f l init diff --git a/kernel/context.mli b/kernel/context.mli index 955e214cb9..0c666a25d9 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -29,110 +29,115 @@ sig module Declaration : sig (* local declaration *) - type t = LocalAssum of Name.t * Constr.t (** name, type *) - | LocalDef of Name.t * Constr.t * Constr.t (** name, value, type *) + type ('constr, 'types) pt = + | LocalAssum of Name.t * 'types (** name, type *) + | LocalDef of Name.t * 'constr * 'types (** name, value, type *) + + type t = (Constr.constr, Constr.types) pt (** Return the name bound by a given declaration. *) - val get_name : t -> Name.t + val get_name : ('c, 't) pt -> Name.t (** Return [Some value] for local-declarations and [None] for local-assumptions. *) - val get_value : t -> Constr.t option + val get_value : ('c, 't) pt -> 'c option (** Return the type of the name bound by a given declaration. *) - val get_type : t -> Constr.t + val get_type : ('c, 't) pt -> 't (** Set the name that is bound by a given declaration. *) - val set_name : Name.t -> t -> t + val set_name : Name.t -> ('c, 't) pt -> ('c, 't) pt (** Set the type of the bound variable in a given declaration. *) - val set_type : Constr.t -> t -> t + val set_type : 't -> ('c, 't) pt -> ('c, 't) pt (** Return [true] iff a given declaration is a local assumption. *) - val is_local_assum : t -> bool + val is_local_assum : ('c, 't) pt -> bool (** Return [true] iff a given declaration is a local definition. *) - val is_local_def : t -> bool + val is_local_def : ('c, 't) pt -> bool (** Check whether any term in a given declaration satisfies a given predicate. *) - val exists : (Constr.t -> bool) -> t -> bool + val exists : ('c -> bool) -> ('c, 'c) pt -> bool (** Check whether all terms in a given declaration satisfy a given predicate. *) - val for_all : (Constr.t -> bool) -> t -> bool + val for_all : ('c -> bool) -> ('c, 'c) pt -> bool (** Check whether the two given declarations are equal. *) - val equal : t -> t -> bool + val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool (** Map the name bound by a given declaration. *) - val map_name : (Name.t -> Name.t) -> t -> t + val map_name : (Name.t -> Name.t) -> ('c, 't) pt -> ('c, 't) pt (** For local assumptions, this function returns the original local assumptions. For local definitions, this function maps the value in the local definition. *) - val map_value : (Constr.t -> Constr.t) -> t -> t + val map_value : ('c -> 'c) -> ('c, 't) pt -> ('c, 't) pt (** Map the type of the name bound by a given declaration. *) - val map_type : (Constr.t -> Constr.t) -> t -> t + val map_type : ('t -> 't) -> ('c, 't) pt -> ('c, 't) pt (** Map all terms in a given declaration. *) - val map_constr : (Constr.t -> Constr.t) -> t -> t + val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt (** Perform a given action on all terms in a given declaration. *) - val iter_constr : (Constr.t -> unit) -> t -> unit + val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit (** Reduce all terms in a given declaration to a single value. *) - val fold_constr : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a - val to_tuple : t -> Name.t * Constr.t option * Constr.t + val to_tuple : ('c, 't) pt -> Name.t * 'c option * 't end (** Rel-context is represented as a list of declarations. Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) + type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list type t = Declaration.t list (** empty rel-context *) - val empty : t + val empty : ('c, 't) pt (** Return a new rel-context enriched by with a given inner-most declaration. *) - val add : Declaration.t -> t -> t + val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt (** Return the number of {e local declarations} in a given context. *) - val length : t -> int + val length : ('c, 't) pt -> int (** Check whether given two rel-contexts are equal. *) - val equal : t -> t -> bool + val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool (** Return the number of {e local assumptions} in a given rel-context. *) - val nhyps : t -> int + val nhyps : ('c, 't) pt -> int (** Return a declaration designated by a given de Bruijn index. @raise Not_found if the designated de Bruijn index outside the range. *) - val lookup : int -> t -> Declaration.t + val lookup : int -> ('c, 't) pt -> ('c, 't) Declaration.pt (** Map all terms in a given rel-context. *) - val map : (Constr.t -> Constr.t) -> t -> t + val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt (** Perform a given action on every declaration in a given rel-context. *) - val iter : (Constr.t -> unit) -> t -> unit + val iter : ('c -> unit) -> ('c, 'c) pt -> unit (** Reduce all terms in a given rel-context to a single value. Innermost declarations are processed first. *) - val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a + val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> 'a (** Reduce all terms in a given rel-context to a single value. Outermost declarations are processed first. *) - val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a + val fold_outside : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a (** 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]. *) - val to_tags : t -> bool list + val to_tags : ('c, 't) pt -> bool list - (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ] + (** [extended_list mk 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]. *) - val to_extended_list : int -> t -> Constr.t list + [args] where [mk] is used to build the corresponding variables. + Example: for [x:T, y:=c, z:U] and [n]=2, it gives [mk 5, mk 3]. *) + val to_extended_list : (int -> 'r) -> int -> ('c, 't) pt -> 'r list (** [extended_vect n Γ] does the same, returning instead an array. *) - val to_extended_vect : int -> t -> Constr.t array + val to_extended_vect : (int -> 'r) -> int -> ('c, 't) pt -> 'r array end (** This module represents contexts that can capture non-anonymous variables. @@ -142,129 +147,136 @@ sig (** Representation of {e local declarations}. *) module Declaration : sig - type t = LocalAssum of Id.t * Constr.t (** identifier, type *) - | LocalDef of Id.t * Constr.t * Constr.t (** identifier, value, type *) + type ('constr, 'types) pt = + | LocalAssum of Id.t * 'types (** identifier, type *) + | LocalDef of Id.t * 'constr * 'types (** identifier, value, type *) + + type t = (Constr.constr, Constr.types) pt (** Return the identifier bound by a given declaration. *) - val get_id : t -> Id.t + val get_id : ('c, 't) pt -> Id.t (** Return [Some value] for local-declarations and [None] for local-assumptions. *) - val get_value : t -> Constr.t option + val get_value : ('c, 't) pt -> 'c option (** Return the type of the name bound by a given declaration. *) - val get_type : t -> Constr.t + val get_type : ('c, 't) pt -> 't (** Set the identifier that is bound by a given declaration. *) - val set_id : Id.t -> t -> t + val set_id : Id.t -> ('c, 't) pt -> ('c, 't) pt (** Set the type of the bound variable in a given declaration. *) - val set_type : Constr.t -> t -> t + val set_type : 't -> ('c, 't) pt -> ('c, 't) pt (** Return [true] iff a given declaration is a local assumption. *) - val is_local_assum : t -> bool + val is_local_assum : ('c, 't) pt -> bool (** Return [true] iff a given declaration is a local definition. *) - val is_local_def : t -> bool + val is_local_def : ('c, 't) pt -> bool (** Check whether any term in a given declaration satisfies a given predicate. *) - val exists : (Constr.t -> bool) -> t -> bool + val exists : ('c -> bool) -> ('c, 'c) pt -> bool (** Check whether all terms in a given declaration satisfy a given predicate. *) - val for_all : (Constr.t -> bool) -> t -> bool + val for_all : ('c -> bool) -> ('c, 'c) pt -> bool (** Check whether the two given declarations are equal. *) - val equal : t -> t -> bool + val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool (** Map the identifier bound by a given declaration. *) - val map_id : (Id.t -> Id.t) -> t -> t + val map_id : (Id.t -> Id.t) -> ('c, 't) pt -> ('c, 't) pt (** For local assumptions, this function returns the original local assumptions. For local definitions, this function maps the value in the local definition. *) - val map_value : (Constr.t -> Constr.t) -> t -> t + val map_value : ('c -> 'c) -> ('c, 't) pt -> ('c, 't) pt (** Map the type of the name bound by a given declaration. *) - val map_type : (Constr.t -> Constr.t) -> t -> t + val map_type : ('t -> 't) -> ('c, 't) pt -> ('c, 't) pt (** Map all terms in a given declaration. *) - val map_constr : (Constr.t -> Constr.t) -> t -> t + val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt (** Perform a given action on all terms in a given declaration. *) - val iter_constr : (Constr.t -> unit) -> t -> unit + val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit (** Reduce all terms in a given declaration to a single value. *) - val fold_constr : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a - val to_tuple : t -> Id.t * Constr.t option * Constr.t - val of_tuple : Id.t * Constr.t option * Constr.t -> t + val to_tuple : ('c, 't) pt -> Id.t * 'c option * 't + val of_tuple : Id.t * 'c option * 't -> ('c, 't) pt (** Convert [Rel.Declaration.t] value to the corresponding [Named.Declaration.t] value. The function provided as the first parameter determines how to translate "names" to "ids". *) - val of_rel_decl : (Name.t -> Id.t) -> Rel.Declaration.t -> t + val of_rel_decl : (Name.t -> Id.t) -> ('c, 't) Rel.Declaration.pt -> ('c, 't) pt (** Convert [Named.Declaration.t] value to the corresponding [Rel.Declaration.t] value. *) (* TODO: Move this function to [Rel.Declaration] module and rename it to [of_named]. *) - val to_rel_decl : t -> Rel.Declaration.t + val to_rel_decl : ('c, 't) pt -> ('c, 't) Rel.Declaration.pt end (** Rel-context is represented as a list of declarations. Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) + type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list type t = Declaration.t list (** empty named-context *) - val empty : t + val empty : ('c, 't) pt (** Return a new rel-context enriched by with a given inner-most declaration. *) - val add : Declaration.t -> t -> t + val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt (** Return the number of {e local declarations} in a given named-context. *) - val length : t -> int + val length : ('c, 't) pt -> int (** Return a declaration designated by an identifier of the variable bound in that declaration. @raise Not_found if the designated identifier is not bound in a given named-context. *) - val lookup : Id.t -> t -> Declaration.t + val lookup : Id.t -> ('c, 't) pt -> ('c, 't) Declaration.pt (** Check whether given two rel-contexts are equal. *) - val equal : t -> t -> bool + val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool (** Map all terms in a given named-context. *) - val map : (Constr.t -> Constr.t) -> t -> t + val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt (** Perform a given action on every declaration in a given named-context. *) - val iter : (Constr.t -> unit) -> t -> unit + val iter : ('c -> unit) -> ('c, 'c) pt -> unit (** Reduce all terms in a given named-context to a single value. Innermost declarations are processed first. *) - val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a + val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> 'a (** Reduce all terms in a given named-context to a single value. Outermost declarations are processed first. *) - val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a + val fold_outside : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a (** Return the set of all identifiers bound in a given named-context. *) - val to_vars : t -> Id.Set.t + val to_vars : ('c, 't) pt -> Id.Set.t (** [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. *) - val to_instance : t -> Constr.t list + val to_instance : (Id.t -> 'r) -> ('c, 't) pt -> 'r list end module Compacted : sig module Declaration : sig - type t = - | LocalAssum of Id.t list * Constr.t - | LocalDef of Id.t list * Constr.t * Constr.t + type ('constr, 'types) pt = + | LocalAssum of Id.t list * 'types + | LocalDef of Id.t list * 'constr * 'types + + type t = (Constr.constr, Constr.types) pt - val map_constr : (Constr.t -> Constr.t) -> t -> t - val of_named_decl : Named.Declaration.t -> t - val to_named_context : t -> Named.t + val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt + val of_named_decl : ('c, 't) Named.Declaration.pt -> ('c, 't) pt + val to_named_context : ('c, 't) pt -> ('c, 't) Named.pt end + type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list type t = Declaration.t list - val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a + val fold : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a end diff --git a/kernel/environ.ml b/kernel/environ.ml index 4a543f1957..9986f439af 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -120,7 +120,7 @@ let lookup_named = lookup_named let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map) let eq_named_context_val c1 c2 = - c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2) + c1 == c2 || Context.Named.equal Constr.equal (named_context_of_val c1) (named_context_of_val c2) (* A local const is evaluable if it is defined *) @@ -469,9 +469,11 @@ let lookup_modtype mp env = (*s Judgments. *) -type unsafe_judgment = { - uj_val : constr; - uj_type : types } +type ('constr, 'types) punsafe_judgment = { + uj_val : 'constr; + uj_type : 'types } + +type unsafe_judgment = (constr, types) punsafe_judgment let make_judge v tj = { uj_val = v; @@ -480,10 +482,12 @@ let make_judge v tj = let j_val j = j.uj_val let j_type j = j.uj_type -type unsafe_type_judgment = { - utj_val : constr; +type 'types punsafe_type_judgment = { + utj_val : 'types; utj_type : sorts } +type unsafe_type_judgment = types punsafe_type_judgment + (*s Compilation of global declaration *) let compile_constant_body = Cbytegen.compile_constant_body false diff --git a/kernel/environ.mli b/kernel/environ.mli index ea570cb4a8..b7431dbe5f 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -238,18 +238,21 @@ val keep_hyps : env -> Id.Set.t -> Context.Named.t actually only a datatype to store a term with its type and the type of its type. *) -type unsafe_judgment = { - uj_val : constr; - uj_type : types } +type ('constr, 'types) punsafe_judgment = { + uj_val : 'constr; + uj_type : 'types } -val make_judge : constr -> types -> unsafe_judgment -val j_val : unsafe_judgment -> constr -val j_type : unsafe_judgment -> types +type unsafe_judgment = (constr, types) punsafe_judgment -type unsafe_type_judgment = { - utj_val : constr; +val make_judge : 'constr -> 'types -> ('constr, 'types) punsafe_judgment +val j_val : ('constr, 'types) punsafe_judgment -> 'constr +val j_type : ('constr, 'types) punsafe_judgment -> 'types + +type 'types punsafe_type_judgment = { + utj_val : 'types; utj_type : sorts } +type unsafe_type_judgment = types punsafe_type_judgment (** {6 Compilation of global declaration } *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index de97268b37..2ff4193384 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -734,7 +734,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params matching with a parameter context. *) let indty, paramsletsubst = (* [ty] = [Ind inst] is typed in context [params] *) - let inst = Context.Rel.to_extended_vect 0 paramslet in + let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in let ty = mkApp (mkIndU indu, inst) in (* [Ind inst] is typed in context [params-wo-let] *) let inst' = rel_list 0 nparamargs in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 3c4c2796ee..d8d365c347 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -297,7 +297,7 @@ let build_dependent_inductive ind (_,mip) params = applist (mkIndU ind, List.map (lift mip.mind_nrealdecls) params - @ Context.Rel.to_extended_list 0 realargs) + @ Context.Rel.to_extended_list mkRel 0 realargs) (* This exception is local *) exception LocalArity of (sorts_family * sorts_family * arity_error) option @@ -355,7 +355,7 @@ let build_branches_type (ind,u) (_,mip as specif) params p = let (lparams,vargs) = List.chop (inductive_params specif) allargs in let cargs = let cstr = ith_constructor_of_inductive ind (i+1) in - let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list 0 cstrsign)) in + let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list mkRel 0 cstrsign)) in vargs @ [dep_cstr] in let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in it_mkProd_or_LetIn base cstrsign in diff --git a/kernel/term.ml b/kernel/term.ml index 62c161be4c..e5a681375d 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -71,20 +71,21 @@ type pconstant = constant puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses -type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term = +type ('constr, 'types, 'sort, 'univs) kind_of_term = + ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = | Rel of int | Var of Id.t | Meta of metavariable | Evar of 'constr pexistential - | Sort of sorts + | Sort of 'sort | Cast of 'constr * cast_kind * 'types | Prod of Name.t * 'types * 'types | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of pconstant - | Ind of pinductive - | Construct of pconstructor + | Const of (constant * 'univs) + | Ind of (inductive * 'univs) + | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint @@ -179,8 +180,6 @@ let destMeta c = match kind_of_term c with | _ -> raise DestKO let isMeta c = match kind_of_term c with Meta _ -> true | _ -> false -let isMetaOf mv c = - match kind_of_term c with Meta mv' -> Int.equal mv mv' | _ -> false (* Destructs a variable *) let destVar c = match kind_of_term c with diff --git a/kernel/term.mli b/kernel/term.mli index a8d9dfbfff..a9bb677050 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -68,20 +68,21 @@ type ('constr, 'types) prec_declaration = type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint -type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term = +type ('constr, 'types, 'sort, 'univs) kind_of_term = + ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = | Rel of int | Var of Id.t | Meta of metavariable | Evar of 'constr pexistential - | Sort of sorts + | Sort of 'sort | Cast of 'constr * cast_kind * 'types | Prod of Name.t * 'types * 'types | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of constant puniverses - | Ind of inductive puniverses - | Construct of constructor puniverses + | Const of (constant * 'univs) + | Ind of (inductive * 'univs) + | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint @@ -98,7 +99,6 @@ val isVarId : Id.t -> constr -> bool val isInd : constr -> bool val isEvar : constr -> bool val isMeta : constr -> bool -val isMetaOf : metavariable -> constr -> bool val isEvar_or_Meta : constr -> bool val isSort : constr -> bool val isCast : constr -> bool @@ -444,7 +444,7 @@ val leq_constr_univs : constr UGraph.check_function application grouping and ignoring universe instances. *) val eq_constr_nounivs : constr -> constr -> bool -val kind_of_term : constr -> (constr, types) kind_of_term +val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term (** Alias for [Constr.kind] *) val constr_ord : constr -> constr -> int diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 5071f0ad5d..5e17638152 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -13,52 +13,56 @@ open Reduction (* Type errors. *) -type guard_error = +type 'constr pguard_error = (* Fixpoints *) | NotEnoughAbstractionInFixBody - | RecursionNotOnInductiveType of constr - | RecursionOnIllegalTerm of int * (env * constr) * int list * int list + | RecursionNotOnInductiveType of 'constr + | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list | NotEnoughArgumentsForFixCall of int (* CoFixpoints *) - | CodomainNotInductiveType of constr + | CodomainNotInductiveType of 'constr | NestedRecursiveOccurrences - | UnguardedRecursiveCall of constr - | RecCallInTypeOfAbstraction of constr - | RecCallInNonRecArgOfConstructor of constr - | RecCallInTypeOfDef of constr - | RecCallInCaseFun of constr - | RecCallInCaseArg of constr - | RecCallInCasePred of constr - | NotGuardedForm of constr - | ReturnPredicateNotCoInductive of constr + | UnguardedRecursiveCall of 'constr + | RecCallInTypeOfAbstraction of 'constr + | RecCallInNonRecArgOfConstructor of 'constr + | RecCallInTypeOfDef of 'constr + | RecCallInCaseFun of 'constr + | RecCallInCaseArg of 'constr + | RecCallInCasePred of 'constr + | NotGuardedForm of 'constr + | ReturnPredicateNotCoInductive of 'constr + +type guard_error = constr pguard_error type arity_error = | NonInformativeToInformative | StrongEliminationOnNonSmallType | WrongArity -type type_error = +type ('constr, 'types) ptype_error = | UnboundRel of int | UnboundVar of variable - | NotAType of unsafe_judgment - | BadAssumption of unsafe_judgment - | ReferenceVariables of identifier * constr - | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment + | NotAType of ('constr, 'types) punsafe_judgment + | BadAssumption of ('constr, 'types) punsafe_judgment + | ReferenceVariables of identifier * 'constr + | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment * (sorts_family * sorts_family * arity_error) option - | CaseNotInductive of unsafe_judgment + | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info - | NumberBranches of unsafe_judgment * int - | IllFormedBranch of constr * pconstructor * constr * constr - | Generalization of (Name.t * types) * unsafe_judgment - | ActualType of unsafe_judgment * types + | NumberBranches of ('constr, 'types) punsafe_judgment * int + | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr + | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment + | ActualType of ('constr, 'types) punsafe_judgment * 'types | CantApplyBadType of - (int * constr * constr) * unsafe_judgment * unsafe_judgment array - | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array + (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of - int * Name.t array * unsafe_judgment array * types array + int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.constraints +type type_error = (constr, types) ptype_error + exception TypeError of env * type_error let nfj env {uj_val=c;uj_type=ct} = diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 0c3a952b8d..bd6032716f 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -14,52 +14,56 @@ open Environ (*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix notation i*) -type guard_error = +type 'constr pguard_error = (** Fixpoints *) | NotEnoughAbstractionInFixBody - | RecursionNotOnInductiveType of constr - | RecursionOnIllegalTerm of int * (env * constr) * int list * int list + | RecursionNotOnInductiveType of 'constr + | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list | NotEnoughArgumentsForFixCall of int (** CoFixpoints *) - | CodomainNotInductiveType of constr + | CodomainNotInductiveType of 'constr | NestedRecursiveOccurrences - | UnguardedRecursiveCall of constr - | RecCallInTypeOfAbstraction of constr - | RecCallInNonRecArgOfConstructor of constr - | RecCallInTypeOfDef of constr - | RecCallInCaseFun of constr - | RecCallInCaseArg of constr - | RecCallInCasePred of constr - | NotGuardedForm of constr - | ReturnPredicateNotCoInductive of constr + | UnguardedRecursiveCall of 'constr + | RecCallInTypeOfAbstraction of 'constr + | RecCallInNonRecArgOfConstructor of 'constr + | RecCallInTypeOfDef of 'constr + | RecCallInCaseFun of 'constr + | RecCallInCaseArg of 'constr + | RecCallInCasePred of 'constr + | NotGuardedForm of 'constr + | ReturnPredicateNotCoInductive of 'constr + +type guard_error = constr pguard_error type arity_error = | NonInformativeToInformative | StrongEliminationOnNonSmallType | WrongArity -type type_error = +type ('constr, 'types) ptype_error = | UnboundRel of int | UnboundVar of variable - | NotAType of unsafe_judgment - | BadAssumption of unsafe_judgment - | ReferenceVariables of identifier * constr - | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment + | NotAType of ('constr, 'types) punsafe_judgment + | BadAssumption of ('constr, 'types) punsafe_judgment + | ReferenceVariables of identifier * 'constr + | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment * (sorts_family * sorts_family * arity_error) option - | CaseNotInductive of unsafe_judgment + | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info - | NumberBranches of unsafe_judgment * int - | IllFormedBranch of constr * pconstructor * constr * constr - | Generalization of (Name.t * types) * unsafe_judgment - | ActualType of unsafe_judgment * types + | NumberBranches of ('constr, 'types) punsafe_judgment * int + | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr + | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment + | ActualType of ('constr, 'types) punsafe_judgment * 'types | CantApplyBadType of - (int * constr * constr) * unsafe_judgment * unsafe_judgment array - | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array + (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of - int * Name.t array * unsafe_judgment array * types array + int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.constraints +type type_error = (constr, types) ptype_error + exception TypeError of env * type_error val error_unbound_rel : env -> int -> 'a diff --git a/kernel/vars.mli b/kernel/vars.mli index f7535e6d8f..adeac422e0 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -75,7 +75,7 @@ val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list (** Take an index in an instance of a context and returns its index wrt to the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *) -val adjust_rel_to_rel_context : Context.Rel.t -> int -> int +val adjust_rel_to_rel_context : ('a, 'b) Context.Rel.pt -> int -> int (** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an] for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates |