diff --git a/Makefile b/Makefile index cb0d8c5..a781c13 100644 --- a/Makefile +++ b/Makefile @@ -11,7 +11,9 @@ all: newt.js REV=$(shell git rev-parse --short HEAD) src/Revision.newt: .PHONY - echo "module Revision\nimport Prelude\ngitRevision : String\ngitRevision = \"${REV}\"" > src/Revision.newt + echo "module Revision\nimport Prelude\ngitRevision : String\ngitRevision = \"${REV}\"" > src/Revision.newt.new + cmp src/Revision.newt.new src/Revision.newt || cp src/Revision.newt.new src/Revision.newt + rm -f src/Revision.newt.new newt.js: ${SRCS} src/Revision.newt -rm build/* >/dev/null diff --git a/TODO.md b/TODO.md index 01d185d..60d2a17 100644 --- a/TODO.md +++ b/TODO.md @@ -1,9 +1,11 @@ ## TODO +- [ ] change "in prefix position" and "trailing operator" errors to do sections - [ ] maybe add fat arrows, I keep wanting to type them, `{{...}}` is a little ugly - - There may be ambiguity issues + - There may be ambiguity issues at the parsing level, but we don't have typecase, so... - [x] get some names on add missing cases (if not too difficult) +- [ ] Implement "add missing cases" for playground - [x] add optional types to case `case xxx : Maybe Int of ...` - [x] "Expected keyword" at `\ a ->` should be error at the `->` - [x] Show Either diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index a6e5d47..cb4eb9c 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -669,8 +669,6 @@ primType fc nm = do Just (MkEntry _ name ty (PrimTCon _) _) => pure $ VRef fc name Lin _ => error fc "Primitive type \{show nm} not in scope" -infer : Context -> Raw -> M (Tm × Val) - data Bind = MkBind String Icit Val instance Show Bind where @@ -1431,6 +1429,7 @@ updateRec ctx fc clauses arg ty = do getTele Nothing v = error (getFC v) "Expected a pi type, got \{show v}" getTele _ v = error (getFC v) "Expected a record type, got \{show v}" +infer : Context -> Raw -> M (Tm × Val) check ctx tm ty = do ty' <- forceType ctx.env ty diff --git a/src/Prelude.newt b/src/Prelude.newt index 12af0f3..662db97 100644 --- a/src/Prelude.newt +++ b/src/Prelude.newt @@ -716,6 +716,13 @@ instance Functor IO where uncurry : ∀ a b c. (a → b → c) → (a × b) → c uncurry f (a,b) = f a b +curry : ∀ a b c. (a × b → c) → (a → b → c) +curry f a b = f (a,b) + +-- TODO Belongs in prelude, but I need to rename a function in Lib.Compile (or let local win over imports) +-- apply : ∀ a b. (a → b) → a → b +-- apply f a = f a + -- TODO Idris has a tail recursive version of this instance Applicative List where return a = a :: Nil