From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 kernel/typeops.mli | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 52c261c5e8..e57d6622c9 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -34,9 +34,11 @@ val check_context :
 (** If [j] is the judgement {% $ %}c:t{% $ %}, then [assumption_of_judgement env j]
    returns the type {% $ %}c{% $ %}, checking that {% $ %}t{% $ %} is a sort. *)
 
-val assumption_of_judgment :  env -> unsafe_judgment -> types
+val assumption_of_judgment :  env -> unsafe_judgment -> types * Sorts.relevance
 val type_judgment          :  env -> unsafe_judgment -> unsafe_type_judgment
 
+val check_binder_annot : env -> Sorts.t -> Name.t Context.binder_annot -> unit
+
 (** {6 Type of sorts. } *)
 val type1 : types
 val type_of_sort : Sorts.t -> types
@@ -65,21 +67,21 @@ val judge_of_apply :
     -> unsafe_judgment
 
 (** {6 Type of an abstraction. } *)
-val judge_of_abstraction :
-  env -> Name.t -> unsafe_type_judgment -> unsafe_judgment
-    -> unsafe_judgment
+(* val judge_of_abstraction : *)
+(*   env -> Name.t -> unsafe_type_judgment -> unsafe_judgment *)
+(*     -> unsafe_judgment *)
 
 (** {6 Type of a product. } *)
 val sort_of_product : env -> Sorts.t -> Sorts.t -> Sorts.t
-val type_of_product : env -> Name.t -> Sorts.t -> Sorts.t -> types
-val judge_of_product :
-  env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment
-    -> unsafe_judgment
+val type_of_product : env -> Name.t Context.binder_annot -> Sorts.t -> Sorts.t -> types
+(* val judge_of_product : *)
+(*   env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment *)
+(*     -> unsafe_judgment *)
 
 (** s Type of a let in. *)
-val judge_of_letin :
-  env -> Name.t -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment
-    -> unsafe_judgment
+(* val judge_of_letin : *)
+(*   env -> Name.t -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment *)
+(*     -> unsafe_judgment *)
 
 (** {6 Type of a cast. } *)
 val judge_of_cast :
-- 
cgit v1.2.3


From 06b29ed748a9d9b99c2c08a3788906dbad5417d2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 11 Jun 2018 13:57:28 +0200
Subject: Repair relevance marks in-kernel.

Prevent errors when under annotating binders.
---
 kernel/typeops.mli | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index e57d6622c9..cc1885f42d 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -16,28 +16,28 @@ open Environ
 (** {6 Typing functions (not yet tagged as safe) }
 
     They return unsafe judgments that are "in context" of a set of
-    (local) universe variables (the ones that appear in the term)
-    and associated constraints. In case of polymorphic definitions,
-    these variables and constraints will be generalized.
- *)
+   (local) universe variables (the ones that appear in the term) and
+   associated constraints. In case of polymorphic definitions, these
+   variables and constraints will be generalized.
 
+    When typechecking a term it may be updated to fix relevance marks.
+   Do not discard the result. *)
 
 val infer      : env -> constr       -> unsafe_judgment
-val infer_v    : env -> constr array -> unsafe_judgment array
 val infer_type : env -> types        -> unsafe_type_judgment
 
 val check_context :
-  env -> Constr.rel_context -> env
+  env -> Constr.rel_context -> env * Constr.rel_context
 
 (** {6 Basic operations of the typing machine. } *)
 
 (** If [j] is the judgement {% $ %}c:t{% $ %}, then [assumption_of_judgement env j]
    returns the type {% $ %}c{% $ %}, checking that {% $ %}t{% $ %} is a sort. *)
 
-val assumption_of_judgment :  env -> unsafe_judgment -> types * Sorts.relevance
+val assumption_of_judgment :  env -> unsafe_judgment -> Sorts.relevance
 val type_judgment          :  env -> unsafe_judgment -> unsafe_type_judgment
 
-val check_binder_annot : env -> Sorts.t -> Name.t Context.binder_annot -> unit
+val check_binder_annot : Sorts.t -> Name.t Context.binder_annot -> Name.t Context.binder_annot
 
 (** {6 Type of sorts. } *)
 val type1 : types
@@ -130,3 +130,6 @@ val judge_of_int : env -> Uint63.t -> unsafe_judgment
 
 val type_of_prim_type : env -> CPrimitives.prim_type -> types
 val type_of_prim : env -> CPrimitives.t -> types
+
+val warn_bad_relevance_name : string
+(** Allow the checker to make this warning into an error. *)
-- 
cgit v1.2.3