{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures             #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE CPP                        #-}

{-# OPTIONS_GHC -Wall #-}

-- TODO: Complex Numbers

{-|

Embeds Fortran's type system in Haskell via the 'D' GADT.

== Note: Phantom Types and GADTs

Lots of the data types in this module are parameterised by phantom types. These
are types which appear at the type-level, but not at the value level. They are
there to make things more type-safe.

In addition, a lot of the data types are GADTs. In a phantom-type-indexed GADT,
the phantom type often restricts which GADT constructors a particular value may
be an instance of. This is very useful for restricting value-level terms based
on type-level information.

-}

module Language.Fortran.Model.Types where

import           Data.Int                              (Int16, Int32, Int64,
                                                        Int8)
import           Data.List                             (intersperse)
import           Data.Monoid                           (Endo (..))
import           Data.Typeable                         (Typeable)
import           Data.Word                             (Word8)

#if MIN_VERSION_singletons(3,0,0)
import           GHC.TypeLits.Singletons
#else
import           Data.Singletons.TypeLits
#endif

import           Data.Vinyl                            hiding (Field)
import           Data.Vinyl.Functor                    hiding (Field)

import           Language.Expression.Pretty

import           Language.Fortran.Model.Singletons

--------------------------------------------------------------------------------
-- * Fortran Types

{-|

This is the main embedding of Fortran types. A value of type @D a@ represents
the Fortran type which corresponds to the Haskell type @a@. @a@ is a phantom
type parameter. There is at most one instance of @D a@ for each @a@. This means
that a value of type @D a@ acts as a kind of proof that it possible to have a
Fortran type corresponding to the Haskell type @a@ -- and that when you match on
@D a@ knowing the particular @a@ you have, you know which constructor you will
get. This is a nice property because it means that GHC (with
@-fwarn-incomplete-patterns@) will not warn when you match on an impossible
case. It eliminates situations where you'd otherwise write @error "impossible:
..."@.

* @'DPrim' p :: D ('PrimS' a)@ is for primitive types. It contains a value @p@
  of type @'Prim' p k a@ for some @p@, @k@, @a@. When matching on something of
  type @D ('PrimS' a)@, you know it can only contain a primitive type.

* @'DArray' i v :: D ('Array' i v)@ is for arrays. It contains instances of @'Index'
  i@ and @'ArrValue' a@. @'Index' i@ is a proof that @i@ can be used as an index,
  and @'ArrValue' a@ is a proof that @a@ can be stored in arrays.

* @'DData' s xs :: D ('Record' name fs)@ is for user-defined data types. The
  type has a name, represented at the type level by the type parameter @name@ of
  kind 'Symbol'. The constructor contains @s :: 'SSymbol' name@, which acts as a
  sort of value-level representation of the name. 'SSymbol' is from the
  @singletons@ library. It also contains @xs :: 'Rec' ('Field' D) fs@. @fs@ is a
  type-level list of pairs, pairing field names with field types. @'Field' D
  '(fname, b)@ is a value-level pair of @'SSymbol' fname@ and @D b@. The vinyl
  record is a list of fields, one for each pair in @fs@.

-}
data D a where
  DPrim :: Prim p k a -> D (PrimS a)
  DArray :: Index i -> ArrValue a -> D (Array i a)
  DData :: (RMap fs, RecordToList fs, RApply fs) => SSymbol name -> Rec (Field D) fs -> D (Record name fs)

--------------------------------------------------------------------------------
-- * Semantic Types

newtype Bool8  = Bool8 { Bool8 -> Int8
getBool8 :: Int8 } deriving (Int -> Bool8 -> ShowS
[Bool8] -> ShowS
Bool8 -> String
(Int -> Bool8 -> ShowS)
-> (Bool8 -> String) -> ([Bool8] -> ShowS) -> Show Bool8
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Bool8 -> ShowS
showsPrec :: Int -> Bool8 -> ShowS
$cshow :: Bool8 -> String
show :: Bool8 -> String
$cshowList :: [Bool8] -> ShowS
showList :: [Bool8] -> ShowS
Show, Integer -> Bool8
Bool8 -> Bool8
Bool8 -> Bool8 -> Bool8
(Bool8 -> Bool8 -> Bool8)
-> (Bool8 -> Bool8 -> Bool8)
-> (Bool8 -> Bool8 -> Bool8)
-> (Bool8 -> Bool8)
-> (Bool8 -> Bool8)
-> (Bool8 -> Bool8)
-> (Integer -> Bool8)
-> Num Bool8
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Bool8 -> Bool8 -> Bool8
+ :: Bool8 -> Bool8 -> Bool8
$c- :: Bool8 -> Bool8 -> Bool8
- :: Bool8 -> Bool8 -> Bool8
$c* :: Bool8 -> Bool8 -> Bool8
* :: Bool8 -> Bool8 -> Bool8
$cnegate :: Bool8 -> Bool8
negate :: Bool8 -> Bool8
$cabs :: Bool8 -> Bool8
abs :: Bool8 -> Bool8
$csignum :: Bool8 -> Bool8
signum :: Bool8 -> Bool8
$cfromInteger :: Integer -> Bool8
fromInteger :: Integer -> Bool8
Num, Bool8 -> Bool8 -> Bool
(Bool8 -> Bool8 -> Bool) -> (Bool8 -> Bool8 -> Bool) -> Eq Bool8
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Bool8 -> Bool8 -> Bool
== :: Bool8 -> Bool8 -> Bool
$c/= :: Bool8 -> Bool8 -> Bool
/= :: Bool8 -> Bool8 -> Bool
Eq, Typeable)
newtype Bool16 = Bool16 { Bool16 -> Int16
getBool16 :: Int16 } deriving (Int -> Bool16 -> ShowS
[Bool16] -> ShowS
Bool16 -> String
(Int -> Bool16 -> ShowS)
-> (Bool16 -> String) -> ([Bool16] -> ShowS) -> Show Bool16
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Bool16 -> ShowS
showsPrec :: Int -> Bool16 -> ShowS
$cshow :: Bool16 -> String
show :: Bool16 -> String
$cshowList :: [Bool16] -> ShowS
showList :: [Bool16] -> ShowS
Show, Integer -> Bool16
Bool16 -> Bool16
Bool16 -> Bool16 -> Bool16
(Bool16 -> Bool16 -> Bool16)
-> (Bool16 -> Bool16 -> Bool16)
-> (Bool16 -> Bool16 -> Bool16)
-> (Bool16 -> Bool16)
-> (Bool16 -> Bool16)
-> (Bool16 -> Bool16)
-> (Integer -> Bool16)
-> Num Bool16
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Bool16 -> Bool16 -> Bool16
+ :: Bool16 -> Bool16 -> Bool16
$c- :: Bool16 -> Bool16 -> Bool16
- :: Bool16 -> Bool16 -> Bool16
$c* :: Bool16 -> Bool16 -> Bool16
* :: Bool16 -> Bool16 -> Bool16
$cnegate :: Bool16 -> Bool16
negate :: Bool16 -> Bool16
$cabs :: Bool16 -> Bool16
abs :: Bool16 -> Bool16
$csignum :: Bool16 -> Bool16
signum :: Bool16 -> Bool16
$cfromInteger :: Integer -> Bool16
fromInteger :: Integer -> Bool16
Num, Bool16 -> Bool16 -> Bool
(Bool16 -> Bool16 -> Bool)
-> (Bool16 -> Bool16 -> Bool) -> Eq Bool16
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Bool16 -> Bool16 -> Bool
== :: Bool16 -> Bool16 -> Bool
$c/= :: Bool16 -> Bool16 -> Bool
/= :: Bool16 -> Bool16 -> Bool
Eq, Typeable)
newtype Bool32 = Bool32 { Bool32 -> Int32
getBool32 :: Int32 } deriving (Int -> Bool32 -> ShowS
[Bool32] -> ShowS
Bool32 -> String
(Int -> Bool32 -> ShowS)
-> (Bool32 -> String) -> ([Bool32] -> ShowS) -> Show Bool32
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Bool32 -> ShowS
showsPrec :: Int -> Bool32 -> ShowS
$cshow :: Bool32 -> String
show :: Bool32 -> String
$cshowList :: [Bool32] -> ShowS
showList :: [Bool32] -> ShowS
Show, Integer -> Bool32
Bool32 -> Bool32
Bool32 -> Bool32 -> Bool32
(Bool32 -> Bool32 -> Bool32)
-> (Bool32 -> Bool32 -> Bool32)
-> (Bool32 -> Bool32 -> Bool32)
-> (Bool32 -> Bool32)
-> (Bool32 -> Bool32)
-> (Bool32 -> Bool32)
-> (Integer -> Bool32)
-> Num Bool32
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Bool32 -> Bool32 -> Bool32
+ :: Bool32 -> Bool32 -> Bool32
$c- :: Bool32 -> Bool32 -> Bool32
- :: Bool32 -> Bool32 -> Bool32
$c* :: Bool32 -> Bool32 -> Bool32
* :: Bool32 -> Bool32 -> Bool32
$cnegate :: Bool32 -> Bool32
negate :: Bool32 -> Bool32
$cabs :: Bool32 -> Bool32
abs :: Bool32 -> Bool32
$csignum :: Bool32 -> Bool32
signum :: Bool32 -> Bool32
$cfromInteger :: Integer -> Bool32
fromInteger :: Integer -> Bool32
Num, Bool32 -> Bool32 -> Bool
(Bool32 -> Bool32 -> Bool)
-> (Bool32 -> Bool32 -> Bool) -> Eq Bool32
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Bool32 -> Bool32 -> Bool
== :: Bool32 -> Bool32 -> Bool
$c/= :: Bool32 -> Bool32 -> Bool
/= :: Bool32 -> Bool32 -> Bool
Eq, Typeable)
newtype Bool64 = Bool64 { Bool64 -> Int64
getBool64 :: Int64 } deriving (Int -> Bool64 -> ShowS
[Bool64] -> ShowS
Bool64 -> String
(Int -> Bool64 -> ShowS)
-> (Bool64 -> String) -> ([Bool64] -> ShowS) -> Show Bool64
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Bool64 -> ShowS
showsPrec :: Int -> Bool64 -> ShowS
$cshow :: Bool64 -> String
show :: Bool64 -> String
$cshowList :: [Bool64] -> ShowS
showList :: [Bool64] -> ShowS
Show, Integer -> Bool64
Bool64 -> Bool64
Bool64 -> Bool64 -> Bool64
(Bool64 -> Bool64 -> Bool64)
-> (Bool64 -> Bool64 -> Bool64)
-> (Bool64 -> Bool64 -> Bool64)
-> (Bool64 -> Bool64)
-> (Bool64 -> Bool64)
-> (Bool64 -> Bool64)
-> (Integer -> Bool64)
-> Num Bool64
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Bool64 -> Bool64 -> Bool64
+ :: Bool64 -> Bool64 -> Bool64
$c- :: Bool64 -> Bool64 -> Bool64
- :: Bool64 -> Bool64 -> Bool64
$c* :: Bool64 -> Bool64 -> Bool64
* :: Bool64 -> Bool64 -> Bool64
$cnegate :: Bool64 -> Bool64
negate :: Bool64 -> Bool64
$cabs :: Bool64 -> Bool64
abs :: Bool64 -> Bool64
$csignum :: Bool64 -> Bool64
signum :: Bool64 -> Bool64
$cfromInteger :: Integer -> Bool64
fromInteger :: Integer -> Bool64
Num, Bool64 -> Bool64 -> Bool
(Bool64 -> Bool64 -> Bool)
-> (Bool64 -> Bool64 -> Bool) -> Eq Bool64
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Bool64 -> Bool64 -> Bool
== :: Bool64 -> Bool64 -> Bool
$c/= :: Bool64 -> Bool64 -> Bool
/= :: Bool64 -> Bool64 -> Bool
Eq, Typeable)
newtype Char8  = Char8 { Char8 -> Word8
getChar8 :: Word8 } deriving (Int -> Char8 -> ShowS
[Char8] -> ShowS
Char8 -> String
(Int -> Char8 -> ShowS)
-> (Char8 -> String) -> ([Char8] -> ShowS) -> Show Char8
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Char8 -> ShowS
showsPrec :: Int -> Char8 -> ShowS
$cshow :: Char8 -> String
show :: Char8 -> String
$cshowList :: [Char8] -> ShowS
showList :: [Char8] -> ShowS
Show, Integer -> Char8
Char8 -> Char8
Char8 -> Char8 -> Char8
(Char8 -> Char8 -> Char8)
-> (Char8 -> Char8 -> Char8)
-> (Char8 -> Char8 -> Char8)
-> (Char8 -> Char8)
-> (Char8 -> Char8)
-> (Char8 -> Char8)
-> (Integer -> Char8)
-> Num Char8
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Char8 -> Char8 -> Char8
+ :: Char8 -> Char8 -> Char8
$c- :: Char8 -> Char8 -> Char8
- :: Char8 -> Char8 -> Char8
$c* :: Char8 -> Char8 -> Char8
* :: Char8 -> Char8 -> Char8
$cnegate :: Char8 -> Char8
negate :: Char8 -> Char8
$cabs :: Char8 -> Char8
abs :: Char8 -> Char8
$csignum :: Char8 -> Char8
signum :: Char8 -> Char8
$cfromInteger :: Integer -> Char8
fromInteger :: Integer -> Char8
Num, Char8 -> Char8 -> Bool
(Char8 -> Char8 -> Bool) -> (Char8 -> Char8 -> Bool) -> Eq Char8
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Char8 -> Char8 -> Bool
== :: Char8 -> Char8 -> Bool
$c/= :: Char8 -> Char8 -> Bool
/= :: Char8 -> Char8 -> Bool
Eq, Typeable)

{-|

This newtype wrapper is used in 'DPrim' for semantic primitive types. This means
that when matching on something of type @'D' ('PrimS' a)@, we know it can't be
an array or a record.

-}
newtype PrimS a = PrimS { forall a. PrimS a -> a
getPrimS :: a }
  deriving (Int -> PrimS a -> ShowS
[PrimS a] -> ShowS
PrimS a -> String
(Int -> PrimS a -> ShowS)
-> (PrimS a -> String) -> ([PrimS a] -> ShowS) -> Show (PrimS a)
forall a. Show a => Int -> PrimS a -> ShowS
forall a. Show a => [PrimS a] -> ShowS
forall a. Show a => PrimS a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> PrimS a -> ShowS
showsPrec :: Int -> PrimS a -> ShowS
$cshow :: forall a. Show a => PrimS a -> String
show :: PrimS a -> String
$cshowList :: forall a. Show a => [PrimS a] -> ShowS
showList :: [PrimS a] -> ShowS
Show, PrimS a -> PrimS a -> Bool
(PrimS a -> PrimS a -> Bool)
-> (PrimS a -> PrimS a -> Bool) -> Eq (PrimS a)
forall a. Eq a => PrimS a -> PrimS a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => PrimS a -> PrimS a -> Bool
== :: PrimS a -> PrimS a -> Bool
$c/= :: forall a. Eq a => PrimS a -> PrimS a -> Bool
/= :: PrimS a -> PrimS a -> Bool
Eq, Typeable)

--------------------------------------------------------------------------------
-- * Primitive Types

{-|

Lists the allowed primitive Fortran types. For example, @'PInt8' :: 'Prim' 'P8
''BTInt' 'Int8'@ represents 8-bit integers. 'Prim' has three phantom type
parameters: precision, base type and semantic Haskell type. Precision is the
number of bits used to store values of that type. The base type represents the
corresponding Fortran base type, e.g. @integer@ or @real@. Constructors are only
provided for those Fortran types which are semantically valid, so for example no
constructor is provided for a 16-bit real. A value of type @'Prim' p k a@ can be
seen as a proof that there is some Fortran primitive type with those parameters.

-}
data Prim p k a where
  PInt8          :: Prim 'P8   'BTInt     Int8
  PInt16         :: Prim 'P16  'BTInt     Int16
  PInt32         :: Prim 'P32  'BTInt     Int32
  PInt64         :: Prim 'P64  'BTInt     Int64

  PBool8         :: Prim 'P8   'BTLogical Bool8
  PBool16        :: Prim 'P16  'BTLogical Bool16
  PBool32        :: Prim 'P32  'BTLogical Bool32
  PBool64        :: Prim 'P64  'BTLogical Bool64

  PFloat         :: Prim 'P32  'BTReal    Float
  PDouble        :: Prim 'P64  'BTReal    Double

  PChar          :: Prim 'P8   'BTChar    Char8

--------------------------------------------------------------------------------
-- * Arrays

-- | Specifies which types can be used as array indices.
data Index a where
  Index :: Prim p 'BTInt a -> Index (PrimS a)

-- | Specifies which types can be stored in arrays. Currently arrays of arrays
-- are not supported.
data ArrValue a where
  ArrPrim :: Prim p k a -> ArrValue (PrimS a)
  ArrData :: (RMap fs, RecordToList fs, RApply fs) => SSymbol name -> Rec (Field ArrValue) fs -> ArrValue (Record name fs)


-- | An array with a phantom index type. Mostly used at the type-level to
-- constrain instances of @'D' (Array i a)@ etc.
newtype Array i a = Array [a]

--------------------------------------------------------------------------------
-- * Records

-- | A field over a pair of name and value type.
data Field f field where
  Field :: SSymbol name -> f a -> Field f '(name, a)

-- | A type of records with the given @name@ and @fields@. Mostly used at the
-- type level to constrain instances of @'D' (Record name fields)@ etc.
data Record name fields where
  Record :: RMap fields => SSymbol name -> Rec (Field Identity) fields -> Record name fields

--------------------------------------------------------------------------------
-- * Combinators

-- | Any Fortran index type is a valid Fortran type.
dIndex :: Index i -> D i
dIndex :: forall i. Index i -> D i
dIndex (Index Prim p 'BTInt a
p) = Prim p 'BTInt a -> D (PrimS a)
forall (name :: Precision) (a :: BasicType) a.
Prim name a a -> D (PrimS a)
DPrim Prim p 'BTInt a
p

-- | Anything that can be stored in Fortran arrays is a valid Fortran type.
dArrValue :: ArrValue a -> D a
dArrValue :: forall a. ArrValue a -> D a
dArrValue (ArrPrim Prim p k a
p) = Prim p k a -> D (PrimS a)
forall (name :: Precision) (a :: BasicType) a.
Prim name a a -> D (PrimS a)
DPrim Prim p k a
p
dArrValue (ArrData SSymbol name
nameSym Rec (Field ArrValue) fs
fieldArrValues) =
  SSymbol name -> Rec (Field D) fs -> D (Record name fs)
forall (name :: [(Symbol, *)]) (a :: Symbol).
(RMap name, RecordToList name, RApply name) =>
SSymbol a -> Rec (Field D) name -> D (Record a name)
DData SSymbol name
nameSym ((forall (x :: (Symbol, *)). Field ArrValue x -> Field D x)
-> Rec (Field ArrValue) fs -> Rec (Field D) fs
forall {u} (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
forall (f :: (Symbol, *) -> *) (g :: (Symbol, *) -> *).
(forall (x :: (Symbol, *)). f x -> g x) -> Rec f fs -> Rec g fs
rmap ((forall a. ArrValue a -> D a) -> Field ArrValue x -> Field D x
forall {k} (f :: k -> *) (g :: k -> *) (nv :: (Symbol, k)).
(forall (a :: k). f a -> g a) -> Field f nv -> Field g nv
overField' ArrValue a -> D a
forall a. ArrValue a -> D a
dArrValue) Rec (Field ArrValue) fs
fieldArrValues)

-- | Given a field with known contents, we can change the functor and value
-- type.
overField :: (f a -> g b) -> Field f '(name, a) -> Field g '(name, b)
overField :: forall {k} {k} (f :: k -> *) (a :: k) (g :: k -> *) (b :: k)
       (name :: Symbol).
(f a -> g b) -> Field f '(name, a) -> Field g '(name, b)
overField f a -> g b
f (Field SSymbol name
n f a
x) = SSymbol name -> g b -> Field g '(name, b)
forall {k} (name :: Symbol) (f :: k -> *) (a :: k).
SSymbol name -> f a -> Field f '(name, a)
Field SSymbol name
SSymbol name
n (f a -> g b
f f a
f a
x)

-- | Given a field with unknown contents, we can change the functor but not the
-- value type.
overField' :: (forall a. f a -> g a) -> Field f nv -> Field g nv
overField' :: forall {k} (f :: k -> *) (g :: k -> *) (nv :: (Symbol, k)).
(forall (a :: k). f a -> g a) -> Field f nv -> Field g nv
overField' forall (a :: k). f a -> g a
f (Field SSymbol name
n f a
x) = SSymbol name -> g a -> Field g '(name, a)
forall {k} (name :: Symbol) (f :: k -> *) (a :: k).
SSymbol name -> f a -> Field f '(name, a)
Field SSymbol name
n (f a -> g a
forall (a :: k). f a -> g a
f f a
x)

traverseField' :: (Functor t) => (forall a. f a -> t (g a)) -> Field f nv -> t (Field g nv)
traverseField' :: forall {k} (t :: * -> *) (f :: k -> *) (g :: k -> *)
       (nv :: (Symbol, k)).
Functor t =>
(forall (a :: k). f a -> t (g a)) -> Field f nv -> t (Field g nv)
traverseField' forall (a :: k). f a -> t (g a)
f (Field SSymbol name
n f a
x) = SSymbol name -> g a -> Field g '(name, a)
forall {k} (name :: Symbol) (f :: k -> *) (a :: k).
SSymbol name -> f a -> Field f '(name, a)
Field SSymbol name
n (g a -> Field g nv) -> t (g a) -> t (Field g nv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> t (g a)
forall (a :: k). f a -> t (g a)
f f a
x

-- | Combine two fields over the same name-value pair but (potentially)
-- different functors.
zipFieldsWith :: (forall a. f a -> g a -> h a) -> Field f nv -> Field g nv -> Field h nv
zipFieldsWith :: forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (nv :: (Symbol, k)).
(forall (a :: k). f a -> g a -> h a)
-> Field f nv -> Field g nv -> Field h nv
zipFieldsWith forall (a :: k). f a -> g a -> h a
f (Field SSymbol name
_ f a
x) (Field SSymbol name
n g a
y) = SSymbol name -> h a -> Field h '(name, a)
forall {k} (name :: Symbol) (f :: k -> *) (a :: k).
SSymbol name -> f a -> Field f '(name, a)
Field SSymbol name
n (f a -> g a -> h a
forall (a :: k). f a -> g a -> h a
f f a
x g a
g a
y)

zip3FieldsWith
  :: (forall a. f a -> g a -> h a -> i a)
  -> Field f nv
  -> Field g nv
  -> Field h nv
  -> Field i nv
zip3FieldsWith :: forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *) (i :: k -> *)
       (nv :: (Symbol, k)).
(forall (a :: k). f a -> g a -> h a -> i a)
-> Field f nv -> Field g nv -> Field h nv -> Field i nv
zip3FieldsWith forall (a :: k). f a -> g a -> h a -> i a
f (Field SSymbol name
_ f a
x) (Field SSymbol name
_ g a
y) (Field SSymbol name
n h a
z) = SSymbol name -> i a -> Field i '(name, a)
forall {k} (name :: Symbol) (f :: k -> *) (a :: k).
SSymbol name -> f a -> Field f '(name, a)
Field SSymbol name
n (f a -> g a -> h a -> i a
forall (a :: k). f a -> g a -> h a -> i a
f f a
x g a
g a
y h a
h a
z)

--------------------------------------------------------------------------------
--  Pretty Printing

instance Pretty1 (Prim p k) where
  prettys1Prec :: forall a. Int -> Prim p k a -> ShowS
prettys1Prec Int
p = \case
    Prim p k a
PInt8   -> String -> ShowS
showString String
"integer8"
    Prim p k a
PInt16  -> String -> ShowS
showString String
"integer16"
    Prim p k a
PInt32  -> String -> ShowS
showString String
"integer32"
    Prim p k a
PInt64  -> String -> ShowS
showString String
"integer64"
    Prim p k a
PFloat  -> String -> ShowS
showString String
"real"
    Prim p k a
PDouble -> Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
8) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"double precision"
    Prim p k a
PBool8  -> String -> ShowS
showString String
"logical8"
    Prim p k a
PBool16 -> String -> ShowS
showString String
"logical16"
    Prim p k a
PBool32 -> String -> ShowS
showString String
"logical32"
    Prim p k a
PBool64 -> String -> ShowS
showString String
"logical64"
    Prim p k a
PChar   -> String -> ShowS
showString String
"character"

instance Pretty1 ArrValue where
  prettys1Prec :: forall a. Int -> ArrValue a -> ShowS
prettys1Prec Int
p = Int -> D a -> ShowS
forall a. Int -> D a -> ShowS
forall {k} (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
p (D a -> ShowS) -> (ArrValue a -> D a) -> ArrValue a -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArrValue a -> D a
forall a. ArrValue a -> D a
dArrValue

instance (Pretty1 f) => Pretty1 (Field f) where
  prettys1Prec :: forall (a :: (Symbol, k)). Int -> Field f a -> ShowS
prettys1Prec Int
_ = \case
    Field SSymbol name
fname f a
x ->
      Int -> f a -> ShowS
forall (a :: k). Int -> f a -> ShowS
forall {k} (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
0 f a
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      Sing name -> (KnownSymbol name => ShowS) -> ShowS
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing name
SSymbol name
fname (String -> ShowS
showString (SSymbol name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal SSymbol name
fname))

-- | e.g. "type custom_type { character a, integer array b }"
instance Pretty1 D where
  prettys1Prec :: forall a. Int -> D a -> ShowS
prettys1Prec Int
p = \case
    DPrim Prim p k a
px -> Int -> Prim p k a -> ShowS
forall a. Int -> Prim p k a -> ShowS
forall {k} (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
p Prim p k a
px
    DArray Index i
_ ArrValue a
pv -> Int -> ArrValue a -> ShowS
forall a. Int -> ArrValue a -> ShowS
forall {k} (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
prettys1Prec Int
p ArrValue a
pv ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" array"
    DData SSymbol name
rname Rec (Field D) fs
fields ->
        Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
8)
      (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"type "
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing name -> (KnownSymbol name => ShowS) -> ShowS
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing name
SSymbol name
rname (String -> ShowS
showString (SSymbol name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal SSymbol name
rname))
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"{ "
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Endo String -> ShowS
forall a. Endo a -> a -> a
appEndo ( [Endo String] -> Endo String
forall a. Monoid a => [a] -> a
mconcat
              ([Endo String] -> Endo String)
-> (Rec (Field D) fs -> [Endo String])
-> Rec (Field D) fs
-> Endo String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Endo String -> [Endo String] -> [Endo String]
forall a. a -> [a] -> [a]
intersperse (ShowS -> Endo String
forall a. (a -> a) -> Endo a
Endo (ShowS -> Endo String) -> ShowS -> Endo String
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
", ")
              ([Endo String] -> [Endo String])
-> (Rec (Field D) fs -> [Endo String])
-> Rec (Field D) fs
-> [Endo String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Const (Endo String)) fs -> [Endo String]
forall a. Rec (Const a) fs -> [a]
forall {u} (rs :: [u]) a.
RecordToList rs =>
Rec (Const a) rs -> [a]
recordToList
              (Rec (Const (Endo String)) fs -> [Endo String])
-> (Rec (Field D) fs -> Rec (Const (Endo String)) fs)
-> Rec (Field D) fs
-> [Endo String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: (Symbol, *)). Field D x -> Const (Endo String) x)
-> Rec (Field D) fs -> Rec (Const (Endo String)) fs
forall {u} (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
forall (f :: (Symbol, *) -> *) (g :: (Symbol, *) -> *).
(forall (x :: (Symbol, *)). f x -> g x) -> Rec f fs -> Rec g fs
rmap (Endo String -> Const (Endo String) x
forall k a (b :: k). a -> Const a b
Const (Endo String -> Const (Endo String) x)
-> (Field D x -> Endo String) -> Field D x -> Const (Endo String) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> Endo String
forall a. (a -> a) -> Endo a
Endo (ShowS -> Endo String)
-> (Field D x -> ShowS) -> Field D x -> Endo String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Field D x -> ShowS
forall {k} (t :: k -> *) (a :: k). Pretty1 t => Int -> t a -> ShowS
forall (a :: (Symbol, *)). Int -> Field D a -> ShowS
prettys1Prec Int
0)
              (Rec (Field D) fs -> Endo String)
-> Rec (Field D) fs -> Endo String
forall a b. (a -> b) -> a -> b
$ Rec (Field D) fs
fields)
      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" }"