Language/Symantic/Typing/Test.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 -- {-# LANGUAGE KindSignatures #-}
   4 {-# LANGUAGE Rank2Types #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE NoOverloadedStrings #-}
   7 {-# LANGUAGE TypeOperators #-}
   8 {-# OPTIONS_GHC -fno-warn-orphans #-}
   9 module Typing.Test where
  10
  11 import Test.Tasty
  12 import Test.Tasty.HUnit
  13 -- import Data.Proxy
  14
  15 import Language.Symantic.Typing
  16
  17 tests :: TestTree
  18 tests = testGroup "Typing" $
  19         let (==>) (stx::Syntax String) expected =
  20                 testCase (show stx) $
  21                 (@?= EType <$> expected) $
  22                 type_from stx (Right . (EType::Type Consts ki h -> EType Consts))
  23         in
  24          [ syBool ==> Right tyBool
  25          , syFun [syBool] ==> Right (tyFun :$ tyBool)
  26          , syEq [syBool] ==> Right (tyEq :~ tyBool)
  27          , syMonad [syIO []] ==> Right (tyMonad :~ tyIO)
  28          , syFun [syIO [syBool]] ==> Right (tyFun :$ (tyIO :$ tyBool))
  29          , (syBool .> syBool) ==> Right
  30            (tyBool ~> tyBool)
  31          , ((syBool .> syBool) .> syBool) ==> Right
  32            ((tyBool ~> tyBool) ~> tyBool)
  33          , ((syBool .> syInt) .> syBool) ==> Right
  34            ((tyBool ~> tyInt) ~> tyBool)
  35          , (syBool .> syInt .> syBool) ==> Right
  36            (tyBool ~> tyInt ~> tyBool)
  37          , ((syBool .> (syBool .> syInt)) .> syBool) ==> Right
  38            ((tyBool ~> (tyBool ~> tyInt)) ~> tyBool)
  39          , testGroup "Error"
  40                  [ syTraversable [syIO []] ==> Left
  41                         (Error_Type_Constraint_missing
  42                           (At (syTraversable [syIO []]) $ EType $ tyTraversable :$ tyIO))
  43                  , syFun [syIO []] ==> Left
  44                          (Error_Type_Kind_mismatch
  45                                  (At (syFun [syIO []]) $ EKind SKiTerm)
  46                                  (At (syIO []) $ EKind $ SKiTerm `SKiArrow` SKiTerm))
  47                  , syIO [syEq [syBool]] ==> Left
  48                          (Error_Type_Kind_mismatch
  49                                  (At (syIO [syEq [syBool]]) $ EKind SKiTerm)
  50                                  (At (syEq [syBool]) $ EKind $ SKiCon))
  51                  , Syntax "Bool" [syBool] ==> Left
  52                          (Error_Type_Kind_not_applicable
  53                                  (At (Syntax "Bool"  [syBool]) $ EKind SKiTerm))
  54                  , Syntax "Unknown" [] ==> Left (Error_Type_Constant_unknown $
  55                          At (Syntax "Unknown" []) ())
  56                  ]
  57          ]