diff --git a/Makefile b/Makefile index e456fb2..91e4a1e 100644 --- a/Makefile +++ b/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 diff --git a/TODO.md b/TODO.md index 7f2c4e7..b3e2bf9 100644 --- a/TODO.md +++ b/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 diff --git a/src/Lib/Compile.newt b/src/Lib/Compile.newt index 5bca8eb..cd99326 100644 --- a/src/Lib/Compile.newt +++ b/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) "}" diff --git a/src/Lib/CompileExp.newt b/src/Lib/CompileExp.newt index 314ce53..6d7c9b3 100644 --- a/src/Lib/CompileExp.newt +++ b/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 diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index ed586f0..00cc6d8 100644 --- a/src/Lib/Elab.newt +++ b/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 diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index 81bee6c..48c3d98 100644 --- a/src/Lib/ProcessDecl.newt +++ b/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 diff --git a/src/Lib/Syntax.newt b/src/Lib/Syntax.newt index b33b41f..7422100 100644 --- a/src/Lib/Syntax.newt +++ b/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 diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index c5544eb..8e65ad2 100644 --- a/src/Lib/Types.newt +++ b/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]" diff --git a/src/Prelude.newt b/src/Prelude.newt index 1607b38..01fbcc9 100644 --- a/src/Prelude.newt +++ b/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