1.1 --- a/src/Tools/isac/BaseDefinitions/rule-def.sml Fri Apr 10 18:32:36 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml Mon Apr 13 13:13:07 2020 +0200
1.3 @@ -62,108 +62,74 @@
1.4
1.5 (* all these different data justify a step in a calculation *)
1.6 datatype rule =
1.7 - Erule (*.the empty rule .*)
1.8 - | Thm of (string * Basic_Thm.thm) (* see TODO CLEANUP Thm *)
1.9 - | Num_Calc of string * (*.sml-code manipulating a (sub)term .*)
1.10 - eval_fn
1.11 - | Cal1 of string * (*.sml-code applied only to whole term
1.12 - or left/right-hand-side of eqality .*)
1.13 - eval_fn
1.14 - | Rls_ of rule_set (*.ie. rule sets may be nested.*)
1.15 -and program =
1.16 - EmptyScr
1.17 - | Prog of term (* a leaf is either a tactic or an 'exp' in 'let v = expr'
1.18 - where 'exp' does not contain a tactic. *)
1.19 - | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *)
1.20 - {init_state : (* initialise for reverse rewriting by the Interpreter *)
1.21 + Erule (* the empty rule *)
1.22 + | Thm of (* theorem associated with the identifier for reflection *)
1.23 + string * (* needless since Thm.get_name_hint *)
1.24 + Thm.thm (* see TODO CLEANUP Thm *)
1.25 + | Num_Calc of (* evaluation by rewriting *)
1.26 + string * (* unique identifier for the evaluation function *)
1.27 + eval_fn (* evaluation function in ML code *)
1.28 + | Cal1 of string * (* applied once to whole term or lhs/rhs of an eqality *)
1.29 + eval_fn (* evaluation function in ML code *)
1.30 + | Rls_ of rule_set (* rule sets may be nested *)
1.31 +and program = (* program for Lucas-Interpretation *)
1.32 + EmptyScr (* DEPRECATED: needless after removal of Rfuns *)
1.33 + | Prog of term (* Lucas-Interpretation works on Isabelle's terms *)
1.34 + | Rfuns of (* DEPRECATED, replaced by Auto_Prog *)
1.35 + {init_state : (* initialise for reverse rewriting by the Interpreter *)
1.36 term -> (* for this the rrlsstate is initialised: *)
1.37 - term * (* the current formula: *)
1.38 - (* goes locate_input_tactic -> find_next_step via istate *)
1.39 + term * (* the current formula via istate *)
1.40 term * (* the final formula *)
1.41 rule list (* of reverse rewrite set (#1#) *)
1.42 list * (* may be serveral, eg. in norm_rational *)
1.43 - ( rule * (* Thm (+ Thm generated from Num_Calc) resulting in ... *)
1.44 + ( rule * (* Thm (+ Thm generated from Num_Calc) resulting in ... *)
1.45 (term * (* ... rewrite with ... *)
1.46 term list)) (* ... assumptions *)
1.47 - list, (* derivation from given term to normalform
1.48 - in reverse order with sym_thm;
1.49 - (#1#) could be extracted from here #1 *)
1.50 - normal_form: (* the function which drives the Rrls ##############################*)
1.51 + list, (* derivation from given term to normalform in reverse order *)
1.52 + normal_form: (* the function which drives the Rrls *)
1.53 term -> (term * term list) option,
1.54 - locate_rule: (* checks a rule R for being a cancel-rule, and if it is,
1.55 - then return the list of rules (+ the terms they are rewriting to)
1.56 - which need to be applied before R should be applied.
1.57 - precondition: the rule is applicable to the argument-term. *)
1.58 + locate_rule: (* checks a rule R for being a cancel-rule *)
1.59 rule list list -> (* the reverse rule list *)
1.60 term -> (* ... to which the rule shall be applied *)
1.61 rule -> (* ... to be applied to term *)
1.62 ( rule * (* value: a rule rewriting to ... *)
1.63 (term * (* ... the resulting term ... *)
1.64 term list)) (* ... with the assumptions ( //#0) *)
1.65 - list, (* there may be several such rules; the list is empty,
1.66 - if the rule has nothing to do with e.g. cancelation *)
1.67 - next_rule: (* for a given term return the next rules to be done for cancelling *)
1.68 + list, (* there may be several such rules *)
1.69 + next_rule: (* for a given term return the next rules to be done for cancel *)
1.70 rule list list->(* the reverse rule list *)
1.71 term -> (* the term for which ... *)
1.72 - rule option, (* ... this rule is appropriate for cancellation;
1.73 - there may be no such rule (if the term is eg.canceled already*)
1.74 - attach_form: (* checks an input term TI, if it may belong to e.g. a current
1.75 - cancellation, by trying to derive it from the given term TG.
1.76 - NOT IMPLEMENTED *)
1.77 - rule list list->(**)
1.78 + rule option, (* ... this rule is appropriate for cancellation *)
1.79 + attach_form: (* checks an input term TI, if it may belong to a current cancel*)
1.80 + rule list list->
1.81 term -> (* TG, the last one agreed upon by user + math-eng *)
1.82 term -> (* TI, the next one input by the user *)
1.83 ( rule * (* the rule to be applied in order to reach TI *)
1.84 (term * (* ... obtained by applying the rule ... *)
1.85 term list)) (* ... and the respective assumptions *)
1.86 - list} (* there may be several such rules; the list is empty, if the
1.87 - users term does not belong to e.g. a cancellation of the term
1.88 - last agreed upon. *)
1.89 -and rule_set =
1.90 - Empty
1.91 - | Repeat of (*a confluent and terminating ruleset, in general *)
1.92 - {id : string, (*for trace_rewrite:=true *)
1.93 - preconds : term list, (*unused WN020820 *)
1.94 - (*WN060616 for efficiency...
1.95 - bdvs : false, (*set in prep_rls' for get_bdvs *)*)
1.96 - rew_ord : rew_ord, (*for rules*)
1.97 - erls : rule_set, (*for the conditions in rules *)
1.98 - srls : rule_set, (*for evaluation of list_fns in script *)
1.99 - calc : calc list, (*for Calculate in scr, set by prep_rls' *)
1.100 - rules : rule list,
1.101 - errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy *)
1.102 - scr : program} (*Prog term: generating intermed.steps *)
1.103 - | Seqence of (*a sequence of rules to be tried only once *)
1.104 - {id : string, (*for trace_rewrite:=true *)
1.105 - preconds : term list, (*unused 20.8.02 *)
1.106 - (*WN060616 for efficiency...
1.107 - bdvs : false, (*set in prep_rls' for get_bdvs *)*)
1.108 - rew_ord : rew_ord, (*for rules *)
1.109 - erls : rule_set, (*for the conditions in rules *)
1.110 - srls : rule_set, (*for evaluation of list_fns in script *)
1.111 - calc : calc list, (*for Calculate in scr, set by prep_rls' *)
1.112 - rules : rule list,
1.113 - errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
1.114 - scr : program} (*Prog term (how to restrict type ???)*)
1.115 -
1.116 - (*Rrls call SML-code and simulate an rule_set
1.117 - difference: there is always _ONE_ redex rewritten in 1 call,
1.118 - thus wrap Rrls by: Rls (Rls_ ...)*)
1.119 - | Rrls of (* SML-functions within rewriting; step-wise execution provided;
1.120 - Rrls simulate an rule_set
1.121 - difference: there is always _ONE_ redex rewritten in 1 call,
1.122 - thus wrap Rrls by: Rls (Rls_ ...) *)
1.123 - {id : string, (* for trace_rewrite := true *)
1.124 - prepat : (term list *(* preconds, eval with subst from pattern;
1.125 - if [@{term True}], match decides alone *)
1.126 - term ) (* pattern matched with current (sub)term *)
1.127 - list, (* meta-conjunction is or *)
1.128 - rew_ord : rew_ord, (* for rules *)
1.129 - erls : rule_set, (* for the conditions in rules and preconds *)
1.130 - calc : calc list, (* for Calculate in scr, set automatic.in prep_rls' *)
1.131 - errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
1.132 - scr : program}; (* Rfuns {...} (how to restrict type ???) *)
1.133 -
1.134 + list} (* there may be several such rules; the list is empty, if ... *)
1.135 +and rule_set = (* a collection for ordered & conditional rewriting *)
1.136 + Empty (* empty Rule_Set.T *)
1.137 + | Repeat of (*a confluent and terminating ruleset, in principle *)
1.138 + {id: string, (* for trace_rewrite *)
1.139 + preconds: term list, (* STILL UNUSED *)
1.140 + rew_ord: rew_ord,(* for rules *)
1.141 + erls: rule_set, (* for the conditions in rules *)
1.142 + srls: rule_set, (* for evaluation of Prog_Expr *)
1.143 + calc: calc list, (* for Calculate in program, set by prep_rls' *)
1.144 + rules: rule list,
1.145 + errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy *)
1.146 + scr: program} (* DEPRECATED: intersteps are created on the fly now *)
1.147 + | Seqence of (* a sequence of rules to be tried only once *)
1.148 + {id: string, preconds: term list, rew_ord: rew_ord, erls: rule_set, srls: rule_set,
1.149 + calc: calc list, rules: rule list, errpatts: errpatID list, scr: program}
1.150 + | Rrls of (* ML-functions within rewriting, _ONE_ redex rewritten per call*)
1.151 + {id: string, (* for trace_rewrite *)
1.152 + prepat: (* a guard which guarantees a redex *)
1.153 + (term list * (* preconds, eval with subst from pattern below *)
1.154 + term) (* pattern matched with current (sub)term *)
1.155 + list, (* meta-conjunction in guarding is or *)
1.156 + rew_ord: rew_ord, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program}
1.157
1.158 (**)end(**)
1.159
2.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Fri Apr 10 18:32:36 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Mon Apr 13 13:13:07 2020 +0200
2.3 @@ -22,12 +22,12 @@
2.4 val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
2.5 val to_kestore: for_kestore list * for_kestore list -> for_kestore list
2.6
2.7 -(*/------- this will disappear eventually -----------\*)
2.8 +(*/------- this will disappear eventually ----------------------------------------------------\*)
2.9 val empty: T
2.10 type rrlsstate = term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list
2.11 val e_rrlsstate: rrlsstate
2.12 val e_rrls: T
2.13 -(*\------- this will disappear eventually -----------/*)
2.14 +(*\------- this will disappear eventually ----------------------------------------------------/*)
2.15
2.16 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.17 (*NONE*)