add sugar for if/then/else

TODO.md

@@ -7,7 +7,6 @@
   - maybe a file listing jobs, whether they are known broken, optional expected output, optional expected JS execution output.
 - [x] forall / ∀ sugar (Maybe drop this, issues with `.` and `{A}` works fine)
 - [x] Bad module name error has FC 0,0 instead of the module or name
-- [x] I've made `{x}` be `{x : _}` instead of `{_ : x}`. Change this.
 - [ ] Remove context lambdas when printing solutions (show names from context)
   - maybe build list of names and strip λ, then call pprint with names
 - [ ] Revisit substitution in case building
@@ -46,12 +45,18 @@
   - [x] day1
   - [x] day2
   - some "real world" examples
+- [ ] Translate newt to newt
+  - [x] Prettier
+  - [x] if / then / else sugar
+  - [ ] `data Foo = A | B` sugar
+  - [ ] records
+  - [ ] where
 - [x] Maybe Eq and stuff would work for typeclass without dealing with unification issues yet
 - [x] unsolved meta errors repeat (need to freeze or only report at end)
 - [x] Sanitize JS idents, e.g. `_+_`
 - [x] Generate some programs that do stuff
 - [x] import
-- [ ] consider making meta application implicit in term, so its more readable when printed
+- [ ] consider making meta application implicit in term, so it's more readable when printed
   - Currently we have explicit `App` surrounding `Meta` when inserting metas. Some people
     leave that implicit for efficiency. I think it would also make printing more readable.
   - When printing `Value`, I now print the spine size instead of spine.

newt-vscode/syntaxes/newt.tmLanguage.json

@@ -16,7 +16,7 @@
     },
     {
       "name": "keyword.newt",
-      "match": "\\b(data|where|case|of|let|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b"
+      "match": "\\b(data|where|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b"
     },
     {
       "name": "string.js",

playground/src/monarch.ts

@@ -76,6 +76,9 @@ export let newtTokens: monaco.languages.IMonarchLanguage = {
     "module",
     "ptype",
     "pfunc",
+    "if",
+    "then",
+    "else",
     "module",
     "infixl",
     "infixr",

src/Lib/Elab.idr

@@ -860,6 +860,9 @@ undo ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo xs
 undo ((DoArrow fc nm tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc nm Explicit !(undo xs)) Explicit
 
 check ctx tm ty = case (tm, !(forceType ctx.env ty)) of
+  (RIf fc a b c, ty) =>
+    let tm' = RCase fc a [ MkAlt (RVar (getFC b) "True") b, MkAlt (RVar (getFC c) "False") c ] in
+    check ctx tm' ty
   (RDo fc stmts, ty) => check ctx !(undo stmts) ty
   (RCase fc rsc alts, ty) => do
     (sc, scty) <- infer ctx rsc

src/Lib/Parser.idr

@@ -240,6 +240,16 @@ doStmt
 doExpr : Parser Raw
 doExpr = RDo <$> getPos <* keyword "do" <*> (startBlock $ someSame doStmt)
 
+ifThenElse : Parser Raw
+ifThenElse = do
+  fc <- getPos
+  keyword "if"
+  a <- term
+  keyword "then"
+  b <- term
+  keyword "else"
+  c <- term
+  pure $ RIf fc a b c
 
 -- This hits an idris codegen bug if parseOp is last and Lazy
 term =  caseExpr
@@ -247,6 +257,7 @@ term =  caseExpr
     <|> lamExpr
     <|> doExpr
     <|> parseOp
+    <|> ifThenElse
 
 varname : Parser String
 varname = (ident <|> uident <|> keyword "_" *> pure "_")

src/Lib/Syntax.idr

@@ -78,6 +78,7 @@ data Raw : Type where
   RImplicit : (fc : FC) -> Raw
   RHole : (fc : FC) -> Raw
   RDo : (fc : FC) -> List DoStmt -> Raw
+  RIf : (fc : FC) -> Raw -> Raw -> Raw -> Raw
 
 
 %name Raw tm
@@ -96,6 +97,8 @@ HasFC Raw where
   getFC (RImplicit fc) = fc
   getFC (RHole fc) = fc
   getFC (RDo fc stmts) = fc
+  getFC (RIf fc _ _ _) = fc
+
 -- derive some stuff - I'd like json, eq, show, ...
 
 
@@ -189,6 +192,7 @@ Show Raw where
   show (RCase _ x xs) = foo [ "Case", show x, show xs]
   show (RDo _ stmts) = foo [ "DO", "FIXME"]
   show (RU _) = "U"
+  show (RIf _ x y z) = foo [ "If", show x, show y, show z]
 
 export
 Pretty Literal where
@@ -240,6 +244,7 @@ Pretty Raw where
     asDoc p (RImplicit _) = text "_"
     asDoc p (RHole _) = text "?"
     asDoc p (RDo _ stmts) = text "TODO - RDo"
+    asDoc p (RIf _ x y z) = par p 0 $ text "if" <+> asDoc 0 x <+/> "then" <+> asDoc 0 y <+/> "else" <+> asDoc 0 z
 
 export
 Pretty Module where

src/Lib/Tokenizer.idr

@@ -9,6 +9,7 @@ keywords : List String
 keywords = ["let", "in", "where", "case", "of", "data", "U", "do",
             "ptype", "pfunc", "module", "infixl", "infixr", "infix",
             "∀", "forall",
+            "if", "then", "else",
              "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_"]
 
 checkKW : String -> Token Kind