From 5bb9833e5655039740dadc56ad993f879c7e127b Mon Sep 17 00:00:00 2001
From: Kaustuv Chaudhuri <kaustuv.chaudhuri@inria.fr>
Date: Wed, 5 Jan 2022 16:37:47 +0100
Subject: [PATCH] Bugfix: Type and Kind declarations were not being committed

We now treat Type and Kind declarations as signature extensions
at the reasoning level, not at the specification level.

This still allows for the following style of declaration:

     Kind nat type.
     Import "nats".   % this also has Kind nat type.

However, you can now also do just:

     Import "nats".

and get the "nat" type declaration for free. There is no
longer any need to repeat the Type declarations before an
Import.
---
 CHANGES       |  3 +++
 src/abella.ml | 17 ++++++++++++++---
 2 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/CHANGES b/CHANGES
index 81dc27d1..26f90129 100644
--- a/CHANGES
+++ b/CHANGES
@@ -23,6 +23,9 @@ Bugfixes
 * Automatic compilation in `Import` statements now does not clobber existing
   partial compilation results. This improves the support for multiple runs
   of Abella in parallel using the same source files.
+* The *first* Type or Kind declaration was accidentally being added to
+  the specification signature.  
+  (Identified by Farah Al Wardani, @innofarah)
 
 
 Changes in 2.0.7
diff --git a/src/abella.ml b/src/abella.ml
index 036d9ccc..6c84c83b 100644
--- a/src/abella.ml
+++ b/src/abella.ml
@@ -241,6 +241,14 @@ let comp_spec_sign = State.rref ([], [])
 let comp_spec_clauses = State.rref []
 let comp_content = State.rref []
 
+let debug_spec_sign1 ?(msg="") () =
+  let (kt, ct) = !comp_spec_sign in
+  Printf.printf "DEBUG: %sspec_ktable = [%s], spec_ctable = [%s]\n"
+    (if msg = "" then "" else "[" ^ msg ^ "] ")
+    (String.concat "," (List.map fst kt))
+    (String.concat "," (List.map fst ct))
+let debug_spec_sign ?(msg="") () = ignore msg
+
 let marshal citem =
   match !compile_out with
   | Some cout -> Marshal.to_channel cout citem []
@@ -254,7 +262,7 @@ let ensure_finalized_specification () =
   end
 
 let compile citem =
-  ensure_finalized_specification () ;
+  (* ensure_finalized_specification () ; *)
   comp_content := citem :: !comp_content
 
 let predicates (_ktable, ctable) =
@@ -267,6 +275,7 @@ let predicates (_ktable, ctable) =
 let write_compilation () =
   marshal Version.self_digest ;
   marshal Version.version ;
+  debug_spec_sign ~msg:"write_compilation" () ;
   marshal !comp_spec_sign ;
   marshal !comp_spec_clauses ;
   marshal (predicates !sign) ;
@@ -853,11 +862,13 @@ and process_top1 () =
   | Kind(ids,knd) ->
       check_noredef ids;
       Prover.add_global_types ids knd;
-      compile (CKind (ids,knd))
+      compile (CKind (ids,knd)) ;
+      debug_spec_sign ~msg:"Kind" ()
   | Type(ids, ty) ->
       check_noredef ids;
       Prover.add_global_consts (List.map (fun id -> (id, ty)) ids) ;
-      compile (CType(ids, ty))
+      compile (CType(ids, ty)) ;
+      debug_spec_sign ~msg:"Type" ()
   | Close(atys) ->
       Prover.close_types !sign !Prover.clauses atys ;
       compile (CClose(List.map (fun aty -> (aty, Subordination.subordinates !sr aty)) atys))