separate struct. Derive
1.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Wed Apr 22 16:53:03 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Thu Apr 23 09:29:56 2020 +0200
1.3 @@ -19,9 +19,11 @@
1.4 type pbt_ = string * (term * term)
1.5 val update_hrls: Thy_Html.thydata -> Error_Fill_Def.errpatID list -> Thy_Html.thydata
1.6
1.7 +(*/------- to ? from Celem -------\*)
1.8 val knowthys: unit -> theory list
1.9 val isabthys: unit -> theory list
1.10 val partID': ThyC.id -> string
1.11 +(*\------- to ? from Celem -------/*)
1.12
1.13 end
1.14
1.15 @@ -64,6 +66,7 @@
1.16 | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments";
1.17
1.18
1.19 +(*/------- to ? from Celem -------\*)
1.20 (* group the theories defined in Isac, compare Build_Thydata:
1.21 section "Get and group the theories defined in Isac" *)
1.22 fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*)
1.23 @@ -112,6 +115,7 @@
1.24 else if member Context.eq_thy (isabthys ()) thy then "Isabelle"
1.25 else error ("closure of thys in Isac is broken by " ^ Context.theory_name thy)
1.26 fun partID' thy' = partID (ThyC.get_theory thy')
1.27 +(*\------- to ? from Celem -------/*)
1.28
1.29 end (*struct*)
1.30
2.1 --- a/src/Tools/isac/BaseDefinitions/libraryC.sml Wed Apr 22 16:53:03 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/libraryC.sml Thu Apr 23 09:29:56 2020 +0200
2.3 @@ -15,76 +15,77 @@
2.4 infix 1 ~~~
2.5
2.6 signature LIBRARY_C =
2.7 - sig
2.8 - val and_: bool * bool -> bool
2.9 - val cand_: bool -> bool -> bool
2.10 - val or_: bool * bool -> bool
2.11 - val cor_: bool -> bool -> bool
2.12 +sig
2.13 + val and_: bool * bool -> bool
2.14 + val cand_: bool -> bool -> bool
2.15 + val or_: bool * bool -> bool
2.16 + val cor_: bool -> bool -> bool
2.17
2.18 - val assoc: (''a * 'b) list * ''a -> 'b option
2.19 - val assoc_string: (string * 'a) list * string -> 'a option
2.20 - val bool2str: bool -> string
2.21 - val commas: string list -> string
2.22 - val compare_strs: string -> string -> unit list
2.23 - val dashs: int -> string
2.24 - val de_quote: string -> string
2.25 - val distinct: ''a list -> ''a list
2.26 - val dots: int -> string
2.27 - val drop: int * 'a list -> 'a list
2.28 - val drop_last: 'a list -> 'a list
2.29 - val drop_last_n: int -> 'a list -> 'a list
2.30 - val drop_nth: 'a list -> int * 'a list -> 'a list
2.31 - val dropuntil: ('a -> bool) -> 'a list -> 'a list
2.32 - val dropwhile: ('a -> bool) -> 'a list -> 'a list
2.33 - val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
2.34 - val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
2.35 - val fst3: 'a * 'b * 'c -> 'a
2.36 - val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list
2.37 - val gen_mem: ('a * 'b -> bool) -> 'a * 'b list -> bool
2.38 - val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
2.39 - val if_none: 'a option -> 'a -> 'a
2.40 - val indent: int -> string
2.41 - val indt: int -> string
2.42 - val idt: string -> int -> string
2.43 - val int2str: int -> string
2.44 - val ints2str': int list -> string
2.45 - val intsto: int -> int list
2.46 - val last_elem: 'a list -> 'a
2.47 - val list2str: string list -> string
2.48 - val list_update: 'a list -> int -> 'a -> 'a list
2.49 - val maxl: int list -> int
2.50 - val member_swap: ('a * 'b -> bool) -> 'a -> 'b list -> bool
2.51 - val nos: string list -> string
2.52 - val nth: int -> 'a list -> 'a
2.53 - val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
2.54 - val overwritel: (''a * 'b) list * (''a * 'b) list -> (''a * 'b) list
2.55 - val pair2str: string * string -> string
2.56 - val pair2str_: string * string -> string
2.57 - val pair2tri: ('a * 'b) * 'c -> 'a * 'b * 'c
2.58 - val snd3: 'a * 'b * 'c -> 'b
2.59 - val spair2str: string * string -> string
2.60 - val split_nlast: int * 'a list -> 'a list * 'a list
2.61 - val string_to_bool: string -> bool
2.62 - val strs2str: string list -> string
2.63 - val strs2str': string list -> string
2.64 - val strs2str_: string list -> string (* duplicates in Rule *)
2.65 - val strslist2strs: string list list -> string
2.66 - val take: int * 'a list -> 'a list
2.67 - val take_fromto: int -> int -> 'a list -> 'a list
2.68 - val takelast: int * 'a list -> 'a list
2.69 - val takerest: int * 'a list -> 'a list
2.70 - val takewhile: 'a list -> ('a -> bool) -> 'a list -> 'a list
2.71 - val termless: term * term -> bool
2.72 - val thd3: 'a * 'b * 'c -> 'c
2.73 - val triple2pair: 'a * 'b * 'c -> 'a * 'b
2.74 - val ~~~ : 'a list * 'b list -> ('a * 'b) list
2.75 - val linefeed: string -> string
2.76 + val assoc: (''a * 'b) list * ''a -> 'b option
2.77 + val assoc_string: (string * 'a) list * string -> 'a option
2.78 + val bool2str: bool -> string
2.79 + val commas: string list -> string
2.80 + val compare_strs: string -> string -> unit list
2.81 + val dashs: int -> string
2.82 + val de_quote: string -> string
2.83 + val distinct: ''a list -> ''a list
2.84 + val dots: int -> string
2.85 + val drop: int * 'a list -> 'a list
2.86 + val drop_last: 'a list -> 'a list
2.87 + val drop_last_n: int -> 'a list -> 'a list
2.88 + val drop_nth: 'a list -> int * 'a list -> 'a list
2.89 + val dropuntil: ('a -> bool) -> 'a list -> 'a list
2.90 + val dropwhile: ('a -> bool) -> 'a list -> 'a list
2.91 + val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
2.92 + val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
2.93 + val fst3: 'a * 'b * 'c -> 'a
2.94 + val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list
2.95 + val gen_mem: ('a * 'b -> bool) -> 'a * 'b list -> bool
2.96 + val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
2.97 + val if_none: 'a option -> 'a -> 'a
2.98 + val indent: int -> string
2.99 + val indt: int -> string
2.100 + val idt: string -> int -> string
2.101 + val int2str: int -> string
2.102 + val ints2str': int list -> string
2.103 + val intsto: int -> int list
2.104 + val last_elem: 'a list -> 'a
2.105 + val list2str: string list -> string
2.106 + val list_update: 'a list -> int -> 'a -> 'a list
2.107 + val maxl: int list -> int
2.108 + val member_swap: ('a * 'b -> bool) -> 'a -> 'b list -> bool
2.109 + val nos: string list -> string
2.110 + val nth: int -> 'a list -> 'a
2.111 + val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
2.112 + val overwritel: (''a * 'b) list * (''a * 'b) list -> (''a * 'b) list
2.113 + val pair2str: string * string -> string
2.114 + val pair2str_: string * string -> string
2.115 + val pair2tri: ('a * 'b) * 'c -> 'a * 'b * 'c
2.116 + val snd3: 'a * 'b * 'c -> 'b
2.117 + val spair2str: string * string -> string
2.118 + val split_nlast: int * 'a list -> 'a list * 'a list
2.119 + val string_to_bool: string -> bool
2.120 + val strs2str: string list -> string
2.121 + val strs2str': string list -> string
2.122 + val strs2str_: string list -> string (* duplicates in Rule *)
2.123 + val strslist2strs: string list list -> string
2.124 + val take: int * 'a list -> 'a list
2.125 + val take_fromto: int -> int -> 'a list -> 'a list
2.126 + val takelast: int * 'a list -> 'a list
2.127 + val takerest: int * 'a list -> 'a list
2.128 + val takewhile: 'a list -> ('a -> bool) -> 'a list -> 'a list
2.129 + val termless: term * term -> bool
2.130 + val thd3: 'a * 'b * 'c -> 'c
2.131 + val triple2pair: 'a * 'b * 'c -> 'a * 'b
2.132 + val ~~~ : 'a list * 'b list -> ('a * 'b) list
2.133 + val linefeed: string -> string
2.134
2.135 + val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
2.136 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.137 (* NONE *)
2.138 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.139 - val enumerate_strings: string list -> string list
2.140 - val quad2pair: 'a * 'b * 'c * 'd -> 'a * 'b
2.141 + val enumerate_strings: string list -> string list
2.142 + val quad2pair: 'a * 'b * 'c * 'd -> 'a * 'b
2.143 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.144
2.145
2.146 @@ -93,11 +94,11 @@
2.147 val strip_thy: string -> string
2.148 (*\\\------------------------------>>> thy ------------------------------------------------///*)
2.149 (*///------------------------------>>> term -----------------------------------------------\\\*)
2.150 - val subs2str: string list -> string
2.151 - val id_of: term -> string
2.152 - val ids_of: term -> string list
2.153 + val subs2str: string list -> string
2.154 + val id_of: term -> string
2.155 + val ids_of: term -> string list
2.156 (*\\\------------------------------>>> term -----------------------------------------------///*)
2.157 - end;
2.158 +end;
2.159
2.160 (**)
2.161 structure LibraryC(**): LIBRARY_C(**) =
2.162 @@ -304,4 +305,21 @@
2.163
2.164 val linefeed = curry op ^ "\n"; (* ?\<longrightarrow> libraryC ?*)
2.165
2.166 +(*the lists contain eq-al elem-pairs at the beginning;
2.167 + return first list reverted (again) - ie. in order as required subsequently*)
2.168 +fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =
2.169 + if equal f1 i1 then
2.170 + if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is)
2.171 + else (rev (f1 :: f2 :: fs), i1 :: i2 :: is)
2.172 + else error "dropwhile': did not start with equal elements"
2.173 + | dropwhile' equal (f::fs) [i] =
2.174 + if equal f i then
2.175 + (rev (f::fs), [i])
2.176 + else error "dropwhile': did not start with equal elements"
2.177 + | dropwhile' equal [f] (i::is) =
2.178 + if equal f i then
2.179 + ([f], i::is)
2.180 + else error "dropwhile': did not start with equal elements"
2.181 + | dropwhile' _ _ _ = error "dropwhile': uncovered case"
2.182 +
2.183 end; (*struct*) open LibraryC
3.1 --- a/src/Tools/isac/Interpret/Interpret.thy Wed Apr 22 16:53:03 2020 +0200
3.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Thu Apr 23 09:29:56 2020 +0200
3.3 @@ -13,6 +13,7 @@
3.4 ML_file "sub-problem.sml"
3.5 ML_file rewtools.sml
3.6 ML_file "error-fill-pattern.sml"
3.7 + ML_file derive.sml
3.8 ML_file "li-tool.sml"
3.9 ML_file "lucas-interpreter.sml"
3.10 ML_file "step-solve.sml"
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Tools/isac/Interpret/derive.sml Thu Apr 23 09:29:56 2020 +0200
4.3 @@ -0,0 +1,167 @@
4.4 +(* Title: Interpret/derive.sml
4.5 + Author: Walther Neuper 2019
4.6 + (c) due to copyright terms
4.7 +
4.8 +
4.9 +*)
4.10 +
4.11 +signature DERIVATION =
4.12 +sig
4.13 + type deriv
4.14 + val make_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->
4.15 + term option -> term -> deriv
4.16 + val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
4.17 + Rule_Set.T -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
4.18 + val reverse_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->
4.19 + term option -> term -> (Rule.rule * (term * term list)) list
4.20 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.21 + (* NONE *)
4.22 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.23 + val trtas2str : (term * Rule.rule * (term * term list)) list -> string
4.24 + val deriv2str : (term * Rule.rule * (term * term list)) list -> string
4.25 + val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
4.26 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.27 +end
4.28 +
4.29 +(**)
4.30 +structure Derive(**): DERIVATION(**) =
4.31 +struct
4.32 +(**)
4.33 +(*/------- to Derive from Rtools -------\*)
4.34 +(*** reverse rewriting ***)
4.35 +(*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
4.36 + * of for connecting a user-input formula with the current calc-state. *
4.37 + *# It is somewhat incompatible with the rest of the math-engine: *
4.38 + * (1) it is not created by a script *
4.39 + * (2) thus there cannot be another user-input within a derivation *
4.40 + *# It suffers particularily from the not-well-foundedness of the math-engine*
4.41 + * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' *
4.42 + * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) *
4.43 + * (3) FIXME and eventually 'lev_back' *
4.44 + *# SOME improvements are evident FIXME.040215 '_deriv'ation: *
4.45 + * (1) FIXME nest Rls_ in 'make_deriv' *
4.46 + * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus *
4.47 + * user-input will become possible in this part of a derivation *
4.48 + * (3) FIXME do (2) only if a derivation has been found -- for efficiency, *
4.49 + * while a non-derivable inform requires to step until End_Proof' *
4.50 + * (4) FIXME find criteria on when _not_ to step until End_Proof' *
4.51 + * (5) FIXME
4.52 +.*)
4.53 +type deriv = (* derivation for inserting one level of nodes into the Ctree *)
4.54 + ( term * (* where the rule is applied to *)
4.55 + Rule.rule * (* rule to be applied *)
4.56 + ( term * (* resulting from rule application *)
4.57 + term list)) (* assumptions resulting from rule application *)
4.58 + list
4.59 +
4.60 +fun trta2str (t, r, (t', a)) =
4.61 + "\n(" ^ UnparseC.term t ^ ", " ^ Rule.to_string_short r ^ ", (" ^ UnparseC.term t' ^ ", " ^ UnparseC.terms a ^ "))"
4.62 +fun trtas2str trtas = (strs2str o (map trta2str)) trtas
4.63 +val deriv2str = trtas2str
4.64 +(*\------- to Derive from Rtools -------/*)
4.65 +(*/------- to Derive from Rtools -------\*)
4.66 +(* derive normalform of a rls, or derive until SOME goal,
4.67 + and record rules applied and rewrites.
4.68 +val it = fn
4.69 + : theory
4.70 + -> rls
4.71 + -> rule list
4.72 + -> rew_ord : the order of this rls, which 1 theorem of is used
4.73 + for rewriting 1 single step (?14.4.03)
4.74 + -> term option : 040214 ??? use for "derive until SOME goal" ???
4.75 + -> term
4.76 + -> (term * : to this term ...
4.77 + rule * : ... this rule is applied yielding ...
4.78 + (term * : ... this term ...
4.79 + term list)) : ... under these assumptions.
4.80 + list :
4.81 +returns empty list for a normal form
4.82 +FIXME.WN040214: treats rules as in Rls, _not_ as in Seq
4.83 +
4.84 +WN060825 too complicated for the intended use by cancel_, common_nominator_
4.85 +and unreflectedly adapted to extension of rules by Rls_: returns Rls_("sym_simpl..
4.86 + -- replaced below *)
4.87 +
4.88 +
4.89 +fun make_deriv thy erls rs ro goal tt =
4.90 + let
4.91 + datatype switch = Appl | Noap (* unify with version in rewrite.sml *)
4.92 + fun rew_once _ rts t Noap [] =
4.93 + (case goal of NONE => rts | SOME _ => error ("make_deriv: no derivation for " ^ UnparseC.term t))
4.94 + | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs
4.95 + (*| Seq _ => rts) FIXXXXXME 14.3.03*)
4.96 + | rew_once lim rts t apno rs' =
4.97 + (case goal of
4.98 + NONE => rew_or_calc lim rts t apno rs'
4.99 + | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
4.100 + and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
4.101 + if lim < 0
4.102 + then (tracing ("make_deriv exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with deriv =\n");
4.103 + tracing (deriv2str rts); rts)
4.104 + else
4.105 + (case r of
4.106 + Rule.Thm (thmid, tm) =>
4.107 + (if not (! Rewrite.trace_on) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
4.108 + case Rewrite.rewrite_ thy ro erls true tm t of
4.109 + NONE => rew_once lim rts t apno rs'
4.110 + | SOME (t', a') =>
4.111 + (if ! Rewrite.trace_on then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
4.112 + rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
4.113 + | Rule.Eval (c as (op_, _)) =>
4.114 + let
4.115 + val _ = if not (! Rewrite.trace_on) then () else tracing ("### trying calc. \"" ^ op_^"\"")
4.116 + val t = TermC.uminus_to_string t
4.117 + in
4.118 + case Eval.adhoc_thm thy c t of
4.119 + NONE => rew_once lim rts t apno rs'
4.120 + | SOME (thmid, tm) =>
4.121 + (let
4.122 + val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of
4.123 + SOME ta => ta
4.124 + | NONE => error "adhoc_thm: NONE"
4.125 + val _ = if not (! Rewrite.trace_on) then () else tracing("=== calc. to: " ^ UnparseC.term t')
4.126 + val r' = Rule.Thm (thmid, tm)
4.127 + in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
4.128 + handle _ => raise ERROR "derive_norm, Eval: no rewrite"
4.129 + end
4.130 + | Rule.Rls_ rls => (* WN060829: CREATES "sym_rlsID", see 7df94616c1bd and earlier*)
4.131 + (case Rewrite.rewrite_set_ thy true rls t of
4.132 + NONE => rew_once lim rts t apno rs'
4.133 + | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
4.134 + | rule => error ("rew_once: uncovered case " ^ Rule.to_string rule))
4.135 + | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"
4.136 + in rew_once (! Rewrite.lim_deriv) [] tt Noap rs end
4.137 +
4.138 +(*version for reverse rewrite used before 040214*)
4.139 +fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a));
4.140 +fun reverse_deriv thy erls rs ro goal t =
4.141 + (rev o (map rev_deriv)) (make_deriv thy erls rs ro goal t)
4.142 +(*\------- to Derive from Rtools -------/*)
4.143 +
4.144 +(*/------- to NEW Derive from Error_Fill_Pattern -------\*)
4.145 +(* 040214: version for concat_deriv *)
4.146 +fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));
4.147 +
4.148 +(* fo = ifo excluded already in inform *)
4.149 +fun concat_deriv rew_ord erls rules fo ifo =
4.150 + let
4.151 + fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
4.152 + | derivat dt = (#1 o #3 o last_elem) dt
4.153 + fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
4.154 + val fod = make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE fo
4.155 + val ifod = make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE ifo
4.156 + in
4.157 + case (fod, ifod) of
4.158 + ([], []) => if fo = ifo then (true, []) else (false, [])
4.159 + | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
4.160 + | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
4.161 + | (fod, ifod) =>
4.162 + if derivat fod = derivat ifod (*common normal form found*) then
4.163 + let
4.164 + val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
4.165 + in (true, fod' @ (map rev_deriv' rifod')) end
4.166 + else (false, [])
4.167 + end
4.168 +(*\------- to NEW Derive from Error_Fill_Pattern-------/*)
4.169 +
4.170 +(**)end(**)
5.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 22 16:53:03 2020 +0200
5.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 23 09:29:56 2020 +0200
5.3 @@ -3,7 +3,8 @@
5.4 0603
5.5 (c) due to copyright terms
5.6
5.7 -TODO: use "Error_Fill_Pattern" for renaming identifiers -- go back to Rule_Def.*
5.8 +In case a term is input, which contains an "error pattern" (provided by a mathauthor),
5.9 +several "fill patterns" can be presented as help for the next step.)
5.10 *)
5.11
5.12 signature ERROR_FILL_PATTERN =
5.13 @@ -12,22 +13,27 @@
5.14 type errpat = errpatID * term list * thm list
5.15 val errpats2str : errpat list -> string
5.16
5.17 - val find_fillpatterns : Calc.T -> Error_Fill_Def.errpatID -> (Error_Fill_Def.fillpatID * term * thm * Selem.subs option) list
5.18 + val find_fillpatterns : Calc.T -> Error_Fill_Def.errpatID ->
5.19 + (Error_Fill_Def.fillpatID * term * thm * Selem.subs option) list
5.20 + val fetchErrorpatterns : Tactic.input -> Error_Fill_Def.errpatID list
5.21 val is_exactly_equal : Calc.T -> string -> string * Tactic.input
5.22 - val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
5.23 - Rule_Set.T -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
5.24 - val mk_tacis: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) -> Tactic.input * Tactic.T * (Pos.pos' * (Istate.T * Proof.context))
5.25 - val fetchErrorpatterns : Tactic.input -> Error_Fill_Def.errpatID list
5.26 - val check_for :
5.27 - term * term ->
5.28 - term * (term * term) list -> (Error_Fill_Def.errpatID * term list * 'a list) list * Rule_Set.T -> Error_Fill_Def.errpatID option
5.29 +
5.30 +(*/------- to ThmC -------\*)
5.31 val rule2thm'' : Rule.rule -> ThmC.T
5.32 val rule2rls' : Rule.rule -> string
5.33 +(*\------- to ThmC -------/*)
5.34 +
5.35 +(*/------- to LItool -------\*)
5.36 + val mk_tacis: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) ->
5.37 + Tactic.input * Tactic.T * (Pos.pos' * (Istate.T * Proof.context))
5.38 + val check_for : term * term -> term * (term * term) list ->
5.39 + (Error_Fill_Def.errpatID * term list * 'a list) list * Rule_Set.T ->
5.40 + Error_Fill_Def.errpatID option
5.41 +(*\------- to LItool -------/*)
5.42 +
5.43 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.44 (* NONE *)
5.45 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.46 - val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
5.47 - val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
5.48 val check_err_patt : term * term -> UnparseC.subst -> Error_Fill_Def.errpatID * term -> Rule_Set.T -> Error_Fill_Def.errpatID option
5.49 val get_fillform :
5.50 'a * (term * term) list -> 'b * term -> Error_Fill_Def.errpatID -> Error_Fill_Def.fillpat -> (Error_Fill_Def.fillpatID * term * 'b * 'a) option
5.51 @@ -44,29 +50,9 @@
5.52 type errpatID = Rule_Def.errpatID
5.53
5.54 fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)
5.55 - | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule.to_string r);
5.56 + | rule2thm'' r = raise ERROR ("rule2thm': not defined for " ^ Rule.to_string r);
5.57 fun rule2rls' (Rule.Rls_ rls) = Rule_Set.id rls
5.58 - | rule2rls' r = error ("rule2rls': not defined for " ^ Rule.to_string r);
5.59 -
5.60 -(*the lists contain eq-al elem-pairs at the beginning;
5.61 - return first list reverted (again) - ie. in order as required subsequently*)
5.62 -fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =
5.63 - if equal f1 i1 then
5.64 - if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is)
5.65 - else (rev (f1 :: f2 :: fs), i1 :: i2 :: is)
5.66 - else error "dropwhile': did not start with equal elements"
5.67 - | dropwhile' equal (f::fs) [i] =
5.68 - if equal f i then
5.69 - (rev (f::fs), [i])
5.70 - else error "dropwhile': did not start with equal elements"
5.71 - | dropwhile' equal [f] (i::is) =
5.72 - if equal f i then
5.73 - ([f], i::is)
5.74 - else error "dropwhile': did not start with equal elements"
5.75 - | dropwhile' _ _ _ = error "dropwhile': uncovered case"
5.76 -
5.77 -(* 040214: version for concat_deriv *)
5.78 -fun rev_deriv' (t, r, (t', a)) = (t', ThmC.make_sym_rule r, (t, a));
5.79 + | rule2rls' r = raise ERROR ("rule2rls': not defined for " ^ Rule.to_string r);
5.80
5.81 fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) =
5.82 (Tactic.Rewrite (id, thm),
5.83 @@ -78,26 +64,6 @@
5.84 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))
5.85 | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term t)
5.86
5.87 -(* fo = ifo excluded already in inform *)
5.88 -fun concat_deriv rew_ord erls rules fo ifo =
5.89 - let
5.90 - fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
5.91 - | derivat dt = (#1 o #3 o last_elem) dt
5.92 - fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
5.93 - val fod = Rtools.make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE fo
5.94 - val ifod = Rtools.make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE ifo
5.95 - in
5.96 - case (fod, ifod) of
5.97 - ([], []) => if fo = ifo then (true, []) else (false, [])
5.98 - | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
5.99 - | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
5.100 - | (fod, ifod) =>
5.101 - if derivat fod = derivat ifod (*common normal form found*) then
5.102 - let
5.103 - val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
5.104 - in (true, fod' @ (map rev_deriv' rifod')) end
5.105 - else (false, [])
5.106 - end
5.107
5.108 (*** handle an error pattern ***)
5.109
5.110 @@ -175,7 +141,7 @@
5.111 |> flat
5.112 in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end
5.113
5.114 -(* check if an input formula is exactly equal the rewrite from a rule
5.115 +(* check if an input formula is exactly equal to the rewrite from a rule
5.116 which is stored at the pos where the input is stored of "ok". *)
5.117 fun is_exactly_equal (pt, pos as (p, _)) istr =
5.118 case TermC.parseNEW (ThyC.get_theory "Isac_Knowledge" |> ThyC.to_ctxt) istr of
6.1 --- a/src/Tools/isac/Interpret/li-tool.sml Wed Apr 22 16:53:03 2020 +0200
6.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Thu Apr 23 09:29:56 2020 +0200
6.3 @@ -8,24 +8,25 @@
6.4 signature LUCAS_INTERPRETER_TOOL =
6.5 sig
6.6 datatype ass =
6.7 - Associated of Tactic.T * term * Proof.context
6.8 - | Ass_Weak of Tactic.T * term * Proof.context
6.9 + Associated of Tactic.T * term (*..result*) * Proof.context
6.10 + | Ass_Weak of Tactic.T * term (*..result*) * Proof.context
6.11 | Not_Associated;
6.12 val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
6.13
6.14 - val implicit_take : Program.T -> (term * term) list -> term option
6.15 - val init_pstate : Rule_Set.T -> Proof.context -> Model.itm list -> Method.id ->
6.16 + val init_pstate: Rule_Set.T -> Proof.context -> Model.itm list -> Method.id ->
6.17 Istate.T * Proof.context * Program.T
6.18 -
6.19 - val get_simplifier : Calc.T -> Rule_Set.T
6.20 - val resume_prog : ThyC.id (*..for lookup in Know_Store*) -> Pos.pos' -> Ctree.ctree ->
6.21 + val resume_prog: ThyC.id (*..for lookup in Know_Store*) -> Pos.pos' -> Ctree.ctree ->
6.22 (Istate.T * Proof.context) * Program.T
6.23
6.24 - val tac_from_prog : Ctree.ctree -> theory (*..for lookup in Know_Store*) -> term -> Tactic.input
6.25 - val check_leaf : string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term ->
6.26 + val check_leaf: string -> Proof.context -> Rule_Set.T -> (Env.T * (term option * term)) -> term ->
6.27 Program.leaf * term option
6.28
6.29 + val implicit_take: Program.T -> (term * term) list -> term option
6.30 + val get_simplifier: Calc.T -> Rule_Set.T
6.31 + val tac_from_prog: Ctree.ctree -> theory (*..for lookup in Know_Store*) -> term -> Tactic.input
6.32 +
6.33 val trace_on: bool Unsynchronized.ref
6.34 +
6.35 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.36 (*NONE*)
6.37 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.38 @@ -103,16 +104,16 @@
6.39 | Ass_Weak of Tactic.T * term * Proof.context
6.40 | Not_Associated;
6.41
6.42 +(*
6.43 + associate is the ONLY code within by_tactic, which handles Tactic.T individually;
6.44 + thus it does ContextC.insert_assumptions in case of Rewrite*.
6.45 + The argument Ctree.ctree is required only for Subproblem'.
6.46 +*)
6.47 fun trace_msg_3 tac =
6.48 if (!trace_on) then
6.49 tracing("@@@ the \"tac_\" proposed to apply does NOT match the leaf found in the program:\n" ^
6.50 "@@@ tac_ = \"" ^ Tactic.string_of tac ^ "\"")
6.51 else ();
6.52 -(*
6.53 - associate is the ONLY code within by_tactic, which handles Tactic.T individually;
6.54 - thus it does ContextC.insert_assumptions in case of Rewrite*.
6.55 - The argument Ctree.ctree is required only for Subproblem'.
6.56 -*)
6.57 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
6.58 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
6.59 (case stac of
7.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 22 16:53:03 2020 +0200
7.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Apr 23 09:29:56 2020 +0200
7.3 @@ -622,7 +622,7 @@
7.4 val fo = Calc.get_current_formula ptp
7.5 val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
7.6 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
7.7 - val (found, der) = Error_Fill_Pattern.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
7.8 + val (found, der) = Derive.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
7.9 in
7.10 if found
7.11 then
8.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Apr 22 16:53:03 2020 +0200
8.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Apr 23 09:29:56 2020 +0200
8.3 @@ -7,23 +7,34 @@
8.4
8.5 signature REWRITE_TOOLS =
8.6 sig
8.7 - type deriv
8.8 - val contains_rule : Rule.rule -> Rule_Set.T -> bool
8.9 - val atomic_appl_tacs : theory -> string -> Rule_Set.T -> term -> Tactic.input -> Tactic.input list
8.10 +
8.11 +(*/------- for error-fill-pattern -------\*)
8.12 + val get_bdv_subst : term -> (term * term) list -> Selem.subs option * UnparseC.subst
8.13 + val thy_containing_thm : string -> string * string
8.14 val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
8.15 val thy_containing_cal : ThyC.id -> Exec_Def.prog_calcID -> string * string
8.16 +(*\------- for error-fill-pattern -------/*)
8.17 +
8.18 +(*/------- for Fetch_Tacs ONLY -------\*)
8.19 + val atomic_appl_tacs : theory -> string -> Rule_Set.T -> term -> Tactic.input -> Tactic.input list
8.20 +(*\------- for Fetch_Tacs ONLY -------/*)
8.21 +
8.22 +(*/------- to Rule_Set from Rtools -------\*)
8.23 + val contains_rule : Rule.rule -> Rule_Set.T -> bool
8.24 +(*\------- to Rule_Set from Rtools -------/*)
8.25 +
8.26 datatype contthy
8.27 - = ContNOrew of {applto: term, thm_rls: Check_Unique.id, thyID: ThyC.id}
8.28 - | ContNOrewInst of {applto: term, bdvs: UnparseC.subst, thm_rls: Check_Unique.id, thminst: term, thyID: ThyC.id}
8.29 - | ContRls of {applto: term, asms: term list, result: term, rls: Check_Unique.id, thyID: ThyC.id}
8.30 - | ContRlsInst of {applto: term, asms: term list, bdvs: UnparseC.subst, result: term, rls: Check_Unique.id, thyID: ThyC.id}
8.31 - | ContThm of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
8.32 - lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', rhs: term * term,
8.33 - thm: Check_Unique.id, thyID: ThyC.id}
8.34 - | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
8.35 - bdvs: UnparseC.subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
8.36 - rhs: term * term, thm: Check_Unique.id, thminst: term, thyID: ThyC.id}
8.37 - | EContThy
8.38 + = ContNOrew of {applto: term, thm_rls: Check_Unique.id, thyID: ThyC.id}
8.39 + | ContNOrewInst of {applto: term, bdvs: UnparseC.subst, thm_rls: Check_Unique.id, thminst: term, thyID: ThyC.id}
8.40 + | ContRls of {applto: term, asms: term list, result: term, rls: Check_Unique.id, thyID: ThyC.id}
8.41 + | ContRlsInst of {applto: term, asms: term list, bdvs: UnparseC.subst, result: term, rls: Check_Unique.id, thyID: ThyC.id}
8.42 + | ContThm of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
8.43 + lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', rhs: term * term,
8.44 + thm: Check_Unique.id, thyID: ThyC.id}
8.45 + | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
8.46 + bdvs: UnparseC.subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
8.47 + rhs: term * term, thm: Check_Unique.id, thminst: term, thyID: ThyC.id}
8.48 + | EContThy
8.49 val guh2filename : Check_Unique.id -> Celem.filename
8.50 val thms_of_rls : Rule_Set.T -> Rule.rule list
8.51 val theID2filename : Thy_Html.theID -> Celem.filename
8.52 @@ -34,24 +45,19 @@
8.53 val context_thy : Calc.T -> Tactic.input -> contthy
8.54 val distinct_Thm : Rule.rule list -> Rule.rule list
8.55 val eq_Thms : string list -> Rule.rule -> bool
8.56 - val make_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->
8.57 - term option -> term -> deriv
8.58 - val reverse_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->
8.59 - term option -> term -> (Rule.rule * (term * term list)) list
8.60 - val get_bdv_subst : term -> (term * term) list -> Selem.subs option * UnparseC.subst
8.61 - val thy_containing_thm : string -> string * string
8.62 +(*/------- to ThmC -------\*)
8.63 + val eq_Thm : Rule.rule * Rule.rule -> bool
8.64 + val deriv_of_thm'' : ThmC.T -> string
8.65 +(*\------- to ThmC -------/*)
8.66 val guh2theID : Check_Unique.id -> Thy_Html.theID
8.67 +
8.68 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.69 (* NONE *)
8.70 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.71 - val trtas2str : (term * Rule.rule * (term * term list)) list -> string
8.72 - val eq_Thm : Rule.rule * Rule.rule -> bool
8.73 - val deriv2str : (term * Rule.rule * (term * term list)) list -> string
8.74 - val deriv_of_thm'' : ThmC.T -> string
8.75 + (* NONE *)
8.76 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.77
8.78 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
8.79 - val deri2str : (Rule.rule * (term * term list)) list -> string
8.80 val sym_trm : term -> term
8.81 end
8.82 (**)
8.83 @@ -59,41 +65,6 @@
8.84 struct
8.85 (**)
8.86
8.87 -(*** reverse rewriting ***)
8.88 -(*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
8.89 - * of for connecting a user-input formula with the current calc-state. *
8.90 - *# It is somewhat incompatible with the rest of the math-engine: *
8.91 - * (1) it is not created by a script *
8.92 - * (2) thus there cannot be another user-input within a derivation *
8.93 - *# It suffers particularily from the not-well-foundedness of the math-engine*
8.94 - * (1) FIXME other branchtyptes than Transitive will change 'embed_deriv' *
8.95 - * (2) FIXME and eventually 'compare_step' (ie. the script interpreter) *
8.96 - * (3) FIXME and eventually 'lev_back' *
8.97 - *# SOME improvements are evident FIXME.040215 '_deriv'ation: *
8.98 - * (1) FIXME nest Rls_ in 'make_deriv' *
8.99 - * (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus *
8.100 - * user-input will become possible in this part of a derivation *
8.101 - * (3) FIXME do (2) only if a derivation has been found -- for efficiency, *
8.102 - * while a non-derivable inform requires to step until End_Proof' *
8.103 - * (4) FIXME find criteria on when _not_ to step until End_Proof' *
8.104 - * (5) FIXME
8.105 -.*)
8.106 -type deriv = (* derivation for insertin one level of nodes into the Ctree *)
8.107 - ( term * (* where the rule is applied to *)
8.108 - Rule.rule * (* rule to be applied *)
8.109 - ( term * (* resulting from rule application *)
8.110 - term list)) (* assumptions resulting from rule application *)
8.111 - list
8.112 -
8.113 -fun trta2str (t, r, (t', a)) =
8.114 - "\n(" ^ UnparseC.term t ^ ", " ^ Rule.to_string_short r ^ ", (" ^ UnparseC.term t' ^ ", " ^ UnparseC.terms a ^ "))"
8.115 -fun trtas2str trtas = (strs2str o (map trta2str)) trtas
8.116 -val deriv2str = trtas2str
8.117 -fun rta2str (r, (t, a)) =
8.118 - "\n(" ^ Rule.to_string_short r ^ ", (" ^ UnparseC.term t ^ ", " ^ UnparseC.terms a ^ "))"
8.119 -fun rtas2str rtas = (strs2str o (map rta2str)) rtas
8.120 -val deri2str = rtas2str
8.121 -
8.122 (* WN100910 weaker than fun sym_thm for Theory.axioms_of in isa02 *)
8.123 fun sym_trm trm =
8.124 let
8.125 @@ -103,84 +74,6 @@
8.126 | SOME cs => TermC.ins_concl cs (TermC.mk_equality (rhs, lhs))
8.127 in trm' end
8.128
8.129 -(* derive normalform of a rls, or derive until SOME goal,
8.130 - and record rules applied and rewrites.
8.131 -val it = fn
8.132 - : theory
8.133 - -> rls
8.134 - -> rule list
8.135 - -> rew_ord : the order of this rls, which 1 theorem of is used
8.136 - for rewriting 1 single step (?14.4.03)
8.137 - -> term option : 040214 ??? use for "derive until SOME goal" ???
8.138 - -> term
8.139 - -> (term * : to this term ...
8.140 - rule * : ... this rule is applied yielding ...
8.141 - (term * : ... this term ...
8.142 - term list)) : ... under these assumptions.
8.143 - list :
8.144 -returns empty list for a normal form
8.145 -FIXME.WN040214: treats rules as in Rls, _not_ as in Seq
8.146 -
8.147 -WN060825 too complicated for the intended use by cancel_, common_nominator_
8.148 -and unreflectedly adapted to extension of rules by Rls_: returns Rls_("sym_simpl..
8.149 - -- replaced below *)
8.150 -
8.151 -
8.152 -fun make_deriv thy erls rs ro goal tt =
8.153 - let
8.154 - datatype switch = Appl | Noap (* unify with version in rewrite.sml *)
8.155 - fun rew_once _ rts t Noap [] =
8.156 - (case goal of NONE => rts | SOME _ => error ("make_deriv: no derivation for " ^ UnparseC.term t))
8.157 - | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs
8.158 - (*| Seq _ => rts) FIXXXXXME 14.3.03*)
8.159 - | rew_once lim rts t apno rs' =
8.160 - (case goal of
8.161 - NONE => rew_or_calc lim rts t apno rs'
8.162 - | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
8.163 - and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
8.164 - if lim < 0
8.165 - then (tracing ("make_deriv exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with deriv =\n");
8.166 - tracing (deriv2str rts); rts)
8.167 - else
8.168 - (case r of
8.169 - Rule.Thm (thmid, tm) =>
8.170 - (if not (! Rewrite.trace_on) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
8.171 - case Rewrite.rewrite_ thy ro erls true tm t of
8.172 - NONE => rew_once lim rts t apno rs'
8.173 - | SOME (t', a') =>
8.174 - (if ! Rewrite.trace_on then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
8.175 - rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
8.176 - | Rule.Eval (c as (op_, _)) =>
8.177 - let
8.178 - val _ = if not (! Rewrite.trace_on) then () else tracing ("### trying calc. \"" ^ op_^"\"")
8.179 - val t = TermC.uminus_to_string t
8.180 - in
8.181 - case Eval.adhoc_thm thy c t of
8.182 - NONE => rew_once lim rts t apno rs'
8.183 - | SOME (thmid, tm) =>
8.184 - (let
8.185 - val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of
8.186 - SOME ta => ta
8.187 - | NONE => error "adhoc_thm: NONE"
8.188 - val _ = if not (! Rewrite.trace_on) then () else tracing("=== calc. to: " ^ UnparseC.term t')
8.189 - val r' = Rule.Thm (thmid, tm)
8.190 - in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
8.191 - handle _ => error "derive_norm, Eval: no rewrite"
8.192 - end
8.193 - (*| Cal1 (cc as (op_,_)) => ... WN080222 see rewrite__set_: see 7df94616c1bd and earlier*)
8.194 - | Rule.Rls_ rls => (* WN060829: CREATES "sym_rlsID", see 7df94616c1bd and earlier*)
8.195 - (case Rewrite.rewrite_set_ thy true rls t of
8.196 - NONE => rew_once lim rts t apno rs'
8.197 - | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
8.198 - | rule => error ("rew_once: uncovered case " ^ Rule.to_string rule))
8.199 - | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"
8.200 - in rew_once (! Rewrite.lim_deriv) [] tt Noap rs end
8.201 -
8.202 -(*version for reverse rewrite used before 040214*)
8.203 -fun rev_deriv (t, r, (_, a)) = (ThmC.make_sym_rule r, (t, a));
8.204 -fun reverse_deriv thy erls rs ro goal t =
8.205 - (rev o (map rev_deriv)) (make_deriv thy erls rs ro goal t)
8.206 -
8.207 fun eq_Thm (Rule.Thm (id1, _), Rule.Thm (id2,_)) = id1 = id2
8.208 | eq_Thm (Rule.Thm (_, _), _) = false
8.209 | eq_Thm (Rule.Rls_ r1, Rule.Rls_ r2) = Rule_Set.id r1 = Rule_Set.id r2
8.210 @@ -523,7 +416,7 @@
8.211 # otherwise []
8.212 WN060617 hack assuming that all scripts use only one bound variable
8.213 and use 'v_' as the formal argument for this bound variable*)
8.214 -fun subs_from (Istate.Pstate (pst as {env, ...})) _ guh =
8.215 +fun subs_from (Istate.Pstate ({env, ...})) _ guh =
8.216 let
8.217 val (_, _, thyID, sect, xstr) = case guh2theID guh of
8.218 theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)
8.219 @@ -577,4 +470,4 @@
8.220 in (SOME (Selem.subst'_to_sube subst), Selem.subst'_to_subst subst) end
8.221 end
8.222
8.223 -end
8.224 +(**)end(**)
9.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Apr 22 16:53:03 2020 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Thu Apr 23 09:29:56 2020 +0200
9.3 @@ -476,7 +476,7 @@
9.4 let
9.5 val SOME (t', _) = factout_p_ thy t;
9.6 val SOME (t'', asm) = cancel_p_ thy t;
9.7 - val der = Rtools.reverse_deriv thy eval_rls rules ro NONE t';
9.8 + val der = Derive.reverse_deriv thy eval_rls rules ro NONE t';
9.9 val der = der @
9.10 [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'', asm))]
9.11 val rs = (Rtools.distinct_Thm o (map #1)) der
9.12 @@ -498,7 +498,7 @@
9.13
9.14 fun next_rule thy eval_rls ro [rs] t =
9.15 let
9.16 - val der = Rtools.make_deriv thy eval_rls rs ro NONE t;
9.17 + val der = Derive.make_deriv thy eval_rls rs ro NONE t;
9.18 in case der of (_, r, _) :: _ => SOME r | _ => NONE end
9.19 | next_rule _ _ _ _ _ = error ("next_rule: doesnt match rev-sets in istate");
9.20
9.21 @@ -537,7 +537,7 @@
9.22 let
9.23 val SOME (t',_) = common_nominator_p_ thy t;
9.24 val SOME (t'', asm) = add_fraction_p_ thy t;
9.25 - val der = Rtools.reverse_deriv thy eval_rls rules ro NONE t';
9.26 + val der = Derive.reverse_deriv thy eval_rls rules ro NONE t';
9.27 val der = der @
9.28 [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'',asm))]
9.29 val rs = (Rtools.distinct_Thm o (map #1)) der;
9.30 @@ -559,7 +559,7 @@
9.31 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
9.32
9.33 fun next_rule thy eval_rls ro [rs] t =
9.34 - let val der = Rtools.make_deriv thy eval_rls rs ro NONE t;
9.35 + let val der = Derive.make_deriv thy eval_rls rs ro NONE t;
9.36 in
9.37 case der of
9.38 (_,r,_)::_ => SOME r
10.1 --- a/test/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 22 16:53:03 2020 +0200
10.2 +++ b/test/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 23 09:29:56 2020 +0200
10.3 @@ -117,21 +117,21 @@
10.4 *)
10.5 "----------------------------------------------------------";
10.6
10.7 - val fod = make_deriv (@{theory "Isac_Knowledge"}) Atools_erls
10.8 + val fod = Derive.make_deriv (@{theory "Isac_Knowledge"}) Atools_erls
10.9 ((#rules o Rule_Set.rep) Test_simplify)
10.10 (sqrt_right false (@{theory "Pure"})) NONE
10.11 (str2term "x + 1 + -1 * 2 = 0");
10.12 - (writeln o trtas2str) fod;
10.13 + (writeln o Derive.trtas2str) fod;
10.14
10.15 - val ifod = make_deriv (@{theory "Isac_Knowledge"}) Atools_erls
10.16 + val ifod = Derive.make_deriv (@{theory "Isac_Knowledge"}) Atools_erls
10.17 ((#rules o Rule_Set.rep) Test_simplify)
10.18 (sqrt_right false (@{theory "Pure"})) NONE
10.19 (str2term "-2 * 1 + (1 + x) = 0");
10.20 - (writeln o trtas2str) ifod;
10.21 + (writeln o Derive.trtas2str) ifod;
10.22 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
10.23 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
10.24 - val der = fod' @ (map rev_deriv' rifod');
10.25 - (writeln o trtas2str) der;
10.26 + val der = fod' @ (map Derive.rev_deriv' rifod');
10.27 + (writeln o Derive.trtas2str) der;
10.28 "----------------------------------------------------------";
10.29 DEconstrCalcTree 1;
10.30
10.31 @@ -1272,14 +1272,14 @@
10.32 (*
10.33 val ({rew_ord, erls, rules,...}, fo, ifo) =
10.34 (Rule_Set.rep Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
10.35 - (tracing o trtas2str) fod';
10.36 + (tracing o Derive.trtas2str) fod';
10.37 > ["
10.38 (x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))","
10.39 (-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))","
10.40 (-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))","
10.41 (1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
10.42 val it = () : unit
10.43 - (tracing o trtas2str) (map rev_deriv' rifod');
10.44 + (tracing o Derive.trtas2str) (map Derive.rev_deriv' rifod');
10.45 > ["
10.46 (1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))","
10.47 (1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))","
11.1 --- a/test/Tools/isac/Knowledge/rational.sml Wed Apr 22 16:53:03 2020 +0200
11.2 +++ b/test/Tools/isac/Knowledge/rational.sml Thu Apr 23 09:29:56 2020 +0200
11.3 @@ -1692,7 +1692,7 @@
11.4 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
11.5 if UnparseC.term tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" then () else error "rls chancel_p 2";
11.6
11.7 -"----- with make_deriv; WN1130912 not investigated further, will be discontinued";
11.8 +"----- with .make_deriv; WN1130912 not investigated further, will be discontinued";
11.9 val SOME (tt, _) = factout_p_ thy t;
11.10 if UnparseC.term tt = "(a + b) * (a + -1 * b) / ((a + -1 * b) * (a + -1 * b))"
11.11 then () else error "rls chancel_p 3";
11.12 @@ -1700,7 +1700,7 @@
11.13
11.14 "--- with simpler ruleset";
11.15 val {rules, rew_ord= (_, ro), ...} = Rule_Set.rep (assoc_rls "rev_rew_p");
11.16 -val der = make_deriv thy Atools_erls rules ro NONE tt;
11.17 +val der = .make_deriv thy Atools_erls rules ro NONE tt;
11.18 if length der = 12 then () else error "WN1130912 rls chancel_p 4";
11.19 (*default_print_depth 99;*) writeln (deriv2str der); (*default_print_depth 3;*)
11.20
11.21 @@ -1709,12 +1709,12 @@
11.22 (*default_print_depth 99;*) map (Rule.to_string o #2) der; (*default_print_depth 3;*)
11.23 (*default_print_depth 99;*) map (UnparseC.term o #1 o #3) der; (*default_print_depth 3;*)
11.24
11.25 -val der = make_deriv thy Atools_erls rules ro NONE
11.26 +val der = .make_deriv thy Atools_erls rules ro NONE
11.27 (str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
11.28 (*default_print_depth 99;*) writeln (deriv2str der); (*default_print_depth 3;*)
11.29
11.30 val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (assoc_rls "rev_rew_p");
11.31 -val der = make_deriv thy Atools_erls rules ro NONE
11.32 +val der = .make_deriv thy Atools_erls rules ro NONE
11.33 (str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");
11.34 (*default_print_depth 99;*) writeln (deriv2str der); (*default_print_depth 3;*)
11.35 (*default_print_depth 99;*) map (UnparseC.term o #1) der; (*default_print_depth 3;*)
12.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 22 16:53:03 2020 +0200
12.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Apr 23 09:29:56 2020 +0200
12.3 @@ -348,12 +348,12 @@
12.4 | _ => TermC.empty (*on PblObj is fo <> ifo*);
12.5 val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
12.6 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls;
12.7 - (*val (found, der) = *)concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
12.8 -"~~~~~ fun concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
12.9 + (*val (found, der) = *)Derive.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
12.10 +"~~~~~ fun .concat_deriv, args:"; val (rew_ord, erls, rules, fo, ifo) =
12.11 (rew_ord, erls, rules, fo, ifo);
12.12 fun derivat ([]:(term * rule * (term * term list)) list) = TermC.empty
12.13 | derivat dt = (#1 o #3 o last_elem) dt
12.14 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
12.15 - (*val fod = *)make_deriv (Isac"") erls rules (snd rew_ord) NONE fo;
12.16 - (*val ifod = *)make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo;
12.17 + (*val fod = *)Derive.make_deriv (Isac"") erls rules (snd rew_ord) NONE fo;
12.18 + (*val ifod = *)Derive.make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo;
12.19
13.1 --- a/test/Tools/isac/Test_Isac.thy Wed Apr 22 16:53:03 2020 +0200
13.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Apr 23 09:29:56 2020 +0200
13.3 @@ -100,7 +100,7 @@
13.4 open Error_Fill_Pattern;
13.5 open Error_Fill_Def;
13.6 open In_Chead;
13.7 - open Rtools; trtas2str;
13.8 + open Rtools; .trtas2str;
13.9 open Chead; pt_extract;
13.10 open Generate; (* NONE *)
13.11 open Ctree; append_problem;
14.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Apr 22 16:53:03 2020 +0200
14.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Apr 23 09:29:56 2020 +0200
14.3 @@ -100,7 +100,7 @@
14.4 open Error_Fill_Pattern;
14.5 open Error_Fill_Def;
14.6 open In_Chead;
14.7 - open Rtools; trtas2str;
14.8 + open Rtools;
14.9 open Chead; pt_extract;
14.10 open Generate; (* NONE *)
14.11 open Ctree; append_problem;
15.1 --- a/test/Tools/isac/Test_Some.thy Wed Apr 22 16:53:03 2020 +0200
15.2 +++ b/test/Tools/isac/Test_Some.thy Thu Apr 23 09:29:56 2020 +0200
15.3 @@ -20,7 +20,7 @@
15.4 open Error_Fill_Pattern;
15.5 open Error_Fill_Def;
15.6 open In_Chead;
15.7 - open Rtools; trtas2str;
15.8 + open Rtools; .trtas2str;
15.9 open Chead; pt_extract;
15.10 open Generate; (* NONE *)
15.11 open Ctree; append_problem;
16.1 --- a/test/Tools/isac/Test_Some_meld.thy Wed Apr 22 16:53:03 2020 +0200
16.2 +++ b/test/Tools/isac/Test_Some_meld.thy Thu Apr 23 09:29:56 2020 +0200
16.3 @@ -12,7 +12,7 @@
16.4 open LI; scan_dn;
16.5 open Istate;
16.6 open Inform; cas_input;
16.7 - open Rtools; trtas2str;
16.8 + open Rtools; .trtas2str;
16.9 open Chead; pt_extract;
16.10 open Generate; (* NONE *)
16.11 open Ctree; append_problem;