1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Nov 26 17:12:27 2019 +0100
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Nov 26 17:37:17 2019 +0100
1.3 @@ -197,10 +197,10 @@
1.4 if Tactical.contained_in t then raise TERM ("scan_dn1 expects Prog_Tac or Prog_Expr", [t])
1.5 else
1.6 case Lucin.interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t of
1.7 - (form_arg, Program.Expr _) =>
1.8 + (Program.Expr _, form_arg) =>
1.9 Term_Val1 (Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) eval
1.10 (subst_atomic (Env.update_opt'' (get_act_env ist, form_arg)) t))
1.11 - | (form_arg, Program.Tac prog_tac) =>
1.12 + | (Program.Tac prog_tac, form_arg) =>
1.13 interpret_tac1 cct ist (form_arg, prog_tac)
1.14
1.15 fun go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) =
1.16 @@ -370,8 +370,8 @@
1.17 if Tactical.contained_in t then raise TERM ("scan_dn2 expects Prog_Tac or Prog_Expr", [t])
1.18 else
1.19 case Lucin.interpret_leaf "next " ctxt eval (get_subst ist) t of
1.20 - (_, Program.Expr s) => Term_Val2 s
1.21 - | (a', Program.Tac stac) =>
1.22 + (Program.Expr s, _) => Term_Val2 s
1.23 + | (Program.Tac stac, a') =>
1.24 let
1.25 val (m, m') = Lucin.stac2tac_ pt (Celem.assoc_thy ctxt) stac
1.26 in
2.1 --- a/src/Tools/isac/Interpret/script.sml Tue Nov 26 17:12:27 2019 +0100
2.2 +++ b/src/Tools/isac/Interpret/script.sml Tue Nov 26 17:37:17 2019 +0100
2.3 @@ -33,7 +33,7 @@
2.4 val rew_only: (Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list) list -> bool
2.5 val interpret_leaf : (*TODO190625: shift to lucas-interpreter.sml ? <- sel_rules, sel_appl_atomic_tacs !*)
2.6 string -> Rule.theory' -> Rule.rls -> (Env.T * (term option * term)) -> term ->
2.7 - term option * Program.leaf
2.8 + Program.leaf * term option
2.9
2.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.11 (*NONE*)
2.12 @@ -615,7 +615,7 @@
2.13 (if (! trace_script)
2.14 then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Tac '" ^ Rule.term2str stac ^ "'")
2.15 else ();
2.16 - (a', Program.Tac stac'))
2.17 + (Program.Tac stac', a'))
2.18 end
2.19 | (a', Program.Expr lexpr) => (* Prog_Expr *)
2.20 let val lexpr' =
2.21 @@ -624,7 +624,7 @@
2.22 (if (! trace_script)
2.23 then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
2.24 else ();
2.25 - (a', Program.Expr lexpr')) (*lexpr' is the value of the Expr*)
2.26 + (Program.Expr lexpr', a')) (*lexpr' is the value of the Expr*)
2.27 end;
2.28
2.29 (*. fetch _all_ tactics from script .*)
2.30 @@ -643,7 +643,7 @@
2.31 val (sc, srls) = (case Specify.get_met metID' of
2.32 {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
2.33 val subst = get_istate pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
2.34 - in map ((stac2tac pt thy) o Program.rep_stacexpr o #2 o
2.35 + in map ((stac2tac pt thy) o Program.rep_stacexpr o #1 o
2.36 (interpret_leaf "selrul" thy' srls subst)) (Auto_Prog.stacpbls sc)
2.37 end;
2.38
2.39 @@ -670,7 +670,7 @@
2.40 val (env, (a, v)) = (case get_istate pt (p, p_) of
2.41 Istate.Pstate pst => (Istate.get_subst pst) | _ => error "sel_appl_atomic_tacs 2")
2.42 val alltacs = (*we expect at least 1 stac in a script*)
2.43 - map ((stac2tac pt thy) o Program.rep_stacexpr o #2 o
2.44 + map ((stac2tac pt thy) o Program.rep_stacexpr o #1 o
2.45 (interpret_leaf "selrul" thy' srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
2.46 val f =
2.47 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
3.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Nov 26 17:12:27 2019 +0100
3.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Nov 26 17:37:17 2019 +0100
3.3 @@ -83,7 +83,7 @@
3.4 (*======= end of scanning tacticals, a leaf =======*)
3.5 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
3.6 = (xxx, (ist |> path_down [L, R]), e);
3.7 -val (a', Program.Tac stac) = interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t;
3.8 +val (Program.Tac stac, a') = interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t;
3.9
3.10
3.11 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
3.12 @@ -151,7 +151,7 @@
3.13 (*======= end of scanning tacticals, a leaf =======*)
3.14 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
3.15 = (xxx, (ist |> path_down [R]), e);
3.16 - val (a', Program.Tac stac) =
3.17 + val (Program.Tac stac, a') =
3.18 (*case*) interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
3.19 val Lucin.Ass (m, v', ctxt) =
3.20 (*case*) associate pt ctxt (m, stac) (*of*);
3.21 @@ -328,7 +328,7 @@
3.22 (*======= end of scanning tacticals, a leaf =======*)
3.23 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, act_arg, or, ...}), t)
3.24 = (xxx, (ist |> path_down [R]), e);
3.25 - val (a', Program.Tac stac) = (*case*) interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
3.26 + val (Program.Tac stac, a') = (*case*) interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
3.27 val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*);
3.28 val ORundef = (*case*) or (*of*);
3.29 val Notappl "norm_equation not applicable" =
4.1 --- a/test/Tools/isac/Interpret/script.sml Tue Nov 26 17:12:27 2019 +0100
4.2 +++ b/test/Tools/isac/Interpret/script.sml Tue Nov 26 17:37:17 2019 +0100
4.3 @@ -207,7 +207,7 @@
4.4 val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
4.5 val Pstate ist = get_istate pt (p,p_)
4.6 val alltacs = (*we expect at least 1 stac in a script*)
4.7 - map ((stac2tac pt thy) o rep_stacexpr o #2 o
4.8 + map ((stac2tac pt thy) o rep_stacexpr o #1 o
4.9 (interpret_leaf "selrul" thy' srls (get_subst ist) )) (stacpbls sc)
4.10 val f =
4.11 case p_ of
5.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue Nov 26 17:12:27 2019 +0100
5.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Tue Nov 26 17:37:17 2019 +0100
5.3 @@ -236,7 +236,7 @@
5.4 ... Accept_Tac1 ... is correct*)
5.5 "~~~~~ fun scan_dn1, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
5.6 ((((y,s),d),ORundef), ((E, l@[R,D], a,v,S,b),ss), body);
5.7 -val (a', Program.Tac stac) = interpret_leaf "locate" thy' sr (E, (a, v)) t
5.8 +val (Program.Tac stac, a') = interpret_leaf "locate" thy' sr (E, (a, v)) t
5.9 val ctxt = get_ctxt pt (p,p_)
5.10 val p' = lev_on p : pos;
5.11 (* WAS val NotAss = associate pt d (m, stac)
6.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Nov 26 17:12:27 2019 +0100
6.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Nov 26 17:37:17 2019 +0100
6.3 @@ -146,7 +146,7 @@
6.4 (* a leaf has been found *)
6.5 "~~~~~ fun scan_dn2, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) =
6.6 (thy, ptp, E, (l @ [Celem.R]), e, a, v);
6.7 -val (a', Program.Tac stac) = interpret_leaf "next " th sr (E, (a, v)) t;
6.8 +val (Program.Tac stac, a') = interpret_leaf "next " th sr (E, (a, v)) t;
6.9 val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac;
6.10 "~~~~~ fun stac2tac_, args:"; val (_, _, (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _)) =
6.11 (pt, (Celem.assoc_thy th), stac);
7.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Nov 26 17:12:27 2019 +0100
7.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Nov 26 17:37:17 2019 +0100
7.3 @@ -79,7 +79,7 @@
7.4 (*======= end of scanning tacticals, a leaf =======*)
7.5 "~~~~~ fun scan_dn1, args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) =
7.6 (xxx, (ist |> path_down_form ([L, R], a)), e);
7.7 -val (a', Program.Tac stac) = (*case*) interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
7.8 +val (Program.Tac stac, a') = (*case*) interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
7.9
7.10 val Ass (Rewrite_Set' _, _, _) = (*case*)
7.11 associate pt ctxt (m, stac) (*of*);
7.12 @@ -216,7 +216,7 @@
7.13 (*========== a leaf has been found ==========*)
7.14 "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
7.15 = (xxx, (ist |> path_down [L, R]), e);
7.16 - val (a', Program.Tac stac) = (*case*) Lucin.interpret_leaf "next " ctxt eval (get_subst ist) t (*of*);
7.17 + val (Program.Tac stac, a') = (*case*) Lucin.interpret_leaf "next " ctxt eval (get_subst ist) t (*of*);
7.18
7.19 (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy ctxt) stac;
7.20 "~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags'))
8.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Tue Nov 26 17:12:27 2019 +0100
8.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Tue Nov 26 17:37:17 2019 +0100
8.3 @@ -94,7 +94,7 @@
8.4 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
8.5 = (xxx, (ist |> path_down [L, R]), e);
8.6
8.7 -val (NONE, Program.Tac _) = (*case*)
8.8 +val (Program.Tac _, NONE) = (*case*)
8.9 interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
8.10 "~~~~~ fun interpret_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
8.11 = ("locate", (Context.theory_name (Rule.Isac"")), eval, (get_subst ist), t);
9.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Tue Nov 26 17:12:27 2019 +0100
9.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Tue Nov 26 17:37:17 2019 +0100
9.3 @@ -84,7 +84,7 @@
9.4 (*========== a leaf has been found ==========*)
9.5 "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
9.6 = (xxx, (ist |> path_up_down [R, D] |> upd_env i), body);
9.7 - val (a', Program.Tac stac) = (*case*)
9.8 + val (Program.Tac stac, a') = (*case*)
9.9 interpret_leaf "next " ctxt eval (get_subst ist) t;
9.10
9.11 val (Check_elementwise "Assumptions", Empty_Tac_) =
10.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Tue Nov 26 17:12:27 2019 +0100
10.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Tue Nov 26 17:37:17 2019 +0100
10.3 @@ -150,7 +150,7 @@
10.4 "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
10.5 = (xxx, (ist |> path_down [R]), e);
10.6
10.7 - val (a', Program.Tac stac) =
10.8 + val (Program.Tac stac, a') =
10.9 (*case*) interpret_leaf "next " th sr (get_subst ist) t (*of*);
10.10 "~~~~~ fun interpret_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
10.11 = ("next ", th, sr, (get_subst ist), t);