camfort-1.0.1: CamFort - Cambridge Fortran infrastructure
Safe HaskellNone
LanguageHaskell2010

Language.Fortran.Model.Types

Description

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.

Synopsis

Fortran Types

data D a where Source #

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.

Constructors

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) 

Instances

Instances details
Pretty1 D Source #

e.g. "type custom_type { character a, integer array b }"

Instance details

Defined in Language.Fortran.Model.Types

Methods

pretty1 :: forall (a :: k). D a -> String

prettys1Prec :: forall (a :: k). Int -> D a -> ShowS

Semantic Types

newtype Bool8 Source #

Constructors

Bool8 

Fields

Instances

Instances details
Eq Bool8 Source # 
Instance details

Defined in Language.Fortran.Model.Types

Methods

(==) :: Bool8 -> Bool8 -> Bool #

(/=) :: Bool8 -> Bool8 -> Bool #

Num Bool8 Source # 
Instance details

Defined in Language.Fortran.Model.Types

Show Bool8 Source # 
Instance details

Defined in Language.Fortran.Model.Types

Methods

showsPrec :: Int -> Bool8 -> ShowS #

show :: Bool8 -> String #

showList :: [Bool8] -> ShowS #

LiftD (PrimS Bool8) Bool Source # 
Instance details

Defined in Language.Fortran.Model.Repr

newtype Bool16 Source #

Constructors

Bool16 

Fields

Instances

Instances details
Eq Bool16 Source # 
Instance details

Defined in Language.Fortran.Model.Types

Methods

(==) :: Bool16 -> Bool16 -> Bool #

(/=) :: Bool16 -> Bool16 -> Bool #

Num Bool16 Source # 
Instance details

Defined in Language.Fortran.Model.Types

Show Bool16 Source # 
Instance details

Defined in Language.Fortran.Model.Types

LiftD (PrimS Bool16) Bool Source # 
Instance details

Defined in Language.Fortran.Model.Repr

newtype Bool32 Source #

Constructors

Bool32 

Fields

Instances

Instances details
Eq Bool32 Source # 
Instance details

Defined in Language.Fortran.Model.Types

Methods

(==) :: Bool32 -> Bool32 -> Bool #

(/=) :: Bool32 -> Bool32 -> Bool #

Num Bool32 Source # 
Instance details

Defined in Language.Fortran.Model.Types

Show Bool32 Source # 
Instance details

Defined in Language.Fortran.Model.Types

LiftD (PrimS Bool32) Bool Source # 
Instance details

Defined in Language.Fortran.Model.Repr

newtype Bool64 Source #

Constructors

Bool64 

Fields

Instances

Instances details
Eq Bool64 Source # 
Instance details

Defined in Language.Fortran.Model.Types

Methods

(==) :: Bool64 -> Bool64 -> Bool #

(/=) :: Bool64 -> Bool64 -> Bool #

Num Bool64 Source # 
Instance details

Defined in Language.Fortran.Model.Types

Show Bool64 Source # 
Instance details

Defined in Language.Fortran.Model.Types

LiftD (PrimS Bool64) Bool Source # 
Instance details

Defined in Language.Fortran.Model.Repr

newtype Char8 Source #

Constructors

Char8 

Fields

Instances

Instances details
Eq Char8 Source # 
Instance details

Defined in Language.Fortran.Model.Types

Methods

(==) :: Char8 -> Char8 -> Bool #

(/=) :: Char8 -> Char8 -> Bool #

Num Char8 Source # 
Instance details

Defined in Language.Fortran.Model.Types

Show Char8 Source # 
Instance details

Defined in Language.Fortran.Model.Types

Methods

showsPrec :: Int -> Char8 -> ShowS #

show :: Char8 -> String #

showList :: [Char8] -> ShowS #

LiftD (PrimS Char8) Word8 Source # 
Instance details

Defined in Language.Fortran.Model.Repr

newtype PrimS a Source #

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.

Constructors

PrimS 

Fields

Instances

Instances details
Eq a => Eq (PrimS a) Source # 
Instance details

Defined in Language.Fortran.Model.Types

Methods

(==) :: PrimS a -> PrimS a -> Bool #

(/=) :: PrimS a -> PrimS a -> Bool #

Show a => Show (PrimS a) Source # 
Instance details

Defined in Language.Fortran.Model.Types

Methods

showsPrec :: Int -> PrimS a -> ShowS #

show :: PrimS a -> String #

showList :: [PrimS a] -> ShowS #

LiftD (PrimS Double) AlgReal Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Float) AlgReal Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Int8) Integer Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Int16) Integer Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Int32) Integer Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Int64) Integer Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Char8) Word8 Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Bool64) Bool Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Bool32) Bool Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Bool16) Bool Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Bool8) Bool Source # 
Instance details

Defined in Language.Fortran.Model.Repr

Primitive Types

data Prim p k a where Source #

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.

Instances

Instances details
Pretty1 (Prim p k :: Type -> Type) Source # 
Instance details

Defined in Language.Fortran.Model.Types

Methods

pretty1 :: forall (a :: k0). Prim p k a -> String

prettys1Prec :: forall (a :: k0). Int -> Prim p k a -> ShowS

Arrays

data Index a where Source #

Specifies which types can be used as array indices.

Constructors

Index :: Prim p 'BTInt a -> Index (PrimS a) 

data ArrValue a where Source #

Specifies which types can be stored in arrays. Currently arrays of arrays are not supported.

Constructors

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) 

Instances

Instances details
Pretty1 ArrValue Source # 
Instance details

Defined in Language.Fortran.Model.Types

Methods

pretty1 :: forall (a :: k). ArrValue a -> String

prettys1Prec :: forall (a :: k). Int -> ArrValue a -> ShowS

newtype Array i a Source #

An array with a phantom index type. Mostly used at the type-level to constrain instances of D (Array i a) etc.

Constructors

Array [a] 

Records

data Field f field where Source #

A field over a pair of name and value type.

Constructors

Field :: SSymbol name -> f a -> Field f '(name, a) 

Instances

Instances details
Pretty1 f => Pretty1 (Field f :: (Symbol, k) -> Type) Source # 
Instance details

Defined in Language.Fortran.Model.Types

Methods

pretty1 :: forall (a :: k0). Field f a -> String

prettys1Prec :: forall (a :: k0). Int -> Field f a -> ShowS

data Record name fields where Source #

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.

Constructors

Record :: RMap fields => SSymbol name -> Rec (Field Identity) fields -> Record name fields 

Combinators

dIndex :: Index i -> D i Source #

Any Fortran index type is a valid Fortran type.

dArrValue :: ArrValue a -> D a Source #

Anything that can be stored in Fortran arrays is a valid Fortran type.

overField :: (f a -> g b) -> Field f '(name, a) -> Field g '(name, b) Source #

Given a field with known contents, we can change the functor and value type.

overField' :: (forall a. f a -> g a) -> Field f nv -> Field g nv Source #

Given a field with unknown contents, we can change the functor but not the value type.

traverseField' :: Functor t => (forall a. f a -> t (g a)) -> Field f nv -> t (Field g nv) Source #

zipFieldsWith :: (forall a. f a -> g a -> h a) -> Field f nv -> Field g nv -> Field h nv Source #

Combine two fields over the same name-value pair but (potentially) different functors.

zip3FieldsWith :: (forall a. f a -> g a -> h a -> i a) -> Field f nv -> Field g nv -> Field h nv -> Field i nv Source #