Map Bool-shaped things to javascript bool, add if/then and tertiary to code gen

Makefile

@@ -21,6 +21,9 @@ newt3.js: newt2.js
 	time $(RUNJS) newt2.js src/Main.newt -o newt3.js
 	cmp newt2.js newt3.js
 
+min.js: newt3.js
+	scripts/pack
+
 test: newt.js
 	scripts/test
 

TODO.md

@@ -2,6 +2,10 @@
 ## TODO
 
 - [x] Take the parens off of FC to make vscode happy
+- [x] Magic to make Bool a boolean
+- [ ] Look into using holes for errors (https://types.pl/@AndrasKovacs/115401455046442009)
+  - This would let us hit more cases in a function when we hit an error.
+  - I've been wanting to try holes for parse errors too.
 - [ ] in-scope type at point in vscode
   - So the idea here is that the references will be via FC, we remember the type at declaration and then point the usage back to the declaration (FC -> FC). We could dump all of this. (If we're still doing json.)
   - Do we want to (maybe later) keep the scope as a FC? We could do scope at point then.
@@ -29,7 +33,7 @@
   - [ ] Add `export` keywords
 - [ ] vscode - run newt when switching editors
 - [ ] who calls X?  We can only do this scoped to the current context for now. Someday whole source dir. #lsp
-- [ ] Magic to make Bool a boolean
+q
 - [ ] case split
   - We could fake this up:
     - given a name and a point in the editor

src/Lib/Compile.newt

@@ -31,15 +31,16 @@ data JAlt : U where
   JLitAlt : ∀ e. JSExp -> JSStmt e -> JAlt
 
 data JSExp : U where
-  LitArray : List JSExp -> JSExp
   LitObject : List (String × JSExp) -> JSExp
   LitString : String -> JSExp
+  LitBool : Bool -> JSExp
   LitInt : Int -> JSExp
   Apply : JSExp -> List JSExp -> JSExp
   Var : String -> JSExp
   JLam : List String -> JSStmt Return -> JSExp
   JPrimOp : String → JSExp → JSExp → JSExp
   JUndefined : JSExp
+  JTernary : JSExp → JSExp → JSExp → JSExp
   Index : JSExp -> JSExp -> JSExp
   Dot : JSExp -> String -> JSExp
   Raw : String -> JSExp
@@ -54,6 +55,7 @@ data JSStmt : StKind -> U where
   JAssign : (nm : String) -> JSExp -> JSStmt (Assign nm)
   -- TODO - switch to Int tags
   JCase : ∀ a. JSExp -> List JAlt -> JSStmt a
+  JIfThen : ∀ a. JSExp -> JSStmt a -> JSStmt a -> JSStmt a
   -- throw can't be used
   JError : ∀ a. String -> JSStmt a
 
@@ -80,6 +82,7 @@ emptyJSEnv = MkEnv Nil 0
 
 litToJS : Literal -> JSExp
 litToJS (LString str) = LitString str
+litToJS (LBool b) = LitBool b
 litToJS (LChar c) = LitString $ pack (c :: Nil)
 litToJS (LInt i) = LitInt i
 
@@ -88,8 +91,6 @@ mkEnv : JSExp -> Int -> JSEnv -> List String -> JSEnv
 mkEnv nm k env Nil = env
 mkEnv nm k env (x :: xs) = mkEnv nm (1 + k) (push env (Dot nm "h\{show k}")) xs
 
-envNames : Env -> List String
-
 -- given a name, find a similar one that doesn't shadow in Env
 freshName : String -> JSEnv -> String
 freshName nm env = if free env.jsenv nm then nm else go nm 1
@@ -195,8 +196,11 @@ termToJS env (CApp t arg) f = termToJS env t (\ t' => termToJS env arg (\arg' =>
 
 termToJS {e} env (CCase t alts) f =
   termToJS env t $ \case
-    (Var nm) => maybeCaseStmt env (Var nm) alts
+    (Var nm) => do
+      let (Nothing) = jsITE (Var nm) alts f | Just rval => rval
+      maybeCaseStmt env (Var nm) alts
     t' => do
+      let (Nothing) = jsITE t' alts f | Just rval => rval
       -- TODO with inlining, we hit cases where the let gets pulled forward more than once
       -- two cases as separate args, se we need actual unique names. For now, we're calling
       -- incr when processing App, as a stopgap, we probably need a fresh names state monad
@@ -207,6 +211,18 @@ termToJS {e} env (CCase t alts) f =
         then (maybeCaseStmt env' t' alts)
         else JSnoc (JConst nm t') (maybeCaseStmt env' (Var nm) alts)
   where
+    tertiary : JSExp → JSStmt e → JSStmt e → Cont e → JSStmt e
+    tertiary sc (JReturn t) (JReturn f) k = JReturn $ JTernary sc t f
+    tertiary sc (JAssign nm t) (JAssign _ f) k = JAssign nm $ JTernary sc t f
+    tertiary sc t f k = JIfThen sc t f
+
+    jsITE : JSExp → List CAlt → Cont e → Maybe (JSStmt e)
+    jsITE sc (CLitAlt (LBool b) rhs :: alt :: Nil) f =
+      let t = termToJS env rhs f
+          e = termToJS env (getBody alt) f
+      in Just $ if b then tertiary sc t e f else tertiary sc e t f
+    jsITE sc alts f = Nothing
+
     termToJSAlt : JSEnv -> JSExp -> CAlt -> JAlt
     termToJSAlt env nm (CConAlt ix name info args u) = JConAlt ix (termToJS (mkEnv nm 0 env args) u f)
     -- intentionally reusing scrutinee name here
@@ -253,7 +269,8 @@ jsIdent id = if elem id jsKeywords then text ("$" ++ id) else text $ pack $ fix
 stmtToDoc : ∀ e. JSStmt e -> Doc
 
 expToDoc : JSExp -> Doc
-expToDoc (LitArray xs) = fatalError "TODO - LitArray to doc"
+expToDoc (LitBool b) = if b then text "true" else text "false"
+expToDoc (JTernary sc t f) = bracket "(" (expToDoc sc <+> text "?" <+> expToDoc t <+> text ":" <+> expToDoc f )")"
 expToDoc (LitObject xs) = text "{" <+> folddoc (\ a e => a ++ text ", " <+/> e) (map entry xs) <+> text "}"
   where
     entry : (String × JSExp) -> Doc
@@ -291,6 +308,10 @@ stmtToDoc (JAssign nm expr) = jsIdent nm <+> text "=" <+> expToDoc expr ++ text
 stmtToDoc (JConst nm x) = text "const" <+> jsIdent nm <+> nest 2 (text "=" <+/> expToDoc x ++ text ";")
 stmtToDoc (JReturn x) = text "return" <+> expToDoc x ++ text ";"
 stmtToDoc (JError str) = text "throw new Error(" ++ text (quoteString str) ++ text ");"
+stmtToDoc (JIfThen sc t e) =
+  text "if (" ++ expToDoc sc ++ text ")"
+    <+> bracket "{" (stmtToDoc t) "}"
+    <+> text "else" <+> bracket "{" (stmtToDoc e) "}"
 stmtToDoc (JCase sc alts) =
   text "switch (" ++ expToDoc sc ++ text ")" <+> bracket "{" (stack $ map altToDoc alts) "}"
 

src/Lib/CompileExp.newt

@@ -52,11 +52,17 @@ lamArity : Tm -> Nat
 lamArity (Lam _ _ _ _ t) = S (lamArity t)
 lamArity _ = Z
 
+-- It would be nice to be able to declare these
 compilePrimOp : String → List CExp → Maybe CExp
 compilePrimOp "Prelude.addString" (x :: y :: Nil) = Just (CPrimOp "+" x y)
 compilePrimOp "Prelude.addInt" (x :: y :: Nil) = Just (CPrimOp "+" x y)
 compilePrimOp "Prelude.mulInt" (x :: y :: Nil) = Just (CPrimOp "*" x y)
 compilePrimOp "Prelude.subInt" (x :: y :: Nil) = Just (CPrimOp "-" x y)
+compilePrimOp "Prelude._&&_" (x :: y :: Nil) = Just (CPrimOp "&&" x y)
+compilePrimOp "Prelude._||_" (x :: y :: Nil) = Just (CPrimOp "||" x y)
+-- Assumes Bool is in the right order!
+compilePrimOp "Prelude.jsEq" (_ :: x :: y :: Nil) = Just (CPrimOp "==" x y)
+compilePrimOp "Prelude.jsLt" (_ :: x :: y :: Nil) = Just (CPrimOp "<" x y)
 compilePrimOp "Prelude.divInt" (x :: y :: Nil) = Just (CPrimOp "|" (CPrimOp "/" x y) (CLit $ LInt 0))
 compilePrimOp _ _ = Nothing
 
@@ -104,6 +110,11 @@ lookupDef fc nm = do
     Nothing => error fc "\{show nm} not in scope"
     Just def => pure def
 
+getBody : CAlt → CExp
+getBody (CConAlt _ _ _ _ t) = t
+getBody (CLitAlt _ t) = t
+getBody (CDefAlt t) = t
+
 compileTerm : {{Ref2 Defs St}} → Tm -> M CExp
 compileTerm (Bnd _ k) = pure $ CBnd k
 -- need to eta expand to arity
@@ -116,6 +127,8 @@ compileTerm t@(Ref fc nm@(QN _ tag)) = do
     Z =>
       case the (Maybe Def) $ lookupMap' nm defs of
         Just (DCon ix EnumCon _ _) => pure $ CLit $ LInt $ cast ix
+        Just (DCon ix FalseCon _ _) => pure $ CLit $ LBool False
+        Just (DCon ix TrueCon _ _) => pure $ CLit $ LBool True
         Just (DCon _ ZeroCon _ _) => pure $ CLit $ LInt 0
         Just (DCon _ SuccCon _ _) =>
           pure $ CLam "x" $ CPrimOp "+" (CLit $ LInt 1) (CBnd 0)
@@ -176,6 +189,8 @@ compileTerm (Case fc t alts) = do
 
     enumAlt : CAlt → CAlt
     enumAlt (CConAlt ix nm EnumCon args tm) = CLitAlt (LInt $ cast ix) tm
+    enumAlt (CConAlt ix nm FalseCon args tm) = CLitAlt (LBool False) tm
+    enumAlt (CConAlt ix nm TrueCon args tm) = CLitAlt (LBool True) tm
     enumAlt alt = alt
 
     isInfo : ConInfo → CAlt → Bool
@@ -186,10 +201,6 @@ compileTerm (Case fc t alts) = do
     isDef (CDefAlt _) = True
     isDef _ = False
 
-    getBody : CAlt → CExp
-    getBody (CConAlt _ _ _ _ t) = t
-    getBody (CLitAlt _ t) = t
-    getBody (CDefAlt t) = t
 
     doNumCon : CExp → List CAlt → List CAlt
     doNumCon sc alts =
@@ -237,6 +248,8 @@ compileFun tm = go tm Lin
 -- What are the Defs used for above? (Arity for name)
 compileDCon : Nat → QName → ConInfo → Int → CExp
 compileDCon ix (QN _ nm) EnumCon 0 = CLit $ LInt $ cast ix
+compileDCon ix (QN _ nm) TrueCon 0 = CLit $ LBool True
+compileDCon ix (QN _ nm) FalseCon 0 = CLit $ LBool False
 compileDCon ix (QN _ nm) info 0 = CConstr ix nm Nil
 compileDCon ix (QN _ nm) info arity =
   let args = map (\k => "h\{show k}") (range 0 arity) in

src/Lib/Elab.newt

@@ -1189,15 +1189,17 @@ buildLitCases ctx prob fc scnm scty = do
 -- TODO - figure out if these need to be in Prelude or have a special namespace
 -- If we lookupRaw "String", we could get different answers in different contexts.
 -- maybe Hardwire this one
-stringType intType charType : QName
+stringType intType charType boolType : QName
 stringType = QN primNS "String"
 intType = QN primNS "Int"
 charType = QN primNS "Char"
+boolType = QN primNS "Bool"
 
 litTyName : Literal -> QName
 litTyName (LString str) = stringType
 litTyName (LInt i) = intType
 litTyName (LChar c) = charType
+litTyName (LBool _) = boolType -- not used
 
 renameContext : String -> String -> Context -> Context
 renameContext from to ctx = MkCtx ctx.lvl ctx.env (go ctx.types) ctx.bds ctx.ctxFC

src/Lib/ProcessDecl.newt

@@ -137,6 +137,7 @@ processPrimFn ns fc nm used ty src = do
   let arity = piArity ty'
   setDef (QN ns nm) fc ty' (PrimFn src arity used') Nil
 
+-- Heuristic for whether a function is simple enough to inline
 -- I'm trying to get ++ and + inlined as javascript +
 complexity : Tm → Int
 complexity (Ref _ _) = 1
@@ -186,7 +187,7 @@ processDef ns fc nm clauses = do
   -- putStrLn $ show tm
   -- TODO we need some protection against inlining a function calling itself.
   -- We need better heuristics, maybe fuel and deciding while inlining.
-  -- bind is explicit here because the complexity has a 100 in it.
+  -- IO,bind is explicit here because the complexity has a 100 in it.
   let name = show $ QN ns nm
   if complexity tm < 15 || name == "Prelude.Prelude.Monad Prelude.IO,bind" || name == "Prelude._>>=_"
     then setFlag (QN ns nm) fc Inline
@@ -404,6 +405,8 @@ processShortData ns fc lhs sigs = do
 populateConInfo : List TopEntry → List TopEntry
 populateConInfo entries =
   let (Nothing) = traverse checkEnum entries
+    -- Boolean
+    | Just (a :: b :: Nil) => (setInfo a FalseCon :: setInfo b TrueCon :: Nil)
     | Just entries => entries in
   let (a :: b :: Nil) = entries | _ => entries in
   let (Just succ) = find isSucc entries | _ => entries in

src/Lib/Syntax.newt

@@ -212,6 +212,7 @@ instance Show Raw where
 
 instance Pretty Literal where
   pretty (LString t) = text t
+  pretty (LBool b) = if b then text "true" else text "false"
   pretty (LInt i) = text $ show i
   pretty (LChar c) = text $ show c
 

src/Lib/Types.newt

@@ -51,10 +51,11 @@ instance HasFC BindInfo where
 
 Tm : U
 
-data Literal = LString String | LInt Int | LChar Char
+data Literal = LString String | LInt Int | LChar Char | LBool Bool
 
 instance Show Literal where
   show (LString str) = quoteString str
+  show (LBool b) = if b then "true" else "false"
   show (LInt i) = show i
   show (LChar c) = "'\{show c}'" -- FIXME single quote
 
@@ -337,17 +338,21 @@ instance Eq MetaMode where
   NoCheck == NoCheck = True
   _ == _ = False
 
-data ConInfo = NormalCon | SuccCon | ZeroCon | EnumCon
+data ConInfo = NormalCon | SuccCon | ZeroCon | EnumCon | TrueCon | FalseCon
 
 instance Eq ConInfo where
   NormalCon == NormalCon = True
   SuccCon == SuccCon = True
   ZeroCon == ZeroCon = True
   EnumCon == EnumCon = True
+  TrueCon == TrueCon = True
+  FalseCon == FalseCon = True
   _ == _ = False
 
 instance Show ConInfo where
   show NormalCon = ""
+  show FalseCon = "[F]"
+  show TrueCon = "[T]"
   show SuccCon = "[S]"
   show ZeroCon = "[Z]"
   show EnumCon = "[E]"

src/Prelude.newt

@@ -10,7 +10,8 @@ const : ∀ a b. a → b → a
 const a b = a
 
 data Unit = MkUnit
-data Bool = True | False
+-- False first so it ends up being false
+data Bool = False | True
 
 not : Bool → Bool
 not True = False