I think I have case expressions compiling

README.md

@@ -1,5 +1,6 @@
-- [ ] case tree building favors the right size, reverse the list
-- [ ] see note in Zoo1.newt - fix the FC in that situation
+- [ ] when it fails/crashes, we don't see it in the editor.
+- [ ] case tree building favors the right side, reverse the list
+- [ ] see notes in Zoo1.newt - fix the FC in those situations
 - [x] Support primitives
 - [ ] Make DCon/TCon separate from Ref? (Or add flavor to VRef/Ref? If processing is often the same. I think I want arity though. I don't think a checked DCon can be overapplied, but it could be underapplied without special form. And special form is possibly difficult if not collecting a stack on the way down...
 

newt/Zoo1.newt

@@ -22,6 +22,10 @@ data Maybe : U -> U where
   Just : {a : U} -> a -> Maybe a
   Nothing : {a : U} -> Maybe a
 
+
+----------------------------------
+
+-- forward declaration
 Val : U
 
 data Tm : U where
@@ -61,11 +65,38 @@ cApp (MkClosure env t) u = eval (Define env u) t
 
 hole : Val
 
-eval env (Var x) =
-  case lookup env x of
+-- TODO need to inline solved metas somewhere, as error messages are unreadable
+-- NEXT fix FC for missing case if we remove _
+
+eval env tm = case tm of
+  (Var x) =>
+    case lookup env x of
     -- case doesn't use the new code.  We've got a wildcard here that
     -- is forced to {Val}, but we don't have forcing/dotting
     -- I guess we see what Jesper says about dotting
     Just x => x
     Nothing => VVar x
-eval env _ = hole
+  -- TODO no tupls yet
+  App t u => case eval env t of
+    VLam t => cApp t (eval env u)
+    t      => VApp t (eval env u)
+  Lam t => VLam (MkClosure env t)
+  Let t u => eval (Define env (eval env t)) u
+  -- NEXT this is unreachable, find out how to warn about it
+  -- _ => hole
+
+lvl2ix : Nat -> Nat -> Nat
+lvl2ix (S k) (S j) = lvl2ix k j
+lvl2ix Z (S j) = j
+lvl2ix _ Z = Z -- shouldn't happen
+
+quote : Nat -> Val -> Tm
+quote l v = case v of
+  VVar x => Var (lvl2ix l x)
+  VApp t u => App (quote l t) (quote l u)
+  VLam t => Lam (quote (S l) (cApp t (VVar l)))
+
+nf : Env -> Tm -> Tm
+nf env t = quote (length env) (eval env t)
+
+-- and then a parser / example

src/Lib/Check.idr

@@ -93,6 +93,7 @@ parameters (ctx: Context)
           -- we don't allow solutions with Case in them
           -- pure (Case fc !(go ren lvl sc) alts)
       go ren lvl (VLit fc lit) = pure (Lit fc lit)
+      go ren lvl (VLet fc {}) = error fc "rename Let not implemented"
 
   lams : Nat -> Tm -> Tm
   lams 0 tm = tm
@@ -498,8 +499,11 @@ check ctx tm ty = case (tm, !(forceType ty)) of
     let ctx' = extend ctx scnm scty
     cons <- getConstructors ctx' scty
     alts <- traverse (buildCase ctx' (MkProb clauses ty) scnm scty) cons
+    -- BROKEN, need scnm in scope for real. ctx' promises it, but we don't have a binder here
+
+
+    pure $ Let fc scnm sc $ Case fc (Bnd fc 0) alts
 
-    pure $ Case fc sc alts
 
     -- buildTree ctx (MkProb{})
     -- ?hole

src/Lib/Compile.idr

@@ -3,6 +3,8 @@
 -- then the stuff happens. We'd need to know more about the callback for that.
 -- TODO And then get primitives and a way to declare extern functions.  That may get us
 -- to utility
+
+-- Audit how much "outside" stuff could pile up in the continuation.
 module Lib.Compile
 
 import Lib.Types
@@ -36,7 +38,8 @@ data JSStmt : Kind -> Type where
   JPlain : JSExp -> JSStmt Plain
   JConst : (nm : String) -> JSExp -> JSStmt Plain
   JReturn : JSExp -> JSStmt Return
-  -- JAssign : (nm : String) -> JSExp -> JSStmt (Assign nm)
+  JLet : (nm : String) -> JSStmt (Assign nm) -> JSStmt Plain  -- need somebody to assign
+  JAssign : (nm : String) -> JSExp -> JSStmt (Assign nm)
   -- TODO - switch to Nat tags
   -- FIXME add e to JAlt (or just drop it?)
   JCase : JSExp -> List JAlt -> JSStmt a
@@ -93,6 +96,11 @@ termToJS env (CRef nm) f = f $ Var nm
 termToJS env (CMeta k) f = f $ LitString "META \{show k}"
 termToJS env (CLit (LString str)) f = f (LitString str)
 termToJS env (CLit (LInt i)) f = f (LitInt i)
+termToJS env (CLet nm t u) f =
+  let nm' = fresh nm env
+      env' = (Var nm' :: env)
+  in JSnoc (JLet nm' $ termToJS env t (JAssign nm')) (termToJS env' u f)
+
 termToJS env (CApp t args) f = termToJS env t (\ t' => argsToJS args [<] (\ args' => f (Apply t' args')))
   where
     argsToJS : List CExp -> SnocList JSExp -> (List JSExp -> JSStmt e) -> JSStmt e
@@ -144,7 +152,7 @@ expToDoc (LitString str) = jsString str
 expToDoc (LitInt i) = text $ show i
 expToDoc (Apply x xs) = expToDoc x ++ "(" ++ commaSep (map expToDoc xs) ++ ")"
 expToDoc (Var nm) = text nm
-expToDoc (JLam nms (JReturn exp)) = text "(" <+> text (joinBy ", " nms) <+> ") =>" <+> expToDoc exp
+expToDoc (JLam nms (JReturn exp)) = text "(" <+> text (joinBy ", " nms) <+> ") =>" <+> "(" ++ expToDoc exp ++ ")"
 expToDoc (JLam nms body) = text "(" <+> text (joinBy ", " nms) <+> ") =>" <+> bracket "{" (stmtToDoc body) "}"
 expToDoc JUndefined = text "undefined"
 expToDoc (Index obj ix) = expToDoc obj ++ "[" ++ expToDoc ix ++ "]"
@@ -160,6 +168,9 @@ altToDoc (JDefAlt stmt) = text "default" ++ ":" ++ caseBody stmt
 
 stmtToDoc (JSnoc x y) = stmtToDoc x </> stmtToDoc y
 stmtToDoc (JPlain x) = expToDoc x ++ ";"
+-- I might not need these split yet.
+stmtToDoc (JLet nm body) = "let" <+> text nm ++ ";" </> stmtToDoc body
+stmtToDoc (JAssign nm expr) = text nm <+> "=" <+> expToDoc expr ++ ";"
 stmtToDoc (JConst nm x) = text "const" <+> text nm <+> "=" <+/> expToDoc x ++ ";"
 stmtToDoc (JReturn x) = text "return" <+> expToDoc x ++ ";"
 stmtToDoc (JError str) = text "throw new Error(" ++ text str ++ ");"
@@ -181,7 +192,9 @@ entryToDoc : TopEntry -> M Doc
 entryToDoc (MkEntry name ty (Fn tm)) = do
   -- so this has a bunch of lambdas on it now, which we want to consolidate
   -- and we might need betas? It seems like a mirror of what happens in CExp
+  debug "compileFun \{pprint [] tm}"
   ct <- compileFun tm
+  -- now show for ct...
   let body = stmtToDoc $ termToJS [] ct JPlain
   pure (text "const" <+> text name <+> text "=" <+/> body)
 entryToDoc (MkEntry name type Axiom) = pure ""

src/Lib/CompileExp.idr

@@ -32,6 +32,7 @@ data CExp : Type where
   CRef : Name -> CExp
   CMeta : Nat -> CExp
   CLit : Literal -> CExp
+  CLet : Name -> CExp -> CExp -> CExp
 
 ||| I'm counting Lam in the term for arity.  This matches what I need in
 ||| code gen.
@@ -110,7 +111,7 @@ compileTerm (Case _ t alts) = do
     CaseCons nm args tm => pure $ CConAlt nm args !(compileTerm tm)) alts
   pure $ CCase t' alts'
 compileTerm (Lit _ lit) = pure $ CLit lit
-
+compileTerm (Let _ nm t u) = pure $ CLet nm !(compileTerm t) !(compileTerm u)
 
 export
 compileFun : Tm -> M CExp

src/Lib/ProcessDecl.idr

@@ -18,8 +18,7 @@ getArity _ = Z
 -- Can metas live in context for now?
 -- We'll have to be able to add them, which might put gamma in a ref
 
--- collect Defs into List Decl, special type, or add Defs to Decl?
-
+||| collectDecl collects multiple Def for one function into one
 export
 collectDecl : List Decl -> List Decl
 collectDecl [] = []

src/Lib/TT.idr

@@ -101,13 +101,9 @@ lookup ctx nm = go ctx.types
 -- if it's top / ctx / IORef, I also need IO...
 -- if I want errors, I need m anyway.  I've already got an error down there.
 
-
-
 export
 eval : Env -> Mode -> Tm -> M Val
 
-
-
 -- REVIEW everything is evalutated whether it's needed or not
 -- It would be nice if the environment were lazy.
 -- e.g. case is getting evaluated when passed to a function because
@@ -174,13 +170,14 @@ eval env mode (Meta fc i) =
         (Solved k t) => pure $ t
 eval env mode (Lam fc x t) = pure $ VLam fc x (MkClosure env t)
 eval env mode (Pi fc x icit a b) = pure $ VPi fc x icit !(eval env mode a) (MkClosure env b)
+eval env mode (Let fc nm t u) = pure $ VLet fc nm !(eval env mode t) (MkClosure env u)
 -- Here, we assume env has everything. We push levels onto it during type checking.
 -- I think we could pass in an l and assume everything outside env is free and
 -- translate to a level
 eval env mode (Bnd fc i) = case getAt i env of
   Just rval => pure rval
   Nothing => error' "Bad deBruin index \{show i}"
-eval env mode (Lit fc lit) =pure $ VLit fc lit
+eval env mode (Lit fc lit) = pure $ VLit fc lit
 
 -- We need a neutral and some code to run the case tree
 
@@ -205,6 +202,7 @@ quote l (VVar fc k sp) = if k < l
 quote l (VMeta fc i sp) = quoteSp l (Meta fc i) sp
 quote l (VLam fc x t) = pure $ Lam fc x !(quote (S l) !(t $$ VVar emptyFC l [<]))
 quote l (VPi fc x icit a b) = pure $ Pi fc x icit !(quote l a) !(quote (S l) !(b $$ VVar emptyFC l [<]))
+quote l (VLet fc nm t u) = pure $ Let fc nm !(quote l t) !(quote (S l) !(u $$ VVar emptyFC l [<]))
 quote l (VU fc) = pure (U fc)
 quote l (VRef fc n def sp) = quoteSp l (Ref fc n def) sp
 quote l (VCase fc sc alts) = pure $ Case fc !(quote l sc) alts

src/Lib/Types.idr

@@ -84,6 +84,8 @@ data Tm : Type where
   Pi  : FC -> Name -> Icit -> Tm -> Tm -> Tm
   -- REVIEW - do we want to just push it up like idris?
   Case : FC -> Tm -> List CaseAlt -> Tm
+  -- need type?
+  Let : FC -> Name -> Tm -> Tm -> Tm
   Lit : FC -> Literal -> Tm
 
 %name Tm t, u, v
@@ -99,6 +101,7 @@ HasFC Tm where
   getFC (Pi fc str icit t u) = fc
   getFC (Case fc t xs) = fc
   getFC (Lit fc _) = fc
+  getFC (Let fc _ _ _) = fc
 
 covering
 Show Tm
@@ -121,6 +124,7 @@ Show Tm where
   show (Pi _ str Explicit t u) = "(Pi (\{str} : \{show t}) => \{show u})"
   show (Pi _ str Implicit t u) = "(Pi {\{str} : \{show t}} => \{show u})"
   show (Case _ sc alts) = "(Case \{show sc} \{show alts})"
+  show (Let _ nm t u) = "(Let \{nm} \{show t} \{show u})"
 
 -- I can't really show val because it's HOAS...
 
@@ -150,8 +154,13 @@ pprint : List String -> Tm -> String
 pprint names tm = render 80 $ go names tm
   where
     go : List String -> Tm -> Doc
+    goAlt : List String -> CaseAlt -> Doc
+
+    goAlt names (CaseDefault t) = "_" <+> "=>" <+> go ("_" :: names) t
+    goAlt names (CaseCons name args t) = text name <+> spread (map text args) <+> "=>" <+> go (args ++ names) t
+
     go names (Bnd _ k) = case getAt k names of
-      Nothing => text "BND \{show k}"
+      Nothing => text "BND:\{show k}"
       Just nm => text "\{nm}:\{show k}"
     go names (Ref _ str mt) = text str
     go names (Meta _ k) = text "?m:\{show k}"
@@ -162,8 +171,10 @@ pprint names tm = render 80 $ go names tm
       text "({" <+> text nm <+> ":" <+> go names t <+> "}" <+> "=>" <+> go (nm :: names) u <+> ")"
     go names (Pi _ nm Explicit t u) =
       text "((" <+> text nm <+> ":" <+> go names t <+> ")" <+> "=>" <+> go (nm :: names) u <+> ")"
-    go names (Case _ _ _) = "FIXME CASE"
+    -- FIXME - probably way wrong on the names here.  There is implicit binding going on
+    go names (Case _ sc alts) = text "case" <+> go names sc <+> text "of" </> (nest 2 (line ++ stack (map (goAlt names) alts)))
     go names (Lit _ lit) = text "\{show lit}"
+    go names (Let _ nm t u) = text "let" <+> text nm <+> ":=" <+> go names t </> (nest 2 $ go names u)
 
 public export
 Pretty Tm where
@@ -176,6 +187,7 @@ Pretty Tm where
   pretty (Pi _ str icit t u) = text "(" <+> text str <+> ":" <+> pretty t <+> ")" <+> "=>" <+> pretty u <+> ")"
   pretty (Case _ _ _) = text "FIXME PRETTY CASE"
   pretty (Lit _ lit) = text (show lit)
+  pretty (Let _ _ _ _) = text "LET"
 
 -- public export
 -- data Closure : Nat -> Type
@@ -209,6 +221,7 @@ data Val : Type where
   VMeta : FC -> (ix : Nat) -> (sp : SnocList Val) -> Val
   VLam : FC -> Name -> Closure -> Val
   VPi : FC -> Name -> Icit -> (a : Lazy Val) -> (b : Closure) -> Val
+  VLet : FC -> Name -> Val -> (b : Closure) -> Val
   VU : FC -> Val
   VLit : FC -> Literal -> Val