1.1 --- a/src/Tools/isac/Interpret/inform.sml Sun May 15 13:23:12 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Sun May 15 13:59:05 2011 +0200
1.3 @@ -152,72 +152,48 @@
1.4 val castab = Unsynchronized.ref ([]: castab);
1.5
1.6
1.7 -(*..*)
1.8 -(* val (dI,pI,mI) = spec;
1.9 - *)
1.10 -(*fun cas_input_ ((dI,pI,mI): spec) dtss =
1.11 - let val thy = assoc_thy dI
1.12 - val {ppc,...} = get_pbt pI
1.13 - val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.14 - val its = add_id its_
1.15 - val pits = map flattup2 its
1.16 - val (pI, mI) = if mI <> ["no_met"] then (pI, mI)
1.17 - else let val SOME (pI,_) = refine_pbl thy pI pits
1.18 - in (pI, (hd o #met o get_pbt) pI) end
1.19 - val {ppc,pre,prls,...} = get_met mI
1.20 - val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.21 - val its = add_id its_
1.22 - val mits = map flattup2 its
1.23 - val pre = check_preconds thy prls pre mits
1.24 -in (pI, pits: itm list, mI, mits: itm list, pre) end;*)
1.25 -
1.26 -(* val (dI,pI,mI) = spec;
1.27 - *)
1.28 -fun cas_input_ ((dI,pI,mI): spec) dtss =
1.29 - let val thy = assoc_thy dI
1.30 - val {ppc,...} = get_pbt pI
1.31 - val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.32 - val its = add_id its_
1.33 - val pits = map flattup2 its
1.34 - val (pI, mI) = if mI <> ["no_met"] then (pI, mI)
1.35 - else case refine_pbl thy pI pits of
1.36 +fun cas_input_ ((dI,pI,mI): spec) dtss = (*WN110515 reconsider thy..ctxt*)
1.37 + let
1.38 + val thy = assoc_thy dI
1.39 + val {ppc, ...} = get_pbt pI
1.40 + val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.41 + val its = add_id its_
1.42 + val pits = map flattup2 its
1.43 + val (pI, mI) =
1.44 + if mI <> ["no_met"]
1.45 + then (pI, mI)
1.46 + else
1.47 + case refine_pbl thy pI pits of
1.48 SOME (pI,_) => (pI, (hd o #met o get_pbt) pI)
1.49 | NONE => (pI, (hd o #met o get_pbt) pI)
1.50 - val {ppc,pre,prls,...} = get_met mI
1.51 - val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.52 - val its = add_id its_
1.53 - val mits = map flattup2 its
1.54 - val pre = check_preconds thy prls pre mits
1.55 -in (pI, pits: itm list, mI, mits: itm list, pre) end;
1.56 + val {ppc, pre, prls, ...} = get_met mI
1.57 + val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.58 + val its = add_id its_
1.59 + val mits = map flattup2 its
1.60 + val pre = check_preconds thy prls pre mits
1.61 + val ctxt = e_ctxt (*WN110515 cas_input_ DOESNT WORK*)
1.62 + in (pI, pits: itm list, mI, mits: itm list, pre, ctxt) end;
1.63
1.64
1.65 -(*.check if the input term is a CAScmd and return a ptree with
1.66 - a _complete_ calchead.*)
1.67 -(* val hdt = ifo;
1.68 - *)
1.69 +(* check if the input term is a CAScmd and return a ptree with a _complete_ calchead *)
1.70 fun cas_input hdt =
1.71 - let val (h,argl) = strip_comb hdt
1.72 - in case assoc (!castab, h) of
1.73 - NONE => NONE
1.74 - (*let val (pt,_) =
1.75 - cappend_problem e_ptree [] e_istate
1.76 - ([], e_spec) ([], e_spec, e_term)
1.77 - in (pt, (false, Pbl, e_term(*FIXXME031:'not found'*),
1.78 - [], [], e_spec)) end*)
1.79 - | SOME (spec as (dI,_,_), argl2dtss) =>
1.80 - (* val SOME (spec as (dI,_,_), argl2dtss ) = assoc (!castab, h);
1.81 - *)
1.82 - let val dtss = argl2dtss argl
1.83 - val (pI, pits, mI, mits, pre) = cas_input_ spec dtss
1.84 - val spec = (dI, pI, mI)
1.85 - val (pt,_) =
1.86 - cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1.87 - ([], e_spec, hdt)
1.88 - val pt = update_spec pt [] spec
1.89 - val pt = update_pbl pt [] pits
1.90 - val pt = update_met pt [] mits
1.91 - in SOME (pt, (true, Met, hdt, mits, pre, spec):ocalhd) end
1.92 - end;
1.93 + let val (h,argl) = strip_comb hdt
1.94 + in
1.95 + case assoc (!castab, h) of
1.96 + NONE => NONE
1.97 + | SOME (spec as (dI,_,_), argl2dtss) =>
1.98 + let
1.99 + val dtss = argl2dtss argl
1.100 + val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
1.101 + val spec = (dI, pI, mI)
1.102 + val (pt,_) =
1.103 + cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, hdt)
1.104 + val pt = update_spec pt [] spec
1.105 + val pt = update_pbl pt [] pits
1.106 + val pt = update_met pt [] mits
1.107 + val pt = update_ctxt pt [] ctxt
1.108 + in SOME (pt, (true, Met, hdt, mits, pre, spec) : ocalhd) end
1.109 + end;
1.110
1.111 (*lazy evaluation for (Thy_Info.get_theory "Isac")*)
1.112 fun Isac _ = assoc_thy "Isac";
1.113 @@ -563,14 +539,13 @@
1.114 fun rev_deriv' (t, r, (t', a)) = (t', sym_Thm r, (t, a));
1.115
1.116 fun mk_tacis ro erls (t, r as Thm _, (t', a)) =
1.117 - (Rewrite (rule2thm' r),
1.118 - Rewrite' ("Isac", fst ro, erls, false,
1.119 - rule2thm' r, t, (t', a)),
1.120 - (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
1.121 + (Rewrite (rule2thm' r),
1.122 + Rewrite' ("Isac", fst ro, erls, false, rule2thm' r, t, (t', a)),
1.123 + (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
1.124 | mk_tacis ro erls (t, r as Rls_ rls, (t', a)) =
1.125 - (Rewrite_Set (rule2rls' r),
1.126 - Rewrite_Set' ("Isac", false, rls, t, (t', a)),
1.127 - (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)));
1.128 + (Rewrite_Set (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
1.132 (*fo = ifo excluded already in inform*)
1.133 fun concat_deriv rew_ord erls rules fo ifo =
1.134 @@ -614,46 +589,47 @@
1.135 *)
1.136
1.137
1.138 -(*.compare inform with ctree.form at current pos by nrls;
1.139 +(* compare inform with ctree.form at current pos by nrls;
1.140 if found, embed the derivation generated during comparison
1.141 - if not, let the mat-engine compute the next ctree.form.*)
1.142 + if not, let the mat-engine compute the next ctree.form *)
1.143 (*structure copied from complete_solve
1.144 CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
1.145 all_modspec etc. has to be inserted at Subproblem'*)
1.146 -(* val (tacis, c, ptp as (pt, pos as (p,p_))) = (tacis, ptp);
1.147 - val (tacis, c, ptp as (pt, pos as (p,p_))) = cs';
1.148 -
1.149 - val (tacis, c, ptp as (pt, pos as (p,p_))) = ([],[],(pt, lev_back pos));
1.150 - -----rec.call:
1.151 - val (tacis, c, ptp as (pt, pos as (p,p_))) = cs';
1.152 - *)
1.153 fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): calcstate') ifo =
1.154 - let val fo = case p_ of Frm => get_obj g_form pt p
1.155 - | Res => (fst o (get_obj g_result pt)) p
1.156 - | _ => e_term (*on PblObj is fo <> ifo*);
1.157 - val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.158 - val {rew_ord, erls, rules,...} = rep_rls nrls
1.159 - val (found, der) = concat_deriv rew_ord erls rules fo ifo;
1.160 - in if found
1.161 - then let val tacis' = map (mk_tacis rew_ord erls) der;
1.162 - val (c', ptp) = embed_deriv tacis' ptp;
1.163 - in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
1.164 - else
1.165 - if pos = ([], Res)
1.166 - then ("no derivation found", (tacis, c, ptp): calcstate')
1.167 - else let val cs' as (tacis, c', ptp) = nxt_solve_ ptp;
1.168 - val cs' as (tacis, c'', ptp) =
1.169 - case tacis of
1.170 - ((Subproblem _, _, _)::_) =>
1.171 - let val ptp as (pt, (p,_)) = all_modspec ptp
1.172 - val mI = get_obj g_metID pt p
1.173 - in nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
1.174 - (e_istate, e_ctxt) ptp end
1.175 - | _ => cs';
1.176 - in compare_step (tacis, c @ c' @ c'', ptp) ifo end
1.177 - end;
1.178 -(* tracing (trtas2str der);
1.179 - *)
1.180 + let
1.181 + val fo =
1.182 + case p_ of
1.183 + Frm => get_obj g_form pt p
1.184 + | Res => (fst o (get_obj g_result pt)) p
1.185 + | _ => e_term (*on PblObj is fo <> ifo*);
1.186 + val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.187 + val {rew_ord, erls, rules, ...} = rep_rls nrls
1.188 + val (found, der) = concat_deriv rew_ord erls rules fo ifo;
1.189 + in
1.190 + if found
1.191 + then
1.192 + let
1.193 + val tacis' = map (mk_tacis rew_ord erls) der;
1.194 + val (c', ptp) = embed_deriv tacis' ptp;
1.195 + in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
1.196 + else
1.197 + if pos = ([], Res)
1.198 + then ("no derivation found", (tacis, c, ptp): calcstate')
1.199 + else
1.200 + let
1.201 + val cs' as (tacis, c', ptp) = nxt_solve_ ptp;
1.202 + val cs' as (tacis, c'', ptp) =
1.203 + case tacis of
1.204 + ((Subproblem _, _, _)::_) =>
1.205 + let
1.206 + val ptp as (pt, (p,_)) = all_modspec ptp
1.207 + val mI = get_obj g_metID pt p
1.208 + in nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
1.209 + (e_istate, e_ctxt) ptp
1.210 + end
1.211 + | _ => cs';
1.212 + in compare_step (tacis, c @ c' @ c'', ptp) ifo end
1.213 + end;
1.214
1.215 (*.handle a user-input formula, which may be a CAS-command, too.
1.216 CAS-command:
1.217 @@ -663,19 +639,8 @@
1.218 compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
1.219 collect all the tacs applied by the way.*)
1.220 (*structure copied from autocalc*)
1.221 -(* val (cs as (_, _, (pt, pos as (p, p_))): calcstate') = cs';
1.222 - val ifo = str2term ifo;
1.223 -
1.224 - val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
1.225 - (cs', encode ifo);
1.226 - val ((cs as (_, _, ptp as (pt, pos as (p, p_)))), istr)=(cs', (encode ifo));
1.227 - val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
1.228 - (([],[],(pt,p)), (encode ifo));
1.229 - *)
1.230 fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
1.231 case parse (assoc_thy "Isac") istr of
1.232 -(* val SOME ifo = parse (assoc_thy "Isac") istr;
1.233 - *)
1.234 SOME ifo =>
1.235 let val ifo = term_of ifo
1.236 val fo = case p_ of Frm => get_obj g_form pt p
2.1 --- a/test/Tools/isac/Test_Isac.thy Sun May 15 13:23:12 2011 +0200
2.2 +++ b/test/Tools/isac/Test_Isac.thy Sun May 15 13:59:05 2011 +0200
2.3 @@ -99,23 +99,17 @@
2.4 use "Minisubpbl/200-start-method.sml"
2.5 use "Minisubpbl/300-init-subpbl.sml"
2.6 ML {*
2.7 -val dI = "Integrate";
2.8 -Thy_Info.get_theory dI;
2.9 -val vals = [];
2.10 -*}
2.11 -ML {*
2.12 -dI |> Thy_Info.get_theory |> ProofContext.init_global |> declare_constraints' vals
2.13 +
2.14 *}
2.15 ML {*
2.16 *}
2.17 ML {*
2.18 -val (p,p_) = ([], Frm):pos';
2.19 -Notappl (" not for pos " ^ pos'2str (p,p_))
2.20 *}
2.21 ML {*
2.22 *}
2.23 ML {*
2.24 -is_e_ctxt e_ctxt;
2.25 +*}
2.26 +ML {*
2.27 *}
2.28 use "Minisubpbl/400-start-meth-subpbl.sml"
2.29 use "Minisubpbl/500-postcond.sml"