Add monad, quote/eval broken

src/Lib/Check.idr

@@ -16,7 +16,15 @@ parameters {0 m : Type -> Type} {auto _ : MonadError String m}
   export
   check : Context -> Raw -> Val -> m Tm
 
-  check ctx (RLam _ _ _) ty = ?ch_rhs
+  check ctx (RLam nm icit tm) ty = case ty of                    
+                    (VPi pinm icit a b) => do
+                      -- TODO icit
+                      let var = VVar (length ctx.env)
+                      let ctx' = extend ctx nm a
+                      tm' <- check ctx' tm (b var)
+                      pure $ Lam nm icit tm'
+                      
+                    other => throwError "Expected pi type \{show $ quote 0 ty}"
   check ctx tm ty = do
     (tm', ty') <- infer ctx tm
     if quote 0 ty /= quote 0 ty' then

src/Lib/TT.idr

@@ -32,6 +32,19 @@ data Tm : Type where
 
 %name Tm t, u, v
 
+public export
+Show Tm where
+  show (Bnd k) = "Bnd \{show k}"
+  show (Ref str) = "Ref \{show str}"
+  show (Lam nm Implicit t) = "(λ {\{nm}} => \{show  t})"
+  show (Lam nm Explicit t) = "(λ \{nm}  => \{show  t})"
+  show (App t u) = "(\{show t} \{show u})"
+  show U = "U"
+  show (Pi str icit t u) = "(∏ \{str} : \{show t} => \{show u})"
+  show (Let str icit t u v) = "let \{str} : \{show t} = \{show u} in \{show v}"
+
+-- I can't really show val because it's HOAS...
+
 -- TODO derive
 export 
 Eq Icit where

src/Main.idr

@@ -26,26 +26,30 @@ Running check is awkward. I need a monad stack.
 Main2.idr has an older App attempt without the code below. Retrofit.
 -}
 
-M = MonadError (String) (StateT Context IO)
+M : Type -> Type
+M = (StateT Context (EitherT String IO))
 
-processDecl : Context -> Decl -> IO Context
+processDecl : Context -> Decl -> M Context
 processDecl ctx (TypeSig nm tm)= do
   putStrLn "TypeSig \{nm} \{show tm}"
-  Right ty <- pure $ the (Either String Tm) (check ctx tm VU)
+  ty <- check ctx tm VU
-    | Left err => printLn err >> pure ctx
+  putStrLn "got \{show ty}"
   let vty = eval ctx.env ty
+  putStrLn "-- \{show $ quote 0 vty}   XXXXXXXXXX"
   pure $ extend ctx nm vty
+
 processDecl ctx (Def nm raw) = do
   putStrLn "def \{show nm}"
   let Just ty = lookup nm ctx.types
     | Nothing => printLn "skip def \{nm} without Decl" >> pure ctx
-  putStrLn "check \{nm} \{show raw} at [no printer for Tm/Val]"
+  putStrLn "check \{nm} = \{show raw} at \{show $ quote 0 ty}"
-  Right ty <- pure $ the (Either String Tm) (check ctx raw ty)
+  Right tm <- pure $ the (Either String Tm) (check ctx raw ty)
     | Left err => printLn err >> pure ctx
+  putStrLn "got \{show tm}"
   pure ctx
 processDecl ctx decl = putStrLn "skip \{show decl}" >> pure ctx
 
-processFile : String -> IO ()
+processFile : String -> M ()
 processFile fn = do
   putStrLn "*** Process \{fn}"
   Right src <- readFile $ "eg/" ++ fn
@@ -58,13 +62,19 @@ processFile fn = do
   ctx <- foldlM processDecl empty res.decls
   putStrLn "done \{show ctx}"
 
-
+main' : M ()
-main : IO ()
+main' = do
-main = do
   args <- getArgs
   putStrLn "Args: \{show args}"
+
   Right files <- listDir "eg"
     | Left err => printLn err
   -- TODO use args
+  
   traverse_ processFile (filter (".newt" `isSuffixOf`) files)
 
+main : IO ()
+main = do
+  foo <- runEitherT $ runStateT TT.empty $ main'
+  putStrLn "done"
+