(* Title:  Interpret/lucas-interpreter.sml

   Author: Walther Neuper 2019

   (c) due to copyright terms

*)

signature COMPUTER_ALGEBRA_SYSTEM_COMMAND =

sig

  type input_pos

  type T = CAS_Def.T

  val input : term -> (Ctree.ctree * SpecificationC.T) option

  val is_from: TermC.as_string -> Formalise.T -> bool

\<^isac_test>\<open>

  val input_: References.T -> (term * term list) list ->

    Problem.id * I_Model.T * MethodC.id * I_Model.T * Pre_Conds.T * Proof.context

  val dtss2itm_: Model_Pattern.T -> term * term list ->

    int list * bool * string * I_Model.feedback (*I_Model.single'*)

  val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e

\<close>

end

(**)

structure CAS_Cmd(**): COMPUTER_ALGEBRA_SYSTEM_COMMAND(**) =

struct

(**)

type input_pos = CAS_Def.input_pos;

type T = CAS_Def.T; (*(term * (References_Def.T * generate_fn))*)

fun dtss2itm_ model (d, ts) =

  let

    val (f, (d, id)) = the (find_first ((curry op= d) o 

  		(#1: (term * term) -> term) o

  		(#2: Model_Pattern.single -> (term * term))) model)

  in

    ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))

  end

fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)

fun is_from (hdf : TermC.as_string) ((fmz_, spec) : Formalise.T) =

  hdf <> "" andalso fmz_ = [] andalso spec = References.empty

(*T_TESTold* )

fun input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*)

  let

    val thy = Know_Store.get_via_last_thy dI

    val ctxt = Proof_Context.init_global thy

	  val {model, ...} = Problem.from_store ctxt pI

	  val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)

	  val its = O_Model.add_enumerate its_

	  val pits = map flattup2 its

	  val (pI, mI) =

      if mI <> ["no_met"]

      then (pI, mI)

		  else

        case Refine.problem thy pI pits of

			    SOME (pI, _) => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)

			  | NONE => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)

	  val {model, where_, where_rls, ...} = MethodC.from_store ctxt mI

	  val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)

	  val its = O_Model.add_enumerate its_

	  val mits = map flattup2 its

	  val (_, where_) = Pre_Conds.check ctxt where_rls where_ mits 0

    val ctxt = Proof_Context.init_global thy

  in (pI, pits, mI, mits, where_, ctxt) end;

( *T_TEST**)

fun input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*)

  let

    val thy = Know_Store.get_via_last_thy dI

    val ctxt = Proof_Context.init_global thy

	  val {model, ...} = Problem.from_store ctxt pI

	  val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)

	  val its = O_Model.add_enumerate its_

	  val pits = map flattup2 its

	  val (pI, mI) =

      if mI <> ["no_met"]

      then (pI, mI)

		  else

        case Refine.problem thy pI pits of

			    SOME (pI, _) => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)

			  | NONE => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)

	  val {model, where_, where_rls, ...} = MethodC.from_store ctxt mI

	  val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)

	  val its = O_Model.add_enumerate its_

	  val mits = map flattup2 its

	  val (_, where_) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_TEST mits)

    val ctxt = Proof_Context.init_global thy

  in (pI, pits, mI, mits, where_, ctxt) end;

(*T_TESTnew*)

(* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)

fun input hdt =

  let

    val (h, argl) = strip_comb hdt

  in

    case get_cas_global h of

      NONE => NONE

    | SOME (spec as (dI,_,_), argl2dtss) =>

	      let

          val dtss = argl2dtss argl

	        val (pI, pits, mI, mits, where_, ctxt) = input_ spec dtss

	        val spec = (dI, pI, mI)

	        val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty)

		        ([], References.empty) ([], References.empty, hdt, ctxt)

	        val pt = Ctree.update_spec pt [] spec

	        val pt = Ctree.update_pbl pt [] pits

	        val pt = Ctree.update_met pt [] mits

	      in

	        SOME (pt, (true, Pos.Met, hdt, mits, where_, spec) : SpecificationC.T)

	      end

  end

(** Isar command **)

local

val parse_theory = Problem.parse_item_name \<^keyword>\<open>Theory_Ref\<close> "Isac_Knowledge";

val parse_problem = Problem.parse_item \<^keyword>\<open>Problem_Ref\<close> Parse.name;

val parse_method = Problem.parse_item_name \<^keyword>\<open>Method_Ref\<close> "no_met";

val ml = ML_Lex.read;

val _ =

  Outer_Syntax.command \<^command_keyword>\<open>cas\<close>

    "prepare ISAC Computer-Algebra System and register it to Knowledge Store"

    (Parse.term -- (\<^keyword>\<open>=\<close> |--

      Parse.!!! (Parse.ML_source -- parse_theory -- parse_problem -- parse_method))

      >> (fn (term, (((source, thry), pbl), met)) => Toplevel.theory (fn thy =>

        let

        (*/------------ replace by ParseC.term_position ------------------\*)

          val SOME t = ParseC.term_opt (Proof_Context.init_global thy) term;

        (*\------------ replace by ParseC.term_position ------------------/*)

          val pblID = References_Def.explode_id pbl;

          val metID = References_Def.explode_id met;

          val set_data =

            ML_Context.expression (Input.pos_of source)

              (ml "Theory.setup (CAS_Def.set_data (" @ ML_Lex.read_source source @ ml "))")

            |> Context.theory_map;

          val data = CAS_Def.the_data (set_data thy);

        in Know_Store.add_cass [(t, ((thry, pblID, metID), data))] thy end)));

in end;

(**)end(**)