From 58f891c100d1a1821ed6385c1d06f9e0a77ecdac Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 6 Nov 2018 09:30:45 +0100
Subject: Move debug term printer to kernel

---
 kernel/constr.ml  | 67 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 kernel/constr.mli |  3 +++
 kernel/sorts.ml   | 10 +++++++++
 kernel/sorts.mli  |  4 ++++
 4 files changed, 84 insertions(+)

(limited to 'kernel')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index d7f35da10d..704e6de6b8 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -1338,3 +1338,70 @@ type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt
 type rel_context = rel_declaration list
 type named_context = named_declaration list
 type compacted_context = compacted_declaration list
+
+(* Sorts and sort family *)
+
+let debug_print_fix pr_constr ((t,i),(lna,tl,bl)) =
+  let open Pp in
+  let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
+  hov 1
+      (str"fix " ++ int i ++ spc() ++  str"{" ++
+         v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
+           Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
+           cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
+         str"}")
+
+let pr_puniverses p u =
+  if Univ.Instance.is_empty u then p
+  else Pp.(p ++ str"(*" ++ Univ.Instance.pr Univ.Level.pr u ++ str"*)")
+
+(* Minimalistic constr printer, typically for debugging *)
+
+let rec debug_print c =
+  let open Pp in
+  match kind c with
+  | Rel n -> str "#"++int n
+  | Meta n -> str "Meta(" ++ int n ++ str ")"
+  | Var id -> Id.print id
+  | Sort s -> Sorts.debug_print s
+  | Cast (c,_, t) -> hov 1
+      (str"(" ++ debug_print c ++ cut() ++
+       str":" ++ debug_print t ++ str")")
+  | Prod (Name(id),t,c) -> hov 1
+      (str"forall " ++ Id.print id ++ str":" ++ debug_print t ++ str"," ++
+       spc() ++ debug_print c)
+  | Prod (Anonymous,t,c) -> hov 0
+      (str"(" ++ debug_print t ++ str " ->" ++ spc() ++
+       debug_print c ++ str")")
+  | Lambda (na,t,c) -> hov 1
+      (str"fun " ++ Name.print na ++ str":" ++
+       debug_print t ++ str" =>" ++ spc() ++ debug_print c)
+  | LetIn (na,b,t,c) -> hov 0
+      (str"let " ++ Name.print na ++ str":=" ++ debug_print b ++
+       str":" ++ brk(1,2) ++ debug_print t ++ cut() ++
+       debug_print c)
+  | App (c,l) ->  hov 1
+      (str"(" ++ debug_print c ++ spc() ++
+       prlist_with_sep spc debug_print (Array.to_list l) ++ str")")
+  | Evar (e,l) -> hov 1
+      (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
+       prlist_with_sep spc debug_print (Array.to_list l) ++str"}")
+  | Const (c,u) -> str"Cst(" ++ pr_puniverses (Constant.debug_print c) u ++ str")"
+  | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i) u ++ str")"
+  | Construct (((sp,i),j),u) ->
+      str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
+  | Proj (p,c) -> str"Proj(" ++ Constant.debug_print (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ debug_print c ++ str")"
+  | Case (_ci,p,c,bl) -> v 0
+      (hv 0 (str"<"++debug_print p++str">"++ cut() ++ str"Case " ++
+             debug_print c ++ str"of") ++ cut() ++
+       prlist_with_sep (fun _ -> brk(1,2)) debug_print (Array.to_list bl) ++
+      cut() ++ str"end")
+  | Fix f -> debug_print_fix debug_print f
+  | CoFix(i,(lna,tl,bl)) ->
+      let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in
+      hov 1
+        (str"cofix " ++ int i ++ spc() ++  str"{" ++
+         v 0 (prlist_with_sep spc (fun (na,ty,bd) ->
+           Name.print na ++ str":" ++ debug_print ty ++
+           cut() ++ str":=" ++ debug_print bd) (Array.to_list fixl)) ++
+         str"}")
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 8753c20eac..1be1f63ff7 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -590,3 +590,6 @@ val case_info_hash : case_info -> int
 (*********************************************************************)
 
 val hcons : constr -> constr
+
+val debug_print : constr -> Pp.t
+val debug_print_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index a7bb08f5b6..566dce04c6 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -102,3 +102,13 @@ module Hsorts =
     end)
 
 let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ
+
+let debug_print = function
+  | Set -> Pp.(str "Set")
+  | Prop -> Pp.(str "Prop")
+  | Type u -> Pp.(str "Type(" ++ Univ.Universe.pr u ++ str ")")
+
+let pr_sort_family = function
+  | InSet -> Pp.(str "Set")
+  | InProp -> Pp.(str "Prop")
+  | InType -> Pp.(str "Type")
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index cac6229b91..6c5ce4df80 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -41,3 +41,7 @@ end
 
 val univ_of_sort : t -> Univ.Universe.t
 val sort_of_univ : Univ.Universe.t -> t
+
+val debug_print : t -> Pp.t
+
+val pr_sort_family : family -> Pp.t
-- 
cgit v1.2.3


From a1bdaf0635b5d5b9e007662f324dd526ba0fe8d3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 9 Oct 2018 18:21:04 +0200
Subject: [checker] Refactor by sharing code with the kernel

For historical reasons, the checker was duplicating a lot of code of the
kernel. The main differences I found were bug fixes that had not been
backported.

With this patch, the checker uses the kernel as a library to serve the
same purpose as before: validation of a `.vo` file, re-typechecking all
definitions a posteriori.

We also rename some files from the checker so that they don't clash with
kernel files.
---
 kernel/indtypes.mli    | 13 +++++++++++++
 kernel/safe_typing.ml  |  2 ++
 kernel/safe_typing.mli |  4 ++++
 3 files changed, 19 insertions(+)

(limited to 'kernel')

diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index cb09cfa827..a827c17683 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -34,6 +34,19 @@ type inductive_error =
 
 exception InductiveError of inductive_error
 
+val infos_and_sort : env -> constr -> Univ.Universe.t
+
+val check_subtyping_arity_constructor : env -> (constr -> constr) -> types -> int -> bool -> unit
+
+val check_positivity : chkpos:bool ->
+           Names.MutInd.t ->
+           Environ.env ->
+           (Constr.constr, Constr.types) Context.Rel.pt ->
+           Declarations.recursivity_kind ->
+           ('a * Names.Id.t list * Constr.types array *
+            (('b, 'c) Context.Rel.pt * 'd))
+           array -> Int.t * Declarations.recarg Rtree.t array
+
 (** The following function does checks on inductive declarations. *)
 
 val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4b64cc6d11..8b11851bbb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1061,6 +1061,8 @@ type compiled_library = {
   comp_natsymbs : Nativecode.symbols
 }
 
+let module_of_library lib = lib.comp_mod
+
 type native_library = Nativecode.global list
 
 let get_library_native_symbols senv dir =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 8fb33b04d4..7af773e3bc 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -141,6 +141,8 @@ val set_share_reduction : bool -> safe_transformer0
 val set_VM : bool -> safe_transformer0
 val set_native_compiler : bool -> safe_transformer0
 
+val check_engagement : Environ.env -> Declarations.set_predicativity -> unit
+
 (** {6 Interactive module functions } *)
 
 val start_module : Label.t -> ModPath.t safe_transformer
@@ -177,6 +179,8 @@ type compiled_library
 
 type native_library = Nativecode.global list
 
+val module_of_library : compiled_library -> Declarations.module_body
+
 val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols
 
 val start_library : DirPath.t -> ModPath.t safe_transformer
-- 
cgit v1.2.3