{-# LANGUAGE DeriveDataTypeable, KindSignatures, PolyKinds, RankNTypes, ScopedTypeVariables,
             TypeApplications, TypeFamilies, TypeFamilyDependencies, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}

-- | Finally Tagless Abstract Syntax Tree definitions for the programming language Oberon

module Language.Oberon.Abstract (-- * Language classes
                                 Wirthy(..), CoWirthy(..), Oberon(..), Oberon2(..), Nameable(..),
                                 -- * Type synonyms
                                 Ident, IdentList, BaseType, ReturnType, ConstExpression,
                                 -- * Auxiliary data types
                                 RelOp(..), WirthySubsetOf(..), Maybe3(..),
                                 -- * Utilities
                                 just3, nothing3, maybe3, 
                                 ) where

import Data.Data (Data)
import Data.Kind (Constraint)
import Data.List.NonEmpty
import Data.Text (Text)

import Prelude hiding (and, not, or, read, subtract)

type Ident = Text

-- | Relational operators
data RelOp = Equal | Unequal | Less | LessOrEqual | Greater | GreaterOrEqual | In
   deriving (Typeable RelOp
RelOp -> DataType
RelOp -> Constr
(forall b. Data b => b -> b) -> RelOp -> RelOp
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> RelOp -> u
forall u. (forall d. Data d => d -> u) -> RelOp -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RelOp -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RelOp -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RelOp -> m RelOp
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RelOp -> m RelOp
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RelOp
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RelOp -> c RelOp
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RelOp)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RelOp)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RelOp -> m RelOp
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RelOp -> m RelOp
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RelOp -> m RelOp
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RelOp -> m RelOp
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RelOp -> m RelOp
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RelOp -> m RelOp
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RelOp -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RelOp -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> RelOp -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RelOp -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RelOp -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RelOp -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RelOp -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RelOp -> r
gmapT :: (forall b. Data b => b -> b) -> RelOp -> RelOp
$cgmapT :: (forall b. Data b => b -> b) -> RelOp -> RelOp
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RelOp)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RelOp)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RelOp)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RelOp)
dataTypeOf :: RelOp -> DataType
$cdataTypeOf :: RelOp -> DataType
toConstr :: RelOp -> Constr
$ctoConstr :: RelOp -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RelOp
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RelOp
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RelOp -> c RelOp
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RelOp -> c RelOp
Data, RelOp -> RelOp -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RelOp -> RelOp -> Bool
$c/= :: RelOp -> RelOp -> Bool
== :: RelOp -> RelOp -> Bool
$c== :: RelOp -> RelOp -> Bool
Eq, Int -> RelOp -> ShowS
[RelOp] -> ShowS
RelOp -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RelOp] -> ShowS
$cshowList :: [RelOp] -> ShowS
show :: RelOp -> String
$cshow :: RelOp -> String
showsPrec :: Int -> RelOp -> ShowS
$cshowsPrec :: Int -> RelOp -> ShowS
Show)

-- | The finally-tagless associated types and methods relevant to all programming languages designed by Niklaus
-- Wirth. Every non-leaf node type has four type variables:
--
-- * type variable @l@ represents the language of the constructs built by the methods,
-- * @l'@ is the language of the child node constructs,
-- * @f'@ wraps all descendant nodes, except
-- * @f@ wraps all direct children of the node.
class Wirthy l where
   type Module l      = (m :: * -> (* -> *) -> (* -> *) -> *) | m -> l
   type Declaration l = (d :: * -> (* -> *) -> (* -> *) -> *) | d -> l
   type Type l        = (t :: * -> (* -> *) -> (* -> *) -> *) | t -> l
   type Statement l   = (s :: * -> (* -> *) -> (* -> *) -> *) | s -> l
   type Expression l  = (e :: * -> (* -> *) -> (* -> *) -> *) | e -> l
   type Designator l  = (d :: * -> (* -> *) -> (* -> *) -> *) | d -> l
   type Value l       = (v :: * -> (* -> *) -> (* -> *) -> *) | v -> l

   type FieldList l         = (x :: * -> (* -> *) -> (* -> *) -> *) | x -> l
   type ProcedureHeading l  = (x :: * -> (* -> *) -> (* -> *) -> *) | x -> l
   type FormalParameters l  = (x :: * -> (* -> *) -> (* -> *) -> *) | x -> l
   type FPSection l         = (x :: * -> (* -> *) -> (* -> *) -> *) | x -> l
   type Block l             = (x :: * -> (* -> *) -> (* -> *) -> *) | x -> l
   type StatementSequence l = (x :: * -> (* -> *) -> (* -> *) -> *) | x -> l
   type Case l              = (x :: * -> (* -> *) -> (* -> *) -> *) | x -> l
   type CaseLabels l        = (x :: * -> (* -> *) -> (* -> *) -> *) | x -> l
   type ConditionalBranch l = (x :: * -> (* -> *) -> (* -> *) -> *) | x -> l
   type Element l           = (x :: * -> (* -> *) -> (* -> *) -> *) | x -> l
   
   type Import l  = x | x -> l
   type IdentDef l  = x | x -> l
   type QualIdent l = x | x -> l

   -- Declaration
   constantDeclaration :: IdentDef l' -> f (ConstExpression l' l' f' f') -> Declaration l l' f' f
   typeDeclaration :: IdentDef l' -> f (Type l' l' f' f') -> Declaration l l' f' f
   variableDeclaration :: IdentList l' -> f (Type l' l' f' f') -> Declaration l l' f' f
   procedureDeclaration :: f (ProcedureHeading l' l' f' f') -> f (Block l' l' f' f') -> Declaration l l' f' f

   formalParameters :: [f (FPSection l' l' f' f')] -> Maybe (ReturnType l') -> FormalParameters l l' f' f
   fpSection :: Bool -> [Ident] -> f (Type l' l' f' f') -> FPSection l l' f' f
   block :: [f (Declaration l' l' f' f')] -> Maybe (f (StatementSequence l' l' f' f')) -> Block l l' f' f

   fieldList :: NonEmpty (IdentDef l') -> f (Type l' l' f' f') -> FieldList l l' f' f

   -- Type
   pointerType :: f (Type l' l' f' f') -> Type l l' f' f
   procedureType :: Maybe (f (FormalParameters l' l' f' f')) -> Type l l' f' f
   typeReference :: QualIdent l' -> Type l l' f' f

   -- Statement
   assignment :: f (Designator l' l' f' f') -> f (Expression l' l' f' f') -> Statement l l' f' f
   caseStatement :: f (Expression l' l' f' f') -> [f (Case l' l' f' f')] -> Maybe (f (StatementSequence l' l' f' f')) 
                 -> Statement l l' f' f
   emptyStatement :: Statement l l' f' f
   exitStatement :: Statement l l' f' f
   ifStatement :: NonEmpty (f (ConditionalBranch l' l' f' f'))
               -> Maybe (f (StatementSequence l' l' f' f')) 
               -> Statement l l' f' f
   loopStatement :: f (StatementSequence l' l' f' f') -> Statement l l' f' f
   procedureCall :: f (Designator l' l' f' f') -> Maybe [f (Expression l' l' f' f')] -> Statement l l' f' f
   repeatStatement :: f (StatementSequence l' l' f' f') -> f (Expression l' l' f' f') -> Statement l l' f' f
   returnStatement :: Maybe (f (Expression l' l' f' f')) -> Statement l l' f' f
   whileStatement :: f (Expression l' l' f' f') -> f (StatementSequence l' l' f' f') -> Statement l l' f' f

   conditionalBranch :: f (Expression l' l' f' f') -> f (StatementSequence l' l' f' f') -> ConditionalBranch l l' f' f
   caseAlternative :: NonEmpty (f (CaseLabels l' l' f' f')) -> f (StatementSequence l' l' f' f') -> Case l l' f' f

   singleLabel :: f (ConstExpression l' l' f' f') -> CaseLabels l l' f' f
   labelRange :: f (ConstExpression l' l' f' f') -> f (ConstExpression l' l' f' f') -> CaseLabels l l' f' f

   statementSequence :: [f (Statement l' l' f' f')] -> StatementSequence l l' f' f

   -- Expression
   add, subtract :: f (Expression l' l' f' f') -> f (Expression l' l' f' f') -> Expression l l' f' f
   and, or :: f (Expression l' l' f' f') -> f (Expression l' l' f' f') -> Expression l l' f' f
   divide, integerDivide, modulo, multiply :: f (Expression l' l' f' f') -> f (Expression l' l' f' f') -> Expression l l' f' f
   functionCall :: f (Designator l' l' f' f') -> [f (Expression l' l' f' f')] -> Expression l l' f' f
   literal :: f (Value l' l' f' f') -> Expression l l' f' f
   negative, positive :: f (Expression l' l' f' f') -> Expression l l' f' f
   not :: f (Expression l' l' f' f') -> Expression l l' f' f
   read :: f (Designator l' l' f' f') -> Expression l l' f' f
   relation :: RelOp -> f (Expression l' l' f' f') -> f (Expression l' l' f' f') -> Expression l l' f' f

   element :: f (Expression l' l' f' f') -> Element l l' f' f
   range :: f (Expression l' l' f' f') -> f (Expression l' l' f' f') -> Element l l' f' f

   -- Value
   integer :: Integer -> Value l l' f' f
   nil, false, true :: Value l l' f' f
   real :: Double -> Value l l' f' f
   string :: Text -> Value l l' f' f
   charCode :: Int -> Value l l' f' f
   builtin :: Text -> Value l l' f' f

   -- Designator
   variable :: QualIdent l' -> Designator l l' f' f
   field :: f (Designator l' l' f' f') -> Ident -> Designator l l' f' f
   index :: f (Designator l' l' f' f') -> NonEmpty (f (Expression l' l' f' f')) -> Designator l l' f' f
   dereference :: f (Designator l' l' f' f') -> Designator l l' f' f

   -- Identifier
   identDef :: Ident -> IdentDef l
   nonQualIdent :: Ident -> QualIdent l

-- | An instance of this type can convert its own constructs to another language that's an instance of 'TargetClass'.
class Wirthy l => CoWirthy l where
   type TargetClass l :: * -> Constraint
   type TargetClass l = Wirthy
   coDeclaration :: TargetClass l l' => Declaration l l'' f' f -> Declaration l' l'' f' f
   coType        :: TargetClass l l' => Type l l'' f' f        -> Type l' l'' f' f
   coStatement   :: TargetClass l l' => Statement l l'' f' f   -> Statement l' l'' f' f
   coExpression  :: TargetClass l l' => Expression l l'' f' f  -> Expression l' l'' f' f
   coDesignator  :: TargetClass l l' => Designator l l'' f' f  -> Designator l' l'' f' f
   coValue       :: TargetClass l l' => Value l l'' f' f       -> Value l' l'' f' f

-- | A language with constructs beyond the base 'Wirthy' class will have constructs that cannot be converted to a
-- | 'Wirthy' target. It can declare its 'TargetClass' to be this transformed language instead, whose language
-- | constructs are all wrapped in 'Maybe' or 'Maybe3'.
data WirthySubsetOf l = WirthySubsetOf l

-- | A modified 'Maybe' with kind that fits the types associated with 'Wirthy'.
newtype Maybe3 f a b c = Maybe3 (Maybe (f a b c)) deriving (Maybe3 f a b c -> Maybe3 f a b c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Eq (f a b c) =>
Maybe3 f a b c -> Maybe3 f a b c -> Bool
/= :: Maybe3 f a b c -> Maybe3 f a b c -> Bool
$c/= :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Eq (f a b c) =>
Maybe3 f a b c -> Maybe3 f a b c -> Bool
== :: Maybe3 f a b c -> Maybe3 f a b c -> Bool
$c== :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Eq (f a b c) =>
Maybe3 f a b c -> Maybe3 f a b c -> Bool
Eq, Maybe3 f a b c -> Maybe3 f a b c -> Bool
Maybe3 f a b c -> Maybe3 f a b c -> Ordering
Maybe3 f a b c -> Maybe3 f a b c -> Maybe3 f a b c
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Ord (f a b c) =>
Eq (Maybe3 f a b c)
forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Ord (f a b c) =>
Maybe3 f a b c -> Maybe3 f a b c -> Bool
forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Ord (f a b c) =>
Maybe3 f a b c -> Maybe3 f a b c -> Ordering
forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Ord (f a b c) =>
Maybe3 f a b c -> Maybe3 f a b c -> Maybe3 f a b c
min :: Maybe3 f a b c -> Maybe3 f a b c -> Maybe3 f a b c
$cmin :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Ord (f a b c) =>
Maybe3 f a b c -> Maybe3 f a b c -> Maybe3 f a b c
max :: Maybe3 f a b c -> Maybe3 f a b c -> Maybe3 f a b c
$cmax :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Ord (f a b c) =>
Maybe3 f a b c -> Maybe3 f a b c -> Maybe3 f a b c
>= :: Maybe3 f a b c -> Maybe3 f a b c -> Bool
$c>= :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Ord (f a b c) =>
Maybe3 f a b c -> Maybe3 f a b c -> Bool
> :: Maybe3 f a b c -> Maybe3 f a b c -> Bool
$c> :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Ord (f a b c) =>
Maybe3 f a b c -> Maybe3 f a b c -> Bool
<= :: Maybe3 f a b c -> Maybe3 f a b c -> Bool
$c<= :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Ord (f a b c) =>
Maybe3 f a b c -> Maybe3 f a b c -> Bool
< :: Maybe3 f a b c -> Maybe3 f a b c -> Bool
$c< :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Ord (f a b c) =>
Maybe3 f a b c -> Maybe3 f a b c -> Bool
compare :: Maybe3 f a b c -> Maybe3 f a b c -> Ordering
$ccompare :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Ord (f a b c) =>
Maybe3 f a b c -> Maybe3 f a b c -> Ordering
Ord, ReadPrec [Maybe3 f a b c]
ReadPrec (Maybe3 f a b c)
ReadS [Maybe3 f a b c]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Read (f a b c) =>
ReadPrec [Maybe3 f a b c]
forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Read (f a b c) =>
ReadPrec (Maybe3 f a b c)
forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Read (f a b c) =>
Int -> ReadS (Maybe3 f a b c)
forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Read (f a b c) =>
ReadS [Maybe3 f a b c]
readListPrec :: ReadPrec [Maybe3 f a b c]
$creadListPrec :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Read (f a b c) =>
ReadPrec [Maybe3 f a b c]
readPrec :: ReadPrec (Maybe3 f a b c)
$creadPrec :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Read (f a b c) =>
ReadPrec (Maybe3 f a b c)
readList :: ReadS [Maybe3 f a b c]
$creadList :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Read (f a b c) =>
ReadS [Maybe3 f a b c]
readsPrec :: Int -> ReadS (Maybe3 f a b c)
$creadsPrec :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Read (f a b c) =>
Int -> ReadS (Maybe3 f a b c)
Read, Int -> Maybe3 f a b c -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Show (f a b c) =>
Int -> Maybe3 f a b c -> ShowS
forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Show (f a b c) =>
[Maybe3 f a b c] -> ShowS
forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Show (f a b c) =>
Maybe3 f a b c -> String
showList :: [Maybe3 f a b c] -> ShowS
$cshowList :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Show (f a b c) =>
[Maybe3 f a b c] -> ShowS
show :: Maybe3 f a b c -> String
$cshow :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Show (f a b c) =>
Maybe3 f a b c -> String
showsPrec :: Int -> Maybe3 f a b c -> ShowS
$cshowsPrec :: forall k k k (f :: k -> k -> k -> *) (a :: k) (b :: k) (c :: k).
Show (f a b c) =>
Int -> Maybe3 f a b c -> ShowS
Show)

-- | Smart 'Maybe3' constructor corresponding to 'Just'
just3 :: f a b c -> Maybe3 f a b c
just3 = forall {k} {k} {k} (f :: k -> k -> k -> *) (a :: k) (b :: k)
       (c :: k).
Maybe (f a b c) -> Maybe3 f a b c
Maybe3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just
-- | Smart 'Maybe3' constructor corresponding to 'Nothing'
nothing3 :: Maybe3 f a b c
nothing3 = forall {k} {k} {k} (f :: k -> k -> k -> *) (a :: k) (b :: k)
       (c :: k).
Maybe (f a b c) -> Maybe3 f a b c
Maybe3 forall a. Maybe a
Nothing
-- | Smart 'Maybe3' destructor corresponding to 'maybe'
maybe3 :: b -> (f a b c -> b) -> Maybe3 f a b c -> b
maybe3 b
n f a b c -> b
f (Maybe3 Maybe (f a b c)
x) = forall b a. b -> (a -> b) -> Maybe a -> b
maybe b
n f a b c -> b
f Maybe (f a b c)
x

instance Wirthy l => Wirthy (WirthySubsetOf l) where
   type Module (WirthySubsetOf l)            = Maybe3 (Module l)
   type Declaration (WirthySubsetOf l)       = Maybe3 (Declaration l)
   type Type (WirthySubsetOf l)              = Maybe3 (Type l)
   type Statement (WirthySubsetOf l)         = Maybe3 (Statement l)
   type Expression (WirthySubsetOf l)        = Maybe3 (Expression l)
   type Designator (WirthySubsetOf l)        = Maybe3 (Designator l)
   type Value (WirthySubsetOf l)             = Maybe3 (Value l)

   type FieldList (WirthySubsetOf l)         = Maybe3 (FieldList l)
   type ProcedureHeading (WirthySubsetOf l)  = Maybe3 (ProcedureHeading l)
   type FormalParameters (WirthySubsetOf l)  = Maybe3 (FormalParameters l)
   type FPSection (WirthySubsetOf l)         = Maybe3 (FPSection l)
   type Block (WirthySubsetOf l)             = Maybe3 (Block l)
   type StatementSequence (WirthySubsetOf l) = Maybe3 (StatementSequence l)
   type Case (WirthySubsetOf l)              = Maybe3 (Case l)
   type CaseLabels (WirthySubsetOf l)        = Maybe3 (CaseLabels l)
   type ConditionalBranch (WirthySubsetOf l) = Maybe3 (ConditionalBranch l)
   type Element (WirthySubsetOf l)           = Maybe3 (Element l)
   
   type Import (WirthySubsetOf l)            = Maybe (Import l)
   type IdentDef (WirthySubsetOf l)          = Maybe (IdentDef l)
   type QualIdent (WirthySubsetOf l)         = Maybe (QualIdent l)

   -- Declaration
   constantDeclaration :: forall l' (f :: * -> *) (f' :: * -> *).
IdentDef l'
-> f (ConstExpression l' l' f' f')
-> Declaration (WirthySubsetOf l) l' f' f
constantDeclaration = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l l' (f :: * -> *) (f' :: * -> *).
Wirthy l =>
IdentDef l'
-> f (ConstExpression l' l' f' f') -> Declaration l l' f' f
constantDeclaration @l
   typeDeclaration :: forall l' (f :: * -> *) (f' :: * -> *).
IdentDef l'
-> f (Type l' l' f' f') -> Declaration (WirthySubsetOf l) l' f' f
typeDeclaration = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l l' (f :: * -> *) (f' :: * -> *).
Wirthy l =>
IdentDef l' -> f (Type l' l' f' f') -> Declaration l l' f' f
typeDeclaration @l
   variableDeclaration :: forall l' (f :: * -> *) (f' :: * -> *).
IdentList l'
-> f (Type l' l' f' f') -> Declaration (WirthySubsetOf l) l' f' f
variableDeclaration = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l l' (f :: * -> *) (f' :: * -> *).
Wirthy l =>
IdentList l' -> f (Type l' l' f' f') -> Declaration l l' f' f
variableDeclaration @l
   procedureDeclaration :: forall (f :: * -> *) l' (f' :: * -> *).
f (ProcedureHeading l' l' f' f')
-> f (Block l' l' f' f') -> Declaration (WirthySubsetOf l) l' f' f
procedureDeclaration = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (ProcedureHeading l' l' f' f')
-> f (Block l' l' f' f') -> Declaration l l' f' f
procedureDeclaration @l

   formalParameters :: forall (f :: * -> *) l' (f' :: * -> *).
[f (FPSection l' l' f' f')]
-> Maybe (ReturnType l')
-> FormalParameters (WirthySubsetOf l) l' f' f
formalParameters = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
[f (FPSection l' l' f' f')]
-> Maybe (ReturnType l') -> FormalParameters l l' f' f
formalParameters @l
   fpSection :: forall (f :: * -> *) l' (f' :: * -> *).
Bool
-> [Ident]
-> f (Type l' l' f' f')
-> FPSection (WirthySubsetOf l) l' f' f
fpSection = ((forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
Bool -> [Ident] -> f (Type l' l' f' f') -> FPSection l l' f' f
fpSection @l
   block :: forall (f :: * -> *) l' (f' :: * -> *).
[f (Declaration l' l' f' f')]
-> Maybe (f (StatementSequence l' l' f' f'))
-> Block (WirthySubsetOf l) l' f' f
block = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
[f (Declaration l' l' f' f')]
-> Maybe (f (StatementSequence l' l' f' f')) -> Block l l' f' f
block @l

   fieldList :: forall l' (f :: * -> *) (f' :: * -> *).
NonEmpty (IdentDef l')
-> f (Type l' l' f' f') -> FieldList (WirthySubsetOf l) l' f' f
fieldList = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l l' (f :: * -> *) (f' :: * -> *).
Wirthy l =>
NonEmpty (IdentDef l')
-> f (Type l' l' f' f') -> FieldList l l' f' f
fieldList @l

   -- Type
   pointerType :: forall (f :: * -> *) l' (f' :: * -> *).
f (Type l' l' f' f') -> Type (WirthySubsetOf l) l' f' f
pointerType = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Type l' l' f' f') -> Type l l' f' f
pointerType @l
   procedureType :: forall (f :: * -> *) l' (f' :: * -> *).
Maybe (f (FormalParameters l' l' f' f'))
-> Type (WirthySubsetOf l) l' f' f
procedureType = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
Maybe (f (FormalParameters l' l' f' f')) -> Type l l' f' f
procedureType @l
   typeReference :: forall l' (f' :: * -> *) (f :: * -> *).
QualIdent l' -> Type (WirthySubsetOf l) l' f' f
typeReference = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l l' (f' :: * -> *) (f :: * -> *).
Wirthy l =>
QualIdent l' -> Type l l' f' f
typeReference @l

   -- Statement
   assignment :: forall (f :: * -> *) l' (f' :: * -> *).
f (Designator l' l' f' f')
-> f (Expression l' l' f' f')
-> Statement (WirthySubsetOf l) l' f' f
assignment = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Designator l' l' f' f')
-> f (Expression l' l' f' f') -> Statement l l' f' f
assignment @l
   caseStatement :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f')
-> [f (Case l' l' f' f')]
-> Maybe (f (StatementSequence l' l' f' f'))
-> Statement (WirthySubsetOf l) l' f' f
caseStatement = ((forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f')
-> [f (Case l' l' f' f')]
-> Maybe (f (StatementSequence l' l' f' f'))
-> Statement l l' f' f
caseStatement @l
   emptyStatement :: forall l' (f' :: * -> *) (f :: * -> *).
Statement (WirthySubsetOf l) l' f' f
emptyStatement = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 (forall l l' (f' :: * -> *) (f :: * -> *).
Wirthy l =>
Statement l l' f' f
emptyStatement @l)
   exitStatement :: forall l' (f' :: * -> *) (f :: * -> *).
Statement (WirthySubsetOf l) l' f' f
exitStatement = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 (forall l l' (f' :: * -> *) (f :: * -> *).
Wirthy l =>
Statement l l' f' f
exitStatement @l)
   ifStatement :: forall (f :: * -> *) l' (f' :: * -> *).
NonEmpty (f (ConditionalBranch l' l' f' f'))
-> Maybe (f (StatementSequence l' l' f' f'))
-> Statement (WirthySubsetOf l) l' f' f
ifStatement = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
NonEmpty (f (ConditionalBranch l' l' f' f'))
-> Maybe (f (StatementSequence l' l' f' f')) -> Statement l l' f' f
ifStatement @l
   loopStatement :: forall (f :: * -> *) l' (f' :: * -> *).
f (StatementSequence l' l' f' f')
-> Statement (WirthySubsetOf l) l' f' f
loopStatement = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (StatementSequence l' l' f' f') -> Statement l l' f' f
loopStatement @l
   procedureCall :: forall (f :: * -> *) l' (f' :: * -> *).
f (Designator l' l' f' f')
-> Maybe [f (Expression l' l' f' f')]
-> Statement (WirthySubsetOf l) l' f' f
procedureCall = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Designator l' l' f' f')
-> Maybe [f (Expression l' l' f' f')] -> Statement l l' f' f
procedureCall @l
   repeatStatement :: forall (f :: * -> *) l' (f' :: * -> *).
f (StatementSequence l' l' f' f')
-> f (Expression l' l' f' f')
-> Statement (WirthySubsetOf l) l' f' f
repeatStatement = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (StatementSequence l' l' f' f')
-> f (Expression l' l' f' f') -> Statement l l' f' f
repeatStatement @l
   returnStatement :: forall (f :: * -> *) l' (f' :: * -> *).
Maybe (f (Expression l' l' f' f'))
-> Statement (WirthySubsetOf l) l' f' f
returnStatement = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
Maybe (f (Expression l' l' f' f')) -> Statement l l' f' f
returnStatement @l
   whileStatement :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f')
-> f (StatementSequence l' l' f' f')
-> Statement (WirthySubsetOf l) l' f' f
whileStatement = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f')
-> f (StatementSequence l' l' f' f') -> Statement l l' f' f
whileStatement @l

   conditionalBranch :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f')
-> f (StatementSequence l' l' f' f')
-> ConditionalBranch (WirthySubsetOf l) l' f' f
conditionalBranch = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f')
-> f (StatementSequence l' l' f' f') -> ConditionalBranch l l' f' f
conditionalBranch @l
   caseAlternative :: forall (f :: * -> *) l' (f' :: * -> *).
NonEmpty (f (CaseLabels l' l' f' f'))
-> f (StatementSequence l' l' f' f')
-> Case (WirthySubsetOf l) l' f' f
caseAlternative = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
NonEmpty (f (CaseLabels l' l' f' f'))
-> f (StatementSequence l' l' f' f') -> Case l l' f' f
caseAlternative @l

   singleLabel :: forall (f :: * -> *) l' (f' :: * -> *).
f (ConstExpression l' l' f' f')
-> CaseLabels (WirthySubsetOf l) l' f' f
singleLabel = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (ConstExpression l' l' f' f') -> CaseLabels l l' f' f
singleLabel @l
   labelRange :: forall (f :: * -> *) l' (f' :: * -> *).
f (ConstExpression l' l' f' f')
-> f (ConstExpression l' l' f' f')
-> CaseLabels (WirthySubsetOf l) l' f' f
labelRange = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (ConstExpression l' l' f' f')
-> f (ConstExpression l' l' f' f') -> CaseLabels l l' f' f
labelRange @l

   statementSequence :: forall (f :: * -> *) l' (f' :: * -> *).
[f (Statement l' l' f' f')]
-> StatementSequence (WirthySubsetOf l) l' f' f
statementSequence = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
[f (Statement l' l' f' f')] -> StatementSequence l l' f' f
statementSequence @l

   -- Expression
   add :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f')
-> f (Expression l' l' f' f')
-> Expression (WirthySubsetOf l) l' f' f
add = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f')
-> f (Expression l' l' f' f') -> Expression l l' f' f
add @l
   subtract :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f')
-> f (Expression l' l' f' f')
-> Expression (WirthySubsetOf l) l' f' f
subtract = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f')
-> f (Expression l' l' f' f') -> Expression l l' f' f
subtract @l
   and :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f')
-> f (Expression l' l' f' f')
-> Expression (WirthySubsetOf l) l' f' f
and = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f')
-> f (Expression l' l' f' f') -> Expression l l' f' f
and @l
   or :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f')
-> f (Expression l' l' f' f')
-> Expression (WirthySubsetOf l) l' f' f
or = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f')
-> f (Expression l' l' f' f') -> Expression l l' f' f
or @l
   divide :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f')
-> f (Expression l' l' f' f')
-> Expression (WirthySubsetOf l) l' f' f
divide = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f')
-> f (Expression l' l' f' f') -> Expression l l' f' f
divide @l
   integerDivide :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f')
-> f (Expression l' l' f' f')
-> Expression (WirthySubsetOf l) l' f' f
integerDivide = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f')
-> f (Expression l' l' f' f') -> Expression l l' f' f
integerDivide @l
   modulo :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f')
-> f (Expression l' l' f' f')
-> Expression (WirthySubsetOf l) l' f' f
modulo = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f')
-> f (Expression l' l' f' f') -> Expression l l' f' f
modulo @l
   multiply :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f')
-> f (Expression l' l' f' f')
-> Expression (WirthySubsetOf l) l' f' f
multiply = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f')
-> f (Expression l' l' f' f') -> Expression l l' f' f
multiply @l
   functionCall :: forall (f :: * -> *) l' (f' :: * -> *).
f (Designator l' l' f' f')
-> [f (Expression l' l' f' f')]
-> Expression (WirthySubsetOf l) l' f' f
functionCall = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Designator l' l' f' f')
-> [f (Expression l' l' f' f')] -> Expression l l' f' f
functionCall @l
   literal :: forall (f :: * -> *) l' (f' :: * -> *).
f (Value l' l' f' f') -> Expression (WirthySubsetOf l) l' f' f
literal = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Value l' l' f' f') -> Expression l l' f' f
literal @l
   negative :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f') -> Expression (WirthySubsetOf l) l' f' f
negative = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f') -> Expression l l' f' f
negative @l
   positive :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f') -> Expression (WirthySubsetOf l) l' f' f
positive = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f') -> Expression l l' f' f
positive @l
   not :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f') -> Expression (WirthySubsetOf l) l' f' f
not = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f') -> Expression l l' f' f
not @l
   read :: forall (f :: * -> *) l' (f' :: * -> *).
f (Designator l' l' f' f') -> Expression (WirthySubsetOf l) l' f' f
read = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Designator l' l' f' f') -> Expression l l' f' f
read @l
   relation :: forall (f :: * -> *) l' (f' :: * -> *).
RelOp
-> f (Expression l' l' f' f')
-> f (Expression l' l' f' f')
-> Expression (WirthySubsetOf l) l' f' f
relation = ((forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
RelOp
-> f (Expression l' l' f' f')
-> f (Expression l' l' f' f')
-> Expression l l' f' f
relation @l

   element :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f') -> Element (WirthySubsetOf l) l' f' f
element = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f') -> Element l l' f' f
element @l
   range :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f')
-> f (Expression l' l' f' f') -> Element (WirthySubsetOf l) l' f' f
range = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Expression l' l' f' f')
-> f (Expression l' l' f' f') -> Element l l' f' f
range @l

   -- Value
   integer :: forall l' (f' :: * -> *) (f :: * -> *).
Integer -> Value (WirthySubsetOf l) l' f' f
integer = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l l' (f' :: * -> *) (f :: * -> *).
Wirthy l =>
Integer -> Value l l' f' f
integer @l
   nil :: forall l' (f' :: * -> *) (f :: * -> *).
Value (WirthySubsetOf l) l' f' f
nil = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 (forall l l' (f' :: * -> *) (f :: * -> *).
Wirthy l =>
Value l l' f' f
nil @l)
   false :: forall l' (f' :: * -> *) (f :: * -> *).
Value (WirthySubsetOf l) l' f' f
false = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 (forall l l' (f' :: * -> *) (f :: * -> *).
Wirthy l =>
Value l l' f' f
false @l)
   true :: forall l' (f' :: * -> *) (f :: * -> *).
Value (WirthySubsetOf l) l' f' f
true = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 (forall l l' (f' :: * -> *) (f :: * -> *).
Wirthy l =>
Value l l' f' f
true @l)
   real :: forall l' (f' :: * -> *) (f :: * -> *).
Double -> Value (WirthySubsetOf l) l' f' f
real = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l l' (f' :: * -> *) (f :: * -> *).
Wirthy l =>
Double -> Value l l' f' f
real @l
   string :: forall l' (f' :: * -> *) (f :: * -> *).
Ident -> Value (WirthySubsetOf l) l' f' f
string = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l l' (f' :: * -> *) (f :: * -> *).
Wirthy l =>
Ident -> Value l l' f' f
string @l
   charCode :: forall l' (f' :: * -> *) (f :: * -> *).
Int -> Value (WirthySubsetOf l) l' f' f
charCode = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l l' (f' :: * -> *) (f :: * -> *).
Wirthy l =>
Int -> Value l l' f' f
charCode @l
   builtin :: forall l' (f' :: * -> *) (f :: * -> *).
Ident -> Value (WirthySubsetOf l) l' f' f
builtin = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l l' (f' :: * -> *) (f :: * -> *).
Wirthy l =>
Ident -> Value l l' f' f
builtin @l

   -- Designator
   variable :: forall l' (f' :: * -> *) (f :: * -> *).
QualIdent l' -> Designator (WirthySubsetOf l) l' f' f
variable = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l l' (f' :: * -> *) (f :: * -> *).
Wirthy l =>
QualIdent l' -> Designator l l' f' f
variable @l
   field :: forall (f :: * -> *) l' (f' :: * -> *).
f (Designator l' l' f' f')
-> Ident -> Designator (WirthySubsetOf l) l' f' f
field = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Designator l' l' f' f') -> Ident -> Designator l l' f' f
field @l
   index :: forall (f :: * -> *) l' (f' :: * -> *).
f (Designator l' l' f' f')
-> NonEmpty (f (Expression l' l' f' f'))
-> Designator (WirthySubsetOf l) l' f' f
index = (forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Designator l' l' f' f')
-> NonEmpty (f (Expression l' l' f' f')) -> Designator l l' f' f
index @l
   dereference :: forall (f :: * -> *) l' (f' :: * -> *).
f (Designator l' l' f' f') -> Designator (WirthySubsetOf l) l' f' f
dereference = forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
f a b c -> Maybe3 f a b c
just3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l (f :: * -> *) l' (f' :: * -> *).
Wirthy l =>
f (Designator l' l' f' f') -> Designator l l' f' f
dereference @l

   -- Identifier
   identDef :: Ident -> IdentDef (WirthySubsetOf l)
identDef = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l. Wirthy l => Ident -> IdentDef l
identDef @l
   nonQualIdent :: Ident -> QualIdent (WirthySubsetOf l)
nonQualIdent = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l. Wirthy l => Ident -> QualIdent l
nonQualIdent @l

-- | Ability to deconstruct named constructs and obtain their 'Ident'.
class Wirthy l => Nameable l where
   getProcedureName :: Nameable l' => ProcedureHeading l l' f' f -> Ident
   getIdentDefName :: IdentDef l -> Ident
   getNonQualIdentName :: QualIdent l -> Maybe Ident

-- | The finally-tagless associated types and methods relevant to both versions of the Oberon language.
class Wirthy l => Oberon l where
   type WithAlternative l = (x :: * -> (* -> *) -> (* -> *) -> *) | x -> l

   moduleUnit :: Ident -> [Import l] -> f (Block l' l' f' f') -> Module l l' f' f
   moduleImport :: Maybe Ident -> Ident -> Import l
   qualIdent :: Ident -> Ident -> QualIdent l
   getQualIdentNames :: QualIdent l -> Maybe (Ident, Ident)
   exported :: Ident -> IdentDef l

   forwardDeclaration :: IdentDef l' -> Maybe (f (FormalParameters l' l' f' f')) -> Declaration l l' f' f
   procedureHeading :: Bool -> IdentDef l' -> Maybe (f (FormalParameters l' l' f' f')) -> ProcedureHeading l l' f' f

   arrayType :: [f (ConstExpression l' l' f' f')] -> f (Type l' l' f' f') -> Type l l' f' f
   recordType :: Maybe (BaseType l') -> [f (FieldList l' l' f' f')] -> Type l l' f' f

   withStatement :: f (WithAlternative l' l' f' f') -> Statement l l' f' f
   withAlternative :: QualIdent l' -> QualIdent l' -> f (StatementSequence l' l' f' f') -> WithAlternative l l' f' f

   is :: f (Expression l' l' f' f') -> QualIdent l' -> Expression l l' f' f
   set :: [f (Element l' l' f' f')] -> Expression l l' f' f

   typeGuard :: f (Designator l' l' f' f') -> QualIdent l' -> Designator l l' f' f

instance Wirthy l => Oberon (WirthySubsetOf l) where
   type WithAlternative (WirthySubsetOf l) = Maybe3 (WithAlternative l)
   moduleUnit :: forall (f :: * -> *) l' (f' :: * -> *).
Ident
-> [Import (WirthySubsetOf l)]
-> f (Block l' l' f' f')
-> Module (WirthySubsetOf l) l' f' f
moduleUnit = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Maybe3 f a b c
nothing3
   moduleImport :: Maybe Ident -> Ident -> Import (WirthySubsetOf l)
moduleImport = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a. Maybe a
Nothing
   qualIdent :: Ident -> Ident -> QualIdent (WirthySubsetOf l)
qualIdent = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a. Maybe a
Nothing
   getQualIdentNames :: QualIdent (WirthySubsetOf l) -> Maybe (Ident, Ident)
getQualIdentNames = forall a b. a -> b -> a
const forall a. Maybe a
Nothing
   exported :: Ident -> IdentDef (WirthySubsetOf l)
exported = forall a b. a -> b -> a
const forall a. Maybe a
Nothing

   forwardDeclaration :: forall l' (f :: * -> *) (f' :: * -> *).
IdentDef l'
-> Maybe (f (FormalParameters l' l' f' f'))
-> Declaration (WirthySubsetOf l) l' f' f
forwardDeclaration = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Maybe3 f a b c
nothing3
   procedureHeading :: forall l' (f :: * -> *) (f' :: * -> *).
Bool
-> IdentDef l'
-> Maybe (f (FormalParameters l' l' f' f'))
-> ProcedureHeading (WirthySubsetOf l) l' f' f
procedureHeading = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Maybe3 f a b c
nothing3

   arrayType :: forall (f :: * -> *) l' (f' :: * -> *).
[f (ConstExpression l' l' f' f')]
-> f (Type l' l' f' f') -> Type (WirthySubsetOf l) l' f' f
arrayType = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Maybe3 f a b c
nothing3
   recordType :: forall l' (f :: * -> *) (f' :: * -> *).
Maybe (BaseType l')
-> [f (FieldList l' l' f' f')] -> Type (WirthySubsetOf l) l' f' f
recordType = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Maybe3 f a b c
nothing3

   withStatement :: forall (f :: * -> *) l' (f' :: * -> *).
f (WithAlternative l' l' f' f')
-> Statement (WirthySubsetOf l) l' f' f
withStatement = forall a b. a -> b -> a
const forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Maybe3 f a b c
nothing3
   withAlternative :: forall l' (f :: * -> *) (f' :: * -> *).
QualIdent l'
-> QualIdent l'
-> f (StatementSequence l' l' f' f')
-> WithAlternative (WirthySubsetOf l) l' f' f
withAlternative = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Maybe3 f a b c
nothing3

   is :: forall (f :: * -> *) l' (f' :: * -> *).
f (Expression l' l' f' f')
-> QualIdent l' -> Expression (WirthySubsetOf l) l' f' f
is = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Maybe3 f a b c
nothing3
   set :: forall (f :: * -> *) l' (f' :: * -> *).
[f (Element l' l' f' f')] -> Expression (WirthySubsetOf l) l' f' f
set = forall a b. a -> b -> a
const forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Maybe3 f a b c
nothing3

   typeGuard :: forall (f :: * -> *) l' (f' :: * -> *).
f (Designator l' l' f' f')
-> QualIdent l' -> Designator (WirthySubsetOf l) l' f' f
typeGuard = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Maybe3 f a b c
nothing3

-- | The finally-tagless associated types and methods relevant to the Oberon 2 language.
class Oberon l => Oberon2 l where
   readOnly :: Ident -> IdentDef l
   typeBoundHeading :: Bool -> Ident -> Ident -> Bool -> IdentDef l' -> Maybe (f (FormalParameters l' l' f' f'))
                    -> ProcedureHeading l l' f' f
   forStatement :: Ident -> f (Expression l' l' f' f') -> f (Expression l' l' f' f')
                -> Maybe (f (Expression l' l' f' f'))
                -> f (StatementSequence l' l' f' f') 
                -> Statement l l' f' f
   variantWithStatement :: NonEmpty (f (WithAlternative l' l' f' f')) -> Maybe (f (StatementSequence l' l' f' f'))
                        -> Statement l l' f' f

instance Wirthy l => Oberon2 (WirthySubsetOf l) where
   readOnly :: Ident -> IdentDef (WirthySubsetOf l)
readOnly = forall a b. a -> b -> a
const forall a. Maybe a
Nothing
   typeBoundHeading :: forall l' (f :: * -> *) (f' :: * -> *).
Bool
-> Ident
-> Ident
-> Bool
-> IdentDef l'
-> Maybe (f (FormalParameters l' l' f' f'))
-> ProcedureHeading (WirthySubsetOf l) l' f' f
typeBoundHeading = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Maybe3 f a b c
nothing3
   forStatement :: forall (f :: * -> *) l' (f' :: * -> *).
Ident
-> f (Expression l' l' f' f')
-> f (Expression l' l' f' f')
-> Maybe (f (Expression l' l' f' f'))
-> f (StatementSequence l' l' f' f')
-> Statement (WirthySubsetOf l) l' f' f
forStatement = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Maybe3 f a b c
nothing3
   variantWithStatement :: forall (f :: * -> *) l' (f' :: * -> *).
NonEmpty (f (WithAlternative l' l' f' f'))
-> Maybe (f (StatementSequence l' l' f' f'))
-> Statement (WirthySubsetOf l) l' f' f
variantWithStatement = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall {k} {k} {k} {f :: k -> k -> k -> *} {a :: k} {b :: k}
       {c :: k}.
Maybe3 f a b c
nothing3

type BaseType l = QualIdent l
type ReturnType l = QualIdent l
type ConstExpression l = Expression l
type IdentList l = NonEmpty (IdentDef l)