(* Title: generate specific entries into Ctree

    Author: Walther Neuper

    (c) due to copyright terms

 *)

 signature GENERATE_CALC_TREE =

 sig

   datatype pblmet = Method of Method.id | Problem of Problem.id | Upblmet

   datatype mout =

     EmptyMout

   | Error' of string

   | FormKF of TermC.as_string

   | PpcKF of pblmet * Model.item Model.ppc

   | RefinedKF of Problem.id * (I_Model.T * (bool * term) list)

   type test_out = Pos.pos' * Pos.pos' list * mout * Ctree.ctree

   val init_pbl: (string * (term * 'a)) list -> I_Model.T

   val init_pbl': (string * (term * term)) list -> I_Model.T

   val generate_inconsistent_rew: Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context ->

     Pos.pos' -> Ctree.ctree -> Calc.T

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

   val mout2str: mout -> string

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

   (* NONE *)

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

 end

 (**)

 structure Generate(**): GENERATE_CALC_TREE(**) =

 struct

 (**)

 open Ctree

 open Pos

 datatype pblmet =           (*%^%*)

   Upblmet                   (*undefined*)

 | Problem of Problem.id    (*%^%*)

 | Method of Method.id;    (*%^%*)

 fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)

   | pblmet2str (Method metID) = "Method " ^ Method.id_to_string metID (*%^%*)

   | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x)

 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)

 datatype foppFK =                  (* in DG cases div 2 *)

   EmptyFoppFK         (*DG internal*)

 | FormFK of TermC.as_string

 | PpcFK of TermC.as_string Model.ppc

 fun foppFK2str (FormFK ct') ="FormFK " ^ ct'

   | foppFK2str (PpcFK  ppc) ="PpcFK " ^ Model.ppc2str ppc

   | foppFK2str EmptyFoppFK  ="EmptyFoppFK"

 datatype nest = Open | Closed | Nundef;

 fun nest2str Open = "Open"

   | nest2str Closed = "Closed"

   | nest2str Nundef = "Nundef"

 type indent = int;

 datatype edit = EdUndef | Write | Protect;

                                    (* bridge --> kernel *)

                                    (* bridge <-> kernel *)

 (* needed in dialog.sml *)         (* bridge <-- kernel *)

 fun edit2str EdUndef = "EdUndef"

   | edit2str Write = "Write"

   | edit2str Protect = "Protect";

 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)

   Error_ of string                                                         (*<--*)

 | FormKF of cellID * edit * indent * nest * TermC.as_string                   (*<--*)

 | PpcKF of cellID * edit * indent * nest * (pblmet * Model.item Model.ppc) (*<--*)

 | RefineKF of Stool.match list                                             (*<--*)

 | RefinedKF of (Problem.id * ((I_Model.T) * ((bool * term) list)))   (*<--*)

 (* 

   datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout

 *)

 datatype mout =

   FormKF of TermC.as_string

 | PpcKF of (pblmet * Model.item Model.ppc) 

 | RefinedKF of Problem.id * (I_Model.T * (bool * term) list)

 | Error' of string

 | EmptyMout

 fun mout2str (FormKF cterm') = "FormKF " ^ cterm'

   | mout2str (PpcKF  (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ "," ^ Model.itemppc2str itemppc ^ ")"

   | mout2str (RefinedKF  (_, _)) = "mout2str: RefinedKF not impl."

   | mout2str (Error'  str) = "Error' " ^ str

   | mout2str (EmptyMout    ) = "EmptyMout"

 type test_out = Pos.pos' * Pos.pos' list * mout * Ctree.ctree;

 (* init pbl with ...,dsc,empty | [] *)

 fun init_pbl pbt = 

   let

     fun pbt2itm (f, (d, _)) = (0, [], false, f, Model.Inc ((d, []), (TermC.empty, [])))

   in map pbt2itm pbt end

 (* take formal parameters from pbt, for transfer from pbl/met-hierarchy *)

 fun init_pbl' pbt = 

   let 

     fun pbt2itm (f, (d, t)) = (0, [], false, f, Model.Inc((d, [t]), (TermC.empty, [])))

   in map pbt2itm pbt end

 fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =

   let

     val f = get_curr_formula (pt, pos)

     val pos' as (p', _) = (lev_on p, Res)

     val (pt, _) = case subs_opt of

       NONE => cappend_atomic pt p' (is, ctxt) f

         (Tactic.Rewrite thm') (f', []) Inconsistent

     | SOME subs => cappend_atomic pt p' (is, ctxt) f

         (Tactic.Rewrite_Inst (subs, thm')) (f', []) Inconsistent

     val pt = update_branch pt p' TransitiveB

   in (pt, pos') end

 (**)end(**)