diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 52 |
1 files changed, 35 insertions, 17 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 1232ab654e..337b66e8e7 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -12,6 +12,7 @@ open CErrors open Util open Names open Univ +open Sorts open Term open Constr open Vars @@ -47,11 +48,19 @@ let check_type env c t = (* This should be a type intended to be assumed. The error message is not as useful as for [type_judgment]. *) -let check_assumption env t ty = - try let _ = check_type env t ty in t +let infer_assumption env t ty = + try + let s = check_type env t ty in + t, (match s with Sorts.SProp -> Irrelevant | _ -> Relevant) with TypeError _ -> error_assumption env (make_judge t ty) +let check_assumption env x t ty = + let r = x.Context.binder_relevance in + let t, r' = infer_assumption env t ty in + if not (r == r') then error_bad_relevance env; + t + (************************************************) (* Incremental typing rules: builds a typing judgment given the *) (* judgments for the subterms. *) @@ -220,7 +229,7 @@ let type_of_prim env t = in let rec nary_int63_op arity ty = if Int.equal arity 0 then ty - else Constr.mkProd(Name (Id.of_string "x"), int_ty, nary_int63_op (arity-1) ty) + else Constr.mkProd(Context.nameR (Id.of_string "x"), int_ty, nary_int63_op (arity-1) ty) in let return_ty = let open CPrimitives in @@ -377,7 +386,9 @@ let type_of_case env ci p pt c ct _lf lft = let (pind, _ as indspec) = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - let () = check_case_info env pind ci in + let _, sp = try dest_arity env pt + with NotArity -> error_elim_arity env pind c (make_judge p pt) None in + let () = check_case_info env pind (Sorts.relevance_of_sort sp) ci in let (bty,rslty) = type_case_branches env indspec (make_judge p pt) c in let () = check_branch_types env pind c ct lft bty in @@ -456,6 +467,10 @@ let constr_of_global_in_context env r = (************************************************************************) (************************************************************************) +let check_binder_annot env s x = + let r = x.Context.binder_relevance in + if not (Sorts.relevance_of_sort s == r) then error_bad_relevance env + (* The typing machine. *) (* ATTENTION : faudra faire le typage du contexte des Const, Ind et Constructsi un jour cela devient des constructions @@ -499,20 +514,23 @@ let rec execute env cstr = type_of_apply env f ft args argst | Lambda (name,c1,c2) -> - let _ = execute_is_type env c1 in + let s = execute_is_type env c1 in + check_binder_annot env s name; let env1 = push_rel (LocalAssum (name,c1)) env in let c2t = execute env1 c2 in type_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> let vars = execute_is_type env c1 in + check_binder_annot env vars name; let env1 = push_rel (LocalAssum (name,c1)) env in let vars' = execute_is_type env1 c2 in type_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> let c1t = execute env c1 in - let _c2s = execute_is_type env c2 in + let c2s = execute_is_type env c2 in + check_binder_annot env c2s name; let () = check_cast env c1 c1t DEFAULTcast c2 in let env1 = push_rel (LocalDef (name,c1,c2)) env in let c3t = execute env1 c3 in @@ -563,7 +581,7 @@ and execute_is_type env constr = and execute_recdef env (names,lar,vdef) i = let lart = execute_array env lar in - let lara = Array.map2 (check_assumption env) lar lart in + let lara = Array.map3 (check_assumption env) names lar lart in let env1 = push_rec_types (names,lara,vdef) env in let vdeft = execute_array env1 vdef in let () = check_fixpoint env1 names lara vdef vdeft in @@ -591,7 +609,7 @@ let infer = else (fun b c -> infer b c) let assumption_of_judgment env {uj_val=c; uj_type=t} = - check_assumption env c t + infer_assumption env c t let type_judgment env {uj_val=c; uj_type=t} = let s = check_type env c t in @@ -644,17 +662,17 @@ let judge_of_apply env funj argjv = let args, argtys = dest_judgev argjv in make_judge (mkApp (funj.uj_val, args)) (type_of_apply env funj.uj_val funj.uj_type args argtys) -let judge_of_abstraction env x varj bodyj = - make_judge (mkLambda (x, varj.utj_val, bodyj.uj_val)) - (type_of_abstraction env x varj.utj_val bodyj.uj_type) +(* let judge_of_abstraction env x varj bodyj = *) +(* make_judge (mkLambda (x, varj.utj_val, bodyj.uj_val)) *) +(* (type_of_abstraction env x varj.utj_val bodyj.uj_type) *) -let judge_of_product env x varj outj = - make_judge (mkProd (x, varj.utj_val, outj.utj_val)) - (mkSort (sort_of_product env varj.utj_type outj.utj_type)) +(* let judge_of_product env x varj outj = *) +(* make_judge (mkProd (x, varj.utj_val, outj.utj_val)) *) +(* (mkSort (sort_of_product env varj.utj_type outj.utj_type)) *) -let judge_of_letin _env name defj typj j = - make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) - (subst1 defj.uj_val j.uj_type) +(* let judge_of_letin env name defj typj j = *) +(* make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) *) +(* (subst1 defj.uj_val j.uj_type) *) let judge_of_cast env cj k tj = let () = check_cast env cj.uj_val cj.uj_type k tj.utj_val in |