(* Title:  interpreter for scripts

   Author: Walther Neuper 2000

   (c) due to copyright terms

*)

signature LUCAS_INTERPRETER_TOOL =

sig

  datatype ass =

    Ass of Tactic.T * term * Proof.context

  | Ass_Weak of Tactic.T * term * Proof.context

  | NotAss;

  val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term) -> ass

  val init_form : 'a -> Program.T -> (term * term) list -> term option

  val init_pstate : Rule.rls -> Proof.context -> Model.itm list -> Celem.metID ->

    Istate.T * Proof.context * Program.T

  val get_simplifier : Calc.T -> Rule.rls

(*vvv initialise : Rule.theory'(*?!?*) -> Calc.T -> (Istate.T * Proof.context) * Program.T*)

  val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> 

    Rule.rls(*..\<in> ist \<rightarrow> REMOVE*) * (Istate.T * Proof.context) * Program.T

  val tac_from_prog : Ctree.ctree -> theory -> term -> Tactic.input

  val check_leaf : string -> Proof.context -> Rule.rls -> (Env.T * (term option * term)) -> term -> 

      Program.leaf * term option

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  (*NONE*)

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

  val itms2args : 'a -> Celem.metID -> Model.itm list -> term list

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end 

(* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step, see "and scr" *)   

val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)

(**)

structure LItool(**): LUCAS_INTERPRETER_TOOL(**) =

struct

(**)

open Ctree

open Pos

(* determine the first tactic in case of a program with one argument (like simplification)

  and without an initial Tactic.Take *)

fun init_form thy (Rule.Prog prog) env =

    (case Prog_Tac.get_first thy prog of

      NONE => NONE 

    | SOME prog_tac => SOME (subst_atomic env prog_tac))

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

type dsc = typ; (* <-> nam..unknow in Descript.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 errmsg = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."

fun errmsg2 d itms = ("itms2args: '" ^ Rule.term2str d ^ "' not in itms:\n" ^

"itms:\n" ^ Model.itms2str_ @{context} itms)

fun itms2args _ mI itms =

  let

    val mvat = Model.max_vt itms

    fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b

    val itms = filter (okv mvat) itms

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

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

        case find_first (test_dsc d) itms of

          NONE => raise ERROR (errmsg2 d itms)

        | SOME (_, _, _, _, itm_) => Model.penvval_in itm_

      (*| SOME (_,_,_,_,itm_) => mk_arg thy (Model.d_in itm_) (ts_in itm_);

            penv postponed; presently penv holds already Env.update for script*)

    val pats = (#ppc o Specify.get_met) mI

    val _ = if pats = [] then raise ERROR errmsg else ()

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

(* convert a Prog_Tac to Tactic.input *)

fun tac_from_prog _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =

    let

      val tid = HOLogic.dest_string thmID

    in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid)) end

  | tac_from_prog _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =

    let

      val tid = HOLogic.dest_string thmID

    in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid))) end

  | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =

     (Tactic.Rewrite_Set (HOLogic.dest_string rls))

  | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =

      (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls))

  | tac_from_prog _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =

      (Tactic.Calculate (HOLogic.dest_string op_))

  | tac_from_prog _ _ (Const ("Prog_Tac.Take", _) $ t) = (Tactic.Take (Rule.term2str t))

  | tac_from_prog _ _ (Const ("Prog_Tac.Substitute", _) $ isasub $ _) =

    (Tactic.Substitute ((Selem.subte2sube o TermC.isalist2list) isasub))

  | tac_from_prog _ thy (Const("Prog_Tac.Check'_elementwise", _) $ _ $ 

    (Const ("Set.Collect", _) $ Abs (_, _, pred))) =

      (Tactic.Check_elementwise (Rule.term_to_string''' thy pred))

  | tac_from_prog _ _ (Const("Prog_Tac.Or'_to'_List", _) $ _ ) = Tactic.Or_to_List

  | tac_from_prog pt _ (ptac as Const ("Prog_Tac.SubProblem", _) $ _ $ _) =

    fst (Sub_Problem.tac_from_prog pt ptac) (*might involve problem refinement etc*)

  | tac_from_prog _ thy t = error ("stac2tac_ TODO: no match for " ^ Rule.term_to_string''' thy t);

datatype ass =

    Ass of

      Tactic.T        (* SubProblem gets args instantiated in associate     *)

      * term          (* for itr_arg, result in ets                         *)

      * Proof.context (* separate from Tactic.T like in locate_input_tactic *)

  | Ass_Weak of Tactic.T * term * Proof.context

  | NotAss;

(* check if tac_ is associated with stac.

   Note: this is the only fun in "fun locate_input_tactic", which handles tactics individually.

   Additional tasks: 

  (1) to "Subproblem'" add "pors, hdl, fmz_, ctxt, f" TODO: ctxt <-?-> sig locate_input_tac

  (2) check if term t (the result has been calculated from) in tac_

   has been changed (see "datatype tac_"); if yes, recalculate result

   TODO.WN120106 recalculate impl.only for Substitute'

args

  pt     : ctree for pushing the thy specified in rootpbl into subpbls

  d      : unused (planned for data for comparison)

  tac_   : from user (via applicable_in); to be compared with ...

  stac   : found in program

returns

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

                       +++ arg   in stac = arg   in m

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

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

*)

fun associate _ ctxt (m as Tactic.Rewrite_Inst'

      (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =

    (case stac of

	    (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) =>

	      if thmID = HOLogic.dest_string thmID_

        then 

	        if f = f_ 

          then Ass (m, f', ContextC.insert_assumptions asms' ctxt)

	        else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)

	      else ((*tracing"3### associate ..NotAss";*) NotAss)

    | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>

	      if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))

        then if f = f_ then Ass (m, f', ContextC.insert_assumptions asms' ctxt)

        else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)

	      else NotAss

    | _ => NotAss)

  | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =

    (case stac of

	    (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) =>

	      if thmID = HOLogic.dest_string thmID_

        then 

	        if f = f_

          then Ass (m, f', ContextC.insert_assumptions asms' ctxt)

	        else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)

	      else NotAss

    | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>

	       if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))

         then

           if f = f_

           then Ass (m, f', ContextC.insert_assumptions asms' ctxt)

	         else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)

	       else NotAss

    | _ => NotAss)

  | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),

      (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) = 

    if Rule.id_rls rls = HOLogic.dest_string rls_ 

    then

      if f = f_

      then Ass (m, f', ContextC.insert_assumptions asms' ctxt)

      else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)

    else NotAss

  | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),

      (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) = 

    if Rule.id_rls rls = HOLogic.dest_string rls_

    then

      if f = f_

      then Ass (m, f', ContextC.insert_assumptions asms' ctxt)

      else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)

    else NotAss

  | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),

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

    if Rule.id_rls rls = HOLogic.dest_string rls_

    then

      if f = f_

      then Ass (m, f', ContextC.insert_assumptions asms' ctxt)

      else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)

    else NotAss

  | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),

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

    if Rule.id_rls rls = HOLogic.dest_string rls_

    then 

      if f = f_

      then Ass (m, f', ContextC.insert_assumptions asms' ctxt)

      else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)

    else NotAss

  | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =

    (case stac of

	    (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) =>

	      if op_ = HOLogic.dest_string op__

        then

          if f = f_

          then Ass (m, f', ctxt)

          else Ass_Weak (m ,f', ctxt)

	      else NotAss

    | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)  =>

        let val thy = Celem.assoc_thy "Isac_Knowledge";

        in

          if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd)) 

            (assoc_rls (HOLogic.dest_string rls_))

          then

            if f = f_

            then Ass (m, f', ctxt)

            else Ass_Weak (m ,f', ctxt)

          else NotAss

        end

    | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>

        let val thy = Celem.assoc_thy "Isac_Knowledge";

        in

          if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd))

            (assoc_rls (HOLogic.dest_string rls_))

          then

            if f = f_

            then Ass (m, f', ctxt)

            else Ass_Weak (m ,f', ctxt)

          else NotAss

        end

    | _ => NotAss)

  | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),

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

    if consts = consts'

    then Ass (m, consts_chkd, ctxt)

    else NotAss

  | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Prog_Tac.Or'_to'_List", _) $ _)) =

    Ass (m, list, ctxt)

  | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) = Ass (m, term, ctxt)

  | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'),

      (Const ("Prog_Tac.Substitute", _) $ _ $ t)) =

	  if f = t then Ass (m, f', ctxt)

	  else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)

		  if foldl and_ (true, map TermC.contains_Var subte)

		  then

		    let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t

		    in if t = t' then error "associate: Substitute' not applicable to val of Expr"

		       else Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)

		    end

		  else (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of

		         SOME (t', _) =>  Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)

		       | NONE => error "associate: Substitute' not applicable to val of Expr")

  | associate pt ctxt (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),

      (stac as Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =

    (case Sub_Problem.tac_from_prog pt stac of

      (_, tac as Tactic.Subproblem' ((dI, pI, _), _, _, _, _, f)) =>

        if domID = dI andalso pblID = pI

        then Ass (tac, f, ctxt)

        else NotAss

    | _ => raise ERROR ("associate: uncovered case"))

  | associate _ _ (m, _) = 

    (if (!trace_script) 

     then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"

		   ^ "@@@ tac_ = " ^ Tactic.string_of m)

     else ();

    NotAss);

(* create the initial interpreter state

  from the items of the guard and the formal arguments of the partial_function.

Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:

  (a) fmz is given by a math author

  (b) fmz_ is transformed to ori list as a prerequisite for efficient interactive modelling

  (c) modelling creates an itm list from ori list + possible user input

  (d) specifying a theory might add some items and create a guard for the partial_function

  (e) fun relate_args creates an environment for evaluating the partial_function.

Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the partial_function:

  * Since the arguments of the partial_function have no description (see Descript.thy),

    (e) depends on the sequence in fmz_ and on the types of the formal arguments.

  * pairing formal arguments with itm's follows the sequence

  * Thus the resulting sequence-relation can be ambiguous.

  * Ambiguities are done by rearranging fmz_ or the formal arguments.

  * The latter is easier, albeit not optimal: a fmz_ can be used by different partial_functions.

  *)

local

val errmsg = "ERROR: found no actual arguments for prog. of "

fun msg_miss sc metID caller f formals actuals =

  "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^

	"and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^

	"formal arg \"" ^ Rule.term2str f ^ "\" doesn't mach an actual arg.\n" ^

	"with:\n" ^

	(string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^

	(string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals

fun msg_miss_type sc metID f formals actuals =

  "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^

	"and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^

	"formal arg \"" ^ Rule.term2str f ^ "\" of type \"" ^ Rule.type2str (type_of f) ^

  "\" doesn't mach an actual arg.\nwith:\n" ^

	(string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^

	(string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals ^ "\n" ^

  "   with types: " ^ (strs2str o (map (Rule.type2str o type_of))) actuals

fun msg_ambiguous sc metID f aas formals actuals =

  "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^

	"and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^

  "formal arg. \"" ^ Rule.term2str f ^ "\" type-matches with several..."  ^

  "actual args. \"" ^ Rule.terms2str aas ^ "\"\n" ^

  "selected \"" ^ Rule.term2str (hd aas) ^ "\"\n" ^

	"with\n" ^

	"formals: " ^ Rule.terms2str formals ^ "\n" ^

	"actuals: " ^ Rule.terms2str actuals

fun trace_init metID =

  if (!trace_script) 

  then tracing("@@@ program " ^ strs2str metID)

  else ();

in

fun init_pstate srls ctxt itms metID =

  let

    val itms = Specify.hack_until_review_Specify_2 metID itms

    val actuals = itms2args (Proof_Context.theory_of ctxt) metID itms

    val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)

    val (scr, sc) = (case (#scr o Specify.get_met) metID of

           scr as Rule.Prog sc => (trace_init metID; (scr, sc))

       | _ => raise ERROR ("init_pstate with " ^ Celem.metID2str metID))

    val formals = Program.formal_args sc    

    fun assoc_by_type f aa =

      case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of

        [] => error (msg_miss_type sc metID f formals actuals)

      | [a] => (f, a)

      | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));

	  fun relate_args _ (f::_)  [] = error (msg_miss sc metID "relate_args" f formals actuals)

	    | relate_args env [] _ = env (*may drop Find?*)

	    | relate_args env (f::ff) (aas as (a::aa)) = 

	      if type_of f = type_of a 

	      then relate_args (env @ [(f, a)]) ff aa

        else

          let val (f, a) = assoc_by_type f aas

          in relate_args (env @ [(f, a)]) ff (remove op = a aas) end

    val {pre, prls, ...} = Specify.get_met metID;

    val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;

    val ctxt = ctxt |> ContextC.insert_assumptions pres;

    val ist = Istate.e_pstate

      |> Istate.set_eval srls

      |> Istate.set_env_true (relate_args [] formals actuals)

  in

    (Istate.Pstate ist, ctxt, scr)

  end;

end (*local*)

fun get_simplifier (pt, (p, _)) =

  let

    val p' = Ctree.par_pblobj pt p

	  val metID = Ctree.get_obj Ctree.g_metID pt p'

	  val {srls, ...} = Specify.get_met metID

  in srls end

(* decide, where to get program/istate from:

   (* 1 *) from PblObj: at begin of program if no init_form

   (* 2 *) from PblObj/PrfObj: if Prog_Tac is in the middle of the program

   (* 3 *) from PrfOb: in case of Math_Engine.detailstep

 *)

fun from_pblobj_or_detail' thy (p, p_) pt =

  if Pos.on_specification p_

  then case get_obj g_env (*!DEPRECATED!*) pt p of                                         (* 1 *)

      NONE => error "from_pblobj_or_detail': no istate"

    | SOME (Istate.Pstate pst, ctxt) =>

        let

          val metID = get_obj g_metID pt p

          val {srls, ...} = Specify.get_met metID

        in

          (srls, (Istate.Pstate (Istate.set_eval srls pst), ctxt), (#scr o Specify.get_met) metID)

        end

    | _ => raise ERROR "from_pblobj_or_detail': unexpected result from g_env"

  else

    let val (pbl, p', rls') = par_pbl_det pt p

    in if pbl

       then (*if last_elem p = 0 nothing written to pt yet*)                               (* 2 *)

         let

	         val metID = get_obj g_metID pt p'

	         val {srls, ...} = Specify.get_met metID

	         val (is, ctxt) =

	           case get_loc pt (p, p_) of

	              (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)

	           | _ => raise ERROR "from_pblobj_or_detail': unexpected result from get_loc"

	       in (srls, (is, ctxt), (#scr o Specify.get_met) metID) end

       else                                                                                (* 3 *)

         (Rule.e_rls(*!!!*),

         get_loc pt (p, p_),

         Rule.Prog (Auto_Prog.gen (Celem.assoc_thy thy) (get_last_formula (pt, (p, p_))) rls'))

    end

(* handle a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr.

  TODO: what is a' ??? *)

fun check_leaf call ctxt srls (E, (a, v)) t =

    case Prog_Tac.eval_leaf E a v t of

	    (Program.Tac stac, a') =>

	      let val stac' =

            Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls 

              (subst_atomic (Env.update_opt E (a, v)) stac)

	      in

          (if (! trace_script) 

	         then tracing ("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Tac '" ^ Rule.term2str stac ^ "'")

	         else ();

	         (Program.Tac stac', a'))

	      end

    | (Program.Expr lexpr, a') =>

	      let val lexpr' =

            Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls

              (subst_atomic (Env.update_opt E (a, v)) lexpr)

	      in

          (if (! trace_script) 

	         then tracing("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")

	         else ();

	         (Program.Expr lexpr', a'))

	      end;

(**)end(**)