1.1 --- a/src/Tools/isac/Build_Isac.thy Thu Aug 22 15:56:48 2019 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Thu Aug 22 16:48:04 2019 +0200
1.3 @@ -23,8 +23,8 @@
1.4 ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
1.5 ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
1.6 theory Tools imports ListC begin
1.7 - theory Script imports Tools begin
1.8 - theory Atools imports Descript Script
1.9 + theory Program imports Tools begin
1.10 + theory Atools imports Descript Program
1.11 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
1.12 theory ProgLang imports Atools
1.13 *) "ProgLang/ProgLang"
2.1 --- a/src/Tools/isac/Interpret/appl.sml Thu Aug 22 15:56:48 2019 +0200
2.2 +++ b/src/Tools/isac/Interpret/appl.sml Thu Aug 22 16:48:04 2019 +0200
2.3 @@ -76,13 +76,13 @@
2.4 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*)
2.5 fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (Rule.e_term, [])
2.6 | mk_set _ pt p (Const ("Tools.UniversalList", _)) pred =
2.7 - (Rule.e_term, if pred <> Const ("Script.Assumptions", HOLogic.boolT)
2.8 + (Rule.e_term, if pred <> Const ("Program.Assumptions", HOLogic.boolT)
2.9 then [pred]
2.10 else get_assumptions_ pt (p, Res))
2.11 | mk_set _ pt p (Const ("List.list.Cons",_) $ eq $ _) pred =
2.12 let
2.13 val (bdv,_) = HOLogic.dest_eq eq;
2.14 - val pred = if pred <> Const ("Script.Assumptions", HOLogic.boolT)
2.15 + val pred = if pred <> Const ("Program.Assumptions", HOLogic.boolT)
2.16 then [pred]
2.17 else get_assumptions_ pt (p, Res)
2.18 in (bdv, pred) end
3.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Aug 22 15:56:48 2019 +0200
3.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Aug 22 16:48:04 2019 +0200
3.3 @@ -115,11 +115,11 @@
3.4 let val E' = LTool.upd_env E (Free (i,T), res);
3.5 in appy thy ptp E' (l @ [Celem.R, Celem.D]) b a v end
3.6 | ay => ay)
3.7 - | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*1*),_) $ c $ e $ a) _ v =
3.8 + | appy (thy as (th,sr)) ptp E l (Const ("Program.While"(*1*),_) $ c $ e $ a) _ v =
3.9 (if Rewrite.eval_true_ th sr (subst_atomic (LTool.upd_env E (a,v)) c)
3.10 then appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v
3.11 else Skip (v, E))
3.12 - | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*2*),_) $ c $ e) a v =
3.13 + | appy (thy as (th,sr)) ptp E l (Const ("Program.While"(*2*),_) $ c $ e) a v =
3.14 (if Rewrite.eval_true_ th sr (subst_atomic (Lucin.upd_env_opt E (a,v)) c)
3.15 then appy thy ptp E (l @ [Celem.R]) e a v
3.16 else Skip (v, E))
3.17 @@ -127,30 +127,30 @@
3.18 (if Rewrite.eval_true_ th sr (subst_atomic (Lucin.upd_env_opt E (a,v)) c)
3.19 then appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v
3.20 else appy thy ptp E (l @ [Celem.R]) e2 a v)
3.21 - | appy thy ptp E l (Const ("Script.Repeat"(*1*),_) $ e $ a) _ v =
3.22 + | appy thy ptp E l (Const ("Program.Repeat"(*1*),_) $ e $ a) _ v =
3.23 appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v
3.24 - | appy thy ptp E l (Const ("Script.Repeat"(*2*),_) $ e) a v = appy thy ptp E (l @ [Celem.R]) e a v
3.25 - | appy thy ptp E l (Const ("Script.Try"(*2*),_) $ e $ a) _ v =
3.26 + | appy thy ptp E l (Const ("Program.Repeat"(*2*),_) $ e) a v = appy thy ptp E (l @ [Celem.R]) e a v
3.27 + | appy thy ptp E l (Const ("Program.Try"(*2*),_) $ e $ a) _ v =
3.28 (case appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v of
3.29 Napp E => (Skip (v, E))
3.30 | ay => ay)
3.31 - | appy thy ptp E l(Const ("Script.Try"(*1*),_) $ e) a v =
3.32 + | appy thy ptp E l(Const ("Program.Try"(*1*),_) $ e) a v =
3.33 (case appy thy ptp E (l @ [Celem.R]) e a v of
3.34 Napp E => (Skip (v, E))
3.35 | ay => ay)
3.36 - | appy thy ptp E l (Const ("Script.Or"(*1*),_) $e1 $ e2 $ a) _ v =
3.37 + | appy thy ptp E l (Const ("Program.Or"(*1*),_) $e1 $ e2 $ a) _ v =
3.38 (case appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v of
3.39 Appy lme => Appy lme
3.40 | _ => appy thy ptp E (*LTool.env*) (l @ [Celem.L, Celem.R]) e2 (SOME a) v)
3.41 - | appy thy ptp E l (Const ("Script.Or"(*2*),_) $e1 $ e2) a v =
3.42 + | appy thy ptp E l (Const ("Program.Or"(*2*),_) $e1 $ e2) a v =
3.43 (case appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v of
3.44 Appy lme => Appy lme
3.45 | _ => appy thy ptp E (l @ [Celem.R]) e2 a v)
3.46 - | appy thy ptp E l (Const ("Script.Seq"(*2*),_) $ e1 $ e2 $ a) _ v =
3.47 + | appy thy ptp E l (Const ("Program.Seq"(*2*),_) $ e1 $ e2 $ a) _ v =
3.48 (case appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v of
3.49 Skip (v,E) => appy thy ptp E (l @ [Celem.L, Celem.R]) e2 (SOME a) v
3.50 | ay => ay)
3.51 - | appy thy ptp E l (Const ("Script.Seq"(*1*),_) $ e1 $ e2) a v =
3.52 + | appy thy ptp E l (Const ("Program.Seq"(*1*),_) $ e1 $ e2) a v =
3.53 (case appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v of
3.54 Skip (v,E) => appy thy ptp E (l @ [Celem.R]) e2 a v
3.55 | ay => ay)
3.56 @@ -190,7 +190,7 @@
3.57 | nxt_up thy ptp scr E l ay (Const ("HOL.Let",_) $ _ $ (Abs _)) a v =
3.58 nstep_up thy ptp scr E l ay a v
3.59 (*no appy_: never causes Napp -> Helpless*)
3.60 - | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*1*), _) $ c $ e $ _) a v =
3.61 + | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Program.While"(*1*), _) $ c $ e $ _) a v =
3.62 if Rewrite.eval_true_ th sr (subst_atomic (Lucin.upd_env_opt E (a, v)) c)
3.63 then case appy thy ptp E (l @ [Celem.L, Celem.R]) e a v of
3.64 Appy lr => Appy lr
3.65 @@ -198,7 +198,7 @@
3.66 | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
3.67 else nstep_up thy ptp scr E l Skip_ a v
3.68 (*no appy_: never causes Napp - Helpless*)
3.69 - | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*2*), _) $ c $ e) a v =
3.70 + | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Program.While"(*2*), _) $ c $ e) a v =
3.71 if Rewrite.eval_true_ th sr (subst_atomic (Lucin.upd_env_opt E (a, v)) c)
3.72 then case appy thy ptp E (l @ [Celem.R]) e a v of
3.73 Appy lr => Appy lr
3.74 @@ -207,40 +207,40 @@
3.75 else nstep_up thy ptp scr E l Skip_ a v
3.76 | nxt_up thy ptp scr E l ay (Const ("If", _) $ _ $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
3.77 | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
3.78 - (Const ("Script.Repeat"(*1*), _) $ e $ _) a v =
3.79 + (Const ("Program.Repeat"(*1*), _) $ e $ _) a v =
3.80 (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [Celem.L, Celem.R]) e a v of
3.81 Appy lr => Appy lr
3.82 | Napp E => nstep_up thy ptp scr E l Skip_ a v
3.83 | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v)
3.84 | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
3.85 - (Const ("Script.Repeat"(*2*), _) $ e) a v =
3.86 + (Const ("Program.Repeat"(*2*), _) $ e) a v =
3.87 (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [Celem.R]) e a v of
3.88 Appy lr => Appy lr
3.89 | Napp E => nstep_up thy ptp scr E l Skip_ a v
3.90 | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v)
3.91 - | nxt_up thy ptp scr E l _ (Const ("Script.Try"(*2*),_) $ _ $ _) a v = (*makes Napp to Skip*)
3.92 + | nxt_up thy ptp scr E l _ (Const ("Program.Try"(*2*),_) $ _ $ _) a v = (*makes Napp to Skip*)
3.93 nstep_up thy ptp scr E l Skip_ a v
3.94
3.95 - | nxt_up thy ptp scr E l _ (Const ("Script.Try"(*1*), _) $ _) a v = (*makes Napp to Skip*)
3.96 + | nxt_up thy ptp scr E l _ (Const ("Program.Try"(*1*), _) $ _) a v = (*makes Napp to Skip*)
3.97 nstep_up thy ptp scr E l Skip_ a v
3.98 - | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _ $ _) a v =
3.99 + | nxt_up thy ptp scr E l ay (Const ("Program.Or",_) $ _ $ _ $ _) a v =
3.100 nstep_up thy ptp scr E l ay a v
3.101 - | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
3.102 - | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ ) a v =
3.103 + | nxt_up thy ptp scr E l ay (Const ("Program.Or",_) $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
3.104 + | nxt_up thy ptp scr E l ay (Const ("Program.Or",_) $ _ ) a v =
3.105 nstep_up thy ptp scr E (drop_last l) ay a v
3.106 - | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*1*), _) $ _ $ _ $ _) a v =
3.107 + | nxt_up thy ptp scr E l ay (Const ("Program.Seq"(*1*), _) $ _ $ _ $ _) a v =
3.108 (*all has been done in (*2*) below*) nstep_up thy ptp scr E l ay a v
3.109 - | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*2*), _) $ _ $ _) a v = (*comes from e2*)
3.110 + | nxt_up thy ptp scr E l ay (Const ("Program.Seq"(*2*), _) $ _ $ _) a v = (*comes from e2*)
3.111 nstep_up thy ptp scr E l ay a v
3.112 - | nxt_up thy ptp (scr as Rule.Prog sc) E l ay (Const ("Script.Seq"(*3*),_) $ _) a v = (*comes from e1*)
3.113 + | nxt_up thy ptp (scr as Rule.Prog sc) E l ay (Const ("Program.Seq"(*3*),_) $ _) a v = (*comes from e1*)
3.114 if ay = Napp_
3.115 then nstep_up thy ptp scr E (drop_last l) Napp_ a v
3.116 else (*Skip_*)
3.117 let val up = drop_last l;
3.118 val e2 =
3.119 (case go up sc of
3.120 - Const ("Script.Seq"(*2*), _) $ _ $ e2 => e2
3.121 - | t => error ("nxt_up..Script.Seq $ _ with " ^ Rule.term2str t))
3.122 + Const ("Program.Seq"(*2*), _) $ _ $ e2 => e2
3.123 + | t => error ("nxt_up..Program.Seq $ _ with " ^ Rule.term2str t))
3.124 in case appy thy ptp E (up @ [Celem.R]) e2 a v of
3.125 Appy lr => Appy lr
3.126 | Napp E => nstep_up thy ptp scr E up Napp_ a v
3.127 @@ -356,11 +356,11 @@
3.128 val E' = LTool.upd_env E (id', v);
3.129 in assy ya ((E', l @ [Celem.R, Celem.D], a,v,S,b),ss) body end
3.130 | ay => ay)
3.131 - | assy (ya as (ctxt,srls,_,_)) ((E,l,_,v,S,b),ss) (Const ("Script.While",_) $ c $ e $ a) =
3.132 + | assy (ya as (ctxt,srls,_,_)) ((E,l,_,v,S,b),ss) (Const ("Program.While",_) $ c $ e $ a) =
3.133 if Rewrite.eval_true_ "Isac" srls (subst_atomic (LTool.upd_env E (a,v)) c)
3.134 then assy ya ((E, l @ [Celem.L, Celem.R], SOME a,v,S,b),ss) e
3.135 else NasNap (v, E)
3.136 - | assy (ya as (ctxt,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("Script.While",_) $ c $ e) =
3.137 + | assy (ya as (ctxt,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("Program.While",_) $ c $ e) =
3.138 if Rewrite.eval_true_ "Isac" srls (subst_atomic (Lucin.upd_env_opt E (a,v)) c)
3.139 then assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e
3.140 else NasNap (v, E)
3.141 @@ -368,25 +368,25 @@
3.142 if Rewrite.eval_true_ "Isac" srls (subst_atomic (Lucin.upd_env_opt E (a,v)) c)
3.143 then assy ya ((E, l @ [Celem.L, Celem.R], a,v,S,b),ss) e1
3.144 else assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e2
3.145 - | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Try"(*2*),_) $ e $ a) =
3.146 + | assy ya ((E,l,_,v,S,b),ss) (Const ("Program.Try"(*2*),_) $ e $ a) =
3.147 (case assy ya ((E, l @ [Celem.L, Celem.R], SOME a,v,S,b),ss) e of ay => ay)
3.148 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try"(*1*),_) $ e) =
3.149 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Program.Try"(*1*),_) $ e) =
3.150 (case assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e of ay => ay)
3.151 - | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Seq"(*2*),_) $e1 $ e2 $ a) =
3.152 + | assy ya ((E,l,_,v,S,b),ss) (Const ("Program.Seq"(*2*),_) $e1 $ e2 $ a) =
3.153 (case assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss) e1 of
3.154 NasNap (v, E) => assy ya ((E, l @ [Celem.L, Celem.R], SOME a,v,S,b),ss) e2
3.155 | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l @ [Celem.L, Celem.R], SOME a,v,S,b),ss) e2
3.156 | ay => ay)
3.157 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Seq"(*1*),_) $e1 $ e2) =
3.158 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Program.Seq"(*1*),_) $e1 $ e2) =
3.159 (case assy ya ((E, l @ [Celem.L, Celem.R], a,v,S,b),ss) e1 of
3.160 NasNap (v, E) => assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e2
3.161 | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e2
3.162 | ay => ay)
3.163 - | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Repeat",_) $ e $ a) =
3.164 + | assy ya ((E,l,_,v,S,b),ss) (Const ("Program.Repeat",_) $ e $ a) =
3.165 assy ya ((E,(l @ [Celem.L, Celem.R]),SOME a,v,S,b),ss) e
3.166 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Repeat",_) $ e) =
3.167 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Program.Repeat",_) $ e) =
3.168 assy ya ((E,(l @ [Celem.R]),a,v,S,b),ss) e
3.169 - | assy ((*y,*)x,s,sc,Aundef) ((E,l,_,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2 $ a) =
3.170 + | assy ((*y,*)x,s,sc,Aundef) ((E,l,_,v,S,b),ss) (Const ("Program.Or",_) $e1 $ e2 $ a) =
3.171 (case assy ((*y,*)x,s,sc,AssOnly) ((E,(l @ [Celem.L, Celem.L, Celem.R]),SOME a,v,S,b),ss) e1 of
3.172 NasNap (v, E) =>
3.173 (case assy ((*y,*)x,s,sc,AssOnly) ((E,(l @ [Celem.L, Celem.R]),SOME a,v,S,b),ss) e2 of
3.174 @@ -398,7 +398,7 @@
3.175 | ay =>ay)
3.176 | NasApp _ => error ("assy: FIXXXME ///must not return NasApp///")
3.177 | ay => (ay))
3.178 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2) =
3.179 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Program.Or",_) $e1 $ e2) =
3.180 (case assy ya ((E, (l @ [Celem.L, Celem.R]),a,v,S,b), ss) e1 of
3.181 NasNap (v, E) => assy ya ((E,(l @ [Celem.R]),a,v,S,b), ss) e2
3.182 | ay => (ay))
3.183 @@ -458,29 +458,29 @@
3.184 end
3.185 | ass_up ys iss (Abs (_,_,_)) = astep_up ys iss (*TODO 5.9.00: LTool.env ?*)
3.186 | ass_up ys iss (Const ("HOL.Let",_) $ _ $ (Abs _)) = astep_up ys iss (*TODO 5.9.00: LTool.env ?*)
3.187 - | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) =
3.188 + | ass_up ysa iss (Const ("Program.Seq",_) $ _ $ _ $ _) =
3.189 astep_up ysa iss (*all has been done in (*2*) below*)
3.190 - | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =
3.191 + | ass_up ysa iss (Const ("Program.Seq",_) $ _ $ _) =
3.192 astep_up ysa iss (*2*: comes from e2*)
3.193
3.194 | ass_up (ysa as ((*y,*)ctxt,s,Rule.Prog sc,d)) ((E,l,a,v,S,b),ss)
3.195 - (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)
3.196 + (Const ("Program.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)
3.197 let
3.198 val up = drop_last l;
3.199 val e2 =
3.200 (case go up sc of
3.201 - Const ("Script.Seq",_) $ _ $ e2 => e2
3.202 - | t => error ("ass_up..Script.Seq $ _ with " ^ Rule.term2str t))
3.203 + Const ("Program.Seq",_) $ _ $ e2 => e2
3.204 + | t => error ("ass_up..Program.Seq $ _ with " ^ Rule.term2str t))
3.205 in case assy ((*y,*)ctxt,s,d,Aundef) ((E, up @ [Celem.R], a,v,S,b),ss) e2 of
3.206 NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss)
3.207 | NasApp iss => astep_up ysa iss
3.208 | ay => ay
3.209 end
3.210 - | ass_up ysa iss (Const ("Script.Try"(*2*),_) $ _ $ _) = astep_up ysa iss
3.211 - | ass_up ysa iss (Const ("Script.Try"(*1*),_) $ _) = astep_up ysa iss
3.212 + | ass_up ysa iss (Const ("Program.Try"(*2*),_) $ _ $ _) = astep_up ysa iss
3.213 + | ass_up ysa iss (Const ("Program.Try"(*1*),_) $ _) = astep_up ysa iss
3.214 | ass_up (ys as ((*y,*)ctxt,s,_,d)) ((E,l,_,v,S,b),ss)
3.215 - (*(Const ("Script.While",_) $ c $ e $ a) = WN050930 blind fix*)
3.216 - (t as Const ("Script.While",_) $ c $ e $ a) =
3.217 + (*(Const ("Program.While",_) $ c $ e $ a) = WN050930 blind fix*)
3.218 + (t as Const ("Program.While",_) $ c $ e $ a) =
3.219 if Rewrite.eval_true_ "Isac" s (subst_atomic (LTool.upd_env E (a,v)) c)
3.220 then case assy ((*y,*)ctxt,s,d,Aundef) ((E, l @ [Celem.L, Celem.R], SOME a,v,S,b),ss) e of
3.221 NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
3.222 @@ -489,8 +489,8 @@
3.223 | ay => ay
3.224 else astep_up ys ((E,l, SOME a,v,S,b),ss)
3.225 | ass_up (ys as ((*y,*)ctxt,s,_,d)) ((E,l,a,v,S,b),ss)
3.226 - (*(Const ("Script.While",_) $ c $ e) = WN050930 blind fix*)
3.227 - (t as Const ("Script.While",_) $ c $ e) =
3.228 + (*(Const ("Program.While",_) $ c $ e) = WN050930 blind fix*)
3.229 + (t as Const ("Program.While",_) $ c $ e) =
3.230 if Rewrite.eval_true_ "Isac" s (subst_atomic (Lucin.upd_env_opt E (a,v)) c)
3.231 then case assy ((*y,*)ctxt,s,d,Aundef) ((E, l @ [Celem.R], a,v,S,b),ss) e of
3.232 NasNap (v,E') => astep_up ys ((E',l, a,v,S,b),ss)
3.233 @@ -500,21 +500,21 @@
3.234 else astep_up ys ((E,l, a,v,S,b),ss)
3.235 | ass_up y iss (Const ("If",_) $ _ $ _ $ _) = astep_up y iss
3.236 | ass_up (ys as ((*y,*)ctxt,s,_,d)) ((E,l,_,v,S,b),ss)
3.237 - (t as Const ("Script.Repeat",_) $ e $ a) =
3.238 + (t as Const ("Program.Repeat",_) $ e $ a) =
3.239 (case assy ((*y,*)ctxt,s,d, Aundef) ((E, (l @ [Celem.L, Celem.R]), SOME a,v,S,b),ss) e of
3.240 NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
3.241 | NasApp ((E',l,a,v,S,b),ss) =>
3.242 ass_up ys ((E',l,a,v,S,b),ss) t
3.243 | ay => ay)
3.244 | ass_up (ys as ((*y,*)ctxt,s,_,d)) ((E,l,a,v,S,b),ss)
3.245 - (t as Const ("Script.Repeat",_) $ e) =
3.246 + (t as Const ("Program.Repeat",_) $ e) =
3.247 (case assy ((*y,*)ctxt,s,d,Aundef) ((E, (l @ [Celem.R]), a,v,S,b),ss) e of
3.248 NasNap (v', E') => astep_up ys ((E',l,a,v',S,b),ss)
3.249 | NasApp ((E',l,a,v',S,_),ss) => ass_up ys ((E',l,a,v',S,b),ss) t
3.250 | ay => ay)
3.251 - | ass_up y iss (Const ("Script.Or",_) $ _ $ _ $ _) = astep_up y iss
3.252 - | ass_up y iss (Const ("Script.Or",_) $ _ $ _) = astep_up y iss
3.253 - | ass_up y ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $ _ ) =
3.254 + | ass_up y iss (Const ("Program.Or",_) $ _ $ _ $ _) = astep_up y iss
3.255 + | ass_up y iss (Const ("Program.Or",_) $ _ $ _) = astep_up y iss
3.256 + | ass_up y ((E,l,a,v,S,b),ss) (Const ("Program.Or",_) $ _ ) =
3.257 astep_up y ((E, (drop_last l), a,v,S,b),ss)
3.258 | ass_up _ _ t =
3.259 error ("ass_up not impl for t= " ^ Rule.term2str t)
4.1 --- a/src/Tools/isac/Interpret/model.sml Thu Aug 22 15:56:48 2019 +0200
4.2 +++ b/src/Tools/isac/Interpret/model.sml Thu Aug 22 16:48:04 2019 +0200
4.3 @@ -108,7 +108,7 @@
4.4 (b)
4.5 ==========================================================================*)
4.6
4.7 -val script_parse = the o (@{theory Script} |> Rule.thy2ctxt |> TermC.parseNEW);
4.8 +val script_parse = the o (@{theory Program} |> Rule.thy2ctxt |> TermC.parseNEW);
4.9 val e_listReal = script_parse "[]::(real list)";
4.10 val e_listBool = script_parse "[]::(bool list)";
4.11
4.12 @@ -233,7 +233,7 @@
4.13 [] => error ("penv_value: no values in '" ^ Rule.term2str id)
4.14 | [v] => (id, v)
4.15 | (v1 :: v2 :: _) => (case v1 of
4.16 - Const ("Script.Arbfix",_) => (id, v2)
4.17 + Const ("Program.Arbfix",_) => (id, v2)
4.18 | _ => (id, v1));
4.19
4.20 (* 9.5.03: still unused, but left for eventual future development *)
5.1 --- a/src/Tools/isac/Interpret/script.sml Thu Aug 22 15:56:48 2019 +0200
5.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Aug 22 16:48:04 2019 +0200
5.3 @@ -103,21 +103,21 @@
5.4 (*.get argument of first stactic in a script for init_form.*)
5.5 fun get_stac thy (_ $ body) =
5.6 let
5.7 - fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a =
5.8 + fun get_t y (Const ("Program.Seq",_) $ e1 $ e2) a =
5.9 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
5.10 - | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ =
5.11 + | get_t y (Const ("Program.Seq",_) $ e1 $ e2 $ a) _ =
5.12 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
5.13 - | get_t y (Const ("Script.Try",_) $ e) a = get_t y e a
5.14 - | get_t y (Const ("Script.Try",_) $ e $ a) _ = get_t y e a
5.15 - | get_t y (Const ("Script.Repeat",_) $ e) a = get_t y e a
5.16 - | get_t y (Const ("Script.Repeat",_) $ e $ a) _ = get_t y e a
5.17 - | get_t y (Const ("Script.Or",_) $e1 $ e2) a =
5.18 + | get_t y (Const ("Program.Try",_) $ e) a = get_t y e a
5.19 + | get_t y (Const ("Program.Try",_) $ e $ a) _ = get_t y e a
5.20 + | get_t y (Const ("Program.Repeat",_) $ e) a = get_t y e a
5.21 + | get_t y (Const ("Program.Repeat",_) $ e $ a) _ = get_t y e a
5.22 + | get_t y (Const ("Program.Or",_) $e1 $ e2) a =
5.23 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
5.24 - | get_t y (Const ("Script.Or",_) $e1 $ e2 $ a) _ =
5.25 + | get_t y (Const ("Program.Or",_) $e1 $ e2 $ a) _ =
5.26 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
5.27 - | get_t y (Const ("Script.While",_) $ _ $ e) a = get_t y e a
5.28 - | get_t y (Const ("Script.While",_) $ _ $ e $ a) _ = get_t y e a
5.29 - | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_, _, e2)) a =
5.30 + | get_t y (Const ("Program.While",_) $ _ $ e) a = get_t y e a
5.31 + | get_t y (Const ("Program.While",_) $ _ $ e $ a) _ = get_t y e a
5.32 + | get_t y (Const ("Program.Letpar",_) $ e1 $ Abs (_, _, e2)) a =
5.33 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
5.34 (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
5.35 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
5.36 @@ -127,21 +127,21 @@
5.37 | get_t _ (Const ("If", _) $ _ $ _ $ _) _ = NONE
5.38 (*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*)
5.39
5.40 - | get_t _ (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a
5.41 - | get_t _ (Const ("Script.Rewrite",_) $ _ $ _ ) a = SOME a
5.42 - | get_t _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
5.43 - | get_t _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a
5.44 - | get_t _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ = SOME a
5.45 - | get_t _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ ) a = SOME a
5.46 - | get_t _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
5.47 - | get_t _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a
5.48 - | get_t _ (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a
5.49 - | get_t _ (Const ("Script.Calculate",_) $ _ ) a = SOME a
5.50 + | get_t _ (Const ("Program.Rewrite",_) $ _ $ _ $ a) _ = SOME a
5.51 + | get_t _ (Const ("Program.Rewrite",_) $ _ $ _ ) a = SOME a
5.52 + | get_t _ (Const ("Program.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
5.53 + | get_t _ (Const ("Program.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a
5.54 + | get_t _ (Const ("Program.Rewrite'_Set",_) $ _ $ _ $ a) _ = SOME a
5.55 + | get_t _ (Const ("Program.Rewrite'_Set",_) $ _ $ _ ) a = SOME a
5.56 + | get_t _ (Const ("Program.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
5.57 + | get_t _ (Const ("Program.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a
5.58 + | get_t _ (Const ("Program.Calculate",_) $ _ $ a) _ = SOME a
5.59 + | get_t _ (Const ("Program.Calculate",_) $ _ ) a = SOME a
5.60
5.61 - | get_t _ (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a
5.62 - | get_t _ (Const ("Script.Substitute",_) $ _ ) a = SOME a
5.63 + | get_t _ (Const ("Program.Substitute",_) $ _ $ a) _ = SOME a
5.64 + | get_t _ (Const ("Program.Substitute",_) $ _ ) a = SOME a
5.65
5.66 - | get_t _ (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE
5.67 + | get_t _ (Const ("Program.SubProblem",_) $ _ $ _) _ = NONE
5.68
5.69 | get_t _ _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
5.70 in get_t thy body Rule.e_term end
5.71 @@ -186,33 +186,33 @@
5.72 in (flat o (map (itm2arg itms))) pats end;
5.73
5.74 (* convert a script-tac 'stac' to 'tac' for users;
5.75 - for "Script.SubProblem" also create a 'tac_' for internal use. FIXME separate?
5.76 + for "Program.SubProblem" also create a 'tac_' for internal use. FIXME separate?
5.77 if stac is an initac, then convert to a 'tac_' (as required in appy).
5.78 arg ctree for pushing the thy specified in rootpbl into subpbls *)
5.79 -fun stac2tac_ _ thy (Const ("Script.Rewrite", _) $ thmID $ _ $ _) =
5.80 +fun stac2tac_ _ thy (Const ("Program.Rewrite", _) $ thmID $ _ $ _) =
5.81 let
5.82 val tid = HOLogic.dest_string thmID
5.83 in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid), Tactic.Empty_Tac_) end
5.84 - | stac2tac_ _ thy (Const ("Script.Rewrite'_Inst", _) $ sub $ thmID $ _ $ _) =
5.85 + | stac2tac_ _ thy (Const ("Program.Rewrite'_Inst", _) $ sub $ thmID $ _ $ _) =
5.86 let
5.87 val tid = HOLogic.dest_string thmID
5.88 in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid)), Tactic.Empty_Tac_) end
5.89 - | stac2tac_ _ _ (Const ("Script.Rewrite'_Set",_) $ rls $ _ $ _) =
5.90 + | stac2tac_ _ _ (Const ("Program.Rewrite'_Set",_) $ rls $ _ $ _) =
5.91 (Tactic.Rewrite_Set (HOLogic.dest_string rls), Tactic.Empty_Tac_)
5.92 - | stac2tac_ _ _ (Const ("Script.Rewrite'_Set'_Inst", _) $ sub $ rls $ _ $ _) =
5.93 + | stac2tac_ _ _ (Const ("Program.Rewrite'_Set'_Inst", _) $ sub $ rls $ _ $ _) =
5.94 (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls), Tactic.Empty_Tac_)
5.95 - | stac2tac_ _ _ (Const ("Script.Calculate", _) $ op_ $ _) =
5.96 + | stac2tac_ _ _ (Const ("Program.Calculate", _) $ op_ $ _) =
5.97 (Tactic.Calculate (HOLogic.dest_string op_), Tactic.Empty_Tac_)
5.98 - | stac2tac_ _ _ (Const ("Script.Take", _) $ t) = (Tactic.Take (Rule.term2str t), Tactic.Empty_Tac_)
5.99 - | stac2tac_ _ _ (Const ("Script.Substitute", _) $ isasub $ _) =
5.100 + | stac2tac_ _ _ (Const ("Program.Take", _) $ t) = (Tactic.Take (Rule.term2str t), Tactic.Empty_Tac_)
5.101 + | stac2tac_ _ _ (Const ("Program.Substitute", _) $ isasub $ _) =
5.102 (Tactic.Substitute ((Selem.subte2sube o TermC.isalist2list) isasub), Tactic.Empty_Tac_)
5.103 - | stac2tac_ _ thy (Const("Script.Check'_elementwise", _) $ _ $
5.104 + | stac2tac_ _ thy (Const("Program.Check'_elementwise", _) $ _ $
5.105 (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
5.106 (Tactic.Check_elementwise (Rule.term_to_string''' thy pred), Tactic.Empty_Tac_)
5.107 - | stac2tac_ _ _ (Const("Script.Or'_to'_List", _) $ _ ) = (Tactic.Or_to_List, Tactic.Empty_Tac_)
5.108 + | stac2tac_ _ _ (Const("Program.Or'_to'_List", _) $ _ ) = (Tactic.Or_to_List, Tactic.Empty_Tac_)
5.109
5.110 (*compare "| associate _ (Subproblem'" ..TODO: extract common code *)
5.111 - | stac2tac_ pt _ (stac as Const ("Script.SubProblem", _) $ spec' $ ags') =
5.112 + | stac2tac_ pt _ (stac as Const ("Program.SubProblem", _) $ spec' $ ags') =
5.113 let
5.114 val (dI, pI, mI) = LTool.dest_spec spec'
5.115 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
5.116 @@ -277,14 +277,14 @@
5.117 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
5.118 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
5.119 (case stac of
5.120 - (Const ("Script.Rewrite'_Inst", _) $ _ $ thmID_ $ _ $ f_) =>
5.121 + (Const ("Program.Rewrite'_Inst", _) $ _ $ thmID_ $ _ $ f_) =>
5.122 if thmID = HOLogic.dest_string thmID_
5.123 then
5.124 if f = f_
5.125 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
5.126 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
5.127 else ((*tracing"3### associate ..NotAss";*) NotAss)
5.128 - | (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ _ $ f_) =>
5.129 + | (Const ("Program.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ _ $ f_) =>
5.130 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
5.131 then if f = f_ then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
5.132 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
5.133 @@ -292,14 +292,14 @@
5.134 | _ => NotAss)
5.135 | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
5.136 (case stac of
5.137 - (Const ("Script.Rewrite", _) $ thmID_ $ _ $ f_) =>
5.138 + (Const ("Program.Rewrite", _) $ thmID_ $ _ $ f_) =>
5.139 if thmID = HOLogic.dest_string thmID_
5.140 then
5.141 if f = f_
5.142 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
5.143 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
5.144 else NotAss
5.145 - | (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_) =>
5.146 + | (Const ("Program.Rewrite'_Set", _) $ rls_ $ _ $ f_) =>
5.147 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
5.148 then
5.149 if f = f_
5.150 @@ -308,7 +308,7 @@
5.151 else NotAss
5.152 | _ => NotAss)
5.153 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
5.154 - (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_)) =
5.155 + (Const ("Program.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_)) =
5.156 if Rule.id_rls rls = HOLogic.dest_string rls_
5.157 then
5.158 if f = f_
5.159 @@ -316,7 +316,7 @@
5.160 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
5.161 else NotAss
5.162 | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
5.163 - (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_)) =
5.164 + (Const ("Program.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_)) =
5.165 if Rule.id_rls rls = HOLogic.dest_string rls_
5.166 then
5.167 if f = f_
5.168 @@ -324,7 +324,7 @@
5.169 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
5.170 else NotAss
5.171 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
5.172 - (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_)) =
5.173 + (Const ("Program.Rewrite'_Set", _) $ rls_ $ _ $ f_)) =
5.174 if Rule.id_rls rls = HOLogic.dest_string rls_
5.175 then
5.176 if f = f_
5.177 @@ -332,7 +332,7 @@
5.178 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
5.179 else NotAss
5.180 | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
5.181 - (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_)) =
5.182 + (Const ("Program.Rewrite'_Set", _) $ rls_ $ _ $ f_)) =
5.183 if Rule.id_rls rls = HOLogic.dest_string rls_
5.184 then
5.185 if f = f_
5.186 @@ -341,14 +341,14 @@
5.187 else NotAss
5.188 | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
5.189 (case stac of
5.190 - (Const ("Script.Calculate",_) $ op__ $ f_) =>
5.191 + (Const ("Program.Calculate",_) $ op__ $ f_) =>
5.192 if op_ = HOLogic.dest_string op__
5.193 then
5.194 if f = f_
5.195 then Ass (m, f', ctxt)
5.196 else Ass_Weak (m ,f', ctxt)
5.197 else NotAss
5.198 - | (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_) =>
5.199 + | (Const ("Program.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_) =>
5.200 let val thy = Celem.assoc_thy "Isac";
5.201 in
5.202 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
5.203 @@ -359,7 +359,7 @@
5.204 else Ass_Weak (m ,f', ctxt)
5.205 else NotAss
5.206 end
5.207 - | (Const ("Script.Rewrite'_Set",_) $ rls_ $ _ $ f_) =>
5.208 + | (Const ("Program.Rewrite'_Set",_) $ rls_ $ _ $ f_) =>
5.209 let val thy = Celem.assoc_thy "Isac";
5.210 in
5.211 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
5.212 @@ -372,15 +372,15 @@
5.213 end
5.214 | _ => NotAss)
5.215 | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
5.216 - (Const ("Script.Check'_elementwise",_) $ consts' $ _)) =
5.217 + (Const ("Program.Check'_elementwise",_) $ consts' $ _)) =
5.218 if consts = consts'
5.219 then Ass (m, consts_chkd, ctxt)
5.220 else NotAss
5.221 - | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Script.Or'_to'_List", _) $ _)) =
5.222 + | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Program.Or'_to'_List", _) $ _)) =
5.223 Ass (m, list, ctxt)
5.224 - | associate _ ctxt (m as Tactic.Take' term, (Const ("Script.Take", _) $ _)) = Ass (m, term, ctxt)
5.225 + | associate _ ctxt (m as Tactic.Take' term, (Const ("Program.Take", _) $ _)) = Ass (m, term, ctxt)
5.226 | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'),
5.227 - (Const ("Script.Substitute", _) $ _ $ t)) =
5.228 + (Const ("Program.Substitute", _) $ _ $ t)) =
5.229 if f = t then Ass (m, f', ctxt)
5.230 else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
5.231 if foldl and_ (true, map TermC.contains_Var subte)
5.232 @@ -393,9 +393,9 @@
5.233 SOME (t', _) => Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
5.234 | NONE => error "associate: Substitute' not applicable to val of Expr")
5.235
5.236 - (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)" ..TODO: extract common code *)
5.237 + (*compare "| stac2tac_ thy (Const ("Program.SubProblem",_)" ..TODO: extract common code *)
5.238 | associate pt _ (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
5.239 - (stac as Const ("Script.SubProblem", _) $ spec' $ ags')) =
5.240 + (stac as Const ("Program.SubProblem", _) $ spec' $ ags')) =
5.241 let
5.242 val (dI, pI, mI) = LTool.dest_spec spec'
5.243 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
5.244 @@ -479,14 +479,14 @@
5.245 val subs' = Selem.subst_to_subst' subs;
5.246 val sT' = type_of subs';
5.247 val fT = type_of f;
5.248 - val lhs = Const ("Script.Rewrite'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
5.249 + val lhs = Const ("Program.Rewrite'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
5.250 $ subs' $ HOLogic.mk_string thmID $ b $ f;
5.251 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
5.252 | rep_tac_ (Tactic.Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
5.253 let
5.254 val fT = type_of f;
5.255 val b = if put then @{term True} else @{term False};
5.256 - val lhs = Const ("Script.Rewrite", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
5.257 + val lhs = Const ("Program.Rewrite", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
5.258 $ HOLogic.mk_string thmID $ b $ f;
5.259 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
5.260 | rep_tac_ (Tactic.Rewrite_Set_Inst' (thy', _, subs, rls, f, (f', _))) =
5.261 @@ -495,20 +495,20 @@
5.262 val subs' = Selem.subst_to_subst' subs;
5.263 val sT' = type_of subs';
5.264 val fT = type_of f;
5.265 - val lhs = Const ("Script.Rewrite'_Set'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
5.266 + val lhs = Const ("Program.Rewrite'_Set'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
5.267 $ subs' $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
5.268 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
5.269 | rep_tac_ (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) =
5.270 let
5.271 val fT = type_of f;
5.272 val b = if put then @{term True} else @{term False};
5.273 - val lhs = Const ("Script.Rewrite'_Set", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
5.274 + val lhs = Const ("Program.Rewrite'_Set", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
5.275 $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
5.276 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
5.277 | rep_tac_ (Tactic.Calculate' (thy', op_, f, (f', _)))=
5.278 let
5.279 val fT = type_of f;
5.280 - val lhs = Const ("Script.Calculate",[HOLogic.stringT,fT] ---> fT) $ HOLogic.mk_string op_ $ f
5.281 + val lhs = Const ("Program.Calculate",[HOLogic.stringT,fT] ---> fT) $ HOLogic.mk_string op_ $ f
5.282 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
5.283 | rep_tac_ (Tactic.Check_elementwise' (_, _, (t', _))) = (Rule.Erule, (Rule.e_term, t'))
5.284 | rep_tac_ (Tactic.Subproblem' (_, _, _, _, _, t')) = (Rule.Erule, (Rule.e_term, t'))
6.1 --- a/src/Tools/isac/Interpret/solve.sml Thu Aug 22 15:56:48 2019 +0200
6.2 +++ b/src/Tools/isac/Interpret/solve.sml Thu Aug 22 16:48:04 2019 +0200
6.3 @@ -133,7 +133,7 @@
6.4 in ("ok",([(Tactic.Apply_Method mI, Tactic.Apply_Method' (mI, SOME t, is, ctxt),
6.5 ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos)))
6.6 end
6.7 - | NONE => (*execute the first tac in the Script, compare solve m*)
6.8 + | NONE => (*execute the first tac in the Program, compare solve m*)
6.9 let
6.10 val (m', (is', ctxt'), _) = LucinNEW.determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
6.11 in
7.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Aug 22 15:56:48 2019 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Aug 22 16:48:04 2019 +0200
7.3 @@ -36,7 +36,7 @@
7.4
7.5 val knowthys' = (*["Isac", .., "Descript", "Delete"]*)
7.6 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys');
7.7 - val progthys' = (*["Script", "Tools", "ListC", "KEStore"]*)
7.8 + val progthys' = (*["Program", "Tools", "ListC", "KEStore"]*)
7.9 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys');
7.10 \<close>
7.11
8.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Thu Aug 22 15:56:48 2019 +0200
8.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Thu Aug 22 16:48:04 2019 +0200
8.3 @@ -1,6 +1,6 @@
8.4 (*8.01: alte Scripts f"ur Extremwertaufgabe gesammelt*)
8.5
8.6 -(* Das erste Script aus dem Maximum-Beispiel.
8.7 +(* Das erste Program aus dem Maximum-Beispiel.
8.8 parse erzeugt aus dem string 's' den
8.9 'cterm 's' im Isabelle-Format (pretty-printing !)*)
8.10
8.11 @@ -43,7 +43,7 @@
8.12 ML> ...
8.13 ML> val c = (the o (parse thy)) s;
8.14 val c =
8.15 - "Script maximum =
8.16 + "Program maximum =
8.17 Input [Bool f_ix, Real m_, BoolList r_s, Real v_v, RealSet itv_, Bool err_]
8.18 Local [Bool e_e, Real t_, Real mx_, RealList v_s]
8.19 Tacs [SEQU
8.20 @@ -63,7 +63,7 @@
8.21 ML> ...
8.22 ML> val c = (the o (parse thy)) s;
8.23 val c =
8.24 - "Script make_fun_by_new_variable =
8.25 + "Program make_fun_by_new_variable =
8.26 Input [Real f_f, Real v_v, BoolList eqs]
8.27 Local [Bool h_, BoolList es_, RealList v_s, Real v1_, Real v2_, Bool e1,
8.28 Bool e2_, BoolList s_1, BoolList s_2]
8.29 @@ -83,7 +83,7 @@
8.30 ML> ...
8.31 ML> val c = (the o (parse thy)) s;
8.32 val c =
8.33 - "Script make_fun_explicit =
8.34 + "Program make_fun_explicit =
8.35 Input [Real f_f, Real v_v, BoolList eqs]
8.36 Local [Bool h_, Bool eq_, RealList v_s, Real v1_, BoolList ss_]
8.37 Tacs [SEQU
9.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Thu Aug 22 15:56:48 2019 +0200
9.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Thu Aug 22 16:48:04 2019 +0200
9.3 @@ -315,7 +315,7 @@
9.4 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
9.5 "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"];
9.6 val (dI',pI',mI')=
9.7 - ("DiffAppl",["Script","maximum_of","function"],Celem.e_metID);
9.8 + ("DiffAppl",["Program","maximum_of","function"],Celem.e_metID);
9.9 val c = []:cid;
9.10
9.11 (*
10.1 --- a/src/Tools/isac/Knowledge/DiffApp.sml Thu Aug 22 15:56:48 2019 +0200
10.2 +++ b/src/Tools/isac/Knowledge/DiffApp.sml Thu Aug 22 16:48:04 2019 +0200
10.3 @@ -6,7 +6,7 @@
10.4
10.5 (*
10.6 > get_pbt ["DiffAppl","maximum_of","function"];
10.7 -> get_met ("Script","max_on_interval_by_calculus");
10.8 +> get_met ("Program","max_on_interval_by_calculus");
10.9 > !pbltypes;
10.10 *)
10.11 pbltypes:= overwritel (!pbltypes,
11.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Aug 22 15:56:48 2019 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Aug 22 16:48:04 2019 +0200
11.3 @@ -161,7 +161,7 @@
11.4 [["simplification","of_rationals","to_partial_fraction"]]))]\<close>
11.5
11.6 subsection \<open>Method\<close>
11.7 -text \<open>rule set for functions called in the Script\<close>
11.8 +text \<open>rule set for functions called in the Program\<close>
11.9 ML \<open>
11.10 val srls_partial_fraction = Rule.Rls {id="srls_partial_fraction",
11.11 preconds = [],
12.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Aug 22 15:56:48 2019 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Aug 22 16:48:04 2019 +0200
12.3 @@ -759,7 +759,7 @@
12.4 Rule.Calc ("Atools.pow", eval_binop "#power_")
12.5 ],
12.6 scr = Rule.EmptyScr
12.7 -(*Script ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)
12.8 +(*Program ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)
12.9 };
12.10 \<close>
12.11 setup \<open>KEStore_Elems.add_rlss
13.1 --- a/src/Tools/isac/ProgLang/Atools.thy Thu Aug 22 15:56:48 2019 +0200
13.2 +++ b/src/Tools/isac/ProgLang/Atools.thy Thu Aug 22 16:48:04 2019 +0200
13.3 @@ -3,7 +3,7 @@
13.4 (c) due to copyright terms
13.5 *)
13.6
13.7 -theory Atools imports Descript Script
13.8 +theory Atools imports Descript Program
13.9 begin
13.10
13.11 subsection \<open>preparation to build up a program from rules\<close>
13.12 @@ -96,7 +96,7 @@
13.13 \item [elements of a key] into the hierarchy of problems or methods must not contain capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
13.14 \item [descriptions in problem-patterns] must contain at least 1 capital letter and must not contain underscores, e.g. {\tt Probe, forPolynomials}.
13.15 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus beware of conflicts~!
13.16 -\item [script identifiers] always end with {\tt Script}, e.g. {\tt ProbeScript}.
13.17 +\item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.
13.18 \item [???] ???
13.19 \item [???] ???
13.20 \end{description}
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/Tools/isac/ProgLang/Program.thy Thu Aug 22 16:48:04 2019 +0200
14.3 @@ -0,0 +1,89 @@
14.4 +(* Title: tactics, tacticals etc. for scripts
14.5 + Author: Walther Neuper 000224
14.6 + (c) due to copyright terms
14.7 + *)
14.8 +
14.9 +theory Program imports Tools begin
14.10 +
14.11 +typedecl
14.12 + arg (* argument of subproblem *)
14.13 +
14.14 +consts
14.15 +
14.16 +(*types of subproblems' arguments*)
14.17 + REAL :: "real => arg"
14.18 + REAL_LIST :: "(real list) => arg"
14.19 + REAL_SET :: "(real set) => arg"
14.20 + BOOL :: "bool => arg"
14.21 + BOOL_LIST :: "(bool list) => arg"
14.22 + REAL_REAL :: "(real => real) => arg"
14.23 + STRING :: "(char list) => arg"
14.24 + STRING_LIST :: "(char list list) => arg"
14.25 +
14.26 +(*tactics*)
14.27 + Rewrite :: "[char list, bool, 'a] => 'a"
14.28 + Rewrite'_Inst:: "[(char list * real) list, char list, bool, 'a] => 'a"
14.29 + ("(Rewrite'_Inst (_ _ _))" 11)
14.30 + (*without last argument ^^ for @@*)
14.31 + Rewrite'_Set :: "[char list, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11)
14.32 + Rewrite'_Set'_Inst
14.33 + :: "[((char list) * real) list, char list, bool, 'a] => 'a"
14.34 + ("(Rewrite'_Set'_Inst (_ _ _))" 11)
14.35 + (*without last argument ^^ for @@*)
14.36 + Calculate :: "[char list, 'a] => 'a" (*WN100816 PLUS, TIMES, POWER miss.in scr*)
14.37 + Calculate1 :: "[char list, 'a] => 'a" (*FIXXXME: unknown to script-interpreter*)
14.38 +
14.39 + (* WN0509 substitution now is rewriting by a list of terms (of type bool)
14.40 + Substitute :: "[(real * real) list, 'a] => 'a"*)
14.41 + Substitute :: "[bool list, 'a] => 'a"
14.42 +
14.43 + Map :: "['a => 'b, 'a list] => 'b list"
14.44 + Check'_elementwise ::
14.45 + "['a list, 'b set] => 'a list"
14.46 + ("Check'_elementwise (_ _)" 11)
14.47 + Take :: "'a => 'a" (*for non-var args as long as no 'o'*)
14.48 + SubProblem :: "[char list * char list list * char list list, arg list] => 'a"
14.49 +
14.50 + Or'_to'_List :: "bool => 'a list" ("Or'_to'_List (_)" 11)
14.51 + (*=========== record these ^^^ in 'tacs' in Program.ML =========*)
14.52 +
14.53 + Assumptions :: bool
14.54 + Problem :: "[char list * char list list] => 'a"
14.55 +
14.56 +(*special formulas for frontend 'CAS format'*)
14.57 + Subproblem :: "(char list * char list list) => 'a"
14.58 +
14.59 +(*script-expressions (tacticals)*)
14.60 + Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10) (*@ used*)
14.61 + Try :: "['a => 'a, 'a] => 'a"
14.62 + Repeat :: "['a => 'a, 'a] => 'a"
14.63 + Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)
14.64 + While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9)
14.65 +(*WN100723 because of "Error in syntax translation" below...
14.66 + (*'b => bool doesn't work with "contains_root _"*)
14.67 + Letpar :: "['a, 'a => 'b] => 'b"
14.68 + (*--- defined in Isabelle/scr/HOL/HOL.thy:
14.69 + Let :: "['a, 'a => 'b] => 'b"
14.70 + "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
14.71 + If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
14.72 + %x. P x .. lambda is defined in Isabelles meta logic
14.73 + --- *)
14.74 +*)
14.75 + failtac :: 'a
14.76 + idletac :: 'a
14.77 + (*... + RECORD IN 'screxpr' in Program.ML *)
14.78 +
14.79 +(*Makarius 10.03
14.80 +syntax
14.81 +
14.82 + "_Letpar" :: "[letbinds, 'a] => 'a" ("(letpar (_)/ in (_))" 10)
14.83 +
14.84 +translations
14.85 +
14.86 + "_Letpar (_binds b bs) e" == "_Letpar b (_Letpar bs e)"
14.87 + "letpar x = a in e" == "Letpar a (%x. e)"
14.88 +*** Error in syntax translation rule: rhs contains extra variables
14.89 +*** ("_Letpar" ("_bind" x a) e) -> (Letpar a ("_abs" x e))
14.90 +*** At command "translations" (line 140 of "/usr/local/isabisac/src/Pure/isac/Scripts/Program").
14.91 +*)
14.92 +end
15.1 --- a/src/Tools/isac/ProgLang/Script.thy Thu Aug 22 15:56:48 2019 +0200
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,89 +0,0 @@
15.4 -(* Title: tactics, tacticals etc. for scripts
15.5 - Author: Walther Neuper 000224
15.6 - (c) due to copyright terms
15.7 - *)
15.8 -
15.9 -theory Script imports Tools begin
15.10 -
15.11 -typedecl
15.12 - arg (* argument of subproblem *)
15.13 -
15.14 -consts
15.15 -
15.16 -(*types of subproblems' arguments*)
15.17 - REAL :: "real => arg"
15.18 - REAL_LIST :: "(real list) => arg"
15.19 - REAL_SET :: "(real set) => arg"
15.20 - BOOL :: "bool => arg"
15.21 - BOOL_LIST :: "(bool list) => arg"
15.22 - REAL_REAL :: "(real => real) => arg"
15.23 - STRING :: "(char list) => arg"
15.24 - STRING_LIST :: "(char list list) => arg"
15.25 -
15.26 -(*tactics*)
15.27 - Rewrite :: "[char list, bool, 'a] => 'a"
15.28 - Rewrite'_Inst:: "[(char list * real) list, char list, bool, 'a] => 'a"
15.29 - ("(Rewrite'_Inst (_ _ _))" 11)
15.30 - (*without last argument ^^ for @@*)
15.31 - Rewrite'_Set :: "[char list, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11)
15.32 - Rewrite'_Set'_Inst
15.33 - :: "[((char list) * real) list, char list, bool, 'a] => 'a"
15.34 - ("(Rewrite'_Set'_Inst (_ _ _))" 11)
15.35 - (*without last argument ^^ for @@*)
15.36 - Calculate :: "[char list, 'a] => 'a" (*WN100816 PLUS, TIMES, POWER miss.in scr*)
15.37 - Calculate1 :: "[char list, 'a] => 'a" (*FIXXXME: unknown to script-interpreter*)
15.38 -
15.39 - (* WN0509 substitution now is rewriting by a list of terms (of type bool)
15.40 - Substitute :: "[(real * real) list, 'a] => 'a"*)
15.41 - Substitute :: "[bool list, 'a] => 'a"
15.42 -
15.43 - Map :: "['a => 'b, 'a list] => 'b list"
15.44 - Check'_elementwise ::
15.45 - "['a list, 'b set] => 'a list"
15.46 - ("Check'_elementwise (_ _)" 11)
15.47 - Take :: "'a => 'a" (*for non-var args as long as no 'o'*)
15.48 - SubProblem :: "[char list * char list list * char list list, arg list] => 'a"
15.49 -
15.50 - Or'_to'_List :: "bool => 'a list" ("Or'_to'_List (_)" 11)
15.51 - (*=========== record these ^^^ in 'tacs' in Script.ML =========*)
15.52 -
15.53 - Assumptions :: bool
15.54 - Problem :: "[char list * char list list] => 'a"
15.55 -
15.56 -(*special formulas for frontend 'CAS format'*)
15.57 - Subproblem :: "(char list * char list list) => 'a"
15.58 -
15.59 -(*script-expressions (tacticals)*)
15.60 - Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10) (*@ used*)
15.61 - Try :: "['a => 'a, 'a] => 'a"
15.62 - Repeat :: "['a => 'a, 'a] => 'a"
15.63 - Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)
15.64 - While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9)
15.65 -(*WN100723 because of "Error in syntax translation" below...
15.66 - (*'b => bool doesn't work with "contains_root _"*)
15.67 - Letpar :: "['a, 'a => 'b] => 'b"
15.68 - (*--- defined in Isabelle/scr/HOL/HOL.thy:
15.69 - Let :: "['a, 'a => 'b] => 'b"
15.70 - "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
15.71 - If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
15.72 - %x. P x .. lambda is defined in Isabelles meta logic
15.73 - --- *)
15.74 -*)
15.75 - failtac :: 'a
15.76 - idletac :: 'a
15.77 - (*... + RECORD IN 'screxpr' in Script.ML *)
15.78 -
15.79 -(*Makarius 10.03
15.80 -syntax
15.81 -
15.82 - "_Letpar" :: "[letbinds, 'a] => 'a" ("(letpar (_)/ in (_))" 10)
15.83 -
15.84 -translations
15.85 -
15.86 - "_Letpar (_binds b bs) e" == "_Letpar b (_Letpar bs e)"
15.87 - "letpar x = a in e" == "Letpar a (%x. e)"
15.88 -*** Error in syntax translation rule: rhs contains extra variables
15.89 -*** ("_Letpar" ("_bind" x a) e) -> (Letpar a ("_abs" x e))
15.90 -*** At command "translations" (line 140 of "/usr/local/isabisac/src/Pure/isac/Scripts/Script").
15.91 -*)
15.92 -end
16.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Thu Aug 22 15:56:48 2019 +0200
16.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Thu Aug 22 16:48:04 2019 +0200
16.3 @@ -1,4 +1,4 @@
16.4 -(* tools which depend on Script.thy and thus are not in termC.sml
16.5 +(* tools which depend on Program.thy and thus are not in termC.sml
16.6 author: Walther Neuper 2000
16.7 (c) copyright due to lincense terms.
16.8 *)
16.9 @@ -85,11 +85,11 @@
16.10
16.11
16.12 (* make the term 'Subproblem (domID, pblID)' to a formula for frontend;
16.13 - needs to be here after def. Subproblem in Script.thy *)
16.14 -val subpbl_t $ (pair_t $ _ $ _) = (Thm.term_of o the o (TermC.parse @{theory Script}))
16.15 + needs to be here after def. Subproblem in Program.thy *)
16.16 +val subpbl_t $ (pair_t $ _ $ _) = (Thm.term_of o the o (TermC.parse @{theory Program}))
16.17 "Subproblem (''Isac'',[''equation'',''univar''])"
16.18 val pbl_t $ _ =
16.19 - (Thm.term_of o the o (TermC.parse @{theory Script})) "Problem (''Isac'',[''equation'',''univar''])"
16.20 + (Thm.term_of o the o (TermC.parse @{theory Program})) "Problem (''Isac'',[''equation'',''univar''])"
16.21
16.22 fun subpbl domID pblID =
16.23 subpbl_t $ (pair_t $ HOLogic.mk_string domID $
16.24 @@ -152,53 +152,53 @@
16.25 (2) the non-curried version must return NONE for a
16.26 (3) non-matching patterns become an Expr by fall-through.
16.27 WN060906 quick and dirty fix: due to (2) a is returned, too *)
16.28 -fun subst_stacexpr E _ _ (t as (Const ("Script.Rewrite",_) $ _ $ _ $ _)) =
16.29 +fun subst_stacexpr E _ _ (t as (Const ("Program.Rewrite",_) $ _ $ _ $ _)) =
16.30 (NONE, STac (subst_atomic E t))
16.31 - | subst_stacexpr E a v (t as (Const ("Script.Rewrite",_) $ _ $ _)) =
16.32 + | subst_stacexpr E a v (t as (Const ("Program.Rewrite",_) $ _ $ _)) =
16.33 (a, (*in these cases we hope, that a = SOME _*)
16.34 STac (case a of SOME a' => (subst_atomic E (t $ a'))
16.35 | NONE => ((subst_atomic E t) $ v)))
16.36 | subst_stacexpr E _ _
16.37 - (t as (Const ("Script.Rewrite'_Inst", _) $ _ $ _ $ _ $ _)) =
16.38 + (t as (Const ("Program.Rewrite'_Inst", _) $ _ $ _ $ _ $ _)) =
16.39 (NONE, STac (subst_atomic E t))
16.40 - | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Inst", _) $ _ $ _ $ _)) =
16.41 + | subst_stacexpr E a v (t as (Const ("Program.Rewrite'_Inst", _) $ _ $ _ $ _)) =
16.42 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
16.43 | NONE => ((subst_atomic E t) $ v)))
16.44 - | subst_stacexpr E _ _ (t as (Const ("Script.Rewrite'_Set", _) $ _ $ _ $ _)) =
16.45 + | subst_stacexpr E _ _ (t as (Const ("Program.Rewrite'_Set", _) $ _ $ _ $ _)) =
16.46 (NONE, STac (subst_atomic E t))
16.47 - | subst_stacexpr E a v (t as (Const ("Script.Rewrite'_Set", _) $ _ $ _)) =
16.48 + | subst_stacexpr E a v (t as (Const ("Program.Rewrite'_Set", _) $ _ $ _)) =
16.49 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
16.50 | NONE => ((subst_atomic E t) $ v)))
16.51 | subst_stacexpr E _ _
16.52 - (t as (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ _ $ _ $ _)) =
16.53 + (t as (Const ("Program.Rewrite'_Set'_Inst", _) $ _ $ _ $ _ $ _)) =
16.54 (NONE, STac (subst_atomic E t))
16.55 | subst_stacexpr E a v
16.56 - (t as (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ _ $ _)) =
16.57 + (t as (Const ("Program.Rewrite'_Set'_Inst", _) $ _ $ _ $ _)) =
16.58 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
16.59 | NONE => ((subst_atomic E t) $ v)))
16.60 - | subst_stacexpr E _ _ (t as (Const ("Script.Calculate", _) $ _ $ _)) =
16.61 + | subst_stacexpr E _ _ (t as (Const ("Program.Calculate", _) $ _ $ _)) =
16.62 (NONE, STac (subst_atomic E t))
16.63 - | subst_stacexpr E a v (t as (Const ("Script.Calculate", _) $ _)) =
16.64 + | subst_stacexpr E a v (t as (Const ("Program.Calculate", _) $ _)) =
16.65 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
16.66 | NONE => ((subst_atomic E t) $ v)))
16.67 | subst_stacexpr E _ _
16.68 - (t as (Const ("Script.Check'_elementwise",_) $ _ $ _)) =
16.69 + (t as (Const ("Program.Check'_elementwise",_) $ _ $ _)) =
16.70 (NONE, STac (subst_atomic E t))
16.71 - | subst_stacexpr E a v (t as (Const ("Script.Check'_elementwise", _) $ _)) =
16.72 + | subst_stacexpr E a v (t as (Const ("Program.Check'_elementwise", _) $ _)) =
16.73 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
16.74 | NONE => ((subst_atomic E t) $ v)))
16.75 - | subst_stacexpr E _ _ (t as (Const ("Script.Or'_to'_List", _) $ _)) =
16.76 + | subst_stacexpr E _ _ (t as (Const ("Program.Or'_to'_List", _) $ _)) =
16.77 (NONE, STac (subst_atomic E t))
16.78 - | subst_stacexpr E a v (t as (Const ("Script.Or'_to'_List", _))) = (*t $ v*)
16.79 + | subst_stacexpr E a v (t as (Const ("Program.Or'_to'_List", _))) = (*t $ v*)
16.80 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
16.81 | NONE => ((subst_atomic E t) $ v)))
16.82 - | subst_stacexpr E _ _ (t as (Const ("Script.SubProblem", _) $ _ $ _)) =
16.83 + | subst_stacexpr E _ _ (t as (Const ("Program.SubProblem", _) $ _ $ _)) =
16.84 (NONE, STac (subst_atomic E t))
16.85 - | subst_stacexpr E _ _ (t as (Const ("Script.Take",_) $ _)) =
16.86 + | subst_stacexpr E _ _ (t as (Const ("Program.Take",_) $ _)) =
16.87 (NONE, STac (subst_atomic E t))
16.88 - | subst_stacexpr E _ _ (t as (Const ("Script.Substitute", _) $ _ $ _)) =
16.89 + | subst_stacexpr E _ _ (t as (Const ("Program.Substitute", _) $ _ $ _)) =
16.90 (NONE, STac (subst_atomic E t))
16.91 - | subst_stacexpr E a v (t as (Const ("Script.Substitute", _) $ _)) =
16.92 + | subst_stacexpr E a v (t as (Const ("Program.Substitute", _) $ _)) =
16.93 (a, STac (case a of SOME a' => subst_atomic E (t $ a')
16.94 | NONE => ((subst_atomic E t) $ v)))
16.95 (*now all tactics are matched out and this leaf must be without a tactic*)
16.96 @@ -211,27 +211,27 @@
16.97 let
16.98 fun scan (Const ("HOL.Let", _) $ e $ (Abs (_, _, b))) = (scan e) @ (scan b)
16.99 | scan (Const ("If", _) $ _ $ e1 $ e2) = (scan e1) @ (scan e2)
16.100 - | scan (Const ("Script.While", _) $ _ $ e $ _) = scan e
16.101 - | scan (Const ("Script.While", _) $ _ $ e) = scan e
16.102 - | scan (Const ("Script.Repeat", _) $ e $ _) = scan e
16.103 - | scan (Const ("Script.Repeat", _) $ e) = scan e
16.104 - | scan (Const ("Script.Try", _) $ e $ _) = scan e
16.105 - | scan (Const ("Script.Try", _) $ e) = scan e
16.106 - | scan (Const ("Script.Or", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
16.107 - | scan (Const ("Script.Or", _) $ e1 $ e2) = (scan e1) @ (scan e2)
16.108 - | scan (Const ("Script.Seq", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
16.109 - | scan (Const ("Script.Seq", _) $ e1 $ e2) = (scan e1) @ (scan e2)
16.110 + | scan (Const ("Program.While", _) $ _ $ e $ _) = scan e
16.111 + | scan (Const ("Program.While", _) $ _ $ e) = scan e
16.112 + | scan (Const ("Program.Repeat", _) $ e $ _) = scan e
16.113 + | scan (Const ("Program.Repeat", _) $ e) = scan e
16.114 + | scan (Const ("Program.Try", _) $ e $ _) = scan e
16.115 + | scan (Const ("Program.Try", _) $ e) = scan e
16.116 + | scan (Const ("Program.Or", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
16.117 + | scan (Const ("Program.Or", _) $ e1 $ e2) = (scan e1) @ (scan e2)
16.118 + | scan (Const ("Program.Seq", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
16.119 + | scan (Const ("Program.Seq", _) $ e1 $ e2) = (scan e1) @ (scan e2)
16.120 | scan t = case subst_stacexpr [] NONE Rule.e_term t of
16.121 (_, STac _) => [t] | (_, Expr _) => []
16.122 in (distinct o scan) body end
16.123 | stacpbls t = raise ERROR ("fun stacpbls not applicable to '" ^ Rule.term2str t ^ "'")
16.124
16.125 (* get operators out of a program *)
16.126 -fun is_calc (Const ("Script.Calculate",_) $ _) = true
16.127 - | is_calc (Const ("Script.Calculate",_) $ _ $ _) = true
16.128 +fun is_calc (Const ("Program.Calculate",_) $ _) = true
16.129 + | is_calc (Const ("Program.Calculate",_) $ _ $ _) = true
16.130 | is_calc _ = false;
16.131 -fun op_of_calc (Const ("Script.Calculate",_) $ op_) = HOLogic.dest_string op_
16.132 - | op_of_calc (Const ("Script.Calculate",_) $ op_ $ _) = HOLogic.dest_string op_
16.133 +fun op_of_calc (Const ("Program.Calculate",_) $ op_) = HOLogic.dest_string op_
16.134 + | op_of_calc (Const ("Program.Calculate",_) $ op_ $ _) = HOLogic.dest_string op_
16.135 | op_of_calc t = error ("op_of_calc called with " ^ Rule.term2str t);
16.136 fun get_calcs thy sc =
16.137 sc
17.1 --- a/src/Tools/isac/TODO.thy Thu Aug 22 15:56:48 2019 +0200
17.2 +++ b/src/Tools/isac/TODO.thy Thu Aug 22 16:48:04 2019 +0200
17.3 @@ -119,7 +119,7 @@
17.4 \item Test.thy: met_test_sqrt2: deleted?!
17.5 \item xxx
17.6 \item Applicable.applicable_in --> Applicable.tactic_at
17.7 - \item Const ("Script.SubProblem", _) --> Const ("Program.SubProblem", _):rename! separate?
17.8 + \item Const ("Program.SubProblem", _) --> Const ("Program.SubProblem", _):rename! separate?
17.9 \item xxx
17.10 \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
17.11 \item xxx
18.1 --- a/src/Tools/isac/calcelems.sml Thu Aug 22 15:56:48 2019 +0200
18.2 +++ b/src/Tools/isac/calcelems.sml Thu Aug 22 16:48:04 2019 +0200
18.3 @@ -191,7 +191,7 @@
18.4 # that scripts should be re-usable ? #
18.5 #############################################################################
18.6
18.7 - eg. 'Script Solve_rat_equation' calls 'SubProblem (RatEq',..'
18.8 + eg. 'Program Solve_rat_equation' calls 'SubProblem (RatEq',..'
18.9 which would not allow to 'solve (y'' = -M_b / EI, M_b)' by this script
18.10 because Biegelinie.thy is subthy of RatEq.thy and thus Biegelinie.M_b
18.11 is unknown in RatEq.thy and M_b cannot be parsed into the scripts guard
18.12 @@ -425,7 +425,7 @@
18.13
18.14 fun assoc_thy thy =
18.15 if thy = "e_domID"
18.16 - then (Rule.Thy_Info_get_theory "Script") (*lower bound of Knowledge*)
18.17 + then (Rule.Thy_Info_get_theory "Program") (*lower bound of Knowledge*)
18.18 else (Rule.Thy_Info_get_theory thy) handle _ => error ("ME_Isa: thy \"" ^ thy ^ "\" not in system");
18.19
18.20 (* overwrite an element in an association list and pair it with a thyID
19.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Thu Aug 22 15:56:48 2019 +0200
19.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Thu Aug 22 16:48:04 2019 +0200
19.3 @@ -641,7 +641,7 @@
19.4 ("name", "Specify_Problem")]), [ct])) = Tactic.Specify_Problem (xml_to_strs ct)
19.5 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
19.6
19.7 -val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Script}))
19.8 +val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Program}))
19.9 ("Problem (" ^ Rule.e_domID ^ "," ^ strs2str' Celem.e_pblID ^ ")");
19.10
19.11 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
20.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Aug 22 15:56:48 2019 +0200
20.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Aug 22 16:48:04 2019 +0200
20.3 @@ -186,7 +186,7 @@
20.4
20.5 text\<open>\noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
20.6 \normalfont and rhs means \em Right Hand Side \normalfont and indicates
20.7 - the left or the right part of an equation.} in the Script language, but
20.8 + the left or the right part of an equation.} in the Program language, but
20.9 we need a function which gets the denominator of a fraction.\<close>
20.10
20.11 subsubsection\<open>Get the Denominator and Numerator out of a Fraction\<close>
20.12 @@ -198,7 +198,7 @@
20.13 get_numerator :: "real => real"
20.14
20.15 text \<open>\noindent With the above definition we run into problems when we parse
20.16 - the Script \texttt{InverseZTransform}. This leads to \em ambiguous
20.17 + the Program \texttt{InverseZTransform}. This leads to \em ambiguous
20.18 parse trees. \normalfont We avoid this by moving the definition
20.19 to \ttfamily Rational.thy \normalfont and re-building {\sisac}.
20.20 \par \noindent ATTENTION: From now on \ttfamily
20.21 @@ -911,7 +911,7 @@
20.22
20.23 consts
20.24 InverseZTransform :: "[bool, bool] => bool"
20.25 - ("((Script InverseZTransform (_ =))// (_))" 9)
20.26 + ("((Program InverseZTransform (_ =))// (_))" 9)
20.27
20.28 subsection \<open>Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}\<close>
20.29
20.30 @@ -958,7 +958,7 @@
20.31 ("#Find", ["stepResponse n_eq"])],
20.32 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
20.33 errpats = [], nrls = e_rls},
20.34 - "Script InverseZTransform (Xeq::bool) =" ^ (*TODO boundVariable X_z*)
20.35 + "Program InverseZTransform (Xeq::bool) =" ^ (*TODO boundVariable X_z*)
20.36 " (let X = Take Xeq;" ^
20.37 " X = Rewrite ruleZY False X" ^
20.38 " in X)")]
20.39 @@ -987,7 +987,7 @@
20.40 subsection \<open>Stepwise Extend the Program\<close>
20.41 ML \<open>
20.42 val str =
20.43 - "Script InverseZTransform (Xeq::bool) = "^
20.44 + "Program InverseZTransform (Xeq::bool) = "^
20.45 " Xeq";
20.46 \<close>
20.47
20.48 @@ -996,7 +996,7 @@
20.49
20.50 ML \<open>
20.51 val str =
20.52 - "Script InverseZTransform (Xeq::bool) = "^
20.53 + "Program InverseZTransform (Xeq::bool) = "^
20.54 (*
20.55 * 1/z) instead of z ^^^ -1
20.56 *)
20.57 @@ -1013,7 +1013,7 @@
20.58 (*
20.59 * NONE
20.60 *)
20.61 - "Script InverseZTransform (Xeq::bool) = "^
20.62 + "Program InverseZTransform (Xeq::bool) = "^
20.63 (*
20.64 * (1/z) instead of z ^^^ -1
20.65 *)
20.66 @@ -1039,7 +1039,7 @@
20.67
20.68 ML \<open>
20.69 val str =
20.70 - "Script InverseZTransform (Xeq::bool) = "^
20.71 + "Program InverseZTransform (Xeq::bool) = "^
20.72 " (let X = Take Xeq; "^
20.73 " X' = Rewrite ruleZY False X; "^
20.74 " X' = (Rewrite_Set norm_Rational False) X'; "^
20.75 @@ -1054,9 +1054,9 @@
20.76 side. The equation itself consists of this denominator and tries to find
20.77 a $z$ for this the denominator is equal to zero.\<close>
20.78
20.79 -text \<open> dropped during switch from Script to partial_function:
20.80 +text \<open> dropped during switch from Program to partial_function:
20.81 val str =
20.82 - "Script InverseZTransform (X_eq::bool) = "^
20.83 + "Program InverseZTransform (X_eq::bool) = "^
20.84 " (let X = Take X_eq; "^
20.85 " X' = Rewrite ruleZY False X; "^
20.86 " X' = (Rewrite_Set norm_Rational False) X'; "^
20.87 @@ -1133,7 +1133,7 @@
20.88 ("#Find", ["stepResponse n_eq"])],
20.89 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls, prls = e_rls, crls = e_rls,
20.90 errpats = [], nrls = e_rls},
20.91 - "Script InverseZTransform (X_eq::bool) = "^
20.92 + "Program InverseZTransform (X_eq::bool) = "^
20.93 (*(1/z) instead of z ^^^ -1*)
20.94 "(let X = Take X_eq; "^
20.95 " X' = Rewrite ruleZY False X; "^
20.96 @@ -1308,7 +1308,7 @@
20.97 We see the SubProblem with correct arguments from searching next
20.98 step (program text !!!--->!!! STac (script tactic) with arguments
20.99 evaluated.)
20.100 - \item Do we have the right Script \ldots difference in the
20.101 + \item Do we have the right Program \ldots difference in the
20.102 arguments in the arguments\ldots
20.103 \begin{verbatim}
20.104 val Prog s =
20.105 @@ -1319,7 +1319,7 @@
20.106 \end{verbatim}
20.107 \ldots shows the right script. Difference in the arguments.
20.108 \item Test --- Why helpless here ? --- shows: \ttfamily replace
20.109 - no\_meth by [no\_meth] \normalfont in Script
20.110 + no\_meth by [no\_meth] \normalfont in Program
20.111 \end{itemize}
20.112 \<close>
20.113
20.114 @@ -1368,7 +1368,7 @@
20.115 \normalfont The only False is the reason: the Where (the precondition) is
20.116 False for good reasons: The precondition seems to check for linear
20.117 equations, not for the one we want to solve! Removed this error by
20.118 - correcting the Script from \ttfamily SubProblem (PolyEq',
20.119 + correcting the Program from \ttfamily SubProblem (PolyEq',
20.120 \lbrack linear,univariate,equation,
20.121 test\rbrack, \lbrack Test,solve\_linear\rbrack \normalfont to
20.122 \ttfamily SubProblem (PolyEq',\\ \lbrack abcFormula,degree\_2,
20.123 @@ -1382,7 +1382,7 @@
20.124 }
20.125 And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont
20.126 at the respective \ttfamily store\_pbt. \normalfont Or you leave the
20.127 - selection of the appropriate type to isac as done in the final Script ;-))
20.128 + selection of the appropriate type to isac as done in the final Program ;-))
20.129 \end{itemize}\<close>
20.130
20.131 ML \<open>
21.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Thu Aug 22 15:56:48 2019 +0200
21.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Thu Aug 22 16:48:04 2019 +0200
21.3 @@ -473,7 +473,7 @@
21.4 \begin{isamarkuptext}%
21.5 \noindent We have rhs\footnote{Note: lhs means \em Left Hand Side
21.6 \normalfont and rhs means \em Right Hand Side \normalfont and indicates
21.7 - the left or the right part of an equation.} in the Script language, but
21.8 + the left or the right part of an equation.} in the Program language, but
21.9 we need a function which gets the denominator of a fraction.%
21.10 \end{isamarkuptext}%
21.11 \isamarkuptrue%
21.12 @@ -493,7 +493,7 @@
21.13 \ \ get{\isaliteral{5F}{\isacharunderscore}}numerator\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}real\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ real{\isaliteral{22}{\isachardoublequoteclose}}%
21.14 \begin{isamarkuptext}%
21.15 \noindent With the above definition we run into problems when we parse
21.16 - the Script \texttt{InverseZTransform}. This leads to \em ambiguous
21.17 + the Program \texttt{InverseZTransform}. This leads to \em ambiguous
21.18 parse trees. \normalfont We avoid this by moving the definition
21.19 to \ttfamily Rational.thy \normalfont and re-building {\sisac}.
21.20 \par \noindent ATTENTION: From now on \ttfamily
21.21 @@ -1749,7 +1749,7 @@
21.22 \isacommand{consts}\isamarkupfalse%
21.23 \isanewline
21.24 \ \ InverseZTransform\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}bool{\isaliteral{2C}{\isacharcomma}}\ bool{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
21.25 -\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{9}}{\isaliteral{29}{\isacharparenright}}%
21.26 +\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Program\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{9}}{\isaliteral{29}{\isacharparenright}}%
21.27 \isamarkupsubsection{Setup Parent Nodes in Hierarchy of Method\label{sec:cparentnode}%
21.28 }
21.29 \isamarkuptrue%
21.30 @@ -1843,7 +1843,7 @@
21.31 \ \ \ \ \ {\isaliteral{7B}{\isacharbraceleft}}rew{\isaliteral{5F}{\isacharunderscore}}ord{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}tless{\isaliteral{5F}{\isacharunderscore}}true{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\ rls{\isaliteral{27}{\isacharprime}}{\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ calc\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
21.32 \ \ \ \ \ \ srls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ prls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\isanewline
21.33 \ \ \ \ \ \ crls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ nrls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
21.34 -\ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
21.35 +\ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Program\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
21.36 \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
21.37 \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{5E}{\isacharcircum}}\isanewline
21.38 \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ in\ X{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
21.39 @@ -1922,7 +1922,7 @@
21.40 \isacommand{ML}\isamarkupfalse%
21.41 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
21.42 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
21.43 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.44 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Program\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.45 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ Xeq{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
21.46 {\isaliteral{2A7D}{\isacharverbatimclose}}%
21.47 \endisatagML
21.48 @@ -1946,7 +1946,7 @@
21.49 \isacommand{ML}\isamarkupfalse%
21.50 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
21.51 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
21.52 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.53 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Program\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.54 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
21.55 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ {\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\isanewline
21.56 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
21.57 @@ -1963,7 +1963,7 @@
21.58 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
21.59 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ NONE\isanewline
21.60 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
21.61 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.62 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Program\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.63 \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\isanewline
21.64 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}\isanewline
21.65 \ \ \ \ \ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
21.66 @@ -2004,7 +2004,7 @@
21.67 \isacommand{ML}\isamarkupfalse%
21.68 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
21.69 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
21.70 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.71 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Program\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}Xeq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.72 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ Xeq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.73 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.74 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.75 @@ -2036,7 +2036,7 @@
21.76 \isacommand{ML}\isamarkupfalse%
21.77 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
21.78 \ \ val\ str\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
21.79 -\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.80 +\ \ \ \ {\isaliteral{22}{\isachardoublequote}}Program\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.81 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ {\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.82 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.83 \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Rewrite{\isaliteral{5F}{\isacharunderscore}}Set\ norm{\isaliteral{5F}{\isacharunderscore}}Rational\ False{\isaliteral{29}{\isacharparenright}}\ X{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.84 @@ -2162,7 +2162,7 @@
21.85 \ \ \ \ \ \ \ prls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\isanewline
21.86 \ \ \ \ \ \ \ crls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls{\isaliteral{2C}{\isacharcomma}}\ nrls\ {\isaliteral{3D}{\isacharequal}}\ e{\isaliteral{5F}{\isacharunderscore}}rls\isanewline
21.87 \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
21.88 -\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Script\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.89 +\ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Program\ InverseZTransform\ {\isaliteral{28}{\isacharparenleft}}X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.90 \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2F}{\isacharslash}}z{\isaliteral{29}{\isacharparenright}}\ instead\ of\ z\ {\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{5E}{\isacharcircum}}\ {\isaliteral{2D}{\isacharminus}}{\isadigit{1}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
21.91 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}let\ X\ {\isaliteral{3D}{\isacharequal}}\ Take\ X{\isaliteral{5F}{\isacharunderscore}}eq{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.92 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}\ \ \ \ \ \ X{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ Rewrite\ ruleZY\ False\ X{\isaliteral{3B}{\isacharsemicolon}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}{\isaliteral{5E}{\isacharcircum}}\isanewline
21.93 @@ -2290,7 +2290,7 @@
21.94 \ \ \ \ \ \ \ {\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5F}{\isacharunderscore}}\isanewline
21.95 \ \ \ \ \ \ {\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ prep{\isaliteral{5F}{\isacharunderscore}}ori\ fmz\ thy\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{23}{\isacharhash}}ppc\ o\ get{\isaliteral{5F}{\isacharunderscore}}pbt{\isaliteral{29}{\isacharparenright}}\ pI{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
21.96 \isanewline
21.97 -\ \ val\ Script\ sc\ \isanewline
21.98 +\ \ val\ Program\ sc\ \isanewline
21.99 \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{23}{\isacharhash}}scr\ o\ get{\isaliteral{5F}{\isacharunderscore}}met{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{22}{\isachardoublequote}}SignalProcessing{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
21.100 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}Z{\isaliteral{5F}{\isacharunderscore}}Transform{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}\isanewline
21.101 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}inverse{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
21.102 @@ -2387,7 +2387,7 @@
21.103 We see the SubProblem with correct arguments from searching next
21.104 step (program text !!!--->!!! STac (script tactic) with arguments
21.105 evaluated.)
21.106 - \item Do we have the right Script \ldots difference in the
21.107 + \item Do we have the right Program \ldots difference in the
21.108 arguments in the arguments\ldots
21.109 \begin{verbatim}
21.110 val Prog s =
21.111 @@ -2398,7 +2398,7 @@
21.112 \end{verbatim}
21.113 \ldots shows the right script. Difference in the arguments.
21.114 \item Test --- Why helpless here ? --- shows: \ttfamily replace
21.115 - no\_meth by [no\_meth] \normalfont in Script
21.116 + no\_meth by [no\_meth] \normalfont in Program
21.117 \end{itemize}%
21.118 \end{isamarkuptext}%
21.119 \isamarkuptrue%
21.120 @@ -2476,7 +2476,7 @@
21.121 \normalfont The only False is the reason: the Where (the precondition) is
21.122 False for good reasons: The precondition seems to check for linear
21.123 equations, not for the one we want to solve! Removed this error by
21.124 - correcting the Script from \ttfamily SubProblem (PolyEq',
21.125 + correcting the Program from \ttfamily SubProblem (PolyEq',
21.126 \lbrack linear,univariate,equation,
21.127 test\rbrack, \lbrack Test,solve\_linear\rbrack \normalfont to
21.128 \ttfamily SubProblem (PolyEq',\\ \lbrack abcFormula,degree\_2,
21.129 @@ -2490,7 +2490,7 @@
21.130 }
21.131 And the respective method in \ttfamily Knowledge/PolyEq.thy \normalfont
21.132 at the respective \ttfamily store\_pbt. \normalfont Or you leave the
21.133 - selection of the appropriate type to isac as done in the final Script ;-))
21.134 + selection of the appropriate type to isac as done in the final Program ;-))
21.135 \end{itemize}%
21.136 \end{isamarkuptext}%
21.137 \isamarkuptrue%
22.1 --- a/test/Tools/isac/Interpret/calchead.sml Thu Aug 22 15:56:48 2019 +0200
22.2 +++ b/test/Tools/isac/Interpret/calchead.sml Thu Aug 22 16:48:04 2019 +0200
22.3 @@ -325,7 +325,7 @@
22.4 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
22.5 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
22.6 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
22.7 -val Const ("Script.SubProblem",_) $
22.8 +val Const ("Program.SubProblem",_) $
22.9 (Const ("Product_Type.Pair",_) $
22.10 Free (dI',_) $
22.11 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
22.12 @@ -350,7 +350,7 @@
22.13 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
22.14
22.15 "-b------------------------------------------------------";
22.16 -val Const ("Script.SubProblem",_) $
22.17 +val Const ("Program.SubProblem",_) $
22.18 (Const ("Product_Type.Pair",_) $
22.19 Free (dI',_) $
22.20 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
22.21 @@ -376,7 +376,7 @@
22.22 | _ => error "calchead.sml match_ags copy-named dropped --------";
22.23
22.24 "-c---ERROR case: stac is missing #Given equalities e_s--";
22.25 -val stac as Const ("Script.SubProblem",_) $
22.26 +val stac as Const ("Program.SubProblem",_) $
22.27 (Const ("Product_Type.Pair",_) $
22.28 Free (dI',_) $
22.29 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
22.30 @@ -416,7 +416,7 @@
22.31
22.32 "-------------------------------------step through end---";
22.33 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
22.34 -val Const ("Script.SubProblem",_) $
22.35 +val Const ("Program.SubProblem",_) $
22.36 (Const ("Product_Type.Pair",_) $
22.37 Free (dI',_) $
22.38 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
22.39 @@ -441,7 +441,7 @@
22.40 | _ => error "calchead.sml match_ags 2 args Nok ----------------";
22.41
22.42 "-b------------------------------------------------------";
22.43 -val Const ("Script.SubProblem",_) $
22.44 +val Const ("Program.SubProblem",_) $
22.45 (Const ("Product_Type.Pair",_) $
22.46 Free (dI',_) $
22.47 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
22.48 @@ -467,7 +467,7 @@
22.49 | _ => error "calchead.sml match_ags copy-named dropped --------";
22.50
22.51 "-c---ERROR case: stac is missing #Given equalities e_s--";
22.52 -val stac as Const ("Script.SubProblem",_) $
22.53 +val stac as Const ("Program.SubProblem",_) $
22.54 (Const ("Product_Type.Pair",_) $
22.55 Free (dI',_) $
22.56 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
22.57 @@ -512,7 +512,7 @@
22.58 | _ => error "calchead.sml match_ags 1st arg missing --------";
22.59
22.60 "-d------------------------------------------------------";
22.61 -val stac as Const ("Script.SubProblem",_) $
22.62 +val stac as Const ("Program.SubProblem",_) $
22.63 (Const ("Product_Type.Pair",_) $
22.64 Free (dI',_) $
22.65 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
22.66 @@ -530,7 +530,7 @@
22.67 | _ => error "calchead.sml match_ags 1st arg missing --------";
22.68
22.69 "-d------------------------------------------------------";
22.70 -val stac as Const ("Script.SubProblem",_) $
22.71 +val stac as Const ("Program.SubProblem",_) $
22.72 (Const ("Product_Type.Pair",_) $
22.73 Free (dI',_) $
22.74 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
23.1 --- a/test/Tools/isac/Interpret/ctree.sml Thu Aug 22 15:56:48 2019 +0200
23.2 +++ b/test/Tools/isac/Interpret/ctree.sml Thu Aug 22 16:48:04 2019 +0200
23.3 @@ -720,7 +720,7 @@
23.4 moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);
23.5 moveActiveFormula 1 ([3],Res)(*3.1.*);
23.6 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
23.7 -moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);
23.8 +moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Program Stepwise t_=*);
23.9
23.10 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
23.11 interSteps 1 ([1],Res)(*..is activeFormula !?!*);
24.1 --- a/test/Tools/isac/Interpret/me.sml Thu Aug 22 15:56:48 2019 +0200
24.2 +++ b/test/Tools/isac/Interpret/me.sml Thu Aug 22 16:48:04 2019 +0200
24.3 @@ -47,7 +47,7 @@
24.4 moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);
24.5 moveActiveFormula 1 ([3],Res)(*3.1.*);
24.6 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
24.7 -moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);
24.8 +moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Program Stepwise t_=*);
24.9
24.10 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
24.11 interSteps 1 ([1],Res)(*..is activeFormula !?!*);
25.1 --- a/test/Tools/isac/Interpret/script.sml Thu Aug 22 15:56:48 2019 +0200
25.2 +++ b/test/Tools/isac/Interpret/script.sml Thu Aug 22 16:48:04 2019 +0200
25.3 @@ -275,7 +275,7 @@
25.4 "----------- fun itms2args ---------------------------------------";
25.5 (*
25.6 > val sc = ... Solve_root_equation ...
25.7 -> val mI = ("Script","sqrt-equ-test");
25.8 +> val mI = ("Program","sqrt-equ-test");
25.9 > val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
25.10 > val ts = itms2args thy mI itms;
25.11 > map (term_to_string''' thy) ts;
25.12 @@ -318,12 +318,12 @@
25.13 > val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
25.14 (map HOLogic.mk_prod subs);
25.15 > val sT' = type_of subs';
25.16 -> val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT)
25.17 +> val lhs = Const ("Program.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT)
25.18 $ subs' $ Free (thmID,idT) $ @{term True} $ f;
25.19 > lhs = tt;
25.20 val it = true : bool
25.21 > rep_tac_ (Rewrite_Inst'
25.22 - ("Script","tless_true","eval_rls",false,subs,
25.23 + ("Program","tless_true","eval_rls",false,subs,
25.24 ("square_equation_left",""),f,(f',[])));
25.25 *)
25.26 (****************************| rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
25.27 @@ -334,11 +334,11 @@
25.28 > val f' = (Thm.term_of o the o (parse thy)) "x=#3";
25.29 > val Thm (id,thm) =
25.30 rep_tac_ (Rewrite'
25.31 - ("Script","tless_true","eval_rls",false,
25.32 + ("Program","tless_true","eval_rls",false,
25.33 ("square_equation_left",""),f,(f',[])));
25.34 > val SOME ct = parse thy
25.35 "Rewrite square_equation_left True (x=#1+#2)";
25.36 -> rewrite_ Script.thy tless_true eval_rls true thm ct;
25.37 +> rewrite_ Program.thy tless_true eval_rls true thm ct;
25.38 val it = SOME ("x = #3",[]) : (cterm * cterm list) option
25.39 *)
25.40 (**************************************** | rep_tac_ (Rewrite_Set_Inst'
25.41 @@ -349,13 +349,13 @@
25.42 (map HOLogic.mk_prod subs);
25.43 val sT' = type_of subs';
25.44 val b = if put then @{term True} else @{term False}
25.45 - val lhs = Const ("Script.Rewrite'_Set'_Inst",
25.46 + val lhs = Const ("Program.Rewrite'_Set'_Inst",
25.47 [sT',idT,fT,fT] ---> fT)
25.48 $ subs' $ Free (id_rls rls,idT) $ b $ f;
25.49 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end*)
25.50 (* ... vals from Rewrite_Inst' ...
25.51 > rep_tac_ (Rewrite_Set_Inst'
25.52 - ("Script",false,subs,
25.53 + ("Program",false,subs,
25.54 "isolate_bdv",f,(f',[])));
25.55 *)
25.56 (* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m;
25.57 @@ -374,7 +374,7 @@
25.58 > val f' = (Thm.term_of o the o (parse thy)) "x=#3";
25.59 > val Thm (id,thm) =
25.60 rep_tac_ (Rewrite_Set'
25.61 - ("Script",false,"SqRoot_simplify",f,(f',[])));
25.62 + ("Program",false,"SqRoot_simplify",f,(f',[])));
25.63 val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string
25.64 val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm
25.65 *)
26.1 --- a/test/Tools/isac/Knowledge/algein.sml Thu Aug 22 15:56:48 2019 +0200
26.2 +++ b/test/Tools/isac/Knowledge/algein.sml Thu Aug 22 16:48:04 2019 +0200
26.3 @@ -24,7 +24,7 @@
26.4 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
26.5 "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
26.6 val str =
26.7 -"Script RechnenSymbolScript (k_k::bool) (q__q::bool) \
26.8 +"Program RechnenSymbolScript (k_k::bool) (q__q::bool) \
26.9 \(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =\
26.10 \ (let t_t = (l_l = 1)\
26.11 \ in t_t)"
27.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml Thu Aug 22 15:56:48 2019 +0200
27.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml Thu Aug 22 16:48:04 2019 +0200
27.3 @@ -146,7 +146,7 @@
27.4 val Ass (m,v', ctxt) = (*case*) associate pt ctxt (m, stac) (*of*);
27.5
27.6 "~~~~~ fun associate , args:"; val (pt, _, (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _)),
27.7 - (stac as Const ("Script.SubProblem", _) $ (Const ("Product_Type.Pair", _) $
27.8 + (stac as Const ("Program.SubProblem", _) $ (Const ("Product_Type.Pair", _) $
27.9 dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags')) =
27.10 (pt, d, m, stac);
27.11 val dI = HOLogic.dest_string dI';
28.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Thu Aug 22 15:56:48 2019 +0200
28.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Thu Aug 22 16:48:04 2019 +0200
28.3 @@ -51,7 +51,7 @@
28.4 take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
28.5 val knowthys' = (*["Isac", .., "Descript", "Delete"]*)
28.6 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys');
28.7 - val progthys' = (*["Script", "Tools", "ListC", "KEStore"]*)
28.8 + val progthys' = (*["Program", "Tools", "ListC", "KEStore"]*)
28.9 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys');
28.10 val isacrlsthms = (*length = 460*)
28.11 thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (thmID * thm) list
29.1 --- a/test/Tools/isac/Knowledge/diff.sml Thu Aug 22 15:56:48 2019 +0200
29.2 +++ b/test/Tools/isac/Knowledge/diff.sml Thu Aug 22 16:48:04 2019 +0200
29.3 @@ -234,7 +234,7 @@
29.4 else error "diff.sml: diff.behav. in 'primed'";
29.5 atomty f'_;
29.6
29.7 -val str = "Script DiffEqScr (f_f::bool) (v_v::real) = \
29.8 +val str = "Program DiffEqScr (f_f::bool) (v_v::real) = \
29.9 \ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) \
29.10 \ in (((Try (Repeat (Rewrite frac_conv False))) @@ \
29.11 \ (Try (Repeat (Rewrite root_conv False))) @@ \
30.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Thu Aug 22 15:56:48 2019 +0200
30.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Thu Aug 22 16:48:04 2019 +0200
30.3 @@ -136,8 +136,8 @@
30.4 (* --vvv-- ausgeliehen von test-root-equ/sml *)
30.5 val loc = e_istate;
30.6 val (dI',pI',mI') =
30.7 - ("Script",["sqroot-test","univariate","equation"],
30.8 - ["Script","squ-equ-test2"]);
30.9 + ("Program",["sqroot-test","univariate","equation"],
30.10 + ["Program","squ-equ-test2"]);
30.11 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
30.12 "solveFor x","errorBound (eps=0)",
30.13 "solutions L"];
30.14 @@ -460,7 +460,7 @@
30.15 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
30.16 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------";
30.17 str2term
30.18 - "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list)\
30.19 + "Program Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list)\
30.20 \ (v_v::real) (itv_v::real set) (err_r::bool) = \
30.21 \ (let e_e = (hd o (filterVar m_m)) r_s; \
30.22 \ t_t = (if 1 < length_h r_s \
30.23 @@ -542,7 +542,7 @@
30.24 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
30.25 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
30.26 str2term
30.27 - "Script Make_fun_by_explicit (f_f::real) (v_v::real) \
30.28 + "Program Make_fun_by_explicit (f_f::real) (v_v::real) \
30.29 \ (eqs::bool list) = \
30.30 \ (let h_h = (hd o (filterVar f_f)) eqs; \
30.31 \ e_1 = hd (dropWhile (ident h_h) eqs); \
30.32 @@ -643,7 +643,7 @@
30.33 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
30.34 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
30.35 str2term
30.36 - "Script Make_fun_by_new_variable (f_f::real) (v_v::real) \
30.37 + "Program Make_fun_by_new_variable (f_f::real) (v_v::real) \
30.38 \ (eqs::bool list) = \
30.39 \(let h_h = (hd o (filterVar f_f)) eqs; \
30.40 \ es_s = dropWhile (ident h_h) eqs; \
31.1 --- a/test/Tools/isac/Knowledge/integrate.sml Thu Aug 22 15:56:48 2019 +0200
31.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Thu Aug 22 16:48:04 2019 +0200
31.3 @@ -376,14 +376,14 @@
31.4 "----------- check Scripts ------------------------------";
31.5 "----------- check Scripts ------------------------------";
31.6 val str =
31.7 -"Script IntegrationScript (f_f::real) (v_v::real) = \
31.8 +"Program IntegrationScript (f_f::real) (v_v::real) = \
31.9 \ (let t_t = Take (Integral f_f D v_v) \
31.10 \ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) (t_t::real))";
31.11 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
31.12 atomty sc;
31.13
31.14 val str =
31.15 -"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \
31.16 +"Program NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \
31.17 \ (let t_t = Take (F_F v_v = Integral f_f D v_v) \
31.18 \ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) t_t)";
31.19 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
32.1 --- a/test/Tools/isac/Knowledge/integrate.thy Thu Aug 22 15:56:48 2019 +0200
32.2 +++ b/test/Tools/isac/Knowledge/integrate.thy Thu Aug 22 16:48:04 2019 +0200
32.3 @@ -21,7 +21,7 @@
32.4 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
32.5 crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
32.6 @{thm integration_test.simps}
32.7 - (*"Script IntegrationScript (f_f::real) (v_v::real) = \
32.8 + (*"Program IntegrationScript (f_f::real) (v_v::real) = \
32.9 \ (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'' False) @@ \
32.10 \ (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'' False) @@ \
32.11 \ (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) (f_f::real))"*))]
33.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Thu Aug 22 15:56:48 2019 +0200
33.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Thu Aug 22 16:48:04 2019 +0200
33.3 @@ -50,7 +50,7 @@
33.4 pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*)
33.5 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";
33.6 (*do_solve_step (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
33.7 - THIS MEANS: replace no_meth by [no_meth] in Script.*)
33.8 + THIS MEANS: replace no_meth by [no_meth] in Program.*)
33.9 (*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *)
33.10 (*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)
33.11
33.12 @@ -462,7 +462,7 @@
33.13 "----------- progr.vers.2: improve program --------------";
33.14 "----------- progr.vers.2: improve program --------------";
33.15 (*WN120318 stopped due to much effort with the test above*)
33.16 - "Script PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
33.17 + "Program PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
33.18 " (let f_f = Take f_f; " ^
33.19 " (num_orig::real) = get_numerator f_f; " ^(*num_orig: 3*)
33.20 " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*f_f: 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
34.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Thu Aug 22 15:56:48 2019 +0200
34.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Thu Aug 22 16:48:04 2019 +0200
34.3 @@ -228,7 +228,7 @@
34.4 (* WAS val NotAss = associate pt d (m, stac)
34.5 ... Ass ... is correct*)
34.6 "~~~~~ fun associate, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
34.7 - (Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
34.8 + (Const ("Program.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
34.9 term2str consts;
34.10 term2str consts';
34.11 if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
35.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Thu Aug 22 15:56:48 2019 +0200
35.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Thu Aug 22 16:48:04 2019 +0200
35.3 @@ -234,7 +234,7 @@
35.4 "----------- met simplification for_polynomials with_minus -------";
35.5 "----------- met simplification for_polynomials with_minus -------";
35.6 val str =
35.7 -"Script SimplifyScript (t_t::real) = \
35.8 +"Program SimplifyScript (t_t::real) = \
35.9 \ (((Try (Rewrite_Set ordne_alphabetisch False)) @@ \
35.10 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \
35.11 \ (Try (Rewrite_Set verschoenere False))) t_t)"
35.12 @@ -338,7 +338,7 @@
35.13 "----------- met probe fuer_polynom ------------------------------";
35.14 "----------- met probe fuer_polynom ------------------------------";
35.15 val str =
35.16 -"Script ProbeScript (e_e::bool) (w_s::bool list) =\
35.17 +"Program ProbeScript (e_e::bool) (w_s::bool list) =\
35.18 \ (let e_e = Take e_e; \
35.19 \ e_e = Substitute w_s e_e \
35.20 \ in (Repeat((Try (Repeat (Calculate ''TIMES''))) @@ \
36.1 --- a/test/Tools/isac/Knowledge/rateq.sml Thu Aug 22 15:56:48 2019 +0200
36.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Thu Aug 22 16:48:04 2019 +0200
36.3 @@ -115,14 +115,14 @@
36.4 (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
36.5 ay = Napp_; (*false*)
36.6 val up = drop_last l;
36.7 -val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; (*Const ("Script.SubProblem",..*)
36.8 +val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; (*Const ("Program.SubProblem",..*)
36.9 val i = mk_Free (i, T);
36.10 val E = upd_env E (i, v);
36.11 "~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) =
36.12 (thy, ptp, E, (up@[R,D]), body, a, v);
36.13 "~~~~~ fun handle_leaf, args:"; val (call, thy, srls, E, a, v, t) = ("next ", th, sr, E, a, v, t);
36.14 "~~~~~ fun subst_stacexpr, args:"; val (E, a, v,
36.15 - (t as (Const ("Script.Check'_elementwise",_) $ _ $ _ ))) = (E, a, v, t);
36.16 + (t as (Const ("Program.Check'_elementwise",_) $ _ $ _ ))) = (E, a, v, t);
36.17 val STac tm = STac (subst_atomic E t);
36.18 term2str tm = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
36.19 (* ------ ^^^ ----- ? "x" ?*)
37.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Thu Aug 22 15:56:48 2019 +0200
37.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Thu Aug 22 16:48:04 2019 +0200
37.3 @@ -478,7 +478,7 @@
37.4
37.5 ===== inhibit exn ?===========================================================*)
37.6
37.7 -(*===== copied here from OLDTESTS in case there is a Script ===vvv=============================
37.8 +(*===== copied here from OLDTESTS in case there is a Program ===vvv=============================
37.9 val c = [];
37.10
37.11 "---------------- root-eq + subpbl: solve_linear ----------";
37.12 @@ -805,4 +805,4 @@
37.13 refine fmz ["univariate","equation","test"];
37.14 match_pbl fmz (get_pbt ["polynomial","univariate","equation","test"]);
37.15
37.16 -===== copied here from OLDTESTS in case there is a Script ===^^^=============================*)
37.17 +===== copied here from OLDTESTS in case there is a Program ===^^^=============================*)
38.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Aug 22 15:56:48 2019 +0200
38.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Aug 22 16:48:04 2019 +0200
38.3 @@ -135,18 +135,18 @@
38.4 l = [] (* = true*);
38.5 "~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) =
38.6 (thy, ptp, E, [Celem.R], body, NONE, v);
38.7 -"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Seq"(*1*),_) $ e1 $ e2 $ a), _, v) =
38.8 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Program.Seq"(*1*),_) $ e1 $ e2 $ a), _, v) =
38.9 (thy, ptp, E, (l @ [Celem.L, Celem.R]), e, a, v);
38.10 -"~~~~~ fun appy, args:"; val (thy, ptp, E, l,(Const ("Script.Try"(*1*),_) $ e), a, v) =
38.11 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l,(Const ("Program.Try"(*1*),_) $ e), a, v) =
38.12 (thy, ptp, E, (l @ [Celem.L, Celem.L, Celem.R]), e1, (SOME a), v);
38.13 (* appy thy ptp E (l @ [Celem.R]) e a v
38.14 -ERROR WAAS: exception TYPE raised (line 168 of "consts.ML"): Illegal type for constant "Script.Rewrite'_Set" :: ID \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool*)
38.15 +ERROR WAAS: exception TYPE raised (line 168 of "consts.ML"): Illegal type for constant "Program.Rewrite'_Set" :: ID \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool*)
38.16 (* a leaf has been found *)
38.17 "~~~~~ fun appy, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) =
38.18 (thy, ptp, E, (l @ [Celem.R]), e, a, v);
38.19 val (a', LTool.STac stac) = handle_leaf "next " th sr E a v t;
38.20 val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac;
38.21 -"~~~~~ fun stac2tac_, args:"; val (_, _, (Const ("Script.Rewrite'_Set",_) $ rls $ _ $ _)) =
38.22 +"~~~~~ fun stac2tac_, args:"; val (_, _, (Const ("Program.Rewrite'_Set",_) $ rls $ _ $ _)) =
38.23 (pt, (Celem.assoc_thy th), stac);
38.24 case stac2tac_ pt (Celem.assoc_thy th) stac of (Rewrite_Set "norm_equation", _) => ()
38.25 | _ => error "stac2tac_ changed"
38.26 @@ -156,7 +156,7 @@
38.27 "~~~~~ fun rep_tac_, args:"; val (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) = (m);
38.28 val fT = type_of f;
38.29 val b = if put then @{term True} else @{term False};
38.30 - val lhs = Const ("Script.Rewrite'_Set", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
38.31 + val lhs = Const ("Program.Rewrite'_Set", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
38.32 $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
38.33 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ here was Free (Rule.id_rls rls, idT) *)
38.34
39.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Aug 22 15:56:48 2019 +0200
39.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Aug 22 16:48:04 2019 +0200
39.3 @@ -67,13 +67,13 @@
39.4
39.5 (*val Assoc (scrstate, steps) = in isabisacREP*)
39.6 (*val NasApp ((E',l,a,v,S,_),ss) = in isabisac*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e;
39.7 -"~~~~~ fun assy, args:"; val (ya, ((E,l,_,v,S,b),ss:step list), (Const ("Script.Seq"(*2[1]*),_) $e1 $ e2 $ a)) =
39.8 +"~~~~~ fun assy, args:"; val (ya, ((E,l,_,v,S,b),ss:step list), (Const ("Program.Seq"(*2[1]*),_) $e1 $ e2 $ a)) =
39.9 (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);
39.10
39.11 (*val Assoc (scrstate, steps) = in isabisacREP*)
39.12 (*val NasApp ((E,_,_,v,_,_),ss) = in isabisac*)
39.13 (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss) e1 (*of*);
39.14 -"~~~~~ fun assy, args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("Script.Try"(*1*),_) $ e)) =
39.15 +"~~~~~ fun assy, args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("Program.Try"(*1*),_) $ e)) =
39.16 ( ya, ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss), e1);
39.17
39.18 term2str e1 = "Try (Rewrite_Set ''norm_equation'' False)" (*in isabisac*);
39.19 @@ -96,9 +96,9 @@
39.20 (*val NotAss = in isabisac*)
39.21 (*case*) associate pt ctxt (m, stac) (*of*);
39.22 "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))),
39.23 - (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_)) = (pt, d, m, stac);
39.24 + (Const ("Program.Rewrite'_Set", _) $ rls_ $ _ $ f_)) = (pt, d, m, stac);
39.25
39.26 -if Rule.id_rls rls = HOLogic.dest_string rls_ then () else error "Script.associate changed";
39.27 +if Rule.id_rls rls = HOLogic.dest_string rls_ then () else error "Program.associate changed";
39.28
39.29 "~~~~~ continue me[1] after locatetac";
39.30 val (pt, p) = ptp''''';
39.31 @@ -132,13 +132,13 @@
39.32 (*isabisac17: nxt_up thy ptp (Celem.Prog sc) E up ay (go up sc) a v ERROR go: no [L,L,R]*)
39.33 (*isabisac17: (go up sc) ERROR go: no [L,L,R]*)
39.34 (*isabisac15:*)
39.35 -val ttt as Const ("Script.Try", _) $ (Const ("Script.Rewrite'_Set", _) $ rls $
39.36 +val ttt as Const ("Program.Try", _) $ (Const ("Program.Rewrite'_Set", _) $ rls $
39.37 Const ("HOL.False", _)) = (go up sc)
39.38 -val (Const ("Script.Try"(*2*), _) $ _) = ttt;
39.39 +val (Const ("Program.Try"(*2*), _) $ _) = ttt;
39.40 if term2str ttt = "Try (Rewrite_Set ''norm_equation'' False)"
39.41 then () else error "250-Rewrite_Set: (go up sc) CHANGED";
39.42
39.43 -"~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, _, (Const ("Script.Try"(*2*), _) $ _), a, v) =
39.44 +"~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, _, (Const ("Program.Try"(*2*), _) $ _), a, v) =
39.45 (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v );
39.46
39.47 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
39.48 @@ -190,7 +190,7 @@
39.49 val up = drop_last l;
39.50
39.51 nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;
39.52 -"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, _, (Const ("Script.Try"(*1*),_) $ _ ), a, v)
39.53 +"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, _, (Const ("Program.Try"(*1*),_) $ _ ), a, v)
39.54 = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);
39.55
39.56 nstep_up thy ptp scr E l Skip_ a v;
39.57 @@ -200,7 +200,7 @@
39.58 val up = drop_last l;
39.59
39.60 nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;
39.61 -"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq"(*2*), _) $ _ $ _), a, v)
39.62 +"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Program.Seq"(*2*), _) $ _ $ _), a, v)
39.63 = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);
39.64
39.65 nstep_up thy ptp scr E l ay a v;
39.66 @@ -210,7 +210,7 @@
39.67 val up = drop_last l;
39.68
39.69 nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;
39.70 -"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq"(*1*), _) $ _ $ _ $ _), a, v)
39.71 +"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Program.Seq"(*1*), _) $ _ $ _ $ _), a, v)
39.72 = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);
39.73
39.74 nstep_up thy ptp scr E l ay a v;
39.75 @@ -241,7 +241,7 @@
39.76 val (a', LTool.STac stac) = (*case*) Lucin.handle_leaf "next " th sr E a v t (*of*);
39.77
39.78 (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy th) stac;
39.79 -"~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Script.SubProblem", _) $ spec' $ ags'))
39.80 +"~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Program.SubProblem", _) $ spec' $ ags'))
39.81 = (pt, (Celem.assoc_thy th), stac);
39.82 val (dI, pI, mI) = LTool.dest_spec spec'
39.83 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
40.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Aug 22 15:56:48 2019 +0200
40.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Aug 22 16:48:04 2019 +0200
40.3 @@ -55,7 +55,7 @@
40.4 val up = drop_last l;
40.5
40.6 ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
40.7 -"~~~~~ fun ass_up, args:"; val (ysa, iss, (Const ("Script.Try",_) $ e)) =
40.8 +"~~~~~ fun ass_up, args:"; val (ysa, iss, (Const ("Program.Try",_) $ e)) =
40.9 (ys, ((E,up,a,v,S,b),ss), (go up sc));
40.10 astep_up ysa iss;
40.11 "~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);
40.12 @@ -63,7 +63,7 @@
40.13 val up = drop_last l;
40.14
40.15 ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
40.16 -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _ )) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
40.17 +"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Program.Seq",_) $ _ $ _ )) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
40.18
40.19 astep_up ysa iss (*2*: comes from e2*);
40.20 "~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);
40.21 @@ -71,7 +71,7 @@
40.22 val up = drop_last l;
40.23
40.24 ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
40.25 -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _ $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
40.26 +"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Program.Seq",_) $ _ $ _ $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
40.27
40.28 astep_up ysa iss (*all has been done in (*2*) below*);
40.29 "~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);
40.30 @@ -103,7 +103,7 @@
40.31 = ("locate", "Isac", sr, E, a, v, t);
40.32
40.33 val (a', LTool.STac stac) = (*case*) LTool.subst_stacexpr E a v t (*of*);
40.34 -"~~~~~ fun subst_stacexpr , args:"; val (E, _, _, (t as (Const ("Script.SubProblem", _) $ _ $ _)))
40.35 +"~~~~~ fun subst_stacexpr , args:"; val (E, _, _, (t as (Const ("Program.SubProblem", _) $ _ $ _)))
40.36 = (E, a, v, t);
40.37
40.38 (NONE, STac (subst_atomic E t)); (*return value*)
41.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Aug 22 15:56:48 2019 +0200
41.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Aug 22 16:48:04 2019 +0200
41.3 @@ -73,12 +73,12 @@
41.4 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;
41.5 val i = mk_Free (i, T);
41.6 val E = upd_env E (i, v);
41.7 -body; (*= Const ("Script.Check'_elementwise"*)
41.8 +body; (*= Const ("Program.Check'_elementwise"*)
41.9 "~~~~~ fun appy, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v)=
41.10 (thy, ptp, E, (up@[R,D]), body, a, v);
41.11 -handle_leaf "next " th sr E a v t; (*= (NONE, STac (Const ("Script.Check'_elementwise"*)
41.12 +handle_leaf "next " th sr E a v t; (*= (NONE, STac (Const ("Program.Check'_elementwise"*)
41.13 val (a', STac stac) = handle_leaf "next " th sr E a v t;
41.14 -"~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Script.Check'_elementwise",_) $ _ $
41.15 +"~~~~~ fun stac2tac_, args:"; val (pt, thy, (Const("Program.Check'_elementwise",_) $ _ $
41.16 (set as Const ("Set.Collect",_) $ Abs (_,_,pred)))) = (pt, (assoc_thy th), stac);
41.17 (*2011 changed ^^^^^ *)
41.18
42.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Thu Aug 22 15:56:48 2019 +0200
42.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Thu Aug 22 16:48:04 2019 +0200
42.3 @@ -117,19 +117,19 @@
42.4 (*if*) l = [] (* = true *);
42.5 appy thy ptp E [Celem.R] body NONE v;
42.6
42.7 -"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Repeat"(*2*),_) $ e), a, v) =
42.8 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Program.Repeat"(*2*),_) $ e), a, v) =
42.9 (thy, ptp, E, [Celem.R], body, NONE, v);
42.10 appy thy ptp E (l @ [Celem.R]) e a v;
42.11
42.12 -"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Seq"(*1*),_) $ e1 $ e2 $ a), _, v) =
42.13 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Program.Seq"(*1*),_) $ e1 $ e2 $ a), _, v) =
42.14 (thy, ptp, E, (l @ [Celem.R]), e, a, v);
42.15 (*case*) appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v (*of*);
42.16
42.17 -"~~~~~ fun appy, args:"; val (thy, ptp, E, l,(Const ("Script.Try"(*1*),_) $ e), a, v) =
42.18 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l,(Const ("Program.Try"(*1*),_) $ e), a, v) =
42.19 (thy, ptp, E, (l @ [Celem.L, Celem.L, Celem.R]), e1, (SOME a), v);
42.20 (*case*) appy thy ptp E (l @ [Celem.R]) e a v (*of*);
42.21
42.22 -"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Repeat"(*2*),_) $ e), a, v) =
42.23 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Program.Repeat"(*2*),_) $ e), a, v) =
42.24 (thy, ptp, E, (l @ [Celem.R]), e, a, v);
42.25 appy thy ptp E (l @ [Celem.R]) e a v;
42.26
43.1 --- a/test/Tools/isac/OLDTESTS/script.sml Thu Aug 22 15:56:48 2019 +0200
43.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Thu Aug 22 16:48:04 2019 +0200
43.3 @@ -39,7 +39,7 @@
43.4 " ################################################# 6.5.03 ";
43.5
43.6 val c = (the o (parse DiffApp.thy))
43.7 - "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
43.8 + "Program Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
43.9 \ (v_::real) (itv_::real set) (err_::bool) = \
43.10 \ (let e_e = (hd o (filterVar m_)) rs_; \
43.11 \ t_ = (if 1 < length_ rs_ \
43.12 @@ -59,7 +59,7 @@
43.13 "################################################### 6.5.03";
43.14
43.15 val sc = (the o (parse DiffApp.thy)) (*start interpretieren*)
43.16 - "Script Make_fun_by_new_variable (f_::real) (v_::real) \
43.17 + "Program Make_fun_by_new_variable (f_::real) (v_::real) \
43.18 \ (eqs_::bool list) = \
43.19 \(let h_ = (hd o (filterVar f_)) eqs_; \
43.20 \ es_ = dropWhile (ident h_) eqs_; \
43.21 @@ -142,7 +142,7 @@
43.22 "############## Make_fun_by_explicit ############## 6.5.03";
43.23 "############## Make_fun_by_explicit ############## 6.5.03";
43.24 val c = (the o (parse DiffApp.thy))
43.25 - "Script Make_fun_by_explicit (f_::real) (v_::real) \
43.26 + "Program Make_fun_by_explicit (f_::real) (v_::real) \
43.27 \ (eqs_::bool list) = \
43.28 \ (let h_ = (hd o (filterVar f_)) eqs_; \
43.29 \ e_1 = hd (dropWhile (ident h_) eqs_); \
43.30 @@ -157,7 +157,7 @@
43.31 "################ Solve_root_equation #################";
43.32 (*#####################################################*)
43.33 val sc = (Thm.term_of o the o (parse Test.thy))
43.34 - "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\
43.35 + "Program Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\
43.36 \ (let e_e = Rewrite square_equation_left True eq_; \
43.37 \ e_e = Rewrite_Set Test_simplify False e_; \
43.38 \ e_e = Rewrite_Set rearrange_assoc False e_; \
43.39 @@ -249,7 +249,7 @@
43.40
43.41 val scr as (Prog sc) = Prog (((inst_abs Test.thy)
43.42 o Thm.term_of o the o (parse thy))
43.43 - "Script Testeq (e_e::bool) = \
43.44 + "Program Testeq (e_e::bool) = \
43.45 \(While (contains_root e_e) Do \
43.46 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \
43.47 \ (Try (Repeat (Rewrite square_equation_left True))) @@ \
43.48 @@ -270,7 +270,7 @@
43.49
43.50 val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0";
43.51 val ve0_= (Thm.term_of o the o (parse thy)) ct;
43.52 -val ets0=[([],(Tac_(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)],
43.53 +val ets0=[([],(Tac_(Program.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)],
43.54 e_term,e_term,Safe)),
43.55 ([],(User', [], [], e_term, e_term,Sundef))]:ets;
43.56 val l0 = [];
43.57 @@ -283,14 +283,14 @@
43.58
43.59 val scr as (Prog sc) =
43.60 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy))
43.61 - "Script Testterm (g_::real) = (Calculate cancel g_)");
43.62 + "Program Testterm (g_::real) = (Calculate cancel g_)");
43.63 (*
43.64 val scr as (Prog sc) =
43.65 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy))
43.66 - "Script Testterm (g_::real) = (Calculate power g_)");
43.67 + "Program Testterm (g_::real) = (Calculate power g_)");
43.68 val scr as (Prog sc) =
43.69 Prog (((inst_abs Test.thy) o Thm.term_of o the o (parse thy))
43.70 - "Script Testterm (g_::real) = (Calculate pow g_)");
43.71 + "Program Testterm (g_::real) = (Calculate pow g_)");
43.72 ..............................................................*)
43.73 writeln
43.74 "%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\
44.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Thu Aug 22 15:56:48 2019 +0200
44.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Thu Aug 22 16:48:04 2019 +0200
44.3 @@ -85,7 +85,7 @@
44.4 ],
44.5 {rew_ord'="tless_true",rls'="tval_rls",erls=e_rls,prls=e_rls,calc=[],
44.6 asm_rls=[],asm_thm=[]},
44.7 - "Script Solve_univar_err (e_e::bool) (v_::real) (err_::bool) = \
44.8 + "Program Solve_univar_err (e_e::bool) (v_::real) (err_::bool) = \
44.9 \ (if (is_rootequation_in e_e v_v)\
44.10 \ then ((SubProblem (IsacX,[squareroot,univariate,equation],\
44.11 \ (SqRoot_,square_equation)) [BOOL e_e, REAL v_v, BOOL err_]))\
45.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Thu Aug 22 15:56:48 2019 +0200
45.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Thu Aug 22 16:48:04 2019 +0200
45.3 @@ -39,7 +39,7 @@
45.4 {rew_ord'="tless_true",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
45.5 crls=tval_rls, errpats = [], nrls=e_rls(*,
45.6 asm_rls=[],asm_thm=[]*)},
45.7 - "Script Testterm (g_::real) = \
45.8 + "Program Testterm (g_::real) = \
45.9 \Repeat\
45.10 \ ((Repeat (Rewrite rmult_1 False)) Or\
45.11 \ (Repeat (Rewrite rmult_0 False)) Or\
45.12 @@ -109,7 +109,7 @@
45.13 [Calc ("Test.contains'_root", eval_contains_root"")],
45.14 prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls=e_rls
45.15 (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},
45.16 - "Script Testeq (e_e::bool) = \
45.17 + "Program Testeq (e_e::bool) = \
45.18 \(While (contains_root e_e) Do \
45.19 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \
45.20 \ (Try (Repeat (Rewrite square_equation_left True))) @@ \
45.21 @@ -167,7 +167,7 @@
45.22 [Calc ("Test.contains'_root",eval_contains_root"")],
45.23 prls=e_rls,calc=[], crls=tval_rls, errpats = [], nrls=e_rls
45.24 (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},
45.25 - "Script Testeq2 (e_e::bool) = \
45.26 + "Program Testeq2 (e_e::bool) = \
45.27 \(let e_e =\
45.28 \ ((While (contains_root e_e) Do \
45.29 \ (Rewrite square_equation_left True))\
45.30 @@ -484,7 +484,7 @@
45.31
45.32 (*GoOn.5.03. script with Map, Subst (biquadr.equ.)
45.33 val scr = Prog ((inst_abs o Thm.term_of o the o (parse thy))
45.34 - "Script Biquadrat_poly (e_e::bool) (v_::real) = \
45.35 + "Program Biquadrat_poly (e_e::bool) (v_::real) = \
45.36 \(let e_e = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_; \
45.37 \ L_0_ = (SubProblem (PolyEqX,[univariate,equation], [no_met]) \
45.38 \ [BOOL e_e, REAL v_0_]); \
46.1 --- a/test/Tools/isac/ProgLang/calculate.thy Thu Aug 22 15:56:48 2019 +0200
46.2 +++ b/test/Tools/isac/ProgLang/calculate.thy Thu Aug 22 16:48:04 2019 +0200
46.3 @@ -44,7 +44,7 @@
46.4 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
46.5 crls=tval_rls, errpats = [], nrls= Rule.e_rls (*, asm_rls=[],asm_thm=[]*)},
46.6 @{thm calc_test.simps}
46.7 - (*"Script STest_simplify (t_t::real) = \
46.8 + (*"Program STest_simplify (t_t::real) = \
46.9 \(Repeat \
46.10 \ ((Try (Repeat (Calculate ''PLUS''))) @@ \
46.11 \ (Try (Repeat (Calculate ''TIMES''))) @@ \
47.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Thu Aug 22 15:56:48 2019 +0200
47.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Thu Aug 22 16:48:04 2019 +0200
47.3 @@ -26,7 +26,7 @@
47.4 "-------- test the same called by interSteps norm_Poly -----------";
47.5 val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
47.6 writeln(term2str auto_script);
47.7 -(*Script Stepwise t_t =
47.8 +(*Program Stepwise t_t =
47.9 (Try (Rewrite_Set discard_minus False) @@
47.10 Try (Rewrite_Set expand_poly_ False) @@
47.11 Try (Repeat (Calculate TIMES)) @@
47.12 @@ -109,35 +109,35 @@
47.13 writeln(term2str auto_script);
47.14 atomty auto_script;
47.15 (***
47.16 -*** Const (Script.Stepwise, 'z => 'z => 'z)
47.17 +*** Const (Program.Stepwise, 'z => 'z => 'z)
47.18 *** . Free (t_t, 'z)
47.19 -*** . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
47.20 -*** . . Const (Script.Try, ('a => 'a) => 'a => 'a)
47.21 -*** . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
47.22 +*** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
47.23 +*** . . Const (Program.Try, ('a => 'a) => 'a => 'a)
47.24 +*** . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
47.25 *** . . . . Free (discard_minus, ID)
47.26 *** . . . . Const (HOL.False, bool)
47.27 -*** . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
47.28 -*** . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
47.29 -*** . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
47.30 +*** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
47.31 +*** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
47.32 +*** . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
47.33 *** . . . . . Free (rat_mult_poly, ID)
47.34 *** . . . . . Const (HOL.False, bool)
47.35 -*** . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
47.36 -*** . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
47.37 -*** . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
47.38 +*** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
47.39 +*** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
47.40 +*** . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
47.41 *** . . . . . . Free (make_rat_poly_with_parentheses, ID)
47.42 *** . . . . . . Const (HOL.False, bool)
47.43 -*** . . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
47.44 -*** . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
47.45 -*** . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
47.46 +*** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
47.47 +*** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
47.48 +*** . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
47.49 *** . . . . . . . Free (cancel_p_rls, ID)
47.50 *** . . . . . . . Const (HOL.False, bool)
47.51 -*** . . . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
47.52 -*** . . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
47.53 -*** . . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
47.54 +*** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
47.55 +*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
47.56 +*** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
47.57 *** . . . . . . . . Free (norm_Rational_rls, ID)
47.58 *** . . . . . . . . Const (HOL.False, bool)
47.59 -*** . . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
47.60 -*** . . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
47.61 +*** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
47.62 +*** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
47.63 *** . . . . . . . . Free (discard_parentheses1, ID)
47.64 *** . . . . . . . . Const (HOL.False, bool)
47.65 *** . . Const (empty, 'a)
47.66 @@ -157,7 +157,7 @@
47.67 interSteps 1 ([1], Res);
47.68 val ((pt,p),_) = get_calc 1; show_pt pt;
47.69
47.70 -(*with "Script SimplifyScript (t_::real) = \
47.71 +(*with "Program SimplifyScript (t_::real) = \
47.72 \ ((Rewrite_Set norm_Rational False) t_)"
47.73 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
47.74 *)
47.75 @@ -217,12 +217,12 @@
47.76 "-------- fun subst_stacexpr, fun stacpbls -----------------------------------";
47.77 val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
47.78 case stacpbls sc of
47.79 - [Const ("Script.Rewrite", _) $ square_equation_left $ Const ("HOL.True", _),
47.80 - Const ("Script.Rewrite'_Set", _) $ Test_simplify $ Const ("HOL.False", _),
47.81 - Const ("Script.Rewrite'_Set", _) $ rearrange_assoc $ Const ("HOL.False", _),
47.82 - Const ("Script.Rewrite'_Set", _) $ isolate_root $ Const ("HOL.False", _),
47.83 - Const ("Script.Rewrite'_Set", _) $ norm_equation $ Const ("HOL.False", _),
47.84 - Const ("Script.Rewrite'_Set'_Inst", _) $
47.85 + [Const ("Program.Rewrite", _) $ square_equation_left $ Const ("HOL.True", _),
47.86 + Const ("Program.Rewrite'_Set", _) $ Test_simplify $ Const ("HOL.False", _),
47.87 + Const ("Program.Rewrite'_Set", _) $ rearrange_assoc $ Const ("HOL.False", _),
47.88 + Const ("Program.Rewrite'_Set", _) $ isolate_root $ Const ("HOL.False", _),
47.89 + Const ("Program.Rewrite'_Set", _) $ norm_equation $ Const ("HOL.False", _),
47.90 + Const ("Program.Rewrite'_Set'_Inst", _) $
47.91 (Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ bdv $ Free ("v_v", _)) $
47.92 Const ("List.list.Nil", _)) $
47.93 isolate_bdv $ Const ("HOL.False", _)] =>
47.94 @@ -248,8 +248,8 @@
47.95 (NONE, Expr (Const ("HOL.eq", _) $
47.96 (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $
47.97 (Const ("HOL.Let", _) $
47.98 - (Const ("Script.Seq", _) $
47.99 - (Const ("Script.While", _) $ _ $
47.100 + (Const ("Program.Seq", _) $
47.101 + (Const ("Program.While", _) $ _ $
47.102 _ ) $
47.103 (_) $
47.104 Free ("e_e", _)) $
47.105 @@ -296,9 +296,9 @@
47.106 if term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'' False))" then ()
47.107 else error "rule2stac_inst Thm.. changed";
47.108 case t of
47.109 - (Const ("Script.Try", _) $
47.110 - (Const ("Script.Repeat", _) $
47.111 - (Const ("Script.Rewrite'_Inst", _) $
47.112 + (Const ("Program.Try", _) $
47.113 + (Const ("Program.Repeat", _) $
47.114 + (Const ("Program.Rewrite'_Inst", _) $
47.115 (Const ("List.list.Cons", _) $
47.116 (Const ("Product_Type.Pair", _) $
47.117 bdv $
48.1 --- a/test/Tools/isac/ProgLang/scrtools.thy Thu Aug 22 15:56:48 2019 +0200
48.2 +++ b/test/Tools/isac/ProgLang/scrtools.thy Thu Aug 22 16:48:04 2019 +0200
48.3 @@ -27,7 +27,7 @@
48.4 {rew_ord' = "dummy_ord", rls' = tval_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
48.5 crls=tval_rls, errpats = [], nrls = Rule.e_rls},
48.6 @{thm stepwise_test.simps}
48.7 - (*"Script Stepwise t_t = \
48.8 + (*"Program Stepwise t_t = \
48.9 \(Try (Rewrite_Set ''discard_minus'' False) @@ \
48.10 \ Try (Rewrite_Set ''expand_poly'' False) @@ \
48.11 \ Try (Repeat (Calculate ''TIMES'')) @@ \
49.1 --- a/test/Tools/isac/Test_Isac.thy Thu Aug 22 15:56:48 2019 +0200
49.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Aug 22 16:48:04 2019 +0200
49.3 @@ -517,7 +517,7 @@
49.4 Delete.thy <--- first_Knowledge_thy (*mv to Atools.thy*)
49.5 ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
49.6 Interpret.thy are generated (simplifies xml structure for theories)
49.7 - Script.thy
49.8 + Program.thy
49.9 Tools.thy
49.10 ListC.thy <--- first_Proglang_thy
49.11 --------------------------------------------------------------------------------
50.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Aug 22 15:56:48 2019 +0200
50.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Aug 22 16:48:04 2019 +0200
50.3 @@ -516,7 +516,7 @@
50.4 Delete.thy <--- first_Knowledge_thy (*mv to Atools.thy*)
50.5 ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
50.6 Interpret.thy are generated (simplifies xml structure for theories)
50.7 - Script.thy
50.8 + Program.thy
50.9 Tools.thy
50.10 ListC.thy <--- first_Proglang_thy
50.11 --------------------------------------------------------------------------------
51.1 --- a/test/Tools/isac/Test_Theory.thy Thu Aug 22 15:56:48 2019 +0200
51.2 +++ b/test/Tools/isac/Test_Theory.thy Thu Aug 22 16:48:04 2019 +0200
51.3 @@ -1,5 +1,5 @@
51.4 (* use this theory for tests before Build_Isac.thy has succeeded *)
51.5 -theory Test_Theory imports Isac.Script
51.6 +theory Test_Theory imports Isac.Program
51.7 begin
51.8 ML_file "~~/src/Tools/isac/library.sml"
51.9 (* ATTENTION: tests with CalcTreeTest, CalcTree do NOT work here, because Thy_Info.get_theory
52.1 --- a/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Thu Aug 22 15:56:48 2019 +0200
52.2 +++ b/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Thu Aug 22 16:48:04 2019 +0200
52.3 @@ -29,7 +29,7 @@
52.4 (*what to do if from 'pbls2file "../../xmldata/pbl/";' you get the error
52.5
52.6 ### pbl2file: id = ["Biegelinie"]
52.7 -*** Type unification failed: Clash of types "fun" and "Script.ID".
52.8 +*** Type unification failed: Clash of types "fun" and "Program.ID".
52.9 *** Type error in application: Incompatible operand type.
52.10 ***
52.11 *** Operator: Problem :: ID * ID list => ??'a
52.12 @@ -113,7 +113,7 @@
52.13 (*Const
52.14 ("Biegelinie.Biegelinie",
52.15 "("Real.real => "Real.real) => Tools.una") : Term.term
52.16 -..I.E. THE "Script.ID" _WAS_ ALREADY OCCUPIED BY A 'description'*)
52.17 +..I.E. THE "Program.ID" _WAS_ ALREADY OCCUPIED BY A 'description'*)
52.18
52.19
52.20 "----- ERROR Illegal reference to internal variable: 'Pure_' -----";