1.1 --- a/src/Tools/isac/Interpret/script.sml Thu Sep 26 17:47:10 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Tue Oct 01 10:47:25 2019 +0200
1.3 @@ -143,17 +143,17 @@
1.4 for "Prog_Tac.SubProblem" also create a 'tac_' for internal use. FIXME separate?
1.5 if stac is an initac, then convert to a 'tac_' (as required in appy).
1.6 arg ctree for pushing the thy specified in rootpbl into subpbls *)
1.7 -fun stac2tac_ _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _ $ _) =
1.8 +fun stac2tac_ _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
1.9 let
1.10 val tid = HOLogic.dest_string thmID
1.11 in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid), Tactic.Empty_Tac_) end
1.12 - | stac2tac_ _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _ $ _) =
1.13 + | stac2tac_ _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
1.14 let
1.15 val tid = HOLogic.dest_string thmID
1.16 in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid)), Tactic.Empty_Tac_) end
1.17 - | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _ $ _) =
1.18 + | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
1.19 (Tactic.Rewrite_Set (HOLogic.dest_string rls), Tactic.Empty_Tac_)
1.20 - | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _ $ _) =
1.21 + | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =
1.22 (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls), Tactic.Empty_Tac_)
1.23 | stac2tac_ _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
1.24 (Tactic.Calculate (HOLogic.dest_string op_), Tactic.Empty_Tac_)
1.25 @@ -231,14 +231,14 @@
1.26 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
1.27 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
1.28 (case stac of
1.29 - (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ _ $ f_) =>
1.30 + (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) =>
1.31 if thmID = HOLogic.dest_string thmID_
1.32 then
1.33 if f = f_
1.34 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.35 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
1.36 else ((*tracing"3### associate ..NotAss";*) NotAss)
1.37 - | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ _ $ f_) =>
1.38 + | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>
1.39 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
1.40 then if f = f_ then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.41 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
1.42 @@ -246,14 +246,14 @@
1.43 | _ => NotAss)
1.44 | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
1.45 (case stac of
1.46 - (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ _ $ f_) =>
1.47 + (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) =>
1.48 if thmID = HOLogic.dest_string thmID_
1.49 then
1.50 if f = f_
1.51 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.52 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
1.53 else NotAss
1.54 - | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ _ $ f_) =>
1.55 + | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>
1.56 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
1.57 then
1.58 if f = f_
1.59 @@ -262,7 +262,7 @@
1.60 else NotAss
1.61 | _ => NotAss)
1.62 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
1.63 - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_)) =
1.64 + (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
1.65 if Rule.id_rls rls = HOLogic.dest_string rls_
1.66 then
1.67 if f = f_
1.68 @@ -270,7 +270,7 @@
1.69 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.70 else NotAss
1.71 | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
1.72 - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_)) =
1.73 + (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
1.74 if Rule.id_rls rls = HOLogic.dest_string rls_
1.75 then
1.76 if f = f_
1.77 @@ -278,7 +278,7 @@
1.78 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.79 else NotAss
1.80 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
1.81 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ _ $ f_)) =
1.82 + (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
1.83 if Rule.id_rls rls = HOLogic.dest_string rls_
1.84 then
1.85 if f = f_
1.86 @@ -286,7 +286,7 @@
1.87 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.88 else NotAss
1.89 | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
1.90 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ _ $ f_)) =
1.91 + (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
1.92 if Rule.id_rls rls = HOLogic.dest_string rls_
1.93 then
1.94 if f = f_
1.95 @@ -302,7 +302,7 @@
1.96 then Ass (m, f', ctxt)
1.97 else Ass_Weak (m ,f', ctxt)
1.98 else NotAss
1.99 - | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_) =>
1.100 + | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
1.101 let val thy = Celem.assoc_thy "Isac_Knowledge";
1.102 in
1.103 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
1.104 @@ -313,7 +313,7 @@
1.105 else Ass_Weak (m ,f', ctxt)
1.106 else NotAss
1.107 end
1.108 - | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ _ $ f_) =>
1.109 + | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
1.110 let val thy = Celem.assoc_thy "Isac_Knowledge";
1.111 in
1.112 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
1.113 @@ -429,35 +429,31 @@
1.114
1.115 fun rep_tac_ (Tactic.Rewrite_Inst' (thy', _, _, _, subs, (thmID, _), f, (f', _))) =
1.116 let
1.117 - val b = @{term False};
1.118 val subs' = Selem.subst_to_subst' subs;
1.119 val sT' = type_of subs';
1.120 val fT = type_of f;
1.121 - val lhs = Const ("Prog_Tac.Rewrite'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.122 - $ subs' $ HOLogic.mk_string thmID $ b $ f;
1.123 + val lhs = Const ("Prog_Tac.Rewrite'_Inst", [sT', HOLogic.stringT, fT] ---> fT)
1.124 + $ subs' $ HOLogic.mk_string thmID $ f;
1.125 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.126 - | rep_tac_ (Tactic.Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
1.127 + | rep_tac_ (Tactic.Rewrite' (thy', _, _, _, (thmID, _), f, (f', _)))=
1.128 let
1.129 val fT = type_of f;
1.130 - val b = if put then @{term True} else @{term False};
1.131 - val lhs = Const ("Prog_Tac.Rewrite", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.132 - $ HOLogic.mk_string thmID $ b $ f;
1.133 + val lhs = Const ("Prog_Tac.Rewrite", [HOLogic.stringT, fT] ---> fT)
1.134 + $ HOLogic.mk_string thmID $ f;
1.135 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.136 | rep_tac_ (Tactic.Rewrite_Set_Inst' (thy', _, subs, rls, f, (f', _))) =
1.137 let
1.138 - val b = @{term False};
1.139 val subs' = Selem.subst_to_subst' subs;
1.140 val sT' = type_of subs';
1.141 val fT = type_of f;
1.142 - val lhs = Const ("Prog_Tac.Rewrite'_Set'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.143 - $ subs' $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
1.144 + val lhs = Const ("Prog_Tac.Rewrite'_Set'_Inst", [sT', HOLogic.stringT, fT] ---> fT)
1.145 + $ subs' $ HOLogic.mk_string (Rule.id_rls rls) $ f;
1.146 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.147 - | rep_tac_ (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) =
1.148 + | rep_tac_ (Tactic.Rewrite_Set' (thy', _, rls, f, (f', _))) =
1.149 let
1.150 val fT = type_of f;
1.151 - val b = if put then @{term True} else @{term False};
1.152 - val lhs = Const ("Prog_Tac.Rewrite'_Set", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.153 - $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
1.154 + val lhs = Const ("Prog_Tac.Rewrite'_Set", [HOLogic.stringT, fT] ---> fT)
1.155 + $ HOLogic.mk_string (Rule.id_rls rls) $ f;
1.156 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.157 | rep_tac_ (Tactic.Calculate' (thy', op_, f, (f', _)))=
1.158 let
1.159 @@ -642,21 +638,21 @@
1.160 fun handle_leaf call thy srls E a v t =
1.161 (*WN050916 'upd_env_opt' is a blind copy from previous version*)
1.162 case Prog_Tac.subst_stacexpr E a v t of
1.163 - (a', Celem.STac stac) => (*script-tactic*)
1.164 + (a', Celem.STac stac) => (* Prog_Tac *)
1.165 let val stac' =
1.166 Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
1.167 in
1.168 (if (! trace_script)
1.169 - then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t^"' ---> STac '" ^ Rule.term2str stac ^"'")
1.170 + then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> STac '" ^ Rule.term2str stac ^ "'")
1.171 else ();
1.172 (a', Celem.STac stac'))
1.173 end
1.174 - | (a', Celem.Expr lexpr) => (*leaf-expression*)
1.175 + | (a', Celem.Expr lexpr) => (* Prog_Expr *)
1.176 let val lexpr' =
1.177 Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
1.178 in
1.179 (if (! trace_script)
1.180 - then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t^"' ---> Expr '" ^ Rule.term2str lexpr'^"'")
1.181 + then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
1.182 else ();
1.183 (a', Celem.Expr lexpr')) (*lexpr' is the value of the Expr*)
1.184 end;