From 861274890a73702aa4c8d74dac8991bdc0e840de Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 11 Jul 2020 15:10:42 +0200
Subject: rename file

---
 spartan/core/typechecking.ML | 53 ++++++++++++++++++++++++++++++++++++++++++++
 spartan/core/types.ML        | 29 ------------------------
 2 files changed, 53 insertions(+), 29 deletions(-)
 create mode 100644 spartan/core/typechecking.ML
 delete mode 100644 spartan/core/types.ML

diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML
new file mode 100644
index 0000000..437a2dc
--- /dev/null
+++ b/spartan/core/typechecking.ML
@@ -0,0 +1,53 @@
+(*  Title:      typechecking.ML
+    Author:     Joshua Chen
+
+Type information and typechecking infrastructure.
+*)
+
+structure Types: sig
+
+val Data: Proof.context -> thm Item_Net.T
+val types: Proof.context -> term -> thm list
+val put_type: thm -> Proof.context -> Proof.context
+val put_types: thm list -> Proof.context -> Proof.context
+
+val check: Proof.context -> thm -> int -> tactic
+val infer: Proof.context -> thm -> int -> tactic
+
+end = struct
+
+(* Context data *)
+
+structure Data = Generic_Data (
+  type T = thm Item_Net.T
+  val empty = Item_Net.init Thm.eq_thm
+    (single o Lib.term_of_typing o Thm.prop_of)
+  val extend = I
+  val merge = Item_Net.merge
+)
+
+val Data = Data.get o Context.Proof
+fun types ctxt tm = Item_Net.retrieve (Data ctxt) tm
+fun put_type typing = Context.proof_map (Data.map (Item_Net.update typing))
+fun put_types typings = foldr1 (op o) (map put_type typings)
+
+
+(* Checking and inference *)
+
+local
+
+fun checkable prop = Lib.is_typing prop
+  andalso not (exists_subterm is_Var (Lib.type_of_typing prop))
+
+in
+
+fun check ctxt rule = Subgoal.FOCUS_PREMS (
+  fn {context = goal_ctxt, prems, concl, ...} => no_tac) ctxt
+
+fun infer ctxt rule = Subgoal.FOCUS_PREMS (
+  fn {context = goal_ctxt, prems, concl, ...} => no_tac) ctxt
+
+end
+
+
+end
diff --git a/spartan/core/types.ML b/spartan/core/types.ML
deleted file mode 100644
index 1eaf60b..0000000
--- a/spartan/core/types.ML
+++ /dev/null
@@ -1,29 +0,0 @@
-(*  Title:      types.ML
-    Author:     Joshua Chen
-
-Type information storage.
-*)
-
-structure Types: sig
-
-val Data: Proof.context -> thm Item_Net.T
-val types: Proof.context -> term -> thm list
-val put_type: thm -> Proof.context -> Proof.context
-val put_types: thm list -> Proof.context -> Proof.context
-
-end = struct
-
-structure Data = Generic_Data (
-  type T = thm Item_Net.T
-  val empty = Item_Net.init Thm.eq_thm
-    (single o Lib.term_of_typing o Thm.prop_of)
-  val extend = I
-  val merge = Item_Net.merge
-)
-
-val Data = Data.get o Context.Proof
-fun types ctxt tm = Item_Net.retrieve (Data ctxt) tm
-fun put_type typing = Context.proof_map (Data.map (Item_Net.update typing))
-fun put_types typings = foldr1 (op o) (map put_type typings)
-
-end
-- 
cgit v1.2.3