1 (* Title: ProgLang/Auto_Prog
2 Author: Walther Neuper, Aug.2019
3 (c) due to copyright terms
6 theory Auto_Prog imports Program 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: Rule.domID -> Celem.pblID -> term
32 val subpbl: string -> string list -> term
33 val stacpbls: term -> term list
34 val op_of_calc: term -> string
35 val get_calcs: theory -> term -> (Rule.prog_calcID * (Rule.calID * Rule.eval_fn)) list
36 val prep_rls: theory -> Rule.rls -> Rule.rls (*ren insert*)
37 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
39 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
40 val subst_typ: string -> typ -> term list -> (typ * typ) list
41 val is_calc: term -> bool
42 val rule2stac: theory -> Rule.rule -> term
43 val rule2stac_inst: theory -> Rule.rule -> term
44 val #> : term list -> term
45 val rules2scr_Rls : theory -> Rule.rule list -> term
46 val rules2scr_Seq : theory -> Rule.rule list -> term
47 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
50 structure Auto_Prog(**): AUTO_GERNERATE_PROGRAM(**) =
54 (** build up a program from rules **)
56 (* make the term 'Subproblem (domID, pblID)' to a formula for frontend;
57 needs to be here after def. Subproblem in Prog_Tac.thy *)
58 val subpbl_t $ (pair_t $ _ $ _) = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac}))
59 "Subproblem (''Isac_Knowledge'',[''equation'',''univar''])"
61 (Thm.term_of o the o (TermC.parse @{theory Prog_Tac})) "Problem (''Isac_Knowledge'',[''equation'',''univar''])"
63 fun subpbl domID pblID =
64 subpbl_t $ (pair_t $ HOLogic.mk_string domID $
65 list_comb (Syntax.const @{const_syntax Char}, map HOLogic.mk_string pblID));
66 fun pblterm domID pblID =
67 pbl_t $ (pair_t $ HOLogic.mk_string domID $
68 list_comb (Syntax.const @{const_syntax Char}, map HOLogic.mk_string pblID));
70 (* fetch tactics from a program omitting tacticals like While, Repeat,.. *)
71 fun stacpbls (_ $ body) =
73 fun scan (Const ("HOL.Let", _) $ e $ (Abs (_, _, b))) = (scan e) @ (scan b)
74 | scan (Const ("Tactical.If", _) $ _ $ e1 $ e2) = (scan e1) @ (scan e2)
75 | scan (Const ("Tactical.While", _) $ _ $ e $ _) = scan e
76 | scan (Const ("Tactical.While", _) $ _ $ e) = scan e
77 | scan (Const ("Tactical.Repeat", _) $ e $ _) = scan e
78 | scan (Const ("Tactical.Repeat", _) $ e) = scan e
79 | scan (Const ("Tactical.Try", _) $ e $ _) = scan e
80 | scan (Const ("Tactical.Try", _) $ e) = scan e
81 | scan (Const ("Tactical.Or", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
82 | scan (Const ("Tactical.Or", _) $ e1 $ e2) = (scan e1) @ (scan e2)
83 | scan (Const ("Tactical.Chain", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
84 | scan (Const ("Tactical.Chain", _) $ e1 $ e2) = (scan e1) @ (scan e2)
85 | scan t = case Prog_Tac.subst_stacexpr [] NONE Rule.e_term t of
86 (_, Celem.STac _) => [t] | (_, Celem.Expr _) => []
87 in (distinct o scan) body end
88 | stacpbls t = raise ERROR ("fun stacpbls not applicable to '" ^ Rule.term2str t ^ "'")
90 (* get operators out of a program *)
91 fun is_calc (Const ("Prog_Tac.Calculate",_) $ _) = true
92 | is_calc (Const ("Prog_Tac.Calculate",_) $ _ $ _) = true
94 fun op_of_calc (Const ("Prog_Tac.Calculate",_) $ op_) = HOLogic.dest_string op_
95 | op_of_calc (Const ("Prog_Tac.Calculate",_) $ op_ $ _) = HOLogic.dest_string op_
96 | op_of_calc t = error ("op_of_calc called with " ^ Rule.term2str t);
97 fun get_calcs thy sc =
102 |> (assoc_calc' thy |> map);
104 (** build up a program from rules **)
106 (* transform type rule to a term *)
107 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body are inconsistent !!!*)
108 val (FunID_Term $ _) = Program.prep_program @{thm auto_generated.simps}
109 val (FunID_Term_Bdv $ _) = Program.prep_program @{thm auto_generated_inst.simps}
110 val Repeat $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
111 "Repeat (Rewrite ''real_diff_minus'' t)";
112 val Try $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
113 "Try (Rewrite ''real_diff_minus'' t)";
114 val Cal $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
115 "Calculate ''PLUS''";
116 val Ca1 $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
117 "Calculate1 ''PLUS''";
118 val Rew $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
119 "Rewrite ''real_diff_minus'' t";
120 (*this is specific to FunHead_inst ...*)
121 val Rew_Inst $ Subs $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
122 "Rewrite_Inst [(''bdv'',v)] ''real_diff_minus''";
123 val Rew_Set $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
124 "Rewrite_Set ''real_diff_minus''";
125 val Rew_Set_Inst $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
126 "Rewrite_Set_Inst [(''bdv'',v)] ''real_diff_minus''";
127 val SEq $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
128 " ((Try (Repeat (Rewrite ''real_diff_minus''))) #> \
129 \ (Try (Repeat (Rewrite ''add_commute''))) #> \
130 \ (Try (Repeat (Rewrite ''mult_commute'')))) t";
132 fun rule2stac _ (Rule.Thm (thmID, _)) = Try $ (Repeat $ (Rew $ HOLogic.mk_string thmID))
133 | rule2stac thy (Rule.Calc (c, _)) = Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
134 | rule2stac thy (Rule.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ HOLogic.mk_string (assoc_calc thy c)))
135 | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule.id_rls rls))
136 | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule.rule2str r ^ "\"");
137 fun rule2stac_inst _ (Rule.Thm (thmID, _)) =
138 Try $ (Repeat $ (Rew_Inst $ Subs $ HOLogic.mk_string thmID))
139 | rule2stac_inst thy (Rule.Calc (c, _)) =
140 Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
141 | rule2stac_inst thy (Rule.Cal1 (c, _)) =
142 Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
143 | rule2stac_inst _ (Rule.Rls_ rls) =
144 Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule.id_rls rls))
145 | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule.rule2str r ^ "\"");
147 (*for appropriate nesting take stacs in _reverse_ order*)
148 fun op #>@ sts [s] = SEq $ s $ sts
149 | op #>@ sts (s::ss) = op #>@ (SEq $ s $ sts) ss
151 raise ERROR ("fun #>@ not applicable to \"" ^ Rule.term2str t ^ "\" \"" ^ Rule.terms2str ts ^ "\"");
153 | #> [s1, s2] = SEq $ s1 $ s2
154 | #> stacs = case rev stacs of
155 s3 :: s2 :: ss => op #>@ (SEq $ s2 $ s3) ss
156 | ts => raise ERROR ("fun #> not applicable to \"" ^ Rule.terms2str ts ^ "\"")
158 val contains_bdv = (not o null o (filter TermC.is_bdv) o TermC.ids2str o #prop o Thm.rep_thm);
160 (* does a rule contain a 'bdv'; descend recursively into Rls_ *)
161 fun contain_bdv [] = false
162 | contain_bdv (Rule.Thm (_, thm) :: rs) =
163 if (not o contains_bdv) thm
166 | contain_bdv (Rule.Calc _ :: rs) = contain_bdv rs
167 | contain_bdv (Rule.Cal1 _ :: rs) = contain_bdv rs
168 | contain_bdv (Rule.Rls_ rls :: rs) =
169 contain_bdv (Rule.get_rules rls) orelse contain_bdv rs
170 | contain_bdv (r :: _) =
171 error ("contain_bdv called with [" ^ Rule.id_rule r ^ ",...]");
173 (* filter Frees for free_str and pair their respective types with typ *)
174 fun subst_typ free_str typ frees =
176 val vars_v = filter (fn t => curry op = (t |> dest_Free |> fst) free_str) frees
177 val typs_v = map (fn t => (t |> dest_Free |> snd)) vars_v
179 map (fn T => (T, typ)) typs_v
181 (* instantiate typs in Prog auto_generated or auto_generated_ins for args "t_t", "v" *)
182 fun subst_typs prog typ_t typ_bdv =
184 val args = Program.formal_args prog
185 val frees = TermC.vars prog
186 val prog' = subst_atomic_types (subst_typ "t_t" typ_t frees) prog
191 else (* auto_generated_inst has second argument "v" *)
192 subst_atomic_types (subst_typ "v" typ_bdv frees) prog'
195 fun rules2scr_Rls thy rules =
197 then FunID_Term_Bdv $ (Repeat $ (((#> o (map (rule2stac_inst thy))) rules) $ Rule.e_term))
198 else FunID_Term $ (Repeat $ (((#> o (map (rule2stac thy))) rules) $ Rule.e_term));
199 fun rules2scr_Seq thy rules =
201 then FunID_Term_Bdv $ (((#> o (map (rule2stac_inst thy))) rules) $ Rule.e_term)
202 else FunID_Term $ (((#> o (map (rule2stac thy))) rules) $ Rule.e_term);
204 (* prepare the input for an rls for use:
205 # generate a script for stepwise execution of the rls
206 # filter the operators for Calc out of the script ?WN111014?
207 !!!use this function while storing (TODO integrate..) into KEStore_Elems.add_rlss *)
208 fun prep_rls _ Rule.Erls = error "prep_rls: not required for Erls"
209 | prep_rls thy (Rule.Rls {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
210 let val sc = (rules2scr_Rls thy rules)
211 in Rule.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls,
213 calc = get_calcs thy sc,
216 scr = Rule.Prog sc} end
217 | prep_rls thy (Rule.Seq {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) =
218 let val sc = (rules2scr_Seq thy rules)
219 in Rule.Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls,
221 calc = get_calcs thy sc,
224 scr = Rule.Prog sc} end
225 | prep_rls _ (Rule.Rrls {id, ...}) =
226 error ("prep_rls: not required for Rrls \"" ^ id ^ "\"");