1.1 --- a/src/Tools/isac/CLEANUP Sat Oct 26 13:03:16 2019 +0200
1.2 +++ b/src/Tools/isac/CLEANUP Sun Oct 27 12:10:57 2019 +0100
1.3 @@ -47,14 +47,14 @@
1.4 rm *.thy~~~~~~~~
1.5 rm *.thy~~~~~~~~~
1.6 rm *.thy~~~~~~~~~~
1.7 - rm #*
1.8 - rm .\#*
1.9 - rm *.tar*
1.10 - rm *.orig
1.11 + rm #*
1.12 + rm .\#*
1.13 + rm *.tar*
1.14 + rm *.orig
1.15 rm *.orig~
1.16 cd ..
1.17 -cd Specify
1.18 - echo "cd Specify was successful"
1.19 +cd ProgLang
1.20 + echo "cd ProgLang was successful"
1.21 rm *.sml~
1.22 rm *.sml~
1.23 rm *.sml~~
1.24 @@ -77,14 +77,14 @@
1.25 rm *.thy~~~~~~~~
1.26 rm *.thy~~~~~~~~~
1.27 rm *.thy~~~~~~~~~~
1.28 - rm #*
1.29 - rm .\#*
1.30 - rm *.tar*
1.31 - rm *.orig
1.32 + rm #*
1.33 + rm .\#*
1.34 + rm *.tar*
1.35 + rm *.orig
1.36 rm *.orig~
1.37 cd ..
1.38 -cd ProgLang
1.39 - echo "cd ProgLang was successful"
1.40 +cd MathEngBasic
1.41 + echo "cd MathEngBasic was successful"
1.42 rm *.sml~
1.43 rm *.sml~
1.44 rm *.sml~~
1.45 @@ -107,14 +107,14 @@
1.46 rm *.thy~~~~~~~~
1.47 rm *.thy~~~~~~~~~
1.48 rm *.thy~~~~~~~~~~
1.49 - rm #*
1.50 - rm .\#*
1.51 - rm *.tar*
1.52 - rm *.orig
1.53 + rm #*
1.54 + rm .\#*
1.55 + rm *.tar*
1.56 + rm *.orig
1.57 rm *.orig~
1.58 cd ..
1.59 -cd Interpret
1.60 - echo "cd Interpret was successful"
1.61 +cd Specify
1.62 + echo "cd Specify was successful"
1.63 rm *.sml~
1.64 rm *.sml~
1.65 rm *.sml~~
1.66 @@ -137,14 +137,15 @@
1.67 rm *.thy~~~~~~~~
1.68 rm *.thy~~~~~~~~~
1.69 rm *.thy~~~~~~~~~~
1.70 - rm #*
1.71 - rm .\#*
1.72 - rm *.tar*
1.73 - rm *.orig
1.74 + rm #*
1.75 + rm *#~
1.76 + rm .\#*
1.77 + rm *.tar*
1.78 + rm *.orig
1.79 rm *.orig~
1.80 cd ..
1.81 -cd MathEngine
1.82 - echo "cd MathEngine was successful"
1.83 +cd Interpret
1.84 + echo "cd Interpret was successful"
1.85 rm *.sml~
1.86 rm *.sml~
1.87 rm *.sml~~
1.88 @@ -167,14 +168,14 @@
1.89 rm *.thy~~~~~~~~
1.90 rm *.thy~~~~~~~~~
1.91 rm *.thy~~~~~~~~~~
1.92 - rm #*
1.93 - rm .\#*
1.94 - rm *.tar*
1.95 - rm *.orig
1.96 + rm #*
1.97 + rm .\#*
1.98 + rm *.tar*
1.99 + rm *.orig
1.100 rm *.orig~
1.101 cd ..
1.102 -cd BridgeLibisabelle
1.103 - echo "cd BridgeLibisabelle was successful"
1.104 +cd MathEngine
1.105 + echo "cd MathEngine was successful"
1.106 rm *.sml~
1.107 rm *.sml~
1.108 rm *.sml~~
1.109 @@ -197,14 +198,15 @@
1.110 rm *.thy~~~~~~~~
1.111 rm *.thy~~~~~~~~~
1.112 rm *.thy~~~~~~~~~~
1.113 - rm #*
1.114 - rm .\#*
1.115 - rm *.tar*
1.116 - rm *.orig
1.117 + rm #*
1.118 + rm #*~
1.119 + rm .\#*
1.120 + rm *.tar*
1.121 + rm *.orig
1.122 rm *.orig~
1.123 cd ..
1.124 -cd Knowledge
1.125 - echo "cd Knowledge was successful"
1.126 +cd BridgeLibisabelle
1.127 + echo "cd BridgeLibisabelle was successful"
1.128 rm *.sml~
1.129 rm *.sml~
1.130 rm *.sml~~
1.131 @@ -227,9 +229,39 @@
1.132 rm *.thy~~~~~~~~
1.133 rm *.thy~~~~~~~~~
1.134 rm *.thy~~~~~~~~~~
1.135 - rm #*
1.136 - rm .\#*
1.137 - rm *.tar*
1.138 - rm *.orig
1.139 + rm #*
1.140 + rm .\#*
1.141 + rm *.tar*
1.142 + rm *.orig
1.143 + rm *.orig~
1.144 + cd ..
1.145 +cd Knowledge
1.146 + echo "cd Knowledge was successful"
1.147 + rm *.sml~
1.148 + rm *.sml~
1.149 + rm *.sml~~
1.150 + rm *.sml~~~
1.151 + rm *.sml~~~~
1.152 + rm *.sml~~~~~
1.153 + rm *.sml~~~~~~
1.154 + rm *.sml~~~~~~~
1.155 + rm *.sml~~~~~~~~
1.156 + rm *.sml~~~~~~~~~
1.157 + rm *.sml~~~~~~~~~~
1.158 + rm *.thy~
1.159 + rm *.thy~
1.160 + rm *.thy~~
1.161 + rm *.thy~~~
1.162 + rm *.thy~~~~
1.163 + rm *.thy~~~~~
1.164 + rm *.thy~~~~~~
1.165 + rm *.thy~~~~~~~
1.166 + rm *.thy~~~~~~~~
1.167 + rm *.thy~~~~~~~~~
1.168 + rm *.thy~~~~~~~~~~
1.169 + rm #*
1.170 + rm .\#*
1.171 + rm *.tar*
1.172 + rm *.orig
1.173 rm *.orig~
1.174 cd ..
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Oct 26 13:03:16 2019 +0200
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Sun Oct 27 12:10:57 2019 +0100
2.3 @@ -32,7 +32,7 @@
2.4 (*val determine_next_tactic :
2.5 Rule.program -> Ctree.state -> Istate.T -> Proof.context -> next_tactic_result *)
2.6 val determine_next_tactic : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.T * 'a ->
2.7 - Tactic.T * (Istate.T * 'a) * (term * Istate.safe)
2.8 + Tactic.T * (Istate.T * 'a) * (term * Telem.safe)
2.9
2.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.11 datatype assoc =
2.12 @@ -42,11 +42,10 @@
2.13 val assoc2str : assoc -> string
2.14 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.15 datatype appy = Appy of Tactic.T * Istate.pstate | Napp of Env.T | Skip of term * Env.T
2.16 - datatype appy_ = Napp_ | Skip_
2.17 val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
2.18 - val nstep_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> appy_ -> appy
2.19 + val nstep_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> appy
2.20 val appy: Rule.theory' * Rule.rls -> Ctree.state -> Istate.pstate -> term -> appy
2.21 - val nxt_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> appy_ -> term -> appy
2.22 + val nxt_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> term -> appy
2.23 datatype asap = Aundef | AssOnly | AssGen;
2.24 val go : Celem.loc_ -> term -> term
2.25 val go_up: Celem.loc_ -> term -> term
2.26 @@ -117,13 +116,6 @@
2.27 term * (* ???*)
2.28 Env.T (* TODO: a stack of env for nested let? *);
2.29
2.30 -datatype appy_ = (* as argument in nxt_up, nstep_up, from appy *)
2.31 -(*Appy is only (final) returnvalue, not argument during search *)
2.32 - Napp_ (* ev. detects 'script is not appropriate for this example' *)
2.33 -| Skip_; (* detects 'script successfully finished'
2.34 - also used as init-value for resuming; this works,
2.35 - because 'nxt_up Or e1' treats as Appy *)
2.36 -
2.37 fun
2.38 (*1* )
2.39 appy thy ptp (ist) E l (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
2.40 @@ -263,11 +255,11 @@
2.41 in
2.42 case m of (*TODO?: make applicable_in..Subproblem analogous to other tacs ?refine problem?*)
2.43 Tactic.Subproblem _ => Appy (m', (
2.44 - get_env ist, get_path ist, a', Lucin.tac_2res m', Istate.Sundef, false))
2.45 + get_env ist, get_path ist, a', Lucin.tac_2res m', Istate.AppUndef_, false))
2.46 | _ =>
2.47 (case Applicable.applicable_in p pt m of
2.48 Chead.Appl m' => (Appy (m', (
2.49 - get_env ist, get_path ist, a', Lucin.tac_2res m', Istate.Sundef, false)))
2.50 + get_env ist, get_path ist, a', Lucin.tac_2res m', Istate.AppUndef_, false)))
2.51 | _ => Napp (get_env ist))
2.52 end
2.53 (*end*)
2.54 @@ -489,8 +481,8 @@
2.55
2.56 fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.Pstate (E, l, a, v, _, _)) =
2.57 if l = []
2.58 - then appy thy ptp (E, [R], NONE, v, Sundef, false) (Program.body_of prog)
2.59 - else nstep_up thy ptp sc (E, l, a, v, Sundef, false) Skip_
2.60 + then appy thy ptp (E, [R], NONE, v, AppUndef_, false) (Program.body_of prog)
2.61 + else nstep_up thy ptp sc (E, l, a, v, AppUndef_, false) Skip_
2.62 | execute_progr_1 _ _ _ _ = raise ERROR "execute_progr_1: uncovered pattern";
2.63
2.64 (* decide for the next applicable stac in the program;
2.65 @@ -511,23 +503,25 @@
2.66 | _ => error "determine_next_tactic: uncovered case next_rule")
2.67 -----*)
2.68 fun determine_next_tactic thy (ptp as (pt, (p, _))) sc (Istate.Pstate (E,l,a,v,s,_), ctxt) =
2.69 - (case execute_progr_1 thy ptp sc (Istate.Pstate (E,l,a,v,s,false)) of
2.70 - Skip (v, _) => (*finished*)
2.71 - (case par_pbl_det pt p of
2.72 - (true, p', _) =>
2.73 - let
2.74 - val (_,pblID,_) = get_obj g_spec pt p';
2.75 - in (Tactic.Check_Postcond' (pblID, (v, [(*assigned in next step*)])),
2.76 - (Istate.e_istate, ctxt), (v,s))
2.77 - end
2.78 - | _ => (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ctxt), (v,s)))
2.79 - | Napp _ => (Tactic.Empty_Tac_, (Istate.e_istate, ctxt), (Rule.e_term, Istate.Sundef)) (*helpless*)
2.80 - | Appy (m', scrst as (_,_,_,v,_,_)) =>
2.81 - (m', (Istate.Pstate scrst, ctxt), (v, Istate.Sundef))) (*next stac*)
2.82 + (case execute_progr_1 thy ptp sc (Istate.Pstate (E,l,a,v,s,false)) of
2.83 + Skip (v, _) => (* program finished *)
2.84 + (case par_pbl_det pt p of
2.85 + (true, p', _) =>
2.86 + let
2.87 + val (_,pblID,_) = get_obj g_spec pt p';
2.88 + in
2.89 + (Tactic.Check_Postcond' (pblID, (v, [(*assigned in next step*)])),
2.90 + (Istate.e_istate, ctxt), (v, Telem.Safe))
2.91 + end
2.92 + | _ =>
2.93 + (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ctxt), (v, Telem.Safe)))
2.94 + | Napp _ =>
2.95 + (Tactic.Empty_Tac_, (Istate.e_istate, ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *)
2.96 + | Appy (m', scrst as (_,_,_,v,_,_)) =>
2.97 + (m', (Istate.Pstate scrst, ctxt), (v, Telem.Safe))) (* found next tac *)
2.98 | determine_next_tactic _ _ _ (is, _) =
2.99 error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is));
2.100
2.101 -
2.102 (**** locate an input tactic within a program ****)
2.103
2.104 datatype input_tactic_result =
2.105 @@ -991,16 +985,18 @@
2.106 val thy' = get_obj g_domID pt pp;
2.107 val thy = Celem.assoc_thy thy';
2.108 val (_, _, (scval, scsaf)) = determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;
2.109 + (* Telem.safe should go on to Check_Postcond' vvvvv *)
2.110 in
2.111 if pp = []
2.112 then
2.113 let
2.114 - val is = Istate.Pstate (E, l, a, scval, scsaf, b)
2.115 - val tac_ = Tactic.Check_Postcond'(pI,(scval, asm))
2.116 + val is = Istate.Pstate (E, l, a, scval, Istate.Skip_, b)
2.117 + val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
2.118 + (*extend Tactic.Check_Postcond' (pI, (scval, asm), scsaf) ^^^^^ *)
2.119 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;
2.120 in ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p, p_))) end
2.121 else
2.122 - let (*resume script of parpbl, transfer value of subpbl-script*)
2.123 + let (*resume script of parent PblObj, transfer value of subpbl-script*)
2.124 val ppp = par_pblobj pt (lev_up p);
2.125 val thy' = get_obj g_domID pt ppp;
2.126 val thy = Celem.assoc_thy thy';
2.127 @@ -1009,7 +1005,7 @@
2.128 | _ => error "begin_end_prog Check_Postcond' script of parpbl: uncovered case get_loc"
2.129 val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'
2.130 val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
2.131 - val is = Istate.Pstate (E,l,a,scval,scsaf,b)
2.132 + val is = Istate.Pstate (E,l,a,scval,Istate.Skip_,b)
2.133 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
2.134 in ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p, p_))) end
2.135 end
3.1 --- a/src/Tools/isac/Interpret/script.sml Sat Oct 26 13:03:16 2019 +0200
3.2 +++ b/src/Tools/isac/Interpret/script.sml Sun Oct 27 12:10:57 2019 +0100
3.3 @@ -551,7 +551,7 @@
3.4 val {pre, prls, ...} = Specify.get_met metID;
3.5 val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
3.6 val ctxt = ctxt |> ContextC.insert_assumptions pres;
3.7 - in (Istate.Pstate (env, [], NONE, Rule.e_term, Istate.Safe, true), ctxt, scr) end;
3.8 + in (Istate.Pstate (env, [], NONE, Rule.e_term, Istate.AppUndef_, true), ctxt, scr) end;
3.9 end (*local*)
3.10
3.11 fun get_simplifier (pt, (p, _)) =
4.1 --- a/src/Tools/isac/MathEngBasic/calc-tree-elem.sml Sat Oct 26 13:03:16 2019 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/calc-tree-elem.sml Sun Oct 27 12:10:57 2019 +0100
4.3 @@ -5,6 +5,9 @@
4.4 signature CALC_TREE_ELEMENT =
4.5 sig
4.6
4.7 + datatype safe = Sundef | Safe | Unsafe | Helpless_;
4.8 + val safe2str: safe -> string
4.9 +
4.10 end
4.11
4.12 (**)
4.13 @@ -12,4 +15,10 @@
4.14 struct
4.15 (**)
4.16
4.17 +datatype safe = Sundef | Safe | Unsafe | Helpless_;
4.18 +fun safe2str Sundef = "Sundef"
4.19 + | safe2str Safe = "Safe"
4.20 + | safe2str Unsafe = "Unsafe"
4.21 + | safe2str Helpless = "Helpless_";
4.22 +
4.23 (**)end(**)
5.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Sat Oct 26 13:03:16 2019 +0200
5.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Sun Oct 27 12:10:57 2019 +0100
5.3 @@ -226,7 +226,7 @@
5.4 env * (* with results of (ready) tacs *)
5.5 term * (* itr_arg of tactic, for upd. env at Repeat, Try *)
5.6 term * (* result value of the tac *)
5.7 - Istate.safe))
5.8 + Telem.safe))
5.9 list;
5.10
5.11 fun ets2s (l,(m,eno,env,iar,res,s)) =
5.12 @@ -235,7 +235,7 @@
5.13 ",\n env= " ^ Env.subst2str env ^
5.14 ",\n iar= " ^ Rule.term2str iar ^
5.15 ",\n res= " ^ Rule.term2str res ^
5.16 - ",\n " ^ Istate.safe2str s ^ "))";
5.17 + ",\n " ^ Telem.safe2str s ^ "))";
5.18 fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets; (* for tests only *)
5.19
5.20 type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)
6.1 --- a/src/Tools/isac/MathEngBasic/istate.sml Sat Oct 26 13:03:16 2019 +0200
6.2 +++ b/src/Tools/isac/MathEngBasic/istate.sml Sun Oct 27 12:10:57 2019 +0100
6.3 @@ -4,12 +4,11 @@
6.4 *)
6.5 signature INTERPRETER_STATE =
6.6 sig
6.7 - datatype safe = Sundef | Safe | Unsafe | Helpless;
6.8 - val safe2str: safe -> string
6.9
6.10 + datatype appy_ = AppUndef_ | Napp_ | Skip_
6.11 type pstate
6.12 val e_scrstate: pstate
6.13 - val scrstate2str: Rule.subst * Celem.loc_ * term option * term * safe * bool -> string
6.14 + val scrstate2str: Rule.subst * Celem.loc_ * term option * term * appy_ * bool -> string
6.15
6.16 datatype T = RrlsState of Rule.rrlsstate | Pstate of pstate | Uistate
6.17 val istate2str: T -> string
6.18 @@ -50,11 +49,16 @@
6.19 struct
6.20 (**)
6.21
6.22 -datatype safe = Sundef | Safe | Unsafe | Helpless;
6.23 -fun safe2str Sundef = "Sundef"
6.24 - | safe2str Safe = "Safe"
6.25 - | safe2str Unsafe = "Unsafe"
6.26 - | safe2str Helpless = "Helpless";
6.27 +datatype appy_ = (* as argument in nxt_up, nstep_up, from appy *)
6.28 +(*Appy is only (final) returnvalue, not argument during search *)
6.29 + AppUndef_
6.30 +| Napp_ (* ev. detects 'script is not appropriate for this example' *)
6.31 +| Skip_; (* detects 'script successfully finished'
6.32 + also used as init-value for resuming; this works,
6.33 + because 'nxt_up Or e1' treats as Appy *)
6.34 +fun appy_2str AppUndef_ = "AppUndef_"
6.35 + | appy_2str Napp_ = "Napp_"
6.36 + | appy_2str Skip_ = "Skip_"
6.37
6.38 type pstate = (* state for script interpreter *)
6.39 Env.T(*stack*) (* used to instantiate tac for checking associate
6.40 @@ -63,30 +67,30 @@
6.41 * term option (*id FORMal ARGument of curried functions *)
6.42 * term (*vl ACTual ARGument (value) for execution of Tactic.T
6.43 updated also after a derivation by 'new_val' *)
6.44 - * safe (* estimation of how result will be obtained *)
6.45 + * appy_ (* estimation of how result will be obtained *)
6.46 * bool; (* true = strongly .., false = weakly associated:
6.47 only used during ass_dn/up *)
6.48 val e_scrstate =
6.49 - ([]: Env.T, []:Celem.loc_, SOME Rule.e_term, Rule.e_term, Sundef, false) : pstate
6.50 + ([]: Env.T, []:Celem.loc_, SOME Rule.e_term, Rule.e_term, AppUndef_, false) : pstate
6.51 fun topt2str NONE = "NONE"
6.52 | topt2str (SOME t) = "SOME" ^ Rule.term2str t;
6.53 fun scrstate2str (env, loc_, topt, t, safe, bool) = (* for tests only *)
6.54 "(" ^ Env.env2str env ^ ", " ^ Celem.loc_2str loc_ ^ ", " ^ topt2str topt ^ ", \n" ^
6.55 - Rule.term2str t ^ ", " ^ safe2str safe ^ ", " ^ bool2str bool ^ ")";
6.56 + Rule.term2str t ^ ", " ^ appy_2str safe ^ ", " ^ bool2str bool ^ ")";
6.57
6.58 (* for handling type T see fun from_pblobj_or_detail', +? *)
6.59 datatype T = (*interpreter state*)
6.60 Uistate (*undefined in modspec, in '_deriv'ation*)
6.61 | Pstate of pstate (*for script interpreter*)
6.62 | RrlsState of Rule.rrlsstate; (*for reverse rewriting*)
6.63 -val e_istate = (Pstate ([], [], NONE, Rule.e_term, Sundef, false));
6.64 +val e_istate = (Pstate ([], [], NONE, Rule.e_term, AppUndef_, false));
6.65
6.66 fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ",(" ^ Rule.term2str t ^", " ^ Rule.terms2str a ^ "))";
6.67 fun istate2str Uistate = "Uistate"
6.68 | istate2str (Pstate (e, l, to, t, s, b)) =
6.69 "Pstate ("^ Env.subst2str e ^ ",\n " ^
6.70 Celem.loc_2str l ^ ", " ^ Rule.termopt2str to ^ ",\n " ^
6.71 - Rule.term2str t ^ ", " ^ safe2str s ^ ", " ^ bool2str b ^ ")"
6.72 + Rule.term2str t ^ ", " ^ appy_2str s ^ ", " ^ bool2str b ^ ")"
6.73 | istate2str (RrlsState (t, t1, rss, rtas)) =
6.74 "RrlsState (" ^ Rule.term2str t ^ ", " ^ Rule.term2str t1 ^ ", " ^
6.75 (strs2str o (map (strs2str o (map Rule.rule2str)))) rss ^ ", " ^
7.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Sat Oct 26 13:03:16 2019 +0200
7.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Sun Oct 27 12:10:57 2019 +0100
7.3 @@ -8,7 +8,7 @@
7.4 sig
7.5 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
7.6 val me : Solve.tac'_ -> Ctree.pos' -> NEW ->
7.7 - Ctree.ctree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Istate.safe * Ctree.ctree
7.8 + Ctree.ctree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Telem.safe * Ctree.ctree
7.9 val autocalc : Ctree.pos' list -> Ctree.pos' -> (Ctree.state) * Generate.taci list ->
7.10 Solve.auto -> string * Ctree.pos' list * (Ctree.state)
7.11 val locatetac :
7.12 @@ -26,7 +26,7 @@
7.13 val set_theory : Rule.thyID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
7.14 val tryrefine : Celem.pblID -> Ctree.ctree -> Ctree.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
7.15 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.16 - val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Tactic.input) * Istate.safe * Ctree.ctree
7.17 + val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Tactic.input) * Telem.safe * Ctree.ctree
7.18 val f2str : Generate.mout -> Rule.cterm'
7.19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.20 type nxt_
7.21 @@ -385,7 +385,7 @@
7.22 val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)
7.23 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
7.24 val f = TESTg_form (pt,p)
7.25 - in (p, []:NEW, f, (Tactic.tac2IDstr tac, tac), Istate.Sundef, pt) end
7.26 + in (p, []:NEW, f, (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt) end
7.27 | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"
7.28
7.29 (*for tests > 15.8.03 after separation setnexttactic / nextTac:
7.30 @@ -423,7 +423,7 @@
7.31 | _ => if p = ([], Ctree.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
7.32 in
7.33 (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
7.34 - (Tactic.tac2IDstr tac, tac), Istate.Sundef, pt)
7.35 + (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt)
7.36 end
7.37
7.38 (* for quick test-print-out, until 'type inout' is removed *)
8.1 --- a/src/Tools/isac/MathEngine/solve.sml Sat Oct 26 13:03:16 2019 +0200
8.2 +++ b/src/Tools/isac/MathEngine/solve.sml Sun Oct 27 12:10:57 2019 +0100
8.3 @@ -136,7 +136,8 @@
8.4 end
8.5 | NONE => (*execute first tac in the Program, compare solve m*)
8.6 let
8.7 - val (m', (is', ctxt'), _) = LucinNEW.determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
8.8 + val (m', (is', ctxt'), _) =
8.9 + LucinNEW.determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
8.10 in
8.11 case LucinNEW.locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' of
8.12 LucinNEW.Safe_Step (istate, ctxt, tac) =>
8.13 @@ -153,7 +154,9 @@
8.14 (*OLD*) [(*ctree NOT cut*)], cstate))
8.15 ( *OLD*)
8.16 | _ => (* NotLocatable *)
8.17 - let val (p, ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (p, Frm) pt;
8.18 + let
8.19 + val (p, ps, _, pt) =
8.20 + Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (p, Frm) pt;
8.21 in
8.22 ("not-found-in-script",([(Lucin.tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt, p)))
8.23 end
8.24 @@ -187,7 +190,7 @@
8.25 if pp = []
8.26 then
8.27 let
8.28 - val is = Istate.Pstate (E,l,a,scval,scsaf,b)
8.29 + val is = Istate.Pstate (E,l,a,scval,Istate.Skip_,b)
8.30 val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
8.31 val (pos, ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;
8.32 in ("ok", ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, pos))) end
8.33 @@ -201,9 +204,9 @@
8.34 | _ => error "solve Check_Postcond resume script of parpbl: uncovered case get_loc"
8.35 val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'
8.36 val ((p, p_), ps, _, pt) = Generate.generate1 thy (Tactic.Check_Postcond' (pI, (scval, asm)))
8.37 - (Istate.Pstate (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
8.38 + (Istate.Pstate (E,l,a,scval,Istate.Skip_,b), ctxt'') (pp,Res) pt;
8.39 in ("ok", ([(Tactic.Check_Postcond pI, Tactic.Check_Postcond'(pI, (scval, asm)),
8.40 - ((pp, Res), (Istate.Pstate (E, l, a, scval, scsaf, b), ctxt'')))], ps, (pt, (p, p_)))) end
8.41 + ((pp, Res), (Istate.Pstate (E, l, a, scval, Istate.Skip_, b), ctxt'')))], ps, (pt, (p, p_)))) end
8.42 end
8.43 | solve (_, Tactic.End_Proof'') (pt, (p, p_)) =
8.44 ("end-proof", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (([], Res), (Istate.Uistate, ContextC.e_ctxt)))], [], (pt, (p, p_))))
9.1 --- a/src/Tools/isac/Specify/calchead.sml Sat Oct 26 13:03:16 2019 +0200
9.2 +++ b/src/Tools/isac/Specify/calchead.sml Sun Oct 27 12:10:57 2019 +0100
9.3 @@ -71,7 +71,7 @@
9.4 datatype appl = Appl of Tactic.T | Notappl of string
9.5 val nxt_specify_init_calc : Selem.fmz -> calcstate
9.6 val specify : Tactic.T -> Ctree.pos' -> Ctree.cid -> Ctree.ctree ->
9.7 - Ctree.pos' * (Ctree.pos' * Istate.T) * Generate.mout * Tactic.input * Istate.safe * Ctree.ctree
9.8 + Ctree.pos' * (Ctree.pos' * Istate.T) * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
9.9 val nxt_specif : Tactic.input -> Ctree.state -> calcstate'
9.10 val nxt_spec : Ctree.pos_ -> bool -> Model.ori list -> Celem.spec -> Model.itm list * Model.itm list ->
9.11 (string * (term * 'a)) list * (string * (term * 'b)) list -> Celem.spec -> Ctree.pos_ * Tactic.input
9.12 @@ -709,7 +709,7 @@
9.13 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
9.14 ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
9.15 in ((p, p_), ((p, p_), Istate.Uistate),
9.16 - Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Istate.Safe, pt')
9.17 + Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Telem.Safe, pt')
9.18 end
9.19 | Err msg =>
9.20 let
9.21 @@ -718,7 +718,7 @@
9.22 val (p_, nxt) =
9.23 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
9.24 ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
9.25 - in ((p,p_), ((p,p_),Istate.Uistate), Generate.Error' msg, nxt, Istate.Safe, pt) end
9.26 + in ((p,p_), ((p,p_),Istate.Uistate), Generate.Error' msg, nxt, Telem.Safe, pt) end
9.27 end
9.28 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
9.29 let
9.30 @@ -750,7 +750,7 @@
9.31 val ppc = if p_= Pbl then pbl' else met
9.32 in
9.33 ((p, p_), ((p, p_), Istate.Uistate),
9.34 - Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Istate.Safe, pt')
9.35 + Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Telem.Safe, pt')
9.36 end
9.37 | Err msg =>
9.38 let
9.39 @@ -759,7 +759,7 @@
9.40 val (p_, nxt) =
9.41 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
9.42 (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
9.43 - in ((p, p_), ((p, p_), Istate.Uistate), Generate.Error' msg, nxt, Istate.Safe,pt) end
9.44 + in ((p, p_), ((p, p_), Istate.Uistate), Generate.Error' msg, nxt, Telem.Safe,pt) end
9.45 end
9.46
9.47 fun specify (Tactic.Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
9.48 @@ -778,11 +778,11 @@
9.49 ["no_met"] =>
9.50 (([], Pbl), (([], Pbl), Istate.Uistate),
9.51 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),
9.52 - Tactic.Refine_Tacitly pI', Istate.Safe, pt)
9.53 + Tactic.Refine_Tacitly pI', Telem.Safe, pt)
9.54 | _ =>
9.55 (([], Pbl), (([], Pbl), Istate.Uistate),
9.56 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),
9.57 - Tactic.Model_Problem, Istate.Safe, pt)
9.58 + Tactic.Model_Problem, Telem.Safe, pt)
9.59 end
9.60 (* ONLY for STARTING modeling phase *)
9.61 | specify (Tactic.Model_Problem' (_, pbl, met)) (pos as (p, p_)) _ pt =
9.62 @@ -803,7 +803,7 @@
9.63 in
9.64 ((p, Pbl), ((p, p_), Istate.Uistate),
9.65 Generate.PpcKF (Generate.Problem pI', Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),
9.66 - nxt, Istate.Safe, pt)
9.67 + nxt, Telem.Safe, pt)
9.68 end
9.69 (* called only if no_met is specified *)
9.70 | specify (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pos as (p, _)) _ pt =
9.71 @@ -818,7 +818,7 @@
9.72 val (pbl, pre, _) = ([], [], false)
9.73 in ((p, Pbl), (pos, Istate.Uistate),
9.74 Generate.PpcKF (Generate.Problem pIre, Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),
9.75 - Tactic.Model_Problem, Istate.Safe, pt)
9.76 + Tactic.Model_Problem, Telem.Safe, pt)
9.77 end
9.78 | specify (Tactic.Refine_Problem' rfd) pos _ pt =
9.79 let
9.80 @@ -826,7 +826,7 @@
9.81 val (pos, _, _, pt) =
9.82 Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Refine_Problem' rfd) (Istate.Uistate, ctxt) pos pt
9.83 in
9.84 - (pos(*p,Pbl*), (pos(*p,Pbl*), Istate.Uistate), Generate.RefinedKF rfd, Tactic.Model_Problem, Istate.Safe, pt)
9.85 + (pos(*p,Pbl*), (pos(*p,Pbl*), Istate.Uistate), Generate.RefinedKF rfd, Tactic.Model_Problem, Telem.Safe, pt)
9.86 end
9.87 (*WN110515 initialise ctxt again from itms and add preconds*)
9.88 | specify (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
9.89 @@ -847,7 +847,7 @@
9.90 in
9.91 ((p,Pbl), (pos,Istate.Uistate),
9.92 Generate.PpcKF (Generate.Problem pI, Specify.itms2itemppc dI'' itms pre),
9.93 - nxt, Istate.Safe, pt)
9.94 + nxt, Telem.Safe, pt)
9.95 end
9.96 (*WN110515 initialise ctxt again from itms and add preconds*)
9.97 | specify (Tactic.Specify_Method' (mID, _, _)) (pos as (p, _)) _ pt =
9.98 @@ -884,7 +884,7 @@
9.99 in
9.100 (pos, (pos,Istate.Uistate),
9.101 Generate.PpcKF (Generate.Method mID, Specify.itms2itemppc (Celem.assoc_thy dI'') itms pre'),
9.102 - nxt, Istate.Safe, pt)
9.103 + nxt, Telem.Safe, pt)
9.104 end
9.105 | specify (Tactic.Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
9.106 | specify (Tactic.Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
9.107 @@ -913,7 +913,7 @@
9.108 in
9.109 ((p, p_), (pos, Istate.Uistate),
9.110 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
9.111 - nxt, Istate.Safe, pt)
9.112 + nxt, Telem.Safe, pt)
9.113 end
9.114 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
9.115 let
9.116 @@ -922,7 +922,7 @@
9.117 in
9.118 ((p,p_), (pos,Istate.Uistate),
9.119 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
9.120 - nxt, Istate.Safe, pt)
9.121 + nxt, Telem.Safe, pt)
9.122 end
9.123 end
9.124 | specify m' _ _ _ = error ("specify: not impl. for " ^ Tactic.tac_2str m')
10.1 --- a/src/Tools/isac/Specify/generate.sml Sat Oct 26 13:03:16 2019 +0200
10.2 +++ b/src/Tools/isac/Specify/generate.sml Sun Oct 27 12:10:57 2019 +0100
10.3 @@ -51,13 +51,13 @@
10.4 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
10.5 "use prep_rls' for storing rule-sets !")
10.6 | Rule.Rls {scr = Rule.Prog s, ...} =>
10.7 - (Istate.Pstate ([(hd (Program.formal_args s), t)], [], NONE, Rule.e_term, Istate.Sundef, true))
10.8 + (Istate.Pstate ([(hd (Program.formal_args s), t)], [], NONE, Rule.e_term, Istate.AppUndef_, true))
10.9 | Rule.Seq {scr = Rule.EmptyScr,...} =>
10.10 error ("interSteps>..>init_istate: \"" ^ rls ^ "\" has EmptyScr." ^
10.11 " Use prep_rls' for storing rule-sets !")
10.12 | Rule.Seq {scr = Rule.Prog s,...} =>
10.13 (writeln ("### init_istate: rls = \"" ^ "rls" ^ "\", Prog = \"" ^ Rule.term2str s ^ "\"");
10.14 - (Istate.Pstate ([(hd (Program.formal_args s), t)], [], NONE, Rule.e_term, Istate.Sundef, true))
10.15 + (Istate.Pstate ([(hd (Program.formal_args s), t)], [], NONE, Rule.e_term, Istate.AppUndef_, true))
10.16 )
10.17 | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")
10.18 | init_istate (Tactic.Rewrite_Set_Inst (subs, rls)) t =
10.19 @@ -72,14 +72,14 @@
10.20 "use prep_rls' for storing rule-sets !")
10.21 | Rule.Rls {scr = Rule.Prog s, ...} =>
10.22 let val env = (Program.formal_args s) ~~ [t, v]
10.23 - in (Istate.Pstate (env, [], NONE, Rule.e_term, Istate.Sundef,true))
10.24 + in (Istate.Pstate (env, [], NONE, Rule.e_term, Istate.AppUndef_, true))
10.25 end
10.26 | Rule.Seq {scr = Rule.EmptyScr, ...} =>
10.27 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." ^
10.28 "use prep_rls' for storing rule-sets !")
10.29 | Rule.Seq {scr = Rule.Prog s,...} =>
10.30 let val env = (Program.formal_args s) ~~ [t, v]
10.31 - in (Istate.Pstate (env,[], NONE, Rule.e_term, Istate.Sundef,true))
10.32 + in (Istate.Pstate (env,[], NONE, Rule.e_term, Istate.AppUndef_,true))
10.33 end
10.34 | _ => error "init_istate Rewrite_Set_Inst: uncovered case assoc_rls"
10.35 end
11.1 --- a/src/Tools/isac/TODO.thy Sat Oct 26 13:03:16 2019 +0200
11.2 +++ b/src/Tools/isac/TODO.thy Sun Oct 27 12:10:57 2019 +0100
11.3 @@ -254,7 +254,9 @@
11.4 val pblterm: Rule.domID -> Celem.pblID -> term vvv vvv\\
11.5 val subpbl: string -> string list -> term unify with ^^^
11.6 \item xxx
11.7 - \item xxx
11.8 + \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
11.9 + Note: replacement of Istate.safe by Istate.appy_ didn't care about Telem.safe.
11.10 + If Telem.safe is kept, consider merge with CTbasic.ostate
11.11 \item xxx
11.12 \item xxx
11.13 \end{itemize}
12.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sat Oct 26 13:03:16 2019 +0200
12.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sun Oct 27 12:10:57 2019 +0100
12.3 @@ -161,7 +161,7 @@
12.4 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; (*<---------------------- orig. test code*)
12.5 (*+isa=REP*) if p = ([1], Frm) andalso term2str (get_obj g_form pt [1]) = "1 + -1 * 2 + x = 0"
12.6 andalso istate2str (get_istate pt p)
12.7 - = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [], NONE,\n ??.empty, Safe, true)"
12.8 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [], NONE,\n ??.empty, AppUndef_, true)"
12.9 then () else error "refFormula = 1 + -1 * 2 + x = 0 changed";
12.10 (*-------------------------------------------------------------------------*)
12.11
12.12 @@ -181,11 +181,11 @@
12.13 (*//******************* locatetac returns tac_ + istate + cstate *****************************\\*)
12.14 locatetac : Tactic.input -> state -> string * (taci list * pos' list * state);
12.15 if istate2str istate
12.16 - = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"
12.17 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
12.18 then () else error "from locatetac return --- changed 1";
12.19
12.20 if istate2str (get_istate (fst cstate) (snd cstate))
12.21 - = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"
12.22 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
12.23 then () else error "from locatetac return --- changed 2";
12.24 (*\\******************* locatetac returns tac_ + istate + cstate *****************************//*)
12.25
12.26 @@ -207,7 +207,7 @@
12.27 (*+*)Safe_Step: Istate.T * Proof.context * T -> input_tactic_result;
12.28 (********************* locate_input_tactic returns cstate * istate * Proof.context *************)
12.29 (*+*)if istate2str istate
12.30 -(*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"(**)
12.31 +(*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"(**)
12.32 then case m of Rewrite_Set_Inst' _ => ()
12.33 else error "from locate_input_tactic return --- changed";
12.34
12.35 @@ -232,7 +232,7 @@
12.36 (*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
12.37 Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
12.38 (*+*)if pos' = ([1], Res) andalso istate2str istate
12.39 - = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"
12.40 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
12.41 then () else error "init. step 1 + -1 * 2 + x = 0 changed";
12.42
12.43 val pIopt = get_pblID (pt,ip);
12.44 @@ -244,7 +244,7 @@
12.45 val ("ok", [], ptp as (pt, p)) = xxxx;
12.46
12.47 if istate2str (get_istate pt p) (* <> <> <> <> ^^^^^^^^^^^^^*)
12.48 -(*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), Safe, true)"
12.49 +(*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"],\n [R,L,R,L,R,L,R], (SOME e_e),\n x = 0 + -1 * (1 + -1 * 2), AppUndef_, true)"
12.50 then () else error "REP autoCalculate on (e_e, 1 + -1 * 2 + x = 0) changed"
12.51
12.52 "~~~~~ from TOPLEVEL to states return:"; upd_calc cI (ptp, []); upd_ipos cI 1 p;
13.1 --- a/test/Tools/isac/CLEANUP Sat Oct 26 13:03:16 2019 +0200
13.2 +++ b/test/Tools/isac/CLEANUP Sun Oct 27 12:10:57 2019 +0100
13.3 @@ -80,7 +80,25 @@
13.4 cd ..
13.5 cd ..
13.6 cd ..
13.7 +cd Minisubpbl
13.8 + rm #*
13.9 + rm .\#*
13.10 + rm *.tar*
13.11 + rm *.orig
13.12 + rm *.orig~
13.13 + rm *.orig~
13.14 + cd ..
13.15 +cd OLDTESTS
13.16 + rm #*
13.17 + rm .\#*
13.18 + rm *.tar*
13.19 + rm *.orig
13.20 + rm *.orig~
13.21 + rm *.orig~
13.22 + rm *.orig*
13.23 + cd ..
13.24 cd CalcElements
13.25 + echo "cd CalcElements was successful"
13.26 rm *.sml~
13.27 rm *.sml~
13.28 rm *.sml~~
13.29 @@ -103,26 +121,14 @@
13.30 rm *.thy~~~~~~~~
13.31 rm *.thy~~~~~~~~~
13.32 rm *.thy~~~~~~~~~~
13.33 - rm #*
13.34 - rm .\#*
13.35 - rm *.tar*
13.36 - rm *.orig
13.37 - cd ..
13.38 -cd Minisubpbl
13.39 - rm *~
13.40 rm #*
13.41 rm .\#*
13.42 rm *.tar*
13.43 - rm *.orig*
13.44 + rm *.orig
13.45 + rm *.orig~
13.46 cd ..
13.47 -cd OLDTESTS
13.48 - rm *~
13.49 - rm #*
13.50 - rm .\#*
13.51 - rm *.tar*
13.52 - rm *.orig*
13.53 - cd ..
13.54 -cd Specify
13.55 +cd ProgLang
13.56 + echo "cd ProgLang was successful"
13.57 rm *.sml~
13.58 rm *.sml~
13.59 rm *.sml~~
13.60 @@ -145,12 +151,15 @@
13.61 rm *.thy~~~~~~~~
13.62 rm *.thy~~~~~~~~~
13.63 rm *.thy~~~~~~~~~~
13.64 - rm #*
13.65 - rm .\#*
13.66 - rm *.tar*
13.67 - rm *.orig
13.68 + rm #*
13.69 + rm .\#*
13.70 + rm *.tar*
13.71 + rm *.orig
13.72 + rm *.orig~
13.73 + rm *.orig~
13.74 cd ..
13.75 -cd ProgLang
13.76 +cd MathEngBasic
13.77 + echo "cd MathEngBasic was successful"
13.78 rm *.sml~
13.79 rm *.sml~
13.80 rm *.sml~~
13.81 @@ -173,12 +182,15 @@
13.82 rm *.thy~~~~~~~~
13.83 rm *.thy~~~~~~~~~
13.84 rm *.thy~~~~~~~~~~
13.85 - rm #*
13.86 - rm .\#*
13.87 - rm *.tar*
13.88 - rm *.orig
13.89 + rm #*
13.90 + rm .\#*
13.91 + rm *.tar*
13.92 + rm *.orig
13.93 + rm *.orig~
13.94 + rm *.orig~
13.95 cd ..
13.96 -cd Interpret
13.97 +cd Specify
13.98 + echo "cd Specify was successful"
13.99 rm *.sml~
13.100 rm *.sml~
13.101 rm *.sml~~
13.102 @@ -201,12 +213,15 @@
13.103 rm *.thy~~~~~~~~
13.104 rm *.thy~~~~~~~~~
13.105 rm *.thy~~~~~~~~~~
13.106 - rm #*
13.107 - rm .\#*
13.108 - rm *.tar*
13.109 - rm *.orig
13.110 + rm #*
13.111 + rm .\#*
13.112 + rm *.tar*
13.113 + rm *.orig
13.114 + rm *.orig~
13.115 + rm *.orig~
13.116 cd ..
13.117 -cd MathEngine
13.118 +cd Interpret
13.119 + echo "cd Interpret was successful"
13.120 rm *.sml~
13.121 rm *.sml~
13.122 rm *.sml~~
13.123 @@ -229,12 +244,43 @@
13.124 rm *.thy~~~~~~~~
13.125 rm *.thy~~~~~~~~~
13.126 rm *.thy~~~~~~~~~~
13.127 - rm #*
13.128 - rm .\#*
13.129 - rm *.tar*
13.130 - rm *.orig
13.131 + rm #*
13.132 + rm .\#*
13.133 + rm *.tar*
13.134 + rm *.orig
13.135 + rm *.orig~
13.136 + cd ..
13.137 +cd MathEngine
13.138 + rm *.sml~
13.139 + rm *.sml~
13.140 + rm *.sml~~
13.141 + rm *.sml~~~
13.142 + rm *.sml~~~~
13.143 + rm *.sml~~~~~
13.144 + rm *.sml~~~~~~
13.145 + rm *.sml~~~~~~~
13.146 + rm *.sml~~~~~~~~
13.147 + rm *.sml~~~~~~~~~
13.148 + rm *.sml~~~~~~~~~~
13.149 + rm *.thy~
13.150 + rm *.thy~
13.151 + rm *.thy~~
13.152 + rm *.thy~~~
13.153 + rm *.thy~~~~
13.154 + rm *.thy~~~~~
13.155 + rm *.thy~~~~~~
13.156 + rm *.thy~~~~~~~
13.157 + rm *.thy~~~~~~~~
13.158 + rm *.thy~~~~~~~~~
13.159 + rm *.thy~~~~~~~~~~
13.160 + rm #*
13.161 + rm .\#*
13.162 + rm *.tar*
13.163 + rm *.orig
13.164 + rm *.orig~
13.165 cd ..
13.166 cd BridgeLibisabelle
13.167 + echo "cd BridgeLibisabelle was successful"
13.168 rm *.sml~
13.169 rm *.sml~
13.170 rm *.sml~~
13.171 @@ -263,6 +309,7 @@
13.172 rm *.orig
13.173 cd ..
13.174 cd Knowledge
13.175 + echo "cd Knowledge was successful"
13.176 rm *~
13.177 rm #*
13.178 rm .\#*
14.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sat Oct 26 13:03:16 2019 +0200
14.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Sun Oct 27 12:10:57 2019 +0100
14.3 @@ -185,9 +185,9 @@
14.4 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
14.5 | _ => if p = ([], Ctree.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
14.6
14.7 - (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Istate.Sundef, pt);
14.8 + (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt);
14.9 "~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
14.10 - = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Istate.Sundef, pt);
14.11 + = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Telem.Sundef, pt);
14.12
14.13 (*//--------------------- check results from modified me ----------------------------------\\*)
14.14 if p = ([1], Res) andalso
14.15 @@ -327,7 +327,7 @@
14.16 t, (res, asm)) = m;
14.17 if scrstate2str is =
14.18 "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,R,R], SOMEt_t, \n" ^
14.19 - "- (8 * g) + (-9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, Safe, false)"
14.20 + "- (8 * g) + (-9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, AppUndef_, false)"
14.21 andalso
14.22 term2str t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
14.23 andalso
15.1 --- a/test/Tools/isac/Interpret/script.sml Sat Oct 26 13:03:16 2019 +0200
15.2 +++ b/test/Tools/isac/Interpret/script.sml Sun Oct 27 12:10:57 2019 +0100
15.3 @@ -414,7 +414,7 @@
15.4 "~~~~~ fun init_pstate , args:"; val (thy, itms, metID) = (assoc_thy thy, meth, metID);
15.5 val (Pstate st, ctxt, Prog _) = init_pstate ctxt itms metID;
15.6 if scrstate2str st =
15.7 -"([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], NONE, \n??.empty, Safe, true)"
15.8 +"([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], NONE, \n??.empty, AppUndef_, true)"
15.9 then () else error "init_pstate changed for Biegelinie";
15.10
15.11 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)
16.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Sat Oct 26 13:03:16 2019 +0200
16.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Sun Oct 27 12:10:57 2019 +0100
16.3 @@ -72,7 +72,7 @@
16.4 val (Pstate (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
16.5 val ctxt'' = from_subpbl_to_caller ctxt scval ctxt'
16.6 val tac_ = Check_Postcond' (pI, (scval, asm))
16.7 - val is = Pstate (E,l,a,scval,scsaf,b);
16.8 + val is = Pstate (E,l,a,scval,Istate.Skip_,b);
16.9 "~~~~~ fun generate1, args:"; val (thy, (Check_Postcond' (pI, (scval, asm))), l, (p,p_), pt) =
16.10 (thy, tac_, (is, ctxt''), (pp, Res), pt);
16.11 val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete;