diff options
| -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 |