{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Compiling.Applicative.Test where
import Test.Tasty
-import Test.Tasty.HUnit
-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))
-import Prelude hiding ((&&), not, (||))
import Language.Symantic.Typing
import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
+import Compiling.Term.Test
-- * Tests
type Ifaces =
, Proxy Maybe
, Proxy Applicative
]
-type Consts = Consts_of_Ifaces Ifaces
-
-(==>) (ast::Syntax Text) expected =
- testCase (show ast) $
- case root_term_from ast of
- Left err -> Left err @?= Prelude.snd `Arrow.left` expected
- Right (ETerm ty (Term te)::ETerm Ifaces) ->
- case expected of
- Left (_, err) -> Right ("…"::Text) @?= Left err
- Right (ty_expected::Type Consts h, _::h, _::Text) ->
- (Monad.>>= (@?= (\(_::Type Consts h, err) -> err) `Arrow.left` expected)) $
- case ty `eq_type` ty_expected of
- Nothing -> Monad.return $ Left $
- Error_Term_Type_mismatch
- (At Nothing $ EType ty)
- (At Nothing $ EType ty_expected)
- Just Refl -> do
- let h = host_from_term te
- Monad.return $
- Right
- ( ty
- , h
- , text_from_term te
- -- , (text_from_expr :: Repr_Text h -> Text) r
- )
+(==>) = test_term_from (Proxy::Proxy Ifaces)
tests :: TestTree
tests = testGroup "Applicative"
{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Compiling.Bool.Test where
import Test.Tasty
-import Test.Tasty.HUnit
-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))
import Prelude hiding ((&&), not, (||))
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
+import Compiling.Term.Test
-- * Class 'Sym_Bool_Vars'
[ Proxy (->)
, Proxy Bool
]
-type Consts = Consts_of_Ifaces Ifaces
-
-(==>) (ast::Syntax Text) expected =
- testCase (show ast) $
- case root_term_from ast of
- Left err -> Left err @?= Prelude.snd `Arrow.left` expected
- Right (ETerm ty (Term te)::ETerm Ifaces) ->
- case expected of
- Left (_, err) -> Right ("…"::Text) @?= Left err
- Right (ty_expected::Type Consts h, _::h, _::Text) ->
- (Monad.>>= (@?= (\(_::Type Consts h, err) -> err) `Arrow.left` expected)) $
- case ty `eq_type` ty_expected of
- Nothing -> Monad.return $ Left $
- Error_Term_Type_mismatch
- (At Nothing $ EType ty)
- (At Nothing $ EType ty_expected)
- Just Refl -> do
- let h = host_from_term te
- Monad.return $
- Right
- ( ty
- , h
- , text_from_term te
- -- , (text_from_expr :: Repr_Text h -> Text) r
- )
+(==>) = test_term_from (Proxy::Proxy Ifaces)
tests :: TestTree
tests = testGroup "Bool" $
where
char_from =
let ty = tyChar in
- from_lex (Text.pack $ show_type ty) ast $ \(i::Char) as ->
- k as ty $ TermLC $ Fun.const $ char i
+ from_ast1 ast $ \ast_lit as ->
+ from_lex (Text.pack $ show_type ty) ast_lit $ \(lit::Char) ->
+ k as ty $ TermLC $ Fun.const $ char lit
char_toUpper_from =
from_ast0 ast $ \_ as ->
k as (tyChar ~> tyChar) $ TermLC $
--- /dev/null
+{-# LANGUAGE DataKinds #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# OPTIONS_GHC -O0 #-} -- speedup compile-time…
+module Compiling.Foldable.Test where
+
+import Test.Tasty
+
+import Data.Proxy (Proxy(..))
+
+import Language.Symantic.Typing
+import Language.Symantic.Compiling
+import Compiling.Term.Test
+
+-- * Tests
+type Ifaces =
+ [ Proxy (->)
+ , Proxy []
+ , Proxy Int
+ , Proxy Foldable
+ ]
+(==>) = test_term_from (Proxy::Proxy Ifaces)
+
+tests :: TestTree
+tests = testGroup "Foldable"
+ [ Syntax "foldMap"
+ [ syLam (Syntax "x" []) syInt $
+ Syntax "list"
+ [ syInt
+ , Syntax "x" []
+ , Syntax "x" []
+ ]
+ , Syntax "list"
+ [ syInt
+ , Syntax "int" [Syntax "1" []]
+ , Syntax "int" [Syntax "2" []]
+ , Syntax "int" [Syntax "3" []]
+ ]
+ ] ==> Right
+ ( tyList :$ tyInt
+ , [1, 1, 2, 2, 3, 3]
+ , "foldMap (\\x0 -> [x0, x0]) [1, 2, 3]" )
+ ]
{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
module Compiling.Functor.Test where
import Test.Tasty
-import Test.Tasty.HUnit
-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))
import Prelude hiding ((&&), not, (||))
import Language.Symantic.Typing
import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
+import Compiling.Term.Test
-- * Tests
type Ifaces =
, Proxy Bool
, Proxy Maybe
, Proxy Functor
- -- , Proxy Foldable
- -- , Proxy Traversable
]
-type Consts = Consts_of_Ifaces Ifaces
-
-(==>) (ast::Syntax Text) expected =
- testCase (show ast) $
- case root_term_from ast of
- Left err -> Left err @?= Prelude.snd `Arrow.left` expected
- Right (ETerm ty (Term te)::ETerm Ifaces) ->
- case expected of
- Left (_, err) -> Right ("…"::Text) @?= Left err
- Right (ty_expected::Type Consts h, _::h, _::Text) ->
- (Monad.>>= (@?= (\(_::Type Consts h, err) -> err) `Arrow.left` expected)) $
- case ty `eq_type` ty_expected of
- Nothing -> Monad.return $ Left $
- Error_Term_Type_mismatch
- (At Nothing $ EType ty)
- (At Nothing $ EType ty_expected)
- Just Refl -> do
- let h = host_from_term te
- Monad.return $
- Right
- ( ty
- , h
- , text_from_term te
- -- , (text_from_expr :: Repr_Text h -> Text) r
- )
+(==>) = test_term_from (Proxy::Proxy Ifaces)
tests :: TestTree
tests = testGroup "Functor"
where
int_from =
let ty = tyInt in
- from_lex (Text.pack $ show_type ty) ast $ \(i::Int) as ->
- k as ty $ TermLC $ Fun.const $ int i
+ from_ast1 ast $ \ast_lit as ->
+ from_lex (Text.pack $ show_type ty) ast_lit $ \(lit::Int) ->
+ k as ty $ TermLC $ Fun.const $ int lit
-- | The 'Int' 'Type'
tyInt :: Inj_Const cs Int => Type cs Int
where
integer_from =
let ty = tyInteger in
- from_lex (Text.pack $ show_type ty) ast $ \(i::Integer) as ->
- k as ty $ TermLC $ Fun.const $ integer i
+ from_ast1 ast $ \ast_lit as ->
+ from_lex (Text.pack $ show_type ty) ast_lit $ \(lit::Integer) ->
+ k as ty $ TermLC $ Fun.const $ integer lit
-- | The 'Integer' 'Type'
tyInteger :: Inj_Const cs Integer => Type cs Integer
-- div :: Integral i => i -> i -> i
-- mod :: Integral i => i -> i -> i
from_ast1 ast $ \ast_a as ->
- term_from ast_a ctx $ \ty_a (TermLC x) ->
- check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
- k as (ty_a ~> ty_a) $ TermLC $
- \c -> lam $ \y -> op (x c) y
+ term_from ast_a ctx $ \ty_a (TermLC x) ->
+ check_constraint (At (Just ast_a) (tyIntegral :$ ty_a)) $ \Con ->
+ k as (ty_a ~> ty_a) $ TermLC $
+ \c -> lam $ \y -> op (x c) y
integral_op2t2_from
(op::forall term a. (Sym_Integral term, Integral a)
=> term a -> term a -> term (a, a)) =
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
+{-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
-- | Symantic for '[]'.
module Language.Symantic.Compiling.List where
type instance Consts_of_Iface (Proxy []) = Proxy [] ': Consts_imported_by []
type instance Consts_imported_by [] =
[ Proxy Applicative
+ , Proxy Bool
, Proxy Eq
, Proxy Foldable
, Proxy Functor
= Just $ case () of
_ | Just Refl <- proj_const q (Proxy::Proxy Eq)
, Just Con <- proj_con (t :$ a) -> Just Con
- | Just Refl <- proj_const q (Proxy::Proxy Monoid)
- , Just Con <- proj_con (t :$ a) -> Just Con
+ | Just Refl <- proj_const q (Proxy::Proxy Monoid) -> Just Con
| Just Refl <- proj_const q (Proxy::Proxy Ord)
, Just Con <- proj_con (t :$ a) -> Just Con
_ -> Nothing
-- * Class 'Sym_Map'
class Sym_Map term where
map_fromList :: Ord k => term [(k, a)] -> term (Map k a)
- mapWithKey :: term (k -> a -> b) -> term (Map k a) -> term (Map k b)
+ map_mapWithKey :: term (k -> a -> b) -> term (Map k a) -> term (Map k b)
map_lookup :: Ord k => term k -> term (Map k a) -> term (Maybe a)
map_keys :: term (Map k a) -> term [k]
map_member :: Ord k => term k -> term (Map k a) -> term Bool
map_foldrWithKey :: term (k -> a -> b -> b) -> term b -> term (Map k a) -> term b
default map_fromList :: (Trans t term, Ord k) => t term [(k, a)] -> t term (Map k a)
- default mapWithKey :: Trans t term => t term (k -> a -> b) -> t term (Map k a) -> t term (Map k b)
+ default map_mapWithKey :: Trans t term => t term (k -> a -> b) -> t term (Map k a) -> t term (Map k b)
default map_lookup :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term (Maybe a)
default map_keys :: Trans t term => t term (Map k a) -> t term [k]
default map_member :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term Bool
default map_foldrWithKey :: Trans t term => t term (k -> a -> b -> b) -> t term b -> t term (Map k a) -> t term b
map_fromList = trans_map1 map_fromList
- mapWithKey = trans_map2 mapWithKey
+ map_mapWithKey = trans_map2 map_mapWithKey
map_lookup = trans_map2 map_lookup
map_keys = trans_map1 map_keys
map_member = trans_map2 map_member
instance Sym_Map HostI where
map_fromList = liftM Map.fromList
- mapWithKey = liftM2 Map.mapWithKey
+ map_mapWithKey = liftM2 Map.mapWithKey
map_lookup = liftM2 Map.lookup
map_keys = liftM Map.keys
map_member = liftM2 Map.member
map_difference = liftM2 Map.difference
map_foldrWithKey = liftM3 Map.foldrWithKey
instance Sym_Map TextI where
- map_fromList = textI_app1 "map_fromList"
- mapWithKey = textI_app2 "mapWithKey"
- map_lookup = textI_app2 "map_lookup"
- map_keys = textI_app1 "map_keys"
- map_member = textI_app2 "map_member"
- map_insert = textI_app3 "map_insert"
- map_delete = textI_app2 "map_delete"
- map_difference = textI_app2 "map_difference"
- map_foldrWithKey = textI_app3 "map_foldrWithKey"
+ map_fromList = textI_app1 "Map.fromList"
+ map_mapWithKey = textI_app2 "Map.mapWithKey"
+ map_lookup = textI_app2 "Map.lookup"
+ map_keys = textI_app1 "Map.keys"
+ map_member = textI_app2 "Map.member"
+ map_insert = textI_app3 "Map.insert"
+ map_delete = textI_app2 "Map.delete"
+ map_difference = textI_app2 "Map.difference"
+ map_foldrWithKey = textI_app3 "Map.foldrWithKey"
instance (Sym_Map r1, Sym_Map r2) => Sym_Map (DupI r1 r2) where
map_fromList = dupI1 sym_Map map_fromList
- mapWithKey = dupI2 sym_Map mapWithKey
+ map_mapWithKey = dupI2 sym_Map map_mapWithKey
map_lookup = dupI2 sym_Map map_lookup
map_keys = dupI1 sym_Map map_keys
map_member = dupI2 sym_Map map_member
term_fromI ast ctx k =
case ast_lexem ast of
"Map.fromList" -> map_fromList_from
- "mapWithKey" -> mapWithKey_from
- "map_lookup" -> map_lookup_from
- "map_keys" -> map_keys_from
- "map_member" -> map_member_from
- "map_insert" -> map_insert_from
- "map_delete" -> map_delete_from
- "map_difference" -> map_difference_from
- "map_foldrWithKey" -> map_foldrWithKey_from
+ "Map.mapWithKey" -> mapWithKey_from
+ "Map.lookup" -> map_lookup_from
+ "Map.keys" -> map_keys_from
+ "Map.member" -> map_member_from
+ "Map.insert" -> map_insert_from
+ "Map.delete" -> map_delete_from
+ "Map.difference" -> map_difference_from
+ "Map.foldrWithKey" -> map_foldrWithKey_from
_ -> Left $ Error_Term_unsupported
where
map_fromList_from =
k as ((tyMap :$ ty_k) :$ ty_a) $ TermLC $
\c -> map_fromList (l c)
mapWithKey_from =
- -- mapWithKey :: (k -> a -> b) -> Map k a -> Map k b
+ -- map_mapWithKey :: (k -> a -> b) -> Map k a -> Map k b
from_ast1 ast $ \ast_k2a2b as ->
term_from ast_k2a2b ctx $ \ty_k2a2b (TermLC k2a2b) ->
check_type2 tyFun ast_k2a2b ty_k2a2b $ \Refl ty_k ty_a2b ->
check_type2 tyFun ast_k2a2b ty_a2b $ \Refl ty_a ty_b ->
k as ((tyMap :$ ty_k) :$ ty_a ~> (tyMap :$ ty_k) :$ ty_b) $ TermLC $
- \c -> lam $ mapWithKey (k2a2b c)
+ \c -> lam $ map_mapWithKey (k2a2b c)
map_lookup_from =
-- lookup :: Ord k => k -> Map k a -> Maybe a
from_ast2 ast $ \ast_k ast_m as ->
--- /dev/null
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# OPTIONS_GHC -O0 #-} -- speedup compile-time…
+module Compiling.Map.Test where
+
+import Test.Tasty
+
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import Data.Proxy (Proxy(..))
+import Data.Text (Text)
+import qualified Data.Text as Text
+import Prelude hiding (zipWith)
+
+import Language.Symantic.Typing
+import Language.Symantic.Compiling.Bool
+import Language.Symantic.Compiling.Map
+import Language.Symantic.Compiling.List
+import Language.Symantic.Compiling.Term
+import Language.Symantic.Compiling.Tuple2
+import Language.Symantic.Compiling.Int
+import Language.Symantic.Compiling.Text
+import Compiling.Term.Test
+
+-- * Terms
+t = bool True
+f = bool False
+e1 = map_fromList $ zipWith (lam (lam . tuple2))
+ (list $ int Prelude.<$> [1..5])
+ (list $ (text . Text.singleton) Prelude.<$> ['a'..'e'])
+
+-- * Tests
+type Ifaces =
+ [ Proxy (->)
+ , Proxy []
+ , Proxy Int
+ , Proxy Map
+ , Proxy Text
+ , Proxy (,)
+ , Proxy Num
+ , Proxy Monoid
+ ]
+(==>) = test_term_from (Proxy::Proxy Ifaces)
+
+tests :: TestTree
+tests = testGroup "Map"
+ [ Syntax "Map.fromList"
+ [ Syntax "zipWith"
+ [ syLam (Syntax "x" []) syInt $
+ syLam (Syntax "y" []) syText $
+ Syntax "(,)"
+ [ Syntax "x" []
+ , Syntax "y" []
+ ]
+ , Syntax "list"
+ [ syInt
+ , Syntax "int" [Syntax "1" []]
+ , Syntax "int" [Syntax "2" []]
+ , Syntax "int" [Syntax "3" []]
+ ]
+ , Syntax "list"
+ [ syText
+ , Syntax "text" [Syntax "\"a\"" []]
+ , Syntax "text" [Syntax "\"b\"" []]
+ , Syntax "text" [Syntax "\"c\"" []]
+ ]
+ ]
+ ] ==> Right
+ ( (tyMap :$ tyInt) :$ tyText
+ , Map.fromList [(1, "a"), (2, "b"), (3, "c")]
+ , "Map.fromList (((\\x0 -> (\\x1 -> zipWith (\\x2 -> (\\x3 -> (x2, x3))) x0 x1)) [1, 2, 3]) [\"a\", \"b\", \"c\"])" )
+ , Syntax "Map.foldrWithKey"
+ [ syLam (Syntax "k" []) syInt $
+ syLam (Syntax "v" []) syText $
+ syLam (Syntax "a" []) (syTuple2 [syInt, syText]) $
+ syTuple2
+ [ Syntax "+"
+ [ Syntax "k" []
+ , Syntax "fst" [ Syntax "a" [] ]
+ ]
+ , Syntax "mappend"
+ [ Syntax "v" []
+ , Syntax "snd" [ Syntax "a" [] ]
+ ]
+ ]
+ , syTuple2
+ [ Syntax "int" [Syntax "0" []]
+ , Syntax "text" [Syntax "\"\"" []]
+ ]
+ , Syntax "Map.fromList"
+ [ Syntax "zipWith"
+ [ syLam (Syntax "x" []) syInt $
+ syLam (Syntax "y" []) syText $
+ syTuple2
+ [ Syntax "x" []
+ , Syntax "y" []
+ ]
+ , Syntax "list"
+ [ syInt
+ , Syntax "int" [Syntax "1" []]
+ , Syntax "int" [Syntax "2" []]
+ , Syntax "int" [Syntax "3" []]
+ ]
+ , Syntax "list"
+ [ syText
+ , Syntax "text" [Syntax "\"a\"" []]
+ , Syntax "text" [Syntax "\"b\"" []]
+ , Syntax "text" [Syntax "\"c\"" []]
+ ]
+ ]
+ ]
+ ] ==> Right
+ ( (tyTuple2 :$ tyInt) :$ tyText
+ , (6, "abc")
+ , "((\\x0 -> (\\x1 -> Map.foldrWithKey (\\x2 -> (\\x3 -> (\\x4 -> ((\\x5 -> x2 + x5) (fst x4), (\\x5 -> mappend x3 x5) (snd x4))))) x0 x1)) (0, \"\")) (Map.fromList (((\\x0 -> (\\x1 -> zipWith (\\x2 -> (\\x3 -> (x2, x3))) x0 x1)) [1, 2, 3]) [\"a\", \"b\", \"c\"]))" )
+ ]
) => Term_fromI is (Proxy Maybe) ast where
term_fromI ast ctx k =
case ast_lexem ast of
- "maybe" -> maybe_from
- "Just" -> _Just_from
"Nothing" -> _Nothing_from
+ "Just" -> _Just_from
+ "maybe" -> maybe_from
_ -> Left $ Error_Term_unsupported
where
+ _Nothing_from =
+ -- Nothing :: Maybe a
+ from_ast1 ast $ \ast_ty_a as ->
+ either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
+ type_from ast_ty_a $ \ty_a -> Right $
+ check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
+ k as (tyMaybe :$ ty_a) $ TermLC $
+ Fun.const _Nothing
+ _Just_from =
+ -- Just :: a -> Maybe a
+ from_ast1 ast $ \ast_a as ->
+ term_from ast_a ctx $ \ty_a (TermLC a) ->
+ k as (tyMaybe :$ ty_a) $ TermLC $
+ \c -> _Just (a c)
maybe_from =
-- maybe :: b -> (a -> b) -> Maybe a -> b
from_ast2 ast $ \ast_b ast_a2b as ->
check_type (At (Just ast_a2b) ty_a2b_b) (At (Just ast_b) ty_b) $ \Refl ->
k as (tyMaybe :$ ty_a2b_a ~> ty_b) $ TermLC $
\c -> lam $ maybe (b c) (a2b c)
- _Just_from =
- -- Just :: a -> Maybe a
- from_ast1 ast $ \ast_a as ->
- term_from ast_a ctx $ \ty_a (TermLC a) ->
- k as (tyMaybe :$ ty_a) $ TermLC $
- \c -> _Just (a c)
- _Nothing_from =
- -- Nothing :: Maybe a
- from_ast1 ast $ \ast_ty_a as ->
- either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
- type_from ast_ty_a $ \ty_a -> Right $
- check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
- k as (tyMaybe :$ ty_a) $ TermLC $
- Fun.const _Nothing
-- | The 'Maybe' 'Type'
tyMaybe :: Inj_Const cs Maybe => Type cs Maybe
type instance Sym_of_Iface (Proxy Num) = Sym_Num
type instance Consts_of_Iface (Proxy Num) = Proxy Num ': Consts_imported_by Num
-type instance Consts_imported_by Num = '[]
+type instance Consts_imported_by Num =
+ '[ Proxy Integer
+ ]
instance Sym_Num HostI where
abs = liftM Prelude.abs
-> Either (Error_Term is ast) ret
-- ** Type 'Term_fromIT'
--- | Convenient type synonym defining a 'term_fromI'.
+-- | Almost like 'Term_fromT', but with the remaining 'ast_nodes'
+-- given to the continuation so that 'term_apply' can be used within
+-- the instance 'Term_fromR'@ is ls (i ': rs) ast@.
type Term_fromIT ast ctx ret is ls rs
= ast
-> LamCtx_Type is (Lexem ast) ctx
term_fromR ast ctx k =
case term_fromI ast ctx $ \as ty (TermLC te
::TermLC ctx h is ls (i ': rs)) ->
- apply ast as ctx ty (TermLC te) k of
+ term_apply ast as ctx ty (TermLC te) k of
Left Error_Term_unsupported ->
term_fromR ast ctx $ \ty (TermLC te
::TermLC ctx h is (i ': ls) rs) ->
-- | End the recursion.
instance AST ast => Term_fromR is ls '[] ast
-apply ::
+-- | Apply the given @ast@s to the given 'TermLC',
+-- or return an 'Error_Term'.
+term_apply ::
( Term_from is ast
, Inj_Const (Consts_of_Ifaces is) (->)
) => ast -> [ast]
-> TermLC ctx h' is ls rs
-> Either (Error_Term is ast) ret )
-> Either (Error_Term is ast) ret
-apply ast_f args ctx ty_f te_f@(TermLC f) k =
+term_apply ast_f args ctx ty_f te_f@(TermLC f) k =
case args of
[] -> k ty_f te_f
ast_a:as ->
term_from ast_a ctx $ \ty_a (TermLC a) ->
check_type2 tyFun ast_f ty_f $ \Refl ty_arg ty_res ->
check_type (At (Just ast_f) ty_arg) (At (Just ast_a) ty_a) $ \Refl ->
- apply ast_f as ctx ty_res (TermLC $ \c -> f c .$ a c) k
+ term_apply ast_f as ctx ty_res (TermLC $ \c -> f c .$ a c) k
-- ** Class 'Term_fromI'
-- | Handle the work of 'Term_from' for a given /interface/ @i@,
--- /dev/null
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+module Compiling.Term.Test where
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+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))
+import Prelude as P
+
+import Language.Symantic.Typing
+import Language.Symantic.Compiling
+import Language.Symantic.Interpreting
+
+test_term_from
+ :: forall is h.
+ ( Sym_of_Ifaces is HostI
+ , Sym_of_Ifaces is TextI
+ , Term_from is (Syntax Text)
+ , Eq h
+ , Show h
+ , Show_Const (Consts_of_Ifaces is)
+ ) => Proxy is -> Syntax Text
+ -> Either (Type (Consts_of_Ifaces is) h, Error_Term is (Syntax Text))
+ (Type (Consts_of_Ifaces is) h, h, Text)
+ -> TestTree
+test_term_from _is ast expected =
+ testCase (elide $ show ast) $
+ case root_term_from ast of
+ Left err -> Left err @?= P.snd `Arrow.left` expected
+ Right (ETerm ty (Term te)::ETerm is) ->
+ case expected of
+ Left (_, err) -> Right ("…"::Text) @?= Left err
+ Right (ty_expected::Type (Consts_of_Ifaces is) h, _::h, _::Text) ->
+ (Monad.>>= (@?= (\(_::Type (Consts_of_Ifaces is) h, err) -> err) `Arrow.left` expected)) $
+ case ty `eq_type` ty_expected of
+ Nothing -> Monad.return $ Left $
+ Error_Term_Type_mismatch
+ (At Nothing $ EType ty)
+ (At Nothing $ EType ty_expected)
+ Just Refl -> do
+ let h = host_from_term te
+ Monad.return $
+ Right
+ ( ty
+ , h
+ , text_from_term te
+ -- , (text_from_term :: Repr_Text h -> Text) r
+ )
+ where
+ elide s | P.length s P.> 42 = P.take 42 s P.++ ['…']
+ elide s = s
import qualified Compiling.Bool.Test as Bool
import qualified Compiling.Functor.Test as Functor
import qualified Compiling.Applicative.Test as Applicative
+import qualified Compiling.Foldable.Test as Foldable
+import qualified Compiling.Map.Test as Map
import Prelude hiding ((&&), not, (||), (==), id)
[ Bool.tests
, Functor.tests
, Applicative.tests
+ , Foldable.tests
+ , Map.tests
]
where
text_from =
let ty = tyText in
- from_lex (Text.pack $ show_type ty) ast $ \(i::Text) as ->
- k as ty $ TermLC $ Fun.const $ text i
+ from_ast1 ast $ \ast_lit as ->
+ from_lex (Text.pack $ show_type ty) ast_lit $ \(lit::Text) ->
+ k as ty $ TermLC $ Fun.const $ text lit
-- | The 'Text' 'Type'
tyText :: Inj_Const cs Text => Type cs Text
-> (t term a -> t term b -> t term c)
trans_map2 f e1 e2 = trans_lift (trans_apply e1 `f` trans_apply e2)
- -- | Convenient method to define the identity transformation for a terary symantic method.
+ -- | Convenient method to define the identity transformation for a ternary symantic method.
trans_map3
:: (term a -> term b -> term c -> term d)
-> (t term a -> t term b -> t term c -> t term d)
type instance Kind_Of (x::Kind.Type) = Kind.Type
type instance Kind_Of (x::a -> b) = Kind_Of (Any::a) -> Kind_Of (Any::b)
-data (a::k1) :~~: (b::k2) where
- HRefl :: forall k (a::k) (b::k). a :~~: b
{-
instance Show (x :~~: y) where
show _ = "HRefl"
:: ( AST ast, Lexem ast ~ Text
, Read ty, Lift_Error_Syntax err )
=> Text -> ast
- -> (ty -> [ast] -> Either (err ast) ret)
+ -> (ty -> Either (err ast) ret)
-> Either (err ast) ret
from_lex msg ast_x k =
from_ast0 ast_x $ \lex_x as ->
case reads $ Text.unpack lex_x of
- [(x, "")] -> k x as
+ [(x, "")] | null as -> k x
_ -> Left $ lift_error_syntax $
Error_Syntax_read $
At (Just ast_x) msg
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Typing.Test where
stability: experimental
synopsis: Library for Typed Tagless-Final Higher-Order Extensible DSL
tested-with: GHC==8.0.1
-version: 3.20161205
+version: 3.20161208
Source-Repository head
location: git://git.autogeree.net/symantic
hs-source-dirs: Language/Symantic
main-is: Test.hs
other-modules:
- Typing.Test
- Compiling.Test
+ Compiling.Applicative.Test
Compiling.Bool.Test
+ Compiling.Foldable.Test
Compiling.Functor.Test
- Compiling.Applicative.Test
+ Compiling.Map.Test
+ Compiling.Term.Test
+ Compiling.Test
+ Typing.Test
if flag(threaded)
ghc-options: -threaded -rtsopts -with-rtsopts=-N
if flag(dev)
sourcephile / git / haskell / symantic.git / commitdiff