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