(* Title:  Specify/specification.sml

   Author: Walther Neuper, Mathias Lehnfeld

   (c) due to copyright terms

*)

(* Survey on type fmz_ .. type ori .. type itm (in probl, meth) .. formal args of root-/SubProblem

   and relations between respective list elements:                                       #1#

                  fmz      =             [ dsc $ v......................................(dsc $ v)..]

root problem on pos = ([], _)            

                  fmz_     =             [(dsc, v).......................................(dsc, v)..]

                  \<down>                                                                       

                  oris     =             [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)...........(dsc, v)..]

                  \<down>                       #Given,..,#Relate  #Find     #undef............#undef   \<down>

                  \<down>                                                     \<down>                 \<down>       \<down>

  Specify_Problem + pbl.ppc=             [(dsc,id)..(dsc,id),(dsc,id)]  \<down>                 \<down>       \<down>

                  \<down>                                                     \<down>                 \<down>       \<down>

                  itms     =             [(dsc, v)..(dsc, v),(dsc, v)]  \<down>                 \<down>       \<down>

  int.modelling                           +Cor ++++++++++Cor +Cor       \<down>                 \<down>       \<down>

                  \<down>                                                     \<down>                 \<down>       \<down>

  Specify_Method  + met.ppc=             [(dsc,id)..(dsc,id),(dsc,id)]  \<down>                 \<down>       \<down>

                  \<down>                                                     \<down>                 \<down>       \<down>

                  itms     =             [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)..(dsc, v)] \<down>       \<down>

  int.modelling                                                       +Cor ++++++Cor      \<down>       \<down>

                  form.args=             [ id ..... id      , ///////  id ....... id    ] \<down>       \<down>

                  env =                  [(id, v)..(id, v)  , /////// (id, v)....(id, v)] \<down>       \<down>

  interpret code env = [(id, v)..(id, v),(id, v)..(id, v)  , /////// (id, v)....(id, v)] \<down>       \<down>

    ..extends env       ^^^^^^^^^^^^^^^^   \<down>                           \<down>   \<down>              \<down>       \<down>

                                   \<down>       \<down>                           \<down>   \<down>              \<down>       \<down>

SubProblem on pos = ([2], _)       \<down>       \<down>                           \<down>   \<down>              \<down>       \<down>

                  form.args=      [id ................................ id ]\<down>              \<down>       \<down>

                  \<down>                REAL..BOOL..                            \<down>              \<down>       \<down>

                  \<down>                                                        \<down>              \<down>       \<down>

                  + met.ppc=      [(dsc,id).......................(dsc,id)]\<down>              \<down>       \<down>

                                    \<down>                               \<down>      \<down>              \<down>       \<down>

                  oris     =      [(dsc, v)...................... (dsc,   v) ........... (dsc, v)]\<down>

  Specify_Problem, int.modelling, Specify_Method, interpret code as above                 #1#    \<down>

                                                                                                  \<down>

SubProblem on pos = ([3, 4], _)                                                                   \<down>

                  form.args=              [id ...................... id ]                         \<down>

                  \<down>                        REAL..BOOL..                                           \<down>

                  + met.ppc=              [(dsc,id).............(dsc,id)]                         \<down>

                  oris     =              [(dsc, v).............(dsc, v)...................(dsc, v)] 

  Specify_Problem, int.modelling, Specify_Method, interpret code as above                    #1#

Notes:

(1) SubProblem implements sub-function calls such, that the arguments (+ pre- + post-condition)

    of the functions become concern of interactive modelling.

(2) In Isac-terms, the above concerns the phases of modelling and 

    and of specifying (Specify_Problem, Specify_Method),

    while stepwise construction of solutions is called solving.

    The latter is supported by Lucas-Interpretation of the functions' body.

(3) ori list is determined by fmz_ (in root-pbl) or by args of SubProblem;

    it is as complete as possible (this has been different up to now).

(4) itm list is initialised by pbl-ppc | met-pps and completed (Cor) by stepwise user input.

(5) model-pattern of pbl can omit technical items, e.g. boundVariable or functionName,

    add them to the model-pattern of met and let this input be done automatically;

    respective items must be in fmz.

*)

signature SPECIFICATION =

sig

  type T = Specification_Def.T

(*val reset: Calc.T -> Calc.T*)

  val reset_calchead: Calc.T -> Calc.T

(*val get: Calc.T -> T*)

  val get_ocalhd: Calc.T -> T

(*val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*)

  val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool

(*val is_complete: Calc.T -> bool*)

  val is_complete_mod: Calc.T -> bool

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

  (*NONE*)

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

  val get: Calc.T -> I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context

  val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T

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

end

(**)

structure Specification(** ): SPECIFICATION( **) =

struct

(**)

type T = Specification_Def.T;

(* is the calchead complete ? *)

fun ocalhd_complete its pre (dI, pI, mI) = 

  foldl and_ (true, map #3 (its: I_Model.T)) andalso 

  foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso 

  dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty

fun is_parsed (I_Model.Syn _) = false

  | is_parsed _ = true

(* get the first term in ts from ori *)

fun getr_ct thy (_, _, fd, d, ts) =

  (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))

(* get a term from ori, notyet input in itm.

   the term from ori is thrown back to a string in order to reuse

   machinery for immediate input by the user. *)

fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =

  (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (I_Model.ts_in itm_) ts))

(* output the headline to a ppc *)

fun header p_ pI mI =

  case p_ of

    Pos.Pbl => Test_Out.Problem (if pI = Problem.id_empty then [] else pI) 

	| Pos.Met => Test_Out.Method mI

	| pos => raise ERROR ("header called with "^ Pos.pos_2str pos)

fun make m_field (term_as_string, i_model) =

  case m_field of

    "#Given" => Tactic.Add_Given' (term_as_string, i_model)

  | "#Find" => Tactic.Add_Find' (term_as_string, i_model)

  | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)

  | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);

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

  case Ctree.get_obj I pt p of

    (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})

      => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)

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

(* fun tag_form thy (formal, given) = Thm.global_cterm_of thy

	 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)

fun tag_form thy (formal, given) =

 (let

    val gf = (head_of given) $ formal;

    val _ = Thm.global_cterm_of thy gf

  in gf end)

  handle _ => raise ERROR ("calchead.tag_form: " ^ UnparseC.term_in_thy thy given ^

    " .. " ^ UnparseC.term_in_thy thy formal ^ " ..types do not match")

fun is_complete_mod (pt, pos as (p, Pos.Pbl)) =

    if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p 

    then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p

    else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)

  | is_complete_mod (pt, pos as (p, Pos.Met)) = 

    if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p 

    then (I_Model.is_complete o (Ctree.get_obj Ctree.g_met pt)) p

    else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)

  | is_complete_mod (_, pos) =

    raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")

(** get the formula from a ctree-node **)

(*

  take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)

  take res from all other PrfObj's

  Designed for interSteps, outcommented 04 in favour of calcChangedEvent

*)

fun formres p (Ctree.Nd (Ctree.PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =

    [("headline", (p, Pos.Frm), h), ("stepform", (p, Pos.Res), r)]

  | formres p (Ctree.Nd (Ctree.PrfObj {form, result = (r, _), ...}, _)) = 

    [("stepform", (p, Pos.Frm), form), ("stepform", (p, Pos.Res), r)]

  | formres _ _ = raise ERROR "formres: uncovered definition" 

fun form p (Ctree.Nd (Ctree.PrfObj {result = (r, _), ...}, _)) = 

    [("stepform", (p, Pos.Res), r)]

  | form _ _ = raise ERROR "form: uncovered definition" 

(* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)

fun get_ocalhd (pt, (p, Pos.Pbl)) = 

    let

	    val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of

	      Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)

	    | _ => raise ERROR "get_ocalhd Pbl: uncovered case get_obj"

      val {prls, where_, ...} = Problem.from_store (#2 (References.select ospec spec))

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

    in

      (ocalhd_complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)

    end

  | get_ocalhd (pt, (p, Pos.Met)) = 

    let

		  val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of

		    Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)

		  | _ => raise ERROR "get_ocalhd Met: uncovered case get_obj"

      val {prls, pre, ...} = Method.from_store (#3 (References.select ospec spec))

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

    in

      (ocalhd_complete meth pre spec, Pos.Met, hdf', meth, pre, spec)

    end

  | get_ocalhd _ = raise ERROR "get_ocalhd: uncovered definition"

(* at the activeFormula set the Specification 

   to empty and return a CalcHead;

   the 'origin' remains (for reconstructing all that) *)

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

  let

    val () = case Ctree.get_obj I pt p of

      Ctree.PblObj _ => ()

    | _ => raise ERROR "reset_calchead: uncovered case get_obj"

    val pt = Ctree.update_pbl pt p []

    val pt = Ctree.update_met pt p []

    val pt = Ctree.update_spec pt p References.empty

  in (pt, (p, Pos.Pbl)) end

(**)end(**)