aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/declarations.ml4
-rw-r--r--kernel/declarations.mli4
-rw-r--r--kernel/environ.ml159
-rw-r--r--kernel/environ.mli88
-rw-r--r--kernel/evd.mli2
-rw-r--r--kernel/generic.ml10
-rw-r--r--kernel/generic.mli6
-rw-r--r--kernel/indtypes.ml42
-rw-r--r--kernel/indtypes.mli14
-rw-r--r--kernel/inductive.ml33
-rw-r--r--kernel/inductive.mli8
-rw-r--r--kernel/instantiate.ml29
-rw-r--r--kernel/instantiate.mli5
-rw-r--r--kernel/names.mli4
-rw-r--r--kernel/reduction.ml48
-rw-r--r--kernel/reduction.mli4
-rw-r--r--kernel/safe_typing.ml100
-rw-r--r--kernel/safe_typing.mli13
-rw-r--r--kernel/sign.ml415
-rw-r--r--kernel/sign.mli176
-rw-r--r--kernel/term.ml136
-rw-r--r--kernel/term.mli62
-rw-r--r--kernel/type_errors.ml42
-rw-r--r--kernel/type_errors.mli2
-rw-r--r--kernel/typeops.ml42
-rw-r--r--kernel/typeops.mli6
26 files changed, 792 insertions, 662 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 510e1f12b..e83e1e509 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -19,7 +19,7 @@ type constant_body = {
const_kind : path_kind;
const_body : constant_value option;
const_type : typed_type;
- const_hyps : typed_type signature;
+ const_hyps : var_context;
const_constraints : constraints;
mutable const_opaque : bool }
@@ -61,7 +61,7 @@ type one_inductive_body = {
type mutual_inductive_body = {
mind_kind : path_kind;
mind_ntypes : int;
- mind_hyps : typed_type signature;
+ mind_hyps : var_context;
mind_packets : one_inductive_body array;
mind_constraints : constraints;
mind_singl : constr option;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 7853a2ce1..1dc4a7cb8 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -20,7 +20,7 @@ type constant_body = {
const_kind : path_kind;
const_body : constant_value option;
const_type : typed_type;
- const_hyps : typed_type signature;
+ const_hyps : var_context; (* New: younger hyp at top *)
const_constraints : constraints;
mutable const_opaque : bool }
@@ -66,7 +66,7 @@ type one_inductive_body = {
type mutual_inductive_body = {
mind_kind : path_kind;
mind_ntypes : int;
- mind_hyps : typed_type signature;
+ mind_hyps : var_context;
mind_packets : one_inductive_body array;
mind_constraints : constraints;
mind_singl : constr option;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 73a8c6487..217a7f989 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -26,13 +26,21 @@ type globals = {
env_locals : (global * section_path) list;
env_imports : import list }
+type context = {
+ env_var_context : var_context;
+ env_rel_context : rel_context }
+
type env = {
env_context : context;
env_globals : globals;
env_universes : universes }
+let empty_context = {
+ env_var_context = empty_var_context;
+ env_rel_context = empty_rel_context }
+
let empty_env = {
- env_context = ENVIRON (nil_sign,nil_dbsign);
+ env_context = empty_context;
env_globals = {
env_constants = Spmap.empty;
env_inductives = Spmap.empty;
@@ -43,29 +51,93 @@ let empty_env = {
let universes env = env.env_universes
let context env = env.env_context
-let var_context env = let (ENVIRON(g,_)) = env.env_context in g
+let var_context env = env.env_context.env_var_context
+let rel_context env = env.env_context.env_rel_context
(* Construction functions. *)
-let push_var idvar env =
- { env with env_context = add_glob idvar env.env_context }
-
-let change_hyps f env =
- let (ENVIRON(g,r)) = env.env_context in
- { env with env_context = ENVIRON (f g, r) }
-
-(* == functions to deal with names in contexts (previously in cases.ml) == *)
-
-(* If cur=(Rel j) then
- * if env = ENVIRON(sign,[na_h:Th]...[na_j:Tj]...[na_1:T1])
- * then it yields ENVIRON(sign,[na_h:Th]...[Name id:Tj]...[na_1:T1])
- *)
-let change_name_rel env j id =
- { env with env_context = change_name_env (context env) j id }
-(****)
-
-let push_rel idrel env =
- { env with env_context = add_rel idrel env.env_context }
+let map_context f env =
+ let context = env.env_context in
+ { env with
+ env_context = {
+ context with
+ env_var_context = map_var_context f context.env_var_context ;
+ env_rel_context = map_rel_context f context.env_rel_context } }
+
+let var_context_app f env =
+ { env with
+ env_context = { env.env_context with
+ env_var_context = f env.env_context.env_var_context } }
+
+let change_hyps = var_context_app
+
+let push_var d = var_context_app (add_var d)
+let push_var_def def = var_context_app (add_var_def def)
+let push_var_decl decl = var_context_app (add_var_decl decl)
+let pop_var id = var_context_app (pop_var id)
+
+let rel_context_app f env =
+ { env with
+ env_context = { env.env_context with
+ env_rel_context = f env.env_context.env_rel_context } }
+
+let reset_context env =
+ { env with
+ env_context = { env_var_context = empty_var_context;
+ env_rel_context = empty_rel_context} }
+
+let fold_var_context f env a =
+ snd (Sign.fold_var_context
+ (fun d (env,e) -> (push_var d env, f env d e))
+ (var_context env) (reset_context env,a))
+
+let process_var_context f env =
+ Sign.fold_var_context
+ (fun d env -> f env d) (var_context env) (reset_context env)
+
+let process_var_context_both_sides f env =
+ fold_var_context_both_sides f (var_context env) (reset_context env)
+
+let push_rel d = rel_context_app (add_rel d)
+let push_rel_def def = rel_context_app (add_rel_def def)
+let push_rel_decl decl = rel_context_app (add_rel_decl decl)
+let push_rels ctxt = rel_context_app (concat_rel_context ctxt)
+
+let push_rels_to_vars env =
+ let sign0 = env.env_context.env_var_context in
+ let (subst,_,sign) =
+ List.fold_right
+ (fun (na,c,t) (subst,avoid,sign) ->
+ let na = if na = Anonymous then Name(id_of_string"_") else na in
+ let id = next_name_away na avoid in
+ ((VAR id)::subst,id::avoid,
+ add_var (id,option_app (substl subst) c,typed_app (substl subst) t)
+ sign))
+ env.env_context.env_rel_context ([],ids_of_var_context sign0,sign0)
+ in subst, (var_context_app (fun _ -> sign) env)
+
+let reset_rel_context env =
+ { env with
+ env_context = { env_var_context = env.env_context.env_var_context;
+ env_rel_context = empty_rel_context} }
+
+let fold_rel_context f env a =
+ snd (List.fold_right
+ (fun d (env,e) -> (push_rel d env, f env d e))
+ (rel_context env) (reset_rel_context env,a))
+
+let process_rel_context f env =
+ List.fold_right (fun d env -> f env d)
+ (rel_context env) (reset_rel_context env)
+
+let instantiate_vars = instantiate_sign
+
+let ids_of_context env =
+ (ids_of_rel_context env.env_context.env_rel_context)
+ @ (ids_of_var_context env.env_context.env_var_context)
+
+let names_of_rel_context env =
+ names_of_rel_context env.env_context.env_rel_context
let set_universes g env =
if env.env_universes == g then env else { env with env_universes = g }
@@ -109,12 +181,19 @@ let new_meta ()=incr meta_ctr;!meta_ctr;;
(* Access functions. *)
-let lookup_var id env =
- let (_,var) = lookup_glob id env.env_context in
- (Name id, var)
+let lookup_var_type id env =
+ lookup_id_type id env.env_context.env_var_context
+
+let lookup_var_value id env =
+ lookup_id_value id env.env_context.env_var_context
+
+let lookup_var id env = lookup_id id env.env_context.env_var_context
-let lookup_rel n env =
- Sign.lookup_rel n env.env_context
+let lookup_rel_type n env =
+ Sign.lookup_rel_type n env.env_context.env_rel_context
+
+let lookup_rel_value n env =
+ Sign.lookup_rel_value n env.env_context.env_rel_context
let lookup_constant sp env =
Spmap.find sp env.env_globals.env_constants
@@ -171,7 +250,7 @@ let hdchar env c =
| Rel n ->
(if n<=k then "p" (* the initial term is flexible product/function *)
else
- try match lookup_rel (n-k) env with
+ try match lookup_rel_type (n-k) env with
| Name id,_ -> lowercase_first_char id
| Anonymous,t -> hdrec 0 (lift (n-k) (body_of_type t))
with Not_found -> "y")
@@ -196,6 +275,32 @@ let it_lambda_name env = List.fold_left (fun c (n,t) ->lambda_name env (n,t,c))
let prod_create env (a,b) = mkProd (named_hd env a Anonymous) a b
let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous) a b
+let name_assumption env (na,c,t) =
+ match c with
+ | None -> (named_hd env (body_of_type t) na, None, t)
+ | Some body -> (named_hd env body na, c, t)
+
+let prod_assum_name env b d = mkProd_or_LetIn (name_assumption env d) b
+let lambda_assum_name env b d = mkLambda_or_LetIn (name_assumption env d) b
+
+let it_mkProd_or_LetIn_name env = List.fold_left (prod_assum_name env)
+let it_mkLambda_or_LetIn_name env = List.fold_left (lambda_assum_name env)
+
+let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c)
+let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
+
+let it_mkNamedProd_or_LetIn = it_var_context_quantifier mkNamedProd_or_LetIn
+let it_mkNamedLambda_or_LetIn = it_var_context_quantifier mkNamedLambda_or_LetIn
+
+let make_all_name_different env =
+ let avoid = ref (ids_of_var_context (var_context env)) in
+ process_rel_context
+ (fun newenv (na,c,t) ->
+ let id = next_name_away na !avoid in
+ avoid := id::!avoid;
+ push_rel (Name id,c,t) newenv)
+ env
+
(* Abstractions. *)
let evaluable_abst env = function
diff --git a/kernel/environ.mli b/kernel/environ.mli
index c8e3642be..616a11162 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -10,26 +10,64 @@ open Univ
open Sign
(*i*)
-(* Unsafe environments. We define here a datatype for environments.
+(*s Unsafe environments. We define here a datatype for environments.
Since typing is not yet defined, it is not possible to check the
informations added in environments, and that is what we speak here
of ``unsafe'' environments. *)
+type context
type env
+val empty_context : context
val empty_env : env
val universes : env -> universes
val context : env -> context
+val rel_context : env -> rel_context
val var_context : env -> var_context
-val push_var : identifier * typed_type -> env -> env
-val change_hyps :
- (typed_type signature -> typed_type signature) -> env -> env
-val change_name_rel : env -> int -> identifier -> env
-
-val push_rel : name * typed_type -> env -> env
-
+(* This forgets var and rel contexts *)
+val reset_context : env -> env
+
+(*s This concerns only the context of local vars referred by names
+ [var_context] *)
+val push_var : var_declaration -> env -> env
+val push_var_decl : identifier * typed_type -> env -> env
+val push_var_def : identifier * constr * typed_type -> env -> env
+val change_hyps : (var_context -> var_context) -> env -> env
+val instantiate_vars : var_context -> constr list -> (identifier * constr) list
+val pop_var : identifier -> env -> env
+
+(*s This concerns only the context of local vars referred by indice
+ [rel_context] *)
+val push_rel : rel_declaration -> env -> env
+val push_rel_decl : name * typed_type -> env -> env
+val push_rel_def : name * constr * typed_type -> env -> env
+val push_rels : rel_context -> env -> env
+val names_of_rel_context : env -> names_context
+
+(*s Returns also the substitution to be applied to rel's *)
+val push_rels_to_vars : env -> constr list * env
+
+(* Gives identifiers in var_context and rel_context *)
+val ids_of_context : env -> identifier list
+val map_context : (constr -> constr) -> env -> env
+
+(*s Recurrence on var_context *)
+val fold_var_context : (env -> var_declaration -> 'a -> 'a) -> env -> 'a -> 'a
+val process_var_context : (env -> var_declaration -> env) -> env -> env
+
+(* [process_var_context_both_sides f env] iters [f] on the var
+ declarations of env taking as argument both the initial segment, the
+ middle value and the tail segment *)
+val process_var_context_both_sides :
+ (env -> var_declaration -> var_context -> env) -> env -> env
+
+(*s Recurrence on rel_context *)
+val fold_rel_context : (env -> rel_declaration -> 'a -> 'a) -> env -> 'a -> 'a
+val process_rel_context : (env -> rel_declaration -> env) -> env -> env
+
+(*s add entries to environment *)
val set_universes : universes -> env -> env
val add_constraints : constraints -> env -> env
val add_constant :
@@ -41,13 +79,34 @@ val add_abstraction :
val new_meta : unit -> int
-val lookup_var : identifier -> env -> name * typed_type
-val lookup_rel : int -> env -> name * typed_type
+(*s Looks up in environment *)
+
+(* Looks up in the context of local vars referred by names (var_context) *)
+(* raises [Not_found] if the identifier is not found *)
+val lookup_var_type : identifier -> env -> typed_type
+val lookup_var_value : identifier -> env -> constr option
+val lookup_var : identifier -> env -> constr option * typed_type
+
+(* Looks up in the context of local vars referred by indice (rel_context) *)
+(* raises [Not_found] if the index points out of the context *)
+val lookup_rel_type : int -> env -> name * typed_type
+val lookup_rel_value : int -> env -> constr option
+
+(* Looks up in the context of global constant names *)
+(* raises [Not_found] if the required path is not found *)
val lookup_constant : section_path -> env -> constant_body
+
+(* Looks up in the context of global inductive names *)
+(* raises [Not_found] if the required path is not found *)
val lookup_mind : section_path -> env -> mutual_inductive_body
+(*s Miscellanous *)
val id_of_global : env -> sorts oper -> identifier
+val make_all_name_different : env -> env
+
+(*s Functions creating names for anonymous names *)
+
val id_of_name_using_hdchar : env -> constr -> name -> identifier
(* [named_hd env t na] just returns [na] is it defined, otherwise it
@@ -68,6 +127,15 @@ val prod_name : env -> name * constr * constr -> constr
val it_lambda_name : env -> constr -> (name * constr) list -> constr
val it_prod_name : env -> constr -> (name * constr) list -> constr
+val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
+val it_mkProd_or_LetIn_name : env -> constr -> rel_context -> constr
+
+val it_mkLambda_or_LetIn : constr -> rel_context -> constr
+val it_mkProd_or_LetIn : constr -> rel_context -> constr
+
+val it_mkNamedLambda_or_LetIn : constr -> var_context -> constr
+val it_mkNamedProd_or_LetIn : constr -> var_context -> constr
+
(* [lambda_create env (t,c)] builds [[x:t]c] where [x] is a name built
from [t]; [prod_create env (t,c)] builds [(x:t)c] where [x] is a
name built from [t] *)
diff --git a/kernel/evd.mli b/kernel/evd.mli
index e9f7818ff..3ae00f651 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -48,6 +48,6 @@ val is_evar : 'a evar_map -> evar -> bool
val is_defined : 'a evar_map -> evar -> bool
-val evar_hyps : 'a evar_info -> typed_type signature
+val evar_hyps : 'a evar_info -> var_context
val id_of_existential : evar -> identifier
diff --git a/kernel/generic.ml b/kernel/generic.ml
index 70acca45d..e7e1acc2f 100644
--- a/kernel/generic.ml
+++ b/kernel/generic.ml
@@ -304,10 +304,14 @@ let replace_vars var_alist =
in
if var_alist = [] then (function x -> x) else substrec 0
-let subst_varn str n = replace_vars [(str, (Rel n))]
-
(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
-let subst_var str = subst_varn str 1
+let subst_var str = replace_vars [(str, Rel 1)]
+
+(* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *)
+let subst_vars vars =
+ let _,subst =
+ List.fold_left (fun (n,l) var -> ((n+1),(var,Rel n)::l)) (1,[]) vars
+ in replace_vars (List.rev subst)
(* [Rel (n+m);...;Rel(n+1)] *)
diff --git a/kernel/generic.mli b/kernel/generic.mli
index 3f14efaee..8c2991ff6 100644
--- a/kernel/generic.mli
+++ b/kernel/generic.mli
@@ -60,8 +60,12 @@ val subst1 : 'a term -> 'a term -> 'a term
val global_vars : 'a term -> identifier list
val global_vars_set : 'a term -> Idset.t
-val subst_var : identifier -> 'a term -> 'a term
val replace_vars : (identifier * 'a term) list -> 'a term -> 'a term
+val subst_var : identifier -> 'a term -> 'a term
+
+(* [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t]
+ if two names are identical, the one of least indice is keeped *)
+val subst_vars : identifier list -> 'a term -> 'a term
(* [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
val rel_vect : int -> int -> 'a term array
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 197f5c299..0536b1f2f 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -27,10 +27,10 @@ open Typeops
type inductive_error =
(* These are errors related to inductive constructions in this module *)
- | NonPos of name list * constr * constr
- | NotEnoughArgs of name list * constr * constr
- | NotConstructor of name list * constr * constr
- | NonPar of name list * constr * int * constr * constr
+ | NonPos of env * constr * constr
+ | NotEnoughArgs of env * constr * constr
+ | NotConstructor of env * constr * constr
+ | NonPar of env * constr * int * constr * constr
| SameNamesTypes of identifier
| SameNamesConstructors of identifier * identifier
| NotAnArity of identifier
@@ -74,30 +74,22 @@ let mind_check_names mie =
for all the given types. *)
let mind_extract_params n c =
- let (l,c') = decompose_prod_n n c in (List.rev l,c')
+ let (l,c') = decompose_prod_n_assum n c in (l,c')
let extract nparams c =
- try mind_extract_params nparams c
+ try fst (mind_extract_params nparams c)
with UserError _ -> raise (InductiveError BadEntry)
-let check_params nparams params c =
- let eparams = fst (extract nparams c) in
- try
- List.iter2
- (fun (n1,t1) (n2,t2) ->
- if n1 <> n2 || strip_all_casts t1 <> strip_all_casts t2 then
- raise (InductiveError BadEntry))
- eparams params
- with Invalid_argument _ ->
- raise (InductiveError BadEntry)
+let check_params params params' =
+ if not (params = params') then raise (InductiveError BadEntry)
let mind_extract_and_check_params mie =
let nparams = mie.mind_entry_nparams in
match mie.mind_entry_inds with
| [] -> anomaly "empty inductive types declaration"
| (_,ar,_,_)::l ->
- let (params,_) = extract nparams ar in
- List.iter (fun (_,c,_,_) -> check_params nparams params c) l;
+ let params = extract nparams ar in
+ List.iter (fun (_,c,_,_) -> check_params params (extract nparams c)) l;
params
let decomp_all_DLAMV_name constr =
@@ -110,7 +102,8 @@ let decomp_all_DLAMV_name constr =
let mind_check_lc params mie =
let nparams = List.length params in
- let check_lc (_,_,_,lc) = List.iter (check_params nparams params) lc in
+ let check_lc (_,_,_,lc) =
+ List.iter (fun c -> check_params params (extract nparams c)) lc in
List.iter check_lc mie.mind_entry_inds
let mind_check_arities env mie =
@@ -130,8 +123,6 @@ let allowed_sorts issmall isunit = function
| Prop Null ->
if isunit then [prop;spec] else [prop]
-let is_small_type t = is_small t.typ
-
type ill_formed_ind =
| LocalNonPos of int
| LocalNotEnoughArgs of int
@@ -140,9 +131,9 @@ type ill_formed_ind =
exception IllFormedInd of ill_formed_ind
-let explain_ind_err ntyp lna nbpar c err =
+let explain_ind_err ntyp env0 nbpar c err =
let (lpar,c') = mind_extract_params nbpar c in
- let env = (List.map fst lpar)@lna in
+ let env = push_rels lpar env0 in
match err with
| LocalNonPos kt ->
raise (InductiveError (NonPos (env,c',Rel (kt+nbpar))))
@@ -290,14 +281,13 @@ let listrec_mconstr env ntypes nparams i indlc =
List.rev lrec
in check_constr_rec []
in
- let lna = it_dbenv (fun l na t -> na::l) [] (context env) in
Array.map
(fun c ->
let c = body_of_type c in
try
check_construct true (1+nparams) (decomp_par nparams c)
with IllFormedInd err ->
- explain_ind_err (ntypes-i+1) lna nparams c err)
+ explain_ind_err (ntypes-i+1) env nparams c err)
indlc
let is_recursive listind =
@@ -357,7 +347,7 @@ let cci_inductive env env_ar kind nparams finite inds cst =
let packets = Array.of_list (list_map_i one_packet 1 inds) in
{ mind_kind = kind;
mind_ntypes = ntypes;
- mind_hyps = keep_hyps (var_context env) ids;
+ mind_hyps = keep_hyps ids (var_context env);
mind_packets = packets;
mind_constraints = cst;
mind_singl = None;
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 5a7f040d9..46c0255a2 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -15,10 +15,10 @@ open Environ
type inductive_error =
(* These are errors related to inductive constructions in this module *)
- | NonPos of name list * constr * constr
- | NotEnoughArgs of name list * constr * constr
- | NotConstructor of name list * constr * constr
- | NonPar of name list * constr * int * constr * constr
+ | NonPos of env * constr * constr
+ | NotEnoughArgs of env * constr * constr
+ | NotConstructor of env * constr * constr
+ | NonPar of env * constr * int * constr * constr
| SameNamesTypes of identifier
| SameNamesConstructors of identifier * identifier
| NotAnArity of identifier
@@ -45,11 +45,11 @@ val mind_check_names : mutual_inductive_entry -> unit
[mind_entry_inds]. *)
val mind_extract_and_check_params :
- mutual_inductive_entry -> (name * constr) list
+ mutual_inductive_entry -> Sign.rel_context
-val mind_extract_params : int -> constr -> (name * constr) list * constr
+val mind_extract_params : int -> constr -> Sign.rel_context * constr
-val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
+val mind_check_lc : Sign.rel_context -> mutual_inductive_entry -> unit
(* [mind_check_arities] checks that the types declared for all the
inductive types are some arities. *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index cdfd27cd0..43b756651 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -18,6 +18,11 @@ type inductive_instance = {
mis_args : constr array;
mis_mip : one_inductive_body }
+
+let build_mis ((sp,tyi),args) mib =
+ { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args;
+ mis_mip = mind_nth_type_packet mib tyi }
+
let mis_ntypes mis = mis.mis_mib.mind_ntypes
let mis_nparams mis = mis.mis_mib.mind_nparams
@@ -36,9 +41,9 @@ let mis_consnames mis = mis.mis_mip.mind_consnames
let mis_inductive mis = ((mis.mis_sp,mis.mis_tyi),mis.mis_args)
let mis_typed_lc mis =
- let ids = ids_of_sign mis.mis_mib.mind_hyps in
+ let sign = mis.mis_mib.mind_hyps in
let args = Array.to_list mis.mis_args in
- Array.map (fun t -> Instantiate.instantiate_type ids t args)
+ Array.map (fun t -> Instantiate.instantiate_type sign t args)
mis.mis_mip.mind_nf_lc
let mis_lc mis = Array.map body_of_type (mis_typed_lc mis)
@@ -75,9 +80,9 @@ let mis_type_mconstruct i mispec =
typed_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1)
let mis_typed_arity mis =
- let idhyps = ids_of_sign mis.mis_mib.mind_hyps
+ let hyps = mis.mis_mib.mind_hyps
and largs = Array.to_list mis.mis_args in
- Instantiate.instantiate_type idhyps mis.mis_mip.mind_nf_arity largs
+ Instantiate.instantiate_type hyps mis.mis_mip.mind_nf_arity largs
(*
let mis_arity mispec = incast_type (mis_typed_arity mispec)
@@ -87,7 +92,7 @@ let mis_arity mis = body_of_type (mis_typed_arity mis)
let mis_params_ctxt mispec =
let paramsign,_ =
- decompose_prod_n mispec.mis_mib.mind_nparams
+ decompose_prod_n_assum mispec.mis_mib.mind_nparams
(body_of_type (mis_typed_arity mispec))
in paramsign
@@ -203,10 +208,8 @@ let find_mcoinductype env sigma c =
| _ -> raise Induc
(* raise Induc if not an inductive type *)
-let lookup_mind_specif ((sp,tyi),args) env =
- let mib = lookup_mind sp env in
- { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args;
- mis_mip = mind_nth_type_packet mib tyi }
+let lookup_mind_specif ((sp,tyi),args as ind) env =
+ build_mis ind (lookup_mind sp env)
let find_rectype env sigma ty =
let (mind,largs) = find_mrectype env sigma ty in
@@ -219,7 +222,7 @@ type constructor_summary = {
cs_cstr : constructor;
cs_params : constr list;
cs_nargs : int;
- cs_args : (name * constr) list;
+ cs_args : rel_context;
cs_concl_realargs : constr array
}
@@ -227,18 +230,18 @@ let lift_constructor n cs = {
cs_cstr = (let (csp,ctxt) = cs.cs_cstr in (csp,Array.map (lift n) ctxt));
cs_params = List.map (lift n) cs.cs_params;
cs_nargs = cs.cs_nargs;
- cs_args = lift_context n cs.cs_args;
+ cs_args = lift_rel_context n cs.cs_args;
cs_concl_realargs = Array.map (liftn n (cs.cs_nargs+1)) cs.cs_concl_realargs
}
let get_constructor (IndFamily (mispec,params)) j =
assert (j <= mis_nconstr mispec);
let typi = mis_type_nf_mconstruct j mispec in
- let (args,ccl) = decompose_prod (prod_applist typi params) in
+ let (args,ccl) = decompose_prod_assum (prod_applist typi params) in
let (_,vargs) = array_chop (mis_nparams mispec + 1) (destAppL (ensure_appl ccl)) in
{ cs_cstr = ith_constructor_of_inductive (mis_inductive mispec) j;
cs_params = params;
- cs_nargs = List.length args;
+ cs_nargs = rel_context_length args;
cs_args = args;
cs_concl_realargs = vargs }
@@ -277,8 +280,8 @@ let make_arity env dep indf s =
let build_branch_type env dep p cs =
let base = appvect (lift cs.cs_nargs p, cs.cs_concl_realargs) in
if dep then
- it_prod_name env
+ it_mkProd_or_LetIn_name env
(applist (base,[build_dependent_constructor cs]))
cs.cs_args
else
- prod_it base cs.cs_args
+ it_mkProd_or_LetIn base cs.cs_args
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 97118a517..3b45dad0b 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -27,6 +27,8 @@ corresponds various appropriated functions *)
type inductive_instance (* ex-[mind_specif] *)
+val build_mis : inductive -> mutual_inductive_body -> inductive_instance
+
val mis_index : inductive_instance -> int
val mis_ntypes : inductive_instance -> int
val mis_nconstr : inductive_instance -> int
@@ -43,7 +45,7 @@ val mis_consnames : inductive_instance -> identifier array
val mis_typed_arity : inductive_instance -> typed_type
val mis_inductive : inductive_instance -> inductive
val mis_arity : inductive_instance -> constr
-val mis_params_ctxt : inductive_instance -> (name * constr) list
+val mis_params_ctxt : inductive_instance -> rel_context
val mis_sort : inductive_instance -> sorts
val mis_type_mconstruct : int -> inductive_instance -> typed_type
@@ -98,7 +100,7 @@ type constructor_summary = {
cs_cstr : constructor;
cs_params : constr list;
cs_nargs : int;
- cs_args : (name * constr) list;
+ cs_args : rel_context;
cs_concl_realargs : constr array
}
@@ -163,6 +165,8 @@ val find_rectype : env -> 'a evar_map -> constr -> inductive_type
val get_constructors : inductive_family -> constructor_summary array
+val get_constructor : inductive_family -> int -> constructor_summary
+
(* [get_arity inf] returns the product and the sort of the
arity of the inductive family described by [is]; global parameters are
already instanciated; [indf] must be defined w.r.t. [env] and [sigma];
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 5ec0e01b0..9fb85961f 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -11,21 +11,22 @@ open Evd
open Declarations
open Environ
-let is_id_inst ids args =
- let is_id id = function
- | VAR id' -> id = id'
+let is_id_inst inst =
+ let is_id = function
+ | id, VAR id' -> id = id'
| _ -> false
in
- List.for_all2 is_id ids args
+ List.for_all is_id inst
-let instantiate_constr ids c args =
- if is_id_inst ids args then
+let instantiate_constr sign c args =
+ let inst = instantiate_vars sign args in
+ if is_id_inst inst then
c
else
- replace_vars (List.combine ids args) c
+ replace_vars inst c
-let instantiate_type ids tty args =
- typed_app (fun c -> instantiate_constr ids c args) tty
+let instantiate_type sign tty args =
+ typed_app (fun c -> instantiate_constr sign c args) tty
(* Constants. *)
@@ -33,8 +34,7 @@ let instantiate_type ids tty args =
let constant_type env sigma (sp,args) =
let cb = lookup_constant sp env in
(* TODO: check args *)
- instantiate_type
- (ids_of_sign cb.const_hyps) cb.const_type (Array.to_list args)
+ instantiate_type cb.const_hyps cb.const_type (Array.to_list args)
type const_evaluation_error = NotDefinedConst | OpaqueConst
@@ -48,8 +48,7 @@ let constant_value env cst =
match cb.const_body with
| Some v ->
let body = cook_constant v in
- instantiate_constr
- (ids_of_sign cb.const_hyps) body (Array.to_list args)
+ instantiate_constr cb.const_hyps body (Array.to_list args)
| None ->
anomalylabstrm "termenv__constant_value"
[< 'sTR "a defined constant with no body." >]
@@ -62,14 +61,14 @@ let existential_type sigma (n,args) =
let info = Evd.map sigma n in
let hyps = evar_hyps info in
(* TODO: check args [this comment was in Typeops] *)
- instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args)
+ instantiate_constr hyps info.evar_concl (Array.to_list args)
let existential_value sigma (n,args) =
let info = Evd.map sigma n in
let hyps = evar_hyps info in
match info.evar_body with
| Evar_defined c ->
- instantiate_constr (ids_of_sign hyps) c (Array.to_list args)
+ instantiate_constr hyps c (Array.to_list args)
| Evar_empty ->
anomaly "a defined existential with no body"
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 40601c604..d3454f1cc 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -5,15 +5,16 @@
open Names
open Term
open Evd
+open Sign
open Environ
(*i*)
(* Instantiation of constants and inductives on their real arguments. *)
val instantiate_constr :
- identifier list -> constr -> constr list -> constr
+ var_context -> constr -> constr list -> constr
val instantiate_type :
- identifier list -> typed_type -> constr list -> typed_type
+ var_context -> typed_type -> constr list -> typed_type
type const_evaluation_error = NotDefinedConst | OpaqueConst
exception NotEvaluableConst of const_evaluation_error
diff --git a/kernel/names.mli b/kernel/names.mli
index 1ccf3c12c..84b25d9cd 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -5,7 +5,7 @@
open Pp
(*i*)
-(* Names. *)
+(*s Identifiers *)
type identifier
type name = Name of identifier | Anonymous
@@ -41,6 +41,7 @@ type path_kind = CCI | FW | OBJ
val string_of_kind : path_kind -> string
val kind_of_string : string -> path_kind
+(*s Section paths *)
type section_path
val make_path : string list -> identifier -> path_kind -> section_path
@@ -71,6 +72,7 @@ val sp_gt : section_path * section_path -> bool
module Spset : Set.S with type elt = section_path
module Spmap : Map.S with type key = section_path
+(*s Specific paths for declarations *)
type inductive_path = section_path * int
type constructor_path = inductive_path * int
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c7acd792a..c4642b933 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -530,32 +530,27 @@ let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) =
let make_Fi j = mkFix ((recindices,nbodies-j-1),typedbodies) in
substl (list_tabulate make_Fi nbodies) bodies.(bodynum)
-let fix_recarg fix stack =
- match fix with
- | DOPN(Fix(recindices,bodynum),_) ->
- if 0 <= bodynum & bodynum < Array.length recindices then
- let recargnum = Array.get recindices bodynum in
- (try
- Some (recargnum, List.nth stack recargnum)
- with Failure "nth" | Invalid_argument "List.nth" ->
- None)
- else
- None
- | _ -> assert false
+let fix_recarg ((recindices,bodynum),_) stack =
+ if 0 <= bodynum & bodynum < Array.length recindices then
+ let recargnum = Array.get recindices bodynum in
+ (try
+ Some (recargnum, List.nth stack recargnum)
+ with Failure "nth" | Invalid_argument "List.nth" ->
+ None)
+ else
+ None
let reduce_fix whfun fix stack =
- match fix with
- | DOPN(Fix(recindices,bodynum),bodyvect) ->
- (match fix_recarg fix stack with
- | None -> (false,(fix,stack))
- | Some (recargnum,recarg) ->
- let (recarg'hd,_ as recarg') = whfun recarg [] in
- let stack' = list_assign stack recargnum (applist recarg') in
- (match recarg'hd with
- | DOPN(MutConstruct _,_) ->
- (true,(contract_fix (destFix fix),stack'))
- | _ -> (false,(fix,stack'))))
- | _ -> assert false
+ let dfix = destFix fix in
+ match fix_recarg dfix stack with
+ | None -> (false,(fix,stack))
+ | Some (recargnum,recarg) ->
+ let (recarg'hd,_ as recarg') = whfun recarg [] in
+ let stack' = list_assign stack recargnum (applist recarg') in
+ (match recarg'hd with
+ | DOPN(MutConstruct _,_) ->
+ (true,(contract_fix dfix,stack'))
+ | _ -> (false,(fix,stack')))
(* NB : Cette fonction alloue peu c'est l'appel
``let (recarg'hd,_ as recarg') = whfun recarg [] in''
@@ -1035,10 +1030,11 @@ let sort_of_arity env c = snd (splay_arity env Evd.empty c)
let decomp_n_prod env sigma n =
let rec decrec m ln c = if m = 0 then (ln,c) else
match whd_betadeltaiota env sigma c with
- | DOP2(Prod,a,DLAM(n,c_0)) -> decrec (m-1) ((n,a)::ln) c_0
+ | DOP2(Prod,a,DLAM(n,c0)) ->
+ decrec (m-1) (Sign.add_rel_decl (n,outcast_type a) ln) c0
| _ -> error "decomp_n_prod: Not enough products"
in
- decrec n []
+ decrec n Sign.empty_rel_context
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index fb623595a..bab5f446f 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -97,7 +97,7 @@ val splay_prod : env -> 'a evar_map -> constr -> (name * constr) list * constr
val splay_arity : env -> 'a evar_map -> constr -> (name * constr) list * sorts
val sort_of_arity : env -> constr -> sorts
val decomp_n_prod :
- env -> 'a evar_map -> int -> constr -> ((name * constr) list) * constr
+ env -> 'a evar_map -> int -> constr -> Sign.rel_context * constr
type 'a miota_args = {
mP : constr; (* the result type *)
@@ -130,7 +130,7 @@ val fold_commands : constr list -> 'a reduction_function
val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
val compute : 'a reduction_function
-val fix_recarg : constr -> 'a list -> (int * 'a) option
+val fix_recarg : fixpoint -> 'a list -> (int * 'a) option
val reduce_fix : (constr -> 'a list -> constr * constr list) -> constr ->
constr list -> bool * (constr * constr list)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d4b610a8e..c99bd4bbb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -48,7 +48,7 @@ let rec execute mf env cstr =
(relative env Evd.empty n, cst0)
| IsVar id ->
- (make_judge cstr (snd (lookup_var id env)), cst0)
+ (make_judge cstr (lookup_var_type id env), cst0)
| IsAbst _ ->
if evaluable_abst env cstr then
@@ -108,7 +108,7 @@ let rec execute mf env cstr =
| IsLambda (name,c1,c2) ->
let (j,cst1) = execute mf env c1 in
let var = assumption_of_judgment env Evd.empty j in
- let env1 = push_rel (name,var) env in
+ let env1 = push_rel_decl (name,var) env in
let (j',cst2) = execute mf env1 c2 in
let (j,cst3) = abs_rel env1 Evd.empty name var j' in
let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
@@ -117,7 +117,7 @@ let rec execute mf env cstr =
| IsProd (name,c1,c2) ->
let (j,cst1) = execute mf env c1 in
let varj = type_judgment env Evd.empty j in
- let env1 = push_rel (name,assumption_of_type_judgment varj) env in
+ let env1 = push_rel_decl (name,assumption_of_type_judgment varj) env in
let (j',cst2) = execute mf env1 c2 in
let (j,cst3) = gen_rel env1 Evd.empty name varj j' in
let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
@@ -137,7 +137,7 @@ and execute_fix mf env lar lfi vdef =
let nlara =
List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
let env1 =
- List.fold_left (fun env nvar -> push_rel nvar env) env nlara in
+ List.fold_left (fun env nvar -> push_rel_decl nvar env) env nlara in
let (vdefj,cst2) = execute_array mf env1 vdef in
let vdefv = Array.map j_val_only vdefj in
let cst3 = type_fixpoint env1 Evd.empty lfi lara vdefj in
@@ -239,8 +239,9 @@ let universes = universes
let context = context
let var_context = var_context
+let lookup_var_type = lookup_var_type
+let lookup_rel_type = lookup_rel_type
let lookup_var = lookup_var
-let lookup_rel = lookup_rel
let lookup_constant = lookup_constant
let lookup_mind = lookup_mind
let lookup_mind_specif = lookup_mind_specif
@@ -248,21 +249,27 @@ let lookup_mind_specif = lookup_mind_specif
(* Insertion of variables (named and de Bruijn'ed). They are now typed before
being added to the environment. *)
-let push_rel_or_var push (id,c) env =
+let push_rel_or_var_def push (id,c) env =
let (j,cst) = safe_machine env c in
let env' = add_constraints cst env in
- let var = assumption_of_judgment env' Evd.empty j in
- push (id,var) env'
+ push (id,j.uj_val,j.uj_type) env'
+
+let push_var_def nvar env = push_rel_or_var_def push_var_def nvar env
+
+let push_rel_def nrel env = push_rel_or_var_def push_rel_def nrel env
-let push_var nvar env = push_rel_or_var push_var nvar env
+let push_rel_or_var_decl push (id,c) env =
+ let (j,cst) = safe_machine_type env c in
+ let env' = add_constraints cst env in
+ let var = assumption_of_type_judgment j in
+ push (id,var) env'
-let push_rel nrel env = push_rel_or_var push_rel nrel env
+let push_var_decl nvar env = push_rel_or_var_decl push_var_decl nvar env
-let push_vars vars env =
- List.fold_left (fun env nvar -> push_var nvar env) env vars
+let push_rel_decl nrel env = push_rel_or_var_decl push_rel_decl nrel env
-let push_rels vars env =
- List.fold_left (fun env nvar -> push_rel nvar env) env vars
+let push_rels_with_univ vars env =
+ List.fold_left (fun env nvar -> push_rel_decl nvar env) env vars
(* Insertion of constants and parameters in environment. *)
@@ -291,7 +298,7 @@ let add_constant_with_value sp body typ env =
const_kind = kind_of_path sp;
const_body = Some (ref (Cooked body));
const_type = ty;
- const_hyps = keep_hyps (var_context env) ids;
+ const_hyps = keep_hyps ids (var_context env);
const_constraints = Constraint.union cst cst';
const_opaque = false }
in
@@ -305,7 +312,7 @@ let add_lazy_constant sp f t env =
const_kind = kind_of_path sp;
const_body = Some (ref (Recipe f));
const_type = assumption_of_judgment env' Evd.empty jt;
- const_hyps = keep_hyps (var_context env) ids;
+ const_hyps = keep_hyps ids (var_context env);
const_constraints = cst;
const_opaque = false }
in
@@ -327,7 +334,7 @@ let add_parameter sp t env =
const_kind = kind_of_path sp;
const_body = None;
const_type = assumption_of_judgment env' Evd.empty jt;
- const_hyps = keep_hyps (var_context env) ids;
+ const_hyps = keep_hyps ids (var_context env);
const_constraints = cst;
const_opaque = false }
in
@@ -344,24 +351,21 @@ let max_universe (s1,cst1) (s2,cst2) g =
| Type u1, _ -> s1, cst1
| _, _ -> s2, cst2
-(* This (re)computes informations relevant to extraction and the sort of
- an arity or type constructor *)
+(* This (re)computes informations relevant to extraction and the sort of an
+ arity or type constructor; we do not to recompute universes constraints *)
let rec infos_and_sort env t =
match kind_of_term t with
| IsProd (name,c1,c2) ->
- let (varj,cst1) = safe_machine_type env c1 in
+ let (varj,_) = safe_machine_type env c1 in
let var = assumption_of_type_judgment varj in
- let env1 = Environ.push_rel (name,var) env in
- let (infos,smax,cst) = infos_and_sort env1 c2 in
+ let env1 = Environ.push_rel_decl (name,var) env in
let s1 = varj.utj_type in
- let smax',cst' = max_universe (s1,cst1) (smax,cst) (universes env) in
let logic = not (is_info_type env Evd.empty varj) in
let small = is_small s1 in
- ((logic,small) :: infos, smax', cst')
+ (logic,small) :: (infos_and_sort env1 c2)
| IsCast (c,_) -> infos_and_sort env c
- | _ ->
- ([],prop (* = neutral element of max_universe *),Constraint.empty)
+ | _ -> []
(* [infos] is a sequence of pair [islogic,issmall] for each type in
the product of a constructor or arity *)
@@ -376,10 +380,12 @@ let is_unit arinfos constrsinfos =
| [constrinfos] -> is_logic_constr constrinfos && is_logic_arity arinfos
| _ -> false
-let small_unit constrsinfos (env_par,nparams,ar) =
+let small_unit constrsinfos (env_ar,nparams,ar) =
let issmall = List.for_all is_small constrsinfos in
- let (arinfos,_,_) =
- let (_,a) = mind_extract_params nparams ar in infos_and_sort env_par a in
+ let arinfos =
+ let (params,a) = mind_extract_params nparams ar in
+ let env_par = push_rels params env_ar in
+ infos_and_sort env_par a in
let isunit = is_unit arinfos constrsinfos in
issmall, isunit
@@ -391,14 +397,19 @@ let enforce_type_constructor arsort smax cst =
| _,_ -> cst
let type_one_constructor env_ar nparams arsort c =
- let (infos,max,cst1) =
+ let infos =
let (params,dc) = mind_extract_params nparams c in
let env_par = push_rels params env_ar in
infos_and_sort env_par dc in
- let (j,cst2) = safe_machine_type env_ar c in
- (*C'est idiot, cst1 et cst2 sont essentiellement des copies l'un de l'autre*)
- let cst3 =enforce_type_constructor arsort max (Constraint.union cst1 cst2) in
- (infos, assumption_of_type_judgment j, cst3)
+ (* Constructors are typed-checked here *)
+ let (j,cst) = safe_machine_type env_ar c in
+
+ (* If the arity is at some level Type arsort, then the sort of the
+ constructor must be below arsort; here we consider constructors with the
+ global parameters (which add a priori more constraints on their sort) *)
+ let cst2 = enforce_type_constructor arsort j.utj_type cst in
+
+ (infos, assumption_of_type_judgment j, cst2)
let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,vc) =
let arsort = sort_of_arity env_ar ar in
@@ -412,7 +423,7 @@ let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,vc) =
in
let vc' = Array.of_list jlc in
let issmall,isunit = small_unit constrsinfos (env_par,nparams,ar) in
- let (_,tyar) = lookup_rel (ninds+1-i) env_ar in
+ let (_,tyar) = lookup_rel_type (ninds+1-i) env_ar in
((id,tyar,cnames,issmall,isunit,vc'), cst)
let add_mind sp mie env =
@@ -425,7 +436,8 @@ let add_mind sp mie env =
let types_sign =
List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds
in
- let env_arities = push_rels types_sign env in
+ (* Arities with params are typed-checked here *)
+ let env_arities = push_rels_with_univ types_sign env in
let env_params = push_rels params env_arities in
let _,inds,cst =
List.fold_right
@@ -445,18 +457,10 @@ let add_mind sp mie env =
let add_constraints = add_constraints
-let pop_vars idl env =
- let rec remove n sign =
- if n = 0 then
- sign
- else
- if isnull_sign sign then anomaly "pop_vars"
- else
- let (id,_) = hd_sign sign in
- if not (List.mem id idl) then anomaly "pop_vars";
- remove (pred n) (tl_sign sign)
- in
- change_hyps (remove (List.length idl)) env
+let rec pop_vars idl env =
+ match idl with
+ | [] -> env
+ | id::l -> pop_vars l (Environ.pop_var id env)
let export = export
let import = import
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 5f6b9b073..6d8c80bd0 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -26,8 +26,13 @@ val universes : safe_environment -> universes
val context : safe_environment -> context
val var_context : safe_environment -> var_context
-val push_var : identifier * constr -> safe_environment -> safe_environment
-val push_rel : name * constr -> safe_environment -> safe_environment
+val push_var_decl : identifier * constr -> safe_environment -> safe_environment
+val push_var_def : identifier * constr -> safe_environment -> safe_environment
+(*
+val push_rel_decl : name * constr -> safe_environment -> safe_environment
+val push_rel_def : name * constr -> safe_environment -> safe_environment
+*)
+
val add_constant :
section_path -> constant_entry -> safe_environment -> safe_environment
val add_lazy_constant :
@@ -42,8 +47,10 @@ val add_constraints : constraints -> safe_environment -> safe_environment
val pop_vars : identifier list -> safe_environment -> safe_environment
-val lookup_var : identifier -> safe_environment -> name * typed_type
+val lookup_var : identifier -> safe_environment -> constr option * typed_type
+(*
val lookup_rel : int -> safe_environment -> name * typed_type
+*)
val lookup_constant : section_path -> safe_environment -> constant_body
val lookup_mind : section_path -> safe_environment -> mutual_inductive_body
val lookup_mind_specif : inductive -> safe_environment -> inductive_instance
diff --git a/kernel/sign.ml b/kernel/sign.ml
index fb2c8d31d..edee43885 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -8,251 +8,190 @@ open Term
(* Signatures *)
-type 'a signature = identifier list * 'a list
-type 'a db_signature = (name * 'a) list
-type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature
-
-let gLOB hyps = ENVIRON (hyps,[])
-
-let ids_of_sign (idl,_) = idl
-let vals_of_sign (_,vals) = vals
-let add_sign (id,ty) (idl,tyl) = (id::idl,ty::tyl)
-let sign_it f (idl,tyl) e = List.fold_right2 f idl tyl e
-let it_sign f e (idl,tyl) = List.fold_left2 f e idl tyl
-let nil_sign = ([],[])
-let rev_sign (idl,tyl) = (List.rev idl, List.rev tyl)
-let map_sign_typ f (idl,tyl) = (idl, List.map f tyl)
-let concat_sign (idl1,tyl1) (idl2,tyl2) = (idl1@idl2, tyl1@tyl2)
-let diff_sign (idl1,tyl1) (idl2,tyl2) =
- (list_subtract idl1 idl2, list_subtract tyl1 tyl2)
-let nth_sign (idl,tyl) n = (List.nth idl (n-1), List.nth tyl (n-1))
-let map_sign_graph f (ids,tys) = List.map2 f ids tys
-
-let isnull_sign = function
- | ([],[]) -> true
- | (_::_,_::_) -> false
- | _ -> invalid_arg "isnull_sign"
-
-let hd_sign = function
- | (id::_,ty::_) -> (id,ty)
- | _ -> failwith "hd_sign"
-
-let tl_sign = function
- | (_::idl,_::tyl) -> (idl,tyl)
- | _ -> failwith "tl_sign"
-
-let lookup_sign id (dom,rang) =
- let rec aux = function
- | ([], []) -> raise Not_found
- | ((id'::id'l), (ty::tyl)) -> if id' = id then (id',ty) else aux (id'l,tyl)
- | _ -> anomaly "Names: lookup_sign"
+let add d sign = d::sign
+let map f = List.map (fun (na,c,t) -> (na,option_app f c,typed_app f t))
+
+let add_decl (n,t) sign = (n,None,t)::sign
+let add_def (n,c,t) sign = (n,Some c,t)::sign
+
+type var_declaration = identifier * constr option * typed_type
+type var_context = var_declaration list
+
+let add_var = add
+let add_var_decl = add_decl
+let add_var_def = add_def
+let rec lookup_id_type id = function
+ | (id',c,t) :: _ when id=id' -> t
+ | _ :: sign -> lookup_id_type id sign
+ | [] -> raise Not_found
+let rec lookup_id_value id = function
+ | (id',c,t) :: _ when id=id' -> c
+ | _ :: sign -> lookup_id_value id sign
+ | [] -> raise Not_found
+let rec lookup_id id = function
+ | (id',c,t) :: _ when id=id' -> (c,t)
+ | _ :: sign -> lookup_id id sign
+ | [] -> raise Not_found
+let empty_var_context = []
+let pop_var id = function
+ | (id',_,_) :: sign -> assert (id = id'); sign
+ | [] -> assert false
+let ids_of_var_context = List.map (fun (id,_,_) -> id)
+let map_var_context = map
+let rec mem_var_context id = function
+ | (id',_,_) :: _ when id=id' -> true
+ | _ :: sign -> mem_var_context id sign
+ | [] -> false
+let fold_var_context = List.fold_right
+let fold_var_context_both_sides = list_fold_right_and_left
+let it_var_context_quantifier f = List.fold_left (fun c d -> f d c)
+
+type rel_declaration = name * constr option * typed_type
+type rel_context = rel_declaration list
+
+let add_rel = add
+let add_rel_decl = add_decl
+let add_rel_def = add_def
+let lookup_rel_type n sign =
+ let rec lookrec = function
+ | (1, (na,_,t) :: _) -> (na,t)
+ | (n, _ :: sign) -> lookrec (n-1,sign)
+ | (_, []) -> raise Not_found
in
- aux (dom,rang)
-
-let list_of_sign (ids,tys) =
- try List.combine ids tys
- with _ -> anomaly "Corrupted signature"
-
-
-let make_sign = List.split
-let do_sign f (ids,tys) = List.iter2 f ids tys
-
-let uncons_sign = function
- | (id::idl,ty::tyl) -> ((id,ty),(idl,tyl))
- | _ -> anomaly "signatures are being manipulated in a non-abstract way"
-
-let sign_length (idl,tyl) =
- let lenid = List.length idl
- and lenty = List.length tyl in
- if lenid = lenty then
- lenid
- else
- invalid_arg "lookup_sign"
-
-let mem_sign sign id = List.mem id (ids_of_sign sign)
-
-let modify_sign id ty =
- let rec modrec = function
- | [],[] -> invalid_arg "modify_sign"
- | sign ->
- let (id',ty') = hd_sign sign in
- if id = id' then
- add_sign (id,ty) (tl_sign sign)
- else
- add_sign (id',ty') (modrec (tl_sign sign))
+ lookrec (n,sign)
+let lookup_rel_value n sign =
+ let rec lookrec = function
+ | (1, (_,c,_) :: _) -> c
+ | (n, _ :: sign ) -> lookrec (n-1,sign)
+ | (_, []) -> raise Not_found
in
- modrec
-
-let exists_sign f =
- let rec exrec sign =
- if isnull_sign sign then
- false
- else
- let ((id,t),tl) = uncons_sign sign in
- f id t or exrec tl
+ lookrec (n,sign)
+let rec lookup_rel_id id sign =
+ let rec lookrec = function
+ | (n, (Anonymous,_,_)::l) -> lookrec (n+1,l)
+ | (n, (Name id',_,t)::l) -> if id' = id then (n,t) else lookrec (n+1,l)
+ | (_, []) -> raise Not_found
in
- exrec
-
-(* [sign_prefix id sign] returns the signature up to and including id,
- with all later assumptions stripped off. It is an error to call it
- with a signature not containing id, and that error is generated
- with error. *)
-
-let sign_prefix id sign =
- let rec prefrec sign =
- if isnull_sign sign then
- error "sign_prefix"
- else
- let ((id',t),sign') = uncons_sign sign in
- if id' = id then sign else prefrec sign'
+ lookrec (1,sign)
+let empty_rel_context = []
+let rel_context_length = List.length
+let lift_rel_context n sign =
+ let rec liftrec k = function
+ | (na,c,t)::sign ->
+ (na,option_app (liftn n k) c,typed_app (liftn n k) t)
+ ::(liftrec (k-1) sign)
+ | [] -> []
+ in
+ liftrec (rel_context_length sign) sign
+let concat_rel_context = (@)
+let ids_of_rel_context sign =
+ List.fold_right
+ (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
+ sign []
+let names_of_rel_context = List.map (fun (na,_,_) -> na)
+let decls_of_rel_context sign =
+ List.fold_right
+ (fun (na,c,t) l -> match c with Some _ -> l | None -> (na,body_of_type t)::l)
+ sign []
+let map_rel_context = map
+
+let instantiate_sign sign args =
+ let rec instrec = function
+ | ((id,None,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args))
+ | ((id,Some c,_) :: _, args) -> (id,c) :: (instrec (sign,args))
+ | ([],[]) -> []
+ | ([],_) | (_,[]) ->
+ anomaly "Signature and its instance do not match"
in
- prefrec sign
-
-let add_sign_after whereid (id,t) sign =
- let rec addrec sign =
- if isnull_sign sign then
- error "add_sign_after"
- else
- let ((id',t'),sign') = uncons_sign sign in
- if id' = whereid then add_sign (id,t) sign
- else add_sign (id',t') (addrec sign')
+ instrec (sign,args)
+
+(* [keep_hyps sign ids] keeps the part of the signature [sign] which
+ contains the variables of the set [ids], and recursively the variables
+ contained in the types of the needed variables. *)
+
+let rec keep_hyps needed = function
+ | (id,copt,t as d) ::sign when Idset.mem id needed ->
+ let globc =
+ match copt with
+ | None -> Idset.empty
+ | Some c -> global_vars_set c in
+ let needed' =
+ Idset.union (global_vars_set (body_of_type t))
+ (Idset.union globc needed) in
+ d :: (keep_hyps needed' sign)
+ | _::sign -> keep_hyps needed sign
+ | [] -> []
+
+(*************************)
+(* Names environments *)
+(*************************)
+type names_context = name list
+let add_name n nl = n::nl
+let lookup_name_of_rel p names =
+ try List.nth names (p-1)
+ with Failure "nth" -> raise Not_found
+let rec lookup_rel_of_name id names =
+ let rec lookrec n = function
+ | Anonymous :: l -> lookrec (n+1) l
+ | (Name id') :: l -> if id' = id then n else lookrec (n+1) l
+ | [] -> raise Not_found
in
- addrec sign
-
-let add_sign_replacing whereid (id,t) sign =
- let rec addrec sign =
- if isnull_sign sign then
- error "add_replacing_after"
- else
- let ((id',t'),sign') = uncons_sign sign in
- if id' = whereid then add_sign (id,t) sign'
- else add_sign (id',t') (addrec sign')
+ lookrec 1 names
+let empty_names_context = []
+
+(*********************************)
+(* Term destructors *)
+(*********************************)
+
+(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
+ ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
+let decompose_prod_assum =
+ let rec prodec_rec l = function
+ | DOP2(Prod,t,DLAM(x,c)) ->
+ prodec_rec (add_rel_decl (x,outcast_type t) l) c
+(* | Letin,t,DLAM(x,c)) ->
+ prodec_rec (add_rel_def (x,c,outcast_type t) l) c*)
+ | DOP2(Cast,c,_) -> prodec_rec l c
+ | c -> l,c
in
- addrec sign
-
-(* [prepend_sign Gamma1 Gamma2]
- prepends Gamma1 to the front of Gamma2, given that their namespaces
- are distinct. *)
-
-let prepend_sign gamma1 gamma2 =
- if [] = list_intersect (ids_of_sign gamma1) (ids_of_sign gamma2) then
- let (ids1,vals1) = gamma1
- and (ids2,vals2) = gamma2 in
- (ids1@ids2, vals1@vals2)
- else
- invalid_arg "prepend_sign"
-
-let dunbind default sign ty = function
- | DLAM(na,c) ->
- let id = next_ident_away (id_of_name default na) (ids_of_sign sign) in
- (add_sign (id,ty) sign, subst1 (VAR id) c)
- | _ -> invalid_arg "dunbind default"
-
-let dunbindv default sign ty = function
- | DLAMV(na,c) ->
- let id = next_ident_away (id_of_name default na) (ids_of_sign sign) in
- (add_sign (id,ty) sign,Array.map (subst1 (VAR id)) c)
- | _ -> invalid_arg "dunbindv default"
-
-let dbind sign c =
- let (id,ty) = hd_sign sign
- and sign' = tl_sign sign in
- (ty,DLAM(Name id,subst_var id c))
-
-let dbindv sign cl =
- let (id,ty) = hd_sign sign
- and sign' = tl_sign sign in
- (ty,DLAMV(Name id,Array.map (subst_var id) cl))
-
-(* de Bruijn environments *)
-
-let nil_dbsign = []
-
-(* Signatures + de Bruijn environments *)
-
-let dbenv_it f (ENVIRON(_,dbs)) init =
- List.fold_right (fun (na,t) v -> f na t v) dbs init
-
-let it_dbenv f init (ENVIRON(_,dbs)) =
- List.fold_left (fun v (na,t) -> f v na t) init dbs
-
-let isnull_rel_env (ENVIRON(_,dbs)) = (dbs = [])
-let uncons_rel_env (ENVIRON(sign,dbs)) = List.hd dbs,ENVIRON(sign,List.tl dbs)
-
-let ids_of_env (ENVIRON(sign,dbenv)) =
- let filter (n,_) l = match n with (Name id) -> id::l | Anonymous -> l in
- (ids_of_sign sign) @ (List.fold_right filter dbenv [])
-
-let get_globals (ENVIRON(g,_)) = g
-let get_rels (ENVIRON(_,r)) = r
-
-let add_rel (n,x) (ENVIRON(g,r)) = (ENVIRON(g,(n,x)::r))
-
-let add_glob (id,x) (ENVIRON((dom,rang),r)) = (ENVIRON((id::dom,x::rang),r))
-
-let lookup_glob id (ENVIRON((dom,rang),_)) =
- let rec aux = function
- | ([], []) -> raise Not_found
- | ((id'::id'l), (ty::tyl)) -> if id' = id then (id',ty) else aux (id'l,tyl)
- | _ -> anomaly "Names: lookup_glob"
+ prodec_rec empty_rel_context
+
+(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
+ ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
+let decompose_lam_assum =
+ let rec lamdec_rec l = function
+ | DOP2(Lambda,t,DLAM(x,c)) ->
+ lamdec_rec (add_rel_decl (x,outcast_type t) l) c
+(* | Letin,t,DLAM(x,c)) ->
+ lamdec_rec (add_rel_def (x,c,outcast_type t) l) c*)
+ | DOP2(Cast,c,_) -> lamdec_rec l c
+ | c -> l,c
in
- aux (dom,rang)
-
-let mem_glob id (ENVIRON((dom,_),_)) = List.mem id dom
-
-let lookup_rel n (ENVIRON(_,r)) =
- let rec lookrec n l = match (n,l) with
- | (1, ((na,x)::l)) -> (na,x)
- | (n, (_::l)) -> lookrec (n-1) l
- | (_, []) -> raise Not_found
+ lamdec_rec empty_rel_context
+
+(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T
+ into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+let decompose_prod_n_assum n =
+ if n < 0 then error "decompose_prod_n: integer parameter must be positive";
+ let rec prodec_rec l n c =
+ if n=0 then l,c
+ else match c with
+ | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec (add_rel_decl (x,outcast_type t) l) (n-1) c
+ | DOP2(Cast,c,_) -> prodec_rec l n c
+ | c -> error "decompose_prod_n: not enough products"
in
- lookrec n r
-
-let rec lookup_rel_id id (ENVIRON(_,r)) =
- let rec lookrec = function
- | (n, ((Anonymous,x)::l)) -> lookrec (n+1,l)
- | (n, ((Name id',x)::l)) -> if id' = id then (n,x) else lookrec (n+1,l)
- | (_, []) -> raise Not_found
+ prodec_rec empty_rel_context n
+
+(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T
+ into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+let decompose_lam_n_assum n =
+ if n < 0 then error "decompose_lam_n: integer parameter must be positive";
+ let rec lamdec_rec l n c =
+ if n=0 then l,c
+ else match c with
+ | DOP2(Lambda,t,DLAM(x,c)) -> lamdec_rec (add_rel_decl (x,outcast_type t) l) (n-1) c
+ | DOP2(Cast,c,_) -> lamdec_rec l n c
+ | c -> error "decompose_lam_n: not enough abstractions"
in
- lookrec (1,r)
-
-let map_rel_env f (ENVIRON(g,r)) =
- ENVIRON (g,List.map (fun (na,x) -> (na,f x)) r)
-
-let map_var_env f (ENVIRON((dom,rang),r)) =
- ENVIRON (List.fold_right2
- (fun na x (doml,rangl) -> (na::doml,(f x)::rangl))
- dom rang ([],[]),r)
-
-let number_of_rels (ENVIRON(_,db)) = List.length db
-
-let change_name_env (ENVIRON(sign,db)) j id =
- match list_chop (j-1) db with
- | db1,((_,ty)::db2) -> ENVIRON(sign,db1@(Name id,ty)::db2)
- | _ -> raise Not_found
-
-let unitize_env env = map_rel_env (fun _ -> ()) env
-
-type ('b,'a) search_result =
- | GLOBNAME of identifier * 'b
- | RELNAME of int * 'a
-
-let lookup_id id env =
- try
- let (x,y) = lookup_rel_id id env in RELNAME(x,y)
- with
- | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y)
-
-let make_all_name_different (ENVIRON((dom,_) as sign,dbs)) =
- let _,newdbs =
- List.fold_right
- (fun (na,t) (avoid,newdbs) ->
- let id = next_name_away na avoid in
- (id::avoid),((Name id,t)::newdbs))
- dbs (dom,[])
- in ENVIRON (sign,newdbs)
-
-type 'b assumptions = (typed_type,'b) sign
-type context = (typed_type,typed_type) sign
-type var_context = typed_type signature
+ lamdec_rec empty_rel_context n
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 763a67471..3add55894 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -7,107 +7,75 @@ open Generic
open Term
(*i*)
-(* Signatures of named variables. *)
-
-type 'a signature
-
-val nil_sign : 'a signature
-val add_sign : (identifier * 'a) -> 'a signature -> 'a signature
-val lookup_sign : identifier -> 'a signature -> (identifier * 'a)
-
-val rev_sign : 'a signature -> 'a signature
-val map_sign_typ : ('a -> 'b) -> 'a signature -> 'b signature
-val isnull_sign : 'a signature -> bool
-val hd_sign : 'a signature -> identifier * 'a
-val tl_sign : 'a signature -> 'a signature
-
-(* [sign_it f sign a] iters [f] on [sign] starting from [a] and
- peeling [sign] from the oldest declaration *)
-
-val sign_it : (identifier -> 'a -> 'b -> 'b) -> 'a signature -> 'b -> 'b
-
-(* [it_sign f a sign] iters [f] on [sign] starting from [a] and
- peeling [sign] from the more recent declaration *)
-
-val it_sign : ('b -> identifier -> 'a -> 'b) -> 'b -> 'a signature -> 'b
-
-val concat_sign : 'a signature -> 'a signature -> 'a signature
-
-val ids_of_sign : 'a signature -> identifier list
-val vals_of_sign : 'a signature -> 'a list
-
-val nth_sign : 'a signature -> int -> (identifier * 'a)
-val map_sign_graph : (identifier -> 'a -> 'b) -> 'a signature -> 'b list
-val list_of_sign : 'a signature -> (identifier * 'a) list
-val make_sign : (identifier * 'a) list -> 'a signature
-val do_sign : (identifier -> 'a -> unit) -> 'a signature -> unit
-val uncons_sign : 'a signature -> (identifier * 'a) * 'a signature
-val sign_length : 'a signature -> int
-val mem_sign : 'a signature -> identifier -> bool
-val modify_sign : identifier -> 'a -> 'a signature -> 'a signature
-
-val exists_sign : (identifier -> 'a -> bool) -> 'a signature -> bool
-val sign_prefix : identifier -> 'a signature -> 'a signature
-val add_sign_after :
- identifier -> (identifier * 'a) -> 'a signature -> 'a signature
-val add_sign_replacing :
- identifier -> (identifier * 'a) -> 'a signature -> 'a signature
-val prepend_sign : 'a signature -> 'a signature -> 'a signature
-
-val dunbind : identifier -> 'a signature -> 'a -> 'b term
- -> 'a signature * 'b term
-val dunbindv : identifier -> 'a signature -> 'a -> 'b term
- -> 'a signature * 'b term array
-val dbind : 'a signature -> 'b term -> 'a * 'b term
-val dbindv : 'a signature -> 'b term array -> 'a * 'b term
-
-(*s Signatures with named and de Bruijn variables. *)
-
-type 'a db_signature
-type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature
-
-val gLOB : 'b signature -> ('b,'a) sign
-
-val add_rel : (name * 'a) -> ('b,'a) sign -> ('b,'a) sign
-val add_glob : (identifier * 'b) -> ('b,'a) sign -> ('b,'a) sign
-val lookup_glob : identifier -> ('b,'a) sign -> (identifier * 'b)
-val lookup_rel : int -> ('b,'a) sign -> (name * 'a)
-val mem_glob : identifier -> ('b,'a) sign -> bool
-
-val nil_dbsign : 'a db_signature
-val get_globals : ('b,'a) sign -> 'b signature
-val get_rels : ('b,'a) sign -> 'a db_signature
-val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) sign -> 'c -> 'c
-val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) sign -> 'c
-val map_rel_env : ('a -> 'b) -> ('c,'a) sign -> ('c,'b) sign
-val map_var_env : ('c -> 'b) -> ('c,'a) sign -> ('b,'a) sign
-val isnull_rel_env : ('a,'b) sign -> bool
-val uncons_rel_env : ('a,'b) sign -> (name * 'b) * ('a,'b) sign
-val ids_of_env : ('a, 'b) sign -> identifier list
-val number_of_rels : ('b,'a) sign -> int
-
-(*i This is for Cases i*)
-(* raise [Not_found] if the integer is out of range *)
-val change_name_env: ('a, 'b) sign -> int -> identifier -> ('a, 'b) sign
-
-val make_all_name_different : ('a, 'b) sign -> ('a, 'b) sign
-
-type ('b,'a) search_result =
- | GLOBNAME of identifier * 'b
- | RELNAME of int * 'a
-
-val lookup_id : identifier -> ('b,'a) sign -> ('b,'a) search_result
-
-
-type 'b assumptions = (typed_type,'b) sign
-type context = (typed_type,typed_type) sign
-type var_context = typed_type signature
-
-val unitize_env : 'a assumptions -> unit assumptions
-
-
-
-
-
-
-
+(*s Signatures of _ordered_ named variables, intended to be accessed by name *)
+
+type var_context = var_declaration list
+
+val add_var : identifier * constr option * typed_type -> var_context -> var_context
+val add_var_decl : identifier * typed_type -> var_context -> var_context
+val add_var_def : identifier * constr * typed_type -> var_context ->var_context
+val lookup_id : identifier -> var_context -> constr option * typed_type
+val lookup_id_type : identifier -> var_context -> typed_type
+val lookup_id_value : identifier -> var_context -> constr option
+val pop_var : identifier -> var_context -> var_context
+val empty_var_context : var_context
+val ids_of_var_context : var_context -> identifier list
+val map_var_context : (constr -> constr) -> var_context -> var_context
+val mem_var_context : identifier -> var_context -> bool
+val fold_var_context : (var_declaration -> 'a -> 'a) -> var_context -> 'a -> 'a
+val fold_var_context_both_sides :
+ ('a -> var_declaration -> var_context -> 'a) -> var_context -> 'a -> 'a
+val it_var_context_quantifier :
+ (var_declaration -> constr -> constr) -> constr -> var_context -> constr
+val instantiate_sign : var_context -> constr list -> (identifier * constr) list
+val keep_hyps : Idset.t -> var_context -> var_context
+
+(*s Signatures of ordered optionally named variables, intended to be
+ accessed by de Bruijn indices *)
+
+type rel_context = rel_declaration list
+
+val add_rel : (name * constr option * typed_type) -> rel_context -> rel_context
+val add_rel_decl : (name * typed_type) -> rel_context -> rel_context
+val add_rel_def : (name * constr * typed_type) -> rel_context -> rel_context
+val lookup_rel_type : int -> rel_context -> name * typed_type
+val lookup_rel_value : int -> rel_context -> constr option
+val lookup_rel_id : identifier -> rel_context -> int * typed_type
+val empty_rel_context : rel_context
+val rel_context_length : rel_context -> int
+val lift_rel_context : int -> rel_context -> rel_context
+val concat_rel_context : newer:rel_context -> older:rel_context -> rel_context
+val ids_of_rel_context : rel_context -> identifier list
+val decls_of_rel_context : rel_context -> (name * constr) list
+val map_rel_context : (constr -> constr) -> rel_context -> rel_context
+
+(*s This is used to translate names into de Bruijn indices and
+ vice-versa without to care about typing information *)
+
+type names_context
+val add_name : name -> names_context -> names_context
+val lookup_name_of_rel : int -> names_context -> name
+val lookup_rel_of_name : identifier -> names_context -> int
+val names_of_rel_context : rel_context -> names_context
+val empty_names_context : names_context
+
+(*s Term destructors *)
+
+(* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ including letins
+ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a
+ product nor a let. *)
+val decompose_prod_assum : constr -> rel_context * constr
+
+(* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ including letins
+ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a
+ lambda nor a let. *)
+val decompose_lam_assum : constr -> rel_context * constr
+
+(* Given a positive integer n, transforms a product term
+ $(x_1:T_1)..(x_n:T_n)T$
+ into the pair $([(xn,Tn);...;(x1,T1)],T)$. *)
+val decompose_prod_n_assum : int -> constr -> rel_context * constr
+
+(* Given a positive integer $n$, transforms a lambda term
+ $[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *)
+val decompose_lam_n_assum : int -> constr -> rel_context * constr
diff --git a/kernel/term.ml b/kernel/term.ml
index 8b5b05679..6b3aa5bec 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -107,6 +107,9 @@ let outcast_type x = x
let typed_combine f g t u = f t u
(**)
+type var_declaration = identifier * constr option * typed_type
+type rel_declaration = name * constr option * typed_type
+
(****************************************************************************)
(* Functions for dealing with constr terms *)
(****************************************************************************)
@@ -159,16 +162,53 @@ let mkCast t1 t2 =
(* Constructs the product (x:t1)t2 *)
let mkProd x t1 t2 = (DOP2 (Prod,t1,(DLAM (x,t2))))
-
-(* non-dependent product t1 -> t2 *)
-let mkArrow t1 t2 = mkProd Anonymous t1 t2
-
-(* named product *)
-let mkNamedProd name typ c = mkProd (Name name) typ (subst_var name c)
+let mkNamedProd id typ c = mkProd (Name id) typ (subst_var id c)
+let mkProd_string s t c = mkProd (Name (id_of_string s)) t c
(* Constructs the abstraction [x:t1]t2 *)
let mkLambda x t1 t2 = (DOP2 (Lambda,t1,(DLAM (x,t2))))
-let mkNamedLambda name typ c = mkLambda (Name name) typ (subst_var name c)
+let mkNamedLambda id typ c = mkLambda (Name id) typ (subst_var id c)
+let mkLambda_string s t c = mkLambda (Name (id_of_string s)) t c
+
+(* Constructs [x=c_1:t]c_2 *)
+let mkLetIn x c1 t c2 = failwith "TODO"
+let mkNamedLetIn id c1 t c2 = mkLetIn (Name id) c1 t (subst_var id c2)
+
+(* Constructs either [(x:t)c] or [[x=b:t]c] *)
+let mkProd_or_LetIn (na,body,t) c =
+ match body with
+ | None -> mkProd na t c
+ | Some b -> mkLetIn na b t c
+
+let mkNamedProd_or_LetIn (id,body,t) c =
+ match body with
+ | None -> mkNamedProd id (body_of_type t) c
+ | Some b -> mkNamedLetIn id b (body_of_type t) c
+
+(* Constructs either [[x:t]c] or [[x=b:t]c] *)
+let mkLambda_or_LetIn (na,body,t) c =
+ match body with
+ | None -> mkLambda na t c
+ | Some b -> mkLetIn na b t c
+
+let mkNamedLambda_or_LetIn (id,body,t) c =
+ match body with
+ | None -> mkNamedLambda id (body_of_type t) c
+ | Some b -> mkNamedLetIn id b (body_of_type t) c
+
+(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
+let mkProd_wo_LetIn (na,body,t) c =
+ match body with
+ | None -> mkProd na (body_of_type t) c
+ | Some b -> subst1 b c
+
+let mkNamedProd_wo_LetIn (id,body,t) c =
+ match body with
+ | None -> mkNamedProd id (body_of_type t) c
+ | Some b -> subst1 b (subst_var id c)
+
+(* non-dependent product t1 -> t2 *)
+let mkArrow t1 t2 = mkProd Anonymous t1 t2
(* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
let mkAppL a = DOPN (AppL, a)
@@ -179,7 +219,7 @@ let mkAppList a l = DOPN (AppL, Array.of_list (a::l))
let mkConst (sp,a) = DOPN (Const sp, a)
(* Constructs an existential variable *)
-let mkEvar n a = DOPN (Evar n, a)
+let mkEvar (n,a) = DOPN (Evar n, a)
(* Constructs an abstract object *)
let mkAbst sp a = DOPN (Abst sp, a)
@@ -215,9 +255,6 @@ let mkMutCaseA ci p c ac =
with fn [ctxn] = bn.
where the lenght of the jth context is ij.
-
- Warning: as an invariant the ti are casted during the Fix formation;
- these casts are then used by destFix
*)
(* Here, we assume the body already constructed *)
@@ -509,10 +546,6 @@ let destCase = function
where the lenght of the jth context is ij.
*)
-let out_fixcast = function
- | DOP2 (Cast, b, DOP0 (Sort s)) as c -> outcast_type c
- | _ -> anomaly "destFix: malformed recursive definition"
-
let destGralFix a =
let nbofdefs = Array.length a in
let types = Array.sub a 0 (nbofdefs-1) in
@@ -529,26 +562,13 @@ let destGralFix a =
let destFix = function
| DOPN (Fix (recindxs,i),a) ->
let (types,funnames,bodies) = destGralFix a in
- ((recindxs,i),((*Array.map out_fixcast *) types,funnames,bodies))
+ ((recindxs,i),(types,funnames,bodies))
| _ -> invalid_arg "destFix"
let destCoFix = function
| DOPN ((CoFix i),a) ->
let (types,funnames,bodies) = destGralFix a in
- (i,((*Array.map out_fixcast *) types,funnames,bodies))
- | _ -> invalid_arg "destCoFix"
-
-(* Provisoire, le temps de maitriser les cast *)
-let destUntypedFix = function
- | DOPN (Fix (recindxs,i),a) ->
- let (types,funnames,bodies) = destGralFix a in
- (recindxs,i,types,funnames,bodies)
- | _ -> invalid_arg "destFix"
-
-let destUntypedCoFix = function
- | DOPN (CoFix i,a) ->
- let (types,funnames,bodies) = destGralFix a in
- (i,types,funnames,bodies)
+ (i,(types,funnames,bodies))
| _ -> invalid_arg "destCoFix"
(**********************************************************************)
@@ -636,9 +656,6 @@ let abs_implicit c = mkLambda Anonymous mkImplicit c
let lambda_implicit a = mkLambda (Name(id_of_string"y")) mkImplicit a
let lambda_implicit_lift n a = iterate lambda_implicit n (lift n a)
-let mkLambda_string s t c = mkLambda (Name (id_of_string s)) t c
-let mkProd_string s t c = mkProd (Name (id_of_string s)) t c
-
(* prod_it b [xn:Tn;..;x1:T1] = (x1:T1)..(xn:Tn)b *)
let prod_it = List.fold_left (fun c (n,t) -> mkProd n t c)
@@ -754,11 +771,11 @@ let rec isArity = function
([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
let decompose_prod =
let rec prodec_rec l = function
- | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) c
+ | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) c
| DOP2(Cast,c,_) -> prodec_rec l c
| c -> l,c
in
- prodec_rec []
+ prodec_rec []
(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
@@ -768,7 +785,7 @@ let decompose_lam =
| DOP2(Cast,c,_) -> lamdec_rec l c
| c -> l,c
in
- lamdec_rec []
+ lamdec_rec []
(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T
into the pair ([(xn,Tn);...;(x1,T1)],T) *)
@@ -1306,13 +1323,14 @@ let rec subst_meta bl c =
substitution is done the list may contain only negative occurrences
that will not be substituted. *)
-let subst_term_occ locs c t =
- let rec substcheck except k occ c t =
+let subst_term_occ_gen locs occ c t =
+ let except = List.for_all (fun n -> n<0) locs in
+ let rec substcheck k occ c t =
if except or List.exists (function u -> u>=occ) locs then
- substrec except k occ c t
+ substrec k occ c t
else
(occ,t)
- and substrec except k occ c t =
+ and substrec k occ c t =
if eq_constr t c then
if except then
if List.mem (-occ) locs then (occ+1,t) else (occ+1,Rel(k))
@@ -1327,44 +1345,60 @@ let subst_term_occ locs c t =
let (occ',cl') =
Array.fold_left
(fun (nocc',lfd) f ->
- let (nocc'',f') = substcheck except k nocc' c f in
+ let (nocc'',f') = substcheck k nocc' c f in
(nocc'',f'::lfd))
(occ,[]) cl
in
(occ',DOPN(i,Array.of_list (List.rev cl')))
| DOP2(i,t1,t2) ->
- let (nocc1,t1')=substrec except k occ c t1 in
- let (nocc2,t2')=substcheck except k nocc1 c t2 in
+ let (nocc1,t1')=substrec k occ c t1 in
+ let (nocc2,t2')=substcheck k nocc1 c t2 in
nocc2,DOP2(i,t1',t2')
| DOP1(i,t) ->
- let (nocc,t')= substrec except k occ c t in
+ let (nocc,t')= substrec k occ c t in
nocc,DOP1(i,t')
| DLAM(n,t) ->
- let (occ',t') = substcheck except (k+1) occ (lift 1 c) t in
+ let (occ',t') = substcheck (k+1) occ (lift 1 c) t in
(occ',DLAM(n,t'))
| DLAMV(n,cl) ->
let (occ',cl') =
Array.fold_left
(fun (nocc',lfd) f ->
let (nocc'',f') =
- substcheck except (k+1) nocc' (lift 1 c) f
+ substcheck (k+1) nocc' (lift 1 c) f
in (nocc'',f'::lfd))
(occ,[]) cl
in
(occ',DLAMV(n,Array.of_list (List.rev cl') ))
| _ -> occ,t
- in
- if locs = [] then
+ in
+ substcheck 1 occ c t
+
+let subst_term_occ locs c t =
+ if locs = [] then
subst_term c t
else if List.mem 0 locs then
t
else
- let except = List.for_all (fun n -> n<0) locs in
- let (nbocc,t') = substcheck except 1 1 c t in
+ let (nbocc,t') = subst_term_occ_gen locs 1 c t in
if List.exists (fun o -> o >= nbocc or o <= -nbocc) locs then
- failwith "subst_term_occ: too few occurences";
+ errorlabstrm "subst_term_occ" [< 'sTR "Too few occurences" >];
t'
+let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
+ match bodyopt with
+ | None -> (id,None,subst_term_occ locs c typ)
+ | Some body ->
+ if locs = [] then
+ (id,Some (subst_term c body),typed_app (subst_term c) typ)
+ else if List.mem 0 locs then
+ d
+ else
+ let (nbocc,body') = subst_term_occ_gen locs 1 c body in
+ let (nbocc',t') = typed_app (subst_term_occ_gen locs nbocc c) typ in
+ if List.exists (fun o -> o >= nbocc' or o <= -nbocc') locs then
+ errorlabstrm "subst_term_occ_decl" [< 'sTR "Too few occurences" >];
+ (id,Some body',t')
(***************************)
(* occurs check functions *)
diff --git a/kernel/term.mli b/kernel/term.mli
index 72ba6f511..9019fa091 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -59,10 +59,9 @@ type constr = sorts oper term
type flat_arity = (name * constr) list * sorts
-type 'a judge = { body : constr; typ : 'a }
+(*type 'a judge = { body : constr; typ : 'a }*)
type typed_type
-type typed_term = typed_type judge
val make_typed : constr -> sorts -> typed_type
val make_typed_lazy : constr -> (constr -> sorts) -> typed_type
@@ -78,6 +77,9 @@ val incast_type : typed_type -> constr
val outcast_type : constr -> typed_type
+type var_declaration = identifier * constr option * typed_type
+type rel_declaration = name * constr option * typed_type
+
(**********************************************************************)
type binder_kind = BProd | BLambda
@@ -96,7 +98,10 @@ type 'ctxt reference =
manipulation of terms. Some of these functions may be overlapped with
previous ones. *)
-(* Concrete type for making pattern-matching. *)
+(* Concrete type for making pattern-matching. *)
+
+(* [constr array] is an instance matching definitional var_context in
+ the same order (i.e. last argument first) *)
type existential = int * constr array
type constant = section_path * constr array
type constructor = constructor_path * constr array
@@ -169,18 +174,30 @@ val implicit_sort : sorts
type $t_2$ (that means t2 is declared as the type of t1). *)
val mkCast : constr -> constr -> constr
-(* Constructs the product $(x:t_1)t_2$. $x$ may be anonymous. *)
+(* Constructs the product $(x:t_1)t_2$ *)
val mkProd : name -> constr -> constr -> constr
-
-(* [mkProd_string s t c] constructs the product $(s:t)c$ *)
+val mkNamedProd : identifier -> constr -> constr -> constr
val mkProd_string : string -> constr -> constr -> constr
+(* Constructs the product $(x:t_1)t_2$ *)
+val mkLetIn : name -> constr -> constr -> constr -> constr
+val mkNamedLetIn : identifier -> constr -> constr -> constr -> constr
+
+(* Constructs either [(x:t)c] or [[x=b:t]c] *)
+val mkProd_or_LetIn : rel_declaration -> constr -> constr
+val mkNamedProd_or_LetIn : var_declaration -> constr -> constr
+
+(* Constructs either [[x:t]c] or [[x=b:t]c] *)
+val mkLambda_or_LetIn : rel_declaration -> constr -> constr
+val mkNamedLambda_or_LetIn : var_declaration -> constr -> constr
+
+(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
+val mkProd_wo_LetIn : rel_declaration -> constr -> constr
+val mkNamedProd_wo_LetIn : var_declaration -> constr -> constr
+
(* non-dependant product $t_1 \rightarrow t_2$ *)
val mkArrow : constr -> constr -> constr
-(* named product *)
-val mkNamedProd : identifier -> constr -> constr -> constr
-
(* Constructs the abstraction $[x:t_1]t_2$ *)
val mkLambda : name -> constr -> constr -> constr
val mkNamedLambda : identifier -> constr -> constr -> constr
@@ -198,7 +215,7 @@ val mkAppList : constr -> constr list -> constr
val mkConst : constant -> constr
(* Constructs an existential variable *)
-val mkEvar : int -> constr array -> constr
+val mkEvar : existential -> constr
(* Constructs an abstract object *)
val mkAbst : section_path -> constr array -> constr
@@ -360,13 +377,6 @@ val destFix : constr -> fixpoint
val destCoFix : constr -> cofixpoint
-(* Provisoire, le temps de maitriser les cast *)
-val destUntypedFix :
- constr -> int array * int * constr array * Names.name list * constr array
-val destUntypedCoFix :
- constr -> int * constr array * Names.name list * constr array
-
-
(*s Other term constructors. *)
val abs_implicit : constr -> constr
@@ -410,7 +420,8 @@ val prod_applist : constr -> constr list -> constr
(*s Other term destructors. *)
(* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ into the pair
- $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product. *)
+ $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product.
+ It includes also local definitions *)
val decompose_prod : constr -> (name*constr) list * constr
(* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ into the pair
@@ -420,11 +431,11 @@ val decompose_lam : constr -> (name*constr) list * constr
(* Given a positive integer n, transforms a product term
$(x_1:T_1)..(x_n:T_n)T$
into the pair $([(xn,Tn);...;(x1,T1)],T)$. *)
-val decompose_prod_n : int -> constr -> (name*constr) list * constr
+val decompose_prod_n : int -> constr -> (name * constr) list * constr
(* Given a positive integer $n$, transforms a lambda term
$[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *)
-val decompose_lam_n : int -> constr -> (name*constr) list * constr
+val decompose_lam_n : int -> constr -> (name * constr) list * constr
(* [nb_lam] $[x_1:T_1]...[x_n:T_n]c$ where $c$ is not an abstraction
gives $n$ (casts are ignored) *)
@@ -565,11 +576,16 @@ val rename_bound_var : identifier list -> constr -> constr
val eta_reduce_head : constr -> constr
val eq_constr : constr -> constr -> bool
val eta_eq_constr : constr -> constr -> bool
-val subst_term : constr -> constr -> constr
-val subst_term_eta_eq : constr -> constr -> constr
+
+(*s The following functions substitutes [what] by [Rel 1] in [where] *)
+val subst_term : what:constr -> where:constr -> constr
+val subst_term_eta_eq : what:constr -> where:constr -> constr
+val subst_term_occ : occs:int list -> what:constr -> where:constr -> constr
+val subst_term_occ_decl : occs:int list -> what:constr ->
+ where:var_declaration -> var_declaration
+
val replace_consts :
(section_path * (identifier list * constr) option) list -> constr -> constr
-val subst_term_occ : int list -> constr -> constr -> constr
(* [subst_meta bl c] substitutes the metavar $i$ by $c_i$ in [c]
for each binding $(i,c_i)$ in [bl],
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index d2891180a..14409c235 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -40,61 +40,59 @@ type type_error =
| WrongPredicateArity of constr * int * int
| NeedsInversion of constr * constr
-exception TypeError of path_kind * context * type_error
+exception TypeError of path_kind * env * type_error
-let context_ise sigma env =
- map_var_env (typed_app (Reduction.nf_ise1 sigma))
- (map_rel_env (typed_app (Reduction.nf_ise1 sigma))
- (context env))
+let env_ise sigma env =
+ map_context (Reduction.nf_ise1 sigma) env
let error_unbound_rel k env sigma n =
- raise (TypeError (k, context_ise sigma env, UnboundRel n))
+ raise (TypeError (k, env_ise sigma env, UnboundRel n))
let error_not_type k env c =
- raise (TypeError (k, context env, NotAType c))
+ raise (TypeError (k, env, NotAType c))
let error_assumption k env c =
- raise (TypeError (k, context env, BadAssumption c))
+ raise (TypeError (k, env, BadAssumption c))
let error_reference_variables k env id =
- raise (TypeError (k, context env, ReferenceVariables id))
+ raise (TypeError (k, env, ReferenceVariables id))
let error_elim_arity k env ind aritylst c p pt okinds =
- raise (TypeError (k, context env, ElimArity (ind,aritylst,c,p,pt,okinds)))
+ raise (TypeError (k, env, ElimArity (ind,aritylst,c,p,pt,okinds)))
let error_case_not_inductive k env c ct =
- raise (TypeError (k, context env, CaseNotInductive (c,ct)))
+ raise (TypeError (k, env, CaseNotInductive (c,ct)))
let error_number_branches k env c ct expn =
- raise (TypeError (k, context env, NumberBranches (c,ct,expn)))
+ raise (TypeError (k, env, NumberBranches (c,ct,expn)))
let error_ill_formed_branch k env c i actty expty =
- raise (TypeError (k, context env, IllFormedBranch (c,i,actty,expty)))
+ raise (TypeError (k, env, IllFormedBranch (c,i,actty,expty)))
let error_generalization k env sigma nvar c =
- raise (TypeError (k, context_ise sigma env, Generalization (nvar,c)))
+ raise (TypeError (k, env_ise sigma env, Generalization (nvar,c)))
let error_actual_type k env c actty expty =
- raise (TypeError (k, context env, ActualType (c,actty,expty)))
+ raise (TypeError (k, env, ActualType (c,actty,expty)))
let error_cant_apply_not_functional k env rator randl =
- raise (TypeError (k, context env, CantApplyNonFunctional (rator,randl)))
+ raise (TypeError (k, env, CantApplyNonFunctional (rator,randl)))
let error_cant_apply_bad_type k env sigma t rator randl =
- raise(TypeError (k, context_ise sigma env, CantApplyBadType (t,rator,randl)))
+ raise(TypeError (k, env_ise sigma env, CantApplyBadType (t,rator,randl)))
let error_ill_formed_rec_body k env str lna i vdefs =
- raise (TypeError (k, context env, IllFormedRecBody (str,lna,i,vdefs)))
+ raise (TypeError (k, env, IllFormedRecBody (str,lna,i,vdefs)))
let error_ill_typed_rec_body k env i lna vdefj vargs =
- raise (TypeError (k, context env, IllTypedRecBody (i,lna,vdefj,vargs)))
+ raise (TypeError (k, env, IllTypedRecBody (i,lna,vdefj,vargs)))
let error_not_inductive k env c =
- raise (TypeError (k, context env, NotInductive c))
+ raise (TypeError (k, env, NotInductive c))
let error_ml_case k env mes c ct br brt =
- raise (TypeError (k, context env, MLCase (mes,c,ct,br,brt)))
+ raise (TypeError (k, env, MLCase (mes,c,ct,br,brt)))
let error_not_product env c =
- raise (TypeError (CCI, context env, NotProduct c))
+ raise (TypeError (CCI, env, NotProduct c))
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 38d6d8b6e..284f244f1 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -42,7 +42,7 @@ type type_error =
| WrongPredicateArity of constr * int * int
| NeedsInversion of constr * constr
-exception TypeError of path_kind * context * type_error
+exception TypeError of path_kind * env * type_error
val error_unbound_rel : path_kind -> env -> 'a Evd.evar_map -> int -> 'b
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a22e5715b..4077d852f 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -37,12 +37,11 @@ let type_judgment env sigma j =
let assumption_of_type_judgment j = make_typed j.utj_val j.utj_type
-
(* Type of a de Bruijn index. *)
let relative env sigma n =
try
- let (_,typ) = lookup_rel n env in
+ let (_,typ) = lookup_rel_type n env in
{ uj_val = Rel n;
uj_type = typed_app (lift n) typ }
with Not_found ->
@@ -51,13 +50,13 @@ let relative env sigma n =
(* Management of context of variables. *)
(* Checks if a context of variable is included in another one. *)
-
+(*
let rec hyps_inclusion env sigma sign1 sign2 =
- if isnull_sign sign1 then true
+ if sign1 = empty_var_context then true
else
let (id1,ty1) = hd_sign sign1 in
let rec search sign2 =
- if isnull_sign sign2 then false
+ if sign2 = empty_var_context then false
else
let (id2,ty2) = hd_sign sign2 in
if id1 = id2 then
@@ -68,15 +67,16 @@ let rec hyps_inclusion env sigma sign1 sign2 =
search (tl_sign sign2)
in
search sign2
+*)
(* Checks if the given context of variables [hyps] is included in the
current context of [env]. *)
-
+(*
let check_hyps id env sigma hyps =
let hyps' = var_context env in
if not (hyps_inclusion env sigma hyps hyps') then
error_reference_variables CCI env id
-
+*)
(* Instantiation of terms on real arguments. *)
let type_of_constant = Instantiate.constant_type
@@ -263,8 +263,11 @@ let sort_of_product_without_univ domsort rangsort =
| Prop _ -> rangsort
| Type u1 -> Type dummy_univ)
-let typed_product_without_universes name var c =
- typed_combine (mkProd name) sort_of_product_without_univ var c
+let generalize_without_universes (_,_,var as d) c =
+ typed_combine
+ (fun _ c -> mkNamedProd_or_LetIn d c)
+ sort_of_product_without_univ
+ var c
let typed_product env name var c =
(* Gros hack ! *)
@@ -443,12 +446,11 @@ let is_subterm_specif env sigma lcx mind_recvec =
stl.(0)
| (DOPN(Fix(_),la) as mc,l) ->
- let (recindxs,i,typarray,funnames,bodies) = destUntypedFix mc in
+ let ((recindxs,i),(typarray,funnames,bodies)) = destFix mc in
let nbfix = List.length funnames in
let decrArg = recindxs.(i) in
let theBody = bodies.(i) in
- let (gamma,strippedBody) = decompose_lam_n (decrArg+1) theBody in
- let absTypes = List.map snd gamma in
+ let (_,strippedBody) = decompose_lam_n (decrArg+1) theBody in
let nbOfAbst = nbfix+decrArg+1 in
let newlst =
if List.length l < (decrArg+1) then
@@ -563,7 +565,7 @@ let rec check_subterm_rec_meta env sigma vectn k def =
| (DOPN(Fix(_),la) as mc,l) ->
(List.for_all (check_rec_call n lst) l) &&
- let (recindxs,i,typarray,funnames,bodies) = destUntypedFix mc in
+ let ((recindxs,i),(typarray,funnames,bodies)) = destFix mc in
let nbfix = List.length funnames in
let decrArg = recindxs.(i) in
if (List.length l < (decrArg+1)) then
@@ -831,18 +833,4 @@ let control_only_guard env sigma =
in
control_rec
-(* [keep_hyps sign ids] keeps the part of the signature [sign] which
- contains the variables of the set [ids], and recursively the variables
- contained in the types of the needed variables. *)
-
-let keep_hyps sign needed =
- rev_sign
- (fst (it_sign
- (fun ((hyps,globs) as sofar) id a ->
- if Idset.mem id globs then
- (add_sign (id,a) hyps,
- Idset.union (global_vars_set (body_of_type a)) globs)
- else
- sofar)
- (nil_sign,needed) sign))
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 6d1faa0ff..a07206fb0 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -51,8 +51,7 @@ val judge_of_prop_contents : contents -> unsafe_judgment
val judge_of_type : universe -> unsafe_judgment * constraints
-val typed_product_without_universes :
- name -> typed_type -> typed_type -> typed_type
+val generalize_without_universes : var_declaration -> typed_type -> typed_type
val abs_rel :
env -> 'a evar_map -> name -> typed_type -> unsafe_judgment
@@ -85,6 +84,7 @@ open Inductive
val find_case_dep_nparams :
env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool
+(*
val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool
+*)
-val keep_hyps : var_context -> Idset.t -> var_context
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-09 08:18:51 +0000