1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Wed Apr 06 18:01:02 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Thu Apr 07 16:31:05 2011 +0200
     1.3 @@ -162,7 +162,7 @@
     1.4      val pt_model : ppobj -> pos_ -> ptform
     1.5      val reset_calchead : ptree * pos' -> ptree * pos'
     1.6      val seek_oridts :
     1.7 -       theory ->
     1.8 +       Proof.context ->
     1.9         string ->
    1.10         Term.term * Term.term list ->
    1.11         (int * SpecifyTools.vats * string * Term.term * Term.term list) list
    1.12 @@ -205,11 +205,9 @@
    1.13  
    1.14  
    1.15  
    1.16 -(*---------------------------------------------------------------------
    1.17  structure CalcHead (**): CALC_HEAD(**) =
    1.18  
    1.19  struct
    1.20 ----------------------------------------------------------------------*)
    1.21  
    1.22  (* datatypes *)
    1.23  
    1.24 @@ -276,18 +274,6 @@
    1.25  
    1.26  (*.to an input (d,ts) find the according ori and insert the ts.*)
    1.27  (*WN.11.03: + dont take first inter<>[]*)
    1.28 -(*fun seek_oridts ctxt sel (d,ts) [] =
    1.29 -    ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
    1.30 -                             (comp_dts (d,ts))) ^
    1.31 -     "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
    1.32 -     [])
    1.33 -  | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
    1.34 -    if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
    1.35 -	 then ("", 
    1.36 -               (id,vat,sel,d, inter op = ts ts'):ori, 
    1.37 -               ts')
    1.38 -    else seek_oridts ctxt sel (d,ts) oris;*)
    1.39 -
    1.40  fun seek_oridts ctxt sel (d,ts) [] =
    1.41      ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
    1.42                               (comp_dts (d,ts))) ^
    1.43 @@ -791,10 +777,10 @@
    1.44  fun appl_add ctxt sel [] ppc pbt t =
    1.45        let
    1.46          val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
    1.47 -      in case parseNEW ctxt t of
    1.48 +      in case parse (ProofContext.theory_of ctxt) t of
    1.49            NONE => Add (i, [], false, sel, Syn t)
    1.50          | SOME t' =>
    1.51 -          let val (d, ts) = split_dts t';
    1.52 +          let val (d, ts) = split_dts (term_of t');
    1.53            in if d = e_term then
    1.54              Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
    1.55              (case find_first (eq1 d) pbt of
    1.56 @@ -820,9 +806,9 @@
    1.57              end
    1.58        end
    1.59    | appl_add ctxt sel oris ppc pbt str =
    1.60 -      case parseNEW ctxt str of
    1.61 +      case parse (ProofContext.theory_of ctxt) str of
    1.62            NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
    1.63 -        | SOME t => case is_known ctxt sel oris t of
    1.64 +        | SOME t => case is_known ctxt sel oris (term_of t) of
    1.65              ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
    1.66                ("", itm) => Add itm
    1.67                | (msg, _) => Err msg)
    1.68 @@ -1066,7 +1052,7 @@
    1.69      end
    1.70  (* val (p,_) = p;
    1.71     *)
    1.72 -| specify_additem sel (ct,_) (p,p_(*Frm, Pbl*)) c pt = 
    1.73 +| specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt = 
    1.74      let
    1.75        val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
    1.76  		  probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
    1.77 @@ -1127,10 +1113,9 @@
    1.78  fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)= 
    1.79    let          (* either """"""""""""""" all empty or complete *)
    1.80      val thy = assoc_thy dI';
    1.81 -    val (istate_, ctxt) = (#ppc o get_pbt) pI' |> prep_ori fmz thy;
    1.82      val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
    1.83 -	       else istate_;
    1.84 -    val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
    1.85 +	       else pI' |> #ppc o get_pbt |> prep_ori fmz thy |> #1;
    1.86 +    val (pt,c) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz,(dI',pI',mI'))
    1.87  				 (oris,(dI',pI',mI'),e_term);
    1.88      val {ppc,prls,where_,...} = get_pbt pI'
    1.89      (*val pbl = init_pbl ppc;  WN.9.03: done in Model/Refine_Problem
    1.90 @@ -1579,7 +1564,7 @@
    1.91  	let val {ppc,...} = get_met mI
    1.92  	    val dI = if dI = "" then "Isac" else dI
    1.93  	    val thy = assoc_thy dI;
    1.94 -	    val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
    1.95 +	    val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
    1.96  					 ([], (dI,pI,mI), e_term(*FIXME met*));
    1.97  	    val pt = update_spec pt [] (dI,pI,mI);
    1.98  	    val mits = init_pbl' ppc;
    1.99 @@ -1601,12 +1586,11 @@
   1.100  	    else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy |> #1, mI)
   1.101  	val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
   1.102  	val dI = theory2theory' (maxthy thy thy');
   1.103 -	val ctxt = prep_ori fmz thy ppc |> #2;
   1.104  	val hdl = case cas of
   1.105  		      NONE => pblterm dI pI
   1.106  		    | SOME t => subst_atomic ((vars_of_pbl_' ppc) 
   1.107  						  ~~~ vals_of_oris pors) t;
   1.108 -        val (pt, _) = cappend_problem e_ptree [] (Uistate, ctxt) (fmz, (dI, pI, mI))
   1.109 +        val (pt, _) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz, (dI, pI, mI))
   1.110  				      (pors, (dI, pI, mI), hdl)
   1.111      in ((pt, ([], Pbl)), 
   1.112          fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
   1.113 @@ -2081,9 +2065,6 @@
   1.114  	val pt = update_spec pt p e_spec
   1.115      in (pt, (p,Pbl):pos') end;
   1.116  
   1.117 -(*---------------------------------------------------------------------
   1.118  end
   1.119  
   1.120  open CalcHead;
   1.121 ----------------------------------------------------------------------*)
   1.122 -

     2.1 --- a/src/Tools/isac/Interpret/ctree.sml	Wed Apr 06 18:01:02 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Thu Apr 07 16:31:05 2011 +0200
     2.3 @@ -567,8 +567,7 @@
     2.4  		     itm list   (*... updated from pbl to met*)
     2.5  | Apply_Method' of metID * 
     2.6  		   (term option) * (*init_form*)
     2.7 -		   istate	*
     2.8 -       Proof.context	        
     2.9 +		   istate * Proof.context
    2.10  | Check_Postcond' of 
    2.11    pblID * 
    2.12    (term *      (*returnvalue of script in solve*)

     3.1 --- a/src/Tools/isac/Interpret/generate.sml	Wed Apr 06 18:01:02 2011 +0200
     3.2 +++ b/src/Tools/isac/Interpret/generate.sml	Thu Apr 07 16:31:05 2011 +0200
     3.3 @@ -409,11 +409,10 @@
     3.4    let val (pt,c) = cappend_form pt p l f 
     3.5        val pt = update_branch pt p TransitiveB (*040312*)
     3.6  
     3.7 -      val ctxt = e_ctxt;
     3.8        val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f 
     3.9 -      val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt)
    3.10 +      val tac_ = Apply_Method' (e_metID, SOME t, is, e_ctxt)
    3.11        val pos' = ((lev_on o lev_dn) p, Frm)
    3.12 -  in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
    3.13 +  in (*implicit Take*) generate1 thy tac_ (is, e_ctxt) pos' pt end
    3.14  
    3.15    | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt =
    3.16    let (*val _= tracing("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*)
    3.17 @@ -428,11 +427,10 @@
    3.18    let val (pt,c) = cappend_form pt p l f 
    3.19        val pt = update_branch pt p TransitiveB (*040312*)
    3.20  
    3.21 -      val ctxt = e_ctxt;
    3.22        val is = init_istate (Rewrite_Set (id_rls rls)) f
    3.23 -      val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt)
    3.24 +      val tac_ = Apply_Method' (e_metID, SOME t, is, e_ctxt)
    3.25        val pos' = ((lev_on o lev_dn) p, Frm)
    3.26 -  in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
    3.27 +  in (*implicit Take*) generate1 thy tac_ (is, e_ctxt) pos' pt end
    3.28  
    3.29    | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
    3.30      let (*val _=tracing("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
    3.31 @@ -487,6 +485,7 @@
    3.32      error ("generate1: not impl.for "^(tac_2str m'))
    3.33  ;
    3.34  
    3.35 +
    3.36  fun generate_hard thy m' (p,p_) pt =
    3.37    let  
    3.38      val p = case p_ of Frm => p | Res => lev_on p

     4.1 --- a/src/Tools/isac/Interpret/inform.sml	Wed Apr 06 18:01:02 2011 +0200
     4.2 +++ b/src/Tools/isac/Interpret/inform.sml	Thu Apr 07 16:31:05 2011 +0200
     4.3 @@ -279,12 +279,12 @@
     4.4     *)
     4.5  fun appl_add' dI oris ppc pbt (sel, ct) = 
     4.6      let 
     4.7 -	val ctxt = assoc_thy dI |> thy2ctxt;
     4.8 -	in case parseNEW ctxt ct of
     4.9 +      val ctxt = assoc_thy dI |> thy2ctxt;
    4.10 +    in case parse (ProofContext.theory_of ctxt) ct of
    4.11  	   NONE => (0,[],false,sel, Syn ct):itm
    4.12 -	 | SOME t => (case is_known ctxt sel oris t of
    4.13 -	     ("", ori', all) =>
    4.14 -	       (case is_notyet_input ctxt ppc all ori' pbt of
    4.15 +	 | SOME ct => (case is_known ctxt sel oris (term_of ct) of
    4.16 +         ("", ori', all) =>
    4.17 +           (case is_notyet_input ctxt ppc all ori' pbt of
    4.18  	         ("",itm)  => itm
    4.19  	       | (msg,_) => error ("appl_add': " ^ msg))
    4.20       | (_, (i, v, _, d, ts), _) => if is_e_ts ts then

     5.1 --- a/src/Tools/isac/Interpret/mstools.sml	Wed Apr 06 18:01:02 2011 +0200
     5.2 +++ b/src/Tools/isac/Interpret/mstools.sml	Thu Apr 07 16:31:05 2011 +0200
     5.3 @@ -324,21 +324,6 @@
     5.4       term list *  lists decomposed for elementwise input
     5.5       term list    pbl_ids not _HERE_: dont know which list-elems input*)
     5.6  fun split_dts (t as d $ arg) =
     5.7 -    if is_dsc d
     5.8 -    then if is_list_dsc d
     5.9 -	 then if is_list arg
    5.10 -	      then if is_unl d
    5.11 -		   then (d, [arg])                 (*e.g. someList [1,3,2]*)
    5.12 -		   else (d, take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*)
    5.13 -	      else (d, [arg])      (*a variable or metavariable for a list*)
    5.14 -	 else (d, [arg])
    5.15 -    else (e_term, dest_list' t(*9.01 ???*))
    5.16 -  | split_dts t = (*either dsc or term*)
    5.17 -  let val (h,argl) = strip_comb t
    5.18 -  in if (not o is_dsc) h then (e_term, dest_list' t)
    5.19 -     else (h, dest_list (h,argl))
    5.20 -  end;
    5.21 -(*fun split_dts (t as d $ arg) =
    5.22        if is_dsc d then
    5.23          if is_list_dsc d andalso is_list arg andalso is_unl d |> not then
    5.24            (d, take_apart arg) else
    5.25 @@ -349,7 +334,8 @@
    5.26        in if is_dsc h then
    5.27          (h, dest_list t') else
    5.28          (e_term, dest_list' t)
    5.29 -      end;*)
    5.30 +      end;
    5.31 +
    5.32  (* tests see fun comp_dts 
    5.33  
    5.34  > val t = str2term "someList []";

     6.1 --- a/src/Tools/isac/Interpret/script.sml	Wed Apr 06 18:01:02 2011 +0200
     6.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu Apr 07 16:31:05 2011 +0200
     6.3 @@ -1363,7 +1363,7 @@
     6.4  		  (*WN.12.03: noticed, that pos is also updated in assy !?!
     6.5  		   instead take p' from Assoc ?????????????????????????????*)
     6.6                    val (p'',c'',f'',pt'') = 
     6.7 -		      generate1 thy m (ScrState is, e_ctxt) (po',p_) pt;
     6.8 +		      generate1 thy m (ScrState is, ctxt) (po',p_) pt;
     6.9  	      (*val _=tracing("### locate_gen, aft g1: p''="^(pos'2str p''));*)
    6.10  	      (*drop the intermediate steps !*)
    6.11  	      in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
    6.12 @@ -1382,14 +1382,14 @@
    6.13  		    ((*tracing"4### locate_gen Assoc after Fini";*)
    6.14  		     if rew_only ss
    6.15  		     then let val(p'',c'',f'',pt'') = 
    6.16 -				 generate1 thy m (ScrState is, e_ctxt) p' pt;
    6.17 +				 generate1 thy m (ScrState is, ctxt) p' pt;
    6.18  			  (*drop the intermediate steps !*)
    6.19  			  in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
    6.20  		     else NotLocatable)
    6.21  	      | _ => ((*tracing ("#### locate_gen: after Fini");*)
    6.22  		      NotLocatable))
    6.23    end
    6.24 -  | locate_gen _ m _ (sc,_) (is, ctxt) = 
    6.25 +  | locate_gen _ m _ (sc,_) (is, _) = 
    6.26      error ("locate_gen: wrong arguments,\n tac= "^(tac_2str m)^
    6.27  		 ",\n scr= "^(scr2str sc)^",\n istate= "^(istate2str is));
    6.28  
    6.29 @@ -1777,7 +1777,7 @@
    6.30  	   (true, p', _) => 
    6.31  	   let val (_,pblID,_) = get_obj g_spec pt p';
    6.32  	   in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])), 
    6.33 -	       (e_istate, ctxt), (v,s)) end
    6.34 +	       (e_istate, e_ctxt), (v,s)) end
    6.35  	 | (_,p',rls') => (End_Detail' (e_term,[])(*8.6.03*), (e_istate, e_ctxt), (v,s)))
    6.36      | Napp _ => (Empty_Tac_, (e_istate, e_ctxt), (e_term, Sundef))         (*helpless*)
    6.37      | Appy (m', scrst as (_,_,_,v,_,_)) => (m', (ScrState scrst, e_ctxt),

     7.1 --- a/test/Tools/isac/Interpret/ctree.sml	Wed Apr 06 18:01:02 2011 +0200
     7.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Thu Apr 07 16:31:05 2011 +0200
     7.3 @@ -64,13 +64,13 @@
     7.4  "this build should be detailed each time a test fails later    \
     7.5  \i.e. all the tests should be caught here first                \
     7.6  \and linked with a reference to the respective test environment";
     7.7 -val fmz = ["equality (x + 1 = (2::int))",
     7.8 +val fmz = ["equality (x+1=(2::real))",
     7.9  	   "solveFor x","solutions L"];
    7.10  val (dI',pI',mI') =
    7.11    ("Test",["sqroot-test","univariate","equation","test"],
    7.12     ["Test","squ-equ-test-subpbl1"]);
    7.13  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    7.14 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* error happens here *)
    7.15 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    7.16  (* nxt = Add_Given "equality (x + 1 = 2)"
    7.17     (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
    7.18     *)

     8.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml	Wed Apr 06 18:01:02 2011 +0200
     8.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml	Thu Apr 07 16:31:05 2011 +0200
     8.3 @@ -26,12 +26,9 @@
     8.4  "----------- rewriting for usecase1 ---------------------";
     8.5  "----------- rewriting for usecase1 ---------------------";
     8.6  "----------- rewriting for usecase1 ---------------------";
     8.7 -val subst = let
     8.8 -      val pair = (parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int");
     8.9 -    in case pair of
    8.10 -        (SOME r, SOME s) => [(r,s)]
    8.11 -      | _ => error "diophanteq.sml: syntax error in rewriting for usecase1"
    8.12 -    end;
    8.13 +val subst = case (parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int") of
    8.14 +      (SOME r, SOME s) => [(r,s)]
    8.15 +    | _ => error "diophanteq.sml: syntax error in rewriting for usecase1"
    8.16  val t = case parseNEW ctxt "xxx + 111 = abc + (123::int)" of
    8.17        SOME t' => t'
    8.18      | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";

     9.1 --- a/test/Tools/isac/Test_Isac.thy	Wed Apr 06 18:01:02 2011 +0200
     9.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Apr 07 16:31:05 2011 +0200
     9.3 @@ -16,7 +16,7 @@
     9.4  (*("ProgLang/listg.sml") ("ProgLang/scrtools.sml") ("ProgLang/tools.sml") *)
     9.5  
     9.6    ("Interpret/mstools.sml") 
     9.7 -(*("Interpret/ctree.sml")*)
     9.8 +  ("Interpret/ctree.sml")
     9.9    ("Interpret/ptyps.sml") 
    9.10  (*("Interpret/generate.sml")*)
    9.11    ("Interpret/calchead.sml") 
    9.12 @@ -82,7 +82,7 @@
    9.13    ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
    9.14    ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
    9.15    use "Interpret/mstools.sml"       (*empty*)
    9.16 -(*use "Interpret/ctree.sml"           TODO*)
    9.17 +  use "Interpret/ctree.sml"
    9.18    use "Interpret/ptyps.sml"         (*    *)
    9.19  (*use "Interpret/generate.sml"        new 2011*)
    9.20    use "Interpret/calchead.sml"      (*    *)