Language/Symantic/Typing/Test.hs

   1 {-# LANGUAGE TypeInType #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 module Typing.Test where
   4
   5 import Test.Tasty
   6 import Test.Tasty.HUnit
   7
   8 import Data.Maybe (isJust)
   9 import Data.Proxy
  10 import Data.Text (Text)
  11 import GHC.Exts (Constraint)
  12
  13 import Language.Symantic.Parsing
  14 import Language.Symantic.Typing
  15 import Language.Symantic.Compiling
  16
  17 import Parsing.Test
  18
  19 -- * Tests
  20 tests :: TestTree
  21 tests = testGroup "Typing" $
  22  [ testGroup "type_from" $
  23         let (==>) (syn::Syntax Text) expected =
  24                 let Right (tok::EToken (Syntax Text) '[Proxy Token_Type]) = tokenize_type syn in
  25                 testCase (show syn) $
  26                 (@?= EType Prelude.<$> expected) $
  27                 (type_from tok (Right . EType)
  28                  :: Either (Error_Type (Syntax Text) '[Proxy Token_Type])
  29                            (EType Constants))
  30         in
  31          [ sy @Bool ==> Right (ty @Bool)
  32          , sy @IO [] ==> Right (ty @IO)
  33          , sy @Eq [] ==> Right (ty @Eq)
  34          , sy @(->) [sy @Bool] ==> Right (ty @(->) :$ ty @Bool)
  35          , sy @Eq [sy @Bool] ==> Right (ty @Eq :$ ty @Bool)
  36          , sy @Monad [sy @IO []] ==> Right (ty @Monad :$ ty @IO)
  37          , sy @(->) [sy @IO [sy @Bool]] ==> Right (ty @(->) :$ (ty @IO :$ ty @Bool))
  38          , (sy @Bool .> sy @Bool) ==> Right
  39            (ty @Bool ~> ty @Bool)
  40          , ((sy @Bool .> sy @Bool) .> sy @Bool) ==> Right
  41            ((ty @Bool ~> ty @Bool) ~> ty @Bool)
  42          , ((sy @Bool .> sy @Int) .> sy @Bool) ==> Right
  43            ((ty @Bool ~> ty @Int) ~> ty @Bool)
  44          , (sy @Bool .> sy @Int .> sy @Bool) ==> Right
  45            (ty @Bool ~> ty @Int ~> ty @Bool)
  46          , ((sy @Bool .> (sy @Bool .> sy @Int)) .> sy @Bool) ==> Right
  47            ((ty @Bool ~> (ty @Bool ~> ty @Int)) ~> ty @Bool)
  48          , testGroup "Error_Type"
  49                  [ sy @(->) [sy @IO []] ==> Left
  50                          (Error_Type_Constraint_Kind $ Constraint_Kind_Eq
  51                                  (At (maybeRight $ tokenize_type $ sy @(->) [sy @IO []]) $ EKind SKiType)
  52                                  (At (maybeRight $ tokenize_type $ sy @IO []) $ EKind $ SKiType `SKiArrow` SKiType))
  53                  , sy @IO [sy @Eq [sy @Bool]] ==> Left
  54                          (Error_Type_Constraint_Kind $ Constraint_Kind_Eq
  55                                  (At (maybeRight $ tokenize_type $ sy @IO [sy @Eq [sy @Bool]]) $ EKind SKiType)
  56                                  (At (maybeRight $ tokenize_type $ sy @Eq [sy @Bool]) $ EKind $ SKiConstraint))
  57                  , Syntax "Bool" [sy @Bool] ==> Left
  58                          (Error_Type_Constraint_Kind $ Constraint_Kind_Arrow
  59                                  (At (maybeRight $ tokenize_type $ Syntax "Bool" [sy @Bool]) $ EKind SKiType))
  60                  , Syntax ("Unknown"::Text) [] ==> Left
  61                          (Error_Type_Constant_unknown $
  62                                 At (maybeRight $ tokenize_type $ Syntax ("Unknown"::Text) []) "Unknown")
  63                  ]
  64          ]
  65  , testGroup "proj_con" $
  66         let (==>) (typ::Type Constants (h::Constraint)) expected =
  67                 testCase (show_type typ) $
  68                 isJust (proj_con typ) @?= expected
  69         in
  70          [ (ty @Eq :$ ty @Bool) ==> True
  71          , (ty @Ord :$ ty @Bool) ==> True
  72          , (ty @Functor :$ ty @Maybe) ==> True
  73          , (ty @Functor :$ ty @IO) ==> True
  74          , (ty @Monad :$ ty @IO) ==> True
  75          , (ty @Traversable :$ ty @IO) ==> False
  76          ]
  77  ]