1.1 --- a/src/Tools/isac/Interpret/inform.sml Wed Dec 21 11:27:22 2016 +0100
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu Dec 22 10:25:49 2016 +0100
1.3 @@ -8,18 +8,18 @@
1.4 sig
1.5 datatype iitem = Find of cterm' list | Given of cterm' list | Relate of cterm' list
1.6 type imodel = iitem list
1.7 - type icalhd = pos' * cterm' * imodel * pos_ * spec
1.8 - val fetchErrorpatterns : tac -> errpatID list
1.9 - val input_icalhd : ptree -> icalhd -> ptree * ocalhd
1.10 + type icalhd = Ctree.pos' * cterm' * imodel * Ctree.pos_ * spec
1.11 + val fetchErrorpatterns : Ctree.tac -> errpatID list
1.12 + val input_icalhd : Ctree.ptree -> icalhd -> Ctree.ptree * Ctree.ocalhd
1.13 val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
1.14 - val find_fillpatterns : ptree * pos' -> errpatID -> (fillpatID * term * thm * subs option) list
1.15 - val is_exactly_equal : ptree * (pos * pos_) -> string -> string * tac
1.16 + val find_fillpatterns : Ctree.ptree * Ctree.pos' -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list
1.17 + val is_exactly_equal : Ctree.ptree * Ctree.pos' -> string -> string * Ctree.tac
1.18
1.19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.20 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
1.21 - val cas_input : term -> (ptree * ocalhd) option
1.22 + val cas_input : term -> (Ctree.ptree * Ctree.ocalhd) option
1.23 val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
1.24 - val compare_step : Generate.taci list * pos' list * (ptree * pos') -> term -> string * Chead.calcstate'
1.25 + val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos') -> term -> string * Chead.calcstate'
1.26 val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
1.27 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
1.28 rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list
1.29 @@ -50,14 +50,14 @@
1.30
1.31 (*calc-head as input*)
1.32 type icalhd =
1.33 - pos' * (*the position of the calc-head in the calc-tree*)
1.34 + Ctree.pos' * (*the position of the calc-head in the calc-tree*)
1.35 cterm' * (*the headline*)
1.36 imodel * (*the model (without Find) of the calc-head*)
1.37 - pos_ * (*model belongs to Pbl or Met*)
1.38 + Ctree.pos_ * (*model belongs to Pbl or Met*)
1.39 spec; (*specification: domID, pblID, metID*)
1.40 -val e_icalhd = (e_pos', "", [Given [""]], Pbl, e_spec) : icalhd
1.41 +val e_icalhd = (Ctree.e_pos', "", [Given [""]], Ctree.Pbl, e_spec) : icalhd
1.42
1.43 -fun is_casinput (hdf : cterm') ((fmz_, spec) : fmz) =
1.44 +fun is_casinput (hdf : cterm') ((fmz_, spec) : Ctree.fmz) =
1.45 hdf <> "" andalso fmz_ = [] andalso spec = e_spec
1.46
1.47 (*.handle an input as into an algebra system.*)
1.48 @@ -91,7 +91,7 @@
1.49 val its = Specify.add_id its_
1.50 val mits = map flattup2 its
1.51 val pre = check_preconds thy prls pre mits
1.52 - val ctxt = e_ctxt (*WN110515 cas_input_ DOESNT WORK*)
1.53 + val ctxt = Ctree.e_ctxt (*WN110515 cas_input_ DOESNT WORK*)
1.54 in (pI, pits: itm list, mI, mits: itm list, pre, ctxt) end;
1.55
1.56
1.57 @@ -108,13 +108,13 @@
1.58 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
1.59 val spec = (dI, pI, mI)
1.60 val (pt,_) =
1.61 - cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, hdt)
1.62 - val pt = update_spec pt [] spec
1.63 - val pt = update_pbl pt [] pits
1.64 - val pt = update_met pt [] mits
1.65 - val pt = update_ctxt pt [] ctxt
1.66 + Ctree.cappend_problem Ctree.e_ptree [] (Ctree.e_istate, Ctree.e_ctxt) ([], e_spec) ([], e_spec, hdt)
1.67 + val pt = Ctree.update_spec pt [] spec
1.68 + val pt = Ctree.update_pbl pt [] pits
1.69 + val pt = Ctree.update_met pt [] mits
1.70 + val pt = Ctree.update_ctxt pt [] ctxt
1.71 in
1.72 - SOME (pt, (true, Met, hdt, mits, pre, spec) : ocalhd)
1.73 + SOME (pt, (true, Ctree.Met, hdt, mits, pre, spec) : Ctree.ocalhd)
1.74 end
1.75 end
1.76
1.77 @@ -262,8 +262,8 @@
1.78 (* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
1.79 fun input_icalhd pt (((p, _), hdf, imodel, Pbl, spec as (dI, pI, mI)) : icalhd) =
1.80 let
1.81 - val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case get_obj I pt p of
1.82 - PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
1.83 + val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
1.84 + Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
1.85 spec = sspec as (sdI, spI, smI), probl, meth, ...}
1.86 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
1.87 | _ => error "input_icalhd: uncovered case of get_obj I pt p"
1.88 @@ -289,22 +289,22 @@
1.89 then let val met = (#ppc o Specify.get_met) mI
1.90 val mits = Chead.complete_metitms oris probl meth met
1.91 in if foldl and_ (true, map #3 mits)
1.92 - then (Pbl, probl, mits) else (Met, probl, mits)
1.93 + then (Pbl, probl, mits) else (Ctree.Met, probl, mits)
1.94 end
1.95 else (Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]
1.96 ((#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec spec)))
1.97 (imodel2fstr imodel), meth)
1.98 - val pt = update_spec pt p spec;
1.99 + val pt = Ctree.update_spec pt p spec;
1.100 in if pos_ = Pbl
1.101 then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))
1.102 val pre =check_preconds(assoc_thy"Isac")prls where_ pits
1.103 - in (update_pbl pt p pits,
1.104 - (Chead.ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec):ocalhd)
1.105 + in (Ctree.update_pbl pt p pits,
1.106 + (Chead.ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec): Ctree.ocalhd)
1.107 end
1.108 else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))
1.109 val pre = check_preconds (assoc_thy"Isac") prls pre mits
1.110 - in (update_met pt p mits,
1.111 - (Chead.ocalhd_complete mits pre spec, Met, hdf', mits, pre, spec) : ocalhd)
1.112 + in (Ctree.update_met pt p mits,
1.113 + (Chead.ocalhd_complete mits pre spec, Ctree.Met, hdf', mits, pre, spec) : Ctree.ocalhd)
1.114 end
1.115 end
1.116 end
1.117 @@ -337,13 +337,13 @@
1.118 fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a));
1.119
1.120 fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) =
1.121 - (Rewrite (id, thm),
1.122 - Rewrite' ("Isac", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
1.123 - (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
1.124 + (Ctree.Rewrite (id, thm),
1.125 + Ctree.Rewrite' ("Isac", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
1.126 + (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Ctree.Uistate, Ctree.e_ctxt)))
1.127 | mk_tacis _ _ (t, r as Rls_ rls, (t', a)) =
1.128 - (Rewrite_Set (Lucin.rule2rls' r),
1.129 - Rewrite_Set' ("Isac", false, rls, t, (t', a)),
1.130 - (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
1.131 + (Ctree.Rewrite_Set (Lucin.rule2rls' r),
1.132 + Ctree.Rewrite_Set' ("Isac", false, rls, t, (t', a)),
1.133 + (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Ctree.Uistate, Ctree.e_ctxt)))
1.134 | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ rule2str r ^ " at " ^ term2str t)
1.135
1.136 (* fo = ifo excluded already in inform *)
1.137 @@ -378,10 +378,10 @@
1.138 let
1.139 val fo =
1.140 case p_ of
1.141 - Frm => get_obj g_form pt p
1.142 - | Res => (fst o (get_obj g_result pt)) p
1.143 + Frm => Ctree.get_obj Ctree.g_form pt p
1.144 + | Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
1.145 | _ => e_term (*on PblObj is fo <> ifo*);
1.146 - val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
1.147 + val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
1.148 val {rew_ord, erls, rules, ...} = rep_rls nrls
1.149 val (found, der) = concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
1.150 in
1.151 @@ -392,18 +392,18 @@
1.152 val (c', ptp) = Generate.embed_deriv tacis' ptp;
1.153 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
1.154 else
1.155 - if pos = ([], Res) (*TODO: we should stop earlier with trying subproblems *)
1.156 + if pos = ([], Ctree.Res) (*TODO: we should stop earlier with trying subproblems *)
1.157 then ("no derivation found", (tacis, c, ptp): Chead.calcstate')
1.158 else
1.159 let
1.160 val cs' as (tacis, c', ptp) = Solve.nxt_solve_ ptp; (*<---------------------*)
1.161 val (tacis, c'', ptp) = case tacis of
1.162 - ((Subproblem _, _, _)::_) =>
1.163 + ((Ctree.Subproblem _, _, _)::_) =>
1.164 let
1.165 val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)
1.166 - val mI = get_obj g_metID pt p
1.167 + val mI = Ctree.get_obj Ctree.g_metID pt p
1.168 in
1.169 - Solve.nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
1.170 + Solve.nxt_solv (Ctree.Apply_Method' (mI, NONE, Ctree.e_istate, Ctree.e_ctxt)) (Ctree.e_istate, Ctree.e_ctxt) ptp
1.171 end
1.172 | _ => cs';
1.173 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
1.174 @@ -460,29 +460,29 @@
1.175 SOME f_in =>
1.176 let
1.177 val f_in = Thm.term_of f_in
1.178 - val f_succ = get_curr_formula (pt, pos);
1.179 + val f_succ = Ctree.get_curr_formula (pt, pos);
1.180 in
1.181 if f_succ = f_in
1.182 then ("same-formula", cs) (* ctree not cut with replaceFormula *)
1.183 else
1.184 case cas_input f_in of
1.185 - SOME (pt, _) => ("ok",([], [], (pt, (p, Met))))
1.186 + SOME (pt, _) => ("ok",([], [], (pt, (p, Ctree.Met))))
1.187 | NONE =>
1.188 let
1.189 - val pos_pred = lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
1.190 - val f_pred = get_curr_formula (pt, pos_pred)
1.191 + val pos_pred = Ctree.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
1.192 + val f_pred = Ctree.get_curr_formula (pt, pos_pred)
1.193 val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*)
1.194 (*last step re-calc in compare_step TODO before WN09*)
1.195 in
1.196 case msg_calcstate' of
1.197 ("no derivation found", calcstate') =>
1.198 let
1.199 - val pp = par_pblobj pt p
1.200 - val (errpats, nrls, prog) = case Specify.get_met (get_obj g_metID pt pp) of
1.201 + val pp = Ctree.par_pblobj pt p
1.202 + val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
1.203 {errpats, nrls, scr = Prog prog, ...} => (errpats, nrls, prog)
1.204 | _ => error "inform: uncovered case of get_met"
1.205 - val env = case get_istate pt pos of
1.206 - ScrState (env, _, _, _, _, _) => env
1.207 + val env = case Ctree.get_istate pt pos of
1.208 + Ctree.ScrState (env, _, _, _, _, _) => env
1.209 | _ => error "inform: uncovered case of get_istate"
1.210 in
1.211 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
1.212 @@ -517,15 +517,15 @@
1.213 val some = map (get_fillform subst (thm, form) errpatID) fillpats
1.214 in some |> filter is_some |> map the end
1.215
1.216 -fun find_fillpatterns (pt, pos as (p, _): pos') errpatID =
1.217 +fun find_fillpatterns (pt, pos as (p, _): Ctree.pos') errpatID =
1.218 let
1.219 - val f_curr = get_curr_formula (pt, pos);
1.220 - val pp = par_pblobj pt p
1.221 - val (errpats, prog) = case Specify.get_met (get_obj g_metID pt pp) of
1.222 + val f_curr = Ctree.get_curr_formula (pt, pos);
1.223 + val pp = Ctree.par_pblobj pt p
1.224 + val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
1.225 {errpats, scr = Prog prog, ...} => (errpats, prog)
1.226 | _ => error "find_fillpatterns: uncovered case of get_met"
1.227 - val env = case get_istate pt pos of
1.228 - ScrState (env, _, _, _, _, _) => env
1.229 + val env = case Ctree.get_istate pt pos of
1.230 + Ctree.ScrState (env, _, _, _, _, _) => env
1.231 | _ => error "inform: uncovered case of get_istate"
1.232 val subst = Rtools.get_bdv_subst prog env
1.233 val errpatthms = errpats
1.234 @@ -538,23 +538,23 @@
1.235 which is stored at the pos where the input is stored of "ok". *)
1.236 fun is_exactly_equal (pt, pos as (p, _)) istr =
1.237 case parseNEW (assoc_thy "Isac" |> thy2ctxt) istr of
1.238 - NONE => ("syntax error in '" ^ istr ^ "'", Tac "")
1.239 + NONE => ("syntax error in '" ^ istr ^ "'", Ctree.Tac "")
1.240 | SOME ifo =>
1.241 let
1.242 - val p' = lev_on p;
1.243 - val tac = get_obj g_tac pt p';
1.244 + val p' = Ctree.lev_on p;
1.245 + val tac = Ctree.get_obj Ctree.g_tac pt p';
1.246 in
1.247 case Applicable.applicable_in pos pt tac of
1.248 - Chead.Notappl msg => (msg, Tac "")
1.249 + Chead.Notappl msg => (msg, Ctree.Tac "")
1.250 | Chead.Appl rew =>
1.251 let
1.252 val res = case rew of
1.253 - Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
1.254 - | Rewrite' (_, _, _, _, _, _, (res, _)) => res
1.255 - | t => error ("is_exactly_equal: uncovered case for " ^ tac_2str t)
1.256 + Ctree.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
1.257 + | Ctree.Rewrite' (_, _, _, _, _, _, (res, _)) => res
1.258 + | t => error ("is_exactly_equal: uncovered case for " ^ Ctree.tac_2str t)
1.259 in
1.260 if not (ifo = res)
1.261 - then ("input does not exactly fill the gaps", Tac "")
1.262 + then ("input does not exactly fill the gaps", Ctree.Tac "")
1.263 else ("ok", tac)
1.264 end
1.265 end
1.266 @@ -564,8 +564,8 @@
1.267 let
1.268 val rlsID =
1.269 case tac of
1.270 - Rewrite_Set rlsID => rlsID
1.271 - | Rewrite_Set_Inst (_, rlsID) => rlsID
1.272 + Ctree.Rewrite_Set rlsID => rlsID
1.273 + | Ctree.Rewrite_Set_Inst (_, rlsID) => rlsID
1.274 | _ => "e_rls"
1.275 val (part, thyID) = Rtools.thy_containing_rls "Isac" rlsID;
1.276 val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of