1.1 --- a/src/Tools/isac/Interpret/script.sml Wed Jul 24 11:30:59 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Wed Jul 24 15:28:11 2019 +0200
1.3 @@ -8,7 +8,7 @@
1.4
1.5 type step = Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list
1.6 datatype ass = Ass of Tactic.T * term | AssWeak of Tactic.T * term | NotAss;
1.7 - val assod: Ctree.ctree -> 'a -> Tactic.T -> term -> ass
1.8 + val associate: Ctree.ctree -> 'a -> Tactic.T -> term -> ass
1.9
1.10 (* can these functions be local to Lucin or part of LItools ? *)
1.11 val sel_rules : Ctree.ctree -> Ctree.pos' -> Tactic.input list
1.12 @@ -208,7 +208,7 @@
1.13 (Tactic.Check_elementwise (Rule.term_to_string''' thy pred), Tactic.Empty_Tac_)
1.14 | stac2tac_ _ _ (Const("Script.Or'_to'_List", _) $ _ ) = (Tactic.Or_to_List, Tactic.Empty_Tac_)
1.15
1.16 - (*compare "| assod _ (Subproblem'" ..TODO: extract common code *)
1.17 + (*compare "| associate _ (Subproblem'" ..TODO: extract common code *)
1.18 | stac2tac_ pt _ (stac as Const ("Script.SubProblem", _) $
1.19 (Const ("Product_Type.Pair", _) $ dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags') =
1.20 let
1.21 @@ -250,7 +250,7 @@
1.22
1.23 datatype ass =
1.24 Ass of
1.25 - Tactic.T * (* SubProblem gets args instantiated in assod *)
1.26 + Tactic.T * (* SubProblem gets args instantiated in associate *)
1.27 term (* for itr_arg, result in ets *)
1.28 | AssWeak of
1.29 Tactic.T *
1.30 @@ -274,61 +274,61 @@
1.31 AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
1.32 NotAss : e.g. thmID in stac/=/thmID in m (not =)
1.33 *)
1.34 -fun assod _ _ (m as Tactic.Rewrite_Inst' (_, _, _, _, _, thm'' as (thmID, _), f, (f', _))) stac =
1.35 +fun associate _ _ (m as Tactic.Rewrite_Inst' (_, _, _, _, _, thm'' as (thmID, _), f, (f', _))) stac =
1.36 (case stac of
1.37 (Const ("Script.Rewrite'_Inst", _) $ _ $ thmID_ $ _ $ f_) =>
1.38 if thmID = HOLogic.dest_string thmID_
1.39 then
1.40 if f = f_
1.41 - then ((*tracing"3### assod ..Ass";*) Ass (m,f'))
1.42 - else ((*tracing"3### assod ..AssWeak";*) AssWeak(m, f'))
1.43 - else ((*tracing"3### assod ..NotAss";*) NotAss)
1.44 + then ((*tracing"3### associate ..Ass";*) Ass (m,f'))
1.45 + else ((*tracing"3### associate ..AssWeak";*) AssWeak(m, f'))
1.46 + else ((*tracing"3### associate ..NotAss";*) NotAss)
1.47 | (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ _ $ f_) =>
1.48 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
1.49 then if f = f_ then Ass (m,f') else AssWeak (m,f')
1.50 else NotAss
1.51 | _ => NotAss)
1.52 - | assod _ _ (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', _))) stac =
1.53 + | associate _ _ (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', _))) stac =
1.54 (case stac of
1.55 (Const ("Script.Rewrite", _) $ thmID_ $ _ $ f_) =>
1.56 - ((*tracing ("3### assod: stac = " ^ ter2str t);
1.57 - tracing ("3### assod: f(m)= " ^ term2str f);*)
1.58 + ((*tracing ("3### associate: stac = " ^ ter2str t);
1.59 + tracing ("3### associate: f(m)= " ^ term2str f);*)
1.60 if thmID = HOLogic.dest_string thmID_
1.61 then
1.62 if f = f_
1.63 - then ((*tracing"3### assod ..Ass";*) Ass (m,f'))
1.64 + then ((*tracing"3### associate ..Ass";*) Ass (m,f'))
1.65 else
1.66 - ((*tracing"### assod ..AssWeak";
1.67 - tracing("### assod: f(m) = " ^ term2str f);
1.68 - tracing("### assod: f(stac)= " ^ term2str f_)*)
1.69 + ((*tracing"### associate ..AssWeak";
1.70 + tracing("### associate: f(m) = " ^ term2str f);
1.71 + tracing("### associate: f(stac)= " ^ term2str f_)*)
1.72 AssWeak (m,f'))
1.73 - else ((*tracing"3### assod ..NotAss";*) NotAss))
1.74 + else ((*tracing"3### associate ..NotAss";*) NotAss))
1.75 | (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_) =>
1.76 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
1.77 then if f = f_ then Ass (m, f') else AssWeak (m, f')
1.78 else NotAss
1.79 | _ => NotAss)
1.80 - | assod _ _ (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', _)))
1.81 + | associate _ _ (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', _)))
1.82 (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_) =
1.83 if Rule.id_rls rls = HOLogic.dest_string rls_
1.84 then if f = f_ then Ass (m, f') else AssWeak (m ,f')
1.85 else NotAss
1.86 - | assod _ _ (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f',_)))
1.87 + | associate _ _ (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f',_)))
1.88 (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_) =
1.89 if Rule.id_rls rls = HOLogic.dest_string rls_
1.90 then if f = f_ then Ass (m, f') else AssWeak (m, f')
1.91 else NotAss
1.92 - | assod _ _ (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _)))
1.93 + | associate _ _ (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _)))
1.94 (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_) =
1.95 if Rule.id_rls rls = HOLogic.dest_string rls_
1.96 then if f = f_ then Ass (m, f') else AssWeak (m, f')
1.97 else NotAss
1.98 - | assod _ _ (m as Tactic.Detail_Set' (_, _, rls, f, (f', _)))
1.99 + | associate _ _ (m as Tactic.Detail_Set' (_, _, rls, f, (f', _)))
1.100 (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_) =
1.101 if Rule.id_rls rls = HOLogic.dest_string rls_
1.102 then if f = f_ then Ass (m, f') else AssWeak (m, f')
1.103 else NotAss
1.104 - | assod _ _ (m as Tactic.Calculate' (_, op_, f, (f', _))) stac =
1.105 + | associate _ _ (m as Tactic.Calculate' (_, op_, f, (f', _))) stac =
1.106 (case stac of
1.107 (Const ("Script.Calculate",_) $ op__ $ f_) =>
1.108 if op_ = HOLogic.dest_string op__
1.109 @@ -351,28 +351,28 @@
1.110 else NotAss
1.111 end
1.112 | _ => NotAss)
1.113 - | assod _ _ (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)))
1.114 + | associate _ _ (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)))
1.115 (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
1.116 if consts = consts'
1.117 then Ass (m, consts_chkd)
1.118 else NotAss
1.119 - | assod _ _ (m as Tactic.Or_to_List' (_, list)) (Const ("Script.Or'_to'_List", _) $ _) = Ass (m, list)
1.120 - | assod _ _ (m as Tactic.Take' term) (Const ("Script.Take", _) $ _) = Ass (m, term)
1.121 - | assod _ _ (m as Tactic.Substitute' (ro, erls, subte, f, f')) (Const ("Script.Substitute", _) $ _ $ t) =
1.122 + | associate _ _ (m as Tactic.Or_to_List' (_, list)) (Const ("Script.Or'_to'_List", _) $ _) = Ass (m, list)
1.123 + | associate _ _ (m as Tactic.Take' term) (Const ("Script.Take", _) $ _) = Ass (m, term)
1.124 + | associate _ _ (m as Tactic.Substitute' (ro, erls, subte, f, f')) (Const ("Script.Substitute", _) $ _ $ t) =
1.125 if f = t then Ass (m, f')
1.126 else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
1.127 if foldl and_ (true, map TermC.contains_Var subte)
1.128 then
1.129 let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
1.130 - in if t = t' then error "assod: Substitute' not applicable to val of Expr"
1.131 + in if t = t' then error "associate: Substitute' not applicable to val of Expr"
1.132 else Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t')
1.133 end
1.134 else (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of
1.135 SOME (t', _) => Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t')
1.136 - | NONE => error "assod: Substitute' not applicable to val of Expr")
1.137 + | NONE => error "associate: Substitute' not applicable to val of Expr")
1.138
1.139 (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)" ..TODO: extract common code *)
1.140 - | assod pt _ (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _))
1.141 + | associate pt _ (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _))
1.142 (stac as Const ("Script.SubProblem", _) $ (Const ("Product_Type.Pair", _) $
1.143 dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags') =
1.144 let
1.145 @@ -409,7 +409,7 @@
1.146 then Ass (Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f), f)
1.147 else NotAss
1.148 end
1.149 - | assod _ _ m _ =
1.150 + | associate _ _ m _ =
1.151 (if (!trace_script)
1.152 then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"
1.153 ^ "@@@ tac_ = " ^ Tactic.tac_2str m)