{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans -fno-warn-partial-type-signatures #-}
module UnitSemantics where

import           Prelude hiding (Bool(..),Bounded(..),(.),filter,id)

import           Syntax
import           GenericInterpreter
import qualified GenericInterpreter as Generic

import           Data.Label
import           Data.Text (Text)
import           Data.Profunctor
import qualified Data.Lens as L

import           Data.Abstract.Error (Error(..))
import           Data.Abstract.Except (Except(..))
import qualified Data.Abstract.Map as M
import qualified Data.Abstract.StrongMap as SM
import           Data.Abstract.Terminating
import           Data.Abstract.FreeCompletion(FreeCompletion)
import           Data.Abstract.DiscretePowerset(Pow)
import qualified Data.Abstract.Widening as W

import           Control.Category
import           Control.Arrow
import           Control.Arrow.Fix
import           Control.Arrow.Fix.Chaotic
import           Control.Arrow.Random
import           Control.Arrow.Order
import           Control.Arrow.Trans as Trans

import           Control.Arrow.Transformer.Value
import           Control.Arrow.Transformer.Abstract.Environment
import           Control.Arrow.Transformer.Abstract.Error
import           Control.Arrow.Transformer.Abstract.Except
import           Control.Arrow.Transformer.Abstract.Fix
import           Control.Arrow.Transformer.Abstract.Fix.Component
import           Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable
import           Control.Arrow.Transformer.Abstract.Fix.Stack
import           Control.Arrow.Transformer.Abstract.Store
import           Control.Arrow.Transformer.Abstract.Terminating

-- Value semantics for the while language that does not approximate values at all.
type Addr = FreeCompletion Label
type Env = SM.Map Text Addr
type Store = M.Map Addr Val
type Val = ()
type Exception = ()

run :: [(Text,Addr)] -> [LStatement] -> Terminating (Error (Pow String) (Except Exception (M.Map Addr Val)))
run env0 ss =
  let ?cacheWidening = W.finite in
  let ?fixpointAlgorithm =
        transform (L.iso' (\(store,(env,stmts)) -> ((env,stmts),store))
                          (\((env,stmts),store) -> (store,(env,stmts))))
                  (L.iso' id id) $
        fixpointAlgorithm $ filter isWhileLoop $ innermost in

  fmap (fmap (fmap fst)) <$>
    snd $
    Trans.run
      (Generic.run ::
        (ValueT Val
          (EnvT Env
            (StoreT Store
              (ExceptT Exception
                (ErrorT (Pow String)
                  (TerminatingT
                    (FixT
                      (ComponentT Component _
                        (StackT Stack _
                          (CacheT Cache _ _
                             (->))))))))))) [Statement] ())
      (M.empty,(SM.fromList env0,generate <$> ss))

instance (ArrowChoice c,Profunctor c) => ArrowAlloc Addr (ValueT Val c) where
  alloc = arr $ \(_,_,l) -> return l

instance (ArrowChoice c, ArrowComplete Val c) => IsVal Val (ValueT Val c) where
  type JoinVal y (ValueT Val c) = ArrowComplete y c
  boolLit = arr (const ())
  and = arr (const ())
  or = arr (const ())
  not = arr (const ())
  numLit = arr (const ())
  add = arr (const ())
  sub = arr (const ())
  mul = arr (const ())
  div = arr (const ())
  eq = arr (const ())
  lt = arr (const ())
  if_ f1 f2 = proc (_,(x,y)) -> (f1 -< x) <⊔> (f2 -< y)

instance (ArrowChoice c) => IsException Exception Val (ValueT Val c) where
  type JoinExc y (ValueT Val c) = ArrowComplete y c
  namedException = proc (_,_) -> returnA -< ()
  matchException f g = proc (_,(),x) -> (f -< ((),x)) <⊔> (g -< x)

instance (ArrowChoice c,Profunctor c) => ArrowRand Val (ValueT Val c) where
  random = arr (const ())

deriving instance (ArrowComplete y c) => ArrowComplete y (ValueT Val c)
