Reorganize theory structure. In particular, the identity type moves out from under Spartan to HoTT. Spartan now only has Pi and Sigma.

16 files changed, 30 insertions, 14 deletions

diff --git a/ROOT b/ROOT
index 09e3042..1e8017c 100644
--- a/ROOT
+++ b/ROOT
@@ -1,15 +1,23 @@
-session Spartan in "spartan/theories" = Pure +
+session Spartan_Core in "spartan/core" = Pure +
   description "
     Spartan type theory: a minimal dependent type theory based on
     intensional Martin-Löf type theory with cumulative Russell-style universes,
-    Pi, Sigma and identity types.
+    Pi, Sigma and identity types. This session consists only of the very core
+    theory files.
   "
   sessions
     "HOL-Eisbach"
   theories
     Spartan (global)
-    Identity
-    Equivalence
+
+session Spartan in spartan = Spartan_Core +
+  description "
+    Type theory based on Spartan, but with a few more bells and whistles.
+  "
+  directories
+    data
+  theories
+    "data/List"
 
 session HoTT in hott = Spartan +
   description "
@@ -21,5 +29,7 @@ session HoTT in hott = Spartan +
   "
   theories
     Base
+    Identity
+    Equivalence
     Nat
 
diff --git a/hott/Base.thy b/hott/Base.thy
index 2a4ff9c..610a373 100644
--- a/hott/Base.thy
+++ b/hott/Base.thy
@@ -1,5 +1,5 @@
 theory Base
-imports Spartan.Equivalence
+imports Equivalence
 
 begin
 
diff --git a/spartan/theories/Equivalence.thy b/hott/Equivalence.thy
index 2975738..2975738 100644
--- a/spartan/theories/Equivalence.thy
+++ b/hott/Equivalence.thy
diff --git a/spartan/theories/Identity.thy b/hott/Identity.thy
index 3a982f6..3a982f6 100644
--- a/spartan/theories/Identity.thy
+++ b/hott/Identity.thy
diff --git a/spartan/theories/Spartan.thy b/spartan/core/Spartan.thy
index d235041..b4f7772 100644
--- a/spartan/theories/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -142,20 +142,20 @@ section \<open>Proof commands\<close>
 
 named_theorems typechk
 
-ML_file \<open>../lib/lib.ML\<close>
-ML_file \<open>../lib/goals.ML\<close>
-ML_file \<open>../lib/focus.ML\<close>
+ML_file \<open>lib.ML\<close>
+ML_file \<open>goals.ML\<close>
+ML_file \<open>focus.ML\<close>
 
 
 section \<open>Congruence automation\<close>
 
 (*Potential to be retired*)
-ML_file \<open>../lib/congruence.ML\<close>
+ML_file \<open>congruence.ML\<close>
 
 
 section \<open>Methods\<close>
 
-ML_file \<open>../lib/elimination.ML\<close> \<comment> \<open>declares the [elims] attribute\<close>
+ML_file \<open>elimination.ML\<close> \<comment> \<open>declares the [elims] attribute\<close>
 
 named_theorems intros and comps
 lemmas
@@ -165,7 +165,7 @@ lemmas
   [comps] = beta Sig_comp and
   [cong] = Pi_cong lam_cong Sig_cong
 
-ML_file \<open>../lib/tactics.ML\<close>
+ML_file \<open>tactics.ML\<close>
 
 method_setup assumptions =
   \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (
@@ -227,7 +227,7 @@ ML_file "~~/src/Tools/misc_legacy.ML"
 ML_file "~~/src/Tools/IsaPlanner/isand.ML"
 ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
 ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
-ML_file "../lib/eqsubst.ML"
+ML_file "eqsubst.ML"
 
 \<comment> \<open>\<open>rewrite\<close> method\<close>
 consts rewrite_HOLE :: "'a::{}"  ("\<hole>")
@@ -254,7 +254,7 @@ lemma imp_cong_eq:
   done
 
 ML_file \<open>~~/src/HOL/Library/cconv.ML\<close>
-ML_file \<open>../lib/rewrite.ML\<close>
+ML_file \<open>rewrite.ML\<close>
 
 \<comment> \<open>\<open>reduce\<close> computes terms via judgmental equalities\<close>
 setup \<open>map_theory_simpset (fn ctxt => ctxt addSolver (mk_solver "" typechk_tac))\<close>
@@ -273,7 +273,7 @@ consts
   iarg :: \<open>'a\<close> ("?")
   hole :: \<open>'b\<close> ("{}")
 
-ML_file \<open>../lib/implicits.ML\<close>
+ML_file \<open>implicits.ML\<close>
 
 attribute_setup implicit = \<open>Scan.succeed Implicits.implicit_defs_attr\<close>
 
diff --git a/spartan/lib/congruence.ML b/spartan/core/congruence.ML
index bb7348c..bb7348c 100644
--- a/spartan/lib/congruence.ML
+++ b/spartan/core/congruence.ML
diff --git a/spartan/lib/elimination.ML b/spartan/core/elimination.ML
index 617f83e..617f83e 100644
--- a/spartan/lib/elimination.ML
+++ b/spartan/core/elimination.ML
diff --git a/spartan/lib/eqsubst.ML b/spartan/core/eqsubst.ML
index ea6f098..ea6f098 100644
--- a/spartan/lib/eqsubst.ML
+++ b/spartan/core/eqsubst.ML
diff --git a/spartan/lib/equality.ML b/spartan/core/equality.ML
index 023147b..023147b 100644
--- a/spartan/lib/equality.ML
+++ b/spartan/core/equality.ML
diff --git a/spartan/lib/focus.ML b/spartan/core/focus.ML
index 1d8de78..1d8de78 100644
--- a/spartan/lib/focus.ML
+++ b/spartan/core/focus.ML
diff --git a/spartan/lib/goals.ML b/spartan/core/goals.ML
index 9f394f0..9f394f0 100644
--- a/spartan/lib/goals.ML
+++ b/spartan/core/goals.ML
diff --git a/spartan/lib/implicits.ML b/spartan/core/implicits.ML
index 04fc825..04fc825 100644
--- a/spartan/lib/implicits.ML
+++ b/spartan/core/implicits.ML
diff --git a/spartan/lib/lib.ML b/spartan/core/lib.ML
index 615f601..615f601 100644
--- a/spartan/lib/lib.ML
+++ b/spartan/core/lib.ML
diff --git a/spartan/lib/rewrite.ML b/spartan/core/rewrite.ML
index f9c5d8e..f9c5d8e 100644
--- a/spartan/lib/rewrite.ML
+++ b/spartan/core/rewrite.ML
diff --git a/spartan/lib/tactics.ML b/spartan/core/tactics.ML
index f23bfee..f23bfee 100644
--- a/spartan/lib/tactics.ML
+++ b/spartan/core/tactics.ML
diff --git a/spartan/data/List.thy b/spartan/data/List.thy
new file mode 100644
index 0000000..71a879b
--- /dev/null
+++ b/spartan/data/List.thy
@@ -0,0 +1,6 @@
+theory List
+imports Spartan
+
+begin
+
+end