Context.hs

{-# LANGUAGE GADTs, DataKinds #-}
-- | Some helpers for workingw ith contexts
module Context where
import Data.Maybe
import Data.Monoid

import AST
import Pretty

existentials :: Context -> [TVar]
existentials (Context gamma) = aux =<< gamma
  where aux (CExists alpha)         = [alpha]
        aux (CExistsSolved alpha _) = [alpha]
        aux _                       = []

unsolved :: Context -> [TVar]
unsolved (Context gamma) = [alpha | CExists alpha <- gamma]

vars :: Context -> [Var]
vars (Context gamma) = [x | CVar x _ <- gamma]

foralls :: Context -> [TVar]
foralls (Context gamma) = [alpha | CForall alpha <- gamma]

markers :: Context -> [TVar]
markers (Context gamma) = [alpha | CMarker alpha <- gamma]

-- | Well-formedness of contexts
--   wf Γ <=> Γ ctx
wf :: Context -> Bool
wf (Context gamma) = case gamma of
  -- EmptyCtx
  [] -> True
  c:cs -> let gamma' = Context cs in wf gamma' && case c of
    -- UvarCtx
    CForall alpha -> alpha `notElem` foralls gamma'
    -- VarCtx
    CVar x a -> x `notElem` vars gamma' && typewf gamma' a
    -- EvarCtx
    CExists alpha -> alpha `notElem` existentials gamma'
    -- SolvedEvarCtx
    CExistsSolved alpha tau -> alpha `notElem` existentials gamma'
                            && typewf gamma' tau
    -- MarkerCtx
    CMarker alpha -> alpha `notElem` markers gamma'
                  && alpha `notElem` existentials gamma'

-- | Well-formedness of types
--   typewf Γ A <=> Γ |- A
typewf :: Context -> Type a -> Bool
typewf gamma typ = case typ of
  -- UvarWF
  TVar alpha -> alpha `elem` foralls gamma
  -- UnitWF
  TUnit -> True
  -- ArrowWF
  TFun a b -> typewf gamma a && typewf gamma b
  -- ForallWF
  TForall alpha a -> typewf (gamma >: CForall alpha) a
  -- EvarWF and SolvedEvarWF
  TExists alpha -> alpha `elem` existentials gamma

-- Assert-like functionality to make sure that contexts and types are
-- well-formed
checkwf :: Context -> x -> x
checkwf gamma x | wf gamma  = x
                | otherwise = error $ "Malformed context: " ++ pretty gamma

checkwftype :: Context -> Polytype -> x -> x
checkwftype gamma a x | typewf gamma a = checkwf gamma x
                      | otherwise      = error $ "Malformed type: "
                                       ++ pretty (a, gamma)

-- | findSolved (ΓL,α^ = τ,ΓR) α = Just τ
findSolved :: Context -> TVar -> Maybe Monotype
findSolved (Context gamma) v = listToMaybe [t | CExistsSolved v' t <- gamma, v == v']

-- | findVarType (ΓL,x : A,ΓR) x = Just A
findVarType :: Context -> Var -> Maybe Polytype
findVarType (Context gamma) v = listToMaybe [t | CVar v' t <- gamma, v == v']

-- | solve (ΓL,α^,ΓR) α τ = (ΓL,α = τ,ΓR)
solve :: Context -> TVar -> Monotype -> Maybe Context
solve gamma alpha tau | typewf gammaL tau = Just gamma'
                             | otherwise         = Nothing
  where (gammaL, gammaR) = breakMarker (CExists alpha) gamma
        gamma' = gammaL >++ [CExistsSolved alpha tau] <> gammaR

-- | insertAt (ΓL,c,ΓR) c Θ = ΓL,Θ,ΓR
insertAt :: Context -> ContextElem Incomplete -> Context -> Context
insertAt gamma c theta = gammaL <> theta <> gammaR
  where (gammaL, gammaR) = breakMarker c gamma

-- | apply Γ A = [Γ]A
apply :: Context -> Polytype -> Polytype
apply gamma typ = case typ of
  TUnit       -> TUnit
  TVar v      -> TVar v
  TForall v t -> TForall v (apply gamma t)
  TExists v   -> maybe (TExists v) (apply gamma . polytype) $ findSolved gamma v
  TFun t1 t2  -> apply gamma t1 `TFun` apply gamma t2

-- | ordered Γ α β = True <=> Γ[α^][β^]
ordered :: Context -> TVar -> TVar -> Bool
ordered gamma alpha beta =
  let gammaL = dropMarker (CExists beta) gamma
   in alpha `elem` existentials gammaL