{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE NoMonomorphismRestriction #-}

module Symantic.Semantics.LetInserterSpec where

import Data.Function (($), (.))
import Data.Functor.Identity (Identity (..))
import Data.Int (Int)
import Data.Maybe (Maybe (..))
import Data.Semigroup (Semigroup (..))
import Debug.Trace (trace)
import Language.Haskell.TH.Syntax qualified as TH
import Symantic.Semantics.LetInserter
import Symantic.Semantics.Viewer
import Symantic.Syntaxes.Classes (Abstractable (..), Constantable, Equalable (..), IfThenElseable (..), Instantiable (..), LetRecable (..), Letable (..), int, unit, (==))
import Test.Syd
import Test.Syd.Validity
import Text.Show (show)
import Prelude qualified as P

import Symantic.Syntaxes.Extras

-- import Debug.Trace (traceShow)

p12 ::
  Addable sem =>
  Instantiable sem =>
  Constantable Int sem =>
  sem Int
p12 = int 1 + int 2

{-
t1 ::
  Abstractable sem =>
  Instantiable sem =>
  Multiplicable sem =>
  Addable sem =>
  Constantable Int sem =>
  --GHC.Num.Num (sem Int) =>
  sem Int -> sem Int
-}
t1 = (\x -> x * (x + int 1))
c1 = t1 p12

t2 x = let_ x (\y -> y * (y + int 1))
c2 = t2 p12
ft1 t x = lam (\u -> t x + t (x + u))
c3 = ft1 t2 p12

p12l loc = genLetAt loc (int 1 + int 2)
c1l = withLocus \loc -> p12l loc

ft11 loc = \t -> \x -> lam (\u -> t x + t (genLetAt loc (x + u)))
c3l1 = withLocus \loc -> ft11 loc t1 (p12l loc)

ft12 = \t -> \x -> lam (\u -> withLocus \loc -> t x + t (genLetAt loc (x + u)))
c3l2 = withLocus \loc -> ft12 t1 (p12l loc)

r12 :: Int
r12 = runIdentity (runLetInserter p12)
runLII = runIdentity . runLetInserter

{-
-- letrec (fun self m -> lam @@ fun n ->
--   if_ (m =. int 0) (n + (int 1)) @@
--      if_ (n =. int 0) (self / (m - int 1) / int 1) @@
--          self / (m - int 1) / (self / m / (n - int 1))
--   ) @@ fun ack -> ack / int 2
fib =
  letR
    (\self ->
      \n ->
        ifThenElse (n == int 0) (log "n==0" (int 1)) $
        ifThenElse (n == int 1) (log "n==1" (int 2)) $
        self .@ int 2
    )
    (\res -> res)
let sac2 = sack 2
;;
ack2 =
  letR
    (\self -> \m ->
      lam $ \n ->
        ifThenElse (m == int 0) (n + int 1) $
        ifThenElse (n == int 0) (self .@ (m - int 1) .@ int 1) $
        self .@ (m - int 1) .@ (self .@ m .@ (n - int 1))
    )
    (\res -> res .@ int 2)

let fibonacci n =
  let rec loop n (x,y) =·
    if n = 0 then x else if n = 1 then y else·
    .< .~(loop (n-1) (x,y)) + .~(loop (n-2) (x,y)) >.
  in .< fun x y -> .~(loop n (.< x >. , .< y >.)) >.

-}

-- derive
quote :: LetInserter (AnnotatedCode code) a -> LetInserter (AnnotatedCode code) a
-- quote :: sem a -> a
quote = P.id

-- liftDerived
unquote :: a -> sem a
unquote = P.undefined

-- unQ ::

{-
fibonacci ::
  ( P.Eq (sem Int)
  , P.Num (sem Int)
  , Substractable sem
  , Instantiable sem
  ) =>
  sem Int -> sem2 Int -> sem3 Int
fibonacci ::
  ( Addable code
  , Abstractable (LetInserter (AnnotatedCode code))
  , Instantiable code
  ) => Int -> LetInserter (AnnotatedCode code) (Int -> Int -> Int)
fibonacci m =
  let loop n (x,y) =
        if n P.== 0 then x else
        if n P.== 1 then y else
        quote (loop (n P.-1) (x, y) + loop (n P.-2) (x, y))
  in quote (lam $ \x -> lam $ \y -> loop m (x, y))
-}

{-
(* Specialized to m. Without memoization, it diverges *)
let sack m =
  with_locus_rec @@ fun l ->
  let g = mkgenlet l (=) in
  let rec loop m =
    if m = 0 then .<fun n -> n + 1>. else
    .<fun n -> if n = 0 then .~(g loop (m-1)) 1
    else .~(g loop (m-1)) (.~(g loop m) (n-1))>.
  in g loop m
;;
-}
-- https://en.wikipedia.org/wiki/Ackermann_function
-- Specialized to m. Without memoization, it diverges
sack ::
  Abstractable code =>
  Addable code =>
  Constantable Int code =>
  Equalable code =>
  IfThenElseable code =>
  Instantiable code =>
  LetRecable Int code =>
  Letable code =>
  Substractable code =>
  Int ->
  LetInserter code (Int -> Int)
sack m0 =
  withLocusRec $ \l ->
    let
      memoLoop k = genLetMemoRec l (P.fromIntegral k) (loop k)
      loop 0 =
        traceShow (["sack", "loop"], ("m", 0 :: Int)) $
          lam $
            \n -> n + int 1
      loop m =
        traceShow (["sack", "loop"], ("m", m)) $
          lam $ \n ->
            ifThenElse
              (n == int 0)
              (memoLoop (m P.- 1) .@ int 1)
              (memoLoop (m P.- 1) .@ (memoLoop m .@ (n - int 1)))
    in
      memoLoop m0

-- https://simple.wikipedia.org/wiki/Fibonacci_number
fibonacci ::
  Addable code =>
  Abstractable code =>
  Letable code =>
  Instantiable code =>
  LetRecable Int code =>
  Int ->
  LetInserter code (Int -> Int -> Int)
fibonacci m =
  withLocusRec $ \loc ->
    let
      memoLoop k = genLetMemoRec loc (P.fromIntegral k) (loop k)
      loop n =
        if n P.== 0
          then lam $ \x -> lam $ \_y -> x
          else
            if n P.== 1
              then lam $ \_x -> lam $ \y -> y
              else lam $ \x -> lam $ \y ->
                add
                  .@ (memoLoop (n P.- 1) .@ x .@ y)
                  .@ (memoLoop (n P.- 2) .@ x .@ y)
    in
      loop m

-- (int -> int -> int) code =
-- .< fun x_1 -> fun y_2 -> (((y_2 + x_1) + y_2) + (y_2 + x_1)) + ((y_2 + x_1) + y_2)>.
tfib :: TH.Quote m => Int -> TH.Code m (Int -> Int -> Int)
tfib m =
  let loop n (x, y) =
        if n P.== 0
          then x
          else
            if n P.== 1
              then y
              else [||$$(loop (n P.- 1) (x, y)) P.+ $$(loop (n P.- 2) (x, y))||]
  in [||\x y -> $$(loop m ([||x||], [||y||]))||]

{-
acs :: Int -> LetInserter (AnnotatedCode Viewer) (Int -> Int)
acs m =
  withLocusRec $ \l ->
  letR
    (\self -> --lam $ \mm ->
      lam $ \n ->
        --if (runIdentity m P.== 0) then (n + int 1) else
        ifThenElse (n == int 0) n $
          --genLetMemoRec l m
          (self .@ int m) .@ (n - int 1)
        --ifThenElse (m == int 0) (n + int 1) $
        --ifThenElse (n == int 0) (self .@ (m - int 1) .@ int 1) $
        --genLetMemo l m $ self .@ (m - int 1) .@ (self .@ m .@ (n - int 1))
    )
    (\self -> genLetMemoRec l (2) (self .@ int 2))
-}
ack :: Int -> Int -> Int
ack 0 n = trace ("ack 0 " <> show n) $ n P.+ 1
ack m 0 = trace ("ack " <> show m <> " 0") $ ack (m P.- 1) 1
ack m n = trace ("ack " <> show n <> " " <> show m) $ ack (m P.- 1) (ack m (n P.- 1))

spec :: Spec
spec = do
  describe "let_" do
    it "can bind a literal" do
      view (runLetInserter (let_ (int 3) (\v -> int 4 + v)))
        `shouldBe` "let x1 = 3 in 4 + x1"
    it "can bind an expression of literals" do
      view (runLetInserter (let_ (int 1 + int 2) (\v -> int 4 + v)))
        `shouldBe` "let x1 = 1 + 2 in 4 + x1"
    it "can bind a variable" do
      view (runLetInserter (lam (\x -> let_ x (\v -> int 4 + v))))
        `shouldBe` "\\x1 -> let x2 = x1 in 4 + x2"
    it "can bind an expression with a variable" do
      view (runLetInserter (lam (\x -> let_ (x + int 1) (\v -> int 4 + v))))
        `shouldBe` "\\x1 -> let x2 = x1 + 1 in 4 + x2"
  describe "genLet" do
    it "can bind" do
      let exp = int 1 + genLet (int 2)
      view (runLetInserter exp) `shouldBe` "let x1 = 2 in 1 + x1"
      runIdentity (runLetInserter exp) `shouldBe` 3
    it "can bind a literal across a lambda" do
      let exp = lam (\x -> x + genLet (int 2))
      view (runLetInserter exp) `shouldBe` "let x1 = 2 in \\x2 -> x2 + x1"
      runIdentity (runLetInserter exp) 1 `shouldBe` 3
    it "can bind an operation across a lambda" do
      let exp = lam (\x -> x + genLet (int 1 + int 2))
      view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in \\x2 -> x2 + x1"
      runIdentity (runLetInserter exp) 1 `shouldBe` 4
    it "can wrap a variable" do
      let exp = lam (\x -> withLocus (\l -> x + genLetAt l x))
      view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 in x1 + x2"
      runIdentity (runLetInserter exp) 1 `shouldBe` 2
    -- This must not raise a lookupVar failure for var=([1])  env=[]
    it "cannot cause a scope extrusion using withLocus" do
      view (runLetInserter (withLocus (\l -> lam (\x -> x + genLetAt l x))))
        `shouldBe` "\\x1 -> let x2 = x1 in x1 + x2"
    -- Check that 'lam' limits the scope extrusion:
    -- as soon as that passing a virtual binding would
    -- make a variable extrude its scope, this virtual binding is bound.
    it "has its locus limited by lam when wrapping its variable" do
      let exp = lam (\x -> x + genLet x)
      view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 in x1 + x2"
      runIdentity (runLetInserter exp) 1 `shouldBe` 2
    it "does not have its locus limited by lam when not wrapping its variable" do
      let exp = lam (\x -> x + genLet (int 1))
      view (runLetInserter exp) `shouldBe` "let x1 = 1 in \\x2 -> x2 + x1"
      runIdentity (runLetInserter exp) 1 `shouldBe` 2
    it "can wrap let_" do
      let exp = lam (\x -> x + genLet (let_ (int 1) (\y -> y)))
      view (runLetInserter exp) `shouldBe` "let x1 = let x2 = 1 in x2 in \\x2 -> x2 + x1"
      runIdentity (runLetInserter exp) 1 `shouldBe` 2
    it "can have its locus limited by withLocus" do
      let exp = lam (\x -> withLocus (\l -> x + genLetAt l (let_ (int 1) (\y -> y))))
      view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = let x3 = 1 in x3 in x1 + x2"
      runIdentity (runLetInserter exp) 1 `shouldBe` 2
    it "can wrap lam and a variable" do
      let exp = lam (\x -> x + genLet (lam (\_y -> x)) .@ unit)
      view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = \\x3 -> x1 in x1 + x2 ()"
      runIdentity (runLetInserter exp) 1 `shouldBe` 2
    it "can wrap lam and be called" do
      let exp = lam (\x -> x + genLet (lam (\y -> y + int 2)) .@ x)
      view (runLetInserter exp) `shouldBe` "let x1 = \\x2 -> x2 + 2 in \\x2 -> x2 + x1 x2"
      runIdentity (runLetInserter exp) 1 `shouldBe` 4
    it "can wrap a variable in an operation" do
      let exp = lam (\x -> x + genLet (x + int 1))
      view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 + 1 in x1 + x2"
      runIdentity (runLetInserter exp) 1 `shouldBe` 3
    it "can wrap literals inside an expression with two variables" do
      let exp = lam (\x -> lam (\y -> x + y + genLet (int 2 + int 3)))
      view (runLetInserter exp) `shouldBe` "let x1 = 2 + 3 in \\x2 -> \\x3 -> x2 + x3 + x1"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 10
    it "can wrap the farthest variable inside two lam" do
      let exp = lam (\x -> lam (\y -> x + y + genLet x))
      view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 in \\x3 -> x1 + x3 + x2"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 6
    it "can wrap another variable inside two lam" do
      let exp = lam (\x -> lam (\y -> x + y + genLet y))
      view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = x2 in x1 + x2 + x3"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 9
    it "can wrap another variable inside two lam" do
      let exp = lam (\x -> lam (\y -> x + y + genLet y))
      view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = x2 in x1 + x2 + x3"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 9
    it "can wrap the farthest variable in an expression inside two lam" do
      let exp = lam (\x -> lam (\y -> x + y + genLet (x + int 1)))
      view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 + 1 in \\x3 -> x1 + x3 + x2"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 7
    it "can wrap the closest variable in an expression inside two lam" do
      let exp = lam (\x -> lam (\y -> x + y + genLet (y + int 1)))
      view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = x2 + 1 in x1 + x2 + x3"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 10
    it "can wrap both variables in an expression inside two lam" do
      let exp = lam (\x -> lam (\y -> x + y + genLet (y + int 1 + x)))
      view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = x2 + 1 + x1 in x1 + x2 + x3"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 11
    it "can be nested" do
      let exp = lam (\x -> lam (\y -> x + y + genLet (genLet (y + int 1 + x))))
      view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = x2 + 1 + x1 in let x4 = x3 in x1 + x2 + x4"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 11
    it "can be nested within an expression of literals" do
      let exp = lam (\x -> lam (\y -> x + y + genLet (y + genLet (int 1 + int 2))))
      view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in \\x2 -> \\x3 -> let x4 = x3 + x1 in x2 + x3 + x4"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 12
    it "can be nested within an expression with a variable" do
      let exp = lam (\x -> lam (\y -> x + y + genLet (y + genLet (int 1 + x))))
      view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = 1 + x1 in \\x3 -> let x4 = x3 + x2 in x1 + x3 + x4"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 11
    it "can be nested within an expression with two variables" do
      let exp = lam (\x -> lam (\y -> x + y + genLet (y + genLet (int 1 + x + y))))
      view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = 1 + x1 + x2 in let x4 = x2 + x3 in x1 + x2 + x4"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 15
    it "can be nested within another expression with two variables" do
      let exp = lam (\x -> lam (\y -> x + y + genLet (x + genLet (int 1 + x + y))))
      view (runLetInserter exp) `shouldBe` "\\x1 -> \\x2 -> let x3 = 1 + x1 + x2 in let x4 = x1 + x3 in x1 + x2 + x4"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 12
    it "can be nested within an expression of literals and one variable" do
      let exp = lam (\x -> lam (\y -> x + y + genLet (int 1 + genLet (int 1 + x + int 2))))
      view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = 1 + x1 + 2 in let x3 = 1 + x2 in \\x4 -> x1 + x4 + x3"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 10
    it "can be nested within an expression of literals" do
      let exp = lam (\x -> lam (\y -> x + y + genLet (int 1 + genLet (int 1 + int 2 + int 3))))
      view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 + 3 in let x2 = 1 + x1 in \\x3 -> \\x4 -> x3 + x4 + x2"
      runIdentity (runLetInserter exp) 1 4 `shouldBe` 12
    it "duplicates literals when used with host-let" do
      let exp = let x = genLet (int 1 + int 2) in x + x
      view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in let x2 = 1 + 2 in x1 + x2"
      runIdentity (runLetInserter exp) `shouldBe` 6
    it "duplicates literals when using host-let and no specific memo key" do
      let exp =
            let x = genLet (int 1 + int 2)
            in let y = genLet (int 1 + x)
               in x + y
      view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in let x2 = 1 + 2 in let x3 = 1 + x2 in x1 + x3"
      runIdentity (runLetInserter exp) `shouldBe` 7
    it "does not duplicate host-let when using a specific memo key" do
      let exp =
            let x = genLetMemoAtMaybe (Just 0) Nothing (int 1 + int 2)
            in let y = genLet (int 1 + x)
               in x + y
      view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in let x2 = 1 + x1 in x1 + x2"
      runIdentity (runLetInserter exp) `shouldBe` 7
    it "does not duplicate host-lets when using specific memo keys" do
      let exp =
            let x = genLetMemoAtMaybe (Just 0) Nothing (int 1 + int 2)
            in let y = genLetMemoAtMaybe (Just 1) Nothing (int 1 + x)
               in let z = genLet (int 1 + y)
                  in x + z + y
      view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in let x2 = 1 + x1 in let x3 = 1 + x2 in x1 + x3 + x2"
      runIdentity (runLetInserter exp) `shouldBe` 12
    it "does not duplicate host-let when using a specific memo key, inside a lam" do
      let exp =
            lam $ \u ->
              let x = genLetMemoAtMaybe (Just 0) Nothing (int 1 + int 2)
              in let y = genLet (u + x)
                 in x + y
      view (runLetInserter exp) `shouldBe` "let x1 = 1 + 2 in \\x2 -> let x3 = x2 + x1 in x1 + x3"
      runIdentity (runLetInserter exp) 2 `shouldBe` 8
    it "does not duplicate host-let when using a specific memo key, inside a lam and using its variable" do
      let exp =
            lam $ \u ->
              let x = genLetMemoAtMaybe (Just 0) Nothing (u + int 2)
              in let y = genLet (int 1 + x)
                 in x + y
      view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 + 2 in let x3 = 1 + x2 in x2 + x3"
      runIdentity (runLetInserter exp) 2 `shouldBe` 9
    it "does not duplicate host-lets when using specific memo keys, inside a lam and using its variable" do
      let exp =
            lam $ \u ->
              let x = genLetMemoAtMaybe (Just 0) Nothing (u + int 2)
              in let y = genLetMemoAtMaybe (Just 1) Nothing (int 1 + x)
                 in let z = genLetMemoAtMaybe (Just 2) Nothing (int 1 + y)
                    in x + z + y + z
      view (runLetInserter exp) `shouldBe` "\\x1 -> let x2 = x1 + 2 in let x3 = 1 + x2 in let x4 = 1 + x3 in x2 + x4 + x3 + x4"
      runIdentity (runLetInserter exp) 2 `shouldBe` 21
  describe "Ex0" do
    it "p12" do
      runLII p12 `shouldBe` 3
    it "p12" do
      view (runLetInserter p12)
        `shouldBe` "1 + 2"
    it "c1" do
      view (runLetInserter c1)
        `shouldBe` "(1 + 2) * (1 + 2 + 1)"
    it "c2" do
      view (runLetInserter c2)
        `shouldBe` "let x1 = 1 + 2 in x1 * (x1 + 1)"
    it "c3" do
      view (runLetInserter c3)
        `shouldBe` "\\x1 -> (let x2 = 1 + 2 in x2 * (x2 + 1)) + (let x2 = 1 + 2 + x1 in x2 * (x2 + 1))"
  describe "Ex1" do
    it "c1l" do
      view (runLetInserter c1l)
        `shouldBe` "let x1 = 1 + 2 in x1"
    -- , it "c3l1" do -- expected scope extrusion
    --     view (runLetInserter c3l1) `shouldBe` ""
    it "c3l2" do
      -- serious duplication
      view (runLetInserter c3l2)
        `shouldBe` "let x1 = 1 + 2 in let x2 = 1 + 2 in let x3 = 1 + 2 in let x4 = 1 + 2 in \\x5 -> let x6 = x3 + x5 in let x7 = x4 + x5 in x1 * (x2 + 1) + x6 * (x7 + 1)"
    it "let x1 = 1 in let x2 = 2 in x1 + x2" do
      let exp = withLocus $ \loc -> genLetAt loc (int 1) + genLetAt loc (int 2)
      view (runLetInserter exp)
        `shouldBe` "let x1 = 1 in let x2 = 2 in x1 + x2"
    it "let_ (genLetAt loc (int 1 + int 2)) (\\x -> x + x)" do
      let exp = withLocus $ \loc ->
            let_ (genLetAt loc (int 1 + int 2)) $ \x ->
              x + x
      view (runLetInserter exp)
        `shouldBe` "let x1 = 1 + 2 in let x2 = x1 in x2 + x2"
    it "withLocus does not cause a scope extrusion" do
      let exp = withLocus $ \loc1 ->
            withLocus $ \loc2 ->
              genLetAt
                loc1 -- expected scope extrusion if it's not bound at loc2 instead of loc1
                (int 1 + genLetAt loc2 (int 2))
                * int 3
      view (runLetInserter exp)
        `shouldBe` "let x1 = 2 in let x2 = 1 + x1 in x2 * 3"
    it "let x1 = 1 + 2 in let x2 = 1 + 2 in let x3 = 1 + x2 in x1 + x3" do
      let exp = withLocus $ \loc ->
            let x = (genLetAt loc (int 1 + int 2))
            in let y = (genLetAt loc (int 1 + x))
               in x + y
      view (runLetInserter exp)
        `shouldBe` "let x1 = 1 + 2 in let x2 = 1 + 2 in let x3 = 1 + x2 in x1 + x3"
    -- , it "let x1 = 1 + 2 in let x2 = 1 + x1 in x1 + x2" do
    --    let exp = withLocus $ \loc ->
    --                let__ (genLetAt loc (int 1 + int 2)) $ \x ->
    --                let__ (genLetAt loc (int 1 + x)) $ \y ->
    --                x + y
    --    view (runLetInserter exp) `shouldBe`
    --      "let x1 = 1 + 2 in let x2 = 1 + x1 in x1 + x2"
    it "let x1 = 1 + 2 in let x2 = x1 in let x3 = 1 + x2 in let x4 = x3 in x2 + x4" do
      let exp = withLocus $ \loc ->
            let_ (genLetAt loc (int 1 + int 2)) $ \x ->
              withLocus $ \locX ->
                let_ (genLetAt locX (int 1 + x)) $ \y ->
                  x + y
      view (runLetInserter exp)
        `shouldBe` "let x1 = 1 + 2 in let x2 = x1 in let x3 = 1 + x2 in let x4 = x3 in x2 + x4"
  describe "Fibonacci" do
    it "fib 2" do
      view (runLetInserter (fibonacci 2))
        `shouldBe` "letRec [u1 = \\x2 -> \\x3 -> x3,u2 = \\x2 -> \\x3 -> x2] in \\x3 -> \\x4 -> u1 x3 x4 + u2 x3 x4"
    it "fib 5" do
      view (runLetInserter (fibonacci 5))
        `shouldBe` "letRec [u1 = \\x2 -> \\x3 -> u2 x2 x3 + u3 x2 x3,u2 = \\x2 -> \\x3 -> u3 x2 x3 + u4 x2 x3,u3 = \\x2 -> \\x3 -> u4 x2 x3 + u5 x2 x3,u4 = \\x2 -> \\x3 -> x3,u5 = \\x2 -> \\x3 -> x2] in \\x6 -> \\x7 -> u1 x6 x7 + u2 x6 x7"
    it "fib 2" do
      runIdentity (runLetInserter (fibonacci 2)) 0 1 `shouldBe` 1
    it "fib 5" do
      runIdentity (runLetInserter (fibonacci 5)) 0 1 `shouldBe` 5
    it "fib 10" do
      runIdentity (runLetInserter (fibonacci 10)) 0 1 `shouldBe` 55
  describe "Ackermann" do
    it "sack 2 3" do
      view (runLetInserter (sack 2))
        `shouldBe` "letRec [u1 = \\x2 -> if x2 == 0 then u2 1 else u2 (u1 (x2 - 1)),u2 = \\x2 -> if x2 == 0 then u3 1 else u3 (u2 (x2 - 1)),u3 = \\x2 -> x2 + 1] in u1"
    it "sack 2 3" do
      runLII (sack 2) 3 `shouldBe` 9
    it "sack 3 4" do
      runLII (sack 3) 4 `shouldBe` 125

--  {-
--    it "fib 0" do
--      runLII (fib .@ int 0) `shouldBe` 1
--  , it "fib 1" do
--      runLII (fib .@ int 1) `shouldBe` 2
--  , it "fib 2" do
--      runLII (fib .@ int 2) `shouldBe` 42
--    it "fib 1" do
--      runIdentity (fib .@ int 1) `shouldBe` 2
--  , it "sack 3" do
--      runIdentity (sack .@ int 3) `shouldBe` 9
--  ,  it "acs" do
--      view (runLetInserter acs) `shouldBe` ""
--  -}