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

   use"ME/ctree.sml";

   use"ctree.sml";

   W.N.26.10.99

tracing (pr_ptree pr_short pt); 

val Nd ( _, ns) = pt;

*)

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

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 rootthy : ptree -> domID

(*  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*);

fun ostate2str Incomplete = "Incomplete"

  | ostate2str Complete = "Complete"

  | ostate2str Inconsistent = "Inconsistent";

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);

(*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*)

val e_subs = ["(bdv, x)"];

(*._sub_stitution as strings of _e_qualities.*)

type sube = cterm' list;

val e_sube = []:cterm' list;

fun sube2str s = strs2str s;

(*._sub_stitution as _t_erms of _e_qualities.*)

type subte = term list;

val e_subte = []:term list;

fun subte2str ss = terms2str ss;

fun subte2sube ss = map term2str ss;

fun subst2subs s = map (pair2str o (apfst term2str) o (apsnd term2str)) s;

fun subst2subs' s = map ((apfst term2str) o (apsnd term2str)) s;

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*)

(*["bdv=x","err=0"] ---> [(bdv,x), (err,0)]*)

fun sube2subst thy s = map (dest_equals' o term_of o the o (parse thy)) s;

(* val ts = sube2subst thy ["bdv=x","err=0"];

   subst2str' ts;

   *)

fun sube2subte ss = map str2term ss;

fun isasub2subst isasub = ((map isapair2pair) o isalist2list) isasub;

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*)

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

val e_ctxt = ProofContext.init_global @{theory};

type iist = istate option * istate option;

(*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 _ _ = error "new_val: only for ScrState";

datatype con = land | lor;

type spec = 

     domID * (*WN.12.03: is replaced by thy from get_met ?FIXME? in:

	      specify (Init_Proof..), nxt_specify_init_calc,

	      assod (.SubProblem...), stac2tac (.SubProblem...)*)

     pblID * 

     metID;

fun spec2str ((dom,pbl,met)(*:spec*)) = 

  "(" ^ (quote dom) ^ ", " ^ (strs2str pbl) ^ 

  ", " ^ (strs2str met) ^ ")";

(*> spec2str empty_spec;

val it = "(\"\", [], (\"\", \"\"))" : string *)

val empty_spec = (e_domID,e_pblID,e_metID):spec;

val e_spec = empty_spec;

(*.tactics propagate the construction of the calc-tree;

   there are

   (a) 'specsteps' for the specify-phase, and others for the solve-phase

   (b) those of the solve-phase are 'initac's and others;

       initacs start with a formula different from the preceding formula.

   see 'type tac_' for the internal representation of tactics.*)

datatype tac = 

  Init_Proof of ((cterm' list) * spec)

(*'specsteps'...*)

| Model_Problem

| Refine_Problem of pblID              | Refine_Tacitly 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

(*...'specsteps'*)

| Apply_Method of metID 

(*.creates an 'istate' in PblObj.env; in case of 'init_form' 

   creates a formula at ((lev_on o lev_dn) p, Frm) and in this ppobj.'loc' 

   'SOME istate' (at fst of 'loc').

   As each step (in the solve-phase) has a resulting formula (at the front-end)

   Apply_Method also does the 1st step in the script (an 'initac') if there

   is no 'init_form' .*)

| 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 WN0509 drop!*)

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

| Calculate of string (* plus | minus | times | cancel | pow | sqrt *)

| End_Ruleset

| Substitute of sube                   | Apply_Assumption of cterm' list

| Take of cterm'      (*an 'initac'*)

| Take_Inst of cterm'  

| Group of (con * int list ) 

| Subproblem of (domID * pblID) (*an 'initac'*)

| CAScmd of cterm'  (*6.6.02 URD: Function formula; WN0509 drop!*)

| End_Subproblem    (*WN0509 drop!*)

| 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'*WN0509 drop! (ab)used to report syntaxerror   *)

| User           (* internal, for ets*WN0509 drop!                            *)

| 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           => "Model_Problem "

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

  | Refine_Problem pblID    => "Refine_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 sube         => "Substitute "^sube2str sube	     

  | 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 is_rewtac (Rewrite _) = true

  | is_rewtac (Rewrite_Inst _) = true

  | is_rewtac (Rewrite_Asm _) = true

  | is_rewtac tac = is_rewset tac;

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 ?!";

fun rls_of (Rewrite_Set_Inst (_, rls)) = rls

  | rls_of (Rewrite_Set rls) = rls

  | rls_of tac = error ("rls_of: called with tac '"^tac2IDstr tac^"'");

fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) = 

    (thmID, SOME ((subs2subst (assoc_thy "Isac") subs):subst))

  | thm_of_rew (Rewrite  (thmID,_)) = (thmID, NONE)

  | thm_of_rew (Rewrite_Asm (thmID,_)) = (thmID, NONE);

fun rls_of_rewset (Rewrite_Set_Inst (subs,rls)) = 

    (rls, SOME ((subs2subst (assoc_thy "Isac") subs):subst))

  | rls_of_rewset (Rewrite_Set rls) = (rls, NONE)

  | rls_of_rewset (Detail_Set rls) = (rls, NONE)

  | rls_of_rewset (Detail_Set_Inst (subs, rls)) = 

    (rls, SOME ((subs2subst (assoc_thy "Isac") subs):subst));

fun rule2tac _ (Calc (opID, thm)) = Calculate (calID2calcID opID)

  | rule2tac [] (Thm (thmID, thm)) = Rewrite (thmID, string_of_thmI thm)

  | rule2tac subst (Thm (thmID, thm)) = 

    Rewrite_Inst (subst2subs subst, (thmID, string_of_thmI thm))

  | rule2tac [] (Rls_ rls) = Rewrite_Set (id_rls rls)

  | rule2tac subst (Rls_ rls) = 

    Rewrite_Set_Inst (subst2subs subst, (id_rls rls))

  | rule2tac _ rule = 

    error ("rule2tac: called with '" ^ rule2str rule ^ "'");

type fmz_ = cterm' list;

(*.a formalization of an example containing data 

   sufficient for mechanically finding the solution for the example.*)

(*FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, 

  this is done in origin*)

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_ = 

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

| Model_Problem' of pblID * 

		    itm list *  (*the 'untouched' pbl*)

		    itm list    (*the casually completed met*)

| 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 * Proof.context

| 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)

| 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 subte  (*the 'substitution': terms of type bool*) 

		 * term (*to be substituted in*)

		 * term (*resulting from the substitution*)

| 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_ * 

     Proof.context *(* transported from assod to generate1 *)

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

| 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*)

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' ^ "," ^

    term2str f ^ ",(" ^ term2str f' ^ "," ^ terms2str 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= " ^ term2str iar ^

  ",\n  res= " ^ term2str 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  : lrd option,       (* where in form tac has been applied *)

	      (*^^^FIXME.WN0607 rename this field*)

  	  form  : term,             (* where tac is applied to *)   

  	  tac   : tac,              (* also in istate *)

  	  loc   : (istate *         (* script interpreter state *)

  	           Proof.context)   (* context for provers, type inference *)

              option *          (* both for interpreter location on Frm, Pbl, Met *)

              (istate *         (* script interpreter state *)

               Proof.context)   (* context for provers, type inference *)

              option,           (* both for interpreter location on Res *)

                                (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc*)

  	  branch: branch,           (* only rudimentary *)

  	  result: term * term list, (* result and assumptions *)

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

  | PblObj of 

     {cell  : lrd option,       (* unused: meaningful only for some _Prf_Obj *)

	    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, as calculated initially(!)*)

	    spec  : spec,             (* explicitly input *)

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

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

	    env   : (istate * Proof.context) option,

                                (* istate only for initac in script

                                   context for specify phase on this node *)

	    loc   : (istate * Proof.context) option * (istate * Proof.context) option,

                                (* like PrfObj *)

	    branch: branch,           (* like PrfObj *)

	    result: term * term list, (* like PrfObj *)

	    ostate: ostate};          (* like PrfObj *)

(*.this tree contains isac's calculations; TODO.WN03 rename to ctree;

   the structure has been copied from an early version of Theorema(c);

   it has the disadvantage, that there is no space 

   for the first tactic in a script generating the first formula at (p,Frm);

   this trouble has been covered by 'init_form' and 'Take' so far,

   but it is crucial if the first tactic in a script is eg. 'Subproblem';

   see 'type tac ', Apply_Method.

.*)

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' = 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")

(*   ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^

    (((Syntax.string_of_term (thy2ctxt' "Isac")) 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) ^"   "^ 

   ((((Syntax.string_of_term (thy2ctxt' "Isac")) o #4 o hd) ori)^" "^

    (((Syntax.string_of_term (thy2ctxt' "Isac")) 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 = Unsynchronized.ref EmptyPtree;

> pt:=Nd("root'",

       [Nd("xx1",[]),

	Nd("xx2",

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

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

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

> tracing (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  (_:pos)  = 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,...}) = NONE

  | g_cell   (PrfObj {cell = c,...}) = c;(*WN0607 hack for quick introduction of lrd + rewrite-at (thms, calcs)*)

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

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

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

  | g_form' (Nd (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_res (PblObj {result = (r,_),...}) = r

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

fun g_res' (Nd (PblObj {result = (r,_),...}, _)) = r

  | g_res' (Nd (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,...},_)) = NONE

  | 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;

(*.does the pos in the ctree exist ?.*)

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

(*.does the pos' in the ctree exist, ie. extra check for result in the node.*)

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