1.1 --- a/src/sml/FE-interface/interface.sml Thu Nov 02 10:56:09 2006 +0100
1.2 +++ b/src/sml/FE-interface/interface.sml Thu Nov 02 16:08:45 2006 +0100
1.3 @@ -531,6 +531,28 @@
1.4 | (msg, cs') => appendformulaERROR2xml cI msg
1.5 end)
1.6 handle _ => sysERROR2xml cI "error in kernel";
1.7 +(*
1.8 +fun appendFormula cI (ifo:cterm') =
1.9 + (let val cs = get_calc cI
1.10 + val pos as (_,p_) = get_pos cI 1
1.11 + in case step pos cs of
1.12 +(* val (str, cs') = step pos cs;
1.13 + *)
1.14 + ("ok", cs') =>
1.15 + (case inform cs' (encode ifo) of
1.16 +(* val (str, (_, c, ptp as (_,p))) = inform cs' (encode ifo);
1.17 + *)
1.18 + ("ok", (_(*use in DG !!!*), c, ptp as (_,p))) =>
1.19 + (upd_calc cI (ptp, []); upd_ipos cI 1 p;
1.20 + appendformulaOK2xml cI pos (if null c then pos
1.21 + else last_elem c) p)
1.22 + | ("same-formula", (_(*use in DG !!!*), c, ptp as (_,p))) =>
1.23 + (appendformulaOK2xml cI pos pos p)
1.24 + | (msg, _) => appendformulaERROR2xml cI msg)
1.25 + | (msg, cs') => appendformulaERROR2xml cI msg
1.26 + end)
1.27 + handle _ => sysERROR2xml cI "error in kernel";
1.28 +*)
1.29
1.30 (*.replace a formula with_in_ a calculation;
1.31 this situation applies for initial CAS-commands, too.*)
2.1 --- a/src/sml/ME/generate.sml Thu Nov 02 10:56:09 2006 +0100
2.2 +++ b/src/sml/ME/generate.sml Thu Nov 02 16:08:45 2006 +0100
2.3 @@ -534,15 +534,19 @@
2.4 ((tac,tac_,((p, Res), ist)):taci)
2.5 ::((insert_pos (lev_on p) tacis):taci list);
2.6
2.7 -(*.embed the tacis created by a '_deriv'ation;
2.8 +fun res_from_taci (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = (res, asm)
2.9 + | res_from_taci (_, Rewrite_Set'(_,_,_,_,(res, asm)), _) = (res, asm)
2.10 + | res_from_taci (_, tac_, _) =
2.11 + raise error ("res_from_taci: called with" ^ tac_2str tac_);
2.12 +
2.13 +(*.embed the tacis created by a '_deriv'ation; sys.form <> input.form
2.14 tacis are in order, thus are reverted for generate.*)
2.15 (* val (tacis, (pt, pos as (p, Frm))) = (tacis', ptp);
2.16 *)
2.17 -fun embed_deriv (*[] ptp = ptp ...sys.form = input.form... excluded in inform
2.18 - | embed_deriv *)tacis (pt, pos as (p, Frm)) =
2.19 +fun embed_deriv (tacis:taci list) (pt, pos as (p, Frm):pos') =
2.20 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
2.21 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
2.22 - let val (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = last_elem tacis
2.23 + let val (res, asm) = (res_from_taci o last_elem) tacis
2.24 val (Some ist,_) = get_obj g_loc pt p
2.25 val form = get_obj g_form pt p
2.26 (*val p = lev_on p; ---------------only difference to (..,Res) below*)
2.27 @@ -556,14 +560,14 @@
2.28 val pt = update_tac pt p (Derive (id_rls nrls))
2.29 (*FIXME.040216 struct.ctree*)
2.30 val pt = update_branch pt p TransitiveB
2.31 - in (c, (pt, pos)) end
2.32 + in (c, (pt, pos:pos')) end
2.33
2.34 (* val (tacis, (pt, (p, Res))) = (tacis', ptp);
2.35 *)
2.36 | embed_deriv tacis (pt, (p, Res)) =
2.37 (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
2.38 and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
2.39 - let val (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = last_elem tacis;
2.40 + let val (res, asm) = (res_from_taci o last_elem) tacis
2.41 val (_, Some ist) = get_obj g_loc pt p
2.42 val (f,a) = get_obj g_result pt p
2.43 val p = lev_on p(*---------------only difference to (..,Frm) above*);
2.44 @@ -578,9 +582,3 @@
2.45 (*FIXME.040216 struct.ctree*)
2.46 val pt = update_branch pt p TransitiveB
2.47 in (c, (pt, pos)) end;
2.48 -(*
2.49 - val (_, Some ist) = get_obj g_loc pt p
2.50 - val (f,a) = get_obj g_result pt p
2.51 -
2.52 -
2.53 -*)
2.54 \ No newline at end of file
3.1 --- a/src/sml/ME/inform.sml Thu Nov 02 10:56:09 2006 +0100
3.2 +++ b/src/sml/ME/inform.sml Thu Nov 02 16:08:45 2006 +0100
3.3 @@ -706,7 +706,36 @@
3.4 lev_back pos)) ifo
3.5 end
3.6 | None => ("syntax error in '"^istr^"'", e_calcstate');
3.7 -
3.8 +(* val ((cs as (tacis, _, ptp as (pt, pos as (p, p_)))), istr) =
3.9 + (cs', (encode ifo));
3.10 + *)
3.11 +(*
3.12 +fun inform (cs as (tacis, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
3.13 + case parse (assoc_thy "Isac.thy") istr of
3.14 +(* val Some ifo = parse (assoc_thy "Isac.thy") istr;
3.15 + *)
3.16 + Some ifo =>
3.17 + let val ifo = term_of ifo
3.18 + val fo = case p_ of Frm => get_obj g_form pt p
3.19 + | Res => (fst o (get_obj g_result pt)) p
3.20 + | _ => #3 (get_obj g_origin pt p)
3.21 + in if ifo = fo
3.22 + then ("same-formula", cs)
3.23 + (*thus ctree not cut with replaceFormula!*)
3.24 + else if ifo = (fst o res_from_taci o hd) tacis
3.25 + (*fo calculated by step before*)
3.26 + then ("ok", cs)
3.27 + else case cas_input ifo of
3.28 +(* val Some (pt, _) = cas_input ifo;
3.29 + *)
3.30 + Some (pt, _) => ("ok",([],[],(pt, (p, Pbl))))
3.31 + | None =>
3.32 + compare_step ([],[],(pt,
3.33 + (*last step re-calc in compare_step TODO*)
3.34 + lev_back pos)) ifo
3.35 + end
3.36 + | None => ("syntax error in '"^istr^"'", e_calcstate');
3.37 +*)
3.38
3.39 (*------------------------------------------------------------------(**)
3.40 end
4.1 --- a/src/smltest/ME/inform.sml Thu Nov 02 10:56:09 2006 +0100
4.2 +++ b/src/smltest/ME/inform.sml Thu Nov 02 16:08:45 2006 +0100
4.3 @@ -480,6 +480,13 @@
4.4 "--- input the next formula that would be presented by mat-engine";
4.5 appendFormula 1 "(4 * y + -3 * x) / (x * y) + -1";
4.6
4.7 +val ((pt,p),_) = get_calc 1;
4.8 +show_pt pt;
4.9 +(*
4.10 +if p = ([], Res) then ()
4.11 +else raise error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
4.12 +*)
4.13 +
4.14 (*
4.15 print_depth 9;
4.16 print_depth 5; cs'; print_depth 3;