{-# LINE 149 "LP.lhs" #-}
  module LP where
{-# LINE 152 "LP.lhs" #-}
  import Prelude hiding (print)
{-# LINE 154 "LP.lhs" #-}
  import Control.Monad.Error
  import Data.List
  import Data.Char
{-# LINE 159 "LP.lhs" #-}
  import Text.PrettyPrint.HughesPJ hiding (parens)
  import qualified Text.PrettyPrint.HughesPJ as PP
{-# LINE 164 "LP.lhs" #-}
  import Text.ParserCombinators.Parsec hiding (parse, State)
  import qualified Text.ParserCombinators.Parsec as P
  import Text.ParserCombinators.Parsec.Token
  import Text.ParserCombinators.Parsec.Language
{-# LINE 171 "LP.lhs" #-}
  import System.Console.Readline
  import System.IO hiding (print)
{-# LINE 176 "LP.lhs" #-}
  putstrln x = putStrLn x
{-# LINE 5 "Parser.lhs" #-}
  simplyTyped = makeTokenParser (haskellStyle { identStart = letter <|> P.char '_',
                                                reservedNames = ["let", "assume", "putStrLn"] })
{-# LINE 9 "Parser.lhs" #-}
  parseBindings :: CharParser () ([String], [Info])
  parseBindings = 
                     (let rec :: [String] -> [Info] -> CharParser () ([String], [Info])
                          rec e ts =
                            do
                             (x,t) <- parens lambdaPi
                                        (do
                                           x <- identifier simplyTyped 
                                           reserved simplyTyped "::"
                                           t <- pInfo
                                           return (x,t))
                             (rec (x : e) (t : ts) <|> return (x : e, t : ts))
                      in rec [] [])
                     <|>
                     do  x <- identifier simplyTyped 
                         reserved simplyTyped "::"
                         t <- pInfo
                         return ([x], [t])
    where
      pInfo = fmap HasType (parseType 0 []) <|> fmap (const (HasKind Star)) (reserved simplyTyped "*")
{-# LINE 30 "Parser.lhs" #-}
  parseStmt :: [String] -> CharParser () (Stmt ITerm Info)
  parseStmt e =
        do
          reserved simplyTyped "let"
          x <- identifier simplyTyped
          reserved simplyTyped "="
          t <- parseITerm 0 e
          return (Let x t)
    <|> do
          reserved simplyTyped "assume"
          (xs, ts) <- parseBindings
          return (Assume (reverse (zip xs ts)))
    <|> do
          reserved simplyTyped "putStrLn"
          x <- stringLiteral simplyTyped
          return (PutStrLn x)
    <|> do
          reserved lambdaPi "out"
          x <- option "" (stringLiteral simplyTyped)
          return (Out x)
    <|> fmap Eval (parseITerm 0 e)
{-# LINE 52 "Parser.lhs" #-}
  parseType :: Int -> [String] -> CharParser () Type
  parseType 0 e =
    try
       (do
          t <- parseType 1 e
          rest t <|> return t)
    where
      rest t =
        do
          reserved simplyTyped "->"
          t' <- parseType 0 e
          return (Fun t t')
  parseType 1 e =
        do
          x <- identifier simplyTyped
          return (TFree (Global x))
    <|> parens simplyTyped (parseType 0 e)
{-# LINE 70 "Parser.lhs" #-}
  parseITerm :: Int -> [String] -> CharParser () ITerm
  parseITerm 0 e =
    try
       (do
          t <- parseITerm 1 e
          return t)
  parseITerm 1 e =
    try
       (do
          t <- parseITerm 2 e
          rest (Inf t) <|> return t)
    <|> do
          t <- parens simplyTyped (parseLam e)
          rest t
    where
      rest t =
        do
          reserved simplyTyped "::"
          t' <- parseType 0 e
          return (Ann t t')
  parseITerm 2 e =
        do
          t <- parseITerm 3 e
          ts <- many (parseCTerm 3 e)
          return (foldl (:@:) t ts)
  parseITerm 3 e =
        do
          x <- identifier simplyTyped
          case findIndex (== x) e of
            Just n  -> return (Bound n)
            Nothing -> return (Free (Global x))
    <|> parens simplyTyped (parseITerm 0 e)
  
  parseCTerm :: Int -> [String] -> CharParser () CTerm
  parseCTerm 0 e =
        parseLam e
    <|> fmap Inf (parseITerm 0 e)
  parseCTerm p e =
        try (parens simplyTyped (parseLam e))
    <|> fmap Inf (parseITerm p e)
  
  parseLam :: [String] -> CharParser () CTerm
  parseLam e =
        do reservedOp simplyTyped "\\"
           xs <- many1 (identifier simplyTyped)
           reservedOp simplyTyped "->"
           t <- parseCTerm 0 (reverse xs ++ e)
           --  reserved simplyTyped "."
           return (iterate Lam t !! length xs)
{-# LINE 122 "Parser.lhs" #-}
  parseIO :: String -> CharParser () a -> String -> IO (Maybe a)
  parseIO f p x = case P.parse (whiteSpace simplyTyped >> p >>= \ x -> eof >> return x) f x of
                    Left e  -> putStrLn (show e) >> return Nothing
                    Right r -> return (Just r)
{-# LINE 5 "Printer.lhs" #-}
  tPrint :: Int -> Type -> Doc
  tPrint p (TFree (Global s))  =  text s
  tPrint p (Fun ty ty')        =  parensIf (p > 0) (sep [tPrint 0 ty <> text " ->", nest 2 (tPrint 0 ty')])
{-# LINE 10 "Printer.lhs" #-}
  iPrint :: Int -> Int -> ITerm -> Doc
  iPrint p ii (Ann c ty)       =  parensIf (p > 1) (cPrint 2 ii c <> text " :: " <> tPrint 0 ty)
  iPrint p ii (Bound k)        =  text (vars !! (ii - k - 1))
  iPrint p ii (Free (Global s))=  text s
  iPrint p ii (i :@: c)        =  parensIf (p > 2) (sep [iPrint 2 ii i, nest 2 (cPrint 3 ii c)])
  iPrint p ii x                =  text ("[" ++ show x ++ "]")
{-# LINE 17 "Printer.lhs" #-}
  cPrint :: Int -> Int -> CTerm -> Doc
  cPrint p ii (Inf i)    = iPrint p ii i
  cPrint p ii (Lam c)    = parensIf (p > 0) (text "\\ " <> text (vars !! ii) <> text " -> " <> cPrint 0 (ii + 1) c)
{-# LINE 21 "Printer.lhs" #-}
  vars :: [String]
  vars = [ c : n | n <- "" : map show [1..], c <- ['x','y','z'] ++ ['a'..'w'] ]
{-# LINE 24 "Printer.lhs" #-}
  parensIf :: Bool -> Doc -> Doc
  parensIf True  = PP.parens
  parensIf False = id
{-# LINE 28 "Printer.lhs" #-}
  print = render . cPrint 0 0
  printType = render . tPrint 0
{-# LINE 5 "Parser-LP.lhs" #-}
  lambdaPi = makeTokenParser (haskellStyle { identStart = letter <|> P.char '_',
                                             reservedNames = ["forall", "let", "assume", "putStrLn", "out"] })
{-# LINE 9 "Parser-LP.lhs" #-}
  parseStmt_ :: [String] -> CharParser () (Stmt ITerm_ CTerm_)
  parseStmt_ e =
        do
          reserved lambdaPi "let"
          x <- identifier lambdaPi
          reserved lambdaPi "="
          t <- parseITerm_ 0 e
          return (Let x t)
    <|> do
          reserved lambdaPi "assume"
          (xs, ts) <- parseBindings_ False [] 
          return (Assume (reverse (zip xs ts)))
    <|> do
          reserved lambdaPi "putStrLn"
          x <- stringLiteral lambdaPi
          return (PutStrLn x)
    <|> do
          reserved lambdaPi "out"
          x <- option "" (stringLiteral lambdaPi)
          return (Out x)
    <|> fmap Eval (parseITerm_ 0 e)
{-# LINE 31 "Parser-LP.lhs" #-}
  parseBindings_ :: Bool -> [String] -> CharParser () ([String], [CTerm_])
  parseBindings_ b e = 
                     (let rec :: [String] -> [CTerm_] -> CharParser () ([String], [CTerm_])
                          rec e ts =
                            do
                             (x,t) <- parens lambdaPi
                                        (do
                                           x <- identifier lambdaPi
                                           reserved lambdaPi "::"
                                           t <- parseCTerm_ 0 (if b then e else [])
                                           return (x,t))
                             (rec (x : e) (t : ts) <|> return (x : e, t : ts))
                      in rec e [])
                     <|>
                     do  x <- identifier lambdaPi
                         reserved lambdaPi "::"
                         t <- parseCTerm_ 0 e
                         return (x : e, [t])
{-# LINE 50 "Parser-LP.lhs" #-}
  parseITerm_ :: Int -> [String] -> CharParser () ITerm_
  parseITerm_ 0 e =
        do
          reserved lambdaPi "forall"
          (fe,t:ts) <- parseBindings_ True e
          reserved lambdaPi "."
          t' <- parseCTerm_ 0 fe
          return (foldl (\ p t -> Pi_ t (Inf_ p)) (Pi_ t t') ts)
    <|>
    try
       (do
          t <- parseITerm_ 1 e
          rest (Inf_ t) <|> return t)
    <|> do
          t <- parens lambdaPi (parseLam_ e)
          rest t
    where
      rest t =
        do
          reserved lambdaPi "->"
          t' <- parseCTerm_ 0 ([]:e)
          return (Pi_ t t')
  parseITerm_ 1 e =
    try
       (do
          t <- parseITerm_ 2 e
          rest (Inf_ t) <|> return t)
    <|> do
          t <- parens lambdaPi (parseLam_ e)
          rest t
    where
      rest t =
        do
          reserved lambdaPi "::"
          t' <- parseCTerm_ 0 e
          return (Ann_ t t')
  parseITerm_ 2 e =
        do
          t <- parseITerm_ 3 e
          ts <- many (parseCTerm_ 3 e)
          return (foldl (:$:) t ts)
  parseITerm_ 3 e =
        do
          reserved lambdaPi "*"
          return Star_
    <|> do
          n <- natural lambdaPi
          return (toNat_ n)
    <|> do
          x <- identifier lambdaPi
          case findIndex (== x) e of
            Just n  -> return (Bound_ n)
            Nothing -> return (Free_ (Global x))
    <|> parens lambdaPi (parseITerm_ 0 e)
  
  parseCTerm_ :: Int -> [String] -> CharParser () CTerm_
  parseCTerm_ 0 e =
        parseLam_ e
    <|> fmap Inf_ (parseITerm_ 0 e)
  parseCTerm_ p e =
        try (parens lambdaPi (parseLam_ e))
    <|> fmap Inf_ (parseITerm_ p e)
  
  parseLam_ :: [String] -> CharParser () CTerm_
  parseLam_ e =
        do reservedOp lambdaPi "\\"
           xs <- many1 (identifier lambdaPi)
           reservedOp lambdaPi "->"
           t <- parseCTerm_ 0 (reverse xs ++ e)
           --  reserved lambdaPi "."
           return (iterate Lam_ t !! length xs)
{-# LINE 123 "Parser-LP.lhs" #-}
  toNat_ :: Integer -> ITerm_
  toNat_ n = Ann_ (toNat_' n) (Inf_ Nat_)
{-# LINE 126 "Parser-LP.lhs" #-}
  toNat_' :: Integer -> CTerm_
  toNat_' 0  =  Zero_
  toNat_' n  =  Succ_ (toNat_' (n - 1))
{-# LINE 5 "Printer-LP.lhs" #-}
  iPrint_ :: Int -> Int -> ITerm_ -> Doc
  iPrint_ p ii (Ann_ c ty)       =  parensIf (p > 1) (cPrint_ 2 ii c <> text " :: " <> cPrint_ 0 ii ty)
  iPrint_ p ii Star_             =  text "*"
  iPrint_ p ii (Pi_ d (Inf_ (Pi_ d' r)))
                                 =  parensIf (p > 0) (nestedForall_ (ii + 2) [(ii + 1, d'), (ii, d)] r)
  iPrint_ p ii (Pi_ d r)         =  parensIf (p > 0) (sep [text "forall " <> text (vars !! ii) <> text " :: " <> cPrint_ 0 ii d <> text " .", cPrint_ 0 (ii + 1) r])
  iPrint_ p ii (Bound_ k)        =  text (vars !! (ii - k - 1))
  iPrint_ p ii (Free_ (Global s))=  text s
  iPrint_ p ii (i :$: c)         =  parensIf (p > 2) (sep [iPrint_ 2 ii i, nest 2 (cPrint_ 3 ii c)])
  iPrint_ p ii Nat_              =  text "Nat"
  iPrint_ p ii (NatElim_ m z s n)=  iPrint_ p ii (Free_ (Global "natElim") :$: m :$: z :$: s :$: n)
  iPrint_ p ii (Vec_ a n)        =  iPrint_ p ii (Free_ (Global "Vec") :$: a :$: n)
  iPrint_ p ii (VecElim_ a m mn mc n xs)
                                 =  iPrint_ p ii (Free_ (Global "vecElim") :$: a :$: m :$: mn :$: mc :$: n :$: xs)
  iPrint_ p ii (Eq_ a x y)       =  iPrint_ p ii (Free_ (Global "Eq") :$: a :$: x :$: y)
  iPrint_ p ii (EqElim_ a m mr x y eq)
                                 =  iPrint_ p ii (Free_ (Global "eqElim") :$: a :$: m :$: mr :$: x :$: y :$: eq)
  iPrint_ p ii (Fin_ n)          =  iPrint_ p ii (Free_ (Global "Fin") :$: n)
  iPrint_ p ii (FinElim_ m mz ms n f)
                                 =  iPrint_ p ii (Free_ (Global "finElim") :$: m :$: mz :$: ms :$: n :$: f)
  iPrint_ p ii x                 =  text ("[" ++ show x ++ "]")
{-# LINE 28 "Printer-LP.lhs" #-}
  cPrint_ :: Int -> Int -> CTerm_ -> Doc
  cPrint_ p ii (Inf_ i)    = iPrint_ p ii i
  cPrint_ p ii (Lam_ c)    = parensIf (p > 0) (text "\\ " <> text (vars !! ii) <> text " -> " <> cPrint_ 0 (ii + 1) c)
  cPrint_ p ii Zero_       = fromNat_ 0 ii Zero_     --  text "Zero"
  cPrint_ p ii (Succ_ n)   = fromNat_ 0 ii (Succ_ n) --  iPrint_ p ii (Free_ (Global "Succ") :$: n)
  cPrint_ p ii (Nil_ a)    = iPrint_ p ii (Free_ (Global "Nil") :$: a)
  cPrint_ p ii (Cons_ a n x xs) =
                             iPrint_ p ii (Free_ (Global "Cons") :$: a :$: n :$: x :$: xs)
  cPrint_ p ii (Refl_ a x) = iPrint_ p ii (Free_ (Global "Refl") :$: a :$: x)
  cPrint_ p ii (FZero_ n)  = iPrint_ p ii (Free_ (Global "FZero") :$: n)
  cPrint_ p ii (FSucc_ n f)= iPrint_ p ii (Free_ (Global "FSucc") :$: n :$: f)
{-# LINE 40 "Printer-LP.lhs" #-}
  fromNat_ :: Int -> Int -> CTerm_ -> Doc
  fromNat_ n ii Zero_ = int n
  fromNat_ n ii (Succ_ k) = fromNat_ (n + 1) ii k
  fromNat_ n ii t = parensIf True (int n <> text " + " <> cPrint_ 0 ii t)
{-# LINE 45 "Printer-LP.lhs" #-}
  nestedForall_ :: Int -> [(Int, CTerm_)] -> CTerm_ -> Doc
  nestedForall_ ii ds (Inf_ (Pi_ d r)) = nestedForall_ (ii + 1) ((ii, d) : ds) r
  nestedForall_ ii ds x                = sep [text "forall " <> sep [parensIf True (text (vars !! n) <> text " :: " <> cPrint_ 0 n d) | (n,d) <- reverse ds] <> text " .", cPrint_ 0 ii x]
{-# LINE 5 "Interpreter.lhs" #-}
  data Stmt i tinf = Let String i           --  let x = t
                   | Assume [(String,tinf)] --  assume x :: t, assume x :: *
                   | Eval i
                   | PutStrLn String        --  lhs2TeX hacking, allow to print "magic" string
                   | Out String             --  more lhs2TeX hacking, allow to print to files
    deriving (Show)
{-# LINE 13 "Interpreter.lhs" #-}
  --  read-eval-print loop
  readevalprint :: Interpreter i c v t tinf inf -> State v inf -> IO ()
  readevalprint int state@(inter, out, ve, te) =
    let rec int state =
          do
            x <- catch
                   (if inter
                    then readline (iprompt int) 
                    else fmap Just getLine)
                   (\_ -> return Nothing)
            case x of
              Nothing   ->  return ()
              Just ""   ->  rec int state
              Just x    ->
                do
                  when inter (addHistory x)
                  c  <- interpretCommand x
                  state' <- handleCommand int state c
                  maybe (return ()) (rec int) state'
    in
      do
        --  welcome
        when inter $ putStrLn ("Interpreter for " ++ iname int ++ ".\n" ++
                               "Type :? for help.")
        --  enter loop
        rec int state
{-# LINE 40 "Interpreter.lhs" #-}
  data Command = TypeOf String
               | Compile CompileForm
               | Browse
               | Quit
               | Help
               | Noop
 
  data CompileForm = CompileInteractive  String
                   | CompileFile         String
  
  data InteractiveCommand = Cmd [String] String (String -> Command) String
  
  type NameEnv v = [(Name, v)]
  type Ctx inf = [(Name, inf)]
  type State v inf = (Bool, String, NameEnv v, Ctx inf)
  
  commands :: [InteractiveCommand]
  commands
    =  [ Cmd [":type"]        "<expr>"  TypeOf         "print type of expression",
         Cmd [":browse"]      ""        (const Browse) "browse names in scope",
         Cmd [":load"]        "<file>"  (Compile . CompileFile)
                                                       "load program from file",
         Cmd [":quit"]        ""        (const Quit)   "exit interpreter",
         Cmd [":help",":?"]   ""        (const Help)   "display this list of commands" ]
  
  helpTxt :: [InteractiveCommand] -> String
  helpTxt cs
    =  "List of commands:  Any command may be abbreviated to :c where\n" ++
       "c is the first character in the full name.\n\n" ++
       "<expr>                  evaluate expression\n" ++
       "let <var> = <expr>      define variable\n" ++
       "assume <var> :: <expr>  assume variable\n\n"
       ++
       unlines (map (\ (Cmd cs a _ d) -> let  ct = concat (intersperse ", " (map (++ if null a then "" else " " ++ a) cs))
                                         in   ct ++ replicate ((24 - length ct) `max` 2) ' ' ++ d) cs)
  
  
  interpretCommand :: String -> IO Command
  interpretCommand x
    =  if isPrefixOf ":" x then
         do  let  (cmd,t')  =  break isSpace x
                  t         =  dropWhile isSpace t'
             --  find matching commands
             let  matching  =  filter (\ (Cmd cs _ _ _) -> any (isPrefixOf cmd) cs) commands
             case matching of
               []  ->  do  putStrLn ("Unknown command `" ++ cmd ++ "'. Type :? for help.")
                           return Noop
               [Cmd _ _ f _]
                   ->  do  return (f t)
               x   ->  do  putStrLn ("Ambiguous command, could be " ++ concat (intersperse ", " [ head cs | Cmd cs _ _ _ <- matching ]) ++ ".")
                           return Noop
       else
         return (Compile (CompileInteractive x))
  
  handleCommand :: Interpreter i c v t tinf inf -> State v inf -> Command -> IO (Maybe (State v inf))
  handleCommand int state@(inter, out, ve, te) cmd
    =  case cmd of
         Quit   ->  when (not inter) (putStrLn "!@#$^&*") >> return Nothing
         Noop   ->  return (Just state)
         Help   ->  putStr (helpTxt commands) >> return (Just state)
         TypeOf x ->
                    do  x <- parseIO "<interactive>" (iiparse int) x
                        t <- maybe (return Nothing) (iinfer int ve te) x
                        maybe (return ()) (\u -> putStrLn (render (itprint int u))) t
                        return (Just state)
         Browse ->  do  putStr (unlines [ s | Global s <- reverse (nub (map fst te)) ])
                        return (Just state)
         Compile c ->
                    do  state <- case c of
                                   CompileInteractive s -> compilePhrase int state s
                                   CompileFile f        -> compileFile int state f
                        return (Just state)
 
  compileFile :: Interpreter i c v t tinf inf -> State v inf -> String -> IO (State v inf)
  compileFile int state@(inter, out, ve, te) f =
    do
      x <- readFile f
      stmts <- parseIO f (many (isparse int)) x
      maybe (return state) (foldM (handleStmt int) state) stmts
  
  compilePhrase :: Interpreter i c v t tinf inf -> State v inf -> String -> IO (State v inf)
  compilePhrase int state@(inter, out, ve, te) x =
    do
      x <- parseIO "<interactive>" (isparse int) x
      maybe (return state) (handleStmt int state) x
  
  data Interpreter i c v t tinf inf =
    I { iname :: String,
        iprompt :: String,
        iitype :: NameEnv v -> Ctx inf -> i -> Result t,
        iquote :: v -> c,
        ieval  :: NameEnv v -> i -> v,
        ihastype :: t -> inf,
        icprint :: c -> Doc,
        itprint :: t -> Doc,
        iiparse :: CharParser () i,
        isparse :: CharParser () (Stmt i tinf),
        iassume :: State v inf -> (String, tinf) -> IO (State v inf) }
 
  st :: Interpreter ITerm CTerm Value Type Info Info
  st = I { iname = "the simply typed lambda calculus",
           iprompt = "ST> ",
           iitype = \ v c -> iType 0 c,
           iquote = quote0,
           ieval  = \ e x -> iEval x (e, []),
           ihastype = HasType,
           icprint = cPrint 0 0,
           itprint = tPrint 0,
           iiparse = parseITerm 0 [],
           isparse = parseStmt [],
           iassume = \ s (x, t) -> stassume s x t }
 
  lp :: Interpreter ITerm_ CTerm_ Value_ Value_ CTerm_ Value_
  lp = I { iname = "lambda-Pi",
           iprompt = "LP> ",
           iitype = \ v c -> iType_ 0 (v, c),
           iquote = quote0_,
           ieval = \ e x -> iEval_ x (e, []),
           ihastype = id,
           icprint = cPrint_ 0 0,
           itprint = cPrint_ 0 0 . quote0_,
           iiparse = parseITerm_ 0 [],
           isparse = parseStmt_ [],
           iassume = \ s (x, t) -> lpassume s x t }
 
  lpte :: Ctx Value_
  lpte =      [(Global "Zero", VNat_),
               (Global "Succ", VPi_ VNat_ (\ _ -> VNat_)),
               (Global "Nat", VStar_),
               (Global "natElim", VPi_ (VPi_ VNat_ (\ _ -> VStar_)) (\ m ->
                                 VPi_ (m `vapp_` VZero_) (\ _ ->
                                 VPi_ (VPi_ VNat_ (\ k -> VPi_ (m `vapp_` k) (\ _ -> (m `vapp_` (VSucc_ k))))) ( \ _ ->
                                 VPi_ VNat_ (\ n -> m `vapp_` n))))),
               (Global "Nil", VPi_ VStar_ (\ a -> VVec_ a VZero_)),
               (Global "Cons", VPi_ VStar_ (\ a ->
                              VPi_ VNat_ (\ n ->
                              VPi_ a (\ _ -> VPi_ (VVec_ a n) (\ _ -> VVec_ a (VSucc_ n)))))),
               (Global "Vec", VPi_ VStar_ (\ _ -> VPi_ VNat_ (\ _ -> VStar_))),
               (Global "vecElim", VPi_ VStar_ (\ a ->
                                 VPi_ (VPi_ VNat_ (\ n -> VPi_ (VVec_ a n) (\ _ -> VStar_))) (\ m ->
                                 VPi_ (m `vapp_` VZero_ `vapp_` (VNil_ a)) (\ _ ->
                                 VPi_ (VPi_ VNat_ (\ n ->
                                       VPi_ a (\ x ->
                                       VPi_ (VVec_ a n) (\ xs ->
                                       VPi_ (m `vapp_` n `vapp_` xs) (\ _ ->
                                       m `vapp_` VSucc_ n `vapp_` VCons_ a n x xs))))) (\ _ ->
                                 VPi_ VNat_ (\ n ->
                                 VPi_ (VVec_ a n) (\ xs -> m `vapp_` n `vapp_` xs))))))),
               (Global "Refl", VPi_ VStar_ (\ a -> VPi_ a (\ x ->
                              VEq_ a x x))),
               (Global "Eq", VPi_ VStar_ (\ a -> VPi_ a (\ x -> VPi_ a (\ y -> VStar_)))),
               (Global "eqElim", VPi_ VStar_ (\ a ->
                                VPi_ (VPi_ a (\ x -> VPi_ a (\ y -> VPi_ (VEq_ a x y) (\ _ -> VStar_)))) (\ m ->
                                VPi_ (VPi_ a (\ x -> m `vapp_` x `vapp_` x `vapp_` VRefl_ a x)) (\ _ ->
                                VPi_ a (\ x -> VPi_ a (\ y ->
                                VPi_ (VEq_ a x y) (\ eq ->
                                m `vapp_` x `vapp_` y `vapp_` eq))))))),
               (Global "FZero", VPi_ VNat_ (\ n -> VFin_ (VSucc_ n))),
               (Global "FSucc", VPi_ VNat_ (\ n -> VPi_ (VFin_ n) (\ f ->
                               VFin_ (VSucc_ n)))),
               (Global "Fin", VPi_ VNat_ (\ n -> VStar_)),
               (Global "finElim", VPi_ (VPi_ VNat_ (\ n -> VPi_ (VFin_ n) (\ _ -> VStar_))) (\ m ->
                                 VPi_ (VPi_ VNat_ (\ n -> m `vapp_` (VSucc_ n) `vapp_` (VFZero_ n))) (\ _ ->
                                 VPi_ (VPi_ VNat_ (\ n -> VPi_ (VFin_ n) (\ f -> VPi_ (m `vapp_` n `vapp_` f) (\ _ -> m `vapp_` (VSucc_ n) `vapp_` (VFSucc_ n f))))) (\ _ ->
                                 VPi_ VNat_ (\ n -> VPi_ (VFin_ n) (\ f ->
                                 m `vapp_` n `vapp_` f))))))]
 
  lpve :: Ctx Value_
  lpve =      [(Global "Zero", VZero_),
               (Global "Succ", VLam_ (\ n -> VSucc_ n)),
               (Global "Nat", VNat_),
               (Global "natElim", cEval_ (Lam_ (Lam_ (Lam_ (Lam_ (Inf_ (NatElim_ (Inf_ (Bound_ 3)) (Inf_ (Bound_ 2)) (Inf_ (Bound_ 1)) (Inf_ (Bound_ 0)))))))) ([], [])),
               (Global "Nil", VLam_ (\ a -> VNil_ a)),
               (Global "Cons", VLam_ (\ a -> VLam_ (\ n -> VLam_ (\ x -> VLam_ (\ xs ->
                              VCons_ a n x xs))))),
               (Global "Vec", VLam_ (\ a -> VLam_ (\ n -> VVec_ a n))),
               (Global "vecElim", cEval_ (Lam_ (Lam_ (Lam_ (Lam_ (Lam_ (Lam_ (Inf_ (VecElim_ (Inf_ (Bound_ 5)) (Inf_ (Bound_ 4)) (Inf_ (Bound_ 3)) (Inf_ (Bound_ 2)) (Inf_ (Bound_ 1)) (Inf_ (Bound_ 0)))))))))) ([],[])),
               (Global "Refl", VLam_ (\ a -> VLam_ (\ x -> VRefl_ a x))),
               (Global "Eq", VLam_ (\ a -> VLam_ (\ x -> VLam_ (\ y -> VEq_ a x y)))),
               (Global "eqElim", cEval_ (Lam_ (Lam_ (Lam_ (Lam_ (Lam_ (Lam_ (Inf_ (EqElim_ (Inf_ (Bound_ 5)) (Inf_ (Bound_ 4)) (Inf_ (Bound_ 3)) (Inf_ (Bound_ 2)) (Inf_ (Bound_ 1)) (Inf_ (Bound_ 0)))))))))) ([],[])),
               (Global "FZero", VLam_ (\ n -> VFZero_ n)),
               (Global "FSucc", VLam_ (\ n -> VLam_ (\ f -> VFSucc_ n f))),
               (Global "Fin", VLam_ (\ n -> VFin_ n)),
               (Global "finElim", cEval_ (Lam_ (Lam_ (Lam_ (Lam_ (Lam_ (Inf_ (FinElim_ (Inf_ (Bound_ 4)) (Inf_ (Bound_ 3)) (Inf_ (Bound_ 2)) (Inf_ (Bound_ 1)) (Inf_ (Bound_ 0))))))))) ([],[]))]
{-# LINE 225 "Interpreter.lhs" #-}
  repLP :: Bool -> IO ()
  repLP b = readevalprint lp (b, [], lpve, lpte)
 
  repST :: Bool -> IO ()
  repST b = readevalprint st (b, [], [], [])
   
  iinfer int d g t =
    case iitype int d g t of
      Left e -> putStrLn e >> return Nothing
      Right v -> return (Just v)
 
  handleStmt :: Interpreter i c v t tinf inf
                -> State v inf -> Stmt i tinf -> IO (State v inf)
  handleStmt int state@(inter, out, ve, te) stmt =
    do
      case stmt of
          Assume ass -> foldM (iassume int) state ass 
          Let x e    -> checkEval x e
          Eval e     -> checkEval it e
          PutStrLn x -> putStrLn x >> return state
          Out f      -> return (inter, f, ve, te)
    where
      --  checkEval :: String -> i -> IO (State v inf)
      checkEval i t =
        check int state i t
          (\ (y, v) -> do
                         --  ugly, but we have limited space in the paper
                         --  usually, you'd want to have the bound identifier *and*
                         --  the result of evaluation
                         let outtext = if i == it then render (icprint int (iquote int v) <> text " :: " <> itprint int y)
                                                  else render (text i <> text " :: " <> itprint int y)
                         putStrLn outtext
                         unless (null out) (writeFile out (process outtext)))
          (\ (y, v) -> (inter, "", (Global i, v) : ve, (Global i, ihastype int y) : te))
 
  check :: Interpreter i c v t tinf inf -> State v inf -> String -> i
           -> ((t, v) -> IO ()) -> ((t, v) -> State v inf) -> IO (State v inf)
  check int state@(inter, out, ve, te) i t kp k =
                  do
                    --  typecheck and evaluate
                    x <- iinfer int ve te t
                    case x of
                      Nothing  ->
                        do
                          --  putStrLn "type error"
                          return state
                      Just y   ->
                        do
                          let v = ieval int ve t
                          kp (y, v)
                          return (k (y, v))
 
  stassume state@(inter, out, ve, te) x t = return (inter, out, ve, (Global x, t) : te)
  lpassume state@(inter, out, ve, te) x t =
    check lp state x (Ann_ t (Inf_ Star_))
          (\ (y, v) -> return ()) --  putStrLn (render (text x <> text " :: " <> cPrint_ 0 0 (quote0_ v))))
          (\ (y, v) -> (inter, out, ve, (Global x, v) : te))
  
  
  it = "it"
{-# LINE 288 "Interpreter.lhs" #-}
  process :: String -> String
  process = unlines . map (\ x -> "< " ++ x) . lines
{-# LINE 293 "Interpreter.lhs" #-}
  main :: IO ()
  main = repLP True
{-# LINE 670 "LP.lhs" #-}
  data ITerm
     =  Ann    CTerm Type
     |  Bound  Int
     |  Free   Name
     |  ITerm :@: CTerm
    deriving (Show, Eq)
  
  data CTerm
     =  Inf  ITerm 
     |  Lam  CTerm
    deriving (Show, Eq)
 
  data Name
     =  Global  String
     |  Local   Int
     |  Quote   Int
    deriving (Show, Eq)
{-# LINE 705 "LP.lhs" #-}
  data Type
     =  TFree  Name
     |  Fun    Type Type
    deriving (Show, Eq)
{-# LINE 712 "LP.lhs" #-}
  data Value
     =  VLam      (Value -> Value)
     |  VNeutral  Neutral
{-# LINE 725 "LP.lhs" #-}
  data Neutral
     =  NFree  Name
     |  NApp   Neutral Value
{-# LINE 732 "LP.lhs" #-}
  vfree :: Name -> Value
  vfree n = VNeutral (NFree n)
{-# LINE 786 "LP.lhs" #-}
  data Kind = Star
    deriving (Show)
 
  data Info
     =  HasKind  Kind
     |  HasType  Type 
    deriving (Show)
 
  type Context = [(Name, Info)]
{-# LINE 801 "LP.lhs" #-}
  type Env = [Value]
 
  iEval :: ITerm -> (NameEnv Value,Env) -> Value
  iEval (Ann  e _)    d  =  cEval e d
  iEval (Free  x)     d  =  case lookup x (fst d) of Nothing ->  (vfree x); Just v -> v
  iEval (Bound  ii)   d  =  (snd d) !! ii
  iEval (e1 :@: e2)   d  =  vapp (iEval e1 d) (cEval e2 d)
 
  vapp :: Value -> Value -> Value
  vapp (VLam f)      v  =  f v
  vapp (VNeutral n)  v  =  VNeutral (NApp n v)
 
  cEval :: CTerm -> (NameEnv Value,Env) -> Value
  cEval (Inf  ii)   d  =  iEval ii d
  cEval (Lam  e)    d  =  VLam (\ x -> cEval e (((\(e, d) -> (e,  (x : d))) d)))
{-# LINE 840 "LP.lhs" #-}
  cKind :: Context -> Type -> Kind -> Result ()
  cKind g (TFree x) Star
    =  case lookup x g of
         Just (HasKind Star)  ->  return ()
         Nothing              ->  throwError "unknown identifier"
  cKind g (Fun kk kk') Star
    =  do  cKind g kk   Star
           cKind g kk'  Star
 
  iType0 :: Context -> ITerm -> Result Type
  iType0 = iType 0
 
  iType :: Int -> Context -> ITerm -> Result Type
  iType ii g (Ann e ty)
    =  do  cKind g ty Star
           cType ii g e ty
           return ty
  iType ii g (Free x)
    =  case lookup x g of
         Just (HasType ty)  ->  return ty
         Nothing            ->  throwError "unknown identifier"
  iType ii g (e1 :@: e2)
    =  do  si <- iType ii g e1
           case si of
             Fun ty ty'  ->  do  cType ii g e2 ty
                                 return ty'
             _           ->  throwError "illegal application"
 
  cType :: Int -> Context -> CTerm -> Type -> Result ()
  cType ii g (Inf e) ty
    =  do  ty' <- iType ii g e
           unless (ty == ty') (throwError "type mismatch")
  cType ii g (Lam e) (Fun ty ty')
    =  cType  (ii + 1) ((Local ii, HasType ty) : g)
              (cSubst 0 (Free (Local ii)) e) ty'
  cType ii g _ _
    =  throwError "type mismatch" 
{-# LINE 888 "LP.lhs" #-}
  type Result a = Either String a
{-# LINE 931 "LP.lhs" #-}
  iSubst :: Int -> ITerm -> ITerm -> ITerm
  iSubst ii r (Ann e ty)   =  Ann (cSubst ii r e) ty
  iSubst ii r (Bound j)    =  if ii == j then r else Bound j
  iSubst ii r (Free y)     =  Free y
  iSubst ii r (e1 :@: e2)  =  iSubst ii r e1 :@: cSubst ii r e2
  
  cSubst :: Int -> ITerm -> CTerm -> CTerm
  cSubst ii r (Inf e)      =  Inf (iSubst ii r e)
  cSubst ii r (Lam e)      =  Lam (cSubst (ii + 1) r e)
{-# LINE 964 "LP.lhs" #-}
  quote0 :: Value -> CTerm
  quote0 = quote 0
 
  quote :: Int -> Value -> CTerm
  quote ii (VLam f)      =  Lam (quote (ii + 1) (f (vfree (Quote ii))))
  quote ii (VNeutral n)  =  Inf (neutralQuote ii n)
 
  neutralQuote :: Int -> Neutral -> ITerm
  neutralQuote ii (NFree x)   =  boundfree ii x
  neutralQuote ii (NApp n v)  =  neutralQuote ii n :@: quote ii v
{-# LINE 996 "LP.lhs" #-}
  boundfree :: Int -> Name -> ITerm
  boundfree ii (Quote k)     =  Bound (ii - k - 1)
  boundfree ii x             =  Free x
{-# LINE 1036 "LP.lhs" #-}
  id'      =  Lam (Inf (Bound 0))
  const'   =  Lam (Lam (Inf (Bound 1)))
 
  tfree a  =  TFree (Global a)
  free x   =  Inf (Free (Global x))
 
  term1    =  Ann id' (Fun (tfree "a") (tfree "a")) :@: free "y" 
  term2    =  Ann const' (Fun  (Fun (tfree "b") (tfree "b"))
                               (Fun  (tfree "a")
                                     (Fun (tfree "b") (tfree "b"))))
              :@: id' :@: free "y" 
 
  env1     =  [  (Global "y", HasType (tfree "a")),
                 (Global "a", HasKind Star)]
  env2     =  [(Global "b", HasKind Star)] ++ env1
{-# LINE 1058 "LP.lhs" #-}
  test_eval1=  quote0 (iEval term1 ([],[]))
   {-  \eval{test_eval1}  -}
 
  test_eval2=  quote0 (iEval term2 ([],[]))
   {-  \eval{test_eval2}  -}
 
  test_type1=  iType0 env1 term1
   {-  \eval{test_type1}  -}
 
  test_type2=  iType0 env2 term2
   {-  \eval{test_type2}  -}
{-# LINE 1514 "LP.lhs" #-}
  data CTerm_
     =  Inf_  ITerm_
     |  Lam_  CTerm_
{-# LINE 2 "CTerm_Nat.lhs" #-}
     |  Zero_
     |  Succ_ CTerm_
{-# LINE 2 "CTerm_Vec.lhs" #-}
    |  Nil_ CTerm_
    |  Cons_ CTerm_ CTerm_ CTerm_ CTerm_
{-# LINE 2 "CTerm_Eq.lhs" #-}
     |  Refl_ CTerm_ CTerm_
{-# LINE 2 "CTerm_Fin.lhs" #-}
    |  FZero_ CTerm_
    |  FSucc_ CTerm_ CTerm_
{-# LINE 1523 "LP.lhs" #-}
    deriving (Show, Eq)
{-# LINE 1548 "LP.lhs" #-}
  data ITerm_
     =  Ann_ CTerm_ CTerm_
     |  Star_
     |  Pi_ CTerm_ CTerm_
     |  Bound_  Int
     |  Free_  Name
     |  ITerm_ :$: CTerm_
{-# LINE 2 "ITerm_Nat.lhs" #-}
     |  Nat_
     |  NatElim_ CTerm_ CTerm_ CTerm_ CTerm_
{-# LINE 2 "ITerm_Vec.lhs" #-}
    |  Vec_ CTerm_ CTerm_
    |  VecElim_ CTerm_ CTerm_ CTerm_ CTerm_ CTerm_ CTerm_
{-# LINE 2 "ITerm_Eq.lhs" #-}
     |  Eq_ CTerm_ CTerm_ CTerm_
     |  EqElim_ CTerm_ CTerm_ CTerm_ CTerm_ CTerm_ CTerm_
{-# LINE 2 "ITerm_Fin.lhs" #-}
     |  Fin_ CTerm_
     |  FinElim_ CTerm_ CTerm_ CTerm_ CTerm_ CTerm_
{-# LINE 1564 "LP.lhs" #-}
    deriving (Show, Eq)
{-# LINE 1569 "LP.lhs" #-}
  data Value_
     =  VLam_  (Value_ -> Value_)
     |  VStar_
     |  VPi_ Value_ (Value_ -> Value_)
     |  VNeutral_ Neutral_
{-# LINE 2 "Value_Nat.lhs" #-}
    |  VNat_
    |  VZero_
    |  VSucc_ Value_
{-# LINE 2 "Value_Vec.lhs" #-}
    |  VNil_ Value_
    |  VCons_ Value_ Value_ Value_ Value_
    |  VVec_ Value_ Value_
{-# LINE 2 "Value_Eq.lhs" #-}
    |  VEq_ Value_ Value_ Value_
    |  VRefl_ Value_ Value_
{-# LINE 2 "Value_Fin.lhs" #-}
    |  VFZero_ Value_
    |  VFSucc_ Value_ Value_
    |  VFin_ Value_
{-# LINE 1582 "LP.lhs" #-}
  data Neutral_
     =  NFree_  Name
     |  NApp_  Neutral_ Value_
{-# LINE 2 "Neutral_Nat.lhs" #-}
    |  NNatElim_ Value_ Value_ Value_ Neutral_
{-# LINE 2 "Neutral_Vec.lhs" #-}
    |  NVecElim_ Value_ Value_ Value_ Value_ Value_ Neutral_
{-# LINE 2 "Neutral_Eq.lhs" #-}
    |  NEqElim_ Value_ Value_ Value_ Value_ Value_ Neutral_
{-# LINE 2 "Neutral_Fin.lhs" #-}
    |  NFinElim_ Value_ Value_ Value_ Value_ Neutral_
{-# LINE 1620 "LP.lhs" #-}
  type Env_ = [Value_]
 
  vapp_ :: Value_ -> Value_ -> Value_
  vapp_ (VLam_ f)      v  =  f v
  vapp_ (VNeutral_ n)  v  =  VNeutral_ (NApp_ n v)
 
  vfree_ :: Name -> Value_
  vfree_ n = VNeutral_ (NFree_ n)
 
  cEval_ :: CTerm_ -> (NameEnv Value_,Env_) -> Value_
  cEval_ (Inf_  ii)    d  =  iEval_ ii d
  cEval_ (Lam_  c)     d  =  VLam_ (\ x -> cEval_ c (((\(e, d) -> (e,  (x : d))) d)))
{-# LINE 2 "cEval_Nat.lhs" #-}
  cEval_ Zero_      d  = VZero_
  cEval_ (Succ_ k)  d  = VSucc_ (cEval_ k d)
{-# LINE 2 "cEval_Vec.lhs" #-}
  cEval_ (Nil_ a)          d  =  VNil_ (cEval_ a d)
  cEval_ (Cons_ a n x xs)  d  =  VCons_  (cEval_ a d) (cEval_ n d)
                                         (cEval_ x d) (cEval_ xs d)
{-# LINE 2 "cEval_Eq.lhs" #-}
  cEval_ (Refl_ a x)       d  =  VRefl_ (cEval_ a d) (cEval_ x d)
{-# LINE 2 "cEval_Fin.lhs" #-}
  cEval_ (FZero_ n)    d  =  VFZero_ (cEval_ n d)
  cEval_ (FSucc_ n f)  d  =  VFSucc_ (cEval_ n d) (cEval_ f d)
{-# LINE 1654 "LP.lhs" #-}
  iEval_ :: ITerm_ -> (NameEnv Value_,Env_) -> Value_
  iEval_ (Ann_  c _)       d  =  cEval_ c d
{-# LINE 1659 "LP.lhs" #-}
  iEval_ Star_           d  =  VStar_   
  iEval_ (Pi_ ty ty')    d  =  VPi_ (cEval_ ty d) (\ x -> cEval_ ty' (((\(e, d) -> (e,  (x : d))) d)))   
{-# LINE 1664 "LP.lhs" #-}
  iEval_ (Free_  x)      d  =  case lookup x (fst d) of Nothing ->  (vfree_ x); Just v -> v 
  iEval_ (Bound_  ii)    d  =  (snd d) !! ii
  iEval_ (i :$: c)       d  =  vapp_ (iEval_ i d) (cEval_ c d)
{-# LINE 2 "iEval_Nat.lhs" #-}
  iEval_ Nat_                  d  =  VNat_
  iEval_ (NatElim_ m mz ms n)  d 
    =  let  mzVal = cEval_ mz d
            msVal = cEval_ ms d
            rec nVal =
              case nVal of
                VZero_       ->  mzVal
                VSucc_ k     ->  msVal `vapp_` k `vapp_` rec k
                VNeutral_ n  ->  VNeutral_
                                 (NNatElim_ (cEval_ m d) mzVal msVal n)
                _            ->  error "internal: eval natElim"
       in   rec (cEval_ n d)
{-# LINE 3 "iEval_Vec.lhs" #-}
  iEval_ (Vec_ a n)                 d  =  VVec_ (cEval_ a d) (cEval_ n d)
{-# LINE 7 "iEval_Vec.lhs" #-}
  iEval_ (VecElim_ a m mn mc n xs)  d  =
    let  mnVal  =  cEval_ mn d
         mcVal  =  cEval_ mc d
         rec nVal xsVal =
           case xsVal of
             VNil_ _          ->  mnVal
             VCons_ _ k x xs  ->  foldl vapp_ mcVal [k, x, xs, rec k xs]
             VNeutral_ n      ->  VNeutral_
                                  (NVecElim_  (cEval_ a d) (cEval_ m d)
                                              mnVal mcVal nVal n)
             _                ->  error "internal: eval vecElim"
    in   rec (cEval_ n d) (cEval_ xs d)
{-# LINE 2 "iEval_Eq.lhs" #-}
  iEval_ (Eq_ a x y)                d  =  VEq_ (cEval_ a d) (cEval_ x d) (cEval_ y d)
  iEval_ (EqElim_ a m mr x y eq)    d  =
    let  mrVal  =  cEval_ mr d
         rec eqVal =
           case eqVal of
             VRefl_ _ z -> mrVal `vapp_` z
             VNeutral_ n ->  
               VNeutral_ (NEqElim_  (cEval_ a d) (cEval_ m d) mrVal
                                    (cEval_ x d) (cEval_ y d) n)
             _ -> error "internal: eval eqElim"
    in   rec (cEval_ eq d)
{-# LINE 2 "iEval_Fin.lhs" #-}
  iEval_ (Fin_ n)                d  =  VFin_ (cEval_ n d)
  iEval_ (FinElim_ m mz ms n f)  d  =
    let  mzVal  =  cEval_ mz d
         msVal  =  cEval_ ms d
         rec fVal =
           case fVal of
             VFZero_ k        ->  mzVal `vapp_` k
             VFSucc_ k g      ->  foldl vapp_ msVal [k, g, rec g]
             VNeutral_ n'     ->  VNeutral_
                                  (NFinElim_  (cEval_ m d) (cEval_ mz d)
                                              (cEval_ ms d) (cEval_ n d) n')
             _                ->  error "internal: eval finElim"
    in   rec (cEval_ f d)
{-# LINE 1679 "LP.lhs" #-}
  iSubst_ :: Int -> ITerm_ -> ITerm_ -> ITerm_
  iSubst_ ii i'   (Ann_ c c')     =  Ann_ (cSubst_ ii i' c) (cSubst_ ii i' c')
{-# LINE 1684 "LP.lhs" #-}
  
  iSubst_ ii r  Star_           =  Star_  
  iSubst_ ii r  (Pi_ ty ty')    =  Pi_  (cSubst_ ii r ty) (cSubst_ (ii + 1) r ty')
{-# LINE 1690 "LP.lhs" #-}
  iSubst_ ii i' (Bound_ j)      =  if ii == j then i' else Bound_ j
  iSubst_ ii i' (Free_ y)       =  Free_ y
  iSubst_ ii i' (i :$: c)       =  iSubst_ ii i' i :$: cSubst_ ii i' c
{-# LINE 2 "iSubst_Nat.lhs" #-}
  iSubst_ ii r  Nat_            =  Nat_
  iSubst_ ii r  (NatElim_ m mz ms n)
                                =  NatElim_ (cSubst_ ii r m)
                                            (cSubst_ ii r mz) (cSubst_ ii r ms)
                                            (cSubst_ ii r ms)
{-# LINE 2 "iSubst_Vec.lhs" #-}
  iSubst_ ii r  (Vec_ a n)      =  Vec_ (cSubst_ ii r a) (cSubst_ ii r n)
  iSubst_ ii r  (VecElim_ a m mn mc n xs)
                                =  VecElim_ (cSubst_ ii r a) (cSubst_ ii r m)
                                            (cSubst_ ii r mn) (cSubst_ ii r mc)
                                            (cSubst_ ii r n) (cSubst_ ii r xs)
{-# LINE 2 "iSubst_Eq.lhs" #-}
  iSubst_ ii r  (Eq_ a x y)     =  Eq_ (cSubst_ ii r a)
                                       (cSubst_ ii r x) (cSubst_ ii r y)
  iSubst_ ii r  (EqElim_ a m mr x y eq)
                                =  VecElim_ (cSubst_ ii r a) (cSubst_ ii r m)
                                            (cSubst_ ii r mr) (cSubst_ ii r x)
                                            (cSubst_ ii r y) (cSubst_ ii r eq)
{-# LINE 2 "iSubst_Fin.lhs" #-}
  iSubst_ ii r  (Fin_ n)        =  Fin_ (cSubst_ ii r n)
  iSubst_ ii r  (FinElim_ m mz ms n f)
                                =  FinElim_ (cSubst_ ii r m)
                                            (cSubst_ ii r mz) (cSubst_ ii r ms)
                                            (cSubst_ ii r n) (cSubst_ ii r f)
{-# LINE 1701 "LP.lhs" #-}
  cSubst_ :: Int -> ITerm_ -> CTerm_ -> CTerm_
  cSubst_ ii i' (Inf_ i)      =  Inf_ (iSubst_ ii i' i)
  cSubst_ ii i' (Lam_ c)      =  Lam_ (cSubst_ (ii + 1) i' c)
{-# LINE 2 "cSubst_Nat.lhs" #-}
  cSubst_ ii r  Zero_         =  Zero_
  cSubst_ ii r  (Succ_ n)     =  Succ_ (cSubst_ ii r n)
{-# LINE 2 "cSubst_Vec.lhs" #-}
  cSubst_ ii r  (Nil_ a)      =  Nil_ (cSubst_ ii r a)
  cSubst_ ii r  (Cons_ a n x xs)
                              =  Cons_ (cSubst_ ii r a) (cSubst_ ii r x)
                                       (cSubst_ ii r x) (cSubst_ ii r xs)
{-# LINE 2 "cSubst_Eq.lhs" #-}
  cSubst_ ii r  (Refl_ a x)   =  Refl_ (cSubst_ ii r a) (cSubst_ ii r x)
{-# LINE 2 "cSubst_Fin.lhs" #-}
  cSubst_ ii r  (FZero_ n)    =  FZero_ (cSubst_ ii r n)
  cSubst_ ii r  (FSucc_ n k)  =  FSucc_ (cSubst_ ii r n) (cSubst_ ii r k)
{-# LINE 1712 "LP.lhs" #-}
  quote_ :: Int -> Value_ -> CTerm_
  quote_ ii (VLam_ t)
    =     Lam_ (quote_ (ii + 1) (t (vfree_ (Quote ii))))
{-# LINE 1718 "LP.lhs" #-}
  
  quote_ ii VStar_ = Inf_ Star_ 
  quote_ ii (VPi_ v f)                                       
      =  Inf_ (Pi_ (quote_ ii v) (quote_ (ii + 1) (f (vfree_ (Quote ii)))))  
{-# LINE 1725 "LP.lhs" #-}
  quote_ ii (VNeutral_ n)
    =     Inf_ (neutralQuote_ ii n)
{-# LINE 2 "quote_Nat.lhs" #-}
  quote_ ii VNat_       =  Inf_ Nat_
  quote_ ii VZero_      =  Zero_
  quote_ ii (VSucc_ n)  =  Succ_ (quote_ ii n)
{-# LINE 2 "quote_Vec.lhs" #-}
  quote_ ii (VVec_ a n)         =  Inf_ (Vec_ (quote_ ii a) (quote_ ii n))
  quote_ ii (VNil_ a)           =  Nil_ (quote_ ii a)
  quote_ ii (VCons_ a n x xs)   =  Cons_  (quote_ ii a) (quote_ ii n)
                                          (quote_ ii x) (quote_ ii xs)
{-# LINE 2 "quote_Eq.lhs" #-}
  quote_ ii (VEq_ a x y)  =  Inf_ (Eq_ (quote_ ii a) (quote_ ii x) (quote_ ii y))
  quote_ ii (VRefl_ a x)  =  Refl_ (quote_ ii a) (quote_ ii x)
{-# LINE 2 "quote_Fin.lhs" #-}
  quote_ ii (VFin_ n)           =  Inf_ (Fin_ (quote_ ii n))
  quote_ ii (VFZero_ n)         =  FZero_ (quote_ ii n)
  quote_ ii (VFSucc_ n f)       =  FSucc_  (quote_ ii n) (quote_ ii f)
{-# LINE 1735 "LP.lhs" #-}
  neutralQuote_ :: Int -> Neutral_ -> ITerm_
  neutralQuote_ ii (NFree_ v)
     =  boundfree_ ii v
  neutralQuote_ ii (NApp_ n v)
     =  neutralQuote_ ii n :$: quote_ ii v
{-# LINE 2 "neutralQuote_Nat.lhs" #-}
  neutralQuote_ ii (NNatElim_ m z s n)
     =  NatElim_ (quote_ ii m) (quote_ ii z) (quote_ ii s) (Inf_ (neutralQuote_ ii n))
{-# LINE 2 "neutralQuote_Vec.lhs" #-}
  neutralQuote_ ii (NVecElim_ a m mn mc n xs)
     =  VecElim_ (quote_ ii a) (quote_ ii m)
                 (quote_ ii mn) (quote_ ii mc)
                 (quote_ ii n) (Inf_ (neutralQuote_ ii xs))
{-# LINE 2 "neutralQuote_Eq.lhs" #-}
  neutralQuote_ ii (NEqElim_ a m mr x y eq)
     =  EqElim_  (quote_ ii a) (quote_ ii m) (quote_ ii mr)
                 (quote_ ii x) (quote_ ii y)
                 (Inf_ (neutralQuote_ ii eq))
{-# LINE 2 "neutralQuote_Fin.lhs" #-}
  neutralQuote_ ii (NFinElim_ m mz ms n f)
     =  FinElim_ (quote_ ii m)
                 (quote_ ii mz) (quote_ ii ms)
                 (quote_ ii n) (Inf_ (neutralQuote_ ii f))
{-# LINE 1746 "LP.lhs" #-}
  boundfree_ :: Int -> Name -> ITerm_
  boundfree_ ii (Quote k)     =  Bound_ ((ii - k - 1) `max` 0)
  boundfree_ ii x             =  Free_ x
{-# LINE 1751 "LP.lhs" #-}
  instance Show Value_ where
    show = show . quote0_
{-# LINE 1775 "LP.lhs" #-}
  type Type_     =  Value_  
  type Context_    =  [(Name, Type_)]
{-# LINE 1818 "LP.lhs" #-}
  quote0_ :: Value_ -> CTerm_
  quote0_ = quote_ 0 
 
  iType0_ :: (NameEnv Value_,Context_) -> ITerm_ -> Result Type_
  iType0_ = iType_ 0
{-# LINE 1826 "LP.lhs" #-}
  iType_ :: Int -> (NameEnv Value_,Context_) -> ITerm_ -> Result Type_
  iType_ ii g (Ann_ e tyt )
    =     do  cType_  ii g tyt VStar_
              let ty = cEval_ tyt (fst g, [])  
              cType_ ii g e ty
              return ty
  iType_ ii g Star_   
     =  return VStar_   
  iType_ ii g (Pi_ tyt tyt')  
     =  do  cType_ ii g tyt VStar_    
            let ty = cEval_ tyt (fst g, [])  
            cType_  (ii + 1) ((\ (d,g) -> (d,  ((Local ii, ty) : g))) g)  
                      (cSubst_ 0 (Free_ (Local ii)) tyt') VStar_  
            return VStar_   
  iType_ ii g (Free_ x)
    =     case lookup x (snd g) of
            Just ty        ->  return ty
            Nothing        ->  throwError ("unknown identifier: " ++ render (iPrint_ 0 0 (Free_ x)))
  iType_ ii g (e1 :$: e2)
    =     do  si <- iType_ ii g e1
              case si of
                VPi_  ty ty'  ->  do  cType_ ii g e2 ty
                                      return ( ty' (cEval_ e2 (fst g, [])))
                _                  ->  throwError "illegal application"
{-# LINE 2 "iType_Nat.lhs" #-}
  iType_ ii g Nat_                  =  return VStar_
  iType_ ii g (NatElim_ m mz ms n)  =
    do  cType_ ii g m (VPi_ VNat_ (const VStar_))
        let mVal  = cEval_ m (fst g, []) 
        cType_ ii g mz (mVal `vapp_` VZero_)
        cType_ ii g ms (VPi_ VNat_ (\ k -> VPi_ (mVal `vapp_` k) (\ _ -> mVal `vapp_` VSucc_ k)))
        cType_ ii g n VNat_
        let nVal = cEval_ n (fst g, [])
        return (mVal `vapp_` nVal)
{-# LINE 2 "iType_Vec.lhs" #-}
  iType_ ii g (Vec_ a n) =
    do  cType_ ii g a  VStar_
        cType_ ii g n  VNat_
        return VStar_
  iType_ ii g (VecElim_ a m mn mc n vs) =
    do  cType_ ii g a VStar_
        let aVal = cEval_ a (fst g, [])
        cType_ ii g m
          (  VPi_ VNat_ (\n -> VPi_ (VVec_ aVal n) (\ _ -> VStar_)))
        let mVal = cEval_ m (fst g, [])
        cType_ ii g mn (foldl vapp_ mVal [VZero_, VNil_ aVal])
        cType_ ii g mc
          (  VPi_ VNat_ (\ n -> 
             VPi_ aVal (\ y -> 
             VPi_ (VVec_ aVal n) (\ ys ->
             VPi_ (foldl vapp_ mVal [n, ys]) (\ _ ->
             (foldl vapp_ mVal [VSucc_ n, VCons_ aVal n y ys]))))))
        cType_ ii g n VNat_
        let nVal = cEval_ n (fst g, [])
        cType_ ii g vs (VVec_ aVal nVal)
        let vsVal = cEval_ vs (fst g, [])
        return (foldl vapp_ mVal [nVal, vsVal])
{-# LINE 2 "iType_Eq.lhs" #-}
  iType_ i g (Eq_ a x y) =
    do  cType_ i g a VStar_
        let aVal = cEval_ a (fst g, [])
        cType_ i g x aVal
        cType_ i g y aVal
        return VStar_
  iType_ i g (EqElim_ a m mr x y eq) =
    do  cType_ i g a VStar_
        let aVal = cEval_ a (fst g, [])
        cType_ i g m
          (VPi_ aVal (\ x ->
           VPi_ aVal (\ y ->
           VPi_ (VEq_ aVal x y) (\ _ -> VStar_)))) 
        let mVal = cEval_ m (fst g, [])
        cType_ i g mr
          (VPi_ aVal (\ x ->
           foldl vapp_ mVal [x, x]))
        cType_ i g x aVal
        let xVal = cEval_ x (fst g, [])
        cType_ i g y aVal
        let yVal = cEval_ y (fst g, [])
        cType_ i g eq (VEq_ aVal xVal yVal)
        let eqVal = cEval_ eq (fst g, [])
        return (foldl vapp_ mVal [xVal, yVal])
{-# LINE 1857 "LP.lhs" #-}
  
{-# LINE 1860 "LP.lhs" #-}
  cType_ :: Int -> (NameEnv Value_,Context_) -> CTerm_ -> Type_ -> Result ()
  cType_ ii g (Inf_ e) v 
    =     do  v' <- iType_ ii g e
              unless ( quote0_ v == quote0_ v') (throwError ("type mismatch:\n" ++ "type inferred:  " ++ render (cPrint_ 0 0 (quote0_ v')) ++ "\n" ++ "type expected:  " ++ render (cPrint_ 0 0 (quote0_ v)) ++ "\n" ++ "for expression: " ++ render (iPrint_ 0 0 e)))
  cType_ ii g (Lam_ e) ( VPi_ ty ty')
    =     cType_  (ii + 1) ((\ (d,g) -> (d,  ((Local ii, ty ) : g))) g)
                  (cSubst_ 0 (Free_ (Local ii)) e) ( ty' (vfree_ (Local ii))) 
{-# LINE 2 "cType_Nat.lhs" #-}
  cType_ ii g Zero_      VNat_  =  return ()
  cType_ ii g (Succ_ k)  VNat_  =  cType_ ii g k VNat_
{-# LINE 2 "cType_Vec.lhs" #-}
  cType_ ii g (Nil_ a) (VVec_ bVal VZero_) =
    do  cType_ ii g a VStar_
        let aVal = cEval_ a (fst g, []) 
        unless  (quote0_ aVal == quote0_ bVal) 
                (throwError "type mismatch")
  cType_ ii g (Cons_ a n x xs) (VVec_ bVal (VSucc_ k)) =
    do  cType_ ii g a VStar_
        let aVal = cEval_ a (fst g, [])
        unless  (quote0_ aVal == quote0_ bVal)
                (throwError "type mismatch")
        cType_ ii g n VNat_
        let nVal = cEval_ n (fst g, [])
        unless  (quote0_ nVal == quote0_ k)
                (throwError "number mismatch")
        cType_ ii g x aVal
        cType_ ii g xs (VVec_ bVal k)
{-# LINE 2 "cType_Eq.lhs" #-}
  cType_ ii g (Refl_ a z) (VEq_ bVal xVal yVal) =
    do  cType_ ii g a VStar_
        let aVal = cEval_ a (fst g, [])
        unless  (quote0_ aVal == quote0_ bVal)
                (throwError "type mismatch")
        cType_ ii g z aVal
        let zVal = cEval_ z (fst g, [])
        unless  (quote0_ zVal == quote0_ xVal && quote0_ zVal == quote0_ yVal)
                (throwError "type mismatch")
{-# LINE 1873 "LP.lhs" #-}
  cType_ ii g _ _
    =     throwError "type mismatch"
{-# LINE 1992 "LP.lhs" #-}
  data Nat = Zero | Succ Nat
{-# LINE 2004 "LP.lhs" #-}
  plus :: Nat -> Nat -> Nat 
  plus Zero n      = n 
  plus (Succ k) n  = Succ (plus k n)