walther@59866
|
1 |
(* Title: BaseDefinitions/rule.sml
|
walther@59850
|
2 |
Author: Walther Neuper 2018
|
wneuper@59415
|
3 |
(c) copyright due to lincense terms
|
walther@59850
|
4 |
|
walther@59858
|
5 |
TODO: use "Rule" for renaming identifiers.
|
walther@59861
|
6 |
Some stuff waits for later rounds of restructuring, e.g. TermC.empty
|
wneuper@59415
|
7 |
*)
|
wneuper@59415
|
8 |
|
wneuper@59415
|
9 |
signature RULE =
|
walther@59850
|
10 |
sig
|
walther@59850
|
11 |
datatype rule = datatype Rule_Def.rule
|
walther@59850
|
12 |
datatype program = datatype Rule_Def.program
|
walther@59849
|
13 |
|
walther@59867
|
14 |
val set_id: Rule_Def.rule_set -> string
|
walther@59867
|
15 |
val id: Rule_Def.rule -> string
|
walther@59867
|
16 |
val equal: Rule_Def.rule * Rule_Def.rule -> bool
|
walther@59867
|
17 |
val to_string: Rule_Def.rule -> string
|
walther@59867
|
18 |
val to_string_short: Rule_Def.rule -> string
|
walther@59864
|
19 |
|
walther@59876
|
20 |
val thm: rule -> thm
|
walther@60017
|
21 |
val distinct' : rule list -> rule list
|
walther@59914
|
22 |
|
walther@59876
|
23 |
val thm_id: rule -> string
|
walther@60389
|
24 |
val eval: rule -> string * Rule_Def.eval_fn
|
walther@60389
|
25 |
val rls: rule -> Rule_Def.rule_set
|
wenzelm@60294
|
26 |
|
wenzelm@60294
|
27 |
val make_eval: string -> Rule_Def.eval_fn -> rule
|
walther@59850
|
28 |
end
|
wneuper@59415
|
29 |
|
wneuper@59415
|
30 |
(**)
|
wneuper@59415
|
31 |
structure Rule(**): RULE(**) =
|
wneuper@59415
|
32 |
struct
|
wneuper@59415
|
33 |
(**)
|
wneuper@59415
|
34 |
|
walther@59867
|
35 |
datatype rule = datatype Rule_Def.rule;
|
walther@59867
|
36 |
datatype program = datatype Rule_Def.program;
|
walther@59876
|
37 |
type is_as_string = string;
|
walther@59850
|
38 |
|
walther@59867
|
39 |
type calc = Rule_Def.calc
|
walther@59867
|
40 |
type calID = Rule_Def.calID;
|
walther@59867
|
41 |
type eval_fn = Rule_Def.eval_fn;
|
wneuper@59416
|
42 |
|
walther@60384
|
43 |
fun set_id Rule_Def.Empty = "empty"
|
walther@59867
|
44 |
| set_id (Rule_Def.Repeat {id, ...}) = id
|
walther@59878
|
45 |
| set_id (Rule_Def.Sequence {id, ...}) = id
|
walther@59867
|
46 |
| set_id (Rule_Def.Rrls {id, ...}) = id;
|
wneuper@59416
|
47 |
|
walther@59867
|
48 |
fun id (Rule_Def.Thm (id, _)) = id
|
walther@59878
|
49 |
| id (Rule_Def.Eval (id, _)) = id
|
walther@59867
|
50 |
| id (Rule_Def.Cal1 (id, _)) = id
|
walther@59867
|
51 |
| id (Rule_Def.Rls_ rls) = set_id rls
|
walther@59867
|
52 |
| id Rule_Def.Erule = "Erule";
|
walther@59867
|
53 |
fun equal (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2
|
walther@59878
|
54 |
| equal (Rule_Def.Eval (id1, _), Rule_Def.Eval (id2, _)) = id1 = id2
|
walther@59867
|
55 |
| equal (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = set_id rls1 = set_id rls2
|
walther@59867
|
56 |
| equal _ = false;
|
walther@60017
|
57 |
fun distinct' rs = distinct equal rs
|
walther@59861
|
58 |
|
walther@59867
|
59 |
fun to_string Rule_Def.Erule = "Erule"
|
walther@59997
|
60 |
| to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm thm ^ ")"
|
walther@59878
|
61 |
| to_string (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
|
walther@59867
|
62 |
| to_string (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
|
walther@59867
|
63 |
| to_string (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
|
walther@59867
|
64 |
fun to_string_short Rule_Def.Erule = "Erule"
|
walther@59867
|
65 |
| to_string_short (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"
|
walther@59878
|
66 |
| to_string_short (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
|
walther@59867
|
67 |
| to_string_short (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
|
walther@59867
|
68 |
| to_string_short (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
|
walther@59864
|
69 |
|
walther@59876
|
70 |
fun thm_id (Rule_Def.Thm (id, _)) = id
|
walther@59876
|
71 |
| thm_id _ = raise ERROR ("Rule.thm_id: uncovered case " (* ^ to_string r *))
|
walther@59876
|
72 |
fun thm (Rule_Def.Thm (_, thm)) = thm
|
walther@59876
|
73 |
| thm r = raise ERROR ("Rule.thm: uncovered case " ^ to_string r)
|
walther@59876
|
74 |
|
walther@60389
|
75 |
fun eval (Eval e) = e
|
walther@60389
|
76 |
| eval r = raise ERROR ("Rule.eval NOT FOR " ^ to_string r)
|
walther@60389
|
77 |
fun rls (Rls_ rls) = rls
|
walther@60389
|
78 |
| rls r = raise ERROR ("Rule.rls NOT FOR " ^ to_string r)
|
walther@60389
|
79 |
|
wenzelm@60294
|
80 |
|
wenzelm@60294
|
81 |
(* ML antiquotations *)
|
wenzelm@60294
|
82 |
|
wenzelm@60294
|
83 |
val make_eval = curry Eval;
|
wenzelm@60294
|
84 |
|
wenzelm@60294
|
85 |
val _ = Theory.setup
|
wenzelm@60294
|
86 |
(ML_Antiquotation.value_embedded \<^binding>\<open>rule_eval\<close>
|
wenzelm@60294
|
87 |
(Args.const {proper = true, strict = true} >>
|
wenzelm@60294
|
88 |
(fn name => "Rule.make_eval " ^ ML_Syntax.print_string name)));
|
wenzelm@60294
|
89 |
|
walther@59861
|
90 |
(**)end(**)
|