14 val set_id: Rule_Def.rule_set -> string |
14 val set_id: Rule_Def.rule_set -> string |
15 val id: Rule_Def.rule -> string |
15 val id: Rule_Def.rule -> string |
16 val equal: Rule_Def.rule * Rule_Def.rule -> bool |
16 val equal: Rule_Def.rule * Rule_Def.rule -> bool |
17 val to_string: Rule_Def.rule -> string |
17 val to_string: Rule_Def.rule -> string |
18 val to_string_short: Rule_Def.rule -> string |
18 val to_string_short: Rule_Def.rule -> string |
|
19 val s_to_string: rule list -> string |
19 |
20 |
20 val thm: rule -> thm |
21 val thm: rule -> thm |
21 val distinct' : rule list -> rule list |
22 val distinct' : rule list -> rule list |
22 |
23 |
23 val thm_id: rule -> string |
24 val thm_id: rule -> string |
64 fun to_string_short Rule_Def.Erule = "Erule" |
65 fun to_string_short Rule_Def.Erule = "Erule" |
65 | to_string_short (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")" |
66 | to_string_short (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")" |
66 | to_string_short (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)" |
67 | to_string_short (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)" |
67 | to_string_short (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" |
68 | to_string_short (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" |
68 | to_string_short (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")"; |
69 | to_string_short (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")"; |
|
70 fun s_to_string rules = rules |> map to_string_short |> commas |> enclose "[" "]" |
69 |
71 |
70 fun thm_id (Rule_Def.Thm (id, _)) = id |
72 fun thm_id (Rule_Def.Thm (id, _)) = id |
71 | thm_id _ = raise ERROR ("Rule.thm_id: uncovered case " (* ^ to_string r *)) |
73 | thm_id _ = raise ERROR ("Rule.thm_id: uncovered case " (* ^ to_string r *)) |
72 fun thm (Rule_Def.Thm (_, thm)) = thm |
74 fun thm (Rule_Def.Thm (_, thm)) = thm |
73 | thm r = raise ERROR ("Rule.thm: uncovered case " ^ to_string r) |
75 | thm r = raise ERROR ("Rule.thm: uncovered case " ^ to_string r) |