1.1 --- a/src/Tools/isac/Interpret/Interpret.thy Mon Dec 16 15:56:20 2019 +0100
1.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Tue Dec 17 16:31:46 2019 +0100
1.3 @@ -7,6 +7,7 @@
1.4 imports "~~/src/Tools/isac/Specify/Specify"
1.5 begin
1.6 (* removed all warnings here, only "handle _" remains *)
1.7 + ML_file istate.sml
1.8 ML_file rewtools.sml
1.9 ML_file script.sml
1.10 ML_file inform.sml
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Tools/isac/Interpret/istate.sml Tue Dec 17 16:31:46 2019 +0100
2.3 @@ -0,0 +1,195 @@
2.4 +(* Title: interpreter-state for Lucas-Interpretation
2.5 + Author: Walther Neuper 190724
2.6 + (c) due to copyright terms
2.7 +*)
2.8 +signature INTERPRETER_STATE =
2.9 +sig
2.10 +
2.11 + datatype asap = datatype Istate_Def.asap
2.12 + datatype appy_ = datatype Istate_Def.appy_
2.13 + type pstate = Istate_Def.pstate
2.14 + val e_scrstate: pstate
2.15 + val scrstate2str: pstate -> string
2.16 +
2.17 + datatype T = datatype Istate_Def.T
2.18 + val e_istate: T
2.19 + val istate2str: T -> string
2.20 + val istates2str: T option * T option -> string
2.21 +
2.22 + val the_pstate: T -> pstate
2.23 +
2.24 + val get_act_env: pstate -> (term * Env.T)
2.25 + val get_subst: pstate -> (Env.T * (term option * term))
2.26 +
2.27 + val trans_scan_down2: pstate -> pstate
2.28 + val trans_scan_up2: pstate -> pstate
2.29 + val trans_ass: pstate -> pstate -> pstate
2.30 + val trans_env_act: pstate -> pstate -> pstate
2.31 +
2.32 + val path_down: Celem.path -> pstate -> pstate
2.33 + val path_down_form: (Celem.path * term) -> pstate -> pstate
2.34 + val path_up': Celem.path -> Celem.path
2.35 + val path_up: pstate -> pstate
2.36 + val path_up_down: Celem.path -> pstate -> pstate
2.37 +
2.38 + val set_form: term -> pstate -> pstate
2.39 + val set_path: Celem.path -> pstate -> pstate
2.40 + val set_eval: Rule.rls -> pstate -> pstate
2.41 + val set_act: term -> pstate -> pstate
2.42 + val set_or: asap -> pstate -> pstate
2.43 + val set_appy: appy_ -> pstate -> pstate
2.44 +
2.45 + val set_subst: Env.T -> (term * term) -> pstate -> pstate
2.46 + val set_subst': (term * term) -> pstate -> pstate
2.47 + val set_subst_true: (term option * term) -> pstate -> pstate
2.48 + val set_subst_false: (term option * term) -> pstate -> pstate
2.49 + val set_subst_reset: (term option * term) -> pstate -> pstate
2.50 +
2.51 + val set_env: Env.T -> pstate -> pstate
2.52 + val set_env_true: Env.T -> pstate -> pstate
2.53 + val set_form_env: (term * Env.T) -> pstate -> pstate
2.54 + val set_act_env: (term * Env.T) -> pstate -> pstate
2.55 + val upd_env: term -> pstate -> pstate
2.56 + val upd_env': Env.T * (term * term) -> pstate -> pstate
2.57 + val upd_env'': (term * term) -> pstate -> pstate
2.58 +
2.59 +end
2.60 +
2.61 +(**)
2.62 +structure Istate(**): INTERPRETER_STATE(**) =
2.63 +struct
2.64 +(**)
2.65 +
2.66 +open Celem
2.67 +
2.68 +datatype asap = datatype Istate_Def.asap
2.69 +(*this constructions doesnt allow arbitrary nesting of Or !!! *)
2.70 +fun asap2str ORundef = "ORundef"
2.71 + | asap2str AssOnly = "AssOnly"
2.72 + | asap2str AssGen = "AssGen"
2.73 +
2.74 +datatype appy_ = datatype Istate_Def.appy_
2.75 +fun appy_2str AppUndef_ = "AppUndef_"
2.76 + | appy_2str Napp_ = "Napp_"
2.77 + | appy_2str Skip_ = "Skip_"
2.78 +
2.79 +type pstate = Istate_Def.pstate
2.80 +val e_scrstate =
2.81 + {env = [], path = [], eval = Rule.e_rls, form_arg = NONE, act_arg = Rule.e_term,
2.82 + or = ORundef, finish = AppUndef_, assoc = false}
2.83 +fun topt2str NONE = "NONE"
2.84 + | topt2str (SOME t) = "SOME" ^ Rule.term2str t;
2.85 +fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *)
2.86 + "(" ^ Env.env2str env ^ ", " ^ Celem.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^
2.87 + topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
2.88 + appy_2str finish ^ ", " ^ bool2str assoc ^ ")";
2.89 +
2.90 +(* for handling type T see fun from_pblobj_or_detail', +? *)
2.91 +datatype T = datatype Istate_Def.T
2.92 +val e_istate = Pstate e_scrstate;
2.93 +fun the_pstate (Pstate pst) = pst
2.94 + | the_pstate _ = raise ERROR ("the_pstate called for RrlsStated")
2.95 +
2.96 +fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ",(" ^ Rule.term2str t ^", " ^ Rule.terms2str a ^ "))";
2.97 +fun istate2str Uistate = "Uistate"
2.98 + | istate2str (Pstate pst) =
2.99 + "Pstate " ^ scrstate2str pst
2.100 + | istate2str (RrlsState (t, t1, rss, rtas)) =
2.101 + "RrlsState (" ^ Rule.term2str t ^ ", " ^ Rule.term2str t1 ^ ", " ^
2.102 + (strs2str o (map (strs2str o (map Rule.rule2str)))) rss ^ ", " ^
2.103 + (strs2str o (map rta2str)) rtas ^ ")";
2.104 +fun istates2str (NONE, NONE) = "(#NONE, #NONE)" (* for tests only *)
2.105 + | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME " ^ istate2str ist ^ ")"
2.106 + | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"
2.107 + | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
2.108 +
2.109 +fun get_act_env {env, act_arg, ...} = (act_arg, env)
2.110 +fun get_subst {env, form_arg, act_arg, ...} = (env, (form_arg, act_arg))
2.111 +
2.112 +fun trans_scan_down2 {env, eval, act_arg, or, ...} =
2.113 + {env = env, path = [R], eval = eval, form_arg = NONE, act_arg = act_arg,
2.114 + or = or, finish = AppUndef_, assoc = false}
2.115 +fun trans_scan_up2 {env, path, eval, form_arg, act_arg, or, ...} =
2.116 + {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.117 + or = or, finish = AppUndef_, assoc = false}
2.118 +fun trans_ass {assoc, ...} {env, path, eval, form_arg, act_arg, or, finish, ...} =
2.119 + {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.120 + or = or, finish = finish, assoc = assoc}
2.121 +fun trans_env_act {env, act_arg, ...} {path, eval, form_arg, or, finish, assoc, ...} =
2.122 + {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.123 + or = or, finish = finish, assoc = assoc}
2.124 +
2.125 +
2.126 +fun path_down p {env, path, eval, form_arg, act_arg, or, finish, assoc} =
2.127 + {env = env, path = path @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.128 + or = or, finish = finish, assoc = assoc}
2.129 +fun path_down_form (p, fa) {env, path, eval, act_arg, or, finish, assoc, ...} =
2.130 + {env = env, path = path @ p, eval = eval, form_arg = SOME fa, act_arg = act_arg,
2.131 + or = or, finish = finish, assoc = assoc}
2.132 +fun path_up' [] = raise ERROR "path_up' []"
2.133 + | path_up' path = drop_last path
2.134 +fun path_up {env, path, eval, form_arg, act_arg, or, finish, assoc} =
2.135 + {env = env, path = path_up' path, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.136 + or = or, finish = finish, assoc = assoc}
2.137 +fun path_up_down p {env, path, eval, form_arg, act_arg, or, finish, assoc} =
2.138 + {env = env, path = (path_up' path) @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.139 + or = or, finish = finish, assoc = assoc}
2.140 +
2.141 +fun set_form f {env, path, eval, act_arg, or, finish, assoc, ...} =
2.142 + {env = env, path = path, eval = eval, form_arg = SOME f, act_arg = act_arg,
2.143 + or = or, finish = finish, assoc = assoc}
2.144 +fun set_path p {env, eval, form_arg, act_arg, or, finish, assoc, ...} =
2.145 + {env = env, path = p, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.146 + or = or, finish = finish, assoc = assoc}
2.147 +val set_eval = Istate_Def.set_eval
2.148 +val set_act = Istate_Def.set_act
2.149 +fun set_or or {env, path, eval, form_arg, act_arg, finish, assoc, ...} =
2.150 + {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.151 + or = or, finish = finish, assoc = assoc}
2.152 +fun set_appy fin {env, path, eval, form_arg, act_arg, or, assoc, ...} =
2.153 + {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.154 + or = or, finish = fin, assoc = assoc}
2.155 +
2.156 +fun set_subst env (form_arg, act_arg) {path, eval, or, finish, assoc, ...} =
2.157 + {env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
2.158 + or = or, finish = finish, assoc = assoc}
2.159 +fun set_subst' (form_arg, act_arg) {env, path, eval, or, finish, assoc, ...} =
2.160 + {env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
2.161 + or = or, finish = finish, assoc = assoc}
2.162 +fun set_subst_true (form_arg, act_arg) {env, path, eval, or, finish, ...} =
2.163 + {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.164 + or = or, finish = finish, assoc = true}
2.165 +fun set_subst_false (form_arg, act_arg) {env, path, eval, or, finish, ...} =
2.166 + {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.167 + or = or, finish = finish, assoc = false}
2.168 +fun set_subst_reset (form_arg, act_arg) {env, path, eval, ...} = (*compare NEW OLD usage*)
2.169 + {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.170 + or = ORundef, finish = AppUndef_, assoc = false}
2.171 +
2.172 +fun set_env env {path, eval, form_arg, act_arg, or, finish, assoc, ...} =
2.173 + {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.174 + or = or, finish = finish, assoc = assoc}
2.175 +val set_env_true = Istate_Def.set_env_true
2.176 +fun set_form_env (form_arg, env) {path, eval, act_arg, or, finish, assoc, ...} =
2.177 + {env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
2.178 + or = or, finish = finish, assoc = assoc}
2.179 +fun set_act_env (act_arg, env) {path, eval, form_arg, or, finish, assoc, ...} =
2.180 + {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.181 + or = or, finish = finish, assoc = assoc}
2.182 +fun upd_env form {env, path, eval, form_arg, act_arg, or, finish, assoc} =
2.183 + {env = Env.update env (form, act_arg), path = path, eval = eval, form_arg = form_arg,
2.184 + act_arg = act_arg, or = or, finish = finish, assoc = assoc}
2.185 +fun upd_env' (env, (form, act)) {path, eval, or, finish, assoc, ...} =
2.186 + {env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,
2.187 + or = or, finish = finish, assoc = assoc}
2.188 +fun upd_env'' (form, act) {env, path, eval, or, finish, assoc, ...} =
2.189 + {env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,
2.190 + or = or, finish = finish, assoc = assoc}
2.191 +
2.192 +(*
2.193 + {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
2.194 + or = or, finish = finish, assoc = assoc}
2.195 +*)
2.196 +
2.197 +(**)end(**)
2.198 +
3.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Mon Dec 16 15:56:20 2019 +0100
3.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Tue Dec 17 16:31:46 2019 +0100
3.3 @@ -11,7 +11,7 @@
3.4 ML_file model.sml
3.5 ML_file mstools.sml
3.6 ML_file "specification-elems.sml"
3.7 - ML_file istate.sml
3.8 + ML_file "istate-def.sml"
3.9 ML_file tactic.sml
3.10 ML_file position.sml
3.11 ML_file "ctree-basic.sml"
3.12 @@ -21,9 +21,32 @@
3.13
3.14 ML \<open>
3.15 \<close> ML \<open>
3.16 +signature XXX_DEF =
3.17 +sig
3.18 + datatype xxx_def = Aaa of string | Bbb of string
3.19 +end
3.20 \<close> ML \<open>
3.21 +structure Xxx_Def: XXX_DEF(**) =
3.22 +struct
3.23 + datatype xxx_def = Aaa of string | Bbb of string
3.24 +end
3.25 \<close> ML \<open>
3.26 +Xxx_Def.Aaa "works"
3.27 \<close> ML \<open>
3.28 \<close> ML \<open>
3.29 +\<close> ML \<open>
3.30 +signature XXX =
3.31 +sig
3.32 + datatype xxx = Aaa of string | Bbb of string
3.33 +end
3.34 +\<close> ML \<open>
3.35 +structure Xxx: XXX(**) =
3.36 +struct
3.37 + open Xxx_Def
3.38 + datatype xxx = datatype xxx_def
3.39 +end
3.40 +\<close> ML \<open>
3.41 +Xxx.Aaa "works"
3.42 +\<close> ML \<open>
3.43 \<close>
3.44 end
4.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Mon Dec 16 15:56:20 2019 +0100
4.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Tue Dec 17 16:31:46 2019 +0100
4.3 @@ -8,7 +8,7 @@
4.4 val get_last_formula: CTbasic.state -> term
4.5 val update_branch : CTbasic.ctree -> CTbasic.pos -> CTbasic.branch -> CTbasic.ctree
4.6 val update_ctxt : CTbasic.ctree -> CTbasic.pos -> Proof.context -> CTbasic.ctree
4.7 - val update_env : CTbasic.ctree -> CTbasic.pos -> (Istate.T * Proof.context) option -> CTbasic.ctree
4.8 + val update_env : CTbasic.ctree -> CTbasic.pos -> (Istate_Def.T * Proof.context) option -> CTbasic.ctree
4.9 val update_domID : CTbasic.ctree -> CTbasic.pos -> Rule.domID -> CTbasic.ctree
4.10 val update_met : CTbasic.ctree -> CTbasic.pos -> Model.itm list -> CTbasic.ctree (* =vvv= ? *)
4.11 val update_metppc : CTbasic.ctree -> CTbasic.pos -> Model.itm list -> CTbasic.ctree (* =^^^= ? *)
4.12 @@ -21,28 +21,28 @@
4.13 val update_spec : CTbasic.ctree -> CTbasic.pos -> Celem.spec -> CTbasic.ctree
4.14 val update_tac : CTbasic.ctree -> CTbasic.pos -> Tactic.input -> CTbasic.ctree
4.15
4.16 - val upd_istate_ctxt : CTbasic.state -> Istate.T * Proof.context -> CTbasic.ctree
4.17 - val upd_istate : CTbasic.state -> Istate.T -> CTbasic.ctree
4.18 + val upd_istate_ctxt : CTbasic.state -> Istate_Def.T * Proof.context -> CTbasic.ctree
4.19 + val upd_istate : CTbasic.state -> Istate_Def.T -> CTbasic.ctree
4.20 val upd_ctxt : CTbasic.state ->Proof.context -> CTbasic.ctree
4.21
4.22 - val cappend_form : CTbasic.ctree -> CTbasic.pos -> Istate.T * Proof.context -> term ->
4.23 + val cappend_form : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context -> term ->
4.24 CTbasic.ctree * CTbasic.pos' list
4.25 - val cappend_problem : CTbasic.ctree -> CTbasic.pos -> Istate.T * Proof.context ->
4.26 + val cappend_problem : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context ->
4.27 Selem.fmz -> Model.ori list * Celem.spec * term -> CTbasic.ctree * CTbasic.pos' list
4.28 - val append_result : CTbasic.ctree -> CTbasic.pos -> Istate.T * Proof.context ->
4.29 + val append_result : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context ->
4.30 Selem.result -> CTbasic.ostate -> CTbasic.ctree * 'a list
4.31 val append_atomic : (* for solve.sml *)
4.32 - CTbasic.pos -> Istate.T * Proof.context -> term -> Tactic.input -> Selem.result ->
4.33 + CTbasic.pos -> Istate_Def.T * Proof.context -> term -> Tactic.input -> Selem.result ->
4.34 CTbasic.ostate -> CTbasic.ctree -> CTbasic.ctree
4.35 - val cappend_atomic : CTbasic.ctree -> CTbasic.pos -> Istate.T * Proof.context -> term ->
4.36 + val cappend_atomic : CTbasic.ctree -> CTbasic.pos -> Istate_Def.T * Proof.context -> term ->
4.37 Tactic.input -> Selem.result -> CTbasic.ostate -> CTbasic.ctree * CTbasic.pos' list
4.38 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.39 - val cappend_parent : CTbasic.ctree -> int list -> Istate.T * Proof.context -> term ->
4.40 + val cappend_parent : CTbasic.ctree -> int list -> Istate_Def.T * Proof.context -> term ->
4.41 Tactic.input -> CTbasic.branch -> CTbasic.ctree * CTbasic.pos' list
4.42 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.43 val update_loc' : CTbasic.ctree -> CTbasic.pos ->
4.44 - (Istate.T * Proof.context) option * (Istate.T * Proof.context) option -> CTbasic.ctree
4.45 - val append_problem : int list -> Istate.T * Proof.context -> Selem.fmz ->
4.46 + (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option -> CTbasic.ctree
4.47 + val append_problem : int list -> Istate_Def.T * Proof.context -> Selem.fmz ->
4.48 Model.ori list * Celem.spec * term -> CTbasic.ctree -> CTbasic.ctree
4.49 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.50 end
4.51 @@ -198,11 +198,11 @@
4.52 if p_ = Res
4.53 then
4.54 case for_result of
4.55 - NONE => update_loc' pt p (for_other, SOME (Istate.e_istate(*!!!*), ctxt))
4.56 + NONE => update_loc' pt p (for_other, SOME (Istate_Def.e_istate(*!!!*), ctxt))
4.57 | SOME (istate, _) => update_loc' pt p (for_other, SOME (istate, ctxt))
4.58 else
4.59 case for_other of
4.60 - NONE => update_loc' pt p (SOME (Istate.e_istate(*!!!*), ctxt), for_result)
4.61 + NONE => update_loc' pt p (SOME (Istate_Def.e_istate(*!!!*), ctxt), for_result)
4.62 | SOME (istate, _) => update_loc' pt p (SOME (istate, ctxt), for_result)
4.63 end
4.64
4.65 @@ -263,7 +263,7 @@
4.66 val (ist_form, f) =
4.67 (get_loc pt (p,Frm), get_obj g_form pt p)
4.68 val (pt, cs) = cut_tree pt (p,Frm)
4.69 - val pt = append_atomic p (Istate.e_istate, ContextC.e_ctxt) f r f' s pt
4.70 + val pt = append_atomic p (Istate_Def.e_istate, ContextC.e_ctxt) f r f' s pt
4.71 val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
4.72 in (pt, cs) end
4.73 else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
5.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Mon Dec 16 15:56:20 2019 +0100
5.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Dec 17 16:31:46 2019 +0100
5.3 @@ -23,7 +23,7 @@
5.4 PblObj of
5.5 {branch: branch,
5.6 cell: Celem.lrd option,
5.7 - loc: (Istate.T * Proof.context) option * (Istate.T * Proof.context) option,
5.8 + loc: (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option,
5.9 ostate: ostate,
5.10 result: Selem.result,
5.11
5.12 @@ -33,11 +33,11 @@
5.13 meth: Model.itm list,
5.14 spec: Celem.spec,
5.15 ctxt: Proof.context,
5.16 - env: (Istate.T * Proof.context) option}
5.17 + env: (Istate_Def.T * Proof.context) option}
5.18 | PrfObj of
5.19 {branch: branch,
5.20 cell: Celem.lrd option,
5.21 - loc: (Istate.T * Proof.context) option * (Istate.T * Proof.context) option,
5.22 + loc: (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option,
5.23 ostate: ostate,
5.24 result: Selem.result,
5.25
5.26 @@ -62,7 +62,7 @@
5.27 val is_pblnd : ctree -> bool
5.28
5.29 val g_spec : ppobj -> Celem.spec
5.30 - val g_loc : ppobj -> (Istate.T * Proof.context) option * (Istate.T * Proof.context) option
5.31 + val g_loc : ppobj -> (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option
5.32 val g_form : ppobj -> term
5.33 val g_pbl : ppobj -> Model.itm list
5.34 val g_met : ppobj -> Model.itm list
5.35 @@ -70,17 +70,17 @@
5.36 val g_result : ppobj -> Selem.result
5.37 val g_tac : ppobj -> Tactic.input
5.38 val g_domID : ppobj -> Rule.domID (* for appl.sml TODO: replace by thyID *)
5.39 - val g_env : ppobj -> (Istate.T * Proof.context) option (* for appl.sml *)
5.40 + val g_env : ppobj -> (Istate_Def.T * Proof.context) option (* for appl.sml *)
5.41
5.42 val g_origin : ppobj -> Model.ori list * Celem.spec * term (* for script.sml *)
5.43 - val get_loc : ctree -> pos' -> Istate.T * Proof.context (* for script.sml *)
5.44 - val get_istate : ctree -> pos' -> Istate.T (* for script.sml *)
5.45 + val get_loc : ctree -> pos' -> Istate_Def.T * Proof.context (* for script.sml *)
5.46 + val get_istate : ctree -> pos' -> Istate_Def.T (* for script.sml *)
5.47 val get_ctxt : ctree -> pos' -> Proof.context
5.48 val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
5.49 val get_curr_formula : state -> term
5.50 val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *)
5.51
5.52 - val new_val : term -> Istate.T -> Istate.T
5.53 + val new_val : term -> Istate_Def.T -> Istate_Def.T
5.54 (* for calchead.sml *)
5.55 type cid = cellID list
5.56 type ocalhd = bool * pos_ * term * Model.itm list * (bool * term) list * Celem.spec
5.57 @@ -159,12 +159,12 @@
5.58 type cid = cellID list;
5.59
5.60
5.61 -type iist = Istate.T option * Istate.T option;
5.62 +type iist = Istate_Def.T option * Istate_Def.T option;
5.63 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
5.64
5.65
5.66 -fun new_val v (Istate.Pstate pst) =
5.67 - (Istate.Pstate (Istate.set_act v pst))
5.68 +fun new_val v (Istate_Def.Pstate pst) =
5.69 + (Istate_Def.Pstate (Istate_Def.set_act v pst))
5.70 | new_val _ _ = error "new_val: only for Pstate";
5.71
5.72 datatype con = land | lor;
5.73 @@ -201,10 +201,10 @@
5.74 {cell : Celem.lrd option, (* where in form tac has been applied, FIXME.WN0607 rename field *)
5.75 form : term, (* where tac is applied to *)
5.76 tac : Tactic.input, (* also in istate *)
5.77 - loc : (Istate.T * (* script interpreter state *)
5.78 + loc : (Istate_Def.T * (* script interpreter state *)
5.79 Proof.context) (* context for provers, type inference *)
5.80 option * (* both for interpreter location on Frm, Pbl, Met *)
5.81 - (Istate.T * (* script interpreter state *)
5.82 + (Istate_Def.T * (* script interpreter state *)
5.83 Proof.context) (* context for provers, type inference *)
5.84 option, (* both for interpreter location on Res *)
5.85 (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc *)
5.86 @@ -222,10 +222,10 @@
5.87 probl : Model.itm list, (* itms explicitly input *)
5.88 meth : Model.itm list, (* itms automatically added to copy of probl *)
5.89 ctxt : Proof.context, (* WN110513 introduced to avoid [*] [**] *)
5.90 - env : (Istate.T * Proof.context) option, (* istate only for initac in script
5.91 + env : (Istate_Def.T * Proof.context) option, (* istate only for initac in script
5.92 context for specify phase on this node NO..
5.93 ..NO: this conflicts with init_form/initac: see Apply_Method without init_form *)
5.94 - loc : (Istate.T * Proof.context) option * (Istate.T * (* like PrfObj *)
5.95 + loc : (Istate_Def.T * Proof.context) option * (Istate_Def.T * (* like PrfObj *)
5.96 Proof.context) option, (* for spec-phase [*], NO..
5.97 ..NO: raises errors not tracable on WN110513 [**] *)
5.98 branch: branch, (* like PrfObj *)
5.99 @@ -483,16 +483,16 @@
5.100 result = (Rule.e_term, []), ostate = Incomplete};
5.101
5.102
5.103 -fun get_loc EmptyPtree _ = (Istate.e_istate, ContextC.e_ctxt)
5.104 +fun get_loc EmptyPtree _ = (Istate_Def.e_istate, ContextC.e_ctxt)
5.105 | get_loc pt (p, Res) =
5.106 (case get_obj g_loc pt p of
5.107 (SOME i, NONE) => i
5.108 - | (NONE , NONE) => (Istate.e_istate, ContextC.e_ctxt)
5.109 + | (NONE , NONE) => (Istate_Def.e_istate, ContextC.e_ctxt)
5.110 | (_ , SOME i) => i)
5.111 | get_loc pt (p, _) =
5.112 (case get_obj g_loc pt p of
5.113 (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
5.114 - | (NONE , NONE) => (Istate.e_istate, ContextC.e_ctxt)
5.115 + | (NONE , NONE) => (Istate_Def.e_istate, ContextC.e_ctxt)
5.116 | (SOME i, _) => i);
5.117 fun get_istate pt p = get_loc pt p |> #1;
5.118 fun get_ctxt pt (pos as (p, p_)) =
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml Tue Dec 17 16:31:46 2019 +0100
6.3 @@ -0,0 +1,105 @@
6.4 +(* Title: interpreter-state for Lucas-Interpretation
6.5 + Author: Walther Neuper 190724
6.6 + (c) due to copyright terms
6.7 +*)
6.8 +signature INTERPRETER_STATE_DEFINITION =
6.9 +sig
6.10 +
6.11 + datatype asap = ORundef | AssOnly | AssGen;
6.12 + datatype appy_ = AppUndef_ | Napp_ | Skip_
6.13 + type pstate
6.14 + val e_scrstate: pstate
6.15 + val scrstate2str: pstate -> string
6.16 +
6.17 + datatype T = RrlsState of Rule.rrlsstate | Pstate of pstate | Uistate
6.18 + val istate2str: T -> string
6.19 + val istates2str: T option * T option -> string
6.20 + val e_istate: T
6.21 +
6.22 + val set_eval: Rule.rls -> pstate -> pstate
6.23 + val set_act: term -> pstate -> pstate
6.24 + val set_env_true: Env.T -> pstate -> pstate
6.25 +
6.26 +end
6.27 +
6.28 +(**)
6.29 +structure Istate_Def(**): INTERPRETER_STATE_DEFINITION(**) =
6.30 +struct
6.31 +(**)
6.32 +
6.33 +open Celem
6.34 +
6.35 +datatype asap = (* arg. of scan_dn1 _only_ for distinction w.r.t. Or *)
6.36 + ORundef (* undefined: set only by (topmost) Or *)
6.37 +| AssOnly (* do not execute applicable Prog_Tac - there could be an associated
6.38 + in parallel Or-branch *)
6.39 +| AssGen; (* no Ass(Weak) found within Or, thus continue scan
6.40 + search for _applicable_ stacs, execute and generate pt *)
6.41 +(*this constructions doesnt allow arbitrary nesting of Or !!! *)
6.42 +fun asap2str ORundef = "ORundef"
6.43 + | asap2str AssOnly = "AssOnly"
6.44 + | asap2str AssGen = "AssGen"
6.45 +
6.46 +datatype appy_ = (* as argument in scan_up2, go_scan_up2, from scan_dn2 *)
6.47 +(*Accept_Tac2 is only (final) returnvalue, not argument during search *)
6.48 + AppUndef_
6.49 +| Napp_ (* ev. detects 'script is not appropriate for this example' *)
6.50 +| Skip_; (* detects 'script successfully finished'
6.51 + also used as init-value for resuming; this works,
6.52 + because 'nxt_up Or e1' treats as Accept_Tac2 *)
6.53 +fun appy_2str AppUndef_ = "AppUndef_"
6.54 + | appy_2str Napp_ = "Napp_"
6.55 + | appy_2str Skip_ = "Skip_"
6.56 +
6.57 +type pstate =
6.58 + {env: Env.T, (* environment for variables in a program *)
6.59 + path: Celem.path, (* to the current location in a program *)
6.60 + eval: Rule.rls, (* rule-set for evaluating a Prog_Expr *)
6.61 + form_arg: term option,(* argument of a curried function *)
6.62 + act_arg: term, (* value for the curried argument *)
6.63 + or: asap, (* flag for scanning tactical "Or" *)
6.64 + finish: appy_, (* flag set after execution of a tactic *)
6.65 + assoc: bool} (* is the tactic associated to input *)
6.66 +val e_scrstate =
6.67 + {env = [], path = [], eval = Rule.e_rls, form_arg = NONE, act_arg = Rule.e_term,
6.68 + or = ORundef, finish = AppUndef_, assoc = false}
6.69 +fun topt2str NONE = "NONE"
6.70 + | topt2str (SOME t) = "SOME" ^ Rule.term2str t;
6.71 +fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *)
6.72 + "(" ^ Env.env2str env ^ ", " ^ Celem.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^
6.73 + topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
6.74 + appy_2str finish ^ ", " ^ bool2str assoc ^ ")";
6.75 +
6.76 +(* for handling type T see fun from_pblobj_or_detail', +? *)
6.77 +datatype T = (*interpreter state*)
6.78 + Uistate (*undefined in modspec, in '_deriv'ation*)
6.79 + | Pstate of pstate (*for script interpreter*)
6.80 + | RrlsState of Rule.rrlsstate; (*for reverse rewriting*)
6.81 +val e_istate = Pstate e_scrstate;
6.82 +
6.83 +fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ",(" ^ Rule.term2str t ^", " ^ Rule.terms2str a ^ "))";
6.84 +fun istate2str Uistate = "Uistate"
6.85 + | istate2str (Pstate pst) =
6.86 + "Pstate " ^ scrstate2str pst
6.87 + | istate2str (RrlsState (t, t1, rss, rtas)) =
6.88 + "RrlsState (" ^ Rule.term2str t ^ ", " ^ Rule.term2str t1 ^ ", " ^
6.89 + (strs2str o (map (strs2str o (map Rule.rule2str)))) rss ^ ", " ^
6.90 + (strs2str o (map rta2str)) rtas ^ ")";
6.91 +fun istates2str (NONE, NONE) = "(#NONE, #NONE)" (* for tests only *)
6.92 + | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME " ^ istate2str ist ^ ")"
6.93 + | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"
6.94 + | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
6.95 +
6.96 +
6.97 +fun set_eval e {env, path, form_arg, act_arg, or, finish, assoc, ...} =
6.98 + {env = env, path = path, eval = e, form_arg = form_arg, act_arg = act_arg,
6.99 + or = or, finish = finish, assoc = assoc}
6.100 +fun set_act act {env, path, eval, form_arg, or, finish, assoc, ...} =
6.101 + {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act,
6.102 + or = or, finish = finish, assoc = assoc}
6.103 +fun set_env_true env {path, eval, form_arg, act_arg, or, finish, ...} =
6.104 + {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
6.105 + or = or, finish = finish, assoc = true}
6.106 +
6.107 +(**)end(**)
6.108 +
7.1 --- a/src/Tools/isac/MathEngBasic/istate.sml Mon Dec 16 15:56:20 2019 +0100
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,222 +0,0 @@
7.4 -(* Title: interpreter-state for Lucas-Interpretation
7.5 - Author: Walther Neuper 190724
7.6 - (c) due to copyright terms
7.7 -*)
7.8 -signature INTERPRETER_STATE =
7.9 -sig
7.10 -
7.11 - datatype asap = ORundef | AssOnly | AssGen;
7.12 - datatype appy_ = AppUndef_ | Napp_ | Skip_
7.13 - type pstate
7.14 - val e_scrstate: pstate
7.15 - val scrstate2str: pstate -> string
7.16 -
7.17 - datatype T = RrlsState of Rule.rrlsstate | Pstate of pstate | Uistate
7.18 - val istate2str: T -> string
7.19 - val istates2str: T option * T option -> string
7.20 - val e_istate: T
7.21 - val the_pstate: T -> pstate
7.22 -
7.23 - val get_act_env: pstate -> (term * Env.T)
7.24 - val get_subst: pstate -> (Env.T * (term option * term))
7.25 -
7.26 - val trans_scan_down2: pstate -> pstate
7.27 - val trans_scan_up2: pstate -> pstate
7.28 - val trans_ass: pstate -> pstate -> pstate
7.29 - val trans_env_act: pstate -> pstate -> pstate
7.30 -
7.31 - val path_down: Celem.path -> pstate -> pstate
7.32 - val path_down_form: (Celem.path * term) -> pstate -> pstate
7.33 - val path_up': Celem.path -> Celem.path
7.34 - val path_up: pstate -> pstate
7.35 - val path_up_down: Celem.path -> pstate -> pstate
7.36 -
7.37 - val set_form: term -> pstate -> pstate
7.38 - val set_path: Celem.path -> pstate -> pstate
7.39 - val set_eval: Rule.rls -> pstate -> pstate
7.40 - val set_act: term -> pstate -> pstate
7.41 - val set_or: asap -> pstate -> pstate
7.42 - val set_appy: appy_ -> pstate -> pstate
7.43 -
7.44 - val set_subst: Env.T -> (term * term) -> pstate -> pstate
7.45 - val set_subst': (term * term) -> pstate -> pstate
7.46 - val set_subst_true: (term option * term) -> pstate -> pstate
7.47 - val set_subst_false: (term option * term) -> pstate -> pstate
7.48 - val set_subst_reset: (term option * term) -> pstate -> pstate
7.49 -
7.50 - val set_env: Env.T -> pstate -> pstate
7.51 - val set_env_true: Env.T -> pstate -> pstate
7.52 - val set_form_env: (term * Env.T) -> pstate -> pstate
7.53 - val set_act_env: (term * Env.T) -> pstate -> pstate
7.54 - val upd_env: term -> pstate -> pstate
7.55 - val upd_env': Env.T * (term * term) -> pstate -> pstate
7.56 - val upd_env'': (term * term) -> pstate -> pstate
7.57 -
7.58 -end
7.59 -
7.60 -(**)
7.61 -structure Istate(**): INTERPRETER_STATE(**) =
7.62 -struct
7.63 -(**)
7.64 -
7.65 -open Celem
7.66 -
7.67 -datatype asap = (* arg. of scan_dn1 _only_ for distinction w.r.t. Or *)
7.68 - ORundef (* undefined: set only by (topmost) Or *)
7.69 -| AssOnly (* do not execute applicable Prog_Tac - there could be an associated
7.70 - in parallel Or-branch *)
7.71 -| AssGen; (* no Ass(Weak) found within Or, thus continue scan
7.72 - search for _applicable_ stacs, execute and generate pt *)
7.73 -(*this constructions doesnt allow arbitrary nesting of Or !!! *)
7.74 -fun asap2str ORundef = "ORundef"
7.75 - | asap2str AssOnly = "AssOnly"
7.76 - | asap2str AssGen = "AssGen"
7.77 -
7.78 -datatype appy_ = (* as argument in scan_up2, go_scan_up2, from scan_dn2 *)
7.79 -(*Accept_Tac2 is only (final) returnvalue, not argument during search *)
7.80 - AppUndef_
7.81 -| Napp_ (* ev. detects 'script is not appropriate for this example' *)
7.82 -| Skip_; (* detects 'script successfully finished'
7.83 - also used as init-value for resuming; this works,
7.84 - because 'nxt_up Or e1' treats as Accept_Tac2 *)
7.85 -fun appy_2str AppUndef_ = "AppUndef_"
7.86 - | appy_2str Napp_ = "Napp_"
7.87 - | appy_2str Skip_ = "Skip_"
7.88 -
7.89 -type pstate =
7.90 - {env: Env.T, (* environment for variables in a program *)
7.91 - path: Celem.path, (* to the current location in a program *)
7.92 - eval: Rule.rls, (* rule-set for evaluating a Prog_Expr *)
7.93 - form_arg: term option,(* argument of a curried function *)
7.94 - act_arg: term, (* value for the curried argument *)
7.95 - or: asap, (* flag for scanning tactical "Or" *)
7.96 - finish: appy_, (* flag set after execution of a tactic *)
7.97 - assoc: bool} (* is the tactic associated to input *)
7.98 -val e_scrstate =
7.99 - {env = [], path = [], eval = Rule.e_rls, form_arg = NONE, act_arg = Rule.e_term,
7.100 - or = ORundef, finish = AppUndef_, assoc = false}
7.101 -fun topt2str NONE = "NONE"
7.102 - | topt2str (SOME t) = "SOME" ^ Rule.term2str t;
7.103 -fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *)
7.104 - "(" ^ Env.env2str env ^ ", " ^ Celem.path2str path ^ ", " ^ Rule.id_rls eval ^ ", " ^
7.105 - topt2str form_arg ^ ", \n" ^ Rule.term2str act_arg ^ ", " ^ asap2str or ^ ", " ^
7.106 - appy_2str finish ^ ", " ^ bool2str assoc ^ ")";
7.107 -
7.108 -(* for handling type T see fun from_pblobj_or_detail', +? *)
7.109 -datatype T = (*interpreter state*)
7.110 - Uistate (*undefined in modspec, in '_deriv'ation*)
7.111 - | Pstate of pstate (*for script interpreter*)
7.112 - | RrlsState of Rule.rrlsstate; (*for reverse rewriting*)
7.113 -val e_istate = Pstate e_scrstate;
7.114 -fun the_pstate (Pstate pst) = pst
7.115 - | the_pstate _ = raise ERROR ("the_pstate called for RrlsStated")
7.116 -
7.117 -fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ",(" ^ Rule.term2str t ^", " ^ Rule.terms2str a ^ "))";
7.118 -fun istate2str Uistate = "Uistate"
7.119 - | istate2str (Pstate pst) =
7.120 - "Pstate " ^ scrstate2str pst
7.121 - | istate2str (RrlsState (t, t1, rss, rtas)) =
7.122 - "RrlsState (" ^ Rule.term2str t ^ ", " ^ Rule.term2str t1 ^ ", " ^
7.123 - (strs2str o (map (strs2str o (map Rule.rule2str)))) rss ^ ", " ^
7.124 - (strs2str o (map rta2str)) rtas ^ ")";
7.125 -fun istates2str (NONE, NONE) = "(#NONE, #NONE)" (* for tests only *)
7.126 - | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME " ^ istate2str ist ^ ")"
7.127 - | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"
7.128 - | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
7.129 -
7.130 -fun get_act_env {env, act_arg, ...} = (act_arg, env)
7.131 -fun get_subst {env, form_arg, act_arg, ...} = (env, (form_arg, act_arg))
7.132 -
7.133 -fun trans_scan_down2 {env, eval, act_arg, or, ...} =
7.134 - {env = env, path = [R], eval = eval, form_arg = NONE, act_arg = act_arg,
7.135 - or = or, finish = AppUndef_, assoc = false}
7.136 -fun trans_scan_up2 {env, path, eval, form_arg, act_arg, or, ...} =
7.137 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.138 - or = or, finish = AppUndef_, assoc = false}
7.139 -fun trans_ass {assoc, ...} {env, path, eval, form_arg, act_arg, or, finish, ...} =
7.140 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.141 - or = or, finish = finish, assoc = assoc}
7.142 -fun trans_env_act {env, act_arg, ...} {path, eval, form_arg, or, finish, assoc, ...} =
7.143 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.144 - or = or, finish = finish, assoc = assoc}
7.145 -
7.146 -
7.147 -fun path_down p {env, path, eval, form_arg, act_arg, or, finish, assoc} =
7.148 - {env = env, path = path @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.149 - or = or, finish = finish, assoc = assoc}
7.150 -fun path_down_form (p, fa) {env, path, eval, act_arg, or, finish, assoc, ...} =
7.151 - {env = env, path = path @ p, eval = eval, form_arg = SOME fa, act_arg = act_arg,
7.152 - or = or, finish = finish, assoc = assoc}
7.153 -fun path_up' [] = raise ERROR "path_up' []"
7.154 - | path_up' path = drop_last path
7.155 -fun path_up {env, path, eval, form_arg, act_arg, or, finish, assoc} =
7.156 - {env = env, path = path_up' path, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.157 - or = or, finish = finish, assoc = assoc}
7.158 -fun path_up_down p {env, path, eval, form_arg, act_arg, or, finish, assoc} =
7.159 - {env = env, path = (path_up' path) @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.160 - or = or, finish = finish, assoc = assoc}
7.161 -
7.162 -fun set_form f {env, path, eval, act_arg, or, finish, assoc, ...} =
7.163 - {env = env, path = path, eval = eval, form_arg = SOME f, act_arg = act_arg,
7.164 - or = or, finish = finish, assoc = assoc}
7.165 -fun set_path p {env, eval, form_arg, act_arg, or, finish, assoc, ...} =
7.166 - {env = env, path = p, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.167 - or = or, finish = finish, assoc = assoc}
7.168 -fun set_eval e {env, path, form_arg, act_arg, or, finish, assoc, ...} =
7.169 - {env = env, path = path, eval = e, form_arg = form_arg, act_arg = act_arg,
7.170 - or = or, finish = finish, assoc = assoc}
7.171 -fun set_act act {env, path, eval, form_arg, or, finish, assoc, ...} =
7.172 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act,
7.173 - or = or, finish = finish, assoc = assoc}
7.174 -fun set_or or {env, path, eval, form_arg, act_arg, finish, assoc, ...} =
7.175 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.176 - or = or, finish = finish, assoc = assoc}
7.177 -fun set_appy fin {env, path, eval, form_arg, act_arg, or, assoc, ...} =
7.178 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.179 - or = or, finish = fin, assoc = assoc}
7.180 -
7.181 -fun set_subst env (form_arg, act_arg) {path, eval, or, finish, assoc, ...} =
7.182 - {env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
7.183 - or = or, finish = finish, assoc = assoc}
7.184 -fun set_subst' (form_arg, act_arg) {env, path, eval, or, finish, assoc, ...} =
7.185 - {env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
7.186 - or = or, finish = finish, assoc = assoc}
7.187 -fun set_subst_true (form_arg, act_arg) {env, path, eval, or, finish, ...} =
7.188 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.189 - or = or, finish = finish, assoc = true}
7.190 -fun set_subst_false (form_arg, act_arg) {env, path, eval, or, finish, ...} =
7.191 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.192 - or = or, finish = finish, assoc = false}
7.193 -fun set_subst_reset (form_arg, act_arg) {env, path, eval, ...} = (*compare NEW OLD usage*)
7.194 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.195 - or = ORundef, finish = AppUndef_, assoc = false}
7.196 -
7.197 -fun set_env env {path, eval, form_arg, act_arg, or, finish, assoc, ...} =
7.198 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.199 - or = or, finish = finish, assoc = assoc}
7.200 -fun set_env_true env {path, eval, form_arg, act_arg, or, finish, ...} =
7.201 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.202 - or = or, finish = finish, assoc = true}
7.203 -fun set_form_env (form_arg, env) {path, eval, act_arg, or, finish, assoc, ...} =
7.204 - {env = env, path = path, eval = eval, form_arg = SOME form_arg, act_arg = act_arg,
7.205 - or = or, finish = finish, assoc = assoc}
7.206 -fun set_act_env (act_arg, env) {path, eval, form_arg, or, finish, assoc, ...} =
7.207 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.208 - or = or, finish = finish, assoc = assoc}
7.209 -fun upd_env form {env, path, eval, form_arg, act_arg, or, finish, assoc} =
7.210 - {env = Env.update env (form, act_arg), path = path, eval = eval, form_arg = form_arg,
7.211 - act_arg = act_arg, or = or, finish = finish, assoc = assoc}
7.212 -fun upd_env' (env, (form, act)) {path, eval, or, finish, assoc, ...} =
7.213 - {env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,
7.214 - or = or, finish = finish, assoc = assoc}
7.215 -fun upd_env'' (form, act) {env, path, eval, or, finish, assoc, ...} =
7.216 - {env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,
7.217 - or = or, finish = finish, assoc = assoc}
7.218 -
7.219 -(*
7.220 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
7.221 - or = or, finish = finish, assoc = assoc}
7.222 -*)
7.223 -
7.224 -(**)end(**)
7.225 -
8.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Mon Dec 16 15:56:20 2019 +0100
8.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Tue Dec 17 16:31:46 2019 +0100
8.3 @@ -13,7 +13,7 @@
8.4 Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
8.5 | Add_Relation' of Rule.cterm' * Model.itm list
8.6 | Apply_Assumption' of term list * term
8.7 - | Apply_Method' of Celem.metID * term option * Istate.T * Proof.context
8.8 + | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
8.9
8.10 | Begin_Sequ' | Begin_Trans' of term
8.11 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
8.12 @@ -335,7 +335,7 @@
8.13 Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
8.14 | Add_Relation' of Rule.cterm' * Model.itm list
8.15 | Apply_Assumption' of term list * term
8.16 - | Apply_Method' of Celem.metID * term option * Istate.T * Proof.context
8.17 + | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
8.18 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
8.19 | Begin_Sequ' | Begin_Trans' of term
8.20 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
9.1 --- a/src/Tools/isac/Specify/appl.sml Mon Dec 16 15:56:20 2019 +0100
9.2 +++ b/src/Tools/isac/Specify/appl.sml Tue Dec 17 16:31:46 2019 +0100
9.3 @@ -238,7 +238,7 @@
9.4 Implement after all tests are running, since this changes
9.5 overall system behavior*)
9.6 in
9.7 - Appl (Tactic.Apply_Method' (mI, NONE, Istate.e_istate (*filled in solve*), ctxt))
9.8 + Appl (Tactic.Apply_Method' (mI, NONE, Istate_Def.e_istate (*filled in solve*), ctxt))
9.9 end
9.10 | applicable_in (p, p_) _ (Tactic.Check_Postcond pI) =
9.11 if member op = [Pbl, Met] p_
10.1 --- a/src/Tools/isac/Specify/calchead.sml Mon Dec 16 15:56:20 2019 +0100
10.2 +++ b/src/Tools/isac/Specify/calchead.sml Tue Dec 17 16:31:46 2019 +0100
10.3 @@ -71,7 +71,7 @@
10.4
10.5 val nxt_specify_init_calc : Selem.fmz -> calcstate
10.6 val specify : Tactic.T -> Ctree.pos' -> Ctree.cid -> Ctree.ctree ->
10.7 - Ctree.pos' * (Ctree.pos' * Istate.T) * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
10.8 + Ctree.pos' * (Ctree.pos' * Istate_Def.T) * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
10.9 val nxt_specif : Tactic.input -> Ctree.state -> calcstate'
10.10 val nxt_spec : Ctree.pos_ -> bool -> Model.ori list -> Celem.spec -> Model.itm list * Model.itm list ->
10.11 (string * (term * 'a)) list * (string * (term * 'b)) list -> Celem.spec -> Ctree.pos_ * Tactic.input
10.12 @@ -697,7 +697,7 @@
10.13 | "#Find" => Tactic.Add_Find' (ct, met')
10.14 | "#Relate"=> Tactic.Add_Relation'(ct, met')
10.15 | str => error ("specify_additem: uncovered case with " ^ str)
10.16 - val (p, pt') = case Generate.generate1 thy arg (Istate.Uistate, ctxt) (p, Met) pt of
10.17 + val (p, pt') = case Generate.generate1 thy arg (Istate_Def.Uistate, ctxt) (p, Met) pt of
10.18 ((p, Met), _, _, pt') => (p, pt')
10.19 | _ => error "specify_additem: uncovered case of generate1"
10.20 val pre' = Stool.check_preconds thy prls pre met'
10.21 @@ -705,7 +705,7 @@
10.22 val (p_, nxt) =
10.23 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
10.24 ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
10.25 - in ((p, p_), ((p, p_), Istate.Uistate),
10.26 + in ((p, p_), ((p, p_), Istate_Def.Uistate),
10.27 Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Telem.Safe, pt')
10.28 end
10.29 | Err msg =>
10.30 @@ -715,7 +715,7 @@
10.31 val (p_, nxt) =
10.32 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
10.33 ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
10.34 - in ((p,p_), ((p,p_),Istate.Uistate), Generate.Error' msg, nxt, Telem.Safe, pt) end
10.35 + in ((p,p_), ((p,p_),Istate_Def.Uistate), Generate.Error' msg, nxt, Telem.Safe, pt) end
10.36 end
10.37 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
10.38 let
10.39 @@ -737,7 +737,7 @@
10.40 | "#Find" => Tactic.Add_Find' (ct, pbl')
10.41 | "#Relate"=> Tactic.Add_Relation'(ct, pbl')
10.42 | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
10.43 - val (p, pt') = case Generate.generate1 thy arg (Istate.Uistate, ctxt) (p,Pbl) pt of
10.44 + val (p, pt') = case Generate.generate1 thy arg (Istate_Def.Uistate, ctxt) (p,Pbl) pt of
10.45 ((p, Pbl), _, _, pt') => (p, pt')
10.46 | _ => error "specify_additem: uncovered case of Generate.generate1"
10.47 val pre = Stool.check_preconds thy prls where_ pbl'
10.48 @@ -746,7 +746,7 @@
10.49 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
10.50 val ppc = if p_= Pbl then pbl' else met
10.51 in
10.52 - ((p, p_), ((p, p_), Istate.Uistate),
10.53 + ((p, p_), ((p, p_), Istate_Def.Uistate),
10.54 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Telem.Safe, pt')
10.55 end
10.56 | Err msg =>
10.57 @@ -756,7 +756,7 @@
10.58 val (p_, nxt) =
10.59 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
10.60 (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
10.61 - in ((p, p_), ((p, p_), Istate.Uistate), Generate.Error' msg, nxt, Telem.Safe,pt) end
10.62 + in ((p, p_), ((p, p_), Istate_Def.Uistate), Generate.Error' msg, nxt, Telem.Safe,pt) end
10.63 end
10.64
10.65 fun specify (Tactic.Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
10.66 @@ -766,18 +766,18 @@
10.67 if dI' = Rule.e_domID orelse pI' = Celem.e_pblID (*andalso? WN110511*)
10.68 then ([], ContextC.e_ctxt)
10.69 else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
10.70 - val (pt, _) = cappend_problem e_ctree [] (Istate.e_istate, ctxt) (fmz, spec')
10.71 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, ctxt) (fmz, spec')
10.72 (oris, (dI',pI',mI'), Rule.e_term)
10.73 val pt = update_ctxt pt [] ctxt
10.74 val (pbl, pre) = ([], [])
10.75 in
10.76 case mI' of
10.77 ["no_met"] =>
10.78 - (([], Pbl), (([], Pbl), Istate.Uistate),
10.79 + (([], Pbl), (([], Pbl), Istate_Def.Uistate),
10.80 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),
10.81 Tactic.Refine_Tacitly pI', Telem.Safe, pt)
10.82 | _ =>
10.83 - (([], Pbl), (([], Pbl), Istate.Uistate),
10.84 + (([], Pbl), (([], Pbl), Istate_Def.Uistate),
10.85 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),
10.86 Tactic.Model_Problem, Telem.Safe, pt)
10.87 end
10.88 @@ -794,11 +794,11 @@
10.89 val pre = Stool.check_preconds thy prls where_ pbl
10.90 val pb = foldl and_ (true, map fst pre)
10.91 val ((p, _), _, _, pt) =
10.92 - Generate.generate1 thy (Tactic.Model_Problem'([],pbl,met)) (Istate.Uistate, ctxt) pos pt
10.93 + Generate.generate1 thy (Tactic.Model_Problem'([],pbl,met)) (Istate_Def.Uistate, ctxt) pos pt
10.94 val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
10.95 (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');
10.96 in
10.97 - ((p, Pbl), ((p, p_), Istate.Uistate),
10.98 + ((p, Pbl), ((p, p_), Istate_Def.Uistate),
10.99 Generate.PpcKF (Generate.Problem pI', Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),
10.100 nxt, Telem.Safe, pt)
10.101 end
10.102 @@ -811,9 +811,9 @@
10.103 val {met, thy,...} = Specify.get_pbt pIre
10.104 val (domID, metID) = (Rule.string_of_thy thy, if length met = 0 then Celem.e_metID else hd met)
10.105 val ((p,_), _, _, pt) =
10.106 - Generate.generate1 thy (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Istate.Uistate, ctxt) pos pt
10.107 + Generate.generate1 thy (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Istate_Def.Uistate, ctxt) pos pt
10.108 val (pbl, pre, _) = ([], [], false)
10.109 - in ((p, Pbl), (pos, Istate.Uistate),
10.110 + in ((p, Pbl), (pos, Istate_Def.Uistate),
10.111 Generate.PpcKF (Generate.Problem pIre, Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),
10.112 Tactic.Model_Problem, Telem.Safe, pt)
10.113 end
10.114 @@ -821,9 +821,9 @@
10.115 let
10.116 val ctxt = get_ctxt pt pos
10.117 val (pos, _, _, pt) =
10.118 - Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Refine_Problem' rfd) (Istate.Uistate, ctxt) pos pt
10.119 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) pos pt
10.120 in
10.121 - (pos(*p,Pbl*), (pos(*p,Pbl*), Istate.Uistate), Generate.RefinedKF rfd, Tactic.Model_Problem, Telem.Safe, pt)
10.122 + (pos(*p,Pbl*), (pos(*p,Pbl*), Istate_Def.Uistate), Generate.RefinedKF rfd, Tactic.Model_Problem, Telem.Safe, pt)
10.123 end
10.124 (*WN110515 initialise ctxt again from itms and add preconds*)
10.125 | specify (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
10.126 @@ -834,7 +834,7 @@
10.127 | _ => error "specify (Specify_Problem': uncovered case get_obj"
10.128 val thy = Celem.assoc_thy dI
10.129 val (p, pt) =
10.130 - case Generate.generate1 thy (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (Istate.Uistate, ctxt) pos pt of
10.131 + case Generate.generate1 thy (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (Istate_Def.Uistate, ctxt) pos pt of
10.132 ((p, Pbl), _, _, pt) => (p, pt)
10.133 | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
10.134 val dI'' = Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)
10.135 @@ -842,7 +842,7 @@
10.136 val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o Specify.get_pbt) pI,
10.137 (#ppc o Specify.get_met) mI'') (dI, pI, mI);
10.138 in
10.139 - ((p,Pbl), (pos,Istate.Uistate),
10.140 + ((p,Pbl), (pos,Istate_Def.Uistate),
10.141 Generate.PpcKF (Generate.Problem pI, Specify.itms2itemppc dI'' itms pre),
10.142 nxt, Telem.Safe, pt)
10.143 end
10.144 @@ -875,11 +875,11 @@
10.145 else itms
10.146 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
10.147 val (pos, _, _, pt) =
10.148 - Generate.generate1 thy (Tactic.Specify_Method' (mID, oris, itms)) (Istate.Uistate, ctxt) pos pt
10.149 + Generate.generate1 thy (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) pos pt
10.150 val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
10.151 ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID)
10.152 in
10.153 - (pos, (pos,Istate.Uistate),
10.154 + (pos, (pos,Istate_Def.Uistate),
10.155 Generate.PpcKF (Generate.Method mID, Specify.itms2itemppc (Celem.assoc_thy dI'') itms pre'),
10.156 nxt, Telem.Safe, pt)
10.157 end
10.158 @@ -908,16 +908,16 @@
10.159 then
10.160 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
10.161 in
10.162 - ((p, p_), (pos, Istate.Uistate),
10.163 + ((p, p_), (pos, Istate_Def.Uistate),
10.164 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
10.165 nxt, Telem.Safe, pt)
10.166 end
10.167 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
10.168 let
10.169 - val ((p, p_), _, _, pt) = Generate.generate1 thy (Tactic.Specify_Theory' domID) (Istate.Uistate, ctxt) (p,p_) pt
10.170 + val ((p, p_), _, _, pt) = Generate.generate1 thy (Tactic.Specify_Theory' domID) (Istate_Def.Uistate, ctxt) (p,p_) pt
10.171 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
10.172 in
10.173 - ((p,p_), (pos,Istate.Uistate),
10.174 + ((p,p_), (pos,Istate_Def.Uistate),
10.175 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
10.176 nxt, Telem.Safe, pt)
10.177 end
10.178 @@ -944,16 +944,16 @@
10.179 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, pbl'))
10.180 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, pbl'))
10.181 | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
10.182 - val (p, c, pt') = case Generate.generate1 thy tac_ (Istate.Uistate, ctxt) (p,Pbl) pt of
10.183 + val (p, c, pt') = case Generate.generate1 thy tac_ (Istate_Def.Uistate, ctxt) (p,Pbl) pt of
10.184 ((p, Pbl), c, _, pt') => (p, c, pt')
10.185 | _ => error "nxt_specif_additem: uncovered case generate1"
10.186 in
10.187 - ([(tac, tac_, ((p, Pbl), (Istate.Uistate, ctxt)))], c, (pt', (p, Pbl)))
10.188 + ([(tac, tac_, ((p, Pbl), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pbl)))
10.189 end
10.190 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
10.191 FIXME ..and dont abuse a tactic for that purpose*)
10.192 ([(Tactic.Tac msg, Tactic.Tac_ (Rule.Thy_Info_get_theory "Isac_Knowledge", msg,msg,msg),
10.193 - (e_pos', (Istate.e_istate, ContextC.e_ctxt)))], [], ptp)
10.194 + (e_pos', (Istate_Def.e_istate, ContextC.e_ctxt)))], [], ptp)
10.195 end
10.196 | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
10.197 let
10.198 @@ -973,11 +973,11 @@
10.199 | "#Find" => (Tactic.Add_Find ct, Tactic.Add_Find' (ct, met'))
10.200 | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, met'))
10.201 | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
10.202 - val (p, c, pt') = case Generate.generate1 thy tac_ (Istate.Uistate, ctxt) (p, Met) pt of
10.203 + val (p, c, pt') = case Generate.generate1 thy tac_ (Istate_Def.Uistate, ctxt) (p, Met) pt of
10.204 ((p, Met), c, _, pt') => (p, c, pt')
10.205 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
10.206 in
10.207 - ([(tac, tac_, ((p, Met), (Istate.Uistate, ctxt)))], c, (pt', (p, Met)))
10.208 + ([(tac, tac_, ((p, Met), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Met)))
10.209 end
10.210 | Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
10.211 end
10.212 @@ -1056,8 +1056,8 @@
10.213 | _ => complete_mod_ (oris, mpc, ppc, probl)
10.214 (*----------------------------------------------------------------*)
10.215 val tac_ = Tactic.Model_Problem' (pI, pbl, met)
10.216 - val (pos,c,_,pt) = Generate.generate1 thy tac_ (Istate.Uistate, ctxt) pos pt
10.217 - in ([(tac, tac_, (pos, (Istate.Uistate, ContextC.e_ctxt)))], c, (pt,pos)) end
10.218 + val (pos,c,_,pt) = Generate.generate1 thy tac_ (Istate_Def.Uistate, ctxt) pos pt
10.219 + in ([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos)) end
10.220 | nxt_specif (Tactic.Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
10.221 | nxt_specif (Tactic.Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
10.222 | nxt_specif (Tactic.Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
10.223 @@ -1077,10 +1077,10 @@
10.224 val mI = if length met = 0 then Celem.e_metID else hd met
10.225 val thy = Celem.assoc_thy dI
10.226 val (pos, c, _, pt) =
10.227 - Generate.generate1 thy (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate.Uistate, ctxt) pos pt
10.228 + Generate.generate1 thy (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) pos pt
10.229 in
10.230 ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
10.231 - (pos, (Istate.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
10.232 + (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
10.233 end
10.234 | NONE => ([], [], ptp)
10.235 end
10.236 @@ -1096,9 +1096,9 @@
10.237 NONE => ([], [], ptp)
10.238 | SOME rfd =>
10.239 let
10.240 - val (pos,c,_,pt) = Generate.generate1 (Celem.assoc_thy thy) (Tactic.Refine_Problem' rfd) (Istate.Uistate, ctxt) pos pt
10.241 + val (pos,c,_,pt) = Generate.generate1 (Celem.assoc_thy thy) (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) pos pt
10.242 in
10.243 - ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd, (pos, (Istate.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
10.244 + ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd, (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
10.245 end
10.246 end
10.247 | nxt_specif (Tactic.Specify_Problem pI) (pt, pos as (p,_)) =
10.248 @@ -1114,11 +1114,11 @@
10.249 then (false, (Generate.init_pbl ppc, []))
10.250 else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
10.251 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
10.252 - val (c, pt) = case Generate.generate1 thy (Tactic.Specify_Problem' (pI, pbl)) (Istate.Uistate, ctxt) pos pt of
10.253 + val (c, pt) = case Generate.generate1 thy (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) pos pt of
10.254 ((_, Pbl), c, _, pt) => (c, pt)
10.255 | _ => error ""
10.256 in
10.257 - ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl), (pos, (Istate.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
10.258 + ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl), (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
10.259 end
10.260 (* transfers oris (not required in pbl) to met-model for script-env
10.261 FIXME.WN.8.03: application of several mIDs to SAME model? *)
10.262 @@ -1148,25 +1148,25 @@
10.263 else itms
10.264 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
10.265 val (pos, c, _, pt) =
10.266 - Generate.generate1 thy (Tactic.Specify_Method' (mID, oris, itms)) (Istate.Uistate, ctxt) pos pt
10.267 + Generate.generate1 thy (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) pos pt
10.268 in
10.269 - ([(Tactic.Specify_Method mID, Tactic.Specify_Method' (mID, oris, itms), (pos, (Istate.Uistate, ContextC.e_ctxt)))], c, (pt, pos))
10.270 + ([(Tactic.Specify_Method mID, Tactic.Specify_Method' (mID, oris, itms), (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt, pos))
10.271 end
10.272 | nxt_specif (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
10.273 let
10.274 val ctxt = get_ctxt pt pos
10.275 val (pos, c, _, pt) =
10.276 - Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Specify_Theory' dI) (Istate.Uistate, ctxt) pos pt
10.277 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) pos pt
10.278 in (*FIXXXME: check if pbl can still be parsed*)
10.279 - ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate.Uistate, ctxt)))], c,
10.280 + ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c,
10.281 (pt, pos))
10.282 end
10.283 | nxt_specif (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) =
10.284 let
10.285 val ctxt = get_ctxt pt pos
10.286 - val (pos, c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Specify_Theory' dI) (Istate.Uistate, ctxt) pos pt
10.287 + val (pos, c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) pos pt
10.288 in (*FIXXXME: check if met can still be parsed*)
10.289 - ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate.Uistate, ctxt)))], c, (pt, pos))
10.290 + ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos))
10.291 end
10.292 | nxt_specif m' _ = error ("nxt_specif: not impl. for " ^ Tactic.tac2str m')
10.293
10.294 @@ -1184,7 +1184,7 @@
10.295 val dI = if dI = "" then Rule.theory2theory' thy else dI
10.296 val mI = if mI = [] then hd met else mI
10.297 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
10.298 - val (pt,_) = cappend_problem e_ctree [] (Istate.Uistate, ContextC.e_ctxt) ([], (dI, pI, mI))
10.299 + val (pt,_) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.e_ctxt) ([], (dI, pI, mI))
10.300 ([], (dI,pI,mI), hdl)
10.301 val pt = update_spec pt [] (dI, pI, mI)
10.302 val pits = Generate.init_pbl' ppc
10.303 @@ -1197,7 +1197,7 @@
10.304 val {ppc, ...} = Specify.get_met mI
10.305 val dI = if dI = "" then "Isac_Knowledge" else dI
10.306 val (pt, _) =
10.307 - cappend_problem e_ctree [] (Istate.e_istate, ContextC.e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), Rule.e_term (*FIXME met*))
10.308 + cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), Rule.e_term (*FIXME met*))
10.309 val pt = update_spec pt [] (dI, pI, mI)
10.310 val mits = Generate.init_pbl' ppc
10.311 val pt = update_met pt [] mits
10.312 @@ -1205,7 +1205,7 @@
10.313 else (* new example, pepare for interactive modeling *)
10.314 let
10.315 val (pt, _) =
10.316 - cappend_problem e_ctree [] (Istate.e_istate, ContextC.e_ctxt) ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term)
10.317 + cappend_problem e_ctree [] (Istate_Def.e_istate, ContextC.e_ctxt) ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term)
10.318 in ((pt, ([], Pbl)), []) end
10.319 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
10.320 let (* both """"""""""""""""""""""""" either empty or complete *)
10.321 @@ -1226,7 +1226,7 @@
10.322 NONE => Auto_Prog.pblterm dI pI
10.323 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
10.324 val (pt, _) =
10.325 - cappend_problem e_ctree [] (Istate.e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
10.326 + cappend_problem e_ctree [] (Istate_Def.e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
10.327 val pt = update_ctxt pt [] pctxt
10.328 in
10.329 ((pt, ([], Pbl)), fst3 (nxt_specif Tactic.Model_Problem (pt, ([], Pbl))))
11.1 --- a/src/Tools/isac/Specify/generate.sml Mon Dec 16 15:56:20 2019 +0100
11.2 +++ b/src/Tools/isac/Specify/generate.sml Tue Dec 17 16:31:46 2019 +0100
11.3 @@ -16,17 +16,17 @@
11.4 | FormKF of Rule.cterm'
11.5 | PpcKF of pblmet * Model.item Model.ppc
11.6 | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)
11.7 - val generate1 : theory -> Tactic.T -> Istate.T * Proof.context ->
11.8 + val generate1 : theory -> Tactic.T -> Istate_Def.T * Proof.context ->
11.9 Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree (* for calchead.sml------------- ^^^ *)
11.10 - val init_istate : Tactic.input -> term -> Istate.T
11.11 + val init_istate : Tactic.input -> term -> Istate_Def.T
11.12 val init_pbl : (string * (term * 'a)) list -> Model.itm list
11.13 val init_pbl' : (string * (term * term)) list -> Model.itm list
11.14 val embed_deriv : taci list -> Ctree.state -> Ctree.pos' list * (Ctree.state) (* for inform.sml *)
11.15 val generate_hard : (* for solve.sml *)
11.16 theory -> Tactic.T -> Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree
11.17 - val generate : (Tactic.input * Tactic.T * (Ctree.pos' * (Istate.T * Proof.context))) list ->
11.18 + val generate : (Tactic.input * Tactic.T * (Ctree.pos' * (Istate_Def.T * Proof.context))) list ->
11.19 Ctree.ctree * Ctree.pos' list * Ctree.pos' -> Ctree.ctree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
11.20 - val generate_inconsistent_rew : Selem.subs option * Celem.thm'' -> term -> Istate.T * Proof.context ->
11.21 + val generate_inconsistent_rew : Selem.subs option * Celem.thm'' -> term -> Istate_Def.T * Proof.context ->
11.22 Ctree.pos' -> Ctree.ctree -> Ctree.state (* for interface.sml *)
11.23 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.24 val tacis2str : taci list -> string
11.25 @@ -47,17 +47,17 @@
11.26 (* initialize istate for Detail_Set *)
11.27 fun init_istate (Tactic.Rewrite_Set rls) t =
11.28 (case assoc_rls rls of
11.29 - Rule.Rrls {scr = Rule.Rfuns {init_state = ii, ...}, ...} => Istate.RrlsState (ii t)
11.30 + Rule.Rrls {scr = Rule.Rfuns {init_state = ii, ...}, ...} => Istate_Def.RrlsState (ii t)
11.31 | Rule.Rls {scr = Rule.EmptyScr, ...} =>
11.32 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
11.33 "use prep_rls' for storing rule-sets !")
11.34 | Rule.Rls {scr = Rule.Prog s, ...} =>
11.35 - (Istate.Pstate (Istate.e_scrstate |> Istate.set_env_true [(hd (Program.formal_args s), t)]))
11.36 + (Istate_Def.Pstate (Istate_Def.e_scrstate |> Istate_Def.set_env_true [(hd (Program.formal_args s), t)]))
11.37 | Rule.Seq {scr = Rule.EmptyScr,...} =>
11.38 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
11.39 " Use prep_rls' for storing rule-sets !")
11.40 | Rule.Seq {scr = Rule.Prog s,...} =>
11.41 - (Istate.Pstate (Istate.e_scrstate |> Istate.set_env_true [(hd (Program.formal_args s), t)]))
11.42 + (Istate_Def.Pstate (Istate_Def.e_scrstate |> Istate_Def.set_env_true [(hd (Program.formal_args s), t)]))
11.43 | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")
11.44 | init_istate (Tactic.Rewrite_Set_Inst (subs, rls)) t =
11.45 let
11.46 @@ -70,12 +70,12 @@
11.47 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
11.48 "use prep_rls' for storing rule-sets !")
11.49 | Rule.Rls {scr = Rule.Prog s, ...} =>
11.50 - Istate.Pstate (Istate.e_scrstate |> Istate.set_env_true ((Program.formal_args s) ~~ [t, v]))
11.51 + Istate_Def.Pstate (Istate_Def.e_scrstate |> Istate_Def.set_env_true ((Program.formal_args s) ~~ [t, v]))
11.52 | Rule.Seq {scr = Rule.EmptyScr, ...} =>
11.53 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
11.54 "use prep_rls' for storing rule-sets !")
11.55 | Rule.Seq {scr = Rule.Prog s,...} =>
11.56 - Istate.Pstate (Istate.e_scrstate |> Istate.set_env_true ((Program.formal_args s) ~~ [t, v]))
11.57 + Istate_Def.Pstate (Istate_Def.e_scrstate |> Istate_Def.set_env_true ((Program.formal_args s) ~~ [t, v]))
11.58 | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls"
11.59 end
11.60 | init_istate tac _ = error ("init_istate: uncovered definition for " ^ Tactic.tac2str tac)
11.61 @@ -93,11 +93,11 @@
11.62 (Tactic.input * (* for comparison with input tac *)
11.63 Tactic.T * (* for ctree generation *)
11.64 (pos' * (* after applying tac_, for ctree generation *)
11.65 - (Istate.T * Proof.context))) (* after applying tac_, for ctree generation *)
11.66 -val e_taci = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (e_pos', (Istate.e_istate, ContextC.e_ctxt))): taci
11.67 + (Istate_Def.T * Proof.context))) (* after applying tac_, for ctree generation *)
11.68 +val e_taci = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (e_pos', (Istate_Def.e_istate, ContextC.e_ctxt))): taci
11.69 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
11.70 "( " ^ Tactic.tac2str tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
11.71 - Istate.istate2str istate ^ " ))"
11.72 + Istate_Def.istate2str istate ^ " ))"
11.73 fun tacis2str tacis = (strs2str o (map (Celem.linefeed o taci2str))) tacis
11.74
11.75 datatype pblmet = (*%^%*)
11.76 @@ -390,7 +390,7 @@
11.77 val p = case p_ of
11.78 Frm => p | Res => lev_on p
11.79 | _ => error ("generate_hard: call by " ^ pos'2str (p,p_))
11.80 - in generate1 thy m' (Istate.e_istate, ContextC.e_ctxt) (p,p_) pt end
11.81 + in generate1 thy m' (Istate_Def.e_istate, ContextC.e_ctxt) (p,p_) pt end
11.82
11.83 (* tacis are in reverse order from do_solve_step/specify_: last = fst to insert *)
11.84 fun generate ([]: taci list) ptp = ptp
11.85 @@ -423,7 +423,7 @@
11.86 | (NONE, _) => error "embed_deriv Frm: uncovered case get_obj"
11.87 val form = get_obj g_form pt p
11.88 (*val p = lev_on p; ---------------only difference to (..,Res) below*)
11.89 - val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate.Uistate, ctxt))) ::
11.90 + val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
11.91 (insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
11.92 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]
11.93 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
11.94 @@ -440,7 +440,7 @@
11.95 | (_, NONE) => error "embed_deriv Frm: uncovered case get_obj"
11.96 val (f, _) = get_obj g_result pt p
11.97 val p = lev_on p(*---------------only difference to (..,Frm) above*);
11.98 - val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Frm), (Istate.Uistate, ctxt))) ::
11.99 + val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Frm), (Istate_Def.Uistate, ctxt))) ::
11.100 (insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
11.101 (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))];
11.102 val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
12.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon Dec 16 15:56:20 2019 +0100
12.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Tue Dec 17 16:31:46 2019 +0100
12.3 @@ -191,7 +191,7 @@
12.4
12.5 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_'));
12.6 val (mI, m) = Solve.mk_tac'_ tac;
12.7 - val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
12.8 + val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
12.9 (*if*) member op = Solve.specsteps mI; (*else*)
12.10
12.11 (*val Updated (cs' as (_, _, (_, p'))) =*) loc_solve_ (mI,m) ptp;
13.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Dec 16 15:56:20 2019 +0100
13.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Dec 17 16:31:46 2019 +0100
13.3 @@ -110,7 +110,7 @@
13.4 (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*) locatetac tac (pt,p) (*of*);
13.5 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
13.6 val (mI, m) = Solve.mk_tac'_ tac;
13.7 - val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
13.8 + val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
13.9 (*if*) member op = Solve.specsteps mI; (*else*)
13.10
13.11 (** )val (***)xxxxx(***) ( *Updated (cs' as (_, _, (_, p'))) =( **) loc_solve_ (mI,m) ptp;
13.12 @@ -274,7 +274,7 @@
13.13 (** )val ("ok", (_, _, ptp as (pt, p))) =( **) locatetac (hd (sel_appl_atomic_tacs pt p)) (pt, p);
13.14 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (hd (sel_appl_atomic_tacs pt p), (pt, p));
13.15 val (mI, m) = Solve.mk_tac'_ tac;
13.16 - val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
13.17 + val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
13.18 (*if*) member op = Solve.specsteps mI (*else*);
13.19
13.20 loc_solve_ (mI, m) ptp;
14.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Mon Dec 16 15:56:20 2019 +0100
14.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Tue Dec 17 16:31:46 2019 +0100
14.3 @@ -226,7 +226,7 @@
14.4 ;
14.5 "~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
14.6 val (mI, m) = Solve.mk_tac'_ tac;
14.7 -val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
14.8 +val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
14.9 (*if*) member op = Solve.specsteps mI = true; (*then*)
14.10
14.11 (*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*)
15.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Mon Dec 16 15:56:20 2019 +0100
15.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Dec 17 16:31:46 2019 +0100
15.3 @@ -156,7 +156,7 @@
15.4 (*+*)case stac2tac_ pt (Proof_Context.theory_of ctxt) stac of (Rewrite_Set "norm_equation", _) => ()
15.5 (*+*)| _ => error "stac2tac_ changed"
15.6 "~~~~~ continue last scan_dn2";
15.7 -val Chead.Appl m' = Applicable.applicable_in p pt m;
15.8 +val Applicable.Appl m' = Applicable.applicable_in p pt m;
15.9 "~~~~~ fun result, args:"; val (m) = (m');
15.10 "~~~~~ fun rep_tac_, args:"; val (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) = (m);
15.11 val fT = type_of f;
16.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Mon Dec 16 15:56:20 2019 +0100
16.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Dec 17 16:31:46 2019 +0100
16.3 @@ -35,7 +35,7 @@
16.4 val ("ok", (_, _, ptp''''')) = (*case*) locatetac tac (pt,p) (*of*);
16.5 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
16.6 val (mI, m) = Solve.mk_tac'_ tac;
16.7 -val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
16.8 +val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
16.9 member op = Solve.specsteps mI (* = false*);
16.10
16.11 loc_solve_ (mI,m) ptp ; (* scan_dn1: call by ([3], Pbl)*)
17.1 --- a/test/Tools/isac/Test_Some.thy Mon Dec 16 15:56:20 2019 +0100
17.2 +++ b/test/Tools/isac/Test_Some.thy Tue Dec 17 16:31:46 2019 +0100
17.3 @@ -212,7 +212,7 @@
17.4 \<close> ML \<open>
17.5 val (mI, m) = Solve.mk_tac'_ tac;
17.6 \<close> ML \<open>
17.7 - val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
17.8 + val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
17.9 \<close> ML \<open>
17.10 (*if*) member op = Solve.specsteps mI (*else*);
17.11 \<close> ML \<open>