1.1 --- a/src/Tools/isac/Interpret/inform.sml Wed Dec 14 14:20:25 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Sun Dec 18 16:27:41 2016 +0100
1.3 @@ -75,20 +75,20 @@
1.4 fun cas_input_ ((dI, pI, mI): spec) dtss = (*WN110515 reconsider thy..ctxt*)
1.5 let
1.6 val thy = assoc_thy dI
1.7 - val {ppc, ...} = get_pbt pI
1.8 + val {ppc, ...} = Specify.get_pbt pI
1.9 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.10 - val its = add_id its_
1.11 + val its = Specify.add_id its_
1.12 val pits = map flattup2 its
1.13 val (pI, mI) =
1.14 if mI <> ["no_met"]
1.15 then (pI, mI)
1.16 else
1.17 - case refine_pbl thy pI pits of
1.18 - SOME (pI,_) => (pI, (hd o #met o get_pbt) pI)
1.19 - | NONE => (pI, (hd o #met o get_pbt) pI)
1.20 - val {ppc, pre, prls, ...} = get_met mI
1.21 + case Specify.refine_pbl thy pI pits of
1.22 + SOME (pI,_) => (pI, (hd o #met o Specify.get_pbt) pI)
1.23 + | NONE => (pI, (hd o #met o Specify.get_pbt) pI)
1.24 + val {ppc, pre, prls, ...} = Specify.get_met mI
1.25 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.26 - val its = add_id its_
1.27 + val its = Specify.add_id its_
1.28 val mits = map flattup2 its
1.29 val pre = check_preconds thy prls pre mits
1.30 val ctxt = e_ctxt (*WN110515 cas_input_ DOESNT WORK*)
1.31 @@ -217,7 +217,7 @@
1.32 let
1.33 val thy = assoc_thy dI
1.34 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
1.35 - val its = add_id its_
1.36 + val its = Specify.add_id its_
1.37 in
1.38 (map flattup2 its): itm list
1.39 end
1.40 @@ -273,35 +273,35 @@
1.41 if dI <> sdI
1.42 then let val its = map (parsitm (assoc_thy dI)) probl;
1.43 val (its, trms) = filter_sep is_Par its;
1.44 - val pbt = (#ppc o get_pbt) (#2 (Chead.some_spec ospec sspec))
1.45 + val pbt = (#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec sspec))
1.46 in (Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
1.47 else
1.48 if pI <> spI
1.49 then if pI = snd3 ospec then (Pbl, probl, meth)
1.50 else
1.51 - let val pbt = (#ppc o get_pbt) pI
1.52 + let val pbt = (#ppc o Specify.get_pbt) pI
1.53 val dI' = #1 (Chead.some_spec ospec spec)
1.54 val oris = if pI = #2 ospec then oris
1.55 - else prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
1.56 + else Specify.prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
1.57 in (Pbl, appl_adds dI' oris probl pbt
1.58 (map itms2fstr probl), meth) end
1.59 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
1.60 - then let val met = (#ppc o get_met) mI
1.61 + then let val met = (#ppc o Specify.get_met) mI
1.62 val mits = Chead.complete_metitms oris probl meth met
1.63 in if foldl and_ (true, map #3 mits)
1.64 then (Pbl, probl, mits) else (Met, probl, mits)
1.65 end
1.66 else (Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]
1.67 - ((#ppc o get_pbt) (#2 (Chead.some_spec ospec spec)))
1.68 + ((#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec spec)))
1.69 (imodel2fstr imodel), meth)
1.70 val pt = update_spec pt p spec;
1.71 in if pos_ = Pbl
1.72 - then let val {prls,where_,...} = get_pbt (#2 (Chead.some_spec ospec spec))
1.73 + then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))
1.74 val pre =check_preconds(assoc_thy"Isac")prls where_ pits
1.75 in (update_pbl pt p pits,
1.76 (Chead.ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec):ocalhd)
1.77 end
1.78 - else let val {prls,pre,...} = get_met (#3 (Chead.some_spec ospec spec))
1.79 + else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))
1.80 val pre = check_preconds (assoc_thy"Isac") prls pre mits
1.81 in (update_met pt p mits,
1.82 (Chead.ocalhd_complete mits pre spec, Met, hdf', mits, pre, spec) : ocalhd)
1.83 @@ -381,7 +381,7 @@
1.84 Frm => get_obj g_form pt p
1.85 | Res => (fst o (get_obj g_result pt)) p
1.86 | _ => e_term (*on PblObj is fo <> ifo*);
1.87 - val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.88 + val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
1.89 val {rew_ord, erls, rules, ...} = rep_rls nrls
1.90 val (found, der) = concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
1.91 in
1.92 @@ -478,7 +478,7 @@
1.93 ("no derivation found", calcstate') =>
1.94 let
1.95 val pp = par_pblobj pt p
1.96 - val (errpats, nrls, prog) = case get_met (get_obj g_metID pt pp) of
1.97 + val (errpats, nrls, prog) = case Specify.get_met (get_obj g_metID pt pp) of
1.98 {errpats, nrls, scr = Prog prog, ...} => (errpats, nrls, prog)
1.99 | _ => error "inform: uncovered case of get_met"
1.100 val env = case get_istate pt pos of
1.101 @@ -511,7 +511,7 @@
1.102 val thmDeriv = Thm.get_name_hint thm
1.103 val (part, thyID) = Rtools.thy_containing_thm thmDeriv
1.104 val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
1.105 - val fillpats = case get_the theID of
1.106 + val fillpats = case Specify.get_the theID of
1.107 Hthm {fillpats, ...} => fillpats
1.108 | _ => error "get_fillpats: uncovered case of get_the"
1.109 val some = map (get_fillform subst (thm, form) errpatID) fillpats
1.110 @@ -521,7 +521,7 @@
1.111 let
1.112 val f_curr = get_curr_formula (pt, pos);
1.113 val pp = par_pblobj pt p
1.114 - val (errpats, prog) = case get_met (get_obj g_metID pt pp) of
1.115 + val (errpats, prog) = case Specify.get_met (get_obj g_metID pt pp) of
1.116 {errpats, scr = Prog prog, ...} => (errpats, prog)
1.117 | _ => error "find_fillpatterns: uncovered case of get_met"
1.118 val env = case get_istate pt pos of
1.119 @@ -568,7 +568,7 @@
1.120 | Rewrite_Set_Inst (_, rlsID) => rlsID
1.121 | _ => "e_rls"
1.122 val (part, thyID) = Rtools.thy_containing_rls "Isac" rlsID;
1.123 - val rls = case get_the [part, thyID, "Rulesets", rlsID] of
1.124 + val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
1.125 Hrls {thy_rls = (_, rls), ...} => rls
1.126 | _ => error "fetchErrorpatterns: uncovered case of get_the"
1.127 in case rls of