1.1 --- a/src/Tools/isac/Interpret/ctree.sml Tue Oct 22 17:38:34 2013 +0200
1.2 +++ b/src/Tools/isac/Interpret/ctree.sml Thu Oct 24 00:02:29 2013 +0100
1.3 @@ -495,14 +495,14 @@
1.4 | rls_of_rewset (Detail_Set_Inst (subs, rls)) =
1.5 (rls, SOME ((subs2subst (assoc_thy "Isac") subs):subst));
1.6
1.7 -fun rule2tac _ (Calc (opID, thm)) = Calculate (assoc_calc opID)
1.8 - | rule2tac [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm)
1.9 - | rule2tac subst (Thm (thmID, thm)) =
1.10 +fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID)
1.11 + | rule2tac _ [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm)
1.12 + | rule2tac _ subst (Thm (thmID, thm)) =
1.13 Rewrite_Inst (subst2subs subst, (thmID, string_of_thmI thm))
1.14 - | rule2tac [] (Rls_ rls) = Rewrite_Set (id_rls rls)
1.15 - | rule2tac subst (Rls_ rls) =
1.16 + | rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls)
1.17 + | rule2tac _ subst (Rls_ rls) =
1.18 Rewrite_Set_Inst (subst2subs subst, (id_rls rls))
1.19 - | rule2tac _ rule =
1.20 + | rule2tac _ _ rule =
1.21 error ("rule2tac: called with '" ^ rule2str rule ^ "'");
1.22
1.23 type fmz_ = cterm' list;
2.1 --- a/src/Tools/isac/Interpret/ptyps.sml Tue Oct 22 17:38:34 2013 +0200
2.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Thu Oct 24 00:02:29 2013 +0100
2.3 @@ -683,7 +683,7 @@
2.4 in ({guh=guh,mathauthors=maa,init=init,
2.5 ppc=gi@fi@re, pre=wh, rew_ord'=ro, erls=rls, srls=srls, prls=prls,
2.6 calc = if scr = "empty_script" then []
2.7 - else ((map assoc_calc') o (map op_of_calc) o
2.8 + else ((assoc_calc' thy |> map) o (map op_of_calc) o
2.9 (filter is_calc) o stacpbls) sc,
2.10 crls=cr, errpats = ep, nrls= nr, scr = Prog sc}:met,
2.11 metID:metID)
3.1 --- a/src/Tools/isac/Interpret/rewtools.sml Tue Oct 22 17:38:34 2013 +0200
3.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Oct 24 00:02:29 2013 +0100
3.3 @@ -493,11 +493,11 @@
3.4 val dropthys' = map (get_thy o (#1 : (theory' * theory) -> theory')) dropthys
3.5 val ancestors_cal =
3.6 filter_out ((curry ((op mem) o swap) dropthys') o (#1 : calc -> string))
3.7 - (rev (!calclist'))
3.8 + (Thy_Info.get_theory thy' |> KEStore_Elems.get_calcs |> rev)
3.9 in case assoc (ancestors_cal, strip_thy termop) of
3.10 SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
3.11 | _ => error ("thy_containing_cal : rls '" ^ termop ^
3.12 - "' not in ! calclist' of ancestors of thy '" ^ thy' ^ "'")
3.13 + "' not in KEStore_Elems of ancestors of thy '" ^ thy' ^ "'")
3.14 end
3.15 end; (*local*)
3.16
3.17 @@ -709,18 +709,18 @@
3.18 fun try_rew thy ((_, ro):rew_ord) erls (subst:subst) f (thm' as Thm(id, thm)) =
3.19 if contains_bdv thm
3.20 then case rewrite_inst_ thy ro erls false subst thm f of
3.21 - SOME (f',_) =>[rule2tac subst thm']
3.22 + SOME (f',_) =>[rule2tac thy subst thm']
3.23 | NONE => []
3.24 else (case rewrite_ thy ro erls false thm f of
3.25 - SOME (f',_) => [rule2tac [] thm']
3.26 + SOME (f',_) => [rule2tac thy [] thm']
3.27 | NONE => [])
3.28 | try_rew thy _ _ _ f (cal as Calc c) =
3.29 (case get_calculation_ thy c f of
3.30 - SOME (str, _) => [rule2tac [] cal]
3.31 + SOME (str, _) => [rule2tac thy [] cal]
3.32 | NONE => [])
3.33 | try_rew thy _ _ _ f (cal as Cal1 c) =
3.34 (case get_calculation_ thy c f of
3.35 - SOME (str, _) => [rule2tac [] cal]
3.36 + SOME (str, _) => [rule2tac thy [] cal]
3.37 | NONE => [])
3.38 | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
3.39 and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules,...}) =
3.40 @@ -734,7 +734,7 @@
3.41 (* val
3.42 *)
3.43 fun atomic_appl_tacs thy _ _ f (Calculate scrID) =
3.44 - try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' scrID |> snd))
3.45 + try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' thy scrID |> snd))
3.46 | atomic_appl_tacs thy ro erls f (Rewrite (thm' as (thmID, _))) =
3.47 try_rew thy (ro, assoc_rew_ord ro) erls [] f
3.48 (Thm (thmID, assoc_thm' thy thm'))
4.1 --- a/src/Tools/isac/Interpret/script.sml Tue Oct 22 17:38:34 2013 +0200
4.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Oct 24 00:02:29 2013 +0100
4.3 @@ -536,16 +536,24 @@
4.4 then
4.5 if f = f_ then Ass (m,f') else AssWeak (m,f')
4.6 else NotAss
4.7 - | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free(rls_,_) $_$f_) =>
4.8 - if contains_rule (Calc (assoc_calc' op_ |> snd)) (assoc_rls rls_)
4.9 - then
4.10 - if f = f_ then Ass (m,f') else AssWeak (m,f')
4.11 - else NotAss
4.12 + | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free(rls_,_) $_$f_) =>
4.13 + let
4.14 + val thy = ML_Context.the_generic_context () |> Context.theory_of;
4.15 + in
4.16 + if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
4.17 + then
4.18 + if f = f_ then Ass (m,f') else AssWeak (m,f')
4.19 + else NotAss
4.20 + end
4.21 | (Const ("Script.Rewrite'_Set",_) $ Free (rls_, _) $ _ $ f_) =>
4.22 - if contains_rule (Calc (assoc_calc' op_ |> snd)) (assoc_rls rls_)
4.23 - then
4.24 - if f = f_ then Ass (m,f') else AssWeak (m,f')
4.25 - else NotAss
4.26 + let
4.27 + val thy = ML_Context.the_generic_context () |> Context.theory_of;
4.28 + in
4.29 + if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
4.30 + then
4.31 + if f = f_ then Ass (m,f') else AssWeak (m,f')
4.32 + else NotAss
4.33 + end
4.34 | _ => NotAss)
4.35
4.36 | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
5.1 --- a/src/Tools/isac/Interpret/solve.sml Tue Oct 22 17:38:34 2013 +0200
5.2 +++ b/src/Tools/isac/Interpret/solve.sml Thu Oct 24 00:02:29 2013 +0100
5.3 @@ -424,10 +424,10 @@
5.4 in complete_solve auto (c @ c') ptp end;
5.5
5.6 (* aux.fun for detailrls with Rrls, reverse rewriting *)
5.7 -fun rul_terms_2nds nds t [] = nds
5.8 - | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) =
5.9 - (append_atomic [] (e_istate, e_ctxt) t (rule2tac [] rule) res Complete EmptyPtree) ::
5.10 - (rul_terms_2nds nds t' rts);
5.11 +fun rul_terms_2nds _ nds t [] = nds
5.12 + | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =
5.13 + (append_atomic [] (e_istate, e_ctxt) t (rule2tac thy [] rule) res Complete EmptyPtree) ::
5.14 + (rul_terms_2nds thy nds t' rts);
5.15
5.16 (* detail steps done internally by Rewrite_Set* into ctree by use of a script *)
5.17 fun detailrls pt (pos as (p,p_):pos') =
5.18 @@ -441,7 +441,7 @@
5.19 Rrls {scr = Rfuns {init_state,...},...} =>
5.20 let
5.21 val (_,_,_,rul_terms) = init_state t
5.22 - val newnds = rul_terms_2nds [] t rul_terms
5.23 + val newnds = rul_terms_2nds (Proof_Context.theory_of ctxt) [] t rul_terms
5.24 val pt''' = ins_chn newnds pt p
5.25 in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
5.26 | _ =>
6.1 --- a/src/Tools/isac/KEStore.thy Tue Oct 22 17:38:34 2013 +0200
6.2 +++ b/src/Tools/isac/KEStore.thy Thu Oct 24 00:02:29 2013 +0100
6.3 @@ -80,7 +80,7 @@
6.4 ("e_rrls", ("Tools", e_rrls))]);
6.5
6.6 (*TODO.WN080102 clarify usage of type cal and type calc..*)
6.7 -fun assoc_calc calID = let
6.8 +(* fun assoc_calc calID = let
6.9 fun ass ([], key) =
6.10 error ("assoc_calc: '"^ key ^"' not found")
6.11 | ass ((calc, (keyi, _)) :: pairs, key) =
6.12 @@ -92,20 +92,21 @@
6.13 error ("assoc_calc': '" ^ key ^ "' not found")
6.14 | ass ((all as (keyi, _)) :: pairs, key) =
6.15 if key = keyi then all else ass (pairs, key);
6.16 - in ass (!calclist', key') end;
6.17 + in ass (!calclist', key') end; *)
6.18
6.19 -(* fun assoc_calc calID = (* commented out *)
6.20 - case AList.lookup (op =) (Thy_Info.get_theory "Isac" |> KEStore_Elems.get_calcs) calID of
6.21 - SOME (_, calc) => calc
6.22 - | NONE => error ("calID " ^ calID ^ " missing in KEStore.\n" ^
6.23 - "TODO exception hierarchy needs to be established.")
6.24 +fun assoc_calc thy calID = let
6.25 + fun ass ([], key) =
6.26 + error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
6.27 + | ass ((calc, (keyi, _)) :: pairs, key) =
6.28 + if key = keyi then calc else ass (pairs, key);
6.29 + in ass (thy |> KEStore_Elems.get_calcs, calID) end;
6.30
6.31 -fun assoc_calc' key' = (* commented out *)
6.32 - case AList.lookup (op =) (Thy_Info.get_theory "Isac" |> KEStore_Elems.get_calcs) key' of
6.33 - SOME (key, calc) => (key, calc)
6.34 - | NONE => error ("calID " ^ key' ^ " missing in KEStore.\n" ^
6.35 - "TODO exception hierarchy needs to be established.") *)
6.36 -
6.37 +fun assoc_calc' thy key = let
6.38 + fun ass ([], key') =
6.39 + error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
6.40 + | ass ((all as (keyi, _)) :: pairs, key') =
6.41 + if key' = keyi then all else ass (pairs, key');
6.42 + in ass (KEStore_Elems.get_calcs thy, key) end;
6.43 *}
6.44 setup {* KEStore_Elems.add_rlss
6.45 [("e_rls", (Context.theory_name @{theory}, e_rls)),
7.1 --- a/src/Tools/isac/Knowledge/Atools.thy Tue Oct 22 17:38:34 2013 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Thu Oct 24 00:02:29 2013 +0100
7.3 @@ -709,7 +709,7 @@
7.4 ("POWER" ,("Atools.pow", eval_binop "#power_")),
7.5 ("boollist2sum",("Atools.boollist2sum", eval_boollist2sum ""))] *}
7.6 ML {*
7.7 -val list_rls = prep_rls (merge_rls "list_erls"
7.8 +val list_rls = prep_rls' @{theory} (merge_rls "list_erls"
7.9 (Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
7.10 erls = Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
7.11 erls = e_rls, srls = Erls, calc = [], errpatts = [],
7.12 @@ -724,6 +724,6 @@
7.13 ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);
7.14 *}
7.15 setup {* KEStore_Elems.add_rlss
7.16 - [("list_rls", (Context.theory_name @{theory}, prep_rls list_rls))] *}
7.17 + [("list_rls", (Context.theory_name @{theory}, prep_rls' @{theory} list_rls))] *}
7.18
7.19 end
8.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Tue Oct 22 17:38:34 2013 +0200
8.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Thu Oct 24 00:02:29 2013 +0100
8.3 @@ -382,13 +382,13 @@
8.4 \ (Try (Repeat (Rewrite add_commute False))) @@ \
8.5 \ (Try (Repeat (Rewrite mult_commute False)))) t";
8.6
8.7 -fun rule2stac (Thm (thmID, _)) =
8.8 +fun rule2stac _ (Thm (thmID, _)) =
8.9 Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ @{term False}))
8.10 - | rule2stac (Calc (c, _)) =
8.11 - Try $ (Repeat $ (Cal $ Free (assoc_calc c, IDtype)))
8.12 - | rule2stac (Cal1 (c, _)) =
8.13 - Try $ (Repeat $ (Ca1 $ Free (assoc_calc c, IDtype)))
8.14 - | rule2stac (Rls_ rls) =
8.15 + | rule2stac thy (Calc (c, _)) =
8.16 + Try $ (Repeat $ (Cal $ Free (assoc_calc thy c, IDtype)))
8.17 + | rule2stac thy (Cal1 (c, _)) =
8.18 + Try $ (Repeat $ (Ca1 $ Free (assoc_calc thy c, IDtype)))
8.19 + | rule2stac _ (Rls_ rls) =
8.20 Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ @{term False});
8.21 (*val t = rule2stac [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));
8.22 atomt t; term2str t;
8.23 @@ -397,14 +397,14 @@
8.24 val t = rule2stac [] (Rls_ rearrange_assoc);
8.25 atomt t; term2str t;
8.26 *)
8.27 -fun rule2stac_inst (Thm (thmID, _)) =
8.28 +fun rule2stac_inst _ (Thm (thmID, _)) =
8.29 Try $ (Repeat $ (Rew_Inst $ Subs $ Free (thmID, IDtype) $
8.30 @{term False}))
8.31 - | rule2stac_inst (Calc (c, _)) =
8.32 - Try $ (Repeat $ (Cal $ Free (assoc_calc c, IDtype)))
8.33 - | rule2stac_inst (Cal1 (c, _)) =
8.34 - Try $ (Repeat $ (Cal $ Free (assoc_calc c, IDtype)))
8.35 - | rule2stac_inst (Rls_ rls) =
8.36 + | rule2stac_inst thy (Calc (c, _)) =
8.37 + Try $ (Repeat $ (Cal $ Free (assoc_calc thy c, IDtype)))
8.38 + | rule2stac_inst thy (Cal1 (c, _)) =
8.39 + Try $ (Repeat $ (Cal $ Free (assoc_calc thy c, IDtype)))
8.40 + | rule2stac_inst _ (Rls_ rls) =
8.41 Try $ (Rew_Set_Inst $ Subs $ Free (id_rls rls, IDtype) $
8.42 @{term False});
8.43 (*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str @{thm real_diff_minus));
8.44 @@ -445,45 +445,47 @@
8.45 | contain_bdv (r::_) =
8.46 error ("contain_bdv called with ["^(id_rule r)^",...]");
8.47
8.48 -fun rules2scr_Rls rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
8.49 +fun rules2scr_Rls thy rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
8.50 if contain_bdv rules
8.51 then ScrStep_inst $ Term $ Bdv $
8.52 - (Repeat $ (((@@ o (map (rule2stac_inst))) rules) $ e_term))
8.53 + (Repeat $ (((@@ o (map (rule2stac_inst thy))) rules) $ e_term))
8.54 else ScrStep $ Term $
8.55 - (Repeat $ (((@@ o (map (rule2stac ))) rules) $ e_term));
8.56 + (Repeat $ (((@@ o (map (rule2stac thy))) rules) $ e_term));
8.57 (* val (calc, rules) = (!calclist', rules);
8.58 *)
8.59 -fun rules2scr_Seq rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
8.60 +fun rules2scr_Seq thy rules = (*WN100816 t_ -> t_t like "Script Stepwise..*)
8.61 if contain_bdv rules
8.62 then ScrStep_inst $ Term $ Bdv $
8.63 - (((@@ o (map (rule2stac_inst))) rules) $ e_term)
8.64 + (((@@ o (map (rule2stac_inst thy))) rules) $ e_term)
8.65 else ScrStep $ Term $
8.66 - (((@@ o (map (rule2stac ))) rules) $ e_term);
8.67 + (((@@ o (map (rule2stac thy))) rules) $ e_term);
8.68
8.69 (*.prepare the input for an rls for use:
8.70 # generate a script for stepwise execution of the rls
8.71 # filter the operators for Calc out of the script ?WN111014?
8.72 !!!use this function in ruleset' := !!! .*)
8.73 -fun prep_rls Erls = error "prep_rls not impl. for Erls"
8.74 - | prep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,rules,errpatts,...}) =
8.75 - let val sc = (rules2scr_Rls rules)
8.76 +fun prep_rls' _ Erls = error "prep_rls not impl. for Erls"
8.77 + | prep_rls' thy (Rls {id,preconds,rew_ord,erls,srls,calc,rules,errpatts,...}) =
8.78 + let val sc = (rules2scr_Rls thy rules)
8.79 in Rls {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
8.80 srls = srls,
8.81 calc = (*FIXXXME.040207 use also for met*)
8.82 - ((map assoc_calc') o (map op_of_calc) o
8.83 + ((assoc_calc' thy |> map) o (map op_of_calc) o
8.84 (filter is_calc) o stacpbls) sc,
8.85 rules = rules,
8.86 errpatts=errpatts,
8.87 scr = Prog sc} end
8.88 - | prep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,rules,errpatts,...}) =
8.89 - let val sc = (rules2scr_Seq rules)
8.90 + | prep_rls' thy (Seq {id,preconds,rew_ord,erls,srls,calc,rules,errpatts,...}) =
8.91 + let val sc = (rules2scr_Seq thy rules)
8.92 in Seq {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
8.93 srls=srls,
8.94 - calc = ((map assoc_calc') o (map op_of_calc) o
8.95 + calc = ((assoc_calc' thy |> map) o (map op_of_calc) o
8.96 (filter is_calc) o stacpbls) sc,
8.97 rules=rules,
8.98 errpatts=errpatts,
8.99 scr = Prog sc} end
8.100 - | prep_rls (Rrls {id,...}) =
8.101 + | prep_rls' _ (Rrls {id,...}) =
8.102 error ("prep_rls not required for Rrls \"" ^ id ^ "\"");
8.103
8.104 +fun prep_rls rls = prep_rls' (ML_Context.the_generic_context () |> Context.theory_of) rls;
8.105 +
9.1 --- a/test/Tools/isac/ProgLang/calculate.sml Tue Oct 22 17:38:34 2013 +0200
9.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Thu Oct 24 00:02:29 2013 +0100
9.3 @@ -28,7 +28,7 @@
9.4 "----------- check return value of get_calculation_ ----";
9.5 "----------- check return value of get_calculation_ ----";
9.6 val thy = @{theory "Poly"};
9.7 -val cal = snd (assoc_calc' "is_polyexp");
9.8 +val cal = snd (assoc_calc' thy "is_polyexp");
9.9 val t = @{term "(x / x) is_polyexp"};
9.10 val SOME (thmID, thm) = get_calculation_ thy cal t;
9.11 (HOLogic.dest_Trueprop (prop_of thm); writeln "all thms wrapped by Trueprop")