1.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Sat Aug 17 15:45:36 2013 +0200
1.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Fri Aug 23 09:32:05 2013 +0200
1.3 @@ -9,10 +9,41 @@
1.4 exception NO_REWRITE;
1.5 exception STOP_REW_SUB; (*WN050820 quick and dirty*)
1.6
1.7 -(*17.6.00: rewrite by going down the term with rew_sub*)
1.8 -(* val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
1.9 - (thy, 1, []:(Term.term * Term.term) list, rew_ord, erls, bool,thm,term);
1.10 - *)
1.11 +(*
1.12 +Synopsis rewriting (prep for reference manual):
1.13 +----------------------------------------------
1.14 +Rewriting uses theorems for transforming terms. However, not all kinds
1.15 +of such transformations can be done by rewriting. Examples are
1.16 +calculation with numerals or cancellation of fractions.
1.17 +
1.18 +Isac tries to present transformations like calculations or cancellation
1.19 +as simple rewrite steps for the naive user. However, some of such
1.20 +transformations should be transparent to the user by single-stepping.
1.21 +For instance, cancellation involves interesting CA algorithms like
1.22 +GCD of multivariate polynomials.
1.23 +
1.24 +Thus Isac has two mechanisms for including SML code, "thm Calc" and "Rrls",
1.25 +the former for steps which are not meant to be inspected by single-stepping
1.26 +the latter meant for single-stepping and providing respective mechanisms.
1.27 +
1.28 +(1) Inclusion by "thm Calc" for 1-step execution
1.29 +TODO
1.30 +
1.31 +(2) Inclusion by "Rrls" for multi-step execution
1.32 +TODO
1.33 +In multi-step execution "reverse rewriting" worked only as passive presentation
1.34 +without any interaction. So the functions init_state, locate_rule etc are just dummies.
1.35 +TODO
1.36 +? multi-step execution did never work.
1.37 +what worked is "reverse rewriting",
1.38 +i.e. presentation of intermediate steps *without* interaction
1.39 +TODO
1.40 +# type rule and scr | Rfuns
1.41 +# type rrlsstate = (*state for reverse rewriting*)
1.42 +# type and rls | Rrls
1.43 +all in calcelems.sml
1.44 +TODO
1.45 +*)
1.46 fun rewrite__ thy i bdv tless rls put_asm thm ct =
1.47 (let
1.48 val (t',asms,lrd,rew) =
2.1 --- a/src/Tools/isac/calcelems.sml Sat Aug 17 15:45:36 2013 +0200
2.2 +++ b/src/Tools/isac/calcelems.sml Fri Aug 23 09:32:05 2013 +0200
2.3 @@ -96,27 +96,51 @@
2.4 | Rls_ of rls (*.ie. rule sets may be nested.*)
2.5 and scr =
2.6 EmptyScr
2.7 - | Prog of term (*for met*)
2.8 - | Rfuns of {init_state : term ->
2.9 - (term * (*the current formula:
2.10 - goes locate_gen -> next_tac via istate*)
2.11 - term * (*the final formula*)
2.12 - rule list (*of reverse rewrite set (#1#)*)
2.13 - list * (*may be serveral, eg. in norm_rational*)
2.14 - (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
2.15 - (term * (*... rewrite with ...*)
2.16 - term list)) (*... assumptions*)
2.17 - list), (*derivation from given term to normalform
2.18 - in reverse order with sym_thm;
2.19 - (#1#) could be extracted from here #1*)
2.20 -
2.21 - normal_form: term -> (term * term list) option,
2.22 - locate_rule: rule list list -> term -> rule
2.23 - -> (rule * (term * term list)) list,
2.24 - next_rule : rule list list -> term -> rule option,
2.25 - attach_form: rule list list -> term -> term
2.26 - -> (rule * (term * term list)) list}
2.27 -
2.28 + | Prog of term (* for met *)
2.29 + | Rfuns of (* for Rrls*)
2.30 + {init_state : (* initialise for reverse rewriting by the Interpreter *)
2.31 + term -> (* for this the rrlsstate is initialised: *)
2.32 + term * (* the current formula: goes locate_gen -> next_tac via istate *)
2.33 + term * (* the final formula *)
2.34 + rule list (* of reverse rewrite set (#1#) *)
2.35 + list * (* may be serveral, eg. in norm_rational *)
2.36 + ( rule * (* Thm (+ Thm generated from Calc) resulting in ... *)
2.37 + (term * (* ... rewrite with ... *)
2.38 + term list)) (* ... assumptions *)
2.39 + list, (* derivation from given term to normalform
2.40 + in reverse order with sym_thm;
2.41 + (#1#) could be extracted from here #1 *)
2.42 + normal_form: (* the function which drives the Rrls ##############################*)
2.43 + term -> (term * term list) option,
2.44 + locate_rule: (* checks a rule R for being a cancel-rule, and if it is,
2.45 + then return the list of rules (+ the terms they are rewriting to)
2.46 + which need to be applied before R should be applied.
2.47 + precondition: the rule is applicable to the argument-term. *)
2.48 + rule list list -> (* the reverse rule list *)
2.49 + term -> (* ... to which the rule shall be applied *)
2.50 + rule -> (* ... to be applied to term *)
2.51 + ( rule * (* value: a rule rewriting to ... *)
2.52 + (term * (* ... the resulting term ... *)
2.53 + term list)) (* ... with the assumptions ( //#0) *)
2.54 + list, (* there may be several such rules; the list is empty,
2.55 + if the rule has nothing to do with e.g. cancelation *)
2.56 + next_rule: (* for a given term return the next rules to be done for cancelling *)
2.57 + rule list list->(* the reverse rule list *)
2.58 + term -> (* the term for which ... *)
2.59 + rule option, (* ... this rule is appropriate for cancellation;
2.60 + there may be no such rule (if the term is eg.canceled already*)
2.61 + attach_form: (* checks an input term TI, if it may belong to e.g. a current
2.62 + cancellation, by trying to derive it from the given term TG.
2.63 + NOT IMPLEMENTED *)
2.64 + rule list list->(**)
2.65 + term -> (* TG, the last one agreed upon by user + math-eng *)
2.66 + term -> (* TI, the next one input by the user *)
2.67 + ( rule * (* the rule to be applied in order to reach TI *)
2.68 + (term * (* ... obtained by applying the rule ... *)
2.69 + term list)) (* ... and the respective assumptions *)
2.70 + list} (* there may be several such rules; the list is empty, if the
2.71 + users term does not belong to e.g. a cancellation of the term
2.72 + last agreed upon. *)
2.73 and rls =
2.74 Erls (*for init e_rls*)
2.75
2.76 @@ -144,23 +168,24 @@
2.77 rules : rule list,
2.78 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
2.79 scr : scr} (*Prog term (how to restrict type ???)*)
2.80 +
2.81 (*Rrls call SML-code and simulate an rls
2.82 difference: there is always _ONE_ redex rewritten in 1 call,
2.83 thus wrap Rrls by: Rls (Rls_ ...)*)
2.84 -
2.85 - | Rrls of (* for 'reverse rewriting' by SML-functions instead Prog *)
2.86 + | Rrls of (* SML-functions within rewriting; step-wise execution provided;
2.87 + Rrls simulate an rls
2.88 + difference: there is always _ONE_ redex rewritten in 1 call,
2.89 + thus wrap Rrls by: Rls (Rls_ ...) *)
2.90 {id : string, (* for trace_rewrite := true *)
2.91 prepat : (term list *(* preconds, eval with subst from pattern;
2.92 - if [@{term True}], match decides alone *)
2.93 - term ) (* pattern matched with current (sub)term *)
2.94 - list, (* meta-conjunction is or *)
2.95 + if [@{term True}], match decides alone *)
2.96 + term ) (* pattern matched with current (sub)term *)
2.97 + list, (* meta-conjunction is or *)
2.98 rew_ord : rew_ord, (* for rules *)
2.99 erls : rls, (* for the conditions in rules and preconds *)
2.100 calc : calc list, (* for Calculate in scr, set automatic.in prep_rls *)
2.101 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
2.102 scr : scr}; (* Rfuns {...} (how to restrict type ???) *)
2.103 -(*1.8.02 ad (how to restrict type ???): scr should be usable indepentently
2.104 - from rls, and then contain both Prog _AND_ Rfuns !!!*)
2.105
2.106 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info.get_theory thy');(*FIXXXME thy-ctxt*)
2.107 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
2.108 @@ -230,19 +255,9 @@
2.109 | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)
2.110 | eqrule _ = false;
2.111
2.112 +type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
2.113 + (term * term * rule list list * (rule * (term * term list)) list);
2.114
2.115 -type rrlsstate = (*state for reverse rewriting*)
2.116 - (term * (*the current formula:
2.117 - goes locate_gen -> next_tac via istate*)
2.118 - term * (*the final formula*)
2.119 - rule list (*of reverse rewrite set (#1#)*)
2.120 - list * (*may be serveral, eg. in norm_rational*)
2.121 - (rule * (*Thm (+ Thm generated from Calc) resulting in ...*)
2.122 - (term * (*... rewrite with ...*)
2.123 - term list)) (*... assumptions*)
2.124 - list); (*derivation from given term to normalform
2.125 - in reverse order with sym_thm;
2.126 - (#1#) could be extracted from here #1*)
2.127 val e_type = Type("empty",[]);
2.128 val a_type = TFree("'a",[]);
2.129 val e_term = Const("empty",e_type);