8 signature RULE_DEFINITION = |
8 signature RULE_DEFINITION = |
9 sig |
9 sig |
10 type calc |
10 type calc |
11 eqtype calID |
11 eqtype calID |
12 eqtype errpatID |
12 eqtype errpatID |
13 type rew_ord' = string |
13 |
14 type rew_ord_ = LibraryC.subst -> term * term -> bool |
14 type rew_ord_id = string |
15 type rew_ord = rew_ord' * rew_ord_ |
15 type rew_ord_function = LibraryC.subst -> term * term -> bool |
|
16 type rew_ord_T = rew_ord_id * rew_ord_function |
|
17 |
16 type eval_fn = string -> term -> Proof.context -> (string * term) option |
18 type eval_fn = string -> term -> Proof.context -> (string * term) option |
17 |
19 |
18 datatype rule_set = |
20 datatype rule_set = |
19 Empty |
21 Empty |
20 | Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string, |
22 | Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string, |
21 preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set} |
23 preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set} |
22 | Sequence of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string, |
24 | Sequence of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string, |
23 preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set} |
25 preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set} |
24 | Rrls of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string, |
26 | Rrls of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string, |
25 prepat: (term list * term) list, rew_ord: rew_ord, scr: program} |
27 prepat: (term list * term) list, rew_ord: rew_ord_T, scr: program} |
26 and rule = Cal1 of string * eval_fn | Eval of string * eval_fn | Erule |
28 and rule = Cal1 of string * eval_fn | Eval of string * eval_fn | Erule |
27 | Rls_ of rule_set | Thm of string * thm |
29 | Rls_ of rule_set | Thm of string * thm |
28 and program = |
30 and program = |
29 Empty_Prog |
31 Empty_Prog |
30 | Prog of term |
32 | Prog of term |
107 and rule_set = (* a collection for ordered & conditional rewriting *) |
109 and rule_set = (* a collection for ordered & conditional rewriting *) |
108 Empty (* empty Rule_Set.T *) |
110 Empty (* empty Rule_Set.T *) |
109 | Repeat of (*a confluent and terminating ruleset, in principle *) |
111 | Repeat of (*a confluent and terminating ruleset, in principle *) |
110 {id: string, (* for trace_rewrite *) |
112 {id: string, (* for trace_rewrite *) |
111 preconds: term list, (* STILL UNUSED *) |
113 preconds: term list, (* STILL UNUSED *) |
112 rew_ord: rew_ord,(* for rules *) |
114 rew_ord: rew_ord_T,(* for rules *) |
113 erls: rule_set, (* for the conditions in rules *) |
115 erls: rule_set, (* for the conditions in rules *) |
114 srls: rule_set, (* for evaluation of Prog_Expr *) |
116 srls: rule_set, (* for evaluation of Prog_Expr *) |
115 calc: calc list, (* for Calculate in program, set by prep_rls' *) |
117 calc: calc list, (* for Calculate in program, set by prep_rls' *) |
116 rules: rule list, |
118 rules: rule list, |
117 errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy *) |
119 errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy *) |
118 scr: program} (* DEPRECATED: intersteps are created on the fly now *) |
120 scr: program} (* DEPRECATED: intersteps are created on the fly now *) |
119 | Sequence of (* a sequence of rules to be tried only once *) |
121 | Sequence of (* a sequence of rules to be tried only once *) |
120 {id: string, preconds: term list, rew_ord: rew_ord, erls: rule_set, srls: rule_set, |
122 {id: string, preconds: term list, rew_ord: rew_ord_T, erls: rule_set, srls: rule_set, |
121 calc: calc list, rules: rule list, errpatts: errpatID list, scr: program} |
123 calc: calc list, rules: rule list, errpatts: errpatID list, scr: program} |
122 | Rrls of (* ML-functions within rewriting, _ONE_ redex rewritten per call*) |
124 | Rrls of (* ML-functions within rewriting, _ONE_ redex rewritten per call*) |
123 {id: string, (* for trace_rewrite *) |
125 {id: string, (* for trace_rewrite *) |
124 prepat: (* a guard which guarantees a redex *) |
126 prepat: (* a guard which guarantees a redex *) |
125 (term list * (* preconds, eval with subst from pattern below *) |
127 (term list * (* preconds, eval with subst from pattern below *) |
126 term) (* pattern matched with current (sub)term *) |
128 term) (* pattern matched with current (sub)term *) |
127 list, (* meta-conjunction in guarding is or *) |
129 list, (* meta-conjunction in guarding is or *) |
128 rew_ord: rew_ord, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program} |
130 rew_ord: rew_ord_T, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program} |
129 |
131 |
130 fun program_to_string Empty_Prog = "Empty_Prog" |
132 fun program_to_string Empty_Prog = "Empty_Prog" |
131 | program_to_string (Prog s) = "Prog " ^ UnparseC.term s |
133 | program_to_string (Prog s) = "Prog " ^ UnparseC.term s |
132 | program_to_string (Rfuns _) = "Rfuns"; |
134 | program_to_string (Rfuns _) = "Rfuns"; |
133 |
135 |