Language/Symantic/Typing/Test.hs

   1 {-# LANGUAGE ScopedTypeVariables #-}
   2 {-# LANGUAGE TypeInType #-}
   3 {-# OPTIONS_GHC -fno-warn-orphans #-}
   4 module Typing.Test where
   5
   6 import Test.Tasty
   7 import Test.Tasty.HUnit
   8
   9 import Data.Text (Text)
  10 import Data.Maybe (isJust)
  11 import GHC.Exts (Constraint)
  12
  13 import Language.Symantic.Typing
  14 import Language.Symantic.Compiling
  15
  16 -- * Tests
  17 tests :: TestTree
  18 tests = testGroup "Typing" $
  19  [ testGroup "type_from" $
  20         let (==>) (sy::Syntax Text) expected =
  21                 testCase (show sy) $
  22                 (@?= EType Prelude.<$> expected) $
  23                 type_from sy (\h -> Right (EType h::EType Constants))
  24         in
  25          [ syBool ==> Right tyBool
  26          , syIO [] ==> Right tyIO
  27          , syEq [] ==> Right tyEq
  28          , syFun [syBool] ==> Right (tyFun :$ tyBool)
  29          , syEq [syBool] ==> Right (tyEq :$ tyBool)
  30          , syMonad [syIO []] ==> Right (tyMonad :$ tyIO)
  31          , syFun [syIO [syBool]] ==> Right (tyFun :$ (tyIO :$ tyBool))
  32          , (syBool .> syBool) ==> Right
  33            (tyBool ~> tyBool)
  34          , ((syBool .> syBool) .> syBool) ==> Right
  35            ((tyBool ~> tyBool) ~> tyBool)
  36          , ((syBool .> syInt) .> syBool) ==> Right
  37            ((tyBool ~> tyInt) ~> tyBool)
  38          , (syBool .> syInt .> syBool) ==> Right
  39            (tyBool ~> tyInt ~> tyBool)
  40          , ((syBool .> (syBool .> syInt)) .> syBool) ==> Right
  41            ((tyBool ~> (tyBool ~> tyInt)) ~> tyBool)
  42          , testGroup "Error_Type"
  43                  [ syFun [syIO []] ==> Left
  44                          (Error_Type_Kind_mismatch
  45                                  (At (Just $ syFun [syIO []]) $ EKind SKiType)
  46                                  (At (Just $ syIO []) $ EKind $ SKiType `SKiArrow` SKiType))
  47                  , syIO [syEq [syBool]] ==> Left
  48                          (Error_Type_Kind_mismatch
  49                                  (At (Just $ syIO [syEq [syBool]]) $ EKind SKiType)
  50                                  (At (Just $ syEq [syBool]) $ EKind $ SKiConstraint))
  51                  , Syntax "Bool" [syBool] ==> Left
  52                          (Error_Type_Kind_not_applicable
  53                                  (At (Just $ Syntax "Bool"  [syBool]) $ EKind SKiType))
  54                  , Syntax "Unknown" [] ==> Left (Error_Type_Constant_unknown $
  55                          At (Just $ Syntax "Unknown" []) "Unknown")
  56                  ]
  57          ]
  58  , testGroup "proj_con" $
  59         let (==>) (ty::Type Constants (h::Constraint)) expected =
  60                 testCase (show_type ty) $
  61                 isJust (proj_con ty) @?= expected
  62         in
  63          [ (tyEq :$ tyBool) ==> True
  64          , (tyOrd :$ tyBool) ==> True
  65          , (tyFunctor :$ tyMaybe) ==> True
  66          , (tyFunctor :$ tyIO) ==> True
  67          , (tyMonad :$ tyIO) ==> True
  68          , (tyTraversable :$ tyIO) ==> False
  69          ]
  70  ]