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@59919
|
5 |
Here is a minimum of code required for Know_Store.thy.
|
walther@59919
|
6 |
For main code see structure Rule.
|
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
|
wenzelm@60293
|
13 |
type rew_ord' = string
|
wenzelm@60293
|
14 |
type rew_ord_ = (term * term) list -> term * term -> bool
|
wenzelm@60293
|
15 |
type rew_ord = rew_ord' * rew_ord_
|
wenzelm@60293
|
16 |
type eval_fn = string -> term -> theory -> (string * term) option
|
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@59878
|
22 |
| Sequence 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@59878
|
26 |
and rule = Cal1 of string * eval_fn | Eval of string * eval_fn | Erule
|
walther@59851
|
27 |
| Rls_ of rule_set | Thm of string * thm
|
walther@59850
|
28 |
and program =
|
walther@59878
|
29 |
Empty_Prog
|
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@60436
|
37 |
val rule_to_string: program -> string
|
walther@59850
|
38 |
end
|
walther@59849
|
39 |
|
walther@59849
|
40 |
(**)
|
walther@59849
|
41 |
structure Rule_Def(**): RULE_DEFINITION(**) =
|
walther@59849
|
42 |
struct
|
walther@59849
|
43 |
(**)
|
walther@59849
|
44 |
|
wenzelm@60293
|
45 |
type eval_fn = string -> term -> theory -> (string * term) option;
|
walther@59849
|
46 |
|
walther@59849
|
47 |
type rew_ord' = string;
|
walther@59850
|
48 |
type rew_ord_ = (term * term) list -> term * term -> bool;
|
walther@59849
|
49 |
type rew_ord = rew_ord' * rew_ord_;
|
walther@59849
|
50 |
|
walther@59850
|
51 |
type calID = string;
|
walther@59849
|
52 |
type cal = calID * eval_fn;
|
walther@59849
|
53 |
type prog_calcID = string;
|
walther@59849
|
54 |
type calc = (prog_calcID * cal);
|
walther@59849
|
55 |
|
walther@59849
|
56 |
(* error patterns and fill patterns *)
|
walther@59849
|
57 |
type errpatID = string
|
walther@59849
|
58 |
|
walther@59849
|
59 |
(* all these different data justify a step in a calculation *)
|
walther@59849
|
60 |
datatype rule =
|
walther@59869
|
61 |
Erule (* the empty rule *)
|
walther@59869
|
62 |
| Thm of (* theorem associated with the identifier for reflection *)
|
walther@60370
|
63 |
string * (* required for ThmC.sym_thm *)
|
walther@59869
|
64 |
Thm.thm (* see TODO CLEANUP Thm *)
|
wenzelm@60293
|
65 |
| Eval of (* evaluation by rewriting *)
|
walther@59869
|
66 |
string * (* unique identifier for the evaluation function *)
|
walther@59869
|
67 |
eval_fn (* evaluation function in ML code *)
|
walther@59869
|
68 |
| Cal1 of string * (* applied once to whole term or lhs/rhs of an eqality *)
|
walther@59869
|
69 |
eval_fn (* evaluation function in ML code *)
|
walther@59869
|
70 |
| Rls_ of rule_set (* rule sets may be nested *)
|
walther@59869
|
71 |
and program = (* program for Lucas-Interpretation *)
|
wenzelm@60293
|
72 |
Empty_Prog (* DEPRECATED: needless after removal of Rfuns *)
|
walther@59869
|
73 |
| Prog of term (* Lucas-Interpretation works on Isabelle's terms *)
|
walther@59869
|
74 |
| Rfuns of (* DEPRECATED, replaced by Auto_Prog *)
|
walther@59869
|
75 |
{init_state : (* initialise for reverse rewriting by the Interpreter *)
|
walther@59849
|
76 |
term -> (* for this the rrlsstate is initialised: *)
|
walther@59869
|
77 |
term * (* the current formula via istate *)
|
walther@59849
|
78 |
term * (* the final formula *)
|
walther@59849
|
79 |
rule list (* of reverse rewrite set (#1#) *)
|
walther@59849
|
80 |
list * (* may be serveral, eg. in norm_rational *)
|
walther@59878
|
81 |
( rule * (* Thm (+ Thm generated from Eval) resulting in ... *)
|
walther@59849
|
82 |
(term * (* ... rewrite with ... *)
|
walther@59849
|
83 |
term list)) (* ... assumptions *)
|
walther@59869
|
84 |
list, (* derivation from given term to normalform in reverse order *)
|
walther@59869
|
85 |
normal_form: (* the function which drives the Rrls *)
|
walther@59849
|
86 |
term -> (term * term list) option,
|
walther@59869
|
87 |
locate_rule: (* checks a rule R for being a cancel-rule *)
|
walther@59849
|
88 |
rule list list -> (* the reverse rule list *)
|
walther@59849
|
89 |
term -> (* ... to which the rule shall be applied *)
|
walther@59849
|
90 |
rule -> (* ... to be applied to term *)
|
walther@59849
|
91 |
( rule * (* value: a rule rewriting to ... *)
|
walther@59849
|
92 |
(term * (* ... the resulting term ... *)
|
walther@59849
|
93 |
term list)) (* ... with the assumptions ( //#0) *)
|
walther@59869
|
94 |
list, (* there may be several such rules *)
|
walther@59869
|
95 |
next_rule: (* for a given term return the next rules to be done for cancel *)
|
walther@59849
|
96 |
rule list list->(* the reverse rule list *)
|
walther@59849
|
97 |
term -> (* the term for which ... *)
|
walther@59869
|
98 |
rule option, (* ... this rule is appropriate for cancellation *)
|
walther@59869
|
99 |
attach_form: (* checks an input term TI, if it may belong to a current cancel*)
|
walther@59869
|
100 |
rule list list->
|
walther@59849
|
101 |
term -> (* TG, the last one agreed upon by user + math-eng *)
|
walther@59849
|
102 |
term -> (* TI, the next one input by the user *)
|
walther@59849
|
103 |
( rule * (* the rule to be applied in order to reach TI *)
|
walther@59849
|
104 |
(term * (* ... obtained by applying the rule ... *)
|
walther@59849
|
105 |
term list)) (* ... and the respective assumptions *)
|
walther@59869
|
106 |
list} (* there may be several such rules; the list is empty, if ... *)
|
walther@59869
|
107 |
and rule_set = (* a collection for ordered & conditional rewriting *)
|
walther@59869
|
108 |
Empty (* empty Rule_Set.T *)
|
walther@59869
|
109 |
| Repeat of (*a confluent and terminating ruleset, in principle *)
|
walther@59869
|
110 |
{id: string, (* for trace_rewrite *)
|
walther@59869
|
111 |
preconds: term list, (* STILL UNUSED *)
|
walther@59869
|
112 |
rew_ord: rew_ord,(* for rules *)
|
walther@59869
|
113 |
erls: rule_set, (* for the conditions in rules *)
|
walther@59869
|
114 |
srls: rule_set, (* for evaluation of Prog_Expr *)
|
walther@59869
|
115 |
calc: calc list, (* for Calculate in program, set by prep_rls' *)
|
walther@59869
|
116 |
rules: rule list,
|
walther@59869
|
117 |
errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy *)
|
walther@59869
|
118 |
scr: program} (* DEPRECATED: intersteps are created on the fly now *)
|
wenzelm@60293
|
119 |
| Sequence of (* a sequence of rules to be tried only once *)
|
walther@59869
|
120 |
{id: string, preconds: term list, rew_ord: rew_ord, erls: rule_set, srls: rule_set,
|
walther@59869
|
121 |
calc: calc list, rules: rule list, errpatts: errpatID list, scr: program}
|
walther@59869
|
122 |
| Rrls of (* ML-functions within rewriting, _ONE_ redex rewritten per call*)
|
walther@59869
|
123 |
{id: string, (* for trace_rewrite *)
|
walther@59869
|
124 |
prepat: (* a guard which guarantees a redex *)
|
walther@59869
|
125 |
(term list * (* preconds, eval with subst from pattern below *)
|
walther@59869
|
126 |
term) (* pattern matched with current (sub)term *)
|
walther@59869
|
127 |
list, (* meta-conjunction in guarding is or *)
|
walther@59869
|
128 |
rew_ord: rew_ord, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program}
|
walther@59850
|
129 |
|
Walther@60436
|
130 |
fun rule_to_string Empty_Prog = "Empty_Prog"
|
Walther@60436
|
131 |
| rule_to_string (Prog s) = "Prog " ^ UnparseC.term s
|
Walther@60436
|
132 |
| rule_to_string (Rfuns _) = "Rfuns";
|
Walther@60436
|
133 |
|
walther@59849
|
134 |
(**)end(**)
|
walther@59849
|
135 |
|