File size: 3,116 Bytes
a10b189 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 | {-# LANGUAGE OverloadedStrings #-}
{-|
Module : Test.Core.Invariants
Description : Tests for AST invariants
-}
module Test.Core.Invariants
( tests
) where
import Test.Tasty
import Test.Tasty.HUnit
import qualified Data.Set as Set
import Data.Text (Text)
import Assertica.Core.AST
import Assertica.Core.Invariants
tests :: TestTree
tests = testGroup "Assertica.Core.Invariants"
[ testGroup "Binding Invariants"
[ testCase "All variables bound" testAllVarsBound
, testCase "Free variables detected" testFreeVarsDetected
]
, testGroup "Qualification Invariants"
[ testCase "Valid qualification" testValidQual
, testCase "Invalid empty local name" testInvalidQual
]
, testGroup "Type Well-Formedness"
[ testCase "Well-formed simple type" testWellFormedType
]
, testGroup "Term Well-Formedness"
[ testCase "Well-formed term" testWellFormedTerm
]
]
-- ============================================================================
-- BINDING INVARIANT TESTS
-- ============================================================================
testAllVarsBound :: Assertion
testAllVarsBound =
let x = Var "x" 1
binder = Binder x Nothing
body = Var x
lam = Lam binder body
in allVariablesBound lam @? "All variables should be bound in λx. x"
testFreeVarsDetected :: Assertion
testFreeVarsDetected =
let x = Var "x" 1
y = Var "y" 2
binder = Binder x Nothing
body = App (Var x) (Var y)
lam = Lam binder body
in not (allVariablesBound lam) @? "Free variable y should be detected"
-- ============================================================================
-- QUALIFICATION INVARIANT TESTS
-- ============================================================================
testValidQual :: Assertion
testValidQual =
let q = QName ["Prelude"] "map"
in case checkQualificationInvariant q of
Right () -> pure ()
Left _ -> assertFailure "Valid qualification failed"
testInvalidQual :: Assertion
testInvalidQual =
let q = QName ["Prelude"] "" -- Empty local name
in case checkQualificationInvariant q of
Left _ -> pure ()
Right () -> assertFailure "Should have rejected empty local name"
-- ============================================================================
-- TYPE WELL-FORMEDNESS TESTS
-- ============================================================================
testWellFormedType :: Assertion
testWellFormedType =
let ty = TyFun (TyVar (Var "a" 1)) (TyVar (Var "a" 1))
in case isWellFormedType ty of
Right () -> pure ()
Left _ -> assertFailure "Type should be well-formed"
-- ============================================================================
-- TERM WELL-FORMEDNESS TESTS
-- ============================================================================
testWellFormedTerm :: Assertion
testWellFormedTerm =
let x = Var "x" 1
binder = Binder x Nothing
term = Lam binder (Var x)
in case isWellFormedTerm term of
Right () -> pure ()
Left _ -> assertFailure "Term should be well-formed"
|