walther@59866
|
1 |
(* Title: BaseDefinitions/rule-def.sml
|
walther@59849
|
2 |
Author: Walther Neuper
|
walther@59849
|
3 |
(c) due to copyright terms
|
walther@59849
|
4 |
|
walther@59850
|
5 |
A minimum of code for a mutual recursive datatype definition
|
walther@59850
|
6 |
awaiting individual specification later.
|
walther@59849
|
7 |
*)
|
walther@59849
|
8 |
signature RULE_DEFINITION =
|
walther@59850
|
9 |
sig
|
walther@59850
|
10 |
type calc
|
walther@59850
|
11 |
eqtype calID
|
walther@59850
|
12 |
eqtype errpatID
|
walther@59850
|
13 |
type rew_ord
|
walther@59850
|
14 |
type rew_ord'
|
walther@59850
|
15 |
type rew_ord_
|
walther@59850
|
16 |
type eval_fn
|
walther@59849
|
17 |
|
walther@59851
|
18 |
datatype rule_set =
|
walther@59851
|
19 |
Empty
|
walther@59851
|
20 |
| Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
|
walther@59851
|
21 |
preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
|
walther@59851
|
22 |
| Seqence of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
|
walther@59851
|
23 |
preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
|
walther@59851
|
24 |
| Rrls of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
|
walther@59850
|
25 |
prepat: (term list * term) list, rew_ord: rew_ord, scr: program}
|
walther@59850
|
26 |
and rule = Cal1 of string * eval_fn | Num_Calc of string * eval_fn | Erule
|
walther@59851
|
27 |
| Rls_ of rule_set | Thm of string * thm
|
walther@59850
|
28 |
and program =
|
walther@59850
|
29 |
EmptyScr
|
walther@59850
|
30 |
| Prog of term
|
walther@59850
|
31 |
| Rfuns of
|
walther@59850
|
32 |
{attach_form: rule list list -> term -> term -> (rule * (term * term list)) list,
|
walther@59850
|
33 |
init_state: term -> term * term * rule list list * (rule * (term * term list)) list,
|
walther@59850
|
34 |
locate_rule: rule list list -> term -> rule -> (rule * (term * term list)) list,
|
walther@59850
|
35 |
next_rule: rule list list -> term -> rule option, normal_form: term ->
|
walther@59850
|
36 |
(term * term list) option}
|
walther@59849
|
37 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59849
|
38 |
(*NONE*)
|
walther@59849
|
39 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59849
|
40 |
(*NONE*)
|
walther@59849
|
41 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59850
|
42 |
end
|
walther@59849
|
43 |
|
walther@59849
|
44 |
(**)
|
walther@59849
|
45 |
structure Rule_Def(**): RULE_DEFINITION(**) =
|
walther@59849
|
46 |
struct
|
walther@59849
|
47 |
(**)
|
walther@59849
|
48 |
|
walther@59849
|
49 |
type eval_fn = (string -> term -> theory -> (string * term) option);
|
walther@59849
|
50 |
|
walther@59849
|
51 |
type rew_ord' = string;
|
walther@59850
|
52 |
type rew_ord_ = (term * term) list -> term * term -> bool;
|
walther@59849
|
53 |
type rew_ord = rew_ord' * rew_ord_;
|
walther@59849
|
54 |
|
walther@59850
|
55 |
type calID = string;
|
walther@59849
|
56 |
type cal = calID * eval_fn;
|
walther@59849
|
57 |
type prog_calcID = string;
|
walther@59849
|
58 |
type calc = (prog_calcID * cal);
|
walther@59849
|
59 |
|
walther@59849
|
60 |
(* error patterns and fill patterns *)
|
walther@59849
|
61 |
type errpatID = string
|
walther@59849
|
62 |
|
walther@59849
|
63 |
(* all these different data justify a step in a calculation *)
|
walther@59849
|
64 |
datatype rule =
|
walther@59869
|
65 |
Erule (* the empty rule *)
|
walther@59869
|
66 |
| Thm of (* theorem associated with the identifier for reflection *)
|
walther@59869
|
67 |
string * (* needless since Thm.get_name_hint *)
|
walther@59869
|
68 |
Thm.thm (* see TODO CLEANUP Thm *)
|
walther@59869
|
69 |
| Num_Calc of (* evaluation by rewriting *)
|
walther@59869
|
70 |
string * (* unique identifier for the evaluation function *)
|
walther@59869
|
71 |
eval_fn (* evaluation function in ML code *)
|
walther@59869
|
72 |
| Cal1 of string * (* applied once to whole term or lhs/rhs of an eqality *)
|
walther@59869
|
73 |
eval_fn (* evaluation function in ML code *)
|
walther@59869
|
74 |
| Rls_ of rule_set (* rule sets may be nested *)
|
walther@59869
|
75 |
and program = (* program for Lucas-Interpretation *)
|
walther@59869
|
76 |
EmptyScr (* DEPRECATED: needless after removal of Rfuns *)
|
walther@59869
|
77 |
| Prog of term (* Lucas-Interpretation works on Isabelle's terms *)
|
walther@59869
|
78 |
| Rfuns of (* DEPRECATED, replaced by Auto_Prog *)
|
walther@59869
|
79 |
{init_state : (* initialise for reverse rewriting by the Interpreter *)
|
walther@59849
|
80 |
term -> (* for this the rrlsstate is initialised: *)
|
walther@59869
|
81 |
term * (* the current formula via istate *)
|
walther@59849
|
82 |
term * (* the final formula *)
|
walther@59849
|
83 |
rule list (* of reverse rewrite set (#1#) *)
|
walther@59849
|
84 |
list * (* may be serveral, eg. in norm_rational *)
|
walther@59869
|
85 |
( rule * (* Thm (+ Thm generated from Num_Calc) resulting in ... *)
|
walther@59849
|
86 |
(term * (* ... rewrite with ... *)
|
walther@59849
|
87 |
term list)) (* ... assumptions *)
|
walther@59869
|
88 |
list, (* derivation from given term to normalform in reverse order *)
|
walther@59869
|
89 |
normal_form: (* the function which drives the Rrls *)
|
walther@59849
|
90 |
term -> (term * term list) option,
|
walther@59869
|
91 |
locate_rule: (* checks a rule R for being a cancel-rule *)
|
walther@59849
|
92 |
rule list list -> (* the reverse rule list *)
|
walther@59849
|
93 |
term -> (* ... to which the rule shall be applied *)
|
walther@59849
|
94 |
rule -> (* ... to be applied to term *)
|
walther@59849
|
95 |
( rule * (* value: a rule rewriting to ... *)
|
walther@59849
|
96 |
(term * (* ... the resulting term ... *)
|
walther@59849
|
97 |
term list)) (* ... with the assumptions ( //#0) *)
|
walther@59869
|
98 |
list, (* there may be several such rules *)
|
walther@59869
|
99 |
next_rule: (* for a given term return the next rules to be done for cancel *)
|
walther@59849
|
100 |
rule list list->(* the reverse rule list *)
|
walther@59849
|
101 |
term -> (* the term for which ... *)
|
walther@59869
|
102 |
rule option, (* ... this rule is appropriate for cancellation *)
|
walther@59869
|
103 |
attach_form: (* checks an input term TI, if it may belong to a current cancel*)
|
walther@59869
|
104 |
rule list list->
|
walther@59849
|
105 |
term -> (* TG, the last one agreed upon by user + math-eng *)
|
walther@59849
|
106 |
term -> (* TI, the next one input by the user *)
|
walther@59849
|
107 |
( rule * (* the rule to be applied in order to reach TI *)
|
walther@59849
|
108 |
(term * (* ... obtained by applying the rule ... *)
|
walther@59849
|
109 |
term list)) (* ... and the respective assumptions *)
|
walther@59869
|
110 |
list} (* there may be several such rules; the list is empty, if ... *)
|
walther@59869
|
111 |
and rule_set = (* a collection for ordered & conditional rewriting *)
|
walther@59869
|
112 |
Empty (* empty Rule_Set.T *)
|
walther@59869
|
113 |
| Repeat of (*a confluent and terminating ruleset, in principle *)
|
walther@59869
|
114 |
{id: string, (* for trace_rewrite *)
|
walther@59869
|
115 |
preconds: term list, (* STILL UNUSED *)
|
walther@59869
|
116 |
rew_ord: rew_ord,(* for rules *)
|
walther@59869
|
117 |
erls: rule_set, (* for the conditions in rules *)
|
walther@59869
|
118 |
srls: rule_set, (* for evaluation of Prog_Expr *)
|
walther@59869
|
119 |
calc: calc list, (* for Calculate in program, set by prep_rls' *)
|
walther@59869
|
120 |
rules: rule list,
|
walther@59869
|
121 |
errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy *)
|
walther@59869
|
122 |
scr: program} (* DEPRECATED: intersteps are created on the fly now *)
|
walther@59869
|
123 |
| Seqence of (* a sequence of rules to be tried only once *)
|
walther@59869
|
124 |
{id: string, preconds: term list, rew_ord: rew_ord, erls: rule_set, srls: rule_set,
|
walther@59869
|
125 |
calc: calc list, rules: rule list, errpatts: errpatID list, scr: program}
|
walther@59869
|
126 |
| Rrls of (* ML-functions within rewriting, _ONE_ redex rewritten per call*)
|
walther@59869
|
127 |
{id: string, (* for trace_rewrite *)
|
walther@59869
|
128 |
prepat: (* a guard which guarantees a redex *)
|
walther@59869
|
129 |
(term list * (* preconds, eval with subst from pattern below *)
|
walther@59869
|
130 |
term) (* pattern matched with current (sub)term *)
|
walther@59869
|
131 |
list, (* meta-conjunction in guarding is or *)
|
walther@59869
|
132 |
rew_ord: rew_ord, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program}
|
walther@59850
|
133 |
|
walther@59849
|
134 |
(**)end(**)
|
walther@59849
|
135 |
|