1.1 --- a/src/sml/ME/ptyps.sml Wed Nov 05 23:20:43 2003 +0100
1.2 +++ b/src/sml/ME/ptyps.sml Wed Nov 05 23:20:44 2003 +0100
1.3 @@ -799,7 +799,7 @@
1.4 (*run subp-rooteq.sml 'root-eq + subpbl: solve_linear'
1.5 until 'val nxt = ("Model_Problem",Model_Problem ["linear","univariate"...
1.6 > val Nd(PblObj _,[_,_,_,_,_,_,_,_,_,_,_,
1.7 - Nd(PblObj{origin=(oris,_),...},[])]) = pt;
1.8 + Nd(PblObj{origin=(oris,_,_),...},[])]) = pt;
1.9 > val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"],
1.10 (#where_ o get_pbt) ["linear","univariate","equation"]);
1.11 > match_oris oris (pbt,pre);
1.12 @@ -816,7 +816,7 @@
1.13 run subp-rooteq.sml 'root-eq + subpbl: solve_plain_square'
1.14 until 'val nxt = ("Model_Problem",Model_Problem ["plain_square","univ...
1.15 > val Nd (PblObj _, [_,_,_,_,_,_,_,Nd (PrfObj _,[]),
1.16 - Nd (PblObj {origin=(oris,_),...},[])]) = pt;
1.17 + Nd (PblObj {origin=(oris,_,_),...},[])]) = pt;
1.18 > val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"],
1.19 (#where_ o get_pbt) ["linear","univariate","equation"]);
1.20 > match_oris oris (pbt,pre);
1.21 @@ -844,15 +844,13 @@
1.22 val pb = foldl and_ (true, map fst pre')
1.23 in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
1.24
1.25 -type fmz = string list;
1.26 -
1.27 (*. for the user .*)
1.28 datatype match' =
1.29 Matches' of item ppc
1.30 | NoMatch' of item ppc;
1.31
1.32 (*. match a formalization with a problem type .*)
1.33 -fun match_pbl (fmz:fmz) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) =
1.34 +fun match_pbl (fmz:fmz_) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) =
1.35 let val oris = prep_ori fmz thy ppc;
1.36 val (bool, (itms, pre')) = match_oris' thy oris (ppc,pre,er);
1.37 in if bool then Matches' (itms2itemppc thy itms pre')
1.38 @@ -995,5 +993,5 @@
1.39 (* val fmz = fmz1; val pblID = ["pbla"]; val pblRD = (rev o tl) pblID;
1.40 val pbls = []; val ptys = !ptyps;
1.41 *)
1.42 -fun refine (fmz:fmz) (pblID:pblID) =
1.43 +fun refine (fmz:fmz_) (pblID:pblID) =
1.44 app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID) (!ptyps);
2.1 --- a/src/sml/ME/script.sml Wed Nov 05 23:20:43 2003 +0100
2.2 +++ b/src/sml/ME/script.sml Wed Nov 05 23:20:44 2003 +0100
2.3 @@ -642,7 +642,7 @@
2.4 val thy' = (get_obj g_domID pt pp):theory';
2.5 val thy = assoc_thy thy';
2.6 val metID = get_obj g_metID pt pp;
2.7 - val metID' = if metID =e_metID then(thd3 o snd)(get_obj g_origin pt pp)
2.8 + val metID' =if metID =e_metID then(thd3 o snd3)(get_obj g_origin pt pp)
2.9 else metID;
2.10 val Script sc = (#scr o get_met) metID';
2.11 val ScrState (env,_,_,_,_,_) = get_istate pt (p,p_);
2.12 @@ -816,13 +816,13 @@
2.13 "SubProblem (DiffApp_,[make,function],[no_met]) \
2.14 \[real_ m_, real_ v_, bool_list_ rs_]";
2.15
2.16 - val (Subproblem' ((domID,pblID,metID),_,f)) = m;
2.17 + val (Subproblem' ((domID,pblID,metID),_,_,_,f)) = m;
2.18 val (Const ("Script.SubProblem",_) $
2.19 (Const ("Pair",_) $
2.20 Free (dI',_) $
2.21 (Const ("Pair",_) $ pI' $ mI')) $ ags') = stac;
2.22 *)
2.23 - | assod _ (Subproblem' ((domID,pblID,metID),_,f))
2.24 + | assod _ (Subproblem' ((domID,pblID,metID),_,_,_,f))
2.25 (Const ("Script.SubProblem",_) $
2.26 (Const ("Pair",_) $
2.27 Free (dI',_) $
2.28 @@ -837,13 +837,18 @@
2.29 de_esc_underscore mI2');*)
2.30 (*5.8.02: really take domID for metID ?
2.31 val _= writeln "### assod: vor match_ags";*)
2.32 - val oris = match_ags (assoc_thy domID) ((#ppc o get_pbt) pblID)
2.33 - (isalist2list ags');
2.34 + val {cas, ppc,...} = get_pbt pblID
2.35 + val ags = isalist2list ags'
2.36 + val fmz_ = map term2str ags
2.37 + val hdl = case cas of
2.38 + None => pblterm domID pblID
2.39 + | Some t => subst_atomic ((vars_of_pbl_ ppc)~~ ags) t
2.40 + val oris = match_ags (assoc_thy domID) ppc ags;
2.41 (*val _= writeln "### assod: nach match_ags";*)
2.42 in
2.43 (*writeln("##### assoc: metID' = "^(metID2str metID'));*)
2.44 if domID = domID' andalso pblID = pblID'
2.45 - then Ass (Subproblem' ((domID, pblID, metID'), oris, f), f)
2.46 + then Ass (Subproblem' ((domID, pblID, metID'), oris, hdl, fmz_, f), f)
2.47 else NotAss
2.48 end
2.49
2.50 @@ -885,7 +890,7 @@
2.51
2.52 | tac_2tac (Tac_ (_,f,id,f')) = Tac id
2.53
2.54 - | tac_2tac (Subproblem' ((domID, pblID, _), _, _)) =
2.55 + | tac_2tac (Subproblem' ((domID, pblID, _), _, _,_,_)) =
2.56 Subproblem (domID, pblID)
2.57 | tac_2tac (Check_Postcond' (pblID, _)) =
2.58 Check_Postcond pblID
3.1 --- a/src/sml/ME/solve.sml Wed Nov 05 23:20:43 2003 +0100
3.2 +++ b/src/sml/ME/solve.sml Wed Nov 05 23:20:44 2003 +0100
3.3 @@ -152,7 +152,7 @@
3.4 | None =>
3.5 let val m = fst3 (next_tac (thy',srls) (pt,(lev_on p,Frm)) scr is);
3.6 val f = case m of
3.7 - Subproblem' ((domID, pblID,_),_,_) =>
3.8 + Subproblem' ((domID, pblID,_),_,_,_,_) =>
3.9 Form' (FormKF (~1,EdUndef,(length p), Nundef,
3.10 (Sign.string_of_term (sign_of (assoc_thy thy'))
3.11 (subpbl domID pblID))))
4.1 --- a/src/sml/kbtest/diffapp.sml Wed Nov 05 23:20:43 2003 +0100
4.2 +++ b/src/sml/kbtest/diffapp.sml Wed Nov 05 23:20:44 2003 +0100
4.3 @@ -558,7 +558,7 @@
4.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.5 (*val nxt = ("Specify_Method",Specify_Method ["DiffApp","max_by_calculus"])*)
4.6
4.7 -val oris = fst (get_obj g_origin pt (fst p));writeln(oris2str oris);
4.8 +val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
4.9 val itms = get_obj g_pbl pt (fst p);writeln(itms2str thy itms);
4.10
4.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.12 @@ -585,7 +585,7 @@
4.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.14 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.15
4.16 -val oris = fst (get_obj g_origin pt (fst p));writeln(oris2str oris);
4.17 +val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
4.18 val itms = get_obj g_pbl pt (fst p);writeln(itms2str thy itms);
4.19
4.20 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.21 @@ -598,7 +598,7 @@
4.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.23 (*val nxt = Refine_Tacitly ["univariate","equation"])*)
4.24
4.25 -val oris = fst (get_obj g_origin pt (fst p));writeln(oris2str oris);
4.26 +val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
4.27 val itms = get_obj g_pbl pt (fst p);writeln(itms2str thy itms);
4.28
4.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.30 @@ -629,7 +629,7 @@
4.31
4.32 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
4.33
4.34 -val oris = fst (get_obj g_origin pt (fst p));writeln(oris2str oris);
4.35 +val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
4.36
4.37 val itms = get_obj g_pbl pt (fst p);writeln(itms2str thy itms);
4.38 val itms = get_obj g_pbl pt [];writeln(itms2str thy itms);
5.1 --- a/src/sml/systest/FE-interface.sml Wed Nov 05 23:20:43 2003 +0100
5.2 +++ b/src/sml/systest/FE-interface.sml Wed Nov 05 23:20:44 2003 +0100
5.3 @@ -329,6 +329,7 @@
5.4 moveRoot 1 1;
5.5
5.6 checkCalcHead 1 (([],Pbl),(*the position*)
5.7 + "solve (x+1=2, x)",(*the headline*)
5.8 [Given ["equality (x+1=2)", "solveFor x"],
5.9 Find ["solutions L"](*,Relate []*)],
5.10 Pbl,
5.11 @@ -336,8 +337,11 @@
5.12 ["sqroot-test","univariate","equation","test"],
5.13 ["Test","squ-equ-test-subpbl1"]));
5.14
5.15 -
5.16 -
5.17 +val (fmz, (dI',pI',mI')) =
5.18 +(["equality (x+1=2)", "solveFor x","solutions L"],
5.19 + ("Test.thy",
5.20 + ["sqroot-test","univariate","equation","test"],
5.21 + ["Test","squ-equ-test-subpbl1"]));
5.22
5.23 "---------------- run scripts for maximum-example ----------------";
5.24 "---------------- run scripts for maximum-example ----------------";
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/sml/systest/inputtest.sml Wed Nov 05 23:20:44 2003 +0100
6.3 @@ -0,0 +1,36 @@
6.4 +(* use"systest/inputtest.sml";
6.5 + use"inputtest.sml";
6.6 + *)
6.7 +
6.8 +
6.9 + val (p,_,f,nxt,_,pt) =
6.10 + CalcTreeTEST
6.11 + [(["equality (x+1=2)", "solveFor x","solutions L"],
6.12 + ("Test.thy",
6.13 + ["sqroot-test","univariate","equation","test"],
6.14 + ["Test","squ-equ-test-subpbl1"]))];
6.15 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.16 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.17 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.18 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.19 +
6.20 + val ichd =
6.21 + (([],Pbl),
6.22 + [Given ["equality (x+1=2)", "solveFor x"], Find ["solutions L"]],
6.23 + Pbl,
6.24 + ("Test.thy",
6.25 + ["sqroot-test","univariate","equation","test"],
6.26 + ["Test","squ-equ-test-subpbl1"]));
6.27 +
6.28 + input_icalhd pt ichd;
6.29 +
6.30 +
6.31 +
6.32 +
6.33 +
6.34 +
6.35 + print_depth 9;
6.36 + pt;
6.37 + print_depth 3;
6.38 +
6.39 +
6.40 \ No newline at end of file
7.1 --- a/src/sml/systest/root-equ.sml Wed Nov 05 23:20:43 2003 +0100
7.2 +++ b/src/sml/systest/root-equ.sml Wed Nov 05 23:20:44 2003 +0100
7.3 @@ -265,7 +265,7 @@
7.4 ["sqroot-test","univariate","equation","test"]);
7.5 val loc = e_istate;
7.6 val (pt,pos) = (e_ptree,[]);
7.7 -val (pt,_) = cappend_problem pt pos loc (oris,empty_spec);
7.8 +val (pt,_) = cappend_problem pt pos loc e_fmz (oris,empty_spec,e_term);
7.9 val pt = update_branch pt [] TransitiveB;
7.10 (*
7.11 val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt [])));
8.1 --- a/src/sml/xmlsrc/datatypes.sml Wed Nov 05 23:20:43 2003 +0100
8.2 +++ b/src/sml/xmlsrc/datatypes.sml Wed Nov 05 23:20:44 2003 +0100
8.3 @@ -117,7 +117,7 @@
8.4 itm_2xml j itm_ ^ itms2xml j itms;
8.5
8.6 fun precond2xml j (true, term) =
8.7 - (indt j ^"<ITEM status=\"true\">\n"^
8.8 + (indt j ^"<ITEM status=\"correct\">\n"^
8.9 term2xml (j) term^"\n"^
8.10 indt j ^"</ITEM>\n"):xml
8.11 | precond2xml j (false, term) =
9.1 --- a/src/sml/xmlsrc/interface-xml.sml Wed Nov 05 23:20:43 2003 +0100
9.2 +++ b/src/sml/xmlsrc/interface-xml.sml Wed Nov 05 23:20:44 2003 +0100
9.3 @@ -123,7 +123,7 @@
9.4 \</NEXTTAC>\n\
9.5 \@@@@@end@@@@@");
9.6
9.7 -fun checkcalcheadOK2xml (cI:calcID) incom chd =
9.8 +fun checkcalcheadOK2xml (cI:calcID) incom (chd:ocalhd) =
9.9 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
9.10 \<CHECKCALCHEAD>\n\
9.11 \ <CALCID> "^string_of_int cI^" </CALCID>\n\