import Control.Monad (forM_)
import Data.Char (chr, ord)
import Debug.Trace
import Prelude hiding (LT, GT, EQ)
import System.Environment (getArgs)
import System.Exit (exitFailure)
import Text.Parsec ((<|>))
import qualified Data.Map.Strict as M
import qualified Text.Parsec as P

-- TT Term
-- -------

-- Term ::=
--   | All: ∀(x: A) B
--   | Lam: λx f
--   | App: (f x)
--   | Slf: $(x: A) B
--   | Ann: {x: T}
--   | Ins: ~x
--   | Sum: (| A B)
--   | Inl: -x
--   | Inr: +x
--   | Mat: λ{ -: ifl | +: ifr }
--   | Mul: (& A B)
--   | Tup: #(a,b)
--   | Get: λ{ (,): ... }
--   | Uni: ⊤
--   | One: ()
--   | Tap: λ{ (): ... }
--   | Emp: ⊥
--   | Efq: λ{}
--   | Let: let x = A; B
--   | Use: use x = A; B
--   | Set: *
--   | Ref: x
--   | Var: x
data Term
  = All String Term (Term -> Term)
  | Lam String (Term -> Term)
  | App Term Term
  | Ann Bool Term Term
  | Slf String Term (Term -> Term)
  | Ins Term
  | Sum Term Term
  | Inl Term
  | Inr Term
  | Mat String String Term Term
  | Mul Term Term
  | Tup Term Term
  | Get String String Term
  | Uni
  | One
  | Tap Term
  | Emp
  | Efq
  | Let String Term (Term -> Term)
  | Use String Term (Term -> Term)
  | Set
  | Ref String
  | Var String Int
  | Hol String [Term]

-- Book of Definitions
type Book = M.Map String Term

-- Type-Checker Error
data Error = Error Int Term Term Term Int

-- Type-Checker Result
type Result a = Either Error a

-- Binding
-- -------

bind :: Term -> Term
bind term = go term [] where
  go (All nam inp bod) ctx = All nam (go inp ctx) (\x -> go (bod (Var nam 0)) ((nam, x) : ctx))
  go (Lam nam bod)     ctx = Lam nam (\x -> go (bod (Var nam 0)) ((nam, x) : ctx))
  go (App fun arg)     ctx = App (go fun ctx) (go arg ctx)
  go (Ann chk val typ) ctx = Ann chk (go val ctx) (go typ ctx)
  go (Slf nam typ bod) ctx = Slf nam (go typ ctx) (\x -> go (bod (Var nam 0)) ((nam, x) : ctx))
  go (Ins val)         ctx = Ins (go val ctx)
  go (Sum a b)         ctx = Sum (go a ctx) (go b ctx)
  go (Inl x)           ctx = Inl (go x ctx)
  go (Inr x)           ctx = Inr (go x ctx)
  go (Mat l r ifl ifr) ctx = Mat l r (go ifl ctx) (go ifr ctx)
  go (Mul a b)         ctx = Mul (go a ctx) (go b ctx)
  go (Tup a b)         ctx = Tup (go a ctx) (go b ctx)
  go (Get a b bod)     ctx = Get a b (go bod ctx)
  go Uni               ctx = Uni
  go One               ctx = One
  go (Tap bod)         ctx = Tap (go bod ctx)
  go Emp               ctx = Emp
  go Efq               ctx = Efq
  go (Let nam val bod) ctx = Let nam (go val ctx) (\x -> go (bod (Var nam 0)) ((nam, x) : ctx))
  go (Use nam val bod) ctx = Use nam (go val ctx) (\x -> go (bod (Var nam 0)) ((nam, x) : ctx))
  go Set               ctx = Set
  go (Ref nam)         ctx = case lookup nam ctx of { Just x -> x; Nothing -> Ref nam }
  go (Var nam idx)     ctx = Var nam idx
  go (Hol nam _)       ctx = Hol nam (map snd ctx)

-- Evaluation
-- ----------

-- Evaluation levels:
-- - 0: reduces refs: never
-- - 1: reduces refs: redexes
-- - 2: reduces refs: always

reduce :: Book -> Int -> Term -> Term
reduce book lv (App fun arg)     = reduceApp book lv (reduce book lv fun) arg
reduce book lv (Ann chk val typ) = reduce book lv val
reduce book lv (Ins val)         = reduce book lv val
reduce book lv (Let nam val bod) = reduce book lv (bod val)
reduce book lv (Use nam val bod) = reduce book lv (bod val)
reduce book lv (Ref nam)         = reduceRef book lv nam
reduce book lv (Hol nam ctx)     = Hol nam ctx
reduce book lv val               = val

reduceApp :: Book -> Int -> Term -> Term -> Term
reduceApp book 2  (Ref nam)         arg       = reduceApp book 2 (reduceRef book 2 nam) arg
reduceApp book 1  (Ref nam)         arg       = reduceApp book 1 (reduceRef book 1 nam) arg
reduceApp book lv (Lam nam bod)     arg       = reduce book lv (bod (reduce book 0 arg))
reduceApp book lv (Get a b bod)     (Tup x y) = reduce book lv (App (App bod (reduce book 0 x)) (reduce book 0 y))
reduceApp book lv (Mat l r ifl ifr) (Inl x)   = reduce book lv (App ifl (reduce book 0 x))
reduceApp book lv (Mat l r ifl ifr) (Inr x)   = reduce book lv (App ifr (reduce book 0 x))
reduceApp book lv fun arg                     = App fun arg

reduceRef :: Book -> Int -> String -> Term
reduceRef book 2  nam = case M.lookup nam book of
  Just val -> reduce book 2 val
  Nothing  -> error $ "Undefined: " ++ nam
reduceRef book 1  nam = Ref nam
reduceRef book lv nam = Ref nam

-- Normalization
-- -------------

normal :: Book -> Int -> Term -> Int -> Term
normal book lv term dep = go book lv (reduce book lv term) dep where
  go book lv (All nam inp bod) dep = All nam (normal book lv inp dep) (\x -> normal book lv (bod (Var nam dep)) (dep + 1))
  go book lv (Lam nam bod)     dep = Lam nam (\x -> normal book lv (bod (Var nam dep)) (dep + 1))
  go book lv (App fun arg)     dep = App (normal book lv fun dep) (normal book lv arg dep)
  go book lv (Slf nam typ bod) dep = Slf nam typ (\x -> normal book lv (bod (Var nam dep)) (dep + 1))
  go book lv (Ins val)         dep = Ins (normal book lv val dep)
  go book lv (Sum a b)         dep = Sum (normal book lv a dep) (normal book lv b dep)
  go book lv (Inl x)           dep = Inl (normal book lv x dep)
  go book lv (Inr x)           dep = Inr (normal book lv x dep)
  go book lv (Mat l r ifl ifr) dep = Mat l r (normal book lv ifl dep) (normal book lv ifr dep)
  go book lv (Mul a b)         dep = Mul (normal book lv a dep) (normal book lv b dep)
  go book lv (Tup a b)         dep = Tup (normal book lv a dep) (normal book lv b dep)
  go book lv (Get a b bod)     dep = Get a b (normal book lv bod dep)
  go book lv Uni               dep = Uni
  go book lv One               dep = One
  go book lv (Tap bod)         dep = Tap (normal book lv bod dep)
  go book lv Emp               dep = Emp
  go book lv Efq               dep = Efq
  go book lv (Let nam val bod) dep = Let nam (normal book lv val dep) (\x -> normal book lv (bod (Var nam dep)) (dep + 1))
  go book lv (Use nam val bod) dep = Use nam (normal book lv val dep) (\x -> normal book lv (bod (Var nam dep)) (dep + 1))
  go book lv Set               dep = Set
  go book lv (Ref nam)         dep = Ref nam
  go book lv (Var nam idx)     dep = Var nam idx
  go book lv (Ann chk val typ) dep = Ann chk (normal book lv val dep) (normal book lv typ dep)
  go book lv (Hol nam ctx)     dep = Hol nam ctx

-- Equality
-- --------

equal :: Book -> Term -> Term -> Int -> Result Bool
equal book a b dep = do
  let a' = reduce book 2 a
  let b' = reduce book 2 b
  same <- identical book a' b' dep
  if same
  then return True
  else similar book a' b' dep

similar :: Book -> Term -> Term -> Int -> Result Bool
similar book a b dep = go a b dep where
  go (All aNam aInp aBod) (All bNam bInp bBod) dep = do
    eInp <- equal book aInp bInp dep
    eBod <- equal book (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1)
    return (eInp && eBod)
  go (Lam aNam aBod) (Lam bNam bBod) dep =
    equal book (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1)
  go (App aFun aArg) (App bFun bArg) dep = do
    eFun <- similar book aFun bFun dep
    eArg <- equal book aArg bArg dep
    return (eFun && eArg)
  go (Slf aNam aTyp aBod) (Slf bNam bTyp bBod) dep =
    similar book (reduce book 0 aTyp) (reduce book 0 bTyp) dep
  go (Sum aA aB) (Sum bA bB) dep = do
    eA <- equal book aA bA dep
    eB <- equal book aB bB dep
    return (eA && eB)
  go (Mul aA aB) (Mul bA bB) dep = do
    eA <- equal book aA bA dep
    eB <- equal book aB bB dep
    return (eA && eB)
  go (Hol _ _) _ dep = return True
  go _ (Hol _ _) dep = return True
  go a b dep = identical book a b dep

identical :: Book -> Term -> Term -> Int -> Result Bool
identical book a b dep = go a b dep where
  go (All aNam aInp aBod) (All bNam bInp bBod) dep = do
    iInp <- identical book aInp bInp dep
    iBod <- identical book (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1)
    return (iInp && iBod)
  go (Lam aNam aBod) (Lam bNam bBod) dep =
    identical book (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1)
  go (App aFun aArg) (App bFun bArg) dep = do
    iFun <- identical book aFun bFun dep
    iArg <- identical book aArg bArg dep
    return (iFun && iArg)
  go (Slf aNam aTyp aBod) (Slf bNam bTyp bBod) dep =
    identical book aTyp bTyp dep
  go (Ins aVal) b dep =
    identical book aVal b dep
  go a (Ins bVal) dep =
    identical book a bVal dep
  go (Let aNam aVal aBod) b dep =
    identical book (aBod aVal) b dep
  go a (Let bNam bVal bBod) dep =
    identical book a (bBod bVal) dep
  go (Use aNam aVal aBod) b dep =
    identical book (aBod aVal) b dep
  go a (Use bNam bVal bBod) dep =
    identical book a (bBod bVal) dep
  go (Sum aA aB) (Sum bA bB) dep = do
    iA <- identical book aA bA dep
    iB <- identical book aB bB dep
    return (iA && iB)
  go (Inl aX) (Inl bX) dep =
    identical book aX bX dep
  go (Inr aX) (Inr bX) dep =
    identical book aX bX dep
  go (Mat aL aR aIfL aIfR) (Mat bL bR bIfL bIfR) dep = do
    iIfL <- identical book aIfL bIfL dep
    iIfR <- identical book aIfR bIfR dep
    return (iIfL && iIfR)
  go (Mul aA aB) (Mul bA bB) dep = do
    iA <- identical book aA bA dep
    iB <- identical book aB bB dep
    return (iA && iB)
  go (Tup aA aB) (Tup bA bB) dep = do
    iA <- identical book aA bA dep
    iB <- identical book aB bB dep
    return (iA && iB)
  go (Get aA aB aBod) (Get bA bB bBod) dep =
    identical book aBod bBod dep
  go Uni Uni dep =
    return True
  go One One dep =
    return True
  go (Tap aBod) (Tap bBod) dep =
    identical book aBod bBod dep
  go Emp Emp dep =
    return True
  go Efq Efq dep =
    return True
  go Set Set dep =
    return True
  go (Ann chk aVal aTyp) b dep =
    identical book aVal b dep
  go a (Ann chk bVal bTyp) dep =
    identical book a bVal dep
  go (Ref aNam) (Ref bNam) dep =
    return (aNam == bNam)
  go (Var aNam aIdx) (Var bNam bIdx) dep =
    return (aIdx == bIdx)
  go (Hol _ _) _ dep = return True
  go _ (Hol _ _) dep = return True
  go a b dep =
    return False

-- Type-Checking
-- -------------

infer :: Book -> Term -> Int -> Result Term
infer book term dep = {-trace ("infer " ++ termStr term dep) $-} go term dep where
  go (All nam inp bod) dep = do
    check book inp Set dep
    check book (bod (Ann False (Var nam dep) inp)) Set (dep + 1)
    return Set
  go (App fun arg) dep = do
    ftyp <- infer book fun dep
    case reduce book 2 ftyp of
      (All ftyp_nam ftyp_inp ftyp_bod) -> do
        check book arg ftyp_inp dep
        return $ ftyp_bod arg
      otherwise ->
        Left (Error 0 (Ref "function") ftyp (App fun arg) dep)
  go (Ann chk val typ) dep = do
    if chk then
      check book val typ dep
    else
      return ()
    return typ
  go (Slf nam typ bod) dep = do
    check book (bod (Ann False (Var nam dep) typ)) Set (dep + 1)
    return Set
  go (Ins val) dep = do
    vtyp <- infer book val dep
    case reduce book 2 vtyp of
      (Slf vtyp_nam vtyp_typ vtyp_bod) ->
        return $ vtyp_bod (Ins val)
      otherwise ->
        Left (Error 0 (Ref "self-type") vtyp (Ins val) dep)
  go (Sum a b) dep = do
    check book a Set dep
    check book b Set dep
    return Set
  go (Mul a b) dep = do
    check book a Set dep
    check book b Set dep
    return Set
  go Uni dep = return Set
  go One dep = return Uni
  go Emp dep = return Set
  go Set dep = return Set
  go (Let nam val bod) dep = do
    typ <- infer book val dep
    infer book (bod (Ann False (Var nam dep) typ)) dep
  go (Use nam val bod) dep =
    infer book (bod val) dep
  go (Inl x) dep = do
    xtyp <- infer book x dep
    return $ Sum xtyp (Hol "right_type" [])
  go (Inr x) dep = do
    xtyp <- infer book x dep
    return $ Sum (Hol "left_type" []) xtyp
  go (Tup a b) dep = do
    atyp <- infer book a dep
    btyp <- infer book b dep
    return $ Mul atyp btyp
  go t@(Mat _ _ _ _) dep =
    Left (Error 0 (Ref "type_annotation") (Ref "untyped_match") t dep)
  go t@(Get _ _ _) dep =
    Left (Error 0 (Ref "type_annotation") (Ref "untyped_get") t dep)
  go t@(Tap _) dep =
    Left (Error 0 (Ref "type_annotation") (Ref "untyped_tap") t dep)
  go t@(Lam nam bod) dep =
    Left (Error 0 (Ref "type_annotation") (Ref "untyped_lambda") t dep)
  go (Ref nam) dep =
    case M.lookup nam book of
      Just val -> infer book val dep
      Nothing  -> Left (Error 0 (Ref "undefined") (Ref "unknown_type") (Ref nam) dep)
  go (Var nam idx) dep =
    Left (Error 0 (Ref "type_annotation") (Ref "untyped_variable") (Var nam idx) dep)
  go (Hol nam ctx) dep = do
    trace (holStr nam (Ref "_") ctx) $ return Set

check :: Book -> Term -> Term -> Int -> Result ()
check book val typ dep = {-trace ("check " ++ termStr val dep ++ " :: " ++ termStr typ dep) $-} go val typ dep where
  go (Lam nam bod) typx dep =
    case reduce book 2 typx of
      (All typ_nam typ_inp typ_bod) -> do
        let ann  = Ann False (Var nam dep) typ_inp
        let term = bod ann
        let typx = typ_bod ann
        check book term typx (dep + 1)
      otherwise -> do
        _ <- infer book (Lam nam bod) dep
        return ()
  go (Tap bod) typx dep = 
    case reduce book 2 typx of
      (All typ_nam typ_inp typ_bod) -> do
        case reduce book 2 typ_inp of
          Uni -> do
            check book bod (typ_bod One) dep
          otherwise -> infer book (Tap bod) dep >> return ()
      otherwise -> infer book (Tap bod) dep >> return ()
  go (Mat l r ifl ifr) typx dep =
    case reduce book 2 typx of
      (All typ_nam typ_inp typ_bod) -> do
        case reduce book 2 typ_inp of
          (Sum typ_a typ_b) -> do
            check book ifl (All l typ_a $ \x -> (typ_bod (Inl x))) dep
            check book ifr (All r typ_b $ \x -> (typ_bod (Inr x))) dep
          otherwise -> infer book (Mat l r ifl ifr) dep >> return ()
      otherwise -> infer book (Mat l r ifl ifr) dep >> return ()
  go (Get a b bod) typx dep =
    case reduce book 2 typx of
      (All typ_nam typ_inp typ_bod) -> do
        case reduce book 2 typ_inp of
          (Mul typ_a typ_b) -> do
            check book bod (All a typ_a $ \x -> All b typ_b $ \y -> typ_bod (Tup x y)) dep
          otherwise -> infer book (Get a b bod) dep >> return ()
      otherwise -> infer book (Get a b bod) dep >> return ()
  go (Ins val) typx dep =
    case reduce book 2 typx of
      Slf typ_nam typ_typ typ_bod ->
        check book val (typ_bod (Ins val)) dep
      _ -> do
        _ <- infer book (Ins val) dep
        return ()
  go (Let nam val bod) typx dep = do
    typ <- infer book val dep
    check book (bod (Ann False (Var nam dep) typ)) typx dep
  go (Use nam val bod) typx dep =
    check book (bod val) typx dep
  go (Ann chk val typ) typx dep = do
    checkCompare book val typ typx dep
    if chk
    then check book val typ dep
    else return ()
  go (Inl x) typx dep =
    case reduce book 2 typx of
      Sum a b -> check book x a dep
      _       -> infer book (Inl x) dep >> return ()
  go (Inr x) typx dep =
    case reduce book 2 typx of
      Sum a b -> check book x b dep
      _       -> infer book (Inr x) dep >> return ()
  go (Tup x y) typx dep =
    case reduce book 2 typx of
      Mul a b -> do
        check book x a dep
        check book y b dep
      _ -> infer book (Tup x y) dep >> return ()
  go One typx dep =
    case reduce book 2 typx of
      Uni -> return ()
      _ -> Left (Error 0 Uni typx One dep)
  go (Hol nam ctx) typx dep = do
    trace (holStr nam typx ctx) $ return ()
  go term typx dep = do
    infer <- infer book term dep
    checkCompare book term typx infer dep

checkCompare :: Book -> Term -> Term -> Term -> Int -> Result ()
checkCompare book term expected detected dep = do
  equal <- equal book expected detected dep
  if equal then
    return ()
  else
    Left (Error 0 expected detected term dep)

checkDef :: Book -> Term -> Result ()
checkDef book (Ref nam) =
  case M.lookup nam book of
    Just val -> case val of
      Ann chk val typ -> check book val typ 0
      Ref nm2         -> checkDef book (Ref nm2)
      _               -> infer book val 0 >> return ()
    Nothing  -> Left (Error 0 (Ref "undefined") (Ref "unknown_type") (Ref nam) 0)
checkDef _ other = error "invalid top-level definition"

holStr :: String -> Term -> [Term] -> String
holStr name ty ctx = unlines $ ("GOAL: ?" ++ name ++ " : " ++ termStr ty 0) : map var (reverse ctx) where
  var (Ann _ tm ty) = "- " ++ termStr tm 0 ++ " : " ++ termStr ty 0
  var tm            = "- " ++ termStr tm 0

-- Stringification
-- ---------------

termStr :: Term -> Int -> String
termStr (All nam inp bod) dep =
  let nam' = nam
      inp' = termStr inp dep
      bod' = termStr (bod (Var nam dep)) (dep + 1)
  in concat ["∀(" , nam' , ": " , inp' , ") " , bod']
termStr (Lam nam bod) dep =
  let nam' = nam
      bod' = termStr (bod (Var nam dep)) (dep + 1)
  in concat ["λ" , nam' , " " , bod']
termStr (App fun arg) dep =
  let fun' = termStr fun dep
      arg' = termStr arg dep
  in concat ["(" , fun' , " " , arg' , ")"]
termStr (Ann chk val typ) dep =
  termStr val dep
  -- let val' = termStr val dep
      -- typ' = termStr typ dep
  -- in concat ["{" , val' , ": " , typ' , "}"]
termStr (Slf nam typ bod) dep =
  let nam' = nam
      typ' = termStr typ dep
      bod' = termStr (bod (Var nam dep)) (dep + 1)
  in concat ["$(" , nam' , ": " , typ' , ") " , bod']
termStr (Ins val) dep =
  let val' = termStr val dep
  in concat ["~" , val']
termStr (Sum a b) dep =
  let a' = termStr a dep
      b' = termStr b dep
  in concat ["(| " , a' , " " , b' , ")"]
termStr (Inl x) dep =
  let x' = termStr x dep
  in concat ["-" , x']
termStr (Inr x) dep =
  let x' = termStr x dep
  in concat ["+" , x']
termStr (Mat l r ifl ifr) dep =
  let l' = l
      r' = r
      ifl' = termStr ifl dep
      ifr' = termStr ifr dep
  in concat ["λ{ -: " , ifl' , " | +: " , ifr' , " }"]
termStr (Mul a b) dep =
  let a' = termStr a dep
      b' = termStr b dep
  in concat ["(& " , a' , " " , b' , ")"]
termStr (Tup a b) dep =
  let a' = termStr a dep
      b' = termStr b dep
  in concat ["#(" , a' , "," , b' , ")"]
termStr (Get a b bod) dep =
  let a' = a
      b' = b
      bod' = termStr bod dep
  in concat ["λ{ (,): " , bod' , " }"]
termStr Uni dep = "⊤"
termStr One dep = "()"
termStr (Tap bod) dep =
  let bod' = termStr bod dep
  in concat ["λ{ (): " , bod' , " }"]
termStr Emp dep = "⊥"
termStr Efq dep = "λ{}"
termStr (Let nam val bod) dep =
  let nam' = nam
      val' = termStr val dep
      bod' = termStr (bod (Var nam dep)) (dep + 1)
  in concat ["let " , nam' , " = " , val' , "; " , bod']
termStr (Use nam val bod) dep =
  let nam' = nam
      val' = termStr val dep
      bod' = termStr (bod (Var nam dep)) (dep + 1)
  in concat ["use " , nam' , " = " , val' , "; " , bod']
termStr Set dep = "*"
termStr (Ref nam) dep = nam
termStr (Var nam idx) dep = nam
termStr (Hol nam ctx) dep = "?" ++ nam

errorStr :: Book -> Error -> String
errorStr book (Error _ expected detected value dep) =
  let exp = termStr (normal book 0 expected dep) dep
      det = termStr (normal book 0 detected dep) dep
      val = termStr (normal book 0 value dep) dep
  in concat ["TypeMismatch:\n- Expected: ", exp, "\n- Detected: ", det, "\n- Bad-Term: ", val]

-- Parsing
-- -------

doParseTerm :: String -> Term
doParseTerm input = case P.parse parseTerm "" input of
  Left  err  -> error $ "Parse error: " ++ show err
  Right term -> bind term

parseTerm :: P.Parsec String () Term
parseTerm = do
  P.spaces
  P.choice
    [ parseAll
    , parseTap
    , parseMat
    , parseGet
    , parseLam
    , parseOne
    , parseSum
    , parseMul
    , parseApp
    , parseAnn
    , parseSlf
    , parseIns
    , parseInl
    , parseInr
    , parseTup
    , parseUni
    , parseEmp
    , parseEfq
    , parseUse
    , parseLet
    , parseSet
    , parseHol
    , parseRef
    ]

parseAll = do
  P.string "∀"
  P.char '('
  nam <- parseName
  P.char ':'
  inp <- parseTerm
  P.char ')'
  bod <- parseTerm
  return $ All nam inp (\x -> bod)

parseLam = do
  P.string "λ"
  nam <- parseName
  bod <- parseTerm
  return $ Lam nam (\x -> bod)

parseApp = do
  P.char '('
  fun <- parseTerm
  arg <- parseTerm
  P.char ')'
  return $ App fun arg

parseAnn = do
  P.char '{'
  val <- parseTerm
  P.spaces
  P.char ':'
  chk <- P.option False (P.char ':' >> return True)
  typ <- parseTerm
  P.spaces
  P.char '}'
  return $ Ann chk val typ

parseSlf = do
  P.string "$("
  nam <- parseName
  P.char ':'
  typ <- parseTerm
  P.char ')'
  bod <- parseTerm
  return $ Slf nam typ (\x -> bod)

parseIns = do
  P.char '~'
  val <- parseTerm
  return $ Ins val

parseSum = do
  P.try (P.string "(|")
  a <- parseTerm
  b <- parseTerm
  P.char ')'
  return $ Sum a b

parseInl = do
  P.char '-'
  x <- parseTerm
  return $ Inl x

parseInr = do
  P.char '+'
  x <- parseTerm
  return $ Inr x

parseMat = do
  P.try $ do
    P.string "λ{"
    P.spaces
    P.char '-'
  P.char ':'
  ifl <- parseTerm
  P.spaces
  P.char '|'
  P.spaces
  P.char '+'
  P.char ':'
  ifr <- parseTerm
  P.spaces
  P.char '}'
  return $ Mat "l" "r" ifl ifr

parseMul = do
  P.try (P.string "(&")
  a <- parseTerm
  b <- parseTerm
  P.char ')'
  return $ Mul a b

parseTup = do
  P.string "#("
  a <- parseTerm
  P.char ','
  b <- parseTerm
  P.char ')'
  return $ Tup a b

parseGet = do
  P.try $ do
    P.string "λ{"
    P.spaces
    P.string "(,):"
  bod <- parseTerm
  P.spaces
  P.char '}'
  return $ Get "a" "b" bod

parseUni = P.string "⊤" >> return Uni

parseOne = P.try (P.string "()" >> return One)

parseTap = do
  P.try $ do
    P.string "λ{"
    P.spaces
    P.string "():"
  bod <- parseTerm
  P.spaces
  P.char '}'
  return $ Tap bod

parseEmp = P.string "⊥" >> return Emp

parseEfq = P.try (P.string "λ{}") >> return Efq

parseUse = do
  P.try (P.string "use ")
  nam <- parseName
  P.spaces
  P.char '='
  val <- parseTerm
  P.char ';'
  bod <- parseTerm
  return $ Use nam val (\x -> bod)

parseLet = do
  P.try (P.string "let ")
  nam <- parseName
  P.spaces
  P.char '='
  val <- parseTerm
  P.char ';'
  bod <- parseTerm
  return $ Let nam val (\x -> bod)

parseSet = P.char '*' >> return Set

parseHol = do
  P.char '?'
  nam <- parseName
  return $ Hol nam []

parseRef = do
  name <- parseName
  return $ case name of
    "Set" -> Set
    _     -> Ref name

parseName :: P.Parsec String () String
parseName = do
  P.spaces
  head <- P.letter
  tail <- P.many (P.alphaNum <|> P.char '/' <|> P.char '.' <|> P.char '_' <|> P.char '-')
  return (head : tail)

parseBook :: P.Parsec String () Book
parseBook = do
  defs <- P.many parseDef
  return $ M.fromList defs

parseDef :: P.Parsec String () (String, Term)
parseDef = do
  name <- parseName
  P.spaces
  (typ, hasType) <- P.option (undefined, False) $ do
    P.char ':'
    typ <- parseTerm
    P.spaces
    return (typ, True)
  P.char '='
  value <- parseTerm
  P.char ';'
  P.spaces
  return (name, if hasType then Ann False value typ else value)

doParseBook :: String -> Book
doParseBook input = case P.parse parseBook "" input of
  Left  err  -> error $ "Parse error: " ++ show err
  Right book -> M.map bind book

-- API
-- ---

-- Normalizes a term
apiNormal :: Book -> Term -> IO ()
apiNormal book term = putStrLn $ termStr (normal book 2 term 0) 0

-- Type-checks a term
apiCheck :: Book -> Term -> IO ()
apiCheck book term = case checkDef book term of
  Right () -> putStrLn "Checked."
  Left err -> putStrLn $ errorStr book err

-- Main
-- ----

book :: Book
book = M.fromList []

main :: IO ()
main = do
  content <- readFile "main.tt"
  let book = doParseBook content
  forM_ (M.toList book) $ \(name, term) -> do
    case checkDef book (Ref name) of
      Right () -> putStrLn $ "Checked " ++ name ++ "."
      Left err -> putStrLn $ errorStr book err