Merge PR #8817: SProp: the definitionally proof irrelevant universe

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82

1 files changed, 153 insertions, 93 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 227a164549..be878dd99b 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -12,8 +12,10 @@ open CErrors
 open Util
 open Names
 open Univ
+open Sorts
 open Term
 open Constr
+open Context
 open Vars
 open Declarations
 open Environ
@@ -47,11 +49,32 @@ 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
+    (match s with Sorts.SProp -> Irrelevant | _ -> Relevant)
   with TypeError _ ->
     error_assumption env (make_judge t ty)
 
+let warn_bad_relevance_name = "bad-relevance"
+let warn_bad_relevance =
+  CWarnings.create ~name:warn_bad_relevance_name ~category:"debug" ~default:CWarnings.Disabled
+    Pp.(function
+        | None ->  str "Bad relevance in case annotation."
+        | Some x -> str "Bad relevance for binder " ++ Name.print x.binder_name ++ str ".")
+
+let warn_bad_relevance_ci ?loc () = warn_bad_relevance ?loc None
+let warn_bad_relevance ?loc x = warn_bad_relevance ?loc (Some x)
+
+let check_assumption env x t ty =
+  let r = x.binder_relevance in
+  let r' = infer_assumption env t ty in
+  let x = if Sorts.relevance_equal r r'
+    then x
+    else (warn_bad_relevance x; {x with binder_relevance = r'})
+  in
+  x
+
 (************************************************)
 (* Incremental typing rules: builds a typing judgment given the *)
 (* judgments for the subterms. *)
@@ -69,7 +92,7 @@ let type_of_type u =
     mkType uu
 
 let type_of_sort = function
-  | Prop | Set -> type1
+  | SProp | Prop | Set -> type1
   | Type u -> type_of_type u
 
 (*s Type of a de Bruijn index. *)
@@ -220,7 +243,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
@@ -264,6 +287,7 @@ let judge_of_int env i =
 
 let sort_of_product env domsort rangsort =
   match (domsort, rangsort) with
+    | (_, SProp) | (SProp, _) -> rangsort
     (* Product rule (s,Prop,Prop) *)
     | (_,       Prop)  -> rangsort
     (* Product rule (Prop/Set,Set,Set) *)
@@ -275,13 +299,13 @@ let sort_of_product env domsort rangsort =
           rangsort
         else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
-          Type (Universe.sup Universe.type0 u1)
+          Sorts.sort_of_univ (Universe.sup Universe.type0 u1)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Set,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
+    | (Set,  Type u2)  -> Sorts.sort_of_univ (Universe.sup Universe.type0 u2)
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop, Type _)  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *)
-    | (Type u1, Type u2) -> Type (Universe.sup u1 u2)
+    | (Type u1, Type u2) -> Sorts.sort_of_univ (Universe.sup u1 u2)
 
 (* [judge_of_product env name (typ1,s1) (typ2,s2)] implements the rule
 
@@ -376,11 +400,17 @@ 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 rp = Sorts.relevance_of_sort sp in
+  let ci = if ci.ci_relevance == rp then ci
+    else (warn_bad_relevance_ci (); {ci with ci_relevance=rp})
+  in
+  let () = check_case_info env pind rp 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
-  rslty
+  ci, rslty
 
 let type_of_projection env p c ct =
   let pty = lookup_projection p env in
@@ -455,6 +485,13 @@ let constr_of_global_in_context env r =
 (************************************************************************)
 (************************************************************************)
 
+let check_binder_annot s x =
+  let r = x.binder_relevance in
+  let r' = Sorts.relevance_of_sort s in
+  if r' == r
+  then x
+  else (warn_bad_relevance x; {x with binder_relevance = r'})
+
 (* The typing machine. *)
     (* ATTENTION : faudra faire le typage du contexte des Const,
     Ind et Constructsi un jour cela devient des constructions
@@ -463,88 +500,110 @@ let rec execute env cstr =
   let open Context.Rel.Declaration in
   match kind cstr with
     (* Atomic terms *)
-    | Sort s -> type_of_sort s
+    | Sort s ->
+      (match s with
+       | SProp -> if not (Environ.sprop_allowed env) then error_disallowed_sprop env
+       | _ -> ());
+      cstr, type_of_sort s
 
     | Rel n ->
-      type_of_relative env n
+      cstr, type_of_relative env n
 
     | Var id ->
-      type_of_variable env id
+      cstr, type_of_variable env id
 
     | Const c ->
-      type_of_constant env c
+      cstr, type_of_constant env c
 	
     | Proj (p, c) ->
-        let ct = execute env c in
-          type_of_projection env p c ct
+      let c', ct = execute env c in
+      let cstr = if c == c' then cstr else mkProj (p,c') in
+      cstr, type_of_projection env p c' ct
 
     (* Lambda calculus operators *)
     | App (f,args) ->
-        let argst = execute_array env args in
-	let ft =
+      let args', argst = execute_array env args in
+        let f', ft =
 	  match kind f with
 	  | Ind ind when Environ.template_polymorphic_pind ind env ->
 	    let args = Array.map (fun t -> lazy t) argst in
-              type_of_inductive_knowing_parameters env ind args
+              f, type_of_inductive_knowing_parameters env ind args
 	  | _ ->
 	    (* No template polymorphism *)
             execute env f
 	in
-
-          type_of_apply env f ft args argst
+        let cstr = if f == f' && args == args' then cstr else mkApp (f',args') in
+        cstr, type_of_apply env f' ft args' argst
 
     | Lambda (name,c1,c2) ->
-      let _ = execute_is_type env c1 in
-      let env1 = push_rel (LocalAssum (name,c1)) env in
-      let c2t = execute env1 c2 in
-        type_of_abstraction env name c1 c2t
+      let c1', s = execute_is_type env c1 in
+      let name' = check_binder_annot s name in
+      let env1 = push_rel (LocalAssum (name',c1')) env in
+      let c2', c2t = execute env1 c2 in
+      let cstr = if name == name' && c1 == c1' && c2 == c2' then cstr else mkLambda(name',c1',c2') in
+      cstr, type_of_abstraction env name' c1 c2t
 
     | Prod (name,c1,c2) ->
-      let vars = execute_is_type env c1 in
-      let env1 = push_rel (LocalAssum (name,c1)) env in
-      let vars' = execute_is_type env1 c2 in
-        type_of_product env name vars vars'
+      let c1', vars = execute_is_type env c1 in
+      let name' = check_binder_annot vars name in
+      let env1 = push_rel (LocalAssum (name',c1')) env in
+      let c2', vars' = execute_is_type env1 c2 in
+      let cstr = if name == name' && c1 == c1' && c2 == c2' then cstr else mkProd(name',c1',c2') in
+      cstr, 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 () = check_cast env c1 c1t DEFAULTcast c2 in
-      let env1 = push_rel (LocalDef (name,c1,c2)) env in
-      let c3t = execute env1 c3 in
-	subst1 c1 c3t
+      let c1', c1t = execute env c1 in
+      let c2', c2s = execute_is_type env c2 in
+      let name' = check_binder_annot c2s name in
+      let () = check_cast env c1' c1t DEFAULTcast c2' in
+      let env1 = push_rel (LocalDef (name',c1',c2')) env in
+      let c3', c3t = execute env1 c3 in
+      let cstr = if name == name' && c1 == c1' && c2 == c2' && c3 == c3' then cstr
+        else mkLetIn(name',c1',c2',c3')
+      in
+      cstr, subst1 c1 c3t
 
     | Cast (c,k,t) ->
-      let ct = execute env c in
-      let _ts = (check_type env t (execute env t)) in
-      let () = check_cast env c ct k t in
-	t
+      let c', ct = execute env c in
+      let t', _ts = execute_is_type env t in
+      let () = check_cast env c' ct k t' in
+      let cstr = if c == c' && t == t' then cstr else mkCast(c',k,t') in
+      cstr, t'
 
     (* Inductive types *)
     | Ind ind ->
-      type_of_inductive env ind
+      cstr, type_of_inductive env ind
 
     | Construct c ->
-      type_of_constructor env c
+      cstr, type_of_constructor env c
 
     | Case (ci,p,c,lf) ->
-        let ct = execute env c in
-        let pt = execute env p in
-        let lft = execute_array env lf in
-          type_of_case env ci p pt c ct lf lft
-
-    | Fix ((_vn,i as vni),recdef) ->
+        let c', ct = execute env c in
+        let p', pt = execute env p in
+        let lf', lft = execute_array env lf in
+        let ci', t = type_of_case env ci p' pt c' ct lf' lft in
+        let cstr = if ci == ci' && c == c' && p == p' && lf == lf' then cstr
+          else mkCase(ci',p',c',lf')
+        in
+        cstr, t
+
+    | Fix ((_vn,i as vni),recdef as fix) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
-      let fix = (vni,recdef') in
-        check_fix env fix; fix_ty
+      let cstr, fix = if recdef == recdef' then cstr, fix else
+          let fix = (vni,recdef') in mkFix fix, fix
+      in
+      check_fix env fix; cstr, fix_ty
 	  
-    | CoFix (i,recdef) ->
+    | CoFix (i,recdef as cofix) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
-      let cofix = (i,recdef') in
-        check_cofix env cofix; fix_ty
+      let cstr, cofix = if recdef == recdef' then cstr, cofix else
+          let cofix = (i,recdef') in mkCoFix cofix, cofix
+      in
+      check_cofix env cofix; cstr, fix_ty
 
     (* Primitive types *)
-    | Int _ -> type_of_int env
-	  
+    | Int _ -> cstr, type_of_int env
+
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
 	anomaly (Pp.str "the kernel does not support metavariables.")
@@ -553,18 +612,22 @@ let rec execute env cstr =
 	anomaly (Pp.str "the kernel does not support existential variables.")
 
 and execute_is_type env constr =
-  let t = execute env constr in
-    check_type env constr t
-
-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 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
-    (lara.(i),(names,lara,vdef))
-
-and execute_array env = Array.map (execute env)
+  let c, t = execute env constr in
+    c, check_type env constr t
+
+and execute_recdef env (names,lar,vdef as recdef) i =
+  let lar', lart = execute_array env lar in
+  let names' = Array.Smart.map_i (fun i na -> check_assumption env na lar'.(i) lart.(i)) names in
+  let env1 = push_rec_types (names',lar',vdef) env in (* vdef is ignored *)
+  let vdef', vdeft = execute_array env1 vdef in
+  let () = check_fixpoint env1 names' lar' vdef' vdeft in
+  let recdef = if names == names' && lar == lar' && vdef == vdef' then recdef else (names',lar',vdef') in
+    (lar'.(i),recdef)
+
+and execute_array env cs =
+  let tys = Array.make (Array.length cs) mkProp in
+  let cs = Array.Smart.map_i (fun i c -> let c, ty = execute env c in tys.(i) <- ty; c) cs in
+  cs, tys
 
 (* Derived functions *)
 
@@ -576,8 +639,8 @@ let check_wellformed_universes env c =
 
 let infer env constr =
   let () = check_wellformed_universes env constr in
-  let t = execute env constr in
-    make_judge constr t
+  let constr, t = execute env constr in
+  make_judge constr t
 
 let infer = 
   if Flags.profile then
@@ -586,7 +649,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
@@ -594,30 +657,27 @@ let type_judgment env {uj_val=c; uj_type=t} =
 
 let infer_type env constr =
   let () = check_wellformed_universes env constr in
-  let t = execute env constr in
+  let constr, t = execute env constr in
   let s = check_type env constr t in
   {utj_val = constr; utj_type = s}
 
-let infer_v env cv =
-  let () = Array.iter (check_wellformed_universes env) cv in
-  let jv = execute_array env cv in
-    make_judgev cv jv
-
 (* Typing of several terms. *)
 
 let check_context env rels =
   let open Context.Rel.Declaration in
-  Context.Rel.fold_outside (fun d env ->
+  Context.Rel.fold_outside (fun d (env,rels) ->
     match d with
-      | LocalAssum (_,ty) ->
-        let _ = infer_type env ty in
-        push_rel d env
-      | LocalDef (_,bd,ty) ->
+      | LocalAssum (x,ty) ->
+        let jty = infer_type env ty in
+        let x = check_binder_annot jty.utj_type x in
+        push_rel d env, LocalAssum (x,jty.utj_val) :: rels
+      | LocalDef (x,bd,ty) ->
         let j1 = infer env bd in
-        let _ = infer_type env ty in
+        let jty = infer_type env ty in
         conv_leq false env j1.uj_type ty;
-        push_rel d env)
-    rels ~init:env
+        let x = check_binder_annot jty.utj_type x in
+        push_rel d env, LocalDef (x,j1.uj_val,jty.utj_val) :: rels)
+    rels ~init:(env,[])
 
 let judge_of_prop = make_judge mkProp type1
 let judge_of_set = make_judge mkSet type1
@@ -639,17 +699,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
@@ -664,8 +724,8 @@ let judge_of_constructor env cu =
 
 let judge_of_case env ci pj cj lfj =
   let lf, lft = dest_judgev lfj in
-  make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft))
-             (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft)
+  let ci, t = type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft in
+  make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) t
 
 (* Building type of primitive operators and type *)