content: {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE ViewPatterns #-}
  {-# LANGUAGE LambdaCase #-}
  module RefineSyntax where
  
  import Control.Monad
  import Control.Monad.Except
  import Control.Monad.State
  import Data.Functor.Identity
  
  import Data.List
  import qualified Data.Map.Strict as M
  import qualified Data.Set as S
  
  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:
  -- + check if main function exists
  -- + built-in data types, interfaces, operators are added
  refine' :: Prog Raw -> Refine (Prog Refined)
  refine' (MkProg xs) = do
    -- Concretise epsilon ty vars
    let (dts, itfs, itfAls) = concretiseEps (getDataTs xs) (getItfs xs) (getItfAliases xs)
        hdrSigs = getHdrSigs xs
        hdrDefs = getHdrDefs xs []
    -- Initialise refinement state
    initialiseRState dts itfs itfAls hdrSigs
    -- Refine top level terms
    putTopLevelCtxt Datatype
    dtTms <- mapM refineDataT dts
    putTopLevelCtxt Interface
    itfTms <- mapM refineItf itfs
    putTopLevelCtxt InterfaceAlias
    itfAlTms <- mapM refineItfAl itfAls
    putTopLevelCtxt Handler
    hdrs <- mapM (refineMH hdrDefs) hdrSigs
    if existsMain hdrs then
      return $ MkProg (map (\dt -> DataTm dt a) builtinDataTs ++ dtTms ++
                       map (\itf -> ItfTm itf a) builtinItfs ++ itfTms ++
                       map (\hdr -> DefTm hdr a) builtinMHDefs ++ hdrs)
    else throwError errorRefNoMainFunction
    where a = Refined (BuiltIn)
  
  existsMain :: [TopTm Refined] -> Bool
  existsMain ((DefTm (Def id _ _ _) _) : xs) = id == "main" || existsMain xs
  existsMain [] = False
  existsMain (_ : xs) = error "invalid top term: expected multihandler"
  
  -- Explicit refinements:
  -- + data type has unique effect & type variables
  -- + implicit eff var [£] is defined explicitly
  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
  -- + implicit eff var [£] is defined explicitly
  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
  -- + implicit eff var [£] is defined explicitly
  refineItfAl :: ItfAlias Raw -> Refine (ItfAlias Refined)
  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 (map tyVar2rawTyVarArg ps)) (Raw Implicit)
         itfMap' <- refineItfMap $ singletonItfMap
         putEVSet S.empty                                -- reset
         putTMap M.empty                                 -- reset
         return $ ItfAlias itfAl ps itfMap' a'
    else throwError $ errorRefDuplParamItfAl i
    where a' = rawToRef a
  
  -- Explicit refinements:
  -- + command has unique effect & type variables
  -- + implicit eff var [£] is defined explicitly
  refineCmd :: Cmd Raw -> Refine (Cmd Refined)
  refineCmd c@(Cmd id ps xs y a) =
  --        id : forall p_1 ... p_m, x_1 -> ... -> x_n -> y
    if uniqueIds (map fst ps) then
      do tmap <- getTMap
         evset <- getEVSet
         -- 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 argument types and result type
             -- first, add temp. val, eff ty vars
             putTMap (M.union tmap (M.fromList $ zip tvs (map (swap TVar a) tvs)))
             putEVSet (S.union evset (S.fromList evs))
             -- then, refine
             xs' <- mapM refineVType xs
             y' <- refineVType y
             -- finally, reset temp. val, eff ty vars
             putTMap tmap
             putEVSet evset
             return $ Cmd id ps xs' y' a'
         else throwError $ "a type parameter of command " ++ id ++
                           "already occurs as interface type parameter"  -- TODO: LC: Shadowing should be allowed, fix this in future
    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 adj ty a) = do adj' <- refineAdj adj
                                  ty' <- refineVType ty
                                  return $ Port adj' 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 if itf_i contains effect variable
       es <- getEVars $ M.toList m
       if null es then do m' <- refineItfMap mp
                          return $ Ab (refineAbMod v) m' a'
       else if length es == 1 then do let u = head es
                                      m' <- refineItfMap (ItfMap (M.delete u m) a)
                                      return $ Ab (AbVar u a') m' a'
       else throwError $ errorRefAbMultEffVars ab es
    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
  getEVars :: [(Id,[TyArg Raw])] -> Refine [Id]
  getEVars ((x, ts) : ys) =
    do p <- getEVSet
       es <- getEVars ys
       if S.member x p then
         if length ts == 0 then return $ x : es
         else throwError $ errorRefEffVarNoParams x ts
       else return es
  getEVars [] = return []
  
  -- Explicit refinements:
  -- + implicit [£] ty args to interfaces are made explicit
  refineItfMap :: ItfMap Raw -> Refine (ItfMap Refined)
  refineItfMap (ItfMap m a) = do
    -- replace interface aliases by interfaces
    xs <- concat <$> mapM substitItfAls (M.toList m)
    -- refine each interface
    xs' <- mapM refineEntry xs
    return $ ItfMap (M.fromList xs') (rawToRef a)
    where refineEntry :: (Id, [TyArg Raw]) -> Refine (Id, [TyArg Refined])
          refineEntry (x, ts) =
  --                  x t_1 ... t_n
            do itfs <- getRItfs
               case M.lookup x itfs of
                 Just ps ->
  --               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} := [£]
                   do let a' = Raw (implicitNear a)
                          ts' = if length ps == length ts + 1 &&
                                   (snd (ps !! length ts) == ET) then
                                     ts ++ [EArg (Ab (AbVar "£" a') (ItfMap M.empty a') a') a']
                                else ts
                      checkArgs x (length ps) (length ts') a
                      ts'' <- mapM refineTyArg ts'
                      return (x, ts'')
                 Nothing -> throwError $ errorRefIdNotDeclared "interface" x a
  
  refineAbMod :: AbMod Raw -> AbMod Refined
  refineAbMod (EmpAb a) = EmpAb (rawToRef a)
  refineAbMod (AbVar x a) = AbVar x (rawToRef a)
  
  refineAdj :: Adj Raw -> Refine (Adj Refined)
  refineAdj (Adj m a) = do m' <- refineItfMap m
                           return $ Adj m' (rawToRef a)
  
  -- Explicit refinements:
  -- + implicit [£] ty args to data types are made explicit
  -- + MkDTTy is distinguished between being (in the following precedence)
  --   1) data type indeed            -> MkDTTy
  --   2) (implicitly) intro'd ty var -> MkTVar  (if no ty args)
  --   3) neither                     -> error
  -- + MkTVar is distinguished between being
  --   1) intro'd ty var              -> MkTVar
  --   2) data type                   -> MkDTTy
  --   3) neither                     -> MkTVar
  -- + 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 dtm <- getRDTs
       case M.lookup x dtm of
         Just ps -> do
  --        1) data x p_1 ... p_n
  --    or  2) data x p_1 ... p_n [£]       ([£] has been explicitly added before)
                        -- If 2), set t_{n+1} := [£]
           let a' = Raw (implicitNear a)
               ts' = if length ps == length ts + 1 &&
                        (snd (ps !! length ts) == ET)
                     then ts ++ [EArg (Ab (AbVar "£" a') (ItfMap M.empty a') a') a']
                     else ts
           checkArgs x (length ps) (length ts') a
           ts'' <- mapM refineTyArg ts'
           return $ DTTy x ts'' (rawToRef a)
         Nothing -> do
           m <- getTMap
           ctx <- getTopLevelCtxt
           if null ts &&  -- there must be no arguments to ty var
              (isHdrCtxt ctx || -- x can be implic. poly. ty var in hdr sign.
               M.member x m)    -- x can be in val ty contexts
           then return $ TVar x (rawToRef a)
           else throwError $ errorRefIdNotDeclared "type variable" x a
  refineVType (SCTy ty a) = refineCType ty >>= return . (swap SCTy (rawToRef a))
  refineVType (TVar x a) =
    do tmap <- getTMap
       dtm <- getRDTs
       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 -> return $ TVar x (rawToRef 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) MkDataCon:              0-ary constructor if matching
  --                        2) MkUse . MkOp . MkCmdId: command operator if matching
  --                        3) MkUse . MkOp . MkPoly:  poly multihandler operator if it exists
  --                        4) MkUse . MkOp . MkMono:  mono multihandler
  -- + 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
       hdrs <- getRMHs
       case id `findPair` ctrs of
          Just n -> do checkArgs id n 0 a
                       return $ Right $ DCon (DataCon id [] a') a'
          Nothing ->
            case id `findPair` cmds of
              Just n -> return $ Left $ Op (CmdId id a') a'
              -- LC: Do we need to check command's arity = 0?
              Nothing ->
                case id `findPair` hdrs of
                  -- polytypic (n=0 means: takes no argument, x!)
                  Just n -> return $ Left $ Op (Poly id a') a'
                  -- LC: Same here, check for handler's arity = 0?
                  -- monotypic: must be local variable
                  Nothing -> return $ Left $ Op (Mono id a') a'
    where a' = rawToRef a
  refineUse (RawComb (RawId id b) xs a) =
    do xs' <- mapM refineTm xs
       ctrs <- getRCtrs
       cmds <- getRCmds
       hdrs <- getRMHs
       case id `findPair` ctrs of
          Just n -> do checkArgs id n (length xs') a
                       return $ Right $ DCon (DataCon id xs' b') a'
          Nothing ->
            case id `findPair` cmds of
              Just n -> do checkArgs id n (length xs') a
                           return $ Left $ App (Op (CmdId id b') b') xs' a'
              Nothing ->
                case id `findPair` hdrs of
                  Just n -> do checkArgs id n (length xs') a
                               return $ Left $ App (Op (Poly id b') b') xs' a'
                  Nothing -> return $ Left $ App (Op (Mono 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
  
  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 (Poly "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 and match # of args
  refinePattern :: Pattern Raw -> Refine (Pattern Refined)
  refinePattern (VPat p a) = VPat <$> refineVPat p <*> (pure $ rawToRef a)
  refinePattern (CmdPat x ps k a) =
    do cmds <- getRCmds
       case x `findPair` cmds of
         Just n -> do checkArgs x n (length ps) a
                      ps' <- mapM refineVPat ps
                      return $ CmdPat x ps' k (rawToRef a)
         Nothing -> throwError $ errorRefIdNotDeclared "command" x a
  refinePattern (ThkPat x a) = return $ ThkPat x (rawToRef a)
  
  -- Explicit refinements:
  -- + variable patterns, e.g. "x", are refined to constructors if "x" is 0-ary constructor
  -- + data patterns have to be fully instantiated constructors
  -- + cons (%::%) and list patterns ([%, %, %]) become data patterns (cons expressions)
  refineVPat :: ValuePat Raw -> Refine (ValuePat Refined)
  refineVPat (VarPat x a) =
    do ctrs <- getRCtrs
       case x `findPair` ctrs of
         Just n -> do checkArgs x n 0 a
                      return $ DataPat x [] (rawToRef a)
         Nothing -> return $ VarPat x (rawToRef a)
  refineVPat (DataPat x xs a) =
    do ctrs <- getRCtrs
       case x `findPair` ctrs of
         Just n -> do checkArgs x n (length xs) a
                      xs' <- mapM refineVPat xs
                      return $ DataPat x xs' (rawToRef a)
         Nothing -> 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] -> [MHSig Raw] -> Refine ()
  initialiseRState dts itfs itfAls hdrs =
    do i <- getRState
       itfs'   <- foldM addItf      (interfaces i)       itfs
       itfAls' <- foldM addItfAlias (interfaceAliases i) itfAls
       dts'    <- foldM addDataT    (datatypes i)        dts
       hdrs'   <- foldM addMH       (handlers i)         hdrs
       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'
       putRMHs        hdrs'
  
  makeIntBinOp :: Refined ->Char -> MHDef Refined
  makeIntBinOp a c = Def [c] (CType [Port (Adj (ItfMap M.empty a) a) (IntTy a) a
                                    ,Port (Adj (ItfMap M.empty a) a) (IntTy a) a]
                                    (Peg (Ab (AbVar "£" a) (ItfMap M.empty a) a) (IntTy 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 "Ref" [("X", VT)] [] b]
    where b = Refined BuiltIn
  
  builtinItfs :: [Itf Refined]
  builtinItfs = [Itf "Console" [] [Cmd "inch" [] [] (CharTy b) b
                                    ,Cmd "ouch" [] [CharTy 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 = Refined BuiltIn
  
  builtinItfAliases :: [ItfAlias Raw]
  builtinItfAliases = []
  
  builtinMHDefs :: [MHDef Refined]
  builtinMHDefs = map (makeIntBinOp (Refined BuiltIn)) "+-" ++ [caseDef]
  
  caseDef :: MHDef Refined
  caseDef = Def
            "case"
            (CType
              [Port (Adj (ItfMap M.empty b) b) (TVar "X" b) b
              ,Port (Adj (ItfMap M.empty b) b)
               (SCTy (CType [Port (Adj (ItfMap M.empty b) b) (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 (Mono "f" b) b) [Use (Op (Mono "x" b) b) b] b) b) b] b
    where b = Refined BuiltIn
  
  builtinMHs :: [IPair]
  builtinMHs = map add builtinMHDefs
    where add (Def x (CType ps _ a) _ _) = (x,length ps)
  
  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 :: [IPair]
  builtinCtrs = map add $ concatMap getCtrs builtinDataTs
    where add (Ctr id ts a) = (id,length ts)
  
  builtinCmds :: [IPair]
  builtinCmds = map add $ concatMap getCmds builtinItfs
    where add (Cmd id _ ts _ a) = (id,length ts)
  
  initRefine :: RState
  initRefine = MkRState builtinIFs builtinIFAliases builtinDTs builtinMHs builtinCtrs
               builtinCmds (MkProg []) M.empty S.empty Nothing
  
  {- Helper functions -}
  
  mem :: Id -> [IPair] -> Bool
  mem x xs = x `elem` (map fst xs)
  
  findPair :: Id -> [IPair] -> Maybe Int
  findPair x ((y,n) : xs) = if x == y then Just n else findPair x xs
  findPair _ _ = Nothing
  
  collectCmds :: [Cmd a] -> [Id]
  collectCmds ((Cmd cmd _ _ _ a) : xs) = cmd : (collectCmds xs)
  collectCmds [] = []
  
  collectCtrs :: [Ctr a] -> [Id]
  collectCtrs ((Ctr ctr _ a) : xs) = ctr : (collectCtrs xs)
  collectCtrs [] = []
  
  getHdrSigs :: [TopTm Raw] -> [MHSig Raw]
  getHdrSigs xs = getHdrSigs' xs []
    where getHdrSigs' :: [TopTm Raw] -> [MHSig Raw] -> [MHSig Raw]
          getHdrSigs' ((SigTm sig a) : xs) ys = getHdrSigs' xs (sig : ys)
          getHdrSigs' (_ : xs) ys = getHdrSigs' xs ys
          getHdrSigs' [] ys = ys
  
  collectMHNames :: [MHSig Raw] -> [Id]
  collectMHNames ((Sig hdr _ a) : xs) = hdr : (collectMHNames xs)
  collectMHNames [] = []
  
  getHdrDefs :: [TopTm Raw] -> [MHCls Raw] -> [MHCls Raw]
  getHdrDefs ((ClsTm cls a) : xs) ys = getHdrDefs xs (cls : ys)
  getHdrDefs (_ : xs) ys = getHdrDefs xs ys
  getHdrDefs [] ys = reverse ys
  
  -- Add the name if not already present
  addEntry :: [IPair] -> Id -> Int -> String -> Refine [IPair]
  addEntry xs x n prefix = if x `mem` xs then throwError (errorRefEntryAlreadyDefined prefix x)
                           else return $ (x,n) : xs
  
  -- addItf :: [IPair] -> Itf a -> Refine [IPair]
  -- addItf xs (MkItf x ps _) = addEntry xs x (length ps) "duplicate interface: "
  
  addItf :: IFMap -> Itf Raw -> Refine IFMap
  addItf m (Itf x ps _ a) = if M.member x m then
                               throwError $ errorRefDuplTopTm "interface" x 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 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 "data type" x a
                             else return $ M.insert x ps m
  
  addCtr :: [IPair] -> Ctr a -> Refine [IPair]
  addCtr xs (Ctr x ts a) = addEntry xs x (length ts) "duplicate constructor: "
  
  addCmd :: [IPair] -> Cmd a -> Refine [IPair]
  addCmd xs (Cmd x _ ts _ a) = addEntry xs x (length ts) "duplicate command: "
  
  -- takes map handler-id -> #-of-ports and adds another handler entry
  addMH :: [IPair] -> MHSig Raw -> Refine [IPair]
  addMH xs (Sig x (CType ps p _) _) =
    addEntry xs x (length ps) "duplicate multihandler: "
  
  uniqueIds :: [Id] -> Bool
  uniqueIds xs = length xs == length (nub xs)
  
  -- helpers
  
  checkArgs :: Id -> Int -> Int -> Raw -> Refine ()
  checkArgs x exp act a =
    if exp /= act then
      throwError $ errorRefNumberOfArguments x exp act a
    else return ()
  
  swap :: (a -> b -> c) -> b -> a -> c
  swap f b a = f a b
  
  rawToRef :: Raw -> Refined
  rawToRef (Raw loc) = Refined loc
  