12 datatype program = datatype Rule_Def.program |
12 datatype program = datatype Rule_Def.program |
13 |
13 |
14 val set_id: Rule_Def.rule_set -> string |
14 val set_id: Rule_Def.rule_set -> string |
15 val id: rule -> string |
15 val id: rule -> string |
16 val equal: rule * rule -> bool |
16 val equal: rule * rule -> bool |
17 val to_string: rule -> string |
17 val to_string: Proof.context -> rule -> string |
18 val to_string_PIDE: Proof.context -> rule -> string |
|
19 val to_string_short: rule -> string |
18 val to_string_short: rule -> string |
20 val s_to_string: rule list -> string |
19 val s_to_string: rule list -> string |
21 |
20 |
22 val thm: rule -> thm |
21 val thm: Proof.context -> rule -> thm |
23 val distinct' : rule list -> rule list |
22 val distinct' : rule list -> rule list |
24 |
23 |
25 val thm_id: rule -> string |
24 val thm_id: rule -> string |
26 val eval: rule -> string * Rule_Def.eval_fn |
25 val eval: Proof.context -> rule -> string * Rule_Def.eval_fn |
27 val rls: rule -> Rule_Def.rule_set |
26 val rls: Proof.context -> rule -> Rule_Def.rule_set |
28 |
27 |
29 val make_eval: string -> Rule_Def.eval_fn -> rule |
28 val make_eval: string -> Rule_Def.eval_fn -> rule |
30 end |
29 end |
31 |
30 |
32 (**) |
31 (**) |
56 | equal (Rule_Def.Eval (id1, _), Rule_Def.Eval (id2, _)) = id1 = id2 |
55 | equal (Rule_Def.Eval (id1, _), Rule_Def.Eval (id2, _)) = id1 = id2 |
57 | equal (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = set_id rls1 = set_id rls2 |
56 | equal (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = set_id rls1 = set_id rls2 |
58 | equal _ = false; |
57 | equal _ = false; |
59 fun distinct' rs = distinct equal rs |
58 fun distinct' rs = distinct equal rs |
60 |
59 |
61 fun to_string_PIDE _ Rule_Def.Erule = "Erule" |
60 fun to_string _ Rule_Def.Erule = "Erule" |
62 | to_string_PIDE ctxt (Rule_Def.Thm (str, thm)) = |
61 | to_string ctxt (Rule_Def.Thm (str, thm)) = |
63 "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm_PIDE ctxt thm ^ ")" |
62 "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm_PIDE ctxt thm ^ ")" |
64 | to_string_PIDE _ (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)" |
63 | to_string _ (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)" |
65 | to_string_PIDE _ (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" |
64 | to_string _ (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" |
66 | to_string_PIDE _ (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")"; |
65 | to_string _ (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")"; |
67 fun to_string Rule_Def.Erule = "Erule" |
|
68 | to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm thm ^ ")" |
|
69 | to_string (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)" |
|
70 | to_string (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" |
|
71 | to_string (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")"; |
|
72 fun to_string_short Rule_Def.Erule = "Erule" |
66 fun to_string_short Rule_Def.Erule = "Erule" |
73 | to_string_short (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")" |
67 | to_string_short (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")" |
74 | to_string_short (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)" |
68 | to_string_short (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)" |
75 | to_string_short (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" |
69 | to_string_short (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" |
76 | to_string_short (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")"; |
70 | to_string_short (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")"; |
77 fun s_to_string rules = rules |> map to_string_short |> commas |> enclose "[" "]" |
71 fun s_to_string rules = rules |> map to_string_short |> commas |> enclose "[" "]" |
78 |
72 |
79 fun thm_id (Rule_Def.Thm (id, _)) = id |
73 fun thm_id (Rule_Def.Thm (id, _)) = id |
80 | thm_id _ = raise ERROR ("Rule.thm_id: uncovered case " (* ^ to_string r *)) |
74 | thm_id _ = raise ERROR ("Rule.thm_id: uncovered case " (* ^ to_string r *)) |
81 fun thm (Rule_Def.Thm (_, thm)) = thm |
75 fun thm _ (Rule_Def.Thm (_, thm)) = thm |
82 | thm r = raise ERROR ("Rule.thm: uncovered case " ^ to_string r) |
76 | thm ctxt r = raise ERROR ("Rule.thm: uncovered case " ^ to_string ctxt r) |
83 |
77 |
84 fun eval (Eval e) = e |
78 fun eval _ (Eval e) = e |
85 | eval r = raise ERROR ("Rule.eval NOT FOR " ^ to_string r) |
79 | eval ctxt r = raise ERROR ("Rule.eval NOT FOR " ^ to_string ctxt r) |
86 fun rls (Rls_ rls) = rls |
80 fun rls _ (Rls_ rls) = rls |
87 | rls r = raise ERROR ("Rule.rls NOT FOR " ^ to_string r) |
81 | rls ctxt r = raise ERROR ("Rule.rls NOT FOR " ^ to_string ctxt r) |
88 |
82 |
89 |
83 |
90 (* ML antiquotations *) |
84 (* ML antiquotations *) |
91 |
85 |
92 val make_eval = curry Eval; |
86 val make_eval = curry Eval; |