Commit 861b2d3f authored by Martin Clochard's avatar Martin Clochard

(wip) mini-compiler: more consistent naming

parent 523006f3
......@@ -62,9 +62,9 @@ module Compile_bexpr
else ms' = VMS (p + out_f) s m
meta rewrite_def function bexpr_post
function exn_bool (b1:bexpr) (cond:bool) : pre 'a =
\x p ms. let VMS _ _ m = ms in beval m b1 = cond
meta rewrite_def function exn_bool
function exec_cond (b1:bexpr) (cond:bool) : pre 'a =
\x p ms. let VMS _ _ m = ms in beval m b1 = cond
meta rewrite_def function exec_cond
let rec compile_bexpr (b : bexpr) (cond: bool) (ofs: pos) : hl 'a
ensures { result.pre = trivial_pre /\ hl_correctness result }
......@@ -76,7 +76,7 @@ module Compile_bexpr
| Bfalse -> $ if cond then inil () else ibranchf ofs
| Bnot b1 -> $ compile_bexpr b1 (not cond) ofs
| Band b1 b2 ->
let c2 = $ compile_bexpr b2 cond ofs % exn_bool b1 true in
let c2 = $ compile_bexpr b2 cond ofs % exec_cond b1 true in
let ofs = if cond then length c2.wcode else ofs + length c2.wcode in
$ compile_bexpr b1 false ofs ~ c2
| Beq a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~
......@@ -122,9 +122,9 @@ module Compile_com
p' = p + len /\ s' = s /\ ceval m cmd m'
meta rewrite_def function com_post
function exn_bool_old (b1:bexpr) (cond:bool) : pre ('a,machine_state) =
function exec_cond_old (b1:bexpr) (cond:bool) : pre ('a,machine_state) =
\x p ms. let VMS _ _ m = snd x in beval m b1 = cond
meta rewrite_def function exn_bool_old
meta rewrite_def function exec_cond_old
function loop_invariant (c:com) : pre ('a,machine_state) =
\x p msi. let VMS _ s0 m0 = snd x in let VMS pi si mi = msi in
......@@ -152,14 +152,14 @@ module Compile_com
| Cif cond cmd1 cmd2 -> let code_false = compile_com cmd2 in
let code_true = $ compile_com cmd1 ~ $ ibranchf code_false.code.length in
$ compile_bexpr cond false code_true.wcode.length ~
(code_true % exn_bool cond true) ~
($ code_false % exn_bool_old cond false)
(code_true % exec_cond cond true) ~
($ code_false % exec_cond_old cond false)
| Cwhile test body -> let code_body = compile_com body in
let body_length = length code_body.code + 1 in
let code_test = compile_bexpr test false body_length in
let ofs = length code_test.code + body_length in
let wp_while = $ code_test ~
($ code_body ~ $ ibranchf (- ofs)) % exn_bool test true in
($ code_body ~ $ ibranchf (- ofs)) % exec_cond test true in
let ghost inv = loop_invariant cmd in
let ghost var = loop_variant body test in
let ghost post = loop_post cmd ofs in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment