1.1 --- a/src/Tools/isac/Frontend/interface.sml Thu Oct 06 17:03:44 2016 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Mon Oct 10 18:24:14 2016 +0200
1.3 @@ -770,7 +770,7 @@
1.4 (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of
1.5 (_, fillform, thm, sube_opt) :: _ =>
1.6 let
1.7 - val (pt, pos') = generate_inconsistent_rew (sube_opt, thm'_of_thm thm)
1.8 + val (pt, pos') = generate_inconsistent_rew (sube_opt, thm''_of_thm thm)
1.9 fillform (get_loc pt pos) pos pt
1.10 in
1.11 (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
2.1 --- a/src/Tools/isac/Interpret/Interpret.thy Thu Oct 06 17:03:44 2016 +0200
2.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Mon Oct 10 18:24:14 2016 +0200
2.3 @@ -17,4 +17,7 @@
2.4 ML_file "~~/src/Tools/isac/Interpret/solve.sml"
2.5 ML_file "~~/src/Tools/isac/Interpret/inform.sml"
2.6 ML_file "~~/src/Tools/isac/Interpret/mathengine.sml"
2.7 +ML {*
2.8 +*} ML {*
2.9 +*}
2.10 end
2.11 \ No newline at end of file
3.1 --- a/src/Tools/isac/Interpret/appl.sml Thu Oct 06 17:03:44 2016 +0200
3.2 +++ b/src/Tools/isac/Interpret/appl.sml Mon Oct 10 18:24:14 2016 +0200
3.3 @@ -357,7 +357,7 @@
3.4 | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))
3.5 | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')
3.6
3.7 - | applicable_in (p, p_) pt (m as Rewrite_Inst (subs, thm')) =
3.8 + | applicable_in (p, p_) pt (m as Rewrite_Inst (subs, thm'')) =
3.9 if member op = [Pbl, Met] p_
3.10 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.11 else
3.12 @@ -374,19 +374,20 @@
3.13 let
3.14 val subst = subs2subst thy subs;
3.15 val subs' = subst2subs' subst;
3.16 - in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (assoc_thm' thy thm') f of
3.17 + val thm = assoc_thm'' thy thm''
3.18 + in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst thm f of
3.19 SOME (f',asm) =>
3.20 - Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm', f, (f', asm)))
3.21 - | NONE => Notappl ((fst thm')^" not applicable")
3.22 + Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
3.23 + | NONE => Notappl (fst thm'' ^ " not applicable")
3.24 end
3.25 handle _ => Notappl ("syntax error in "^(subs2str subs))
3.26 end
3.27
3.28 -| applicable_in (p,p_) pt (m as Rewrite thm') =
3.29 +| applicable_in (p,p_) pt (m as Rewrite thm'') =
3.30 if member op = [Pbl,Met] p_
3.31 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.32 else
3.33 - let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt;
3.34 + let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm'' p pt;
3.35 val thy = assoc_thy thy';
3.36 val f = case p_ of
3.37 Frm => get_obj g_form pt p
3.38 @@ -397,16 +398,16 @@
3.39 then
3.40 ((*tracing("### applicable_in rls'= "^rls');*)
3.41 (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f;
3.42 - *)
3.43 - case rewrite_ thy (assoc_rew_ord ro)
3.44 - rls' false (assoc_thm' thy thm') f of
3.45 - SOME (f',asm) => Appl (
3.46 - Rewrite' (thy',ro,rls',(*put_asm*)false,thm', f, (f', asm)))
3.47 - | NONE => Notappl ("'"^(fst thm')^"' not applicable") )
3.48 + *)
3.49 + let val thm = assoc_thm'' thy thm''
3.50 + in case rewrite_ thy (assoc_rew_ord ro) rls' false thm f of
3.51 + SOME (f',asm) => Appl (Rewrite' (thy', ro, rls', false, thm, f, (f', asm)))
3.52 + | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable")
3.53 + end)
3.54 else Notappl msg
3.55 end
3.56
3.57 -| applicable_in (p,p_) pt (m as Rewrite_Asm thm') =
3.58 +| applicable_in (p,p_) pt (m as Rewrite_Asm thm'') =
3.59 if member op = [Pbl,Met] p_
3.60 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
3.61 else
3.62 @@ -417,16 +418,16 @@
3.63 val {rew_ord'=ro',erls=erls,...} =
3.64 get_met (get_obj g_metID pt pp);
3.65 (*val put_asm = true;*)
3.66 - val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
3.67 + val (f, _) = case p_ of
3.68 Frm => (get_obj g_form pt p, p)
3.69 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
3.70 | _ => error ("applicable_in: call by "^
3.71 (pos'2str (p,p_)));
3.72 - in case rewrite_ thy (assoc_rew_ord ro') erls
3.73 - (*put_asm*)false (assoc_thm' thy thm') f of
3.74 + val thm = assoc_thm'' thy thm''
3.75 + in case rewrite_ thy (assoc_rew_ord ro') erls false thm f of
3.76 SOME (f',asm) => Appl (
3.77 - Rewrite' (thy',ro',erls,(*put_asm*)false,thm', f, (f', asm)))
3.78 - | NONE => Notappl ("'"^(fst thm')^"' not applicable") end
3.79 + Rewrite' (thy', ro', erls, false, thm, f, (f', asm)))
3.80 + | NONE => Notappl ("'" ^ fst thm'' ^ "' not applicable") end
3.81
3.82 | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =
3.83 if member op = [Pbl,Met] p_
4.1 --- a/src/Tools/isac/Interpret/ctree.sml Thu Oct 06 17:03:44 2016 +0200
4.2 +++ b/src/Tools/isac/Interpret/ctree.sml Mon Oct 10 18:24:14 2016 +0200
4.3 @@ -297,7 +297,7 @@
4.4
4.5
4.6
4.7 -(*.tactics propagate the construction of the calc-tree;
4.8 +(*.tactics propagate the construction of the calc-tree (as seen by the user);
4.9 there are
4.10 (a) 'specsteps' for the specify-phase, and others for the solve-phase
4.11 (b) those of the solve-phase are 'initac's and others;
4.12 @@ -326,8 +326,7 @@
4.13 | Check_Postcond of pblID
4.14 | Free_Solve
4.15
4.16 -| Rewrite_Inst of ( subs * thm') | Rewrite of thm'
4.17 - | Rewrite_Asm of thm'
4.18 +| Rewrite_Inst of ( subs * thm'') | Rewrite of thm'' | Rewrite_Asm of thm''
4.19 | Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls'
4.20 | Detail_Set_Inst of ( subs * rls') | Detail_Set of rls'
4.21 | End_Detail (*end of script from next_tac,
4.22 @@ -379,10 +378,10 @@
4.23 | Check_Postcond pblID => "Check_Postcond "^(strs2str pblID)
4.24 | Free_Solve => "Free_Solve"
4.25
4.26 - | Rewrite_Inst (subs,thm')=>
4.27 - "Rewrite_Inst "^(pair2str (subs2str subs, spair2str thm'))
4.28 - | Rewrite thm' => "Rewrite "^(spair2str thm')
4.29 - | Rewrite_Asm thm' => "Rewrite_Asm "^(spair2str thm')
4.30 + | Rewrite_Inst (subs, (id, term)) =>
4.31 + "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, term2str term)))
4.32 + | Rewrite (id, term) => "Rewrite " ^ spair2str (id, term2str term)
4.33 + | Rewrite_Asm (id, term) => "Rewrite_Asm " ^ spair2str (id, term2str term)
4.34 | Rewrite_Set_Inst (subs, rls) =>
4.35 "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls))
4.36 | Rewrite_Set rls => "Rewrite_Set "^(quote rls )
4.37 @@ -488,9 +487,9 @@
4.38 (rls, SOME ((subs2subst (assoc_thy "Isac") subs):subst));
4.39
4.40 fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID)
4.41 - | rule2tac _ [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm)
4.42 + | rule2tac _ [] (Thm (thmID, thm)) = Rewrite (thmID, Thm.prop_of thm)
4.43 | rule2tac _ subst (Thm (thmID, thm)) =
4.44 - Rewrite_Inst (subst2subs subst, (thmID, string_of_thmI thm))
4.45 + Rewrite_Inst (subst2subs subst, (thmID, Thm.prop_of thm))
4.46 | rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls)
4.47 | rule2tac _ subst (Rls_ rls) =
4.48 Rewrite_Set_Inst (subst2subs subst, (id_rls rls))
4.49 @@ -559,9 +558,9 @@
4.50 butlast tac is Check_elementwise: take only these asms*)
4.51 | Free_Solve'
4.52 (* context_thy would be simpler if instead thm' woudl be thm *)
4.53 - | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm' * term * (term * term list)
4.54 - | Rewrite' of theory' * rew_ord' * rls * bool * thm' * term * (term * term list)
4.55 - | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' * term * (term * term list)
4.56 + | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm * term * (term * term list)
4.57 + | Rewrite' of theory' * rew_ord' * rls * bool * thm * term * (term * term list)
4.58 + | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm * term * (term * term list)
4.59 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
4.60 | Detail_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
4.61 | Rewrite_Set' of theory' * bool * rls * term * (term * term list)
5.1 --- a/src/Tools/isac/Interpret/generate.sml Thu Oct 06 17:03:44 2016 +0200
5.2 +++ b/src/Tools/isac/Interpret/generate.sml Mon Oct 10 18:24:14 2016 +0200
5.3 @@ -331,17 +331,17 @@
5.4 val (pt,c) = append_result pt p' l tasm Complete;
5.5 in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
5.6
5.7 - | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f', asm))) (is, ctxt) (p,p_) pt =
5.8 + | generate1 thy (Rewrite_Inst' (_,_,_,_,subs', thm, f, (f', asm))) (is, ctxt) (p,p_) pt =
5.9 let
5.10 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
5.11 - (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
5.12 + (Rewrite_Inst (subst2subs subs', (thm''_of_thm thm))) (f', asm) Complete;
5.13 val pt = update_branch pt p TransitiveB
5.14 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
5.15
5.16 - | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) (is, ctxt) (p,p_) pt =
5.17 + | generate1 thy (Rewrite' (thy', ord', rls', pa, thm, f, (f', asm))) (is, ctxt) (p, p_) pt =
5.18 let
5.19 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
5.20 - (Rewrite thm') (f',asm) Complete
5.21 + (Rewrite (thm''_of_thm thm)) (f',asm) Complete
5.22 val pt = update_branch pt p TransitiveB
5.23 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
5.24
6.1 --- a/src/Tools/isac/Interpret/inform.sml Thu Oct 06 17:03:44 2016 +0200
6.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Oct 10 18:24:14 2016 +0200
6.3 @@ -522,8 +522,8 @@
6.4 (*040214: version for concat_deriv*)
6.5 fun rev_deriv' (t, r, (t', a)) = (t', sym_rule r, (t, a));
6.6
6.7 -fun mk_tacis ro erls (t, r as Thm _, (t', a)) =
6.8 - (Rewrite (rule2thm' r),
6.9 +fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) =
6.10 + (Rewrite (id, Thm.prop_of thm),
6.11 Rewrite' ("Isac", fst ro, erls, false, rule2thm' r, t, (t', a)),
6.12 (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
6.13 | mk_tacis ro erls (t, r as Rls_ rls, (t', a)) =
7.1 --- a/src/Tools/isac/Interpret/rewtools.sml Thu Oct 06 17:03:44 2016 +0200
7.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Mon Oct 10 18:24:14 2016 +0200
7.3 @@ -407,10 +407,11 @@
7.4 (* val (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) = tac';
7.5 *)
7.6 fun context_thy (pt, pos as (p,p_)) (tac as Rewrite (thmID,_)) =
7.7 + let val thm = Global_Theory.get_thm (Isac ()) thmID
7.8 + in
7.9 (case applicable_in pos pt tac of
7.10 - Appl (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) =>
7.11 + Appl (Rewrite' (thy', ord', erls, _, thm, f, (res,asm))) =>
7.12 let
7.13 - val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
7.14 val thm_deriv = Thm.get_name_hint thm
7.15 in
7.16 ContThm
7.17 @@ -442,12 +443,14 @@
7.18 thm_rls =
7.19 thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
7.20 applto = f}
7.21 - end)
7.22 + end)
7.23 + end
7.24 | context_thy (pt, pos as (p,p_)) (tac as Rewrite_Inst (subs, (thmID,_))) =
7.25 + let val thm = Global_Theory.get_thm (Isac ()) thmID
7.26 + in
7.27 (case applicable_in pos pt tac of
7.28 - Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), f, (res, asm))) =>
7.29 + Appl (Rewrite_Inst' (thy', ord', erls, _, subst, thm, f, (res, asm))) =>
7.30 let
7.31 - val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
7.32 val thm_deriv = Thm.get_name_hint thm
7.33 val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)
7.34 in
7.35 @@ -486,6 +489,7 @@
7.36 thminst = thminst,
7.37 applto = f}
7.38 end)
7.39 + end
7.40 | context_thy (pt,p) (tac as Rewrite_Set rls') =
7.41 (case applicable_in p pt tac of
7.42 Appl (Rewrite_Set' (thy', _, rls, f, (res,asm))) =>
7.43 @@ -564,12 +568,12 @@
7.44 *)
7.45 fun atomic_appl_tacs thy _ _ f (Calculate scrID) =
7.46 try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' thy scrID |> snd))
7.47 - | atomic_appl_tacs thy ro erls f (Rewrite (thm' as (thmID, _))) =
7.48 + | atomic_appl_tacs thy ro erls f (Rewrite (thm'' as (thmID, _))) =
7.49 try_rew thy (ro, assoc_rew_ord ro) erls [] f
7.50 - (Thm (thmID, assoc_thm' thy thm'))
7.51 - | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm' as (thmID, _))) =
7.52 + (Thm (thmID, assoc_thm'' thy thm''))
7.53 + | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm'' as (thmID, _))) =
7.54 try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f
7.55 - (Thm (thmID, assoc_thm' thy thm'))
7.56 + (Thm (thmID, assoc_thm'' thy thm''))
7.57
7.58 | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') =
7.59 filter_appl_rews thy [] f (assoc_rls rls')
7.60 @@ -636,16 +640,17 @@
7.61 fun guh2rewtac (guh:guh) ([] : subs) =
7.62 let val [isa, thy, sect, xstr] = guh2theID guh
7.63 in case sect of
7.64 - "Theorems" => Rewrite (xstr, "")
7.65 + "Theorems" => Rewrite (xstr, (Thm.prop_of o assoc_thm'' (assoc_thy thy)) (xstr, e_term))
7.66 | "Rulesets" => Rewrite_Set xstr
7.67 | str => error ("guh2rewtac: not impl. for '"^xstr^"'")
7.68 end
7.69 | guh2rewtac (guh:guh) subs =
7.70 let val [isa, thy, sect, xstr] = guh2theID guh
7.71 in case sect of
7.72 - "Theorems" => Rewrite_Inst (subs, (xstr, ""))
7.73 - | "Rulesets" => Rewrite_Set_Inst (subs, xstr)
7.74 - | str => error ("guh2rewtac: not impl. for '"^xstr^"'")
7.75 + "Theorems" =>
7.76 + Rewrite_Inst (subs, (xstr, (Thm.prop_of o assoc_thm'' (assoc_thy thy)) (xstr, e_term)))
7.77 + | "Rulesets" => Rewrite_Set_Inst (subs, xstr)
7.78 + | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'")
7.79 end;
7.80 (*> guh2rewtac "thy_isac_Test-thm-constant_mult_square" [];
7.81 val it = Rewrite ("constant_mult_square", "") : tac
8.1 --- a/src/Tools/isac/Interpret/script.sml Thu Oct 06 17:03:44 2016 +0200
8.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Oct 10 18:24:14 2016 +0200
8.3 @@ -58,7 +58,7 @@
8.4 * pos' list; (*of ptree-nodes probably cut (by fst tac_)*)
8.5 val e_step = (Empty_Tac_, EmptyMout, EmptyPtree, e_pos',[]:pos' list):step;
8.6
8.7 -fun rule2thm' (Thm (id, thm)) = (id, string_of_thmI thm):thm'
8.8 +fun rule2thm' (Thm (_, thm)) = thm
8.9 | rule2thm' r = error ("rule2thm': not defined for "^(rule2str r));
8.10 fun rule2rls' (Rls_ rls) = id_rls rls
8.11 | rule2rls' r = error ("rule2rls': not defined for "^(rule2str r));
8.12 @@ -343,7 +343,7 @@
8.13 fun stac2tac_ pt thy (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ f) =
8.14 let
8.15 val tid = (de_esc_underscore o strip_thy) thmID
8.16 - in (Rewrite (tid, (string_of_thmI o (assoc_thm' thy)) (tid,"")), Empty_Tac_)
8.17 + in (Rewrite (tid, (Thm.prop_of o (assoc_thm'' thy)) (tid, e_term)), Empty_Tac_)
8.18 end
8.19
8.20 | stac2tac_ pt thy (Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thmID,_) $ _ $ f) =
8.21 @@ -351,7 +351,7 @@
8.22 val subML = ((map isapair2pair) o isalist2list) sub
8.23 val subStr = subst2subs subML
8.24 val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)
8.25 - in (Rewrite_Inst (subStr, (tid, (string_of_thmI o (assoc_thm' thy)) (tid,""))), Empty_Tac_)
8.26 + in (Rewrite_Inst (subStr, (tid, (Thm.prop_of o (assoc_thm'' thy)) (tid, e_term))), Empty_Tac_)
8.27 end
8.28
8.29 | stac2tac_ pt thy (Const ("Script.Rewrite'_Set",_) $ Free (rls,_) $ _ $ f) =
8.30 @@ -462,7 +462,9 @@
8.31 AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
8.32 NotAss : e.g. thmID in stac/=/thmID in m (not =)
8.33 *)
8.34 -fun assod pt d (m as Rewrite_Inst' (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) stac =
8.35 +fun assod pt d (m as Rewrite_Inst' (thy', rod, rls, put, subs, thm, f, (f', asm))) stac =
8.36 + let val thmID = (thmID_of_derivation_name o Thm.get_name_hint) thm
8.37 + in
8.38 (case stac of
8.39 (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_) =>
8.40 if thmID = thmID_
8.41 @@ -477,8 +479,10 @@
8.42 if f = f_ then Ass (m,f') else AssWeak (m,f')
8.43 else NotAss
8.44 | _ => NotAss)
8.45 -
8.46 - | assod pt d (m as Rewrite' (thy,rod,rls,put,(thmID,thm),f,(f',asm))) stac =
8.47 + end
8.48 + | assod pt d (m as Rewrite' (thy, rod, rls, put, thm, f, (f', asm))) stac =
8.49 + let val thmID = (thmID_of_derivation_name o Thm.get_name_hint) thm
8.50 + in
8.51 (case stac of
8.52 (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
8.53 ((*tracing ("3### assod: stac = " ^ ter2str t);
8.54 @@ -499,6 +503,7 @@
8.55 if f = f_ then Ass (m,f') else AssWeak (m,f')
8.56 else NotAss
8.57 | _ => NotAss)
8.58 + end
8.59
8.60 | assod pt d (m as Rewrite_Set_Inst' (thy',put,sub,rls,f,(f',asm)))
8.61 (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_) =
8.62 @@ -643,10 +648,10 @@
8.63 | tac_2tac (Specify_Problem' (dI,_)) = Specify_Problem dI
8.64 | tac_2tac (Specify_Method' (dI,_,_)) = Specify_Method dI
8.65
8.66 - | tac_2tac (Rewrite' (thy,rod,erls,put,(thmID,thm),f,(f',asm))) = Rewrite (thmID,thm)
8.67 + | tac_2tac (Rewrite' (_(*thy*), _, _, _, thm, _, _)) = Rewrite (thm''_of_thm thm)
8.68
8.69 - | tac_2tac (Rewrite_Inst' (thy,rod,erls,put,sub,(thmID,thm),f,(f',asm)))=
8.70 - Rewrite_Inst (subst2subs sub,(thmID,thm))
8.71 + | tac_2tac (Rewrite_Inst' (_(*thy*), _, _, _, sub, thm, _, _))=
8.72 + Rewrite_Inst (subst2subs sub, thm''_of_thm thm)
8.73
8.74 | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) = Rewrite_Set (id_rls rls)
8.75 | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) = Detail_Set (id_rls rls)
8.76 @@ -693,8 +698,7 @@
8.77 (*decompose tac_ to a rule and to (lhs,rhs) for ets FIXME.12.03: obsolete!
8.78 NOTE.12.03: also used for msg 'not locatable' ?!: 'Subproblem' missing !!!
8.79 WN0508 only use in tac_2res, which uses only last return-value*)
8.80 -fun rep_tac_ (Rewrite_Inst'
8.81 - (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) =
8.82 +fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, thm, f, (f', _))) =
8.83 let val fT = type_of f;
8.84 val b = if put then @{term True} else @{term False};
8.85 val sT = (type_of o fst o hd) subs;
8.86 @@ -702,7 +706,7 @@
8.87 (map HOLogic.mk_prod subs);
8.88 val sT' = type_of subs';
8.89 val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,(*fT*)bool,fT] ---> fT)
8.90 - $ subs' $ Free (thmID,idT) $ b $ f;
8.91 + $ subs' $ Free (thmID_of_derivation_name' thm, idT) $ b $ f;
8.92 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
8.93 (*Fehlersuche 25.4.01
8.94 (a)----- als String zusammensetzen:
8.95 @@ -745,12 +749,12 @@
8.96 ("Script","tless_true","eval_rls",false,subs,
8.97 ("square_equation_left",""),f,(f',[])));
8.98 *)
8.99 - | rep_tac_ (Rewrite' (thy',rod,rls,put,(thmID,thm),f,(f',asm)))=
8.100 + | rep_tac_ (Rewrite' (thy', _, _, put, thm, f, (f', _)))=
8.101 let
8.102 val fT = type_of f;
8.103 val b = if put then @{term True} else @{term False};
8.104 val lhs = Const ("Script.Rewrite",[idT,HOLogic.boolT,fT] ---> fT)
8.105 - $ Free (thmID,idT) $ b $ f;
8.106 + $ Free (thmID_of_derivation_name' thm, idT) $ b $ f;
8.107 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
8.108 (*
8.109 > val tt = (Thm.term_of o the o (parse thy)) (*____ ____..test*)
8.110 @@ -1179,9 +1183,9 @@
8.111 NOT IMPL. -- "error: do other step before"
8.112 NotLocatable: thus generate_hard
8.113 *)
8.114 -fun locate_gen (thy',g_) (Rewrite'(_,ro,er,pa,(id,str),f,_)) (pt,p)
8.115 +fun locate_gen (thy', g_) (Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p)
8.116 (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) =
8.117 - (case lo rss f (Thm (id, mk_thm (assoc_thy thy') str)) of
8.118 + (case lo rss f (Thm (thmID_of_derivation_name' thm, thm)) of
8.119 [] => NotLocatable
8.120 | rts' =>
8.121 Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
8.122 @@ -1463,7 +1467,7 @@
8.123 NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*)
8.124 | SOME (Thm (id,thm))(*8.6.03: muss auch f' liefern ?!!*) =>
8.125 (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false,
8.126 - (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
8.127 + thm, f, (e_term, [(*!?!8.6.03*)])),
8.128 (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
8.129
8.130 | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Prog (h $ body))
9.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Thu Oct 06 17:03:44 2016 +0200
9.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Mon Oct 10 18:24:14 2016 +0200
9.3 @@ -318,6 +318,11 @@
9.4 handle _ => error ("get_rls_scr: no script for " ^ rls');
9.5
9.6 (*Thm.make_thm added to Pure/thm.ML*)
9.7 +fun mk_thm'' thy t =
9.8 + let val t' = case t of
9.9 + Const ("==>",_) $ _ $ _ => t
9.10 + | _ => Trueprop $ t
9.11 + in Thm.make_thm (Thm.global_cterm_of thy t') end;
9.12 fun mk_thm thy str =
9.13 let val t = (Thm.term_of o the o (parse thy)) str
9.14 val t' = case t of
9.15 @@ -410,6 +415,18 @@
9.16 (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
9.17 identifiers starting with "#" come from Calc and
9.18 get a hand-made theorem (containing numerals only).*)
9.19 +fun assoc_thm'' (thy : theory) ((thmid, term) : thm'') =
9.20 + (case Symbol.explode thmid of
9.21 + "s"::"y"::"m"::"_"::id =>
9.22 + if hd id = "#"
9.23 + then mk_thm'' thy term
9.24 + else ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
9.25 + | id =>
9.26 + if hd id = "#"
9.27 + then mk_thm'' thy term
9.28 + else thmid |> convert_metaview_to_thmid thy |> num_str
9.29 + ) handle _ (*TODO: fin exn behind ERROR: Undefined fact: "add_commute"*) =>
9.30 + error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)")
9.31 fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
9.32 (case Symbol.explode thmid of
9.33 "s"::"y"::"m"::"_"::id =>
10.1 --- a/src/Tools/isac/calcelems.sml Thu Oct 06 17:03:44 2016 +0200
10.2 +++ b/src/Tools/isac/calcelems.sml Mon Oct 10 18:24:14 2016 +0200
10.3 @@ -24,7 +24,7 @@
10.4 thmID : type for data from user input + program
10.5 thmDeriv : type for thy_hierarchy ONLY
10.6 obsolete types : thm' (SEE "ad thm'"), thm''.
10.7 -revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm'_of_thm thm.
10.8 +revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
10.9 activate : thmID_of_derivation_name'
10.10 *)
10.11 type iterID = int;
10.12 @@ -37,7 +37,7 @@
10.13 Thm.get_name_hint survives num_str and seems perfectly reliable *)
10.14
10.15 type thm' = thmID * cterm';(*WN060610 deprecated in favour of thm''*)
10.16 -type thm'' = thmID * term;
10.17 +type thm'' = thmID * term; (* only for transport via libisabelle isac-java <--- ME *)
10.18 type rls' = string;
10.19
10.20 (*.a 'guh'='globally unique handle' is a string unique for each element
10.21 @@ -286,6 +286,7 @@
10.22 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
10.23 fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
10.24 fun thyID_of_derivation_name dn = hd (space_explode "." dn);
10.25 +fun thm''_of_thm thm = (thmID_of_derivation_name' thm, Thm.prop_of thm) : thm''
10.26
10.27 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
10.28 (strip_thy thmid1) = (strip_thy thmid2);
10.29 @@ -309,9 +310,6 @@
10.30 | _ => str
10.31 end
10.32
10.33 -fun thm'_of_thm thm =
10.34 - ((thmID_of_derivation_name o Thm.get_name_hint) thm, string_of_thmI thm): thm'
10.35 -
10.36 (*.id requested for all, Rls,Seq,Rrls.*)
10.37 fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)
10.38 | id_rls (Rls {id,...}) = id
11.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Thu Oct 06 17:03:44 2016 +0200
11.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Mon Oct 10 18:24:14 2016 +0200
11.3 @@ -1,12 +1,8 @@
11.4 -(* convert sml-datatypes to xml
11.5 - authors: Walther Neuper 2003
11.6 +(* convert sml-datatypes to xml for libisabelle and for kbase.
11.7 + authors: Walther Neuper 2003, 2016
11.8 (c) due to copyright terms
11.9 -
11.10 -use"xmlsrc/datatypes.sml";
11.11 -use"datatypes.sml";
11.12 *)
11.13
11.14 -
11.15 signature DATATYPES = (*TODO: redo with xml_of/to *)
11.16 sig
11.17 val authors2xml : int -> string -> string list -> xml
11.18 @@ -59,14 +55,239 @@
11.19 val thmstr2xml : int -> string -> xml
11.20 end
11.21
11.22 -
11.23 -
11.24 (*------------------------------------------------------------------
11.25 structure datatypes:DATATYPES =
11.26 (*structure datatypes =*)
11.27 struct
11.28 ------------------------------------------------------------------*)
11.29
11.30 +(*** convert sml-datatypes to xml for kbase ***)
11.31 +(* NOTE: funs with siblings in xml_of_* are together with them in 'xml for libisabelle' *)
11.32 +
11.33 +val i = indentation;
11.34 +
11.35 +fun id2xml j ids =
11.36 + let fun id2x _ [] = ""
11.37 + | id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
11.38 + (id2x j ss)
11.39 + in (indt j) ^ "<STRINGLIST>\n" ^
11.40 + (id2x (j + indentation) ids) ^
11.41 + (indt j) ^ "</STRINGLIST>\n" end;
11.42 +(* writeln(id2xml 8 ["linear","univariate","equation"]);
11.43 + <STRINGLIST>
11.44 + <STRING>linear</STRING>
11.45 + <STRING>univariate</STRING>
11.46 + <STRING>equation</STRING>
11.47 + </STRINGLIST>*)
11.48 +fun calc2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
11.49 + indt j ^ "<CALC>\n" ^
11.50 + indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
11.51 + indt (j+i) ^ "<GUH>\n" ^ cal2guh ("IsacKnowledge",
11.52 + thyID) scrop ^ "</GUH>\n" ^
11.53 + indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
11.54 + indt j ^ "</CALC>\n" : xml;
11.55 +(*replace by 'fun calc2xml' as developed for thy in 0607*)
11.56 +fun calc2xmlOLD _ ((scr_op, (isa_op, _)):calc) =
11.57 + indt i ^ "<CALCULATE> (" ^ scr_op ^ ", (" ^ isa_op ^ ")) </CALCULATE>\n";
11.58 +fun calcs2xmlOLD _ [] = ("":xml) (*TODO replace with 'strs2xml'*)
11.59 + | calcs2xmlOLD j (r::rs) = calc2xmlOLD j r ^ calcs2xmlOLD j rs;
11.60 +
11.61 +(*.for creating a href for a rule within an rls's rule list;
11.62 + the guh points to the thy of definition of the rule, NOT of use in rls.*)
11.63 +fun rule2xml _ (_ : thyID) Erule =
11.64 + error "rule2xml called with 'Erule'"
11.65 + | rule2xml j _ (Thm (thmDeriv, _)) =
11.66 + indt j ^ "<RULE>\n" ^
11.67 + indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
11.68 + indt (j+i) ^ "<STRING> " ^ thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
11.69 + indt (j+i) ^ "<GUH> " ^
11.70 + thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
11.71 + indt j ^ "</RULE>\n" : xml
11.72 + | rule2xml _ _ (Calc (_(*termop*), _)) = ""
11.73 +(*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
11.74 + see smltest/../datatypes.sml !
11.75 + indt j ^ "<RULE>\n" ^
11.76 + indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^
11.77 + indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop)
11.78 + termop ^ " </GUH>\n" ^
11.79 + indt j ^ "</RULE>\n"
11.80 +*)
11.81 + | rule2xml _ _ (Cal1 (_(*termop*), _)) = ""
11.82 + | rule2xml j thyID (Rls_ rls) =
11.83 + let val rls' = (#id o rep_rls) rls
11.84 + in
11.85 + indt j ^ "<RULE>\n" ^
11.86 + indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
11.87 + indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
11.88 + indt (j+i) ^ "<GUH> " ^ rls2guh (thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
11.89 + indt j ^ "</RULE>\n"
11.90 + end;
11.91 +fun rules2xml _ _ [] = ("":xml)
11.92 + | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;
11.93 +
11.94 +fun filterpbl str =
11.95 + let fun filt [] = []
11.96 + | filt ((s, (t1, t2)) :: ps) =
11.97 + if str = s then (t1 $ t2) :: filt ps else filt ps
11.98 + in filt end;
11.99 +fun pattern2xml j p where_ =
11.100 + (case filterpbl "#Given" p of
11.101 + [] => (indt j) ^ "<GIVEN> </GIVEN>\n"
11.102 +(* val gis = filterpbl "#Given" p;
11.103 + *)
11.104 + | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^
11.105 + (indt j) ^ "</GIVEN>\n")
11.106 + ^
11.107 + (case where_ of
11.108 + [] => (indt j) ^ "<WHERE> </WHERE>\n"
11.109 + | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^
11.110 + (indt j) ^ "</WHERE>\n")
11.111 + ^
11.112 + (case filterpbl "#Find" p of
11.113 + [] => (indt j) ^ "<FIND> </FIND>\n"
11.114 + | fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^
11.115 + (indt j) ^ "</FIND>\n")
11.116 + ^
11.117 + (case filterpbl "#Relate" p of
11.118 + [] => (indt j) ^ "<RELATE> </RELATE>\n"
11.119 + | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
11.120 + (indt j) ^ "</RELATE>\n");
11.121 +(*
11.122 +writeln(pattern2xml 3 ((#ppc o get_pbt)
11.123 + ["squareroot","univariate","equation","test"]) []);
11.124 + *)
11.125 +
11.126 +(*url to a source external to isac*)
11.127 +fun extref2xml j linktext url =
11.128 + indt j ^ "<EXTREF>\n" ^
11.129 + indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^
11.130 + indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
11.131 + indt j ^ "</EXTREF>\n" : xml;
11.132 +fun theref2xml j (thyID:thyID) typ (xstring:xstring) =
11.133 + let val guh = theID2guh ["IsacKnowledge", thyID, typ, xstring]
11.134 + val typ' = (implode o (drop_last_n 1) o Symbol.explode) typ
11.135 + in indt j ^ "<KESTOREREF>\n" ^
11.136 + indt (j+i) ^ "<TAG> " ^ typ' ^ " </TAG>\n" ^
11.137 + indt (j+i) ^ "<ID> " ^ xstring ^ " </ID>\n" ^
11.138 + indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
11.139 + indt j ^ "</KESTOREREF>\n" : xml
11.140 + end;
11.141 +fun keref2xml j typ (kestoreID:kestoreID) =
11.142 + let val id = strs2str' kestoreID
11.143 + val guh = kestoreID2guh typ kestoreID
11.144 + in indt j ^ "<KESTOREREF>\n" ^
11.145 + indt (j+i) ^ "<TAG> " ^ ketype2str' typ ^ "</TAG>\n" ^
11.146 + indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^
11.147 + indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
11.148 + indt j ^ "</KESTOREREF>\n" : xml
11.149 + end;
11.150 +fun authors2xml j str auts =
11.151 + let fun autx _ [] = ""
11.152 + | autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
11.153 + (autx j ss)
11.154 + in indt j ^ "<"^str^">\n" ^
11.155 + autx (j + i) auts ^
11.156 + indt j ^ "</"^str^">\n" : xml
11.157 + end;
11.158 +(* writeln(authors2xml 2 "MATHAUTHORS" []);
11.159 + writeln(authors2xml 2 "MATHAUTHORS"
11.160 + ["isac-team 2001", "Richard Lang 2003"]);
11.161 + *)
11.162 +fun scr2xml j EmptyScr =
11.163 + indt j ^"<SCRIPT> </SCRIPT>\n" : xml
11.164 + | scr2xml j (Prog term) =
11.165 + if term = e_term
11.166 + then indt j ^"<SCRIPT> </SCRIPT>\n"
11.167 + else indt j ^"<SCRIPT>\n"^
11.168 + term2xml j (inst_abs (assoc_thy "Isac") term) ^ "\n" ^
11.169 + indt j ^"</SCRIPT>\n"
11.170 + | scr2xml j (Rfuns _) =
11.171 + indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
11.172 +
11.173 +fun calcref2xml j (thyID:thyID, (scrop, (_(*rewop*), _)):calc) =
11.174 + indt j ^ "<CALCREF>\n" ^
11.175 + indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
11.176 + indt (j+i) ^ "<GUH> " ^ cal2guh ("IsacKnowledge",
11.177 + thyID) scrop ^ " </GUH>\n" ^
11.178 + indt j ^ "</CALCREF>\n" : xml;
11.179 +fun calcrefs2xml _ (_,[]) = "":xml
11.180 + | calcrefs2xml j (thyID, cal::cs) =
11.181 + calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);
11.182 +
11.183 +fun prepa12xml j (terms, term) =
11.184 + indt j ^"<PREPAT>\n"^
11.185 + indt (j+i) ^"<PRECONDS>\n"^
11.186 + terms2xml (j+2*i) terms ^
11.187 + indt (j+i) ^"</PRECONDS>\n"^
11.188 + indt (j+i) ^"<PATTERN>\n"^
11.189 + term2xml (j+2*i) term ^
11.190 + indt (j+i) ^"</PATTERN>\n"^
11.191 + indt j ^"</PREPAT>\n" : xml;
11.192 +fun prepat2xml _ [] = ""
11.193 + | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps : xml;
11.194 +
11.195 +fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
11.196 + srls, calc, rules, errpatts, scr}) =
11.197 + indt j ^"<RULESET>\n"^
11.198 + indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
11.199 + indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^
11.200 + indt (j+i) ^"<RULES>\n" ^
11.201 + rules2xml (j+2*i) thyID rules ^
11.202 + indt (j+i) ^"</RULES>\n" ^
11.203 + indt (j+i) ^"<PRECONDS> " ^
11.204 + terms2xml' (j+2*i) preconds ^
11.205 + indt (j+i) ^"</PRECONDS>\n" ^
11.206 + indt (j+i) ^"<ORDER>\n" ^
11.207 + indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
11.208 +(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
11.209 + indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
11.210 + thyID) ord ^ " </GUH>\n" ^
11.211 +..................................................................*)
11.212 + indt (j+i) ^"</ORDER>\n" ^
11.213 + indt (j+i) ^"<ERLS>\n" ^
11.214 + indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
11.215 + indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
11.216 + indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
11.217 + (id_rls erls) ^ " </GUH>\n" ^
11.218 + indt (j+i) ^"</ERLS>\n" ^
11.219 + indt (j+i) ^"<SRLS>\n" ^
11.220 + indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
11.221 + indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
11.222 + indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
11.223 + (id_rls srls) ^ " </GUH>\n" ^
11.224 + indt (j+i) ^"</SRLS>\n" ^
11.225 + calcrefs2xml (j+i) (thyID, calc) ^
11.226 + scr2xml (j+i) scr ^
11.227 + indt j ^"</RULESET>\n" : xml;
11.228 +fun rls2xml j (thyID, Erls) = rls2xml j (thyID, e_rls)
11.229 + | rls2xml j (thyID, Rls data) = rls2xm j (thyID, "Rls", data)
11.230 + | rls2xml j (thyID, Seq data) = rls2xm j (thyID, "Seq", data)
11.231 + | rls2xml j (thyID, Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) =
11.232 + indt j ^"<RULESET>\n"^
11.233 + indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
11.234 + indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^
11.235 + prepat2xml (j+i) prepat ^
11.236 + indt (j+i) ^"<ORDER> " ^
11.237 + indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^
11.238 + indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
11.239 +(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
11.240 + indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
11.241 + thyID) ord ^ " </GUH>\n" ^
11.242 +.................................................................*)
11.243 + indt (j+i) ^"</ORDER>\n" ^
11.244 + indt (j+i) ^"<ERLS> " ^
11.245 + indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
11.246 + indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
11.247 + indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) (id_rls erls) ^ " </GUH>\n" ^
11.248 + indt (j+i) ^"</ERLS>\n" ^
11.249 + calcrefs2xml (j+i) (thyID, calc) ^
11.250 + indt (j+i) ^"<SCRIPT>\n"^
11.251 + scr2xml (j+2*i) scr ^
11.252 + indt (j+i) ^" </SCRIPT>\n"^
11.253 + indt j ^"</RULESET>\n" : xml;
11.254 +
11.255 +(*** convert sml-datatypes to xml for libisabelle ***)
11.256 +
11.257 (** general types: lists, **)
11.258
11.259 fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])
11.260 @@ -85,7 +306,7 @@
11.261 | xml_to_strs tree = raise ERROR ("xml_to_strs: wrong XML.tree \n" ^ xmlstr 0 tree)
11.262
11.263 fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])
11.264 -fun xml_of_ints is = (*xml/datatypes.sml: fun ints2xml*)
11.265 +fun xml_of_ints is =
11.266 XML.Elem (("INTLIST", []), map xml_of_int is)
11.267
11.268 fun xml_to_int (XML.Elem (("INT", []), [XML.Text i])) =
11.269 @@ -94,7 +315,6 @@
11.270 fun xml_to_ints (XML.Elem (("INTLIST", []), is)) = map xml_to_int is
11.271 | xml_to_ints tree = raise ERROR ("xml_to_ints: wrong XML.tree \n" ^ xmlstr 0 tree)
11.272
11.273 -
11.274 (** isac datatypes **)
11.275 fun xml_of_pos tag (is, pp) =
11.276 XML.Elem ((tag, []), [
11.277 @@ -140,7 +360,7 @@
11.278 XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (comp_dts' dts)])
11.279 | xml_of_itm_ (Mis (d, pid)) =
11.280 XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])
11.281 -
11.282 + | xml_of_itm_ _ = error "xml_of_itm_: wrong argument"
11.283 fun xml_of_itms itms =
11.284 let
11.285 fun extract (_, _, _, _, itm_) = itm_
11.286 @@ -247,22 +467,33 @@
11.287 xml_var_val_pairs)) = subst2sube (map xml_to_sub xml_var_val_pairs)
11.288 | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
11.289
11.290 +fun thm''2xml j (thm : thm) =
11.291 + indt j ^ "<THEOREM>\n" ^
11.292 + indt (j+i) ^ "<ID> " ^ thmID_of_derivation_name' thm ^ " </ID>\n"^
11.293 + term2xml j (Thm.prop_of thm) ^ "\n" ^
11.294 + indt j ^ "</THEOREM>\n" : xml;
11.295 fun xml_of_thm' ((ID, form) : thm') =
11.296 XML.Elem (("THEOREM", []), [
11.297 XML.Elem (("ID", []), [XML.Text ID]),
11.298 XML.Elem (("FORMULA", []), [
11.299 XML.Text form])]) (* repair for MathML: use term instead String *)
11.300 +(* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *)
11.301 +fun xml_of_thm'' ((ID, term) : thm'') =
11.302 + XML.Elem (("THEOREM", []), [
11.303 + XML.Elem (("ID", []), [XML.Text ID]),
11.304 + xml_of_term_NEW term])
11.305 fun xml_to_thm'
11.306 (XML.Elem (("THEOREM", []), [
11.307 XML.Elem (("ID", []), [XML.Text ID]),
11.308 XML.Elem (("FORMULA", []), [(* repair for MathML: use term instead String *)
11.309 XML.Text form])])) = ((ID, form) : thm')
11.310 | xml_to_thm' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
11.311 -
11.312 -fun xml_of_thm (thm : thm) =
11.313 - XML.Elem (("THEOREM", []), [
11.314 - XML.Elem (("ID", []), [XML.Text (thmID_of_derivation_name' thm)]),
11.315 - xml_of_term (Thm.prop_of thm)])
11.316 +(* at the front-end theorems are identified only by their name, so NO isac-java \<longrightarrow> ME *)
11.317 +fun xml_to_thm''
11.318 + (XML.Elem (("THEOREM", []), [
11.319 + XML.Elem (("ID", []), [XML.Text ID])])) =
11.320 + (ID, Thm.prop_of (Global_Theory.get_thm (Isac ()) ID)) : thm''
11.321 + | xml_to_thm'' x = raise ERROR ("xml_to_thm'' wrong arg:" ^ xmlstr 0 x)
11.322
11.323 fun xml_of_src EmptyScr =
11.324 XML.Elem (("NOCODE", []), [XML.Text "empty"])
11.325 @@ -282,12 +513,12 @@
11.326 (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
11.327 XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
11.328 (*----- Rewrite* -----------------------------------------------------*)
11.329 - | xml_of_tac (Rewrite thm') =
11.330 - XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm' thm'])
11.331 - | xml_of_tac (Rewrite_Inst (subs, thm')) =
11.332 + | xml_of_tac (Rewrite thm'') =
11.333 + XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm'' thm''])
11.334 + | xml_of_tac (Rewrite_Inst (subs, thm'')) =
11.335 XML.Elem (("REWRITEINSTTACTIC", [("name", "Rewrite_Inst")]), (
11.336 xml_of_subs subs ::
11.337 - xml_of_thm' thm' :: []))
11.338 + xml_of_thm'' thm'' :: []))
11.339 | xml_of_tac (Rewrite_Set rls') =
11.340 XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])
11.341 | xml_of_tac (Rewrite_Set_Inst (subs, rls')) =
11.342 @@ -338,11 +569,11 @@
11.343 (*----- Rewrite* -----------------------------------------------------*)
11.344 | xml_to_tac
11.345 (XML.Elem (("REWRITETACTIC", [
11.346 - ("name", "Rewrite")]), [thm'])) = Rewrite (xml_to_thm' thm')
11.347 + ("name", "Rewrite")]), [thm])) = Rewrite (xml_to_thm'' thm)
11.348 | xml_to_tac
11.349 (XML.Elem (("REWRITEINSTTACTIC", [
11.350 ("name", "Rewrite_Inst")]), [
11.351 - subs, thm'])) = Rewrite_Inst (xml_to_subs subs, xml_to_thm' thm')
11.352 + subs, thm])) = Rewrite_Inst (xml_to_subs subs, xml_to_thm'' thm)
11.353 | xml_to_tac
11.354 (XML.Elem (("REWRITESETTACTIC", [
11.355 ("name", "Rewrite_Set")]), [XML.Text rls'])) = Rewrite_Set (rls')
12.1 --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Thu Oct 06 17:03:44 2016 +0200
12.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Mon Oct 10 18:24:14 2016 +0200
12.3 @@ -1,5 +1,5 @@
12.4 (* export problem-data and method-data to xml
12.5 - author: Walther Neuper
12.6 + author: Walther Neuper 2004
12.7 (c) isac-team
12.8 *)
12.9
12.10 @@ -29,8 +29,6 @@
12.11 val it = "linear_univariate_equation.xml" : string
12.12 *)
12.13
12.14 -
12.15 -
12.16 (*ad DTD: a NODE contains an ID and zero or more NODEs*)
12.17 (*old version with pos2filename*)
12.18 fun hierarchy pm(*"pbl" | "met"*) h =
12.19 @@ -103,72 +101,19 @@
12.20 (hierarchy_met (get_mets ())) ^
12.21 "</NODE>");
12.22
12.23 -
12.24 -
12.25 (**.create the xml-files for the pbls, mets from the hierarchy.**)
12.26
12.27 -val i = indentation;
12.28 -
12.29 +(*.format a problem in xml for presentation on the problem browser;
12.30 + new version with <KESTOREREF>s -- not used because linking
12.31 + requires elements (rls, calc, ...) to be reorganized.*)
12.32 +(*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
12.33 fun pbl2term thy (pblRD:pblRD) = (*WN120405.TODO.txt*)
12.34 str2term ("Problem (" ^ (get_thy o theory2domID) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")");
12.35 (* term2str (pbl2term (Thy_Info.get_theory "Isac") ["equations","univariate","normalize"]);
12.36 val it = "Problem (Isac, [normalize, univariate, equations])" : string
12.37 *)
12.38 +val i = indentation;
12.39
12.40 -(*.a reference to an element in the kestore EXCEPT theory hierarchy;
12.41 - compare 'fun theref2xml'.*)
12.42 -fun keref2xml j typ (kestoreID:kestoreID) =
12.43 - let val id = strs2str' kestoreID
12.44 - val guh = kestoreID2guh typ kestoreID
12.45 - in indt j ^ "<KESTOREREF>\n" ^
12.46 - indt (j+i) ^ "<TAG> " ^ ketype2str' typ ^ "</TAG>\n" ^
12.47 - indt (j+i) ^ "<ID> " ^ id ^ " </ID>\n" ^
12.48 - indt (j+i) ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
12.49 - indt j ^ "</KESTOREREF>\n" : xml
12.50 - end;
12.51 -
12.52 -fun pattern2xml j p where_ =
12.53 - (case filterpbl "#Given" p of
12.54 - [] => (indt j) ^ "<GIVEN> </GIVEN>\n"
12.55 -(* val gis = filterpbl "#Given" p;
12.56 - *)
12.57 - | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^
12.58 - (indt j) ^ "</GIVEN>\n")
12.59 - ^
12.60 - (case where_ of
12.61 - [] => (indt j) ^ "<WHERE> </WHERE>\n"
12.62 - | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^
12.63 - (indt j) ^ "</WHERE>\n")
12.64 - ^
12.65 - (case filterpbl "#Find" p of
12.66 - [] => (indt j) ^ "<FIND> </FIND>\n"
12.67 - | fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^
12.68 - (indt j) ^ "</FIND>\n")
12.69 - ^
12.70 - (case filterpbl "#Relate" p of
12.71 - [] => (indt j) ^ "<RELATE> </RELATE>\n"
12.72 - | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^
12.73 - (indt j) ^ "</RELATE>\n");
12.74 -
12.75 -fun authors2xml j str auts =
12.76 - let fun autx _ [] = ""
12.77 - | autx j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
12.78 - (autx j ss)
12.79 - in indt j ^ "<"^str^">\n" ^
12.80 - autx (j + i) auts ^
12.81 - indt j ^ "</"^str^">\n" : xml
12.82 - end;
12.83 -fun id2xml j ids =
12.84 - let fun id2x _ [] = ""
12.85 - | id2x j (s::ss) = (indt j) ^ "<STRING> " ^ s ^ " </STRING>\n" ^
12.86 - (id2x j ss)
12.87 - in (indt j) ^ "<STRINGLIST>\n" ^
12.88 - (id2x (j + indentation) ids) ^
12.89 - (indt j) ^ "</STRINGLIST>\n" end;
12.90 -(*.format a problem in xml for presentation on the problem browser;
12.91 - new version with <KESTOREREF>s -- not used because linking
12.92 - requires elements (rls, calc, ...) to be reorganized.*)
12.93 -(*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
12.94 fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
12.95 thy,where_}:pbt) =
12.96 let val thy' = theory2theory' thy
12.97 @@ -203,107 +148,16 @@
12.98 "</NODECONTENT>" : xml
12.99 end;
12.100
12.101 -(*.format a problem in xml for presentation on the problem browser;
12.102 - old version with 'dead' strings for rls, calc, ....*)
12.103 -(*
12.104 -val pblID = ["linear","univariate","equation"];
12.105 -val pblID = ["degree_4","polynomial","univariate","equation"];
12.106 -val pblID = rev ["tool","find_values"];
12.107 -val (id, {guh,mathauthors,init,cas,met,ppc,prls,thy,where_}:pbt) =
12.108 - (pblID, get_pbt pblID);
12.109 - *)
12.110 -fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
12.111 - thy,where_}:pbt) =
12.112 - "<NODECONTENT>\n" ^
12.113 - indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
12.114 - (((id2xml i)(* o rev*)) id) ^
12.115 - indt i ^ "<META> </META>\n" ^
12.116 - (*--------------- begin display ------------------------------*)
12.117 - indt i ^ "<HEADLINE>\n" ^
12.118 - (case cas of NONE => term2xml i (pbl2term thy id)
12.119 - | SOME t => term2xml i t) ^ "\n" ^
12.120 - indt i ^ "</HEADLINE>\n" ^
12.121 - (*--------------- hline --------------------------------------*)
12.122 - pattern2xml i ppc where_ ^
12.123 - (*--------------- hline --------------------------------------*)
12.124 - indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n"
12.125 - (*--------------- end display --------------------------------*)
12.126 - ^
12.127 - indt i ^ "<THEORY>\n" ^
12.128 - theref2xml (i+i) (theory2theory' thy) "Theorems" "" ^
12.129 - indt i ^ "</THEORY>\n" ^
12.130 - (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
12.131 - | _ => (indt i) ^ "<METHODS>\n" ^
12.132 - foldl op^ ("", map (keref2xml (i+i) Met_) met) ^
12.133 - (indt i) ^ "</METHODS>\n") ^
12.134 - indt i ^ "<EVALPRECOND> " ^ (#id o rep_rls)
12.135 - prls ^ " </EVALPRECOND>\n" ^
12.136 - authors2xml i "MATHAUTHORS" mathauthors ^
12.137 - authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
12.138 - "</NODECONTENT>" : xml;
12.139 -(*
12.140 -val pblID = ["linear","univariate","equation"];
12.141 -val pblID = ["degree_4","polynomial","univariate","equation"];
12.142 -writeln (pbl2xml pblID (get_pbt pblID));
12.143 -*)
12.144 -
12.145 -(*replace by 'fun calc2xml' as developed for thy in 0607*)
12.146 -fun calc2xmlOLD j ((scr_op, (isa_op, _)):calc) =
12.147 - indt i ^ "<CALCULATE> (" ^ scr_op ^ ", (" ^ isa_op ^ ")) </CALCULATE>\n";
12.148 -fun calcs2xmlOLD j [] = ("":xml) (*TODO replace with 'strs2xml'*)
12.149 - | calcs2xmlOLD j (r::rs) = calc2xmlOLD j r ^ calcs2xmlOLD j rs;
12.150 -
12.151 -fun scr2xml j EmptyScr =
12.152 - indt j ^"<SCRIPT> </SCRIPT>\n" : xml
12.153 - | scr2xml j (Prog term) =
12.154 - if term = e_term
12.155 - then indt j ^"<SCRIPT> </SCRIPT>\n"
12.156 - else indt j ^"<SCRIPT>\n"^
12.157 - term2xml j (inst_abs (assoc_thy "Isac") term) ^ "\n" ^
12.158 - indt j ^"</SCRIPT>\n"
12.159 - | scr2xml j (Rfuns _) =
12.160 - indt j ^"<REVERSREWRITE> reverse rewrite functions </REVERSREWRITE>\n";
12.161 -
12.162 +(**. write pbls from hierarchy to files.**)
12.163 +fun pbl2file (path:path) (pos:pos) (id:metID) (pbl as {guh,...}) =
12.164 + (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ pos2str pos);
12.165 + ((str2file (path ^ guh2filename guh)) o (pbl2xml id)) pbl
12.166 + );
12.167 +
12.168 +(**. write mets from hierarchy to files.**)
12.169 (*.format a method in xml for presentation on the method browser;
12.170 new version with <KESTOREREF>s -- not used because linking
12.171 requires elements (rls, calc, ...) to be reorganized.*)
12.172 -(*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
12.173 -fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
12.174 - crls,erls,errpats,nrls,prls,srls,rew_ord'}:met) =
12.175 - let val thy' = "Isac" (*FIXME.WN0607 get thy from met ?!?*)
12.176 - val crls' = (#id o rep_rls) crls
12.177 - val erls' = (#id o rep_rls) erls
12.178 - val nrls' = (#id o rep_rls) nrls
12.179 - val prls' = (#id o rep_rls) prls
12.180 - val srls' = (#id o rep_rls) srls
12.181 - in "<NODECONTENT>\n" ^
12.182 - indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
12.183 - id2xml i id ^
12.184 - indt i ^ "<META> </META>\n" ^
12.185 - scr2xml i scr ^
12.186 - pattern2xml i ppc pre ^
12.187 - indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
12.188 - indt i ^ "<EVALPRECOND>\n" ^
12.189 - theref2xml (i+i) (snd (thy_containing_rls thy' prls')) "Rulesets" prls'^
12.190 - indt i ^ "</EVALPRECOND>\n" ^
12.191 - indt i ^ "<EVALCOND>\n" ^
12.192 - theref2xml (i+i) (snd (thy_containing_rls thy' erls')) "Rulesets" erls'^
12.193 - indt i ^ "</EVALCOND>\n" ^
12.194 - indt i ^ "<EVALLISTEXPR>\n"^
12.195 - theref2xml (i+i) (snd (thy_containing_rls thy' srls')) "Rulesets" srls'^
12.196 - indt i ^ "</EVALLISTEXPR>\n" ^
12.197 - indt i ^ "<CHECKELEMENTWISE>\n" ^
12.198 - theref2xml (i+i) (snd (thy_containing_rls thy' crls')) "Rulesets" crls'^
12.199 - indt i ^ "</CHECKELEMENTWISE>\n" ^
12.200 - indt i ^ "<NORMALFORM>\n" ^
12.201 - theref2xml (i+i) (snd (thy_containing_rls thy' nrls')) "Rulesets" nrls'^
12.202 - indt i ^ "</NORMALFORM>\n" ^
12.203 - indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
12.204 - calcs2xmlOLD i calc ^
12.205 - authors2xml i "MATHAUTHORS" mathauthors ^
12.206 - authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
12.207 - "</NODECONTENT>" : xml
12.208 - end;
12.209 (*.format a method in xml for presentation on the method browser;
12.210 old version with 'dead' strings for rls, calc, ....*)
12.211 fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
12.212 @@ -326,28 +180,10 @@
12.213 authors2xml i "MATHAUTHORS" mathauthors ^
12.214 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
12.215 "</NODECONTENT>" : xml;
12.216 -
12.217 (* writeln (met2xml ["Test", "solve_linear"]
12.218 (get_met ["Test", "solve_linear"]));
12.219 *)
12.220
12.221 -(**. write pbls from hierarchy to files.**)
12.222 -
12.223 -(*.write the files using an int-key (pos') as filename.*)
12.224 -fun pbl2file (path:path) (pos:pos) (id:metID) (pbl as {guh,...}) =
12.225 - (writeln ("### pbl2file: id = " ^ strs2str id);
12.226 - ((str2file (path ^ pos2filename pos)) o (pbl2xml id)) pbl
12.227 - );
12.228 -
12.229 -(*.write the files using the guh as filename.*)
12.230 -(* *)
12.231 -fun pbl2file (path:path) (pos:pos) (id:metID) (pbl as {guh,...}) =
12.232 - (writeln ("### pbl2file: id = " ^ strs2str id ^ ", pos = " ^ pos2str pos);
12.233 - ((str2file (path ^ guh2filename guh)) o (pbl2xml id)) pbl
12.234 - );
12.235 -
12.236 -(**. write mets from hierarchy to files.**)
12.237 -
12.238 (*.write the files using an int-key (pos') as filename.*)
12.239 fun met2file (path:path) (pos:pos) (id:metID) met =
12.240 (writeln ("### met2file: id = " ^ strs2str id);
12.241 @@ -358,7 +194,6 @@
12.242 (writeln ("### met2file: id = " ^ strs2str id);
12.243 ((str2file (path ^ guh2filename guh)) o (met2xml id)) met);
12.244
12.245 -
12.246 (*.scan the mtree Ptyp and print the nodes using wfn.*)
12.247 fun node (pa:path) ids po wfn (Ptyp (id,[n],ns)) =
12.248 let val po' = lev_on po
12.249 @@ -370,7 +205,6 @@
12.250 | nodes pa ids po wfn (n::ns) =
12.251 (node pa ids po wfn n; nodes pa ids (lev_on po) wfn ns);
12.252
12.253 -
12.254 fun pbls2file (p:path) = nodes p [] [0] pbl2file (get_ptyps ());
12.255 fun mets2file (p:path) = nodes p [] [0] met2file (get_mets ());
12.256 (*
13.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Oct 06 17:03:44 2016 +0200
13.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Mon Oct 10 18:24:14 2016 +0200
13.3 @@ -118,145 +118,6 @@
13.4 (hierarchy_guh (get_thes ())) ^
13.5 "</NODE>");
13.6
13.7 -(*url to a source external to isac*)
13.8 -fun extref2xml j linktext url =
13.9 - indt j ^ "<EXTREF>\n" ^
13.10 - indt (j+i) ^ "<TEXT> " ^ linktext ^ " </TEXT>\n" ^
13.11 - indt (j+i) ^ "<URL> " ^ url ^ " </URL>\n" ^
13.12 - indt j ^ "</EXTREF>\n" : xml;
13.13 -
13.14 -(*.for creating a href for a rule within an rls's rule list;
13.15 - the guh points to the thy of definition of the rule, NOT of use in rls.*)
13.16 -fun rule2xml j (thyID:thyID) Erule =
13.17 - error "rule2xml called with 'Erule'"
13.18 - | rule2xml j thyID (Thm (thmDeriv, thm)) =
13.19 - indt j ^ "<RULE>\n" ^
13.20 - indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
13.21 - indt (j+i) ^ "<STRING> " ^ thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
13.22 - indt (j+i) ^ "<GUH> " ^
13.23 - thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
13.24 - indt j ^ "</RULE>\n" : xml
13.25 - | rule2xml j thyID (Calc (termop, _)) = ""
13.26 -(*FIXXXXXXXME.WN060714 in rls make Calc : calc -> rule [add scriptop!]
13.27 - see smltest/../datatypes.sml !
13.28 - indt j ^ "<RULE>\n" ^
13.29 - indt (j+i) ^ "<STRING> " ^ termop ^ " </STRING>\n" ^
13.30 - indt (j+i) ^ "<GUH> " ^ cal2guh (thy_containing_cal thyID termop)
13.31 - termop ^ " </GUH>\n" ^
13.32 - indt j ^ "</RULE>\n"
13.33 -*)
13.34 - | rule2xml j thyID (Cal1 (termop, _)) = ""
13.35 - | rule2xml j thyID (Rls_ rls) =
13.36 - let val rls' = (#id o rep_rls) rls
13.37 - in
13.38 - indt j ^ "<RULE>\n" ^
13.39 - indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
13.40 - indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
13.41 - indt (j+i) ^ "<GUH> " ^ rls2guh (thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
13.42 - indt j ^ "</RULE>\n"
13.43 - end;
13.44 -
13.45 -fun calcref2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
13.46 - indt j ^ "<CALCREF>\n" ^
13.47 - indt (j+i) ^ "<STRING> " ^ scrop ^ "</STRING>\n" ^
13.48 - indt (j+i) ^ "<GUH> " ^ cal2guh ("IsacKnowledge",
13.49 - thyID) scrop ^ " </GUH>\n" ^
13.50 - indt j ^ "</CALCREF>\n" : xml;
13.51 -fun calcrefs2xml _ (_,[]) = "":xml
13.52 - | calcrefs2xml j (thyID, cal::cs) =
13.53 - calcref2xml j (thyID, cal) ^ calcrefs2xml j (thyID, cs);
13.54 -
13.55 -fun rules2xml j thyID [] = ("":xml)
13.56 - | rules2xml j thyID (r::rs) = rule2xml j thyID r ^ rules2xml j thyID rs;
13.57 -fun rls2xm j (thyID, seqrls, {id, preconds, rew_ord=(ord,_), erls,
13.58 - srls, calc, rules, errpatts, scr}) =
13.59 - indt j ^"<RULESET>\n"^
13.60 - indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
13.61 - indt (j+i) ^"<TYPE> "^ seqrls ^" </TYPE>\n"^
13.62 - indt (j+i) ^"<RULES>\n" ^
13.63 - rules2xml (j+2*i) thyID rules ^
13.64 - indt (j+i) ^"</RULES>\n" ^
13.65 - indt (j+i) ^"<PRECONDS> " ^
13.66 - terms2xml' (j+2*i) preconds ^
13.67 - indt (j+i) ^"</PRECONDS>\n" ^
13.68 - indt (j+i) ^"<ORDER>\n" ^
13.69 - indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
13.70 -(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
13.71 - indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
13.72 - thyID) ord ^ " </GUH>\n" ^
13.73 -..................................................................*)
13.74 - indt (j+i) ^"</ORDER>\n" ^
13.75 - indt (j+i) ^"<ERLS>\n" ^
13.76 - indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
13.77 - indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
13.78 - indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
13.79 - (id_rls erls) ^ " </GUH>\n" ^
13.80 - indt (j+i) ^"</ERLS>\n" ^
13.81 - indt (j+i) ^"<SRLS>\n" ^
13.82 - indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
13.83 - indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
13.84 - indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID)
13.85 - (id_rls srls) ^ " </GUH>\n" ^
13.86 - indt (j+i) ^"</SRLS>\n" ^
13.87 - calcrefs2xml (j+i) (thyID, calc) ^
13.88 - scr2xml (j+i) scr ^
13.89 - indt j ^"</RULESET>\n" : xml;
13.90 -
13.91 -fun prepa12xml j (terms, term) =
13.92 - indt j ^"<PREPAT>\n"^
13.93 - indt (j+i) ^"<PRECONDS>\n"^
13.94 - terms2xml (j+2*i) terms ^
13.95 - indt (j+i) ^"</PRECONDS>\n"^
13.96 - indt (j+i) ^"<PATTERN>\n"^
13.97 - term2xml (j+2*i) term ^
13.98 - indt (j+i) ^"</PATTERN>\n"^
13.99 - indt j ^"</PREPAT>\n" : xml;
13.100 -
13.101 -fun prepat2xml j [] = ""
13.102 - | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps : xml;
13.103 -
13.104 -fun rls2xml j (thyID, Erls) = rls2xml j (thyID, e_rls)
13.105 - | rls2xml j (thyID, Rls data) = rls2xm j (thyID, "Rls", data)
13.106 - | rls2xml j (thyID, Seq data) = rls2xm j (thyID, "Seq", data)
13.107 - | rls2xml j (thyID, Rrls {id, prepat, rew_ord=(ord,_), erls, calc, errpatts, scr}) =
13.108 - indt j ^"<RULESET>\n"^
13.109 - indt (j+i) ^"<ID> "^ id ^" </ID>\n"^
13.110 - indt (j+i) ^"<TYPE> Rrls </TYPE>\n"^
13.111 - prepat2xml (j+i) prepat ^
13.112 - indt (j+i) ^"<ORDER> " ^
13.113 - indt (j+2*i) ^ "<TAG> Rewrite order </TAG>\n" ^
13.114 - indt (j+2*i) ^ "<STRING> " ^ ord ^ " </STRING>\n" ^
13.115 -(*WN060714 thy_isac_*-ord-*.xml not yet generated ................
13.116 - indt (j+2*i) ^ "<GUH> " ^ ord2guh ("IsacKnowledge",
13.117 - thyID) ord ^ " </GUH>\n" ^
13.118 -.................................................................*)
13.119 - indt (j+i) ^"</ORDER>\n" ^
13.120 - indt (j+i) ^"<ERLS> " ^
13.121 - indt (j+2*i) ^ "<TAG> Ruleset </TAG>\n" ^
13.122 - indt (j+2*i) ^ "<STRING> " ^ id_rls erls ^ " </STRING>\n" ^
13.123 - indt (j+2*i) ^ "<GUH> " ^ rls2guh ("IsacKnowledge", thyID) (id_rls erls) ^ " </GUH>\n" ^
13.124 - indt (j+i) ^"</ERLS>\n" ^
13.125 - calcrefs2xml (j+i) (thyID, calc) ^
13.126 - indt (j+i) ^"<SCRIPT>\n"^
13.127 - scr2xml (j+2*i) scr ^
13.128 - indt (j+i) ^" </SCRIPT>\n"^
13.129 - indt j ^"</RULESET>\n" : xml;
13.130 -
13.131 -(*WN060627 scope of thy's not considered ?!?*)
13.132 -fun thm''2xml j (thm : thm) =
13.133 - indt j ^ "<THEOREM>\n" ^
13.134 - indt (j+i) ^ "<ID> " ^ thmID_of_derivation_name' thm ^ " </ID>\n"^
13.135 - term2xml j (Thm.prop_of thm) ^ "\n" ^
13.136 - indt j ^ "</THEOREM>\n" : xml;
13.137 -
13.138 -fun calc2xml j (thyID:thyID, (scrop, (rewop, _)):calc) =
13.139 - indt j ^ "<CALC>\n" ^
13.140 - indt (j+i) ^ "<STRING>\n" ^ scrop ^ "</STRING>\n" ^
13.141 - indt (j+i) ^ "<GUH>\n" ^ cal2guh ("IsacKnowledge",
13.142 - thyID) scrop ^ "</GUH>\n" ^
13.143 - indt (j+i) ^ "<TERMOP>\n" ^ rewop ^ "</TERMOP>\n" ^
13.144 - indt j ^ "</CALC>\n" : xml;
13.145 -
13.146 (* create the xml-files for the thydata in the hierarchy *)
13.147 val i = indentation;
13.148 (* analoguous to 'fun met2xml' *)
14.1 --- a/src/Tools/isac/xmlsrc/xmlsrc.thy Thu Oct 06 17:03:44 2016 +0200
14.2 +++ b/src/Tools/isac/xmlsrc/xmlsrc.thy Mon Oct 10 18:24:14 2016 +0200
14.3 @@ -16,9 +16,6 @@
14.4
14.5 ML {*
14.6 *} ML {*
14.7 -*} ML {*
14.8 -*} ML {*
14.9 -*} ML {*
14.10 *}
14.11
14.12 end