diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 32 |
1 files changed, 19 insertions, 13 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index cd969ea457..2966acae45 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -812,7 +812,7 @@ let rec subterm_specif renv stack t = | Not_subterm -> Not_subterm) | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ - | Construct _ | CoFix _ | Int _ -> Not_subterm + | Construct _ | CoFix _ | Int _ | Float _ -> Not_subterm (* Other terms are not subterms *) @@ -885,6 +885,9 @@ let filter_stack_domain env p stack = in filter_stack env ar stack +let judgment_of_fixpoint (_, types, bodies) = + Array.map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies + (* Check if [def] is a guarded fixpoint body with decreasing arg. given [recpos], the decreasing arguments of each mutually defined fixpoint. *) @@ -982,7 +985,12 @@ let check_one_fix renv recpos trees def = if Int.equal i j && (List.length stack' > decrArg) then let recArg = List.nth stack' decrArg in let arg_sp = stack_element_specif recArg in - check_nested_fix_body renv' (decrArg+1) arg_sp body + let illformed () = + error_ill_formed_rec_body renv.env NotEnoughAbstractionInFixBody + (pi1 recdef) i (push_rec_types recdef renv.env) + (judgment_of_fixpoint recdef) + in + check_nested_fix_body illformed renv' (decrArg+1) arg_sp body else check_rec_call renv' [] body) with (FixGuardError _ as exn) -> let exn = CErrors.push exn in @@ -1057,7 +1065,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv stack (Term.applist(c,l)) end - | Sort _ | Int _ -> + | Sort _ | Int _ | Float _ -> assert (List.is_empty l) (* l is not checked because it is considered as the meta's context *) @@ -1065,23 +1073,20 @@ let check_one_fix renv recpos trees def = | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) - and check_nested_fix_body renv decr recArgsDecrArg body = + and check_nested_fix_body illformed renv decr recArgsDecrArg body = if Int.equal decr 0 then check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body else - match kind body with + match kind (whd_all renv.env body) with | Lambda (x,a,b) -> check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in - check_nested_fix_body renv' (decr-1) recArgsDecrArg b - | _ -> anomaly (Pp.str "Not enough abstractions in fix body.") + check_nested_fix_body illformed renv' (decr-1) recArgsDecrArg b + | _ -> illformed () 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 if Int.equal nbfix 0 @@ -1119,9 +1124,10 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = | _ -> raise_err env i NotEnoughAbstractionInFixBody in let ((ind, _), _) as res = check_occur fixenv 1 def in - let _, ind = lookup_mind_specif env ind in + let _, mip = lookup_mind_specif env ind in (* recursive sprop means non record with projections -> squashed *) - if Sorts.Irrelevant == ind.mind_relevance + if mip.mind_relevance == Sorts.Irrelevant && + not (Environ.is_type_in_type env (GlobRef.IndRef ind)) then begin if names.(i).Context.binder_relevance == Sorts.Relevant @@ -1254,7 +1260,7 @@ let check_one_cofix env nbfix def deftype = | Evar _ -> List.iter (check_rec_call env alreadygrd n tree vlra) args | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ - | Ind _ | Fix _ | Proj _ | Int _ -> + | Ind _ | Fix _ | Proj _ | Int _ | Float _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in let ((mind, _),_) = codomain_is_coind env deftype in |