1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Oct 19 14:26:58 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Oct 19 14:59:09 2019 +0200
1.3 @@ -171,7 +171,7 @@
1.4 | ay => ay)
1.5 (* a leaf has been found *)
1.6 | appy ((th,sr)) (pt, p) E l t a v =
1.7 - case Lucin.handle_leaf "next " th sr E a v t of
1.8 + case Lucin.handle_leaf "next " th sr (E, (a, v)) t of
1.9 (_, Celem.Expr s) => Skip (s, E)
1.10 | (a', Celem.STac stac) =>
1.11 let val (m,m') = Lucin.stac2tac_ pt (Celem.assoc_thy th) stac
1.12 @@ -481,7 +481,7 @@
1.13 NasNap (v, E) => assy ya ((E,(l @ [R]),a,v,S,b), ss) e2
1.14 | ay => (ay))
1.15 ( *NEW..*)
1.16 - | assy ya (ist as (E,l,a,v,S,b), ss) (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =
1.17 + | assy ya (ist, ss) (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =
1.18 (case assy ya (ist |> path_down [L, R], ss) e1 of
1.19 NasNap (v, E) => assy ya (ist |> path_down [R] |> upd_act_env (v, E), ss) e2
1.20 | ay => (ay))
1.21 @@ -489,7 +489,7 @@
1.22 (*======= end of scanning tacticals, a leaf =======*)
1.23 (*12* )
1.24 | assy (ctxt,sr,(pt,p),ap) ((E,l,a,v,S,_), m) t =
1.25 - (case Lucin.handle_leaf "locate" "Isac_Knowledge" sr E a v t of
1.26 + (case Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t of
1.27 (a', Celem.Expr _) =>
1.28 (NasNap (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") sr
1.29 (subst_atomic (Env.upd_env_opt E (a',v)) t), E))
1.30 @@ -508,11 +508,11 @@
1.31 | Chead.Notappl _ => (NasNap (v, E)
1.32 ))))
1.33 ( *NEW..*)
1.34 - | assy (ctxt,sr,(pt,p),ap) (ist as ((*TODO-----------------------------*) E,l,a,v,S,_), m) t =
1.35 - (case Lucin.handle_leaf "locate" (Context.theory_name (Rule.Isac"")) sr E a v t of
1.36 + | assy (ctxt,sr,(pt,p),ap) (ist, m) t =
1.37 + (case Lucin.handle_leaf "locate" (Context.theory_name (Rule.Isac"")) sr (get_subst ist) t of
1.38 (a', Celem.Expr _) =>
1.39 (NasNap (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") sr
1.40 - (subst_atomic (Env.upd_env_opt'' (get_act_env ist, a')) t), E))
1.41 + (subst_atomic (Env.upd_env_opt'' (get_act_env ist, a')) t), get_env ist))
1.42 | (a', Celem.STac stac) =>
1.43 (case Lucin.associate pt ctxt (m, stac) of
1.44 (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE *)
2.1 --- a/src/Tools/isac/Interpret/script.sml Sat Oct 19 14:26:58 2019 +0200
2.2 +++ b/src/Tools/isac/Interpret/script.sml Sat Oct 19 14:59:09 2019 +0200
2.3 @@ -32,7 +32,7 @@
2.4 val stac2tac : Ctree.ctree -> theory -> term -> Tactic.input
2.5 val rew_only: (Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list) list -> bool
2.6 val handle_leaf : (*TODO190625: shift to lucas-interpreter.sml ? <- sel_rules, sel_appl_atomic_tacs !*)
2.7 - string -> Rule.theory' -> Rule.rls -> Env.T -> term option -> term -> term ->
2.8 + string -> Rule.theory' -> Rule.rls -> (Env.T * (term option * term)) -> term ->
2.9 term option * Celem.stacexpr
2.10
2.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.12 @@ -629,7 +629,7 @@
2.13 (1) 'subst_stacexpr' substitute Env.upd_env and complete curried tactic
2.14 (2) rewrite the leaf by 'srls'
2.15 *)
2.16 -fun handle_leaf call thy srls E a v t =
2.17 +fun handle_leaf call thy srls (E, (a, v)) t =
2.18 (*WN050916 'upd_env_opt' is a blind copy from previous version*)
2.19 case Prog_Tac.subst_stacexpr E a v t of
2.20 (a', Celem.STac stac) => (* Prog_Tac *)
2.21 @@ -669,7 +669,7 @@
2.22 val (env, a, v) = (case get_istate pt (p, p_) of
2.23 Istate.Pstate (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_rules 2")
2.24 in map ((stac2tac pt thy) o Celem.rep_stacexpr o #2 o
2.25 - (handle_leaf "selrul" thy' srls env a v)) (Auto_Prog.stacpbls sc)
2.26 + (handle_leaf "selrul" thy' srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
2.27 end;
2.28
2.29 (* fetch tactics from script and filter _applicable_ tactics;
2.30 @@ -696,7 +696,7 @@
2.31 Istate.Pstate (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_appl_atomic_tacs 2")
2.32 val alltacs = (*we expect at least 1 stac in a script*)
2.33 map ((stac2tac pt thy) o Celem.rep_stacexpr o #2 o
2.34 - (handle_leaf "selrul" thy' srls env a v)) (Auto_Prog.stacpbls sc)
2.35 + (handle_leaf "selrul" thy' srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
2.36 val f =
2.37 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
2.38 | _ => error "")
3.1 --- a/src/Tools/isac/Specify/istate.sml Sat Oct 19 14:26:58 2019 +0200
3.2 +++ b/src/Tools/isac/Specify/istate.sml Sat Oct 19 14:59:09 2019 +0200
3.3 @@ -17,6 +17,7 @@
3.4 val e_istate: T
3.5
3.6 val get_path: scrstate -> Celem.loc_
3.7 + val get_env: scrstate -> Env.T
3.8 val get_act_env: scrstate -> (term * Env.T)
3.9 val get_subst: scrstate -> (Env.T * (term option * term))
3.10 val get_assoc: scrstate -> bool
3.11 @@ -93,6 +94,7 @@
3.12 | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
3.13
3.14 fun get_path (_, path, _, _, _, _) = path
3.15 +fun get_env (env, _, _, _, _, _) = env
3.16 fun get_act_env (env, _, _, act_arg, _, _) = (act_arg, env)
3.17 fun get_assoc (_, _, _, _, _, ass) = ass
3.18 fun get_subst (env, _, form_arg, act_arg, _, _) = (env, (form_arg, act_arg))
4.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sat Oct 19 14:26:58 2019 +0200
4.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Sat Oct 19 14:59:09 2019 +0200
4.3 @@ -63,7 +63,7 @@
4.4 (*check: true*) term2str e = "Take (Integral f_f D v_v)";
4.5 "~~~~~ fun assy, args:"; val ((thy',ctxt,sr,d,ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
4.6 (ya, ((E , l@[L,R], a,v,S,b),ss), e);
4.7 -val (a', STac stac) = handle_leaf "locate" thy' sr E a v t;
4.8 +val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t;
4.9 (* val ctxt = get_ctxt pt (p,p_)
4.10 exception PTREE "get_obj: pos = [0] does not exist" raised
4.11 (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)
5.1 --- a/test/Tools/isac/Interpret/script.sml Sat Oct 19 14:26:58 2019 +0200
5.2 +++ b/test/Tools/isac/Interpret/script.sml Sat Oct 19 14:59:09 2019 +0200
5.3 @@ -207,7 +207,7 @@
5.4 val Pstate (env,_,a,v,_,_) = get_istate pt (p,p_)
5.5 val alltacs = (*we expect at least 1 stac in a script*)
5.6 map ((stac2tac pt thy) o rep_stacexpr o #2 o
5.7 - (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
5.8 + (handle_leaf "selrul" thy' srls (env, (a, v)))) (stacpbls sc)
5.9 val f =
5.10 case p_ of
5.11 Frm => get_obj g_form pt p
6.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Sat Oct 19 14:26:58 2019 +0200
6.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Sat Oct 19 14:59:09 2019 +0200
6.3 @@ -194,7 +194,7 @@
6.4
6.5 "~~~~~ fun assy , args:"; val (((*thy',*)ctxt,sr,d,ap), ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss), t) =
6.6 (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);
6.7 -val (a', STac stac) = (*case*) handle_leaf "locate" thy' sr E a v t (*of*);
6.8 +val (a', STac stac) = (*case*) handle_leaf "locate" thy' sr (E, (a, v)) t (*of*);
6.9 (*+*)writeln (term2str stac); (*SubProblem
6.10 (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
6.11 [''Biegelinien'', ''ausBelastung''])
7.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Sat Oct 19 14:26:58 2019 +0200
7.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Sat Oct 19 14:59:09 2019 +0200
7.3 @@ -238,7 +238,7 @@
7.4 ... Assoc ... is correct*)
7.5 "~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
7.6 ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
7.7 -val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
7.8 +val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t
7.9 val ctxt = get_ctxt pt (p,p_)
7.10 val p' = lev_on p : pos;
7.11 (* WAS val NotAss = associate pt d (m, stac)
8.1 --- a/test/Tools/isac/Knowledge/rateq.sml Sat Oct 19 14:26:58 2019 +0200
8.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Sat Oct 19 14:59:09 2019 +0200
8.3 @@ -120,7 +120,7 @@
8.4 val E = Env.upd_env E (i, v);
8.5 "~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) =
8.6 (thy, ptp, E, (up@[R,D]), body, a, v);
8.7 -"~~~~~ fun handle_leaf, args:"; val (call, thy, srls, E, a, v, t) = ("next ", th, sr, E, a, v, t);
8.8 +"~~~~~ fun handle_leaf, args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t);
8.9 "~~~~~ fun subst_stacexpr, args:"; val (E, a, v,
8.10 (t as (Const ("Prog_Tac.Check'_elementwise",_) $ _ $ _ ))) = (E, a, v, t);
8.11 val STac tm = STac (subst_atomic E t);
9.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Sat Oct 19 14:26:58 2019 +0200
9.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Sat Oct 19 14:59:09 2019 +0200
9.3 @@ -144,7 +144,7 @@
9.4 (* a leaf has been found *)
9.5 "~~~~~ fun appy, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) =
9.6 (thy, ptp, E, (l @ [Celem.R]), e, a, v);
9.7 -val (a', STac stac) = handle_leaf "next " th sr E a v t;
9.8 +val (a', STac stac) = handle_leaf "next " th sr (E, (a, v)) t;
9.9 val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac;
9.10 "~~~~~ fun stac2tac_, args:"; val (_, _, (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _)) =
9.11 (pt, (Celem.assoc_thy th), stac);
10.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Sat Oct 19 14:26:58 2019 +0200
10.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Sat Oct 19 14:59:09 2019 +0200
10.3 @@ -86,7 +86,7 @@
10.4 (*======= end of scanning tacticals, a leaf =======*)
10.5 "~~~~~ fun assy, args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,S,_), m), t) =
10.6 (ya, ((E, l @ [Celem.R], a,v,S,b),ss), e);
10.7 -val (a', STac stac) = (*case*) handle_leaf "locate" thy' sr E a v t (*of*);
10.8 +val (a', STac stac) = (*case*) handle_leaf "locate" thy' sr (E, (a, v)) t (*of*);
10.9
10.10 (*val Ass (m,v') = in isabisacREP*)
10.11 (*val NotAss = in isabisac*)
10.12 @@ -233,7 +233,7 @@
10.13 (*case*) appy thy ptp E (l @ [Celem.L, Celem.R]) e a v (*of*);
10.14 "~~~~~ fun appy , args:"; val (((th,sr)), (pt, p), E, l, t, a, v)
10.15 = (thy, ptp, E, (l @ [Celem.L, Celem.R]), e, a, v);
10.16 - val (a', STac stac) = (*case*) Lucin.handle_leaf "next " th sr E a v t (*of*);
10.17 + val (a', STac stac) = (*case*) Lucin.handle_leaf "next " th sr (E, (a, v)) t (*of*);
10.18
10.19 (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy th) stac;
10.20 "~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags'))
11.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Sat Oct 19 14:26:58 2019 +0200
11.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Sat Oct 19 14:59:09 2019 +0200
11.3 @@ -98,9 +98,9 @@
11.4 "~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,S,_), m), t)
11.5 = (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);
11.6
11.7 -(*val (a', STac stac) = ( *case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr E a v t (*of*);
11.8 -"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, E, a, v, t)
11.9 - = ("locate", "Isac_Knowledge", sr, E, a, v, t);
11.10 +(*val (a', STac stac) = ( *case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
11.11 +"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
11.12 + = ("locate", "Isac_Knowledge", sr, (E, (a, v)), t);
11.13
11.14 val (a', STac stac) = (*case*) Prog_Tac.subst_stacexpr E a v t (*of*);
11.15 "~~~~~ fun subst_stacexpr , args:"; val (E, _, _, (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)))
12.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Sat Oct 19 14:26:58 2019 +0200
12.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Sat Oct 19 14:59:09 2019 +0200
12.3 @@ -76,8 +76,8 @@
12.4 body; (*= Const ("Prog_Tac.Check'_elementwise"*)
12.5 "~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v)=
12.6 (thy, ptp, E, (up@[R,D]), body, a, v);
12.7 -handle_leaf "next " th sr E a v t; (*= (NONE, STac (Const ("Prog_Tac.Check'_elementwise"*)
12.8 -val (a', STac stac) = handle_leaf "next " th sr E a v t;
12.9 +handle_leaf "next " th sr (E, (a, v)) t; (*= (NONE, STac (Const ("Prog_Tac.Check'_elementwise"*)
12.10 +val (a', STac stac) = handle_leaf "next " th sr (E, (a, v)) t;
12.11 "~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Prog_Tac.Check'_elementwise",_) $ _ $
12.12 (set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) = (pt, (assoc_thy th), stac);
12.13 (*2011 changed ^^^^^ *)
13.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Sat Oct 19 14:26:58 2019 +0200
13.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Sat Oct 19 14:59:09 2019 +0200
13.3 @@ -145,9 +145,9 @@
13.4
13.5 "~~~~~ fun appy, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) =
13.6 (thy, ptp, E, (l @ [Celem.R]), e, a, v);
13.7 - val (a', STac stac) = (*case*) handle_leaf "next " th sr E a v t (*of*);
13.8 + val (a', STac stac) = (*case*) handle_leaf "next " th sr (E, (a, v)) t (*of*);
13.9
13.10 -"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, E, a, v, t) = ("next ", th, sr, E, a, v, t);
13.11 +"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t);
13.12 (*+*)val [(Free ("t_t", Tt_t), Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Free ("-1", _) $ Free ("x", _)) $ Free ("0", _)),
13.13 (Free ("v", Tv), Free ("x", Tx))] = E (* THE WRONG TYPES IN E ..(TODO.4)*)
13.14
14.1 --- a/test/Tools/isac/Test_Some.thy Sat Oct 19 14:26:58 2019 +0200
14.2 +++ b/test/Tools/isac/Test_Some.thy Sat Oct 19 14:59:09 2019 +0200
14.3 @@ -158,7 +158,7 @@
14.4 "~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,S,_), m), t)
14.5 = (ya, ((E, l @ [Celem.R], a,v,S,b),ss), e);
14.6 \<close> ML \<open>
14.7 - val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr E a v t (*of*);
14.8 + val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
14.9 \<close> ML \<open>
14.10 (*OLD* ) let
14.11 (*OLD*) val p' =
14.12 @@ -582,7 +582,7 @@
14.13 "~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,a,v,S,_), m), t)
14.14 = (ya, ((E, l @ [Celem.R], a,v,S,b),ss), e);
14.15 \<close> ML \<open>
14.16 - val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr E a v t (*of*);
14.17 + val (a', Celem.STac stac) = (*case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
14.18 \<close> ML \<open>
14.19 val Lucin.NotAss = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
14.20 \<close> ML \<open>