(* Title:  Specify/input-calchead.sml

   Author: Walther Neuper

   (c) due to copyright terms

This will be dropped at switch to Isabelle/PIDE.

*)

signature INPUT_CALCHEAD =

sig

  type pbt_ = string * (term * term)

  datatype iitem =

      Find of TermC.as_string list

    | Given of TermC.as_string list

    | Relate of TermC.as_string list

  type imodel = iitem list

  type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * Spec.T

  val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd

  val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option

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

  (*  NONE *)

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

  (*  NONE *)

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

(*----- unused code, kept as hints to design ideas ---------------------------------------------*)

  val e_icalhd : icalhd

  val oris2itms : 'a -> ''b list -> ('c * ''b * 'd * term * term list) list ->

    ('c * ''b * bool * 'd * I_Model.feedback) list

end

structure In_Chead(**): INPUT_CALCHEAD(**) =

struct

(* types for problems models (TODO rename to specification models) *)

type pbt_ =

  (string *   (* field "#Given",..*)(*deprecated due to 'type pat'*)

    (term *   (* description      *)

      term)); (* id | struct-var  *)

(*** handle an input by CAS-command ***)

fun dtss2itm_ ppc (d, ts) =

  let

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

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

  		(#2: pbt_ -> (term * term))) ppc)

  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 cas_input_ ((dI, pI, mI): Spec.T) dtss = (*WN110515 reconsider thy..ctxt*)

  let

    val thy = ThyC.get_theory dI

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

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

	  val its = O_Model.add_id 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 #met o Specify.get_pbt) pI)

			  | NONE => (pI, (hd o #met o Specify.get_pbt) pI)

	  val {ppc, pre, prls, ...} = Specify.get_met mI

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

	  val its = O_Model.add_id its_

	  val mits = map flattup2 its

	  val pre = Pre_Conds.check' thy prls pre mits

    val ctxt = Proof_Context.init_global thy

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

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

fun cas_input hdt =

  let

    val (h, argl) = strip_comb hdt

  in

    case assoc_cas (ThyC.get_theory "Isac_Knowledge") h of

      NONE => NONE

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

	      let

          val dtss = argl2dtss argl

	        val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss

	        val spec = (dI, pI, mI)

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

		        ([], Spec.empty) ([], Spec.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, pre, spec) : Ctree.ocalhd)

	      end

  end

(*** handle an input calc-head ***)

datatype iitem = 

  Given of TermC.as_string list

(*Where is never input*) 

| Find  of TermC.as_string list

| Relate  of TermC.as_string list

type imodel = iitem list

(*calc-head as input*)

type icalhd =

  Pos.pos' *     (*the position of the calc-head in the calc-tree*) 

  TermC.as_string *   (*the headline*)

  imodel *         (*the model (without Find) of the calc-head*)

  Pos.pos_ *     (*model belongs to Pbl or Met*)

  Spec.T;      (*specification: domID, pblID, metID*)

val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Spec.empty)

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

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

(* re-parse itms with a new thy and prepare for checking with ori list *)

fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =

    (let val t = Input_Descript.join (d, ts)

     val _ = (UnparseC.term_in_thy dI t)

     (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)

    in itm end

    handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))

  | parsitm dI (i, v, b, f, I_Model.Syn str) =

    (let val _ = (Thm.term_of o the o (TermC.parse dI)) str

    in (i, v, b ,f, I_Model.Par str) end

    handle _ => (i, v, b, f, I_Model.Syn str))

  | parsitm dI (i, v, b, f, I_Model.Typ str) =

    (let val _ = (Thm.term_of o the o (TermC.parse dI)) str

     in (i, v, b, f, I_Model.Par str) end

     handle _ => (i, v, b, f, I_Model.Syn str))

  | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =

    (let val t = Input_Descript.join (d,ts);

	       val _ = UnparseC.term_in_thy dI t;

     (*this    ^ should raise the exn on unability of re-parsing dts*)

     in itm end

     handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))

  | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) =

    (let val t = Input_Descript.join (d,ts);

	       val _ = UnparseC.term_in_thy dI t;

     (*this    ^ should raise the exn on unability of re-parsing dts*)

    in itm end

    handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))

  | parsitm dI (itm as (i, v, _, f, I_Model.Mis (d, t'))) =

    (let val t = d $ t';

	       val _ = UnparseC.term_in_thy dI t;

     (*this    ^ should raise the exn on unability of re-parsing dts*)

    in itm end

    handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))

  | parsitm dI (itm as (_, _, _, _, I_Model.Par _)) = 

    raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.to_ctxt dI) itm ^ "): Par should be internal");

(*separate a list to a pair of elements that do NOT satisfy the predicate,

 and of elements that satisfy the predicate, i.e. (false, true)*)

fun filter_sep pred xs =

  let

    fun filt ab [] = ab

      | filt (a, b) (x :: xs) =

        if pred x 

			  then filt (a, b @ [x]) xs 

			  else filt (a @ [x], b) xs

  in filt ([], []) xs end;

fun is_Par (_, _, _, _, I_Model.Par _) = true

  | is_Par _ = false;

fun is_e_ts [] = true

  | is_e_ts [Const ("List.list.Nil", _)] = true

  | is_e_ts _ = false;

(* WN.9.11.03 copied from fun appl_add *)

fun appl_add' dI oris ppc pbt (sel, ct) = 

  let 

     val ctxt = ThyC.get_theory dI |> ThyC.to_ctxt;

  in

    case TermC.parseNEW ctxt ct of

	    NONE => (0, [], false, sel, I_Model.Syn ct)

	  | SOME t =>

	    (case I_Model.is_known ctxt sel oris t of

        ("", ori', all) =>

          (case I_Model.is_notyet_input ctxt ppc all ori' pbt of

            ("",itm)  => itm

          | (msg,_) => raise ERROR ("appl_add': " ^ msg))

      | (_, (i, v, _, d, ts), _) =>

        if is_e_ts ts

        then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, [])))

        else (i, v, false, sel, I_Model.Sup (d, ts)))

   end

(* generate preliminary itm_ from a strin (with field "#Given" etc.) *)

fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';

fun fstr2itm_ thy pbt (f, str) =

  let

    val topt = TermC.parse thy str

  in

    case topt of

      NONE => ([], false, f, I_Model.Syn str)

    | SOME ct => 

	    let

	      val (d, ts) = (Input_Descript.split o Thm.term_of) ct

	      val popt = find_first (eq7 (f, d)) pbt

	    in

	      case popt of

	        NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts))

	      | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts))) 

	    end

  end

(*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)

fun unknown_expl dI pbt selcts =

  let

    val thy = ThyC.get_theory dI

    val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)

    val its = O_Model.add_id its_ 

  in map flattup2 its end

(* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation

   appl_add': generate 1 item 

   appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)

   appl_add' . is_notyet_input: compare with items in model already input

   insert_ppc': insert this 1 item*)

fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts

    (*already present itms in model are being overwritten*)

  | appl_adds _ _ ppc _ [] = ppc

  | appl_adds dI oris ppc pbt (selct :: ss) =

    let val itm = appl_add' dI oris ppc pbt selct;

    in appl_adds dI oris (Chead.insert_ppc' itm ppc) pbt ss end

fun oris2itms _  _ [] = [] (* WN161130: similar in ptyps ?!? *)

  | oris2itms pbt vat ((i, v, f, d, ts) :: os) =

    if member op = vat v 

    then (i, v, true, f, I_Model.Cor ((d, ts), (TermC.empty, []))) :: (oris2itms pbt vat os)

    else oris2itms pbt vat os

fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)

  | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)

fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))

  | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str)

  | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str)

  | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))

  | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))

  | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t))

  | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) = 

    raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");

fun imodel2fstr iitems = 

  let 

    fun xxx is [] = is

	    | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis

	    | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis

	    | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis

  in xxx [] iitems end;

(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)

fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =

    let

		  val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of

		    Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), 

		      spec = sspec as (sdI, spI, smI), probl, meth, ...}

        => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)

      | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"

    in if is_casinput hdf fmz then the (cas_input (TermC.str2term hdf)) 

       else        (*hacked WN0602 ~~~            ~~~~~~~~~,   ..dropped !*)

         let val (pos_, pits, mits) = 

	         if dI <> sdI

	         then let val its = map (parsitm (ThyC.get_theory dI)) probl;

			            val (its, trms) = filter_sep is_Par its;

			            val pbt = (#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec sspec))

		            in (Pos.Pbl, appl_adds dI oris its pbt  (map par2fstr trms), meth) end 

           else

             if pI <> spI 

	           then if pI = snd3 ospec then (Pos.Pbl, probl, meth) 

                  else

		                let val pbt = (#ppc o Specify.get_pbt) pI

			                val dI' = #1 (Chead.some_spec ospec spec)

			                val oris = if pI = #2 ospec then oris 

				                         else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*);

		                in (Pos.Pbl, appl_adds dI' oris probl pbt 

				              (map itms2fstr probl), meth) end 

             else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)

	                then let val met = (#ppc o Specify.get_met) mI

		                     val mits = Chead.complete_metitms oris probl meth met

		                   in if foldl and_ (true, map #3 mits)

		                      then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits) 

		                   end 

                  else (Pos.Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]

			                  ((#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec spec)))

			                  (imodel2fstr imodel), meth)

	         val pt = Ctree.update_spec pt p spec;

         in if pos_ = Pos.Pbl

	          then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))

		               val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits

	               in (Ctree.update_pbl pt p pits,

		                 (Chead.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Ctree.ocalhd) 

                 end

	           else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))

		                val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits

	                in (Ctree.update_met pt p mits,

		                  (Chead.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Ctree.ocalhd)

                  end

         end 

    end

  | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl."

(**)end (**)