    {-# OPTIONS -fglasgow-exts #-}

    module Agda.Auto.Typecheck where

    import Data.IORef

    import Agda.Auto.NarrowingSearch
    import Agda.Auto.Syntax
    import Agda.Auto.SearchControl
    import Agda.Auto.Print

    closify :: a -> Clos a o
    closify = Clos []

    sub :: CExp o -> Clos a o -> Clos a o
    -- sub e (Clos [] x) = Clos [Sub e] x
    sub e (Clos (Skip : as) x) = Clos (Sub e : as) x
    {-sub e (Clos (Weak n : as) x) = if n == 1 then
                                    Clos as x
                                   else
                                    Clos (Weak (n - 1) : as) x-}
    sub _ _ = error "sub: pattern not matched"

    msubs :: [CExp o] -> a -> Clos a o
    msubs ss x = Clos (map Sub ss) x

    weak :: Nat -> Clos a o -> Clos a o
    weak 0 x = x
    weak n (Clos as x) = Clos (Weak n : as) x

    {- -- only used by eta-conversion
    weakarglist :: Nat -> CArgList -> CArgList
    weakarglist 0 = id
    weakarglist n = f
     where f CALNil = CALNil
           f (CALConcat cl as as2) = CALConcat (Weak n : cl) as (f as2)

    weakelr :: Nat -> Elr -> Elr
    weakelr 0 elr = elr
    weakelr n (Var v) = Var (v + n)
    weakelr _ elr@(Const _) = elr
    -}

    -- ---------------------------------

    tcExp :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
    tcExp isdep ctx typ trm =
     mbpcase prioTypeUnknown (hnn typ) (ptcTypeUnknown isdep ctx typ trm) $ \hntyp ->
     mmpcase (True, prioTypecheck isdep, Just (RIMainInfo (length ctx) hntyp)) trm (ptcTypeCheck isdep ctx hntyp trm) $ \trm -> case trm of
      App elr args -> do
       (ityp, sc) <- case elr of
                Var v ->  -- assuming within scope
                 return (weak (v + 1) (snd $ ctx !! v), id)
                Const c -> do
                 cdef <- readIORef c
                 return (closify (cdtype cdef), \x -> mpret $ And (Just [Term args]) (noiotastep' c args) x)
       sc $ tcargs isdep ctx typ ityp args
      Lam hid (Abs id1 b) -> case hntyp of
       HNFun hid' it ot | hid == hid' ->
        tcExp isdep ((id1, it) : ctx) (weak 1 ot) b
       HNPi hid' _ it (Abs id2 ot) | hid == hid' ->
        tcExp isdep ((pickid id1 id2, it) : ctx) ot b
       _ -> mpret $ Error "tcExp, type of lam should be fun or pi (and same hid)"
      Fun _ it ot -> case hntyp of
       HNSort s ->
        mpret $ And (Just [Term ctx])
         (tcExp isdep ctx (closify (NotM $ Sort s)) it)
         (tcExp isdep ctx (closify (NotM $ Sort s)) ot)
       _ -> mpret $ Error "tcExp, type of fun should be set"
      Pi _ _ it (Abs id ot) -> case hntyp of
       HNSort s ->
        mpret $ And (Just [Term ctx, Term it])
         (tcExp True ctx (closify (NotM $ Sort s)) it)
         (tcExp isdep ((id, closify it) : ctx) (closify (NotM $ Sort s)) ot)
       _ -> mpret $ Error "tcExp, type of pi should be set"
      Sort (SortLevel i) -> case hntyp of
       HNSort s2 -> case s2 of
        SortLevel j -> mpret $ if i < j then OK else Error "tcExp, type of set should be larger set"
        Type -> mpret OK
       _ -> mpret $ Error "tcExp, type of set should be set"
      Sort Type -> error "tcexp: Sort Type should not occur"

    tcargs :: Bool -> Ctx o -> CExp o -> CExp o -> MArgList o -> EE (MyPB o)
    tcargs isdep ctx etyp ityp args = mmpcase (True, prioTypecheckArgList, Nothing) args (ptcTypecheckArgList "" isdep ctx etyp ityp args) $ \args' -> case args' of
     ALNil -> comp' etyp ityp
     ALCons hid a as ->
      mbpcase prioInferredTypeUnknown (hnn ityp) (ptcTypecheckArgList "inferred_type_unknown" isdep ctx etyp ityp args) $ \hnityp -> case hnityp of
       HNFun hid' it ot | hid == hid' -> mpret $
        And (Just [Term ctx])
            (tcExp isdep ctx it a)
            (tcargs isdep ctx etyp ot as)
       HNPi hid' possdep it (Abs _ ot) | hid == hid' -> mpret $
        And (Just [Term ctx, Term a])
            (tcExp (isdep || possdep) ctx it a)
            (tcargs isdep ctx etyp (sub (closify a) ot) as)
       _ -> mpret $ Error "tcargs, inf type should be fun or pi (and same hid)"
     ALConPar _ -> error "ConPar should not occur here"

    -- ---------------------------------

    hnn :: CExp o -> EE (MyMB (HNExp o) o)
    hnn e = hnn' e CALNil

    hnn' :: CExp o -> CArgList o -> EE (MyMB (HNExp o) o)
    hnn' e as =
     mbcase (hn' e as) $ \hne ->
      mbcase (iotastep hne) $ \res -> case res of
       Nothing -> mbret hne
       Just (e, as) -> hnn' e as

    hn' :: CExp o -> CArgList o -> EE (MyMB (HNExp o) o)
    hn' e as = mbcase (hnc False e as) $ \res -> case res of
                HNDone hne -> mbret hne
                HNMeta _ _ -> error "hn': should not happen"

    data HNRes o = HNDone (HNExp o)
                 | HNMeta (CExp o) (CArgList o)

    hnc :: Bool -> CExp o -> CArgList o -> EE (MyMB (HNRes o) o)
    hnc haltmeta = loop
     where
      loop ce@(Clos cl e) cargs =
       (if haltmeta then mmmcase e (mbret $ HNMeta ce cargs) else mmcase e) $
       \e -> case e of
        App elr args ->
         let cargs' = CALConcat (Clos cl args) cargs
         in  case elr of
          Var v -> case doclos cl v of
           Left v' -> mbret $ HNDone $ HNApp (Var v') cargs'
           Right f -> loop f cargs'
          Const _ -> mbret $ HNDone $ HNApp elr cargs'
        Lam _ (Abs id b) ->
         let cb = Clos (Skip : cl) b
         in  mbcase (hnarglist cargs) $ \hncargs -> case hncargs of
          HNALNil -> mbret $ HNDone $ HNLam (Abs id cb)
          HNALCons arg cargs' -> loop (sub arg cb) cargs'
          HNALConPar _ -> error "ConPar should not occur here"
        Fun hid it ot -> checkNoArgs cargs $ mbret $ HNDone $ HNFun hid (Clos cl it) (Clos cl ot)
        Pi hid possdep it (Abs id ot) -> checkNoArgs cargs $ mbret $ HNDone $ HNPi hid possdep (Clos cl it) (Abs id (Clos (Skip : cl) ot))
        Sort s -> checkNoArgs cargs $ mbret $ HNDone $ HNSort s
      checkNoArgs cargs c =
       mbcase (hnarglist cargs) $ \hncargs -> case hncargs of
        HNALNil -> c
        HNALCons _ _ -> mbfailed "hnc: there should be no args"
        HNALConPar _ -> error "ConPar should not occur here"

    doclos :: [CAction o] -> Nat -> Either Nat (CExp o)
    doclos = f 0
     where
      f ns [] i = Left (ns + i)
      f ns (Weak n : xs) i = f (ns + n) xs i
      f ns (Skip : _) 0 = Left ns
      f ns (Sub s : _) 0 = Right (weak ns s)
      f ns (Skip : xs) i = f (ns + 1) xs (i - 1)
      f ns (Sub _ : xs) i = f ns xs (i - 1)

    hnarglist :: CArgList o -> EE (MyMB (HNArgList o) o)
    hnarglist args = case args of
     CALNil -> mbret HNALNil
     CALConcat (Clos cl args) args2 -> mmcase args $ \args -> case args of
       ALNil -> hnarglist args2
       ALCons _ arg args' -> mbret $ HNALCons (Clos cl arg) (CALConcat (Clos cl args') args2)
       ALConPar args' -> mbret $ HNALConPar (CALConcat (Clos cl args') args2)

    -- -----------------------------

    getNArgs :: Nat -> CArgList o -> EE (MyMB (Maybe ([CExp o], CArgList o)) o)
    getNArgs 0 args = mbret $ Just ([], args)
    getNArgs narg args =
     mbcase (hnarglist args) $ \hnargs -> case hnargs of
      HNALNil -> mbret Nothing
      HNALCons arg args' ->
       mbcase (getNArgs (narg - 1) args') $ \res -> case res of
        Nothing -> mbret Nothing
        Just (pargs, rargs) -> mbret $ Just (arg : pargs, rargs)
      HNALConPar _ -> error "ConPar should not occur here"

    getAllArgs :: CArgList o -> EE (MyMB [PEval o] o)
    getAllArgs args =
     mbcase (hnarglist args) $ \hnargs -> case hnargs of
      HNALNil -> mbret []
      HNALCons arg args' ->
       mbcase (getAllArgs args') $ \args'' ->
        mbret (PENo arg : args'')
      HNALConPar args' ->
       mbcase (getAllArgs args') $ \args'' ->
        mbret (PEConPar : args'')

    iotastep :: HNExp o -> EE (MyMB (Maybe (CExp o, CArgList o)) o)
    iotastep e = case e of
     HNApp (Const c) args -> do
      cd <- readIORef c
      case cdcont cd of
       Def narg cls ->
        mbcase (getNArgs narg args) $ \res -> case res of
         Nothing -> mbret Nothing
         Just (pargs, rargs) ->
          mbcase (dorules cls (map PENo pargs)) $ \res -> case res of
           Nothing -> mbret Nothing
           Just rhs -> mbret $ Just (rhs, rargs)
       _ -> mbret Nothing
     _ -> mbret Nothing

    data PEval o = PENo (CExp o)
                 | PEConApp (CExp o) (ConstRef o) [PEval o]
                 | PEConPar

    dorules :: [Clause o] -> [PEval o] -> EE (MyMB (Maybe (CExp o)) o)
    dorules [] _ = mbret Nothing
    dorules (rule:rules') as =
     mbcase (dorule rule as) $ \x -> case x of
      Left (Just as') -> dorules rules' as'
      Left Nothing -> mbret Nothing
      Right rhs -> mbret $ Just rhs

    dorule :: Clause o -> [PEval o] -> EE (MyMB (Either (Maybe [PEval o]) (CExp o)) o)
    dorule (pats, rhs) as =
     mbcase (dopats pats as) $ \x -> case x of
      Right (_, ss) -> mbret $ Right (msubs ss rhs)
      Left hnas -> mbret $ Left hnas

    dopats :: [Pat o] -> [PEval o] -> EE (MyMB (Either (Maybe [PEval o]) ([PEval o], [CExp o])) o)
    dopats [] [] = mbret $ Right ([], [])
    dopats (p:ps') (a:as') =
     mbcase (dopat p a) $ \x -> case x of
      Right (hna, ss) ->
       mbcase (dopats ps' as') $ \x -> case x of
        Right (hnas, ss2) -> mbret $ Right (hna : hnas, ss2 ++ ss)
        Left Nothing -> mbret $ Left Nothing
        Left (Just hnas) -> mbret $ Left $ Just (hna : hnas)
      Left Nothing -> mbret $ Left Nothing
      Left (Just hna) -> mbret $ Left $ Just (hna : as')
    dopats _ _ = error "dopats: pattern not matched"

    dopat :: Pat o -> PEval o -> EE (MyMB (Either (Maybe (PEval o)) (PEval o, [CExp o])) o)
    dopat (PatConApp c pas) a =
     case a of
      PENo a -> mbcase (hnn a) $ \hna -> case hna of
       HNApp (Const c') as ->
        if c == c' then
         mbcase (getAllArgs as) $ \as' ->
          if length as' == length pas then
           mbcase (dopats pas as') $ \x -> case x of
            Right (hnas, ss) -> mbret $ Right (PEConApp a c' hnas, ss)
            Left Nothing -> mbret $ Left Nothing
            Left (Just hnas) -> mbret $ Left $ Just (PEConApp a c' hnas)
          else
           mbfailed "dopat: wrong amount of args"
        else do
         cd <- readIORef c'
         case cdcont cd of
          Constructor -> mbcase (getAllArgs as) $ \as' ->
           mbret $ Left (Just (PEConApp a c' as'))
          _ -> mbret $ Left Nothing
       _ -> mbret $ Left Nothing
      aa@(PEConApp a c' as) ->
       if c == c' then
        if length as == length pas then
         mbcase (dopats pas as) $ \x -> case x of
          Right (hnas, ss) -> mbret $ Right (PEConApp a c' hnas, ss)
          Left Nothing -> mbret $ Left Nothing
          Left (Just hnas) -> mbret $ Left $ Just (PEConApp a c' hnas)
        else
         mbfailed "dopat: wrong amount of args"
       else
        mbret $ Left (Just aa)
      PEConPar -> error "ConPar should not occur here"
    dopat PatVar a@(PENo a') = mbret $ Right (a, [a'])
    dopat PatVar a@(PEConApp a' _ _) = mbret $ Right (a, [a'])
    dopat PatVar PEConPar = error "ConPar should not occur here"
    dopat PatExp a = mbret $ Right (a, [])

    -- -----------------------------

    noiotastep :: HNExp o -> EE (MyPB o)
    noiotastep hne =
     mbpcase prioNo (iotastep hne) (ptcNoIotaStep hne) $ \res -> case res of
      Just _ -> mpret $ Error "iota step possible contrary to assumed"
      Nothing -> mpret OK

    noiotastep' :: ConstRef o -> MArgList o -> EE (MyPB o)
    noiotastep' c args = do
     cd <- readIORef c
     let isshorthand =
          case cdcont cd of
           Def _ [(pats, _)] -> all (\pat -> case pat of {PatConApp{} -> False; _ -> True}) pats
           _ -> False
     if isshorthand then
       mpret OK
      else
       noiotastep $ HNApp (Const c) (CALConcat (Clos [] args) CALNil)

    comp' :: CExp o -> CExp o -> EE (MyPB o)
    comp' = comp True

    comp :: Bool -> CExp o -> CExp o -> EE (MyPB o)
    comp ineq e1 e2 = f e1 CALNil $ \res1 -> f e2 CALNil $ \res2 -> g res1 res2
     where
      f e as cont =
       mbpcase prioPreCompare (hnc True e as) (ptcCompare "beta" ineq e1 e2) $ \res ->
        case res of
         HNDone hne ->
          mmbpcase (iotastep hne)
           (mpret $ Or prioCompChoice
            (mpret $ And Nothing
             (noiotastep hne)
             (cont res)
            )
            (mbpcase prioCompIota (iotastep hne) (ptcCompare "iota" ineq e1 e2) $ \res -> case res of
             Nothing -> mpret $ Error "no iota step possible, contrary to assumed"
             Just (e, as) -> f e as cont
            )
           )
           (\res' -> case res' of
             Nothing -> cont res
             Just (e, as) -> f e as cont
           )
         HNMeta _ _ -> cont res
      g res1 res2 =
       case (res1, res2) of
        (HNDone hne1, HNDone hne2) -> comphn' ineq hne1 hne2
        (HNDone hne1, HNMeta ce2 cargs2) -> unif True hne1 ce2 cargs2
        (HNMeta ce1 cargs1, HNDone hne2) -> unif False hne2 ce1 cargs1
        (HNMeta ce1@(Clos _ m1) cargs1, HNMeta ce2@(Clos _ m2) cargs2) -> doubleblock m1 m2 $ f ce1 cargs1 $ \res1 -> f ce2 cargs2 $ \res2 -> g res1 res2
      unif oppis1 opphne = loop
       where
        loop ce@(Clos cl m) cargs =
         do
          let Meta mm = m
          mmpcase (False, prioCompare, Just (RIUnifInfo mm cl opphne)) m (ptcCompare "unify" ineq e1 e2) $ \_ ->
           f ce cargs $ \res ->
            case res of
             HNDone hne -> if oppis1 then comphn' ineq opphne hne else comphn' ineq hne opphne
             HNMeta ce' cargs' -> loop ce' cargs'

    comphn' :: Bool -> HNExp o -> HNExp o -> EE (MyPB o)
    comphn' ineq hne1 hne2 =
     case (hne1, hne2) of
      (HNApp elr1 args1, HNApp elr2 args2) ->
       let ce = case (elr1, elr2) of
                 (Var v1, Var v2) -> if v1 == v2 then Nothing else Just "comphn, elr, vars not equal"
                 (Const c1, Const c2) -> if c1 == c2 then Nothing else Just "comphn, elr, consts not equal"
                 (_, _) -> Just "comphn, elrs not equal"
       in  case ce of
            Nothing -> compargs args1 args2
            Just msg -> mpret $ Error msg
      (HNLam (Abs id1 b1), HNLam (Abs id2 b2)) -> comp False b1 b2
    {- eta-conversion disabled
      (HNLam (Abs id b), HNApp elr args) ->
       mbpcase False prioCompare (hn b) $ \hnb ->
       comphn False (id : idctx) hnb (HNApp (weakelr 1 elr) (CALConcat (weakarglist 1 args) (CALCons (closify (NotM $ App (Var 0) $ NotM ALNil)) CALNil)))
      (HNApp elr args, HNLam (Abs id b)) ->
       mbpcase False prioCompare (hn b) $ \hnb ->
       comphn False (id : idctx) (HNApp (weakelr 1 elr) (CALConcat (weakarglist 1 args) (CALCons (closify (NotM $ App (Var 0) $ NotM ALNil)) CALNil))) hnb
    -}
      (HNFun hid1 it1 ot1, HNFun hid2 it2 ot2) | hid1 == hid2 -> mpret $
       And (Just []) (comp False it1 it2) (comp ineq ot1 ot2)
      (HNPi hid1 _ it1 (Abs id1 ot1), HNPi hid2 _ it2 (Abs id2 ot2)) | hid1 == hid2 -> mpret $
       And (Just []) (comp False it1 it2) (comp ineq ot1 ot2)
      (HNFun hid1 it1 ot1, HNPi hid2 _ it2 (Abs id ot2)) | hid1 == hid2 -> mpret $  -- ?? exclude this case
       And (Just []) (comp False it1 it2) (comp ineq (weak 1 ot1) ot2)
      (HNPi hid1 _ it1 (Abs id ot1), HNFun hid2 it2 ot2) | hid1 == hid2 -> mpret $  -- ?? exclude this case
       And (Just []) (comp False it1 it2) (comp ineq ot1 (weak 1 ot2))
      (HNSort s1, HNSort s2) -> mpret $
       case (s1, s2) of
        (SortLevel i1, SortLevel i2) -> if i1 == i2 || ineq && i1 > i2 then OK else Error "comphn, set levels not matching"
        (Type, SortLevel _) | ineq -> OK
        _ -> error "comphn'.2: case should not occur"
      (_, _) -> mpret $ Error "comphn, not equal"

    compargs :: CArgList o -> CArgList o -> EE (MyPB o)
    compargs args1 args2 =
     mbpcase prioCompareArgList (hnarglist args1) (ptcCompareArgList "lhs" args1 args2) $ \hnargs1 ->
     mbpcase prioCompareArgList (hnarglist args2) (ptcCompareArgList "rhs" args1 args2) $ \hnargs2 ->
     case (hnargs1, hnargs2) of
      (HNALNil, HNALNil) -> mpret OK
      (HNALCons arg1 args1', HNALCons arg2 args2') -> mpret $
       And (Just []) (comp False arg1 arg2) (compargs args1' args2')
      (HNALConPar args1', HNALCons _ args2') -> compargs args1' args2'
      (HNALCons _ args1', HNALConPar args2') -> compargs args1' args2'
      (HNALConPar args1', HNALConPar args2') -> compargs args1' args2'
      (_, _) -> mpret $ Error $ "compargs, not equal"

    pickid :: MId -> MId -> MId
    pickid mid1@(Id _) _ = mid1
    pickid _ mid2 = mid2

    -- ---------------------------------

    tcSearch :: Ctx o -> CExp o -> MExp o -> EE (MyPB o)
    tcSearch ctx typ trm = tcExp False ctx typ trm

    -- ----------------------------

    norm = True

    ptcTypeUnknown :: Bool -> Ctx o -> CExp o -> MExp o -> EE String
    ptcTypeUnknown isdep ctx typ trm = do
     pctx <- printCtx norm ctx
     ptyp <- printCExp norm (map fst ctx) typ
     ptrm <- printExp (map fst ctx) trm
     return $ "tt_unknown " ++ (if isdep then "dep " else "") ++ pctx ++ " | " ++ ptrm ++ " : " ++ ptyp

    ptcTypeCheck :: Bool -> Ctx o -> HNExp o -> MExp o -> EE String
    ptcTypeCheck isdep ctx hntyp trm = do
     pctx <- printCtx norm ctx
     ptyp <- printHNExp norm (map fst ctx) hntyp
     ptrm <- printExp (map fst ctx) trm
     return $ (if isdep then "dep " else "") ++ pctx ++ " | " ++ ptrm ++ " : " ++ ptyp

    ptcTypecheckArgList :: String -> Bool -> Ctx o -> CExp o -> CExp o -> MArgList o -> EE String
    ptcTypecheckArgList msg isdep ctx etyp ityp args = do
     pctx <- printCtx norm ctx
     petyp <- printCExp norm (map fst ctx) etyp
     pityp <- printCExp norm (map fst ctx) ityp
     pargs <- pargs (map fst ctx) args
     return $ msg ++ " " ++ (if isdep then "dep " else "") ++ pctx ++ " | " ++ pargs ++ " : " ++ pityp ++ " => " ++ petyp

    ptcNoIotaStep :: HNExp o -> EE String
    ptcNoIotaStep hne = do
     phne <- printHNExp norm [] hne
     return $ "no_iota " ++ phne

    ptcCompare :: String -> Bool -> CExp o -> CExp o -> EE String
    ptcCompare msg ineq e1 e2 = do
     pe1 <- printCExp norm [] e1
     pe2 <- printCExp norm [] e2
     return $ msg ++ " " ++ pe1 ++ (if ineq then " >= " else " == ") ++ pe2

    ptcCompareArgList :: String -> CArgList o -> CArgList o -> EE String
    ptcCompareArgList msg args1 args2 = do
     pargs1 <- pcargs norm [] args1
     pargs2 <- pcargs norm [] args2
     return $ msg ++ " " ++ pargs1 ++ " == " ++ pargs2

    -- ---------------------------------------------------

    phnexp :: Bool -> Int -> [MId] -> HNExp o -> IO String
    phnexp norm p ctx e = case e of
     HNApp elr args -> do
      elr' <- pelr ctx elr
      args' <- pcargs norm ctx args
      par p 3 $ elr' ++ args'
     HNLam (Abs id b) -> do
      b' <- pcexp norm 1 (id : ctx) b
      par p 1 $ "\\" ++ pid ctx id ++ " -> " ++ b'
     HNFun _ it ot -> do
      it' <- pcexp norm 3 ctx it
      ot' <- pcexp norm 2 ctx ot
      par p 2 $ it' ++ " -> " ++ ot'
     HNPi _ _ it (Abs id ot) -> do
      it' <- pcexp norm 1 ctx it
      ot' <- pcexp norm 2 (id : ctx) ot
      par p 2 $ "[" ++ pid ctx id ++ ":" ++ it' ++ "] -> " ++ ot'
     HNSort (SortLevel 0) -> return "*"
     HNSort (SortLevel n) -> return $ "*" ++ show n
     HNSort Type -> return "Type"

    printHNExp norm = phnexp norm 4

    phnargs :: Bool -> [MId] -> HNArgList o -> IO String
    phnargs norm ctx args = case args of
      HNALNil -> return ""
      HNALCons arg args -> do
       arg' <- pcexp norm 4 ctx arg
       args' <- pcargs norm ctx args
       return $ " " ++ arg' ++ args'
      HNALConPar args -> do
       args' <- pcargs norm ctx args
       return $ " " ++ "$" ++ args'

    pcexp :: Bool -> Int -> [MId] -> CExp o -> IO String
    pcexp True p ctx cexp = do
     res <- hnn cexp
     case res of
      NotB hnexp -> phnexp True p ctx hnexp
      _ -> pcexp False p ctx cexp
    pcexp False p ctx (Clos acts e) = do  -- TODO: handle closure properly
     pe <- pexp p ctx e
     return $ "<..>" ++ pe

    printCExp norm = pcexp norm 4

    pcargs :: Bool -> [MId] -> CArgList o -> IO String
    pcargs True ctx args = do
     res <- hnarglist args
     case res of
      NotB hnargs -> phnargs True ctx hnargs
      _ -> pcargs False ctx args
    pcargs False ctx args = case args of
      CALNil -> return ""
      CALConcat (Clos acts arg) args -> do  -- TODO: handle closure properly
       arg' <- pargs ctx arg
       args' <- pcargs False ctx args
       return $ "<..>" ++ arg' ++ args'

    printCtx :: Bool -> Ctx o -> IO String
    printCtx _ [] = return ""
    printCtx norm ((mid, t) : ctx) = do
     p <- printCExp norm (map fst ctx) t
     ps <- printCtx norm ctx
     return $ ps ++ ", " ++ pid (map fst ctx) mid ++ " : " ++ p