(* The 2nd Verified Software Competition (VSTTE 2012)
   https://sites.google.com/site/vstte2012/compet

   Problem 2:
   Combinators S and K *)

module Combinators
  type term = S | K | App term term

  let rec predicate eq (x y : term)
    ensures { result <-> x = y }
  = match x, y with
    | S, S -> True
    | K, K -> True
    | App x1 x2, App y1 y2 -> eq x1 y1 && eq x2 y2
    | _, _ -> False
    end

  (* specification of the CBV reduction *)

  predicate is_value (t: term) = match t with
    | K | S -> true
    | App K v | App S v -> is_value v
    | App (App S v1) v2 -> is_value v1 /\ is_value v2
    | _ -> false
  end

  (* contexts *)

  type context = Hole | Left context term | Right term context

  predicate is_context (c: context) = match c with
    | Hole -> true
    | Left c _ -> is_context c
    | Right v c -> is_value v && is_context c
  end

  function subst (c: context) (t: term) : term = match c with
    | Hole -> t
    | Left c1 t2 -> App (subst c1 t) t2
    | Right v1 c2 -> App v1 (subst c2 t)
  end

  (* one step reduction
     (the notion of context is inlined in the following definition) *)

  inductive (-->) (t1 t2: term) =
    | red_K:
       forall c: context. is_context c ->
       forall v1 v2: term. is_value v1 -> is_value v2 ->
       subst c (App (App K v1) v2) --> subst c v1
    | red_S:
       forall c: context. is_context c ->
       forall v1 v2 v3: term. is_value v1 -> is_value v2 -> is_value v3 ->
       subst c (App (App (App S v1) v2) v3) -->
       subst c (App (App v1 v3) (App v2 v3))

  clone relations.ReflTransClosure
    with type t = term, predicate rel = (-->)
  predicate (-->*) (t1 t2: term) = relTR t1 t2

  type zipper = ZHole | ZLeft context term | ZRight term context

  let rec function subst_c (c ct:context) : context
    ensures { is_context c /\ is_context ct -> is_context result }
  = match c with
    | Hole -> ct
    | Left c1 t2 -> Left (subst_c c1 ct) t2
    | Right v1 c2 -> Right v1 (subst_c c2 ct)
    end

  lemma subst_c_commute : forall c [@induction] ct t.
    subst c (subst ct t) = subst (subst_c c ct) t

  (* task 1: implement CBV reduction *)

  let rec reduction (ghost c:context) (t: term) : term
    diverges (* there are non-normalizable terms... *)
    requires { is_context c }
    ensures { subst c t -->* subst c result }
    ensures { is_value result }
  = match t with
    | S -> S
    | K -> K
    | App t1 t2 ->
      let v1 = reduction (subst_c c (Left Hole t2)) t1 in
      let v2 = reduction (subst_c c (Right v1 Hole)) t2 in
      match v1 with
      | K | S | App S _ -> App v1 v2
      | App K v3 -> v3
      | App (App S v3) v4 -> reduction c (App (App v3 v2) (App v4 v2))
      | _ -> absurd
      end
    end

  exception BenchFailure

  let constant i = App (App S K) K

  let test_SKK ()
    diverges (* would be hard to prove terminating *)
    raises { BenchFailure -> true }
  = let t1 = reduction Hole (App i i) in
    if not (eq t1 i) then raise BenchFailure;
    let t2 = reduction Hole (App (App (App (App K K) K) K) K) in
    if not (eq t2 K) then raise BenchFailure;
    t1, t2

  (* an irreducible term is a value *)
  predicate irreducible (t: term) = forall t': term. not (t-->t')

  exception Fail
  let rec ghost reduce_step (c:context) (t:term) : term
    requires { is_context c }
    ensures  { subst c t --> subst c result }
    raises   { Fail -> is_value t }
    variant  { t }
  = match t with
    | App t1 t2 ->
      try App (reduce_step (subst_c c (Left Hole t2)) t1) t2 with Fail ->
      try App t1 (reduce_step (subst_c c (Right t1 Hole)) t2) with Fail ->
      match t1 with
      | App K v -> v
      | App (App S v1) v2 -> App (App v1 t2) (App v2 t2)
      | _ -> raise Fail
      end end end
    | _ -> raise Fail
    end

  let rec lemma value_in_context (c:context) (t:term) : unit
    requires { is_value (subst c t) }
    ensures  { is_value t }
    variant  { c }
  = match c with
    | Hole -> ()
    | Left cl _ -> value_in_context cl t
    | Right _ cr -> value_in_context cr t
    end

  let lemma irreducible_is_value (t:term) : unit
    ensures { irreducible t <-> is_value t }
  = try let _ = reduce_step Hole t in () with Fail -> () end

  (* task 2 *)

  use int.Int

  inductive only_K (t: term) =
    | only_K_K:
        only_K K
    | only_K_App:
        forall t1 t2: term. only_K t1 -> only_K t2 -> only_K (App t1 t2)

  let rec reduction2 (ghost c:context) (t: term) : term
    requires { only_K t /\ is_context c }
    ensures { only_K result /\ is_value result }
    ensures { subst c t -->* subst c result }
    variant { t }
  = match t with
    | K -> K
    | App t1 t2 ->
      let v1 = reduction2 (subst_c c (Left Hole t2)) t1 in
      let v2 = reduction2 (subst_c c (Right v1 Hole)) t2 in
      match v1 with
      | K -> App v1 v2
      | App K v3 -> v3
      | _ -> absurd
      end
    | _ -> absurd
    end

  (* task 3 *)

  let rec function ks (n: int) : term
    requires { n >= 0 }
    ensures  { only_K result }
    variant { n }
  = if n = 0 then K else App (ks (n-1)) K

  use number.Parity

  let rec reduction3 (ghost c:context) (ghost n:int) (t: term) : term
    requires { n >= 0 /\ t = ks n /\ is_context c }
    variant { n }
    ensures { subst c t -->* subst c result }
    ensures { is_value result }
    ensures { even n -> result = K }
    ensures { odd n -> result = App K K }
  = match t with
    | K -> K
    | App t1 t2 ->
      let v1 = reduction3 (subst_c c (Left Hole t2)) (n-1) t1 in
      let v2 = reduction3 (subst_c c (Right v1 Hole)) 0 t2 in
      match v1 with
      | K -> App v1 v2
      | App K v3 -> v3
      | _ -> absurd
      end
    | _ -> absurd
    end

  let lemma ks_even_odd (n:int) : unit
    requires { n >= 0 }
    ensures  { ks (2*n) -->* K }
    ensures  { ks (2*n+1) -->* App K K }
  = let _ = reduction3 Hole (2*n) (ks (2*n)) in
    let _ = reduction3 Hole (2*n+1) (ks (2*n+1)) in
    ()

end