1.1 --- a/src/Tools/isac/Interpret/inform.sml Thu Jul 31 14:21:49 2014 +0200
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu Jul 31 14:32:05 2014 +0200
1.3 @@ -534,27 +534,25 @@
1.4
1.5 (*fo = ifo excluded already in inform*)
1.6 fun concat_deriv rew_ord erls rules fo ifo =
1.7 - let fun derivat ([]:(term * rule * (term * term list)) list) = e_term
1.8 - | derivat dt = (#1 o #3 o last_elem) dt
1.9 - fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
1.10 - val fod = make_deriv (Isac"") erls rules (snd rew_ord) NONE fo
1.11 - val ifod = make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo
1.12 - in case (fod, ifod) of
1.13 - ([], []) => if fo = ifo then (true, [])
1.14 - else (false, [])
1.15 - | (fod, []) => if derivat fod = ifo
1.16 - then (true, fod) (*ifo is normal form*)
1.17 - else (false, [])
1.18 - | ([], ifod) => if fo = derivat ifod
1.19 - then (true, ((map rev_deriv') o rev) ifod)
1.20 - else (false, [])
1.21 - | (fod, ifod) =>
1.22 - if derivat fod = derivat ifod (*common normal form found*)
1.23 - then let val (fod', rifod') =
1.24 - dropwhile' equal (rev fod) (rev ifod)
1.25 - in (true, fod' @ (map rev_deriv' rifod')) end
1.26 - else (false, [])
1.27 - end;
1.28 + let
1.29 + fun derivat ([]:(term * rule * (term * term list)) list) = e_term
1.30 + | derivat dt = (#1 o #3 o last_elem) dt
1.31 + fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
1.32 + val fod = make_deriv (Isac"") erls rules (snd rew_ord) NONE fo
1.33 + val ifod = make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo
1.34 + in
1.35 + case (fod, ifod) of
1.36 + ([], []) => if fo = ifo then (true, []) else (false, [])
1.37 + | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
1.38 + | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
1.39 + | (fod, ifod) =>
1.40 + if derivat fod = derivat ifod (*common normal form found*)
1.41 + then
1.42 + let
1.43 + val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
1.44 + in (true, fod' @ (map rev_deriv' rifod')) end
1.45 + else (false, [])
1.46 + end;
1.47 (*
1.48 val ({rew_ord, erls, rules,...}, fo, ifo) =
1.49 (rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
1.50 @@ -598,7 +596,7 @@
1.51 val (c', ptp) = embed_deriv tacis' ptp;
1.52 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
1.53 else
1.54 - if pos = ([], Res)
1.55 + if pos = ([], Res) (*TODO: we should stop earlier with trying subproblems *)
1.56 then ("no derivation found", (tacis, c, ptp): calcstate')
1.57 else
1.58 let
1.59 @@ -607,7 +605,7 @@
1.60 case tacis of
1.61 ((Subproblem _, _, _)::_) =>
1.62 let
1.63 - val ptp as (pt, (p,_)) = all_modspec ptp
1.64 + val ptp as (pt, (p,_)) = all_modspec ptp (*<------------------*)
1.65 val mI = get_obj g_metID pt p
1.66 in
1.67 nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
2.1 --- a/src/Tools/isac/Interpret/rewtools.sml Thu Jul 31 14:21:49 2014 +0200
2.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Jul 31 14:32:05 2014 +0200
2.3 @@ -85,7 +85,7 @@
2.4
2.5
2.6
2.7 -(*.derive normalform of a rls, or derive until SOME goal,
2.8 +(* derive normalform of a rls, or derive until SOME goal,
2.9 and record rules applied and rewrites.
2.10 val it = fn
2.11 : theory
2.12 @@ -93,7 +93,7 @@
2.13 -> rule list
2.14 -> rew_ord : the order of this rls, which 1 theorem of is used
2.15 for rewriting 1 single step (?14.4.03)
2.16 - -> term option : 040214 ??? nonsense ???
2.17 + -> term option : 040214 ??? use for "derive until SOME goal" ???
2.18 -> term
2.19 -> (term * : to this term ...
2.20 rule * : ... this rule is applied yielding ...
2.21 @@ -104,112 +104,54 @@
2.22 FIXME.WN040214: treats rules as in Rls, _not_ as in Seq
2.23
2.24 WN060825 too complicated for the intended use by cancel_, common_nominator_
2.25 -and unreflectedly adapted to extion of rules by Rls_: returns Rls_("sym_simpl..
2.26 - -- replaced below*)
2.27 -(* val (thy, erls, rs, ro, goal, tt) = (thy, erls, rs, ro, goal, t);
2.28 - val (thy, erls, rs, ro, goal, tt) = (thy, Atools_erls, rules, ro, NONE, tt);
2.29 - *)
2.30 +and unreflectedly adapted to extension of rules by Rls_: returns Rls_("sym_simpl..
2.31 + -- replaced below *)
2.32 fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt =
2.33 - let datatype switch = Appl | Noap
2.34 - fun rew_once lim rts t Noap [] =
2.35 - (case goal of
2.36 - NONE => rts
2.37 - | SOME g =>
2.38 - error ("make_deriv: no derivation for "^(term2str t)))
2.39 - | rew_once lim rts t Appl [] =
2.40 - (*(case rs of Rls _ =>*) rew_once lim rts t Noap rs
2.41 - (*| Seq _ => rts) FIXXXXXME 14.3.03*)
2.42 - | rew_once lim rts t apno rs' =
2.43 - (case goal of
2.44 - NONE => rew_or_calc lim rts t apno rs'
2.45 - | SOME g =>
2.46 - if g = t then rts
2.47 - else rew_or_calc lim rts t apno rs')
2.48 - and rew_or_calc lim rts t apno (rrs' as (r::rs')) =
2.49 - if lim < 0
2.50 - then (tracing ("make_deriv exceeds " ^ int2str (!lim_deriv) ^
2.51 - "with deriv =\n"); tracing (deriv2str rts); rts)
2.52 - else
2.53 - case r of
2.54 - Thm (thmid, tm) =>
2.55 - (if not (!trace_rewrite) then () else
2.56 - tracing ("### trying thm '" ^ thmid ^ "'");
2.57 - case rewrite_ thy ro erls true tm t of
2.58 - NONE => rew_once lim rts t apno rs'
2.59 - | SOME (t',a') =>
2.60 - (if ! trace_rewrite
2.61 - then tracing ("### rewrites to: "^(term2str t')) else();
2.62 - rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs'))
2.63 - | Calc (c as (op_,_)) =>
2.64 - let val _ = if not (!trace_rewrite) then () else
2.65 - tracing ("### trying calc. '" ^ op_ ^ "'")
2.66 - val t = uminus_to_string t
2.67 - in case get_calculation_ thy c t of
2.68 - NONE => rew_once lim rts t apno rs'
2.69 - | SOME (thmid, tm) =>
2.70 - (let val SOME (t',a') = rewrite_ thy ro erls true tm t
2.71 - val _ = if not (!trace_rewrite) then () else
2.72 - tracing("### calc. to: " ^ (term2str t'))
2.73 - val r' = Thm (thmid, tm)
2.74 - in rew_once (lim-1) (rts@[(t,r',(t',a'))]) t' Appl rrs'
2.75 - end)
2.76 - handle _ => error "derive_norm, Calc: no rewrite"
2.77 - end
2.78 -(* TODO.WN080222: see rewrite__set_
2.79 - @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
2.80 - | Cal1 (cc as (op_,_)) =>
2.81 - (let val _= if !trace_rewrite andalso i < ! depth then
2.82 - tracing((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
2.83 - val ct = uminus_to_string ct
2.84 - in case get_calculation_ thy cc ct of
2.85 - NONE => (ct, asm)
2.86 - | SOME (thmid, thm') =>
2.87 - let
2.88 - val pairopt =
2.89 - rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
2.90 - ((#erls o rep_rls) rls) put_asm thm' ct;
2.91 - val _ = if pairopt <> NONE then ()
2.92 - else error("rewrite_set_, rewrite_ \""^
2.93 - (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
2.94 - val _ = if ! trace_rewrite andalso i < ! depth
2.95 - then tracing((idt"="(i+1))^" cal1. to: "^
2.96 - (term2str ((fst o the) pairopt)))
2.97 - else()
2.98 - in the pairopt end
2.99 - end)
2.100 -@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
2.101 - | Rls_ rls =>
2.102 - (case rewrite_set_ thy true rls t of
2.103 - NONE => rew_once lim rts t apno rs'
2.104 - | SOME (t',a') =>
2.105 - rew_once (lim-1) (rts @ [(t,r,(t',a'))]) t' Appl rrs');
2.106 -(*WN060829 | Rls_ rls =>
2.107 - (case rewrite_set_ thy true rls t of
2.108 - NONE => rew_once lim rts t apno rs'
2.109 - | SOME (t',a') =>
2.110 - if ro [] (t, t') then rew_once lim rts t apno rs'
2.111 - else rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs');
2.112 -...lead to deriv = [] with make_polynomial.
2.113 -THERE IS SOMETHING DIFFERENT beetween rewriting with the code above
2.114 -and between rewriting with rewrite_set: with rules from make_polynomial and
2.115 -t = "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)" the actual code
2.116 -leads to cycling Rls_ order_mult_rls_..Rls_ discard_parentheses1..Rls_ order..
2.117 -*)
2.118 - in rew_once (!lim_deriv) [] tt Noap rs end;
2.119 + let
2.120 + datatype switch = Appl | Noap
2.121 + fun rew_once lim rts t Noap [] =
2.122 + (case goal of NONE => rts | SOME g => error ("make_deriv: no derivation for " ^ term2str t))
2.123 + | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs
2.124 + (*| Seq _ => rts) FIXXXXXME 14.3.03*)
2.125 + | rew_once lim rts t apno rs' =
2.126 + (case goal of
2.127 + NONE => rew_or_calc lim rts t apno rs'
2.128 + | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')
2.129 + and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =
2.130 + if lim < 0
2.131 + then (tracing ("make_deriv exceeds " ^ int2str (! lim_deriv) ^
2.132 + "with deriv =\n"); tracing (deriv2str rts); rts)
2.133 + else
2.134 + case r of
2.135 + Thm (thmid, tm) =>
2.136 + (if not (! trace_rewrite) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
2.137 + case rewrite_ thy ro erls true tm t of
2.138 + NONE => rew_once lim rts t apno rs'
2.139 + | SOME (t', a') =>
2.140 + (if ! trace_rewrite then tracing ("### rewrites to: " ^ term2str t') else ();
2.141 + rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
2.142 + | Calc (c as (op_,_)) =>
2.143 + let
2.144 + val _ = if not (! trace_rewrite) then () else tracing ("### trying calc. \"" ^ op_^"\"")
2.145 + val t = uminus_to_string t
2.146 + in
2.147 + case get_calculation_ thy c t of
2.148 + NONE => rew_once lim rts t apno rs'
2.149 + | SOME (thmid, tm) =>
2.150 + (let
2.151 + val SOME (t', a') = rewrite_ thy ro erls true tm t
2.152 + val _ = if not (! trace_rewrite) then () else tracing("### calc. to: " ^term2str t')
2.153 + val r' = Thm (thmid, tm)
2.154 + in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
2.155 + handle _ => error "derive_norm, Calc: no rewrite"
2.156 + end
2.157 + (*| Cal1 (cc as (op_,_)) => ... WN080222 see rewrite__set_: see 7df94616c1bd and earlier*)
2.158 + | Rls_ rls => (* WN060829: CREATES "sym_rlsID", see 7df94616c1bd and earlier*)
2.159 + (case rewrite_set_ thy true rls t of
2.160 + NONE => rew_once lim rts t apno rs'
2.161 + | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs');
2.162 + in rew_once (! lim_deriv) [] tt Noap rs end;
2.163
2.164 -
2.165 -(*.toggles the marker for 'fun sym_thm'.*)
2.166 -fun sym_thmID (thmID : thmID) =
2.167 - case Symbol.explode thmID of
2.168 - "s"::"y"::"m"::"_"::id => implode id : thmID
2.169 - | id => "sym_"^thmID;
2.170 -(*
2.171 -> val thmID = "sym_real_mult_2";
2.172 -> sym_thmID thmID;
2.173 -val it = "real_mult_2" : string
2.174 -> val thmID = "real_num_collect";
2.175 -> sym_thmID thmID;
2.176 -val it = "sym_real_num_collect" : string*)
2.177 fun sym_drop (thmID : thmID) =
2.178 case Symbol.explode thmID of
2.179 "s"::"y"::"m"::"_"::id => implode id : thmID
2.180 @@ -219,7 +161,6 @@
2.181 "s"::"y"::"m"::"_"::id => true
2.182 | id => false;
2.183
2.184 -
2.185 (*FIXXXXME.040219: detail has to handle Rls id="sym_..."
2.186 by applying make_deriv, rev_deriv'; see concat_deriv*)
2.187 fun sym_rls Erls = Erls
3.1 --- a/src/Tools/isac/Knowledge/Atools.thy Thu Jul 31 14:21:49 2014 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Thu Jul 31 14:32:05 2014 +0200
3.3 @@ -224,12 +224,12 @@
3.4 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
3.5 ("xxxxxx",op_,t,thy);
3.6 *)
3.7 -fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) =
3.8 - thmid ^ "Float ((" ^
3.9 - (string_of_int v11)^","^(string_of_int v12)^"), ("^
3.10 - (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
3.11 - (string_of_int v21)^","^(string_of_int v22)^"), ("^
3.12 - (string_of_int p21)^","^(string_of_int p22)^"))";
3.13 +fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)
3.14 + thmid ^ "Float ((" ^
3.15 + (string_of_int v11)^","^(string_of_int v12)^"), ("^
3.16 + (string_of_int p11)^","^(string_of_int p12)^")) __ (("^
3.17 + (string_of_int v21)^","^(string_of_int v22)^"), ("^
3.18 + (string_of_int p21)^","^(string_of_int p22)^"))";
3.19
3.20 (*.convert int and float to internal floatingpoint prepresentation.*)
3.21 fun numeral (Free (str, T)) =
3.22 @@ -246,49 +246,46 @@
3.23 | _ => NONE)
3.24 | numeral _ = NONE;
3.25
3.26 -(*.evaluate binary associative operations.*)
3.27 -fun eval_binop (thmid:string) (op_:string)
3.28 - (t as ( Const(op0,t0) $
3.29 - (Const(op0',t0') $ v $ t1) $ t2))
3.30 - thy = (*binary . (v.n1).n2*)
3.31 +(* evaluate binary associative operations *)
3.32 +fun eval_binop (thmid : string) (op_: string)
3.33 + (t as (Const (op0, t0) $ (Const (op0', _) $ v $ t1) $ t2)) _ = (* binary . (v.n1).n2 *)
3.34 if op0 = op0' then
3.35 - case (numeral t1, numeral t2) of
3.36 - (SOME n1, SOME n2) =>
3.37 - let val (T1,T2,Trange) = dest_binop_typ t0
3.38 - val res = calc (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0) n1 n2
3.39 - (*WN071229 "Fields.inverse_class.divide" never tried*)
3.40 - val rhs = var_op_float v op_ t0 T1 res
3.41 - val prop = Trueprop $ (mk_equality (t, rhs))
3.42 - in SOME ("#: " ^ term2str prop, prop) end
3.43 - | _ => NONE
3.44 + case (numeral t1, numeral t2) of
3.45 + (SOME n1, SOME n2) =>
3.46 + let
3.47 + val (T1, _, _) = dest_binop_typ t0
3.48 + val res =
3.49 + calc (if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0)n1 n2
3.50 + (*WN071229 "Fields.inverse_class.divide" never tried*)
3.51 + val rhs = var_op_float v op_ t0 T1 res
3.52 + val prop = Trueprop $ (mk_equality (t, rhs))
3.53 + in SOME ("#: " ^ term2str prop, prop) end
3.54 + | _ => NONE
3.55 else NONE
3.56 - | eval_binop (thmid:string) (op_:string)
3.57 - (t as
3.58 - (Const (op0, t0) $ t1 $
3.59 - (Const (op0', t0') $ t2 $ v)))
3.60 - thy = (*binary . n1.(n2.v)*)
3.61 - if op0 = op0' then
3.62 - case (numeral t1, numeral t2) of
3.63 - (SOME n1, SOME n2) =>
3.64 - if op0 = "Groups.minus_class.minus" then NONE else
3.65 - let val (T1,T2,Trange) = dest_binop_typ t0
3.66 - val res = calc op0 n1 n2
3.67 - val rhs = float_op_var v op_ t0 T1 res
3.68 - val prop = Trueprop $ (mk_equality (t, rhs))
3.69 - in SOME ("#: " ^ term2str prop, prop) end
3.70 - | _ => NONE
3.71 - else NONE
3.72 -
3.73 - | eval_binop (thmid:string) (op_:string)
3.74 - (t as (Const (op0,t0) $ t1 $ t2)) thy = (*binary . n1.n2*)
3.75 + | eval_binop (thmid : string) (op_ : string)
3.76 + (t as (Const (op0, t0) $ t1 $ (Const (op0', _) $ t2 $ v))) _ = (* binary . n1.(n2.v) *)
3.77 + if op0 = op0' then
3.78 + case (numeral t1, numeral t2) of
3.79 + (SOME n1, SOME n2) =>
3.80 + if op0 = "Groups.minus_class.minus" then NONE
3.81 + else let
3.82 + val (T1, _, _) = dest_binop_typ t0
3.83 + val res = calc op0 n1 n2
3.84 + val rhs = float_op_var v op_ t0 T1 res
3.85 + val prop = Trueprop $ (mk_equality (t, rhs))
3.86 + in SOME ("#: " ^ term2str prop, prop) end
3.87 + | _ => NONE
3.88 + else NONE
3.89 + | eval_binop (thmid : string) _ (t as (Const (op0, t0) $ t1 $ t2)) _ = (* binary . n1.n2 *)
3.90 (case (numeral t1, numeral t2) of
3.91 - (SOME n1, SOME n2) =>
3.92 - let val (T1,T2,Trange) = dest_binop_typ t0;
3.93 - val res = calc op0 n1 n2;
3.94 - val rhs = term_of_float Trange res;
3.95 - val prop = Trueprop $ (mk_equality (t, rhs));
3.96 - in SOME ("#: " ^ term2str prop, prop) end
3.97 - | _ => NONE)
3.98 + (SOME n1, SOME n2) =>
3.99 + let
3.100 + val (_, _, Trange) = dest_binop_typ t0;
3.101 + val res = calc op0 n1 n2;
3.102 + val rhs = term_of_float Trange res;
3.103 + val prop = Trueprop $ (mk_equality (t, rhs));
3.104 + in SOME ("#: " ^ term2str prop, prop) end
3.105 + | _ => NONE)
3.106 | eval_binop _ _ _ _ = NONE;
3.107 (*
3.108 > val SOME (thmid, t) = eval_binop "#add_" "Groups.plus_class.plus" (str2term "-1 + 2") thy;
4.1 --- a/src/Tools/isac/ProgLang/calculate.sml Thu Jul 31 14:21:49 2014 +0200
4.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Thu Jul 31 14:32:05 2014 +0200
4.3 @@ -62,79 +62,46 @@
4.4 fn : string -> string -> term -> theory -> (string * term) option
4.5 ^^^^^^... the selecting operator op_ (variable for eval_binop)
4.6 *)
4.7 -fun get_pair thy op_ (ef:string -> term -> theory -> (string * term) option)
4.8 - (t as (Const(op0,t0) $ arg)) = (* unary fns *)
4.9 -(* val (thy, op_, (ef), (t as (Const(op0,t0) $ arg))) =
4.10 - (thy, op_, eval_fn, ct);
4.11 - *)
4.12 +fun get_pair thy op_ (ef: eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
4.13 if op_ = op0 then
4.14 - let val popt = ef op_ t thy
4.15 - in case popt of
4.16 - SOME _ => popt
4.17 - | NONE => get_pair thy op_ ef arg end
4.18 + let val popt = ef op_ t thy
4.19 + in case popt of SOME _ => popt | NONE => get_pair thy op_ ef arg end
4.20 else get_pair thy op_ ef arg
4.21 -
4.22 - | get_pair thy "Atools.ident" ef (t as (Const("Atools.ident",t0) $ _ $ _ )) =
4.23 -(* val (thy, "Atools.ident", ef, t as (Const(op0,_) $ t1 $ t2)) =
4.24 - (thy, op_, eval_fn, ct);
4.25 - *)
4.26 - ef "Atools.ident" t thy (* not nested *)
4.27 + | get_pair thy "Atools.ident" ef (t as (Const ("Atools.ident", _) $ _ $ _ )) =
4.28 + ef "Atools.ident" t thy (* not nested *)
4.29 + | get_pair thy op_ ef (t as (Const (op0,_) $ t1 $ t2)) = (* binary funs *)
4.30 + ((* tracing ("1.. get_pair: binop = "^op_); *)
4.31 + if op_ = op0 then
4.32 + let val popt = ef op_ t thy
4.33 + (* val _ = tracing ("2.. get_pair: " ^ term2str t ^ " -> " ^ popt2str popt) *)
4.34 + in case popt of SOME _ => popt | NONE =>
4.35 + let val popt = get_pair thy op_ ef t1
4.36 + (* val _ = tracing ("3.. get_pair: " ^ term2str t1 ^ " -> "^popt2str popt) *)
4.37 + in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end
4.38 + end
4.39 + else (* search subterms *)
4.40 + let val popt = get_pair thy op_ ef t1
4.41 + (*val _ = tracing("4.. get_pair: "^term2str t^" -> "^popt2str popt)*)
4.42 + in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end)
4.43 + | get_pair thy op_ ef (t as (Const (op0, _) $ t1 $ t2 $ t3)) = (* ternary funs *)
4.44 + ((*tracing ("### get_pair 4a: t= " ^ term2str t);
4.45 + tracing ("### get_pair 4a: op_= " ^ op_);
4.46 + tracing ("### get_pair 4a: op0= " ^ op0); *)
4.47 + if op_ = op0 then
4.48 + case ef op_ t thy of st as SOME _ => st | NONE =>
4.49 + (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)
4.50 + else
4.51 + (case get_pair thy op_ ef t1 of st as SOME _ => st | NONE =>
4.52 + (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)))
4.53 + | get_pair thy op_ ef (Abs (_, _, body)) = get_pair thy op_ ef body
4.54 + | get_pair thy op_ ef (t1 $ t2) =
4.55 + let (* val _= tracing ("5.. get_pair t1 $ t2: " ^ term2str t1 ^ " $ " ^ term2str t2) *)
4.56 + val popt = get_pair thy op_ ef t1
4.57 + in case popt of SOME _ => popt
4.58 + | NONE => ((* tracing "### get_pair: t1 $ t2 -> NONE"; *) get_pair thy op_ ef t2)
4.59 + end
4.60 + | get_pair _ _ _ _ = NONE
4.61
4.62 - | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2)) = (* binary funs*)
4.63 -(* val (thy, op_, ef, (t as (Const(op0,_) $ t1 $ t2))) =
4.64 - (thy, op_, eval_fn, ct);
4.65 - *)
4.66 - ((*tracing("1.. get_pair: binop = "^op_);*)
4.67 - if op_ = op0 then
4.68 - let val popt = ef op_ t thy
4.69 - (*val _ = tracing("2.. get_pair: "^term2str t^" -> "^popt2str popt)*)
4.70 - in case popt of
4.71 - SOME (id,_) => popt
4.72 - | NONE =>
4.73 - let val popt = get_pair thy op_ ef t1
4.74 - (*val _ = tracing("3.. get_pair: "^term2str t1^
4.75 - " -> "^popt2str popt)*)
4.76 - in case popt of
4.77 - SOME (id,_) => popt
4.78 - | NONE => get_pair thy op_ ef t2
4.79 - end
4.80 - end
4.81 - else (*search subterms*)
4.82 - let val popt = get_pair thy op_ ef t1
4.83 - (*val _ = tracing("4.. get_pair: "^term2str t^" -> "^popt2str popt)*)
4.84 - in case popt of
4.85 - SOME (id,_) => popt
4.86 - | NONE => get_pair thy op_ ef t2
4.87 - end)
4.88 - | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2 $ t3)) =(* trinary funs*)
4.89 - ((*tracing("### get_pair 4a: t= "^term2str t);
4.90 - tracing("### get_pair 4a: op_= "^op_);
4.91 - tracing("### get_pair 4a: op0= "^op0);*)
4.92 - if op_ = op0 then
4.93 - case ef op_ t thy of
4.94 - SOME tt => SOME tt
4.95 - | NONE => (case get_pair thy op_ ef t2 of
4.96 - SOME tt => SOME tt
4.97 - | NONE => get_pair thy op_ ef t3)
4.98 - else (case get_pair thy op_ ef t1 of
4.99 - SOME tt => SOME tt
4.100 - | NONE => (case get_pair thy op_ ef t2 of
4.101 - SOME tt => SOME tt
4.102 - | NONE => get_pair thy op_ ef t3)))
4.103 - | get_pair thy op_ ef (Const _) = NONE
4.104 - | get_pair thy op_ ef (Free _) = NONE
4.105 - | get_pair thy op_ ef (Var _) = NONE
4.106 - | get_pair thy op_ ef (Bound _) = NONE
4.107 - | get_pair thy op_ ef (Abs(a,T,body)) = get_pair thy op_ ef body
4.108 - | get_pair thy op_ ef (t1$t2) =
4.109 - let(*val _= tracing("5.. get_pair t1 $ t2: "^term2str t1^"
4.110 - $ "^term2str t2)*)
4.111 - val popt = get_pair thy op_ ef t1
4.112 - in case popt of
4.113 - SOME _ => popt
4.114 - | NONE => ((*tracing"### get_pair: t1 $ t2 -> NONE";*)
4.115 - get_pair thy op_ ef t2)
4.116 - end;
4.117 (*
4.118 > val t = (term_of o the o (parse thy)) "#3 + #4";
4.119 > val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));
4.120 @@ -221,15 +188,11 @@
4.121 (*.get a thm from an op_ somewhere in the term;
4.122 apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711).*)
4.123 fun get_calculation_ thy (op_, eval_fn) ct =
4.124 -(* val (thy, (op_, eval_fn), ct) =
4.125 - (thy, (the (assoc(!calclist',"order_system"))), t);
4.126 - *)
4.127 case get_pair thy op_ eval_fn ct of
4.128 - NONE => ((*tracing("@@@ get_calculation: NONE, op_="^op_);
4.129 - tracing("@@@ get_calculation: ct= ");atomty ct;*)
4.130 - NONE)
4.131 - | SOME (thmid,t) =>
4.132 - SOME (thmid, (make_thm o (cterm_of thy)) t);
4.133 + NONE => ((* tracing ("@@@ get_calculation: NONE, op_= " ^ op_);
4.134 + tracing ("@@@ get_calculation: ct= "); atomty ct; *)
4.135 + NONE)
4.136 + | SOME (thmid, t) => SOME (thmid, (make_thm o (cterm_of thy)) t);
4.137 (*
4.138 > val ct = (the o (parse thy)) "#9 is_const";
4.139 > get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
5.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Thu Jul 31 14:21:49 2014 +0200
5.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Thu Jul 31 14:32:05 2014 +0200
5.3 @@ -386,18 +386,17 @@
5.4 identifiers starting with "#" come from Calc and
5.5 get a hand-made theorem (containing numerals only).*)
5.6 fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
5.7 - (case Symbol.explode thmid of
5.8 - "s"::"y"::"m"::"_"::id =>
5.9 - if hd id = "#"
5.10 - then mk_thm thy ct'
5.11 - else ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
5.12 - | id =>
5.13 - if hd id = "#"
5.14 - then mk_thm thy ct'
5.15 - else (num_str o (Global_Theory.get_thm thy)) thmid
5.16 - ) handle _ =>
5.17 - error ("assoc_thm': '"^thmid^"' not in '"^
5.18 - (theory2domID thy)^"' (and parents)");
5.19 + (case Symbol.explode thmid of
5.20 + "s"::"y"::"m"::"_"::id =>
5.21 + if hd id = "#"
5.22 + then mk_thm thy ct'
5.23 + else ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
5.24 + | id =>
5.25 + if hd id = "#"
5.26 + then mk_thm thy ct'
5.27 + else (num_str o (Global_Theory.get_thm thy)) thmid
5.28 + ) handle _ =>
5.29 + error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)")
5.30 (*> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_#mult_2_3","6 = 2 * 3");
5.31 val it = "6 = 2 * 3" : thm
5.32
5.33 @@ -407,7 +406,7 @@
5.34 > assoc_thm' (Thy_Info.get_theory "Isac") ("sym_real_add_zero_left","");
5.35 val it = "?t = 0 + ?t" [.] : thm
5.36
5.37 -> assoc_thm' HOL.thy ("sym_real_add_zero_left","");
5.38 +> assoc_thm' @{theory HOL} ("sym_real_add_zero_left","");
5.39 *** Unknown theorem(s) "add_0_left"
5.40 *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)
5.41 uncaught exception ERROR*)
6.1 --- a/src/Tools/isac/calcelems.sml Thu Jul 31 14:21:49 2014 +0200
6.2 +++ b/src/Tools/isac/calcelems.sml Thu Jul 31 14:32:05 2014 +0200
6.3 @@ -18,13 +18,14 @@
6.4 val empty_cterm' = "empty_cterm'";
6.5
6.6 (* TODO CLEANUP Thm:
6.7 -type rule = Thm : (a) needs no identifier since reflection is built-in since Isabelle2011
6.8 - (b) investigate if ""RS sym" attaches a [.]" still occurs: string_of_thmI
6.9 -thmID : user input + program
6.10 -thmDeriv : for thy_hierarchy ONLY
6.11 -obsolete types : thm' (SEE "ad thm'"), thm''.
6.12 -revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm'_of_thm thm.
6.13 -activate : thmID_of_derivation_name'
6.14 +type rule =
6.15 +Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
6.16 + (b) investigate if ""RS sym" attaches a [.]" still occurs: string_of_thmI
6.17 +thmID : type for data from user input + program
6.18 +thmDeriv : type for thy_hierarchy ONLY
6.19 +obsolete types : thm' (SEE "ad thm'"), thm''.
6.20 +revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm'_of_thm thm.
6.21 +activate : thmID_of_derivation_name'
6.22 *)
6.23 type thmID = string; (* identifier for a thm (the shortest possible identifier) *)
6.24 type thmDeriv = string; (* WN120524 deprecated
6.25 @@ -114,10 +115,10 @@
6.26 Erule (*.the empty rule .*)
6.27 | Thm of (string * Basic_Thm.thm) (* see TODO CLEANUP Thm *)
6.28 | Calc of string * (*.sml-code manipulating a (sub)term .*)
6.29 - (string -> term -> theory -> (string * term) option)
6.30 + eval_fn
6.31 | Cal1 of string * (*.sml-code applied only to whole term
6.32 or left/right-hand-side of eqality .*)
6.33 - (string -> term -> theory -> (string * term) option)
6.34 + eval_fn
6.35 | Rls_ of rls (*.ie. rule sets may be nested.*)
6.36 and scr =
6.37 EmptyScr
6.38 @@ -535,7 +536,7 @@
6.39 fun thes2str thes = map the2str thes |> list2str;
6.40
6.41 (* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
6.42 -TODO (a): thehier does not contain sym_thmID theorems
6.43 + (a): thehier does not contain sym_thmID theorems
6.44 (b): lookup for sym_thmID directly from Isabelle using sym_thm
6.45 (within math-engine NO lookup in thehier -- within java in *.xml only!)
6.46 TODO (c): export from thehier to xml
7.1 --- a/test/Tools/isac/Knowledge/atools.sml Thu Jul 31 14:21:49 2014 +0200
7.2 +++ b/test/Tools/isac/Knowledge/atools.sml Thu Jul 31 14:32:05 2014 +0200
7.3 @@ -18,6 +18,7 @@
7.4 "----------- boollist2sum -------------------------------";
7.5 "----------- Matthias Goldgruber 2003 rewrite orders ----";
7.6 (*"----------- introduction by MG 2003 --------------------";*)
7.7 +"----------- fun eval_binop -----------------------------";
7.8 "--------------------------------------------------------";
7.9
7.10
7.11 @@ -299,3 +300,31 @@
7.12 val t = (term_of o the o (parseold thy)) "7";
7.13 ##################################################################################*)
7.14
7.15 +"----------- fun eval_binop -----------------------------";
7.16 +"----------- fun eval_binop -----------------------------";
7.17 +"----------- fun eval_binop -----------------------------";
7.18 +val (op_, ef) = the (assoc (calclist, "TIMES"));
7.19 +val t = (term_of o the o (parse thy)) "2 * 3";
7.20 +(*val SOME (thmid,t') = *)get_pair thy op_ ef t;
7.21 +;
7.22 +"~~~~~ fun get_pair, args:"; val (thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
7.23 + (thy, op_, ef, t);
7.24 +op_ = op0 = true;
7.25 +ef op_ t thy
7.26 +;
7.27 +"~~~~~ fun eval_binop, args:"; val ((thmid : string), (op_: string),
7.28 + (t as (Const (op0, t0) $ t1 $ t2)), _) = ("#mult_", op_, t, thy); (* binary . n1.(n2.v) *)
7.29 +val (SOME n1, SOME n2) = (numeral t1, numeral t2)
7.30 + val (_, _, Trange) = dest_binop_typ t0;
7.31 + val res = calc op0 n1 n2;
7.32 + val rhs = term_of_float Trange res;
7.33 + val prop = Trueprop $ (mk_equality (t, rhs));
7.34 +val SOME (thmid, tm) = SOME ("#: " ^ term2str prop, prop)
7.35 +;
7.36 +if thmid = "#: 2 * 3 = 6" andalso term2str prop = "2 * 3 = 6" then ()
7.37 +else error "eval_binop changed"
7.38 +;
7.39 +val SOME (thmid, tm) = eval_binop "#mult_" op_ t thy;
7.40 +if thmid = "#: 2 * 3 = 6" andalso term2str prop = "2 * 3 = 6" then ()
7.41 +else error "eval_binop changed 2"
7.42 +