aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/environ.ml1
-rw-r--r--kernel/indtypes.ml232
-rw-r--r--kernel/indtypes.mli10
-rw-r--r--kernel/instantiate.ml6
-rw-r--r--kernel/instantiate.mli4
-rw-r--r--kernel/reduction.ml8
-rw-r--r--kernel/reduction.mli1
-rw-r--r--kernel/term.ml2
-rw-r--r--kernel/term.mli2
-rw-r--r--kernel/typing.ml123
10 files changed, 365 insertions, 24 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 5cd8cc801c..3608e969fe 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -223,3 +223,4 @@ type unsafe_judgment = {
let cast_of_judgment = function
| { uj_val = DOP2 (Cast,_,_) as c } -> c
| { uj_val = c; uj_type = ty } -> mkCast c ty
+
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 82da97329a..0988ae1972 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -1,8 +1,13 @@
(* $Id$ *)
+open Util
+open Generic
+open Term
open Inductive
+open Sign
open Environ
+open Instantiate
open Reduction
let mind_check_arities env mie =
@@ -11,3 +16,230 @@ let mind_check_arities env mie =
in
List.iter (fun (id,ar,_,_) -> check_arity id ar) mie.mind_entry_inds
+let sort_of_arity env c =
+ let rec sort_of ar =
+ match whd_betadeltaiota env ar with
+ | DOP0 (Sort s) -> s
+ | DOP2 (Prod, _, DLAM (_, c)) -> sort_of c
+ | _ -> error "not an arity"
+ in
+ sort_of c
+
+let allowed_sorts issmall isunit = function
+ | Type _ ->
+ [prop;spec;types]
+ | Prop Pos ->
+ if issmall then [prop;spec;types] else [prop;spec]
+ | Prop Null ->
+ if isunit then [prop;spec] else [prop]
+
+let is_small_type t = is_small t.typ
+
+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 (InductiveError (NonPos (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 (InductiveError (NotEnoughArgs 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 lpar.(k)) then
+ raise (InductiveError (NonPar (k+1,l)))
+ done;
+ if not (array_for_all (noccur_bet n ntypes) largs') then
+ failwith_non_pos_vect n ntypes largs'
+
+let abstract_mind_lc env ntyps npars lc =
+ let lC = decomp_DLAMV ntyps lc in
+ if npars = 0 then
+ lC
+ else
+ let make_abs =
+ list_tabulate
+ (function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps
+ in
+ Array.map (compose (nf_beta env) (substl make_abs)) lC
+
+let decomp_par n c = snd (decompose_prod_n n c)
+
+let listrec_mconstr env ntypes nparams i indlc =
+ (* check the inductive types occur positively in C *)
+ let rec check_pos n c =
+ match whd_betadeltaiota env c with
+ | DOP2(Prod,b,DLAM(na,d)) ->
+ if not (noccur_bet n ntypes b) then raise (InductiveError (NonPos n));
+ check_pos (n+1) d
+ | x ->
+ (match ensure_appl x with
+ | DOPN(AppL,cl) ->
+ let hd = array_hd cl
+ and largs = array_tl cl in
+ (match hd with
+ | Rel k ->
+ check_correct_par env nparams ntypes n (k-n+1) largs;
+ if k >= n && k<n+ntypes then
+ Mrec(n+ntypes-k-1)
+ else if noccur_bet n ntypes x then
+ if (n-nparams) <= k & k <= (n-1)
+ then Param(n-1-k)
+ else Norec
+ else
+ raise (InductiveError (NonPos n))
+ | (DOPN(MutInd(sp,i),_) as mi) ->
+ if (noccur_bet n ntypes x) then
+ Norec
+ else
+ Imbr(sp,i,imbr_positive n mi largs)
+ | err ->
+ if noccur_bet n ntypes x then Norec
+ else raise (InductiveError (NonPos n)))
+ | _ -> anomaly "check_pos")
+
+ 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 (InductiveError (NonPos n));
+ let auxlc = mis_lc env mispeci
+ and auxntyp = mis_ntypes mispeci in
+ if auxntyp <> 1 then raise (InductiveError (NonPos n));
+ let lrecargs = array_map_to_list (check_param_pos n) lpar in
+ (* The abstract imbricated inductive type with parameters substituted *)
+ let auxlcvect = abstract_mind_lc env auxntyp auxnpar auxlc in
+ let newidx = n + auxntyp in
+ let _ =
+ (* fails if the inductive type occurs non positively *)
+ (* when substituted *)
+ Array.map
+ (function c ->
+ let c' = hnf_prod_appvect env "is_imbr_pos" c
+ (Array.map (lift auxntyp) lpar) in
+ check_construct false newidx c')
+ auxlcvect
+ in
+ lrecargs
+
+ (* The function check_param_pos is exactly the same as check_pos, but
+ with an extra case for traversing abstractions, like in Marseille's
+ contribution about bisimulations:
+
+ CoInductive strong_eq:process->process->Prop:=
+ str_eq:(p,q:process)((a:action)(p':process)(transition p a p')->
+ (Ex [q':process] (transition q a q')/\(strong_eq p' q')))->
+ ((a:action)(q':process)(transition q a q')->
+ (Ex [p':process] (transition p a p')/\(strong_eq p' q')))->
+ (strong_eq p q).
+
+ Abstractions may occur in imbricated recursive ocurrences, but I am
+ not sure if they make sense in a form of constructor. This is why I
+ chose to duplicated the code. Eduardo 13/7/99. *)
+ and check_param_pos n c =
+ match whd_betadeltaiota env c with
+ (* The extra case *)
+ | DOP2(Lambda,b,DLAM(na,d)) ->
+ if noccur_bet n ntypes b
+ then check_param_pos (n+1) d
+ else raise (InductiveError (NonPos n))
+ (******************)
+ | DOP2(Prod,b,DLAM(na,d)) ->
+ if (noccur_bet n ntypes b)
+ then check_param_pos (n+1) d
+ else raise (InductiveError (NonPos n))
+ | x ->
+ (match ensure_appl x with
+ | DOPN(AppL,cl) ->
+ let hd = array_hd cl
+ and largs = array_tl cl in
+ (match hd with
+ | Rel k ->
+ check_correct_par env nparams ntypes n (k-n+1) largs;
+ if k >= n & k<n+ntypes then
+ Mrec(n+ntypes-k-1)
+ else if noccur_bet n ntypes x then
+ if (n-nparams) <= k & k <= (n-1)
+ then Param(n-1-k)
+ else Norec
+ else raise (InductiveError (NonPos n))
+ | (DOPN(MutInd(sp,i),_) as mi) ->
+ if (noccur_bet n ntypes x)
+ then Norec
+ else Imbr(sp,i,imbr_positive n mi largs)
+ | err -> if noccur_bet n ntypes x then Norec
+ else raise (InductiveError (NonPos n)))
+ | _ -> anomaly "check_param_pos")
+
+ (* check the inductive types occur positively in the products of C, if
+ checkhd=true, also check the head corresponds to a constructor of
+ the ith type *)
+
+ and check_construct check =
+ let rec check_constr_rec lrec n c =
+ match whd_betadeltaiota env c with
+ | DOP2(Prod,b,DLAM(na,d)) ->
+ let recarg = (check_pos n b) in
+ check_constr_rec (recarg::lrec) (n+1) d
+ | x ->
+ (match ensure_appl x with
+ | DOPN(AppL,cl) ->
+ let hd = array_hd cl
+ and largs = array_tl cl in
+ if check then
+ (match hd with
+ | Rel k ->
+ check_correct_par env nparams ntypes n (k-n+1) largs;
+ if k = n+ntypes-i then
+ List.rev lrec
+ else
+ raise (InductiveError (NonPos n))
+ | _ -> raise (InductiveError (NonPos n)))
+ else
+ if array_for_all (noccur_bet n ntypes) largs
+ then List.rev lrec
+ else raise (InductiveError (NonPos n))
+ | _ -> anomaly "ensure_appl should return an AppL")
+ in check_constr_rec []
+ in
+ let (lna,lC) = decomp_DLAMV_name ntypes indlc in
+ Array.map
+ (fun c ->
+ (* try *)
+ check_construct true (1+nparams) (decomp_par nparams c)
+ (* with InductiveError err ->
+ explain_ind_err (ntypes-i+1) lna nparams c err *))
+ lC
+
+let is_recursive listind =
+ let rec one_is_rec rvec =
+ List.exists (function Mrec(i) -> List.mem i listind
+ | Imbr(_,_,lvec) -> one_is_rec lvec
+ | Norec -> false
+ | Param _ -> false) rvec
+ in
+ array_exists one_is_rec
+
+let cci_inductive env env_ar kind nparams finite inds =
+ let ntypes = List.length inds in
+ 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 kelim = allowed_sorts issmall isunit (sort_of_arity env ar.body) in
+ { mind_consnames = Array.of_list cnames;
+ mind_typename = id;
+ mind_lc = lc;
+ mind_arity = ar;
+ mind_kelim = kelim;
+ mind_listrec = recargs;
+ mind_finite = finite }
+ in
+ let packets = Array.of_list (list_map_i one_packet 1 inds) in
+ { mind_kind = kind;
+ mind_ntypes = ntypes;
+ mind_hyps = get_globals (context env);
+ mind_packets = packets;
+ mind_singl = None;
+ mind_nparams = nparams }
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 8723ec3c65..ebb1e1f679 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -2,6 +2,8 @@
(* $Id$ *)
(*i*)
+open Names
+open Term
open Inductive
open Environ
(*i*)
@@ -10,3 +12,11 @@ open Environ
inductive types are some arities. *)
val mind_check_arities : 'a unsafe_env -> mutual_inductive_entry -> unit
+
+val sort_of_arity : 'a unsafe_env -> constr -> sorts
+
+val cci_inductive :
+ 'a unsafe_env -> 'a unsafe_env -> path_kind -> int -> bool ->
+ (identifier * typed_type * identifier list * bool * bool * constr) list ->
+ mutual_inductive_body
+
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 6302badc22..9b4c1ae710 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -8,6 +8,7 @@ open Generic
open Term
open Sign
open Constant
+open Inductive
open Evd
open Environ
@@ -101,3 +102,8 @@ let const_abst_opt_value env c =
| DOPN(Abst sp,_) ->
if evaluable_abst env c then Some (abst_value env c) else None
| _ -> invalid_arg "const_abst_opt_value"
+
+let mis_lc env mis =
+ instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc
+ (Array.to_list mis.mis_args)
+
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 0bcdabf6d2..73d6de1b12 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -4,6 +4,7 @@
(*i*)
open Names
open Term
+open Inductive
open Environ
(*i*)
@@ -21,3 +22,6 @@ val const_or_ex_value : 'a unsafe_env -> constr -> constr
val const_or_ex_type : 'a unsafe_env -> constr -> constr
val const_abst_opt_value : 'a unsafe_env -> constr -> constr option
+
+val mis_lc : 'a unsafe_env -> mind_specif -> constr
+
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 7e81089453..77331bf5a2 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1306,7 +1306,13 @@ let is_type_arity env =
| _ -> false
in
srec
-
+
+let is_info_type env t =
+ let s = t.typ in
+ (s = Prop Pos) ||
+ (s <> Prop Null &&
+ try info_arity env t.body with IsType -> true)
+
let is_info_cast_type env c =
match c with
| DOP2(Cast,c,t) ->
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index c9cafccec4..6e6c243c76 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -104,6 +104,7 @@ val is_info_arity : 'c unsafe_env -> constr -> bool
val is_info_sort : 'c unsafe_env -> constr -> bool
val is_logic_arity : 'c unsafe_env -> constr -> bool
val is_type_arity : 'c unsafe_env -> constr -> bool
+val is_info_type : 'c unsafe_env -> typed_type -> bool
val is_info_cast_type : 'c unsafe_env -> constr -> bool
val contents_of_cast_type : 'c unsafe_env -> constr -> contents
val poly_args : 'a unsafe_env -> constr -> int list
diff --git a/kernel/term.ml b/kernel/term.ml
index 94ce20615e..46bcebcd84 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -59,6 +59,8 @@ type 'a judge = { body : constr; typ : 'a }
type typed_type = sorts judge
type typed_term = typed_type judge
+let make_typed t s = { body = t; typ = s }
+
let typed_app f tt = { body = f tt.body; typ = tt.typ }
let body_of_type ty = ty.body
diff --git a/kernel/term.mli b/kernel/term.mli
index 0af1cf6133..0fc2a5e8f0 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -56,6 +56,8 @@ type 'a judge = { body : constr; typ : 'a }
type typed_type = sorts judge
type typed_term = typed_type judge
+val make_typed : constr -> sorts -> typed_type
+
val typed_app : (constr -> constr) -> typed_type -> typed_type
val body_of_type : typed_type -> constr
diff --git a/kernel/typing.ml b/kernel/typing.ml
index b9ef2893a2..1366738689 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -16,6 +16,8 @@ open Type_errors
open Typeops
open Indtypes
+type judgment = unsafe_judgment
+
(* Fonctions temporaires pour relier la forme castée de la forme jugement *)
let tjudge_of_cast env = function
@@ -232,6 +234,23 @@ let unsafe_type_of env c =
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 =
+ let type_one (env,l) c =
+ let (j,u) = safe_machine env c in
+ (set_universes u env, j::l)
+ in
+ List.fold_left type_one (env,[]) cl
+
+let safe_machine_v env cv =
+ let type_one (env,l) c =
+ let (j,u) = safe_machine env c in
+ (set_universes u env, j::l)
+ in
+ let env',l = Array.fold_left type_one (env,[]) cv in
+ (env', Array.of_list l)
+
(*s Safe environments. *)
@@ -307,39 +326,97 @@ let add_parameter sp c env =
(* Insertion of inductive types. *)
-let check_type_constructs env_params univ nparams lc =
- let check_one env c =
- let (_,c) = decompose_prod_n nparams c in
- let (j,u) = safe_machine env c in
- match whd_betadeltaiota env j.uj_type with
- | DOP0 (Sort (Type uc)) -> set_universes (enforce_geq univ uc u) env
- | _ -> error "Type of Constructor not well-formed"
+(* [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 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,u) = unsafe_machine env b in
+ let var = assumption_of_judgement env jb in
+ (p var) &&
+ (let env' = Environ.push_rel (name,var) (set_universes u 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 =
+ match whd_betadeltaiota env j.uj_type with
+ | DOP0 (Sort (Type uc)) ->
+ let u = universes env in
+ set_universes (enforce_geq univ uc u) env
+ | _ -> error "Type of Constructor not well-formed"
+
+let type_one_constructor env_ar env_par nparams ar c =
+ let (jc,u) = safe_machine env_ar c in
+ let env = set_universes u env_ar in
+ let env' = match sort_of_arity env_ar ar with
+ | Type u -> enforce_type_constructor env u jc
+ | Prop _ -> env
in
- Array.fold_left check_one env_params lc
-
-let check_prop_constructs env_ar lc =
- let check_one c =
- let (j,_) = safe_machine env_ar c in
- match whd_betadeltaiota env_ar j.uj_type with
- | DOP0 (Sort _) -> cast_of_judgment j
- | _ -> error "The type of a constructor must be a type"
+ let (_,c) = decompose_prod_n nparams jc.uj_val in
+ let issmall = is_small_type env_par c in
+ (env', (issmall,jc))
+
+let logic_constr env c =
+ for_all_prods (fun t -> not (is_info_type env t)) env c
+
+let logic_arity env c =
+ for_all_prods
+ (fun t -> (not (is_info_type env 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) = decompose_prod_n nparams ar in logic_arity env_par ar) &&
+ (let (_,c') = decompose_prod_n nparams c in logic_constr env_par c')
+ | _ -> false
+
+let type_one_inductive env_ar env_par nparams (id,ar,cnames,spec) =
+ let (lna,vc) = decomp_all_DLAMV_name spec in
+ let (env',(issmall,jlc)) =
+ List.fold_left
+ (fun (env,(small,jl)) c ->
+ let (env',(sm,jc)) = type_one_constructor env env_par nparams ar c in
+ (env', (small && sm,jc::jl)))
+ (env_ar,(true,[])) (Array.to_list vc)
in
- Array.map check_one lc
+ let castlc = List.map cast_of_judgment jlc in
+ let spec' = put_DLAMSV lna (Array.of_list castlc) in
+ let isunit = is_unit env_par nparams ar spec in
+ let (_,tyar) = lookup_var id env' in
+ (env', (id,tyar,cnames,issmall,isunit,spec'))
let add_mind sp mie env =
mind_check_names mie;
mind_check_arities env mie;
let params = mind_extract_and_check_params mie in
+ let nparams = mie.mind_entry_nparams in
mind_check_lc params mie;
- let env_arities =
- push_rels
- (List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds) 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
let env_params = push_rels params env_arities in
- (* ICI *)
- env_arities
-
-type judgment = unsafe_judgment
+ let env_arities',inds =
+ List.fold_left
+ (fun (env,inds) ind ->
+ let (env',ind') = type_one_inductive env env_params nparams ind in
+ (env',ind'::inds))
+ (env_arities,[]) mie.mind_entry_inds
+ in
+ let kind = kind_of_path sp in
+ let mib =
+ cci_inductive env env_arities' kind nparams mie.mind_entry_finite inds
+ in
+ add_mind sp mib (set_universes (universes env_arities') env)
(*s Machines with information. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:17:52 +0000