1 (* Title: CalcElements/rule-def.sml
3 (c) due to copyright terms
5 A minimum of code for a mutual recursive datatype definition
6 awaiting individual specification later.
8 signature RULE_DEFINITION =
20 | 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}
22 | Seqence 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}
24 | 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}
26 and rule = Cal1 of string * eval_fn | Num_Calc of string * eval_fn | Erule
27 | Rls_ of rule_set | Thm of string * thm
32 {attach_form: rule list list -> term -> term -> (rule * (term * term list)) list,
33 init_state: term -> term * term * rule list list * (rule * (term * term list)) list,
34 locate_rule: rule list list -> term -> rule -> (rule * (term * term list)) list,
35 next_rule: rule list list -> term -> rule option, normal_form: term ->
36 (term * term list) option}
37 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
39 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
41 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
45 structure Rule_Def(**): RULE_DEFINITION(**) =
49 type eval_fn = (string -> term -> theory -> (string * term) option);
51 type rew_ord' = string;
52 type rew_ord_ = (term * term) list -> term * term -> bool;
53 type rew_ord = rew_ord' * rew_ord_;
56 type cal = calID * eval_fn;
57 type prog_calcID = string;
58 type calc = (prog_calcID * cal);
60 (* error patterns and fill patterns *)
61 type errpatID = string
63 (* all these different data justify a step in a calculation *)
65 Erule (*.the empty rule .*)
66 | Thm of (string * Basic_Thm.thm) (* see TODO CLEANUP Thm *)
67 | Num_Calc of string * (*.sml-code manipulating a (sub)term .*)
69 | Cal1 of string * (*.sml-code applied only to whole term
70 or left/right-hand-side of eqality .*)
72 | Rls_ of rule_set (*.ie. rule sets may be nested.*)
75 | Prog of term (* a leaf is either a tactic or an 'exp' in 'let v = expr'
76 where 'exp' does not contain a tactic. *)
77 | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *)
78 {init_state : (* initialise for reverse rewriting by the Interpreter *)
79 term -> (* for this the rrlsstate is initialised: *)
80 term * (* the current formula: *)
81 (* goes locate_input_tactic -> find_next_step via istate *)
82 term * (* the final formula *)
83 rule list (* of reverse rewrite set (#1#) *)
84 list * (* may be serveral, eg. in norm_rational *)
85 ( rule * (* Thm (+ Thm generated from Num_Calc) resulting in ... *)
86 (term * (* ... rewrite with ... *)
87 term list)) (* ... assumptions *)
88 list, (* derivation from given term to normalform
89 in reverse order with sym_thm;
90 (#1#) could be extracted from here #1 *)
91 normal_form: (* the function which drives the Rrls ##############################*)
92 term -> (term * term list) option,
93 locate_rule: (* checks a rule R for being a cancel-rule, and if it is,
94 then return the list of rules (+ the terms they are rewriting to)
95 which need to be applied before R should be applied.
96 precondition: the rule is applicable to the argument-term. *)
97 rule list list -> (* the reverse rule list *)
98 term -> (* ... to which the rule shall be applied *)
99 rule -> (* ... to be applied to term *)
100 ( rule * (* value: a rule rewriting to ... *)
101 (term * (* ... the resulting term ... *)
102 term list)) (* ... with the assumptions ( //#0) *)
103 list, (* there may be several such rules; the list is empty,
104 if the rule has nothing to do with e.g. cancelation *)
105 next_rule: (* for a given term return the next rules to be done for cancelling *)
106 rule list list->(* the reverse rule list *)
107 term -> (* the term for which ... *)
108 rule option, (* ... this rule is appropriate for cancellation;
109 there may be no such rule (if the term is eg.canceled already*)
110 attach_form: (* checks an input term TI, if it may belong to e.g. a current
111 cancellation, by trying to derive it from the given term TG.
114 term -> (* TG, the last one agreed upon by user + math-eng *)
115 term -> (* TI, the next one input by the user *)
116 ( rule * (* the rule to be applied in order to reach TI *)
117 (term * (* ... obtained by applying the rule ... *)
118 term list)) (* ... and the respective assumptions *)
119 list} (* there may be several such rules; the list is empty, if the
120 users term does not belong to e.g. a cancellation of the term
124 | Repeat of (*a confluent and terminating ruleset, in general *)
125 {id : string, (*for trace_rewrite:=true *)
126 preconds : term list, (*unused WN020820 *)
127 (*WN060616 for efficiency...
128 bdvs : false, (*set in prep_rls' for get_bdvs *)*)
129 rew_ord : rew_ord, (*for rules*)
130 erls : rule_set, (*for the conditions in rules *)
131 srls : rule_set, (*for evaluation of list_fns in script *)
132 calc : calc list, (*for Calculate in scr, set by prep_rls' *)
134 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy *)
135 scr : program} (*Prog term: generating intermed.steps *)
136 | Seqence of (*a sequence of rules to be tried only once *)
137 {id : string, (*for trace_rewrite:=true *)
138 preconds : term list, (*unused 20.8.02 *)
139 (*WN060616 for efficiency...
140 bdvs : false, (*set in prep_rls' for get_bdvs *)*)
141 rew_ord : rew_ord, (*for rules *)
142 erls : rule_set, (*for the conditions in rules *)
143 srls : rule_set, (*for evaluation of list_fns in script *)
144 calc : calc list, (*for Calculate in scr, set by prep_rls' *)
146 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
147 scr : program} (*Prog term (how to restrict type ???)*)
149 (*Rrls call SML-code and simulate an rule_set
150 difference: there is always _ONE_ redex rewritten in 1 call,
151 thus wrap Rrls by: Rls (Rls_ ...)*)
152 | Rrls of (* SML-functions within rewriting; step-wise execution provided;
153 Rrls simulate an rule_set
154 difference: there is always _ONE_ redex rewritten in 1 call,
155 thus wrap Rrls by: Rls (Rls_ ...) *)
156 {id : string, (* for trace_rewrite := true *)
157 prepat : (term list *(* preconds, eval with subst from pattern;
158 if [@{term True}], match decides alone *)
159 term ) (* pattern matched with current (sub)term *)
160 list, (* meta-conjunction is or *)
161 rew_ord : rew_ord, (* for rules *)
162 erls : rule_set, (* for the conditions in rules and preconds *)
163 calc : calc list, (* for Calculate in scr, set automatic.in prep_rls' *)
164 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
165 scr : program}; (* Rfuns {...} (how to restrict type ???) *)