Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.

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