summaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /kernel
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'kernel')
-rw-r--r--kernel/closure.ml239
-rw-r--r--kernel/closure.mli65
-rw-r--r--kernel/cooking.ml4
-rw-r--r--kernel/declarations.ml61
-rw-r--r--kernel/declarations.mli29
-rw-r--r--kernel/environ.ml6
-rw-r--r--kernel/environ.mli5
-rw-r--r--kernel/esubst.ml46
-rw-r--r--kernel/esubst.mli25
-rw-r--r--kernel/indtypes.ml222
-rw-r--r--kernel/inductive.ml575
-rw-r--r--kernel/inductive.mli46
-rw-r--r--kernel/modops.ml36
-rw-r--r--kernel/modops.mli4
-rw-r--r--kernel/names.ml6
-rw-r--r--kernel/names.mli6
-rw-r--r--kernel/pre_env.ml7
-rw-r--r--kernel/pre_env.mli5
-rw-r--r--kernel/reduction.ml66
-rw-r--r--kernel/safe_typing.ml100
-rw-r--r--kernel/safe_typing.mli14
-rw-r--r--kernel/sign.ml5
-rw-r--r--kernel/subtyping.ml9
-rw-r--r--kernel/term.ml42
-rw-r--r--kernel/term.mli10
-rw-r--r--kernel/type_errors.ml6
-rw-r--r--kernel/type_errors.mli10
-rw-r--r--kernel/typeops.ml65
-rw-r--r--kernel/typeops.mli5
-rw-r--r--kernel/univ.ml40
-rw-r--r--kernel/univ.mli17
-rw-r--r--kernel/vconv.ml7
32 files changed, 949 insertions, 834 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 8e16a922..617611bf 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: closure.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
+(* $Id: closure.ml 8802 2006-05-10 20:47:28Z barras $ *)
open Util
open Pp
@@ -394,90 +394,6 @@ let create mk_cl flgs env =
(**********************************************************************)
-(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
-
-type 'a stack_member =
- | Zapp of 'a list
- | Zcase of case_info * 'a * 'a array
- | Zfix of 'a * 'a stack
- | Zshift of int
- | Zupdate of 'a
-
-and 'a stack = 'a stack_member list
-
-let empty_stack = []
-let append_stack_list = function
- | ([],s) -> s
- | (l1, Zapp l :: s) -> Zapp (l1@l) :: s
- | (l1, s) -> Zapp l1 :: s
-let append_stack v s = append_stack_list (Array.to_list v, s)
-
-(* Collapse the shifts in the stack *)
-let zshift n s =
- match (n,s) with
- (0,_) -> s
- | (_,Zshift(k)::s) -> Zshift(n+k)::s
- | _ -> Zshift(n)::s
-
-let rec stack_args_size = function
- | Zapp l::s -> List.length l + stack_args_size s
- | Zshift(_)::s -> stack_args_size s
- | Zupdate(_)::s -> stack_args_size s
- | _ -> 0
-
-(* When used as an argument stack (only Zapp can appear) *)
-let rec decomp_stack = function
- | Zapp[v]::s -> Some (v, s)
- | Zapp(v::l)::s -> Some (v, (Zapp l :: s))
- | Zapp [] :: s -> decomp_stack s
- | _ -> None
-let rec decomp_stackn = function
- | Zapp [] :: s -> decomp_stackn s
- | Zapp l :: s -> (Array.of_list l, s)
- | _ -> assert false
-let array_of_stack s =
- let rec stackrec = function
- | [] -> []
- | Zapp args :: s -> args :: (stackrec s)
- | _ -> assert false
- in Array.of_list (List.concat (stackrec s))
-let rec list_of_stack = function
- | [] -> []
- | Zapp args :: s -> args @ (list_of_stack s)
- | _ -> assert false
-let rec app_stack = function
- | f, [] -> f
- | f, (Zapp [] :: s) -> app_stack (f, s)
- | f, (Zapp args :: s) ->
- app_stack (applist (f, args), s)
- | _ -> assert false
-let rec stack_assign s p c = match s with
- | Zapp args :: s ->
- let q = List.length args in
- if p >= q then
- Zapp args :: stack_assign s (p-q) c
- else
- (match list_chop p args with
- (bef, _::aft) -> Zapp (bef@c::aft) :: s
- | _ -> assert false)
- | _ -> s
-let rec stack_tail p s =
- if p = 0 then s else
- match s with
- | Zapp args :: s ->
- let q = List.length args in
- if p >= q then stack_tail (p-q) s
- else Zapp (list_skipn p args) :: s
- | _ -> failwith "stack_tail"
-let rec stack_nth s p = match s with
- | Zapp args :: s ->
- let q = List.length args in
- if p >= q then stack_nth s (p-q)
- else List.nth args p
- | _ -> raise Not_found
-
-
-(**********************************************************************)
(* Lazy reduction: the one used in kernel operations *)
(* type of shared terms. fconstr and frterm are mutually recursive.
@@ -543,6 +459,81 @@ let update v1 (no,t) =
v1)
else {norm=no;term=t}
+(**********************************************************************)
+(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
+
+type stack_member =
+ | Zapp of fconstr array
+ | Zcase of case_info * fconstr * fconstr array
+ | Zfix of fconstr * stack
+ | Zshift of int
+ | Zupdate of fconstr
+
+and stack = stack_member list
+
+let empty_stack = []
+let append_stack v s =
+ if Array.length v = 0 then s else
+ match s with
+ | Zapp l :: s -> Zapp (Array.append v l) :: s
+ | _ -> Zapp v :: s
+
+(* Collapse the shifts in the stack *)
+let zshift n s =
+ match (n,s) with
+ (0,_) -> s
+ | (_,Zshift(k)::s) -> Zshift(n+k)::s
+ | _ -> Zshift(n)::s
+
+let rec stack_args_size = function
+ | Zapp v :: s -> Array.length v + stack_args_size s
+ | Zshift(_)::s -> stack_args_size s
+ | Zupdate(_)::s -> stack_args_size s
+ | _ -> 0
+
+(* When used as an argument stack (only Zapp can appear) *)
+let rec decomp_stack = function
+ | Zapp v :: s ->
+ (match Array.length v with
+ 0 -> decomp_stack s
+ | 1 -> Some (v.(0), s)
+ | _ ->
+ Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s)))
+ | _ -> None
+let rec decomp_stackn = function
+ | Zapp v :: s -> if Array.length v = 0 then decomp_stackn s else (v, s)
+ | _ -> assert false
+let array_of_stack s =
+ let rec stackrec = function
+ | [] -> []
+ | Zapp args :: s -> args :: (stackrec s)
+ | _ -> assert false
+ in Array.concat (stackrec s)
+let rec stack_assign s p c = match s with
+ | Zapp args :: s ->
+ let q = Array.length args in
+ if p >= q then
+ Zapp args :: stack_assign s (p-q) c
+ else
+ (let nargs = Array.copy args in
+ nargs.(p) <- c;
+ Zapp nargs :: s)
+ | _ -> s
+let rec stack_tail p s =
+ if p = 0 then s else
+ match s with
+ | Zapp args :: s ->
+ let q = Array.length args in
+ if p >= q then stack_tail (p-q) s
+ else Zapp (Array.sub args p (q-p)) :: s
+ | _ -> failwith "stack_tail"
+let rec stack_nth s p = match s with
+ | Zapp args :: s ->
+ let q = Array.length args in
+ if p >= q then stack_nth s (p-q)
+ else args.(p)
+ | _ -> raise Not_found
+
(* Lifting. Preserves sharing (useful only for cell with norm=Red).
lft_fconstr always create a new cell, while lift_fconstr avoids it
when the lift is 0. *)
@@ -554,7 +545,7 @@ let rec lft_fconstr n ft =
| FFix(fx,e) -> {norm=Cstr; term=FFix(fx,subs_shft(n,e))}
| FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))}
| FLIFT(k,m) -> lft_fconstr (n+k) m
- | FLOCKED -> anomaly "lft_constr found locked term"
+ | FLOCKED -> assert false
| _ -> {norm=ft.norm; term=FLIFT(n,ft)}
let lift_fconstr k f =
if k=0 then f else lft_fconstr k f
@@ -568,7 +559,7 @@ let clos_rel e i =
| Inl(n,mt) -> lift_fconstr n mt
| Inr(k,None) -> {norm=Norm; term= FRel k}
| Inr(k,Some p) ->
- lift_fconstr (k-p) {norm=Norm;term=FFlex(RelKey p)}
+ lift_fconstr (k-p) {norm=Red;term=FFlex(RelKey p)}
(* since the head may be reducible, we might introduce lifts of 0 *)
let compact_stack head stk =
@@ -654,9 +645,9 @@ and compact_v acc s v k i =
let optimise_closure env c =
if is_subs_id env then (env,c) else
let (c',(_,s)) = compact_constr (0,[]) c 1 in
- let env' = List.fold_left
- (fun subs i -> subs_cons (clos_rel env i, subs)) (ESID 0) s in
- (env',c')
+ let env' =
+ Array.map (fun i -> clos_rel env i) (Array.of_list s) in
+ (subs_cons (env', ESID 0),c')
let mk_lambda env t =
let (env,t) = optimise_closure env t in
@@ -772,8 +763,7 @@ let rec to_constr constr_fun lfts v =
let fr = mk_clos2 env t in
let unfv = update v (fr.norm,fr.term) in
to_constr constr_fun lfts unfv
- | FLOCKED -> (*anomaly "Closure.to_constr: found locked term"*)
-mkVar(id_of_string"_LOCK_")
+ | FLOCKED -> assert false (*mkVar(id_of_string"_LOCK_")*)
(* This function defines the correspondance between constr and
fconstr. When we find a closure whose substitution is the identity,
@@ -802,14 +792,12 @@ let rec fstrong unfreeze_fun lfts v =
let rec zip m stk =
match stk with
| [] -> m
- | Zapp args :: s ->
- let args = Array.of_list args in
- zip {norm=neutr m.norm; term=FApp(m, args)} s
+ | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s
| Zcase(ci,p,br)::s ->
let t = FCases(ci, p, m, br) in
zip {norm=neutr m.norm; term=t} s
| Zfix(fx,par)::s ->
- zip fx (par @ append_stack_list ([m], s))
+ zip fx (par @ append_stack [|m|] s)
| Zshift(n)::s ->
zip (lift_fconstr n m) s
| Zupdate(rf)::s ->
@@ -842,31 +830,30 @@ let strip_update_shift_app head stk =
strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s
| (Zapp args :: s) ->
strip_rec (Zapp args :: rstk)
- {norm=h.norm;term=FApp(h,Array.of_list args)} depth s
+ {norm=h.norm;term=FApp(h,args)} depth s
| Zupdate(m)::s ->
strip_rec rstk (update m (h.norm,h.term)) depth s
| stk -> (depth,List.rev rstk, stk) in
strip_rec [] head 0 stk
-let rec get_nth_arg head n stk =
+let get_nth_arg head n stk =
assert (head.norm <> Red);
let rec strip_rec rstk h depth n = function
| Zshift(k) as e :: s ->
strip_rec (e::rstk) (lift_fconstr k h) (depth+k) n s
| Zapp args::s' ->
- let q = List.length args in
+ let q = Array.length args in
if n >= q
then
strip_rec (Zapp args::rstk)
- {norm=h.norm;term=FApp(h,Array.of_list args)} depth (n-q) s'
+ {norm=h.norm;term=FApp(h,args)} depth (n-q) s'
else
- (match list_chop n args with
- (bef, v::aft) ->
- let stk' =
- List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in
- (Some (stk', v), append_stack_list (aft,s'))
- | _ -> assert false)
+ let bef = Array.sub args 0 n in
+ let aft = Array.sub args (n+1) (q-n-1) in
+ let stk' =
+ List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in
+ (Some (stk', args.(n)), append_stack aft s')
| Zupdate(m)::s ->
strip_rec rstk (update m (h.norm,h.term)) depth n s
| s -> (None, List.rev rstk @ s) in
@@ -888,18 +875,15 @@ let rec get_args n tys f e stk =
| Zshift k :: s ->
get_args n tys f (subs_shft (k,e)) s
| Zapp l :: s ->
- let na = List.length l in
- if n == na then
- let e' = List.fold_left (fun e arg -> subs_cons(arg,e)) e l in
- (Inl e',s)
+ let na = Array.length l in
+ if n == na then (Inl (subs_cons(l,e)),s)
else if n < na then (* more arguments *)
- let (args,eargs) = list_chop n l in
- let e' = List.fold_left (fun e arg -> subs_cons(arg,e)) e args in
- (Inl e', Zapp eargs :: s)
+ let args = Array.sub l 0 n in
+ let eargs = Array.sub l n (na-n) in
+ (Inl (subs_cons(args,e)), Zapp eargs :: s)
else (* more lambdas *)
- let (_,etys) = list_chop na tys in
- let e' = List.fold_left (fun e arg -> subs_cons(arg,e)) e l in
- get_args (n-na) etys f e' s
+ let etys = list_skipn na tys in
+ get_args (n-na) etys f (subs_cons(l,e)) s
| _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
@@ -908,7 +892,7 @@ let rec get_args n tys f e stk =
let rec reloc_rargs_rec depth stk =
match stk with
Zapp args :: s ->
- Zapp (lift_fconstr_list depth args) :: reloc_rargs_rec depth s
+ Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s
| Zshift(k)::s -> if k=depth then s else reloc_rargs_rec (depth-k) s
| _ -> stk
@@ -918,12 +902,12 @@ let reloc_rargs depth stk =
let rec drop_parameters depth n stk =
match stk with
Zapp args::s ->
- let q = List.length args in
+ let q = Array.length args in
if n > q then drop_parameters depth (n-q) s
else if n = q then reloc_rargs depth s
else
- let aft = list_skipn n args in
- reloc_rargs depth (append_stack_list (aft,s))
+ let aft = Array.sub args n (q-n) in
+ reloc_rargs depth (append_stack aft s)
| Zshift(k)::s -> drop_parameters (depth-k) n s
| [] -> assert (n=0); []
| _ -> assert false (* we know that n < stack_args_size(stk) *)
@@ -949,15 +933,9 @@ let contract_fix_vect fix =
(bds.(i),
(fun j -> { norm = Cstr; term = FCoFix ((j,rdcl),env) }),
env, Array.length bds)
- | _ -> anomaly "Closure.contract_fix_vect: not a (co)fixpoint"
+ | _ -> assert false
in
- let rec subst_bodies_from_i i env =
- if i = nfix then
- (env, thisbody)
- else
- subst_bodies_from_i (i+1) (subs_cons (make_body i, env))
- in
- subst_bodies_from_i 0 env
+ (subs_cons(Array.init nfix make_body, env), thisbody)
(*********************************************************************)
@@ -969,7 +947,7 @@ let rec knh m stk =
match m.term with
| FLIFT(k,a) -> knh a (zshift k stk)
| FCLOS(t,e) -> knht e t (zupdate m stk)
- | FLOCKED -> anomaly "Closure.knh: found lock"
+ | FLOCKED -> assert false
| FApp(a,b) -> knh a (append_stack b (zupdate m stk))
| FCases(ci,p,t,br) -> knh t (Zcase(ci,p,br)::zupdate m stk)
| FFix(((ri,n),(_,_,_)),_) ->
@@ -1037,7 +1015,7 @@ let rec knr info m stk =
knit info fxe fxbd (args@stk')
| (_,args,s) -> (m,args@s))
| FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
- knit info (subs_cons(v,e)) bd stk
+ knit info (subs_cons([|v|],e)) bd stk
| _ -> (m,stk)
(* Computes the weak head normal form of a term *)
@@ -1056,7 +1034,6 @@ let rec zip_term zfun m stk =
match stk with
| [] -> m
| Zapp args :: s ->
- let args = Array.of_list args in
zip_term zfun (mkApp(m, Array.map zfun args)) s
| Zcase(ci,p,br)::s ->
let t = mkCase(ci, zfun p, m, Array.map zfun br) in
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 706a089e..feec8395 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: closure.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: closure.mli 8793 2006-05-05 17:41:41Z barras $ i*)
(*i*)
open Pp
@@ -91,33 +91,6 @@ val info_flags: 'a infos -> reds
val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
(************************************************************************)
-(*s A [stack] is a context of arguments, arguments are pushed by
- [append_stack] one array at a time but popped with [decomp_stack]
- one by one *)
-
-type 'a stack_member =
- | Zapp of 'a list
- | Zcase of case_info * 'a * 'a array
- | Zfix of 'a * 'a stack
- | Zshift of int
- | Zupdate of 'a
-
-and 'a stack = 'a stack_member list
-
-val empty_stack : 'a stack
-val append_stack : 'a array -> 'a stack -> 'a stack
-
-val decomp_stack : 'a stack -> ('a * 'a stack) option
-val list_of_stack : 'a stack -> 'a list
-val array_of_stack : 'a stack -> 'a array
-val stack_assign : 'a stack -> int -> 'a -> 'a stack
-val stack_args_size : 'a stack -> int
-val app_stack : constr * constr stack -> constr
-val stack_tail : int -> 'a stack -> 'a stack
-val stack_nth : 'a stack -> int -> 'a
-val zip_term : ('a -> constr) -> constr -> 'a stack -> constr
-
-(************************************************************************)
(*s Lazy reduction. *)
(* [fconstr] is the type of frozen constr *)
@@ -146,17 +119,43 @@ type fterm =
| FCLOS of constr * fconstr subs
| FLOCKED
+(************************************************************************)
+(*s A [stack] is a context of arguments, arguments are pushed by
+ [append_stack] one array at a time but popped with [decomp_stack]
+ one by one *)
+
+type stack_member =
+ | Zapp of fconstr array
+ | Zcase of case_info * fconstr * fconstr array
+ | Zfix of fconstr * stack
+ | Zshift of int
+ | Zupdate of fconstr
+
+and stack = stack_member list
+
+val empty_stack : stack
+val append_stack : fconstr array -> stack -> stack
+
+val decomp_stack : stack -> (fconstr * stack) option
+val array_of_stack : stack -> fconstr array
+val stack_assign : stack -> int -> fconstr -> stack
+val stack_args_size : stack -> int
+val stack_tail : int -> stack -> stack
+val stack_nth : stack -> int -> fconstr
+val zip_term : (fconstr -> constr) -> constr -> stack -> constr
+
(* To lazy reduce a constr, create a [clos_infos] with
[create_clos_infos], inject the term to reduce with [inject]; then use
a reduction function *)
val inject : constr -> fconstr
+(* mk_atom: prevents a term from being evaluated *)
+val mk_atom : constr -> fconstr
+
val fterm_of : fconstr -> fterm
val term_of_fconstr : fconstr -> constr
val destFLambda :
(fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr
-(* mk_atom: prevents a term from being evaluated *)
-val mk_atom : constr -> fconstr
(* Global and local constant cache *)
type clos_infos
@@ -173,7 +172,7 @@ val whd_val : clos_infos -> fconstr -> constr
(* [whd_stack] performs weak head normalization in a given stack. It
stops whenever a reduction is blocked. *)
val whd_stack :
- clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
+ clos_infos -> fconstr -> stack -> fconstr * stack
(* Conversion auxiliary functions to do step by step normalisation *)
@@ -195,8 +194,8 @@ val mk_clos_deep :
(fconstr subs -> constr -> fconstr) ->
fconstr subs -> constr -> fconstr
-val kni: clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
-val knr: clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
+val kni: clos_infos -> fconstr -> stack -> fconstr * stack
+val knr: clos_infos -> fconstr -> stack -> fconstr * stack
val kl : clos_infos -> fconstr -> constr
val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index a6aa2a8e..58c21d9f 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: cooking.ml 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id: cooking.ml 8752 2006-04-27 19:37:33Z herbelin $ i*)
open Pp
open Util
@@ -113,7 +113,7 @@ type recipe = {
d_modlist : work_list }
let on_body f =
- option_app (fun c -> Declarations.from_val (f (Declarations.force c)))
+ option_map (fun c -> Declarations.from_val (f (Declarations.force c)))
let cook_constant env r =
let cb = r.d_from in
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 33d9959c..c52b5c48 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declarations.ml 8653 2006-03-22 09:41:17Z herbelin $ i*)
+(*i $Id: declarations.ml 8845 2006-05-23 07:41:58Z herbelin $ i*)
(*i*)
open Util
@@ -45,6 +45,13 @@ type constant_body = {
(*s Inductive types (internal representation with redundant
information). *)
+let subst_rel_declaration sub (id,copt,t as x) =
+ let copt' = option_smartmap (subst_mps sub) copt in
+ let t' = subst_mps sub t in
+ if copt == copt' & t == t' then x else (id,copt',t')
+
+let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
+
type recarg =
| Norec
| Mrec of int
@@ -83,6 +90,20 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
*)
+type polymorphic_inductive_arity = {
+ mind_param_levels : universe option list;
+ mind_level : universe;
+}
+
+type monomorphic_inductive_arity = {
+ mind_user_arity : constr;
+ mind_sort : sorts;
+}
+
+type inductive_arity =
+| Monomorphic of monomorphic_inductive_arity
+| Polymorphic of polymorphic_inductive_arity
+
type one_inductive_body = {
(* Primitive datas *)
@@ -90,8 +111,11 @@ type one_inductive_body = {
(* Name of the type: [Ii] *)
mind_typename : identifier;
- (* Arity of [Ii] with parameters: [forall params, Ui] *)
- mind_user_arity : types;
+ (* Arity context of [Ii] with parameters: [forall params, Ui] *)
+ mind_arity_ctxt : rel_context;
+
+ (* Arity sort, original user arity, and allowed elim sorts, if monomorphic *)
+ mind_arity : inductive_arity;
(* Names of the constructors: [cij] *)
mind_consnames : identifier array;
@@ -103,15 +127,9 @@ type one_inductive_body = {
(* Derived datas *)
- (* Head normalized arity so that the conclusion is a sort *)
- mind_nf_arity : types;
-
(* Number of expected real arguments of the type (no let, no params) *)
mind_nrealargs : int;
- (* Conclusion of the arity *)
- mind_sort : sorts;
-
(* List of allowed elimination sorts *)
mind_kelim : sorts_family list;
@@ -171,24 +189,29 @@ type mutual_inductive_body = {
(* TODO: should be changed to non-coping after Term.subst_mps *)
let subst_const_body sub cb = {
const_hyps = (assert (cb.const_hyps=[]); []);
- const_body = option_app (subst_constr_subst sub) cb.const_body;
- const_type = type_app (subst_mps sub) cb.const_type;
+ const_body = option_map (subst_constr_subst sub) cb.const_body;
+ const_type = subst_mps sub cb.const_type;
const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
(*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*)
const_constraints = cb.const_constraints;
const_opaque = cb.const_opaque }
+let subst_arity sub = function
+| Monomorphic s ->
+ Monomorphic {
+ mind_user_arity = subst_mps sub s.mind_user_arity;
+ mind_sort = s.mind_sort;
+ }
+| Polymorphic s as x -> x
+
let subst_mind_packet sub mbp =
{ mind_consnames = mbp.mind_consnames;
mind_consnrealdecls = mbp.mind_consnrealdecls;
mind_typename = mbp.mind_typename;
- mind_nf_lc =
- array_smartmap (type_app (subst_mps sub)) mbp.mind_nf_lc;
- mind_nf_arity = type_app (subst_mps sub) mbp.mind_nf_arity;
- mind_user_lc =
- array_smartmap (type_app (subst_mps sub)) mbp.mind_user_lc;
- mind_user_arity = type_app (subst_mps sub) mbp.mind_user_arity;
- mind_sort = mbp.mind_sort;
+ mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc;
+ mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
+ mind_arity = subst_arity sub mbp.mind_arity;
+ mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc;
mind_nrealargs = mbp.mind_nrealargs;
mind_kelim = mbp.mind_kelim;
mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
@@ -208,7 +231,7 @@ let subst_mind sub mib =
map_rel_context (subst_mps sub) mib.mind_params_ctxt;
mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
mind_constraints = mib.mind_constraints ;
- mind_equiv = option_app (subst_kn sub) mib.mind_equiv }
+ mind_equiv = option_map (subst_kn sub) mib.mind_equiv }
(*s Modules: signature component specifications, module types, and
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 7ad953e5..c96d2131 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declarations.mli 8653 2006-03-22 09:41:17Z herbelin $ i*)
+(*i $Id: declarations.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
(*i*)
open Names
@@ -70,6 +70,20 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
\end{verbatim}
*)
+type polymorphic_inductive_arity = {
+ mind_param_levels : universe option list;
+ mind_level : universe;
+}
+
+type monomorphic_inductive_arity = {
+ mind_user_arity : constr;
+ mind_sort : sorts;
+}
+
+type inductive_arity =
+| Monomorphic of monomorphic_inductive_arity
+| Polymorphic of polymorphic_inductive_arity
+
type one_inductive_body = {
(* Primitive datas *)
@@ -77,8 +91,11 @@ type one_inductive_body = {
(* Name of the type: [Ii] *)
mind_typename : identifier;
- (* Arity of [Ii] with parameters: [forall params, Ui] *)
- mind_user_arity : types;
+ (* Arity context of [Ii] with parameters: [forall params, Ui] *)
+ mind_arity_ctxt : rel_context;
+
+ (* Arity sort and original user arity if monomorphic *)
+ mind_arity : inductive_arity;
(* Names of the constructors: [cij] *)
mind_consnames : identifier array;
@@ -90,15 +107,9 @@ type one_inductive_body = {
(* Derived datas *)
- (* Head normalized arity so that the conclusion is a sort *)
- mind_nf_arity : types;
-
(* Number of expected real arguments of the type (no let, no params) *)
mind_nrealargs : int;
- (* Conclusion of the arity *)
- mind_sort : sorts;
-
(* List of allowed elimination sorts *)
mind_kelim : sorts_family list;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 77d77118..a1e19815 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: environ.ml 7830 2006-01-10 22:45:28Z herbelin $ *)
+(* $Id: environ.ml 8810 2006-05-12 18:50:21Z barras $ *)
open Util
open Names
@@ -91,7 +91,7 @@ let named_context_of_val = fst
*** /!\ *** [f t] should be convertible with t *)
let map_named_val f (ctxt,ctxtv) =
let ctxt =
- List.map (fun (id,body,typ) -> (id, option_app f body, f typ)) ctxt in
+ List.map (fun (id,body,typ) -> (id, option_map f body, f typ)) ctxt in
(ctxt,ctxtv)
let empty_named_context = empty_named_context
@@ -186,6 +186,8 @@ let evaluable_constant cst env =
(* Mutual Inductives *)
let lookup_mind = lookup_mind
+let scrape_mind = scrape_mind
+
let add_mind kn mib env =
let new_inds = KNmap.add kn mib env.env_globals.env_inductives in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 701159da..cfc23651 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: environ.mli 7640 2005-12-05 10:16:24Z gregoire $ i*)
+(*i $Id: environ.mli 8810 2006-05-12 18:50:21Z barras $ i*)
(*i*)
open Names
@@ -140,6 +140,9 @@ val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env
(* raises [Not_found] if the required path is not found *)
val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
+(* Find the ultimate inductive in the [mind_equiv] chain *)
+val scrape_mind : env -> mutual_inductive -> mutual_inductive
+
(************************************************************************)
(*s Modules *)
val add_modtype : kernel_name -> module_type_body -> env -> env
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 0a3f4578..e32fc963 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: esubst.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: esubst.ml 8799 2006-05-09 21:15:07Z barras $ *)
open Util
@@ -55,7 +55,10 @@ let rec is_lift_id = function
(* (bounded) explicit substitutions of type 'a *)
type 'a subs =
| ESID of int (* ESID(n) = %n END bounded identity *)
- | CONS of 'a * 'a subs (* CONS(t,S) = (S.t) parallel substitution *)
+ | CONS of 'a array * 'a subs
+ (* CONS([|t1..tn|],S) =
+ (S.t1...tn) parallel substitution
+ beware of the order *)
| SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *)
(* with n vars *)
| LIFT of int * 'a subs (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
@@ -64,7 +67,7 @@ type 'a subs =
* Needn't be recursive if we always use these functions
*)
-let subs_cons(x,s) = CONS(x,s)
+let subs_cons(x,s) = if Array.length x = 0 then s else CONS(x,s)
let subs_liftn n = function
| ESID p -> ESID (p+n) (* bounded identity lifted extends by p *)
@@ -85,11 +88,12 @@ let subs_shift_cons = function
| (k, SHIFT(n,s1), t) -> CONS(t,SHIFT(k+n, s1))
| (k, s, t) -> CONS(t,SHIFT(k, s));;
-(* Tests whether a substitution is extensionnaly equal to the identity *)
+(* Tests whether a substitution is equal to the identity *)
let rec is_subs_id = function
ESID _ -> true
| LIFT(_,s) -> is_subs_id s
| SHIFT(0,s) -> is_subs_id s
+ | CONS(x,s) -> Array.length x = 0 && is_subs_id s
| _ -> false
(* Expands de Bruijn k in the explicit substitution subs
@@ -108,14 +112,15 @@ let rec is_subs_id = function
* variable points k bindings beyond subs.
*)
let rec exp_rel lams k subs =
- match (k,subs) with
- | (1, CONS (def,_)) -> Inl(lams,def)
- | (_, CONS (_,l)) -> exp_rel lams (pred k) l
- | (_, LIFT (n,_)) when k<=n -> Inr(lams+k,None)
- | (_, LIFT (n,l)) -> exp_rel (n+lams) (k-n) l
- | (_, SHIFT (n,s)) -> exp_rel (n+lams) k s
- | (_, ESID n) when k<=n -> Inr(lams+k,None)
- | (_, ESID n) -> Inr(lams+k,Some (k-n))
+ match subs with
+ | CONS (def,_) when k <= Array.length def
+ -> Inl(lams,def.(Array.length def - k))
+ | CONS (v,l) -> exp_rel lams (k - Array.length v) l
+ | LIFT (n,_) when k<=n -> Inr(lams+k,None)
+ | LIFT (n,l) -> exp_rel (n+lams) (k-n) l
+ | SHIFT (n,s) -> exp_rel (n+lams) k s
+ | ESID n when k<=n -> Inr(lams+k,None)
+ | ESID n -> Inr(lams+k,Some (k-n))
let expand_rel k subs = exp_rel 0 k subs
@@ -124,9 +129,20 @@ let rec comp mk_cl s1 s2 =
| _, ESID _ -> s1
| ESID _, _ -> s2
| SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2)
- | _, CONS(x,s') -> CONS(mk_cl(s1,x), comp mk_cl s1 s')
- | CONS(x,s), SHIFT(k,s') -> comp mk_cl s (subs_shft(k-1, s'))
- | CONS(x,s), LIFT(k,s') -> CONS(x,comp mk_cl s (subs_liftn (k-1) s'))
+ | _, CONS(x,s') ->
+ CONS(Array.map (fun t -> mk_cl(s1,t)) x, comp mk_cl s1 s')
+ | CONS(x,s), SHIFT(k,s') ->
+ let lg = Array.length x in
+ if k == lg then comp mk_cl s s'
+ else if k > lg then comp mk_cl s (SHIFT(k-lg, s'))
+ else comp mk_cl (CONS(Array.sub x 0 (lg-k), s)) s'
+ | CONS(x,s), LIFT(k,s') ->
+ let lg = Array.length x in
+ if k == lg then CONS(x, comp mk_cl s s')
+ else if k > lg then CONS(x, comp mk_cl s (LIFT(k-lg, s')))
+ else
+ CONS(Array.sub x (lg-k) k,
+ comp mk_cl (CONS(Array.sub x 0 (lg-k),s)) s')
| LIFT(k,s), SHIFT(k',s') ->
if k<k'
then subs_shft(k, comp mk_cl s (subs_shft(k'-k, s')))
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index 39fbbede..3b40bdfc 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: esubst.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
+(*i $Id: esubst.mli 8799 2006-05-09 21:15:07Z barras $ i*)
(*s Compact representation of explicit relocations. \\
[ELSHFT(l,n)] == lift of [n], then apply [lift l].
@@ -22,21 +22,22 @@ val el_lift : lift -> lift
val reloc_rel : int -> lift -> int
val is_lift_id : lift -> bool
-(*s Explicit substitutions of type ['a]. [ESID n] = %n~END = bounded identity.
- [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] =
- $(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars.
- [LIFT(n,S)] = $(\%n~S)$ stands for $((\uparrow n~o~S).n...1)$. *)
+(*s Explicit substitutions of type ['a]. *)
type 'a subs =
- | ESID of int
- | CONS of 'a * 'a subs
- | SHIFT of int * 'a subs
- | LIFT of int * 'a subs
+ | ESID of int (* ESID(n) = %n END bounded identity *)
+ | CONS of 'a array * 'a subs
+ (* CONS([|t1..tn|],S) =
+ (S.t1...tn) parallel substitution
+ beware of the order *)
+ | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *)
+ (* with n vars *)
+ | LIFT of int * 'a subs (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
-val subs_cons: 'a * 'a subs -> 'a subs
+val subs_cons: 'a array * 'a subs -> 'a subs
val subs_shft: int * 'a subs -> 'a subs
val subs_lift: 'a subs -> 'a subs
val subs_liftn: int -> 'a subs -> 'a subs
-val subs_shift_cons: int * 'a subs * 'a -> 'a subs
+val subs_shift_cons: int * 'a subs * 'a array -> 'a subs
val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union
val is_subs_id: 'a subs -> bool
-val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs \ No newline at end of file
+val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a3fc0db4..e7dc09ee 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: indtypes.ml 8653 2006-03-22 09:41:17Z herbelin $ *)
+(* $Id: indtypes.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
open Util
open Names
@@ -116,12 +116,10 @@ let is_info_type env t =
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
(* An inductive definition is a "unit" if it has only one constructor
and that all arguments expected by this constructor are
- logical, this is the case for equality, conjonction of logical properties
+ logical, this is the case for equality, conjunction of logical properties
*)
let is_unit constrsinfos =
match constrsinfos with (* One info = One constructor *)
@@ -145,45 +143,54 @@ let small_unit constrsinfos =
and isunit = is_unit constrsinfos in
issmall, isunit
-(* This (re)computes informations relevant to extraction and the sort of an
- arity or type constructor; we do not to recompute universes constraints *)
+(* Computing the levels of polymorphic inductive types
-(* [smax] is the max of the sorts of the products of the constructor type *)
+ For each inductive type of a block that is of level u_i, we have
+ the constraints that u_i >= v_i where v_i is the type level of the
+ types of the constructors of this inductive type. Each v_i depends
+ of some of the u_i and of an extra (maybe non variable) universe,
+ say w_i that summarize all the other constraints. Typically, for
+ three inductive types, we could have
-let enforce_type_constructor env arsort smax cst =
- match smax, arsort with
- | Type uc, Type ua -> enforce_geq ua uc cst
- | Type uc, Prop Pos when engagement env <> Some ImpredicativeSet ->
- error "Large non-propositional inductive types must be in Type"
- | _,_ -> cst
+ u1,u2,u3,w1 <= u1
+ u1 w2 <= u2
+ u2,u3,w3 <= u3
-let type_one_constructor env_ar_par params arsort c =
- let infos = infos_and_sort env_ar_par c in
+ From this system of inequations, we shall deduce
- (* Each constructor is typed-checked here *)
- let (j,cst) = infer_type env_ar_par c in
- let full_cstr_type = it_mkProd_or_LetIn j.utj_val params in
+ w1,w2,w3 <= u1
+ w1,w2 <= u2
+ w1,w2,w3 <= u3
+*)
- (* If the arity is at some level Type arsort, then the sort of the
- constructor must be below arsort; here we consider constructors with the
- global parameters (which add a priori more constraints on their sort) *)
- let cst2 = enforce_type_constructor env_ar_par arsort j.utj_type cst in
+let inductive_levels arities inds =
+ let levels = Array.map pi3 arities in
+ let cstrs_levels = Array.map (fun (_,_,_,_,lev) -> lev) inds in
+ (* Take the transitive closure of the system of constructors *)
+ (* level constraints and remove the recursive dependencies *)
+ solve_constraints_system levels cstrs_levels
- (infos, full_cstr_type, cst2)
+(* This (re)computes informations relevant to extraction and the sort of an
+ arity or type constructor; we do not to recompute universes constraints *)
-let infer_constructor_packet env_ar params arsort lc =
+let constraint_list_union =
+ List.fold_left Constraint.union Constraint.empty
+
+let infer_constructor_packet env_ar params lc =
+ (* builds the typing context "Gamma, I1:A1, ... In:An, params" *)
let env_ar_par = push_rel_context params env_ar in
- let (constrsinfos,jlc,cst) =
- List.fold_right
- (fun c (infosl,l,cst) ->
- let (infos,ct,cst') =
- type_one_constructor env_ar_par params arsort c in
- (infos::infosl,ct::l, Constraint.union cst cst'))
- lc
- ([],[],Constraint.empty) in
- let lc' = Array.of_list jlc in
- let issmall,isunit = small_unit constrsinfos in
- (issmall,isunit,lc',cst)
+ (* type-check the constructors *)
+ let jlc,cstl = List.split (List.map (infer_type env_ar_par) lc) in
+ let cst = constraint_list_union cstl in
+ let jlc = Array.of_list jlc in
+ (* generalize the constructor over the parameters *)
+ let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in
+ (* compute the max of the sorts of the products of the constructor type *)
+ let level = max_inductive_sort (Array.map (fun j -> j.utj_type) jlc) in
+ (* compute *)
+ let info = small_unit (List.map (infos_and_sort env_ar_par) lc) in
+
+ (info,lc'',level,cst)
(* Type-check an inductive definition. Does not check positivity
conditions. *)
@@ -192,50 +199,82 @@ let typecheck_inductive env mie =
(* Check unicity of names *)
mind_check_names mie;
mind_check_arities env mie;
- (* Params are typed-checked here *)
- let params = mie.mind_entry_params in
- let env_params, params, cstp = infer_local_decls env params in
+ (* Params are typed-checked here *)
+ let env_params, params, cst1 = infer_local_decls env mie.mind_entry_params in
(* We first type arity of each inductive definition *)
(* This allows to build the environment of arities and to share *)
(* the set of constraints *)
- let cst, arities, rev_params_arity_list =
+ let cst, env_arities, rev_arity_list =
List.fold_left
- (fun (cst,arities,l) ind ->
+ (fun (cst,env_ar,l) ind ->
(* Arities (without params) are typed-checked here *)
- let arity, cst2 =
- infer_type env_params ind.mind_entry_arity in
+ let arity, cst2 = infer_type env_params ind.mind_entry_arity in
(* We do not need to generate the universe of full_arity; if
later, after the validation of the inductive definition,
full_arity is used as argument or subject to cast, an
upper universe will be generated *)
- let id = ind.mind_entry_typename in
let full_arity = it_mkProd_or_LetIn arity.utj_val params in
- Constraint.union cst cst2,
- Sign.add_rel_decl (Name id, None, full_arity) arities,
- (params, id, full_arity, arity.utj_val)::l)
- (cstp,empty_rel_context,[])
+ let cst = Constraint.union cst cst2 in
+ let id = ind.mind_entry_typename in
+ let env_ar' = push_rel (Name id, None, full_arity) env_ar in
+ let lev =
+ (* Decide that if the conclusion is not explicitly Type *)
+ (* then the inductive type is not polymorphic *)
+ match kind_of_term (snd (decompose_prod_assum arity.utj_val)) with
+ | Sort (Type u) -> Some u
+ | _ -> None in
+ (cst,env_ar',(id,full_arity,lev)::l))
+ (cst1,env,[])
mie.mind_entry_inds in
- let env_arities = push_rel_context arities env in
-
- let params_arity_list = List.rev rev_params_arity_list in
+ let arity_list = List.rev rev_arity_list in
(* Now, we type the constructors (without params) *)
let inds,cst =
List.fold_right2
- (fun ind (params,id,full_arity,short_arity) (inds,cst) ->
- let (_,arsort) = dest_arity env full_arity in
- let lc = ind.mind_entry_lc in
- let (issmall,isunit,lc',cst') =
- infer_constructor_packet env_arities params arsort lc in
+ (fun ind arity_data (inds,cst) ->
+ let (info,lc',cstrs_univ,cst') =
+ infer_constructor_packet env_arities params ind.mind_entry_lc in
let consnames = ind.mind_entry_consnames in
- let ind' = (id,full_arity,consnames,issmall,isunit,lc')
- in
+ let ind' = (arity_data,consnames,info,lc',cstrs_univ) in
(ind'::inds, Constraint.union cst cst'))
mie.mind_entry_inds
- params_arity_list
+ arity_list
([],cst) in
- (env_arities, params, Array.of_list inds, cst)
+
+ let inds = Array.of_list inds in
+ let arities = Array.of_list arity_list in
+ let param_ccls = List.fold_left (fun l (_,b,p) ->
+ if b = None then
+ let _,c = dest_prod_assum env p in
+ let u = match kind_of_term c with Sort (Type u) -> Some u | _ -> None in
+ u::l
+ else
+ l) [] params in
+
+ (* Compute/check the sorts of the inductive types *)
+ let ind_min_levels = inductive_levels arities inds in
+ let inds, cst =
+ array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst ->
+ let sign, s = dest_arity env full_arity in
+ let status,cst = match s with
+ | Type _ when ar_level <> None (* Explicitly polymorphic *) ->
+ (* The polymorphic level is a function of the level of the *)
+ (* conclusions of the parameters *)
+ Inr (param_ccls, lev), cst
+ | Type u (* Not an explicit occurrence of Type *) ->
+ Inl (info,full_arity,s), enforce_geq u lev cst
+ | Prop Pos when engagement env <> Some ImpredicativeSet ->
+ (* Predicative set: check that the content is indeed predicative *)
+ if not (is_empty_univ lev) & not (is_base_univ lev) then
+ error "Large non-propositional inductive types must be in Type";
+ Inl (info,full_arity,s), cst
+ | Prop _ ->
+ Inl (info,full_arity,s), cst in
+ (id,cn,lc,(sign,status)),cst)
+ inds ind_min_levels cst in
+
+ (env_arities, params, inds, cst)
(************************************************************************)
(************************************************************************)
@@ -479,7 +518,7 @@ let check_positivity env_ar params inds =
List.rev (list_tabulate (fun j -> (Mrec j, Rtree.mk_param j)) ntypes) in
let lparams = rel_context_length params in
let nmr = rel_context_nhyps params in
- let check_one i (_,_,_,_,_,lc) =
+ let check_one i (_,_,lc,_) =
let ra_env =
list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
@@ -505,22 +544,34 @@ let is_recursive = Rtree.is_infinite
array_exists one_is_rec
*)
+(* Allowed eliminations *)
+
let all_sorts = [InProp;InSet;InType]
-let impredicative_sorts = [InProp;InSet]
+let small_sorts = [InProp;InSet]
let logical_sorts = [InProp]
-let allowed_sorts env issmall isunit = function
- | Type _ -> all_sorts
- | Prop Pos ->
- if issmall then all_sorts
- else impredicative_sorts
- | Prop Null ->
-(* 29/1/02: added InType which is derivable when the type is unit and small *)
- if isunit then all_sorts
- else logical_sorts
+let allowed_sorts issmall isunit s =
+ match family_of_sort s with
+ (* Type: all elimination allowed *)
+ | InType -> all_sorts
+
+ (* Small Set is predicative: all elimination allowed *)
+ | InSet when issmall -> all_sorts
+
+ (* Large Set is necessarily impredicative: forbids large elimination *)
+ | InSet -> small_sorts
+
+ (* Unitary/empty Prop: elimination to all sorts are realizable *)
+ (* unless the type is large. If it is large, forbids large elimination *)
+ (* which otherwise allows to simulate the inconsistent system Type:Type *)
+ | InProp when isunit -> if issmall then all_sorts else small_sorts
+
+ (* Other propositions: elimination only to Prop *)
+ | InProp -> logical_sorts
let fold_inductive_blocks f =
- Array.fold_left (fun acc (_,ar,_,_,_,lc) -> f (Array.fold_left f acc lc) ar)
+ Array.fold_left (fun acc (_,_,lc,(arsign,_)) ->
+ f (Array.fold_left f acc lc) (it_mkProd_or_LetIn (* dummy *) mkSet arsign))
let used_section_variables env inds =
let ids = fold_inductive_blocks
@@ -534,10 +585,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
let hyps = used_section_variables env inds in
let nparamargs = rel_context_nhyps params in
(* Check one inductive *)
- let build_one_packet (id,ar,cnames,issmall,isunit,lc) recarg =
- (* Arity in normal form *)
- let (ar_sign,ar_sort) = dest_arity env ar in
- let nf_ar = if isArity ar then ar else mkArity (ar_sign,ar_sort) in
+ let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg =
(* Type of constructors in normal form *)
let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
@@ -546,8 +594,19 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
Array.map (fun (d,_) -> rel_context_length d - rel_context_length params)
splayed_lc in
(* Elimination sorts *)
- let isunit = isunit && ntypes = 1 && (not (is_recursive recargs.(0))) in
- let kelim = allowed_sorts env issmall isunit ar_sort in
+ let arkind,kelim = match ar_kind with
+ | Inr (param_levels,lev) ->
+ Polymorphic {
+ mind_param_levels = param_levels;
+ mind_level = lev;
+ }, all_sorts
+ | Inl ((issmall,isunit),ar,s) ->
+ let isunit = isunit && ntypes = 1 && not (is_recursive recargs.(0)) in
+ let kelim = allowed_sorts issmall isunit s in
+ Monomorphic {
+ mind_user_arity = ar;
+ mind_sort = s;
+ }, kelim in
let nconst, nblock = ref 0, ref 0 in
let transf num =
let arity = List.length (dest_subterms recarg).(num) in
@@ -563,16 +622,15 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
let rtbl = Array.init (List.length cnames) transf in
(* Build the inductive packet *)
{ mind_typename = id;
- mind_user_arity = ar;
- mind_nf_arity = nf_ar;
+ mind_arity = arkind;
+ mind_arity_ctxt = ar_sign;
mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
- mind_sort = ar_sort;
mind_kelim = kelim;
mind_consnames = Array.of_list cnames;
mind_consnrealdecls = consnrealargs;
mind_user_lc = lc;
mind_nf_lc = nf_lc;
- mind_recargs = recarg;
+ mind_recargs = recarg;
mind_nb_constant = !nconst;
mind_nb_args = !nblock;
mind_reloc_tbl = rtbl;
@@ -600,5 +658,5 @@ let check_inductive env mie =
(* Then check positivity conditions *)
let (nmr,recargs) = check_positivity env_ar params inds in
(* Build the inductive packets *)
- build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite
+ build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite
inds nmr recargs cst
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 736f4da1..d9f9f912 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: inductive.ml 8673 2006-03-29 21:21:52Z herbelin $ *)
+(* $Id: inductive.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
open Util
open Names
@@ -47,6 +47,8 @@ let find_coinductive env c =
when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
| _ -> raise Not_found
+let inductive_params (mib,_) = mib.mind_nparams
+
(************************************************************************)
(* Build the substitution that replaces Rels by the appropriate *)
@@ -80,10 +82,12 @@ let instantiate_params full t args sign =
let instantiate_partial_params = instantiate_params false
-let full_inductive_instantiate mib params t =
- instantiate_params true t params mib.mind_params_ctxt
+let full_inductive_instantiate mib params sign =
+ let dummy = mk_Prop in
+ let t = mkArity (sign,dummy) in
+ fst (destArity (instantiate_params true t params mib.mind_params_ctxt))
-let full_constructor_instantiate (((mind,_),mib,_),params) =
+let full_constructor_instantiate ((mind,_),(mib,_),params) =
let inst_ind = constructor_instantiate mind mib in
(fun t ->
instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
@@ -93,22 +97,6 @@ let full_constructor_instantiate (((mind,_),mib,_),params) =
(* Functions to build standard types related to inductive *)
-(* For each inductive type of a block that is of level u_i, we have
- the constraints that u_i >= v_i where v_i is the type level of the
- types of the constructors of this inductive type. Each v_i depends
- of some of the u_i and of an extra (maybe non variable) universe,
- say w_i. Typically, for three inductive types, we could have
-
- u1,u2,u3,w1 <= u1
- u1 w2 <= u2
- u2,u3,w3 <= u3
-
- From this system of inequations, we shall deduce
-
- w1,w2,w3 <= u1
- w1,w2 <= u2
- w1,w2,w3 <= u3
-*)
let number_of_inductives mib = Array.length mib.mind_packets
let number_of_constructors mip = Array.length mip.mind_consnames
@@ -134,17 +122,6 @@ where
Remark: Set (predicative) is encoded as Type(0)
*)
-let find_constraint levels level_bounds i nci =
- if nci = 0 then mk_Prop
- else
- let level_bounds' = solve_constraints_system levels level_bounds in
- let level = level_bounds'.(i) in
- if nci = 1 & is_empty_universe level then mk_Prop
- else if Univ.is_base level then mk_Set else Type level
-
-let find_inductive_level env (mib,mip) (_,i) levels level_bounds =
- find_constraint levels level_bounds i (number_of_constructors mip)
-
let set_inductive_level env s t =
let sign,s' = dest_prod_assum env t in
if family_of_sort s <> family_of_sort (destSort s') then
@@ -153,45 +130,69 @@ let set_inductive_level env s t =
else
t
-let constructor_instances env (mib,mip) (_,i) args =
- let nargs = Array.length args in
- let args = Array.to_list args in
- let uargs =
- if nargs > mib.mind_nparams_rec then
- fst (list_chop mib.mind_nparams_rec args)
- else args in
- let arities =
- Array.map (fun mip -> destArity mip.mind_nf_arity) mib.mind_packets in
- (* Compute the minimal type *)
- let levels = Array.init
- (number_of_inductives mib) (fun _ -> fresh_local_univ ()) in
- let arities = list_tabulate (fun i ->
- let ctx,s = arities.(i) in
- let s = match s with Type _ -> Type (levels.(i)) | s -> s in
- (Name mib.mind_packets.(i).mind_typename,None,mkArity (ctx,s)))
- (number_of_inductives mib) in
- (* Remark: all arities are closed hence no need for lift *)
- let env_ar = push_rel_context (List.rev arities) env in
- let uargs = List.map (lift (number_of_inductives mib)) uargs in
- let lc =
- Array.map (fun mip ->
- Array.map (fun c ->
- instantiate_partial_params c uargs mib.mind_params_ctxt)
- mip.mind_nf_lc)
- mib.mind_packets in
- env_ar, lc, levels
-
-let is_small_inductive (mip,mib) = is_small (snd (destArity mib.mind_nf_arity))
-
-let max_inductive_sort v =
- let v = Array.map (function
- | Type u -> u
- | _ -> anomaly "Only type levels when computing the minimal sort of an inductive type") v in
- Univ.sup_array v
-
-(* Type of an inductive type *)
-
-let type_of_inductive (_,mip) = mip.mind_user_arity
+let sort_as_univ = function
+| Type u -> u
+| Prop Null -> neutral_univ
+| Prop Pos -> base_univ
+
+let rec make_subst env exp act =
+ match exp, act with
+ (* Bind expected levels of parameters to actual levels *)
+ | None :: exp, _ :: act ->
+ make_subst env exp act
+ | Some u :: exp, t :: act ->
+ (u, sort_as_univ (snd (dest_arity env t))) :: make_subst env exp act
+ (* Not enough parameters, create a fresh univ *)
+ | Some u :: exp, [] ->
+ (u, fresh_local_univ ()) :: make_subst env exp []
+ | None :: exp, [] ->
+ make_subst env exp []
+ (* Uniform parameters are exhausted *)
+ | [], _ -> []
+
+let sort_of_instantiated_universe mip subst level =
+ let level = subst_large_constraints subst level in
+ let nci = number_of_constructors mip in
+ if nci = 0 then mk_Prop
+ else
+ if is_empty_univ level then if nci = 1 then mk_Prop else mk_Set
+ else if is_base_univ level then mk_Set
+ else Type level
+
+let instantiate_inductive_with_param_levels env ar mip paramtyps =
+ let args = Array.to_list paramtyps in
+ let subst = make_subst env ar.mind_param_levels args in
+ sort_of_instantiated_universe mip subst ar.mind_level
+
+let type_of_inductive_knowing_parameters env mip paramtyps =
+ match mip.mind_arity with
+ | Monomorphic s ->
+ s.mind_user_arity
+ | Polymorphic ar ->
+ let s = instantiate_inductive_with_param_levels env ar mip paramtyps in
+ mkArity (mip.mind_arity_ctxt,s)
+
+(* The max of an array of universes *)
+
+let cumulate_constructor_univ u = function
+ | Prop Null -> u
+ | Prop Pos -> sup base_univ u
+ | Type u' -> sup u u'
+
+let max_inductive_sort =
+ Array.fold_left cumulate_constructor_univ neutral_univ
+
+(* Type of a (non applied) inductive type *)
+
+let type_of_inductive (_,mip) =
+ match mip.mind_arity with
+ | Monomorphic s -> s.mind_user_arity
+ | Polymorphic s ->
+ let subst = map_succeed (function
+ | Some u -> (u, fresh_local_univ ())
+ | None -> failwith "") s.mind_param_levels in
+ let s = mkSort (sort_of_instantiated_universe mip subst s.mind_level) in
+ it_mkProd_or_LetIn s mip.mind_arity_ctxt
(************************************************************************)
(* Type of a constructor *)
@@ -215,19 +216,11 @@ let arities_of_constructors ind specif =
(************************************************************************)
-let is_info_arity env c =
- match dest_arity env c with
- | (_,Prop Null) -> false
- | (_,Prop Pos) -> true
- | (_,Type _) -> true
-
-let error_elim_expln env kp ki =
- if is_info_arity env kp && not (is_info_arity env ki) then
- NonInformativeToInformative
- else
- match (kind_of_term kp,kind_of_term ki) with
- | Sort (Type _), Sort (Prop _) -> StrongEliminationOnNonSmallType
- | _ -> WrongArity
+let error_elim_expln kp ki =
+ match kp,ki with
+ | (InType | InSet), InProp -> NonInformativeToInformative
+ | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *)
+ | _ -> WrongArity
(* Type of case predicates *)
@@ -244,9 +237,20 @@ let local_rels ctxt =
rels
(* Get type of inductive, with parameters instantiated *)
-let get_arity mib mip params =
- let arity = mip.mind_nf_arity in
- destArity (full_inductive_instantiate mib params arity)
+
+let inductive_sort_family mip =
+ match mip.mind_arity with
+ | Monomorphic s -> family_of_sort s.mind_sort
+ | Polymorphic _ -> InType
+
+let mind_arity mip =
+ mip.mind_arity_ctxt, inductive_sort_family mip
+
+let get_instantiated_arity (mib,mip) params =
+ let sign, s = mind_arity mip in
+ full_inductive_instantiate mib params sign, s
+
+let elim_sorts (_,mip) = mip.mind_kelim
let rel_list n m =
let rec reln l p =
@@ -254,66 +258,48 @@ let rel_list n m =
in
reln [] 1
-let build_dependent_inductive ind mib mip params =
+let build_dependent_inductive ind (_,mip) params =
let nrealargs = mip.mind_nrealargs in
applist
(mkInd ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
-
(* This exception is local *)
-exception LocalArity of (constr * constr * arity_error) option
+exception LocalArity of (sorts_family * sorts_family * arity_error) option
-let is_correct_arity env c pj ind mib mip params =
- let kelim = mip.mind_kelim in
- let arsign,s = get_arity mib mip params in
- let nodep_ar = it_mkProd_or_LetIn (mkSort s) arsign in
- let rec srec env pt t u =
+let check_allowed_sort ksort specif =
+ if not (List.exists ((=) ksort) (elim_sorts specif)) then
+ let s = inductive_sort_family (snd specif) in
+ raise (LocalArity (Some(ksort,s,error_elim_expln ksort s)))
+
+let is_correct_arity env c pj ind specif params =
+ let arsign,_ = get_instantiated_arity specif params in
+ let rec srec env pt ar u =
let pt' = whd_betadeltaiota env pt in
- let t' = whd_betadeltaiota env t in
- match kind_of_term pt', kind_of_term t' with
- | Prod (na1,a1,a2), Prod (_,a1',a2') ->
+ match kind_of_term pt', ar with
+ | Prod (na1,a1,t), (_,None,a1')::ar' ->
let univ =
try conv env a1 a1'
with NotConvertible -> raise (LocalArity None) in
- srec (push_rel (na1,None,a1) env) a2 a2' (Constraint.union u univ)
- | Prod (_,a1,a2), _ ->
- let k = whd_betadeltaiota env a2 in
- let ksort = match kind_of_term k with
+ srec (push_rel (na1,None,a1) env) t ar' (Constraint.union u univ)
+ | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *)
+ let ksort = match kind_of_term (whd_betadeltaiota env a2) with
| Sort s -> family_of_sort s
| _ -> raise (LocalArity None) in
-
- let dep_ind = build_dependent_inductive ind mib mip params
- in
+ let dep_ind = build_dependent_inductive ind specif params in
let univ =
try conv env a1 dep_ind
with NotConvertible -> raise (LocalArity None) in
- if List.exists ((=) ksort) kelim then
- (true, Constraint.union u univ)
- else
- raise (LocalArity (Some(k,t',error_elim_expln env k t')))
- | k, Prod (_,_,_) ->
+ check_allowed_sort ksort specif;
+ (true, Constraint.union u univ)
+ | Sort s', [] ->
+ check_allowed_sort (family_of_sort s') specif;
+ (false, u)
+ | _ ->
raise (LocalArity None)
- | k, ki ->
- let ksort = match k with
- | Sort s -> family_of_sort s
- | _ -> raise (LocalArity None) in
- if List.exists ((=) ksort) kelim then
- (false, u)
- else
- raise (LocalArity (Some(pt',t',error_elim_expln env pt' t')))
in
- try srec env pj.uj_type nodep_ar Constraint.empty
+ try srec env pj.uj_type (List.rev arsign) Constraint.empty
with LocalArity kinds ->
- let create_sort = function
- | InProp -> mkProp
- | InSet -> mkSet
- | InType -> mkSort type_0 in
- let listarity = List.map create_sort kelim
-(* let listarity =
- (List.map (fun s -> make_arity env true indf (create_sort s)) kelim)
- @(List.map (fun s -> make_arity env false indf (create_sort s)) kelim)*)
- in
- error_elim_arity env ind listarity c pj kinds
+ error_elim_arity env ind (elim_sorts specif) c pj kinds
(************************************************************************)
@@ -321,13 +307,13 @@ let is_correct_arity env c pj ind mib mip params =
(* [p] is the predicate, [i] is the constructor number (starting from 0),
and [cty] is the type of the constructor (params not instantiated) *)
-let build_branches_type ind mib mip params dep p =
+let build_branches_type ind (_,mip as specif) params dep p =
let build_one_branch i cty =
- let typi = full_constructor_instantiate ((ind,mib,mip),params) cty in
+ let typi = full_constructor_instantiate (ind,specif,params) cty in
let (args,ccl) = decompose_prod_assum typi in
let nargs = rel_context_length args in
let (_,allargs) = decompose_app ccl in
- let (lparams,vargs) = list_chop mib.mind_nparams allargs in
+ let (lparams,vargs) = list_chop (inductive_params specif) allargs in
let cargs =
if dep then
let cstr = ith_constructor_of_inductive ind (i+1) in
@@ -346,12 +332,12 @@ let build_case_type dep p c realargs =
beta_appvect p (Array.of_list args)
let type_case_branches env (ind,largs) pj c =
- let (mib,mip) = lookup_mind_specif env ind in
- let nparams = mib.mind_nparams in
+ let specif = lookup_mind_specif env ind in
+ let nparams = inductive_params specif in
let (params,realargs) = list_chop nparams largs in
let p = pj.uj_val in
- let (dep,univ) = is_correct_arity env c pj ind mib mip params in
- let lc = build_branches_type ind mib mip params dep p in
+ let (dep,univ) = is_correct_arity env c pj ind specif params in
+ let lc = build_branches_type ind specif params dep p in
let ty = build_case_type dep p c realargs in
(lc, ty, univ)
@@ -399,24 +385,27 @@ let check_case_info env indsp ci =
first argument.
*)
-(*************************)
-(* Environment annotated with marks on recursive arguments:
- it is a triple (env,lst,n) where
- - env is the typing environment
- - lst is a mapping from de Bruijn indices to list of recargs
- (tells which subterms of that variable are recursive)
- - n is the de Bruijn index of the fixpoint for which we are
- checking the guard condition.
+(*************************************************************)
+(* Environment annotated with marks on recursive arguments *)
- Below are functions to handle such environment.
- *)
+(* tells whether it is a strict or loose subterm *)
type size = Large | Strict
+(* merging information *)
let size_glb s1 s2 =
match s1,s2 with
Strict, Strict -> Strict
| _ -> Large
+(* possible specifications for a term:
+ - Not_subterm: when the size of a term is not related to the
+ recursive argument of the fixpoint
+ - Subterm: when the term is a subterm of the recursive argument
+ the wf_paths argument specifies which subterms are recursive
+ - Dead_code: when the term has been built by elimination over an
+ empty type
+ *)
+
type subterm_spec =
Subterm of (size * wf_paths)
| Dead_code
@@ -517,31 +506,14 @@ let lookup_subterms env ind =
(*********************************)
-(* finds the inductive type of the recursive argument of a fixpoint *)
-let inductive_of_fix env recarg body =
- let (ctxt,b) = decompose_lam_n_assum recarg body in
- let env' = push_rel_context ctxt env in
- let (_,ty,_) = destLambda(whd_betadeltaiota env' b) in
- let (i,_) = decompose_app (whd_betadeltaiota env' ty) in
- destInd i
-
-(*
- subterm_specif env c ind
-
- subterm_specif should test if [c] (building objects of inductive
- type [ind], not necessarily the same as that of the recursive
- argument) is a subterm of the recursive argument of the fixpoint we
- are checking and fails with Not_found if not. In case it is, it
- should send its recursive specification (i.e. on which arguments we
- are allowed to make recursive calls). This recursive spec should be
- the same size as the number of constructors of the type of c.
-
- Returns:
- - [Some lc] if [c] is a strict subterm of the rec. arg. (or a Meta)
- - [None] otherwise
+(* [subterm_specif renv t] computes the recursive structure of [t] and
+ compare its size with the size of the initial recursive argument of
+ the fixpoint we are checking. [renv] collects such information
+ about variables.
*)
-let rec subterm_specif renv t ind =
+let rec subterm_specif renv t =
+ (* maybe reduction is not always necessary! *)
let f,l = decompose_app (whd_betadeltaiota renv.env t) in
match kind_of_term f with
| Rel k -> subterm_var k renv
@@ -551,7 +523,7 @@ let rec subterm_specif renv t ind =
else
let lbr_spec = case_branches_specif renv c ci.ci_ind lbr in
let stl =
- Array.map (fun (renv',br') -> subterm_specif renv' br' ind)
+ Array.map (fun (renv',br') -> subterm_specif renv' br')
lbr_spec in
subterm_spec_glb stl
@@ -561,33 +533,43 @@ let rec subterm_specif renv t ind =
furthermore when f is applied to a term which is strictly less than
n, one may assume that x itself is strictly less than n
*)
- let nbfix = Array.length typarray in
- let recargs = lookup_subterms renv.env ind in
- (* pushing the fixpoints *)
- let renv' = push_fix_renv renv recdef in
- let renv' =
- assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in
- let decrArg = recindxs.(i) in
- let theBody = bodies.(i) in
- let nbOfAbst = decrArg+1 in
- let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
- (* pushing the fix parameters *)
- let renv'' = push_ctxt_renv renv' sign in
- let renv'' =
- if List.length l < nbOfAbst then renv''
- else
- let decrarg_ind = inductive_of_fix renv''.env decrArg theBody in
- let theDecrArg = List.nth l decrArg in
- let arg_spec = subterm_specif renv theDecrArg decrarg_ind in
- assign_var_spec renv'' (1, arg_spec) in
- subterm_specif renv'' strippedBody ind
-
+ let (ctxt,clfix) = dest_prod renv.env typarray.(i) in
+ let oind =
+ let env' = push_rel_context ctxt renv.env in
+ try Some(fst(find_inductive env' clfix))
+ with Not_found -> None in
+ (match oind with
+ None -> Not_subterm (* happens if fix is polymorphic *)
+ | Some ind ->
+ let nbfix = Array.length typarray in
+ let recargs = lookup_subterms renv.env ind in
+ (* pushing the fixpoints *)
+ let renv' = push_fix_renv renv recdef in
+ let renv' =
+ (* Why Strict here ? To be general, it could also be
+ Large... *)
+ assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in
+ let decrArg = recindxs.(i) in
+ let theBody = bodies.(i) in
+ let nbOfAbst = decrArg+1 in
+ let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
+ (* pushing the fix parameters *)
+ let renv'' = push_ctxt_renv renv' sign in
+ let renv'' =
+ if List.length l < nbOfAbst then renv''
+ else
+ let theDecrArg = List.nth l decrArg in
+ let arg_spec = subterm_specif renv theDecrArg in
+ assign_var_spec renv'' (1, arg_spec) in
+ subterm_specif renv'' strippedBody)
+
| Lambda (x,a,b) ->
assert (l=[]);
- subterm_specif (push_var_renv renv (x,a)) b ind
+ subterm_specif (push_var_renv renv (x,a)) b
+
+ (* Metas and evars are considered OK *)
+ | (Meta _|Evar _) -> Dead_code
- (* A term with metas is considered OK *)
- | Meta _ -> Dead_code
(* Other terms are not subterms *)
| _ -> Not_subterm
@@ -595,16 +577,20 @@ let rec subterm_specif renv t ind =
object is a recursive subterm then compute the information
associated to its own subterms.
Rq: if branch is not eta-long, then the recursive information
- is not propagated *)
+ is not propagated to the missing abstractions *)
and case_branches_specif renv c ind lbr =
- let c_spec = subterm_specif renv c ind in
+ let c_spec = subterm_specif renv c in
let rec push_branch_args renv lrec c =
- let c' = strip_outer_cast (whd_betadeltaiota renv.env c) in
- match lrec, kind_of_term c' with
- | (ra::lr,Lambda (x,a,b)) ->
- let renv' = push_var renv (x,a,ra) in
- push_branch_args renv' lr b
- | (_,_) -> (renv,c') in
+ match lrec with
+ ra::lr ->
+ let c' = whd_betadeltaiota renv.env c in
+ (match kind_of_term c' with
+ Lambda(x,a,b) ->
+ let renv' = push_var renv (x,a,ra) in
+ push_branch_args renv' lr b
+ | _ -> (* branch not in eta-long form: cannot perform rec. calls *)
+ (renv,c'))
+ | [] -> (renv, c) in
match c_spec with
Subterm (_,t) ->
let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in
@@ -618,8 +604,8 @@ and case_branches_specif renv c ind lbr =
| Not_subterm -> Array.map (fun c -> (renv,c)) lbr
(* Check term c can be applied to one of the mutual fixpoints. *)
-let check_is_subterm renv c ind =
- match subterm_specif renv c ind with
+let check_is_subterm renv c =
+ match subterm_specif renv c with
Subterm (Strict,_) | Dead_code -> true
| _ -> false
@@ -642,42 +628,45 @@ let error_illegal_rec_call renv fx arg =
let error_partial_apply renv fx =
raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
-
(* Check if [def] is a guarded fixpoint body with decreasing arg.
given [recpos], the decreasing arguments of each mutually defined
fixpoint. *)
let check_one_fix renv recpos def =
let nfi = Array.length recpos in
+
+ (* Checks if [t] only make valid recursive calls *)
let rec check_rec_call renv t =
(* if [t] does not make recursive calls, it is guarded: *)
- noccur_with_meta renv.rel_min nfi t or
- (* Rq: why not try and expand some definitions ? *)
- let f,l = decompose_app (whd_betaiotazeta renv.env t) in
- match kind_of_term f with
- | Rel p ->
- (* Test if it is a recursive call: *)
- if renv.rel_min <= p & p < renv.rel_min+nfi then
- (* the position of the invoked fixpoint: *)
- let glob = renv.rel_min+nfi-1-p in
- (* the decreasing arg of the rec call: *)
- let np = recpos.(glob) in
- if List.length l <= np then error_partial_apply renv glob;
- match list_chop np l with
- (la,(z::lrest)) ->
- (* Check the decreasing arg is smaller *)
- if not (check_is_subterm renv z renv.inds.(glob)) then
- error_illegal_rec_call renv glob z;
- List.for_all (check_rec_call renv) (la@lrest)
- | _ -> assert false
- (* otherwise check the arguments are guarded: *)
- else List.for_all (check_rec_call renv) l
+ if noccur_with_meta renv.rel_min nfi t then ()
+ else
+ (* Rq: why not try and expand some definitions ? *)
+ let f,l = decompose_app (whd_betaiotazeta renv.env t) in
+ match kind_of_term f with
+ | Rel p ->
+ (* Test if [p] is a fixpoint (recursive call) *)
+ if renv.rel_min <= p & p < renv.rel_min+nfi then
+ (* the position of the invoked fixpoint: *)
+ let glob = renv.rel_min+nfi-1-p in
+ (* the decreasing arg of the rec call: *)
+ let np = recpos.(glob) in
+ if List.length l <= np then error_partial_apply renv glob
+ else
+ (match list_chop np l with
+ (la,(z::lrest)) ->
+ (* Check the decreasing arg is smaller *)
+ if not (check_is_subterm renv z) then
+ error_illegal_rec_call renv glob z;
+ List.iter (check_rec_call renv) (la@lrest)
+ | _ -> assert false)
+ (* otherwise check the arguments are guarded: *)
+ else List.iter (check_rec_call renv) l
| Case (ci,p,c_0,lrest) ->
- List.for_all (check_rec_call renv) (c_0::p::l) &&
+ List.iter (check_rec_call renv) (c_0::p::l);
(* compute the recarg information for the arguments of
each branch *)
let lbr = case_branches_specif renv c_0 ci.ci_ind lrest in
- array_for_all (fun (renv',br') -> check_rec_call renv' br') lbr
+ Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
(* Enables to traverse Fixpoint definitions in a more intelligent
way, ie, the rule :
@@ -695,65 +684,58 @@ let check_one_fix renv recpos def =
Eduardo 7/9/98 *)
| Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
- List.for_all (check_rec_call renv) l &&
- array_for_all (check_rec_call renv) typarray &&
+ List.iter (check_rec_call renv) l;
+ Array.iter (check_rec_call renv) typarray;
let decrArg = recindxs.(i) in
let renv' = push_fix_renv renv recdef in
if (List.length l < (decrArg+1)) then
- array_for_all (check_rec_call renv') bodies
+ Array.iter (check_rec_call renv') bodies
else
- let ok_vect =
- Array.mapi
- (fun j body ->
- if i=j then
- let decrarg_ind =
- inductive_of_fix renv'.env decrArg body in
- let theDecrArg = List.nth l decrArg in
- let arg_spec =
- subterm_specif renv theDecrArg decrarg_ind in
- check_nested_fix_body renv' (decrArg+1) arg_spec body
- else check_rec_call renv' body)
- bodies in
- array_for_all (fun b -> b) ok_vect
+ Array.iteri
+ (fun j body ->
+ if i=j then
+ let theDecrArg = List.nth l decrArg in
+ let arg_spec = subterm_specif renv theDecrArg in
+ check_nested_fix_body renv' (decrArg+1) arg_spec body
+ else check_rec_call renv' body)
+ bodies
| Const kn ->
- (try List.for_all (check_rec_call renv) l
- with (FixGuardError _ ) as e ->
- if evaluable_constant kn renv.env then
- check_rec_call renv
- (applist(constant_value renv.env kn, l))
- else raise e)
+ if evaluable_constant kn renv.env then
+ try List.iter (check_rec_call renv) l
+ with (FixGuardError _ ) ->
+ check_rec_call renv(applist(constant_value renv.env kn, l))
+ else List.iter (check_rec_call renv) l
(* The cases below simply check recursively the condition on the
subterms *)
| Cast (a,_, b) ->
- List.for_all (check_rec_call renv) (a::b::l)
+ List.iter (check_rec_call renv) (a::b::l)
| Lambda (x,a,b) ->
- check_rec_call (push_var_renv renv (x,a)) b &&
- List.for_all (check_rec_call renv) (a::l)
+ check_rec_call (push_var_renv renv (x,a)) b;
+ List.iter (check_rec_call renv) (a::l)
| Prod (x,a,b) ->
- check_rec_call (push_var_renv renv (x,a)) b &&
- List.for_all (check_rec_call renv) (a::l)
+ check_rec_call (push_var_renv renv (x,a)) b;
+ List.iter (check_rec_call renv) (a::l)
| CoFix (i,(_,typarray,bodies as recdef)) ->
- array_for_all (check_rec_call renv) typarray &&
- List.for_all (check_rec_call renv) l &&
+ Array.iter (check_rec_call renv) typarray;
+ List.iter (check_rec_call renv) l;
let renv' = push_fix_renv renv recdef in
- array_for_all (check_rec_call renv') bodies
-
- | Evar (_,la) ->
- array_for_all (check_rec_call renv) la &&
- List.for_all (check_rec_call renv) l
+ Array.iter (check_rec_call renv') bodies
- | Meta _ -> true
+ | Evar _ ->
+ List.iter (check_rec_call renv) l
- | (App _ | LetIn _) ->
- anomaly "check_rec_call: should have been reduced"
+ (* l is not checked because it is considered as the meta's context *)
+ | Meta _ -> ()
| (Ind _ | Construct _ | Var _ | Sort _) ->
- List.for_all (check_rec_call renv) l
+ List.iter (check_rec_call renv) l
+
+ | (App _ | LetIn _) -> assert false (* beta zeta reduction *)
and check_nested_fix_body renv decr recArgsDecrArg body =
if decr = 0 then
@@ -761,11 +743,11 @@ let check_one_fix renv recpos def =
else
match kind_of_term body with
| Lambda (x,a,b) ->
+ check_rec_call renv a;
let renv' = push_var_renv renv (x,a) in
- check_rec_call renv a &&
check_nested_fix_body renv' (decr-1) recArgsDecrArg b
| _ -> anomaly "Not enough abstractions in fix body"
-
+
in
check_rec_call renv def
@@ -784,7 +766,6 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
error_ill_formed_rec_body env err names i in
(* Check the i-th definition with recarg k *)
let find_ind i k def =
- if k < 0 then anomaly "negative recarg position";
(* check fi does not appear in the k+1 first abstractions,
gives the type of the k+1-eme abstraction (must be an inductive) *)
let rec check_occur env n def =
@@ -813,8 +794,7 @@ let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) =
for i = 0 to Array.length bodies - 1 do
let (fenv,body) = rdef.(i) in
let renv = make_renv fenv minds nvect.(i) minds.(i) in
- try
- let _ = check_one_fix renv nvect body in ()
+ try check_one_fix renv nvect body
with FixGuardError (fixenv,err) ->
error_ill_formed_rec_body fixenv err names i
done
@@ -825,14 +805,6 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
*)
(************************************************************************)
-(* Scrape *)
-
-let rec scrape_mind env kn =
- match (Environ.lookup_mind kn env).mind_equiv with
- | None -> kn
- | Some kn' -> scrape_mind env kn'
-
-(************************************************************************)
(* Co-fixpoints. *)
exception CoFixGuardError of env * guard_error
@@ -852,25 +824,19 @@ let rec codomain_is_coind env c =
let check_one_cofix env nbfix def deftype =
let rec check_rec_call env alreadygrd n vlra t =
- if noccur_with_meta n nbfix t then
- true
- else
+ if not (noccur_with_meta n nbfix t) then
let c,args = decompose_app (whd_betadeltaiota env t) in
match kind_of_term c with
- | Meta _ -> true
-
| Rel p when n <= p && p < n+nbfix ->
- (* recursive call *)
- if alreadygrd then
- if List.for_all (noccur_with_meta n nbfix) args then
- true
- else
- raise (CoFixGuardError (env,NestedRecursiveOccurrences))
- else
+ (* recursive call: must be guarded and no nested recursive
+ call allowed *)
+ if not alreadygrd then
raise (CoFixGuardError (env,UnguardedRecursiveCall t))
+ else if not(List.for_all (noccur_with_meta n nbfix) args) then
+ raise (CoFixGuardError (env,NestedRecursiveOccurrences))
| Construct (_,i as cstr_kn) ->
- let lra =vlra.(i-1) in
+ let lra = vlra.(i-1) in
let mI = inductive_of_constructor cstr_kn in
let (mib,mip) = lookup_mind_specif env mI in
let realargs = list_skipn mib.mind_nparams args in
@@ -883,17 +849,17 @@ let check_one_cofix env nbfix def deftype =
(env,RecCallInNonRecArgOfConstructor t))
else
let spec = dest_subterms rar in
- check_rec_call env true n spec t &&
+ check_rec_call env true n spec t;
process_args_of_constr (lr, lrar)
- | [],_ -> true
+ | [],_ -> ()
| _ -> anomaly_ill_typed ()
in process_args_of_constr (realargs, lra)
| Lambda (x,a,b) ->
assert (args = []);
- if (noccur_with_meta n nbfix a) then
- check_rec_call (push_rel (x, None, a) env)
- alreadygrd (n+1) vlra b
+ if noccur_with_meta n nbfix a then
+ let env' = push_rel (x, None, a) env in
+ check_rec_call env' alreadygrd (n+1) vlra b
else
raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
@@ -903,10 +869,8 @@ let check_one_cofix env nbfix def deftype =
let nbfix = Array.length vdefs in
if (array_for_all (noccur_with_meta n nbfix) varit) then
let env' = push_rec_types recdef env in
- (array_for_all
- (check_rec_call env' alreadygrd (n+1) vlra) vdefs)
- &&
- (List.for_all (check_rec_call env alreadygrd (n+1) vlra) args)
+ (Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs;
+ List.iter (check_rec_call env alreadygrd n vlra) args)
else
raise (CoFixGuardError (env,RecCallInTypeOfDef c))
else
@@ -916,7 +880,7 @@ let check_one_cofix env nbfix def deftype =
if (noccur_with_meta n nbfix p) then
if (noccur_with_meta n nbfix tm) then
if (List.for_all (noccur_with_meta n nbfix) args) then
- (array_for_all (check_rec_call env alreadygrd n vlra) vrest)
+ Array.iter (check_rec_call env alreadygrd n vlra) vrest
else
raise (CoFixGuardError (env,RecCallInCaseFun c))
else
@@ -924,7 +888,12 @@ let check_one_cofix env nbfix def deftype =
else
raise (CoFixGuardError (env,RecCallInCasePred c))
+ | Meta _ -> ()
+ | Evar _ ->
+ List.iter (check_rec_call env alreadygrd n vlra) args
+
| _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in
+
let (mind, _) = codomain_is_coind env deftype in
let vlra = lookup_subterms env mind in
check_rec_call env false 1 (dest_subterms vlra) def
@@ -936,9 +905,7 @@ let check_cofix env (bodynum,(names,types,bodies as recdef)) =
let nbfix = Array.length bodies in
for i = 0 to nbfix-1 do
let fixenv = push_rec_types recdef env in
- try
- let _ = check_one_cofix fixenv nbfix bodies.(i) types.(i)
- in ()
+ try check_one_cofix fixenv nbfix bodies.(i) types.(i)
with CoFixGuardError (errenv,err) ->
error_ill_formed_rec_body errenv err names i
done
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index e60f909e..d81904cc 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: inductive.mli 8673 2006-03-29 21:21:52Z herbelin $ i*)
+(*i $Id: inductive.mli 8871 2006-05-28 16:46:48Z herbelin $ i*)
(*i*)
open Names
@@ -38,6 +38,8 @@ val lookup_mind_specif : env -> inductive -> mind_specif
val type_of_inductive : mind_specif -> types
+val elim_sorts : mind_specif -> sorts_family list
+
(* Return type as quoted by the user *)
val type_of_constructor : constructor -> mind_specif -> types
@@ -58,28 +60,48 @@ val type_case_branches :
env -> inductive * constr list -> unsafe_judgment -> constr
-> types array * types * constraints
+(* Return the arity of an inductive type *)
+val mind_arity : one_inductive_body -> Sign.rel_context * sorts_family
+
+val inductive_sort_family : one_inductive_body -> sorts_family
+
(* Check a [case_info] actually correspond to a Case expression on the
given inductive type. *)
val check_case_info : env -> inductive -> case_info -> unit
-(* Find the ultimate inductive in the [mind_equiv] chain *)
-
-val scrape_mind : env -> mutual_inductive -> mutual_inductive
-
(*s Guard conditions for fix and cofix-points. *)
val check_fix : env -> fixpoint -> unit
val check_cofix : env -> cofixpoint -> unit
(*s Support for sort-polymorphic inductive types *)
-val constructor_instances : env -> mind_specif -> inductive ->
- constr array -> env * types array array * universe array
+val type_of_inductive_knowing_parameters :
+ env -> one_inductive_body -> types array -> types
val set_inductive_level : env -> sorts -> types -> types
-val find_inductive_level : env -> mind_specif -> inductive ->
- universe array -> universe array -> sorts
-
-val is_small_inductive : mind_specif -> bool
-
val max_inductive_sort : sorts array -> universe
+
+(***************************************************************)
+(* Debug *)
+
+type size = Large | Strict
+type subterm_spec =
+ Subterm of (size * wf_paths)
+ | Dead_code
+ | Not_subterm
+type guard_env =
+ { env : env;
+ (* dB of last fixpoint *)
+ rel_min : int;
+ (* inductive of recarg of each fixpoint *)
+ inds : inductive array;
+ (* the recarg information of inductive family *)
+ recvec : wf_paths array;
+ (* dB of variables denoting subterms *)
+ genv : subterm_spec list;
+ }
+
+val subterm_specif : guard_env -> constr -> subterm_spec
+val case_branches_specif : guard_env -> constr -> inductive ->
+ constr array -> (guard_env * constr) array
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 3d041c6c..b2f02a5f 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modops.ml 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: modops.ml 8879 2006-05-30 21:32:10Z letouzey $ i*)
(*i*)
open Util
@@ -41,7 +41,7 @@ let error_incompatible_labels l l' =
error ("Opening and closing labels are not the same: "
^string_of_label l^" <> "^string_of_label l'^" !")
-let error_result_must_be_signature mtb =
+let error_result_must_be_signature () =
error "The result module type must be a signature"
let error_signature_expected mtb =
@@ -190,35 +190,13 @@ and constants_of_modtype env mp modtype =
(subst_signature_msid msid mp sign)
| MTBfunsig _ -> []
-(* returns a resolver for kn that maps mbid to mp and then delta-expands
- the obtained constants according to env *)
+(* returns a resolver for kn that maps mbid to mp *)
+(* Nota: Some delta-expansions used to happen here.
+ Browse SVN if you want to know more. *)
let resolver_of_environment mbid modtype mp env =
let constants = constants_of_modtype env (MPbound mbid) modtype in
- let resolve =
- List.map
- (fun (con,expecteddef) ->
- let con' = replace_mp_in_con (MPbound mbid) mp con in
- let constr =
- try
- if expecteddef.Declarations.const_body <> None then
- (* Do not expand constants that already have a body in the
- expected type (i.e. only parameters/axioms in the module type
- are expanded). In the few examples we have this seems to
- be the more reasonable behaviour for the user. *)
- None
- else
- let constant = lookup_constant con' env in
- if constant.Declarations.const_opaque then
- None
- else
- option_app Declarations.force
- constant.Declarations.const_body
- with Not_found -> error_no_such_label (con_label con')
- in
- con,constr
- ) constants
- in
- Mod_subst.make_resolver resolve
+ let resolve = List.map (fun (con,_) -> con,None) constants in
+ Mod_subst.make_resolver resolve
(* we assume that the substitution of "mp" into "msid" is already done
(or unnecessary) *)
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 371860f5..2aca6511 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modops.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
+(*i $Id: modops.mli 8721 2006-04-15 15:30:04Z herbelin $ i*)
(*i*)
open Util
@@ -74,7 +74,7 @@ val error_incompatible_labels : label -> label -> 'a
val error_no_such_label : label -> 'a
-val error_result_must_be_signature : module_type_body -> 'a
+val error_result_must_be_signature : unit -> 'a
val error_signature_expected : module_type_body -> 'a
diff --git a/kernel/names.ml b/kernel/names.ml
index 4c8cf7bb..ae5afebd 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: names.ml 7834 2006-01-11 00:15:01Z herbelin $ *)
+(* $Id: names.ml 8852 2006-05-23 17:52:43Z notin $ *)
open Pp
open Util
@@ -198,6 +198,10 @@ let con_label = label
let pr_con = pr_kn
let con_modpath = modpath
+let mind_modpath = modpath
+let ind_modpath ind = mind_modpath (fst ind)
+let constr_modpath c = ind_modpath (fst c)
+
let ith_mutual_inductive (kn,_) i = (kn,i)
let ith_constructor_of_inductive ind i = (ind,i)
let inductive_of_constructor (ind,i) = ind
diff --git a/kernel/names.mli b/kernel/names.mli
index 5b0a7a30..82a638c0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: names.mli 6736 2005-02-18 20:49:04Z herbelin $ i*)
+(*i $Id: names.mli 8852 2006-05-23 17:52:43Z notin $ i*)
(*s Identifiers *)
@@ -134,6 +134,10 @@ val con_label : constant -> label
val con_modpath : constant -> module_path
val pr_con : constant -> Pp.std_ppcmds
+val mind_modpath : mutual_inductive -> module_path
+val ind_modpath : inductive -> module_path
+val constr_modpath : constructor -> module_path
+
val ith_mutual_inductive : inductive -> int -> inductive
val ith_constructor_of_inductive : inductive -> int -> constructor
val inductive_of_constructor : constructor -> inductive
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 5a45c167..947e4675 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pre_env.ml 7642 2005-12-06 08:56:29Z gregoire $ *)
+(* $Id: pre_env.ml 8810 2006-05-12 18:50:21Z barras $ *)
open Util
open Names
@@ -144,3 +144,8 @@ let lookup_constant kn env =
(* Mutual Inductives *)
let lookup_mind kn env =
KNmap.find kn env.env_globals.env_inductives
+
+let rec scrape_mind env kn =
+ match (lookup_mind kn env).mind_equiv with
+ | None -> kn
+ | Some kn' -> scrape_mind env kn'
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index be74decf..2642bc92 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pre_env.mli 7642 2005-12-06 08:56:29Z gregoire $ *)
+(* $Id: pre_env.mli 8810 2006-05-12 18:50:21Z barras $ *)
open Util
open Names
@@ -83,4 +83,7 @@ val lookup_constant : constant -> env -> constant_body
(* Mutual Inductives *)
val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
+(* Find the ultimate inductive in the [mind_equiv] chain *)
+val scrape_mind : env -> mutual_inductive -> mutual_inductive
+
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 6477078a..bd849dad 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: reduction.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
+(* $Id: reduction.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
open Util
open Names
@@ -41,8 +41,8 @@ let compare_stack_shape stk1 stk2 =
([],[]) -> bal=0
| ((Zupdate _|Zshift _)::s1, _) -> compare_rec bal s1 stk2
| (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
- | (Zapp l1::s1, _) -> compare_rec (bal+List.length l1) s1 stk2
- | (_, Zapp l2::s2) -> compare_rec (bal-List.length l2) stk1 s2
+ | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2
+ | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
| (Zcase(c1,_,_)::s1, Zcase(c2,_,_)::s2) ->
bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2
| (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
@@ -50,6 +50,16 @@ let compare_stack_shape stk1 stk2 =
| (_,_) -> false in
compare_rec 0 stk1 stk2
+type lft_constr_stack_elt =
+ Zlapp of (lift * fconstr) array
+ | Zlfix of (lift * fconstr) * lft_constr_stack
+ | Zlcase of case_info * lift * fconstr * fconstr array
+and lft_constr_stack = lft_constr_stack_elt list
+
+let rec zlapp v = function
+ Zlapp v2 :: s -> zlapp (Array.append v v2) s
+ | s -> Zlapp v :: s
+
let pure_stack lfts stk =
let rec pure_rec lfts stk =
match stk with
@@ -58,15 +68,13 @@ let pure_stack lfts stk =
(match (zi,pure_rec lfts s) with
(Zupdate _,lpstk) -> lpstk
| (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
- | (Zapp a1,(l,Zapp a2::pstk)) ->
- (l,Zapp (List.map (fun t -> (l,t)) a1 @ a2)::pstk)
| (Zapp a, (l,pstk)) ->
- (l,Zapp (List.map (fun t -> (l,t)) a)::pstk)
+ (l,zlapp (Array.map (fun t -> (l,t)) a) pstk)
| (Zfix(fx,a),(l,pstk)) ->
let (lfx,pa) = pure_rec l a in
- (l, Zfix((lfx,fx),pa)::pstk)
+ (l, Zlfix((lfx,fx),pa)::pstk)
| (Zcase(ci,p,br),(l,pstk)) ->
- (l,Zcase(ci,(l,p),Array.map (fun t -> (l,t)) br)::pstk)) in
+ (l,Zlcase(ci,l,p,br)::pstk)) in
snd (pure_rec lfts stk)
(****************************************************************************)
@@ -98,10 +106,10 @@ let whd_betadeltaiota_nolet env t =
let beta_appvect c v =
let rec stacklam env t stack =
- match (decomp_stack stack,kind_of_term t) with
- | Some (h,stacktl), Lambda (_,_,c) -> stacklam (h::env) c stacktl
- | _ -> app_stack (substl env t, stack) in
- stacklam [] c (append_stack v empty_stack)
+ match kind_of_term t, stack with
+ Lambda(_,_,c), arg::stacktl -> stacklam (arg::env) c stacktl
+ | _ -> applist (substl env t, stack) in
+ stacklam [] c (Array.to_list v)
(********************************************************************)
(* Conversion *)
@@ -117,17 +125,17 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
let rec cmp_rec pstk1 pstk2 cuniv =
match (pstk1,pstk2) with
| (z1::s1, z2::s2) ->
- let c1 = cmp_rec s1 s2 cuniv in
+ let cu1 = cmp_rec s1 s2 cuniv in
(match (z1,z2) with
- | (Zapp a1,Zapp a2) -> List.fold_right2 f a1 a2 c1
- | (Zfix(fx1,a1),Zfix(fx2,a2)) ->
- let c2 = f fx1 fx2 c1 in
- cmp_rec a1 a2 c2
- | (Zcase(ci1,p1,br1),Zcase(ci2,p2,br2)) ->
+ | (Zlapp a1,Zlapp a2) -> array_fold_right2 f a1 a2 cu1
+ | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
+ let cu2 = f fx1 fx2 cu1 in
+ cmp_rec a1 a2 cu2
+ | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
if not (fmind ci1.ci_ind ci2.ci_ind) then
raise NotConvertible;
- let c2 = f p1 p2 c1 in
- array_fold_right2 f br1 br2 c2
+ let cu2 = f (l1,p1) (l2,p2) cu1 in
+ array_fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2
| _ -> assert false)
| _ -> cuniv in
if compare_stack_shape stk1 stk2 then
@@ -291,10 +299,18 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
convert_stacks infos lft1 lft2 v1 v2 u2
else raise NotConvertible
- | ( (FLetIn _, _) | (_, FLetIn _) | (FCases _,_) | (_,FCases _)
- | (FApp _,_) | (_,FApp _) | (FCLOS _, _) | (_,FCLOS _)
- | (FLIFT _, _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED)) ->
- anomaly "Unexpected term returned by fhnf"
+ (* Can happen because whd_stack on one arg may have side-effects
+ on the other arg and coulb be no more in hnf... *)
+ | ( (FLetIn _, _) | (FCases _,_) | (FApp _,_)
+ | (FCLOS _, _) | (FLIFT _, _)) ->
+ eqappr cv_pb infos (lft1, whd_stack infos hd1 v1) appr2 cuniv
+
+ | ( (_, FLetIn _) | (_,FCases _) | (_,FApp _)
+ | (_,FCLOS _) | (_,FLIFT _)) ->
+ eqappr cv_pb infos (lft1, whd_stack infos hd1 v1) appr2 cuniv
+
+ (* Should not happen because whd_stack unlocks references *)
+ | ((FLOCKED,_) | (_,FLOCKED)) -> assert false
| _ -> raise NotConvertible
@@ -422,7 +438,7 @@ let dest_prod_assum env =
prodec_rec env Sign.empty_rel_context
let dest_arity env c =
- let l, c = dest_prod env c in
+ let l, c = dest_prod_assum env c in
match kind_of_term c with
| Sort s -> l,s
| _ -> error "not an arity"
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 34071182..95092814 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: safe_typing.ml 7602 2005-11-23 15:10:16Z barras $ *)
+(* $Id: safe_typing.ml 8898 2006-06-05 23:15:51Z letouzey $ *)
open Util
open Names
@@ -30,7 +30,6 @@ type modvariant =
| NONE
| SIG of (* funsig params *) (mod_bound_id * module_type_body) list
| STRUCT of (* functor params *) (mod_bound_id * module_type_body) list
- * (* optional result type *) module_type_body option
| LIBRARY of dir_path
type module_info =
@@ -224,36 +223,18 @@ let add_module l me senv =
(* Interactive modules *)
-let start_module l params result senv =
+let start_module l senv =
check_label l senv.labset;
- let rec trans_params env = function
- | [] -> env,[]
- | (mbid,mte)::rest ->
- let mtb = translate_modtype env mte in
- let env =
- full_add_module (MPbound mbid) (module_body_of_type mtb) env
- in
- let env,transrest = trans_params env rest in
- env, (mbid,mtb)::transrest
- in
- let env,params_body = trans_params senv.env params in
- let check_sig mtb = match scrape_modtype env mtb with
- | MTBsig _ -> ()
- | MTBfunsig _ -> error_result_must_be_signature mtb
- | _ -> anomaly "start_module: modtype not scraped"
- in
- let result_body = option_app (translate_modtype env) result in
- ignore (option_app check_sig result_body);
let msid = make_msid senv.modinfo.seed (string_of_label l) in
let mp = MPself msid in
let modinfo = { msid = msid;
modpath = mp;
seed = senv.modinfo.seed;
label = l;
- variant = STRUCT(params_body,result_body) }
+ variant = STRUCT [] }
in
mp, { old = senv;
- env = env;
+ env = senv.env;
modinfo = modinfo;
labset = Labset.empty;
revsign = [];
@@ -261,21 +242,21 @@ let start_module l params result senv =
imports = senv.imports;
loads = [] }
-
-
-let end_module l senv =
+let end_module l restype senv =
let oldsenv = senv.old in
let modinfo = senv.modinfo in
- let params, restype =
+ let restype = option_map (translate_modtype senv.env) restype in
+ let params =
match modinfo.variant with
| NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
- | STRUCT(params,restype) -> (params,restype)
+ | STRUCT params -> params
in
if l <> modinfo.label then error_incompatible_labels l modinfo.label;
if not (empty_context senv.env) then error_local_context None;
- let functorize_type =
- List.fold_right
- (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb))
+ let functorize_type tb =
+ List.fold_left
+ (fun mtb (arg_id,arg_b) -> MTBfunsig (arg_id,arg_b,mtb))
+ tb
params
in
let auto_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
@@ -288,10 +269,10 @@ let end_module l senv =
mtb, Some mtb, cst
in
let mexpr =
- List.fold_right
- (fun (arg_id,arg_b) mtb -> MEBfunctor (arg_id,arg_b,mtb))
- params
+ List.fold_left
+ (fun mtb (arg_id,arg_b) -> MEBfunctor (arg_id,arg_b,mtb))
(MEBstruct (modinfo.msid, List.rev senv.revstruct))
+ params
in
let mb =
{ mod_expr = Some mexpr;
@@ -326,31 +307,44 @@ let end_module l senv =
loads = senv.loads@oldsenv.loads }
+(* Adding parameters to modules or module types *)
+
+let add_module_parameter mbid mte senv =
+ if senv.revsign <> [] or senv.revstruct <> [] or senv.loads <> [] then
+ anomaly "Cannot add a module parameter to a non empty module";
+ let mtb = translate_modtype senv.env mte in
+ let env = full_add_module (MPbound mbid) (module_body_of_type mtb) senv.env
+ in
+ let new_variant = match senv.modinfo.variant with
+ | STRUCT params -> STRUCT ((mbid,mtb) :: params)
+ | SIG params -> SIG ((mbid,mtb) :: params)
+ | _ ->
+ anomaly "Module parameters can only be added to modules or signatures"
+ in
+ { old = senv.old;
+ env = env;
+ modinfo = { senv.modinfo with variant = new_variant };
+ labset = senv.labset;
+ revsign = [];
+ revstruct = [];
+ imports = senv.imports;
+ loads = [] }
+
+
(* Interactive module types *)
-let start_modtype l params senv =
+let start_modtype l senv =
check_label l senv.labset;
- let rec trans_params env = function
- | [] -> env,[]
- | (mbid,mte)::rest ->
- let mtb = translate_modtype env mte in
- let env =
- full_add_module (MPbound mbid) (module_body_of_type mtb) env
- in
- let env,transrest = trans_params env rest in
- env, (mbid,mtb)::transrest
- in
- let env,params_body = trans_params senv.env params in
let msid = make_msid senv.modinfo.seed (string_of_label l) in
let mp = MPself msid in
let modinfo = { msid = msid;
modpath = mp;
seed = senv.modinfo.seed;
label = l;
- variant = SIG params_body }
+ variant = SIG [] }
in
mp, { old = senv;
- env = env;
+ env = senv.env;
modinfo = modinfo;
labset = Labset.empty;
revsign = [];
@@ -370,10 +364,10 @@ let end_modtype l senv =
if not (empty_context senv.env) then error_local_context None;
let res_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
let mtb =
- List.fold_right
- (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb))
- params
+ List.fold_left
+ (fun mtb (arg_id,arg_b) -> MTBfunsig (arg_id,arg_b,mtb))
res_tb
+ params
in
let kn = make_kn oldsenv.modinfo.modpath empty_dirpath l in
let newenv = oldsenv.env in
@@ -520,9 +514,9 @@ let import (dp,mb,depends,engmt) digest senv =
let rec lighten_module mb =
{ mb with
- mod_expr = option_app lighten_modexpr mb.mod_expr;
+ mod_expr = option_map lighten_modexpr mb.mod_expr;
mod_type = lighten_modtype mb.mod_type;
- mod_user_type = option_app lighten_modtype mb.mod_user_type }
+ mod_user_type = option_map lighten_modtype mb.mod_user_type }
and lighten_modtype = function
| MTBident kn as x -> x
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 148a9d9d..c3d0abde 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: safe_typing.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: safe_typing.mli 8723 2006-04-16 15:51:02Z herbelin $ i*)
(*i*)
open Names
@@ -72,17 +72,17 @@ val set_engagement : engagement -> safe_environment -> safe_environment
(*s Interactive module functions *)
val start_module :
- label -> (mod_bound_id * module_type_entry) list
- -> module_type_entry option
- -> safe_environment -> module_path * safe_environment
+ label -> safe_environment -> module_path * safe_environment
val end_module :
- label -> safe_environment -> module_path * safe_environment
+ label -> module_type_entry option
+ -> safe_environment -> module_path * safe_environment
+val add_module_parameter :
+ mod_bound_id -> module_type_entry -> safe_environment -> safe_environment
val start_modtype :
- label -> (mod_bound_id * module_type_entry) list
- -> safe_environment -> module_path * safe_environment
+ label -> safe_environment -> module_path * safe_environment
val end_modtype :
label -> safe_environment -> kernel_name * safe_environment
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 7caf667f..75342f2c 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: sign.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
+(* $Id: sign.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
open Names
open Util
@@ -89,7 +89,7 @@ let push_named_to_rel_context hyps ctxt =
let rec push = function
| (id,b,t) :: l ->
let s, hyps = push l in
- let d = (Name id, option_app (subst_vars s) b, type_app (subst_vars s) t) in
+ let d = (Name id, option_map (subst_vars s) b, type_app (subst_vars s) t) in
id::s, d::hyps
| [] -> [],[] in
let s, hyps = push hyps in
@@ -191,3 +191,4 @@ let decompose_lam_n_assum n =
| c -> error "decompose_lam_n_assum: not enough abstractions"
in
lamdec_rec empty_rel_context n
+
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 94251d90..bbc89e39 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtyping.ml 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: subtyping.ml 8845 2006-05-23 07:41:58Z herbelin $ i*)
(*i*)
open Util
@@ -89,14 +89,15 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
(* nf_arity later *)
(* user_lc ignored *)
(* user_arity ignored *)
- let cst = check_conv cst conv_sort env p1.mind_sort p2.mind_sort in
check (fun p -> p.mind_nrealargs);
(* kelim ignored *)
(* listrec ignored *)
(* finite done *)
(* nparams done *)
(* params_ctxt done *)
- let cst = check_conv cst conv env p1.mind_nf_arity p2.mind_nf_arity in
+ (* Don't check the sort of the type if polymorphic *)
+ let cst = check_conv cst conv env (type_of_inductive (mib1,p1)) (type_of_inductive (mib2,p2))
+ in
cst
in
let check_cons_types i cst p1 p2 =
@@ -181,7 +182,7 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
"name.") ;
assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
if cb2.const_body <> None then error () ;
- let arity1 = mind1.mind_packets.(i).mind_user_arity in
+ let arity1 = type_of_inductive (mind1,mind1.mind_packets.(i)) in
check_conv cst conv_leq env arity1 cb2.const_type
| IndConstr (((kn,i),j) as cstr,mind1) ->
Util.error ("The kernel does not recognize yet that a parameter can be " ^
diff --git a/kernel/term.ml b/kernel/term.ml
index 7060d000..228ae48a 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: term.ml 8049 2006-02-16 10:42:18Z coq $ *)
+(* $Id: term.ml 8850 2006-05-23 16:11:31Z herbelin $ *)
(* This module instantiates the structure of generic deBruijn terms to Coq *)
@@ -643,7 +643,7 @@ let body_of_type ty = ty
type named_declaration = identifier * constr option * types
type rel_declaration = name * constr option * types
-let map_named_declaration f (id, v, ty) = (id, option_app f v, f ty)
+let map_named_declaration f (id, v, ty) = (id, option_map f v, f ty)
let map_rel_declaration = map_named_declaration
(****************************************************************************)
@@ -752,36 +752,34 @@ let rec lift_substituend depth s =
let make_substituend c = { sinfo=Unknown; sit=c }
-let substn_many lamv n =
+let substn_many lamv n c =
let lv = Array.length lamv in
- let rec substrec depth c = match kind_of_term c with
- | Rel k ->
- if k<=depth then
- c
- else if k-depth <= lv then
- lift_substituend depth lamv.(k-depth-1)
- else
- mkRel (k-lv)
- | _ -> map_constr_with_binders succ substrec depth c
- in
- substrec n
+ if lv = 0 then c
+ else
+ let rec substrec depth c = match kind_of_term c with
+ | Rel k ->
+ if k<=depth then c
+ else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1)
+ else mkRel (k-lv)
+ | _ -> map_constr_with_binders succ substrec depth c in
+ substrec n c
(*
let substkey = Profile.declare_profile "substn_many";;
let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;;
*)
-let substnl laml k =
- substn_many (Array.map make_substituend (Array.of_list laml)) k
-let substl laml =
- substn_many (Array.map make_substituend (Array.of_list laml)) 0
+let substnl laml n =
+ substn_many (Array.map make_substituend (Array.of_list laml)) n
+let substl laml = substnl laml 0
let subst1 lam = substl [lam]
-let substl_decl laml (id,bodyopt,typ) =
- match bodyopt with
- | None -> (id,None,substl laml typ)
- | Some body -> (id, Some (substl laml body), type_app (substl laml) typ)
+let substnl_decl laml k (id,bodyopt,typ) =
+ (id,option_map (substnl laml k) bodyopt,substnl laml k typ)
+let substl_decl laml = substnl_decl laml 0
let subst1_decl lam = substl_decl [lam]
+let subst1_named_decl = subst1_decl
+let substl_named_decl = substl_decl
(* (thin_val sigma) removes identity substitutions from sigma *)
diff --git a/kernel/term.mli b/kernel/term.mli
index 0eccd170..8d72e0d8 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: term.mli 8049 2006-02-16 10:42:18Z coq $ i*)
+(*i $Id: term.mli 8850 2006-05-23 16:11:31Z herbelin $ i*)
(*i*)
open Names
@@ -460,8 +460,12 @@ val substnl : constr list -> int -> constr -> constr
val substl : constr list -> constr -> constr
val subst1 : constr -> constr -> constr
-val substl_decl : constr list -> named_declaration -> named_declaration
-val subst1_decl : constr -> named_declaration -> named_declaration
+val substnl_decl : constr list -> int -> rel_declaration -> rel_declaration
+val substl_decl : constr list -> rel_declaration -> rel_declaration
+val subst1_decl : constr -> rel_declaration -> rel_declaration
+
+val subst1_named_decl : constr -> named_declaration -> named_declaration
+val substl_named_decl : constr list -> named_declaration -> named_declaration
val replace_vars : (identifier * constr) list -> constr -> constr
val subst_var : identifier -> constr -> constr
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 3807ecdb..87de6698 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: type_errors.ml 8673 2006-03-29 21:21:52Z herbelin $ *)
+(* $Id: type_errors.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
open Names
open Term
@@ -45,8 +45,8 @@ type type_error =
| NotAType of unsafe_judgment
| BadAssumption of unsafe_judgment
| ReferenceVariables of constr
- | ElimArity of inductive * types list * constr * unsafe_judgment
- * (constr * constr * arity_error) option
+ | ElimArity of inductive * sorts_family list * constr * unsafe_judgment
+ * (sorts_family * sorts_family * arity_error) option
| CaseNotInductive of unsafe_judgment
| WrongCaseInfo of inductive * case_info
| NumberBranches of unsafe_judgment * int
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index c56b174b..138c313c 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: type_errors.mli 6019 2004-08-06 18:15:24Z herbelin $ i*)
+(*i $Id: type_errors.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
(*i*)
open Names
@@ -47,8 +47,8 @@ type type_error =
| NotAType of unsafe_judgment
| BadAssumption of unsafe_judgment
| ReferenceVariables of constr
- | ElimArity of inductive * types list * constr * unsafe_judgment
- * (constr * constr * arity_error) option
+ | ElimArity of inductive * sorts_family list * constr * unsafe_judgment
+ * (sorts_family * sorts_family * arity_error) option
| CaseNotInductive of unsafe_judgment
| WrongCaseInfo of inductive * case_info
| NumberBranches of unsafe_judgment * int
@@ -75,8 +75,8 @@ val error_assumption : env -> unsafe_judgment -> 'a
val error_reference_variables : env -> constr -> 'a
val error_elim_arity :
- env -> inductive -> types list -> constr
- -> unsafe_judgment -> (constr * constr * arity_error) option -> 'a
+ env -> inductive -> sorts_family list -> constr -> unsafe_judgment ->
+ (sorts_family * sorts_family * arity_error) option -> 'a
val error_case_not_inductive : env -> unsafe_judgment -> 'a
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 779a427a..8299a3c9 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: typeops.ml 8673 2006-03-29 21:21:52Z herbelin $ *)
+(* $Id: typeops.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
open Util
open Names
@@ -245,14 +245,28 @@ let judge_of_cast env cj k tj =
(* Inductive types. *)
-let judge_of_inductive env i =
- let constr = mkInd i in
- let _ =
- let (kn,_) = i in
- let mib = lookup_mind kn env in
- check_args env constr mib.mind_hyps in
- let specif = lookup_mind_specif env i in
- make_judge constr (type_of_inductive specif)
+(* The type is parametric over the uniform parameters whose conclusion
+ is in Type; to enforce the internal constraints between the
+ parameters and the instances of Type occurring in the type of the
+ constructors, we use the level variables _statically_ assigned to
+ the conclusions of the parameters as mediators: e.g. if a parameter
+ has conclusion Type(alpha), static constraints of the form alpha<=v
+ exist between alpha and the Type's occurring in the constructor
+ types; when the parameters is finally instantiated by a term of
+ conclusion Type(u), then the constraints u<=alpha is computed in
+ the App case of execute; from this constraints, the expected
+ dynamic constraints of the form u<=v are enforced *)
+
+let judge_of_inductive_knowing_parameters env ind jl =
+ let c = mkInd ind in
+ let (mib,mip) = lookup_mind_specif env ind in
+ check_args env c mib.mind_hyps;
+ let paramstyp = Array.map (fun j -> j.uj_type) jl in
+ let t = Inductive.type_of_inductive_knowing_parameters env mip paramstyp in
+ make_judge c t
+
+let judge_of_inductive env ind =
+ judge_of_inductive_knowing_parameters env ind [||]
(* Constructors. *)
@@ -334,14 +348,15 @@ let rec execute env cstr cu =
(* Lambda calculus operators *)
| App (f,args) ->
- let (j,cu1) = execute env f cu in
- let (jl,cu2) = execute_array env args cu1 in
- let (j',cu) = univ_combinator cu2 (judge_of_apply env j jl) in
- if isInd f then
- (* Sort-polymorphism of inductive types *)
- adjust_inductive_level env (destInd f) args (j',cu)
- else
- (j',cu)
+ let (jl,cu1) = execute_array env args cu in
+ let (j,cu2) =
+ if isInd f then
+ (* Sort-polymorphism of inductive types *)
+ judge_of_inductive_knowing_parameters env (destInd f) jl, cu1
+ else
+ execute env f cu1
+ in
+ univ_combinator cu2 (judge_of_apply env j jl)
| Lambda (name,c1,c2) ->
let (varj,cu1) = execute_type env c1 cu in
@@ -421,22 +436,6 @@ and execute_array env = array_fold_map' (execute env)
and execute_list env = list_fold_map' (execute env)
-and adjust_inductive_level env ind args (j,cu) =
- let specif = lookup_mind_specif env ind in
- if is_small_inductive specif then
- (* No polymorphism *)
- (j,cu)
- else
- (* Retyping constructor with the actual arguments *)
- let env',llc,ls0 = constructor_instances env specif ind args in
- let (llj,cu1) = array_fold_map' (execute_array env') llc cu in
- let ls =
- Array.map (fun lj ->
- max_inductive_sort (Array.map (sort_judgment env) lj)) llj
- in
- let s = find_inductive_level env specif ind ls0 ls in
- (on_judgment_type (set_inductive_level env s) j, cu1)
-
(* Derived functions *)
let infer env constr =
let (j,(cst,_)) =
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 34ecd103..86a795b5 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: typeops.mli 8673 2006-03-29 21:21:52Z herbelin $ i*)
+(*i $Id: typeops.mli 8871 2006-05-28 16:46:48Z herbelin $ i*)
(*i*)
open Names
@@ -78,6 +78,9 @@ val judge_of_cast :
val judge_of_inductive : env -> inductive -> unsafe_judgment
+val judge_of_inductive_knowing_parameters :
+ env -> inductive -> unsafe_judgment array -> unsafe_judgment
+
val judge_of_constructor : env -> constructor -> unsafe_judgment
(*s Type of Cases. *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 23e50282..e76b7b02 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: univ.ml 8673 2006-03-29 21:21:52Z herbelin $ *)
+(* $Id: univ.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+
+(* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
+(* Extension with algebraic universes by HH [Sep 2001] *)
+(* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *)
(* Universes are stratified by a partial ordering $\le$.
Let $\~{}$ be the associated equivalence. We also have a strict ordering
@@ -92,7 +96,7 @@ let sup u v =
let gtl'' = list_union gtl gtl' in
Max (list_subtract gel'' gtl'',gtl'')
-let sup_array ls = Array.fold_right sup ls (Max ([],[]))
+let neutral_univ = Max ([],[])
(* Comparison on this type is pointer equality *)
type canonical_arc =
@@ -125,7 +129,7 @@ let declare_univ u g =
(* The level of Set *)
let base_univ = Atom Base
-let is_base = function
+let is_base_univ = function
| Atom Base -> true
| Max ([Base],[]) -> warning "Non canonical Set"; true
| u -> false
@@ -428,11 +432,11 @@ let make_max = function
| ([u],[]) -> Atom u
| (le,lt) -> Max (le,lt)
-let remove_constraint u = function
+let remove_large_constraint u = function
| Atom u' as x -> if u = u' then Max ([],[]) else x
| Max (le,lt) -> make_max (list_remove u le,lt)
-let is_empty_universe = function
+let is_empty_univ = function
| Max ([],[]) -> true
| _ -> false
@@ -454,22 +458,40 @@ where
- the wi are arbitrary complex universes that do not mention the ui.
*)
+let is_direct_sort_constraint s v = match s with
+ | Some u -> is_direct_constraint u v
+ | None -> false
+
let solve_constraints_system levels level_bounds =
let levels =
- Array.map (function Atom u -> u | _ -> anomaly "expects Atom") levels in
+ Array.map (option_map (function Atom u -> u | _ -> anomaly "expects Atom"))
+ levels in
let v = Array.copy level_bounds in
let nind = Array.length v in
for i=0 to nind-1 do
for j=0 to nind-1 do
- if i<>j & is_direct_constraint levels.(j) v.(i) then
- v.(i) <- sup v.(i) v.(j)
+ if i<>j & is_direct_sort_constraint levels.(j) v.(i) then
+ v.(i) <- sup v.(i) level_bounds.(j)
done;
for j=0 to nind-1 do
- v.(i) <- remove_constraint levels.(j) v.(i)
+ match levels.(j) with
+ | Some u -> v.(i) <- remove_large_constraint u v.(i)
+ | None -> ()
done
done;
v
+let subst_large_constraint u u' v =
+ match u with
+ | Atom u ->
+ if is_direct_constraint u v then sup u' (remove_large_constraint u v)
+ else v
+ | _ ->
+ anomaly "expect a universe level"
+
+let subst_large_constraints =
+ List.fold_right (fun (u,u') -> subst_large_constraint u u')
+
(* Pretty-printing *)
let num_universes g =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index f39f05d9..f3af0861 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: univ.mli 8673 2006-03-29 21:21:52Z herbelin $ i*)
+(*i $Id: univ.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
(* Universes. *)
@@ -14,9 +14,10 @@ type universe
val base_univ : universe
val prop_univ : universe
+val neutral_univ : universe
val make_univ : Names.dir_path * int -> universe
-val is_base : universe -> bool
+val is_base_univ : universe -> bool
(* The type of a universe *)
val super : universe -> universe
@@ -24,9 +25,6 @@ val super : universe -> universe
(* The max of 2 universes *)
val sup : universe -> universe -> universe
-(* The max of an array of universes *)
-val sup_array : universe array -> universe
-
(*s Graphs of universes. *)
type universes
@@ -58,10 +56,15 @@ val merge_constraints : constraints -> universes -> universes
val fresh_local_univ : unit -> universe
-val solve_constraints_system : universe array -> universe array ->
+val solve_constraints_system : universe option array -> universe array ->
universe array
-val is_empty_universe : universe -> bool
+val is_empty_univ : universe -> bool
+
+val subst_large_constraint : universe -> universe -> universe -> universe
+
+val subst_large_constraints :
+ (universe * universe) list -> universe -> universe
(*s Pretty-printing of universes. *)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index f038c04f..653f8978 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -342,8 +342,8 @@ let constr_type_of_idkey env idkey =
mkRel n, lift n ty
let type_of_ind env ind =
- let (_,mip) = Inductive.lookup_mind_specif env ind in
- mip.mind_nf_arity
+ let specif = Inductive.lookup_mind_specif env ind in
+ Inductive.type_of_inductive specif
let build_branches_type (mind,_ as _ind) mib mip params dep p rtbl =
(* [build_one_branch i cty] construit le type de la ieme branche (commence
@@ -461,7 +461,8 @@ and nf_stk env c t stk =
in
let aux =
nf_predicate env (type_of_switch sw)
- (hnf_prod_applist env mip.mind_nf_arity (Array.to_list params)) in
+ (hnf_prod_applist env (type_of_ind env ind) (Array.to_list params))
+ in
!dep,aux in
(* Calcul du type des branches *)
let btypes =
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-28 21:33:15 +0000