(**

{1 Defunctionalization}

This is inspired from student exercises proposed by
{h <a href="http://cs.au.dk/~danvy/">Olivier Danvy</a>}
at the {h <a href="http://jfla.inria.fr/2014/">JFLA 2014 conference</a>}

*)


(** {2 Simple Arithmetic Expressions} *)

module Expr

use export int.Int

(** Grammar of expressions
{h <blockquote><pre>
n  :  int

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

p  :  program
p ::= e
</pre></blockquote>}
*)

type expr = Cte int | Sub expr expr

type prog = expr

(** Examples:
{h <blockquote><pre>
p0 = 0
p1 = 10 - 6
p2 = (10 - 6) - (7 - 2)
p3 = (7 - 2) - (10 - 6)
p4 = 10 - (2 - 3)
</pre></blockquote>}
*)

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


(** {2 Direct Semantics} *)

module DirectSem

use Expr

(** Values:
{h <blockquote><pre>
v  :  value
v ::= n
</pre></blockquote>
}
Expressible Values:
{h <blockquote><pre>
ve  :  expressible_value
ve ::= v
</pre></blockquote>}
Interpretation:
{h <blockquote><pre>
------
n => n

e1 => n1   e2 => n2   n1 - n2 = n3
----------------------------------
      e1 - e2 => n3
</pre></blockquote>}
A program e is interpreted into a value n if judgement
{h <blockquote><pre>
  e => n
</pre></blockquote>}
holds.
*)

(** {4 Exercise 0.0}
  Program the interpreter above and test it on the examples.
{h <blockquote><pre>
  eval_0 : expression -> expressible_value
  interpret_0 : program -> expressible_value
</pre></blockquote>}
*)

(* 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
{h <blockquote><pre>
  why3 defunctionalization.mlw --exec DirectSem.test
</pre></blockquote>}
(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


(** {2 CPS: Continuation Passing Style} *)

module CPS

use Expr

(** {4 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
{h <blockquote><pre>
      eval_1 : expression -> (expressible_value -> 'a) -> 'a
  interpret_1 : program -> expressible_value
</pre></blockquote>}

*)

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



(** {2 Defunctionalization} *)

module Defunctionalization

use Expr
use 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

(** 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


(** {2 Defunctionalization with an algebraic variant} *)

module Defunctionalization2

use Expr
use 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} *)

module SemWithError

use Expr

(** Errors:
{h <blockquote><pre>
s  :  error
</pre></blockquote>}
Expressible values:
{h <blockquote><pre>
ve  :  expressible_value
ve ::= v | s
</pre></blockquote>}
*)

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

(** Interpretation:
{h <blockquote><pre>
------
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
</pre></blockquote>}
We interpret the program `e` into value `n` if the judgement
{h <blockquote><pre>
  e => n
</pre></blockquote>}
holds, and into error `s` if the judgement
{h <blockquote><pre>
  e => s
</pre></blockquote>}
holds.


{4 Exercise 1.0}

  Program the interpreter above and test it on the examples.
{h <blockquote><pre>
  eval_0 : expr -> expressible_value
  interpret_0 : program -> expressible_value
</pre></blockquote>}
*)

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



(** {4 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.
{h <blockquote><pre>
      eval_1 : expr -> (expressible_value -> 'a) -> 'a
  interpret_1 : program -> expressible_value
</pre></blockquote>}
*)


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

(** {4 Exercise 1.2}

  Divide the continuation
{h <blockquote><pre>
    expressible_value -> 'a
</pre></blockquote>}
  in two:
{h <blockquote><pre>
    (value -> 'a) * (error -> 'a)
</pre></blockquote>}
  and adapt `eval_1` and `interpret_1` as
{h <blockquote><pre>
       eval_2 : expr -> (value -> 'a) -> (error -> 'a) -> 'a
  interpret_2 : program -> expressible_value
</pre></blockquote>}
*)



(*
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

(** {4 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
{h <blockquote><pre>
       eval_3 : expr -> (value -> expressible_value) -> expressible_value
  interpret_3 : program -> expressible_value
</pre></blockquote>}
  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


(** {4 Exercise 1.4}
  De-functionalize the continuation of `eval_3`.
{h <blockquote><pre>
         cont ::= ...

    continue_4 : cont -> value -> expressible_value
        eval_4 : expr -> cont -> expressible_value
  interprete_4 : program -> expressible_value
</pre></blockquote>}
  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

(**

One would want to write in Why:
{h <blockquote><pre>
function eval_cont (c:cont) (v:value) : value =
  match v with
  | Underflow -> Underflow
  | Vnum v ->
  match c with
  | A e2 k -> eval_cont (B (Vnum v) k) (eval_0 e2)
  | B v1 k -> eval_cont k (if v1 >= v then Vnum (v1 - v) else Underflow)
  | I -> Vnum v (* v >= 0 by construction *)
  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




(** {2 Reduction Semantics} *)

module ReductionSemantics

(**
A small step semantics, defined iteratively with reduction contexts
*)

  use Expr
  use DirectSem

(**
Expressions:
{h <blockquote><pre>
n  :  int

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

p  :  program
p ::= e
</pre></blockquote>}

Values:
{h <blockquote><pre>
v  :  value
v ::= n
</pre></blockquote>}

Potential Redexes:
{h <blockquote><pre>
  rp ::= n1 - n2
</pre></blockquote>}

Reduction Rule:
{h <blockquote><pre>
  n1 - n2 -> n3
</pre></blockquote>}
(in the case of relative integers Z, all potential redexes are true redexes;
 but for natural numbers, not all of them are true ones:
{h <blockquote><pre>
   n1 - n2 -> n3   if n1 >= n2
</pre></blockquote>}
a potential redex that is not a true one is stuck.)

Contraction Function:
{h <blockquote><pre>
  contract : redex_potentiel -> expression + stuck
  contract (n1 - n2) = n3   si n3 = n1 - n2
</pre></blockquote>}
and if there are only non-negative numbers:
{h <blockquote><pre>
  contract (n1 - n2) = n3     if n1 >= n2 and n3 = n1 - n2
  contract (n1 - n2) = stuck  if n1 < n2
</pre></blockquote>}
*)

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:
{h <blockquote><pre>
C  : cont
C ::= [] | [C e] | [v C]
</pre></blockquote>}
*)

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

(**
Recomposition:
{h <blockquote><pre>
             recompose : cont * expression -> expression
     recompose ([], e) = e
recompose ([C e2], e1) = recompose (C, e1 - e2)
recompose ([n1 C], e2) = recompose (C, n1 - e2)
</pre></blockquote>}
*)

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:
{h <blockquote><pre>
dec_or_val = (C, rp) | v
</pre></blockquote>}
Decomposition function:
{h <blockquote><pre>
             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, [])
</pre></blockquote>}
*)

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:
{h <blockquote><pre>
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)
</pre></blockquote>}
*)

(** {4 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:
{h <blockquote><pre>
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)))
</pre></blockquote>}
*)


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

(** {4 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




(** {4 Exercise 2.2}
  Derive an abstract machine
*)

(**
{h <blockquote><pre>
(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
</pre></blockquote>}
*)

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

(** {4 Exercise 2.3}
  An abstract machine for the case with errors
*)

(**

{h <blockquote><pre>
(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
</pre></blockquote>}

*)

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