1 (* Title: ProgLang/Auto_Prog
2 Author: Walther Neuper, Aug.2019
3 (c) due to copyright terms
6 theory Auto_Prog imports Prog_Tac Tactical begin
9 The tactics Rewrite_Set* create ONE step in a calculation by application of usually
10 MORE than one theorem (here called "rule").
11 However, students can request details of rewriting down to single applications of theorems.
12 For accomplishing such requests, a program is auto-generated from the items of a rule-set.
15 subsection \<open>consts for programs automatically built from rules\<close>
17 partial_function (tailrec) auto_generated :: "'z \<Rightarrow> 'z"
18 where "auto_generated t_t = t_t"
19 partial_function (tailrec) auto_generated_inst :: "'z \<Rightarrow> real \<Rightarrow> 'z"
20 where "auto_generated_inst t_t v = t_t"
23 subsection \<open>TODO: code for above\<close>
26 signature AUTO_GERNERATE_PROGRAM =
28 val contain_bdv: Rule.rule list -> bool
29 val contains_bdv: thm -> bool
30 val subst_typs: term -> typ -> typ -> term
31 val pblterm: ThyC.id -> Probl_Def.id -> term
32 val pbltermPIDE: ThyC.id -> Probl_Def.id -> term
33 val subpbl: string -> string list -> term
34 val stacpbls: term -> term list
35 val op_of_calc: term -> string
36 val get_calcs: theory -> term -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
37 val prep_rls: theory -> Rule_Set.T -> Rule_Set.T (*ren insert*)
38 val gen: theory -> term -> Rule_Set.T -> term
39 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
41 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
42 val subst_typ: string -> typ -> term list -> (typ * typ) list
43 val is_calc: term -> bool
44 val rule2stac: theory -> Rule.rule -> term
45 val rule2stac_inst: theory -> Rule.rule -> term
46 val #> : term list -> term
47 val rules2scr_Rls : theory -> Rule.rule list -> term
48 val rules2scr_Seq : theory -> Rule.rule list -> term
49 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
52 structure Auto_Prog(**): AUTO_GERNERATE_PROGRAM(**) =
56 (** build up a program from rules **)
58 (* make the term 'Subproblem (domID, pblID)' to a formula for frontend;
59 needs to be here after def. Subproblem in Prog_Tac.thy *)
60 val subpbl_t $ (pair_t $ _ $ _) = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac}))
61 "Subproblem (''Isac_Knowledge'',[''equation'',''univar''])"
63 (Thm.term_of o the o (TermC.parse @{theory Prog_Tac})) "Problem (''Isac_Knowledge'',[''equation'',''univar''])"
65 fun subpbl domID pblID =
66 subpbl_t $ (pair_t $ HOLogic.mk_string domID $
67 list_comb (Syntax.const @{const_syntax Char}, map HOLogic.mk_string pblID));
68 fun pblterm domID pblID =
69 pbl_t $ (pair_t $ HOLogic.mk_string domID $
70 list_comb (Syntax.const @{const_syntax Char}, map HOLogic.mk_string pblID));
71 fun pbltermPIDE domID pblID =
72 pair_t $ HOLogic.mk_string domID $
73 list_comb (Syntax.const @{const_syntax Char}, map HOLogic.mk_string pblID);
75 (* fetch tactics from a program omitting tacticals like While, Repeat,.. *)
76 fun stacpbls (_ $ body) =
78 fun scan (Const ("HOL.Let", _) $ e $ (Abs (_, _, b))) = (scan e) @ (scan b)
79 | scan (Const ("Tactical.If", _) $ _ $ e1 $ e2) = (scan e1) @ (scan e2)
80 | scan (Const ("Tactical.While", _) $ _ $ e $ _) = scan e
81 | scan (Const ("Tactical.While", _) $ _ $ e) = scan e
82 | scan (Const ("Tactical.Repeat", _) $ e $ _) = scan e
83 | scan (Const ("Tactical.Repeat", _) $ e) = scan e
84 | scan (Const ("Tactical.Try", _) $ e $ _) = scan e
85 | scan (Const ("Tactical.Try", _) $ e) = scan e
86 | scan (Const ("Tactical.Or", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
87 | scan (Const ("Tactical.Or", _) $ e1 $ e2) = (scan e1) @ (scan e2)
88 | scan (Const ("Tactical.Chain", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
89 | scan (Const ("Tactical.Chain", _) $ e1 $ e2) = (scan e1) @ (scan e2)
90 | scan t = case Prog_Tac.eval_leaf [] NONE TermC.empty t of
91 (Program.Tac _, _) => [t] | (Program.Expr _, _) => []
92 in ((distinct op =) o scan) body end
93 | stacpbls t = raise ERROR ("fun stacpbls not applicable to '" ^ UnparseC.term t ^ "'")
95 (* get operators out of a program *)
96 fun is_calc (Const ("Prog_Tac.Calculate",_) $ _) = true
97 | is_calc (Const ("Prog_Tac.Calculate",_) $ _ $ _) = true
99 fun op_of_calc (Const ("Prog_Tac.Calculate",_) $ op_) = HOLogic.dest_string op_
100 | op_of_calc (Const ("Prog_Tac.Calculate",_) $ op_ $ _) = HOLogic.dest_string op_
101 | op_of_calc t = raise ERROR ("op_of_calc called with " ^ UnparseC.term t);
102 fun get_calcs thy sc =
107 |> (assoc_calc' thy |> map);
109 (** build up a program from rules **)
111 (* transform type rule to a term *)
112 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body are inconsistent !!!*)
113 val (FunID_Term $ _) = Program.prep_program @{thm auto_generated.simps}
114 val (FunID_Term_Bdv $ _) = Program.prep_program @{thm auto_generated_inst.simps}
115 val Repeat $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
116 "Repeat (Rewrite ''real_diff_minus'' t)";
117 val Try $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
118 "Try (Rewrite ''real_diff_minus'' t)";
119 val Cal $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
120 "Calculate ''PLUS''";
121 val Ca1 $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
122 "Calculate1 ''PLUS''";
123 val Rew $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
124 "Rewrite ''real_diff_minus'' t";
125 (*this is specific to FunHead_inst ...*)
126 val Rew_Inst $ Subs $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
127 "Rewrite_Inst [(''bdv'',v)] ''real_diff_minus''";
128 val Rew_Set $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
129 "Rewrite_Set ''real_diff_minus''";
130 val Rew_Set_Inst $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
131 "Rewrite_Set_Inst [(''bdv'',v)] ''real_diff_minus''";
132 val SEq $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
133 " ((Try (Repeat (Rewrite ''real_diff_minus''))) #> \
134 \ (Try (Repeat (Rewrite ''add.commute''))) #> \
135 \ (Try (Repeat (Rewrite ''mult_commute'')))) t";
137 fun rule2stac _ (Rule.Thm (thmID, _)) = Try $ (Repeat $ (Rew $ HOLogic.mk_string thmID))
138 | rule2stac thy (Rule.Eval (c, _)) = Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
139 | rule2stac thy (Rule.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ HOLogic.mk_string (assoc_calc thy c)))
140 | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule_Set.id rls))
141 | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule.to_string r ^ "\"");
142 fun rule2stac_inst _ (Rule.Thm (thmID, _)) =
143 Try $ (Repeat $ (Rew_Inst $ Subs $ HOLogic.mk_string thmID))
144 | rule2stac_inst thy (Rule.Eval (c, _)) =
145 Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
146 | rule2stac_inst thy (Rule.Cal1 (c, _)) =
147 Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
148 | rule2stac_inst _ (Rule.Rls_ rls) =
149 Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule_Set.id rls))
150 | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule.to_string r ^ "\"");
152 (*for appropriate nesting take stacs in _reverse_ order*)
153 fun op #>@ sts [s] = SEq $ s $ sts
154 | op #>@ sts (s::ss) = op #>@ (SEq $ s $ sts) ss
156 raise ERROR ("fun #>@ not applicable to \"" ^ UnparseC.term t ^ "\" \"" ^ UnparseC.terms ts ^ "\"");
158 | #> [s1, s2] = SEq $ s1 $ s2
159 | #> stacs = case rev stacs of
160 s3 :: s2 :: ss => op #>@ (SEq $ s2 $ s3) ss
161 | ts => raise ERROR ("fun #> not applicable to \"" ^ UnparseC.terms ts ^ "\"")
163 val contains_bdv = not o null o filter TermC.is_bdv o TermC.ids2str o Thm.prop_of;
165 (* does a rule contain a 'bdv'; descend recursively into Rls_ *)
166 fun contain_bdv [] = false
167 | contain_bdv (Rule.Thm (_, thm) :: rs) =
168 if (not o contains_bdv) thm
171 | contain_bdv (Rule.Eval _ :: rs) = contain_bdv rs
172 | contain_bdv (Rule.Cal1 _ :: rs) = contain_bdv rs
173 | contain_bdv (Rule.Rls_ rls :: rs) =
174 contain_bdv (Rule_Set.get_rules rls) orelse contain_bdv rs
175 | contain_bdv (r :: _) =
176 raise ERROR ("contain_bdv called with [" ^ Rule.id r ^ ",...]");
178 (* filter Frees for free_str and pair their respective types with typ *)
179 fun subst_typ free_str typ frees =
181 val vars_v = filter (fn t => curry op = (t |> dest_Free |> fst) free_str) frees
182 val typs_v = map (fn t => (t |> dest_Free |> snd)) vars_v
184 map (fn T => (T, typ)) typs_v
186 (* instantiate typs in Prog auto_generated or auto_generated_ins for args "t_t", "v" *)
187 fun subst_typs prog typ_t typ_bdv =
189 val args = Program.formal_args prog
190 val frees = TermC.vars prog
191 val prog' = subst_atomic_types (subst_typ "t_t" typ_t frees) prog
196 else (* auto_generated_inst has second argument "v" *)
197 subst_atomic_types (subst_typ "v" typ_bdv frees) prog'
200 fun rules2scr_Rls thy rules =
202 then FunID_Term_Bdv $ (Repeat $ (((op #> o (map (rule2stac_inst thy))) rules) $ TermC.empty))
203 else FunID_Term $ (Repeat $ (((op #> o (map (rule2stac thy))) rules) $ TermC.empty));
204 fun rules2scr_Seq thy rules =
206 then FunID_Term_Bdv $ (((op #> o (map (rule2stac_inst thy))) rules) $ TermC.empty)
207 else FunID_Term $ (((op #> o (map (rule2stac thy))) rules) $ TermC.empty);
209 (* REPLACED BY Auto_Prog.gen:
210 prepare the input for an rls for use:
211 # generate a program for stepwise execution of the rls
212 # filter the operators for Eval out of the script ?WN111014?
213 use this function while storing (TODO integrate..) into KEStore_Elems.add_rlss
215 fun prep_rls _ Rule_Set.Empty = raise ERROR "prep_rls: not required for Erls"
216 | prep_rls thy (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
218 val sc = (rules2scr_Rls thy rules)
220 Rule_Def.Repeat {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
221 calc = get_calcs thy sc,
222 rules = rules, errpatts = errpatts,
223 scr = Rule.Empty_Prog (*Rule.Prog sc AD-HOC REPLACED BY Auto_Prog.gen*)} end
224 | prep_rls thy (Rule_Set.Sequence {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
226 val sc = (rules2scr_Seq thy rules)
228 Rule_Set.Sequence {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
229 calc = get_calcs thy sc,
230 rules = rules, errpatts = errpatts,
231 scr = Rule.Empty_Prog (*Rule.Prog sc AD-HOC REPLACED BY Auto_Prog.gen*)} end
232 | prep_rls _ (Rule_Set.Rrls {id, ...}) =
233 raise ERROR ("prep_rls: not required for Rrls \"" ^ id ^ "\"");
235 (* on the fly generate a Prog from an rls for Detail_Step.go.
236 Types are not precise, but these are not required by LI.
237 Argument "thy" is only required for lookup in Know_Store.
241 val prog = case rls of
242 Rule_Def.Repeat {rules, ...} => rules2scr_Rls thy rules
243 | Rule_Set.Sequence {rules, ...} => rules2scr_Seq thy rules
244 | _ => raise ERROR ("Auto_Prog.gen: not for rule-set \"" ^ Rule_Set.id rls ^ "\"")
246 subst_typs prog (type_of t) (TermC.guess_bdv_typ t)