update bootstrap

Allow:
```newt
data Foo : U
```
as a forward declaration for data. (The `Foo : U` syntax still works for
now.)

TODO.md

@@ -1,9 +1,21 @@
 
 ## TODO
 
+- [ ] For errors in other files, point to import
+- [x] Unsolved metas should be errors (user metas are fine)
+- [x] Better syntax for forward declared data (so we can distinguish from functions)
+- [ ] maybe allow "Main" module name for any file
+- [ ] Improve handling of names:
+  - We need FC on names in a lot of places
+  - [x] FC for duplicate `data`, `record`, `class` name is wrong (points to `data`)
+  - [x] FC on bad import should point to the name
+  - [x] Current module overrides imports
+  - [ ] Allow Qualified names in surface syntax
+  - Don't disambiguate on type for now
 - [x] 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 at the parsing level, but we don't have typecase, so...
+  - There may be ambiguity issues at the parsing level, but we don't have typecase, so.
+  - It's less to type, too.
 - [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 ...`
@@ -13,7 +25,7 @@
   - I can do `let f : ... = \ a b c => ...`. But it doesn't work for recursion and cases are awkward.
 - [x] Erasure checking happens at compile time and isn't surfaced to editor..
 - [ ] Erasure issue during AoC from case building replacing a non-erased value with erased.
-- [ ] Add Foldable?
+- [x] Add Foldable
 - [ ] Maybe return constraints instead of solving metas during unification
   - We already return non-meta constraints for work on the LHS.
   - We might get into a situation where solving immediately would have gotten us more progress?
@@ -53,6 +65,7 @@
 - [ ] See if we can split up `Elab.newt`
   - Unify, checking, and case builder have circular references.
   - Perhaps unify should return constraints instead of calling solve directly.
+  - passing a pointer to `check` in the context may suffice
 - [ ] Add error for non-linear names in pattern matching (currently it picks one)
   - We probably should handle forced values. Idris requires them to have the same name.
 - [ ] Functions with erased-only arguments still get called with `()` - do we want this or should they be constants?
@@ -82,6 +95,7 @@
 - [ ] Look into descriptions, etc.
   - Can generating descriptions help with automatic "show" implementations
   - We lost debug printing when switching to numeric tags
+  - Where did I see the idea of generating descriptions for inductive types?
 - [ ] Add info to Ref/VRef (is dcon, arity, etc)
   - To save lookups during compilation and it might make eval faster
 - [x] number tags for data constructors

newt-vscode/src/extension.ts

@@ -128,6 +128,7 @@ export function activate(context: vscode.ExtensionContext) {
             let range = new vscode.Range(start, end);
             if (file !== fileName) {
               range = new vscode.Range(new vscode.Position(0,0), new vscode.Position(0,0));
+              message = `Error in ${file}: ${message}`
             }
             // anything indented after the ERROR/INFO line are part of
             // the message

src/Data/SortedMap.newt

@@ -220,3 +220,8 @@ foldMap f m ((a,b) :: xs) = case lookupMap a m of
 
 listValues : ∀ k v. SortedMap k v → List v
 listValues sm = map snd $ toList sm
+
+instance ∀ k. Foldable (SortedMap k) where
+  foldr f z m = foldr f z (listValues m)
+  foldl f z m = foldl f z (listValues m)
+

src/Lib/Parser.newt

@@ -533,10 +533,11 @@ parseImport : Parser Import
 parseImport = do
   fc <- getPos
   keyword "import"
-  ident <- uident
-  rest <- many $ token Projection
+  -- TODO revisit when we have parser for qualified names in source
+  (nameFC, ident) <- withFC uident
+  (restFC,rest) <- withFC $ many $ token Projection
   let name = joinBy "" (ident :: rest)
-  pure $ MkImport fc name
+  pure $ MkImport fc (nameFC + restFC, name)
 
 -- Do we do pattern stuff now? or just name = lambda?
 -- TODO multiple names
@@ -613,11 +614,12 @@ parseData : Parser Decl
 parseData = do
   fc <- getPos
   -- commit when we hit ":"
-  name <- try $ (keyword "data" *> (uident <|> ident <|> token MixFix) <* keyword ":")
+  name <- try $ (keyword "data" *> withFC (uident <|> token MixFix) <* keyword ":")
   ty <- typeExpr
-  keyword "where"
+  Just _ <- optional (keyword "where")
+    | _ => pure $ Data fc name ty Nothing
   decls <- startBlock $ manySame $ parseSig
-  pure $ Data fc name ty decls
+  pure $ Data fc name ty (Just decls)
 
 nakedBind : Parser Telescope
 nakedBind = do
@@ -631,10 +633,10 @@ parseRecord : Parser Decl
 parseRecord = do
   fc <- getPos
   keyword "record"
-  name <- uident
+  name <- withFC uident
   teles <- many $ ebind <|> nakedBind
   keyword "where"
-  cname <- optional $ keyword "constructor" *> (uident <|> token MixFix)
+  cname <- optional $ keyword "constructor" *> withFC (uident <|> token MixFix)
   decls <- startBlock $ manySame $ parseSig
   pure $ Record fc name (join teles) cname decls
 
@@ -644,7 +646,7 @@ parseClass : Parser Decl
 parseClass = do
   fc <- getPos
   keyword "class"
-  name <- uident
+  name <- withFC uident
   teles <- many $ ebind <|> nakedBind
   keyword "where"
   decls <- startBlock $ manySame $ parseSig

src/Lib/ProcessDecl.newt

@@ -69,7 +69,8 @@ logMetas (Unsolved fc k ctx ty kind cons :: rest) = do
           pure ("  \{show $ length' matches} Solutions: \{show matches}" :: Nil)
 
         _ => pure Nil
-      info fc $ unlines ((msg :: Nil) ++ msgs ++ sols)
+      -- info fc $ unlines ((msg :: Nil) ++ msgs ++ sols)
+      addError $ E fc $ unlines ((msg :: Nil) ++ msgs ++ sols)
       logMetas rest
 
 
@@ -94,7 +95,7 @@ impTele tele = map foo tele
 checkAlreadyDef : FC → Name → M Unit
 checkAlreadyDef fc nm = do
   top <- getTop
-  case lookupRaw nm top of
+  case lookup (QN top.ns nm) top of
     Nothing => pure MkUnit
     Just entry => error fc "\{show nm} is already defined at \{show entry.fc}"
 
@@ -104,14 +105,9 @@ processDecl : List String -> Decl -> M Unit
 processTypeSig : List String → FC → List Name → Raw → M Unit
 processTypeSig ns fc names tm = do
   log 1 $ \ _ => "-----"
-
   top <- getTop
-  let mc = top.metaCtx
-  -- let mstart = length' mc.metas
   traverse (checkAlreadyDef fc) names
   ty <- check (mkCtx fc) tm (VU fc)
-  -- this is not needed
-  -- ty <- zonk top 0 Nil ty
   log 1 $ \ _ => "TypeSig \{unwords names} : \{render 90 $ pprint Nil ty}"
   ignore $ for names $ \nm => setDef (QN ns nm) fc ty Axiom Nil
 
@@ -163,7 +159,7 @@ processDef ns fc nm clauses = do
   log 1 $ \ _ => "Def \{show nm}"
   top <- getTop
   let mc = top.metaCtx
-  let (Just entry) = lookupRaw nm top
+  let (Just entry) = lookup (QN ns nm) top
     | Nothing => throwError $ E fc "No declaration for \{nm}"
   let (MkEntry fc name ty Axiom _) = entry
     | _ => throwError $ E fc "\{nm} already defined at \{show entry.fc}"
@@ -213,8 +209,8 @@ processCheck ns fc tm ty = do
   putStrLn "  NF \{render 90 $ pprint Nil norm}"
 
 
-processClass : List String → FC → String → Telescope → List Decl → M Unit
-processClass ns classFC nm tele decls = do
+processClass : List String → FC → (FC × String) → Telescope → List Decl → M Unit
+processClass ns classFC (nameFC, nm) tele decls = do
   -- REVIEW maybe we can leverage Record for this
   -- a couple of catches, we don't want the dotted accessors and
   -- the self argument should be an auto-implicit
@@ -229,7 +225,7 @@ processClass ns classFC nm tele decls = do
 
   log 1 $ \ _ => "tcon type \{render 90 $ pretty tcType}"
   log 1 $ \ _ => "dcon type \{render 90 $ pretty dcType}"
-  let decl = Data classFC nm tcType (TypeSig classFC (dcName :: Nil) dcType :: Nil)
+  let decl = Data classFC (nameFC, nm) tcType (Just $ TypeSig classFC (dcName :: Nil) dcType :: Nil)
   log 1 $ \ _ => "Decl:"
   log 1 $ \ _ => render 90 $ pretty decl
   processDecl ns decl
@@ -284,7 +280,7 @@ processInstance ns instfc ty decls = do
   -- This needs to be declared before processing the defs, but the defs need to be
   -- declared before this - side effect is that a duplicate def is noted at the first
   -- member
-  case lookupRaw instname top of
+  case lookup (QN ns instname) top of
     Just _ => pure MkUnit -- TODO check that the types match
     Nothing => do
       -- only add once
@@ -378,10 +374,10 @@ processInstance ns instfc ty decls = do
 -- desugars to Data and processes it
 processShortData : List String → FC → Raw → List Raw → M Unit
 processShortData ns fc lhs sigs = do
-  (nm,args) <- getArgs lhs Nil
+  (nameFC, nm,args) <- getArgs lhs Nil
   let ty = foldr mkPi (RU fc) args
   cons <- traverse (mkDecl args Nil) sigs
-  let dataDecl = Data fc nm ty cons
+  let dataDecl = Data fc (nameFC, nm) ty (Just cons)
   log 1 $ \ _ => "SHORTDATA"
   log 1 $ \ _ => "\{render 90 $ pretty dataDecl}"
   processDecl ns dataDecl
@@ -389,8 +385,8 @@ processShortData ns fc lhs sigs = do
     mkPi : FC × Name → Raw → Raw
     mkPi (fc,n) a = RPi fc (BI fc n Explicit Zero) (RU fc) a
 
-    getArgs : Raw -> List (FC × String) -> M (String × List (FC × String))
-    getArgs (RVar fc1 nm) acc = pure (nm, acc)
+    getArgs : Raw -> List (FC × String) -> M (FC × String × List (FC × String))
+    getArgs (RVar fc1 nm) acc = pure (fc1, nm, acc)
     getArgs (RApp _ t (RVar fc' nm) _) acc = getArgs t ((fc', nm) :: acc)
     getArgs tm _ = error (getFC tm) "Expected contructor application, got: \{show tm}"
 
@@ -435,19 +431,19 @@ populateConInfo entries =
     isSucc (MkEntry fc nm dty@(Pi _ _ _ _ (Ref _ a) (Ref _ b)) (DCon _ _ (Many :: Nil) hn) _) = a == b
     isSucc _ = False
 
-processData : List String → FC → String → Raw → List Decl → M Unit
-processData ns fc nm ty cons = do
+processData : List String → FC → FC × String → Raw → List Decl → M Unit
+processData ns fc (nameFC, nm) ty cons = do
   log 1 $ \ _ => "-----"
   log 1 $ \ _ => "Data \{nm}"
   top <- getTop
   let mc = top.metaCtx
   tyty <- check (mkCtx fc) ty (VU fc)
-  case lookupRaw nm top of
+  case lookup (QN ns nm) top of
     Just (MkEntry _ name type Axiom _) => do
       tyty' <- eval Nil tyty
       type' <- eval Nil type
       unifyCatch fc (mkCtx fc) tyty' type'
-    Just _ => error fc "\{show nm} already declared"
+    Just _ => error nameFC "\{show nm} already declared"
     Nothing => setDef (QN ns nm) fc tyty Axiom Nil
   -- check cons, return list of type,con
   allCons <- join <$> (for cons $ \x => case x of
@@ -491,25 +487,25 @@ processData ns fc nm ty cons = do
     checkDeclType _ = error fc "data type doesn't return U"
 
 
-processRecord : List String → FC → String → Telescope → Maybe Name → List Decl → M Unit
-processRecord ns recordFC nm tele cname decls = do
+processRecord : List String → FC → FC × String → Telescope → Maybe (FC × Name) → List Decl → M Unit
+processRecord ns recordFC (nameFC, nm) tele cname decls = do
   log 1 $ \ _ => "-----"
   log 1 $ \ _ => "Record"
   let fields = getSigs decls
-  let dcName = fromMaybe "Mk\{show nm}" cname
+  let (dcFC,dcName) = fromMaybe (nameFC,"Mk\{show nm}") cname
   let tcType = teleToPi tele (RU recordFC)
-  let tail = foldl (\ acc bi => case bi : BindInfo × Raw of (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar recordFC nm) tele
+  let tail = foldl (\ acc bi => case bi : BindInfo × Raw of (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar nameFC nm) tele
   let dcType = teleToPi (impTele tele) $
     foldr (\ x acc => case x : FC × String × Raw of (fc, nm, ty) =>  RPi fc (BI fc nm Explicit Many) ty acc  ) tail fields
 
   log 1 $ \ _ => "tcon type \{render 90 $ pretty tcType}"
   log 1 $ \ _ => "dcon type \{render 90 $ pretty dcType}"
-  let decl = Data recordFC nm tcType (TypeSig recordFC (dcName :: Nil) dcType :: Nil)
+  let decl = Data recordFC (nameFC,nm) tcType (Just $ TypeSig recordFC (dcName :: Nil) dcType :: Nil)
   log 1 $ \ _ => "Decl:"
   log 1 $ \ _ => render 90 $ pretty decl
   processDecl ns decl
   -- pattern to peel out fields on LHS
-  let autoPat = foldl (\acc x => case x : FC × String × Raw of (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar recordFC dcName) fields
+  let autoPat = foldl (\acc x => case x : FC × String × Raw of (fc,nm,ty) => RApp fc acc (RVar nameFC nm) Explicit) (RVar nameFC dcName) fields
   processFields autoPat tail Nil fields
   where
     processFields : Raw → Raw → List (String × Raw) → List (FC × String × Raw) → M Unit
@@ -544,5 +540,7 @@ processDecl ns (DCheck fc tm ty) = processCheck ns fc tm ty
 processDecl ns (Class classFC nm tele decls) = processClass ns classFC nm tele decls
 processDecl ns (Instance instfc ty decls) = processInstance ns instfc ty decls
 processDecl ns (ShortData fc lhs sigs) = processShortData ns fc lhs sigs
-processDecl ns (Data fc nm ty cons) = processData ns fc nm ty cons
+processDecl ns (Data fc nm ty (Just cons)) = processData ns fc nm ty cons
+-- TODO distinguish from function signatures
+processDecl ns (Data fc (_, nm) ty Nothing) = processTypeSig ns fc (nm :: Nil) ty
 processDecl ns (Record recordFC nm tele cname decls) = processRecord ns recordFC nm tele cname decls

src/Lib/Syntax.newt

@@ -74,26 +74,24 @@ instance HasFC Raw where
   getFC (RUpdateRec fc _ _) = fc
   getFC (RImpossible fc) = fc
 
-data Import = MkImport FC Name
-
-
+data Import = MkImport FC (FC × Name)
 
 Telescope : U
 Telescope = List (BindInfo × Raw)
 
-
 data Decl
   = TypeSig FC (List Name) Raw
   | FunDef FC Name (List (Raw × Maybe Raw))
   | DCheck FC Raw Raw
-  | Data FC Name Raw (List Decl)
+  -- TODO maybe add Telescope (before `:`) and auto-add to constructors...
+  | Data FC (FC × Name) Raw (Maybe $ List Decl)
   | ShortData FC Raw (List Raw)
   | PType FC Name (Maybe Raw)
   | PFunc FC Name (List String) Raw String
   | PMixFix FC (List Name) Int Fixity
-  | Class FC Name Telescope (List Decl)
+  | Class FC (FC × Name) Telescope (List Decl)
   | Instance FC Raw (Maybe (List Decl))
-  | Record FC Name Telescope (Maybe Name) (List Decl)
+  | Record FC (FC × Name) Telescope (Maybe $ FC × Name) (List Decl)
 
 
 instance HasFC Decl where
@@ -142,7 +140,7 @@ instance Show Decl where
   show (ShortData _ lhs sigs) = foo ("ShortData" :: show lhs :: show sigs :: Nil)
   show (PFunc _ nm used ty src) = foo ("PFunc" :: nm :: show used :: show ty :: show src :: Nil)
   show (PMixFix _ nms prec fix) = foo ("PMixFix" :: show nms :: show prec :: show fix :: Nil)
-  show (Class _ nm tele decls) = foo ("Class" ::  nm :: "..." :: (show $ map show decls) :: Nil)
+  show (Class _ (_,nm) tele decls) = foo ("Class" ::  nm :: "..." :: (show $ map show decls) :: Nil)
   show (Instance _ nm decls) = foo ("Instance" ::  show nm :: (show $ map show decls) :: Nil)
   show (Record _ nm tele nm1 decls) = foo ("Record" :: show nm :: show tele :: show nm1 :: show decls :: Nil)
 
@@ -247,15 +245,16 @@ instance Pretty Decl where
       prettyPair : Raw × Maybe Raw → Doc
       prettyPair (a, Nothing) = pretty a
       prettyPair (a, Just b) = pretty a <+> text "=" <+> pretty b
-  pretty (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map pretty xs))
+  pretty (Data _ (_,nm) x Nothing) = text "data" <+> text nm <+> text ":" <+>  pretty x
+  pretty (Data _ (_,nm) x (Just xs)) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map pretty xs))
   pretty (DCheck _ x y) = text "#check" <+> pretty x <+> text ":" <+> pretty y
   pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => text ":" <+> pretty ty) ty)
   pretty (PFunc _ nm Nil ty src) = text "pfunc" <+> text nm <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src))
   pretty (PFunc _ nm used ty src) = text "pfunc" <+> text nm <+> text "uses" <+> spread (map text used) <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src))
   pretty (PMixFix _ names prec fix) = text (show fix) <+> text (show prec) <+> spread (map text names)
-  pretty (Record _ nm tele cname decls) = text "record" <+> text nm <+> text ":" <+> spread (map prettyBind tele)
-    <+> (nest 2 $ text "where" </> stack (maybe empty (\ nm' => text "constructor" <+> text nm') cname :: map pretty decls))
-  pretty (Class _ nm tele decls) = text "class" <+> text nm <+> text ":" <+> spread (map prettyBind tele)
+  pretty (Record _ (_,nm) tele (cname) decls) = text "record" <+> text nm <+> text ":" <+> spread (map prettyBind tele)
+    <+> (nest 2 $ text "where" </> stack (maybe empty (\ nm' => text "constructor" <+> text (snd nm')) cname :: map pretty decls))
+  pretty (Class _ (_,nm) tele decls) = text "class" <+> text nm <+> text ":" <+> spread (map prettyBind tele)
     <+> (nest 2 $ text "where" </> stack (map pretty decls))
   pretty (Instance _ _ _) = text "TODO pretty Instance"
   pretty (ShortData _ lhs sigs) = text "data" <+> pretty lhs <+> text "=" <+> pipeSep (map pretty sigs)
@@ -329,5 +328,5 @@ instance Pretty Module where
       </> stack (map pretty decls)
       where
         doImport : Import -> Doc
-        doImport (MkImport _ nm) = text "import" <+> text nm ++ line
+        doImport (MkImport _ (_,nm)) = text "import" <+> text nm ++ line
 

src/Main.newt

@@ -94,7 +94,7 @@ importHints (entry :: entries) = do
   importHints entries
 
 importToQN : Import → QName
-importToQN  (MkImport fc name') = uncurry QN $ unsnoc $ split1 name' "."
+importToQN  (MkImport fc (_,name)) = uncurry QN $ unsnoc $ split1 name "."
 
 -- New style loader, one def at a time
 processModule : FC -> String -> List String -> QName -> M String
@@ -128,13 +128,11 @@ processModule importFC base stk qn@(QN ns nm) = do
   let importNames = map importToQN imports
 
   imported <- for imports $ \case
-    MkImport fc name' => do
+    MkImport fc (nameFC,name') => do
       let (a,b) = unsnoc $ split1 name' "."
       let qname = QN a b
-      -- we could use `fc` if it had a filename in it
-      when (elem name' stk) $ \ _ => error emptyFC "import loop \{show name} -> \{show name'}"
-
-      processModule fc base (name :: stk) qname
+      when (elem name' stk) $ \ _ => error nameFC "import loop \{show name} -> \{show name'}"
+      processModule nameFC base (name :: stk) qname
       pure $ split name' "."
   let imported = snoc imported primNS
   srcSum <- liftIO $ checksum src
@@ -208,6 +206,9 @@ showErrors fn src = do
         exitFailure "Compile failed"
   pure MkUnit
 
+invalidateModule : QName -> M Unit
+invalidateModule (QN ns nm) = modifyTop [modules $= deleteMap (snoc ns nm)]
+
 -- processFile called on the top level file
 -- it sets up everything and then recurses into processModule
 processFile : String -> M Unit
@@ -239,6 +240,8 @@ processFile fn = do
   let modules = updateMap primNS (MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil) top.modules
   modifyTop (\ top => MkTop modules (primNS :: Nil) emptyMap Nil emptyMap top.metaCtx top.verbose top.errors top.ops)
 
+  invalidateModule qn
+
   src <- processModule emptyFC base Nil qn
   top <- getTop
 
@@ -305,16 +308,21 @@ runCommand (Verbose Nothing) = modifyTop [ verbose $= _+_ 1 ]
 runCommand (Verbose (Just v)) = modifyTop [ verbose := v ]
 runCommand (OutputJS fn) = writeSource fn
 
+-- Broken out to a separate function so I can hook it.
+runString : String → M Unit
+runString line = do
+  let (Right toks) = tokenise "<stdin>" line
+    | Left err => putStrLn (showError line err)
+  let (Right cmd) = parse "<stdin>" parseCommand toks
+    | Left err => putStrLn (showError line err)
+  catchError (runCommand cmd) (\ err => putStrLn $ showError line err)
+
 runRepl : M Unit
 runRepl = do
   liftIO $ putStr "> "
   Right line <- liftIO {M} $ readLine
     | Left err => pure MkUnit
-  let (Right toks) = tokenise "<stdin>" line
-    | Left err => putStrLn (showError line err) >> runRepl
-  let (Right cmd) = parse "<stdin>" parseCommand toks
-    | Left err => putStrLn (showError line err) >> runRepl
-  catchError (runCommand cmd) (\ err => putStrLn $ showError line err)
+  runString line
   runRepl
 
 -- TODO translate args into REPL commands?

src/Prelude.newt

@@ -476,15 +476,23 @@ pfunc stringToInt : String → Int := `(s) => {
   return rval
 }`
 
--- TODO - add Foldable
+class Foldable (m : U → U) where
+  foldl : ∀ a b. (b → a → b) → b → m a → b
+  foldr : ∀ a b. (a → b → b) → b → m a → b
 
-foldl : ∀ A B. (B → A → B) → B → List A → B
-foldl f acc Nil = acc
-foldl f acc (x :: xs) = foldl f (f acc x) xs
+instance Foldable List where
+  foldl f acc Nil = acc
+  foldl f acc (x :: xs) = foldl f (f acc x) xs
 
-foldr : ∀ a b. (a → b → b) → b → List a → b
-foldr f b Nil = b
-foldr f b (x :: xs) = f x (foldr f b xs)
+  foldr f b Nil = b
+  foldr f b (x :: xs) = f x (foldr f b xs)
+
+instance Foldable SnocList where
+  foldl f acc Lin = acc
+  foldl f acc (xs :< x) = f (foldl f acc xs) x
+
+  foldr f b Lin = b
+  foldr f b (xs :< x) = foldr f (f x b) xs
 
 infixl 9 _∘_
 _∘_ : ∀ A B C. (B → C) → (A → B) → A → C

tests/BadImport.newt

@@ -0,0 +1,4 @@
+module BadImport
+
+-- Error should point to name here
+import Does.Not.Exist

tests/BadImport.newt.fail

@@ -0,0 +1,2 @@
+*** Process tests/BadImport.newt
+ERROR at tests/BadImport.newt:4:8--4:22: error reading tests/Does/Not/Exist.newt: Error: ENOENT: no such file or directory, open 'tests/Does/Not/Exist.newt'

tests/ErrorDup.newt

@@ -0,0 +1,9 @@
+module ErrorDup
+
+data Nat = Z | S Nat
+
+data Nat = Z | S Nat
+
+record Nat where
+
+class Nat where

tests/ErrorDup.newt.fail

@@ -0,0 +1,21 @@
+*** Process tests/ErrorDup.newt
+module ErrorDup
+ERROR at tests/ErrorDup.newt:5:6--5:9: Nat already declared
+  data Nat = Z | S Nat
+  
+  data Nat = Z | S Nat
+       ^^^
+
+ERROR at tests/ErrorDup.newt:7:8--7:11: Nat already declared
+  data Nat = Z | S Nat
+  
+  record Nat where
+         ^^^
+
+ERROR at tests/ErrorDup.newt:9:7--9:10: Nat already declared
+  record Nat where
+  
+  class Nat where
+        ^^^
+
+Compile failed

tests/TestCase5.newt

@@ -1,35 +0,0 @@
-module TestCase5
-
--- last bit tests pulling solutions from context
-
-data Plus : U -> U where
-    MkPlus : {A : U} -> (A -> A -> A) -> Plus A
-
-infixl 7 _+_
-_+_ : {A : U} {{_ : Plus A}} -> A -> A -> A
-_+_ {{MkPlus plus}} x y = plus x y
-
-
-pfunc plusInt : Int -> Int -> Int := `(x,y) => x + y`
-
-PlusInt : Plus Int
-PlusInt = MkPlus plusInt
-
--- TODO this needs some aggressive inlining...
-double : Int -> Int
-double x = x + x
-
-data Nat : U where
-    Z : Nat
-    S : Nat -> Nat
-
-plus : Nat -> Nat -> Nat
-plus Z m = m
-plus (S n) m = S (plus n m)
-
-PlusNat : Plus Nat
-PlusNat = MkPlus plus
-
-double2 : {A : U} {{foo : Plus A}} -> A -> A
-double2 = \ a => a + a
-

tests/TypeClass.newt

@@ -1,84 +0,0 @@
-module TypeClass
-
-data Monad : (U -> U) -> U where
-  MkMonad : { M : U -> U } ->
-            (bind : ∀ A B. (M A) -> (A -> M B) -> M B) ->
-            (pure : ∀ A. A -> M A) ->
-            Monad M
-
-infixl 1 _>>=_ _>>_
-_>>=_ : ∀ m a b. {{Monad m}} -> (m a) -> (a -> m b) -> m b
-_>>=_ {{MkMonad bind' _}}  ma amb = bind' ma amb
-
-_>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b
-ma >> mb = mb
-
-pure : ∀ m a. {{Monad m}} -> a -> m a
-pure {{MkMonad _ pure'}} a = pure' a
-
-data Either : U -> U -> U where
-  Left : ∀ A B. A -> Either A B
-  Right : ∀ A B. B -> Either A B
-
-bindEither : ∀ A B C. (Either A B) -> (B -> Either A C) -> Either A C
-bindEither (Left a) amb = Left a
-bindEither (Right b) amb = amb b
-
-EitherMonad : {A : U} -> Monad (Either A)
-EitherMonad = MkMonad {Either A} bindEither Right
-
-data Maybe : U -> U where
-  Just    : ∀ A. A -> Maybe A
-  Nothing : ∀ A. Maybe A
-
-bindMaybe : ∀ A B. Maybe A -> (A -> Maybe B) -> Maybe B
-bindMaybe Nothing amb = Nothing
-bindMaybe (Just a) amb = amb a
-
-MaybeMonad : Monad Maybe
-MaybeMonad = MkMonad bindMaybe Just
-
-infixr 7 _::_
-data List : U -> U where
-  Nil : ∀ A. List A
-  _::_ : ∀ A. A -> List A -> List A
-
-infixl 7 _++_
-_++_ : ∀ A. List A -> List A -> List A
-Nil ++ ys = ys
-(x :: xs) ++ ys = x :: (xs ++ ys)
-
-bindList : ∀ A B. List A -> (A -> List B) -> List B
-bindList Nil f = Nil
-bindList (x :: xs) f = f x ++ bindList xs f
-
-singleton : ∀ A. A -> List A
-singleton a = a :: Nil
-
--- TODO need better error when the monad is not defined
-ListMonad : Monad List
-ListMonad = MkMonad bindList singleton
-
-infixr 1 _,_
-data Pair : U -> U -> U where
-  _,_ : ∀ A B. A -> B -> Pair A B
-
-
-
-test : Maybe Int
-test = pure 10
-
-foo : Int -> Maybe Int
-foo x = Just 42 >> Just x >>= (\ x => pure 10)
-
-bar : Int -> Maybe Int
-bar x = do
-  let y = x
-  z <- Just x
-  pure z
-
-baz : ∀ A B. List A -> List B -> List (Pair A B)
-baz xs ys = do
-  x <- xs
-  y <- ys
-  pure (x , y)