1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Thu Dec 22 11:55:16 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Thu Dec 22 14:05:55 2016 +0100
     1.3 @@ -11,26 +11,26 @@
     1.4    val nxt_specify_init_calc : Ctree.fmz -> calcstate
     1.5    val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ctree ->
     1.6      Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ctree
     1.7 -  val nxt_specif : Ctree.tac -> Ctree.ctree * Ctree.pos' -> calcstate'
     1.8 +  val nxt_specif : Ctree.tac -> Ctree.state -> calcstate'
     1.9    val nxt_spec : Ctree.pos_ -> bool -> ori list -> spec -> itm list * itm list ->
    1.10      (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac
    1.11  
    1.12 -  val reset_calchead : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos'
    1.13 -  val get_ocalhd : Ctree.ctree * Ctree.pos' -> Ctree.ocalhd
    1.14 +  val reset_calchead : Ctree.state -> Ctree.state
    1.15 +  val get_ocalhd : Ctree.state -> Ctree.ocalhd
    1.16    val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool
    1.17 -  val all_modspec : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' 
    1.18 +  val all_modspec : Ctree.state -> Ctree.state 
    1.19  
    1.20    val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list
    1.21    val insert_ppc' : itm -> itm list -> itm list
    1.22  
    1.23 -  val complete_mod : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos'
    1.24 -  val is_complete_mod : Ctree.ctree * Ctree.pos' -> bool
    1.25 -  val complete_spec : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos'
    1.26 -  val is_complete_spec : Ctree.ctree * Ctree.pos' -> bool
    1.27 +  val complete_mod : Ctree.state -> Ctree.state
    1.28 +  val is_complete_mod : Ctree.state -> bool
    1.29 +  val complete_spec : Ctree.state -> Ctree.state
    1.30 +  val is_complete_spec : Ctree.state -> bool
    1.31    val some_spec : spec -> spec -> spec
    1.32    (* these could go to Ctree ..*)
    1.33    val show_pt : Ctree.ctree -> unit
    1.34 -  val pt_extract : Ctree.ctree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list 
    1.35 +  val pt_extract : Ctree.state -> Ctree.ptform * Ctree.tac option * term list 
    1.36    val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ctree -> (Ctree.pos' * term) list
    1.37  
    1.38    val match_ags : theory -> pat list -> term list -> ori list

     2.1 --- a/src/Tools/isac/Interpret/ctree.sml	Thu Dec 22 11:55:16 2016 +0100
     2.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Thu Dec 22 14:05:55 2016 +0100
     2.3 @@ -6,6 +6,7 @@
     2.4  signature CALC_TREEE =
     2.5  sig (* vvv--- *.sml require these typs incrementally, with these exception -----------------vvv *)
     2.6    (* for ptyps.sml *)
     2.7 +  type state
     2.8    type fmz_ = cterm' list
     2.9    type fmz = fmz_ * spec;
    2.10    val e_fmz : fmz_ * spec                                                  (* for datatypes.sml *)
    2.11 @@ -188,7 +189,7 @@
    2.12    val children : ctree -> ctree list                                           (* for solve.sml *)
    2.13    val get_nd : ctree -> pos -> ctree                                           (* for solve.sml *)
    2.14    val just_created_ : ppobj -> bool                                       (* for mathengine.sml *)
    2.15 -  val just_created : ctree * pos' -> bool                                 (* for mathengine.sml *)
    2.16 +  val just_created : state -> bool                                 (* for mathengine.sml *)
    2.17    val is_curr_endof_calc : ctree -> pos' -> bool                           (* for interface.sml *)
    2.18    val e_origin : ori list * spec * term                                   (* for mathengine.sml *)
    2.19  
    2.20 @@ -214,7 +215,7 @@
    2.21    val get_istate : ctree -> pos' -> istate                                    (* for script.sml *)
    2.22    val get_ctxt : ctree -> pos' -> Proof.context
    2.23    val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
    2.24 -  val get_curr_formula : ctree * pos' -> term
    2.25 +  val get_curr_formula : state -> term
    2.26    val get_assumptions_ : ctree -> pos' -> term list                             (* for appl.sml *)
    2.27  
    2.28    val append_result : ctree -> pos -> istate * Proof.context -> result ->
    2.29 @@ -941,6 +942,7 @@
    2.30    | is_pblobj _ = false;
    2.31  (*val is_pblobj' = get_obj is_pblobj; 'Error: unbound constructor get_obj'*)
    2.32  
    2.33 +type state = ctree * pos'
    2.34  
    2.35  exception PTREE of string;
    2.36  fun nth _ []      = raise PTREE "nth _ []"

     3.1 --- a/src/Tools/isac/Interpret/generate.sml	Thu Dec 22 11:55:16 2016 +0100
     3.2 +++ b/src/Tools/isac/Interpret/generate.sml	Thu Dec 22 14:05:55 2016 +0100
     3.3 @@ -21,13 +21,13 @@
     3.4    val init_istate : Ctree.tac -> term -> Ctree.istate (* for solve.sml *)
     3.5    val init_pbl : (string * (term * 'a)) list -> itm list
     3.6    val init_pbl' : (string * (term * term)) list -> itm list
     3.7 -  val embed_deriv : taci list -> Ctree.ctree * Ctree.pos' -> Ctree.pos' list * (Ctree.ctree * Ctree.pos') (* for inform.sml *)
     3.8 +  val embed_deriv : taci list -> Ctree.state -> Ctree.pos' list * (Ctree.state) (* for inform.sml *)
     3.9    val generate_hard : (* for solve.sml *)
    3.10      theory -> Ctree.tac_ -> Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree
    3.11    val generate : (Ctree.tac * Ctree.tac_ * (Ctree.pos' * (Ctree.istate * Proof.context))) list ->
    3.12      Ctree.ctree * Ctree.pos' list * Ctree.pos' -> Ctree.ctree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
    3.13    val generate_inconsistent_rew : Ctree.subs option * thm'' -> term -> Ctree.istate * Proof.context ->
    3.14 -    Ctree.pos' -> Ctree.ctree -> Ctree.ctree * Ctree.pos' (* for interface.sml *)
    3.15 +    Ctree.pos' -> Ctree.ctree -> Ctree.state (* for interface.sml *)
    3.16  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    3.17  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    3.18  end

     4.1 --- a/src/Tools/isac/Interpret/inform.sml	Thu Dec 22 11:55:16 2016 +0100
     4.2 +++ b/src/Tools/isac/Interpret/inform.sml	Thu Dec 22 14:05:55 2016 +0100
     4.3 @@ -12,14 +12,14 @@
     4.4    val fetchErrorpatterns : Ctree.tac -> errpatID list
     4.5    val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
     4.6    val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
     4.7 -  val find_fillpatterns : Ctree.ctree * Ctree.pos' -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list
     4.8 -  val is_exactly_equal : Ctree.ctree * Ctree.pos' -> string -> string * Ctree.tac
     4.9 +  val find_fillpatterns : Ctree.state -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list
    4.10 +  val is_exactly_equal : Ctree.state -> string -> string * Ctree.tac
    4.11  
    4.12  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    4.13    val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
    4.14    val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
    4.15    val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
    4.16 -  val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.ctree * Ctree.pos') -> term -> string * Chead.calcstate'
    4.17 +  val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
    4.18    val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
    4.19    val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
    4.20      rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list

     5.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Thu Dec 22 11:55:16 2016 +0100
     5.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Thu Dec 22 14:05:55 2016 +0100
     5.3 @@ -11,21 +11,21 @@
     5.4    type NEW (* TODO: refactor "fun me" with calcstate and remove *)
     5.5    val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ctree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ctree
     5.6    val autocalc :
     5.7 -     Ctree.pos' list -> Ctree.pos' -> (Ctree.ctree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ctree * Ctree.pos')
     5.8 +     Ctree.pos' list -> Ctree.pos' -> (Ctree.state) * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.state)
     5.9    val locatetac :
    5.10 -    Ctree.tac -> Ctree.ctree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ctree * Ctree.pos'))
    5.11 +    Ctree.tac -> Ctree.state -> string * (Generate.taci list * Ctree.pos' list * (Ctree.state))
    5.12    val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
    5.13    val detailstep :
    5.14      Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
    5.15 -  val get_pblID : Ctree.ctree * Ctree.pos' -> pblID option
    5.16 +  val get_pblID : Ctree.state -> pblID option
    5.17  
    5.18    val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list
    5.19    val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list
    5.20    val context_met : metID -> Ctree.ctree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list
    5.21    val context_pbl : pblID -> Ctree.ctree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list
    5.22 -  val set_method : metID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd
    5.23 -  val set_problem : pblID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd
    5.24 -  val set_theory : thyID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd
    5.25 +  val set_method : metID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
    5.26 +  val set_problem : pblID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
    5.27 +  val set_theory : thyID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
    5.28    val tryrefine : pblID -> Ctree.ctree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list
    5.29  
    5.30  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    5.31 @@ -34,7 +34,7 @@
    5.32    val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ctree
    5.33    val f2str : Generate.mout -> cterm'
    5.34    val loc_solve_ : string * Ctree.tac_ -> Ctree.ctree *  Ctree.pos' -> lOc_
    5.35 -  val loc_specify_ : Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> lOc_
    5.36 +  val loc_specify_ : Ctree.tac_ -> Ctree.state -> lOc_
    5.37  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    5.38  end
    5.39  

     6.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Thu Dec 22 11:55:16 2016 +0100
     6.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Thu Dec 22 14:05:55 2016 +0100
     6.3 @@ -32,7 +32,7 @@
     6.4    val subs_from : Ctree.istate -> 'a -> guh -> Ctree.subs
     6.5    val guh2rewtac : guh -> Ctree.subs -> Ctree.tac
     6.6    val get_tac_checked : Ctree.ctree -> Ctree.pos' -> Ctree.tac
     6.7 -  val context_thy : Ctree.ctree * Ctree.pos' -> Ctree.tac -> contthy
     6.8 +  val context_thy : Ctree.state -> Ctree.tac -> contthy
     6.9    val distinct_Thm : rule list -> rule list
    6.10    val eq_Thms : string list -> rule -> bool
    6.11    val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->

     7.1 --- a/src/Tools/isac/Interpret/script.sml	Thu Dec 22 11:55:16 2016 +0100
     7.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu Dec 22 14:05:55 2016 +0100
     7.3 @@ -12,9 +12,9 @@
     7.4    datatype locate = NotLocatable | Steps of Ctree.istate * step list
     7.5    
     7.6    val next_tac : (*diss: next-tactic-function*)
     7.7 -    theory' * rls -> Ctree.ctree * Ctree.pos' -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe)
     7.8 +    theory' * rls -> Ctree.state -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe)
     7.9    val locate_gen : (*diss: locate-function*)
    7.10 -    theory' * rls -> Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> scr * 'a -> Ctree.istate * Proof.context -> locate
    7.11 +    theory' * rls -> Ctree.tac_ -> Ctree.state -> scr * 'a -> Ctree.istate * Proof.context -> locate
    7.12  
    7.13  (* can these functions be local to Lucin or part of LItools ? *)
    7.14    val sel_rules : Ctree.ctree -> Ctree.pos' -> Ctree.tac list 
    7.15 @@ -31,7 +31,7 @@
    7.16    datatype asap = Aundef | AssOnly | AssGen
    7.17    datatype appy = Appy of Ctree.tac_ * Ctree.scrstate | Napp of env | Skip of term * env
    7.18    datatype appy_ = Napp_ | Skip_
    7.19 -  val appy : theory' * rls -> Ctree.ctree * Ctree.pos' -> env -> lrd list -> term -> term option -> term -> appy
    7.20 +  val appy : theory' * rls -> Ctree.state -> env -> lrd list -> term -> term option -> term -> appy
    7.21    val formal_args : term -> term list
    7.22    val get_stac : 'a -> term -> term option 
    7.23    val go : loc_ -> term -> term
    7.24 @@ -40,7 +40,7 @@
    7.25    val id_of_scr : term -> string
    7.26     val is_spec_pos : Ctree.pos_ -> bool
    7.27    val itms2args : 'a -> metID -> itm list -> term list
    7.28 -  val nstep_up : theory' * rls -> Ctree.ctree * Ctree.pos' -> scr -> env -> lrd list -> appy_ -> 
    7.29 +  val nstep_up : theory' * rls -> Ctree.state -> scr -> env -> lrd list -> appy_ -> 
    7.30      term option -> term -> appy
    7.31    val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Ctree.tac list
    7.32    val stac2tac : Ctree.ctree -> theory -> term -> Ctree.tac