(* interpreter for scripts

   (c) Walther Neuper 2000

use"~/proto2/isac/src/sml/ME/script.sml";

*)

signature INTERPRETER =

sig

  (*type ets (list of executed tactics) see sequent.sml*)

  datatype locate

    = NotLocatable

    | Steps of (tac_ * mout * ptree * pos' * cid * safe (* ets*)) list

(*    | ToDo of ets 28.4.02*)

  (*diss: next-tactic-function*)

  val next_tac : theory' -> ptree * pos' -> metID -> scr -> ets -> tac_

  (*diss: locate-function*)

  val locate_gen : theory'

                   -> tac_

                      -> ptree * pos' -> scr * rls -> ets -> loc_ -> locate

  val sel_rules : ptree -> pos' -> tac list

  val init_form : scr -> ets -> loc_ * term option (*FIXME not up to date*)

  val formal_args : term -> term list

  (*shift to library ...*)

  val inst_abs : theory' -> term -> term

  val itms2args : metID -> itm list -> term list

  val user_interrupt : loc_ * (tac_ * env * env * term * term * safe)

  (*val empty : term*) 

end 

(*

structure Interpreter : INTERPRETER =

struct

*)

val string_of_thm' = (implode o tl o drop_last o explode o string_of_thm);

(*

  string_of_thm sym;

val it = "\"?s = ?t ==> ?t = ?s\"" : string

  string_of_thm' sym;

val it = "?s = ?t ==> ?t = ?s" : string*)

type step =     (*data for creating a new node in the ptree;

		 designed for use:

               	 fun ass* scrstate steps =

               	 ... case ass* scrstate steps of

               	     Assoc (scrstate, steps) => ... ass* scrstate steps*)

    tac_       (*transformed from associated tac*)

    * mout       (*result with indentation etc.*)

    * ptree      (*containing node created by tac_ + resp. scrstate*)

    * pos'       (*position in ptree; ptree * pos' is the proofstate*)

    * pos' list; (*of ptree-nodes probably cut (by fst tac_)*)

val e_step = (Empty_Tac_, EmptyMout, EmptyPtree, e_pos',[]:pos' list):step;

fun rule2thm' (Thm (id, thm)) = (id, string_of_thm thm):thm'

  | rule2thm' r = raise error ("rule2thm': not defined for "^(rule2str r));

(*.makes a (rule,term) list to a Step (m, mout, pt', p', cid) for solve;

   complicated with current t in rrlsstate.*)

fun rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) [(r, (f', am))] =

    let val thy = assoc_thy thy'

	val m = Rewrite' (thy',ro,er,pa, rule2thm' r, f, (f', am))

	val is = RrlsState (f',f'',rss,rts)

	val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)

	val (p', cid, mout, pt') = generate1 thy m is p pt

    in (is, (m, mout, pt', p', cid)::steps) end

  | rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) 

	      ((r, (f', am))::rts') =

    let val thy = assoc_thy thy'

	val m = Rewrite' (thy',ro,er,pa, rule2thm' r, f, (f', am))

	val is = RrlsState (f',f'',rss,rts)

	val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)

	val (p', cid, mout, pt') = generate1 thy m is p pt

    in rts2steps ((m, mout, pt', p', cid)::steps) 

		 ((pt',p'),(f',f'',rss,rts),(thy',ro,er,pa)) rts' end;

val trace_locate = ref false; (*23.11.01*)

(*. functions for the environment stack .*)

fun accessenv id es = the (assoc((top es):env, id))

    handle _ => error ("accessenv: "^(free2str id)^" not in env");

fun updateenv id vl (es:env stack) = 

    (push (overwrite(top es, (id, vl))) (pop es)):env stack;

fun pushenv id vl (es:env stack) = 

    (push (overwrite(top es, (id, vl))) es):env stack;

val popenv = pop:env stack -> env stack;

fun de_esc_underscore str =

  let fun scan [] = []

	| scan (s::ss) = if s = "'" then (scan ss)

			 else (s::(scan ss))

  in (implode o scan o explode) str end;

(*

> val str = "Rewrite_Set_Inst";

> val esc = esc_underscore str;

val it = "Rewrite'_Set'_Inst" : string

> val des = de_esc_underscore esc;

 val des = de_esc_underscore esc;*)

(*WN.12.5.03 not used any more,

  tacs are more stable than listepxr: subst_tacexpr

fun is_listexpr t = 

  (((ids_of o head_of) t) inter (!listexpr)) <> [];

----*)

(*go at a location in a script and fetch the contents*)

fun go [] t = t

  | go (D::p) (Abs(s,ty,t0)) = go (p:loc_) t0

  | go (L::p) (t1 $ t2) = go p t1

  | go (R::p) (t1 $ t2) = go p t2

  | go l _ = raise error ("go: no "^(loc_2str l));

(*

> val t = (term_of o the o (parse thy)) "a+b";

val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term

> val plus_a = go [L] t; 

> val b = go [R] t; 

> val plus = go [L,L] t; 

> val a = go [L,R] t;

> val t = (term_of o the o (parse thy)) "a+b+c";

val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term

> val pl_pl_a_b = go [L] t; 

> val c = go [R] t; 

> val a = go [L,R,L,R] t; 

> val b = go [L,R,R] t; 

*)

(* get a subterm t with test t, and record location *)

fun get l test (t as Const (s,T)) = 

    if test t then Some (l,t) else None

  | get l test (t as Free (s,T)) = 

    if test t then Some (l,t) else None 

  | get l test (t as Bound n) =

    if test t then Some (l,t) else None 

  | get l test (t as Var (s,T)) =

    if test t then Some (l,t) else None

  | get l test (t as Abs (s,T,body)) =

    if test t then Some (l:loc_,t) else get ((l@[D]):loc_) test body

  | get l test (t as t1 $ t2) =

    if test t then Some (l,t) 

    else case get (l@[L]) test t1 of 

      None => get (l@[R]) test t2

    | Some (l',t') => Some (l',t');

(*18.6.00

> val sss = ((term_of o the o (parse thy))

  "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\

   \ (let e_ = Try (Rewrite square_equation_left True eq_) \

   \  in [e_])");

          ______ compares head_of !!

> get [] (eq_str "Let") sss;            [R]

> get [] (eq_str "Script.Try") sss;     [R,L,R]

> get [] (eq_str "Script.Rewrite") sss; [R,L,R,R]

> get [] (eq_str "True") sss;           [R,L,R,R,L,R]

> get [] (eq_str "e_") sss;             [R,R]

*)

fun test_negotiable t = ((strip_thy o (term_str Script.thy) o head_of) t) 

  mem (!negotiable);

(*30.4.02: vvv--- doesnt work with curried functions ---> get_tac ------

(*18.6.00: below _ALL_ negotiables must be in fun-patterns !

  then the last (non)pattern must be a subproblem*)

fun init_frm thy (Const ("Script.Rewrite",_) $ _ $ _ $ eq) = Some eq

  | init_frm thy (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ eq) = Some eq

  | init_frm thy (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ eq) = Some eq

  | init_frm thy (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ eq) = 

    Some eq

  | init_frm thy (Const ("Script.Calculate",_) $ _ $ t) = Some t

  | init_frm thy t = 

  (*if ((strip_thy o (term_str thy) o head_of) t) mem (!subpbls)

    then None 

  else *)raise error ("init_frm: not impl. for "^

		    (Sign.string_of_term (sign_of thy) t));

> val t = (term_of o the o (parse thy)) 

 "Rewrite square_equation_left True (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))";

> val Some ini = init_frm thy t;

> Sign.string_of_term (sign_of thy) ini;

val it = "sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)" : string

> val t = (term_of o the o (parse thy)) 

 "solve_univar (Reals, [univar,equation], no_met) e1_ v1_";

> val ini = init_frm thy t;

> Sign.string_of_term (sign_of thy) ini;

val it = "empty" : string

> val t = (term_of o the o (parse thy)) 

 "Rewrite_Set norm_equation False x + #1 = #2";

> val Some ini = init_frm thy t;

> Sign.string_of_term (sign_of thy) ini;

val it = "x + #1 = #2" : string                                                

> val t = (term_of o the o (parse thy)) 

 "Rewrite_Set_Inst [(bdv,x)] isolate_bdv False x + #1 = #2";

> val Some ini = init_frm thy t;

> Sign.string_of_term (sign_of thy) ini;

val it = "x + #1 = #2" : string                           *)

(*.get argument of first stactic in a script for init_form.*)

fun get_stac thy (h $ body) =

(* 

   *)

  let

    fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a = 

    	(case get_t y e1 a of None => get_t y e2 a | la => la)

      | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ = 

    	(case get_t y e1 a of None => get_t y e2 a | la => la)

      | get_t y (Const ("Script.Try",_) $ e) a = get_t y e a

      | get_t y (Const ("Script.Try",_) $ e $ a) _ = get_t y e a

      | get_t y (Const ("Script.Repeat",_) $ e) a = get_t y e a

      | get_t y (Const ("Script.Repeat",_) $ e $ a) _ = get_t y e a

      | get_t y (Const ("Script.Or",_) $e1 $ e2) a =

    	(case get_t y e1 a of None => get_t y e2 a | la => la)

      | get_t y (Const ("Script.Or",_) $e1 $ e2 $ a) _ =

    	(case get_t y e1 a of None => get_t y e2 a | la => la)

      | get_t y (Const ("Script.While",_) $ c $ e) a = get_t y e a

      | get_t y (Const ("Script.While",_) $ c $ e $ a) _ = get_t y e a

      | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a = 

    	(case get_t y e1 a of None => get_t y e2 a | la => la)

    (*| get_t y (Const ("Let",_) $ e1 $ Abs (_,_,e2)) a =

    	(writeln("get_t: Let e1= "^(term2str e1)^", e2= "^(term2str e2));

	 case get_t y e1 a of None => get_t y e2 a | la => la)

      | get_t y (Abs (_,_,e)) a = get_t y e a*)

      | get_t y (Const ("Let",_) $ e1 $ Abs (_,_,e2)) a =

    	get_t y e1 a (*don't go deeper without evaluation !*)

      | get_t y (Const ("If",_) $ c $ e1 $ e2) a = None

    	(*(case get_t y e1 a of None => get_t y e2 a | la => la)*)

      | get_t y (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = Some a

      | get_t y (Const ("Script.Rewrite",_) $ _ $ _    ) a = Some a

      | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = Some a

      | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ )    a = Some a

      | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ = Some a

      | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ )    a = Some a

      | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =Some a

      | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ )  a =Some a

      | get_t y (Const ("Script.Calculate",_) $ _ $ a) _ = Some a

      | get_t y (Const ("Script.Calculate",_) $ _ )    a = Some a

      | get_t y (Const ("Script.Substitute",_) $ _ $ a) _ = Some a

      | get_t y (Const ("Script.Substitute",_) $ _ )    a = Some a

      | get_t y (Const ("Script.SubProblem",_) $ _ $ _) _ = None

      | get_t y x _ =  

	((*writeln ("### get_t yac: list-expr "^(term2str x));*)

	 None)

in get_t thy body e_term end;

(*FIXME: get 1st stac by next_stac [] instead of ... ?? 29.7.02*)

(* val Script sc = scr;

   *)

fun init_form thy (Script sc) env =

  (case get_stac thy sc of

     None => None (*raise error ("init_form: no 1st stac in "^

			  (Sign.string_of_term (sign_of thy) sc))*)

   | Some stac => Some (subst_atomic env stac))

  | init_form _ _ _ = raise error "init_form: no match";

(* use"ME/script.sml";

   use"script.sml";

   *)

(*the 'iteration-argument' of a stac (args not eval)*)

fun itr_arg _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ v) = v

  | itr_arg _ (Const ("Script.Rewrite",_) $ _ $ _ $ v) = v

  | itr_arg _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ v) = v

  | itr_arg _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ v) = v

  | itr_arg _ (Const ("Script.Calculate",_) $ _ $ v) = v

  | itr_arg _ (Const ("Script.Check'_elementwise",_) $ consts $ _) = consts

  | itr_arg _ (Const ("Script.Or'_to'_List",_) $ _) = e_term

  | itr_arg _ (Const ("Script.Tac",_) $ _) = e_term

  | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term

  | itr_arg thy t = raise error 

    ("itr_arg not impl. for "^

     (Sign.string_of_term (sign_of (assoc_thy thy)) t));

(* val t = (term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";

> itr_arg "Script.thy" t;

val it = Free ("e_","RealDef.real") : term 

> val t = (term_of o the o (parse thy))"xxx";

> itr_arg "Script.thy" t;

*** itr_arg not impl. for xxx

uncaught exception ERROR

  raised at: library.ML:1114.35-1114.40*)

(*.get the arguments of the script out of the scripts parsetree.*)

fun formal_args scr = (fst o split_last o snd o strip_comb) scr;

(*

> formal_args scr;

  [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),

   Free ("eqs_","bool List.list")] : term list

*)

(*.get the identifier of the script out of the scripts parsetree.*)

fun id_of_scr sc = (id_of o fst o strip_comb) sc;

(*26.5.02: not clear, when a is available in ass_up for eva-_true*)

fun upd_env_opt env (Some a, v) = upd_env env (a,v)

  | upd_env_opt env (None, v) = 

    (writeln("*** upd_env_opt: (None,"^(term2str v)^")");env);

type dsc = typ; (*<-> nam..unknow in Descript.thy*)

fun typ_str (Type (s,_)) = s

  | typ_str (TFree(s,_)) = s

  | typ_str (TVar ((s,i),_)) = s^(string_of_int i);

(*get the _result_-type of a description*)

fun dsc_valT (Const (_,(Type (_,[_,T])))) = (strip_thy o typ_str) T;

(*> val t = (term_of o the o (parse thy)) "equality";

> val T = type_of t;

val T = "bool => Tools.una" : typ

> val dsc = dsc_valT t;

val dsc = "una" : string

> val t = (term_of o the o (parse thy)) "fixedValues";

> val T = type_of t;

val T = "bool List.list => Tools.nam" : typ

> val dsc = dsc_valT t;

val dsc = "nam" : string*)

(*.from penv in itm_ make args for script depending on type of description.*)

(*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv

  9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*)

fun mk_arg thy d [] = raise error ("mk_arg: no data for "^

			       (Sign.string_of_term (sign_of thy) d))

  | mk_arg thy d [t] = 

    (case dsc_valT d of

	 "una" => [t]

       | "nam" => 

	 [case t of

	      r as (Const ("op =",_) $ _ $ _) => r

	    | _ => raise error 

			     ("mk_arg: dsc-typ 'nam' applied to non-equality "^

			      (Sign.string_of_term (sign_of thy) t))]

       | s => raise error ("mk_arg: not impl. for "^s))

  | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts);

(* 

 val d = d_in itm_;

 val [t] = ts_in itm_;

mk_arg thy

*)

(*.create the actual parameters (args) of script: their order 

  is given by the order in met.pat .*)

(*WN.5.5.03: ?: does this allow for different descriptions ???

             ?: why not taken from formal args of script ???

!: FIXXXME penv: push it here in itms2args into script-evaluation*)

(* val (thy, mI, itms) = (thy, metID, itms);

   *)

fun itms2args thy mI (itms:itm list) =

    let val mvat = max_vt itms

	fun okv mvat (_,vats,b,_,_) = mvat mem vats andalso b

	val itms = filter (okv mvat) itms

	fun test_dsc d (_,_,_,_,itm_) = (d = d_in itm_)

	fun itm2arg itms (_,(d,_)) =

	    case find_first (test_dsc d) itms of

		None => 

		raise error ("itms2args: '"^term2str d^"' not in itms")

	      (*| Some (_,_,_,_,itm_) => mk_arg thy (d_in itm_) (ts_in itm_);

               penv postponed; presently penv holds already env for script*)

	      | Some (_,_,_,_,itm_) => penvval_in itm_

	fun sel_given_find (s,_) = (s = "#Given") orelse (s = "#Find")

	val pats = (#ppc o get_met) mI

    in (flat o (map (itm2arg itms))) pats end;

(*

> val sc = ... Solve_root_equation ...

> val mI = ("Script.thy","sqrt-equ-test");

> val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];

> val ts = itms2args thy mI itms;

> map (Sign.string_of_term (sign_of thy)) ts;

["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list

*)

(*["bool_ (1+x=2)","real_ x"] --match_ags--> oris 

  --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"]*)

fun oris2fmz_vals oris =

    let fun ori2fmz_vals ((_,_,_,dsc,ts):ori) = 

	    ((term2str o comp_dts') (dsc, ts), last_elem ts) 

	    handle _ => raise error ("ori2fmz_env called with "^terms2str ts)

    in (split_list o (map ori2fmz_vals)) oris end;

(*detour necessary, because generate1 delivers a string-result*)

fun mout2term thy (Form' (FormKF (_,_,_,_,res))) = 

  (term_of o the o (parse (assoc_thy thy))) res

  | mout2term thy (Form' (PpcKF _)) = e_term;(*3.8.01: res of subpbl 

					   at time of detection in script*)

(*.convert a script-tac to a tac (and SubProblem to tac_, too).*)

fun stac2tac_ thy (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ f) =

    let val tid = (de_esc_underscore o strip_thy) thmID

    in (Rewrite (tid, (de_quote o string_of_thm o 

		       (assoc_thm' thy)) (tid,"")), Empty_Tac_) end

(* val (thy,

	mm as(Const ("Script.Rewrite'_Inst",_) $  sub $ Free(thmID,_) $ _ $ f))

     = (assoc_thy th,stac);

   stac2tac_ thy mm;

   assoc_thm' (assoc_thy "Isac.thy") (tid,"");

   assoc_thm' Isac.thy (tid,"");

   *)

  | stac2tac_ thy (Const ("Script.Rewrite'_Inst",_) $ 

	       sub $ Free (thmID,_) $ _ $ f) =

  let val subML = ((map isapair2pair) o isalist2list) sub

    val subStr = subst2subs subML

    val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)

  in (Rewrite_Inst 

	  (subStr, (tid, (de_quote o string_of_thm o

			  (assoc_thm' thy)) (tid,""))), Empty_Tac_) end

  | stac2tac_ thy (Const ("Script.Rewrite'_Set",_) $ Free (rls,_) $ _ $ f)=

  (Rewrite_Set ((de_esc_underscore o strip_thy) rls), Empty_Tac_)

  | stac2tac_ thy (Const ("Script.Rewrite'_Set'_Inst",_) $ 

	       sub $ Free (rls,_) $ _ $ f) =

  let val subML = ((map isapair2pair) o isalist2list) sub;

    val subStr = subst2subs subML;

  in (Rewrite_Set_Inst (subStr,rls), Empty_Tac_) end

  | stac2tac_ thy (Const ("Script.Calculate",_) $ Free (op_,_) $ f) =

  (Calculate op_, Empty_Tac_)

  | stac2tac_ thy (Const ("Script.Take",_) $ t) =

  (Take (term2str t), Empty_Tac_)

  | stac2tac_ thy (Const ("Script.Substitute",_) $ isasub) =

  (Substitute ((subst2subs o isasub2subst) isasub), Empty_Tac_)

(*12.1.01.*)

  | stac2tac_ thy (Const("Script.Check'_elementwise",_) $ _ $ 

		    (set as Const ("Collect",_) $ Abs (_,_,pred))) = 

  (Check_elementwise (Sign.string_of_term (sign_of thy) pred), 

   (*set*)Empty_Tac_)

  | stac2tac_ thy (Const("Script.Or'_to'_List",_) $ _ ) = 

  (Or_to_List, Empty_Tac_)

(*12.1.01.for subproblem_equation_dummy in root-equation *)

  | stac2tac_ thy (Const ("Script.Tac",_) $ Free (str,_)) = 

  (Tac ((de_esc_underscore o strip_thy) str),  Empty_Tac_) 

		    (*L_ will come from pt in appl_in*)

  (*3.12.03 copied from assod SubProblem*)

(* val Const ("Script.SubProblem",_) $

			 (Const ("Pair",_) $

				Free (dI',_) $ 

				(Const ("Pair",_) $ pI' $ mI')) $ ags' =

    str2term 

    "SubProblem (Test_,[linear,univariate,equation,test],[Test,solve_linear])\

    \ [bool_ (-1+x=0), real_ x]";

*)

  | stac2tac_ thy (Const ("Script.SubProblem",_) $

			 (Const ("Pair",_) $

				Free (dI',_) $ 

				(Const ("Pair",_) $ pI' $ mI')) $ ags') =

(*compare "| assod _ (Subproblem'"*)

    let val dI = ((implode o drop_last o explode) dI')^".thy";

	val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';

	val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';

	val ags = isalist2list ags';

	val thy = assoc_thy dI;

	val (pI, pors, mI) = 

	    if mI = ["no_met"] 

	    then let val pors = match_ags thy ((#ppc o get_pbt) pI) ags;

		     val pI' = refine_ori' pors pI;

		 in (pI', pors (*refinement over models with diff.prec only*), 

		     (hd o #met o get_pbt) pI') end

	    else (pI, match_ags thy ((#ppc o get_pbt) pI) ags, mI);

        val (fmz_, vals) = oris2fmz_vals pors;

	val {cas,ppc,thy,...} = get_pbt pI

	val dI = theory2theory' thy (*take dI from _refined_ pbl*)

	val hdl = case cas of

		      None => pblterm dI pI

		    | Some t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t

        val f = subpbl (strip_thy dI) pI

    in (Subproblem (dI, pI),

	Subproblem' ((dI, pI, mI), pors, hdl, fmz_, f))

    end

  | stac2tac_ thy t = raise error 

  ("stac2tac_ TODO: no match for "^

   (Sign.string_of_term (sign_of thy) t));

(*

> val t = (term_of o the o (parse thy)) 

 "Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False (x=a+#1)";

> stac2tac_ t;

val it = Rewrite_Set_Inst ([(#,#)],"isolate_bdv") : tac

> val t = (term_of o the o (parse SqRoot.thy)) 

"(SubProblem (SqRoot_,[equation,univariate],(SqRoot_,solve_linear))\

   \         [bool_ e_, real_ v_])::bool list";

> stac2tac_ SqRoot.thy t;

val it = (Subproblem ("SqRoot.thy",[#,#]),Const (#,#) $ (# $ # $ (# $ #)))

*)

fun stac2tac thy t = (fst o stac2tac_ thy) t;

(*24.6.02 unused, use subst_stac instead !*)

fun is_stac t =

    (stac2tac_ Script.thy t; true)

    handle _ => false;

(*.get the stactics and problems of a script as tacs

  instantiated with the current environment;

  l is the location which generated the given formula.*)

(*WN.12.5.03: quick-and-dirty repair for listexpressions*)

fun is_spec_pos Pbl = true

  | is_spec_pos Met = true

  | is_spec_pos _ = false;

fun sel_rules _ (([],Res):pos') = 

    raise PTREE "no tactics applicable at the end of a calculation"

| sel_rules pt (p,p_) =

  if is_spec_pos p_ 

  then [get_obj g_tac pt p]

  else

    let val pp = par_pblobj pt p;

	val thy' = (get_obj g_domID pt pp):theory';

	val thy = assoc_thy thy';

	val metID = get_obj g_metID pt pp;

	val metID' =if metID =e_metID then(thd3 o snd3)(get_obj g_origin pt pp)

		     else metID;

        val Script sc = (#scr o get_met) metID';

	val ScrState (env,_,_,_,_,_) = get_istate pt (p,p_);

    in map ((stac2tac thy) o rep_stacexpr o 

	    (subst_stacexpr env None e_term)) (stacpbls sc) end;

(*

> val Script sc = (#scr o get_met) ("SqRoot.thy","sqrt-equ-test");

> val env = [((term_of o the o (parse Isac.thy)) "bdv",

             (term_of o the o (parse Isac.thy)) "x")];

> map ((stac2tac thy) o (subst_stacexpr env None e_term)) (stacpbls sc);

*)

(*test a term for being a _list_ (set ?) of constants; could be more rigorous*)

fun list_of_consts (Const ("List.list.Cons",_) $ _ $ _) = true

  | list_of_consts (Const ("List.list.Nil",_)) = true

  | list_of_consts _ = false;

(*val ttt = (term_of o the o (parse thy)) "[x=#1,x=#2,x=#3]";

> list_of_consts ttt;

val it = true : bool

> val ttt = (term_of o the o (parse thy)) "[]";

> list_of_consts ttt;

val it = true : bool*)

(* 15.1.01: evaluation of preds only works occasionally,

            but luckily for the 2 examples of root-equ:

> val s = ((term_of o the o (parse thy)) "x",

	   (term_of o the o (parse thy)) "-#5//#12");

> val asm = (term_of o the o (parse thy)) 

             "#0 <= #9 + #4 * x  &  #0 <= sqrt x + sqrt (#-3 + x)";

> val pred = subst_atomic [s] asm;

> rewrite_set_ thy false (cterm_of (sign_of thy) pred);

val it = None : (cterm * cterm list) option !!!!!!!!!!!!!!!!!!!!!!!!!!!!

> eval_true' (string_of_thy thy) "eval_rls" (subst_atomic [s] pred);

val it = false : bool

> val s = ((term_of o the o (parse thy)) "x",

	   (term_of o the o (parse thy)) "#4");

> val asm = (term_of o the o (parse thy)) 

             "#0 <= #9 + #4 * x  &  #0 <= sqrt x + sqrt (#5 + x)";

> val pred = subst_atomic [s] asm;

> rewrite_set_ thy false (cterm_of (sign_of thy) pred);

val it = Some ("True & True",[]) : (cterm * cterm list) option

> eval_true' (string_of_thy thy) "eval_rls" (subst_atomic [s] pred);

val it = true : bool`*)

(*for check_elementwise: take apart the set, ev. instantiate assumptions

fun rep_set thy pt p (set as Const ("Collect",_) $ Abs _) =

  let val (_ $ Abs (bdv,T,pred)) = inst_abs thy set;

    val bdv = Free (bdv,T);

    val pred = if pred <> Const ("Script.Assumptions",bool)

		 then pred 

	       else (mk_and o (map fst)) (get_assumptions_ pt (p,Res))

  in (bdv, pred) end

  | rep_set thy _ _ set = 

    raise error ("check_elementwise: no set "^ (*from script*)

		 (Sign.string_of_term (sign_of thy) set));

(*> val set = (term_of o the o (parse thy)) "{(x::real). Assumptions}";

> val p = [];

> val pt = union_asm pt p [("#0 <= sqrt x + sqrt (#5 + x)",[11]),

                           ("#0 <= #9 + #4 * x",[22]),

			   ("#0 <= x ^^^ #2 + #5 * x",[33]),

			   ("#0 <= #2 + x",[44])];

> val (bdv,pred) = rep_set thy pt p set;

val bdv = Free ("x","RealDef.real") : term

> writeln (Sign.string_of_term (sign_of thy) pred);

((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) &

 #0 <= x ^^^ #2 + #5 * x) &

#0 <= #2 + x

*)

--------------------------------------------11.6.03--was unused*)

datatype ass = 

  Ass of tac_ *  (*SubProblem gets args instantiated in assod*)

	 term      (*for itr_arg,result in ets*)

| AssWeak of tac_ *

	     term  (*for itr_arg,result in ets*)

| NotAss;

(*.assod: tac_ associated with stac w.r.t. d

returns

 Ass    : associated: e.g. thmID in stac = thmID in m

                       +++ arg   in stac = arg   in m

 AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//

 NotAss :             e.g. thmID in stac/=/thmID in m (not =)

8.01:

 tac_ SubProblem with args completed from script

.*)

fun assod d (m as Rewrite_Inst' (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))

  (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $ b $ f_) = 

   if thmID = thmID_ then 

    if f = f_ then ((*writeln"3### assod ..Ass";*)Ass (m,f')) 

    else ((*writeln"3### assod ..AssWeak";*)AssWeak(m, f'))

  else ((*writeln"3### assod ..NotAss";*)NotAss)

  | assod d (m as Rewrite' (thy,rod,rls,put,(thmID,thm),f,(f',asm))) 

  (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =

  ((*writeln("3### assod: stac = "^

	   (Sign.string_of_term (sign_of (assoc_thy thy)) t));

   writeln("3### assod: f(m)= "^

	   (Sign.string_of_term (sign_of (assoc_thy thy)) f));*)

   if thmID = thmID_ then 

    if f = f_ then ((*writeln"3### assod ..Ass";*)Ass (m,f')) 

    else ((*writeln"### assod ..AssWeak";

	  writeln("### assod: f(m)  = "^

		  (Sign.string_of_term (sign_of (assoc_thy thy)) f));

	  writeln("### assod: f(stac)= "^

		  (Sign.string_of_term (sign_of (assoc_thy thy)) f_));*)

	  AssWeak (m,f'))

  else ((*writeln"3### assod ..NotAss";*)NotAss))

(*val f = (term_of o the o (parse thy))"#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0";

> val f'= (term_of o the o (parse thy))"#0+(sqrt(sqrt a))^^^#2=#0";

> val m =   Rewrite'("Script.thy","tless_true","eval_rls",false,

 ("rroot_square_inv",""),f,(f',[]));

> val stac = (term_of o the o (parse thy))

 "Rewrite rroot_square_inv False (#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0)";

> assod e_rls m stac;

val it =

  (Some (Rewrite' (#,#,#,#,#,#,#)),Const ("empty","RealDef.real"),

   Const ("empty","RealDef.real")) : tac_ option * term * term*)

  | assod d (m as Rewrite_Set_Inst' (thy',put,sub,rls,f,(f',asm))) 

  (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_)= 

  if id_rls rls = rls_ then 

    if f = f_ then Ass (m,f') else AssWeak (m,f')

  else NotAss

  | assod d (m as Detail_Set_Inst' (thy',put,sub,rls,f,(f',asm))) 

  (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_)= 

  if id_rls rls = rls_ then 

    if f = f_ then Ass (m,f') else AssWeak (m,f')

  else NotAss

  | assod d (m as Rewrite_Set' (thy,put,rls,f,(f',asm))) 

  (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) = 

  if id_rls rls = rls_ then 

    if f = f_ then Ass (m,f') else AssWeak (m,f')

  else NotAss

  | assod d (m as Detail_Set' (thy,put,rls,f,(f',asm))) 

  (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) = 

  if id_rls rls = rls_ then 

    if f = f_ then Ass (m,f') else AssWeak (m,f')

  else NotAss

  | assod d (m as Calculate' (thy',op_,f,(f',thm'))) 

  (Const ("Script.Calculate",_) $ Free (op__,_) $ f_) = 

  if op_ = op__ then

    if f = f_ then Ass (m,f') else AssWeak (m,f')

  else NotAss

  | assod _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))

    (Const ("Script.Check'_elementwise",_) $ consts' $ _) =

    ((*writeln("### assod Check'_elementwise: consts= "^(term2str consts)^

	     ", consts'= "^(term2str consts'));

     atomty(assoc_thy "Isac.thy")consts; atomty(assoc_thy "Isac.thy")consts';*)

     if consts = consts' then ((*writeln"### assod Check'_elementwise: Ass";*)

			       Ass (m, consts_chkd))

     else ((*writeln"### assod Check'_elementwise: NotAss";*) NotAss))

  | assod _ (m as Or_to_List' (ors, list)) 

	  (Const ("Script.Or'_to'_List",_) $ _) =

	  Ass (m, list) 

  | assod _ (m as Take' term) 

	  (Const ("Script.Take",_) $ _) =

	  Ass (m, term)

  | assod _ (m as Substitute' (_, _, res)) 

	  (Const ("Script.Substitute",_) $ _ $ _) =

	  Ass (m, res) 

(* val t = str2term "Substitute [(x, 3)] (x^^^2 + x + 1)";

   val (Const ("Script.Substitute",_) $ _ $ _) = t;

   *)

  | assod _ (m as Tac_ (thy,f,id,f'))  

    (Const ("Script.Tac",_) $ Free (id',_)) =

    if id = id' then Ass (m, ((term_of o the o (parse thy)) f'))

    else NotAss

(* val t = str2term 

              "SubProblem (DiffApp_,[make,function],[no_met]) \

	      \[real_ m_, real_ v_, bool_list_ rs_]";

 val (Subproblem' ((domID,pblID,metID),_,_,_,f)) = m;

 val (Const ("Script.SubProblem",_) $

		 (Const ("Pair",_) $

			Free (dI',_) $

			(Const ("Pair",_) $ pI' $ mI')) $ ags') = stac;

 *)

  | assod _ (Subproblem' ((domID,pblID,metID),_,_,_,f))

	  (Const ("Script.SubProblem",_) $

		 (Const ("Pair",_) $

			Free (dI',_) $ 

			(Const ("Pair",_) $ pI' $ mI')) $ ags') =

(*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)

    let val dI = ((implode o drop_last o explode) dI')^".thy";

	val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';

	val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';

	val ags = isalist2list ags';

	val thy = assoc_thy dI;

	val (pI, pors, mI) = 

	    if mI = ["no_met"] 

	    then let val pors = match_ags thy ((#ppc o get_pbt) pI) ags;

		     val pI' = refine_ori' pors pI;

		 in (pI', pors (*refinement over models with diff.prec only*), 

		     (hd o #met o get_pbt) pI') end

	    else (pI, match_ags thy ((#ppc o get_pbt) pI) ags, mI);

        val (fmz_, vals) = oris2fmz_vals pors;

	val {cas, ppc,...} = get_pbt pI

	val {cas, ppc, thy,...} = get_pbt pI

	val dI = theory2theory' thy (*take dI from _refined_ pbl*)

	val hdl = case cas of

		      None => pblterm dI pI

		    | Some t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t

        val f = subpbl (strip_thy dI) pI

    in if domID = dI andalso pblID = pI

       then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, f), f) 

       else NotAss

    end

  | assod d m t = 

    (

writeln("### assod: NotAss m= "^(tac_2str m)^" ,\n stac= "^(term2str t));

     NotAss);

fun tac_2tac (Refine_Tacitly' (pI,_,_,_,_)) = Refine_Tacitly pI

  | tac_2tac (Model_Problem' (pI,_))        = Model_Problem pI

  | tac_2tac (Add_Given' (t,_))             = Add_Given t

  | tac_2tac (Add_Find' (t,_))              = Add_Find t

  | tac_2tac (Add_Relation' (t,_))          = Add_Relation t

  | tac_2tac (Specify_Theory' dI)           = Specify_Theory dI

  | tac_2tac (Specify_Problem' (dI,_))      = Specify_Problem dI

  | tac_2tac (Specify_Method' (dI,_,_))     = Specify_Method dI

  | tac_2tac (Rewrite' (thy,rod,erls,put,(thmID,thm),f,(f',asm))) =

    Rewrite (thmID,thm)

  | tac_2tac (Rewrite_Inst' (thy,rod,erls,put,sub,(thmID,thm),f,(f',asm)))=

    Rewrite_Inst (subst2subs sub,(thmID,thm))

  | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) = 

    Rewrite_Set (id_rls rls)

  | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) = 

    Detail_Set (id_rls rls)

  | tac_2tac (Rewrite_Set_Inst' (thy,put,sub,rls,f,(f',asm))) = 

    Rewrite_Set_Inst (subst2subs sub,id_rls rls)

  | tac_2tac (Detail_Set_Inst' (thy,put,sub,rls,f,(f',asm))) = 

    Detail_Set_Inst (subst2subs sub,id_rls rls)

  | tac_2tac (Calculate' (thy,op_,t,(t',thm'))) = Calculate (op_)

  | tac_2tac (Check_elementwise' (consts,pred,consts')) =

    Check_elementwise pred

  | tac_2tac (Or_to_List' _) = Or_to_List

  | tac_2tac (Take' term) = Take (term2str term)

  | tac_2tac (Substitute' (subs, t, res)) = Substitute (subst2subs subs) 

  | tac_2tac (Tac_ (_,f,id,f')) = Tac id

  | tac_2tac (Subproblem' ((domID, pblID, _), _, _,_,_)) = 

		  Subproblem (domID, pblID)

  | tac_2tac (Check_Postcond' (pblID, _)) = 

		  Check_Postcond pblID

  | tac_2tac Empty_Tac_ = Empty_Tac

  | tac_2tac m = 

  raise error ("tac_2tac: not impl. for "^(tac_2str m));

(** decompose tac_ to a rule and to (lhs,rhs)

    unly needed                            ~~~ **)

val idT = Type ("Script.ID",[]);

(*val tt = (term_of o the o (parse thy)) "square_equation_left::ID";

type_of tt = idT;

val it = true : bool

*)

(* 13.3.01

v

*)

fun make_rule thy t =

  let val ct = cterm_of (sign_of thy) (Trueprop $ t)

  in Thm (string_of_cterm ct, make_thm ct) end;

(* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;

   *)

(*decompose tac_ to a rule and to (lhs,rhs) for ets FIXME.12.03: obsolete!

 NOTE.12.03: also used for msg 'not locatable' ?!: 'Subproblem' missing !!!

WN0508 only use in tac_2res, which uses only last return-value*)

fun rep_tac_ (Rewrite_Inst' 

		 (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) = 

  let val fT = type_of f;

    val b = if put then HOLogic.true_const else HOLogic.false_const;

    val sT = (type_of o fst o hd) subs;

    val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))

      (map HOLogic.mk_prod subs);

    val sT' = type_of subs';

    val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,(*fT*)bool,fT] ---> fT) 

      $ subs' $ Free (thmID,idT) $ b $ f;

  in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end

(*Fehlersuche 25.4.01

(a)----- als String zusammensetzen:

ML> Sign.string_of_term (sign_of thy)f; 

val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string

ML> Sign.string_of_term (sign_of thy)f'; 

val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string

ML> subs;

val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst

> val tt = (term_of o the o (parse thy))

  "(Rewrite_Inst[(bdv,x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";

> atomty thy tt;

ML> writeln(Sign.string_of_term (sign_of thy)tt); 

(Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =

 #0 + d_d x (x ^^^ #2 + #3 * x)

(b)----- laut rep_tac_:

> val ttt=HOLogic.mk_eq (lhs,f');

> atomty thy ttt;

(*Fehlersuche 1-2Monate vor 4.01:*)

> val tt = (term_of o the o (parse thy))

  "Rewrite_Inst[(bdv,x)]square_equation_left True(x=#1+#2)";

> atomty thy tt;

> val f = (term_of o the o (parse thy)) "x=#1+#2";

> val f' = (term_of o the o (parse thy)) "x=#3";

> val subs = [((term_of o the o (parse thy)) "bdv",

	       (term_of o the o (parse thy)) "x")];

> val sT = (type_of o fst o hd) subs;

> val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))

			      (map HOLogic.mk_prod subs);

> val sT' = type_of subs';

> val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT) 

  $ subs' $ Free (thmID,idT) $ HOLogic.true_const $ f;

> lhs = tt;

val it = true : bool

> rep_tac_ (Rewrite_Inst' 

	       ("Script.thy","tless_true","eval_rls",false,subs,

		("square_equation_left",""),f,(f',[])));

*)

  | rep_tac_ (Rewrite' (thy',rod,rls,put,(thmID,thm),f,(f',asm)))=

  let 

    val fT = type_of f;

    val b = if put then HOLogic.true_const else HOLogic.false_const;

    val lhs = Const ("Script.Rewrite",[idT,HOLogic.boolT,fT] ---> fT)

      $ Free (thmID,idT) $ b $ f;

  in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end

(* 

> val tt = (term_of o the o (parse thy)) (*____   ____..test*)

  "Rewrite square_equation_left True (x=#1+#2) = (x=#3)";

> val f = (term_of o the o (parse thy)) "x=#1+#2";

> val f' = (term_of o the o (parse thy)) "x=#3";

> val Thm (id,thm) = 

  rep_tac_ (Rewrite' 

   ("Script.thy","tless_true","eval_rls",false,

    ("square_equation_left",""),f,(f',[])));

> val Some ct = parse thy   

  "Rewrite square_equation_left True (x=#1+#2)"; 

> rewrite_ Script.thy tless_true eval_rls true thm ct;

val it = Some ("x = #3",[]) : (cterm * cterm list) option

*)

  | rep_tac_ (Rewrite_Set_Inst' 

		 (thy',put,subs,rls,f,(f',asm))) =

    (e_rule, (e_term, f'))

(*WN050824: type error ...

  let val fT = type_of f;

    val sT = (type_of o fst o hd) subs;

    val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))

      (map HOLogic.mk_prod subs);

    val sT' = type_of subs';

    val b = if put then HOLogic.true_const else HOLogic.false_const

    val lhs = Const ("Script.Rewrite'_Set'_Inst",

		     [sT',idT,fT,fT] ---> fT) 

      $ subs' $ Free (id_rls rls,idT) $ b $ f;

  in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end*)

(* ... vals from Rewrite_Inst' ...

> rep_tac_ (Rewrite_Set_Inst' 

	       ("Script.thy",false,subs,

		"isolate_bdv",f,(f',[])));

*)

(* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m;

*)

  | rep_tac_ (Rewrite_Set' (thy',put,rls,f,(f',asm)))=

  let val fT = type_of f;

    val b = if put then HOLogic.true_const else HOLogic.false_const;

    val lhs = Const ("Script.Rewrite'_Set",[idT,bool,fT] ---> fT) 

      $ Free (id_rls rls,idT) $ b $ f;

  in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end

(* 13.3.01:

val thy = assoc_thy thy';

val t = HOLogic.mk_eq (lhs,f');

make_rule thy t;

--------------------------------------------------

val lll = (term_of o the o (parse thy)) 

  "Rewrite_Set SqRoot_simplify False (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";

--------------------------------------------------

> val f = (term_of o the o (parse thy)) "x=#1+#2";

> val f' = (term_of o the o (parse thy)) "x=#3";

> val Thm (id,thm) = 

  rep_tac_ (Rewrite_Set' 

   ("Script.thy",false,"SqRoot_simplify",f,(f',[])));

val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string

val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm

*)

  | rep_tac_ (Calculate' (thy',op_,f,(f',thm')))=

  let val fT = type_of f;

    val lhs = Const ("Script.Calculate",[idT,fT] ---> fT) 

      $ Free (op_,idT) $ f

  in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end

(*

> val lhs'=(term_of o the o (parse thy))"Calculate plus (#1+#2)";

  ... test-root-equ.sml: calculate ...

> val Appl m'=applicable_in p pt (Calculate "plus");

> val (lhs,_)=tac_2etac m';

> lhs'=lhs;

val it = true : bool*)

  | rep_tac_ (Check_elementwise' (t,str,(t',asm)))  = (Erule, (e_term, t'))

  | rep_tac_ (Subproblem' (_,_,_,_,t'))  = (Erule, (e_term, t'))

  | rep_tac_ (Take' (t'))  = (Erule, (e_term, t'))

  | rep_tac_ (Substitute' (subst,t,t'))  = (Erule, (e_term, t'))

  | rep_tac_ (Or_to_List' (t, t'))  = (Erule, (t, t'))

  | rep_tac_ m = raise error ("rep_tac_: not impl.for "^

				 (tac_2str m));