1.1 --- a/src/Tools/isac/Interpret/generate.sml Wed Dec 14 14:20:25 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/generate.sml Sun Dec 18 16:27:41 2016 +0100
1.3 @@ -176,7 +176,7 @@
1.4 (*generate 1 ppobj in ptree*)
1.5 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
1.6 fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt =
1.7 - (pos: pos', [], PpcKF (Upblmet, itms2itemppc thy [][]),
1.8 + (pos: pos', [], PpcKF (Upblmet, Specify.itms2itemppc thy [][]),
1.9 case p_ of
1.10 Pbl => update_pbl pt p itmlist
1.11 | Met => update_met pt p itmlist
1.12 @@ -184,27 +184,27 @@
1.13 (* WN110515 probably declare_constraints with input item (without dsc) --
1.14 -- important when specifying without formalisation *)
1.15 | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p, p_)) pt =
1.16 - (pos, [], (PpcKF (Upblmet, itms2itemppc thy [] [])),
1.17 + (pos, [], (PpcKF (Upblmet, Specify.itms2itemppc thy [] [])),
1.18 case p_ of
1.19 Pbl => update_pbl pt p itmlist
1.20 | Met => update_met pt p itmlist
1.21 | _ => error ("uncovered case " ^ pos_2str p_))
1.22 (*WN110515 probably declare_constraints with input item (without dsc)*)
1.23 | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p, p_)) pt =
1.24 - (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []),
1.25 + (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []),
1.26 case p_ of
1.27 Pbl => update_pbl pt p itmlist
1.28 | Met => update_met pt p itmlist
1.29 | _ => error ("uncovered case " ^ pos_2str p_))
1.30 | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt =
1.31 - (pos, [] , PpcKF (Upblmet, itms2itemppc thy [] []),
1.32 + (pos, [] , PpcKF (Upblmet, Specify.itms2itemppc thy [] []),
1.33 update_domID pt p domID)
1.34 | generate1 thy (Specify_Problem' (pI, (_, (itms, _)))) _ (p, _) pt =
1.35 let
1.36 val pt = update_pbl pt p itms
1.37 val pt = update_pblID pt p pI
1.38 in
1.39 - ((p, Pbl), [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
1.40 + ((p, Pbl), [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)
1.41 end
1.42 | generate1 thy (Specify_Method' (mID, oris, itms)) _ (p, _) pt =
1.43 let
1.44 @@ -212,28 +212,28 @@
1.45 val pt = update_met pt p itms
1.46 val pt = update_metID pt p mID
1.47 in
1.48 - ((p, Met), [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
1.49 + ((p, Met), [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)
1.50 end
1.51 | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
1.52 let
1.53 val pt = update_pbl pt p itms
1.54 val pt = update_met pt p met
1.55 in
1.56 - (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
1.57 + (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)
1.58 end
1.59 | generate1 thy (Refine_Tacitly' (_, pIre, domID, metID, pbl)) _ (pos as (p, _)) pt =
1.60 let
1.61 val pt = update_pbl pt p pbl
1.62 val pt = update_orispec pt p (domID, pIre, metID)
1.63 in
1.64 - (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
1.65 + (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)
1.66 end
1.67 | generate1 thy (Refine_Problem' (pI, _)) _ (pos as (p, _)) pt =
1.68 let
1.69 val (dI, _, mI) = get_obj g_spec pt p
1.70 val pt = update_spec pt p (dI, pI, mI)
1.71 in
1.72 - (pos, [], PpcKF (Upblmet, itms2itemppc thy [] []), pt)
1.73 + (pos, [], PpcKF (Upblmet, Specify.itms2itemppc thy [] []), pt)
1.74 end
1.75 | generate1 _ (Apply_Method' (_, topt, is, ctxt)) _ (pos as (p, _)) pt =
1.76 (case topt of
1.77 @@ -424,7 +424,7 @@
1.78 val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, ctxt))) ::
1.79 (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm),
1.80 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]
1.81 - val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.82 + val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
1.83 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
1.84 val pt = update_tac pt p (Derive (id_rls nrls))
1.85 val pt = update_branch pt p TransitiveB
1.86 @@ -441,7 +441,7 @@
1.87 val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, ctxt))) ::
1.88 (insert_pos ((lev_on o lev_dn) p) tacis) @ [(End_Trans, End_Trans' (res, asm),
1.89 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))];
1.90 - val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.91 + val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
1.92 val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
1.93 val pt = update_tac pt p (Derive (id_rls nrls))
1.94 val pt = update_branch pt p TransitiveB