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