Theory Canonicalization
subsection ‹Canonicalization DSL›
theory Canonicalization
imports
Markup
Phase
"HOL-Eisbach.Eisbach"
keywords
"phase" :: thy_decl and
"terminating" :: quasi_command and
"print_phases" :: diag and
"export_phases" :: thy_decl and
"optimization" :: thy_goal_defn
begin
print_methods
ML ‹
datatype 'a Rewrite =
Transform of 'a * 'a |
Conditional of 'a * 'a * term |
Sequential of 'a Rewrite * 'a Rewrite |
Transitive of 'a Rewrite
type rewrite = {
name: binding,
rewrite: term Rewrite,
proofs: thm list,
code: thm list,
source: term
}
structure RewriteRule : Rule =
struct
type T = rewrite;
fun pretty_thm ctxt thm =
(Proof_Context.pretty_fact ctxt ("", [thm]))
fun pretty ctxt obligations t =
let
val is_skipped = Thm_Deps.has_skip_proof (#proofs t);
val warning = (if is_skipped
then [Pretty.str "(proof skipped)", Pretty.brk 0]
else []);
val obligations = (if obligations
then [Pretty.big_list
"obligations:"
(map (pretty_thm ctxt) (#proofs t)),
Pretty.brk 0]
else []);
fun pretty_bind binding =
Pretty.markup
(Position.markup (Binding.pos_of binding) Markup.position)
[Pretty.str (Binding.name_of binding)];
in
Pretty.block ([
pretty_bind (#name t), Pretty.str ": ",
Syntax.pretty_term ctxt (#source t), Pretty.fbrk
] @ obligations @ warning)
end
end
structure RewritePhase = DSL_Phase(RewriteRule);
val _ =
Outer_Syntax.command \<^command_keyword>‹phase› "enter an optimization phase"
(Parse.binding --| Parse.$$$ "terminating" -- Parse.const --| Parse.begin
>> (Toplevel.begin_main_target true o RewritePhase.setup));
fun print_phases print_obligations ctxt =
let
val thy = Proof_Context.theory_of ctxt;
fun print phase = RewritePhase.pretty print_obligations phase ctxt
in
map print (RewritePhase.phases thy)
end
fun print_optimizations print_obligations thy =
print_phases print_obligations thy |> Pretty.writeln_chunks
val _ =
Outer_Syntax.command \<^command_keyword>‹print_phases›
"print debug information for optimizations"
(Parse.opt_bang >>
(fn b => Toplevel.keep ((print_optimizations b) o Toplevel.context_of)));
fun export_phases thy name =
let
val state = Toplevel.make_state (SOME thy);
val ctxt = Toplevel.context_of state;
val content = Pretty.string_of (Pretty.chunks (print_phases false ctxt));
val cleaned = YXML.content_of content;
val filename = Path.explode (name^".rules");
val directory = Path.explode "optimizations";
val path = Path.binding (
Path.append directory filename,
Position.none);
val thy' = thy |> Generated_Files.add_files (path, (Bytes.string content));
val _ = Export.export thy' path [YXML.parse cleaned];
val _ = writeln (Export.message thy' (Path.basic "optimizations"));
in
thy'
end
val _ =
Outer_Syntax.command \<^command_keyword>‹export_phases›
"export information about encoded optimizations"
(Parse.path >>
(fn name => Toplevel.theory (fn state => export_phases state name)))
›
ML_file "rewrites.ML"
subsubsection ‹Semantic Preservation Obligation›
fun rewrite_preservation :: "IRExpr Rewrite ⇒ bool" where
"rewrite_preservation (Transform x y) = (y ≤ x)" |
"rewrite_preservation (Conditional x y cond) = (cond ⟶ (y ≤ x))" |
"rewrite_preservation (Sequential x y) = (rewrite_preservation x ∧ rewrite_preservation y)" |
"rewrite_preservation (Transitive x) = rewrite_preservation x"
subsubsection ‹Termination Obligation›
fun rewrite_termination :: "IRExpr Rewrite ⇒ (IRExpr ⇒ nat) ⇒ bool" where
"rewrite_termination (Transform x y) trm = (trm x > trm y)" |
"rewrite_termination (Conditional x y cond) trm = (cond ⟶ (trm x > trm y))" |
"rewrite_termination (Sequential x y) trm = (rewrite_termination x trm ∧ rewrite_termination y trm)" |
"rewrite_termination (Transitive x) trm = rewrite_termination x trm"
fun intval :: "Value Rewrite ⇒ bool" where
"intval (Transform x y) = (x ≠ UndefVal ∧ y ≠ UndefVal ⟶ x = y)" |
"intval (Conditional x y cond) = (cond ⟶ (x = y))" |
"intval (Sequential x y) = (intval x ∧ intval y)" |
"intval (Transitive x) = intval x"
subsubsection ‹Standard Termination Measure›
fun size :: "IRExpr ⇒ nat" where
unary_size:
"size (UnaryExpr op x) = (size x) + 2" |
bin_const_size:
"size (BinaryExpr op x (ConstantExpr cy)) = (size x) + 2" |
bin_size:
"size (BinaryExpr op x y) = (size x) + (size y) + 2" |
cond_size:
"size (ConditionalExpr c t f) = (size c) + (size t) + (size f) + 2" |
const_size:
"size (ConstantExpr c) = 1" |
param_size:
"size (ParameterExpr ind s) = 2" |
leaf_size:
"size (LeafExpr nid s) = 2" |
"size (ConstantVar c) = 2" |
"size (VariableExpr x s) = 2"
subsubsection ‹Automated Tactics›
named_theorems size_simps "size simplication rules"
method unfold_optimization =
(unfold rewrite_preservation.simps, unfold rewrite_termination.simps,
unfold intval.simps,
rule conjE, simp, simp del: le_expr_def, force?)
| (unfold rewrite_preservation.simps, unfold rewrite_termination.simps,
rule conjE, simp, simp del: le_expr_def, force?)
method unfold_size =
(((unfold size.simps, simp add: size_simps del: le_expr_def)?
; (simp add: size_simps del: le_expr_def)?
; (auto simp: size_simps)?
; (unfold size.simps)?)[1])
print_methods
ML ‹
structure System : RewriteSystem =
struct
val preservation = @{const rewrite_preservation};
val termination = @{const rewrite_termination};
val intval = @{const intval};
end
structure DSL = DSL_Rewrites(System);
val _ =
Outer_Syntax.local_theory_to_proof \<^command_keyword>‹optimization›
"define an optimization and open proof obligation"
(Parse_Spec.thm_name ":" -- Parse.term
>> DSL.rewrite_cmd);
›
ML_file "~~/src/Doc/antiquote_setup.ML"
snipbegin ‹PhaseRail›
text ‹
\<^rail>‹
@{syntax_def phase}: @'phase' @{syntax name} ⏎
@'terminating' @{syntax measure} ⏎
@'begin' (body*)
@'end'
;
@{syntax_def optimization}: @'optimization' @{syntax name} options? ':' ⏎
rule proof
;
options: '[' (intval | subgoals) ']'
;
rule: term '↦' term ⏎
('when' condition ((condition '&&')*))?
;
@{syntax_def print_phases}: @'print_phases' '!'?
;
@{syntax_def export_phases}: @'export_phases' filename
;
@{syntax_def gencode}: @'gencode' filename term
;
›
➧ @{command phase}~‹name›~‹terminating›~‹measure›
opens a new optimization phase environment.
A termination measure is provided as the measure argument.
All optimizations within the phase must satisfy termination for the given measure.
➧ @{command optimization}~‹name›
defines a new optimization rule with a proof of correctness.
An obligation for semantic preservation and termination are opened.
An optimization can only be defined within a ∗‹phase›.
›
snipend -
print_syntax
end