Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- data EconSection
- = EconGeneral
- | EconProduction
- data EconPhase
- = Oil
- | Water
- | NumPhase Nat
- data ContState
- = ContNone
- | ContProd EconPhase
- data Keyword : EconSection -> ContState -> ContState -> Type where
- Prod : (p : EconPhase) -> Keyword EconProduction c (ContProd p)
- Continue : Keyword s c c
- data Expression : (s : EconSection) ->
- (d : ContState) ->
- Keyword s c d ->
- Type where
- ExProc : Double -> Double -> Expression EconProduction (ContProd p) k
- data Line : EconSection -> ContState -> ContState -> Type where
- L : (k : Keyword s c d) -> Expression s d k -> Line s c d
- data Lines : EconSection -> ContState -> Type where
- First : Line s ContNone d -> Lines s d
- Then : Lines s c -> Line s c d -> Lines s d
- infixl 0 `Then`
- good : Lines EconProduction (ContProd (NumPhase 1))
- good = First (L (Prod Oil) (ExProc 23.2 70.1))
- `Then` (L (Continue) (ExProc 27.9 1.2))
- `Then` (L (Prod (NumPhase 1)) (ExProc 91.2 7014.1))
- `Then` (L (Continue) (ExProc 91.2 7014.1))
- {-# LANGUAGE GADTs, KindSignatures, DataKinds #-}
- {-# LANGUAGE RankNTypes, TypeInType, TypeOperators #-}
- {-# LANGUAGE TypeFamilies, TypeFamilyDependencies, MultiParamTypeClasses #-}
- import Data.Kind (Type)
- data Nat
- = Z
- | S Nat
- data SNat :: Nat -> Type where
- SZ :: SNat 'Z
- SS :: SNat n -> SNat ('S n)
- data SSNat :: forall (n :: Nat) . SNat n -> Type where
- SSZ :: SSNat 'SZ
- SSS :: SSNat n -> SSNat ('SS n)
- type family SingNat (n :: Nat) :: SNat n where
- SingNat 'Z = 'SZ
- SingNat ('S n) = 'SS (SingNat n)
- data EconSection
- = EconGeneral
- | EconProduction
- data SEconSection :: EconSection -> Type where
- SEconGeneral :: SEconSection 'EconGeneral
- SEconProduction :: SEconSection 'EconProduction
- type family SingSection (s :: EconSection) :: SEconSection s where
- SingSection 'EconGeneral = 'SEconGeneral
- SingSection 'EconProduction = 'SEconProduction
- data EconPhase
- = Oil
- | Water
- | NumPhase Nat
- data SEconPhase :: EconPhase -> Type where
- SOil :: SEconPhase 'Oil
- SWater :: SEconPhase 'Water
- SNumPhase :: SNat n -> SEconPhase ('NumPhase n)
- data SSEconPhase :: forall (p :: EconPhase) . SEconPhase p -> Type where
- SSOil :: SSEconPhase 'SOil
- SSWater :: SSEconPhase 'SWater
- SSNumPhase :: SSNat n -> SSEconPhase ('SNumPhase n)
- type family SingEconPhase (p :: EconPhase) :: SEconPhase p where
- SingEconPhase 'Oil = 'SOil
- SingEconPhase 'Water = 'SWater
- SingEconPhase ('NumPhase n) = 'SNumPhase (SingNat n)
- data ContState
- = ContNone
- | ContProd EconPhase
- data SContState :: ContState -> Type where
- SContNone :: SContState 'ContNone
- SContProd :: SEconPhase p -> SContState ('ContProd p)
- type family SingContState (c :: ContState) :: SContState c where
- SingContState 'ContNone = 'SContNone
- SingContState (ContProd p) = 'SContProd (SingEconPhase p)
- data Keyword :: EconSection -> ContState -> ContState -> Type where
- Prod :: SEconPhase p -> Keyword 'EconProduction c ('ContProd p)
- Continue :: Keyword s c c
- data SKeyword :: forall (s :: EconSection) (c :: ContState) (d :: ContState) .
- Keyword s c d -> Type where
- SProd :: SSEconPhase p -> SKeyword ('Prod p)
- SContinue :: SKeyword 'Continue
- data Expression :: forall (s :: EconSection) (c :: ContState) (d :: ContState) .
- SEconSection s -> SContState d -> Keyword s c d -> Type where
- ExProc :: Double -> Double -> Expression SEconProduction (SContProd p) k
- type family KWSection k where
- KWSection (Keyword s _ _) = s
- type family KWFrom k where
- KWFrom (Keyword _ c _) = c
- type family KWTo k where
- KWTo (Keyword _ _ d) = d
- data Line :: EconSection -> ContState -> ContState -> Type where
- L :: SKeyword (k :: Keyword s c d)
- -> Expression (SingSection s) (SingContState d) k
- -> Line s c d
- data Lines :: EconSection -> ContState -> Type where
- First :: Line s 'ContNone d -> Lines s d
- Then :: Lines s c -> Line s c d -> Lines s d
- infixl 0 `Then`
- good :: Lines 'EconProduction ('ContProd ('NumPhase ('S 'Z)))
- good = First (L (SProd SSOil) (ExProc 23.2 70.1))
- `Then` (L (SContinue) (ExProc 27.9 1.2))
- `Then` (L (SProd (SSNumPhase (SSS SSZ))) (ExProc 91.2 7014.1))
- `Then` (L (SContinue) (ExProc 91.2 7014.1))
Add Comment
Please, Sign In to add comment