blob: 437a2dccd44705fba4dea44fac69ac292f65e1ed (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
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
|
