{-# LANGUAGE OverloadedStrings #-}
# OPTIONS_GHC -Wall #

module CCC where

import Bound
import Control.Arrow ((&&&))
import Data.Bool (bool)
import Data.Monoid ((<>))
import TypeChecking
import Types
import Utils


fork :: (a -> b) -> (a -> c) -> (a -> (b, c))
fork = (&&&)

apply :: (a -> b, a) -> b
apply = uncurry ($)


simplify :: Exp VName -> Exp VName
simplify ("." :@ "apply" :@ ("fork" :@ ("curry" :@ h) :@ g)) =
  simplify $ "." :@ h :@ ("fork" :@ "id" :@ g)
simplify (V n)       = V n
simplify (LCon c)    = LCon c
simplify (a :@ b)    = simplify a :@ simplify b
simplify _           = error "simplify can only be done on pointfree exps"


toCCC :: Exp VName -> Exp VName
toCCC (Lam n x) =
  case unscope x of
    V (B ())    -> "id"
    V (F (V a)) ->
      (case a of
  TODO(sandy ): more generally we should look at the SymTable and see
         -- if there is a categorical context in order to return id here
        "id"  -> id
        ","   -> id
        "fst" -> id
        "snd" -> id
        "inr" -> id
        "inl" -> id
        "."   -> id
        _ -> \z -> ("." :@ z :@ "shouldInline")
      ) "const" :@ V a
    V (F _)     -> error "this should never be hit"
    z | Just (c, as) <- unravel z
        ->  "const" :@ (foldl (\a b -> a :@ anonLam b) (LCon c) as)
    u :@ v      ->
      foldl1 (:@)
        [ "."
        , "apply"
        , foldl1 (:@)
          [ "fork"
          , anonLam u
          , anonLam v
          ]
        ]
    Lam n2 y    ->
      let name = VName $ unVName n <> "+" <> unVName n2
       in
        ( case unscope y of
            V (F _) -> ("curry" :@)
            _       -> id
        ) . toCCC
          . lam name
          . unsafeInst1  ("snd" :@ V name)
          . instantiate1 ("fst" :@ V name)
          $ x
    LInt i     -> "const" :@ LInt i
    -- TODO(sandy): is this right? it discards info
    Assert a _ -> anonLam a
    Let _ b e  -> anonLam $ instantiate1 b e
  where
    anonLam = toCCC . Lam n . Scope
-- eta abstract a point-free function
toCCC z = toCCC $ lam "!!!!z" $ z :@ "!!!!z"


unsafeInst1 :: Exp VName -> Exp VName -> Exp VName
unsafeInst1 z (Lam _ x) = instantiate1 z x
unsafeInst1 _ _ = error "unsafeInst1"


# LANGUAGE OverloadedStrings #
 if there is a categorical context in order to return id here
 TODO(sandy): is this right? it discards info
 eta abstract a point-free function
# OPTIONS_GHC -Wall #

module CCC where

import Bound
import Control.Arrow ((&&&))
import Data.Bool (bool)
import Data.Monoid ((<>))
import TypeChecking
import Types
import Utils


fork :: (a -> b) -> (a -> c) -> (a -> (b, c))
fork = (&&&)

apply :: (a -> b, a) -> b
apply = uncurry ($)


simplify :: Exp VName -> Exp VName
simplify ("." :@ "apply" :@ ("fork" :@ ("curry" :@ h) :@ g)) =
  simplify $ "." :@ h :@ ("fork" :@ "id" :@ g)
simplify (V n)       = V n
simplify (LCon c)    = LCon c
simplify (a :@ b)    = simplify a :@ simplify b
simplify _           = error "simplify can only be done on pointfree exps"


toCCC :: Exp VName -> Exp VName
toCCC (Lam n x) =
  case unscope x of
    V (B ())    -> "id"
    V (F (V a)) ->
      (case a of
  TODO(sandy ): more generally we should look at the SymTable and see
        "id"  -> id
        ","   -> id
        "fst" -> id
        "snd" -> id
        "inr" -> id
        "inl" -> id
        "."   -> id
        _ -> \z -> ("." :@ z :@ "shouldInline")
      ) "const" :@ V a
    V (F _)     -> error "this should never be hit"
    z | Just (c, as) <- unravel z
        ->  "const" :@ (foldl (\a b -> a :@ anonLam b) (LCon c) as)
    u :@ v      ->
      foldl1 (:@)
        [ "."
        , "apply"
        , foldl1 (:@)
          [ "fork"
          , anonLam u
          , anonLam v
          ]
        ]
    Lam n2 y    ->
      let name = VName $ unVName n <> "+" <> unVName n2
       in
        ( case unscope y of
            V (F _) -> ("curry" :@)
            _       -> id
        ) . toCCC
          . lam name
          . unsafeInst1  ("snd" :@ V name)
          . instantiate1 ("fst" :@ V name)
          $ x
    LInt i     -> "const" :@ LInt i
    Assert a _ -> anonLam a
    Let _ b e  -> anonLam $ instantiate1 b e
  where
    anonLam = toCCC . Lam n . Scope
toCCC z = toCCC $ lam "!!!!z" $ z :@ "!!!!z"


unsafeInst1 :: Exp VName -> Exp VName -> Exp VName
unsafeInst1 z (Lam _ x) = instantiate1 z x
unsafeInst1 _ _ = error "unsafeInst1"

