aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2020-07-11 15:10:42 +0200
committerJosh Chen2020-07-11 15:10:42 +0200
commit861274890a73702aa4c8d74dac8991bdc0e840de (patch)
treeabfd90e62063436333924e6acf4ddac7960af996
parent831f33468f227c0dc96bd31380236f2c77e70c52 (diff)
rename file
-rw-r--r--spartan/core/typechecking.ML (renamed from spartan/core/types.ML)28
1 files changed, 26 insertions, 2 deletions
diff --git a/spartan/core/types.ML b/spartan/core/typechecking.ML
index 1eaf60b..437a2dc 100644
--- a/spartan/core/types.ML
+++ b/spartan/core/typechecking.ML
@@ -1,7 +1,7 @@
-(* Title: types.ML
+(* Title: typechecking.ML
Author: Joshua Chen
-Type information storage.
+Type information and typechecking infrastructure.
*)
structure Types: sig
@@ -11,8 +11,13 @@ 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
@@ -26,4 +31,23 @@ 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