1.1 --- a/src/sml/FE-interface/interface.sml	Fri Nov 18 19:19:22 2005 +0100
     1.2 +++ b/src/sml/FE-interface/interface.sml	Fri Nov 25 16:15:11 2005 +0100
     1.3 @@ -5,9 +5,8 @@
     1.4  
     1.5  
     1.6  (* interface to knowledge interpreter
     1.7 -   use"../FE-interface/interface.sml";
     1.8     use"FE-interface/interface.sml";
     1.9 -  use"interface.sml";
    1.10 +   use"interface.sml";
    1.11  
    1.12   print_depth 11;locatetac;print_depth 3;
    1.13   print_depth 11;e_calcstate';print_depth 3;
    1.14 @@ -28,6 +27,7 @@
    1.15      val getAssumptions : calcID -> pos' -> unit
    1.16      val getElementsFromTo : calcID -> pos' -> pos' -> int -> bool -> unit
    1.17      val getTactic : calcID -> pos' -> unit
    1.18 +    val initMatchProblem : calcID -> unit
    1.19      val interSteps : calcID -> pos' -> unit
    1.20      val modifyCalcHead : calcID -> inform.icalhd -> unit
    1.21      val moveActiveCalcHead : calcID -> unit
    1.22 @@ -288,8 +288,18 @@
    1.23  	    modifycalcheadOK2xml cI "complete" chd)
    1.24      end;
    1.25  
    1.26 -(*. without update of CalcTree .*)
    1.27 +(**. without update of CalcTree .**)
    1.28  
    1.29 +(*.initialiye matching; before 'tryMatch' get the pblID to match with.*)
    1.30 +fun initMatchProblem cI =
    1.31 +    (let val ((pt,_),_) = get_calc cI
    1.32 +	 val p = get_pos cI 1
    1.33 +	 val chd = initmatch pt p
    1.34 +    in trymatchOK2xml cI chd end)
    1.35 +    handle _ => sysERROR2xml cI "";
    1.36 +
    1.37 +(*.match the model of a problem at pos p 
    1.38 +   with the model-pattern of the problem with pblID*)
    1.39  fun tryMatchProblem cI pblID =
    1.40      (let val ((pt,_),_) = get_calc cI
    1.41  	 val p = get_pos cI 1

     2.1 --- a/src/sml/ME/mathengine.sml	Fri Nov 18 19:19:22 2005 +0100
     2.2 +++ b/src/sml/ME/mathengine.sml	Fri Nov 25 16:15:11 2005 +0100
     2.3 @@ -32,7 +32,7 @@
     2.4      val detailstep : ptree -> pos' -> string * ptree * pos'
     2.5     (* val e_tac_ : tac_ *)
     2.6     (* val get_pblID : ptree * pos' -> pblID Library.option *)
     2.7 -
     2.8 +    val initmatch : ptree -> pos' -> ptform
     2.9     (* val loc_solve_ :
    2.10         string * tac_ -> ptree * (int list * pos_) -> lOc_ *)
    2.11     (* val loc_specify_ : tac_ -> ptree * pos' -> lOc_ *)
    2.12 @@ -343,7 +343,25 @@
    2.13  
    2.14  
    2.15  
    2.16 -fun trymatch pI pt (pos as (p,_)) =
    2.17 +(*.initialiye matching; before 'tryMatch' get the pblID to match with:
    2.18 +   if no pbl has been specified, take the init from origin.*)
    2.19 +fun initmatch pt (pos as (p,_):pos') =
    2.20 +    let val PblObj {probl,origin=(os,(_,pI,_),_),spec=(dI',pI',mI'),...} = 
    2.21 +	    get_obj I pt p
    2.22 +	val pblID = if pI' = e_pblID 
    2.23 +		    then (*TODO.WN051125 (#init o get_pbt) pI          <<<*) 
    2.24 +			takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
    2.25 +		    else pI'
    2.26 +	val spec = (dI',pblID,mI')
    2.27 +	val {ppc,where_,prls,...} = get_pbt pblID
    2.28 +	val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac.thy") probl 
    2.29 +				  (ppc,where_,prls) os
    2.30 +    in ModSpec (ocalhd_complete pbl pre spec,
    2.31 +		Pbl, e_term, pbl, pre, spec) end;
    2.32 +
    2.33 +(*.match the model of a problem at pos p 
    2.34 +   with the model-pattern of the problem with pblID*)
    2.35 +fun trymatch pI pt (pos as (p,_):pos') =
    2.36      let val PblObj {probl,origin=(os,_,_),spec=(dI,_,mI),...} = get_obj I pt p
    2.37  	val spec = (dI,pI,mI)
    2.38  	val {ppc,where_,prls,...} = get_pbt pI
    2.39 @@ -352,7 +370,7 @@
    2.40      in ModSpec (ocalhd_complete pbl pre spec,
    2.41  		Pbl, e_term, pbl, pre, spec) end;
    2.42  
    2.43 -fun tryrefine pI pt (pos as (p,_)) =
    2.44 +fun tryrefine pI pt (pos as (p,_):pos') =
    2.45      let val PblObj {probl,origin=(os,_,_),spec=(dI,_,mI),...} = get_obj I pt p
    2.46      in case refine_pbl (assoc_thy "Isac.thy") pI probl of
    2.47  	   None => (*copy from trymatch*)

     3.1 --- a/src/sml/ME/ptyps.sml	Fri Nov 18 19:19:22 2005 +0100
     3.2 +++ b/src/sml/ME/ptyps.sml	Fri Nov 25 16:15:11 2005 +0100
     3.3 @@ -361,7 +361,12 @@
     3.4  (* data for methods stored in 'methods'-database *)
     3.5  type met = 
     3.6       (*defaults for Rewrite' (rls have their own data):*)
     3.7 -     {rew_ord'  : rew_ord',   (*for rules in Detail
     3.8 +     {(*TODO.WN0511: 
     3.9 +       unid      : string      (*unique within this isac-knowledge*)
    3.10 +       author    : string      (*copyright*)
    3.11 +       init      : metID       (*to start manual search in hierarchy with*)
    3.12 +       *)
    3.13 +      rew_ord'  : rew_ord',   (*for rules in Detail
    3.14  			       TODO.WN0509 store fun itself, see 'type pbt'*)
    3.15        erls      : rls,        (*the eval_rls for cond. in rules FIXME "rls'"*)
    3.16        srls      : rls,        (*for evaluating list expressions in scr*)
    3.17 @@ -424,7 +429,12 @@
    3.18  	       term));   (* id | struct-var  *)
    3.19  val e_pbt_ = ("#Undef", (e_term, e_term)):pbt_;
    3.20  type pbt = 
    3.21 -     {thy   : theory,     (* which allows to compile that pbt
    3.22 +     {(*TODO.WN0511: 
    3.23 +       unid  : string      (*unique within this isac-knowledge*)
    3.24 +       author: string      (*copyright*)
    3.25 +       init  : pblID       (*to start refinement with*)
    3.26 +       *)
    3.27 +      thy   : theory,     (* which allows to compile that pbt
    3.28  			  TODO: search generalized for subthy (ref.p.69*)
    3.29        (*^^^ WN050912 NOT used during application of the problem,
    3.30         because applied terms may be from 'subthy' as well as from super;

     4.1 --- a/src/sml/ROOT.ML	Fri Nov 18 19:19:22 2005 +0100
     4.2 +++ b/src/sml/ROOT.ML	Fri Nov 25 16:15:11 2005 +0100
     4.3 @@ -2,6 +2,7 @@
     4.4     (c) Walther Neuper 1997
     4.5  
     4.6    /usr/local/Isabelle2002/bin/isabelle HOL-Real-Isac
     4.7 +  cd"/home/neuper/proto2/isac/src/sml";
     4.8  
     4.9    /usr/local/Isabelle2002/bin/isabelle HOL-Real
    4.10    cd"~/proto2/isac/src/sml";

     5.1 --- a/src/sml/library.sml	Fri Nov 18 19:19:22 2005 +0100
     5.2 +++ b/src/sml/library.sml	Fri Nov 25 16:15:11 2005 +0100
     5.3 @@ -49,6 +49,11 @@
     5.4  fun and_ (b1,b2) = b1 andalso b2;(* ~/Design.98/ModelSpec.sml/library_G.sml *) 
     5.5  fun or_ (b1,b2) = b1 orelse b2;
     5.6  fun takerest (i, ls) = (rev o take) (length ls - i, rev ls);
     5.7 +fun takelast (i, ls) = (rev o take) (i, rev ls);
     5.8 +(* > takelast (2, ["normalize","polynomial","univariate","equation"]);
     5.9 +val it = ["univariate", "equation"] : pblID
    5.10 +> takelast (2,["equation"]);
    5.11 +val it = ["equation"] : pblID*)
    5.12  fun pair2tri ((a,b),c) = (a,b,c);
    5.13  fun fst3 (a,_,_) = a;
    5.14  fun snd3 (_,b,_) = b;

     6.1 --- a/src/smltest/FE-interface/interface.sml	Fri Nov 18 19:19:22 2005 +0100
     6.2 +++ b/src/smltest/FE-interface/interface.sml	Fri Nov 25 16:15:11 2005 +0100
     6.3 @@ -1,5 +1,4 @@
     6.4 -(* use"../systest/interface.sml";
     6.5 -   use"systest/interface.sml";
     6.6 +(* use"../smltest/FE-interface/interface.sml";
     6.7     use"interface.sml";
     6.8  
     6.9  tests the interface of isac's SML-kernel in accordance to 
    6.10 @@ -622,6 +621,9 @@
    6.11   setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = 2)");
    6.12   autoCalculate 1 (Step 1); 
    6.13  
    6.14 + "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
    6.15 + initMatchProblem 1; 
    6.16 +
    6.17   "--------- this match will show some incomplete items: ---------";
    6.18   tryMatchProblem 1 ["univariate","equation"];
    6.19