1.1 --- a/src/sml/ME/script.sml Wed Sep 06 08:44:45 2006 +0200
1.2 +++ b/src/sml/ME/script.sml Wed Sep 06 10:03:22 2006 +0200
1.3 @@ -318,7 +318,7 @@
1.4 (*WN020526: not clear, when a is available in ass_up for eva-_true*)
1.5 (*WN060906: in "fun handle_leaf" eg. uses "Some M__"(from some PREVIOUS
1.6 curried Rewrite) for CURRENT value (which may be different from PREVIOUS);
1.7 - thus "None" must be set in ????????????????????????????????????*)
1.8 + thus "None" must be set at the end of currying (ill designed anyway)*)
1.9 fun upd_env_opt env (Some a, v) = upd_env env (a,v)
1.10 | upd_env_opt env (None, v) =
1.11 (writeln("*** upd_env_opt: (None,"^(term2str v)^")");env);
1.12 @@ -995,27 +995,28 @@
1.13 handling a leaf comprises
1.14 (1) 'subst_stacexpr' substitute env and complete curried tactic
1.15 (2) rewrite the leaf by 'srls'
1.16 +WN060906 quick and dirty fix: return a' too (for updating E later)
1.17 .*)
1.18 fun handle_leaf call thy srls E a v t =
1.19 (*WN050916 'upd_env_opt' is a blind copy from previous version*)
1.20 case subst_stacexpr E a v t of
1.21 - STac stac => (*script-tactic*)
1.22 + (a', STac stac) => (*script-tactic*)
1.23 let val stac' = eval_listexpr_ (assoc_thy thy) srls
1.24 (subst_atomic (upd_env_opt E (a,v)) stac)
1.25 in (if (!trace_script)
1.26 then writeln ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^
1.27 term2str stac'^"'")
1.28 else ();
1.29 - STac stac')
1.30 + (a', STac stac'))
1.31 end
1.32 - | Expr lexpr => (*leaf-expression*)
1.33 + | (a', Expr lexpr) => (*leaf-expression*)
1.34 let val lexpr' = eval_listexpr_ (assoc_thy thy) srls
1.35 (subst_atomic (upd_env_opt E (a,v)) lexpr)
1.36 in (if (!trace_script)
1.37 then writeln("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^
1.38 term2str lexpr'^"'")
1.39 else ();
1.40 - Expr lexpr')
1.41 + (a', Expr lexpr'))
1.42 end;
1.43
1.44
1.45 @@ -1166,17 +1167,17 @@
1.46 writeln("### assy, is= ");
1.47 writeln(istate2str (ScrState is));*)
1.48 case handle_leaf "locate" thy' sr E a v t of
1.49 - Expr s =>
1.50 + (a', Expr s) =>
1.51 ((*writeln("### assy: listexpr t= "^(term2str t));
1.52 writeln("### assy, E= "^(env2str E));
1.53 writeln("### assy, eval(..)= "^(term2str
1.54 (eval_listexpr_ (assoc_thy thy') sr
1.55 - (subst_atomic (upd_env_opt E (a,v)) t))));*)
1.56 + (subst_atomic (upd_env_opt E (a',v)) t))));*)
1.57 NasNap (eval_listexpr_ (assoc_thy thy') sr
1.58 - (subst_atomic (upd_env_opt E (a,v)) t), E))
1.59 - (* val STac stac = subst_stacexpr E a v t;
1.60 + (subst_atomic (upd_env_opt E (a',v)) t), E))
1.61 + (* val (_,STac stac) = subst_stacexpr E a v t;
1.62 *)
1.63 - | STac stac =>
1.64 + | (a', STac stac) =>
1.65 let (*val _=writeln("### assy, stac = "^term2str stac);*)
1.66 val p' = case p_ of Frm => p | Res => lev_on p
1.67 | _ => raise error ("assy: call by "^
1.68 @@ -1186,12 +1187,12 @@
1.69 let (*val _=writeln("### assy: Ass ("^tac_2str m^",
1.70 "^term2str v'^")");*)
1.71 val (p'',c',f',pt') = generate1 (assoc_thy thy') m
1.72 - (ScrState (E,l,a,v',S,true)) (p',p_) pt;
1.73 - in Assoc ((E,l,a,v',S,true), (m,f',pt',p'',c @ c')::ss) end
1.74 + (ScrState (E,l,a',v',S,true)) (p',p_) pt;
1.75 + in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
1.76 | AssWeak (m,v') =>
1.77 let val (p'',c',f',pt') = generate1 (assoc_thy thy') m
1.78 - (ScrState (E,l,a,v',S,false)) (p',p_) pt;
1.79 - in Assoc ((E,l,a,v',S,false), (m,f',pt',p'',c @ c')::ss) end
1.80 + (ScrState (E,l,a',v',S,false)) (p',p_) pt;
1.81 + in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
1.82 | NotAss =>
1.83 ((*writeln("### assy, NotAss");*)
1.84 case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
1.85 @@ -1199,7 +1200,7 @@
1.86 | gen => (case applicable_in (p,p_) pt
1.87 (stac2tac pt (assoc_thy thy') stac) of
1.88 Appl m' =>
1.89 - let val is = (E,l,a,tac_2res m',S,false(*FIXXXME*))
1.90 + let val is = (E,l,a',tac_2res m',S,false(*FIXXXME*))
1.91 val (p'',c',f',pt') =
1.92 generate1 (assoc_thy thy') m' (ScrState is) (p',p_) pt;
1.93 in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
1.94 @@ -1645,26 +1646,25 @@
1.95 val (thy as (th,sr),(pt, p),E, l, t, a, v) =
1.96 (thy, ptp, E,(l@[R]), e, a, v);
1.97 *)
1.98 - ((*case subst_stacexpr E a v t of*)
1.99 - case handle_leaf "next " th sr E a v t of
1.100 -(* val Expr s = handle_leaf "next " th sr E a v t;
1.101 + (case handle_leaf "next " th sr E a v t of
1.102 +(* val (a', Expr s) = handle_leaf "next " th sr E a v t;
1.103 *)
1.104 - Expr s => Skip (s, E)
1.105 -(* val STac stac = handle_leaf "next " th sr E a v t;
1.106 + (a', Expr s) => Skip (s, E)
1.107 +(* val (a', STac stac) = handle_leaf "next " th sr E a v t;
1.108 *)
1.109 - | STac stac =>
1.110 + | (a', STac stac) =>
1.111 let
1.112 (*val _= writeln("### appy t, vor stac2tac_ is=");
1.113 - val _= writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.114 + val _= writeln(istate2str (ScrState (E,l,a',v,Sundef,false)));*)
1.115 val (m,m') = stac2tac_ pt (assoc_thy th) stac
1.116 in case m of
1.117 - Subproblem _ => Appy (m', (E,l,a,tac_2res m',Sundef,false))
1.118 + Subproblem _ => Appy (m', (E,l,a',tac_2res m',Sundef,false))
1.119 | _ => (case applicable_in p pt m of
1.120 (* val Appl m' = applicable_in p pt m;
1.121 *)
1.122 Appl m' =>
1.123 ((*writeln("### appy: Appy");*)
1.124 - Appy (m', (E,l,a,tac_2res m',Sundef,false)))
1.125 + Appy (m', (E,l,a',tac_2res m',Sundef,false)))
1.126 | _ => ((*writeln("### appy: Napp");*)Napp E))
1.127 end);
1.128
1.129 @@ -2002,13 +2002,13 @@
1.130 else metID
1.131 val {scr=Script sc,srls,...} = get_met metID'
1.132 val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_);
1.133 - in map ((stac2tac pt thy) o rep_stacexpr o
1.134 + in map ((stac2tac pt thy) o rep_stacexpr o #2 o
1.135 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) end;
1.136 (*
1.137 > val Script sc = (#scr o get_met) ("SqRoot.thy","sqrt-equ-test");
1.138 > val env = [((term_of o the o (parse Isac.thy)) "bdv",
1.139 (term_of o the o (parse Isac.thy)) "x")];
1.140 -> map ((stac2tac pt thy) o (subst_stacexpr env None e_term)) (stacpbls sc);
1.141 +> map ((stac2tac pt thy) o #2 o(subst_stacexpr env None e_term)) (stacpbls sc);
1.142 *)
1.143
1.144
2.1 --- a/src/sml/Scripts/scrtools.sml Wed Sep 06 08:44:45 2006 +0200
2.2 +++ b/src/sml/Scripts/scrtools.sml Wed Sep 06 10:03:22 2006 +0200
2.3 @@ -182,77 +182,80 @@
2.4 a leaf is either a tactic or an 'exp' in 'let v = expr'
2.5 where 'exp' does not contain a tactic.
2.6 CAUTION: (1) currying with @@ requires 2 patterns for each tactic
2.7 - (2) non-matching patterns become an Expr by fall-through.
2.8 -.*)
2.9 + (2) the non-curried version must return None for a
2.10 + (3) non-matching patterns become an Expr by fall-through.
2.11 +WN060906 quick and dirty fix: due to (2) a is returned, too.*)
2.12 fun subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _ ))=
2.13 - STac (subst_atomic E t)
2.14 + (None, STac (subst_atomic E t))
2.15
2.16 | subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _ ))=
2.17 - STac (case a of Some a' => (subst_atomic E (t $ a'))
2.18 - | None => ((subst_atomic E t) $ v))
2.19 + (a, (*in these cases we hope, that a = Some _*)
2.20 + STac (case a of Some a' => (subst_atomic E (t $ a'))
2.21 + | None => ((subst_atomic E t) $ v)))
2.22
2.23 | subst_stacexpr E a v
2.24 (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ _ )) =
2.25 - STac (subst_atomic E t)
2.26 + (None, STac (subst_atomic E t))
2.27
2.28 | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _))=
2.29 - STac (case a of Some a' => subst_atomic E (t $ a')
2.30 - | None => ((subst_atomic E t) $ v))
2.31 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
2.32 + | None => ((subst_atomic E t) $ v)))
2.33
2.34 | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ _ ))=
2.35 - STac (subst_atomic E t)
2.36 + (None, STac (subst_atomic E t))
2.37
2.38 | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set",_) $ _ $ _ )) =
2.39 - STac (case a of Some a' => subst_atomic E (t $ a')
2.40 - | None => ((subst_atomic E t) $ v))
2.41 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
2.42 + | None => ((subst_atomic E t) $ v)))
2.43
2.44 | subst_stacexpr E a v
2.45 (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ _ )) =
2.46 - STac (subst_atomic E t)
2.47 + (None, STac (subst_atomic E t))
2.48
2.49 | subst_stacexpr E a v
2.50 (t as (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ )) =
2.51 - STac (case a of Some a' => subst_atomic E (t $ a')
2.52 - | None => ((subst_atomic E t) $ v))
2.53 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
2.54 + | None => ((subst_atomic E t) $ v)))
2.55
2.56 | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ $ _ )) =
2.57 - STac (subst_atomic E t)
2.58 + (None, STac (subst_atomic E t))
2.59
2.60 | subst_stacexpr E a v (t as (Const ("Script.Calculate",_) $ _ )) =
2.61 - STac (case a of Some a' => subst_atomic E (t $ a')
2.62 - | None => ((subst_atomic E t) $ v))
2.63 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
2.64 + | None => ((subst_atomic E t) $ v)))
2.65
2.66 | subst_stacexpr E a v
2.67 (t as (Const("Script.Check'_elementwise",_) $ _ $ _ )) =
2.68 - STac (subst_atomic E t)
2.69 + (None, STac (subst_atomic E t))
2.70
2.71 | subst_stacexpr E a v (t as (Const("Script.Check'_elementwise",_) $ _ )) =
2.72 - STac (case a of Some a' => subst_atomic E (t $ a')
2.73 - | None => ((subst_atomic E t) $ v))
2.74 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
2.75 + | None => ((subst_atomic E t) $ v)))
2.76
2.77 | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_) $ _ )) =
2.78 - STac (subst_atomic E t)
2.79 + (None, STac (subst_atomic E t))
2.80
2.81 | subst_stacexpr E a v (t as (Const("Script.Or'_to'_List",_))) = (*t $ v*)
2.82 - STac (case a of Some a' => subst_atomic E (t $ a')
2.83 - | None => ((subst_atomic E t) $ v))
2.84 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
2.85 + | None => ((subst_atomic E t) $ v)))
2.86
2.87 | subst_stacexpr E a v (t as (Const ("Script.SubProblem",_) $ _ $ _ )) =
2.88 - STac (subst_atomic E t)
2.89 + (None, STac (subst_atomic E t))
2.90
2.91 | subst_stacexpr E a v (t as (Const ("Script.Take",_) $ _ )) =
2.92 - STac (subst_atomic E t)
2.93 + (None, STac (subst_atomic E t))
2.94
2.95 | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ $ _ )) =
2.96 - STac (subst_atomic E t)
2.97 + (None, STac (subst_atomic E t))
2.98
2.99 | subst_stacexpr E a v (t as (Const ("Script.Substitute",_) $ _ )) =
2.100 - STac (case a of Some a' => subst_atomic E (t $ a')
2.101 - | None => ((subst_atomic E t) $ v))
2.102 + (a, STac (case a of Some a' => subst_atomic E (t $ a')
2.103 + | None => ((subst_atomic E t) $ v)))
2.104
2.105 (*now all tactics are matched out and this leaf must be without a tactic*)
2.106 | subst_stacexpr E a v t =
2.107 - Expr (subst_atomic (case a of Some a => upd_env E (a,v) | None => E) t);
2.108 + (a, Expr (subst_atomic (case a of Some a => upd_env E (a,v)
2.109 + | None => E) t));
2.110 (*> val t = str2term "SubProblem(Test_, [linear, univariate, equation, test], [Test, solve_linear]) [bool_ e_, real_ v_]";
2.111 > subst_stacexpr [] None e_term t;*)
2.112
2.113 @@ -277,7 +280,7 @@
2.114 | scan ts (Const ("Script.Seq",_) $e1 $ e2) =
2.115 (scan ts e1) @ (scan ts e2)
2.116 | scan ts t = case subst_stacexpr [] None e_term t of
2.117 - STac _ => [t] | Expr _ => []
2.118 + (_, STac _) => [t] | (_, Expr _) => []
2.119 in (distinct o (scan [])) body end;
2.120 (*sc = Solve_root_equation ...
2.121 > val ts = stacpbls sc;
3.1 --- a/src/smltest/IsacKnowledge/biegel-test-stimmen2.sml Wed Sep 06 08:44:45 2006 +0200
3.2 +++ b/src/smltest/IsacKnowledge/biegel-test-stimmen2.sml Wed Sep 06 10:03:22 2006 +0200
3.3 @@ -122,6 +122,8 @@
3.4 val (ttt, _) = vvv;
3.5 term2str ttt;
3.6
3.7 +trace_script := true;
3.8 +
3.9 val ScrState (E,l,a,XXX,YYY,b) = get_istate pt (p,p_);
3.10 (*val a = Some (str2term "B__::bool"); (*!!!!!!!!!!!!!!!!!!!vvv is M__*)*)
3.11 val a = None;