1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml	Wed Jul 03 15:09:16 2019 +0200
     1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml	Wed Jul 03 15:30:31 2019 +0200
     1.3 @@ -5,22 +5,22 @@
     1.4  
     1.5  signature LUCAS_INTERPRETER =
     1.6  sig
     1.7 -  val determine_next_tactic : Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> Selem.istate * 'a ->
     1.8 +  val determine_next_tactic : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Selem.istate * 'a ->
     1.9      Tac.tac_ * (Selem.istate * 'a) * (term * Selem.safe)
    1.10  
    1.11    datatype locate = Steps of Selem.istate * Lucin.step list | NotLocatable
    1.12 -  val locate_input_tactic : Rule.theory' * Rule.rls -> Tac.tac_ -> Ctree.state -> Rule.scr * 'a ->
    1.13 +  val locate_input_tactic : Rule.theory' * Rule.rls -> Tac.tac_ -> Ctree.state -> Rule.program * 'a ->
    1.14      Selem.istate * Proof.context -> locate
    1.15  
    1.16    datatype input_formula_result =
    1.17      Step of Ctree.state * Selem.istate * Proof.context
    1.18    | Not_Derivable of Chead.calcstate'
    1.19 -  val locate_input_formula : Rule.scr -> Ctree.state -> Selem.istate -> Proof.context -> term
    1.20 +  val locate_input_formula : Rule.program -> Ctree.state -> Selem.istate -> Proof.context -> term
    1.21      -> input_formula_result
    1.22 +  val do_solve_step : Ctree.state ->
    1.23 +    (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state
    1.24    val begin_end_prog : Tac.tac_ -> Selem.istate * Proof.context -> Ctree.state ->
    1.25      (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state
    1.26 -  val do_solve_step : Ctree.state ->
    1.27 -    (Tac.tac * Tac.tac_ * (Ctree.pos' * (Selem.istate * Proof.context))) list * Ctree.pos' list * Ctree.state
    1.28  
    1.29  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.30    type assoc
    1.31 @@ -29,11 +29,11 @@
    1.32    datatype appy = Appy of Tac.tac_ * Selem.scrstate | Napp of LTool.env | Skip of term * LTool.env
    1.33    datatype appy_ = Napp_ | Skip_
    1.34    val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
    1.35 -  val nstep_up : Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> LTool.env ->
    1.36 +  val nstep_up : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> LTool.env ->
    1.37      Celem.lrd list -> appy_ -> term option -> term -> appy
    1.38    val appy : Rule.theory' * Rule.rls -> Ctree.state -> LTool.env -> Celem.lrd list -> term ->
    1.39      term option -> term -> appy
    1.40 -  val nxt_up : Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> LTool.env ->
    1.41 +  val nxt_up : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> LTool.env ->
    1.42      Celem.lrd list -> appy_ -> term -> term option -> term -> appy
    1.43    datatype asap = Aundef | AssOnly  | AssGen;
    1.44    val go : Celem.loc_ -> term -> term

     2.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Wed Jul 03 15:09:16 2019 +0200
     2.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Wed Jul 03 15:30:31 2019 +0200
     2.3 @@ -17,9 +17,9 @@
     2.4    val detailstep : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
     2.5    val get_pblID : Ctree.state -> Celem.pblID option
     2.6  
     2.7 -  val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Rule.scr * Model.itm list * (bool * term) list
     2.8 +  val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Rule.program * Model.itm list * (bool * term) list
     2.9    val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * Model.itm list * (bool * term) list
    2.10 -  val context_met : Celem.metID -> Ctree.ctree -> Ctree.pos -> bool * Celem.metID * Rule.scr * Model.itm list * (bool * term) list
    2.11 +  val context_met : Celem.metID -> Ctree.ctree -> Ctree.pos -> bool * Celem.metID * Rule.program * Model.itm list * (bool * term) list
    2.12    val context_pbl : Celem.pblID -> Ctree.ctree -> Ctree.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
    2.13    val set_method : Celem.metID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
    2.14    val set_problem : Celem.pblID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd

     3.1 --- a/src/Tools/isac/Interpret/script.sml	Wed Jul 03 15:09:16 2019 +0200
     3.2 +++ b/src/Tools/isac/Interpret/script.sml	Wed Jul 03 15:30:31 2019 +0200
     3.3 @@ -11,12 +11,12 @@
     3.4    
     3.5  (* can these functions be local to Lucin or part of LItools ? *)
     3.6    val sel_rules : Ctree.ctree -> Ctree.pos' -> Tac.tac list 
     3.7 -  val init_form : 'a -> Rule.scr -> (term * term) list -> term option
     3.8 +  val init_form : 'a -> Rule.program -> (term * term) list -> term option
     3.9    val tac_2tac : Tac.tac_ -> Tac.tac
    3.10 -  val init_scrstate : theory -> Model.itm list -> Celem.metID -> Selem.istate * Proof.context * Rule.scr
    3.11 -  val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> Rule.rls * (Selem.istate * Proof.context) * Rule.scr
    3.12 +  val init_scrstate : theory -> Model.itm list -> Celem.metID -> Selem.istate * Proof.context * Rule.program
    3.13 +  val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> Rule.rls * (Selem.istate * Proof.context) * Rule.program
    3.14    val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> 
    3.15 -    Rule.rls * (Selem.istate * Proof.context) * Rule.scr
    3.16 +    Rule.rls * (Selem.istate * Proof.context) * Rule.program
    3.17    val rule2thm'' : Rule.rule -> Celem.thm''
    3.18    val rule2rls' : Rule.rule -> string
    3.19    val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Tac.tac list

     4.1 --- a/src/Tools/isac/ThydataC/rule.sml	Wed Jul 03 15:09:16 2019 +0200
     4.2 +++ b/src/Tools/isac/ThydataC/rule.sml	Wed Jul 03 15:30:31 2019 +0200
     4.3 @@ -34,14 +34,14 @@
     4.4      datatype rls
     4.5        =  Erls
     4.6         | Rls of {calc: calc list, erls: rls, errpatts: errpatID list, id: string,
     4.7 -         preconds: term list, rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
     4.8 +         preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rls}
     4.9         | Seq of {calc: calc list, erls: rls, errpatts: errpatID list, id: string,
    4.10 -         preconds: term list, rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
    4.11 +         preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rls}
    4.12         | Rrls of {calc: calc list, erls: rls, errpatts: errpatID list, id: string,
    4.13 -         prepat: (term list * term) list, rew_ord: rew_ord, scr: scr}
    4.14 +         prepat: (term list * term) list, rew_ord: rew_ord, scr: program}
    4.15      and rule = Cal1 of string * eval_fn | Calc of string * eval_fn | Erule
    4.16         | Rls_ of rls | Thm of string * thm
    4.17 -    and scr
    4.18 +    and program
    4.19        =  EmptyScr
    4.20         | Prog of term
    4.21         | Rfuns of
    4.22 @@ -57,14 +57,14 @@
    4.23      val id_rule: rule -> string
    4.24      val eq_rule: rule * rule -> bool
    4.25  
    4.26 -    val scr2str: scr -> string
    4.27 +    val scr2str: program -> string
    4.28      val e_rrls: rls
    4.29  
    4.30      val e_rls: rls
    4.31      val rls2str: rls -> string
    4.32      val id_rls: rls -> string
    4.33      val rep_rls: rls -> {calc: calc list, erls: rls, errpats: errpatID list, id: string,
    4.34 -      preconds: term list, rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
    4.35 +      preconds: term list, rew_ord: rew_ord, rules: rule list, scr: program, srls: rls}
    4.36      val append_rls: string -> rls -> rule list -> rls
    4.37      val merge_rls: string -> rls -> rls -> rls
    4.38      val remove_rls: string -> rls -> rule list -> rls
    4.39 @@ -237,7 +237,7 @@
    4.40                            or left/right-hand-side of eqality .*)
    4.41  	  eval_fn
    4.42  | Rls_ of rls          (*.ie. rule sets may be nested.*)
    4.43 -and scr =
    4.44 +and program =
    4.45      EmptyScr
    4.46    | Prog of term (* a leaf is either a tactic or an 'exp' in 'let v = expr' 
    4.47                      where 'exp' does not contain a tactic. *)
    4.48 @@ -299,7 +299,7 @@
    4.49       calc     : calc list, (*for Calculate in scr, set by prep_rls'                  *)
    4.50       rules    : rule list,                                                           
    4.51       errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy                *)
    4.52 -     scr      : scr}       (*Prog term: generating intermed.steps  *)                
    4.53 +     scr      : program}   (*Prog term: generating intermed.steps  *)                
    4.54    | Seq of (*a sequence of rules to be tried only once                               *)
    4.55      {id : string,          (*for trace_rewrite:=true                                 *)
    4.56       preconds : term list, (*unused 20.8.02                                          *)
    4.57 @@ -311,7 +311,7 @@
    4.58       calc     : calc list, (*for Calculate in scr, set by prep_rls'                  *)
    4.59       rules    : rule list,
    4.60       errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
    4.61 -     scr      : scr}  (*Prog term  (how to restrict type ???)*)
    4.62 +     scr      : program}   (*Prog term  (how to restrict type ???)*)
    4.63  
    4.64    (*Rrls call SML-code and simulate an rls
    4.65      difference: there is always _ONE_ redex rewritten in 1 call,
    4.66 @@ -329,7 +329,7 @@
    4.67       erls     : rls,       (* for the conditions in rules and preconds               *)
    4.68       calc     : calc list, (* for Calculate in scr, set automatic.in prep_rls'       *)
    4.69       errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)              
    4.70 -     scr      : scr};      (* Rfuns {...}  (how to restrict type ???)                *)
    4.71 +     scr      : program};      (* Rfuns {...}  (how to restrict type ???)                *)
    4.72  
    4.73  fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs! TODO "Erls"*)
    4.74    | id_rls (Rls {id, ...}) = id

     5.1 --- a/src/Tools/isac/calcelems.sml	Wed Jul 03 15:09:16 2019 +0200
     5.2 +++ b/src/Tools/isac/calcelems.sml	Wed Jul 03 15:30:31 2019 +0200
     5.3 @@ -606,7 +606,7 @@
     5.4          copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
     5.5          see ME/calchead.sml 'fun is_copy_named'.                                     *)
     5.6        pre        : term list,       (* preconditions in where                        *)
     5.7 -      scr        : Rule.scr         (* progam, empty as @{thm refl} or Rfuns         *)
     5.8 +      scr        : Rule.program     (* progam, empty as @{thm refl} or Rfuns         *)
     5.9  	   };
    5.10  val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = "e_rew_ord'",
    5.11  	erls = Rule.e_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [], crls = Rule.e_rls,

     6.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml	Wed Jul 03 15:09:16 2019 +0200
     6.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml	Wed Jul 03 15:30:31 2019 +0200
     6.3 @@ -40,7 +40,7 @@
     6.4      val rls2xml : int -> Rule.thyID * Rule.rls -> Celem.xml
     6.5      val rule2xml : int -> Celem.guh -> Rule.rule -> Celem.xml
     6.6      val rules2xml : int -> Celem.guh -> Rule.rule list -> Celem.xml
     6.7 -    val scr2xml : int -> Rule.scr -> Celem.xml
     6.8 +    val scr2xml : int -> Rule.program -> Celem.xml
     6.9      val spec2xml : int -> Celem.spec -> Celem.xml
    6.10      val sub2xml : int -> Term.term * Term.term -> Celem.xml
    6.11      val subs2xml : int -> Selem.subs -> Celem.xml

     7.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Wed Jul 03 15:09:16 2019 +0200
     7.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Wed Jul 03 15:30:31 2019 +0200
     7.3 @@ -124,7 +124,7 @@
     7.4                      LucinNEW.Step (cstate, get_istate pt' pos', get_ctxt pt' pos')
     7.5                  | _ => raise ERROR "compare_step: uncovered case"
     7.6  ;
     7.7 -locate_input_formula: scr -> state -> istate -> Proof.context -> term -> input_formula_result;
     7.8 +locate_input_formula: program -> state -> istate -> Proof.context -> term -> input_formula_result;
     7.9  "~~~~~ to inform  return val:"; val () = ();
    7.10      case locate_input_formula prog (pt, pos) istate ctxt f_in of
    7.11        LucinNEW.Step (cstate, _(*istate*), _(*ctxt*)) =>