(*
type exp =
  | Const int
  | Sub exp exp

type context = exp -> exp

function eval (e: exp) : int = match e with
  | Const n -> n
  | Sub e1 e2 ->
     (eval e1) - (eval e2)
  end

predicate is_redex (e: exp) = match e with
  | Sub (Const _) (Const _) -> true
  | _ -> false
  end

let head_reduction (e: exp) : exp
  requires { is_redex e }
  ensures  { eval result = eval e }
= match e with
  | Sub (Const v1) (Const v2) ->
     Const (v1 - v2)
  | _ -> absurd
  end

predicate is_value (e: exp) = match e with
  | Const _ -> true
  | _ -> false
  end

(* given an expression calculate the corresponding reduction context *)
let rec decompose_term (e: exp) (c: context) : (contex, exp)
  requires { not (is_value e) }
  returns  { let (c', e') = result in
               is_redex e' && forall res.post c e res -> post c' e' res }
= match e with
  | Const _ ->
     (* a value is not a hole *)
     assert false
  | Sub (Const v1, Const v2) as e ->
     (* this exp can be head-reduced so it is a whole hole *)
     (c, e)
  | Sub (Const v1, e) ->
     (* this exp corresponds to a right application context *)
     decompose_term e (fun x -> ensures { post c (Sub (Const v) x) result } c (Sub (Const v) x))
  | Sub (e1, e2) ->
     (* this expression corresponds to a left application context *)
     decompose_term e1 (fun x -> ensures { post c (Sub x e) result } c (Sub x e2))

let decompose (e: exp) : (context, exp)
  requires { not (is_value e) }
  ensures  { let (c', e') = result in is_redex e' && post c' e' e }
= decompose_term (fun x -> x) e

let red (e: exp) : int
  ensures { result = eval e }
= match e with
  | Const v -> v
  | _ ->
     let (c, r) = decompose e in
     let     r' = head_reduction r in
     red (c r')
*)

module Exp

  use export int.Int

  type exp =
    | Const int
    | Sub exp exp

  type prog = exp

end

module DirecSem

  use Exp

  function eval (e: exp) : int = match e with
    | Const n -> n
    | Sub e1 e2 ->
       (eval e1) - (eval e2)
    end

end

module ReductionSemantics

  use Exp
  use DirecSem

  predicate is_value (e: exp) = match e with
    | Const _ -> true
    | _ -> false
    end

  predicate is_redex (e: exp) = match e with
    | Sub (Const _) (Const _) -> true
    | _ -> false
    end

  let head_reduction (e: exp) : exp
    requires { is_redex e }
    ensures  { eval result = eval e }
  = match e with
    | Sub (Const v1) (Const v2) ->
       Const (v1 - v2)
    | _ -> absurd
    end

  type context =
    | KHole
    | KApp_left context exp
    | KApp_right int context

  predicate post (k: context) (arg result: exp) = match k with
    | KHole -> arg = result
    | KApp_left c e -> post c (Sub arg e) result
    | KApp_right n c -> post c (Sub (Const n) arg) result
    end

  let rec decompose_term (e: exp) (c: context) : (context, exp)
    requires { not (is_value e) }
    returns  { (c', e') ->
                 is_redex e' && forall res. post c e res -> post c' e' res }
    variant  { e }
  = match e with
    | Const _ ->
       absurd
    | Sub (Const _) (Const _) ->
       (c, e)
    | Sub (Const v1) e ->
       decompose_term e (KApp_right v1 c)
    | Sub e1 e2 ->
       decompose_term e1 (KApp_left c e2)
    end

  let decompose (e: exp) : (context, exp)
    requires { not (is_value e) }
    returns  { (c', e') -> post c' e' e && is_redex e' }
  = decompose_term e KHole

  let rec apply (k: context) (arg: exp) : exp
    ensures { post k arg result }
    variant { k }
  = match k with
    | KHole ->
       let x = arg in x
    | KApp_left c e ->
       let x = arg in
       apply c (Sub x e)
    | KApp_right n c ->
       let x = arg in
       apply c (Sub (Const n) x)
    end

  let rec lemma post_eval (k: context) (arg1 arg2 r1 r2: exp)
    requires { eval arg1 = eval arg2 }
    requires { post k arg1 r1 && post k arg2 r2 }
    ensures  { eval r1 = eval r2 }
    variant  { k }
  = match k with
    | KHole -> ()
    | KApp_left c e ->
       post_eval c (Sub arg1 e) (Sub arg2 e) r1 r2
    | KApp_right n c ->
       post_eval c (Sub (Const n) arg1) (Sub (Const n) arg2) r1 r2
    end

  let rec red (e: exp) : int
    ensures { result = eval e }
    diverges
  = match e with
    | Const v -> v
    | _ ->
       let (cxt, e') = decompose e in
       let       r' = head_reduction e' in
       red (apply cxt r')
    end

end