Commit a0f563cc authored by Andrei Paskevich's avatar Andrei Paskevich

defunctionalization: add a variant with algebraic variant

14 lines instead of 23 for the termination proofs
parent 15e0350c
......@@ -290,6 +290,114 @@ let test () =
end
(** {2 Defunctionalization with an alebraic variant} *)
module Defunctionalization2
use import Expr
use import DirectSem
(** {4 Exercise 0.2}
De-functionalize the continuation of [eval_1].
{h <blockquote><pre>
cont ::= ...
continue_2 : cont -> value -> value
eval_2 : expression -> cont -> value
interpret_2 : program -> value
</pre></blockquote>}
The data type [cont] represents the grammar of contexts.
The two mutually recursive functions [eval_2] and [continue_2]
implement an abstract machine, that is a state transition system.
*)
type cont = A1 expr cont | A2 int cont | I
(** One would want to write in Why:
{h <blockquote><pre>
function eval_cont (c:cont) (v:int) : int =
match c with
| A1 e2 k ->
let v2 = eval_0 e2 in
eval_cont (A2 v k) v2
| A2 v1 k -> eval_cont k (v1 - v)
| I -> v
end
</pre></blockquote>}
But since the recursion is not structural, Why3 kernel rejects it
(definitions in the logic part of the language must be total)
We replace that with a relational definition, an inductive one.
*)
inductive eval_cont cont int int =
| a1 :
forall e2:expr, k:cont, v:int, r:int.
eval_cont (A2 v k) (eval_0 e2) r -> eval_cont (A1 e2 k) v r
| a2 :
forall v1:int, k:cont, v:int, r:int.
eval_cont k (v1 - v) r -> eval_cont (A2 v1 k) v r
| a3 :
forall v:int. eval_cont I v v
(** Peano naturals to serve as the measure for the termination proof *)
type nat = S nat | O
function size_e (e:expr) (acc:nat) : nat =
match e with
| Cte _ -> S acc
| Sub e1 e2 -> S (size_e e1 (S (size_e e2 (S acc))))
end
function size_c (c:cont) (acc:nat) : nat =
match c with
| I -> acc
| A1 e2 k -> S (size_e e2 (S (size_c k acc)))
| A2 _ k -> S (size_c k acc)
end
(** WhyML programs (declared with "let" instead of "function"),
mutually recursive, resulting from de-functionalization *)
let rec continue_2 (c:cont) (v:int) : int
variant { size_c c O }
ensures { eval_cont c v result }
=
match c with
| A1 e2 k -> eval_2 e2 (A2 v k)
| A2 v1 k -> continue_2 k (v1 - v)
| I -> v
end
with eval_2 (e:expr) (c:cont) : int
variant { size_e e (size_c c O) }
ensures { eval_cont c (eval_0 e) result }
=
match e with
| Cte n -> continue_2 c n
| Sub e1 e2 -> eval_2 e1 (A1 e2 c)
end
(** The interpreter. The post-condition specifies that this program
computes the same thing as [eval_0] *)
let interpret_2 (p:prog) : int
ensures { result = eval_0 p }
= eval_2 p I
let test () =
(interpret_2 p0,
interpret_2 p1,
interpret_2 p2,
interpret_2 p3,
interpret_2 p4)
end
(** {2 Semantics with errors} *)
......@@ -1114,4 +1222,4 @@ let test () =
interpret p4)
end
\ No newline at end of file
end
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