diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 52 |
1 files changed, 29 insertions, 23 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 00901686..9415941d 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductive.ml 10173 2007-10-04 13:02:56Z herbelin $ *) +(* $Id: inductive.ml 10920 2008-05-12 10:19:32Z herbelin $ *) open Util open Names @@ -83,7 +83,7 @@ let instantiate_params full t args sign = let instantiate_partial_params = instantiate_params false let full_inductive_instantiate mib params sign = - let dummy = mk_Prop in + let dummy = prop_sort in let t = mkArity (sign,dummy) in fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) @@ -124,8 +124,8 @@ Remark: Set (predicative) is encoded as Type(0) let sort_as_univ = function | Type u -> u -| Prop Null -> neutral_univ -| Prop Pos -> base_univ +| Prop Null -> type0m_univ +| Prop Pos -> type0_univ let cons_subst u su subst = try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst @@ -179,9 +179,12 @@ let instantiate_universes env ctx ar argsorts = let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in let level = subst_large_constraints subst ar.poly_level in ctx, - if is_empty_univ level then mk_Prop - else if is_base_univ level then mk_Set - else Type level + (* Singleton type not containing types are interpretable in Prop *) + if is_type0m_univ level then prop_sort + (* Non singleton type not containing types are interpretable in Set *) + else if is_type0_univ level then set_sort + (* This is a Type with constraints *) + else Type level let type_of_inductive_knowing_parameters env mip paramtyps = match mip.mind_arity with @@ -201,11 +204,11 @@ let type_of_inductive env (_,mip) = let cumulate_constructor_univ u = function | Prop Null -> u - | Prop Pos -> sup base_univ u + | Prop Pos -> sup type0_univ u | Type u' -> sup u u' let max_inductive_sort = - Array.fold_left cumulate_constructor_univ neutral_univ + Array.fold_left cumulate_constructor_univ type0m_univ (************************************************************************) (* Type of a constructor *) @@ -425,8 +428,8 @@ type subterm_spec = | Not_subterm let spec_of_tree t = - if t=mk_norec then Not_subterm else Subterm(Strict,t) - + if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t) + let subterm_spec_glb = let glb2 s1 s2 = match s1,s2 with @@ -435,7 +438,7 @@ let subterm_spec_glb = | Not_subterm, _ -> Not_subterm | _, Not_subterm -> Not_subterm | Subterm (a1,t1), Subterm (a2,t2) -> - if t1=t2 then Subterm (size_glb a1 a2, t1) + if Rtree.eq_rtree (=) t1 t2 then Subterm (size_glb a1 a2, t1) (* branches do not return objects with same spec *) else Not_subterm in Array.fold_left glb2 Dead_code @@ -653,7 +656,7 @@ let check_one_fix renv recpos def = (* if [t] does not make recursive calls, it is guarded: *) if noccur_with_meta renv.rel_min nfi t then () else - let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in + let (f,l) = decompose_app (whd_betaiotazeta t) in match kind_of_term f with | Rel p -> (* Test if [p] is a fixpoint (recursive call) *) @@ -666,12 +669,10 @@ let check_one_fix renv recpos def = 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 - | _ -> assert false + (* Check the decreasing arg is smaller *) + let z = List.nth l np in + if not (check_is_subterm renv z) then + error_illegal_rec_call renv glob z end else begin @@ -779,6 +780,8 @@ let check_one_fix renv recpos def = in check_rec_call renv def +let judgment_of_fixpoint (_, types, bodies) = + array_map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = let nbfix = Array.length bodies in @@ -790,8 +793,9 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = or bodynum >= nbfix then anomaly "Ill-formed fix term"; let fixenv = push_rec_types recdef env in + let vdefj = judgment_of_fixpoint recdef in let raise_err env i err = - error_ill_formed_rec_body env err names i in + error_ill_formed_rec_body env err names i fixenv vdefj in (* Check the i-th definition with recarg k *) let find_ind i k def = (* check fi does not appear in the k+1 first abstractions, @@ -817,14 +821,15 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (Array.map fst rv, Array.map snd rv) -let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) = +let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = let (minds, rdef) = inductive_of_mutfix env fix in 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 check_one_fix renv nvect body with FixGuardError (fixenv,err) -> - error_ill_formed_rec_body fixenv err names i + error_ill_formed_rec_body fixenv err names i + (push_rec_types recdef env) (judgment_of_fixpoint recdef) done (* @@ -935,5 +940,6 @@ let check_cofix env (bodynum,(names,types,bodies as recdef)) = let fixenv = push_rec_types recdef env in try check_one_cofix fixenv nbfix bodies.(i) types.(i) with CoFixGuardError (errenv,err) -> - error_ill_formed_rec_body errenv err names i + error_ill_formed_rec_body errenv err names i + fixenv (judgment_of_fixpoint recdef) done |