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