Defunctionalization

This is inspired from student exercises proposed by Olivier Danvy at the JFLA 2014 conference

Simple Arithmetic Expressions

module Expr

use export int.Int

Grammar of expressions

n  :  int

e  :  expression
e ::= n | e - e

p  :  program
p ::= e

type expr = Cte int | Sub expr expr

type prog = expr

Examples:

p0 = 0
p1 = 10 - 6
p2 = (10 - 6) - (7 - 2)
p3 = (7 - 2) - (10 - 6)
p4 = 10 - (2 - 3)

let constant p0 : prog = Cte 0

let constant p1 : prog = Sub (Cte 10) (Cte 6)

let constant p2 : prog = Sub (Sub (Cte 10) (Cte 6)) (Sub (Cte 7) (Cte 2))

let constant p3 : prog = Sub (Sub (Cte 7) (Cte 2)) (Sub (Cte 10) (Cte 6))

let constant p4 : prog = Sub (Cte 10) (Sub (Cte 2) (Cte 3))

end

Direct Semantics

module DirectSem

use Expr

Values:

v  :  value
v ::= n

Expressible Values:

ve  :  expressible_value
ve ::= v

Interpretation:

------
n => n

e1 => n1   e2 => n2   n1 - n2 = n3
----------------------------------
      e1 - e2 => n3

A program e is interpreted into a value n if judgement

  e => n

holds.

Exercise 0.0

Program the interpreter above and test it on the examples.

  eval_0 : expression -> expressible_value
  interpret_0 : program -> expressible_value

(* Note: Why3 definitions introduced by "function" belong to the logic
   part of Why3 language *)

let rec function eval_0 (e:expr) : int =
  match e with
  | Cte n -> n
  | Sub e1 e2 -> eval_0 e1 - eval_0 e2
  end

let function interpret_0 (p:prog) : int = eval_0 p

Tests, can be replayed using

  why3 defunctionalization.mlw --exec DirectSem.test

(Why3 version at least 0.82 required)

let test () =
   interpret_0 p0,
   interpret_0 p1,
   interpret_0 p2,
   interpret_0 p3,
   interpret_0 p4

constant v3 : int = eval_0 p3

goal eval_p3 : v3 = 1

end

CPS: Continuation Passing Style

module CPS

use Expr

Exercise 0.1

CPS-transform (call by value, left to right) the function eval_0, and call it from the main interpreter with the identity function as initial continuation

      eval_1 : expression -> (expressible_value -> 'a) -> 'a
  interpret_1 : program -> expressible_value

use DirectSem

let rec eval_1 (e:expr) (k: int->'a) : 'a
  variant { e }
  ensures { result = k (eval_0 e) }
= match e with
    | Cte n -> k n
    | Sub e1 e2 ->
      eval_1 e1 (fun v1 -> eval_1 e2 (fun v2 -> k (v1 - v2)))
  end

let interpret_1 (p : prog) : int
  ensures { result = eval_0 p }
= eval_1 p (fun n -> n)

end

Defunctionalization

module Defunctionalization

use Expr
use DirectSem

Exercise 0.2

De-functionalize the continuation of eval_1.

         cont ::= ...

   continue_2 : cont -> value -> value
       eval_2 : expression -> cont -> value
  interpret_2 : program -> value

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:

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

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

Some functions to serve as measures for the termination proof

function size_e (e:expr) : int =
  match e with
  | Cte _ -> 1
  | Sub e1 e2 -> 3 + size_e e1 + size_e e2
  end

lemma size_e_pos: forall e: expr. size_e e >= 1

function size_c (c:cont) : int =
  match c with
  | I -> 0
  | A1 e2 k -> 2 + size_e e2 + size_c k
  | A2 _ k -> 1 + size_c k
  end

lemma size_c_pos: forall c: cont. size_c c >= 0

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 }
  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_c c + size_e e }
  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

Defunctionalization with an algebraic variant

module Defunctionalization2

use Expr
use DirectSem

Exercise 0.2

De-functionalize the continuation of eval_1.

         cont ::= ...

   continue_2 : cont -> value -> value
       eval_2 : expression -> cont -> value
  interpret_2 : program -> value

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:

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

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

Semantics with errors

module SemWithError

use Expr

Errors:

s  :  error

Expressible values:

ve  :  expressible_value
ve ::= v | s

type value = Vnum int | Underflow
(* in (Vnum n), n should always be >= 0 *)

Interpretation:

------
n => n

     e1 => s
------------
e1 - e2 => s

e1 => n1   e2 => s
------------------
      e1 - e2 => s

e1 => n1   e2 => n2   n1 < n2
-----------------------------
      e1 - e2 => "underflow"

e1 => n1   e2 => n2   n1 >= n2   n1 - n2 = n3
---------------------------------------------
      e1 - e2 => n3

We interpret the program e into value n if the judgement

  e => n

holds, and into error s if the judgement

  e => s

holds.

Exercise 1.0

Program the interpreter above and test it on the examples.

  eval_0 : expr -> expressible_value
  interpret_0 : program -> expressible_value

function eval_0 (e:expr) : value =
  match e with
  | Cte n -> if n >= 0 then Vnum n else Underflow
  | Sub e1 e2 ->
     match eval_0 e1 with
     | Underflow -> Underflow
     | Vnum v1 ->
       match eval_0 e2 with
       | Underflow -> Underflow
       | Vnum v2 ->
         if v1 >= v2 then Vnum (v1 - v2) else Underflow
       end
     end
  end

function interpret_0 (p:prog) : value = eval_0 p

Exercise 1.1

CPS-transform (call by value, from left to right) the function eval_0, call it from the main interpreter with the identity function as initial continuation.

      eval_1 : expr -> (expressible_value -> 'a) -> 'a
  interpret_1 : program -> expressible_value

function eval_1 (e:expr) (k:value -> 'a) : 'a =
  match e with
    | Cte n -> k (if n >= 0 then Vnum n else Underflow)
    | Sub e1 e2 ->
      eval_1 e1 (fun v1 ->
       match v1 with
       | Underflow -> k Underflow
       | Vnum v1 ->
         eval_1 e2 (fun v2 ->
         match v2 with
         | Underflow -> k Underflow
         | Vnum v2 -> k (if v1 >= v2 then Vnum (v1 - v2) else Underflow)
         end)
       end)
  end

function interpret_1 (p : prog) : value = eval_1 p (fun n ->  n)

lemma cps_correct_expr:
  forall e: expr. forall k:value -> 'a. eval_1 e k = k (eval_0 e)

lemma cps_correct: forall p. interpret_1 p = interpret_0 p

Exercise 1.2

Divide the continuation

    expressible_value -> 'a

in two:

    (value -> 'a) * (error -> 'a)

and adapt eval_1 and interpret_1 as

       eval_2 : expr -> (value -> 'a) -> (error -> 'a) -> 'a
  interpret_2 : program -> expressible_value

(*
function eval_2 (e:expr) (k:int -> 'a) (kerr: unit -> 'a) : 'a =
  match e with
    | Cte n -> if n >= 0 then k n else kerr ()
    | Sub e1 e2 ->
      eval_2 e1 (fun v1 ->
         eval_2 e2 (fun v2 ->
           if v1 >= v2 then k (v1 - v2) else kerr ())
           kerr) kerr
  end
*)

function eval_2 (e:expr) (k:int -> 'a) (kerr: unit -> 'a) : 'a =
  match e with
    | Cte n -> if n >= 0 then k n else kerr ()
    | Sub e1 e2 ->
      eval_2 e1 (eval_2a e2 k kerr) kerr
  end

with eval_2a (e2:expr) (k:int -> 'a) (kerr : unit -> 'a) : int -> 'a =
  (fun v1 ->  eval_2 e2 (eval_2b v1 k kerr) kerr)

with eval_2b (v1:int) (k:int -> 'a) (kerr : unit -> 'a) : int -> 'a =
  (fun v2 ->  if v1 >= v2 then k (v1 - v2) else kerr ())

function interpret_2 (p : prog) : value =
  eval_2 p (fun n ->  Vnum n) (fun _ ->  Underflow)

lemma cps2_correct_expr_aux:
  forall k: int -> 'a, e1 e2, kerr: unit -> 'a.
  eval_2 (Sub e1 e2) k kerr = eval_2 e1 (eval_2a e2 k kerr) kerr

lemma cps2_correct_expr:
  forall e, kerr: unit->'a, k:int -> 'a. eval_2 e k kerr =
  match eval_0 e with Vnum n -> k n | Underflow -> kerr () end

lemma cps2_correct: forall p. interpret_2 p = interpret_0 p

Exercise 1.3

Specialize the codomain of the continuations and of the evaluation function so that it is not polymorphic anymore but is expressible_value, and then short-circuit the second continuation to stop in case of error

       eval_3 : expr -> (value -> expressible_value) -> expressible_value
  interpret_3 : program -> expressible_value

NB: Now there is only one continuation and it is applied only in absence of error.

function eval_3 (e:expr) (k:int -> value) : value =
  match e with
    | Cte n -> if n >= 0 then k n else Underflow
    | Sub e1 e2 ->
      eval_3 e1 (eval_3a e2 k)
  end

with eval_3a (e2:expr) (k:int -> value) : int -> value =
  (fun v1 ->  eval_3 e2 (eval_3b v1 k))

with eval_3b (v1:int) (k:int -> value) : int -> value =
  (fun v2 ->  if v1 >= v2 then k (v1 - v2) else Underflow)

function interpret_3 (p : prog) : value = eval_3 p (fun n ->  Vnum n)

let rec lemma cps3_correct_expr (e:expr) : unit
  variant { e }
  ensures { forall k. eval_3 e k =
    match eval_0 e with Vnum n -> k n | Underflow -> Underflow end }
= match e with
  | Cte _ -> ()
  | Sub e1 e2 ->
      cps3_correct_expr e1;
      cps3_correct_expr e2;
      assert {forall k. eval_3 e k = eval_3 e1 (eval_3a e2 k) }
  end

lemma cps3_correct: forall p. interpret_3 p = interpret_0 p

Exercise 1.4

De-functionalize the continuation of eval_3.

         cont ::= ...

    continue_4 : cont -> value -> expressible_value
        eval_4 : expr -> cont -> expressible_value
  interprete_4 : program -> expressible_value

The data type cont represents the grammar of contexts. (NB. has it changed w.r.t to previous exercise?)

The two mutually recursive functions eval_4 and continue_4 implement an abstract machine, that is a transition system that stops immediately in case of error, or and the end of computation.

type cont = I | A expr cont | B int cont

  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 value value =
| underflow :
  forall k:cont. eval_cont k Underflow Underflow
| a1 :
  forall e2:expr, k:cont, v:int, r:value.
  eval_cont (B v k) (eval_0 e2) r -> eval_cont (A e2 k) (Vnum v) r
| a2 :
  forall v1:int, k:cont, v:int, r:value.
  eval_cont k (if v1 >= v then Vnum (v1 - v) else Underflow) r
  -> eval_cont (B v1 k) (Vnum v) r
| a3 :
  forall v:int. eval_cont I (Vnum v) (Vnum v)

Some functions to serve as measures for the termination proof

function size_e (e:expr) : int =
  match e with
  | Cte _ -> 1
  | Sub e1 e2 -> 3 + size_e e1 + size_e e2
  end

lemma size_e_pos: forall e: expr. size_e e >= 1

use Defunctionalization as D

function size_c (c:cont) : int =
  match c with
  | I -> 0
  | A e2 k -> 2 + D.size_e e2 + size_c k
  | B _ k -> 1 + size_c k
  end

lemma size_c_pos: forall c: cont. size_c c >= 0

let rec continue_4 (c:cont) (v:int) : value
  requires { v >= 0 }
  variant { size_c c }
  ensures { eval_cont c (Vnum v) result }
  =
  match c with
    | A e2 k -> eval_4 e2 (B v k)
    | B v1 k -> if v1 >= v then continue_4 k (v1 - v) else Underflow
    | I -> Vnum v
  end

with eval_4 (e:expr) (c:cont) : value
  variant { size_c c + D.size_e e }
  ensures { eval_cont c (eval_0 e) result }
  =
  match e with
    | Cte n -> if n >= 0 then continue_4 c n else Underflow
    | Sub e1 e2 -> eval_4 e1 (A e2 c)
  end

The interpreter. The post-condition specifies that this program computes the same thing as eval_0

let interpret_4 (p:prog) : value
  ensures { result = eval_0 p }
  = eval_4 p I

let test () =
   interpret_4 p0,
   interpret_4 p1,
   interpret_4 p2,
   interpret_4 p3,
   interpret_4 p4

end

Reduction Semantics

module ReductionSemantics

A small step semantics, defined iteratively with reduction contexts

  use Expr
  use DirectSem

Expressions:

n  :  int

e  :  expression
e ::= n | e - e

p  :  program
p ::= e

Values:

v  :  value
v ::= n

Potential Redexes:

  rp ::= n1 - n2

Reduction Rule:

  n1 - n2 -> n3

(in the case of relative integers Z, all potential redexes are true redexes; but for natural numbers, not all of them are true ones:

   n1 - n2 -> n3   if n1 >= n2

a potential redex that is not a true one is stuck.)

Contraction Function:

  contract : redex_potentiel -> expression + stuck
  contract (n1 - n2) = n3   si n3 = n1 - n2

and if there are only non-negative numbers:

  contract (n1 - n2) = n3     if n1 >= n2 and n3 = n1 - n2
  contract (n1 - n2) = stuck  if n1 < n2

predicate is_a_redex (e:expr) =
  match e with
  | Sub (Cte _) (Cte _) -> true
  | _ -> false
  end

let contract (e:expr) : expr
  requires { is_a_redex e }
  ensures { eval_0 result = eval_0 e }
  =
  match e with
  | Sub (Cte v1) (Cte v2) -> Cte (v1 - v2)
  | _ -> absurd
  end

Reduction Contexts:

C  : cont
C ::= [] | [C e] | [v C]

type context = Empty | Left context expr | Right int context

Recomposition:

             recompose : cont * expression -> expression
     recompose ([], e) = e
recompose ([C e2], e1) = recompose (C, e1 - e2)
recompose ([n1 C], e2) = recompose (C, n1 - e2)

let rec function recompose (c:context) (e:expr) : expr =
  match c with
  | Empty -> e
  | Left c e2 -> recompose c (Sub e e2)
  | Right n1 c -> recompose c (Sub (Cte n1) e)
  end

let rec lemma recompose_values (c:context) (e1 e2:expr) : unit
  requires { eval_0 e1 = eval_0 e2 }
  variant  { c }
  ensures  { eval_0 (recompose c e1) = eval_0 (recompose c e2) }
= match c with
  | Empty -> ()
  | Left c e -> recompose_values c (Sub e1 e) (Sub e2 e)
  | Right n c -> recompose_values c (Sub (Cte n) e1) (Sub (Cte n) e2)
  end

(* not needed anymore
let rec lemma recompose_inversion (c:context) (e:expr)
  requires {
      match c with Empty -> false | _ -> true end \/
      match e with Cte _ -> false | Sub _ _ -> true end }
  variant { c }
  ensures {  match recompose c e with
               Cte _ -> false | Sub _ _ -> true end }
= match c with
  | Empty -> ()
  | Left c e2 -> recompose_inversion c (Sub e e2)
  | Right n1 c -> recompose_inversion c (Sub (Cte n1) e)
  end
*)

Decomposition:

dec_or_val = (C, rp) | v

Decomposition function:

             decompose_term : expression * cont -> dec_or_val
      decompose_term (n, C) = decompose_cont (C, n)
decompose_term (e1 - e2, C) = decompose_term (e1, [C e2])

             decompose_cont : cont * value -> dec_or_val
     decompose_cont ([], n) = n
  decompose_cont ([C e], n) = decompose_term (e, [n c])
decompose_term ([n1 C], n2) = (C, n1 - n2)

  decompose : expression -> dec_or_val
decompose e = decompose_term (e, [])

exception Stuck

predicate is_a_value (e:expr) =
  match e with
  | Cte _ -> true
  | _ -> false
  end

predicate is_empty_context (c:context) =
  match c with
  | Empty -> true
  | _ -> false
  end

use Defunctionalization as D (* for size_e *)

function size_e (e:expr) : int = D.size_e e

function size_c (c:context) : int =
  match c with
  | Empty -> 0
  | Left c e -> 2 + size_c c + size_e e
  | Right _ c -> 1 + size_c c
  end

lemma size_c_pos: forall c: context. size_c c >= 0

let rec decompose_term (e:expr) (c:context) : (context, expr)
  variant { size_e e + size_c c }
  ensures { let c1,e1 = result in
            recompose c1 e1 = recompose c e /\
            is_a_redex e1 }
  raises { Stuck -> is_empty_context c /\ is_a_value e }
  (* raises { Stuck -> is_a_value (recompose c e) } *)
  =
  match e with
  | Cte n -> decompose_cont c n
  | Sub e1 e2 -> decompose_term e1 (Left c e2)
  end

with decompose_cont (c:context) (n:int) : (context, expr)
  variant { size_c c }
  ensures { let c1,e1 = result in
            recompose c1 e1 = recompose c (Cte n)  /\
            is_a_redex e1 }
  raises { Stuck -> is_empty_context c }
(*  raises { Stuck -> is_a_value (recompose c (Cte n)) } *)
  =
  match c with
  | Empty -> raise Stuck
  | Left c e -> decompose_term e (Right n c)
  | Right n1 c -> c, Sub (Cte n1) (Cte n)
  end

let decompose (e:expr) : (context, expr)
  ensures { let c1,e1 = result in recompose c1 e1 = e  /\
            is_a_redex e1 }
  raises { Stuck -> is_a_value e }
  =
  decompose_term e Empty

One reduction step:

reduce : expression -> expression + stuck

if decompose e = v
then reduce e = stuck

if decompose e = (C, rp)
and contract rp = stuck
then reduce e = stuck

if decompose e = (C, rp)
and contract rp = c
then reduce e = recompose (C, c)

Exercise 2.0

Implement the reduction semantics above and test it

let reduce (e:expr) : expr
  ensures { eval_0 result = eval_0 e }
  raises { Stuck -> is_a_value e }
  =
  let c,r = decompose e in
  recompose c (contract r)

Evaluation based on iterated reduction:

itere : red_ou_val -> value + erreur

itere v = v

if contract rp = stuck
then itere (C, rp) = stuck

if contract rp = c
then itere (C, rp) = itere (decompose (recompose (C, c)))

let rec itere (e:expr) : int
  diverges (* termination could be proved but that's not the point *)
  ensures { eval_0 e = result }
  =
  match reduce e with
  | e' -> itere e'
  | exception Stuck ->
     match e with
     | Cte n -> n
     | _ -> absurd
     end
  end

Exercise 2.1

Optimize the step recomposition / decomposition into a single function refocus.

let refocus c e
  ensures { let c1,e1 = result in
            recompose c1 e1 = recompose c e /\
            is_a_redex e1 }
  raises { Stuck -> is_empty_context c /\ is_a_value e }
= decompose_term e c

let rec itere_opt (c:context) (e:expr) : int
  diverges
  ensures { result = eval_0 (recompose c e) }
= match refocus c e with
  | c, r -> itere_opt c (contract r)
  | exception Stuck ->
     assert { is_empty_context c };
     match e with
     | Cte n -> n
     | _ -> absurd
     end
  end

let rec normalize (e:expr)
  diverges
  ensures { result = eval_0 e }
= itere_opt Empty e

Exercise 2.2

Derive an abstract machine

(c,Cte n)_1 -> (c,n)_2
(c,Sub e1 e2)_1 -> (Left c e2,e1)_1
(Empty,n)_2 -> stop with result = n
(Left c e,n)_2 -> (Right n c,e)_1
(Right n1 c,n)_2 -> (c,Cte (n1 - n))_1

let rec eval_1 c e
  variant { 2 * (size_c c + size_e e) }
  ensures { result = eval_0 (recompose c e) }
= match e with
  | Cte n -> eval_2 c n
  | Sub e1 e2 -> eval_1 (Left c e2) e1
  end

with eval_2 c n
  variant { 1 + 2 * size_c c }
  ensures { result = eval_0 (recompose c (Cte n)) }
= match c with
  | Empty -> n
  | Left c e -> eval_1 (Right n c) e
  | Right n1 c -> eval_1 c (Cte (n1 - n))
  end

let interpret p
  ensures { result = eval_0 p }
= eval_1 Empty p

let test () =
   interpret p0,
   interpret p1,
   interpret p2,
   interpret p3,
   interpret p4

end

module RWithError

use Expr
use SemWithError

Exercise 2.3

An abstract machine for the case with errors

(c,Cte n)_1 -> stop on Underflow if  n < 0
(c,Cte n)_1 -> (c,n)_2 if n >= 0
(c,Sub e1 e2)_1 -> (Left c e2,e1)_1
(Empty,n)_2 -> stop on Vnum n
(Left c e,n)_2 -> (Right n c,e)_1
(Right n1 c,n)_2 -> stop on Underflow if n1 < n
(Right n1 c,n)_2 -> (c,Cte (n1 - n))_1 if n1 >= n

type context = Empty | Left context expr | Right int context

use Defunctionalization as D (* for size_e *)

function size_e (e:expr) : int = D.size_e e

function size_c (c:context) : int =
  match c with
  | Empty -> 0
  | Left c e -> 2 + size_c c + size_e e
  | Right _ c -> 1 + size_c c
  end

lemma size_c_pos: forall c: context. size_c c >= 0

function recompose (c:context) (e:expr) : expr =
  match c with
  | Empty -> e
  | Left c e2 -> recompose c (Sub e e2)
  | Right n1 c -> recompose c (Sub (Cte n1) e)
  end

let rec lemma recompose_values (c:context) (e1 e2:expr) : unit
  requires { eval_0 e1 = eval_0 e2 }
  variant  { c }
  ensures  { eval_0 (recompose c e1) = eval_0 (recompose c e2) }
= match c with
  | Empty -> ()
  | Left c e -> recompose_values c (Sub e1 e) (Sub e2 e)
  | Right n c -> recompose_values c (Sub (Cte n) e1) (Sub (Cte n) e2)
  end

let rec lemma recompose_underflow (c:context) (e:expr) : unit
  requires { eval_0 e = Underflow }
  variant { c }
  ensures { eval_0 (recompose c e) = Underflow }
= match c with
  | Empty -> ()
  | Left c e1 -> recompose_underflow c (Sub e e1)
  | Right n c -> recompose_underflow c (Sub (Cte n) e)
  end

let rec eval_1 c e
  variant { 2 * (size_c c + size_e e) }
  ensures { result = eval_0 (recompose c e) }
= match e with
  | Cte n -> if n >= 0 then eval_2 c n else Underflow
  | Sub e1 e2 -> eval_1 (Left c e2) e1
  end

with eval_2 c n
  variant { 1 + 2 * size_c c }
  requires { n >= 0 }
  ensures { result = eval_0 (recompose c (Cte n)) }
= match c with
  | Empty -> Vnum n
  | Left c e -> eval_1 (Right n c) e
  | Right n1 c -> if n1 >= n then eval_1 c (Cte (n1 - n)) else Underflow
  end

let interpret p
  ensures { result = eval_0 p }
= eval_1 Empty p

let test () =
   interpret p0,
   interpret p1,
   interpret p2,
   interpret p3,
   interpret p4

end