module LambdaEval where

import Data.List        (lookup)

import LiquidPrelude   

{-# ANN module "spec   lambdaEval.hs.spec" #-}
{-# ANN module "hquals lambdaEval.hs.hquals" #-}

---------------------------------------------------------------------
----------------------- Datatype Definition -------------------------
---------------------------------------------------------------------

type Bndr 
  = Int

data Expr 
  = Lam Bndr Expr
  | Var Bndr  
  | App Expr Expr
  | Const Int
  | Plus Expr Expr
  | Pair Expr Expr
  | Fst Expr
  | Snd Expr

---------------------------------------------------------------------
-------------------------- The Evaluator ----------------------------
---------------------------------------------------------------------

evalVar :: Bndr -> [(Bndr, Expr)] -> Expr
Int
-> [(Int, {VV:Expr | (? isValue([VV]))})]
-> {VV:Expr | (? isValue([VV]))}evalVar Intx ((y,v):sto) 
  | {VV:Int | true,(VV = x)}x x:Int -> y:Int -> {VV:Bool | ((? VV) <=> (x = y))}`eq` {VV:Int | true,(VV = y)}y
  = {VV:Expr | (? isValue([VV])),(VV = v)}v
  | otherwise
  = Int
-> [(Int, {VV:Expr | (? isValue([VV]))})]
-> {VV:Expr | (? isValue([VV]))}evalVar {VV:Int | true,(VV = x)}x {VV:[(Int, {VV:Expr | (? isValue([VV]))})] | (VV = sto)}sto

evalVar x []      
  = forall a. [Char] -> aerror Addr# -> [Char]"unbound variable"

-- A "value" is simply: {v: Expr | (? (isValue v)) } *)

[(Int, {VV:Expr | (? isValue([VV]))})]
-> Expr
-> ([(Int, {VV:Expr | (? isValue([VV]))})],
    {VV:Expr | (? isValue([VV]))})eval [(Int, {VV:Expr | (? isValue([VV]))})]sto (Const i) 
  = forall a b. a -> b -> (a, b)({VV:[(Int, {VV:Expr | (? isValue([VV]))})] | true,(VV = sto)}sto, Int -> {VV:Expr | ((? isValue([VV])) <=> true)}Const {VV:Int | true,(VV = i)}i)

eval sto (Var x)  
  = forall a b. a -> b -> (a, b)({VV:[(Int, {VV:Expr | (? isValue([VV]))})] | true,(VV = sto)}sto, Int
-> [(Int, {VV:Expr | (? isValue([VV]))})]
-> {VV:Expr | (? isValue([VV]))}evalVar {VV:Int | true,(VV = x)}x {VV:[(Int, {VV:Expr | (? isValue([VV]))})] | true,(VV = sto)}sto) 

eval sto (Plus e1 e2)
  = let (_, e1') = eval sto e1
        (_, e2') = eval sto e2
    in case forall a b. a -> b -> (a, b)({VV:Expr | (VV = e1)}e1, {VV:Expr | (VV = e2)}e2) of
         (Const i1, Const i2) -> forall a b. a -> b -> (a, b)({VV:[(Int, {VV:Expr | (? isValue([VV]))})] | true,(VV = sto)}sto, Int -> {VV:Expr | ((? isValue([VV])) <=> true)}Const ({VV:Int | true,(VV = i1)}i1 forall a. ?Num a? -> a -> a -> a+ {VV:Int | true,(VV = i2)}i2))
         _                    -> forall a. [Char] -> aerror Addr# -> [Char]"non-integer addition"

eval sto (App e1 e2)
  = let (_,    v2 ) = [(Int, {VV:Expr | (? isValue([VV]))})]
-> Expr
-> ([(Int, {VV:Expr | (? isValue([VV]))})],
    {VV:Expr | (? isValue([VV]))})eval {VV:[(Int, {VV:Expr | (? isValue([VV]))})] | true,(VV = sto)}sto {VV:Expr | (VV = e2)}e2 
        (sto1, e1') = [(Int, {VV:Expr | (? isValue([VV]))})]
-> Expr
-> ([(Int, {VV:Expr | (? isValue([VV]))})],
    {VV:Expr | (? isValue([VV]))})eval {VV:[(Int, {VV:Expr | (? isValue([VV]))})] | true,(VV = sto)}sto {VV:Expr | (VV = e1)}e1
    in case {VV:([(Int, {VV:Expr | (? isValue([VV]))})],
     {VV:Expr | (? isValue([VV]))}) | true,(VV = X1)}e1' of
         (Lam x e) -> [(Int, {VV:Expr | (? isValue([VV]))})]
-> Expr
-> ([(Int, {VV:Expr | (? isValue([VV]))})],
    {VV:Expr | (? isValue([VV]))})eval (forall a b. a -> b -> (a, b)({VV:Int | true,(VV = x)}x, ([(Int, {VV:Expr | (? isValue([VV]))})],
 {VV:Expr | (? isValue([VV]))})v2)forall a. a -> [a] -> [a]: {VV:([(Int, {VV:Expr | (? isValue([VV]))})],
     {VV:Expr | (? isValue([VV]))}) | true,(VV = X1)}sto1) {VV:Expr | (VV = e)}e
         _         -> forall a. [Char] -> aerror Addr# -> [Char]"non-function application"

eval sto (Lam x e) 
  = forall a b. a -> b -> (a, b)({VV:[(Int, {VV:Expr | (? isValue([VV]))})] | true,(VV = sto)}sto, Int -> Expr -> {VV:Expr | ((? isValue([VV])) <=> true)}Lam {VV:Int | true,(VV = x)}x {VV:Expr | (VV = e)}e)

eval sto (Pair e1 e2)
  = forall a b. a -> b -> (a, b)({VV:[(Int, {VV:Expr | (? isValue([VV]))})] | true,(VV = sto)}sto, e1:Expr
-> e2:Expr
-> {VV:Expr | ((? isValue([VV])) <=> && [(? isValue([e1]));
                                         (? isValue([e2]))])}Pair ([(Int, {VV:Expr | (? isValue([VV]))})],
 {VV:Expr | (? isValue([VV]))})v1 ([(Int, {VV:Expr | (? isValue([VV]))})],
 {VV:Expr | (? isValue([VV]))})v2)
  where (_, v1) = [(Int, {VV:Expr | (? isValue([VV]))})]
-> Expr
-> ([(Int, {VV:Expr | (? isValue([VV]))})],
    {VV:Expr | (? isValue([VV]))})eval {VV:[(Int, {VV:Expr | (? isValue([VV]))})] | true,(VV = sto)}sto {VV:Expr | (VV = e1)}e1
        (_, v2) = [(Int, {VV:Expr | (? isValue([VV]))})]
-> Expr
-> ([(Int, {VV:Expr | (? isValue([VV]))})],
    {VV:Expr | (? isValue([VV]))})eval {VV:[(Int, {VV:Expr | (? isValue([VV]))})] | true,(VV = sto)}sto {VV:Expr | (VV = e2)}e2

eval sto (Fst e)
  = let (sto', e') = [(Int, {VV:Expr | (? isValue([VV]))})]
-> Expr
-> ([(Int, {VV:Expr | (? isValue([VV]))})],
    {VV:Expr | (? isValue([VV]))})eval {VV:[(Int, {VV:Expr | (? isValue([VV]))})] | true,(VV = sto)}sto {VV:Expr | (VV = e)}e in
    case {VV:([(Int, {VV:Expr | (? isValue([VV]))})],
     {VV:Expr | (? isValue([VV]))}) | true,(VV = X1)}e' of
      Pair v _ -> forall a b. a -> b -> (a, b)({VV:([(Int, {VV:Expr | (? isValue([VV]))})],
     {VV:Expr | (? isValue([VV]))}) | true,(VV = X1)}sto', {VV:Expr | (VV = v)}v)
      _        -> forall a. [Char] -> aerror Addr# -> [Char]"non-tuple fst"

eval sto (Snd e)
  = let (sto', e') = [(Int, {VV:Expr | (? isValue([VV]))})]
-> Expr
-> ([(Int, {VV:Expr | (? isValue([VV]))})],
    {VV:Expr | (? isValue([VV]))})eval {VV:[(Int, {VV:Expr | (? isValue([VV]))})] | true,(VV = sto)}sto {VV:Expr | (VV = e)}e in
    case {VV:([(Int, {VV:Expr | (? isValue([VV]))})],
     {VV:Expr | (? isValue([VV]))}) | true,(VV = X1)}e' of
      Pair _ v -> forall a b. a -> b -> (a, b)({VV:([(Int, {VV:Expr | (? isValue([VV]))})],
     {VV:Expr | (? isValue([VV]))}) | true,(VV = X1)}sto', {VV:Expr | (VV = v)}v)
      _        -> forall a. [Char] -> aerror Addr# -> [Char]"non-tuple snd"

---------------------------------------------------------------------
-------------------------- Value Checker ----------------------------
---------------------------------------------------------------------

{VV:Expr | (? isValue([VV]))} -> Boolcheck (Const _)    = {VV:Bool | (? VV),(VV = True)}True
check (Lam _ _)    = {VV:Bool | (? VV),(VV = True)}True
check (Var _)      = {VV:Bool | (? VV)} -> {VV:Bool | (? VV)}assert {VV:Bool | (~ ((? VV))),(VV = False)}False
check (App _ _)    = {VV:Bool | (? VV)} -> {VV:Bool | (? VV)}assert {VV:Bool | (~ ((? VV))),(VV = False)}False
check (Pair v1 v2) = {VV:Expr | (? isValue([VV]))} -> Boolcheck {VV:Expr | (VV = v1)}v1 Bool -> Bool -> Bool&& {VV:Expr | (? isValue([VV]))} -> Boolcheck {VV:Expr | (VV = v2)}v2
check (Fst _)      = {VV:Bool | (? VV)} -> {VV:Bool | (? VV)}assert {VV:Bool | (~ ((? VV))),(VV = False)}False
check (Snd _)      = {VV:Bool | (? VV)} -> {VV:Bool | (? VV)}assert {VV:Bool | (~ ((? VV))),(VV = False)}False
check (Plus _ _)   = {VV:Bool | (? VV)} -> {VV:Bool | (? VV)}assert {VV:Bool | (~ ((? VV))),(VV = False)}False

---------------------------------------------------------------------
-------------------------- Unit Tests -------------------------------
---------------------------------------------------------------------

[Bool]tests =
  let ({VV:Int | (VV < g),(VV < x),(VV <= g),(VV <= x),(0 <= VV),(0 = VV)}f,{VV:Int | (VV < x),(VV <= x),(0 <= VV),(VV = 1)}g,{VV:Int | (0 <= VV)}x) = forall a b c. a -> b -> c -> (a, b, c)(x:Int# -> {VV:Int | (VV = x)}0,x:Int# -> {VV:Int | (VV = x)}1,x:Int# -> {VV:Int | (VV = x)}2) 
      {VV:Expr | ((? isValue([VV])) <=> true)}e1      = Int -> Expr -> {VV:Expr | ((? isValue([VV])) <=> true)}Lam {VV:Int | (0 <= VV),(VV = x)}x (Int -> {VV:Expr | ((? isValue([VV])) <=> false)}Var {VV:Int | (0 <= VV),(VV = x)}x)
      e2      = Expr -> Expr -> {VV:Expr | ((? isValue([VV])) <=> false)}App {VV:Expr | ((? isValue([VV])) <=> true),(VV = e1)}e1 {VV:Expr | ((? isValue([VV])) <=> true),(VV = e1)}e1 
      {VV:Expr | ((? isValue([VV])) <=> true)}e3      = Int -> Expr -> {VV:Expr | ((? isValue([VV])) <=> true)}Lam {VV:Int | (VV < g),
          (VV < x),
          (VV <= g),
          (VV <= x),
          (0 <= VV),
          (0 = VV),
          (VV = f)}f (Int -> Expr -> {VV:Expr | ((? isValue([VV])) <=> true)}Lam {VV:Int | (VV < x),(VV <= x),(0 <= VV),(VV = 1),(VV = g)}g (Int -> Expr -> {VV:Expr | ((? isValue([VV])) <=> true)}Lam {VV:Int | (0 <= VV),(VV = x)}x (Expr -> Expr -> {VV:Expr | ((? isValue([VV])) <=> false)}App (Int -> {VV:Expr | ((? isValue([VV])) <=> false)}Var {VV:Int | (VV < g),
          (VV < x),
          (VV <= g),
          (VV <= x),
          (0 <= VV),
          (0 = VV),
          (VV = f)}f)  (Expr -> Expr -> {VV:Expr | ((? isValue([VV])) <=> false)}App (Int -> {VV:Expr | ((? isValue([VV])) <=> false)}Var {VV:Int | (VV < x),(VV <= x),(0 <= VV),(VV = 1),(VV = g)}g) (Int -> {VV:Expr | ((? isValue([VV])) <=> false)}Var {VV:Int | (0 <= VV),(VV = x)}x)))))
      {VV:Expr | ((? isValue([VV])) <=> true)}e4      = Int -> {VV:Expr | ((? isValue([VV])) <=> true)}Const x:Int# -> {VV:Int | (VV = x)}10
      e5      = Expr -> Expr -> {VV:Expr | ((? isValue([VV])) <=> false)}App {VV:Expr | ((? isValue([VV])) <=> true),(VV = e1)}e1 {VV:Expr | ((? isValue([VV])) <=> true),(VV = e4)}e4
      {VV:Expr | ((? isValue([VV])) <=> true)}e6      = Int -> Expr -> {VV:Expr | ((? isValue([VV])) <=> true)}Lam {VV:Int | (0 <= VV),(VV = x)}x (Expr -> Expr -> {VV:Expr | ((? isValue([VV])) <=> false)}Plus (Int -> {VV:Expr | ((? isValue([VV])) <=> false)}Var {VV:Int | (0 <= VV),(VV = x)}x) {VV:Expr | ((? isValue([VV])) <=> true),(VV = e4)}e4)
      {VV:Expr | ((? isValue([VV])) <=> false)}e7      = Expr -> Expr -> {VV:Expr | ((? isValue([VV])) <=> false)}App (Expr -> Expr -> {VV:Expr | ((? isValue([VV])) <=> false)}App {VV:Expr | ((? isValue([VV])) <=> true),(VV = e3)}e3 {VV:Expr | ((? isValue([VV])) <=> true),(VV = e6)}e6) {VV:Expr | ((? isValue([VV])) <=> true),(VV = e6)}e6
      Expre8      = e1:Expr
-> e2:Expr
-> {VV:Expr | ((? isValue([VV])) <=> && [(? isValue([e1]));
                                         (? isValue([e2]))])}Pair (Expr -> Expr -> {VV:Expr | ((? isValue([VV])) <=> false)}App {VV:Expr | ((? isValue([VV])) <=> false),(VV = e7)}e7 (Int -> {VV:Expr | ((? isValue([VV])) <=> true)}Const x:Int# -> {VV:Int | (VV = x)}0)) (Expr -> Expr -> {VV:Expr | ((? isValue([VV])) <=> false)}App {VV:Expr | ((? isValue([VV])) <=> false),(VV = e7)}e7 (Int -> {VV:Expr | ((? isValue([VV])) <=> true)}Const x:Int# -> {VV:Int | (VV = x)}100))
      {VV:Expr | ((? isValue([VV])) <=> false)}e9      = Expr -> {VV:Expr | ((? isValue([VV])) <=> false)}Fst {VV:Expr | (VV = e8)}e8
      e10     = Expr -> {VV:Expr | ((? isValue([VV])) <=> false)}Snd {VV:Expr | ((? isValue([VV])) <=> false),(VV = e9)}e9
      vs      = forall a b. (a -> b) -> [a] -> [b]map (forall a b. (a, b) -> bsnd forall a b c. (a -> b) -> (c -> a) -> c -> b. [(Int, {VV:Expr | (? isValue([VV]))})]
-> Expr
-> ([(Int, {VV:Expr | (? isValue([VV]))})],
    {VV:Expr | (? isValue([VV]))})eval forall a. [a][]) forall a. a -> [a] -> [a][{VV:Expr | ((? isValue([VV])) <=> true),(VV = e1)}e1, e2, {VV:Expr | ((? isValue([VV])) <=> true),(VV = e3)}e3, {VV:Expr | ((? isValue([VV])) <=> true),(VV = e4)}e4, e5, {VV:Expr | ((? isValue([VV])) <=> true),(VV = e6)}e6, {VV:Expr | ((? isValue([VV])) <=> false),(VV = e7)}e7, {VV:Expr | (VV = e8)}e8, {VV:Expr | ((? isValue([VV])) <=> false),(VV = e9)}e9, e10]
  in forall a b. (a -> b) -> [a] -> [b]map {VV:Expr | (? isValue([VV]))} -> Boolcheck vs