(* convert sml-datatypes to xml for libisabelle and for kbase.

   authors: Walther Neuper 2003, 2016

   (c) due to copyright terms

This code remains in order to

keep tests of interaction Java-frontend <-> Kernel running.

*)

(*** convert sml-datatypes to xml for kbase ***)

fun filterpbl str =

  let fun filt [] = []

        | filt ((s, (t1, t2)) :: ps) = 

	  if str = s then (t1 $ t2) :: filt ps else filt ps

  in filt end;

fun pattern2xml j p where_ =

    (case filterpbl "#Given" p of

	[] =>  (indt j) ^ "<GIVEN>  </GIVEN>\n"

(* val gis = filterpbl "#Given" p;

   *)

      | gis => (indt j) ^ "<GIVEN>\n" ^ terms2xml' j gis ^

	       (indt j) ^ "</GIVEN>\n")

    ^ 

    (case where_ of

	 [] =>  (indt j) ^ "<WHERE>  </WHERE>\n"

       | whs => (indt j) ^ "<WHERE>\n" ^ terms2xml' j whs ^

		(indt j) ^ "</WHERE>\n")

    ^ 

    (case filterpbl "#Find" p of

	 [] =>  (indt j) ^ "<FIND>  </FIND>\n"

       | fis => (indt j) ^ "<FIND>\n" ^ terms2xml' j fis ^

		(indt j) ^ "</FIND>\n")

    ^ 

    (case filterpbl "#Relate" p of

	 [] =>  (indt j) ^ "<RELATE>  </RELATE>\n"

       | res => (indt j) ^ "<RELATE>\n" ^ terms2xml' j res ^

		(indt j) ^ "</RELATE>\n");

fun prepa12xml j (terms, term) =

    indt j ^"<PREPAT>\n"^

    indt (j+i) ^"<PRECONDS>\n"^

    terms2xml (j+2*i) terms ^

    indt (j+i) ^"</PRECONDS>\n"^

    indt (j+i) ^"<PATTERN>\n"^

    term2xml (j+2*i) term ^

    indt (j+i) ^"</PATTERN>\n"^

    indt j ^"</PREPAT>\n";

fun prepat2xml _ [] = ""

  | prepat2xml j (p::ps) = prepa12xml j p ^ prepat2xml j ps;

(*** convert sml-datatypes to xml for libisabelle ***)

(** general types: lists, etc **)

fun xml_of_bool b = XML.Elem (("BOOL", []), [XML.Text (bool2str b)])

fun xml_of_str str = XML.Elem (("STRING", []), [XML.Text str])

fun xml_of_strs strs = XML.Elem (("STRINGLIST", []), map xml_of_str strs)

fun xml_of_int i = XML.Elem (("INT", []), [XML.Text (string_of_int i)])

fun xml_of_ints is =

  XML.Elem (("INTLIST", []), map xml_of_int is)

(** isac datatypes **)

fun xml_of_pos tag (is, pp) =

  XML.Elem ((tag, []), [

    xml_of_ints is,

    XML.Elem (("POS", []), [XML.Text (Pos.pos_2str pp)])])

fun xml_of_auto (Solve.Steps i) = 

      XML.Elem (("AUTO", []), [XML.Text "Step", XML.Text (string_of_int i)])

  | xml_of_auto Solve.CompleteModel = XML.Elem (("AUTO", []), [XML.Text "CompleteModel"])

  | xml_of_auto Solve.CompleteCalcHead = XML.Elem (("AUTO", []), [XML.Text "CompleteCalcHead"])

  | xml_of_auto Solve.CompleteToSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteToSubpbl"])

  | xml_of_auto Solve.CompleteSubpbl = XML.Elem (("AUTO", []), [XML.Text "CompleteSubpbl"])

  | xml_of_auto Solve.CompleteCalc = XML.Elem (("AUTO", []), [XML.Text "CompleteCalc"])

fun filterpbl str =

  let fun filt [] = []

        | filt ((s, (t1, t2)) :: ps) = 

	  if str = s then (t1 $ t2) :: filt ps else filt ps

  in filt end;

fun xml_of_itm_ (I_Model.Cor (dts, _)) =

    XML.Elem (("ITEM", [("status", "correct")]), [xml_of_term (Input_Descript.join' dts)])

  | xml_of_itm_ (I_Model.Syn c) =

    XML.Elem (("ITEM", [("status", "syntaxerror")]), [XML.Text c])

  | xml_of_itm_ (I_Model.Typ c) =

    XML.Elem (("ITEM", [("status", "typeerror")]), [XML.Text c])

  (*type item also has 'False of cterm' set in preconds2xml WN 050618*)

  | xml_of_itm_ (I_Model.Inc (dts, _)) = 

    XML.Elem (("ITEM", [("status", "incomplete")]), [xml_of_term (Input_Descript.join' dts)])

  | xml_of_itm_ (I_Model.Sup dts) = 

    XML.Elem (("ITEM", [("status", "superfluous")]), [xml_of_term (Input_Descript.join' dts)])

  | xml_of_itm_ (I_Model.Mis (d, pid)) = 

    XML.Elem (("ITEM", [("status", "missing")]), [xml_of_term (d $ pid)])

  | xml_of_itm_ _ = raise ERROR "xml_of_itm_: wrong argument"

fun xml_of_itms itms =

  let 

    fun extract (_, _, _, _, itm_) = itm_

  in map (xml_of_itm_ o extract) itms end

fun xml_of_precond (status, term) =

    XML.Elem (("ITEM", [("status", if status then "correct" else "false")]), [xml_of_term term])

fun xml_of_preconds ps = map xml_of_precond ps

fun xml_of_model itms where_ =

  let

    fun eq str (_, _, _,field, _) = str = field

  in 

    XML.Elem (("MODEL", []), [

      XML.Elem (("GIVEN", []), 

        filter (eq "#Given") itms |> xml_of_itms),

      XML.Elem (("WHERE", []), 

        xml_of_preconds where_),

      XML.Elem (("FIND", []), 

        filter (eq "#Find") itms |> xml_of_itms),

      XML.Elem (("RELATE", []), 

        filter (eq "#Relate") itms |> xml_of_itms)])

  end 

fun xml_of_spec (thyID, pblID, metID) =

  XML.Elem (("SPECIFICATION", []), [

    XML.Elem (("THEORYID", []), [XML.Text thyID]),

    XML.Elem (("PROBLEMID", []), [xml_of_strs pblID]),

    XML.Elem (("METHODID", []), [xml_of_strs metID])])

fun xml_of_variant (items, spec) = 

  XML.Elem (("VARIANT", []), [xml_of_strs items, xml_of_spec spec])

fun xml_of_fmz [] = xml_of_fmz [Formalise.empty]

  | xml_of_fmz vs = XML.Elem (("FORMALIZATION", []), map xml_of_variant vs)

fun xml_of_modspec ((b, p_, head, gfr, where_, spec): SpecificationC.T) =

  XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [

    XML.Elem (("HEAD", []), [xml_of_term_NEW head]),

    xml_of_model gfr where_,

    XML.Elem (("BELONGSTO", []), [

      XML.Text (case p_ of Pos.Pbl => "Pbl" | Pos.Met => "Met" | _ => "Und")]),

    xml_of_spec spec])

fun xml_of_posmodspec ((p: Pos.pos', (b, p_, head, gfr, where_, spec): SpecificationC.T)) =

  XML.Elem (("CALCHEAD", [("status", if b then "correct" else "incorrect")]), [

    xml_of_pos "POSITION" p,

    XML.Elem (("HEAD", []), [xml_of_term_NEW head]),

    xml_of_model gfr where_,

    XML.Elem (("BELONGSTO", []), [

      XML.Text (case p_ of Pos.Pbl => "Pbl" | Pos.Met => "Met" | _ => "Und")]),

    xml_of_spec spec])

fun xml_of_sub (id, value) =

  XML.Elem (("PAIR", []), [

    XML.Elem (("VARIABLE", []), [xml_of_term id]),

    XML.Elem (("VALUE", []), [xml_of_term value])])

fun xml_of_subs (subs : Subst.input) =

  XML.Elem (("SUBSTITUTION", []), 

    map xml_of_sub (Tactic.subst_adapt_to_type (ThyC.id_to_ctxt "Isac_Knowledge") subs))

fun xml_of_sube sube =

  XML.Elem (("SUBSTITUTION", []), 

    map xml_of_sub (Subst.T_from_string_eqs (Know_Store.get_via_last_thy "Isac_Knowledge") sube))

fun thm''2xml j (thm : thm) =

    indt j ^ "<THEOREM>\n" ^

    indt (j+i) ^ "<ID> " ^ ThmC.id_of_thm thm ^ " </ID>\n"^

    term2xml j (Thm.prop_of thm) ^ "\n" ^

    indt j ^ "</THEOREM>\n";

fun xml_of_thm' (ID, form) =

  XML.Elem (("THEOREM", []), [

    XML.Elem (("ID", []), [XML.Text ID]),

    XML.Elem (("FORMULA", []), [

      XML.Text form])])           (* repair for MathML: use term instead String *)

(* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *)

fun xml_of_thm'' (ID, thm) =

  XML.Elem (("THEOREM", []), [

    XML.Elem (("ID", []), [XML.Text ID]),

    XML.Elem (("FORMULA", []), [

      XML.Text ((UnparseC.term o Thm.prop_of) thm)])])           (* repair for MathML: use term instead String *)

fun xml_of_src Rule.Empty_Prog =

    XML.Elem (("NOCODE", []), [XML.Text "empty"])

  | xml_of_src (Rule.Prog term) =

    XML.Elem (("CODE", []), [

      if term = TermC.empty then xml_of_src Rule.Empty_Prog

      else xml_of_term (TermC.inst_abs term)])

  | xml_of_src (Rule.Rfuns _) =

    XML.Elem (("NOCODE", []), [XML.Text "reverse rewrite functions"])

(*.convert a tactic into xml-format .*)

fun xml_of_tac (Tactic.Subproblem (dI, pI)) =

    XML.Elem (("SUBPROBLEMTACTIC", [("name", "Subproblem")]), [

      XML.Elem (("THEORY", []), [XML.Text dI]),

      XML.Elem (("PROBLEM", []), [xml_of_strs pI])])

  | xml_of_tac (Tactic.Substitute cterms) =

    (*Substitute: sube -> tac; Subst.string_eqs_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)

    XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])

    (*----- Rewrite* -----------------------------------------------------*)

  | xml_of_tac (Tactic.Rewrite thm'') =

    XML.Elem (("REWRITETACTIC", [("name", "Rewrite")]), [xml_of_thm'' thm''])

  | xml_of_tac (Tactic.Rewrite_Inst (subs, thm'')) =

    XML.Elem (("REWRITEINSTTACTIC", [("name", "Rewrite_Inst")]), (

      xml_of_subs subs ::

      xml_of_thm'' thm'' :: []))

  | xml_of_tac (Tactic.Rewrite_Set rls') =

    XML.Elem (("REWRITESETTACTIC", [("name", "Rewrite_Set")]), [XML.Text rls'])

  | xml_of_tac (Tactic.Rewrite_Set_Inst (subs, rls')) =

    XML.Elem (("REWRITESETINSTTACTIC", [("name", "Rewrite_Set_Inst")]), ([

      xml_of_subs subs,

      XML.Elem (("RULESET", []), [XML.Text rls'])]))

    (*----- FORMTACTIC ---------------------------------------------------*)

  | xml_of_tac (Tactic.Add_Find ct) =

    XML.Elem (("FORMTACTIC", [("name", "Add_Find")]), [xml_of_cterm ct])

  | xml_of_tac (Tactic.Add_Given ct) =

    XML.Elem (("FORMTACTIC", [("name", "Add_Given")]), [xml_of_cterm ct])

  | xml_of_tac (Tactic.Add_Relation ct) =

    XML.Elem (("FORMTACTIC", [("name", "Add_Relation")]), [xml_of_cterm ct])

  | xml_of_tac (Tactic.Check_elementwise ct) =

    XML.Elem (("FORMTACTIC", [("name", "Check_elementwise")]), [xml_of_cterm ct])

  | xml_of_tac (Tactic.Take ct) =

    XML.Elem (("FORMTACTIC", [("name", "Take")]), [xml_of_cterm ct])

    (*----- SIMPLETACTIC -------------------------------------------------*)

  | xml_of_tac (Tactic.Calculate opstr) =

    XML.Elem (("SIMPLETACTIC", [("name", "Calculate")]), [XML.Text opstr])

  | xml_of_tac (Tactic.Or_to_List) =

    XML.Elem (("SIMPLETACTIC", [("name", "Or_to_List")]), [(*//////////*)])

  | xml_of_tac (Tactic.Specify_Theory ct) =

    XML.Elem (("SIMPLETACTIC", [("name", "Specify_Theory")]), [XML.Text ct])

    (*----- STRINGLISTTACTIC ---------------------------------------------*)

  | xml_of_tac (Tactic.Apply_Method mI) =

    XML.Elem (("STRINGLISTTACTIC", [("name", "Apply_Method")]), [xml_of_strs mI])

  | xml_of_tac (Tactic.Check_Postcond pI) =

    XML.Elem (("STRINGLISTTACTIC", [("name", "Check_Postcond")]), [xml_of_strs pI])

  | xml_of_tac Tactic.Model_Problem =

    XML.Elem (("STRINGLISTTACTIC", [("name", "Model_Problem")]), [])

  | xml_of_tac (Tactic.Refine_Tacitly pI) =

    XML.Elem (("STRINGLISTTACTIC", [("name", "Refine_Tacitly")]), [xml_of_strs pI])

  | xml_of_tac (Tactic.Specify_Method ct) =

    XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Method")]), [xml_of_strs ct])

  | xml_of_tac (Tactic.Specify_Problem ct) =

    XML.Elem (("STRINGLISTTACTIC", [("name", "Specify_Problem")]), [xml_of_strs ct])

  | xml_of_tac tac =

    let

      val ctxt = Proof_Context.init_global (Know_Store.get_via_last_thy "Isac_Knowledge")

    in

      raise ERROR ("xml_of_tac: not impl. for " ^ Tactic.input_to_string ctxt tac)

    end;

val e_pblterm = TermC.parseNEW'' @{theory Prog_Tac}

		    ("Problem (" ^ ThyC.id_empty ^ ", " ^ strs2str' Problem.id_empty ^ ")");

(*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)

fun xml_of_posterm (p, t, _) =

  let val input_request = Free ("________________________________________________", dummyT)

  in 

    XML.Elem (("CALCFORMULA", []),

      [xml_of_pos "POSITION" p,

       if t = e_pblterm (*headline in pbl is e_ <- _root_pbl for CAS-command*)

       then xml_of_term_NEW input_request

       else xml_of_term_NEW t])

  end

fun xml_of_asm_val (asm, vl) =

  XML.Elem (("ASMEVALUATED", []),[

    XML.Elem (("ASM", []), [xml_of_term asm]),

    XML.Elem (("VALUE", []), [xml_of_term vl])])

fun xml_of_matchpbl (model_ok, _(*pI*), hdl, pbl, where_) =

  XML.Elem (("CONTEXTDATA", []), [

    XML.Elem (("GUH", []), [(XML.Text "would-need-ctxt")(*XML.Text (Ptool.pblID2guh pI)*)]),

    XML.Elem (("STATUS", []), [

      XML.Text ((if model_ok then "correct" else "incorrect"))]),

    XML.Elem (("HEAD", []), [xml_of_term_NEW hdl]),

    xml_of_model pbl where_])

fun xml_of_matchmet (model_ok, pI, program, pbl, where_) =

  XML.Elem (("CONTEXTDATA", []), [

    XML.Elem (("GUH", []), [XML.Text (Ptool.metID2guh pI)]),

    XML.Elem (("STATUS", []), [

      XML.Text ((if model_ok then "correct" else "incorrect"))]),

    XML.Elem (("PROGRAM", []), [xml_of_src program]),

    xml_of_model pbl where_])

fun xml_of_calcchanged calcid tag old del new =

  XML.Elem ((tag, []),[

    XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),

    XML.Elem (("CALCCHANGED", []), [

      xml_of_pos "UNCHANGED" old,

      xml_of_pos "DELETED" del,

      xml_of_pos "GENERATED" new])])

(* for checking output at Frontend *)

fun cut_xml xml i = xml |> xmlstr 0 |> Symbol.explode |> curry take i |> implode