From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- kernel/closure.ml | 239 +++++++++----------- kernel/closure.mli | 65 +++--- kernel/cooking.ml | 4 +- kernel/declarations.ml | 61 +++-- kernel/declarations.mli | 29 ++- kernel/environ.ml | 6 +- kernel/environ.mli | 5 +- kernel/esubst.ml | 46 ++-- kernel/esubst.mli | 25 ++- kernel/indtypes.ml | 222 ++++++++++++------- kernel/inductive.ml | 575 +++++++++++++++++++++++------------------------- kernel/inductive.mli | 46 +++- kernel/modops.ml | 36 +-- kernel/modops.mli | 4 +- kernel/names.ml | 6 +- kernel/names.mli | 6 +- kernel/pre_env.ml | 7 +- kernel/pre_env.mli | 5 +- kernel/reduction.ml | 66 +++--- kernel/safe_typing.ml | 100 ++++----- kernel/safe_typing.mli | 14 +- kernel/sign.ml | 5 +- kernel/subtyping.ml | 9 +- kernel/term.ml | 42 ++-- kernel/term.mli | 10 +- kernel/type_errors.ml | 6 +- kernel/type_errors.mli | 10 +- kernel/typeops.ml | 65 +++--- kernel/typeops.mli | 5 +- kernel/univ.ml | 40 +++- kernel/univ.mli | 17 +- kernel/vconv.ml | 7 +- 32 files changed, 949 insertions(+), 834 deletions(-) (limited to 'kernel') 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 @@ -393,90 +393,6 @@ let create mk_cl flgs env = i_tab = Hashtbl.create 17 } -(**********************************************************************) -(* 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 *) @@ -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 @@ -90,33 +90,6 @@ val ref_value_cache: 'a infos -> table_key -> 'a option 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. *) @@ -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 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 @@ -824,14 +804,6 @@ let cfkey = Profile.declare_profile "check_fix";; 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. *) @@ -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 = -- cgit v1.2.3