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
  14 import Data.Maybe (isJust)
  15 -- import Data.Proxy
  16 -- import GHC.Prim (Constraint)
  17
  18 import Language.Symantic.Typing
  19
  20 tests :: TestTree
  21 tests = testGroup "Typing" $
  22          [ testGroup "type_from" $
  23                 let (==>) (sy::Syntax String) expected =
  24                         testCase (show sy) $
  25                         (@?= EType <$> expected) $
  26                         type_from sy (Right . (EType::Type Consts ki h -> EType Consts))
  27                 in
  28                  [ syBool ==> Right tyBool
  29                  , syFun [syBool] ==> Right (tyFun :$ tyBool)
  30                  , syEq [syBool] ==> Right (tyEq :$ tyBool)
  31                  , syMonad [syIO []] ==> Right (tyMonad :$ tyIO)
  32                  , syFun [syIO [syBool]] ==> Right (tyFun :$ (tyIO :$ tyBool))
  33                  , (syBool .> syBool) ==> Right
  34                    (tyBool ~> tyBool)
  35                  , ((syBool .> syBool) .> syBool) ==> Right
  36                    ((tyBool ~> tyBool) ~> tyBool)
  37                  , ((syBool .> syInt) .> syBool) ==> Right
  38                    ((tyBool ~> tyInt) ~> tyBool)
  39                  , (syBool .> syInt .> syBool) ==> Right
  40                    (tyBool ~> tyInt ~> tyBool)
  41                  , ((syBool .> (syBool .> syInt)) .> syBool) ==> Right
  42                    ((tyBool ~> (tyBool ~> tyInt)) ~> tyBool)
  43                  , testGroup "Error_Type"
  44                          [ syFun [syIO []] ==> Left
  45                                  (Error_Type_Kind_mismatch
  46                                          (At (syFun [syIO []]) $ EKind SKiTerm)
  47                                          (At (syIO []) $ EKind $ SKiTerm `SKiArrow` SKiTerm))
  48                          , syIO [syEq [syBool]] ==> Left
  49                                  (Error_Type_Kind_mismatch
  50                                          (At (syIO [syEq [syBool]]) $ EKind SKiTerm)
  51                                          (At (syEq [syBool]) $ EKind $ SKiCon))
  52                          , Syntax "Bool" [syBool] ==> Left
  53                                  (Error_Type_Kind_not_applicable
  54                                          (At (Syntax "Bool"  [syBool]) $ EKind SKiTerm))
  55                          , Syntax "Unknown" [] ==> Left (Error_Type_Constant_unknown $
  56                                  At (Syntax "Unknown" []) ())
  57                          ]
  58                  ]
  59          , testGroup "proj_con" $
  60                 let (==>) (ty::Type Consts 'KiCon h) expected =
  61                         testCase (show_type ty) $
  62                         isJust (proj_con ty) @?= expected
  63                 in
  64                  [ (tyEq :$ tyBool) ==> True
  65                  , (tyMonad :$ tyIO) ==> True
  66                  , (tyTraversable :$ tyIO) ==> False
  67                  ]
  68          ]