1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml Fri Apr 10 15:02:50 2020 +0200
1.3 @@ -0,0 +1,169 @@
1.4 +(* Title: BaseDefinitions/rule-def.sml
1.5 + Author: Walther Neuper
1.6 + (c) due to copyright terms
1.7 +
1.8 +A minimum of code for a mutual recursive datatype definition
1.9 +awaiting individual specification later.
1.10 +*)
1.11 +signature RULE_DEFINITION =
1.12 +sig
1.13 + type calc
1.14 + eqtype calID
1.15 + eqtype errpatID
1.16 + type rew_ord
1.17 + type rew_ord'
1.18 + type rew_ord_
1.19 + type eval_fn
1.20 +
1.21 + datatype rule_set =
1.22 + Empty
1.23 + | Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
1.24 + preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
1.25 + | Seqence of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
1.26 + preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rule_set}
1.27 + | Rrls of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,
1.28 + prepat: (term list * term) list, rew_ord: rew_ord, scr: program}
1.29 + and rule = Cal1 of string * eval_fn | Num_Calc of string * eval_fn | Erule
1.30 + | Rls_ of rule_set | Thm of string * thm
1.31 + and program =
1.32 + EmptyScr
1.33 + | Prog of term
1.34 + | Rfuns of
1.35 + {attach_form: rule list list -> term -> term -> (rule * (term * term list)) list,
1.36 + init_state: term -> term * term * rule list list * (rule * (term * term list)) list,
1.37 + locate_rule: rule list list -> term -> rule -> (rule * (term * term list)) list,
1.38 + next_rule: rule list list -> term -> rule option, normal_form: term ->
1.39 + (term * term list) option}
1.40 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.41 + (*NONE*)
1.42 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.43 + (*NONE*)
1.44 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.45 +end
1.46 +
1.47 +(**)
1.48 +structure Rule_Def(**): RULE_DEFINITION(**) =
1.49 +struct
1.50 +(**)
1.51 +
1.52 +type eval_fn = (string -> term -> theory -> (string * term) option);
1.53 +
1.54 +type rew_ord' = string;
1.55 +type rew_ord_ = (term * term) list -> term * term -> bool;
1.56 +type rew_ord = rew_ord' * rew_ord_;
1.57 +
1.58 +type calID = string;
1.59 +type cal = calID * eval_fn;
1.60 +type prog_calcID = string;
1.61 +type calc = (prog_calcID * cal);
1.62 +
1.63 +(* error patterns and fill patterns *)
1.64 +type errpatID = string
1.65 +
1.66 +(* all these different data justify a step in a calculation *)
1.67 +datatype rule =
1.68 + Erule (*.the empty rule .*)
1.69 + | Thm of (string * Basic_Thm.thm) (* see TODO CLEANUP Thm *)
1.70 + | Num_Calc of string * (*.sml-code manipulating a (sub)term .*)
1.71 + eval_fn
1.72 + | Cal1 of string * (*.sml-code applied only to whole term
1.73 + or left/right-hand-side of eqality .*)
1.74 + eval_fn
1.75 + | Rls_ of rule_set (*.ie. rule sets may be nested.*)
1.76 +and program =
1.77 + EmptyScr
1.78 + | Prog of term (* a leaf is either a tactic or an 'exp' in 'let v = expr'
1.79 + where 'exp' does not contain a tactic. *)
1.80 + | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *)
1.81 + {init_state : (* initialise for reverse rewriting by the Interpreter *)
1.82 + term -> (* for this the rrlsstate is initialised: *)
1.83 + term * (* the current formula: *)
1.84 + (* goes locate_input_tactic -> find_next_step via istate *)
1.85 + term * (* the final formula *)
1.86 + rule list (* of reverse rewrite set (#1#) *)
1.87 + list * (* may be serveral, eg. in norm_rational *)
1.88 + ( rule * (* Thm (+ Thm generated from Num_Calc) resulting in ... *)
1.89 + (term * (* ... rewrite with ... *)
1.90 + term list)) (* ... assumptions *)
1.91 + list, (* derivation from given term to normalform
1.92 + in reverse order with sym_thm;
1.93 + (#1#) could be extracted from here #1 *)
1.94 + normal_form: (* the function which drives the Rrls ##############################*)
1.95 + term -> (term * term list) option,
1.96 + locate_rule: (* checks a rule R for being a cancel-rule, and if it is,
1.97 + then return the list of rules (+ the terms they are rewriting to)
1.98 + which need to be applied before R should be applied.
1.99 + precondition: the rule is applicable to the argument-term. *)
1.100 + rule list list -> (* the reverse rule list *)
1.101 + term -> (* ... to which the rule shall be applied *)
1.102 + rule -> (* ... to be applied to term *)
1.103 + ( rule * (* value: a rule rewriting to ... *)
1.104 + (term * (* ... the resulting term ... *)
1.105 + term list)) (* ... with the assumptions ( //#0) *)
1.106 + list, (* there may be several such rules; the list is empty,
1.107 + if the rule has nothing to do with e.g. cancelation *)
1.108 + next_rule: (* for a given term return the next rules to be done for cancelling *)
1.109 + rule list list->(* the reverse rule list *)
1.110 + term -> (* the term for which ... *)
1.111 + rule option, (* ... this rule is appropriate for cancellation;
1.112 + there may be no such rule (if the term is eg.canceled already*)
1.113 + attach_form: (* checks an input term TI, if it may belong to e.g. a current
1.114 + cancellation, by trying to derive it from the given term TG.
1.115 + NOT IMPLEMENTED *)
1.116 + rule list list->(**)
1.117 + term -> (* TG, the last one agreed upon by user + math-eng *)
1.118 + term -> (* TI, the next one input by the user *)
1.119 + ( rule * (* the rule to be applied in order to reach TI *)
1.120 + (term * (* ... obtained by applying the rule ... *)
1.121 + term list)) (* ... and the respective assumptions *)
1.122 + list} (* there may be several such rules; the list is empty, if the
1.123 + users term does not belong to e.g. a cancellation of the term
1.124 + last agreed upon. *)
1.125 +and rule_set =
1.126 + Empty
1.127 + | Repeat of (*a confluent and terminating ruleset, in general *)
1.128 + {id : string, (*for trace_rewrite:=true *)
1.129 + preconds : term list, (*unused WN020820 *)
1.130 + (*WN060616 for efficiency...
1.131 + bdvs : false, (*set in prep_rls' for get_bdvs *)*)
1.132 + rew_ord : rew_ord, (*for rules*)
1.133 + erls : rule_set, (*for the conditions in rules *)
1.134 + srls : rule_set, (*for evaluation of list_fns in script *)
1.135 + calc : calc list, (*for Calculate in scr, set by prep_rls' *)
1.136 + rules : rule list,
1.137 + errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy *)
1.138 + scr : program} (*Prog term: generating intermed.steps *)
1.139 + | Seqence of (*a sequence of rules to be tried only once *)
1.140 + {id : string, (*for trace_rewrite:=true *)
1.141 + preconds : term list, (*unused 20.8.02 *)
1.142 + (*WN060616 for efficiency...
1.143 + bdvs : false, (*set in prep_rls' for get_bdvs *)*)
1.144 + rew_ord : rew_ord, (*for rules *)
1.145 + erls : rule_set, (*for the conditions in rules *)
1.146 + srls : rule_set, (*for evaluation of list_fns in script *)
1.147 + calc : calc list, (*for Calculate in scr, set by prep_rls' *)
1.148 + rules : rule list,
1.149 + errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
1.150 + scr : program} (*Prog term (how to restrict type ???)*)
1.151 +
1.152 + (*Rrls call SML-code and simulate an rule_set
1.153 + difference: there is always _ONE_ redex rewritten in 1 call,
1.154 + thus wrap Rrls by: Rls (Rls_ ...)*)
1.155 + | Rrls of (* SML-functions within rewriting; step-wise execution provided;
1.156 + Rrls simulate an rule_set
1.157 + difference: there is always _ONE_ redex rewritten in 1 call,
1.158 + thus wrap Rrls by: Rls (Rls_ ...) *)
1.159 + {id : string, (* for trace_rewrite := true *)
1.160 + prepat : (term list *(* preconds, eval with subst from pattern;
1.161 + if [@{term True}], match decides alone *)
1.162 + term ) (* pattern matched with current (sub)term *)
1.163 + list, (* meta-conjunction is or *)
1.164 + rew_ord : rew_ord, (* for rules *)
1.165 + erls : rule_set, (* for the conditions in rules and preconds *)
1.166 + calc : calc list, (* for Calculate in scr, set automatic.in prep_rls' *)
1.167 + errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
1.168 + scr : program}; (* Rfuns {...} (how to restrict type ???) *)
1.169 +
1.170 +
1.171 +(**)end(**)
1.172 +