module LambdaEval where
import Data.List (lookup)
import LiquidPrelude
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
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"
[(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"
{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
[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