{-# LANGUAGE FlexibleInstances
, GADTs
, DataKinds
, TypeOperators
, ViewPatterns
, KindSignatures
, RankNTypes
, UndecidableInstances
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Syntax.Command where
import Language.Hakaru.Types.Sing
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Syntax.ABT
import Language.Hakaru.Syntax.AST
import Language.Hakaru.Syntax.IClasses
import GHC.TypeLits (Symbol)
import Data.List (isInfixOf)
import Data.Char (toLower)
import Data.Function (on)
data CommandType (c :: Symbol) (i :: Hakaru) (o :: Hakaru) where
Simplify :: CommandType "Simplify" a a
DisintMeas :: CommandType "Disintegrate" (HMeasure (HPair a b)) (a :-> HMeasure b)
DisintFun :: !(CommandType "Disintegrate" x x')
-> CommandType "Disintegrate" (a :-> x) (a :-> x')
Summarize :: CommandType "Summarize" a a
commandIsType :: CommandType c i o -> Sing i -> Sing o
commandIsType DisintMeas (SMeasure (sUnPair->(a,b))) = SFun a (SMeasure b)
commandIsType (DisintFun t) (SFun a x) = SFun a (commandIsType t x)
commandIsType Simplify x = x
commandIsType Summarize x = x
nameOfCommand :: CommandType c i o -> Sing c
nameOfCommand Simplify{} = sing
nameOfCommand Summarize{} = sing
nameOfCommand DisintMeas{} = sing
nameOfCommand DisintFun{} = sing
parseCommand = flip (isInfixOf `on` map toLower)
commandFromName
:: String
-> Sing i
-> (forall o c . Either Bool (CommandType c i o, Sing o) -> k)
-> k
commandFromName (parseCommand "Simplify"->True) i k = k $ Right (Simplify, i)
commandFromName (parseCommand "Disintegrate"->True) i k =
let disint_commandFromType
:: Sing i
-> (forall o . Either Bool (CommandType "Disintegrate" i o, Sing o) -> k)
-> k
disint_commandFromType i k =
case i of
SMeasure (SData (STyApp (STyApp (STyCon (jmEq1 sSymbol_Pair -> Just Refl)) a) b) _) ->
k $ Right (DisintMeas, SFun a (SMeasure b))
SFun a x ->
disint_commandFromType x $ \q ->
k $ fmap (\(c,x') -> (DisintFun c, SFun a x')) q
_ -> k $ Left True
in disint_commandFromType i k
commandFromName (parseCommand "Summarize"->True) i k = k $ Right (Summarize, i)
commandFromName _ _ k = k $ Left False