content: {-# LANGUAGE DataKinds                  #-}
  {-# LANGUAGE DeriveDataTypeable         #-}
  {-# LANGUAGE EmptyCase                  #-}
  {-# LANGUAGE FlexibleInstances          #-}
  {-# LANGUAGE FunctionalDependencies     #-}
  {-# LANGUAGE GADTs                      #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE KindSignatures             #-}
  {-# LANGUAGE LambdaCase                 #-}
  {-# LANGUAGE MultiParamTypeClasses      #-}
  {-# LANGUAGE PolyKinds                  #-}
  {-# LANGUAGE RankNTypes                 #-}
  {-# LANGUAGE ScopedTypeVariables        #-}
  
  {-# OPTIONS_GHC -Wall #-}
  
  
  {-|
  
  Symbolic representations of Fortran values, for symbolic reasoning.
  
  There is a distinction between core representations ('CoreRepr') and high-level
  representations ('HighRepr'). 'CoreRepr' represents any @a@ such that @'D' a@
  exists; i.e. anything with a corresponding Fortran type. 'HighRepr' is a
  superset of 'CoreRepr'. It represents Fortran types, and also higher-level types
  that facilitate reasoning. There is more information about this distinction in
  "Language.Fortran.Model.Op".
  
  -}
  module Language.Fortran.Model.Repr where
  
  import           Data.Int                        (Int16, Int32, Int64, Int8)
  import           Data.Word                       (Word8)
  
  import           Data.Functor.Compose
  
  import           Data.SBV
  import           Data.SBV.Dynamic
  import           Data.SBV.Internals              (SBV (..))
  
  import           Data.Vinyl                      hiding (Field)
  
  import           Language.Expression
  import           Language.Expression.Prop
  
  import           Language.Fortran.Model.Repr.Prim
  import           Language.Fortran.Model.Types
  
  --------------------------------------------------------------------------------
  -- * Core Fortran Representations
  
  {-|
  
  Symbolic representations of Fortran values, using "Data.SBV.Dynamic".
  
  -}
  data CoreRepr a where
    CRPrim
      :: D (PrimS a)
      -> SVal
      -> CoreRepr (PrimS a)
  
    CRArray
      :: D (Array i a)
      -> ArrRepr i a
      -> CoreRepr (Array i a)
  
    CRData
      :: D (Record name fs)
      -> Rec (Field CoreRepr) fs
      -> CoreRepr (Record name fs)
  
  {-|
  
  Symbolic respresentations of Fortran arrays. SBV arrays can only contain basic
  values, so in order to represent arrays of derived data types, we use multiple
  flat arrays, one for each basic field. Nested derived data types are recursively
  expanded.
  
  Arrays of arrays are not yet supported.
  
  -}
  data ArrRepr i a where
    -- | A primitive type is represented by a flat 'SArr'.
    ARPrim :: SArr -> ArrRepr i (PrimS a)
  
    -- | A derived data type is represented by a record of 'ArrRepr's over the
    -- record's fields.
    ARData :: Rec (Field (ArrRepr i)) fs -> ArrRepr i (Record name fs)
  
  
  --------------------------------------------------------------------------------
  -- * High-level data representations
  
  {-|
  
  Symbolic representations of Fortran values plus types in the higher-level
  meta-language (see "Language.Fortran.Op" for more information).
  
  -}
  data HighRepr a where
    HRCore :: CoreRepr a -> HighRepr a
    HRHigh :: SBV a -> HighRepr a
  
  instance HFoldableAt HighRepr LogicOp where
    hfoldMap = implHfoldMap $ \case
      LogLit x     -> HRHigh (fromBool x)
      LogNot x     -> HRHigh . sNot . getHrBool $ x
      LogAnd x y   -> appBinop (.&&) x y
      LogOr x y    -> appBinop (.||) x y
      LogImpl x y  -> appBinop (.=>) x y
      LogEquiv x y -> appBinop (.<=>) x y
  
      where
        appBinop (g :: SBool -> SBool -> SBool) x y =
          HRHigh $ g (getHrBool x) (getHrBool y)
        getHrBool :: HighRepr Bool -> SBool
        getHrBool (HRHigh x) = x
        getHrBool (HRCore x) = case x of -- I.e. absurd
  
  instance (Monad m) => HFoldableAt (Compose m HighRepr) LogicOp where
    hfoldMap = implHfoldMapCompose (pure . hfold)
  
  --------------------------------------------------------------------------------
  -- *  Lifting Fortran types to high-level representations
  
  -- | Provides conversions between symbolic representations of core Fortran
  -- values and their corresponding high-level types.
  class (SymVal a) => LiftD b a | b -> a where
    -- | Go from a core value to the corresponding high-level value.
    liftD :: b -> a
    -- | Go from a symbolic core value to the corresponding symbolic high-level
    -- value.
    liftDRepr :: PrimReprHandlers -> HighRepr b -> HighRepr a
  
  liftDInt :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Integer
  liftDInt _ (HRCore (CRPrim _ x)) = HRHigh (SBV (svFromIntegral KUnbounded x))
  liftDInt _ _ = error "impossible"
  
  
  liftDReal :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr AlgReal
  liftDReal env (HRCore (CRPrim (DPrim prim) x)) =
    HRHigh $ case primSBVKind prim env of
                KFloat -> fromSFloat sRTZ (SBV x)
                KDouble -> fromSDouble sRTZ (SBV x)
                KReal -> SBV x
                k -> error $ "liftDReal: can't convert something of kind " ++
                     show k ++ " to a real"
  liftDReal _ _ = error "impossible"
  
  liftDBool :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Bool
  liftDBool _ (HRCore (CRPrim _ x)) = HRHigh (SBV (x `svGreaterThan` svFalse))
  liftDBool _ _ = error "impossible"
  
  
  instance LiftD (PrimS Int8) Integer where
    liftD = fromIntegral . getPrimS
    liftDRepr = liftDInt
  instance LiftD (PrimS Int16) Integer where
    liftD = fromIntegral . getPrimS
    liftDRepr = liftDInt
  instance LiftD (PrimS Int32) Integer where
    liftD = fromIntegral . getPrimS
    liftDRepr = liftDInt
  instance LiftD (PrimS Int64) Integer where
    liftD = fromIntegral . getPrimS
    liftDRepr = liftDInt
  
  instance LiftD (PrimS Float) AlgReal where
    liftD = realToFrac . getPrimS
    liftDRepr = liftDReal
  instance LiftD (PrimS Double) AlgReal where
    liftD = realToFrac . getPrimS
    liftDRepr = liftDReal
  
  instance LiftD (PrimS Bool8) Bool where
    liftD = (> 0) . getBool8 . getPrimS
    liftDRepr = liftDBool
  instance LiftD (PrimS Bool16) Bool where
    liftD = (> 0) . getBool16 . getPrimS
    liftDRepr = liftDBool
  instance LiftD (PrimS Bool32) Bool where
    liftD = (> 0) . getBool32 . getPrimS
    liftDRepr = liftDBool
  instance LiftD (PrimS Bool64) Bool where
    liftD = (> 0) . getBool64 . getPrimS
    liftDRepr = liftDBool
  
  instance LiftD (PrimS Char8) Word8 where
    liftD = getChar8 . getPrimS
    liftDRepr _ (HRCore (CRPrim _ x)) = HRHigh (sFromIntegral (SBV x :: SBV Word8))
    liftDRepr _ _ =
      error "liftDRepr: a 'PrimS Char8' has a non-primitive representation"
  
  --------------------------------------------------------------------------------
  -- * Combinators
  
  -- | Any type that has a core representation has a corresponding Fortran type.
  coreReprD :: CoreRepr a -> D a
  coreReprD = \case
    CRPrim d _  -> d
    CRArray d _ -> d
    CRData d _  -> d
  