1.1 --- a/src/Tools/isac/calcelems.sml Wed Jun 11 16:11:26 2014 +0200
1.2 +++ b/src/Tools/isac/calcelems.sml Sun Jun 15 18:27:23 2014 +0200
1.3 @@ -897,6 +897,20 @@
1.4 else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))
1.5 );
1.6
1.7 +fun update_ptyps ID _ _ [] =
1.8 + error ("update_ptyps: " ^ strs2str' ID ^ " does not exist")
1.9 + | update_ptyps ID [i] data ((py as Ptyp (key, _, pys)) :: pyss) =
1.10 + if i = key
1.11 + then
1.12 + if length pys = 0
1.13 + then ((Ptyp (key, [data], [])) :: pyss)
1.14 + else error ("update_ptyps: " ^ strs2str' ID ^ " has descendants")
1.15 + else py :: update_ptyps ID [i] data pyss
1.16 + | update_ptyps ID (i :: is) data ((py as Ptyp (key, d, pys)) :: pyss) =
1.17 + if i = key
1.18 + then ((Ptyp (key, d, update_ptyps ID is data pys)) :: pyss)
1.19 + else (py :: (update_ptyps ID (i :: is) data pyss))
1.20 +
1.21 (* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge
1.22 function for trees / ptyps *)
1.23 fun merge_ptyps ([], pt) = pt
1.24 @@ -905,7 +919,7 @@
1.25 if k = k'
1.26 then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)
1.27 else x' :: merge_ptyps (xs, xs');
1.28 -
1.29 +fun merge_ptyps' pt1 pt2 = merge_ptyps (pt1, pt2)
1.30
1.31 (* data for methods stored in 'methods'-database*)
1.32 type met =
1.33 @@ -1006,22 +1020,75 @@
1.34 parents of thydata in list, missing in thehier, are inserted
1.35 (causing msgs '*** insert: not found');
1.36 (1) is kept in case (2) contains same theID (causing msgs '*** insert: preserved ') *)
1.37 -fun the_hier th ([]: (theID * thydata) list) = th
1.38 - | the_hier th ((theID, thydata)::ths) =
1.39 - if can_insert theID th
1.40 - then
1.41 +fun (*KEStore_Elems.*)add_thes th thes = (* for tests bypassing setup KEStore_Elems *)
1.42 + let
1.43 + fun add_the th ((thydata, theID)) =
1.44 + if can_insert theID th
1.45 + then
1.46 + if exist_the theID th
1.47 + then (writeln ("*** insert: preserved " ^ strs2str theID); (fn x => x))
1.48 + else insrt theID thydata theID
1.49 + else
1.50 + let
1.51 + val th' = fill_parents th theID theID (*..*** insert: not found*)
1.52 + val th' = insrt theID thydata theID th'
1.53 + in merge_ptyps' th' end;
1.54 +in fold (add_the th) thes end
1.55 +
1.56 +
1.57 +fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
1.58 + Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
1.59 + fillpats = fillpats', thm = thm}
1.60 + | update_hthm _ _ = raise ERROR "wrong data";
1.61 +
1.62 +(* for interface for dialog-authoring *)
1.63 +fun update_hrls (Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
1.64 + let
1.65 + val rls' =
1.66 + case rls of
1.67 + Rls {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>
1.68 + Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
1.69 + calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
1.70 + | Seq {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...} =>
1.71 + Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
1.72 + calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
1.73 + | Rrls {id, prepat, rew_ord, erls, calc, scr, ...} =>
1.74 + Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,
1.75 + scr = scr, errpatts = errpatIDs}
1.76 + | Erls => Erls
1.77 + in
1.78 + Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
1.79 + thy_rls = (thyID, rls')}
1.80 + end
1.81 + | update_hrls _ _ = raise ERROR "wrong data";
1.82 +
1.83 +fun app_py p f (d:pblID) (k(*:pblRD*)) = let
1.84 + fun py_err _ =
1.85 + error ("app_py: not found: " ^ (strs2str d));
1.86 + fun app_py' _ [] = py_err ()
1.87 + | app_py' [] _ = py_err ()
1.88 + | app_py' [k0] ((p' as Ptyp (k', _, _ ))::ps) =
1.89 + if k0 = k' then f p' else app_py' [k0] ps
1.90 + | app_py' (k' as (k0::ks)) (Ptyp (k'', _, ps)::ps') =
1.91 + if k0 = k'' then app_py' ks ps else app_py' k' ps';
1.92 + in app_py' k p end;
1.93 +
1.94 +fun get_py p = let
1.95 + fun extract_py (Ptyp (_, [py], _)) = py
1.96 + | extract_py _ = error ("extract_py: Ptyp has wrong format.");
1.97 + in app_py p extract_py end;
1.98 +
1.99 +(*
1.100 +fun (*KEStore_Elems.*)insert_fillpats th fis = (* for tests bypassing setup KEStore_Elems *)
1.101 + let
1.102 + fun update_elem th (theID, fillpats) =
1.103 let
1.104 - val th' =
1.105 - if exist_the theID th
1.106 - then (writeln ("*** insert: preserved " ^ strs2str theID); th)
1.107 - else insrt theID thydata theID th
1.108 - in the_hier th' ths end
1.109 - else
1.110 - let
1.111 - val th' = fill_parents th theID theID (*..*** insert: not found*)
1.112 - val th' = insrt theID thydata theID th'
1.113 - in the_hier th' ths end;
1.114 -
1.115 + val hthm = get_py th theID theID
1.116 + val hthm' = update_hthm hthm fillpats
1.117 + handle ERROR _ => error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
1.118 + in update_ptyps theID theID hthm' end
1.119 + in fold (update_elem th) fis end
1.120 + *)
1.121 (*
1.122 end (*struct*)
1.123 *)