1.1 --- a/src/Tools/isac/Interpret/script.sml Thu Aug 22 15:56:48 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Aug 22 16:48:04 2019 +0200
1.3 @@ -103,21 +103,21 @@
1.4 (*.get argument of first stactic in a script for init_form.*)
1.5 fun get_stac thy (_ $ body) =
1.6 let
1.7 - fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a =
1.8 + fun get_t y (Const ("Program.Seq",_) $ e1 $ e2) a =
1.9 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.10 - | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ =
1.11 + | get_t y (Const ("Program.Seq",_) $ e1 $ e2 $ a) _ =
1.12 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.13 - | get_t y (Const ("Script.Try",_) $ e) a = get_t y e a
1.14 - | get_t y (Const ("Script.Try",_) $ e $ a) _ = get_t y e a
1.15 - | get_t y (Const ("Script.Repeat",_) $ e) a = get_t y e a
1.16 - | get_t y (Const ("Script.Repeat",_) $ e $ a) _ = get_t y e a
1.17 - | get_t y (Const ("Script.Or",_) $e1 $ e2) a =
1.18 + | get_t y (Const ("Program.Try",_) $ e) a = get_t y e a
1.19 + | get_t y (Const ("Program.Try",_) $ e $ a) _ = get_t y e a
1.20 + | get_t y (Const ("Program.Repeat",_) $ e) a = get_t y e a
1.21 + | get_t y (Const ("Program.Repeat",_) $ e $ a) _ = get_t y e a
1.22 + | get_t y (Const ("Program.Or",_) $e1 $ e2) a =
1.23 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.24 - | get_t y (Const ("Script.Or",_) $e1 $ e2 $ a) _ =
1.25 + | get_t y (Const ("Program.Or",_) $e1 $ e2 $ a) _ =
1.26 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.27 - | get_t y (Const ("Script.While",_) $ _ $ e) a = get_t y e a
1.28 - | get_t y (Const ("Script.While",_) $ _ $ e $ a) _ = get_t y e a
1.29 - | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_, _, e2)) a =
1.30 + | get_t y (Const ("Program.While",_) $ _ $ e) a = get_t y e a
1.31 + | get_t y (Const ("Program.While",_) $ _ $ e $ a) _ = get_t y e a
1.32 + | get_t y (Const ("Program.Letpar",_) $ e1 $ Abs (_, _, e2)) a =
1.33 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.34 (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
1.35 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.36 @@ -127,21 +127,21 @@
1.37 | get_t _ (Const ("If", _) $ _ $ _ $ _) _ = NONE
1.38 (*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*)
1.39
1.40 - | get_t _ (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a
1.41 - | get_t _ (Const ("Script.Rewrite",_) $ _ $ _ ) a = SOME a
1.42 - | get_t _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
1.43 - | get_t _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a
1.44 - | get_t _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ = SOME a
1.45 - | get_t _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ ) a = SOME a
1.46 - | get_t _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
1.47 - | get_t _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a
1.48 - | get_t _ (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a
1.49 - | get_t _ (Const ("Script.Calculate",_) $ _ ) a = SOME a
1.50 + | get_t _ (Const ("Program.Rewrite",_) $ _ $ _ $ a) _ = SOME a
1.51 + | get_t _ (Const ("Program.Rewrite",_) $ _ $ _ ) a = SOME a
1.52 + | get_t _ (Const ("Program.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
1.53 + | get_t _ (Const ("Program.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a
1.54 + | get_t _ (Const ("Program.Rewrite'_Set",_) $ _ $ _ $ a) _ = SOME a
1.55 + | get_t _ (Const ("Program.Rewrite'_Set",_) $ _ $ _ ) a = SOME a
1.56 + | get_t _ (Const ("Program.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
1.57 + | get_t _ (Const ("Program.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a
1.58 + | get_t _ (Const ("Program.Calculate",_) $ _ $ a) _ = SOME a
1.59 + | get_t _ (Const ("Program.Calculate",_) $ _ ) a = SOME a
1.60
1.61 - | get_t _ (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a
1.62 - | get_t _ (Const ("Script.Substitute",_) $ _ ) a = SOME a
1.63 + | get_t _ (Const ("Program.Substitute",_) $ _ $ a) _ = SOME a
1.64 + | get_t _ (Const ("Program.Substitute",_) $ _ ) a = SOME a
1.65
1.66 - | get_t _ (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE
1.67 + | get_t _ (Const ("Program.SubProblem",_) $ _ $ _) _ = NONE
1.68
1.69 | get_t _ _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
1.70 in get_t thy body Rule.e_term end
1.71 @@ -186,33 +186,33 @@
1.72 in (flat o (map (itm2arg itms))) pats end;
1.73
1.74 (* convert a script-tac 'stac' to 'tac' for users;
1.75 - for "Script.SubProblem" also create a 'tac_' for internal use. FIXME separate?
1.76 + for "Program.SubProblem" also create a 'tac_' for internal use. FIXME separate?
1.77 if stac is an initac, then convert to a 'tac_' (as required in appy).
1.78 arg ctree for pushing the thy specified in rootpbl into subpbls *)
1.79 -fun stac2tac_ _ thy (Const ("Script.Rewrite", _) $ thmID $ _ $ _) =
1.80 +fun stac2tac_ _ thy (Const ("Program.Rewrite", _) $ thmID $ _ $ _) =
1.81 let
1.82 val tid = HOLogic.dest_string thmID
1.83 in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid), Tactic.Empty_Tac_) end
1.84 - | stac2tac_ _ thy (Const ("Script.Rewrite'_Inst", _) $ sub $ thmID $ _ $ _) =
1.85 + | stac2tac_ _ thy (Const ("Program.Rewrite'_Inst", _) $ sub $ thmID $ _ $ _) =
1.86 let
1.87 val tid = HOLogic.dest_string thmID
1.88 in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid)), Tactic.Empty_Tac_) end
1.89 - | stac2tac_ _ _ (Const ("Script.Rewrite'_Set",_) $ rls $ _ $ _) =
1.90 + | stac2tac_ _ _ (Const ("Program.Rewrite'_Set",_) $ rls $ _ $ _) =
1.91 (Tactic.Rewrite_Set (HOLogic.dest_string rls), Tactic.Empty_Tac_)
1.92 - | stac2tac_ _ _ (Const ("Script.Rewrite'_Set'_Inst", _) $ sub $ rls $ _ $ _) =
1.93 + | stac2tac_ _ _ (Const ("Program.Rewrite'_Set'_Inst", _) $ sub $ rls $ _ $ _) =
1.94 (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls), Tactic.Empty_Tac_)
1.95 - | stac2tac_ _ _ (Const ("Script.Calculate", _) $ op_ $ _) =
1.96 + | stac2tac_ _ _ (Const ("Program.Calculate", _) $ op_ $ _) =
1.97 (Tactic.Calculate (HOLogic.dest_string op_), Tactic.Empty_Tac_)
1.98 - | stac2tac_ _ _ (Const ("Script.Take", _) $ t) = (Tactic.Take (Rule.term2str t), Tactic.Empty_Tac_)
1.99 - | stac2tac_ _ _ (Const ("Script.Substitute", _) $ isasub $ _) =
1.100 + | stac2tac_ _ _ (Const ("Program.Take", _) $ t) = (Tactic.Take (Rule.term2str t), Tactic.Empty_Tac_)
1.101 + | stac2tac_ _ _ (Const ("Program.Substitute", _) $ isasub $ _) =
1.102 (Tactic.Substitute ((Selem.subte2sube o TermC.isalist2list) isasub), Tactic.Empty_Tac_)
1.103 - | stac2tac_ _ thy (Const("Script.Check'_elementwise", _) $ _ $
1.104 + | stac2tac_ _ thy (Const("Program.Check'_elementwise", _) $ _ $
1.105 (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
1.106 (Tactic.Check_elementwise (Rule.term_to_string''' thy pred), Tactic.Empty_Tac_)
1.107 - | stac2tac_ _ _ (Const("Script.Or'_to'_List", _) $ _ ) = (Tactic.Or_to_List, Tactic.Empty_Tac_)
1.108 + | stac2tac_ _ _ (Const("Program.Or'_to'_List", _) $ _ ) = (Tactic.Or_to_List, Tactic.Empty_Tac_)
1.109
1.110 (*compare "| associate _ (Subproblem'" ..TODO: extract common code *)
1.111 - | stac2tac_ pt _ (stac as Const ("Script.SubProblem", _) $ spec' $ ags') =
1.112 + | stac2tac_ pt _ (stac as Const ("Program.SubProblem", _) $ spec' $ ags') =
1.113 let
1.114 val (dI, pI, mI) = LTool.dest_spec spec'
1.115 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
1.116 @@ -277,14 +277,14 @@
1.117 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
1.118 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
1.119 (case stac of
1.120 - (Const ("Script.Rewrite'_Inst", _) $ _ $ thmID_ $ _ $ f_) =>
1.121 + (Const ("Program.Rewrite'_Inst", _) $ _ $ thmID_ $ _ $ f_) =>
1.122 if thmID = HOLogic.dest_string thmID_
1.123 then
1.124 if f = f_
1.125 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.126 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
1.127 else ((*tracing"3### associate ..NotAss";*) NotAss)
1.128 - | (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ _ $ f_) =>
1.129 + | (Const ("Program.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ _ $ f_) =>
1.130 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
1.131 then if f = f_ then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.132 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
1.133 @@ -292,14 +292,14 @@
1.134 | _ => NotAss)
1.135 | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
1.136 (case stac of
1.137 - (Const ("Script.Rewrite", _) $ thmID_ $ _ $ f_) =>
1.138 + (Const ("Program.Rewrite", _) $ thmID_ $ _ $ f_) =>
1.139 if thmID = HOLogic.dest_string thmID_
1.140 then
1.141 if f = f_
1.142 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.143 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
1.144 else NotAss
1.145 - | (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_) =>
1.146 + | (Const ("Program.Rewrite'_Set", _) $ rls_ $ _ $ f_) =>
1.147 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
1.148 then
1.149 if f = f_
1.150 @@ -308,7 +308,7 @@
1.151 else NotAss
1.152 | _ => NotAss)
1.153 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
1.154 - (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_)) =
1.155 + (Const ("Program.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_)) =
1.156 if Rule.id_rls rls = HOLogic.dest_string rls_
1.157 then
1.158 if f = f_
1.159 @@ -316,7 +316,7 @@
1.160 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.161 else NotAss
1.162 | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
1.163 - (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_)) =
1.164 + (Const ("Program.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_)) =
1.165 if Rule.id_rls rls = HOLogic.dest_string rls_
1.166 then
1.167 if f = f_
1.168 @@ -324,7 +324,7 @@
1.169 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.170 else NotAss
1.171 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
1.172 - (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_)) =
1.173 + (Const ("Program.Rewrite'_Set", _) $ rls_ $ _ $ f_)) =
1.174 if Rule.id_rls rls = HOLogic.dest_string rls_
1.175 then
1.176 if f = f_
1.177 @@ -332,7 +332,7 @@
1.178 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.179 else NotAss
1.180 | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
1.181 - (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_)) =
1.182 + (Const ("Program.Rewrite'_Set", _) $ rls_ $ _ $ f_)) =
1.183 if Rule.id_rls rls = HOLogic.dest_string rls_
1.184 then
1.185 if f = f_
1.186 @@ -341,14 +341,14 @@
1.187 else NotAss
1.188 | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
1.189 (case stac of
1.190 - (Const ("Script.Calculate",_) $ op__ $ f_) =>
1.191 + (Const ("Program.Calculate",_) $ op__ $ f_) =>
1.192 if op_ = HOLogic.dest_string op__
1.193 then
1.194 if f = f_
1.195 then Ass (m, f', ctxt)
1.196 else Ass_Weak (m ,f', ctxt)
1.197 else NotAss
1.198 - | (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_) =>
1.199 + | (Const ("Program.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_) =>
1.200 let val thy = Celem.assoc_thy "Isac";
1.201 in
1.202 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
1.203 @@ -359,7 +359,7 @@
1.204 else Ass_Weak (m ,f', ctxt)
1.205 else NotAss
1.206 end
1.207 - | (Const ("Script.Rewrite'_Set",_) $ rls_ $ _ $ f_) =>
1.208 + | (Const ("Program.Rewrite'_Set",_) $ rls_ $ _ $ f_) =>
1.209 let val thy = Celem.assoc_thy "Isac";
1.210 in
1.211 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
1.212 @@ -372,15 +372,15 @@
1.213 end
1.214 | _ => NotAss)
1.215 | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
1.216 - (Const ("Script.Check'_elementwise",_) $ consts' $ _)) =
1.217 + (Const ("Program.Check'_elementwise",_) $ consts' $ _)) =
1.218 if consts = consts'
1.219 then Ass (m, consts_chkd, ctxt)
1.220 else NotAss
1.221 - | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Script.Or'_to'_List", _) $ _)) =
1.222 + | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Program.Or'_to'_List", _) $ _)) =
1.223 Ass (m, list, ctxt)
1.224 - | associate _ ctxt (m as Tactic.Take' term, (Const ("Script.Take", _) $ _)) = Ass (m, term, ctxt)
1.225 + | associate _ ctxt (m as Tactic.Take' term, (Const ("Program.Take", _) $ _)) = Ass (m, term, ctxt)
1.226 | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'),
1.227 - (Const ("Script.Substitute", _) $ _ $ t)) =
1.228 + (Const ("Program.Substitute", _) $ _ $ t)) =
1.229 if f = t then Ass (m, f', ctxt)
1.230 else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
1.231 if foldl and_ (true, map TermC.contains_Var subte)
1.232 @@ -393,9 +393,9 @@
1.233 SOME (t', _) => Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
1.234 | NONE => error "associate: Substitute' not applicable to val of Expr")
1.235
1.236 - (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)" ..TODO: extract common code *)
1.237 + (*compare "| stac2tac_ thy (Const ("Program.SubProblem",_)" ..TODO: extract common code *)
1.238 | associate pt _ (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
1.239 - (stac as Const ("Script.SubProblem", _) $ spec' $ ags')) =
1.240 + (stac as Const ("Program.SubProblem", _) $ spec' $ ags')) =
1.241 let
1.242 val (dI, pI, mI) = LTool.dest_spec spec'
1.243 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
1.244 @@ -479,14 +479,14 @@
1.245 val subs' = Selem.subst_to_subst' subs;
1.246 val sT' = type_of subs';
1.247 val fT = type_of f;
1.248 - val lhs = Const ("Script.Rewrite'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.249 + val lhs = Const ("Program.Rewrite'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.250 $ subs' $ HOLogic.mk_string thmID $ b $ f;
1.251 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.252 | rep_tac_ (Tactic.Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
1.253 let
1.254 val fT = type_of f;
1.255 val b = if put then @{term True} else @{term False};
1.256 - val lhs = Const ("Script.Rewrite", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.257 + val lhs = Const ("Program.Rewrite", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.258 $ HOLogic.mk_string thmID $ b $ f;
1.259 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.260 | rep_tac_ (Tactic.Rewrite_Set_Inst' (thy', _, subs, rls, f, (f', _))) =
1.261 @@ -495,20 +495,20 @@
1.262 val subs' = Selem.subst_to_subst' subs;
1.263 val sT' = type_of subs';
1.264 val fT = type_of f;
1.265 - val lhs = Const ("Script.Rewrite'_Set'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.266 + val lhs = Const ("Program.Rewrite'_Set'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.267 $ subs' $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
1.268 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.269 | rep_tac_ (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) =
1.270 let
1.271 val fT = type_of f;
1.272 val b = if put then @{term True} else @{term False};
1.273 - val lhs = Const ("Script.Rewrite'_Set", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.274 + val lhs = Const ("Program.Rewrite'_Set", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.275 $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
1.276 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.277 | rep_tac_ (Tactic.Calculate' (thy', op_, f, (f', _)))=
1.278 let
1.279 val fT = type_of f;
1.280 - val lhs = Const ("Script.Calculate",[HOLogic.stringT,fT] ---> fT) $ HOLogic.mk_string op_ $ f
1.281 + val lhs = Const ("Program.Calculate",[HOLogic.stringT,fT] ---> fT) $ HOLogic.mk_string op_ $ f
1.282 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.283 | rep_tac_ (Tactic.Check_elementwise' (_, _, (t', _))) = (Rule.Erule, (Rule.e_term, t'))
1.284 | rep_tac_ (Tactic.Subproblem' (_, _, _, _, _, t')) = (Rule.Erule, (Rule.e_term, t'))