git.iko.soy/elk
on c19392f help sign in
elk/src/Type/Constraint.hs
94 lines 1.7 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2{-# LANGUAGE OverloadedStrings #-}
3module Type.Constraint
4 ( Constraint(..)
5 , (/\), ex, forall
6 , exists, existsNumber
7 , Scheme(..), SchemeName
8 , monoscheme
9 )
10 where
12import qualified Data.Map.Strict as Map
13import Data.Text (Text)
15import qualified Reporting.Annotation as A
16import qualified Reporting.Error.Type as Error
17import qualified Reporting.Region as R
18import Type.Type (Type(VarN), Variable, mkFlexVar, mkFlexNumber)
22-- CONSTRAINTS
25data Constraint
26 = CTrue
27 | CSaveEnv
28 | CEqual Error.Hint R.Region Type Type
29 | CAnd [Constraint]
30 | CLet [Scheme] Constraint
31 | CInstance R.Region SchemeName Type
35-- SCHEMES
38type SchemeName = Text
41data Scheme =
42 Scheme
43 { _rigidQuantifiers :: [Variable]
44 , _flexibleQuantifiers :: [Variable]
45 , _constraint :: Constraint
46 , _header :: Map.Map Text (A.Located Type)
47 }
51-- SCHEME HELPERS
54monoscheme :: Map.Map Text (A.Located Type) -> Scheme
55monoscheme headers =
56 Scheme [] [] CTrue headers
60-- CONSTRAINT HELPERS
63infixl 8 /\
66(/\) :: Constraint -> Constraint -> Constraint
67(/\) c1 c2 =
68 case (c1, c2) of
69 (CTrue, _) -> c2
70 (_, CTrue) -> c1
71 _ -> CAnd [c1,c2]
74-- ex qs constraint == exists qs. constraint
75ex :: [Variable] -> Constraint -> Constraint
76ex fqs constraint =
77 CLet [Scheme [] fqs constraint Map.empty] CTrue
80forall :: [Variable] -> Constraint -> Constraint
81forall rqs constraint =
82 CLet [Scheme rqs [] constraint Map.empty] CTrue
85exists :: (Type -> IO Constraint) -> IO Constraint
86exists f =
87 do v <- mkFlexVar
88 ex [v] <$> f (VarN v)
91existsNumber :: (Type -> IO Constraint) -> IO Constraint
92existsNumber f =
93 do v <- mkFlexNumber
94 ex [v] <$> f (VarN v)