(* use"../ME/ctree.sml";

   use"ME/ctree.sml";

   use"ctree.sml";

   W.N.26.10.99

writeln (pr_ptree pr_short pt);

val Nd ( _, ns) = pt;

*)

signature PTREE =

sig

  type ptree

  type envp

  val e_ptree : ptree

  exception PTREE of string

  type branch

  type ostate

  type cellID

  type cid

  type posel

  type pos

  type pos'

  type loc

  type domID

  type pblID

  type metID

  type spec

  type 'a ppc

  type con

  type subs

  type subst

  type env

  type ets

  val ets2str : ets -> string

  type item

  type tac

  type tac_

  val tac_2str : tac_ -> string

  type safe

  val safe2str : safe -> string

  type meth

  val cappend_atomic : ptree -> pos -> loc -> cterm' -> tac

    -> cterm' -> ostate -> cid -> ptree * posel list * cid

  val cappend_form : ptree

    -> pos -> loc -> cterm' -> cid -> ptree * pos * cid

  val cappend_parent : ptree -> pos -> loc -> cterm' -> tac

    -> branch -> cid -> ptree * int list * cid

  val cappend_problem : ptree -> posel list(*FIXME*) -> loc

    -> cterm' list * spec -> cid -> ptree * int list * cellID list

  val append_result : ptree -> pos -> cterm' -> ostate -> ptree * pos

  type ppobj

  val g_branch : ppobj -> branch

  val g_cell : ppobj -> cid

  val g_args : ppobj -> (int * (term list)) list (*args of scr*)

  val g_form : ppobj -> cterm'

  val g_loc : ppobj -> loc

  val g_met : ppobj -> meth

  val g_domID : ppobj -> domID

  val g_metID : ppobj -> metID

  val g_model : ppobj -> cterm' ppc

  val g_tac : ppobj -> tac

  val g_origin : ppobj -> cterm' list * spec

  val g_ostate : ppobj -> ostate

  val g_pbl : ppobj -> pblID * item ppc

  val g_result : ppobj -> cterm'

  val g_spec : ppobj -> spec

(*  val get_all : (ppobj -> 'a) -> ptree -> 'a list

  val get_alls : (ppobj -> 'a) -> ptree list -> 'a list *)

  val get_obj : (ppobj -> 'a) -> ptree -> pos -> 'a     

  val gpt_cell : ptree -> cid

  val par_pblobj : ptree -> pos -> pos

  val pre_pos : pos -> pos

  val lev_dn : int list -> int list

  val lev_on : pos -> posel list

  val lev_pred : pos -> pos

  val lev_up : pos -> pos

(*  val pr_cell : pos -> ppobj -> string

  val pr_pos : int list -> string        *)

  val pr_ptree : (pos -> ppobj -> string) -> ptree -> string

  val pr_short : pos -> ppobj -> string

(*  val repl : 'a list -> int -> 'a -> 'a list

  val repl_app : 'a list -> int -> 'a -> 'a list

  val repl_branch : branch -> ppobj -> ppobj

  val repl_domID : domID -> ppobj -> ppobj

  val repl_form : cterm' -> ppobj -> ppobj

  val repl_met : item ppc -> ppobj -> ppobj

  val repl_metID : metID -> ppobj -> ppobj

  val repl_model : cterm' list -> ppobj -> ppobj

  val repl_tac : tac -> ppobj -> ppobj

  val repl_pbl : item ppc -> ppobj -> ppobj

  val repl_pblID : pblID -> ppobj -> ppobj

  val repl_result : cterm' -> ostate -> ppobj -> ppobj

  val repl_spec : spec -> ppobj -> ppobj

  val repl_subs : (string * string) list -> ppobj -> ppobj

  val test_trans : ppobj -> bool

  val uni__asm : (string * pos) list -> ppobj -> ppobj

  val uni__cid : cellID list -> ppobj -> ppobj                 *)

  val union_asm : ptree -> pos -> (string * pos) list -> ptree

  val union_cid : ptree -> pos -> cellID list -> ptree

  val update_branch : ptree -> pos -> branch -> ptree

  val update_domID : ptree -> pos -> domID -> ptree

  val update_met : ptree -> pos -> meth -> ptree

  val update_metppc : ptree -> pos -> item ppc -> ptree

  val update_metID : ptree -> pos -> metID -> ptree

  val update_tac : ptree -> pos -> tac -> ptree

  val update_pbl : ptree -> pos -> pblID * item ppc -> ptree

  val update_pblppc : ptree -> pos -> item ppc -> ptree

  val update_pblID : ptree -> pos -> pblID -> ptree

  val update_spec : ptree -> pos -> spec -> ptree

  val update_subs : ptree -> pos -> (string * string) list -> ptree

  val rep_pblobj : ppobj

    -> {branch:branch, cell:cid, env:envp, loc:loc, meth:meth, model:cterm' ppc,

        origin:cterm' list * spec, ostate:ostate, probl:pblID * item ppc,

        result:cterm', spec:spec}

  val rep_prfobj : ppobj

    -> {branch:branch, cell:cid, form:cterm', loc:loc, tac:tac,

        ostate:ostate, result:cterm'}

end 

(* -------------- 

structure Ptree (**): PTREE (**) =

struct

 -------------- *)

type env = (term * term) list;

datatype branch = 

	 NoBranch | AndB | OrB 

       | TransitiveB  (* FIXXXME.8.03: set branch from met in Apply_Method

                         FIXXXME.0402: -"- in Begin_Trans'*)

       | SequenceB | IntersectB | CollectB | MapB;

fun branch2str NoBranch = "NoBranch"

  | branch2str AndB = "AndB"

  | branch2str OrB = "OrB"

  | branch2str TransitiveB = "TransitiveB" 

  | branch2str SequenceB = "SequenceB"

  | branch2str IntersectB = "IntersectB"

  | branch2str CollectB = "CollectB"

  | branch2str MapB = "MapB";

datatype ostate = 

    Incomplete | Complete | Inconsistent(*WN041020 latter unused*);

type cellID = int;     

type cid = cellID list;

type posel = int;     (* roundabout for (some of) nice signatures *)

type pos = posel list;

val pos2str = ints2str';

datatype pos_ = 

    Pbl    (*PblObj-position: problem-type*)

  | Met    (*PblObj-position: method*)

  | Frm    (*PblObj-position: -> Pbl in ME (not by moveDown !)

           | PrfObj-position: formula*)

  | Res    (*PblObj | PrfObj-position: result*)

  | Und;   (*undefined*)

fun pos_2str Pbl = "Pbl"

  | pos_2str Met = "Met"

  | pos_2str Frm = "Frm"

  | pos_2str Res = "Res"

  | pos_2str Und = "Und";

type pos' = pos * pos_;

(*WN.12.03 remembering interator (pos * pos_) for ptree 

	   pos : lev_on, lev_dn, lev_up, 

                 lev_onFrm, lev_dnRes (..see solve Apply_Method !) 

           pos_:

# generate1 sets pos_ if possible  ...?WN0502?NOT...

# generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn

                     exceptions: Begin/End_Trans

# thus generate(1) called in

.# assy, locate_gen 

.# nxt_solv (tac_ -cases); general case: 

  val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'

# WN050220, S(604):

  generate1...(Rewrite(f,..,res))..(pos, pos_)

     cappend_atomic.................pos //////  gets f+res always!!!

        cut_tree....................pos, pos_ 

*)

fun pos'2str (p,p_) = pair2str (ints2str' p, pos_2str p_);

fun pos's2str ps = (strs2str' o (map pos'2str)) ps;

val e_pos' = ([],Und):pos';

fun res2str (t, ts) = pair2str (term2str t, terms2str ts);

fun asm2str (t, p:pos) = pair2str (term2str t, ints2str' p);

fun asms2str asms = (strs2str' o (map asm2str)) asms;

datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)

	 L     (*go left at $*) 

       | R     (*go right at $*)

       | D;     (*go down at Abs*)

type loc_ = lrd list;

fun ldr2str L = "L"

  | ldr2str R = "R"

  | ldr2str D = "D";

fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;

(*26.4.02: never used after introduction of scripts !!!

type loc =  loc_ *        (* + interpreter-state          *)

	    (loc_ * rls') (* -"- for script of the ruleset*)

		option;

val e_loc = ([],None):loc;

val ee_loc = (e_loc,e_loc);*)

datatype safe = Sundef | Safe | Unsafe | Helpless;

fun safe2str Sundef   = "Sundef"

  | safe2str Safe     = "Safe"

  | safe2str Unsafe   = "Unsafe" 

  | safe2str Helpless = "Helpless";

type subs = cterm' list; (*16.11.00 for FE-KE*)

fun subst2str' thy' (s:subst) =

  (strs2str o 

   (map (pair2str o

	 (apsnd (Sign.string_of_term (sign_of (assoc_thy thy')))) o 

	 (apfst (Sign.string_of_term (sign_of (assoc_thy thy'))))))) s;

type scrstate =       (*state for script interpreter*)

	 env(*stack*) (*used to instantiate tac for checking assod

		       12.03.noticed: e_ not updated during execution ?!?*)

	 * loc_       (*location of tac in script*)

	 * term option(*argument of curried functions*)

	 * term       (*value obtained by tac executed

		       updated also after a derivation by 'new_val'*)

	 * safe       (*estimation of how result will be obtained*)

	 * bool;      (*true = strongly .., false = weakly associated: 

					    only used during ass_dn/up*)

val e_scrstate = ([],[],None,e_term,Sundef,false):scrstate;

(*21.8.02 ---> definitions.sml for datatype scr 

type rrlsstate =      (*state for reverse rewriting*)

     (term *          (*the current formula*)

      rule list      (*of reverse rewrite set (#1#)*)

	    list *    (*may be serveral, eg. in norm_rational*)

      (rule *         (*Thm (+ Thm generated from Calc) resulting in ...*)

       (term *        (*... rewrite with ...*)

	term list))   (*... assumptions*)

	  list);      (*derivation from given term to normalform

		       in reverse order with sym_thm; 

                       (#1#) could be extracted from here #1*) --------*)

datatype istate =     (*interpreter state*)

	 Uistate                 (*undefined in modspec, in '_deriv'ation*)

       | ScrState of scrstate    (*for script interpreter*)

       | RrlsState of rrlsstate; (*for reverse rewriting*)

type iist = istate option * istate option;

val e_istate = (ScrState ([],[],None,e_term,Sundef,false)):istate;

(*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*) 

fun rta2str (r,(t,a)) = "\n("^(rule2str r)^",("^(term2str t)^", "^

		      (terms2str a)^"))";

fun istate2str Uistate = "Uistate"

  | istate2str (ScrState (e,l,to,t,s,b):istate) =

    "ScrState ("^ subst2str e ^",\n "^ 

    loc_2str l ^", "^ termopt2str to ^",\n "^

    term2str t ^", "^ safe2str s ^", "^ bool2str b ^")"

  | istate2str (RrlsState (t,t1,rss,rtas)) = 

    "RrlsState ("^(term2str t)^", "^(term2str t1)^", "^

    ((strs2str o (map (strs2str o (map rule2str)))) rss)^", "^

    ((strs2str o (map rta2str)) rtas)^")";

fun istates2str (None, None) = "(#None, #None)"

  | istates2str (None, Some ist) = "(#None,\n#Some "^istate2str ist^")"

  | istates2str (Some ist, None) = "(#Some "^istate2str ist^",\n #None)"

  | istates2str (Some i1, Some i2) = "(#Some "^istate2str i1^",\n #Some "^

				     istate2str i2^")";

fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) =

    (ScrState (env, loc_, topt, v, safe, bool))

  | new_val _ _ = raise error "new_val: only for ScrState";

datatype con = land | lor;

fun subst2subs s = map (pair2str o 

			(apfst (Sign.string_of_term (sign_of thy))) o

			(apsnd (Sign.string_of_term (sign_of thy)))) s;

fun subst2subs' s = map ((apfst (Sign.string_of_term (sign_of thy))) o

			 (apsnd (Sign.string_of_term (sign_of thy)))) s;

fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b);

fun subs2subst thy s = map (isapair2pair o term_of o the o (parse thy)) s;

(*> subs2subst thy ["(bdv,x)","(err,#0)"];

val it =

  [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real")),

   (Free ("err","RealDef.real"),Free ("#0","RealDef.real"))] 

   : (term * term) list*)

(*FE <-> KE: strings*)

datatype tac = 

  Init_Proof of ((cterm' list) * spec) 

(*Init_Proo_Hid of (dgmode * (cterm' list) * spec) 

| Init_Proof                                       7.6.02java-sml*)

| Model_Problem of pblID

| Refine_Problem of pblID              | Refine_Tacitly of pblID

(*| Match_Problem of pblID*)

| Add_Given of cterm'                  | Del_Given of cterm'

| Add_Find of cterm'                   | Del_Find of cterm'

| Add_Relation of cterm'               | Del_Relation of cterm'

| Specify_Theory of domID              | Specify_Problem of pblID

| Specify_Method of metID

| Apply_Method of metID                | Check_Postcond of pblID

| Free_Solve

| Rewrite_Inst of ( subs * thm')       | Rewrite of thm'

                                       | Rewrite_Asm of thm'

| Rewrite_Set_Inst of ( subs * rls')   | Rewrite_Set of rls'        

| Detail_Set_Inst of ( subs * rls')    | Detail_Set of rls'

| End_Detail  (*end of script from next_tac, 

                in solve: switches back to parent script*)

| Derive of rls' (*an input formula using rls*)

| Calculate of string                  | End_Ruleset

            (* plus | minus | times | cancel | pow | sqrt *)

| Substitute of subs                   | Apply_Assumption of cterm' list

| Take of cterm'                       | Take_Inst of cterm'  

| Group of (con * int list ) 

(*| Subproblem_Full of (spec * (cterm' list))   *)

| Subproblem of (domID * pblID)

| CAScmd of cterm'  (*6.6.02 URD: Function formula *)                   

| End_Subproblem

| Split_And                            | Conclude_And

| Split_Or                             | Conclude_Or

| Begin_Trans                          | End_Trans

| Begin_Sequ                           | End_Sequ(* substitute root.env *)

| Split_Intersect                      | End_Intersect

| Check_elementwise of cterm'          | Collect_Trues

| Or_to_List

| Empty_Tac (*TODO.11.6.03 ... of string: could carry msg of (Notappl msg)

	       in 'helpless'*)

| Tac of string(* eg.'repeat'*)

| User (*internal, for ets*)           | End_Proof';(* inout*)

(* tac2str /--> library.sml: needed in dialog.sml for 'separable *)

fun tac2str (ma:tac) = case ma of

    Init_Proof (ppc, spec)  => 

      "Init_Proof "^(pair2str (strs2str ppc, spec2str spec))

  | Model_Problem pblID     => "Model_Problem "^(strs2str pblID)

  | Refine_Tacitly pblID    => "Refine_Tacitly "^(strs2str pblID)

  | Refine_Problem pblID    => "Refine_Problem "^(strs2str pblID)

(*| Match_Problem pblID     => "Match_Problem "^(strs2str pblID)*)

  | Add_Given cterm'        => "Add_Given "^cterm'

  | Del_Given cterm'        => "Del_Given "^cterm'

  | Add_Find cterm'         => "Add_Find "^cterm'

  | Del_Find cterm'         => "Del_Find "^cterm'

  | Add_Relation cterm'     => "Add_Relation "^cterm'

  | Del_Relation cterm'     => "Del_Relation "^cterm'

  | Specify_Theory domID    => "Specify_Theory "^(quote domID    )

  | Specify_Problem pblID   => "Specify_Problem "^(strs2str pblID )

  | Specify_Method metID    => "Specify_Method "^(strs2str metID)

  | Apply_Method metID      => "Apply_Method "^(strs2str metID)

  | Check_Postcond pblID    => "Check_Postcond "^(strs2str pblID)

  | Free_Solve              => "Free_Solve"

  | Rewrite_Inst (subs,thm')=> 

      "Rewrite_Inst "^(pair2str (subs2str subs, spair2str thm'))

  | Rewrite thm'            => "Rewrite "^(spair2str thm')

  | Rewrite_Asm thm'        => "Rewrite_Asm "^(spair2str thm')

  | Rewrite_Set_Inst (subs, rls) => 

      "Rewrite_Set_Inst "^(pair2str (subs2str subs, quote rls))

  | Rewrite_Set rls         => "Rewrite_Set "^(quote rls    )

  | Detail_Set rls          => "Detail_Set "^(quote rls    )

  | Detail_Set_Inst (subs, rls) => 

      "Detail_Set_Inst "^(pair2str (subs2str subs, quote rls))

  | End_Detail              => "End_Detail"

  | Derive rls'             => "Derive "^rls' 

  | Calculate op_           => "Calculate "^op_ 

  | Substitute subs         => "Substitute "^(subs2str subs)	     

  | Apply_Assumption ct's   => "Apply_Assumption "^(strs2str ct's)

  | Take cterm'             => "Take "^(quote cterm'	)

  | Take_Inst cterm'        => "Take_Inst "^(quote cterm' )

  | Group (con, ints)       => 

      "Group "^(pair2str (con2str con, ints2str ints))

  | Subproblem (domID, pblID) => 

      "Subproblem "^(pair2str (domID, strs2str pblID))

(*| Subproblem_Full (spec, cts') => 

      "Subproblem_Full "^(pair2str (spec2str spec, strs2str cts'))*)

  | End_Subproblem          => "End_Subproblem"

  | CAScmd cterm'           => "CAScmd "^(quote cterm')

  | Check_elementwise cterm'=> "Check_elementwise "^(quote cterm') 

  | Or_to_List              => "Or_to_List "

  | Collect_Trues           => "Collect_Trues"

  | Empty_Tac             => "Empty_Tac"

  | Tac string            => "Tac "^string

  | User                    => "User"

  | End_Proof'              => "tac End_Proof'"

  | _                       => "tac2str not impl. for ?!";

fun is_rewset (Rewrite_Set_Inst _) = true 

  | is_rewset (Rewrite_Set _) = true 

  | is_rewset _ = false;

fun tac2IDstr (ma:tac) = case ma of

    Model_Problem _     => "Model_Problem"

  | Refine_Tacitly pblID    => "Refine_Tacitly"

  | Refine_Problem pblID    => "Refine_Problem"

  | Add_Given cterm'        => "Add_Given"

  | Del_Given cterm'        => "Del_Given"

  | Add_Find cterm'         => "Add_Find"

  | Del_Find cterm'         => "Del_Find"

  | Add_Relation cterm'     => "Add_Relation"

  | Del_Relation cterm'     => "Del_Relation"

  | Specify_Theory domID    => "Specify_Theory"

  | Specify_Problem pblID   => "Specify_Problem"

  | Specify_Method metID    => "Specify_Method"

  | Apply_Method metID      => "Apply_Method"

  | Check_Postcond pblID    => "Check_Postcond"

  | Free_Solve              => "Free_Solve"

  | Rewrite_Inst (subs,thm')=> "Rewrite_Inst"

  | Rewrite thm'            => "Rewrite"

  | Rewrite_Asm thm'        => "Rewrite_Asm"

  | Rewrite_Set_Inst (subs, rls) => "Rewrite_Set_Inst"

  | Rewrite_Set rls         => "Rewrite_Set"

  | Detail_Set rls          => "Detail_Set"

  | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst"

  | Derive rls'             => "Derive "

  | Calculate op_           => "Calculate "

  | Substitute subs         => "Substitute" 

  | Apply_Assumption ct's   => "Apply_Assumption"

  | Take cterm'             => "Take"

  | Take_Inst cterm'        => "Take_Inst"

  | Group (con, ints)       => "Group"

  | Subproblem (domID, pblID) => "Subproblem"

  | End_Subproblem          => "End_Subproblem"

  | CAScmd cterm'           => "CAScmd"

  | Check_elementwise cterm'=> "Check_elementwise"

  | Or_to_List              => "Or_to_List "

  | Collect_Trues           => "Collect_Trues"

  | Empty_Tac             => "Empty_Tac"

  | Tac string            => "Tac "

  | User                    => "User"

  | End_Proof'              => "End_Proof'"

  | _                       => "tac2str not impl. for ?!";

type fmz_ = cterm' list;

type fmz = fmz_ * spec;

val e_fmz = ([],e_spec);

(*tac_ is made from tac in applicable_in,

  and carries all data necessary for generate;*)

datatype tac_ = 

(* datatype tac = *)

  Init_Proof' of ((cterm' list) * spec)

                (* ori list !: code specify -> applicable*)

| Model_Problem' of pblID * 

		    itm list   (*the 'untouched' pbl*)

| Refine_Tacitly' of pblID *    (*input*)

		     pblID *    (*the refined from applicable_in*)

		     domID *    (*from new pbt?! filled in specify*)

		     metID *    (*from new pbt?! filled in specify*)

		     itm list   (*drop ! 9.03: remains [] for

                                  Model_Problem recognizing its activation*)

| Refine_Problem' of (pblID * (itm list * (bool * Term.term) list))

 (*FIXME?040215 drop: done automatically in init_proof + Subproblem'*)

| Add_Given'    of cterm' *

		   itm list (*updated with input in fun specify_additem*)

| Add_Find'     of cterm' *

		   itm list (*updated with input in fun specify_additem*)

| Add_Relation' of cterm' *

		 itm list (*updated with input in fun specify_additem*)

| Del_Given' of cterm'   | Del_Find' of cterm'   | Del_Relation' of cterm'

  (*4.00.: all..    term: in applicable_in ..? Syn ?only for FormFK?*)

| Specify_Theory' of domID              

| Specify_Problem' of (pblID *        (*               *)

		       (bool *        (* matches	     *)

			(itm list *   (* ppc	     *)

			 (bool * term) list))) (* preconditions *)

| Specify_Method' of metID *

		     ori list * (*repl. "#undef"*)

		     itm list   (*... updated from pbl to met*)

| Apply_Method' of metID * 

		   (term option) * (*init_form*)

		   istate		        

| Check_Postcond' of 

  pblID * 

  (term *      (*returnvalue of script in solve*)

   cterm' list)(*collect by get_assumptions_ in applicable_in, except if 

                 butlast tac is Check_elementwise: take only these asms*)

| Free_Solve'

| Rewrite_Inst' of theory' * rew_ord' * rls

  * bool * subst * thm' * term * (term  * term list)

                    (*... form * (result* asumpts  ), saves time*)

| Rewrite' of theory' * rew_ord' * rls * bool * thm' * 

  term * (term * term list)

| Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' * 

  term * (term * term list)

| Rewrite_Set_Inst' of theory' * bool * subst * rls * 

		       term * (term * term list)

| Detail_Set_Inst' of theory' * bool * subst * rls * 

		      term * (term * term list)

| Rewrite_Set' of theory' * bool * rls * term * (term * term list)

| Detail_Set' of theory' * bool * rls * term * (term * term list)

| End_Detail' of (term * (term list)) (*see End_Trans'*)

| End_Ruleset' of term

| Derive' of rls

| Calculate' of theory' * string * term * (term * thm') 

	      (*WN.29.4.03 asm?: * term list??*)

| Substitute' of subst * term (*10.8.00+..*)* term              

| Apply_Assumption' of term list * term

| Take' of term                         | Take_Inst' of term  

| Group' of (con * int list * term)

| Subproblem' of (spec * 

		  (ori list) * (*filled in assod Subproblem'*)

		  term *       (*-"-, headline of calc-head *)

		  fmz_ * 

		  term)        (*Subproblem(dom,pbl)*)  

| CAScmd' of term

| End_Subproblem' of term (*???*)

| Split_And' of term                    | Conclude_And' of term

| Split_Or' of term                     | Conclude_Or' of term

| Begin_Trans' of term                  | End_Trans' of (term * (term list))

| Begin_Sequ'                           | End_Sequ'(* substitute root.env*)

| Split_Intersect' of term              | End_Intersect' of term

| Check_elementwise' of (*special case:*)

  term *   (*(1)the current formula: [x=1,x=...]*)

  string * (*(2)the pred from Check_elementwise   *)

  (term *  (*(3)composed from (1) and (2): {x. pred}*)

   term list) (*20.5.03 assumptions*)

| Or_to_List' of term * term            (* (a | b, [a,b]) *)

| Collect_Trues' of term

| Empty_Tac_                          | Tac_ of  (*for dummies*)

                                            theory *

                                            string * (*form*)

					    string * (*in Tac*)

					    string   (*result of Tac".."*)

| User' (*internal for ets*)            | End_Proof'';(*End_Proof:inout*)

(*TODO?: done partially for tests*)

fun tac_2str ma = case ma of

    Init_Proof' (ppc, spec)  => 

      "Init_Proof' "^(pair2str (strs2str ppc, spec2str spec))

  | Model_Problem' (pblID,_)     => "Model_Problem' "^(strs2str pblID )

  | Refine_Tacitly'(p,prefin,domID,metID,itms)=> 

    "Refine_Tacitly' ("

    ^(strs2str p)^", "^(strs2str prefin)^", "

    ^domID^", "^(strs2str metID)^", pbl-itms)"

  | Refine_Problem' ms       => "Refine_Problem' ("^(*matchs2str ms*)"..."^")"

(*| Match_Problem' (pI, (ok, (itms, pre))) => 

    "Match_Problem' "^(spair2str (strs2str pI,

				  spair2str (bool2str ok,

					     spair2str ("itms2str itms", 

							"items2str pre"))))*)

  | Add_Given' cterm'        => "Add_Given' "(*^cterm'*)

  | Del_Given' cterm'        => "Del_Given' "(*^cterm'*)

  | Add_Find' cterm'         => "Add_Find' "(*^cterm'*)

  | Del_Find' cterm'         => "Del_Find' "(*^cterm'*)

  | Add_Relation' cterm'     => "Add_Relation' "(*^cterm'*)

  | Del_Relation' cterm'     => "Del_Relation' "(*^cterm'*)

  | Specify_Theory' domID    => "Specify_Theory' "^(quote domID    )

  | Specify_Problem' (pI, (ok, (itms, pre))) => 

    "Specify_Problem' "^(spair2str (strs2str pI,

				  spair2str (bool2str ok,

					     spair2str ("itms2str itms", 

							"items2str pre"))))

  | Specify_Method' (pI,oris,itms) => 

    "Specify_Method' ("^metID2str pI^", "^oris2str oris^", )"

  | Apply_Method' (metID,_,_)      => "Apply_Method' "^(strs2str metID)

  | Check_Postcond' (pblID,(scval,asm)) => 

      "Check_Postcond' "^(spair2str(strs2str pblID, 

				    spair2str (term2str scval, strs2str asm)))

  | Free_Solve'              => "Free_Solve'"

  | Rewrite_Inst' (*subs,thm'*) _ => 

      "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)

  | Rewrite' thm'            => "Rewrite' "(*^(spair2str thm')*)

  | Rewrite_Asm' thm'        => "Rewrite_Asm' "(*^(spair2str thm')*)

  | Rewrite_Set_Inst' (*subs,thm'*) _ => 

      "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)

  | Rewrite_Set'(thy',pasm,rls',f,(f',asm))          

    => "Rewrite_Set' ("^thy'^","^(bool2str pasm)^","^(id_rls rls')^","

    ^(Sign.string_of_term (sign_of thy) f)^",("^(Sign.string_of_term (sign_of thy) f')

    ^","^((strs2str o (map (Sign.string_of_term (sign_of thy)))) asm)^"))"

  | End_Detail' _             => "End_Detail' xxx"

  | Detail_Set' _             => "Detail_Set' xxx"

  | Detail_Set_Inst' _        => "Detail_Set_Inst' xxx"

  | Derive' rls              => "Derive' "^id_rls rls

  | Calculate'  _            => "Calculate' "

  | Substitute' subs         => "Substitute' "(*^(subs2str subs)*)    

  | Apply_Assumption' ct's   => "Apply_Assumption' "(*^(strs2str ct's)*)

  | Take' cterm'             => "Take' "(*^(quote cterm'	)*)

  | Take_Inst' cterm'        => "Take_Inst' "(*^(quote cterm' )*)

  | Group' (con, ints, _)     => 

      "Group' "^(pair2str (con2str con, ints2str ints))

  | Subproblem' (spec, oris, _,_,pbl_form) => 

      "Subproblem' "(*^(pair2str (domID, strs2str ,...))*)

  | End_Subproblem'  _       => "End_Subproblem'"

  | CAScmd' cterm'           => "CAScmd' "(*^(quote cterm')*)

  | Empty_Tac_             => "Empty_Tac_"

  | User'                    => "User'"

  | Tac_ (_,form,id,result) => "Tac_ (thy,"^form^","^id^","^result^")"

  | _                       => "tac_2str not impl. for arg";

(*'executed tactics' (tac_s) with local environment etc.;

  used for continuing eval script + for generate*)

type ets =

    (loc_ *      (* of tactic in scr, tactic (weakly) associated with tac_*)

     (tac_ * 	 (* (for generate)  *)

      env *      (* with 'tactic=result' as a rule, tactic ev. _not_ ready:

		  for handling 'parallel let'*)

      env *      (* with results of (ready) tacs        *)

      term *     (* itr_arg of tactic, for upd. env at Repeat, Try*)

      term * 	 (* result value of the tac         *)

      safe))

    list;

val Ets = []:ets;

fun ets2s (l,(m,eno,env,iar,res,s)) = 

  "\n("^(loc_2str l)^",("^(tac_2str m)^

  ",\n  ens= "^(subst2str eno)^

  ",\n  env= "^(subst2str env)^

  ",\n  iar= "^(Sign.string_of_term (sign_of thy) iar)^

  ",\n  res= "^(Sign.string_of_term (sign_of thy) res)^

  ",\n  "^(safe2str s)^"))";

fun ets2str (ets:ets) = (strs2str o (map ets2s)) ets;

type envp =(*9.5.03: unused, delete with field in ptree.PblObj FIXXXME*)

   (int * term list) list * (*assoc-list: args of met*)

   (int * rls) list *       (*assoc-list: tacs already done ///15.9.00*)

   (int * ets) list *       (*assoc-list: tacs etc. already done*)

   (string * pos) list;     (*asms * from where*)

val empty_envp = ([],[],[],[]):envp; 

datatype ppobj = 

    PrfObj of {cell  : cid,    (* 4.00 superfluous: use cid in DG only!!*)

	       form  : term,    

	       tac : tac,         (* also in istate*)

	       loc   : istate option * istate option, (*for form, result 

13.8.02: (None,None) <==> e_istate ! see update_loc, get_loc*)

	       branch: branch,

	       result: term * term list,    

	                          (*FIXX@ME result:term * term list

				   => applicable_in =..rewrite_set_

			           => rls = {erls: rls (NOT rls'),...}*)

	       ostate: ostate}    (*Complete <=> result is OK*)

  | PblObj of {cell  : cid,       (*unused*)

	       fmz   : fmz,       (*from init:FIXME never use this spec;-drop*)

	       origin: (ori list) * (*representation from fmz+pbt

                                  for efficiently adding items in probl, meth*)

		       spec *     (*updated by Refine_Tacitly*)

		       term,      (*headline of calc-head*)

	       spec  : spec,      (*explicitly input*)

	       probl : itm list,  (*itms explicitly input*)

	       meth  : itm list,  (*itms automatically added to copy of probl*)

	       env   : istate option,(*for _sub_problem, if no init_form*)

	       loc   : istate option * istate option, (*for pbl+met, result*)

	       branch: branch,

	       result: term * term list,

	       ostate: ostate};   (*Complete <=> result is _proven_ OK*)

datatype ptree = 

    EmptyPtree

  | Nd of ppobj * (ptree list);

val e_ptree = EmptyPtree;

fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =

  {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};

fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,env,

			loc,branch,result,ostate}) =

  {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,meth=meth,

   env=env,loc=loc,branch=branch,result=result,ostate=ostate};

fun is_prfobj (PrfObj _) = true

  | is_prfobj _ =false;

(*val is_prfobj' = get_obj is_prfobj; *)

fun is_pblobj (PblObj _) = true

  | is_pblobj _ = false;

(*val is_pblobj' = get_obj is_pblobj; 'Error: unbound constructor get_obj'*)

exception PTREE of string;

fun nth _ []      = raise PTREE "nth _ []"

  | nth 1 (x::xs) = x

  | nth n (x::xs) = nth (n-1) xs;

(*> nth 2 [11,22,33]; -->> val it = 22 : int*)

fun lev_up ([]:pos) = raise PTREE "lev_up []"

  | lev_up p = (drop_last p):pos;

fun lev_on ([]:pos) = raise PTREE "lev_on []"

  | lev_on pos = 

    let val len = length pos

    in (drop_last pos) @ [(nth len pos)+1] end;

fun lev_onFrm ((p,_):pos') = (lev_on p,Frm):pos'

  | lev_onFrm p = raise PTREE ("*** lev_onFrm: pos'="^(pos'2str p));

(*040216: for inform --> embed_deriv: remains on same level*)

fun lev_back (([],_):pos') = raise PTREE "lev_on_back: called by ([],_)"

  | lev_back (p,_) =

    if last_elem p <= 1 then (p, Frm):pos' 

    else ((drop_last p) @ [(nth (length p) p) - 1], Res);

(*.increase pos by n within a level.*)

fun pos_plus 0 pos = pos

  | pos_plus n ((p,Frm):pos') = pos_plus (n-1) (p, Res)

  | pos_plus n ((p,  _):pos') = pos_plus (n-1) (lev_on p, Res);

fun lev_pred ([]:pos) = raise PTREE "lev_pred []"

  | lev_pred (pos:pos) = 

    let val len = length pos

    in ((drop_last pos) @ [(nth len pos)-1]):pos end;

(*lev_pred [1,2,3];

val it = [1,2,2] : pos

> lev_pred [1];

val it = [0] : pos          *)

fun lev_dn p = p @ [0];

(*> (lev_dn o lev_on) [1,2,3];

val it = [1,2,4,0] : pos    *)

(*fun lev_dn' ((p,p_):pos') = (lev_dn p, Frm):pos'; WN.3.12.03: never used*)

fun lev_dnRes ((p,_):pos') = (lev_dn p, Res):pos';

(*4.4.00*)

fun lev_up_ ((p,Res):pos') = (lev_up p,Res):pos'

  | lev_up_ p' = raise error ("lev_up_: called for "^(pos'2str p'));

fun lev_dn_ ((p,_):pos') = (lev_dn p,Res):pos'

fun ind ((p,_):pos') = length p; (*WN050108 deprecated in favour of lev_of*)

fun lev_of ((p,_):pos') = length p;

(** convert ptree to a string **)

(* convert a pos from list to string *)

fun pr_pos ps = (space_implode "." (map string_of_int ps))^".   ";

(* show hd origin or form only *)

fun pr_short (p:pos) (PblObj {origin = (ori,_,_),...}) = 

  ((pr_pos p) ^ " ----- pblobj -----\n")

(*   ((((Sign.string_of_term (sign_of thy)) o #4 o hd) ori)^" "^

    (((Sign.string_of_term (sign_of thy)) o hd(*!?!*) o #5 o hd) ori))^

   "\n") *)

  | pr_short p (PrfObj {form = form,...}) =

  ((pr_pos p) ^ (term2str form) ^ "\n");

fun pr_cell (p:pos) (PblObj {cell = c, origin = (ori,_,_),...}) = 

  ((ints2str c) ^"   "^ 

   ((((Sign.string_of_term (sign_of thy)) o #4 o hd) ori)^" "^

    (((Sign.string_of_term (sign_of thy)) o hd(*!?!*) o #5 o hd) ori))^

   "\n")

  | pr_cell p (PrfObj {cell = c, form = form,...}) =

  ((ints2str c) ^"   "^ (term2str form) ^ "\n");

(* convert ptree *)

fun pr_ptree f pt =

  let

    fun pr_pt pfn _  EmptyPtree = ""

      | pr_pt pfn ps (Nd (b, [])) = pfn ps b

      | pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^

      (prts pfn (ps:pos) 1 ts)

    and prts pfn ps p [] = ""

      | prts pfn ps p (t::ts) = (pr_pt pfn (ps @ [p]) t)^

      (prts pfn ps (p+1) ts)

  in pr_pt f [] pt end;

(*

> fun prfn ps b = (pr_pos ps)^"   "^b(*TODO*)^"\n";

> val pt = ref EmptyPtree;

> pt:=Nd("root",

       [Nd("xx1",[]),

	Nd("xx2",

	   [Nd("xx2.1.",[]),

	    Nd("xx2.2.",[])]),

	Nd("xx3",[])]);

> writeln (pr_ptree prfn (!pt));

*)

(** access the branches of ptree **)

fun ins_nth 1 e l  = e::l

  | ins_nth n e [] = raise PTREE "ins_nth n e []"

  | ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls);

fun repl []      _ _ = raise PTREE "repl [] _ _"

  | repl (l::ls) 1 e = e::ls

  | repl (l::ls) n e = l::(repl ls (n-1) e);

fun repl_app ls n e = 

    let val lim = 1 + length ls

    in if n > lim then raise PTREE "repl_app: n > lim"

       else if n = lim then ls @ [e]

	    else repl ls n e end;

(*  

> repl [1,2,3] 2 22222;

val it = [1,22222,3] : int list

> repl_app [1,2,3,4] 5 5555;

val it = [1,2,3,4,5555] : int list

> repl_app [1,2,3] 2 22222;

val it = [1,22222,3] : int list

> repl_app [1] 2 22222 ;

val it = [1,22222] : int list

*)

(*.get from obj at pos by f : ppobj -> 'a.*)

fun get_obj f EmptyPtree    _      = raise PTREE "get_obj f EmptyPtree"

  | get_obj f (Nd (b,  _)) []      = f b

  | get_obj f (Nd (b, bs)) (p::ps) =

(* val (f, Nd (b, bs), (p::ps)) = (I, pt, p);

   *)

  let val _ = (nth p bs) handle _ => raise PTREE ("get_obj: pos = "^

			   (ints2str' (p::ps))^" does not exist");

  in (get_obj f (nth p bs) (ps:pos)) 

      (*before WN050419: 'wrong type..' raised also if pos doesn't exist*)

    handle _ => raise PTREE (*"get_obj: at pos = "^

			     (ints2str' (p::ps))^" wrong type of ppobj"*)

			  ("get_obj: pos = "^

			   (ints2str' (p::ps))^" does not exist")

  end;

fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"

  | get_nd n [] = n

  | get_nd (Nd (_,nds)) (pos as p::(ps:pos)) = (get_nd (nth p nds) ps)

    handle _ => raise PTREE ("get_nd: not existent pos = "^(ints2str' pos));

(* for use by get_obj *)

fun g_cell   (PblObj {cell = c,...}) = c

  | g_cell   (PrfObj {cell = c,...}) = c;

fun g_form   (PrfObj {form = f,...}) = f

  | g_form   (PblObj {origin=(_,_,f),...}) = f;

(*  | g_form   _ = raise PTREE "g_form not for PblObj";*)

fun g_origin (PblObj {origin = ori,...}) = ori

  | g_origin _ = raise PTREE "g_origin not for PrfObj";

fun g_fmz (PblObj {fmz = f,...}) = f

  | g_fmz _ = raise PTREE "g_fmz not for PrfObj";

fun g_spec   (PblObj {spec = s,...}) = s

  | g_spec _   = raise PTREE "g_spec not for PrfObj";

fun g_pbl    (PblObj {probl = p,...}) = p

  | g_pbl  _   = raise PTREE "g_pbl not for PrfObj";

fun g_met    (PblObj {meth = p,...}) = p

  | g_met  _   = raise PTREE "g_met not for PrfObj";

fun g_domID  (PblObj {spec = (d,_,_),...}) = d

  | g_domID  _ = raise PTREE "g_metID not for PrfObj";

fun g_metID  (PblObj {spec = (_,_,m),...}) = m

  | g_metID  _ = raise PTREE "g_metID not for PrfObj";

fun g_env    (PblObj {env,...}) = env

  | g_env    _ = raise PTREE "g_env not for PrfObj"; 

fun g_loc    (PblObj {loc = l,...}) = l

  | g_loc    (PrfObj {loc = l,...}) = l;

fun g_branch (PblObj {branch = b,...}) = b

  | g_branch (PrfObj {branch = b,...}) = b;

fun g_tac  (PblObj {spec = (d,p,m),...}) = Apply_Method m

  | g_tac  (PrfObj {tac = m,...}) = m;

fun g_result (PblObj {result = r,...}) = r

  | g_result (PrfObj {result = r,...}) = r;

fun g_ostate (PblObj {ostate = r,...}) = r

  | g_ostate (PrfObj {ostate = r,...}) = r;

fun g_ostate' (Nd (PblObj {ostate = r,...}, _)) = r

  | g_ostate' (Nd (PrfObj {ostate = r,...}, _)) = r;

fun gpt_cell (Nd (PblObj {cell = c,...},_)) = c

  | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c;

(*in CalcTree/Subproblem an 'just_created_' model is created;

  this is filled to 'untouched' by Model/Refine_Problem*)

fun just_created_ (PblObj {meth, probl, spec, ...}) = 

    null meth andalso null probl andalso spec = e_spec;

val e_origin = ([],e_spec,e_term): (ori list) * spec * term;

fun just_created (pt,(p,_):pos') =

    let val ppobj = get_obj I pt p

    in is_pblobj ppobj andalso just_created_ ppobj end;

fun existpt pos pt = can (get_obj I pt) pos;

fun existpt' ((p,p_):pos') pt = 

    if can (get_obj I pt) p 

    then case p_ of 

	     Res => get_obj g_ostate pt p = Complete

	   | _ => true

    else false;

fun fst_onlev (([], Frm):pos') = true

  | fst_onlev (([], Pbl):pos') = true

  | fst_onlev (([], Met):pos') = true

  | fst_onlev (pos, Frm) = last_elem pos = 1

  | fst_onlev _ = false;

fun last_onlev pt pos = not (existpt (lev_on pos) pt);

(*.find the position of the next parent which is a PblObj in ptree.*)

fun par_pblobj pt ([]:pos) = ([]:pos)

  | par_pblobj pt p =

    let fun par pt [] = []

	  | par pt p = if is_pblobj (get_obj I pt p) then p

		       else par pt (lev_up p)

    in par pt (lev_up p) end; 

(* lev_up for hard_gen operating with pos = [...,0] *)

(*.find the position and the children of the next parent which is a PblObj.*)

fun par_children (Nd (PblObj _, children)) ([]:pos) = (children, []:pos)

  | par_children (pt as Nd (PblObj _, children)) p =

    let fun par [] = (children, [])

	  | par p = let val Nd (obj, children) = get_nd pt p

		    in if is_pblobj obj then (children, p) else par (lev_up p)

		    end;

    in par (lev_up p) end; 

(*.get the children of a node in ptree.*)

fun children (Nd (PblObj _, cn)) = cn

  | children (Nd (PrfObj _, cn)) = cn;

(*.find the next parent, which is either a PblObj (return true)

  or a PrfObj with tac = Detail_Set (return false).*)

(*FIXME.3.4.03:re-organize par_pbl_det after rls' --> rls*)

fun par_pbl_det pt ([]:pos) = (true, []:pos, Erls)

  | par_pbl_det pt p =

    let fun par pt [] = (true, [], Erls)

	  | par pt p = if is_pblobj (get_obj I pt p) then (true, p, Erls)

		       else case get_obj g_tac pt p of

				(*Detail_Set rls' => (false, p, assoc_rls rls')

			      (*^^^--- before 040206 after ---vvv*)

			      |*)Rewrite_Set rls' => (false, p, assoc_rls rls')

			      | Rewrite_Set_Inst (_, rls') => 

				(false, p, assoc_rls rls')

			      | _ => par pt (lev_up p)

    in par pt (lev_up p) end; 

(*.get from the whole ptree by f : ppobj -> 'a.*)

fun get_all f EmptyPtree   = []

  | get_all f (Nd (b, [])) = [f b]

  | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)

and get_alls f [] = []

  | get_alls f pts = flat (map (get_all f) pts);

(*.insert obj b into ptree at pos, ev.overwriting this pos.*)

fun insert b EmptyPtree   ([]:pos)  = Nd (b, [])

  | insert b EmptyPtree    _        = raise PTREE "insert b Empty _"

  | insert b (Nd ( _,  _)) []       = raise PTREE "insert b _ []"

  | insert b (Nd (b', bs)) (p::[])  = 

     Nd (b', repl_app bs p (Nd (b,[]))) 

  | insert b (Nd (b', bs)) (p::ps)  =

     Nd (b', repl_app bs p (insert b (nth p bs) ps));

(*

> type ppobj = string;

> writeln (pr_ptree prfn (!pt));

  val pt = ref Empty;

  pt:= insert ("root":ppobj) EmptyPtree [];

  pt:= insert ("xx1":ppobj) (!pt) [1];

  pt:= insert ("xx2":ppobj) (!pt) [2];

  pt:= insert ("xx3":ppobj) (!pt) [3];

  pt:= insert ("xx2.1":ppobj) (!pt) [2,1];

  pt:= insert ("xx2.2":ppobj) (!pt) [2,2];

  pt:= insert ("xx2.1.1":ppobj) (!pt) [2,1,1];

  pt:= insert ("xx2.1.2":ppobj) (!pt) [2,1,2];

  pt:= insert ("xx2.1.3":ppobj) (!pt) [2,1,3];

*)

(*.insert children to a node without children.*)

(*compare: fun insert*)

fun ins_chn _  EmptyPtree   (_:pos) = raise PTREE "ins_chn: EmptyPtree"

  | ins_chn ns (Nd _)       []      = raise PTREE "ins_chn: pos = []"

  | ins_chn ns (Nd (b, bs)) (p::[]) =

    if p > length bs then raise PTREE "ins_chn: pos not existent"