diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.ml | 40 | ||||
| -rw-r--r-- | kernel/closure.mli | 4 | ||||
| -rw-r--r-- | kernel/environ.ml | 18 | ||||
| -rw-r--r-- | kernel/reduction.ml | 4 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 203 | ||||
| -rw-r--r-- | kernel/term.ml | 232 | ||||
| -rw-r--r-- | kernel/term.mli | 6 | ||||
| -rw-r--r-- | kernel/type_errors.ml | 4 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 8 | ||||
| -rw-r--r-- | kernel/typeops.ml | 103 | ||||
| -rw-r--r-- | kernel/typeops.mli | 16 | ||||
| -rw-r--r-- | kernel/univ.ml | 22 |
12 files changed, 342 insertions, 318 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 714a8be3d..a09368fcd 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -438,9 +438,9 @@ and fterm = | FInd of inductive_path * fconstr array | FConstruct of constructor_path * fconstr array | FApp of fconstr * fconstr array - | FFix of (int array * int) * (fconstr array * name list * fconstr array) + | FFix of (int array * int) * (name array * fconstr array * fconstr array) * constr array * fconstr subs - | FCoFix of int * (fconstr array * name list * fconstr array) + | FCoFix of int * (name array * fconstr array * fconstr array) * constr array * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array | FLambda of name * fconstr * fconstr * constr * fconstr subs @@ -535,18 +535,20 @@ let mk_clos_deep clos_fun env t = { norm = Red; term = FCases (ci, clos_fun env p, clos_fun env c, Array.map (clos_fun env) v) } - | IsFix (op,(tys,lna,bds)) -> + | IsFix (op,(lna,tys,bds)) -> let env' = subs_liftn (Array.length bds) env in { norm = Cstr; - term = FFix (op, (Array.map (clos_fun env) tys, lna, - Array.map (clos_fun env') bds), - bds, env) } - | IsCoFix (op,(tys,lna,bds)) -> + term = FFix + (op,(lna, Array.map (clos_fun env) tys, + Array.map (clos_fun env') bds), + bds, env) } + | IsCoFix (op,(lna,tys,bds)) -> let env' = subs_liftn (Array.length bds) env in { norm = Cstr; - term = FCoFix (op, (Array.map (clos_fun env) tys, lna, - Array.map (clos_fun env') bds), - bds, env) } + term = FCoFix + (op,(lna, Array.map (clos_fun env) tys, + Array.map (clos_fun env') bds), + bds, env) } | IsLambda (n,t,c) -> { norm = Cstr; @@ -590,14 +592,14 @@ let rec to_constr constr_fun lfts v = mkMutCase (ci, constr_fun lfts p, constr_fun lfts c, Array.map (constr_fun lfts) ve) - | FFix (op,(tys,lna,bds),_,_) -> + | FFix (op,(lna,tys,bds),_,_) -> let lfts' = el_liftn (Array.length bds) lfts in - mkFix (op, (Array.map (constr_fun lfts) tys, lna, - Array.map (constr_fun lfts') bds)) - | FCoFix (op,(tys,lna,bds),_,_) -> + mkFix (op, (lna, Array.map (constr_fun lfts) tys, + Array.map (constr_fun lfts') bds)) + | FCoFix (op,(lna,tys,bds),_,_) -> let lfts' = el_liftn (Array.length bds) lfts in - mkCoFix (op, (Array.map (constr_fun lfts) tys, lna, - Array.map (constr_fun lfts') bds)) + mkCoFix (op, (lna, Array.map (constr_fun lfts) tys, + Array.map (constr_fun lfts') bds)) | FApp (f,ve) -> mkApp (constr_fun lfts f, Array.map (constr_fun lfts) ve) @@ -903,9 +905,9 @@ and down_then_up info m stk = FInd(ind, Array.map (kl info) args) | FConstruct(c,args) -> FConstruct(c, Array.map (kl info) args) - | FCoFix(n,(ftys,na,fbds),bds,e) -> - FCoFix(n,(Array.map (kl info) ftys, na, - Array.map (kl info) fbds),bds,e) + | FCoFix(n,(na,ftys,fbds),bds,e) -> + FCoFix(n,(na, Array.map (kl info) ftys, + Array.map (kl info) fbds),bds,e) | FFlex(FConst(sp,args)) -> FFlex(FConst(sp, Array.map (kl info) args)) | FFlex(FEvar((i,args),e)) -> diff --git a/kernel/closure.mli b/kernel/closure.mli index 45088b3ac..3d8fb71f3 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -145,9 +145,9 @@ type fterm = | FInd of inductive_path * fconstr array | FConstruct of constructor_path * fconstr array | FApp of fconstr * fconstr array - | FFix of (int array * int) * (fconstr array * name list * fconstr array) + | FFix of (int array * int) * (name array * fconstr array * fconstr array) * constr array * fconstr subs - | FCoFix of int * (fconstr array * name list * fconstr array) + | FCoFix of int * (name array * fconstr array * fconstr array) * constr array * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array | FLambda of name * fconstr * fconstr * constr * fconstr subs diff --git a/kernel/environ.ml b/kernel/environ.ml index ee4666a63..ac813e233 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -125,11 +125,11 @@ let push_rel_context_to_named_context env = env.env_context.env_rel_context ([],ids_of_named_context sign0,sign0) in subst, (named_context_app (fun _ -> sign) env) -let push_rec_types (typarray,names,_) env = - let vect_lift_type = Array.mapi (fun i t -> lift i t) in - let nlara = - List.combine (List.rev names) (Array.to_list (vect_lift_type typarray)) in - List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara +let push_rec_types (lna,typarray,_) env = + let ctxt = + array_map2_i (fun i na t -> (na, type_app (lift i) t)) lna typarray in + Array.fold_left + (fun e assum -> push_rel_assum assum e) env ctxt let reset_rel_context env = { env with @@ -252,11 +252,11 @@ let hdchar env c = | Name id,_ -> lowercase_first_char id | Anonymous,t -> hdrec 0 (lift (n-k) (body_of_type t)) with Not_found -> "y") - | IsFix ((_,i),(_,ln,_)) -> - let id = match List.nth ln i with Name id -> id | _ -> assert false in + | IsFix ((_,i),(lna,_,_)) -> + let id = match lna.(i) with Name id -> id | _ -> assert false in lowercase_first_char id - | IsCoFix (i,(_,ln,_)) -> - let id = match List.nth ln i with Name id -> id | _ -> assert false in + | IsCoFix (i,(lna,_,_)) -> + let id = match lna.(i) with Name id -> id | _ -> assert false in lowercase_first_char id | IsMeta _|IsEvar _|IsMutCase (_, _, _, _) -> "y" in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 478ffa5a8..312ee83d2 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -803,7 +803,7 @@ and eqappr cv_pb infos appr1 appr2 cuniv = convert_stacks infos lft1 lft2 v1 v2 u1 else raise NotConvertible - | (FFix (op1,(tys1,_,cl1),_,_), FFix(op2,(tys2,_,cl2),_,_)) -> + | (FFix (op1,(_,tys1,cl1),_,_), FFix(op2,(_,tys2,cl2),_,_)) -> if op1 = op2 then let u1 = convert_vect infos el1 el2 tys1 tys2 cuniv in @@ -814,7 +814,7 @@ and eqappr cv_pb infos appr1 appr2 cuniv = convert_stacks infos lft1 lft2 v1 v2 u2 else raise NotConvertible - | (FCoFix (op1,(tys1,_,cl1),_,_), FCoFix(op2,(tys2,_,cl2),_,_)) -> + | (FCoFix (op1,(_,tys1,cl1),_,_), FCoFix(op2,(_,tys2,cl2),_,_)) -> if op1 = op2 then let u1 = convert_vect infos el1 el2 tys1 tys2 cuniv in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d1ca1a52f..7df425894 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -32,145 +32,139 @@ let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t) (* The typing machine without information. *) -let rec execute env cstr = - let cst0 = Constraint.empty in + (* ATTENTION : faudra faire le typage du contexte des Const, + MutInd et MutConstructsi un jour cela devient des constructions + arbitraires et non plus des variables *) + +let univ_combinator (cst,univ) (j,c') = + (j,(Constraint.union cst c', merge_constraints c' univ)) + +let rec execute env cstr cu = match kind_of_term cstr with | IsMeta _ -> anomaly "the kernel does not understand metas" | IsEvar _ -> anomaly "the kernel does not understand existential variables" - - | IsRel n -> - (relative env Evd.empty n, cst0) - - | IsVar id -> - (make_judge cstr (lookup_named_type id env), cst0) - - (* ATTENTION : faudra faire le typage du contexte des Const, - MutInd et MutConstructsi un jour cela devient des constructions - arbitraires et non plus des variables *) - | IsConst c -> - (make_judge cstr (type_of_constant env Evd.empty c), cst0) - - | IsMutInd ind -> - (make_judge cstr (type_of_inductive env Evd.empty ind), cst0) - - | IsMutConstruct c -> - (make_judge cstr (type_of_constructor env Evd.empty c), cst0) - - | IsMutCase (ci,p,c,lf) -> - let (cj,cst1) = execute env c in - let (pj,cst2) = execute env p in - let (lfj,cst3) = execute_array env lf in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (type_of_case env Evd.empty ci pj cj lfj, cst) - - | IsFix ((vn,i as vni),(lar,lfi,vdef)) -> - if array_exists (fun n -> n < 0) vn then - error "General Fixpoints not allowed"; - let (larjv,vdefv,cst) = execute_fix env lar lfi vdef in - let larv = Array.map body_of_type larjv in - let fix = (vni,(larv,lfi,vdefv)) in - check_fix env Evd.empty fix; - (make_judge (mkFix fix) larjv.(i), cst) - - | IsCoFix (i,(lar,lfi,vdef)) -> - let (larjv,vdefv,cst) = execute_fix env lar lfi vdef in - let larv = Array.map body_of_type larjv in - let cofix = (i,(larv,lfi,vdefv)) in - check_cofix env Evd.empty cofix; - (make_judge (mkCoFix cofix) larjv.(i), cst) - | IsSort (Prop c) -> - (judge_of_prop_contents c, cst0) + (judge_of_prop_contents c, cu) | IsSort (Type u) -> let inst_u = if u == dummy_univ then new_univ() else u in - judge_of_type inst_u - + univ_combinator cu (judge_of_type inst_u) + | IsApp (f,args) -> - let (j,cst1) = execute env f in - let (jl,cst2) = execute_array env args in - let (j,cst3) = - apply_rel_list env Evd.empty false (Array.to_list jl) j in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (j, cst) + let (j,cu1) = execute env f cu in + let (jl,cu2) = execute_array env args cu1 in + univ_combinator cu2 + (apply_rel_list env Evd.empty false (Array.to_list jl) j) | IsLambda (name,c1,c2) -> - let (j,cst1) = execute env c1 in + let (j,cu1) = execute env c1 cu in let var = assumption_of_judgment env Evd.empty j in let env1 = push_rel_assum (name,var) env in - let (j',cst2) = execute env1 c2 in - let (j,cst3) = abs_rel env1 Evd.empty name var j' in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (j, cst) + let (j',cu2) = execute env1 c2 cu1 in + univ_combinator cu2 (abs_rel env1 Evd.empty name var j') - | IsProd (name,c1,c2) -> - let (j,cst1) = execute env c1 in + | IsProd (name,c1,c2) -> + let (j,cu1) = execute env c1 cu in let varj = type_judgment env Evd.empty j in let env1 = push_rel_assum (name,varj.utj_val) env in - let (j',cst2) = execute env1 c2 in + let (j',cu2) = execute env1 c2 cu1 in let varj' = type_judgment env Evd.empty j' in - let (j,cst3) = gen_rel env1 Evd.empty name varj varj' in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (j, cst) - - | IsLetIn (name,c1,c2,c3) -> - let (j1,cst1) = execute env c1 in - let (j2,cst2) = execute env c2 in - let tj2 = assumption_of_judgment env Evd.empty j2 in - let ({uj_val = b; uj_type = t},cst0) = cast_rel env Evd.empty j1 tj2 in - let (j3,cst3) = execute (push_rel_def (name,b,t) env) c3 in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - ({ uj_val = mkLetIn (name, j1.uj_val, tj2, j3.uj_val) ; - uj_type = type_app (subst1 j1.uj_val) j3.uj_type }, - Constraint.union cst cst0) + univ_combinator cu2 + (gen_rel env1 Evd.empty name varj varj') + + | IsLetIn (name,c1,c2,c3) -> + let (j,cu1) = execute env (mkCast(c1,c2)) cu in + let env1 = push_rel_def (name,j.uj_val,j.uj_type) env in + let (j',cu2) = execute env1 c3 cu1 in + univ_combinator cu2 + (judge_of_letin env1 Evd.empty name j j') | IsCast (c,t) -> - let (cj,cst1) = execute env c in - let (tj,cst2) = execute env t in + let (cj,cu1) = execute env c cu in + let (tj,cu2) = execute env t cu1 in let tj = assumption_of_judgment env Evd.empty tj in - let cst = Constraint.union cst1 cst2 in - let (j, cst0) = cast_rel env Evd.empty cj tj in - (j, Constraint.union cst cst0) + univ_combinator cu2 + (cast_rel env Evd.empty cj tj) + + | IsRel n -> + (relative env Evd.empty n, cu) + + | IsVar id -> + (make_judge cstr (lookup_named_type id env), cu) + + | IsConst c -> + (make_judge cstr (type_of_constant env Evd.empty c), cu) + + (* Inductive types *) + | IsMutInd ind -> + (make_judge cstr (type_of_inductive env Evd.empty ind), cu) + + | IsMutConstruct c -> + (make_judge cstr (type_of_constructor env Evd.empty c), cu) + + | IsMutCase (ci,p,c,lf) -> + let (cj,cu1) = execute env c cu in + let (pj,cu2) = execute env p cu1 in + let (lfj,cu3) = execute_array env lf cu2 in + univ_combinator cu3 + (judge_of_case env Evd.empty ci pj cj lfj) + + | IsFix ((vn,i as vni),recdef) -> + if array_exists (fun n -> n < 0) vn then + error "General Fixpoints not allowed"; + let ((_,tys,_ as recdef'),cu1) = execute_fix env recdef cu in + let fix = (vni,recdef') in + check_fix env Evd.empty fix; + (make_judge (mkFix fix) tys.(i), cu1) + + | IsCoFix (i,recdef) -> + let ((_,tys,_ as recdef'),cu1) = execute_fix env recdef cu in + let cofix = (i,recdef') in + check_cofix env Evd.empty cofix; + (make_judge (mkCoFix cofix) tys.(i), cu1) -and execute_fix env lar lfi vdef = - let (larj,cst1) = execute_array env lar in +and execute_fix env (names,lar,vdef) cu = + let (larj,cu1) = execute_array env lar cu in let lara = Array.map (assumption_of_judgment env Evd.empty) larj in - let nlara = - List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in - let env1 = - List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara in - let (vdefj,cst2) = execute_array env1 vdef in + let env1 = push_rec_types (names,lara,vdef) env in + let (vdefj,cu2) = execute_array env1 vdef cu1 in let vdefv = Array.map j_val vdefj in - let cst3 = type_fixpoint env1 Evd.empty lfi lara vdefj in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (lara,vdefv,cst) + let cst = type_fixpoint env1 Evd.empty names lara vdefj in + univ_combinator cu2 ((names,lara,vdefv),cst) -and execute_array env v = - let (jl,u1) = execute_list env (Array.to_list v) in - (Array.of_list jl, u1) +and execute_array env v cu = + let (jl,cu1) = execute_list env (Array.to_list v) cu in + (Array.of_list jl, cu1) -and execute_list env = function +and execute_list env l cu = + match l with | [] -> - ([], Constraint.empty) + ([], cu) | c::r -> - let (j,cst1) = execute env c in - let (jr,cst2) = execute_list env r in - (j::jr, Constraint.union cst1 cst2) + let (j,cu1) = execute env c cu in + let (jr,cu2) = execute_list env r cu1 in + (j::jr, cu2) (* The typed type of a judgment. *) -let execute_type env constr = - let (j,cst) = execute env constr in - (type_judgment env Evd.empty j, cst) +let execute_type env constr cu = + let (j,cu1) = execute env constr cu in + (type_judgment env Evd.empty j, cu1) -(* Renaming for the following. *) +(* Exported machines. *) -let safe_infer = execute +let safe_infer env constr = + let (j,(cst,_)) = + execute env constr (Constraint.empty, universes env) in + (j, cst) -let safe_infer_type = execute_type +let safe_infer_type env constr = + let (j,(cst,_)) = + execute_type env constr (Constraint.empty, universes env) in + (j, cst) (* Typing of several terms. *) @@ -474,7 +468,6 @@ let env_of_safe_env e = e let typing env c = let (j,cst) = safe_infer env c in - let _ = add_constraints cst env in j let typing_in_unsafe_env = typing diff --git a/kernel/term.ml b/kernel/term.ml index 5d7be75ee..65cb495cd 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -70,7 +70,7 @@ type existential = existential_key * constr array type constant = section_path * constr array type constructor = constructor_path * constr array type inductive = inductive_path * constr array -type rec_declaration = constr array * name list * constr array +type rec_declaration = name array * constr array * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration @@ -134,7 +134,7 @@ type 'constr constant = constant_path * 'constr array type 'constr constructor = constructor_path * 'constr array type 'constr inductive = inductive_path * 'constr array type ('constr, 'types) rec_declaration = - 'types array * name list * 'constr array + name array * 'types array * 'constr array type ('constr, 'types) fixpoint = (int array * int) * ('constr, 'types) rec_declaration type ('constr, 'types) cofixpoint = @@ -170,7 +170,7 @@ type existential = existential_key * constr array type constant = constant_path * constr array type constructor = constructor_path * constr array type inductive = inductive_path * constr array -type rec_declaration = constr array * name list * constr array +type rec_declaration = name array * constr array * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration @@ -197,15 +197,19 @@ let comp_term t1 t2 = c1 == c2 & array_for_all2 (==) l1 l2 | IsMutCase (ci1,p1,c1,bl1), IsMutCase (ci2,p2,c2,bl2) -> ci1 == ci2 & p1 == p2 & c1 == c2 & array_for_all2 (==) bl1 bl2 - | IsFix (ln1,(tl1,lna1,bl1)), IsFix (ln2,(tl2,lna2,bl2)) -> - lna1 == lna2 & ln1 = ln2 - & array_for_all2 (==) tl1 tl2 & array_for_all2 (==) bl1 bl2 - | IsCoFix(ln1,(tl1,lna1,bl1)), IsCoFix(ln2,(tl2,lna2,bl2)) -> - lna1 == lna2 & ln1 = ln2 - & array_for_all2 (==) tl1 tl2 & array_for_all2 (==) bl1 bl2 + | IsFix (ln1,(lna1,tl1,bl1)), IsFix (ln2,(lna2,tl2,bl2)) -> + ln1 = ln2 + & array_for_all2 (==) lna1 lna2 + & array_for_all2 (==) tl1 tl2 + & array_for_all2 (==) bl1 bl2 + | IsCoFix(ln1,(lna1,tl1,bl1)), IsCoFix(ln2,(lna2,tl2,bl2)) -> + ln1 = ln2 + & array_for_all2 (==) lna1 lna2 + & array_for_all2 (==) tl1 tl2 + & array_for_all2 (==) bl1 bl2 | _ -> false -let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id,sh_str)) t = +let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id)) t = match t with | IsRel _ | IsMeta _ -> t | IsVar x -> IsVar (sh_id x) @@ -222,10 +226,14 @@ let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id,sh_str)) t = IsMutConstruct (((sh_sp sp,i),j), Array.map sh_rec l) | IsMutCase (ci,p,c,bl) -> (* TO DO: extract ind_sp *) IsMutCase (ci, sh_rec p, sh_rec c, Array.map sh_rec bl) - | IsFix (ln,(tl,lna,bl)) -> - IsFix (ln,(Array.map sh_rec tl,List.map sh_na lna,Array.map sh_rec bl)) - | IsCoFix(ln,(tl,lna,bl)) -> - IsCoFix (ln,(Array.map sh_rec tl,List.map sh_na lna,Array.map sh_rec bl)) + | IsFix (ln,(lna,tl,bl)) -> + IsFix (ln,(Array.map sh_na lna, + Array.map sh_rec tl, + Array.map sh_rec bl)) + | IsCoFix(ln,(lna,tl,bl)) -> + IsCoFix (ln,(Array.map sh_na lna, + Array.map sh_rec tl, + Array.map sh_rec bl)) module Hconstr = Hashcons.Make( @@ -233,15 +241,14 @@ module Hconstr = type t = constr type u = (constr -> constr) * ((sorts -> sorts) * (section_path -> section_path) - * (name -> name) * (identifier -> identifier) - * (string -> string)) + * (name -> name) * (identifier -> identifier)) let hash_sub = hash_term let equal = comp_term let hash = Hashtbl.hash end) -let hcons_term (hsorts,hsp,hname,hident,hstr) = - Hashcons.recursive_hcons Hconstr.f (hsorts,hsp,hname,hident,hstr) +let hcons_term (hsorts,hsp,hname,hident) = + Hashcons.recursive_hcons Hconstr.f (hsorts,hsp,hname,hident) (* Constructs a DeBrujin index with number n *) let mkRel n = IsRel n @@ -502,11 +509,11 @@ let destCase c = match kind_of_term c with | _ -> anomaly "destCase" let destFix c = match kind_of_term c with - | IsFix ((recindxs,i),(types,funnames,bodies) as fix) -> fix + | IsFix fix -> fix | _ -> invalid_arg "destFix" let destCoFix c = match kind_of_term c with - | IsCoFix (i,(types,funnames,bodies) as cofix) -> cofix + | IsCoFix cofix -> cofix | _ -> invalid_arg "destCoFix" (******************************************************************) @@ -562,10 +569,12 @@ let fold_constr f acc c = match kind_of_term c with | IsMutInd (_,l) -> Array.fold_left f acc l | IsMutConstruct (_,l) -> Array.fold_left f acc l | IsMutCase (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl - | IsFix (_,(tl,_,bl)) -> - array_fold_left2 (fun acc b t -> f (f acc b) t) acc bl tl - | IsCoFix (_,(tl,_,bl)) -> - array_fold_left2 (fun acc b t -> f (f acc b) t) acc bl tl + | IsFix (_,(lna,tl,bl)) -> + let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in + Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd + | IsCoFix (_,(lna,tl,bl)) -> + let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in + Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd (* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate subterms of [c] starting from [acc] and proceeding from left to @@ -586,12 +595,14 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with | IsMutInd (_,l) -> Array.fold_left (f n) acc l | IsMutConstruct (_,l) -> Array.fold_left (f n) acc l | IsMutCase (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl - | IsFix (_,(tl,_,bl)) -> + | IsFix (_,(lna,tl,bl)) -> let n' = iterate g (Array.length tl) n in - array_fold_left2 (fun acc b t -> f n (f n' acc b) t) acc bl tl - | IsCoFix (_,(tl,_,bl)) -> + let fd = array_map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd + | IsCoFix (_,(lna,tl,bl)) -> let n' = iterate g (Array.length tl) n in - array_fold_left2 (fun acc b t -> f n (f n' acc b) t) acc bl tl + let fd = array_map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd (* [iter_constr f c] iters [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is @@ -609,8 +620,8 @@ let iter_constr f c = match kind_of_term c with | IsMutInd (_,l) -> Array.iter f l | IsMutConstruct (_,l) -> Array.iter f l | IsMutCase (_,p,c,bl) -> f p; f c; Array.iter f bl - | IsFix (_,(tl,_,bl)) -> Array.iter f tl; Array.iter f bl - | IsCoFix (_,(tl,_,bl)) -> Array.iter f tl; Array.iter f bl + | IsFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl + | IsCoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl (* [iter_constr_with_binders g f n c] iters [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift @@ -630,10 +641,12 @@ let iter_constr_with_binders g f n c = match kind_of_term c with | IsMutInd (_,l) -> Array.iter (f n) l | IsMutConstruct (_,l) -> Array.iter (f n) l | IsMutCase (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl - | IsFix (_,(tl,_,bl)) -> - Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl - | IsCoFix (_,(tl,_,bl)) -> - Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl + | IsFix (_,(_,tl,bl)) -> + Array.iter (f n) tl; + Array.iter (f (iterate g (Array.length tl) n)) bl + | IsCoFix (_,(_,tl,bl)) -> + Array.iter (f n) tl; + Array.iter (f (iterate g (Array.length tl) n)) bl (* [map_constr f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is @@ -651,8 +664,10 @@ let map_constr f c = match kind_of_term c with | IsMutInd (c,l) -> mkMutInd (c, Array.map f l) | IsMutConstruct (c,l) -> mkMutConstruct (c, Array.map f l) | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f p, f c, Array.map f bl) - | IsFix (ln,(tl,lna,bl)) -> mkFix (ln,(Array.map f tl,lna,Array.map f bl)) - | IsCoFix(ln,(tl,lna,bl)) -> mkCoFix (ln,(Array.map f tl,lna,Array.map f bl)) + | IsFix (ln,(lna,tl,bl)) -> + mkFix (ln,(lna,Array.map f tl,Array.map f bl)) + | IsCoFix(ln,(lna,tl,bl)) -> + mkCoFix (ln,(lna,Array.map f tl,Array.map f bl)) (* [map_constr_with_binders g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift @@ -672,12 +687,12 @@ let map_constr_with_binders g f l c = match kind_of_term c with | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al) | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al) | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl) - | IsFix (ln,(tl,lna,bl)) -> + | IsFix (ln,(lna,tl,bl)) -> let l' = iterate g (Array.length tl) l in - mkFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) - | IsCoFix(ln,(tl,lna,bl)) -> + mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) + | IsCoFix(ln,(lna,tl,bl)) -> let l' = iterate g (Array.length tl) l in - mkCoFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) + mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate subterms of [c]; it carries an extra data [l] (typically a name @@ -697,12 +712,12 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al) | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al) | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl) - | IsFix (ln,(tl,lna,bl)) -> - let l' = List.fold_right g lna l in - mkFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) - | IsCoFix(ln,(tl,lna,bl)) -> - let l' = List.fold_right g lna l in - mkCoFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) + | IsFix (ln,(lna,tl,bl)) -> + let l' = Array.fold_left (fun l na -> g na l) l lna in + mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) + | IsCoFix(ln,(lna,tl,bl)) -> + let l' = Array.fold_left (fun l na -> g na l) l lna in + mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) (* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically @@ -752,14 +767,14 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with | IsMutCase (ci,p,c,bl) -> let p' = f l p in let c' = f l c in mkMutCase (ci, p', c', array_map_left (f l) bl) - | IsFix (ln,(tl,lna,bl)) -> + | IsFix (ln,(lna,tl,bl)) -> let l' = iterate g (Array.length tl) l in - let tl', bl' = array_map_left_pair (f l) tl (f l') bl in - mkFix (ln,(tl',lna,bl')) - | IsCoFix(ln,(tl,lna,bl)) -> + let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in + mkFix (ln,(lna,tl',bl')) + | IsCoFix(ln,(lna,tl,bl)) -> let l' = iterate g (Array.length tl) l in - let tl', bl' = array_map_left_pair (f l) tl (f l') bl in - mkCoFix (ln,(tl',lna,bl')) + let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in + mkCoFix (ln,(lna,tl',bl')) (* strong *) let map_constr_with_full_binders g f l c = match kind_of_term c with @@ -774,14 +789,14 @@ let map_constr_with_full_binders g f l c = match kind_of_term c with | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al) | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al) | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl) - | IsFix (ln,(tl,lna,bl)) -> - let tll = Array.to_list tl in - let l' = List.fold_right2 (fun na t l -> g (na,None,t) l) lna tll l in - mkFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) - | IsCoFix(ln,(tl,lna,bl)) -> - let tll = Array.to_list tl in - let l' = List.fold_right2 (fun na t l -> g (na,None,t) l) lna tll l in - mkCoFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) + | IsFix (ln,(lna,tl,bl)) -> + let l' = + array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in + mkFix (ln,(lna,Array.map (f l) tl, Array.map (f l') bl)) + | IsCoFix(ln,(lna,tl,bl)) -> + let l' = + array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in + mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) (* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed; Cast's, @@ -815,9 +830,9 @@ let compare_constr f t1 t2 = c1 = c2 & array_for_all2 f l1 l2 | IsMutCase (_,p1,c1,bl1), IsMutCase (_,p2,c2,bl2) -> f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2 - | IsFix (ln1,(tl1,_,bl1)), IsFix (ln2,(tl2,_,bl2)) -> + | IsFix (ln1,(_,tl1,bl1)), IsFix (ln2,(_,tl2,bl2)) -> ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 - | IsCoFix(ln1,(tl1,_,bl1)), IsCoFix(ln2,(tl2,_,bl2)) -> + | IsCoFix(ln1,(_,tl1,bl1)), IsCoFix(ln2,(_,tl2,bl2)) -> ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 | _ -> false @@ -1132,37 +1147,38 @@ let mkMutCase = mkMutCase let mkMutCaseL (ci, p, c, ac) = mkMutCase (ci, p, c, Array.of_list ac) (* If recindxs = [|i1,...in|] + funnames = [|f1,...fn|] typarray = [|t1,...tn|] - funnames = [f1,.....fn] + bodies = [|b1,...bn|] then - mkFix recindxs i typarray funnames bodies + mkFix ((recindxs,i),(funnames,typarray,bodies)) constructs the ith function of the block - Fixpoint f1 [ctx1] = b1 - with f2 [ctx2] = b2 + Fixpoint f1 [ctx1] : t1 := b1 + with f2 [ctx2] : t2 := b2 ... - with fn [ctxn] = bn. + with fn [ctxn] : tn := bn. where the lenght of the jth context is ij. *) let mkFix = mkFix -(* If typarray = [|t1,...tn|] - funnames = [f1,.....fn] - bodies = [b1,.....bn] - then +(* If funnames = [|f1,...fn|] + typarray = [|t1,...tn|] + bodies = [|b1,...bn|] + then - mkCoFix i typsarray funnames bodies + mkCoFix (i,(funnames,typsarray,bodies)) constructs the ith function of the block - CoFixpoint f1 = b1 - with f2 = b2 + CoFixpoint f1 : t1 := b1 + with f2 : t2 := b2 ... - with fn = bn. + with fn : tn := bn. *) let mkCoFix = mkCoFix @@ -1686,8 +1702,8 @@ let hsort _ _ s = s let hcons_constr (hspcci,hspfw,hname,hident,hstr) = let hsortscci = Hashcons.simple_hcons hsort hspcci in let hsortsfw = Hashcons.simple_hcons hsort hspfw in - let hcci = hcons_term (hsortscci,hspcci,hname,hident,hstr) in - let hfw = hcons_term (hsortsfw,hspfw,hname,hident,hstr) in + let hcci = hcons_term (hsortscci,hspcci,hname,hident) in + let hfw = hcons_term (hsortsfw,hspfw,hname,hident) in let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in (hcci,hfw,htcci) @@ -1710,7 +1726,7 @@ type constr_operator = | OpMutInd of inductive_path | OpMutConstruct of constructor_path | OpMutCase of case_info - | OpRec of fix_kind * name list + | OpRec of fix_kind * name array let splay_constr c = match kind_of_term c with | IsRel n -> OpRel n, [||] @@ -1727,8 +1743,8 @@ let splay_constr c = match kind_of_term c with | IsMutInd (ind_sp, l) -> OpMutInd ind_sp, l | IsMutConstruct (cstr_sp,l) -> OpMutConstruct cstr_sp, l | IsMutCase (ci,p,c,bl) -> OpMutCase ci, Array.append [|p;c|] bl - | IsFix (fi,(tl,lna,bl)) -> OpRec (RFix fi,lna), Array.append tl bl - | IsCoFix (fi,(tl,lna,bl)) -> OpRec (RCoFix fi,lna), Array.append tl bl + | IsFix (fi,(lna,tl,bl)) -> OpRec (RFix fi,lna), Array.append tl bl + | IsCoFix (fi,(lna,tl,bl)) -> OpRec (RCoFix fi,lna), Array.append tl bl let gather_constr = function | OpRel n, [||] -> mkRel n @@ -1747,24 +1763,14 @@ let gather_constr = function | OpMutCase ci, v -> let p = v.(0) and c = v.(1) and bl = Array.sub v 2 (Array.length v -2) in mkMutCase (ci, p, c, bl) - | OpRec (RFix fi,lna), a -> + | OpRec (RFix fi,na), a -> let n = Array.length a / 2 in - mkFix (fi,(Array.sub a 0 n, lna, Array.sub a n n)) - | OpRec (RCoFix i,lna), a -> + mkFix (fi,(na, Array.sub a 0 n, Array.sub a n n)) + | OpRec (RCoFix i,na), a -> let n = Array.length a / 2 in - mkCoFix (i,(Array.sub a 0 n, lna, Array.sub a n n)) + mkCoFix (i,(na, Array.sub a 0 n, Array.sub a n n)) | _ -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed splayed constr">] -let rec mycombine l1 l3 = - match (l1, l3) with - ([], []) -> [] - | (a1::l1, a3::l3) -> (a1, None, a3) :: mycombine l1 l3 - | (_, _) -> invalid_arg "mycombine" - -let rec mysplit = function - [] -> ([], []) - | (x, _, z)::l -> let (rx, rz) = mysplit l in (x::rx, z::rz) - let splay_constr_with_binders c = match kind_of_term c with | IsRel n -> OpRel n, [], [||] | IsVar id -> OpVar id, [], [||] @@ -1774,25 +1780,25 @@ let splay_constr_with_binders c = match kind_of_term c with | IsProd (x, t1, t2) -> OpProd x, [x,None,t1], [|t2|] | IsLambda (x, t1, t2) -> OpLambda x, [x,None,t1], [|t2|] | IsLetIn (x, b, t1, t2) -> OpLetIn x, [x,Some b,t1], [|t2|] - | IsApp (f,v) -> OpApp, [], Array.append [|f|] v + | IsApp (f,v) -> OpApp, [], Array.append [|f|] v | IsConst (sp, a) -> OpConst sp, [], a | IsEvar (sp, a) -> OpEvar sp, [], a | IsMutInd (ind_sp, l) -> OpMutInd ind_sp, [], l | IsMutConstruct (cstr_sp,l) -> OpMutConstruct cstr_sp, [], l | IsMutCase (ci,p,c,bl) -> let v = Array.append [|p;c|] bl in OpMutCase ci, [], v - | IsFix (fi,(tl,lna,bl)) -> + | IsFix (fi,(na,tl,bl)) -> let n = Array.length bl in - let ctxt = mycombine - (List.rev lna) - (Array.to_list (Array.mapi lift tl)) in - OpRec (RFix fi,lna), ctxt, bl - | IsCoFix (fi,(tl,lna,bl)) -> + let ctxt = + Array.to_list + (array_map2_i (fun i x t -> (x,None,lift i t)) na tl) in + OpRec (RFix fi,na), ctxt, bl + | IsCoFix (fi,(na,tl,bl)) -> let n = Array.length bl in - let ctxt = mycombine - (List.rev lna) - (Array.to_list (Array.mapi lift tl)) in - OpRec (RCoFix fi,lna), ctxt, bl + let ctxt = + Array.to_list + (array_map2_i (fun i x t -> (x,None,lift i t)) na tl) in + OpRec (RCoFix fi,na), ctxt, bl let gather_constr_with_binders = function | OpRel n, [], [||] -> mkRel n @@ -1811,14 +1817,14 @@ let gather_constr_with_binders = function | OpMutCase ci, [], v -> let p = v.(0) and c = v.(1) and bl = Array.sub v 2 (Array.length v -2) in mkMutCase (ci, p, c, bl) - | OpRec (RFix fi,lna), ctxt, bl -> - let (lna, tl) = mysplit ctxt in - let tl = Array.mapi (fun i -> lift (-i)) (Array.of_list tl) in - mkFix (fi,(tl, List.rev lna, bl)) - | OpRec (RCoFix i,lna), ctxt, bl -> - let (lna, tl) = mysplit ctxt in - let tl = Array.mapi (fun i -> lift (-i)) (Array.of_list tl) in - mkCoFix (i,(tl, List.rev lna, bl)) + | OpRec (RFix fi,na), ctxt, bl -> + let tl = + Array.mapi (fun i (_,_,t) -> lift (-i) t) (Array.of_list ctxt) in + mkFix (fi,(na, tl, bl)) + | OpRec (RCoFix i,na), ctxt, bl -> + let tl = + Array.mapi (fun i (_,_,t) -> lift (-i) t) (Array.of_list ctxt) in + mkCoFix (i,(na, tl, bl)) | _ -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed splayed constr">] let generic_fold_left f acc bl tl = diff --git a/kernel/term.mli b/kernel/term.mli index c8f6ea4a1..e873525ce 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -48,7 +48,7 @@ type 'constr constant = constant_path * 'constr array type 'constr constructor = constructor_path * 'constr array type 'constr inductive = inductive_path * 'constr array type ('constr, 'types) rec_declaration = - 'types array * name list * 'constr array + name array * 'types array * 'constr array type ('constr, 'types) fixpoint = (int array * int) * ('constr, 'types) rec_declaration type ('constr, 'types) cofixpoint = @@ -124,7 +124,7 @@ type existential = existential_key * constr array type constant = constant_path * constr array type constructor = constructor_path * constr array type inductive = inductive_path * constr array -type rec_declaration = types array * name list * constr array +type rec_declaration = name array * types array * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration @@ -561,7 +561,7 @@ type constr_operator = | OpMutInd of inductive_path | OpMutConstruct of constructor_path | OpMutCase of case_info - | OpRec of fix_kind * Names.name list + | OpRec of fix_kind * name array val splay_constr : constr -> constr_operator * constr array diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 387b7a930..320a30369 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -49,8 +49,8 @@ type type_error = | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment list | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment list - | IllFormedRecBody of guard_error * name list * int * constr array - | IllTypedRecBody of int * name list * unsafe_judgment array + | IllFormedRecBody of guard_error * name array * int * constr array + | IllTypedRecBody of int * name array * unsafe_judgment array * types array exception TypeError of path_kind * env * type_error diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index e022be01d..277e5ca4e 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -53,8 +53,8 @@ type type_error = | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment list | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment list - | IllFormedRecBody of guard_error * name list * int * constr array - | IllTypedRecBody of int * name list * unsafe_judgment array + | IllFormedRecBody of guard_error * name array * int * constr array + | IllTypedRecBody of int * name array * unsafe_judgment array * types array exception TypeError of path_kind * env * type_error @@ -94,9 +94,9 @@ val error_cant_apply_bad_type : unsafe_judgment -> unsafe_judgment list -> 'b val error_ill_formed_rec_body : - path_kind -> env -> guard_error -> name list -> int -> constr array -> 'b + path_kind -> env -> guard_error -> name array -> int -> constr array -> 'b val error_ill_typed_rec_body : - path_kind -> env -> int -> name list -> unsafe_judgment array + path_kind -> env -> int -> name array -> unsafe_judgment array -> types array -> 'b diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 997db29c3..37106b200 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -170,6 +170,14 @@ let abs_rel env sigma name var j = uj_type = mkProd (name, var, j.uj_type) }, Constraint.empty +let judge_of_letin env sigma name defj j = + let v = match kind_of_term defj.uj_val with + IsCast(c,t) -> c + | _ -> defj.uj_val in + ({ uj_val = mkLetIn (name, v, defj.uj_type, j.uj_val) ; + uj_type = type_app (subst1 v) j.uj_type }, + Constraint.empty) + (* [gen_rel env sigma name (typ1,s1) (typ2,s2)] implements the rule env |- typ1:s1 env, name:typ |- typ2 : s2 @@ -282,38 +290,38 @@ let error_elim_expln env sigma kp ki = exception Arity of (constr * constr * string) option let is_correct_arity env sigma kelim (c,p) indf (pt,t) = - let rec srec (pt,t) = + let rec srec (pt,t) u = let pt' = whd_betadeltaiota env sigma pt in let t' = whd_betadeltaiota env sigma t in match kind_of_term pt', kind_of_term t' with | IsProd (_,a1,a2), IsProd (_,a1',a2') -> - if is_conv env sigma a1 a1' then - srec (a2,a2') - else - raise (Arity None) + let univ = + try conv env sigma a1 a1' + with NotConvertible -> raise (Arity None) in + srec (a2,a2') (Constraint.union u univ) | IsProd (_,a1,a2), _ -> let k = whd_betadeltaiota env sigma a2 in let ksort = (match kind_of_term k with IsSort s -> s | _ -> raise (Arity None)) in let ind = build_dependent_inductive indf in - if is_conv env sigma a1 ind then - if List.exists (base_sort_cmp CONV ksort) kelim then - (true,k) - else - raise (Arity (Some(k,t',error_elim_expln env sigma k t'))) - else - raise (Arity None) + let univ = + try conv env sigma a1 ind + with NotConvertible -> raise (Arity None) in + if List.exists (base_sort_cmp CONV ksort) kelim then + ((true,k), Constraint.union u univ) + else + raise (Arity (Some(k,t',error_elim_expln env sigma k t'))) | k, IsProd (_,_,_) -> raise (Arity None) | k, ki -> let ksort = (match k with IsSort s -> s | _ -> raise (Arity None)) in if List.exists (base_sort_cmp CONV ksort) kelim then - false, pt' + (false, pt'), u else raise (Arity (Some(pt',t',error_elim_expln env sigma pt' t'))) -in - try srec (pt,t) + in + try srec (pt,t) Constraint.empty with Arity kinds -> let listarity = (List.map (make_arity env true indf) kelim) @@ -327,8 +335,9 @@ let find_case_dep_nparams env sigma (c,p) (IndFamily (mis,_) as indf) typP = let kelim = mis_kelim mis in let arsign,s = get_arity indf in let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in - let (dep,_) = is_correct_arity env sigma kelim (c,p) indf (typP,glob_t) in - dep + let ((dep,_),univ) = + is_correct_arity env sigma kelim (c,p) indf (typP,glob_t) in + (dep,univ) (* type_case_branches type un <p>Case c of ... end IndType (indf,realargs) = type de c @@ -338,37 +347,43 @@ let find_case_dep_nparams env sigma (c,p) (IndFamily (mis,_) as indf) typP = *) let type_case_branches env sigma (IndType (indf,realargs)) pt p c = - let dep = find_case_dep_nparams env sigma (c,p) indf pt in + let (dep,univ) = find_case_dep_nparams env sigma (c,p) indf pt in let constructs = get_constructors indf in let lc = Array.map (build_branch_type env dep p) constructs in if dep then - (lc, beta_applist (p,(realargs@[c]))) + (lc, beta_applist (p,(realargs@[c])), univ) else - (lc, beta_applist (p,realargs)) + (lc, beta_applist (p,realargs), univ) let check_branches_message env sigma (c,ct) (explft,lft) = let expn = Array.length explft and n = Array.length lft in if n<>expn then error_number_branches CCI env c ct expn; - for i = 0 to n-1 do - if not (is_conv_leq env sigma lft.(i) (explft.(i))) then + let univ = ref Constraint.empty in + (for i = 0 to n-1 do + try + univ := Constraint.union !univ + (conv_leq env sigma lft.(i) (explft.(i))) + with NotConvertible -> error_ill_formed_branch CCI env c i (nf_betaiota env sigma lft.(i)) (nf_betaiota env sigma explft.(i)) - done + done; + !univ) -let type_of_case env sigma ci pj cj lfj = +let judge_of_case env sigma ci pj cj lfj = let lft = Array.map (fun j -> body_of_type j.uj_type) lfj in let indspec = try find_rectype env sigma (body_of_type cj.uj_type) with Induc -> error_case_not_inductive CCI env cj.uj_val (body_of_type cj.uj_type) in - let (bty,rslty) = + let (bty,rslty,univ) = type_case_branches env sigma indspec (body_of_type pj.uj_type) pj.uj_val cj.uj_val in let kind = mysort_of_arity env sigma (body_of_type pj.uj_type) in - check_branches_message env sigma - (cj.uj_val,body_of_type cj.uj_type) (bty,lft); - { uj_val = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); - uj_type = rslty } + let univ' = check_branches_message env sigma + (cj.uj_val,body_of_type cj.uj_type) (bty,lft) in + ({ uj_val = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); + uj_type = rslty }, + Constraint.union univ univ') (* let tocasekey = Profile.declare_profile "type_of_case";; @@ -492,8 +507,8 @@ let is_subterm_specif env sigma lcx mind_recvec = if array_for_all (fun st -> st=stl0) stl then stl0 else None - | IsFix ((recindxs,i),(typarray,funnames,bodies as recdef)) -> - let nbfix = List.length funnames in + | IsFix ((recindxs,i),(_,typarray,bodies as recdef)) -> + let nbfix = Array.length typarray in let decrArg = recindxs.(i) in let theBody = bodies.(i) in let sign,strippedBody = decompose_lam_n_assum (decrArg+1) theBody in @@ -620,11 +635,11 @@ let rec check_subterm_rec_meta env sigma vectn k def = Eduardo 7/9/98 *) - | IsFix ((recindxs,i),(typarray,funnames,bodies as recdef)) -> + | IsFix ((recindxs,i),(_,typarray,bodies as recdef)) -> (List.for_all (check_rec_call env n lst) l) && (array_for_all (check_rec_call env n lst) typarray) && - let nbfix = List.length funnames - in let decrArg = recindxs.(i) + let nbfix = Array.length typarray in + let decrArg = recindxs.(i) and env' = push_rec_types recdef env and n' = n+nbfix and lst' = map_lift_fst_n nbfix lst @@ -696,8 +711,8 @@ let rec check_subterm_rec_meta env sigma vectn k def = (array_for_all (check_rec_call env n lst) la) && (List.for_all (check_rec_call env n lst) l) - | IsCoFix (i,(typarray,funnames,bodies as recdef)) -> - let nbfix = Array.length bodies in + | IsCoFix (i,(_,typarray,bodies as recdef)) -> + let nbfix = Array.length typarray in let env' = push_rec_types recdef env in (array_for_all (check_rec_call env n lst) typarray) && (List.for_all (check_rec_call env n lst) l) && @@ -735,12 +750,12 @@ nvect is [|n1;..;nk|] which gives for each recursive definition the inductive-decreasing index the function checks the convertibility of ti with Ai *) -let check_fix env sigma ((nvect,bodynum),(types,names,bodies as recdef)) = +let check_fix env sigma ((nvect,bodynum),(names,types,bodies as recdef)) = let nbfix = Array.length bodies in if nbfix = 0 or Array.length nvect <> nbfix or Array.length types <> nbfix - or List.length names <> nbfix + or Array.length names <> nbfix or bodynum < 0 or bodynum >= nbfix then anomaly "Ill-formed fix term"; @@ -750,7 +765,7 @@ let check_fix env sigma ((nvect,bodynum),(types,names,bodies as recdef)) = let _ = check_subterm_rec_meta fixenv sigma nvect nvect.(i) bodies.(i) in () with FixGuardError err -> - error_ill_formed_rec_body CCI fixenv err (List.rev names) i bodies + error_ill_formed_rec_body CCI fixenv err names i bodies done (* @@ -845,7 +860,7 @@ let check_guard_rec_meta env sigma nbfix def deftype = else raise (CoFixGuardError (RecCallInTypeOfAbstraction t)) - | IsCoFix (j,(varit,lna,vdefs as recdef)) -> + | IsCoFix (j,(_,varit,vdefs as recdef)) -> if (List.for_all (noccur_with_meta n nbfix) args) then let nbfix = Array.length vdefs in @@ -880,7 +895,7 @@ let check_guard_rec_meta env sigma nbfix def deftype = (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env sigma (bodynum,(types,names,bodies as recdef)) = +let check_cofix env sigma (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 @@ -888,7 +903,7 @@ let check_cofix env sigma (bodynum,(types,names,bodies as recdef)) = let _ = check_guard_rec_meta fixenv sigma nbfix bodies.(i) types.(i) in () with CoFixGuardError err -> - error_ill_formed_rec_body CCI fixenv err (List.rev names) i bodies + error_ill_formed_rec_body CCI fixenv err names i bodies done (* Checks the type of a (co)fixpoint. @@ -918,11 +933,11 @@ let control_only_guard env sigma = let rec control_rec c = match kind_of_term c with | IsRel _ | IsVar _ -> () | IsSort _ | IsMeta _ -> () - | IsCoFix (_,(tys,_,bds) as cofix) -> + | IsCoFix (_,(_,tys,bds) as cofix) -> check_cofix env sigma cofix; Array.iter control_rec tys; Array.iter control_rec bds; - | IsFix (_,(tys,_,bds) as fix) -> + | IsFix (_,(_,tys,bds) as fix) -> check_fix env sigma fix; Array.iter control_rec tys; Array.iter control_rec bds; diff --git a/kernel/typeops.mli b/kernel/typeops.mli index aaa07142f..3008c87cb 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -50,6 +50,11 @@ val abs_rel : env -> 'a evar_map -> name -> types -> unsafe_judgment -> unsafe_judgment * constraints +(* s Type of a let in. *) +val judge_of_letin : + env -> 'a evar_map -> name -> unsafe_judgment -> unsafe_judgment + -> unsafe_judgment * constraints + (*s Type of application. *) val apply_rel_list : env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment @@ -75,21 +80,22 @@ val type_of_inductive : env -> 'a evar_map -> inductive -> types val type_of_constructor : env -> 'a evar_map -> constructor -> types (*s Type of Cases. *) -val type_of_case : env -> 'a evar_map -> case_info +val judge_of_case : env -> 'a evar_map -> case_info -> unsafe_judgment -> unsafe_judgment - -> unsafe_judgment array -> unsafe_judgment + -> unsafe_judgment array -> unsafe_judgment * constraints val find_case_dep_nparams : - env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool + env -> 'a evar_map -> constr * constr -> inductive_family -> constr + -> bool * constraints val type_case_branches : env -> 'a evar_map -> Inductive.inductive_type -> constr -> types - -> constr -> types array * types + -> constr -> types array * types * constraints (*s Type of fixpoints and guard condition. *) val check_fix : env -> 'a evar_map -> fixpoint -> unit val check_cofix : env -> 'a evar_map -> cofixpoint -> unit -val type_fixpoint : env -> 'a evar_map -> name list -> types array +val type_fixpoint : env -> 'a evar_map -> name array -> types array -> unsafe_judgment array -> constraints val control_only_guard : env -> 'a evar_map -> constr -> unit diff --git a/kernel/univ.ml b/kernel/univ.ml index e8f692300..b3d5a9b0e 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -288,18 +288,18 @@ let enforce_univ_gt u v g = (match compare g v u with | NGE -> setgt g u v | _ -> error_inconsistency()) - +(* let enforce_univ_relation g = function | Equiv (u,v) -> enforce_univ_eq u v g | Canonical {univ=u; gt=gt; ge=ge} -> let g' = List.fold_right (enforce_univ_gt u) gt g in List.fold_right (enforce_univ_geq u) ge g' - - +*) (* Merging 2 universe graphs *) +(* let merge_universes sp u1 u2 = UniverseMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2 - +*) (* Constraints and sets of consrtaints. *) @@ -308,6 +308,13 @@ type constraint_type = Gt | Geq | Eq type univ_constraint = universe * constraint_type * universe +let enforce_constraint cst g = + match cst with + | (u,Gt,v) -> enforce_univ_gt u v g + | (u,Geq,v) -> enforce_univ_geq u v g + | (u,Eq,v) -> enforce_univ_eq u v g + + module Constraint = Set.Make( struct type t = univ_constraint @@ -324,12 +331,7 @@ let enforce_geq u v c = Constraint.add (u,Geq,v) c let enforce_eq u v c = Constraint.add (u,Eq,v) c let merge_constraints c g = - Constraint.fold - (fun cst g -> match cst with - | (u,Gt,v) -> enforce_univ_gt u v g - | (u,Geq,v) -> enforce_univ_geq u v g - | (u,Eq,v) -> enforce_univ_eq u v g) - c g + Constraint.fold enforce_constraint c g (* Returns a fresh universe, juste above u. Does not create new universes for Type_0 (the sort of Prop and Set). |