Language/Symantic/Typing/Test.hs

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