( Eq_Type (Type_Root_of_Expr root)
, Type_from AST (Type_Root_of_Expr root)
, Expr_from AST root
- , String_from_Type (Type_Root_of_Expr root)
- -- , Lift_Type Type_Var1 (Type_of_Expr root)
, Lift_Type (Type_Fun lam) (Type_of_Expr root)
, Unlift_Type (Type_Fun lam) (Type_of_Expr root)
, Unlift_Type1 (Type_of_Expr root)
( Eq_Type (Type_Root_of_Expr root)
, Type1_from AST (Type_Root_of_Expr root)
, Expr_from AST root
- , String_from_Type (Type_Root_of_Expr root)
- -- , Lift_Type Type_Var1 (Type_of_Expr root)
, Lift_Type (Type_Fun lam) (Type_of_Expr root)
, Unlift_Type (Type_Fun lam) (Type_of_Expr root)
, Eq_Type1 (Type_Root_of_Expr root)
AST "pure" asts -> from_ast2 asts pure_from ex ast ctx k
AST "<*>" asts -> from_ast2 asts ltstargt_from ex ast ctx k
_ -> Left $ error_expr_unsupported ex ast
+instance -- Expr_from AST Expr_Traversable
+ ( Eq_Type (Type_Root_of_Expr root)
+ , Type1_from AST (Type_Root_of_Expr root)
+ , Expr_from AST root
+ , Lift_Type (Type_Fun lam) (Type_of_Expr root)
+ , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
+ , Eq_Type1 (Type_Root_of_Expr root)
+ , Unlift_Type1 (Type_of_Expr root)
+ , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
+ , Constraint_Type1 Applicative (Type_Root_of_Expr root)
+ , Constraint_Type1 Traversable (Type_Root_of_Expr root)
+ , Root_of_Expr root ~ root
+ , IBool (Is_Last_Expr (Expr_Traversable lam root) root)
+ ) => Expr_from AST (Expr_Traversable lam root) where
+ expr_from ex ast ctx k =
+ case ast of
+ AST "traverse" asts -> from_ast2 asts traverse_from ex ast ctx k
+ _ -> Left $ error_expr_unsupported ex ast
( module Language.Symantic.Expr.Alt
, module Language.Symantic.Expr.Applicative
, module Language.Symantic.Expr.Bool
+ , module Language.Symantic.Expr.Either
, module Language.Symantic.Expr.Eq
, module Language.Symantic.Expr.Error
, module Language.Symantic.Expr.From
, module Language.Symantic.Expr.List
, module Language.Symantic.Expr.Map
, module Language.Symantic.Expr.Maybe
+ , module Language.Symantic.Expr.Monad
, module Language.Symantic.Expr.Ord
, module Language.Symantic.Expr.Root
+ , module Language.Symantic.Expr.Traversable
, module Language.Symantic.Expr.Tuple
) where
import Language.Symantic.Expr.Alt
import Language.Symantic.Expr.Applicative
import Language.Symantic.Expr.Bool
+import Language.Symantic.Expr.Either
import Language.Symantic.Expr.Eq
import Language.Symantic.Expr.Error
import Language.Symantic.Expr.From
import Language.Symantic.Expr.List
import Language.Symantic.Expr.Map
import Language.Symantic.Expr.Maybe
+import Language.Symantic.Expr.Monad
import Language.Symantic.Expr.Ord
import Language.Symantic.Expr.Root
+import Language.Symantic.Expr.Traversable
import Language.Symantic.Expr.Tuple
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Expression for 'Applicative'.
module Language.Symantic.Expr.Applicative where
import Control.Applicative (Applicative)
+-- import qualified Control.Applicative as Applicative
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
-import Prelude hiding (Applicative(..))
+import Prelude hiding ((<$>), Applicative(..))
import Language.Symantic.Type
import Language.Symantic.Trans.Common
-- * Class 'Sym_Applicative'
-- | Symantic.
-class Sym_Applicative repr where
- pure :: Applicative f => repr a -> repr (f a)
- -- (*>) :: Applicative f => repr (f a) -> repr (f b) -> repr (f b)
- -- (<*) :: Applicative f => repr (f a) -> repr (f b) -> repr (f a)
+class
+ ( Sym_Applicative_Lam (Lambda_from_Repr repr) repr
+ -- , Applicative (Lambda_from_Repr repr)
+ -- , Applicative repr
+ ) => Sym_Applicative repr where
+ pure :: Applicative f => repr a -> repr (f a)
default pure :: (Trans t repr, Applicative f) => t repr a -> t repr (f a)
pure = trans_map1 pure
+ {-
+ (*>) :: Applicative f => repr (f a) -> repr (f b) -> repr (f b)
+ (<*) :: Applicative f => repr (f a) -> repr (f b) -> repr (f a)
+ (*>) fa = (g <$> fa <*>)
+ where
+ g :: repr (Lambda (Lambda_from_Repr repr) a (Lambda (Lambda_from_Repr repr) b b))
+ g = Applicative.pure $ Lambda $ const $ Applicative.pure $ Lambda id
+ (<*) fa = (g <$> fa <*>)
+ where
+ g :: repr (Lambda (Lambda_from_Repr repr) a (Lambda (Lambda_from_Repr repr) b a))
+ g = Applicative.pure $ Lambda $ \a -> Applicative.pure $ Lambda (const a)
+infixl 4 *>
+infixl 4 <*
+-}
-- * Class 'Sym_Applicative_Lam'
-- | Symantic requiring a 'Lambda'.
class Sym_Functor lam repr => Sym_Applicative_Lam lam repr where
(<*>) :: Applicative f => repr (f (Lambda lam a b)) -> repr (f a) -> repr (f b)
- -- (*>) :: Applicative f => repr (f a) -> repr (f b) -> repr (f b)
- -- (<*) :: Applicative f => repr (f a) -> repr (f b) -> repr (f a)
-
- default (<*>) :: (Trans t repr, Applicative f) => t repr (f (Lambda lam a b)) -> t repr (f a) -> t repr (f b)
- -- default (*>) :: (Trans t, Applicative f) => t repr (f a) -> t repr (f b) -> t repr (f b)
- -- default (<*) :: (Trans t, Applicative f) => t repr (f a) -> t repr (f b) -> t repr (f a)
+ default (<*>) :: (Trans t repr, Applicative f)
+ => t repr (f (Lambda lam a b)) -> t repr (f a) -> t repr (f b)
(<*>) = trans_map2 (<*>)
infixl 4 <*>
ltstargt_from
:: forall root ty lam ast hs ret.
( ty ~ Type_Root_of_Expr (Expr_Applicative lam root)
- , String_from_Type ty
, Eq_Type (Type_Root_of_Expr root)
, Eq_Type1 (Type_Root_of_Expr root)
, Expr_from ast root
import Test.Tasty
import Test.Tasty.HUnit
-import Control.Arrow (left)
+import qualified Control.Arrow as Arrow
+import qualified Control.Monad as Monad
import Data.Functor.Identity
import Data.Proxy (Proxy(..))
import Data.Text (Text)
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `left` expected
+ Left err -> Left err @?= snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
Right (ty_expected::Type_Root_of_Expr (Ex Identity) h, _::h, _::Text) ->
- (>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
+ (Monad.>>= (@?= (\(_::Proxy h, err) -> err) `Arrow.left` expected)) $
case ty `eq_type` ty_expected of
- Nothing -> return $ Left $
+ Nothing -> Monad.return $ Left $
error_expr (Proxy::Proxy (Ex Identity)) $
Error_Expr_Type_mismatch ast
(Exists_Type ty)
(Exists_Type ty_expected)
Just Refl -> do
let h = runIdentity $ host_from_expr r
- return $
+ Monad.return $
Right
( ty
, h
, text_from_expr r
- -- , (text_from_expr :: Repr_String Identity h -> Text) r
+ -- , (text_from_expr :: Repr_Text Identity h -> Text) r
)
tests :: TestTree
import Test.Tasty
import Test.Tasty.HUnit
-import Control.Arrow (left)
--- import Data.Functor.Identity (Identity)
+import qualified Control.Arrow as Arrow
+import qualified Control.Monad as Monad
+import Data.Functor.Identity
-- import Control.Monad.IO.Class (MonadIO(..))
import Data.Proxy (Proxy(..))
import Data.Text (Text)
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `left` expected
+ Left err -> Left err @?= snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
- Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
- (>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
+ Right (ty_expected::Type_Root_of_Expr (Ex Identity) h, _::h, _::Text) ->
+ (Monad.>>= (@?= (\(_::Proxy h, err) -> err) `Arrow.left` expected)) $
case ty `eq_type` ty_expected of
- Nothing -> return $ Left $
- error_expr (Proxy::Proxy (Ex IO)) $
+ Nothing -> Monad.return $ Left $
+ error_expr (Proxy::Proxy (Ex Identity)) $
Error_Expr_Type_mismatch ast
(Exists_Type ty)
(Exists_Type ty_expected)
Just Refl -> do
- h <- host_from_expr r
- return $
+ let h = runIdentity $ host_from_expr r
+ Monad.return $
Right
( ty
, h
, text_from_expr r
- -- , (text_from_expr :: Repr_Text IO h -> String) r
+ -- , (text_from_expr :: Repr_Text Identity h -> Text) r
)
tests :: TestTree
Error_Expr_Alt_Curr $
Error_Expr_Type_mismatch ast
(Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
- ::Type_Root (Type_Var0 :|: Type_Var1 :|: Type_Fun IO :|: Type_Bool)
- (Lambda IO Var0 Var0)))
+ ::Type_Root (Type_Var0 :|: Type_Var1 :|: Type_Fun Identity :|: Type_Bool)
+ (Lambda Identity Var0 Var0)))
(Exists_Type type_bool))
, AST "app"
[ AST "val"
--- /dev/null
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-- | Expression for 'Either'.
+module Language.Symantic.Expr.Either where
+
+import Data.Proxy (Proxy(..))
+import Prelude hiding (maybe)
+
+import Language.Symantic.Type
+import Language.Symantic.Trans.Common
+import Language.Symantic.Expr.Root
+import Language.Symantic.Expr.Error
+import Language.Symantic.Expr.From
+
+-- * Class 'Sym_Tuple_Lam'
+-- | Symantic.
+class Sym_Either repr where
+ left :: repr l -> repr (Either l r)
+ right :: repr r -> repr (Either l r)
+ default left :: Trans t repr => t repr l -> t repr (Either l r)
+ default right :: Trans t repr => t repr r -> t repr (Either l r)
+ left = trans_map1 left
+ right = trans_map1 right
+
+-- * Type 'Expr_Either'
+-- | Expression.
+data Expr_Either (lam:: * -> *) (root:: *)
+type instance Root_of_Expr (Expr_Either lam root) = root
+type instance Type_of_Expr (Expr_Either lam root) = Type_Either
+type instance Sym_of_Expr (Expr_Either lam root) repr = (Sym_Either repr)
+type instance Error_of_Expr ast (Expr_Either lam root) = No_Error_Expr
+
+instance Constraint_Type1 Functor (Type_Type1 (Proxy (Either l)) root) where
+ constraint_type1 _c Type_Type1{} = Just Dict
+instance Constraint_Type1 Functor (Type_Either root) where
+ constraint_type1 _c Type_Type2{} = Just Dict
+instance Constraint_Type1 Applicative (Type_Type1 (Proxy (Either l)) root)
+
+-- | Parsing utility to check that the given type is a 'Type_Either'
+-- or raise 'Error_Expr_Type_mismatch'.
+check_type_either
+ :: forall ast ex root ty h ret.
+ ( root ~ Root_of_Expr ex
+ , ty ~ Type_Root_of_Expr ex
+ , Lift_Type Type_Either (Type_of_Expr root)
+ , Unlift_Type Type_Either (Type_of_Expr root)
+ , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ )
+ => Proxy ex -> ast -> ty h
+ -> (Type_Either ty h -> Either (Error_of_Expr ast root) ret)
+ -> Either (Error_of_Expr ast root) ret
+check_type_either ex ast ty k =
+ case unlift_type $ unType_Root ty of
+ Just ty_e -> k ty_e
+ Nothing -> Left $
+ error_expr ex $
+ Error_Expr_Type_mismatch ast
+ (Exists_Type (type_either (type_var0 SZero) (type_var0 $ SSucc SZero)
+ :: Type_Root_of_Expr ex (Either Var0 Var0)))
+ (Exists_Type ty)
+
+-- | Parse 'left'.
+left_from
+ :: forall root lam ty ty_root ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Either lam root)
+ , ty_root ~ Type_Root_of_Expr root
+ , Type_from ast ty_root
+ , Eq_Type (Type_Root_of_Expr root)
+ , Expr_from ast root
+ , Lift_Type Type_Either (Type_of_Expr root)
+ , Unlift_Type Type_Either (Type_of_Expr root)
+ , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Root_of_Expr root ~ root
+ ) => ast -> ast
+ -> Expr_From ast (Expr_Either lam root) hs ret
+left_from ast_l ast_ty_r ex ast ctx k =
+ expr_from (Proxy::Proxy root) ast_l ctx $
+ \(ty_l::Type_Root_of_Expr root h_l) (Forall_Repr_with_Context l) ->
+ either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
+ type_from (Proxy::Proxy ty_root) ast_ty_r $ \ty_r -> Right $
+ k (type_either ty_l ty_r) $ Forall_Repr_with_Context $
+ \c -> left (l c)
+
+-- | Parse 'right'.
+right_from
+ :: forall root lam ty ty_root ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Either lam root)
+ , ty_root ~ Type_Root_of_Expr root
+ , Type_from ast ty_root
+ , Eq_Type (Type_Root_of_Expr root)
+ , Expr_from ast root
+ , Lift_Type Type_Either (Type_of_Expr root)
+ , Unlift_Type Type_Either (Type_of_Expr root)
+ , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Root_of_Expr root ~ root
+ ) => ast -> ast
+ -> Expr_From ast (Expr_Either lam root) hs ret
+right_from ast_r ast_ty_l ex ast ctx k =
+ expr_from (Proxy::Proxy root) ast_r ctx $
+ \(ty_r::Type_Root_of_Expr root h_r) (Forall_Repr_with_Context r) ->
+ either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
+ type_from (Proxy::Proxy ty_root) ast_ty_l $ \ty_l -> Right $
+ k (type_either ty_l ty_r) $ Forall_Repr_with_Context $
+ \c -> right (r c)
import Test.Tasty
import Test.Tasty.HUnit
-import Control.Arrow (left)
+import qualified Control.Arrow as Arrow
+import qualified Control.Monad as Monad
+import Data.Functor.Identity
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `left` expected
+ Left err -> Left err @?= snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
- Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
- (>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
+ Right (ty_expected::Type_Root_of_Expr (Ex Identity) h, _::h, _::Text) ->
+ (Monad.>>= (@?= (\(_::Proxy h, err) -> err) `Arrow.left` expected)) $
case ty `eq_type` ty_expected of
- Nothing -> return $ Left $
- error_expr (Proxy::Proxy (Ex IO)) $
+ Nothing -> Monad.return $ Left $
+ error_expr (Proxy::Proxy (Ex Identity)) $
Error_Expr_Type_mismatch ast
(Exists_Type ty)
(Exists_Type ty_expected)
Just Refl -> do
- h <- host_from_expr r
- return $
+ let h = runIdentity $ host_from_expr r
+ Monad.return $
Right
( ty
, h
, text_from_expr r
- -- , (text_from_expr :: Repr_String IO h -> Text) r
+ -- , (text_from_expr :: Repr_Text Identity h -> Text) r
)
tests :: TestTree
( root ~ Root_of_Expr ex
, ty ~ Type_Root_of_Expr ex
, Unlift_Type1 (Type_of_Expr root)
- , String_from_Type ty
, Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
(Error_of_Expr ast root)
)
fmap_from
:: forall root ty lam ast hs ret.
( ty ~ Type_Root_of_Expr (Expr_Functor lam root)
- , String_from_Type ty
, Eq_Type (Type_Root_of_Expr root)
, Expr_from ast root
, Lift_Type (Type_Fun lam) (Type_of_Expr root)
import Test.Tasty
import Test.Tasty.HUnit
-import Control.Arrow (left)
+import qualified Control.Arrow as Arrow
+import qualified Control.Monad as Monad
import Data.Functor.Identity
import Data.Proxy (Proxy(..))
import Data.Text (Text)
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `left` expected
+ Left err -> Left err @?= snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
Right (ty_expected::Type_Root_of_Expr (Ex Identity) h, _::h, _::Text) ->
- (>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
+ (Monad.>>= (@?= (\(_::Proxy h, err) -> err) `Arrow.left` expected)) $
case ty `eq_type` ty_expected of
- Nothing -> return $ Left $
+ Nothing -> Monad.return $ Left $
error_expr (Proxy::Proxy (Ex Identity)) $
Error_Expr_Type_mismatch ast
(Exists_Type ty)
(Exists_Type ty_expected)
Just Refl -> do
let h = runIdentity $ host_from_expr r
- return $
+ Monad.return $
Right
( ty
, h
, text_from_expr r
- -- , (text_from_expr :: Repr_String Identity h -> Text) r
+ -- , (text_from_expr :: Repr_Text Identity h -> Text) r
)
tests :: TestTree
import Test.Tasty
import Test.Tasty.HUnit
-import Control.Arrow (left)
+import qualified Control.Arrow as Arrow
+import qualified Control.Monad as Monad
+import Data.Functor.Identity
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
-import Prelude hiding (maybe, not, (&&))
+import Prelude hiding (maybe, not, (&&), Monad(..))
import Language.Symantic.Repr
import Language.Symantic.Expr
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `left` expected
+ Left err -> Left err @?= snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
- Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
- (>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
+ Right (ty_expected::Type_Root_of_Expr (Ex Identity) h, _::h, _::Text) ->
+ (Monad.>>= (@?= (\(_::Proxy h, err) -> err) `Arrow.left` expected)) $
case ty `eq_type` ty_expected of
- Nothing -> return $ Left $
- error_expr (Proxy::Proxy (Ex IO)) $
+ Nothing -> Monad.return $ Left $
+ error_expr (Proxy::Proxy (Ex Identity)) $
Error_Expr_Type_mismatch ast
(Exists_Type ty)
(Exists_Type ty_expected)
Just Refl -> do
- h <- host_from_expr r
- return $
+ let h = runIdentity $ host_from_expr r
+ Monad.return $
Right
( ty
, h
, text_from_expr r
- -- , (text_from_expr :: Repr_String IO h -> String) r
+ -- , (text_from_expr :: Repr_Text Identity h -> Text) r
)
tests :: TestTree
import Test.Tasty
import Test.Tasty.HUnit
-import Control.Arrow (left)
--- import Data.Functor.Identity (Identity)
+import qualified Control.Arrow as Arrow
+import qualified Control.Monad as Monad
+import Data.Functor.Identity
-- import Control.Monad.IO.Class (MonadIO(..))
import Data.Proxy (Proxy(..))
import Data.Text (Text)
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `left` expected
+ Left err -> Left err @?= snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
- Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
- (>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
+ Right (ty_expected::Type_Root_of_Expr (Ex Identity) h, _::h, _::Text) ->
+ (Monad.>>= (@?= (\(_::Proxy h, err) -> err) `Arrow.left` expected)) $
case ty `eq_type` ty_expected of
- Nothing -> return $ Left $
- error_expr (Proxy::Proxy (Ex IO)) $
+ Nothing -> Monad.return $ Left $
+ error_expr (Proxy::Proxy (Ex Identity)) $
Error_Expr_Type_mismatch ast
(Exists_Type ty)
(Exists_Type ty_expected)
Just Refl -> do
- h <- host_from_expr r
- return $
+ let h = runIdentity $ host_from_expr r
+ Monad.return $
Right
( ty
, h
, text_from_expr r
- -- , (text_from_expr :: Repr_Text IO h -> String) r
+ -- , (text_from_expr :: Repr_Text Identity h -> Text) r
)
tests :: TestTree
Error_Expr_Alt_Curr $
Error_Expr_Type_mismatch ast
(Exists_Type (type_var0 SZero `type_fun` type_var0 (SSucc SZero)
- ::Type_Root (Type_Var0 :|: Type_Var1 :|: Type_Fun IO :|: Type_Int)
- (Lambda IO Var0 Var0)))
+ ::Type_Root (Type_Var0 :|: Type_Var1 :|: Type_Fun Identity :|: Type_Int)
+ (Lambda Identity Var0 Var0)))
(Exists_Type type_int))
, AST "app"
[ AST "val"
--
-- Basically this means having sometimes to add a type annotation
-- to the interpreter call to specify @lam@.
+--
+-- FIXME: 'lazy' requires @lam@ to contain 'IO',
+-- which is not escapable (there is no safe function: @IO a -> a@),
+-- this is problematic when writing 'Repr_Host' instances
+-- where 'app'lying an object-function on the elements of a 'Functor'
+-- return a value wrapped inside @lam@, which is then not unwrappable
+-- as needed to write the instance.
+-- I think the way to solve this is to require all object-values
+-- to be wrapped inside @lam@.
type family Lambda_from_Repr (repr:: * -> *) :: {-lam-}(* -> *)
-- * Class 'Sym_Lambda_App'
type instance Error_of_Expr ast (Expr_List lam root) = No_Error_Expr
instance Constraint_Type1 Functor (Type_List root) where
- constraint_type1 _c (Type_Type1 _ _) = Just Dict
+ constraint_type1 _c Type_Type1{} = Just Dict
instance Constraint_Type1 Applicative (Type_List root) where
- constraint_type1 _c (Type_Type1 _ _) = Just Dict
+ constraint_type1 _c Type_Type1{} = Just Dict
+instance Constraint_Type1 Traversable (Type_List root) where
+ constraint_type1 _c Type_Type1{} = Just Dict
-- | Parsing utility to check that the given type is a 'Type_List'
-- or raise 'Error_Expr_Type_mismatch'.
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Expression for 'Map'.
module Language.Symantic.Expr.Map where
type instance Type_of_Expr (Expr_Map lam root) = Type_Map
type instance Sym_of_Expr (Expr_Map lam root) repr = (Sym_Map repr, Sym_Map_Lam lam repr)
type instance Error_of_Expr ast (Expr_Map lam root) = No_Error_Expr
+
+instance Constraint_Type1 Functor (Type_Map root) where
+ constraint_type1 _c Type_Type2{} = Just Dict
+instance Constraint_Type1 Functor (Type_Type1 (Proxy (Map k)) root) where
+ constraint_type1 _c Type_Type1{} = Just Dict
+instance Constraint_Type1 Applicative (Type_Map root)
+instance Constraint_Type1 Applicative (Type_Type1 (Proxy (Map k)) root)
+instance Constraint_Type1 Traversable (Type_Map root) where
+ constraint_type1 _c Type_Type2{} = Just Dict
+instance Constraint_Type1 Traversable (Type_Type1 (Proxy (Map k)) root) where
+ constraint_type1 _c Type_Type1{} = Just Dict
constraint_type1 _c (Type_Type1 _ _) = Just Dict
instance Constraint_Type1 Applicative (Type_Maybe root) where
constraint_type1 _c (Type_Type1 _ _) = Just Dict
+instance Constraint_Type1 Traversable (Type_Maybe root) where
+ constraint_type1 _c (Type_Type1 _ _) = Just Dict
-- | Parsing utility to check that the given type is a 'Type_Maybe'
-- or raise 'Error_Expr_Type_mismatch'.
import Test.Tasty
import Test.Tasty.HUnit
-import Control.Arrow (left)
+import qualified Control.Arrow as Arrow
+import qualified Control.Monad as Monad
+import Data.Functor.Identity
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `left` expected
+ Left err -> Left err @?= snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
- Right (ty_expected::Type_Root_of_Expr (Ex IO) h, _::h, _::Text) ->
- (>>= (@?= (\(_::Proxy h, err) -> err) `left` expected)) $
+ Right (ty_expected::Type_Root_of_Expr (Ex Identity) h, _::h, _::Text) ->
+ (Monad.>>= (@?= (\(_::Proxy h, err) -> err) `Arrow.left` expected)) $
case ty `eq_type` ty_expected of
- Nothing -> return $ Left $
- error_expr (Proxy::Proxy (Ex IO)) $
+ Nothing -> Monad.return $ Left $
+ error_expr (Proxy::Proxy (Ex Identity)) $
Error_Expr_Type_mismatch ast
(Exists_Type ty)
(Exists_Type ty_expected)
Just Refl -> do
- h <- host_from_expr r
- return $
+ let h = runIdentity $ host_from_expr r
+ Monad.return $
Right
( ty
, h
, text_from_expr r
- -- , (text_from_expr :: Repr_String IO h -> Text) r
+ -- , (text_from_expr :: Repr_Text Identity h -> Text) r
)
tests :: TestTree
--- /dev/null
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-- | Expression for 'Monad'.
+module Language.Symantic.Expr.Monad where
+
+import Control.Monad (Monad)
+-- import qualified Control.Monad as Monad
+import Data.Proxy (Proxy(..))
+import Data.Type.Equality ((:~:)(Refl))
+import Prelude hiding ((<$>), Monad(..))
+
+import Language.Symantic.Type
+import Language.Symantic.Trans.Common
+import Language.Symantic.Expr.Root
+import Language.Symantic.Expr.Error
+import Language.Symantic.Expr.From
+import Language.Symantic.Expr.Lambda
+import Language.Symantic.Expr.Functor
+
+-- * Class 'Sym_Monad'
+-- | Symantic.
+class
+ ( Sym_Monad_Lam (Lambda_from_Repr repr) repr
+ ) => Sym_Monad repr where
+ return :: Monad f => repr a -> repr (f a)
+ default return :: (Trans t repr, Monad f) => t repr a -> t repr (f a)
+ return = trans_map1 return
+
+-- * Class 'Sym_Monad_Lam'
+-- | Symantic requiring a 'Lambda'.
+class Sym_Functor lam repr => Sym_Monad_Lam lam repr where
+ (>>=) :: Monad m => repr (m a) -> repr (Lambda lam a (m b)) -> repr (m b)
+ default (>>=) :: (Trans t repr, Monad m)
+ => t repr (m a) -> t repr (Lambda lam a (m b)) -> t repr (m b)
+ (>>=) = trans_map2 (>>=)
+infixl 1 >>=
+
+-- * Type 'Expr_Monad'
+-- | Expression.
+data Expr_Monad (lam:: * -> *) (root:: *)
+type instance Root_of_Expr (Expr_Monad lam root) = root
+type instance Type_of_Expr (Expr_Monad lam root) = No_Type
+type instance Sym_of_Expr (Expr_Monad lam root) repr = (Sym_Monad repr, Sym_Monad_Lam lam repr)
+type instance Error_of_Expr ast (Expr_Monad lam root) = No_Error_Expr
+instance Constraint_Type1 Monad (Type_Type0 px root)
+instance Constraint_Type1 Monad (Type_Var1 root)
+instance Constraint_Type1 Monad (Type_Type2 px root)
+
+return_from
+ :: forall root ty ty_root lam ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Monad lam root)
+ , ty_root ~ Type_Root_of_Expr root
+ , Eq_Type (Type_Root_of_Expr root)
+ , Type1_from ast (Type_Root_of_Expr root)
+ , Expr_from ast root
+ , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Root_of_Expr root ~ root
+ , Constraint_Type1 Monad ty
+ ) => ast -> ast
+ -> Expr_From ast (Expr_Monad lam root) hs ret
+return_from ast_f ast_a ex ast ctx k =
+ -- return :: Monad f => a -> f a
+ either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
+ type1_from (Proxy::Proxy ty_root) ast_f $ \_f ty_f -> Right $
+ expr_from (Proxy::Proxy root) ast_a ctx $
+ \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
+ let ty_fa = ty_f ty_a in
+ check_constraint1_type ex (Proxy::Proxy Monad) ast ty_fa $ \Dict ->
+ k ty_fa $ Forall_Repr_with_Context $
+ \c -> return (a c)
+
+bind_from
+ :: forall root ty lam ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Monad lam root)
+ , Eq_Type (Type_Root_of_Expr root)
+ , Eq_Type1 (Type_Root_of_Expr root)
+ , Expr_from ast root
+ , Lift_Type (Type_Fun lam) (Type_of_Expr root)
+ , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
+ , Unlift_Type1 (Type_of_Expr root)
+ , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Root_of_Expr root ~ root
+ , Constraint_Type1 Monad ty
+ ) => ast -> ast
+ -> Expr_From ast (Expr_Monad lam root) hs ret
+bind_from ast_ma ast_f ex ast ctx k =
+ -- (>>=) :: Monad m => m a -> (a -> m b) -> m b
+ expr_from (Proxy::Proxy root) ast_ma ctx $
+ \(ty_ma::Type_Root_of_Expr root h_ma) (Forall_Repr_with_Context ma) ->
+ expr_from (Proxy::Proxy root) ast_f ctx $
+ \(ty_f::Type_Root_of_Expr root h_f) (Forall_Repr_with_Context f) ->
+ check_type1 ex ast ty_ma $ \(Type_Type1 m ty_m_a, Lift_Type1 ty_m) ->
+ check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_mb
+ :: Type_Fun lam (Type_Root_of_Expr root) h_f) ->
+ check_eq_type ex ast ty_m_a ty_f_a $ \Refl ->
+ check_type1 ex ast ty_f_mb $ \(Type_Type1 _ ty_f_m_b, _) ->
+ check_eq_type1 ex ast ty_ma ty_f_mb $ \Refl ->
+ check_constraint1_type ex (Proxy::Proxy Monad) ast ty_ma $ \Dict ->
+ k (Type_Root $ ty_m $ Type_Type1 m ty_f_m_b) $ Forall_Repr_with_Context $
+ \c -> (>>=) (ma c) (f c)
--- /dev/null
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-- | Expression for 'Traversable'.
+module Language.Symantic.Expr.Traversable where
+
+import Data.Traversable (Traversable)
+import Data.Proxy (Proxy(..))
+import Data.Type.Equality ((:~:)(Refl))
+import Prelude hiding (Traversable(..))
+
+import Language.Symantic.Type
+import Language.Symantic.Trans.Common
+import Language.Symantic.Expr.Root
+import Language.Symantic.Expr.Error
+import Language.Symantic.Expr.From
+import Language.Symantic.Expr.Lambda
+import Language.Symantic.Expr.Applicative
+
+-- * Class 'Sym_Traversable'
+-- | Symantic.
+class
+ ( Sym_Applicative repr
+ , Sym_Applicative_Lam lam repr
+ ) => Sym_Traversable lam repr where
+ traverse :: (Traversable t, Applicative f) => repr (Lambda lam a (f b)) -> repr (t a) -> repr (f (t b))
+ default traverse :: (Trans tr repr, Traversable t, Applicative f)
+ => tr repr (Lambda lam a (f b)) -> tr repr (t a) -> tr repr (f (t b))
+ traverse = trans_map2 traverse
+
+-- * Type 'Expr_Traversable'
+-- | Expression.
+data Expr_Traversable (lam:: * -> *) (root:: *)
+type instance Root_of_Expr (Expr_Traversable lam root) = root
+type instance Type_of_Expr (Expr_Traversable lam root) = No_Type
+type instance Sym_of_Expr (Expr_Traversable lam root) repr = (Sym_Traversable lam repr)
+type instance Error_of_Expr ast (Expr_Traversable lam root) = No_Error_Expr
+instance Constraint_Type1 Traversable (Type_Type0 px root)
+instance Constraint_Type1 Traversable (Type_Var1 root)
+instance Constraint_Type1 Traversable (Type_Type2 px root)
+
+traverse_from
+ :: forall root ty lam ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Traversable lam root)
+ , Eq_Type (Type_Root_of_Expr root)
+ , Eq_Type1 (Type_Root_of_Expr root)
+ , Expr_from ast root
+ , Lift_Type (Type_Fun lam) (Type_of_Expr root)
+ , Unlift_Type (Type_Fun lam) (Type_of_Expr root)
+ , Unlift_Type1 (Type_of_Expr root)
+ , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Root_of_Expr root ~ root
+ , Constraint_Type1 Applicative ty
+ , Constraint_Type1 Traversable ty
+ ) => ast -> ast
+ -> Expr_From ast (Expr_Traversable lam root) hs ret
+traverse_from ast_g ast_ta ex ast ctx k =
+ -- traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
+ expr_from (Proxy::Proxy root) ast_g ctx $
+ \(ty_g::Type_Root_of_Expr root h_g) (Forall_Repr_with_Context g) ->
+ expr_from (Proxy::Proxy root) ast_ta ctx $
+ \(ty_ta::Type_Root_of_Expr root h_ta) (Forall_Repr_with_Context ta) ->
+
+ check_type_fun ex ast ty_g $ \(Type_Type2 Proxy ty_g_a ty_g_fb
+ :: Type_Fun lam (Type_Root_of_Expr root) h_g) ->
+
+ check_type1 ex ast ty_g_fb $ \(Type_Type1 f (ty_g_fb_b::Type_Root_of_Expr root h_f), Lift_Type1 ty_f) ->
+ check_type1 ex ast ty_ta $ \(Type_Type1 t ty_ta_a, Lift_Type1 ty_t) ->
+
+ check_constraint1_type ex (Proxy::Proxy Applicative) ast ty_g_fb $ \Dict ->
+ check_constraint1_type ex (Proxy::Proxy Traversable) ast ty_ta $ \Dict ->
+
+ check_eq_type ex ast ty_g_a ty_ta_a $ \Refl ->
+
+ k (
+ Type_Root $ ty_f $ Type_Type1 f $
+ Type_Root $ ty_t $ Type_Type1 t ty_g_fb_b
+ ) $ Forall_Repr_with_Context $
+ \c -> traverse (g c) (ta c)
--- /dev/null
+../HLint.hs
\ No newline at end of file
--- /dev/null
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+
+module Expr.Applicative.Test where
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import qualified Control.Arrow as Arrow
+import qualified Control.Monad as Monad
+import Data.Functor.Identity
+import Data.Proxy (Proxy(..))
+import Data.Text (Text)
+import Data.Type.Equality ((:~:)(Refl))
+import Prelude hiding ((&&), not, (||), (==), (<$>), (+), Applicative(..), (>>=))
+
+import Language.Symantic.Type
+import Language.Symantic.Expr as Expr
+import Language.Symantic.Repr
+
+import AST.Test
+
+-- * Expressions
+t = bool True
+f = bool False
+e1 = val (\x -> val $ \y -> x + y)
+ <$> just (int 1)
+ <*> just (int 2)
+
+-- * Tests
+type Ex lam = Expr_Root
+ ( Expr_Lambda_App lam
+ .|. Expr_Lambda_Val lam
+ .|. Expr_List lam
+ .|. Expr_Maybe lam
+ .|. Expr_Int
+ .|. Expr_Bool
+ .|. Expr_Functor lam
+ .|. Expr_Applicative lam
+ .|. Expr_Traversable lam
+ )
+ex_from = root_expr_from (Proxy::Proxy (Ex lam)) (Proxy::Proxy lam)
+
+(==>) ast expected =
+ testCase (show ast) $
+ case ex_from ast of
+ Left err -> Left err @?= snd `Arrow.left` expected
+ Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
+ case expected of
+ Left (_, err) -> Right ("…"::String) @?= Left err
+ Right (ty_expected::Type_Root_of_Expr (Ex Identity) h, _::h, _::Text) ->
+ (Monad.>>= (@?= (\(_::Proxy h, err) -> err) `Arrow.left` expected)) $
+ case ty `eq_type` ty_expected of
+ Nothing -> Monad.return $ Left $
+ error_expr (Proxy::Proxy (Ex Identity)) $
+ Error_Expr_Type_mismatch ast
+ (Exists_Type ty)
+ (Exists_Type ty_expected)
+ Just Refl -> do
+ let h = runIdentity $ host_from_expr r
+ Monad.return $
+ Right
+ ( ty
+ , h
+ , text_from_expr r
+ -- , (text_from_expr :: Repr_Text Identity h -> Text) r
+ )
+
+tests :: TestTree
+tests = testGroup "Traversable"
+ [ AST "<*>"
+ [ AST "<$>"
+ [ AST "val"
+ [ AST "x" [], AST "Int" []
+ , AST "val"
+ [ AST "y" [], AST "Int" []
+ , AST "+" [ AST "var" [AST "x" []]
+ , AST "var" [AST "y" []] ]
+ ]
+ ]
+ , AST "just" [ AST "int" [AST "1" []] ]
+ ]
+ , AST "just" [ AST "int" [AST "2" []] ]
+ ] ==> Right
+ ( type_maybe type_int
+ , Just 3
+ , "fmap (\\x0 -> (\\x1 -> x0 + x1)) (just 1) <*> just 2" )
+ ]
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
--- | Expression for 'Tuple'.
+-- | Expression for tuples.
module Language.Symantic.Expr.Tuple where
import Data.Proxy (Proxy(..))
default tuple2 :: Trans t repr => t repr a -> t repr b -> t repr (a, b)
tuple2 = trans_map2 tuple2
-instance Constraint_Type1 Functor (Type_Type1 (Proxy ((,) fst)) root) where
- constraint_type1 _c Type_Type1{} = Just Dict
-
-- * Type 'Expr_Tuple2'
-- | Expression.
data Expr_Tuple2 (lam:: * -> *) (root:: *)
type instance Sym_of_Expr (Expr_Tuple2 lam root) repr = (Sym_Tuple2 repr)
type instance Error_of_Expr ast (Expr_Tuple2 lam root) = No_Error_Expr
+instance Constraint_Type1 Functor (Type_Type1 (Proxy ((,) fst)) root) where
+ constraint_type1 _c Type_Type1{} = Just Dict
+instance Constraint_Type1 Functor (Type_Tuple2 root) where
+ constraint_type1 _c Type_Type2{} = Just Dict
+instance Constraint_Type1 Applicative (Type_Type1 (Proxy ((,) fst)) root)
+
-- | Parsing utility to check that the given type is a 'Type_Tuple2'
-- or raise 'Error_Expr_Type_mismatch'.
check_type_tuple2
-> Either (Error_of_Expr ast root) ret
check_type_tuple2 ex ast ty k =
case unlift_type $ unType_Root ty of
- Just ty_l -> k ty_l
+ Just ty_t -> k ty_t
Nothing -> Left $
error_expr ex $
Error_Expr_Type_mismatch ast
+{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
-- | Interpreter to duplicate the representation of an expression
-- in order to evaluate it with different interpreters.
--
) => Sym_Map_Lam lam (Dup r1 r2) where
map_map (f1 `Dup` f2) (m1 `Dup` m2) =
map_map f1 m1 `Dup` map_map f2 m2
+instance -- Sym_Functor
+ ( Sym_Functor lam r1
+ , Sym_Functor lam r2
+ ) => Sym_Functor lam (Dup r1 r2) where
+ fmap (f1 `Dup` f2) (m1 `Dup` m2) =
+ fmap f1 m1 `Dup` fmap f2 m2
+instance -- Sym_Applicative
+ ( Sym_Applicative r1
+ , Sym_Applicative r2
+ , Sym_Applicative_Lam (Lambda_from_Repr r1) (Dup r1 r2)
+ ) => Sym_Applicative (Dup r1 r2) where
+ pure (a1 `Dup` a2) =
+ pure a1 `Dup` pure a2
+instance -- Sym_Applicative_Lam
+ ( Sym_Applicative_Lam lam r1
+ , Sym_Applicative_Lam lam r2
+ ) => Sym_Applicative_Lam lam (Dup r1 r2) where
+ (<*>) (f1 `Dup` f2) (m1 `Dup` m2) =
+ (<*>) f1 m1 `Dup` (<*>) f2 m2
+instance -- Sym_Traversable
+ ( Sym_Traversable lam r1
+ , Sym_Traversable lam r2
+ , lam ~ Lambda_from_Repr r1
+ ) => Sym_Traversable lam (Dup r1 r2) where
+ traverse (f1 `Dup` f2) (m1 `Dup` m2) =
+ traverse f1 m1 `Dup` traverse f2 m2
+instance -- Sym_Monad
+ ( Sym_Monad_Lam lam r1
+ , Sym_Monad_Lam lam r2
+ , lam ~ Lambda_from_Repr r1
+ ) => Sym_Monad_Lam lam (Dup r1 r2) where
+ (>>=) (m1 `Dup` m2) (f1 `Dup` f2) =
+ (>>=) m1 f1 `Dup` (>>=) m2 f2
+{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
-- | Interpreter to compute a host-term.
module Language.Symantic.Repr.Host where
-import Data.Functor as Functor
-import Data.Functor.Identity
import Control.Applicative as Applicative
import Control.Monad as Monad
import Control.Monad.IO.Class (MonadIO(..))
+import Data.Functor as Functor
+import Data.Functor.Identity
import Data.IORef
+import Data.Traversable as Traversable
import qualified Data.Bool as Bool
import qualified Data.Maybe as Maybe
import qualified Data.Map.Strict as Map
import Language.Symantic.Lib.Control.Monad
import Language.Symantic.Type
-import Language.Symantic.Expr
+import Language.Symantic.Expr hiding (Sym_Monad(..), Sym_Monad_Lam(..))
+import qualified Language.Symantic.Expr as Expr
-- * Type 'Repr_Host'
{- NOTE: need Traversable
fmap f = liftMJoin $ sequence . ((\a -> f `app` return a) Functor.<$>)
-}
-instance Monad lam => Sym_Applicative (Repr_Host lam) where
+instance
+ ( Sym_Applicative_Lam lam (Repr_Host lam)
+ , Applicative lam
+ ) => Sym_Applicative (Repr_Host lam) where
pure = Functor.fmap Applicative.pure
instance Sym_Applicative_Lam Identity (Repr_Host Identity) where
(<*>) = liftM2Join $ \fg ->
Applicative.<*>
(return Functor.<$> fa)
-}
+instance Sym_Traversable Identity (Repr_Host Identity) where
+ traverse ra2fb = liftMJoin $
+ return . Traversable.traverse a2fb
+ where a2fb a = runIdentity $ unRepr_Host $ ra2fb `app` return a
+instance
+ ( Expr.Sym_Monad_Lam lam (Repr_Host lam)
+ , Monad lam
+ ) => Expr.Sym_Monad (Repr_Host lam) where
+ return = Functor.fmap Monad.return
+instance Expr.Sym_Monad_Lam Identity (Repr_Host Identity) where
+ (>>=) rma ra2mb = do
+ ma <- rma
+ return $ (Monad.>>=) ma a2mb
+ where a2mb a = runIdentity $ unRepr_Host $ ra2mb `app` return a
-- | Helper to store arguments of 'lazy' into an 'IORef'.
lazy_share :: MonadIO m => m a -> m (m a)
import Data.Functor.Identity
import Data.Text (Text)
import qualified Data.Text as Text
-import Prelude hiding (and, not, or)
+import Prelude hiding (and, not, or, Monad(..))
import Language.Symantic.Repr
import Language.Symantic.Expr
tests :: TestTree
tests = testGroup "Host" $
[ testGroup "Bool" $
- let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root ( Expr_Lambda_App IO
- .|. Expr_Lambda_Val IO
+ let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root ( Expr_Lambda_App Identity
+ .|. Expr_Lambda_Val Identity
.|. Expr_Bool
)) repr => repr h) expected =
- testCase (Text.unpack $ (text_from_expr :: Repr_Text IO _h -> Text) $ expr) $
- (>>= (@?= expected)) $
+ testCase (Text.unpack $ (text_from_expr :: Repr_Text Identity _h -> Text) $ expr) $
+ -- (>>= (@?= expected)) $
+ (\(Identity a) -> (a @?= expected)) $
host_from_expr expr in
[ Bool.Test.e1 ==> False
, Bool.Test.e2 ==> True
, Bool.Test.e4 ==> True
]
, testGroup "Lambda" $
- let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root ( Expr_Lambda_App IO
- .|. Expr_Lambda_Val IO
+ let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root ( Expr_Lambda_App Identity
+ .|. Expr_Lambda_Val Identity
.|. Expr_Bool
)) repr => repr h) expected =
- testCase (Text.unpack $ (text_from_expr :: Repr_Text IO _h -> Text) $ expr) $
- (>>= (@?= expected)) $
+ testCase (Text.unpack $ (text_from_expr :: Repr_Text Identity _h -> Text) $ expr) $
+ (\(Identity a) -> (a @?= expected)) $
host_from_expr expr in
[ (Lambda.Test.e1 `app` bool True `app` bool True) ==> False
, (Lambda.Test.e1 `app` bool True `app` bool False) ==> True
, (Lambda.Test.e7 `app` val not) ==> False
]
, testGroup "Maybe" $
- let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root ( Expr_Lambda_App IO
- .|. Expr_Lambda_Val IO
- .|. Expr_Maybe IO
+ let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root ( Expr_Lambda_App Identity
+ .|. Expr_Lambda_Val Identity
+ .|. Expr_Maybe Identity
.|. Expr_Bool )) repr => repr h) expected =
- testCase (Text.unpack $ (text_from_expr :: Repr_Text IO _h -> Text) $ expr) $
- (>>= (@?= expected)) $
+ testCase (Text.unpack $ (text_from_expr :: Repr_Text Identity _h -> Text) $ expr) $
+ (\(Identity a) -> (a @?= expected)) $
host_from_expr expr in
[ Maybe.Test.e1 ==> False
]
, testGroup "If" $
- let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root ( Expr_Lambda_App IO
- .|. Expr_Lambda_Val IO
+ let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root ( Expr_Lambda_App Identity
+ .|. Expr_Lambda_Val Identity
.|. Expr_If
.|. Expr_Bool )) repr => repr h) expected =
- testCase (Text.unpack $ (text_from_expr :: Repr_Text IO _h -> Text) $ expr) $
- (>>= (@?= expected)) $
+ testCase (Text.unpack $ (text_from_expr :: Repr_Text Identity _h -> Text) $ expr) $
+ (\(Identity a) -> (a @?= expected)) $
host_from_expr expr in
[ If.Test.e1 ==> False
]
, testGroup "List" $
- let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root ( Expr_Lambda_App IO
- .|. Expr_Lambda_Val IO
- .|. Expr_List IO
+ let (==>) (expr::forall repr. Sym_of_Expr (Expr_Root ( Expr_Lambda_App Identity
+ .|. Expr_Lambda_Val Identity
+ .|. Expr_List Identity
.|. Expr_Bool
.|. Expr_Int
.|. Expr_If
.|. Expr_Eq )) repr => repr h) expected =
- testCase (Text.unpack $ (text_from_expr :: Repr_Text IO _h -> Text) $ expr) $
- (>>= (@?= expected)) $
+ testCase (Text.unpack $ (text_from_expr :: Repr_Text Identity _h -> Text) $ expr) $
+ (\(Identity a) -> (a @?= expected)) $
host_from_expr expr in
[ List.Test.e1 ==> [2::Int,4]
]
+{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
-- | Interpreter to serialize an expression into a 'Text'.
module Language.Symantic.Repr.Text where
Repr_Text $ \_p v ->
let p' = precedence_App in
"fmap " <> f p' v <> " " <> m p' v
-instance Monad lam => Sym_Applicative (Repr_Text lam) where
+instance (Sym_Applicative_Lam lam (Repr_Text lam), Applicative lam) => Sym_Applicative (Repr_Text lam) where
pure (Repr_Text a) =
Repr_Text $ \_p v ->
let p' = precedence_App in
Repr_Text $ \p v ->
let p' = precedence_LtStarGt in
paren p p' $ fg p' v <> " <*> " <> fa p' v
+instance Monad lam => Sym_Traversable lam (Repr_Text lam) where
+ traverse (Repr_Text g) (Repr_Text ta) =
+ Repr_Text $ \p v ->
+ let p' = precedence_App in
+ paren p p' $ "traverse " <> g p' v <> " " <> ta p' v
-- ** Type 'Precedence'
, module Language.Symantic.Type.Ordering
, module Language.Symantic.Type.Tuple
, module Language.Symantic.Type.Map
+ , module Language.Symantic.Type.Either
) where
import Language.Symantic.Type.Root
import Language.Symantic.Type.Ordering
import Language.Symantic.Type.Tuple
import Language.Symantic.Type.Map
+import Language.Symantic.Type.Either
--- /dev/null
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module Language.Symantic.Type.Either where
+
+import Data.Proxy
+import Language.Symantic.Type.Root
+import Language.Symantic.Type.Type0
+import Language.Symantic.Type.Type2
+
+-- * Type 'Type_Either'
+-- | The 'Either' type.
+type Type_Either = Type_Type2 (Proxy Either)
+
+type instance Constraint2_of (Proxy Either)
+ = Constraint2_Empty
+
+pattern Type_Either
+ :: root a -> root b
+ -> Type_Either root (Either a b)
+pattern Type_Either a b
+ = Type_Type2 Proxy a b
+
+instance -- String_from_Type
+ String_from_Type root =>
+ String_from_Type (Type_Either root) where
+ string_from_type (Type_Type2 _ a b) =
+ "Either"
+ ++ " (" ++ string_from_type a ++ ")"
+ ++ " (" ++ string_from_type b ++ ")"
+
+-- | Inject 'Type_Either' within a root type.
+type_either
+ :: forall root h_a h_b.
+ Lift_Type_Root Type_Either root
+ => root h_a
+ -> root h_b
+ -> root (Either h_a h_b)
+type_either a b = lift_type_root
+ (Type_Either a b
+ ::Type_Either root (Either h_a h_b))
import Language.Symantic.Type.Type2
-- * Type 'Type_Tuple2'
--- | The (,) type.
+-- | The @(,)@ type.
type Type_Tuple2 = Type_Type2 (Proxy (,))
type instance Constraint2_of (Proxy (,))
Language.Symantic.Expr.Alt
Language.Symantic.Expr.Applicative
Language.Symantic.Expr.Bool
+ Language.Symantic.Expr.Either
Language.Symantic.Expr.Eq
Language.Symantic.Expr.Error
Language.Symantic.Expr.From
Language.Symantic.Expr.List
Language.Symantic.Expr.Map
Language.Symantic.Expr.Maybe
+ Language.Symantic.Expr.Monad
Language.Symantic.Expr.Ord
Language.Symantic.Expr.Root
+ Language.Symantic.Expr.Traversable
Language.Symantic.Expr.Tuple
Language.Symantic.Lib.Control.Monad
Language.Symantic.Lib.Data.Bool
Language.Symantic.Type
Language.Symantic.Type.Alt
Language.Symantic.Type.Bool
+ Language.Symantic.Type.Either
Language.Symantic.Type.Error
Language.Symantic.Type.Fun
Language.Symantic.Type.Int
sourcephile / git / haskell / symantic.git / commitdiff