1.1 --- a/src/Tools/isac/Interpret/script.sml Wed Dec 14 14:20:25 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/script.sml Sun Dec 18 16:27:41 2016 +0100
1.3 @@ -205,7 +205,7 @@
1.4 | SOME (_, _, _, _, itm_) => penvval_in itm_
1.5 (*| SOME (_,_,_,_,itm_) => mk_arg thy (d_in itm_) (ts_in itm_);
1.6 penv postponed; presently penv holds already env for script*)
1.7 - val pats = (#ppc o get_met) mI
1.8 + val pats = (#ppc o Specify.get_met) mI
1.9 val _ = if pats = [] then raise ERROR errmsg else ()
1.10 in (flat o (map (itm2arg itms))) pats end;
1.11
1.12 @@ -254,17 +254,17 @@
1.13 if mI = ["no_met"]
1.14 then
1.15 let
1.16 - val pors = (Chead.match_ags thy ((#ppc o get_pbt) pI) ags)
1.17 + val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
1.18 handle ERROR "actual args do not match formal args"
1.19 => (Chead.match_ags_msg pI stac ags(*raise exn*); [])
1.20 - val pI' = refine_ori' pors pI;
1.21 + val pI' = Specify.refine_ori' pors pI;
1.22 in (pI', pors (* refinement over models with diff.prec only *),
1.23 - (hd o #met o get_pbt) pI') end
1.24 - else (pI, (Chead.match_ags thy ((#ppc o get_pbt) pI) ags)
1.25 + (hd o #met o Specify.get_pbt) pI') end
1.26 + else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
1.27 handle ERROR "actual args do not match formal args"
1.28 => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
1.29 val (fmz_, vals) = Chead.oris2fmz_vals pors;
1.30 - val {cas,ppc,thy,...} = get_pbt pI
1.31 + val {cas,ppc,thy,...} = Specify.get_pbt pI
1.32 val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
1.33 val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
1.34 val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global |> declare_constraints' vals
1.35 @@ -416,17 +416,17 @@
1.36 if mI = ["no_met"]
1.37 then
1.38 let
1.39 - val pors = (Chead.match_ags thy ((#ppc o get_pbt) pI) ags)
1.40 + val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
1.41 handle ERROR "actual args do not match formal args"
1.42 => (Chead.match_ags_msg pI stac ags(*raise exn*);[]);
1.43 - val pI' = refine_ori' pors pI;
1.44 - in (pI', pors (*refinement over models with diff.prec only*), (hd o #met o get_pbt) pI')
1.45 + val pI' = Specify.refine_ori' pors pI;
1.46 + in (pI', pors (*refinement over models with diff.prec only*), (hd o #met o Specify.get_pbt) pI')
1.47 end
1.48 - else (pI, (Chead.match_ags thy ((#ppc o get_pbt) pI) ags)
1.49 + else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
1.50 handle ERROR "actual args do not match formal args"
1.51 => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
1.52 val (fmz_, vals) = Chead.oris2fmz_vals pors;
1.53 - val {cas, ppc, thy, ...} = get_pbt pI
1.54 + val {cas, ppc, thy, ...} = Specify.get_pbt pI
1.55 val dI = theory2theory' thy (*take dI from _refined_ pbl*)
1.56 val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
1.57 val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global |> declare_constraints' vals
1.58 @@ -1082,7 +1082,7 @@
1.59 let
1.60 val actuals = itms2args thy metID itms
1.61 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
1.62 - val (scr, sc) = (case (#scr o get_met) metID of
1.63 + val (scr, sc) = (case (#scr o Specify.get_met) metID of
1.64 scr as Prog sc => (scr, sc) | _ => raise ERROR ("init_scrstate with " ^ metID2str metID))
1.65 val formals = formal_args sc
1.66 (*expects same sequence of (actual) args in itms and (formal) args in met*)
1.67 @@ -1095,7 +1095,7 @@
1.68 else error (msg_type (sc, metID, a, f, formals, actuals))
1.69 val env = relate_args [] formals actuals;
1.70 val ctxt = Proof_Context.init_global thy |> declare_constraints' actuals
1.71 - val {pre, prls, ...} = get_met metID;
1.72 + val {pre, prls, ...} = Specify.get_met metID;
1.73 val pres = check_preconds thy prls pre itms |> map snd;
1.74 val ctxt = ctxt |> insert_assumptions pres;
1.75 in (ScrState (env, [], NONE, e_term, Safe, true), ctxt, scr) : istate * Proof.context * scr end;
1.76 @@ -1112,16 +1112,16 @@
1.77 | SOME is =>
1.78 let
1.79 val metID = get_obj g_metID pt p
1.80 - val {srls, ...} = get_met metID
1.81 - in (srls, is, (#scr o get_met) metID) end
1.82 + val {srls, ...} = Specify.get_met metID
1.83 + in (srls, is, (#scr o Specify.get_met) metID) end
1.84 else
1.85 let val (pbl, p', rls') = par_pbl_det pt p
1.86 in if pbl
1.87 then (*if last_elem p = 0 nothing written to pt yet*) (* 2 *)
1.88 let
1.89 val metID = get_obj g_metID pt p'
1.90 - val {srls,...} = get_met metID
1.91 - in (srls, get_loc pt (p,p_), (#scr o get_met) metID) end
1.92 + val {srls,...} = Specify.get_met metID
1.93 + in (srls, get_loc pt (p,p_), (#scr o Specify.get_met) metID) end
1.94 else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_gen, next_tac*) (* 3 *)
1.95 (e_rls, get_loc pt (p,p_),
1.96 case rls' of
1.97 @@ -1141,7 +1141,7 @@
1.98 PblObj {meth = itms, ...} => itms
1.99 | PrfObj _ => error "from_pblobj' NOT with PrfObj")
1.100 val metID = get_obj g_metID pt p'
1.101 - val {srls, scr, ...} = get_met metID
1.102 + val {srls, scr, ...} = Specify.get_met metID
1.103 in
1.104 if last_elem p = 0 (*nothing written to pt yet*)
1.105 then
1.106 @@ -1171,7 +1171,7 @@
1.107 val thy = assoc_thy thy';
1.108 val metID = get_obj g_metID pt pp;
1.109 val metID' = if metID =e_metID then (thd3 o snd3) (get_obj g_origin pt pp) else metID
1.110 - val (sc, srls) = (case get_met metID' of
1.111 + val (sc, srls) = (case Specify.get_met metID' of
1.112 {scr = Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
1.113 val (env, a, v) = (case get_istate pt (p, p_) of
1.114 ScrState (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_rules 2")
1.115 @@ -1196,7 +1196,7 @@
1.116 if metID = e_metID
1.117 then (thd3 o snd3) (get_obj g_origin pt pp)
1.118 else metID
1.119 - val (sc, srls, erls, ro) = (case get_met metID' of
1.120 + val (sc, srls, erls, ro) = (case Specify.get_met metID' of
1.121 {scr = Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
1.122 | _ => error "sel_appl_atomic_tacs 1")
1.123 val (env, a, v) = (case get_istate pt (p, p_) of