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

{-# 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)

import           Data.Singletons.TypeLits

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
showList :: [Bool8] -> ShowS
$cshowList :: [Bool8] -> ShowS
show :: Bool8 -> String
$cshow :: Bool8 -> String
showsPrec :: Int -> Bool8 -> ShowS
$cshowsPrec :: Int -> 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
fromInteger :: Integer -> Bool8
$cfromInteger :: Integer -> Bool8
signum :: Bool8 -> Bool8
$csignum :: Bool8 -> Bool8
abs :: Bool8 -> Bool8
$cabs :: Bool8 -> Bool8
negate :: Bool8 -> Bool8
$cnegate :: Bool8 -> Bool8
* :: Bool8 -> Bool8 -> Bool8
$c* :: Bool8 -> Bool8 -> Bool8
- :: Bool8 -> Bool8 -> Bool8
$c- :: Bool8 -> Bool8 -> Bool8
+ :: Bool8 -> Bool8 -> Bool8
$c+ :: Bool8 -> Bool8 -> Bool8
Num, Bool8 -> Bool8 -> Bool
(Bool8 -> Bool8 -> Bool) -> (Bool8 -> Bool8 -> Bool) -> Eq Bool8
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Bool8 -> Bool8 -> Bool
$c/= :: Bool8 -> Bool8 -> Bool
== :: Bool8 -> Bool8 -> Bool
$c== :: 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
showList :: [Bool16] -> ShowS
$cshowList :: [Bool16] -> ShowS
show :: Bool16 -> String
$cshow :: Bool16 -> String
showsPrec :: Int -> Bool16 -> ShowS
$cshowsPrec :: Int -> 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
fromInteger :: Integer -> Bool16
$cfromInteger :: Integer -> Bool16
signum :: Bool16 -> Bool16
$csignum :: Bool16 -> Bool16
abs :: Bool16 -> Bool16
$cabs :: Bool16 -> Bool16
negate :: Bool16 -> Bool16
$cnegate :: Bool16 -> Bool16
* :: Bool16 -> Bool16 -> Bool16
$c* :: Bool16 -> Bool16 -> Bool16
- :: Bool16 -> Bool16 -> Bool16
$c- :: Bool16 -> Bool16 -> Bool16
+ :: Bool16 -> Bool16 -> Bool16
$c+ :: Bool16 -> Bool16 -> Bool16
Num, Bool16 -> Bool16 -> Bool
(Bool16 -> Bool16 -> Bool)
-> (Bool16 -> Bool16 -> Bool) -> Eq Bool16
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Bool16 -> Bool16 -> Bool
$c/= :: Bool16 -> Bool16 -> Bool
== :: Bool16 -> Bool16 -> Bool
$c== :: 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
showList :: [Bool32] -> ShowS
$cshowList :: [Bool32] -> ShowS
show :: Bool32 -> String
$cshow :: Bool32 -> String
showsPrec :: Int -> Bool32 -> ShowS
$cshowsPrec :: Int -> 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
fromInteger :: Integer -> Bool32
$cfromInteger :: Integer -> Bool32
signum :: Bool32 -> Bool32
$csignum :: Bool32 -> Bool32
abs :: Bool32 -> Bool32
$cabs :: Bool32 -> Bool32
negate :: Bool32 -> Bool32
$cnegate :: Bool32 -> Bool32
* :: Bool32 -> Bool32 -> Bool32
$c* :: Bool32 -> Bool32 -> Bool32
- :: Bool32 -> Bool32 -> Bool32
$c- :: Bool32 -> Bool32 -> Bool32
+ :: Bool32 -> Bool32 -> Bool32
$c+ :: Bool32 -> Bool32 -> Bool32
Num, Bool32 -> Bool32 -> Bool
(Bool32 -> Bool32 -> Bool)
-> (Bool32 -> Bool32 -> Bool) -> Eq Bool32
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Bool32 -> Bool32 -> Bool
$c/= :: Bool32 -> Bool32 -> Bool
== :: Bool32 -> Bool32 -> Bool
$c== :: 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
showList :: [Bool64] -> ShowS
$cshowList :: [Bool64] -> ShowS
show :: Bool64 -> String
$cshow :: Bool64 -> String
showsPrec :: Int -> Bool64 -> ShowS
$cshowsPrec :: Int -> 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
fromInteger :: Integer -> Bool64
$cfromInteger :: Integer -> Bool64
signum :: Bool64 -> Bool64
$csignum :: Bool64 -> Bool64
abs :: Bool64 -> Bool64
$cabs :: Bool64 -> Bool64
negate :: Bool64 -> Bool64
$cnegate :: Bool64 -> Bool64
* :: Bool64 -> Bool64 -> Bool64
$c* :: Bool64 -> Bool64 -> Bool64
- :: Bool64 -> Bool64 -> Bool64
$c- :: Bool64 -> Bool64 -> Bool64
+ :: Bool64 -> Bool64 -> Bool64
$c+ :: Bool64 -> Bool64 -> Bool64
Num, Bool64 -> Bool64 -> Bool
(Bool64 -> Bool64 -> Bool)
-> (Bool64 -> Bool64 -> Bool) -> Eq Bool64
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Bool64 -> Bool64 -> Bool
$c/= :: Bool64 -> Bool64 -> Bool
== :: Bool64 -> Bool64 -> Bool
$c== :: 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
showList :: [Char8] -> ShowS
$cshowList :: [Char8] -> ShowS
show :: Char8 -> String
$cshow :: Char8 -> String
showsPrec :: Int -> Char8 -> ShowS
$cshowsPrec :: Int -> 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
fromInteger :: Integer -> Char8
$cfromInteger :: Integer -> Char8
signum :: Char8 -> Char8
$csignum :: Char8 -> Char8
abs :: Char8 -> Char8
$cabs :: Char8 -> Char8
negate :: Char8 -> Char8
$cnegate :: Char8 -> Char8
* :: Char8 -> Char8 -> Char8
$c* :: Char8 -> Char8 -> Char8
- :: Char8 -> Char8 -> Char8
$c- :: Char8 -> Char8 -> Char8
+ :: Char8 -> Char8 -> Char8
$c+ :: Char8 -> Char8 -> Char8
Num, Char8 -> Char8 -> Bool
(Char8 -> Char8 -> Bool) -> (Char8 -> Char8 -> Bool) -> Eq Char8
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Char8 -> Char8 -> Bool
$c/= :: Char8 -> Char8 -> Bool
== :: Char8 -> Char8 -> Bool
$c== :: 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 { 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
showList :: [PrimS a] -> ShowS
$cshowList :: forall a. Show a => [PrimS a] -> ShowS
show :: PrimS a -> String
$cshow :: forall a. Show a => PrimS a -> String
showsPrec :: Int -> PrimS a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> 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
/= :: PrimS a -> PrimS a -> Bool
$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
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 :: Index i -> D i
dIndex (Index Prim p 'BTInt a
p) = Prim p 'BTInt a -> D (PrimS a)
forall (p :: Precision) (k :: BasicType) a.
Prim p k 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 :: ArrValue a -> D a
dArrValue (ArrPrim Prim p k a
p) = Prim p k a -> D (PrimS a)
forall (p :: Precision) (k :: BasicType) a.
Prim p k 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 (fs :: [(Symbol, *)]) (name :: Symbol).
(RMap fs, RecordToList fs, RApply fs) =>
SSymbol name -> Rec (Field D) fs -> D (Record name fs)
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
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' 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 :: (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
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 (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 (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 '(name, a)) -> t (g a) -> t (Field g '(name, a))
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 (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 (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 :: 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 :: Int -> ArrValue a -> ShowS
prettys1Prec Int
p = 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 :: Int -> Field f a -> ShowS
prettys1Prec Int
_ = \case
    Field SSymbol name
fname f a
x ->
      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 :: Int -> D a -> ShowS
prettys1Prec Int
p = \case
    DPrim Prim p k a
px -> 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 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 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
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
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
" }"