{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}

module IR.Constraint.Canonical (
  Type (..),
  Scheme (..),
  FreeVars,
  Annotation (..),
  Annotations (..),
  Kind,
  schemeOf,
  freeVars,
  foldArrow,
  unfoldArrow,
  (-->),
  pattern Unit,
  pattern Ref,
  pattern List,
  pattern Time,
  pattern I64,
  pattern U64,
  pattern I32,
  pattern U32,
  pattern I16,
  pattern U16,
  pattern I8,
  pattern U8,
  tuple,
  unAnnotations,
  annToType,
  builtinKinds,
) where

import qualified Common.Identifiers as Ident
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import qualified IR.IR as I
import IR.Types.Type (
  Annotation (..),
  Annotations (..),
  Type (..),
  builtinKinds,
  foldArrow,
  tupleId,
  unAnnotations,
  unfoldArrow,
 )


-- | SCHEMES
data Scheme = Forall FreeVars I.Type


type FreeVars = Map.Map Ident.TVarId ()


-- | Construct a scheme from all free type variables and a trivial constraint.
schemeOf :: I.Type -> Scheme
schemeOf :: Type -> Scheme
schemeOf Type
t = FreeVars -> Type -> Scheme
Forall (Type -> FreeVars
freeVars Type
t) Type
t


freeVars :: I.Type -> FreeVars
freeVars :: Type -> FreeVars
freeVars Type
t = [(TVarId, ())] -> FreeVars
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TVarId, ())] -> FreeVars)
-> (Set TVarId -> [(TVarId, ())]) -> Set TVarId -> FreeVars
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TVarId -> (TVarId, ())) -> [TVarId] -> [(TVarId, ())]
forall a b. (a -> b) -> [a] -> [b]
map (,()) ([TVarId] -> [(TVarId, ())])
-> (Set TVarId -> [TVarId]) -> Set TVarId -> [(TVarId, ())]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set TVarId -> [TVarId]
forall a. Set a -> [a]
Set.toList (Set TVarId -> FreeVars) -> Set TVarId -> FreeVars
forall a b. (a -> b) -> a -> b
$ Type -> Set TVarId
forall t i. HasFreeVars t i => t -> Set i
Ident.freeVars Type
t


-- | KINDS

-- no support for higher-kinded stuff yet, so Int suffices
type Kind = Int


-- | HELPERS
infixr 0 -->


(-->) :: I.Type -> I.Type -> I.Type
--> :: Type -> Type -> Type
(-->) Type
t1 Type
t2 = TConId -> [Type] -> Type
TCon TConId
"->" [Type
t1, Type
t2]


-- | The builtin singleton 'Type', whose only data constructor is just @()@.
pattern Unit :: Type
pattern $bUnit :: Type
$mUnit :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
Unit = TCon "()" []


-- | The builtin reference 'Type', created using @new@.
pattern Ref :: Type -> Type
pattern $bRef :: Type -> Type
$mRef :: forall r. Type -> (Type -> r) -> (Void# -> r) -> r
Ref a = TCon "&" [a]


-- | The builtin list 'Type', created using list syntax, e.g., @[a, b]@.
pattern List :: Type -> Type
pattern $bList :: Type -> Type
$mList :: forall r. Type -> (Type -> r) -> (Void# -> r) -> r
List a = TCon "[]" [a]


-- | The builtin 64-bit timestamp 'Type'.
pattern Time :: Type
pattern $bTime :: Type
$mTime :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
Time = TCon "Time" []


-- | Builtin 'Type' for signed 64-bit integers.
pattern I64 :: Type
pattern $bI64 :: Type
$mI64 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
I64 = TCon "Int64" []


-- | Builtin 'Type' for unsigned 64-bit integers.
pattern U64 :: Type
pattern $bU64 :: Type
$mU64 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
U64 = TCon "UInt64" []


-- | Builtin 'Type' for signed 32-bit integers.
pattern I32 :: Type
pattern $bI32 :: Type
$mI32 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
I32 = TCon "Int32" []


-- | Builtin 'Type' for unsigned 32-bit integers.
pattern U32 :: Type
pattern $bU32 :: Type
$mU32 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
U32 = TCon "UInt32" []


-- | Builtin 'Type' for signed 16-bit integers.
pattern I16 :: Type
pattern $bI16 :: Type
$mI16 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
I16 = TCon "Int16" []


-- | Builtin 'Type' for unsigned 16-bit integers.
pattern U16 :: Type
pattern $bU16 :: Type
$mU16 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
U16 = TCon "UInt16" []


-- | Builtin 'Type' for signed 8-bit integers.
pattern I8 :: Type
pattern $bI8 :: Type
$mI8 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
I8 = TCon "Int8" []


-- | Builtin 'Type' for unsigned 8-bit integers.
pattern U8 :: Type
pattern $bU8 :: Type
$mU8 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
U8 = TCon "UInt8" []


-- | Construct a builtin tuple type out of a list of at least 2 types.
tuple :: [Type] -> Type
tuple :: [Type] -> Type
tuple [Type]
ts = TConId -> [Type] -> Type
TCon (Int -> TConId
forall v. Identifiable v => Int -> v
tupleId (Int -> TConId) -> Int -> TConId
forall a b. (a -> b) -> a -> b
$ [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts) [Type]
ts


-- | ANNOTATION
annToType :: Annotation -> Type
annToType :: Annotation -> Type
annToType Annotation
ann = case Annotation
ann of
  AnnDCon DConId
_ [Annotation]
_ -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error [Char]
"No need for AnnDCon anymore."
  AnnType Type
canType -> Type
canType
  AnnArrows [Annotation]
paramAnns Annotation
retAnn ->
    let paramCanTypes :: [Type]
paramCanTypes = (Annotation -> Type) -> [Annotation] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Annotation -> Type
annToType [Annotation]
paramAnns
        retCanType :: Type
retCanType = Annotation -> Type
annToType Annotation
retAnn
     in ([Type], Type) -> Type
foldArrow ([Type]
paramCanTypes, Type
retCanType)