aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-04-20 15:51:40 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-04-20 15:51:40 +0000
commita002d6ef127b4f0103012c23fc5d272739649043 (patch)
tree99c7ba136ce8488d2086290b3ff18fe91cdf6073 /kernel
parentb8cd60cf1b3817a1802459310e79a8addb628ee7 (diff)
Abstraction du type typed_type (un pas vers les jugements 2 niveaux)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@362 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-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
13 files changed, 308 insertions, 265 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 :