aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/indtypes.ml140
-rw-r--r--kernel/indtypes.mli39
-rw-r--r--kernel/inductive.ml85
-rw-r--r--kernel/inductive.mli36
-rw-r--r--kernel/instantiate.ml42
-rw-r--r--kernel/instantiate.mli7
-rw-r--r--kernel/reduction.ml4
-rw-r--r--kernel/safe_typing.ml149
-rw-r--r--kernel/safe_typing.mli9
-rw-r--r--kernel/term.ml29
-rw-r--r--kernel/term.mli2
-rw-r--r--kernel/typeops.ml30
-rw-r--r--kernel/typeops.mli1
-rw-r--r--parsing/pretty.ml31
-rw-r--r--parsing/printer.ml8
-rw-r--r--pretyping/coercion.ml3
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/pretyping.ml15
-rw-r--r--proofs/logic.ml10
-rw-r--r--proofs/proof_trees.ml3
-rw-r--r--proofs/tacmach.ml2
-rw-r--r--tactics/equality.ml2
-rw-r--r--toplevel/command.ml6
-rw-r--r--toplevel/discharge.ml26
-rw-r--r--toplevel/errors.ml2
-rw-r--r--toplevel/himsg.ml3
-rw-r--r--toplevel/himsg.mli2
-rw-r--r--toplevel/record.ml4
28 files changed, 369 insertions, 323 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ab7263503..e48e9dc97 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -16,6 +16,94 @@ open Typeops
is given, since inductive types are typed in an environment without
existentials. *)
+(* [check_constructors_names id s cl] checks that all the constructors names
+ appearing in [l] are not present in the set [s], and returns the new set
+ of names. The name [id] is the name of the current inductive type, used
+ when reporting the error. *)
+
+(***********************************************************************)
+(* Various well-formedness check for inductive declarations *)
+
+type inductive_error =
+ | 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
+ | SameNamesTypes of identifier
+ | SameNamesConstructors of identifier * identifier
+ | NotAnArity of identifier
+ | BadEntry
+
+exception InductiveError of inductive_error
+
+let check_constructors_names id =
+ let rec check idset = function
+ | [] -> idset
+ | c::cl ->
+ if Idset.mem c idset then
+ raise (InductiveError (SameNamesConstructors (id,c)))
+ else
+ check (Idset.add c idset) cl
+ in
+ check
+
+(* [mind_check_names mie] checks the names of an inductive types declaration,
+ and raises the corresponding exceptions when two types or two constructors
+ have the same name. *)
+
+let mind_check_names mie =
+ let rec check indset cstset = function
+ | [] -> ()
+ | (id,_,cl,_)::inds ->
+ if Idset.mem id indset then
+ raise (InductiveError (SameNamesTypes id))
+ else
+ let cstset' = check_constructors_names id cstset cl in
+ check (Idset.add id indset) cstset' inds
+ in
+ check Idset.empty Idset.empty mie.mind_entry_inds
+
+(* [mind_extract_params mie] extracts the params from an inductive types
+ declaration, and checks that they are all present (and all the same)
+ 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 extract nparams c =
+ try 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 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;
+ params
+
+let mind_check_lc params mie =
+ let ntypes = List.length mie.mind_entry_inds in
+ let nparams = List.length params in
+ let check_lc (_,_,_,lc) =
+ let (lna,c) = decomp_all_DLAMV_name lc in
+ Array.iter (check_params nparams params) c;
+ if not (List.length lna = ntypes) then raise (InductiveError BadEntry)
+ in
+ List.iter check_lc mie.mind_entry_inds
+
let mind_check_arities env mie =
let check_arity id c =
if not (is_arity env Evd.empty c) then
@@ -23,6 +111,8 @@ let mind_check_arities env mie =
in
List.iter (fun (id,ar,_,_) -> check_arity id ar) mie.mind_entry_inds
+(***********************************************************************)
+
let allowed_sorts issmall isunit = function
| Type _ ->
[prop;spec;types]
@@ -34,10 +124,10 @@ let allowed_sorts issmall isunit = function
let is_small_type t = is_small t.typ
type ill_formed_ind =
- | NonPos of int
- | NotEnoughArgs of int
- | NotConstructor
- | NonPar of int * int
+ | LocalNonPos of int
+ | LocalNotEnoughArgs of int
+ | LocalNotConstructor
+ | LocalNonPar of int * int
exception IllFormedInd of ill_formed_ind
@@ -45,33 +135,33 @@ let explain_ind_err ntyp lna nbpar c err =
let (lpar,c') = mind_extract_params nbpar c in
let env = (List.map fst lpar)@lna in
match err with
- | NonPos kt ->
- raise (InductiveError (Inductive.NonPos (env,c',Rel (kt+nbpar))))
- | NotEnoughArgs kt ->
+ | LocalNonPos kt ->
+ raise (InductiveError (NonPos (env,c',Rel (kt+nbpar))))
+ | LocalNotEnoughArgs kt ->
raise (InductiveError
- (Inductive.NotEnoughArgs (env,c',Rel (kt+nbpar))))
- | NotConstructor ->
+ (NotEnoughArgs (env,c',Rel (kt+nbpar))))
+ | LocalNotConstructor ->
raise (InductiveError
- (Inductive.NotConstructor (env,c',Rel (ntyp+nbpar))))
- | NonPar (n,l) ->
+ (NotConstructor (env,c',Rel (ntyp+nbpar))))
+ | LocalNonPar (n,l) ->
raise (InductiveError
- (Inductive.NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar))))
+ (NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar))))
let failwith_non_pos_vect n ntypes v =
for i = 0 to Array.length v - 1 do
for k = n to n + ntypes - 1 do
- if not (noccurn k v.(i)) then raise (IllFormedInd (NonPos (k-n+1)))
+ if not (noccurn k v.(i)) then raise (IllFormedInd (LocalNonPos (k-n+1)))
done
done;
anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur in v"
let check_correct_par env nparams ntypes n l largs =
if Array.length largs < nparams then
- raise (IllFormedInd (NotEnoughArgs l));
+ raise (IllFormedInd (LocalNotEnoughArgs l));
let (lpar,largs') = array_chop nparams largs in
for k = 0 to nparams - 1 do
if not ((Rel (n-k-1))= whd_betadeltaiotaeta env Evd.empty lpar.(k)) then
- raise (IllFormedInd (NonPar (k+1,l)))
+ raise (IllFormedInd (LocalNonPar (k+1,l)))
done;
if not (array_for_all (noccur_bet n ntypes) largs') then
failwith_non_pos_vect n ntypes largs'
@@ -95,7 +185,7 @@ let listrec_mconstr env ntypes nparams i indlc =
let rec check_pos n c =
match whd_betadeltaiota env Evd.empty c with
| DOP2(Prod,b,DLAM(na,d)) ->
- if not (noccur_bet n ntypes b) then raise (IllFormedInd (NonPos n));
+ if not (noccur_bet n ntypes b) then raise (IllFormedInd (LocalNonPos n));
check_pos (n+1) d
| x ->
let hd,largs = destApplication (ensure_appl x) in
@@ -109,23 +199,23 @@ let listrec_mconstr env ntypes nparams i indlc =
then Param(n-1-k)
else Norec
else
- raise (IllFormedInd (NonPos n))
+ raise (IllFormedInd (LocalNonPos n))
| DOPN(MutInd ind_sp,a) ->
if (noccur_bet n ntypes x) then Norec
else Imbr(ind_sp,imbr_positive n (ind_sp,a) largs)
| err ->
if noccur_bet n ntypes x then Norec
- else raise (IllFormedInd (NonPos n))
+ else raise (IllFormedInd (LocalNonPos n))
and imbr_positive n mi largs =
let mispeci = lookup_mind_specif mi env in
let auxnpar = mis_nparams mispeci in
let (lpar,auxlargs) = array_chop auxnpar largs in
if not (array_for_all (noccur_bet n ntypes) auxlargs) then
- raise (IllFormedInd (NonPos n));
+ raise (IllFormedInd (LocalNonPos n));
let auxlc = mis_lc mispeci
and auxntyp = mis_ntypes mispeci in
- if auxntyp <> 1 then raise (IllFormedInd (NonPos n));
+ if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
let lrecargs = array_map_to_list (check_weak_pos n) lpar in
(* The abstract imbricated inductive type with parameters substituted *)
let auxlcvect = abstract_mind_lc env auxntyp auxnpar auxlc in
@@ -165,7 +255,7 @@ let listrec_mconstr env ntypes nparams i indlc =
| DOP2(Lambda,b,DLAM(na,d)) ->
if noccur_bet n ntypes b
then check_weak_pos (n+1) d
- else raise (IllFormedInd (NonPos n))
+ else raise (IllFormedInd (LocalNonPos n))
(******************)
| x -> check_pos n x
@@ -185,10 +275,10 @@ let listrec_mconstr env ntypes nparams i indlc =
match hd with
| Rel k when k = n+ntypes-i ->
check_correct_par env nparams ntypes n (k-n+1) largs
- | _ -> raise (IllFormedInd NotConstructor)
+ | _ -> raise (IllFormedInd LocalNotConstructor)
else
if not (array_for_all (noccur_bet n ntypes) largs)
- then raise (IllFormedInd (NonPos n));
+ then raise (IllFormedInd (LocalNonPos n));
List.rev lrec
in check_constr_rec []
in
@@ -215,7 +305,7 @@ let cci_inductive env env_ar kind nparams finite inds cst =
let one_packet i (id,ar,cnames,issmall,isunit,lc) =
let recargs = listrec_mconstr env_ar ntypes nparams i lc in
let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in
- let (ar_sign,ar_sort) = splay_arity env Evd.empty ar.body in
+ let (ar_sign,ar_sort) = splay_arity env Evd.empty (body_of_type ar) in
let kelim = allowed_sorts issmall isunit ar_sort in
{ mind_consnames = Array.of_list cnames;
mind_typename = id;
@@ -229,7 +319,7 @@ let cci_inductive env env_ar kind nparams finite inds cst =
let ids =
List.fold_left
(fun acc (_,ar,_,_,_,lc) ->
- Idset.union (global_vars_set ar.body)
+ Idset.union (global_vars_set (body_of_type ar))
(Idset.union (global_vars_set lc) acc))
Idset.empty inds
in
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 1e675b2c0..e955f6009 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -9,11 +9,50 @@ open Inductive
open Environ
(*i*)
+
+(*s The different kinds of errors that may result of a malformed inductive
+ definition. *)
+
+type inductive_error =
+ | 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
+ | SameNamesTypes of identifier
+ | SameNamesConstructors of identifier * identifier
+ | NotAnArity of identifier
+ | BadEntry
+
+exception InductiveError of inductive_error
+
+(*s The following functions are utility functions to check and to
+ decompose a declaration. *)
+
+(* [mind_check_names] checks the names of an inductive types declaration
+ i.e. that all the types and constructors names are distinct.
+ It raises an exception [InductiveError _] if it is not the case. *)
+
+val mind_check_names : mutual_inductive_entry -> unit
+
+(* [mind_extract_and_check_params] extracts the parameters of an inductive
+ types declaration. It raises an exception [InductiveError _] if there is
+ not enough abstractions in any of the terms of the field
+ [mind_entry_inds]. *)
+
+val mind_extract_and_check_params :
+ mutual_inductive_entry -> (name * constr) list
+
+val mind_extract_params : int -> constr -> (name * constr) list * constr
+
+val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
+
(* [mind_check_arities] checks that the types declared for all the
inductive types are some arities. *)
val mind_check_arities : env -> mutual_inductive_entry -> unit
+(* [cci_inductive] checks positivity and builds an inductive body *)
+
val cci_inductive :
env -> env -> path_kind -> int -> bool ->
(identifier * typed_type * identifier list * bool * bool * constr) list ->
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index fda1190d1..9a59a889b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -106,91 +106,6 @@ type mutual_inductive_entry = {
mind_entry_finite : bool;
mind_entry_inds : (identifier * constr * identifier list * constr) list }
-type inductive_error =
- | 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
- | SameNamesTypes of identifier
- | SameNamesConstructors of identifier * identifier
- | NotAnArity of identifier
- | BadEntry
-
-exception InductiveError of inductive_error
-
-(* [check_constructors_names id s cl] checks that all the constructors names
- appearing in [l] are not present in the set [s], and returns the new set
- of names. The name [id] is the name of the current inductive type, used
- when reporting the error. *)
-
-let check_constructors_names id =
- let rec check idset = function
- | [] -> idset
- | c::cl ->
- if Idset.mem c idset then
- raise (InductiveError (SameNamesConstructors (id,c)))
- else
- check (Idset.add c idset) cl
- in
- check
-
-(* [mind_check_names mie] checks the names of an inductive types declaration,
- and raises the corresponding exceptions when two types or two constructors
- have the same name. *)
-
-let mind_check_names mie =
- let rec check indset cstset = function
- | [] -> ()
- | (id,_,cl,_)::inds ->
- if Idset.mem id indset then
- raise (InductiveError (SameNamesTypes id))
- else
- let cstset' = check_constructors_names id cstset cl in
- check (Idset.add id indset) cstset' inds
- in
- check Idset.empty Idset.empty mie.mind_entry_inds
-
-(* [mind_extract_params mie] extracts the params from an inductive types
- declaration, and checks that they are all present (and all the same)
- 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 extract nparams c =
- try 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 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;
- params
-
-let mind_check_lc params mie =
- let ntypes = List.length mie.mind_entry_inds in
- let nparams = List.length params in
- let check_lc (_,_,_,lc) =
- let (lna,c) = decomp_all_DLAMV_name lc in
- Array.iter (check_params nparams params) c;
- if not (List.length lna = ntypes) then raise (InductiveError BadEntry)
- in
- List.iter check_lc mie.mind_entry_inds
-
let inductive_path_of_constructor_path (ind_sp,i) = ind_sp
let ith_constructor_path_of_inductive_path ind_sp i = (ind_sp,i)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index c9857daaf..c5520cf49 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -112,42 +112,6 @@ type mutual_inductive_entry = {
mind_entry_finite : bool;
mind_entry_inds : (identifier * constr * identifier list * constr) list }
-(*s The different kinds of errors that may result of a malformed inductive
- definition. *)
-
-type inductive_error =
- | 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
- | SameNamesTypes of identifier
- | SameNamesConstructors of identifier * identifier
- | NotAnArity of identifier
- | BadEntry
-
-exception InductiveError of inductive_error
-
-(*s The following functions are utility functions to check and to
- decompose a declaration. *)
-
-(* [mind_check_names] checks the names of an inductive types declaration
- i.e. that all the types and constructors names are distinct.
- It raises an exception [InductiveError _] if it is not the case. *)
-
-val mind_check_names : mutual_inductive_entry -> unit
-
-(* [mind_extract_and_check_params] extracts the parameters of an inductive
- types declaration. It raises an exception [InductiveError _] if there is
- not enough abstractions in any of the terms of the field
- [mind_entry_inds]. *)
-
-val mind_extract_and_check_params :
- mutual_inductive_entry -> (name * constr) list
-
-val mind_extract_params : int -> constr -> (name * constr) list * constr
-
-val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
-
val inductive_of_constructor : constructor -> inductive
val ith_constructor_of_inductive : inductive -> int -> constructor
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index bf3135790..5e48b8e0c 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -26,33 +26,34 @@ let instantiate_constr ids c args =
replace_vars (List.combine ids (List.map make_substituend args)) c
let instantiate_type ids tty args =
- { body = instantiate_constr ids tty.body args;
- typ = tty.typ }
+ typed_app (fun c -> instantiate_constr ids c args) tty
(* Constants. *)
(* constant_type gives the type of a constant *)
-let constant_type env k =
- let (sp,args) = destConst k in
+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)
-let constant_value env k =
- let (sp,args) = destConst k in
- let cb = lookup_constant sp env in
- if not cb.const_opaque & defined_constant env k then
- 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)
- | None ->
- anomalylabstrm "termenv__constant_value"
- [< 'sTR "a defined constant with no body." >]
- else
- failwith "opaque"
+type const_evaluation_error = NotDefinedConst | OpaqueConst
+
+exception NotEvaluableConst of const_evaluation_error
+let constant_value env cst =
+ let (sp,args) = destConst cst in
+ let cb = lookup_constant sp env in
+ if cb.const_opaque then raise (NotEvaluableConst OpaqueConst) else
+ if not (is_defined cb) then raise (NotEvaluableConst NotDefinedConst) else
+ 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)
+ | None ->
+ anomalylabstrm "termenv__constant_value"
+ [< 'sTR "a defined constant with no body." >]
let mis_lc mis =
instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc
@@ -115,7 +116,6 @@ let mis_typed_arity mis =
and largs = Array.to_list mis.mis_args in
instantiate_type idhyps mis.mis_mip.mind_arity largs
-let mis_arity mispec =
- let { body = b; typ = t } = mis_typed_arity mispec in
- DOP2 (Cast, b, DOP0 (Sort t))
+let mis_arity mispec = incast_type (mis_typed_arity mispec)
+
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 9f5b02e92..8d267021f 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -16,8 +16,13 @@ val instantiate_constr :
val instantiate_type :
identifier list -> typed_type -> constr list -> typed_type
+type const_evaluation_error = NotDefinedConst | OpaqueConst
+exception NotEvaluableConst of const_evaluation_error
+
+(* [constant_value env c] raises [NotEvaluableConst OpaqueConst] if
+ [c] is opaque and [NotEvaluableConst NotDefinedConst] if undefined *)
val constant_value : env -> constr -> constr
-val constant_type : env -> constr -> typed_type
+val constant_type : env -> 'a evar_map -> constant -> typed_type
val existential_value : 'a evar_map -> constr -> constr
val existential_type : 'a evar_map -> constr -> constr
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 6f41a3c64..caf667dae 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1227,10 +1227,10 @@ let is_type_arity env sigma =
srec
let is_info_type env sigma t =
- let s = t.typ in
+ let s = level_of_type t in
(s = Prop Pos) ||
(s <> Prop Null &&
- try info_arity env sigma t.body with IsType -> true)
+ try info_arity env sigma (body_of_type t) with IsType -> true)
let is_info_cast_type env sigma c =
match c with
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0e855e443..0f0907786 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -110,7 +110,7 @@ let rec execute mf env cstr =
let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in
(j, cst)
- | IsProd (name,c1,c2) ->
+ | IsProd (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
@@ -156,8 +156,8 @@ and execute_list mf env = function
(* The typed type of a judgment. *)
let execute_type mf env constr =
- let (j,_) = execute mf env constr in
- assumption_of_judgment env Evd.empty j
+ let (j,cst) = execute mf env constr in
+ (assumption_of_judgment env Evd.empty j, cst)
(* Exported machines. First safe machines, with no general fixpoint
@@ -198,15 +198,16 @@ let unsafe_machine_type env constr =
let type_of env c =
let (j,_) = safe_machine env c in nf_betaiota env Evd.empty j.uj_type
+(* obsolètes
let type_of_type env c =
- let tt = safe_machine_type env c in DOP0 (Sort tt.typ)
+ let tt = safe_machine_type env c in DOP0 (Sort (level_of_type tt.typ)
let unsafe_type_of env c =
let (j,_) = unsafe_machine env c in nf_betaiota env Evd.empty j.uj_type
let unsafe_type_of_type env c =
let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ)
-
+*)
(* Typing of several terms. *)
let safe_machine_l env cl =
@@ -281,7 +282,7 @@ let add_constant_with_value sp body typ env =
error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
in
let ids =
- Idset.union (global_vars_set body) (global_vars_set ty.body)
+ Idset.union (global_vars_set body) (global_vars_set (body_of_type ty))
in
let cb = {
const_kind = kind_of_path sp;
@@ -331,76 +332,84 @@ let add_parameter sp t env =
(* Insertion of inductive types. *)
-(* [for_all_prods p env c] checks a boolean condition [p] on all types
- appearing in products in front of [c]. The boolean condition [p] is a
- function taking a value of type [typed_type] as argument. *)
-
-let rec for_all_prods p env c =
- match whd_betadeltaiota env Evd.empty c with
- | DOP2(Prod, DOP2(Cast,t,DOP0 (Sort s)), DLAM(name,c)) ->
- (p (make_typed t s)) &&
- (let ty = { body = t; typ = s } in
- let env' = Environ.push_rel (name,ty) env in
- for_all_prods p env' c)
- | DOP2(Prod, b, DLAM(name,c)) ->
- let (jb,cst) = unsafe_machine env b in
- let var = assumption_of_judgment env Evd.empty jb in
- (p var) &&
- (let env' = Environ.push_rel (name,var) (add_constraints cst env) in
- for_all_prods p env' c)
- | _ -> true
-
-let is_small_type e c = for_all_prods (fun t -> is_small t.typ) e c
-
-let enforce_type_constructor env univ j cst =
- match whd_betadeltaiota env Evd.empty j.uj_type with
- | DOP0 (Sort (Type uc)) ->
- Constraint.add (univ,Geq,uc) cst
- | _ -> error "Type of Constructor not well-formed"
-
-let type_one_constructor env_ar nparams ar c =
- let (params,dc) = mind_extract_params nparams c in
- let env_par = push_rels params env_ar in
- let (jc,cst) = safe_machine env_par dc in
- let cst' = match sort_of_arity env_ar ar with
- | Type u -> enforce_type_constructor env_par u jc cst
- | Prop _ -> cst
- in
- let (j,cst'') = safe_machine env_ar c in
- let issmall = is_small_type env_par dc in
- ((issmall,j), Constraint.union cst' cst'')
-
-let logic_constr env c =
- for_all_prods (fun t -> not (is_info_type env Evd.empty t)) env c
-
-let logic_arity env c =
- for_all_prods
- (fun t ->
- (not (is_info_type env Evd.empty t)) or (is_small_type env t.body))
- env c
-
-let is_unit env_par nparams ar spec =
- match decomp_all_DLAMV_name spec with
- | (_,[|c|]) ->
- (let (_,a) = mind_extract_params nparams ar in
- logic_arity env_par ar) &&
- (let (_,c') = mind_extract_params nparams c in
- logic_constr env_par c')
- | _ -> false
+(* Only the case where at least s1 or s2 is a [Type] is taken into account *)
+let max_universe (s1,cst1) (s2,cst2) g =
+ match s1,s2 with
+ | Type u1, Type u2 ->
+ let (u12,cst) = sup u1 u2 g in
+ Type u12, Constraint.union cst (Constraint.union cst1 cst2)
+ | Type u1, _ -> s1, cst1
+ | _, _ -> s2, cst2
+
+(* This (re)computes informations relevant to extraction and the sort of
+ an arity or type constructor *)
+
+let rec infos_and_sort env t =
+ match kind_of_term t with
+ | IsProd (name,c1,c2) ->
+ let (var,cst1) = safe_machine_type env c1 in
+ let env1 = Environ.push_rel (name,var) env in
+ let (infos,smax,cst) = infos_and_sort env1 c2 in
+ let s1 = level_of_type var in
+ let smax',cst' = max_universe (s1,cst1) (smax,cst) (universes env) in
+ let logic = not (is_info_type env Evd.empty var) in
+ let small = is_small s1 in
+ ((logic,small) :: infos, smax', cst')
+ | IsCast (c,t) -> 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 *)
+
+let is_small infos = List.for_all (fun (logic,small) -> small) infos
+let is_logic_constr infos = List.for_all (fun (logic,small) -> logic) infos
+let is_logic_arity infos =
+ List.for_all (fun (logic,small) -> logic || small) infos
+
+let is_unit arinfos constrsinfos =
+ match constrsinfos with (* One info = One constructor *)
+ | [constrinfos] -> is_logic_constr constrinfos && is_logic_arity arinfos
+ | _ -> false
+
+let small_unit constrsinfos (env_par,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 isunit = is_unit arinfos constrsinfos in
+ issmall, isunit
+
+(* [smax] is the max of the sorts of the products of the constructor type *)
+
+let enforce_type_constructor arsort smax cst =
+ match smax, arsort with
+ | Type uc, Type ua -> Constraint.add (ua,Geq,uc) cst
+ | _,_ -> cst
+
+let type_one_constructor env_ar nparams arsort c =
+ let (infos,max,cst1) =
+ 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, j, cst3)
let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,spec) =
let (lna,vc) = decomp_all_DLAMV_name spec in
- let ((issmall,jlc),cst') =
+ let arsort = sort_of_arity env_ar ar in
+ let (constrsinfos,jlc,cst') =
List.fold_right
- (fun c ((small,jl),cst) ->
- let ((sm,jc),cst') = type_one_constructor env_ar nparams ar c in
- ((small && sm,jc::jl), Constraint.union cst cst'))
+ (fun c (infosl,jl,cst) ->
+ let (infos,jc,cst') = type_one_constructor env_ar nparams arsort c in
+ (infos::infosl,jc::jl, Constraint.union cst cst'))
(Array.to_list vc)
- ((true,[]),Constraint.empty)
+ ([],[],Constraint.empty)
in
- let castlc = List.map cast_of_judgment jlc in
+ let castlc = List.map incast_type jlc in
let spec' = put_DLAMSV lna (Array.of_list castlc) in
- let isunit = is_unit env_par nparams ar spec in
+ let issmall,isunit = small_unit constrsinfos (env_par,nparams,ar) in
let (_,tyar) = lookup_rel (ninds+1-i) env_ar in
((id,tyar,cnames,issmall,isunit,spec'), cst')
@@ -431,7 +440,7 @@ let add_mind sp mie env =
cci_inductive env env_arities kind nparams mie.mind_entry_finite inds cst
in
add_mind sp mib (add_constraints cst env)
-
+
let add_constraints = add_constraints
let pop_vars idl env =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 07e95197c..e95aa2390 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -62,19 +62,20 @@ val j_type : judgment -> constr
val j_kind : judgment -> constr
val safe_machine : safe_environment -> constr -> judgment * constraints
-val safe_machine_type : safe_environment -> constr -> typed_type
+val safe_machine_type : safe_environment -> constr -> typed_type * constraints
val fix_machine : safe_environment -> constr -> judgment * constraints
-val fix_machine_type : safe_environment -> constr -> typed_type
+val fix_machine_type : safe_environment -> constr -> typed_type * constraints
val unsafe_machine : safe_environment -> constr -> judgment * constraints
-val unsafe_machine_type : safe_environment -> constr -> typed_type
+val unsafe_machine_type : safe_environment -> constr -> typed_type * constraints
val type_of : safe_environment -> constr -> constr
+(*i obsolète
val type_of_type : safe_environment -> constr -> constr
-
val unsafe_type_of : safe_environment -> constr -> constr
+i*)
(*s Typing with information (extraction). *)
diff --git a/kernel/term.ml b/kernel/term.ml
index 576a92182..3ed337847 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -68,6 +68,7 @@ type constr = sorts oper term
type 'a judge = { body : constr; typ : 'a }
+(**)
type typed_type = sorts judge
type typed_term = typed_type judge
@@ -83,6 +84,21 @@ let incast_type tty = DOP2 (Cast, tty.body, (DOP0 (Sort tty.typ)))
let outcast_type = function
DOP2 (Cast, b, DOP0 (Sort s)) -> {body=b; typ=s}
| _ -> anomaly "outcast_type: Not an in-casted type judgement"
+(**)
+(*
+type typed_type = constr
+type typed_term = typed_type judge
+
+let make_typed t s = t
+
+let typed_app f tt = f tt
+
+let body_of_type ty = ty
+let level_of_type t = failwith "N'existe plus"
+
+let incast_type tty = tty
+let outcast_type x = x
+*)
(****************************************************************************)
(* Functions for dealing with constr terms *)
@@ -196,11 +212,10 @@ let mkMutCaseA ci p c ac =
Warning: as an invariant the ti are casted during the Fix formation;
these casts are then used by destFix
*)
-let in_fixcast {body=b; typ=s} = DOP2 (Cast, b, DOP0 (Sort s))
(* Here, we assume the body already constructed *)
let mkFixDlam recindxs i jtypsarray body =
- let typsarray = Array.map in_fixcast jtypsarray in
+ let typsarray = Array.map incast_type jtypsarray in
DOPN (Fix (recindxs,i),Array.append typsarray body)
let mkFix recindxs i jtypsarray funnames bodies =
@@ -229,7 +244,7 @@ let mkFix recindxs i jtypsarray funnames bodies =
*)
(* Here, we assume the body already constructed *)
let mkCoFixDlam i jtypsarray body =
- let typsarray = Array.map in_fixcast jtypsarray in
+ let typsarray = Array.map incast_type jtypsarray in
DOPN ((CoFix i),(Array.append typsarray body))
let mkCoFix i jtypsarray funnames bodies =
@@ -491,7 +506,7 @@ let destCase = function
*)
let out_fixcast = function
- | DOP2 (Cast, b, DOP0 (Sort s)) -> { body = b; typ = s }
+ | DOP2 (Cast, b, DOP0 (Sort s)) as c -> outcast_type c
| _ -> anomaly "destFix: malformed recursive definition"
let destGralFix a =
@@ -1368,8 +1383,14 @@ module Htype =
struct
type t = typed_type
type u = (constr -> constr) * (sorts -> sorts)
+(**)
let hash_sub (hc,hs) j = {body=hc j.body; typ=hs j.typ}
let equal j1 j2 = j1.body==j2.body & j1.typ==j2.typ
+(**)
+(*
+ let hash_sub (hc,hs) j = hc j
+ let equal j1 j2 = j1==j2
+*)
let hash = Hashtbl.hash
end)
diff --git a/kernel/term.mli b/kernel/term.mli
index d307e8dae..f3afa5e0a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -59,7 +59,7 @@ type constr = sorts oper term
type 'a judge = { body : constr; typ : 'a }
-type typed_type = sorts judge
+type typed_type
type typed_term = typed_type judge
val make_typed : constr -> sorts -> typed_type
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 5c4b5e41c..c88711635 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -17,8 +17,8 @@ open Type_errors
let make_judge v tj =
{ uj_val = v;
- uj_type = tj.body;
- uj_kind= DOP0 (Sort tj.typ) }
+ uj_type = body_of_type tj;
+ uj_kind= DOP0 (Sort (level_of_type tj)) }
let j_val_only j = j.uj_val
(* Faut-il caster ? *)
@@ -28,12 +28,13 @@ let j_val_cast j = mkCast j.uj_val j.uj_type
let typed_type_of_judgment env sigma j =
match whd_betadeltaiota env sigma j.uj_kind with
- | DOP0(Sort s) -> { body = j.uj_type; typ = s }
+ | DOP0(Sort s) -> make_typed j.uj_type s
| _ -> error_not_type CCI env j.uj_type
+
let assumption_of_judgment env sigma j =
match whd_betadeltaiota env sigma j.uj_type with
- | DOP0(Sort s) -> { body = j.uj_val; typ = s }
+ | DOP0(Sort s) -> make_typed j.uj_val s
| _ -> error_assumption CCI env j.uj_val
(* Type of a de Bruijn index. *)
@@ -42,8 +43,8 @@ let relative env n =
try
let (_,typ) = lookup_rel n env in
{ uj_val = Rel n;
- uj_type = lift n typ.body;
- uj_kind = DOP0 (Sort typ.typ) }
+ uj_type = lift n (body_of_type typ);
+ uj_kind = DOP0 (Sort (level_of_type typ)) }
with Not_found ->
error_unbound_rel CCI env n
@@ -78,11 +79,7 @@ let check_hyps id env sigma hyps =
(* Instantiation of terms on real arguments. *)
-let type_of_constant env sigma (sp,args) =
- let cb = lookup_constant sp env in
- let hyps = cb.const_hyps in
- (* TODO: check args *)
- instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args)
+let type_of_constant = Instantiate.constant_type
(* Inductive types. *)
@@ -244,7 +241,7 @@ let is_correct_arity env sigma kelim (c,p) =
in
srec
-let find_case_dep_nparams env sigma (c,p) (mind,largs) typP =
+let find_case_dep_nparams env sigma (c,p) (mind,largs) typP =
let mis = lookup_mind_specif mind env in
let nparams = mis_nparams mis
and kelim = mis_kelim mis
@@ -387,7 +384,8 @@ let sort_of_product_without_univ domsort rangsort =
let abs_rel env sigma name var j =
let rngtyp = whd_betadeltaiota env sigma j.uj_kind in
let cvar = incast_type var in
- let (s,cst) = sort_of_product var.typ (destSort rngtyp) (universes env) in
+ let (s,cst) =
+ sort_of_product (level_of_type var) (destSort rngtyp) (universes env) in
{ uj_val = mkLambda name cvar (j_val j);
uj_type = mkProd name cvar j.uj_type;
uj_kind = mkSort s },
@@ -404,11 +402,11 @@ let gen_rel env sigma name var j =
else
match jtyp with
| DOP0(Sort s) ->
- let (s',g) = sort_of_product var.typ s (universes env) in
+ let (s',g) = sort_of_product (level_of_type var) s (universes env) in
let res_type = mkSort s' in
let (res_kind,g') = type_of_sort res_type in
{ uj_val =
- mkProd name (mkCast var.body (mkSort var.typ)) (j_val_cast j);
+ mkProd name (incast_type var) (j_val_cast j);
uj_type = res_type;
uj_kind = res_kind }, g'
| _ ->
@@ -967,7 +965,7 @@ let keep_hyps sign needed =
(fun ((hyps,globs) as sofar) id a ->
if Idset.mem id globs then
(add_sign (id,a) hyps,
- Idset.union (global_vars_set a.body) globs)
+ 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 e526d82fb..541135442 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -55,6 +55,7 @@ val gen_rel :
env -> 'a evar_map -> name -> typed_type -> unsafe_judgment
-> unsafe_judgment * constraints
+val sort_of_product : sorts -> sorts -> universes -> sorts * constraints
val sort_of_product_without_univ : sorts -> sorts -> sorts
val cast_rel :
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index ab1aef1f5..10e43172b 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -136,7 +136,7 @@ let print_mutual sp mib =
let env = Global.env () in
let evd = Evd.empty in
let {mind_packets=mipv; mind_nparams=nparams} = mib in
- let (lpars,_) = decomp_n_prod env evd nparams mipv.(0).mind_arity.body in
+ let (lpars,_) = decomp_n_prod env evd nparams (body_of_type mipv.(0).mind_arity) in
let lparsname = List.map fst lpars in
let lparsprint = assumptions_for_print lparsname in
let prass ass_name (id,c) =
@@ -154,7 +154,7 @@ let print_mutual sp mib =
(hV 0 [< 'sTR " "; plidC >])
in
let print_oneind mip =
- let (_,arity) = decomp_n_prod env evd nparams mip.mind_arity.body in
+ let (_,arity) = decomp_n_prod env evd nparams (body_of_type mip.mind_arity) in
(hOV 0
[< (hOV 0
[< print_id mip.mind_typename ; 'bRK(1,2);
@@ -169,7 +169,7 @@ let print_mutual sp mib =
let mip = mipv.(0) in
(* Case one [co]inductive *)
if Array.length mipv = 1 then
- let (_,arity) = decomp_n_prod env evd nparams mip.mind_arity.body in
+ let (_,arity) = decomp_n_prod env evd nparams (body_of_type mip.mind_arity) in
let sfinite = if mip.mind_finite then "Inductive " else "CoInductive " in
(hOV 0 [< 'sTR sfinite ; print_id mip.mind_typename ;
if nparams = 0 then
@@ -369,13 +369,13 @@ let crible (fn : string -> unit assumptions -> constr -> unit) name =
(match (spopt,object_tag lobj) with
| (_,"VARIABLE") ->
let (namec,typ,_,_) = out_variable spopt in
- if (head_const typ.body) = const then
- fn (string_of_id namec) hyps typ.body;
+ if (head_const (body_of_type typ)) = const then
+ fn (string_of_id namec) hyps (body_of_type typ);
crible_rec rest
| (sp,("CONSTANT"|"PARAMETER")) ->
let {const_type=typ} = Global.lookup_constant sp in
- if (head_const typ.body) = const then
- fn (print_basename sp) hyps typ.body;
+ if (head_const (body_of_type typ)) = const then
+ fn (print_basename sp) hyps (body_of_type typ);
crible_rec rest
| (sp,"INDUCTIVE") ->
let mib = Global.lookup_mind sp in
@@ -466,20 +466,21 @@ let print_opaque_name name =
let env = Global.env () in
let sign = Global.var_context () in
try
- match global_reference CCI name with
- | DOPN(Const sp,_) as x ->
+ let x = global_reference CCI name in
+ match kind_of_term x with
+ | IsConst (sp,_ as cst) ->
let cb = Global.lookup_constant sp in
if is_defined cb then
- let typ = constant_type env x in
- print_typed_value (constant_value env x,typ.body)
+ let typ = constant_type env Evd.empty cst in
+ print_typed_value (constant_value env x, body_of_type typ)
else
anomaly "print_opaque_name"
- | DOPN(MutInd (sp,_),_) as x ->
+ | IsMutInd ((sp,_),_) ->
print_mutual sp (Global.lookup_mind sp)
- | DOPN(MutConstruct cstr_sp,a) as x ->
- let ty = Typeops.type_of_constructor env sigma (cstr_sp,a) in
+ | IsMutConstruct cstr ->
+ let ty = Typeops.type_of_constructor env sigma cstr in
print_typed_value(x, ty)
- | VAR id ->
+ | IsVar id ->
let a = snd(lookup_sign id sign) in
print_var (string_of_id id) a
| _ -> failwith "print_name"
diff --git a/parsing/printer.ml b/parsing/printer.ml
index c8059e37e..99db762e0 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -86,10 +86,10 @@ let prterm = prterm_env (gLOB nil_sign)
let fprterm_env a = gentermpr FW a
let fprterm = fprterm_env (gLOB nil_sign)
-let prtype_env env typ = prterm_env env (mkCast typ.body (mkSort typ.typ))
+let prtype_env env typ = prterm_env env (incast_type typ)
let prtype = prtype_env (gLOB nil_sign)
-let fprtype_env env typ = fprterm_env env (mkCast typ.body (mkSort typ.typ))
+let fprtype_env env typ = fprterm_env env (incast_type typ)
let fprtype = fprtype_env (gLOB nil_sign)
let pr_constant cst = gencompr CCI (ast_of_constant cst)
@@ -124,11 +124,11 @@ and default_tacpr = function
| gt -> dfltpr gt
let print_decl k sign (s,typ) =
- let ptyp = gentermpr k (gLOB sign) typ.body in
+ let ptyp = gentermpr k (gLOB sign) (body_of_type typ) in
[< print_id s ; 'sTR" : "; ptyp >]
let print_binding k env (na,typ) =
- let ptyp = gentermpr k env typ.body in
+ let ptyp = gentermpr k env (body_of_type typ) in
match na with
| Anonymous -> [< 'sTR"<>" ; 'sTR" : " ; ptyp >]
| Name id -> [< print_id id ; 'sTR" : "; ptyp >]
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 15945dd45..15577dd9e 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -91,8 +91,7 @@ let inh_tosort env isevars j =
let inh_ass_of_j env isevars j =
let typ = whd_betadeltaiota env !isevars j.uj_type in
match typ with
- | DOP0(Sort s) ->
- { body = j.uj_val; typ = s }
+ | DOP0(Sort s) -> make_typed j.uj_val s
| _ ->
let j1 = inh_tosort_force env isevars j in
assumption_of_judgment env !isevars j1
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 539a953a1..241e4ec05 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -22,7 +22,7 @@ let tjudge_of_cast_safe sigma env var =
match under_casts (fun _ -> nf_ise1) env sigma var with
| DOP2 (Cast, b, t) ->
(match whd_betadeltaiota env sigma t with
- | DOP0 (Sort s) -> {body=b; typ=s}
+ | DOP0 (Sort s) -> make_typed b s
| _ -> anomaly "Not a type (tjudge_of_cast)")
| c -> execute_rec_type env sigma c
(* FIN TMP ***** *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f7b1c51cc..e9b74bd95 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -208,14 +208,14 @@ let evar_type_case isevars env ct pt lft p c =
let pretype_var loc env id =
try
match lookup_id id (context env) with
- | RELNAME (n,{body=typ;typ=s}) ->
+ | RELNAME (n,typ) ->
{ uj_val = Rel n;
- uj_type = lift n typ;
- uj_kind = DOP0 (Sort s) }
- | GLOBNAME (id,{body=typ;typ=s}) ->
+ uj_type = lift n (body_of_type typ);
+ uj_kind = DOP0 (Sort (level_of_type typ)) }
+ | GLOBNAME (id,typ) ->
{ uj_val = VAR id;
- uj_type = typ;
- uj_kind = DOP0 (Sort s) }
+ uj_type = body_of_type typ;
+ uj_kind = DOP0 (Sort (level_of_type typ)) }
with Not_found ->
error_var_not_found_loc loc CCI id
@@ -448,7 +448,8 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
let tj = pretype def_vty_con env isevars t in
let tj = inh_tosort_force env isevars tj in
let cj =
- pretype (mk_tycon2 vtcon (assumption_of_judgment env !isevars tj).body)
+ pretype
+ (mk_tycon2 vtcon (body_of_type (assumption_of_judgment env !isevars tj)))
env isevars c in
inh_cast_rel env isevars cj tj
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 8579b495b..71e79a791 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -191,9 +191,9 @@ let split_sign hfrom hto l =
let move_after with_dep toleft (left,htfrom,right) hto =
let test_dep (hyp,typ) (hyp2,typ2) =
if toleft then
- occur_var hyp2 typ.body
+ occur_var hyp2 (body_of_type typ)
else
- occur_var hyp typ2.body
+ occur_var hyp (body_of_type typ2)
in
let rec moverec first middle = function
| [] -> error ("No such hypothesis : " ^ (string_of_id hto))
@@ -264,7 +264,7 @@ let prim_refiner r sigma goal =
if not (List.for_all
(mem_sign (tl_sign (sign_prefix id sign)))
(global_vars c1))
- or List.exists (fun t -> occur_var id t.body)
+ or List.exists (fun t -> occur_var id (body_of_type t))
(vals_of_sign sign)
then
error
@@ -368,7 +368,7 @@ let prim_refiner r sigma goal =
(* Faut-il garder la sorte d'origine ou celle du converti ?? *)
let env' = change_hyps (sign_before id) env in
let tj = execute_type env' sigma ty' in
- if is_conv env sigma ty' (snd(lookup_sign id sign)).body then
+ if is_conv env sigma ty' (body_of_type (snd(lookup_sign id sign))) then
let env' = change_hyps (modify_sign id tj) env in
[mk_goal info env' cl]
else
@@ -381,7 +381,7 @@ let prim_refiner r sigma goal =
let (s',ty),tlsign = uncons_sign sign in
if s = s' then
tlsign
- else if occur_var s ty.body then
+ else if occur_var s (body_of_type ty) then
error ((string_of_id s) ^ " is used in the hypothesis "
^ (string_of_id s'))
else
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index a02ee4fae..a9c65d50c 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -318,7 +318,8 @@ let pr_seq evd =
let pc = pr_ctxt info in
let pdcl =
prlist_with_sep pr_spc
- (fun (id,ty) -> hOV 0 [< print_id id; 'sTR" : ";prterm ty.body >])
+ (fun (id,ty) ->
+ hOV 0 [< print_id id; 'sTR" : ";prterm (body_of_type ty) >])
sign
in
let pcl = prterm_env_at_top (gLOB hyps) cl in
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 720936110..b0880065a 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -46,7 +46,7 @@ let pf_concl gls = (sig_it gls).evar_concl
let pf_untyped_hyps gls =
let sign = Environ.var_context (pf_env gls) in
- map_sign_typ (fun x -> x.body) sign
+ map_sign_typ (fun x -> body_of_type x) sign
let pf_nth_hyp gls n = nth_sign (pf_untyped_hyps gls) n
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 10bf2e53b..9f207d27d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1372,7 +1372,7 @@ let sub_term_with_unif cref ceq =
let general_rewrite_in lft2rgt id (c,lb) gls =
let typ_id =
(try
- let (_,ty) = lookup_var id (pf_env gls) in ty.body
+ let (_,ty) = lookup_var id (pf_env gls) in (body_of_type ty)
with Not_found ->
errorlabstrm "general_rewrite_in"
[< 'sTR"No such hypothesis : "; print_id id >])
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 91bab946e..2f755b4e3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -154,7 +154,7 @@ let build_mutual lparams lnamearconstrs finite =
(mkProdCit lparams constr))
lname_constr
in
- (name, ar.body, List.map fst lname_constr,
+ (name, (body_of_type ar), List.map fst lname_constr,
put_DLAMSV_subst (List.rev lrecnames) (Array.of_list consconstrl)))
(List.rev arityl) lnamearconstrs
in
@@ -219,7 +219,7 @@ let build_recursive lnameargsardef =
List.fold_left
(fun (env,arl) (recname,lparams,arityc,_) ->
let arity = typed_type_of_com Evd.empty env (mkProdCit lparams arityc) in
- declare_variable recname (arity.body,NeverDischarge,false);
+ declare_variable recname (body_of_type arity,NeverDischarge,false);
(Environ.push_var (recname,arity) env, (arity::arl)))
(env0,[]) lnameargsardef
with e ->
@@ -282,7 +282,7 @@ let build_corecursive lnameardef =
List.fold_left
(fun (env,arl) (recname,arityc,_) ->
let arity = typed_type_of_com Evd.empty env0 arityc in
- declare_variable recname (arity.body,NeverDischarge,false);
+ declare_variable recname (body_of_type arity,NeverDischarge,false);
(Environ.push_var (recname,arity) env, (arity::arl)))
(env0,[]) lnameardef
with e ->
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index aab790252..8de338b40 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -27,14 +27,14 @@ let recalc_sp sp =
let whd_all c = whd_betadeltaiota (Global.env()) Evd.empty c
let generalize_type id var c =
- let c' = mkProd (Name id) var.body (subst_var id c.body) in
- let c'ty = sort_of_product_without_univ var.typ c.typ in
- { body = c'; typ = c'ty }
+ let c' = mkProd (Name id) (body_of_type var) (subst_var id (body_of_type c)) in
+ let c'ty = sort_of_product_without_univ (level_of_type var) (level_of_type c) in
+ make_typed c' c'ty
let casted_generalize id var c =
- let c' = mkProd (Name id) var.body (subst_var id (cast_term c)) in
+ let c' = mkProd (Name id) (body_of_type var) (subst_var id (cast_term c)) in
let s = destSort (whd_all (cast_type c)) in
- let c'ty = sort_of_product_without_univ var.typ s in
+ let c'ty = sort_of_product_without_univ (level_of_type var) s in
mkCast c' (DOP0 (Sort c'ty))
type modification_action = ABSTRACT | ERASE
@@ -125,7 +125,7 @@ let abstract_inductive ids_to_abs hyps inds =
in
let (_,inds',revmodl) =
List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in
- let inds'' = List.map (fun (a,b,c,d) -> (a,b.body,c,d)) inds' in
+ let inds'' = List.map (fun (a,b,c,d) -> (a,body_of_type b,c,d)) inds' in
(inds'', List.rev revmodl)
let abstract_constant ids_to_abs hyps (body,typ) =
@@ -144,9 +144,9 @@ let abstract_constant ids_to_abs hyps (body,typ) =
Some (ref (Recipe
(fun () -> mkLambda name cvar (subst_var id (f())))))
in
- let typ' =
- { body = mkProd name cvar (subst_var id typ.body);
- typ = sort_of_product_without_univ var.typ typ.typ }
+ let typ' = make_typed
+ (mkProd name cvar (subst_var id (body_of_type typ)))
+ (sort_of_product_without_univ (level_of_type var) (level_of_type typ))
in
(tl_sign hyps,body',typ',ABSTRACT::modl)
in
@@ -182,8 +182,8 @@ let expmod_constr oldenv modlist c =
| DOP2 (Cast,val_0,typ) -> DOP2 (Cast,simpfun val_0,simpfun typ)
| _ -> simpfun c'
-let expmod_type oldenv modlist {body=c;typ=s} =
- { body = expmod_constr oldenv modlist c; typ = s }
+let expmod_type oldenv modlist c =
+ typed_app (expmod_constr oldenv modlist) c
let expmod_constant_value opaque oldenv modlist = function
| None -> None
@@ -236,7 +236,7 @@ let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb =
let hyps = map_sign_typ (expmod_type oldenv modlist) cb.const_hyps in
let (body',typ',modl) = abstract_constant ids_to_discard hyps (body,typ) in
let mods = [ (Const osecsp, DO_ABSTRACT(Const nsecsp,modl)) ] in
- (body', typ'.body, mods)
+ (body', body_of_type typ', mods)
(* Discharge of the various objects of the environment. *)
@@ -273,7 +273,7 @@ let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
if stre = (DischargeAt sec_sp) or ids_to_discard <> [] then
(ops,id::ids_to_discard,work_alist)
else
- let expmod_a = expmod_constr oldenv work_alist a.body in
+ let expmod_a = expmod_constr oldenv work_alist (body_of_type a) in
(Variable (id,expmod_a,stre,sticky) :: ops,
ids_to_discard,work_alist)
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index ad4f6f389..bce23275f 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -4,7 +4,7 @@
open Pp
open Util
open Ast
-open Inductive
+open Indtypes
open Type_errors
open Lexer
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8c2b61eb4..4c1b0e4b7 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -8,6 +8,7 @@ open Names
open Generic
open Term
open Inductive
+open Indtypes
open Sign
open Environ
open Type_errors
@@ -93,7 +94,7 @@ let explain_ill_formed_branch k ctx c i actty expty =
let explain_generalization k ctx (name,var) c =
let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
- let pv = gentermpr k ctx var.body in
+ let pv = gentermpr k ctx (body_of_type var) in
let pc = gentermpr k (add_rel (name,var) ctx) c in
[< 'sTR"Illegal generalization: "; pe; 'fNL;
'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 7bf0ef9c8..edebaaf52 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -4,7 +4,7 @@
(*i*)
open Pp
open Names
-open Inductive
+open Indtypes
open Sign
open Type_errors
open Logic
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 673f4a4f6..c4cc168d7 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -71,14 +71,14 @@ let typecheck_params_and_field ps fs =
List.fold_left
(fun (env,newps) (id,t) ->
let tj = typed_type_of_com Evd.empty env t in
- (Environ.push_var (id,tj) env,(id,tj.body)::newps))
+ (Environ.push_var (id,tj) env,(id,body_of_type tj)::newps))
(env0,[]) ps
in
let env2,newfs =
List.fold_left
(fun (env,newfs) (id,t) ->
let tj = typed_type_of_com Evd.empty env t in
- (Environ.push_var (id,tj) env,(id,tj.body)::newfs)) (env1,[]) fs
+ (Environ.push_var (id,tj) env,(id,body_of_type tj)::newfs)) (env1,[]) fs
in
List.rev(newps),List.rev(newfs)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 21:25:32 +0000