1.1 --- a/src/Tools/isac/CalcElements/environment.sml Sat Dec 14 09:41:17 2019 +0100
1.2 +++ b/src/Tools/isac/CalcElements/environment.sml Sat Dec 14 13:36:40 2019 +0100
1.3 @@ -45,7 +45,7 @@
1.4 thus "NONE" must be set at the end of currying (ill designed anyway)*)
1.5 fun update_opt env (SOME id, vl) = update env (id, vl)
1.6 | update_opt env (NONE, vl) =
1.7 - ((**)tracing ("*** update_opt: (NONE," ^ Rule.term2str vl ^ ")");(**) env);
1.8 + ((** )tracing ("*** update_opt: (NONE," ^ Rule.term2str vl ^ ")");( **) env);
1.9 fun update_opt' (env, (id, vl)) = update_opt env (id, vl)
1.10 fun update_opt'' ((vl, env), id) = update_opt env (id, vl)
1.11
2.1 --- a/src/Tools/isac/CalcElements/libraryC.sml Sat Dec 14 09:41:17 2019 +0100
2.2 +++ b/src/Tools/isac/CalcElements/libraryC.sml Sat Dec 14 13:36:40 2019 +0100
2.3 @@ -234,6 +234,7 @@
2.4 fun if_none NONE y = y (*cp from 2002 Pure/library.ML FIXXXME replace*)
2.5 | if_none (SOME x) _ = x;
2.6
2.7 +(* for tests only *)
2.8 fun compare_strs str1 str2 =
2.9 let
2.10 fun comp_char (c1, c2) = tracing ("comp_strs: " ^ c1 ^ " = " ^ c2 ^ " ..." ^ bool2str (c1 = c2))
3.1 --- a/src/Tools/isac/Interpret/Interpret.thy Sat Dec 14 09:41:17 2019 +0100
3.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Sat Dec 14 13:36:40 2019 +0100
3.3 @@ -13,27 +13,6 @@
3.4 ML_file "lucas-interpreter.sml"
3.5 ML \<open>
3.6 \<close> ML \<open>
3.7 -fun msg call t Tac_Expr ptac =
3.8 -if (! trace_script)
3.9 -then tracing ("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^
3.10 - "' ---> " ^ Tac_Expr ^ " '" ^ Rule.term2str ptac ^ "'")
3.11 -else ();
3.12 -
3.13 -fun interpret_leaf ctxt srls (E, (a, v)) t =
3.14 - case Prog_Tac.eval_leaf E a v t of
3.15 - (Program.Tac stac, a') =>
3.16 - let val stac' =
3.17 - Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
3.18 - (subst_atomic (Env.update_opt E (a,v)) stac)
3.19 - in
3.20 - msg " leaf '" t "Tac" stac; (Program.Tac stac', a')
3.21 - end
3.22 - | (Program.Expr lexpr, a') =>
3.23 - let val lexpr' =
3.24 - Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls (subst_atomic (Env.update_opt E (a,v)) lexpr)
3.25 - in
3.26 - msg " leaf '" t "Expr" lexpr'; (Program.Expr lexpr', a')
3.27 - end;
3.28 \<close> ML \<open>
3.29 \<close>
3.30 end
4.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Dec 14 09:41:17 2019 +0100
4.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Dec 14 13:36:40 2019 +0100
4.3 @@ -557,7 +557,7 @@
4.4 Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p (*collects and instantiates asms*)
4.5 | _ => get_assumptions_ pt (p, p_))
4.6 val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
4.7 - (*extend Tactic.Check_Postcond' (pI, (scval, asm), scsaf) ^^^^^ ?*)
4.8 + (*TODO?: extend Tactic.Check_Postcond' (pI, (prog_res, asm), ^^^^^ scsaf) ?*)
4.9 val (pst, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate pst, ctxt) => (pst, ctxt)
4.10 | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc"
4.11 val thy' = get_obj g_domID pt pp;
5.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sat Dec 14 09:41:17 2019 +0100
5.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sat Dec 14 13:36:40 2019 +0100
5.3 @@ -491,10 +491,10 @@
5.4 let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Celem.thm_of_thm r) t;
5.5 in
5.6 case ropt of SOME ta => [(r, ta)]
5.7 - | NONE => (tracing
5.8 - ("### locate_rule: rewrite " ^ Celem.id_of_thm r ^ " " ^ Rule.term2str t ^ " = NONE"); [])
5.9 + | NONE => ((*tracing
5.10 + ("### locate_rule: rewrite " ^ Celem.id_of_thm r ^ " " ^ Rule.term2str t ^ " = NONE");*) [])
5.11 end
5.12 - else (tracing ("### locate_rule: " ^ Celem.id_of_thm r ^ " not mem rrls"); [])
5.13 + else ((*tracing ("### locate_rule: " ^ Celem.id_of_thm r ^ " not mem rrls");*) [])
5.14 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
5.15
5.16 fun next_rule thy eval_rls ro [rs] t =
5.17 @@ -555,9 +555,9 @@
5.18 case ropt of
5.19 SOME ta => [(r, ta)]
5.20 | NONE =>
5.21 - (tracing ("### locate_rule: rewrite " ^ Celem.id_of_thm r ^ " " ^ Rule.term2str t ^ " = NONE");
5.22 + ((*tracing ("### locate_rule: rewrite " ^ Celem.id_of_thm r ^ " " ^ Rule.term2str t ^ " = NONE");*)
5.23 []) end
5.24 - else (tracing ("### locate_rule: " ^ Celem.id_of_thm r ^ " not mem rrls"); [])
5.25 + else ((*tracing ("### locate_rule: " ^ Celem.id_of_thm r ^ " not mem rrls");*) [])
5.26 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
5.27
5.28 fun next_rule thy eval_rls ro [rs] t =
6.1 --- a/src/Tools/isac/MathEngBasic/model.sml Sat Dec 14 09:41:17 2019 +0100
6.2 +++ b/src/Tools/isac/MathEngBasic/model.sml Sat Dec 14 13:36:40 2019 +0100
6.3 @@ -342,9 +342,9 @@
6.4 (* 14.9.01: not used after putting values for penv into itm_
6.5 WN.5.5.03: used in upd .. upd_envv *)
6.6 fun upd_penv ctxt penv dsc (id, vl) =
6.7 -(tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
6.8 +((*tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
6.9 tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
6.10 - tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
6.11 + tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";*)
6.12 overwrite (penv, (id, Input_Descript.pbl_ids ctxt dsc vl))
6.13 );
6.14
6.15 @@ -437,21 +437,21 @@
6.16 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;
6.17 val unique = (Thm.term_of o the o (TermC.parse @{theory "Real"} )) "UnIqE_tErM";
6.18 fun d_in (Cor ((d ,_), _)) = d
6.19 - | d_in (Syn c) = (tracing ("*** d_in: Syn ("^c^")"); unique)
6.20 - | d_in (Typ c) = (tracing ("*** d_in: Typ ("^c^")"); unique)
6.21 + | d_in (Syn c) = ((*tracing ("*** d_in: Syn ("^c^")");*) unique)
6.22 + | d_in (Typ c) = ((*tracing ("*** d_in: Typ ("^c^")");*) unique)
6.23 | d_in (Inc ((d, _), _)) = d
6.24 | d_in (Sup (d, _)) = d
6.25 | d_in (Mis (d, _)) = d
6.26 - | d_in _ = error "d_in: uncovered case in fun.def.";
6.27 + | d_in _ = raise ERROR "d_in: uncovered case in fun.def.";
6.28
6.29 fun dts2str (d, ts) = pair2str (Rule.term2str d, Rule.terms2str ts);
6.30 fun penvval_in (Cor ((d, _), (_, ts))) = [comp_ts (d,ts)]
6.31 - | penvval_in (Syn (c)) = (tracing("*** penvval_in: Syn ("^c^")"); [])
6.32 - | penvval_in (Typ (c)) = (tracing("*** penvval_in: Typ ("^c^")"); [])
6.33 + | penvval_in (Syn (c)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
6.34 + | penvval_in (Typ (c)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
6.35 | penvval_in (Inc (_, (_, ts))) = ts
6.36 - | penvval_in (Sup dts) = (tracing ("*** penvval_in: Sup "^(dts2str dts)); [])
6.37 - | penvval_in (Mis (d, t)) = (tracing ("*** penvval_in: Mis " ^
6.38 - pair2str(Rule.term2str d, Rule.term2str t)); [])
6.39 + | penvval_in (Sup dts) = ((*tracing ("*** penvval_in: Sup " ^ dts2str dts);*) [])
6.40 + | penvval_in (Mis (d, t)) = ((*tracing ("*** penvval_in: Mis " ^
6.41 + pair2str(Rule.term2str d, Rule.term2str t));*) [])
6.42 | penvval_in _ = error "penvval_in: uncovered case in fun.def.";
6.43
6.44 (* check a predicate labelled with indication of incomplete substitution;
7.1 --- a/src/Tools/isac/MathEngine/solve.sml Sat Dec 14 09:41:17 2019 +0100
7.2 +++ b/src/Tools/isac/MathEngine/solve.sml Sat Dec 14 13:36:40 2019 +0100
7.3 @@ -171,20 +171,26 @@
7.4 let
7.5 val pp = par_pblobj pt p
7.6 val asm =
7.7 - (case get_obj g_tac pt p of (*assumes Check_elementwise IMMEDIATELY BEFORE Check_Postcond*)
7.8 - Tactic.Check_elementwise _ => (*collects and instantiates asms*)
7.9 - (snd o (get_obj g_result pt)) p
7.10 + (case get_obj g_tac pt p of (*collects and instantiates asms*)
7.11 + Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
7.12 | _ => get_assumptions_ pt (p,p_))
7.13 - handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
7.14 + handle _ => []
7.15 val metID = get_obj g_metID pt pp;
7.16 - val {scr = sc, ...} = Specify.get_met metID;
7.17 + val {scr = sc as Rule.Prog prog, ...} = Specify.get_met metID;
7.18 val (pst, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate pst, ctxt) => (pst, ctxt)
7.19 | _ => error "solve Check_Postcond: uncovered case get_loc"
7.20
7.21 val thy' = get_obj g_domID pt pp;
7.22 val thy = Celem.assoc_thy thy';
7.23 - val (_, _, (scval, _(*scsaf*))) = LucinNEW.determine_next_tactic sc (pt, (p, p_)) (Istate.Pstate pst) ctxt;
7.24 - (* Telem.safe should go on to Check_Postcond' vvvvv *)
7.25 +(*OLD*)(*TODO?: required for 1 step in caller ??? vvvvvvvvvvvvvvvvvvvvv; dropped in begin_end_prog*)
7.26 +(*OLD*)val (_, _, (scval, _(*scsaf*))) = LucinNEW.determine_next_tactic (sc) (pt, (p, p_)) (Istate.Pstate pst) ctxt;
7.27 +(*OLD*)
7.28 +(*NEW* )(* Tactic.input has NO prog_result, but *)
7.29 +(*NEW*)val tac =
7.30 +(*NEW*) case LucinNEW.determine_next_tactic (sc) (pt, (p, p_)) (Istate.Pstate pst) ctxt of
7.31 +(*NEW*) End_Program (_, tac as Tactic.Check_Postcond' _) => tac
7.32 +(*NEW*) | _ \<Rightarrow> raise ERROR ("solve Check_Postcond " ^ Rule.strs2str' pI)
7.33 +( *NEW*)
7.34 in
7.35 if pp = []
7.36 then
8.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Sat Dec 14 09:41:17 2019 +0100
8.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Sat Dec 14 13:36:40 2019 +0100
8.3 @@ -93,8 +93,8 @@
8.4 (**)
8.5
8.6 (*+ for Or_to_List +*)
8.7 -fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True"; UniversalList)
8.8 - | or2list (Const ("HOL.False",_)) = (tracing"### or2list False"; EmptyList)
8.9 +fun or2list (Const ("HOL.True",_)) = ((*tracing"### or2list True";*) UniversalList)
8.10 + | or2list (Const ("HOL.False",_)) = ((*tracing"### or2list False";*) EmptyList)
8.11 | or2list (t as Const ("HOL.eq",_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
8.12 | or2list ors =
8.13 let
9.1 --- a/src/Tools/isac/Specify/ptyps.sml Sat Dec 14 09:41:17 2019 +0100
9.2 +++ b/src/Tools/isac/Specify/ptyps.sml Sat Dec 14 13:36:40 2019 +0100
9.3 @@ -582,7 +582,7 @@
9.4 (* refine a problem; version providing output for math-experts *)
9.5 fun refin' (pblRD: pblRD) fmz pbls (Celem.Ptyp (pI, [py], [])) =
9.6 let
9.7 - val _ = (tracing o ((curry op ^) "*** pass ") o strs2str) (pblRD @ [pI])
9.8 + val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
9.9 val {thy, ppc, where_, prls, ...} = py
9.10 val oris = prep_ori fmz thy ppc |> #1;
9.11 (* WN020803: itms!: oris might _not_ be complete here *)
10.1 --- a/src/Tools/isac/TODO.thy Sat Dec 14 09:41:17 2019 +0100
10.2 +++ b/src/Tools/isac/TODO.thy Sat Dec 14 13:36:40 2019 +0100
10.3 @@ -76,6 +76,8 @@
10.4 text \<open>
10.5 \begin{itemize}
10.6 \item xxx
10.7 + \item ? rename begin_end_prog -> check_switch_prog
10.8 + \item xxx
10.9 \item decompose do_solve_step, begin_end_prog: mutual recursion only avoids multiple generate1
10.10 ! ^^^ in determine_next_tactic --- ? ? ? in locate_input_tactic ?
10.11 \item xxx
10.12 @@ -326,14 +328,14 @@
10.13 \item xxx
10.14 \end{itemize}
10.15 \<close>
10.16 -subsection \<open>solve, loc_solve_, ...\<close>
10.17 +subsection \<open>solve, loc_solve_, begin_end_prog, do_solve_step, ...\<close>
10.18 text \<open>
10.19 - unify to calcstate, calcstate'
10.20 + unify to calcstate, calcstate', ?Ctree.state?
10.21 \begin{itemize}
10.22 - \item ?delete Check_Postcond' in begin_end_prog (already done in solve?)
10.23 - in case both are needed, unify !
10.24 + \item begin_end_prog Check_Postcond' needs NO 2.determine_next_tactic
10.25 + solve Check_Postcond' needs, because NO prog_result in Tactic.input
10.26 + and applicable_in cannot get it.
10.27 \item xxx
10.28 - \item ? rename begin_end_prog -> check_switch_prog
10.29 \item adopt the same for specification phase
10.30 \item xxx
10.31 \end{itemize}