walther@59866: (* Title: BaseDefinitions/rule-def.sml walther@59849: Author: Walther Neuper walther@59849: (c) due to copyright terms walther@59849: walther@59919: Here is a minimum of code required for Know_Store.thy. walther@59919: For main code see structure Rule. walther@59849: *) walther@59849: signature RULE_DEFINITION = walther@59850: sig walther@59850: type calc walther@59850: eqtype calID walther@59850: eqtype errpatID Walther@60509: Walther@60509: type rew_ord_id = string Walther@60509: type rew_ord_function = LibraryC.subst -> term * term -> bool Walther@60509: type rew_ord_T = rew_ord_id * rew_ord_function Walther@60509: Walther@60504: type eval_fn = string -> term -> Proof.context -> (string * term) option walther@59849: walther@59851: datatype rule_set = walther@59851: Empty walther@59851: | Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string, Walther@60509: preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set} walther@59878: | Sequence of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string, Walther@60509: preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set} walther@59851: | Rrls of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string, Walther@60509: prepat: (term list * term) list, rew_ord: rew_ord_T, scr: program} walther@59878: and rule = Cal1 of string * eval_fn | Eval of string * eval_fn | Erule walther@59851: | Rls_ of rule_set | Thm of string * thm walther@59850: and program = walther@59878: Empty_Prog walther@59850: | Prog of term walther@59850: | Rfuns of walther@59850: {attach_form: rule list list -> term -> term -> (rule * (term * term list)) list, walther@59850: init_state: term -> term * term * rule list list * (rule * (term * term list)) list, walther@59850: locate_rule: rule list list -> term -> rule -> (rule * (term * term list)) list, walther@59850: next_rule: rule list list -> term -> rule option, normal_form: term -> walther@59850: (term * term list) option} Walther@60440: val program_to_string: program -> string walther@59850: end walther@59849: walther@59849: (**) walther@59849: structure Rule_Def(**): RULE_DEFINITION(**) = walther@59849: struct walther@59849: (**) walther@59849: Walther@60504: type eval_fn = string -> term -> Proof.context -> (string * term) option; walther@59849: Walther@60509: type rew_ord_id = string; Walther@60509: type rew_ord_function = LibraryC.subst -> term * term -> bool; Walther@60509: type rew_ord_T = rew_ord_id * rew_ord_function; walther@59849: walther@59850: type calID = string; walther@59849: type cal = calID * eval_fn; walther@59849: type prog_calcID = string; walther@59849: type calc = (prog_calcID * cal); walther@59849: walther@59849: (* error patterns and fill patterns *) walther@59849: type errpatID = string walther@59849: walther@59849: (* all these different data justify a step in a calculation *) walther@59849: datatype rule = walther@59869: Erule (* the empty rule *) walther@59869: | Thm of (* theorem associated with the identifier for reflection *) walther@60370: string * (* required for ThmC.sym_thm *) walther@59869: Thm.thm (* see TODO CLEANUP Thm *) wenzelm@60293: | Eval of (* evaluation by rewriting *) walther@59869: string * (* unique identifier for the evaluation function *) walther@59869: eval_fn (* evaluation function in ML code *) walther@59869: | Cal1 of string * (* applied once to whole term or lhs/rhs of an eqality *) walther@59869: eval_fn (* evaluation function in ML code *) walther@59869: | Rls_ of rule_set (* rule sets may be nested *) walther@59869: and program = (* program for Lucas-Interpretation *) wenzelm@60293: Empty_Prog (* DEPRECATED: needless after removal of Rfuns *) walther@59869: | Prog of term (* Lucas-Interpretation works on Isabelle's terms *) walther@59869: | Rfuns of (* DEPRECATED, replaced by Auto_Prog *) walther@59869: {init_state : (* initialise for reverse rewriting by the Interpreter *) walther@59849: term -> (* for this the rrlsstate is initialised: *) walther@59869: term * (* the current formula via istate *) walther@59849: term * (* the final formula *) walther@59849: rule list (* of reverse rewrite set (#1#) *) walther@59849: list * (* may be serveral, eg. in norm_rational *) walther@59878: ( rule * (* Thm (+ Thm generated from Eval) resulting in ... *) walther@59849: (term * (* ... rewrite with ... *) walther@59849: term list)) (* ... assumptions *) walther@59869: list, (* derivation from given term to normalform in reverse order *) walther@59869: normal_form: (* the function which drives the Rrls *) walther@59849: term -> (term * term list) option, walther@59869: locate_rule: (* checks a rule R for being a cancel-rule *) walther@59849: rule list list -> (* the reverse rule list *) walther@59849: term -> (* ... to which the rule shall be applied *) walther@59849: rule -> (* ... to be applied to term *) walther@59849: ( rule * (* value: a rule rewriting to ... *) walther@59849: (term * (* ... the resulting term ... *) walther@59849: term list)) (* ... with the assumptions ( //#0) *) walther@59869: list, (* there may be several such rules *) walther@59869: next_rule: (* for a given term return the next rules to be done for cancel *) walther@59849: rule list list->(* the reverse rule list *) walther@59849: term -> (* the term for which ... *) walther@59869: rule option, (* ... this rule is appropriate for cancellation *) walther@59869: attach_form: (* checks an input term TI, if it may belong to a current cancel*) walther@59869: rule list list-> walther@59849: term -> (* TG, the last one agreed upon by user + math-eng *) walther@59849: term -> (* TI, the next one input by the user *) walther@59849: ( rule * (* the rule to be applied in order to reach TI *) walther@59849: (term * (* ... obtained by applying the rule ... *) walther@59849: term list)) (* ... and the respective assumptions *) walther@59869: list} (* there may be several such rules; the list is empty, if ... *) walther@59869: and rule_set = (* a collection for ordered & conditional rewriting *) walther@59869: Empty (* empty Rule_Set.T *) walther@59869: | Repeat of (*a confluent and terminating ruleset, in principle *) walther@59869: {id: string, (* for trace_rewrite *) walther@59869: preconds: term list, (* STILL UNUSED *) Walther@60509: rew_ord: rew_ord_T,(* for rules *) walther@59869: erls: rule_set, (* for the conditions in rules *) walther@59869: srls: rule_set, (* for evaluation of Prog_Expr *) walther@59869: calc: calc list, (* for Calculate in program, set by prep_rls' *) walther@59869: rules: rule list, walther@59869: errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy *) walther@59869: scr: program} (* DEPRECATED: intersteps are created on the fly now *) wenzelm@60293: | Sequence of (* a sequence of rules to be tried only once *) Walther@60509: {id: string, preconds: term list, rew_ord: rew_ord_T, erls: rule_set, srls: rule_set, walther@59869: calc: calc list, rules: rule list, errpatts: errpatID list, scr: program} walther@59869: | Rrls of (* ML-functions within rewriting, _ONE_ redex rewritten per call*) walther@59869: {id: string, (* for trace_rewrite *) walther@59869: prepat: (* a guard which guarantees a redex *) walther@59869: (term list * (* preconds, eval with subst from pattern below *) walther@59869: term) (* pattern matched with current (sub)term *) walther@59869: list, (* meta-conjunction in guarding is or *) Walther@60509: rew_ord: rew_ord_T, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program} walther@59850: Walther@60440: fun program_to_string Empty_Prog = "Empty_Prog" Walther@60440: | program_to_string (Prog s) = "Prog " ^ UnparseC.term s Walther@60440: | program_to_string (Rfuns _) = "Rfuns"; Walther@60436: walther@59849: (**)end(**) walther@59849: