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