content: module RefineSyntax where
  
  import Control.Monad
  import Control.Monad.Except
  import Control.Monad.State
  import Data.Foldable
  import Data.Functor.Identity
  
  import Data.List
  import Data.Maybe
  import qualified Data.Map.Strict as M
  import qualified Data.Set as S
  
  import BwdFwd
  import Syntax
  import RefineSyntaxCommon
  import RefineSyntaxConcretiseEps
  import RefineSyntaxSubstitItfAliases
  import Debug
  
  -- Main refinement function
  refine :: Prog Raw -> Either String (Prog Refined)
  refine prog = evalState (runExceptT (refine' prog)) initRefine
  
  -- Explicit refinements:
  -- + concretise epsilons in top level definitions
  -- + built-in data types, interfaces, operators are added
  refine' :: Prog Raw -> Refine (Prog Refined)
  refine' (MkProg xs) = do
    -- Concretise epsilon vars
    let (dts, itfs, itfAls) = concretiseEps [d | DataTm d _ <- xs]
                                            [i | ItfTm i _ <- xs]
                                            [i | ItfAliasTm i _ <- xs]
    let hdrSigs = [s | SigTm s _ <- xs]
    let hdrDefs = [c | ClsTm c _ <- xs]
    let rawBuiltinItfTms = map (\itf -> ItfTm itf b) builtinItfs
    let builtinMHDTms = map (\hdr -> DefTm hdr a) builtinMHDefs
    -- Initialise refinement state
    initialiseRState dts itfs itfAls
    -- Refine top level terms
    putTopLevelCtxt Datatype
    dtTms <- mapM refineDataT dts
    putTopLevelCtxt Interface
    itfTms <- mapM refineItf itfs
    putTopLevelCtxt InterfaceAlias
    mapM_ refineItfAl itfAls
    putTopLevelCtxt Handler
    hdrs <- mapM (refineMH hdrDefs) hdrSigs
    -- Make sure (built-in) interfaces and interface aliases have unique ids
    -- Performing this check after refinement to prioritise more precise error
    -- messages.
    checkUniqueIds ([i | i@(ItfTm _ _) <- xs] ++
                    [i | i@(ItfAliasTm _ _) <- xs] ++
                    [i | i@(ItfTm _ _) <- rawBuiltinItfTms])
      (errorRefDuplTopTm "interface/interface alias")
    -- Check uniqueness of hdrs w.r.t builtin ones
    checkUniqueIds ([h | h@(DefTm _ _) <- hdrs] ++
                    [h | h@(DefTm _ _) <- builtinMHDTms])
      (errorRefDuplTopTm "operator")
    builtinItfTms <- mapM refineItf builtinItfs
    return $ MkProg (map (\dt -> DataTm dt a) builtinDataTs ++ dtTms ++
                     builtinItfTms ++ itfTms ++ builtinMHDTms ++ hdrs)
    where a = Refined BuiltIn
          b = Raw BuiltIn
  
  -- Explicit refinements:
  -- + data type has unique effect & type variables
  refineDataT :: DataT Raw -> Refine (TopTm Refined)
  refineDataT d@(DT dt ps ctrs a) =
   --         data dt p_1 ... p_m = ctr_1 | ... | ctr_n
    if uniqueIds (map fst ps) then
      do let tvs = [x | (x, VT) <- ps] -- val ty vars
         let evs = [x | (x, ET) <- ps] -- eff ty vars
         -- refine constructors
         putTMap (M.fromList $ zip tvs (map (swap TVar a) tvs)) -- temp. val ty vars
         putEVSet (S.fromList evs)                       -- temp. eff ty vars
         ctrs' <- mapM refineCtr ctrs
         putEVSet S.empty                                -- reset
         putTMap M.empty                                 -- reset
         return $ DataTm (DT dt ps ctrs' a') a'
    else throwError $ errorRefDuplParamData d
    where a' = rawToRef a
  
  -- Explicit refinements:
  -- + interface has unique effect & type variables
  refineItf :: Itf Raw -> Refine (TopTm Refined)
  refineItf i@(Itf itf ps cmds a) =
  --        interface itf p_1 ... p_m = cmd_1 | ... | cmd_n
    if uniqueIds (map fst ps) then
      do let tvs = [x | (x, VT) <- ps] -- val ty vars
         let evs = [x | (x, ET) <- ps] -- eff ty vars
         -- refine commands
         putTMap (M.fromList $ zip tvs (map (swap TVar a) tvs)) -- temp. val ty vars
         putEVSet (S.fromList evs)                       -- temp. eff ty vars
         cmds' <- mapM refineCmd cmds
         putEVSet S.empty                                -- reset
         putTMap M.empty                                 -- reset
         return $ ItfTm (Itf itf ps cmds' a') a'
    else throwError $ errorRefDuplParamItf i
    where a' = rawToRef a
  
  -- Explicit refinements:
  -- + interface has unique effect & type variables
  refineItfAl :: ItfAlias Raw -> Refine ()
  refineItfAl i@(ItfAlias itfAl ps _ a) =
  --          interface itf p_1 ... p_m = [itf_1 t_11 ... t_1n, ...]
    if uniqueIds (map fst ps) then
      do let tvs = [x | (x, VT) <- ps] -- val ty vars
         let evs = [x | (x, ET) <- ps] -- eff ty vars
         -- refine itf map
         putTMap (M.fromList $ zip tvs (map (swap TVar a) tvs)) -- temp. val ty vars
         putEVSet (S.fromList evs)                       -- temp. eff ty vars
         -- interpret RHS of interface alias def. as the instantiation of itf with
         -- the generic type variables ps (this "lift" is possible as the
         -- itf map of itf is part of the RState)
         let singletonItfMap = ItfMap (M.singleton itfAl (BEmp :< map tyVar2rawTyVarArg ps)) (Raw Generated)
         itfMap' <- refineItfMap singletonItfMap
         putEVSet S.empty                                -- reset
         putTMap M.empty                                 -- reset
    else throwError $ errorRefDuplParamItfAl i
    where a' = rawToRef a
  
  -- Explicit refinements:
  -- + command has unique effect & type variables
  refineCmd :: Cmd Raw -> Refine (Cmd Refined)
  refineCmd c@(Cmd id ps xs y a) =
  --        id p_1 ... p_m: x_1 -> ... -> x_n -> y
    if uniqueIds (map fst ps) then
      do tmap <- getTMap
         evset <- getEVSet
         -- TODO: LC: Shadowing should be allowed, fix this in future
         -- check that none of this cmd's ty vars coincide with the itf's ones
         if uniqueIds (map fst ps ++ map fst (M.toList tmap) ++ S.toList evset) then
           do let tvs = [x | (x, VT) <- ps] -- val ty vars
              let evs = [x | (x, ET) <- ps] -- eff ty vars
              -- refine ty args
              putTMap (M.union tmap (M.fromList $ zip tvs (map (swap TVar a) tvs))) -- temp. val ty vars
              putEVSet (S.union evset (S.fromList evs))    -- temp. eff ty vars
              xs' <- mapM refineVType xs
              y' <- refineVType y
              putTMap tmap                                 -- reset
              putEVSet evset                               -- reset
              return $ Cmd id ps xs' y' a'
         else throwError $ "a type parameter of command " ++ id ++
                           "already occurs as interface type parameter"
    else throwError $ errorRefDuplParamCmd c
    where a' = rawToRef a
  
  
  refineCtr :: Ctr Raw -> Refine (Ctr Refined)
  refineCtr (Ctr id xs a) = do xs' <- mapM refineVType xs
                               return $ Ctr id xs' (rawToRef a)
  
  refineCType :: CType Raw -> Refine (CType Refined)
  refineCType (CType xs z a) = do ys <- mapM refinePort xs
                                  peg <- refinePeg z
                                  return $ CType ys peg (rawToRef a)
  
  refinePort :: Port Raw -> Refine (Port Refined)
  refinePort (Port adjs ty a) = do adjs' <- mapM refineAdj adjs
                                   ty' <- refineVType ty
                                   return $ Port (concat adjs') ty' (rawToRef a)
  
  refinePeg :: Peg Raw -> Refine (Peg Refined)
  refinePeg (Peg ab ty a) = do ab' <- refineAb ab
                               ty' <- refineVType ty
                               return $ Peg ab' ty' (rawToRef a)
  
  refineAb :: Ab Raw -> Refine (Ab Refined)
  refineAb ab@(Ab v mp@(ItfMap m _) a) =
  --       [v | itf_1 x_11 ... x_1k, ..., itf_l x_l1 ... x_ln]
    do -- Check that v has been introduced before or is now implicitly introduced
       evset <- getEVSet
       ctx <- getTopLevelCtxt
       case v of
         (EmpAb b) -> do m' <- refineItfMap mp
                         return $ Ab (EmpAb (rawToRef b)) m' a'
         (AbVar x b) ->
           if x `S.member` evset || isHdrCtxt ctx then
              do m' <- refineItfMap mp
                 return $ Ab (AbVar x (rawToRef b)) m' a'
           else throwError $ errorRefIdNotDeclared "effect type variable" x a
    where a' = rawToRef a
  
  -- Input: itf_1 x_11 ... x_1k, ..., itf_l x_l1 ... x_ln
  -- If a itf_i is an already-introduced effect variable, require that there are
  --   no x_ij (else throw error)
  -- Output: all itf_i which refer to already-introduced effect variables
  getIntroducedEVars :: ItfMap Raw -> Refine [Id]
  getIntroducedEVars (ItfMap m _) = do
    p <- getEVSet
    let candidates = [(itf, (maximum . map length . bwd2fwd) xs) | (itf, xs) <- M.toList m, S.member itf p]
    let errors = filter (\(itf, n) -> n > 0) candidates
    case errors of []             -> return $ map fst candidates
                   ((itf, _) : _) -> throwError $ errorRefEffVarNoParams itf
  
  refineAbMod :: AbMod Raw -> AbMod Refined
  refineAbMod (EmpAb a) = EmpAb (rawToRef a)
  refineAbMod (AbVar x a) = AbVar x (rawToRef a)
  
  refineAdj :: Adjustment Raw -> Refine [Adjustment Refined]
  refineAdj (ConsAdj x ts a) = do
    tss' <- refineItfInst a (x, ts)
    let tss'' = M.foldlWithKey (\acc itf ts' -> acc ++ instsToAdjs itf ts') [] tss'
    --LAST STOP
    return $ tss''
    where instsToAdjs :: Id -> Bwd [TyArg Refined] -> [Adjustment Refined]
          instsToAdjs itf ts = map (\ts' -> ConsAdj itf ts' (rawToRef a)) (bwd2fwd ts)
  refineAdj (AdaptorAdj adp a) = do
    adp' <- refineAdaptor adp
    return $ [AdaptorAdj adp' (rawToRef a)]
  
  -- Explicit refinements:
  -- + interface aliases are substituted
  refineItfInst :: Raw -> (Id, [TyArg Raw]) ->
                   Refine (M.Map Id (Bwd [TyArg Refined]))
  refineItfInst a (x, ts) = do
  --                  x t_11 ... t_1n
    -- replace interface aliases by interfaces
    m' <- substitItfAls (x, ts) >>= \i -> case i of
      ItfMap m _ -> pure m
      _ -> throwError "Expected ItfMap but found something else."
  --                  x t_11 ... t_1n, ..., x t_m1 t_mn
    -- refine instantiations of each interface
    m'' <- M.fromList <$> (mapM (refineItfInsts a)) (M.toList m')
    return m''
  
  -- Explicit refinements:
  -- + interface aliases are substituted
  refineItfMap :: ItfMap Raw -> Refine (ItfMap Refined)
  refineItfMap (ItfMap m a) = do
    -- replace interface aliases by interfaces
    ms <- mapM (\(x, insts) -> mapM (\inst -> substitItfAls (x, inst)) (bwd2fwd insts)) (M.toList m)
    let (ItfMap m' a') = foldl plusItfMap (emptyItfMap a) (concat ms)
    -- refine instantiations of each interface
    m'' <- M.fromList <$> (mapM (refineItfInsts a)) (M.toList m')
    return $ ItfMap m'' (rawToRef a)
  
  refineItfInsts :: Raw -> (Id, Bwd [TyArg Raw]) ->
                    Refine (Id, Bwd [TyArg Refined])
  refineItfInsts a (x, insts) = do
  --                  x t_11 ... t_1n, ..., x t_m1 t_mn
    itfs <- getRItfs
    case M.lookup x itfs of
      Just ps -> do
  --            1) interface x p_1 ... p_n     = ...
  --         or 2) interface x p_1 ... p_n [£] = ...
  --               and [£] has been explicitly added before
  --            if 2), set t_{n+1} := [£]
         evset <- getEVSet
         ctx <- getTopLevelCtxt
         insts' <- mapM (\ts -> do let a' = Raw (implicitNear a)
                                   let ts' = if "£" `S.member` evset ||
                                                isHdrCtxt ctx
                                             then concretiseEpsArg ps ts a'
                                             else ts
                                   checkArgs x (length ps) (length ts') a
                                   mapM refineTyArg ts')
                        insts
         return (x, insts')
      Nothing -> throwError $ errorRefIdNotDeclared "interface" x a
  
  -- Explicit refinements:
  -- + implicit [£] ty args to data types are made explicit
  -- + DTTy is distinguished between being (in the following precedence)
  --   1) data type indeed            -> DTTy
  --   2) (implicitly) intro'd ty var -> TVar  (if no ty args)
  --   3) neither                     -> error
  -- + MkTVar is distinguished between being
  --   1) intro'd ty var              -> TVar
  --   2) data type                   -> DTTy
  --   3) neither                     -> TVar
  -- + ty arguments refer only to introduced val tys
  refineVType :: VType Raw -> Refine (VType Refined)
  refineVType (DTTy x ts a) =
  --           x t_1 ... t_n
    do -- Check that x is datatype or introduced or just-implicitly intro'd ty var
       dtm <- getRDTs
       tmap <- getTMap
       ctx <- getTopLevelCtxt
       evset <- getEVSet
       case M.lookup x dtm of
         Just ps -> do
  --       data x p_1 ... p_n
           let a' = Raw (implicitNear a)
           let ts' = if "£" `S.member` evset || isHdrCtxt ctx
                     then concretiseEpsArg ps ts a'
                     else ts
           checkArgs x (length ps) (length ts') a
           ts'' <- mapM refineTyArg ts'
           return $ DTTy x ts'' (rawToRef a)
         Nothing ->
           if null ts &&          -- there must be no arguments to ty var
              (isHdrCtxt ctx ||   -- x can be implic. ty var in hdr sign.
               x `M.member` tmap)    -- x can be in val ty contexts
           then return $ TVar x (rawToRef a)
           else throwError $ errorRefIdNotDeclared "value type variable" x a
  refineVType (SCTy ty a) = refineCType ty >>= return . swap SCTy (rawToRef a)
  refineVType (TVar x a) =
    do -- Check that x is intro'd ty-var or datatype or just-implicitly intro'd ty var
       tmap <- getTMap
       dtm <- getRDTs
       ctx <- getTopLevelCtxt
       case M.lookup x tmap of
         Just _  -> return $ TVar x (rawToRef a)
         Nothing -> case M.lookup x dtm of
           Just ps ->
             -- if the data type is parameterised by a single eff var then instantiate it to [£|]
             do let ts = case ps of
                           [(_, ET)] -> [EArg (Ab (AbVar "£" a) (ItfMap M.empty a) a) a]
                           _ -> []
                checkArgs x (length ps) (length ts) a
                ts' <- mapM refineTyArg ts
                return $ DTTy x ts' (rawToRef a)
           Nothing ->
             -- last possibility: x can be implic. ty var in hdr sign.
             if isHdrCtxt ctx
             then return $ TVar x (rawToRef a)
             else throwError $ errorRefIdNotDeclared "value type variable" x a
  refineVType (StringTy a) = return $ StringTy (rawToRef a)
  refineVType (IntTy a) = return $ IntTy (rawToRef a)
  refineVType (CharTy a) = return $ CharTy (rawToRef a)
  
  refineTyArg :: TyArg Raw -> Refine (TyArg Refined)
  refineTyArg (VArg t a) = VArg <$> refineVType t <*> pure (rawToRef a)
  refineTyArg (EArg ab a) = EArg <$> refineAb ab <*> pure (rawToRef a)
  
  refineMH :: [MHCls Raw] -> MHSig Raw -> Refine (TopTm Refined)
  refineMH xs (Sig id ty a) = do cs <- mapM refineMHCls ys
                                 ty' <- refineCType ty
                                 return $ DefTm (Def id ty' cs a') a'
    where ys = filter (\(MHCls id' _ _) -> id' == id) xs
          a' = rawToRef a
  
  refineMHCls :: MHCls Raw -> Refine (Clause Refined)
  refineMHCls (MHCls _ cls a) = refineClause cls
  
  -- Explicit refinements:
  -- + id "x" is refined to 1) DataCon:          0-ary constructor if matching
  --                        2) Use . Op . CmdId: command operator if matching
  --                        3) Use . Op . VarId: value variable otherwise
  -- + applications (MkRawComb) are refined same way as ids
  -- + let x = e1 in e2    -->   case e1 {x -> e2}
  -- + [x, y, z]           -->   x cons (y cons (z cons nil))
  refineUse :: Use Raw -> Refine (Either (Use Refined) (Tm Refined))
  refineUse (RawId id a) =
    do ctrs <- getRCtrs
       cmds <- getRCmds
       if id `elem` ctrs
         then return $ Right $ DCon (DataCon id [] a') a'
         else if id `elem` cmds
              then return $ Left $ Op (CmdId id a') a'
              else return $ Left $ Op (VarId id a') a'
    where a' = rawToRef a
  refineUse (RawComb (RawId id b) xs a) =
    do xs' <- mapM refineTm xs
       ctrs <- getRCtrs
       cmds <- getRCmds
       if id `elem` ctrs
         then return $ Right $ DCon (DataCon id xs' b') a'
         else if id `elem` cmds
              then return $ Left $ App (Op (CmdId id b') b') xs' a'
              else return $ Left $ App (Op (VarId id b') b') xs' a'
    where a' = rawToRef a
          b' = rawToRef b
  refineUse (RawComb x xs a) =
    do x' <- refineUse x
       case x' of
         Left use -> do xs' <- mapM refineTm xs
                        return $ Left $ App use xs' (rawToRef a)
         Right tm -> throwError $ errorRefExpectedUse tm
  refineUse (Adapted rs t a) =
    -- First check the existence of the interfaces
    do rs' <- mapM refineAdaptor rs
       t' <- refineUse t
       case t' of
         Left u   -> return $ Left $ Adapted rs' u (rawToRef a)
         Right tm -> throwError $ errorRefExpectedUse tm
  
  refineAdaptor :: Adaptor Raw -> Refine (Adaptor Refined)
  refineAdaptor adp@(RawAdp x liat left right a) = do
    itfCx <- getRItfs
    if x `M.member` itfCx then
      -- TODO: LC: left-hand side must consist of distinct names
      -- Check whether first element of right-hand side is liat
      if null right || head right == liat then
        if null right then return $ Adp x Nothing [] (rawToRef a)
        else
          let mm = Just (length left) in
          let right' = tail right in
          let rightNs = map (\p -> elemIndex p (reverse left)) right' in
          if any isNothing rightNs then throwError "adaptor error"
          else return $ Adp x (Just (length left)) (map fromJust rightNs) (rawToRef a)
      else
        throwError $ "adaptor error"
    else throwError $ errorRefIdNotDeclared "interface" x a
  
  refineTm :: Tm Raw -> Refine (Tm Refined)
  refineTm (Let x t1 t2 a) =
    do s1 <- refineTm t1
       s2 <- refineTm $ SC (SComp [Cls [VPat (VarPat x a) a] t2 a] a) a
       return $ Use (App (Op (VarId "case" a') a') [s1, s2] a') a'
    where a' = rawToRef a
  refineTm (SC x a) = do x' <- refineSComp x
                         return $ SC x' (rawToRef a)
  refineTm (StrTm x a) = return $ StrTm x (rawToRef a)
  refineTm (IntTm x a) = return $ IntTm x (rawToRef a)
  refineTm (CharTm x a) = return $ CharTm x (rawToRef a)
  refineTm (ListTm ts a) =
    do ts' <- mapM refineTm ts
       return $
         foldr
           (\x y -> DCon (DataCon "cons" [x, y] a') a')
           (DCon (DataCon "nil" [] a') a')
           ts'
    where a' = rawToRef a
  refineTm (TmSeq t1 t2 a) = do t1' <- refineTm t1
                                t2' <- refineTm t2
                                return $ TmSeq t1' t2' (rawToRef a)
  refineTm (Use u a) = do u' <- refineUse u
                          case u' of
                            Left use -> return $ Use use (rawToRef a)
                            Right tm -> return tm
  
  refineSComp :: SComp Raw -> Refine (SComp Refined)
  refineSComp (SComp xs a) = do xs' <- mapM refineClause xs
                                return $ SComp xs' (rawToRef a)
  
  refineClause :: Clause Raw -> Refine (Clause Refined)
  refineClause (Cls ps tm a) = do ps' <- mapM refinePattern ps
                                  tm' <- refineTm tm
                                  return $ Cls ps' tm' (rawToRef a)
  
  -- Explicit refinements:
  -- + command patterns (e.g. <send x -> k>) must refer to existing command.
  refinePattern :: Pattern Raw -> Refine (Pattern Refined)
  refinePattern (VPat p a) = VPat <$> refineVPat p <*> (pure $ rawToRef a)
  refinePattern (CmdPat x n ps k a) =
    do cmds <- getRCmds
       if x `elem` cmds
         then do ps' <- mapM refineVPat ps
                 return $ CmdPat x n ps' k (rawToRef a)
         else throwError $ errorRefIdNotDeclared "command" x a
  refinePattern (ThkPat x a) = return $ ThkPat x (rawToRef a)
  
  -- Explicit refinements:
  -- + variable patterns, e.g. "x", are refined to ctrs if "x" is 0-ary ctr
  -- + data patterns have to be defined constructors
  -- + cons (%::%) and list patterns ([%, %, %]) become data patterns (cons exps)
  refineVPat :: ValuePat Raw -> Refine (ValuePat Refined)
  refineVPat (VarPat x a) =
    do ctrs <- getRCtrs
       if x `elem` ctrs
         then return $ DataPat x [] (rawToRef a)
         else return $ VarPat x (rawToRef a)
  refineVPat (DataPat x xs a) =
    do ctrs <- getRCtrs
       if x `elem` ctrs
         then do xs' <- mapM refineVPat xs
                 return $ DataPat x xs' (rawToRef a)
         else throwError $ errorRefIdNotDeclared "constructor" x a
  refineVPat (IntPat i a) = return $ IntPat i (rawToRef a)
  refineVPat (CharPat c a) = return $ CharPat c (rawToRef a)
  refineVPat (StrPat s a) = return $ StrPat s (rawToRef a)
  refineVPat (ConsPat x xs a) =
    do x' <- refineVPat x
       xs' <- refineVPat xs
       return $ DataPat "cons" [x', xs'] (rawToRef a)
  refineVPat (ListPat ps a) =
    do ps' <- mapM refineVPat ps
       return $
         foldr
           (\x y -> DataPat "cons" [x, y] (rawToRef a))
           (DataPat "nil" [] (rawToRef a))
           ps'
  
  initialiseRState :: [DataT Raw] -> [Itf Raw] -> [ItfAlias Raw] -> Refine ()
  initialiseRState dts itfs itfAls =
    do i <- getRState
       itfs'   <- foldM addItf      (interfaces i)       itfs
       itfAls' <- foldM addItfAlias (interfaceAliases i) itfAls
       dts'    <- foldM addDataT    (datatypes i)        dts
       cmds'   <- foldM addCmd      (cmds i)             (concatMap getCmds itfs)
       ctrs'   <- foldM addCtr      (ctrs i)             (concatMap getCtrs dts)
       putRItfs       itfs'
       putRItfAliases itfAls'
       putRDTs        dts'
       putRCmds       cmds'
       putRCtrs       ctrs'
  
  makeIntBinOp :: Refined -> Char -> MHDef Refined
  makeIntBinOp a c = Def [c] (CType [Port [] (IntTy a) a
                                    ,Port [] (IntTy a) a]
                                    (Peg (Ab (AbVar "£" a) (ItfMap M.empty a) a) (IntTy a) a) a) [] a
  
  makeIntBinCmp :: Refined -> Char -> MHDef Refined
  makeIntBinCmp a c = Def [c] (CType [Port [] (IntTy a) a
                                     ,Port [] (IntTy a) a]
                               (Peg (Ab (AbVar "£" a) (ItfMap M.empty a) a)
                                (DTTy "Bool" [] a) a) a) [] a
  
  {-- The initial state for the refinement pass. -}
  
  builtinDataTs :: [DataT Refined]
  builtinDataTs = [DT "List" [("X", VT)] [Ctr "cons" [TVar "X" b
                                                         ,DTTy "List" [VArg (TVar "X" b) b] b] b
                                           ,Ctr "nil" [] b] b
                  ,DT "Unit" [] [Ctr "unit" [] b] b
                  ,DT "Bool" [] [Ctr "true" [] b, Ctr "false" [] b] b
                  ,DT "Ref" [("X", VT)] [] b]
    where b = Refined BuiltIn
  
  builtinItfs :: [Itf Raw]
  builtinItfs = [Itf "Console" [] [Cmd "inch" [] [] (CharTy b) b
                                  ,Cmd "ouch" [] [CharTy b]
                                   (DTTy "Unit" [] b) b
                                  ,Cmd "ouint" [] [IntTy b]
                                   (DTTy "Unit" [] b) b] b
                ,Itf "RefState" [] [Cmd "new" [("X", VT)] [TVar "X" b]
                                                              (DTTy "Ref" [VArg (TVar "X" b) b] b) b
                                     ,Cmd "write" [("X", VT)] [DTTy "Ref" [VArg (TVar "X" b) b] b
                                                               ,TVar "X" b]
                                                               (DTTy "Unit" [] b) b
                                     ,Cmd "read" [("X", VT)] [DTTy "Ref" [VArg (TVar "X" b) b] b]
                                                                (TVar "X" b) b] b]
    where b = Raw BuiltIn
  
  builtinItfAliases :: [ItfAlias Raw]
  builtinItfAliases = []
  
  builtinMHDefs :: [MHDef Refined]
  builtinMHDefs = map (makeIntBinOp (Refined BuiltIn)) "+-" ++
                  map (makeIntBinCmp (Refined BuiltIn)) "><" ++
                  [caseDef, charEq, alphaNumPred]
  
  charEq :: MHDef Refined
  charEq = Def "eqc" (CType [Port [] (CharTy a) a
                            ,Port [] (CharTy a) a]
                            (Peg (Ab (AbVar "£" a) (ItfMap M.empty a) a)
                                 (DTTy "Bool" [] a) a) a) [] a
    where a = Refined BuiltIn
  
  alphaNumPred :: MHDef Refined
  alphaNumPred = Def "isAlphaNum"
                 (CType [Port [] (CharTy a) a]
                            (Peg (Ab (AbVar "£" a) (ItfMap M.empty a) a)
                                 (DTTy "Bool" [] a) a) a) [] a
    where a = Refined BuiltIn
  
  caseDef :: MHDef Refined
  caseDef = Def
            "case"
            (CType
              [Port [] (TVar "X" b) b
              ,Port []
               (SCTy (CType [Port [] (TVar "X" b) b]
                        (Peg (Ab (AbVar "£" b) (ItfMap M.empty b) b) (TVar "Y" b) b) b) b) b]
              (Peg (Ab (AbVar "£" b) (ItfMap M.empty b) b) (TVar "Y" b) b) b)
            [Cls
              [VPat (VarPat "x" b) b, VPat (VarPat "f" b) b]
              (Use (App (Op (VarId "f" b) b)
                    [Use (Op (VarId "x" b) b) b] b) b) b] b
    where b = Refined BuiltIn
  
  builtinDTs :: DTMap
  builtinDTs = foldl add M.empty builtinDataTs
    where add m (DT id ps _ a) = M.insert id ps m
  
  builtinIFs :: IFMap
  builtinIFs = foldl add M.empty builtinItfs
    where add m (Itf id ps _ a) = M.insert id ps m
  
  builtinIFAliases :: IFAliasesMap
  builtinIFAliases = foldl add M.empty builtinItfAliases
    where add m (ItfAlias id ps itfMap a) = M.insert id (ps, itfMap) m
  
  builtinCtrs :: [Id]
  builtinCtrs = map add $ concatMap getCtrs builtinDataTs
    where add (Ctr id ts a) = id
  
  builtinCmds :: [Id]
  builtinCmds = map add $ concatMap getCmds builtinItfs
    where add (Cmd id _ ts _ a) = id
  
  initRefine :: RState
  initRefine = MkRState builtinIFs builtinIFAliases builtinDTs builtinCtrs
               builtinCmds M.empty S.empty Nothing
  
  {- Helper functions -}
  
  -- Add the id if not already present
  addEntry :: [Id] -> Id -> String -> Refine [Id]
  addEntry xs x prefix =
    if x `elem` xs then throwError (errorRefEntryAlreadyDefined prefix x)
    else return $ x : xs
  
  addItf :: IFMap -> Itf Raw -> Refine IFMap
  addItf m (Itf x ps _ a) =
    if M.member x m then
      throwError $ errorRefDuplTopTm "interface" x (getSource a)
    else return $ M.insert x ps m
  
  addItfAlias :: IFAliasesMap -> ItfAlias Raw -> Refine IFAliasesMap
  addItfAlias m (ItfAlias x ps itfMap a) =
    if M.member x m then
       throwError $ errorRefDuplTopTm "interface alias" x (getSource a)
    else return $ M.insert x (ps, itfMap) m
  
  addDataT :: DTMap -> DataT Raw -> Refine DTMap
  addDataT m (DT x ps _ a) =
    if M.member x m then
      throwError $ errorRefDuplTopTm "datatype" x (getSource a)
    else return $ M.insert x ps m
  
  addCtr :: [Id] -> Ctr a -> Refine [Id]
  addCtr xs (Ctr x _ _) = addEntry xs x "duplicate constructor:"
  
  addCmd :: [Id] -> Cmd a -> Refine [Id]
  addCmd xs (Cmd x _ _ _ _) = addEntry xs x "duplicate command:"
  
  uniqueIds :: [Id] -> Bool
  uniqueIds xs = length xs == length (nub xs)
  
  -- Helpers
  
  swap :: (a -> b -> c) -> b -> a -> c
  swap f b a = f a b
  
  rawToRef :: Raw -> Refined
  rawToRef (Raw loc) = Refined loc
  