showsPrec prec_arrow a .
showString (" "++n++" ") .
showsPrec prec_arrow b
+ AST "\\" [var, ty, body] ->
+ showParen (p >= prec_lambda) $
+ showString ("\\(") .
+ showsPrec prec_lambda var .
+ showString (":") .
+ showsPrec prec_lambda ty .
+ showString (") -> ") .
+ showsPrec prec_lambda body
+ AST "$" [fun, arg] ->
+ showParen (p >= prec_app) $
+ showsPrec prec_app fun .
+ showString (" $ ") .
+ showsPrec prec_app arg
_ ->
showString n .
showString "(" .
showString (List.intercalate ", " $ show Prelude.<$> args) .
showString ")"
- where prec_arrow = 1
+ where prec_arrow = 1
+ prec_lambda = 1
+ prec_app = 1
-- ** Parsing utilities
from_ast0
_ -> Left $ lift_error_type $
Error_Type_Wrong_number_of_arguments ast 0
_ -> Left $ error_type_unsupported ty ast
+instance -- Type_from AST Type_Text
+ ( Lift_Type_Root Type_Text root
+ , Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
+ , IBool (Is_Last_Type (Type_Text root) root)
+ ) => Type_from AST (Type_Text root) where
+ type_from ty ast k =
+ case ast of
+ AST "Text" asts ->
+ case asts of
+ [] -> k type_text
+ _ -> Left $ lift_error_type $
+ Error_Type_Wrong_number_of_arguments ast 0
+ _ -> Left $ error_type_unsupported ty ast
instance -- Type_from AST Type_Ordering
( Lift_Type_Root Type_Ordering root
, Lift_Error_Type (Error_Type AST) (Error_of_Type AST root)
[ast_k, ast_a] ->
type_from (Proxy::Proxy root) ast_k $ \ty_k ->
type_from (Proxy::Proxy root) ast_a $ \ty_a ->
- check_type_constraint (Proxy::Proxy Ord) ast_k ty_k $ \Dict ->
k (type_map ty_k ty_a)
_ -> Left $ lift_error_type $
Error_Type_Wrong_number_of_arguments ast 2
AST "*" asts -> op2_from_AST (Expr.*) type_int asts ex ast
AST "mod" asts -> op2_from_AST Expr.mod type_int asts ex ast
_ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
+instance -- Expr_from AST Expr_Text
+ ( Eq_Type (Type_Root_of_Expr root)
+ , Expr_from AST root
+ , Lift_Type_Root Type_Text (Type_Root_of_Expr root)
+ , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
+ , Unlift_Type Type_Text (Type_of_Expr root)
+ , Root_of_Expr root ~ root
+ , IBool (Is_Last_Expr (Expr_Text root) root)
+ ) => Expr_from AST (Expr_Text root) where
+ expr_from ex ast =
+ case ast of
+ AST "text" asts ->
+ case asts of
+ [AST lit []] -> \_ctx k ->
+ k type_text $ Forall_Repr_with_Context $ \_c -> text lit
+ _ -> \_ctx _k -> Left $ error_expr ex $
+ Error_Expr_Wrong_number_of_arguments ast 1
+ _ -> \_ctx _k -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Lambda
( Eq_Type (Type_Root_of_Expr root)
, Type_from AST (Type_Root_of_Expr root)
ast_ty_a:asts' -> list_from ast_ty_a asts' ex ast ctx k
_ -> Left $ error_expr ex $
Error_Expr_Wrong_number_of_arguments ast 1
+ AST "list_zipWith" asts -> from_ast3 asts list_zipWith_from ex ast ctx k
+ AST "list_reverse" asts -> from_ast1 asts list_reverse_from ex ast ctx k
_ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Map
( Eq_Type (Type_Root_of_Expr root)
, Expr_from AST root
- , Lift_Type Type_Fun (Type_of_Expr root)
- , Unlift_Type Type_Fun (Type_of_Expr root)
- , Lift_Type Type_Map (Type_of_Expr root)
- , Unlift_Type Type_Map (Type_of_Expr root)
- , Lift_Type Type_List (Type_of_Expr root)
- , Unlift_Type Type_List (Type_of_Expr root)
- , Lift_Type Type_Tuple2 (Type_of_Expr root)
- , Unlift_Type Type_Tuple2 (Type_of_Expr root)
+ , Lift_Type Type_Fun (Type_of_Expr root)
+ , Unlift_Type Type_Fun (Type_of_Expr root)
+ , Lift_Type Type_Bool (Type_of_Expr root)
+ , Unlift_Type Type_Bool (Type_of_Expr root)
+ , Lift_Type Type_List (Type_of_Expr root)
+ , Unlift_Type Type_List (Type_of_Expr root)
+ , Lift_Type Type_Map (Type_of_Expr root)
+ , Unlift_Type Type_Map (Type_of_Expr root)
+ , Lift_Type Type_Maybe (Type_of_Expr root)
+ , Unlift_Type Type_Maybe (Type_of_Expr root)
+ , Lift_Type Type_Tuple2 (Type_of_Expr root)
+ , Unlift_Type Type_Tuple2 (Type_of_Expr root)
, Constraint_Type Ord (Type_Root_of_Expr root)
, Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
, Root_of_Expr root ~ root
) => Expr_from AST (Expr_Map root) where
expr_from ex ast ctx k =
case ast of
- AST "map_from_list" asts -> from_ast1 asts map_from_list_from ex ast ctx k
- AST "mapWithKey" asts -> from_ast2 asts mapWithKey_from ex ast ctx k
+ AST "map_from_list" asts -> from_ast1 asts map_from_list_from ex ast ctx k
+ AST "mapWithKey" asts -> from_ast2 asts mapWithKey_from ex ast ctx k
+ AST "map_lookup" asts -> from_ast2 asts map_lookup_from ex ast ctx k
+ AST "map_keys" asts -> from_ast1 asts map_keys_from ex ast ctx k
+ AST "map_member" asts -> from_ast2 asts map_member_from ex ast ctx k
+ AST "map_insert" asts -> from_ast3 asts map_insert_from ex ast ctx k
+ AST "map_delete" asts -> from_ast2 asts map_delete_from ex ast ctx k
+ AST "map_difference" asts -> from_ast2 asts map_difference_from ex ast ctx k
+ AST "map_foldrWithKey" asts -> from_ast3 asts map_foldrWithKey_from ex ast ctx k
_ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Functor
( Eq_Type (Type_Root_of_Expr root)
case ast of
AST "mempty" asts -> from_ast1 asts mempty_from ex ast ctx k
AST "mappend" asts -> from_ast2 asts mappend_from ex ast ctx k
+ AST "<>" asts -> from_ast2 asts mappend_from ex ast ctx k
_ -> Left $ error_expr_unsupported ex ast
instance -- Expr_from AST Expr_Monad
( Eq_Type (Type_Root_of_Expr root)
AST "left" asts -> from_ast2 asts left_from ex ast ctx k
AST "right" asts -> from_ast2 asts right_from ex ast ctx k
_ -> Left $ error_expr_unsupported ex ast
+instance -- Expr_from AST Expr_Tuple2
+ ( Eq_Type (Type_Root_of_Expr root)
+ , Expr_from AST root
+ , Lift_Type Type_Tuple2 (Type_of_Expr root)
+ , Unlift_Type Type_Tuple2 (Type_of_Expr root)
+ , Lift_Error_Expr (Error_Expr_of_Root AST root) (Error_of_Expr AST root)
+ , Root_of_Expr root ~ root
+ , IBool (Is_Last_Expr (Expr_Tuple2 root) root)
+ ) => Expr_from AST (Expr_Tuple2 root) where
+ expr_from ex ast ctx k =
+ case ast of
+ AST "(,)" asts -> from_ast2 asts tuple2_from ex ast ctx k
+ AST "fst" asts -> from_ast1 asts fst_from ex ast ctx k
+ AST "snd" asts -> from_ast1 asts snd_from ex ast ctx k
+ _ -> Left $ error_expr_unsupported ex ast
type instance Type_of_Expr (Expr_Applicative root) = No_Type
type instance Sym_of_Expr (Expr_Applicative root) repr = (Sym_Applicative repr)
type instance Error_of_Expr ast (Expr_Applicative root) = No_Error_Expr
-instance Constraint_Type1 Applicative (Type_Type0 px root)
instance Constraint_Type1 Applicative (Type_Var1 root)
--- instance Constraint_Type1 Applicative (Type_Type2 px root)
-- | Parse 'pure'.
pure_from
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `Arrow.left` expected
+ Left err -> Left err @?= Prelude.snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `Arrow.left` expected
+ Left err -> Left err @?= Prelude.snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `Arrow.left` expected
+ Left err -> Left err @?= Prelude.snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
type instance Type_of_Expr (Expr_Foldable root) = No_Type
type instance Sym_of_Expr (Expr_Foldable root) repr = (Sym_Foldable repr)
type instance Error_of_Expr ast (Expr_Foldable root) = No_Error_Expr
-
-instance Constraint_Type1 Foldable (Type_Type0 px root)
instance Constraint_Type1 Foldable (Type_Var1 root)
-- | Parse 'foldMap'.
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `Arrow.left` expected
+ Left err -> Left err @?= Prelude.snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
type instance Type_of_Expr (Expr_Functor root) = No_Type
type instance Sym_of_Expr (Expr_Functor root) repr = (Sym_Functor repr)
type instance Error_of_Expr ast (Expr_Functor root) = No_Error_Expr
-instance Constraint_Type1 Functor (Type_Type0 px root)
instance Constraint_Type1 Functor (Type_Var1 root)
-- | Parse 'fmap'.
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `Arrow.left` expected
+ Left err -> Left err @?= Prelude.snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `Arrow.left` expected
+ Left err -> Left err @?= Prelude.snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
import qualified Control.Arrow as Arrow
import qualified Control.Monad as Monad
--- import Control.Monad.IO.Class (MonadIO(..))
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 `Arrow.left` expected
+ Left err -> Left err @?= Prelude.snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
import Test.Tasty
-import Prelude hiding ((&&), not, (||), (==))
+import Prelude hiding ((&&), not, (||), (==), id)
import Language.Symantic.Expr.Lambda
import Language.Symantic.Expr.Bool
-- | Expression for 'List'.
module Language.Symantic.Expr.List where
+import qualified Data.Function as Fun
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
-- | Symantic.
class Sym_List repr where
list_empty :: repr [a]
- list_cons :: repr a -> repr [a] -> repr [a]
- list :: [repr a] -> repr [a]
- list_filter
- :: repr ((->) a Bool)
- -> repr [a]
- -> repr [a]
+ list_cons :: repr a -> repr [a] -> repr [a]
+ list :: [repr a] -> repr [a]
+ list_filter :: repr (a -> Bool) -> repr [a] -> repr [a]
+ list_zipWith :: repr (a -> b -> c) -> repr [a] -> repr [b] -> repr [c]
+ list_reverse :: repr [a] -> repr [a]
- default list_empty :: Trans t repr => t repr [a]
- default list_cons :: Trans t repr => t repr a -> t repr [a] -> t repr [a]
- default list :: Trans t repr => [t repr a] -> t repr [a]
- default list_filter
- :: Trans t repr
- => t repr ((->) a Bool)
- -> t repr [a]
- -> t repr [a]
+ default list_empty :: Trans t repr => t repr [a]
+ default list_cons :: Trans t repr => t repr a -> t repr [a] -> t repr [a]
+ default list :: Trans t repr => [t repr a] -> t repr [a]
+ default list_filter :: Trans t repr => t repr (a -> Bool) -> t repr [a] -> t repr [a]
+ default list_zipWith :: Trans t repr => t repr (a -> b -> c) -> t repr [a] -> t repr [b] -> t repr [c]
+ default list_reverse :: Trans t repr => t repr [a] -> t repr [a]
- list_empty = trans_lift list_empty
- list_cons = trans_map2 list_cons
- list l = trans_lift $ list (trans_apply Prelude.<$> l)
- list_filter = trans_map2 list_filter
+ list_empty = trans_lift list_empty
+ list_cons = trans_map2 list_cons
+ list l = trans_lift $ list (trans_apply Prelude.<$> l)
+ list_filter = trans_map2 list_filter
+ list_zipWith = trans_map3 list_zipWith
+ list_reverse = trans_map1 list_reverse
-- * Type 'Expr_List'
-- | Expression.
) => ast
-> Expr_From ast (Expr_List root) hs ret
list_empty_from ast_ty_a ex ast _ctx k =
- either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) id $
+ either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
type_from (Proxy::Proxy ty) ast_ty_a $ \ty_a -> Right $
k (type_list ty_a) $ Forall_Repr_with_Context $
- const list_empty
+ Fun.const list_empty
-- | Parse 'list_cons'.
list_cons_from
check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_a) ->
check_eq_type ex ast ty_a ty_l_a $ \Refl ->
k (type_list ty_a) $ Forall_Repr_with_Context $
- \c -> list_cons (a c) (l c)
+ \c -> list_cons (a c) (l c)
-- | Parse 'list'.
list_from
-> Expr_From ast (Expr_List root) hs ret
go ty_a as [] _ex _ast _ctx k =
k (type_list ty_a) $ Forall_Repr_with_Context $
- \c -> list ((\(Forall_Repr_with_Context a) -> a c) Prelude.<$> reverse as)
+ \c -> list ((\(Forall_Repr_with_Context a) -> a c) Prelude.<$> reverse as)
go ty_a as (ast_x:ast_xs) ex ast ctx k =
expr_from (Proxy::Proxy root) ast_x ctx $
\(ty_x::ty h_x) x ->
check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
k ty_l $ Forall_Repr_with_Context $
\c -> list_filter (f c) (l c)
+
+-- | Parse 'list_zipWith'.
+list_zipWith_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_List root)
+ , Eq_Type ty
+ , Expr_from ast root
+ , Lift_Type Type_Fun (Type_of_Expr root)
+ , Unlift_Type Type_Fun (Type_of_Expr root)
+ , Lift_Type Type_List (Type_of_Expr root)
+ , Unlift_Type Type_List (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 -> ast
+ -> Expr_From ast (Expr_List root) hs ret
+list_zipWith_from ast_f ast_la ast_lb ex ast ctx k =
+ -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
+ expr_from (Proxy::Proxy root) ast_f ctx $
+ \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
+ expr_from (Proxy::Proxy root) ast_la ctx $
+ \(ty_la::ty h_la) (Forall_Repr_with_Context la) ->
+ expr_from (Proxy::Proxy root) ast_lb ctx $
+ \(ty_lb::ty h_lb) (Forall_Repr_with_Context lb) ->
+ check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b2c
+ :: Type_Fun ty h_f) ->
+ check_type_fun ex ast ty_f_b2c $ \(Type_Type2 Proxy ty_f_b ty_f_c
+ :: Type_Fun ty h_f_b2c) ->
+ check_type_list ex ast ty_la $ \(Type_Type1 _ ty_l_a) ->
+ check_type_list ex ast ty_lb $ \(Type_Type1 _ ty_l_b) ->
+ check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
+ check_eq_type ex ast ty_f_b ty_l_b $ \Refl ->
+ check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
+ k (type_list ty_f_c) $ Forall_Repr_with_Context $
+ \c -> list_zipWith (f c) (la c) (lb c)
+
+-- | Parse 'list_reverse'.
+list_reverse_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_List root)
+ , Eq_Type ty
+ , Expr_from ast root
+ , Lift_Type Type_List (Type_of_Expr root)
+ , Unlift_Type Type_List (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
+ -> Expr_From ast (Expr_List root) hs ret
+list_reverse_from ast_l ex ast ctx k =
+ expr_from (Proxy::Proxy root) ast_l ctx $
+ \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
+ check_type_list ex ast ty_l $ \(Type_Type1 _ _ty_l_a) ->
+ k ty_l $ Forall_Repr_with_Context $
+ \c -> list_reverse (l c)
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Expr.List.Test where
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.Proxy (Proxy(..))
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
--}
-import Prelude hiding (mod, (==))
+import Prelude hiding (mod, (==), return)
--- import Language.Symantic.Repr
+import Language.Symantic.Repr
import Language.Symantic.Expr
--- import Language.Symantic.Type
+import Language.Symantic.Type
--- import AST.Test
+import AST.Test
-- * Expressions
t = bool True
e1 = list_filter (lam $ \x -> if_ (x `mod` int 2 == int 0) t f)
(list $ int Prelude.<$> [1..5])
-{-
-- * Tests
+type Ex = Expr_Root
+ ( Expr_Lambda
+ .|. Expr_List
+ .|. Expr_Int
+ .|. Expr_Bool
+ )
+ex_from = root_expr_from (Proxy::Proxy Ex)
+
(==>) ast expected =
testCase (show ast) $
- case ex_from (Proxy::Proxy IO) ast of
- Left err -> Left err @?= snd `left` expected
+ case ex_from ast of
+ Left err -> Left err @?= Prelude.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 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) $
Error_Expr_Type_mismatch ast
(Exists_Type ty)
(Exists_Type ty_expected)
Just Refl -> do
- h <- host_from_expr r
- return $
+ let h = 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 h -> Text) r
)
--}
+
tests :: TestTree
tests = testGroup "List"
- [{- AST "just" [AST "bool" [AST "True" []]] ==> Right
- ( type_maybe type_bool
- , Just True
- , "just True" )
- , AST "just"
- [ AST "let"
- [ AST "x" []
- , AST "bool" [AST "True" []]
- , AST "var" [AST "x" []]
- ]
- ] ==> Right
- ( type_maybe type_bool
- , Just True
- , "just (let x0 = True in x0)" )
- , AST "maybe"
- [ AST "bool" [AST "True" []]
- , AST "\\"
- [ AST "x" []
- , AST "Bool" []
- , AST "not" [AST "var" [AST "x" []]]
- ]
- , AST "nothing"
- [ AST "Bool" []
- ]
- ] ==> Right
- ( type_bool
- , True
- , "maybe True (\\x0 -> !x0) nothing" )
- , AST "maybe"
- [ AST "bool" [AST "False" []]
- , AST "\\"
- [ AST "x" []
- , AST "Bool" []
- , AST "not" [AST "var" [AST "x" []]]
- ]
- , AST "just"
- [ AST "bool" [AST "True" []]
+ [ AST "list_reverse"
+ [ AST "list"
+ [ AST "Int" []
+ , AST "int" [AST "1" []]
+ , AST "int" [AST "2" []]
+ , AST "int" [AST "3" []]
]
] ==> Right
- ( type_bool
- , False
- , "maybe False (\\x0 -> !x0) (just True)" )
- -}]
+ ( type_list type_int
+ , [3,2,1]
+ , "list_reverse [1, 2, 3]" )
+ ]
module Language.Symantic.Expr.Map where
import Data.Map.Strict (Map)
+-- import qualified Data.Map.Strict as Map
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
-- | Symantic.
class Sym_Map repr where
map_from_list :: Ord k => repr [(k, a)] -> repr (Map k a)
- mapWithKey
- :: repr (k -> a -> b)
- -> repr (Map k a)
- -> repr (Map k b)
+ mapWithKey :: repr (k -> a -> b) -> repr (Map k a) -> repr (Map k b)
+ map_lookup :: Ord k => repr k -> repr (Map k a) -> repr (Maybe a)
+ map_keys :: repr (Map k a) -> repr [k]
+ map_member :: Ord k => repr k -> repr (Map k a) -> repr Bool
+ map_insert :: Ord k => repr k -> repr a -> repr (Map k a) -> repr (Map k a)
+ map_delete :: Ord k => repr k -> repr (Map k a) -> repr (Map k a)
+ map_difference :: Ord k => repr (Map k a) -> repr (Map k b) -> repr (Map k a)
+ map_foldrWithKey :: repr (k -> a -> b -> b) -> repr b -> repr (Map k a) -> repr b
default map_from_list :: (Trans t repr, Ord k) => t repr [(k, a)] -> t repr (Map k a)
- default mapWithKey
- :: Trans t repr
- => t repr (k -> a -> b)
- -> t repr (Map k a)
- -> t repr (Map k b)
+ default mapWithKey :: Trans t repr => t repr (k -> a -> b) -> t repr (Map k a) -> t repr (Map k b)
+ default map_lookup :: (Trans t repr, Ord k) => t repr k -> t repr (Map k a) -> t repr (Maybe a)
+ default map_keys :: (Trans t repr, Ord k) => t repr (Map k a) -> t repr [k]
+ default map_member :: (Trans t repr, Ord k) => t repr k -> t repr (Map k a) -> t repr Bool
+ default map_insert :: (Trans t repr, Ord k) => t repr k -> t repr a -> t repr (Map k a) -> t repr (Map k a)
+ default map_delete :: (Trans t repr, Ord k) => t repr k -> t repr (Map k a) -> t repr (Map k a)
+ default map_difference :: (Trans t repr, Ord k) => t repr (Map k a) -> t repr (Map k b) -> t repr (Map k a)
+ default map_foldrWithKey :: Trans t repr => t repr (k -> a -> b -> b) -> t repr b -> t repr (Map k a) -> t repr b
- map_from_list = trans_map1 map_from_list
- mapWithKey = trans_map2 mapWithKey
+ map_from_list = trans_map1 map_from_list
+ mapWithKey = trans_map2 mapWithKey
+ map_lookup = trans_map2 map_lookup
+ map_keys = trans_map1 map_keys
+ map_member = trans_map2 map_member
+ map_insert = trans_map3 map_insert
+ map_delete = trans_map2 map_delete
+ map_difference = trans_map2 map_difference
+ map_foldrWithKey = trans_map3 map_foldrWithKey
-- | Parsing utility to check that the given type is a 'Type_List'
-- or raise 'Error_Expr_Type_mismatch'.
, Expr_from ast root
, Lift_Type Type_Fun (Type_of_Expr root)
, Unlift_Type Type_Fun (Type_of_Expr root)
- , Lift_Type Type_Map (Type_of_Expr root)
- , Unlift_Type Type_Map (Type_of_Expr root)
- , Constraint_Type Ord ty
+ , Lift_Type Type_Map (Type_of_Expr root)
+ , Unlift_Type Type_Map (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_Map root) hs ret
mapWithKey_from ast_f ast_m ex ast ctx k =
+ -- mapWithKey :: (k -> a -> b) -> Map k a -> Map k b
expr_from (Proxy::Proxy root) ast_f ctx $
\(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
expr_from (Proxy::Proxy root) ast_m ctx $
check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
check_eq_type ex ast ty_f_k ty_m_k $ \Refl ->
check_eq_type ex ast ty_f_a ty_m_a $ \Refl ->
- check_constraint_type ex (Proxy::Proxy Ord) ast ty_m_k $ \Dict ->
k (type_map ty_m_k ty_f_b) $ Forall_Repr_with_Context $
\c -> mapWithKey (f c) (m c)
+-- | Parse 'map_lookup'.
+map_lookup_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Map root)
+ , Eq_Type ty
+ , Expr_from ast root
+ , Lift_Type Type_Map (Type_of_Expr root)
+ , Unlift_Type Type_Map (Type_of_Expr root)
+ , Lift_Type Type_Maybe (Type_of_Expr root)
+ , Constraint_Type Ord ty
+ , 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_Map root) hs ret
+map_lookup_from ast_k ast_m ex ast ctx k =
+ -- lookup :: Ord k => k -> Map k a -> Maybe a
+ expr_from (Proxy::Proxy root) ast_k ctx $
+ \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
+ expr_from (Proxy::Proxy root) ast_m ctx $
+ \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
+ check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
+ check_eq_type ex ast ty_k ty_m_k $ \Refl ->
+ check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
+ k (type_maybe ty_m_a) $ Forall_Repr_with_Context $
+ \c -> map_lookup (key c) (m c)
+
+-- | Parse 'map_keys'.
+map_keys_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Map root)
+ , Eq_Type ty
+ , Expr_from ast root
+ , Lift_Type Type_Map (Type_of_Expr root)
+ , Unlift_Type Type_Map (Type_of_Expr root)
+ , Lift_Type Type_List (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
+ -> Expr_From ast (Expr_Map root) hs ret
+map_keys_from ast_m ex ast ctx k =
+ -- keys :: Map k a -> [k]
+ expr_from (Proxy::Proxy root) ast_m ctx $
+ \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
+ check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k _ty_m_a) ->
+ k (type_list ty_m_k) $ Forall_Repr_with_Context $
+ \c -> map_keys (m c)
+
+-- | Parse 'map_member'.
+map_member_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Map root)
+ , Eq_Type ty
+ , Expr_from ast root
+ , Constraint_Type Ord ty
+ , Lift_Type Type_Map (Type_of_Expr root)
+ , Unlift_Type Type_Map (Type_of_Expr root)
+ , Lift_Type Type_Bool (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_Map root) hs ret
+map_member_from ast_k ast_m ex ast ctx k =
+ -- member :: Ord k => k -> Map k a -> Bool
+ expr_from (Proxy::Proxy root) ast_k ctx $
+ \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
+ expr_from (Proxy::Proxy root) ast_m ctx $
+ \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
+ check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k _ty_m_a) ->
+ check_eq_type ex ast ty_k ty_m_k $ \Refl ->
+ check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
+ k type_bool $ Forall_Repr_with_Context $
+ \c -> map_member (key c) (m c)
+
+-- | Parse 'map_insert'.
+map_insert_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Map root)
+ , Eq_Type ty
+ , Expr_from ast root
+ , Constraint_Type Ord ty
+ , Lift_Type Type_Map (Type_of_Expr root)
+ , Unlift_Type Type_Map (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 -> ast
+ -> Expr_From ast (Expr_Map root) hs ret
+map_insert_from ast_k ast_a ast_m ex ast ctx k =
+ -- insert :: Ord k => k -> a -> Map k a -> Map k a
+ expr_from (Proxy::Proxy root) ast_k ctx $
+ \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
+ expr_from (Proxy::Proxy root) ast_a ctx $
+ \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
+ expr_from (Proxy::Proxy root) ast_m ctx $
+ \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
+ check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
+ check_eq_type ex ast ty_k ty_m_k $ \Refl ->
+ check_eq_type ex ast ty_a ty_m_a $ \Refl ->
+ check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
+ k ty_m $ Forall_Repr_with_Context $
+ \c -> map_insert (key c) (a c) (m c)
+
+-- | Parse 'map_delete'.
+map_delete_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Map root)
+ , Eq_Type ty
+ , Expr_from ast root
+ , Lift_Type Type_Map (Type_of_Expr root)
+ , Unlift_Type Type_Map (Type_of_Expr root)
+ , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Constraint_Type Ord ty
+ , Root_of_Expr root ~ root
+ ) => ast -> ast
+ -> Expr_From ast (Expr_Map root) hs ret
+map_delete_from ast_k ast_m ex ast ctx k =
+ -- delete :: Ord k => k -> Map k a -> Map k a
+ expr_from (Proxy::Proxy root) ast_k ctx $
+ \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
+ expr_from (Proxy::Proxy root) ast_m ctx $
+ \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
+ check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k _ty_m_a) ->
+ check_eq_type ex ast ty_k ty_m_k $ \Refl ->
+ check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
+ k ty_m $ Forall_Repr_with_Context $
+ \c -> map_delete (key c) (m c)
+
+-- | Parse 'map_difference'.
+map_difference_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Map root)
+ , Eq_Type ty
+ , Expr_from ast root
+ , Lift_Type Type_Map (Type_of_Expr root)
+ , Unlift_Type Type_Map (Type_of_Expr root)
+ , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Constraint_Type Ord ty
+ , Root_of_Expr root ~ root
+ ) => ast -> ast
+ -> Expr_From ast (Expr_Map root) hs ret
+map_difference_from ast_ma ast_mb ex ast ctx k =
+ -- difference :: Ord k => Map k a -> Map k b -> Map k a
+ expr_from (Proxy::Proxy root) ast_ma ctx $
+ \(ty_ma::ty h_ma) (Forall_Repr_with_Context ma) ->
+ expr_from (Proxy::Proxy root) ast_mb ctx $
+ \(ty_mb::ty h_mb) (Forall_Repr_with_Context mb) ->
+ check_type_map ex ast ty_ma $ \(Type_Type2 Proxy ty_ma_k _ty_ma_a) ->
+ check_type_map ex ast ty_mb $ \(Type_Type2 Proxy ty_mb_k _ty_mb_b) ->
+ check_eq_type ex ast ty_ma_k ty_mb_k $ \Refl ->
+ check_constraint_type ex (Proxy::Proxy Ord) ast ty_ma_k $ \Dict ->
+ k ty_ma $ Forall_Repr_with_Context $
+ \c -> map_difference (ma c) (mb c)
+
+-- | Parse 'map_foldrWithKey'.
+map_foldrWithKey_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Map root)
+ , Eq_Type ty
+ , Expr_from ast root
+ , Lift_Type Type_Fun (Type_of_Expr root)
+ , Unlift_Type Type_Fun (Type_of_Expr root)
+ , Lift_Type Type_Map (Type_of_Expr root)
+ , Unlift_Type Type_Map (Type_of_Expr root)
+ , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
+ (Error_of_Expr ast root)
+ , Constraint_Type Ord ty
+ , Root_of_Expr root ~ root
+ ) => ast -> ast -> ast
+ -> Expr_From ast (Expr_Map root) hs ret
+map_foldrWithKey_from ast_f ast_b ast_m ex ast ctx k =
+ -- foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
+ expr_from (Proxy::Proxy root) ast_f ctx $
+ \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
+ expr_from (Proxy::Proxy root) ast_b ctx $
+ \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
+ expr_from (Proxy::Proxy root) ast_m ctx $
+ \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
+ check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_k ty_f_a2b2b) ->
+ check_type_fun ex ast ty_f_a2b2b $ \(Type_Type2 Proxy ty_f_a ty_f_b2b) ->
+ check_type_fun ex ast ty_f_b2b $ \(Type_Type2 Proxy ty_f_b ty_f_b') ->
+ check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
+ check_eq_type ex ast ty_f_k ty_m_k $ \Refl ->
+ check_eq_type ex ast ty_f_a ty_m_a $ \Refl ->
+ check_eq_type ex ast ty_b ty_f_b $ \Refl ->
+ check_eq_type ex ast ty_f_b ty_f_b' $ \Refl ->
+ check_constraint_type ex (Proxy::Proxy Ord) ast ty_m_k $ \Dict ->
+ k ty_b $ Forall_Repr_with_Context $
+ \c -> map_foldrWithKey (f c) (b c) (m c)
+
-- * Type 'Expr_Map'
-- | Expression.
data Expr_Map (root:: *)
type instance Type_of_Expr (Expr_Map root) = Type_Map
type instance Sym_of_Expr (Expr_Map root) repr = (Sym_Map repr)
type instance Error_of_Expr ast (Expr_Map 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
--- /dev/null
+../HLint.hs
\ No newline at end of file
--- /dev/null
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module Expr.Map.Test where
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import qualified Control.Arrow as Arrow
+import qualified Control.Monad as Monad
+-- import qualified Data.List as List
+import qualified Data.Map.Strict as Map
+import Data.Proxy (Proxy(..))
+import Data.Text (Text)
+import qualified Data.Text as Text
+import Data.Type.Equality ((:~:)(Refl))
+import Prelude hiding (maybe, not)
+
+import Language.Symantic.Repr
+import Language.Symantic.Expr
+import Language.Symantic.Type
+
+import AST.Test
+
+-- * Expressions
+t = bool True
+f = bool False
+e1 = map_from_list $ list_zipWith (lam (lam . tuple2))
+ (list $ int Prelude.<$> [1..5])
+ (list $ (text . Text.singleton) Prelude.<$> ['a'..'e'])
+
+-- * Tests
+type Ex = Expr_Root
+ ( Expr_Lambda
+ .|. Expr_Map
+ .|. Expr_Bool
+ .|. Expr_Maybe
+ .|. Expr_List
+ .|. Expr_Eq
+ .|. Expr_Ord
+ .|. Expr_Tuple2
+ .|. Expr_Int
+ .|. Expr_Text
+ .|. Expr_Monoid
+ )
+ex_from = root_expr_from (Proxy::Proxy Ex)
+
+(==>) ast expected =
+ testCase (show ast) $
+ case ex_from ast of
+ Left err -> Left err @?= Prelude.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 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) $
+ Error_Expr_Type_mismatch ast
+ (Exists_Type ty)
+ (Exists_Type ty_expected)
+ Just Refl -> do
+ let h = host_from_expr r
+ Monad.return $
+ Right
+ ( ty
+ , h
+ , text_from_expr r
+ -- , (text_from_expr :: Repr_Text h -> Text) r
+ )
+
+tests :: TestTree
+tests = testGroup "Map"
+ [ AST "map_from_list"
+ [ AST "list_zipWith"
+ [ AST "\\"
+ [ AST "x" []
+ , AST "Int" []
+ , AST "\\"
+ [ AST "y" []
+ , AST "Text" []
+ , AST "(,)"
+ [ AST "var" [AST "x" []]
+ , AST "var" [AST "y" []]
+ ]
+ ]
+ ]
+ , AST "list"
+ [ AST "Int" []
+ , AST "int" [AST "1" []]
+ , AST "int" [AST "2" []]
+ , AST "int" [AST "3" []]
+ ]
+ , AST "list"
+ [ AST "Text" []
+ , AST "text" [AST "a" []]
+ , AST "text" [AST "b" []]
+ , AST "text" [AST "c" []]
+ ]
+ ]
+ ] ==> Right
+ ( type_map type_int type_text
+ , Map.fromList [(1, "a"), (2, "b"), (3, "c")]
+ , "map_from_list (list_zipWith (\\x0 -> (\\x1 -> (x0, x1))) [1, 2, 3] [\"a\", \"b\", \"c\"])" )
+ , AST "map_foldrWithKey"
+ [ AST "\\"
+ [ AST "k" []
+ , AST "Int" []
+ , AST "\\"
+ [ AST "v" []
+ , AST "Text" []
+ , AST "\\"
+ [ AST "a" []
+ , AST "(,)" [AST "Int" [], AST "Text" []]
+ , AST "(,)"
+ [ AST "+"
+ [ AST "var" [AST "k" []]
+ , AST "fst" [ AST "var" [AST "a" []] ]
+ ]
+ , AST "mappend"
+ [ AST "var" [AST "v" []]
+ , AST "snd" [ AST "var" [AST "a" []] ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ , AST "(,)"
+ [ AST "int" [AST "0" []]
+ , AST "text" [AST "" []]
+ ]
+ , AST "map_from_list"
+ [ AST "list_zipWith"
+ [ AST "\\"
+ [ AST "x" []
+ , AST "Int" []
+ , AST "\\"
+ [ AST "y" []
+ , AST "Text" []
+ , AST "(,)"
+ [ AST "var" [AST "x" []]
+ , AST "var" [AST "y" []]
+ ]
+ ]
+ ]
+ , AST "list"
+ [ AST "Int" []
+ , AST "int" [AST "1" []]
+ , AST "int" [AST "2" []]
+ , AST "int" [AST "3" []]
+ ]
+ , AST "list"
+ [ AST "Text" []
+ , AST "text" [AST "a" []]
+ , AST "text" [AST "b" []]
+ , AST "text" [AST "c" []]
+ ]
+ ]
+ ]
+ ] ==> Right
+ ( type_tuple2 type_int type_text
+ , (6, "abc")
+ , "map_foldrWithKey (\\x0 -> (\\x1 -> (\\x2 -> (x0 + fst x2, mappend x1 (snd x2))))) (0, \"\") (map_from_list (list_zipWith (\\x0 -> (\\x1 -> (x0, x1))) [1, 2, 3] [\"a\", \"b\", \"c\"]))" )
+ ]
-- | Expression for 'Maybe'.
module Language.Symantic.Expr.Maybe where
+import qualified Data.Function as Fun
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (maybe)
Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
Right (Exists_Type ty_a) ->
k (type_maybe ty_a) $ Forall_Repr_with_Context $
- const nothing
+ Fun.const nothing
-- | Parse 'just'.
just_from
just_from ast_a _ex _ast ctx k =
expr_from (Proxy::Proxy root) ast_a ctx $
\(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
- k (type_maybe ty_a) $ Forall_Repr_with_Context $
- \c -> just (a c)
+ k (type_maybe ty_a) $ Forall_Repr_with_Context $
+ \c -> just (a c)
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `Arrow.left` expected
+ Left err -> Left err @?= Prelude.snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
module Language.Symantic.Expr.Monad where
import Control.Monad (Monad)
--- import qualified Control.Monad as Monad
+import qualified Data.Function as Fun
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding ((<$>), Monad(..))
type instance Type_of_Expr (Expr_Monad root) = No_Type
type instance Sym_of_Expr (Expr_Monad root) repr = (Sym_Monad repr)
type instance Error_of_Expr ast (Expr_Monad root) = No_Error_Expr
-instance Constraint_Type1 Monad (Type_Type0 px root)
instance Constraint_Type1 Monad (Type_Var1 root)
return_from
-> Expr_From ast (Expr_Monad 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 $
+ either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
type1_from (Proxy::Proxy ty) ast_f $ \_f ty_f -> Right $
expr_from (Proxy::Proxy root) ast_a ctx $
\(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `Arrow.left` expected
+ Left err -> Left err @?= Prelude.snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
import qualified Expr.Foldable.Test as Foldable
import qualified Expr.Traversable.Test as Traversable
import qualified Expr.Monad.Test as Monad
+import qualified Expr.Map.Test as Map
tests :: TestTree
tests =
, Foldable.tests
, Traversable.tests
, Monad.tests
+ , Map.tests
]
type instance Type_of_Expr (Expr_Traversable root) = No_Type
type instance Sym_of_Expr (Expr_Traversable root) repr = (Sym_Traversable repr)
type instance Error_of_Expr ast (Expr_Traversable root) = No_Error_Expr
-instance Constraint_Type1 Traversable (Type_Type0 px root)
instance Constraint_Type1 Traversable (Type_Var1 root)
traverse_from
(==>) ast expected =
testCase (show ast) $
case ex_from ast of
- Left err -> Left err @?= snd `Arrow.left` expected
+ Left err -> Left err @?= Prelude.snd `Arrow.left` expected
Right (Exists_Type_and_Repr ty (Forall_Repr r)) ->
case expected of
Left (_, err) -> Right ("…"::String) @?= Left err
module Language.Symantic.Expr.Tuple where
import Data.Proxy (Proxy(..))
-import Prelude hiding (maybe)
+import Prelude hiding (maybe, fst, snd)
import Language.Symantic.Type
import Language.Symantic.Trans.Common
-- | Symantic.
class Sym_Tuple2 repr where
tuple2 :: repr a -> repr b -> repr (a, b)
+ fst :: repr (a, b) -> repr a
+ snd :: repr (a, b) -> repr b
+
default tuple2 :: Trans t repr => t repr a -> t repr b -> t repr (a, b)
+ default fst :: Trans t repr => t repr (a, b) -> t repr a
+ default snd :: Trans t repr => t repr (a, b) -> t repr b
+
tuple2 = trans_map2 tuple2
+ fst = trans_map1 fst
+ snd = trans_map1 snd
-- * Type 'Expr_Tuple2'
-- | Expression.
type instance Sym_of_Expr (Expr_Tuple2 root) repr = (Sym_Tuple2 repr)
type instance Error_of_Expr ast (Expr_Tuple2 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
expr_from (Proxy::Proxy root) ast_b ctx $
\(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
k (type_tuple2 ty_a ty_b) $ Forall_Repr_with_Context $
- \c -> tuple2 (a c) (b c)
+ \c -> tuple2 (a c) (b c)
+
+-- | Parse 'fst'.
+fst_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
+ , Eq_Type ty
+ , Expr_from ast root
+ , Lift_Type Type_Tuple2 (Type_of_Expr root)
+ , Unlift_Type Type_Tuple2 (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
+ -> Expr_From ast (Expr_Tuple2 root) hs ret
+fst_from ast_t ex ast ctx k =
+ expr_from (Proxy::Proxy root) ast_t ctx $
+ \(ty_t::ty h_t) (Forall_Repr_with_Context t) ->
+ check_type_tuple2 ex ast ty_t $ \(Type_Type2 _ ty_a _ty_b) ->
+ k ty_a $ Forall_Repr_with_Context $
+ \c -> fst (t c)
+
+-- | Parse 'snd'.
+snd_from
+ :: forall root ty ast hs ret.
+ ( ty ~ Type_Root_of_Expr (Expr_Tuple2 root)
+ , Eq_Type ty
+ , Expr_from ast root
+ , Lift_Type Type_Tuple2 (Type_of_Expr root)
+ , Unlift_Type Type_Tuple2 (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
+ -> Expr_From ast (Expr_Tuple2 root) hs ret
+snd_from ast_t ex ast ctx k =
+ expr_from (Proxy::Proxy root) ast_t ctx $
+ \(ty_t::ty h_t) (Forall_Repr_with_Context t) ->
+ check_type_tuple2 ex ast ty_t $ \(Type_Type2 _ _ty_a ty_b) ->
+ k ty_b $ Forall_Repr_with_Context $
+ \c -> snd (t c)
list l1 `Dup` list l2
list_filter (f1 `Dup` f2) (l1 `Dup` l2) =
list_filter f1 l1 `Dup` list_filter f2 l2
+ list_zipWith (f1 `Dup` f2) (la1 `Dup` la2) (lb1 `Dup` lb2) =
+ list_zipWith f1 la1 lb1 `Dup` list_zipWith f2 la2 lb2
+ list_reverse (l1 `Dup` l2) =
+ list_reverse l1 `Dup` list_reverse l2
instance -- Sym_Maybe
( Sym_Maybe r1
, Sym_Maybe r2
) => Sym_Tuple2 (Dup r1 r2) where
tuple2 (a1 `Dup` a2) (b1 `Dup` b2) =
tuple2 a1 b1 `Dup` tuple2 a2 b2
+ fst (t1 `Dup` t2) = fst t1 `Dup` fst t2
+ snd (t1 `Dup` t2) = snd t1 `Dup` snd t2
instance -- Sym_Map
( Sym_Map r1
, Sym_Map r2
map_from_list l1 `Dup` map_from_list l2
mapWithKey (f1 `Dup` f2) (m1 `Dup` m2) =
mapWithKey f1 m1 `Dup` mapWithKey f2 m2
+ map_lookup (k1 `Dup` k2) (m1 `Dup` m2) =
+ map_lookup k1 m1 `Dup` map_lookup k2 m2
+ map_keys (m1 `Dup` m2) =
+ map_keys m1 `Dup` map_keys m2
+ map_member (k1 `Dup` k2) (m1 `Dup` m2) =
+ map_member k1 m1 `Dup` map_member k2 m2
+ map_insert (k1 `Dup` k2) (a1 `Dup` a2) (m1 `Dup` m2) =
+ map_insert k1 a1 m1 `Dup` map_insert k2 a2 m2
+ map_delete (k1 `Dup` k2) (m1 `Dup` m2) =
+ map_delete k1 m1 `Dup` map_delete k2 m2
+ map_difference (ma1 `Dup` ma2) (mb1 `Dup` mb2) =
+ map_difference ma1 mb1 `Dup` map_difference ma2 mb2
+ map_foldrWithKey (f1 `Dup` f2) (b1 `Dup` b2) (m1 `Dup` m2) =
+ map_foldrWithKey f1 b1 m1 `Dup` map_foldrWithKey f2 b2 m2
instance -- Sym_Functor
( Sym_Functor r1
, Sym_Functor r2
import Data.Functor as Functor
import Data.Monoid as Monoid
import Data.Traversable as Traversable
+import qualified Data.Tuple as Tuple
import qualified Data.Bool as Bool
import qualified Data.List as List
import qualified Data.Map.Strict as Map
instance Sym_Ord Repr_Host where
compare = liftM2 Prelude.compare
instance Sym_List Repr_Host where
- list_empty = return []
- list_cons = liftM2 (:)
- list = sequence
- list_filter = liftM2 List.filter
+ list_empty = return []
+ list_cons = liftM2 (:)
+ list = sequence
+ list_filter = liftM2 List.filter
+ list_zipWith = liftM3 List.zipWith
+ list_reverse = liftM List.reverse
instance Sym_Tuple2 Repr_Host where
tuple2 = liftM2 (,)
+ fst = liftM Tuple.fst
+ snd = liftM Tuple.snd
instance Sym_Map Repr_Host where
- map_from_list = liftM Map.fromList
- mapWithKey = liftM2 Map.mapWithKey
+ map_from_list = liftM Map.fromList
+ mapWithKey = liftM2 Map.mapWithKey
+ map_lookup = liftM2 Map.lookup
+ map_keys = liftM Map.keys
+ map_member = liftM2 Map.member
+ map_insert = liftM3 Map.insert
+ map_delete = liftM2 Map.delete
+ map_difference = liftM2 Map.difference
+ map_foldrWithKey = liftM3 Map.foldrWithKey
instance Sym_Functor Repr_Host where
fmap = liftM2 (Functor.<$>)
instance Expr.Sym_Monad Repr_Host where
import Data.Text (Text)
import qualified Data.Text as Text
-import Prelude hiding (and, not, or, Monad(..))
+import Prelude hiding (and, not, or, Monad(..), id)
import Language.Symantic.Repr
import Language.Symantic.Expr
list l = Repr_Text $ \_p v ->
let p' = precedence_Toplevel in
"[" <> Text.intercalate ", " ((\(Repr_Text a) -> a p' v) Prelude.<$> l) <> "]"
- list_filter = repr_text_app2 "list_filter"
+ list_filter = repr_text_app2 "list_filter"
+ list_zipWith = repr_text_app3 "list_zipWith"
+ list_reverse = repr_text_app1 "list_reverse"
instance Sym_Tuple2 Repr_Text where
tuple2 (Repr_Text a) (Repr_Text b) =
Repr_Text $ \_p v ->
let p' = precedence_Toplevel in
"(" <> a p' v <> ", " <> b p' v <> ")"
+ fst = repr_text_app1 "fst"
+ snd = repr_text_app1 "snd"
instance Sym_Map Repr_Text where
- map_from_list = repr_text_app1 "map_from_list"
- mapWithKey = repr_text_app2 "mapWithKey"
+ map_from_list = repr_text_app1 "map_from_list"
+ mapWithKey = repr_text_app2 "mapWithKey"
+ map_lookup = repr_text_app2 "map_lookup"
+ map_keys = repr_text_app1 "map_keys"
+ map_member = repr_text_app2 "map_member"
+ map_insert = repr_text_app3 "map_insert"
+ map_delete = repr_text_app2 "map_delete"
+ map_difference = repr_text_app2 "map_difference"
+ map_foldrWithKey = repr_text_app3 "map_foldrWithKey"
instance Sym_Functor Repr_Text where
fmap = repr_text_app2 "fmap"
instance Sym_Applicative Repr_Text where
import qualified Expr.Functor.Test as Functor.Test
import qualified Expr.Applicative.Test as Applicative.Test
import qualified Expr.Foldable.Test as Foldable.Test
+import qualified Expr.Map.Test as Map.Test
tests :: TestTree
tests = testGroup "Text" $
, Lambda.Test.e3 ==> "let x0 = True in x0 && x0"
, Lambda.Test.e4 ==> "let x0 = \\x1 -> x1 && x1 in x0 True"
, Lambda.Test.e5 ==> "\\x0 -> (\\x1 -> x0 && x1)"
- , Lambda.Test.e6 ==> "(let x0 = True in x0) && False"
+ , Lambda.Test.e6 ==> "(let x0 = True in (\\x1 -> x1) x0) && False"
, Lambda.Test.e7 ==> "\\x0 -> x0 True && True"
, Lambda.Test.e8 ==> "\\x0 -> x0 (True && True)"
]
, testGroup "Foldable"
[ Foldable.Test.e1 ==> "foldMap (\\x0 -> [x0, x0]) [1, 2, 3]"
]
+ , testGroup "Map"
+ [ Map.Test.e1 ==> "map_from_list (list_zipWith (\\x0 -> (\\x1 -> (x0, x1))) [1, 2, 3, 4, 5] [\"a\", \"b\", \"c\", \"d\", \"e\"])"
+ ]
]
pattern Type_Bool :: Type_Bool root Bool
pattern Type_Bool = Type_Type0 Proxy
-instance -- String_from_Type
- String_from_Type (Type_Bool root) where
+instance Constraint_Type Eq (Type_Bool root) where
+ constraint_type _c Type_Type0{} = Just Dict
+instance Constraint_Type Ord (Type_Bool root) where
+ constraint_type _c Type_Type0{} = Just Dict
+instance Constraint_Type Monoid (Type_Bool root)
+instance String_from_Type (Type_Bool root) where
string_from_type _ = "Bool"
-- | Inject 'Type_Bool' within a root type.
type_bool :: Lift_Type_Root Type_Bool root => root Bool
type_bool = type_type0
-
-instance Constraint_Type Monoid (Type_Bool root)
-- | The 'Either' type.
type Type_Either = Type_Type2 (Proxy Either)
-type instance Constraint2_of (Proxy Either)
- = Constraint2_Empty
-instance Unlift_Type1 (Type_Type2 (Proxy Either)) where
+instance Unlift_Type1 Type_Either where
unlift_type1 (Type_Type2 px a b) k =
k ( Type_Type1 (Proxy::Proxy (Either a)) b
, Lift_Type1 (\(Type_Type1 _ b') -> Type_Type2 px a b')
)
-instance Eq_Type root => Eq_Type1 (Type_Type2 (Proxy Either) root) where
+instance Eq_Type root => Eq_Type1 (Type_Either root) where
eq_type1 (Type_Type2 _ a1 _b1) (Type_Type2 _ a2 _b2)
| Just Refl <- eq_type a1 a2
= Just Refl
-- * Type 'Type_Fun'
-- | The @->@ type.
-type Type_Fun
- = Type_Type2 (Proxy (->))
+type Type_Fun = Type_Type2 (Proxy (->))
-type instance Constraint2_of (Proxy (->))
- = Constraint2_Empty
-instance Unlift_Type1 (Type_Type2 (Proxy (->))) where
+instance Unlift_Type1 Type_Fun where
unlift_type1 (Type_Type2 px a b) k =
k ( Type_Type1 (Proxy::Proxy ((->) a)) b
, Lift_Type1 (\(Type_Type1 _ b') -> Type_Type2 px a b')
)
-instance Eq_Type root => Eq_Type1 (Type_Type2 (Proxy (->)) root) where
+instance Eq_Type root => Eq_Type1 (Type_Fun root) where
eq_type1 (Type_Type2 _ a1 _b1) (Type_Type2 _ a2 _b2)
| Just Refl <- eq_type a1 a2
= Just Refl
eq_type1 _ _ = Nothing
+instance Constraint_Type Eq (Type_Fun root) where
+ constraint_type _c _ = Nothing
+instance Constraint_Type Ord (Type_Fun root) where
+ constraint_type _c _ = Nothing
instance
Constraint_Type Monoid root =>
- Constraint_Type Monoid (Type_Type2 (Proxy (->)) root) where
+ Constraint_Type Monoid (Type_Fun root) where
constraint_type c (Type_Type2 _ _arg res)
| Just Dict <- constraint_type c res
= Just Dict
constraint_type _c _ = Nothing
-instance (Constraint_Type1 Functor root)
- => Constraint_Type1 Functor (Type_Type2 (Proxy (->)) root) where
+instance Constraint_Type1 Functor (Type_Fun root) where
constraint_type1 _c Type_Type2{} = Just Dict
-instance (Constraint_Type1 Applicative root)
- => Constraint_Type1 Applicative (Type_Type2 (Proxy (->)) root) where
+instance Constraint_Type1 Applicative (Type_Fun root) where
constraint_type1 _c Type_Type2{} = Just Dict
instance Constraint_Type1 Foldable (Type_Fun root)
instance Constraint_Type1 Traversable (Type_Fun root)
instance -- Eq_Type
Eq_Type root =>
- Eq_Type (Type_Type2 (Proxy (->)) root) where
+ Eq_Type (Type_Fun root) where
eq_type
(Type_Type2 _ arg1 res1)
(Type_Type2 _ arg2 res2)
pattern Type_Int :: Type_Type0 (Proxy Int) root Int
pattern Type_Int = Type_Type0 Proxy
-instance -- String_from_Type
- String_from_Type (Type_Int root) where
+instance Constraint_Type Eq (Type_Int root) where
+ constraint_type _c Type_Type0{} = Just Dict
+instance Constraint_Type Ord (Type_Int root) where
+ constraint_type _c Type_Type0{} = Just Dict
+instance Constraint_Type Monoid (Type_Int root)
+instance String_from_Type (Type_Int root) where
string_from_type _ = "Int"
-- | Inject 'Type_Int' within a root type.
type_int :: Lift_Type_Root Type_Int root => root Int
type_int = type_type0
-
-instance Constraint_Type Monoid (Type_Int root)
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Type.Map where
-import Data.Proxy
import Data.Map.Strict as Map
+import Data.Proxy
+import Data.Type.Equality ((:~:)(Refl))
import Language.Symantic.Type.Root
import Language.Symantic.Type.Type0
+import Language.Symantic.Type.Type1
import Language.Symantic.Type.Type2
-- * Type 'Type_Map'
-- | The 'Map' type.
type Type_Map = Type_Type2 (Proxy Map)
-type instance Constraint2_of (Proxy Map)
- = Constraint2_Map
-
-{- FIXME: Could not deduce (Ord k) arising from a pattern…
pattern Type_Map
- :: Ord k => root k -> root a
+ :: root k -> root a
-> Type_Type2 (Proxy Map) root (Map k a)
pattern Type_Map k a
= Type_Type2 Proxy k a
--}
-
--- ** Class 'Constraint2_Map'
-class Constraint2_Map k a
-instance Ord k => Constraint2_Map k a
+instance Unlift_Type1 Type_Map where
+ unlift_type1 (Type_Type2 px a b) k =
+ k ( Type_Type1 (Proxy::Proxy (Map a)) b
+ , Lift_Type1 (\(Type_Type1 _ b') -> Type_Type2 px a b')
+ )
+instance
+ Constraint_Type Eq root =>
+ Constraint_Type Eq (Type_Map root) where
+ constraint_type c (Type_Type2 _ k a)
+ | Just Dict <- constraint_type c k
+ , Just Dict <- constraint_type c a
+ = Just Dict
+ constraint_type _c _ = Nothing
+instance
+ Constraint_Type Ord root =>
+ Constraint_Type Ord (Type_Map root) where
+ constraint_type c (Type_Type2 _ k a)
+ | Just Dict <- constraint_type c k
+ , Just Dict <- constraint_type c a
+ = Just Dict
+ constraint_type _c _ = Nothing
+instance
+ Constraint_Type Ord root =>
+ Constraint_Type Monoid (Type_Map root) where
+ constraint_type _c (Type_Type2 _ k _a)
+ | Just Dict <- constraint_type (Proxy::Proxy Ord) k
+ = Just Dict
+ constraint_type _c _ = Nothing
+instance Constraint_Type1 Functor (Type_Map root) where
+ constraint_type1 _c Type_Type2{} = Just Dict
+instance Constraint_Type1 Traversable (Type_Map root) where
+ constraint_type1 _c Type_Type2{} = Just Dict
+instance Constraint_Type1 Foldable (Type_Map root) where
+ constraint_type1 _c Type_Type2{} = Just Dict
+instance -- Eq_Type
+ Eq_Type root =>
+ Eq_Type (Type_Map root) where
+ eq_type (Type_Type2 _px1 k1 a1) (Type_Type2 _px2 k2 a2)
+ | Just Refl <- k1 `eq_type` k2
+ , Just Refl <- a1 `eq_type` a2
+ = Just Refl
+ eq_type _ _ = Nothing
+instance -- Eq_Type1
+ Eq_Type root =>
+ Eq_Type1 (Type_Map root) where
+ eq_type1 (Type_Type2 _px1 k1 _a1) (Type_Type2 _px2 k2 _a2)
+ | Just Refl <- k1 `eq_type` k2
+ = Just Refl
+ eq_type1 _ _ = Nothing
instance -- String_from_Type
String_from_Type root =>
String_from_Type (Type_Map root) where
-- | Inject 'Type_Map' within a root type.
type_map
:: forall root h_k h_a.
- (Lift_Type_Root Type_Map root, Ord h_k)
+ (Lift_Type_Root Type_Map root)
=> root h_k -> root h_a
-> root (Map h_k h_a)
type_map k a = lift_type_root (Type_Type2 Proxy k a
-- | The 'Maybe' type.
type Type_Maybe = Type_Type1 (Proxy Maybe)
-pattern Type_Map :: root a -> Type_Maybe root (Maybe a)
-pattern Type_Map a = Type_Type1 Proxy a
+pattern Type_Maybe :: root a -> Type_Maybe root (Maybe a)
+pattern Type_Maybe a = Type_Type1 Proxy a
instance Constraint_Type Eq root => Constraint_Type Eq (Type_Maybe root) where
constraint_type c (Type_Type1 _ a)
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
pattern Type_Ordering :: Type_Ordering root Ordering
pattern Type_Ordering = Type_Type0 Proxy
-instance -- String_from_Type
- String_from_Type (Type_Ordering root) where
+instance Constraint_Type Eq (Type_Ordering root) where
+ constraint_type _c Type_Type0{} = Just Dict
+instance Constraint_Type Ord (Type_Ordering root) where
+ constraint_type _c Type_Type0{} = Just Dict
+instance Constraint_Type Monoid (Type_Ordering root)
+instance String_from_Type (Type_Ordering root) where
string_from_type _ = "Ordering"
-- | Inject 'Type_Ordering' within a root type.
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
import Data.Text (Text)
import Language.Symantic.Type.Root
import Language.Symantic.Type.Type0
+import Language.Symantic.Type.Type1
-- * Type 'Type_Text'
-- | The 'Text' type.
pattern Type_Text :: Type_Type0 (Proxy Text) root Text
pattern Type_Text = Type_Type0 Proxy
+instance Constraint_Type Eq (Type_Text root) where
+ constraint_type _c Type_Type0{} = Just Dict
+instance Constraint_Type Ord (Type_Text root) where
+ constraint_type _c Type_Type0{} = Just Dict
+instance Constraint_Type Monoid (Type_Text root) where
+ constraint_type _c Type_Type0{} = Just Dict
+instance Constraint_Type1 Functor (Type_Text root)
+instance Constraint_Type1 Applicative (Type_Text root)
+instance Constraint_Type1 Foldable (Type_Text root)
+instance Constraint_Type1 Traversable (Type_Text root)
+instance Constraint_Type1 Monad (Type_Text root)
instance -- String_from_Type
String_from_Type (Type_Text root) where
string_from_type _ = "Text"
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Language.Symantic.Type.Tuple where
import Data.Proxy
+import Data.Type.Equality ((:~:)(Refl))
import Language.Symantic.Type.Root
import Language.Symantic.Type.Type0
+import Language.Symantic.Type.Type1
import Language.Symantic.Type.Type2
-- * Type 'Type_Tuple2'
-- | The @(,)@ type.
type Type_Tuple2 = Type_Type2 (Proxy (,))
-type instance Constraint2_of (Proxy (,))
- = Constraint2_Empty
-
pattern Type_Tuple2
:: root a -> root b
-> Type_Tuple2 root ((,) a b)
pattern Type_Tuple2 a b
= Type_Type2 Proxy a b
+instance Unlift_Type1 Type_Tuple2 where
+ unlift_type1 (Type_Type2 px a b) k =
+ k ( Type_Type1 (Proxy::Proxy ((,) a)) b
+ , Lift_Type1 (\(Type_Type1 _ b') -> Type_Type2 px a b')
+ )
+instance
+ Constraint_Type Eq root =>
+ Constraint_Type Eq (Type_Tuple2 root) where
+ constraint_type c (Type_Type2 _ a b)
+ | Just Dict <- constraint_type c a
+ , Just Dict <- constraint_type c b
+ = Just Dict
+ constraint_type _c _ = Nothing
+instance
+ Constraint_Type Ord root =>
+ Constraint_Type Ord (Type_Tuple2 root) where
+ constraint_type c (Type_Type2 _ a b)
+ | Just Dict <- constraint_type c a
+ , Just Dict <- constraint_type c b
+ = Just Dict
+ constraint_type _c _ = Nothing
+instance Constraint_Type1 Functor (Type_Tuple2 root) where
+ constraint_type1 _c Type_Type2{} = Just Dict
+instance
+ Constraint_Type Monoid root =>
+ Constraint_Type1 Applicative (Type_Tuple2 root) where
+ constraint_type1 _c (Type_Type2 _ a _b)
+ | Just Dict <- constraint_type (Proxy::Proxy Monoid) a
+ = Just Dict
+ constraint_type1 _c _ = Nothing
+instance Constraint_Type1 Foldable (Type_Tuple2 root) where
+ constraint_type1 _c Type_Type2{} = Just Dict
+instance Constraint_Type1 Traversable (Type_Tuple2 root) where
+ constraint_type1 _c Type_Type2{} = Just Dict
+instance
+ Constraint_Type Monoid root =>
+ Constraint_Type Monoid (Type_Tuple2 root) where
+ constraint_type c (Type_Type2 _ a b)
+ | Just Dict <- constraint_type c a
+ , Just Dict <- constraint_type c b
+ = Just Dict
+ constraint_type _c _ = Nothing
+instance -- Eq_Type
+ Eq_Type root =>
+ Eq_Type (Type_Tuple2 root) where
+ eq_type (Type_Type2 _px1 a1 b1) (Type_Type2 _px2 a2 b2)
+ | Just Refl <- a1 `eq_type` a2
+ , Just Refl <- b1 `eq_type` b2
+ = Just Refl
+ eq_type _ _ = Nothing
+instance -- Eq_Type1
+ Eq_Type root =>
+ Eq_Type1 (Type_Tuple2 root) where
+ eq_type1 (Type_Type2 _px1 a1 _b1) (Type_Type2 _px2 a2 _b2)
+ | Just Refl <- a1 `eq_type` a2
+ = Just Refl
+ eq_type1 _ _ = Nothing
instance -- String_from_Type
String_from_Type root =>
String_from_Type (Type_Tuple2 root) where
String_from_Type (Type_Type0 (Proxy h0) root) =>
Show (Type_Type0 (Proxy h0) root h0) where
show = string_from_type
-instance Eq h0 => Constraint_Type Eq (Type_Type0 (Proxy h0) root) where
- constraint_type _c Type_Type0{} = Just Dict
-instance Ord h0 => Constraint_Type Ord (Type_Type0 (Proxy h0) root) where
- constraint_type _c Type_Type0{} = Just Dict
-- | Convenient alias to include a 'Type_Type0' within a type.
type_type0 :: forall root h0. Lift_Type_Root (Type_Type0 (Proxy h0)) root => root h0
) => Constraint_Type1 c (Type_Alt curr next root) where
constraint_type1 c (Type_Alt_Curr ty) = constraint_type1 c ty
constraint_type1 c (Type_Alt_Next ty) = constraint_type1 c ty
+instance Constraint_Type1 c (Type_Type0 px root)
-- * Class 'Type1_from'
-- | Parse given @ast@ into a 'Root_of_Type' constructor,
import Data.Maybe (isJust)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
-import GHC.Prim (Constraint)
import Language.Symantic.Lib.Data.Peano
-- import Language.Symantic.Lib.Data.Bool
-- * Type 'Type_Type2'
data Type_Type2 px (root:: * -> *) h where
Type_Type2
- :: (Constraint2_of px) a b
- => px -> root a -> root b
+ :: px -> root a -> root b
-> Type_Type2 px root ((Host2_of px) a b)
-class Constraint2_Empty a b
-instance Constraint2_Empty a b
type instance Root_of_Type (Type_Type2 px root) = root
type instance Error_of_Type ast (Type_Type2 px root) = No_Error_Type
, String_from_Type (Type_Type2 px root)
) => Show (Type_Type2 px root h) where
show = string_from_type
-instance Constraint_Type Eq (Type_Type2 px root)
-instance Constraint_Type Ord (Type_Type2 px root)
--- instance Unlift_Type1 (Type_Type2 px) -- NOTE: done case by case
--- instance Eq_Type1 (Type_Type2 px root) -- FIXME: should be doable
-- ** Type 'Host2_of'
type family Host2_of px :: * -> * -> *
type instance Host2_of (Proxy h2) = h2
-
--- ** Type 'Constraint2_of'
-type family Constraint2_of px :: (* -> * -> Constraint)
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
pattern Type_Unit :: Type_Unit root ()
pattern Type_Unit = Type_Type0 Proxy
+instance Constraint_Type Eq (Type_Unit root) where
+ constraint_type _c Type_Type0{} = Just Dict
+instance Constraint_Type Ord (Type_Unit root) where
+ constraint_type _c Type_Type0{} = Just Dict
+instance Constraint_Type Monoid (Type_Unit root)
instance -- String_from_Type
String_from_Type (Type_Unit root) where
string_from_type _ = "()"
and then interpret them at will.
.
One important drawback of this flexibility
- is the introduction of a lot of type constraints,
- so far this hasn't discouraged me… because for this
- reading the vertically-aligned source code is easier
- than its Haddock rendition.
+ is the introduction of a lot of type constraints;
+ those may be more readable directly in the source code
+ than in its Haddock rendition.
.
Your comments, problem reports, or questions are very welcome! :-)
.
Expr.Int.Test
Expr.Lambda.Test
Expr.List.Test
+ Expr.Map.Test
Expr.Maybe.Test
Expr.Monad.Test
Expr.Test
ghc-options: -fprof-auto
build-depends:
base >= 4.6 && < 5
+ , containers
, transformers
, tasty >= 0.11
, tasty-hunit
sourcephile / git / haskell / symantic.git / commitdiff