Add flags to TopEntry, detect duplicate constructors, fix issue with missing constructors in CompileExp.

Makefile

@@ -39,7 +39,7 @@ newt2.js: newt.js
 
 newt3.js: newt2.js
 	rm -f build/*
-	$(RUNJS) newt2.js src/Main.newt -o newt3.js
+	time $(RUNJS) newt2.js src/Main.newt -o newt3.js
 	cmp newt2.js newt3.js
 
 test: newt.js

TODO.md

@@ -8,9 +8,10 @@ Syntax -> Parser.Impl ?
 - [ ] implement magic nat (need primitive `+`, '-', and `==` in `CompileExp`)
 - [ ] drop erased args on types and top level functions
 - [ ] can I do some inlining without blowing up code size?
-- [ ] implement string enum (or number, but I'm using strings for tags at the moment)
+- [ ] use hint table for auto solving. (I think walking the `toList` is a big chunk of performance in `Elab.newt`.)
-- [ ] use monaco input method instead of lean's
+- [x] implement string enum (or number, but I'm using strings for tags at the moment)
-- [ ] `Def` is shadowed between Types and Syntax (TCon vs DCon), detect this
+- [x] use monaco input method instead of lean's
+- [x] `Def` is shadowed between Types and Syntax (TCon vs DCon), detect this
 - [ ] review pattern matching. goal is to have a sane context on the other end. secondary goal - bring it closer to the paper.
   - Two issues
     - I'm rewriting stuff in the context, leaving it in a bad state (forward references). I think I can avoid this.
@@ -88,15 +89,15 @@ More comments in code! This is getting big enough that I need to re-find my bear
 - [ ] add default failing case for constructor matching to catch errors
 - [x] Add icit to Lam
 - [ ] add jump to definition magic to vscode extension
-  - [x] Cheap dump to def - dump context
+  - [x] Working for top level, we may want a proper REPL or LSP (and FC ranges?) before we do others
-- [ ] TCO? Probably needed in browser, since v8 doesn't do it. bun and JavaScriptCore do support it.
+- [x] TCO? Probably needed in browser, since v8 doesn't do it. bun and JavaScriptCore do support it.
 - [x] deconstructing `let` (and do arrows)
 - [x] Fix string printing to be js instead of weird Idris strings
 - [x] make $ special
   - Makes inference easier, cleaner output, and allows `foo $ \ x => ...`
   - [ ] `$` no longer works inside ≡⟨ ⟩ sort out how to support both that and `$ \ x => ...` (or don't bother)
     - We'd either need to blacklist all non-initial mixfix bits at the appropriate spots or always pass around a terminating token.
-- [ ] **Translate newt to newt**
+- [x] **Translate newt to newt**
   - [x] Support @ on the LHS
   - [x] if / then / else sugar
   - [x] `data Foo = A | B` sugar
@@ -152,7 +153,7 @@ More comments in code! This is getting big enough that I need to re-find my bear
 - [ ] copattern matching
 - [ ] Get `Combinatory.newt` to work
 - [x] Remember operators from imports
-- [ ] Default cases for non-primitives (currently gets expanded to all constructors)
+- [x] Default cases for non-primitives (currently gets expanded to all constructors)
   - This may need a little care. But I think I could collect all constructors that only match wildcards into a single case. This would lose any information from breaking out the individual, unnamed cases though.
   - There are cases where we have  `_` and then `Foo` on the next line, but they should all get collected into the `Foo` case. I think I sorted all of this out for primitives.
 - [x] Case for primitives

newt-vscode/.eslintrc.json

@@ -17,7 +17,7 @@
             }
         ],
         "@typescript-eslint/semi": "warn",
-        "curly": ["warn", "multi", "consistent"],
+        "curly": "off",
         "eqeqeq": "warn",
         "no-throw-literal": "warn",
         "semi": "off"

newt-vscode/src/extension.ts

@@ -85,6 +85,7 @@ export function activate(context: vscode.ExtensionContext) {
         // extract errors and messages from stdout
         const lines = stdout.split("\n");
         const diagnostics: vscode.Diagnostic[] = [];
+        const others: Record<string, vscode.Diagnostic[]> = {};
 
         if (err) {
           let start = new vscode.Position(0, 0);
@@ -117,7 +118,26 @@ export function activate(context: vscode.ExtensionContext) {
             let [_full, kind, file, line, column, message] = match;
             let lnum = Number(line);
             let cnum = Number(column);
-            if (file !== fileName) lnum = cnum = 0;
+
+            let severity;
+            if (kind === "ERROR") severity = vscode.DiagnosticSeverity.Error;
+            else if (kind === "WARN") severity = vscode.DiagnosticSeverity.Warning;
+            else severity = vscode.DiagnosticSeverity.Information;
+
+            // anything indented after the ERROR/INFO line are part of
+            // the message
+            while (lines[i + 1]?.match(/^(  )/)) message += "\n" + lines[++i];
+
+            if (file !== fileName) {
+              console.log('MM', file, fileName, lnum, cnum);
+              let start = new vscode.Position(lnum, cnum);
+              let end = new vscode.Position(lnum, cnum + 1);
+              let range = new vscode.Range(start, end);
+              const diag = new vscode.Diagnostic(range, message, severity);
+              if (!others[file]) others[file] = [];
+              others[file].push(diag);
+              lnum = cnum = 0;
+            }
 
             let start = new vscode.Position(lnum, cnum);
             // we don't have the full range, so grab the surrounding word
@@ -125,19 +145,13 @@ export function activate(context: vscode.ExtensionContext) {
             let range =
               document.getWordRangeAtPosition(start) ??
               new vscode.Range(start, end);
-            // anything indented after the ERROR/INFO line are part of
-            // the message
-            while (lines[i + 1]?.match(/^(  )/)) message += "\n" + lines[++i];
-
-            let severity;
-
-            if (kind === "ERROR") severity = vscode.DiagnosticSeverity.Error;
-            else if (kind === "WARN") severity = vscode.DiagnosticSeverity.Warning;
-            else severity = vscode.DiagnosticSeverity.Information;
             const diag = new vscode.Diagnostic(range, message, severity);
             if (kind === "ERROR" || lnum > 0) diagnostics.push(diag);
           }
         }
+        for (let file in others) {
+          diagnosticCollection.set(vscode.Uri.file(file), others[file])
+        }
         diagnosticCollection.set(vscode.Uri.file(fileName), diagnostics);
       }
     );

src/Lib/Compile.newt

@@ -308,7 +308,7 @@ getNames (Case x t alts) acc = foldl getAltNames acc alts
   where
     getAltNames : List QName -> CaseAlt -> List QName
     getAltNames acc (CaseDefault t) = getNames t acc
-    getAltNames acc (CaseCons name args t) = getNames t acc
+    getAltNames acc (CaseCons name args t) = name :: getNames t acc
     getAltNames acc (CaseLit lit t) = getNames t acc
 getNames _ acc = acc
 
@@ -321,12 +321,12 @@ getEntries acc name = do
     Nothing => do
       putStrLn "bad name \{show name}"
       pure acc
-    Just (MkEntry _ name type def@(Fn exp)) => case lookupMap' name acc of
+    Just (MkEntry _ name type def@(Fn exp) _) => case lookupMap' name acc of
       Just _ => pure acc
       Nothing =>
         let acc = updateMap name def acc in
         foldlM getEntries acc $ getNames exp Nil
-    Just (MkEntry _ name type def@(PrimFn _ _ used)) =>
+    Just (MkEntry _ name type def@(PrimFn _ _ used) _) =>
       let acc = updateMap name def acc in
       foldlM getEntries acc used
     Just entry => pure $ updateMap name entry.def acc
@@ -402,7 +402,7 @@ compile : M (List Doc)
 compile = do
   top <- getTop
   case lookupRaw "main" top of
-    Just (MkEntry fc name type def) => do
+    Just (MkEntry fc name type def _) => do
       tmp <- process name
       -- tack on call to main function
       let exec = stmtToDoc $ JPlain $ Apply (Var $ show name) Nil

src/Lib/CompileExp.newt

@@ -68,7 +68,6 @@ arityForName fc nm = do
     (Just (PrimFn t arity used)) => pure arity
 
 
-compileTerm : {{Ref2 Defs St}} → Tm -> M CExp
 
 -- need to eta out extra args, fill in the rest of the apps
 -- NOW - maybe eta here instead of Compile.newt, drop number on CApp
@@ -89,6 +88,14 @@ apply t ts acc Z = go (CApp t (acc <>> Nil) 0) ts
     go t Nil = pure t
     go t (arg :: args) = go (CApp t (arg :: Nil) 0) args
 
+lookupDef : {{Ref2 Defs St}} → FC → QName → M Def
+lookupDef fc nm = do
+  defs <- getRef Defs
+  case lookupMap' nm defs of
+    Nothing => error fc "\{show nm} not in scope"
+    Just def => pure def
+
+compileTerm : {{Ref2 Defs St}} → Tm -> M CExp
 compileTerm (Bnd _ k) = pure $ CBnd k
 -- need to eta expand to arity
 compileTerm t@(Ref fc nm@(QN _ tag)) = do
@@ -119,7 +126,6 @@ compileTerm tm@(App _ _ _) = case funArgs tm of
         t' <- compileTerm t
         args' <- traverse compileTerm args
         apply t' args' Lin Z
-        -- error (getFC t) "Don't know how to apply \{showTm t}"
 compileTerm (UU _) = pure $ CRef (QN Nil "U")
 compileTerm (Pi _ nm icit rig t u) = do
   t' <- compileTerm t
@@ -132,8 +138,9 @@ compileTerm (Case _ t alts) = do
     -- we use the base name for the tag, some primitives assume this
     CaseCons qn@(QN ns nm) args tm => do
       defs <- getRef Defs
-      case the (Maybe Def) $ lookupMap' qn defs of
+      def <- lookupDef emptyFC qn
-        Just (DCon EnumCon _ _) => CLitAlt (LString nm) <$> compileTerm tm
+      case def of
+        DCon EnumCon _ _ => CLitAlt (LString nm) <$> compileTerm tm
         _ => CConAlt nm args <$> compileTerm tm
     CaseLit lit tm => CLitAlt lit <$> compileTerm tm
   pure $ CCase t' alts'

src/Lib/Elab.newt

@@ -23,9 +23,9 @@ vprint ctx v = do
 -- collectDecl collects multiple Def for one function into one
 collectDecl : List Decl -> List Decl
 collectDecl Nil = Nil
-collectDecl ((Def fc nm cl) :: rest@(Def _ nm' cl' :: xs)) =
+collectDecl ((FunDef fc nm cl) :: rest@(FunDef _ nm' cl' :: xs)) =
-  if nm == nm' then collectDecl (Def fc nm (cl ++ cl') :: xs)
+  if nm == nm' then collectDecl (FunDef fc nm (cl ++ cl') :: xs)
-  else (Def fc nm cl :: collectDecl rest)
+  else (FunDef fc nm cl :: collectDecl rest)
 collectDecl (x :: xs) = x :: collectDecl xs
 
 rpprint : List String → Tm → String
@@ -116,8 +116,11 @@ isCandidate _ _ = False
 
 findMatches : Context -> Val -> List TopEntry -> M (List String)
 findMatches ctx ty Nil = pure Nil
-findMatches ctx ty ((MkEntry _ name type def) :: xs) = do
+findMatches ctx ty ((MkEntry _ name type def flags) :: xs) = do
-  let (True) = isCandidate ty type | False => findMatches ctx ty xs
+  let (True) = elem Hint flags | False => findMatches ctx ty xs
+  let (True) = isCandidate ty type
+    | False => findMatches ctx ty xs
+
   top <- getTop
   mc <- readIORef top.metaCtx
   catchError (do
@@ -473,7 +476,7 @@ unify env mode t u = do
       debug $ \ _ => "expand \{show t} =?= %ref \{show k'}"
       top <- getTop
       case lookup k' top of
-        Just (MkEntry _ name ty (Fn tm)) => do
+        Just (MkEntry _ name ty (Fn tm) _) => do
           vtm <- eval Nil CBN tm
           appvtm <- vappSpine vtm sp'
           unify env mode t appvtm
@@ -483,7 +486,7 @@ unify env mode t u = do
       debug $ \ _ => "expand %ref \{show k} \{show sp} =?= \{show u}"
       top <- getTop
       case lookup k top of
-        Just (MkEntry _ name ty (Fn tm)) => do
+        Just (MkEntry _ name ty (Fn tm) _) => do
           vtm <- eval Nil CBN tm
           tmsp <- vappSpine vtm sp
           unify env mode tmsp u
@@ -620,7 +623,7 @@ primType : FC -> QName -> M Val
 primType fc nm = do
   top <- getTop
   case lookup nm top of
-      Just (MkEntry _ name ty (PrimTCon _)) => pure $ VRef fc name Lin
+      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)
@@ -688,13 +691,13 @@ getConstructors ctx scfc (VRef fc nm _) = do
     lookupTCon str = do
       top <- getTop
       case lookup nm top of
-        (Just (MkEntry _ name type (TCon _ names))) => pure names
+        (Just (MkEntry _ name type (TCon _ names) _)) => pure names
         _ => error scfc "Not a type constructor \{show nm}"
     lookupDCon : QName -> M (QName × Int × Tm)
     lookupDCon nm = do
       top <- getTop
       case lookup nm top of
-        (Just (MkEntry _ name type (DCon _ k str))) => pure (name, k, type)
+        (Just (MkEntry _ name type (DCon _ k str) _)) => pure (name, k, type)
         Just _ => error fc "Internal Error: \{show nm} is not a DCon"
         Nothing => error fc "Internal Error: DCon \{show nm} not found"
 getConstructors ctx scfc tm = do
@@ -946,7 +949,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
               -- TODO can we check this when we make the PatCon?
               top <- getTop
               case lookup nm top of
-                  (Just (MkEntry _ name type (DCon _ k tcname))) =>
+                  (Just (MkEntry _ name type (DCon _ k tcname) _)) =>
                     if (tcname /= sctynm)
                       then error fc "Constructor is \{show tcname} expected \{show sctynm}"
                       else pure Nothing
@@ -974,7 +977,7 @@ mkPat (tm, icit) = do
   top <- getTop
   case splitArgs tm Nil of
     ((RVar fc nm), b) => case lookupRaw nm top of
-                (Just (MkEntry _ name type (DCon _ k str))) => do
+                (Just (MkEntry _ name type (DCon _ k str) _)) => do
                   -- TODO check arity, also figure out why we need reverse
                   bpat <- traverse (mkPat) b
                   pure $ PatCon fc icit name bpat Nothing
@@ -1006,7 +1009,7 @@ checkWhere ctx decls body ty = do
     | _ => check ctx body ty
   funTy <- check ctx rawtype (VU sigFC)
   debug $ \ _ => "where clause \{name} : \{rpprint (names ctx) funTy}"
-  let (Def defFC name' clauses :: decls') = decls
+  let (FunDef defFC name' clauses :: decls') = decls
     | x :: _ => error (getFC x) "expected function definition"
     | _ => error sigFC "expected function definition after this signature"
   unless (name == name') $ \ _ => error defFC "Expected def for \{name}"
@@ -1407,7 +1410,7 @@ infer ctx (RVar fc nm) = go 0 ctx.types
     go i Nil = do
       top <- getTop
       case lookupRaw nm top of
-        Just (MkEntry _ name ty def) => do
+        Just (MkEntry _ name ty def _) => do
           debug $ \ _ => "lookup \{show name} as \{show def}"
           vty <- eval Nil CBN ty
           pure (Ref fc name, vty)

src/Lib/Erasure.newt

@@ -19,7 +19,7 @@ getType (Ref fc nm) = do
   top <- getTop
   case lookup nm top of
     Nothing => error fc "\{show nm} not in scope"
-    (Just (MkEntry _ name type def)) => pure $ Just type
+    (Just (MkEntry _ name type def _)) => pure $ Just type
 getType tm = pure Nothing
 
 
@@ -48,7 +48,7 @@ doAlt : EEnv -> CaseAlt -> M CaseAlt
 doAlt env (CaseDefault t) = CaseDefault <$> erase env t Nil
 doAlt env (CaseCons name args t) = do
   top <- getTop
-  let (Just (MkEntry _ str type def)) = lookup name top
+  let (Just (MkEntry _ str type def _)) = lookup name top
     | _ => error emptyFC "\{show name} dcon missing from context"
   let env' = piEnv env type args
   CaseCons name args <$> erase env' t Nil
@@ -69,7 +69,7 @@ erase env t sp = case t of
     top <- getTop
     case lookup nm top of
       Nothing => error fc "\{show nm} not in scope"
-      (Just (MkEntry _ name type def)) => eraseSpine env t sp (Just type)
+      (Just (MkEntry _ name type def _)) => eraseSpine env t sp (Just type)
   (Lam fc nm icit rig u) => Lam fc nm icit rig <$> erase ((nm, rig, Nothing) :: env) u Nil
   -- If we get here, we're looking at a runtime pi type
   (Pi fc nm icit rig u v) => do

src/Lib/Eval.newt

@@ -70,7 +70,7 @@ tryEval : Env -> Val -> M (Maybe Val)
 tryEval env (VRef fc k sp) = do
   top <- getTop
   case lookup k top of
-      Just (MkEntry _ name ty (Fn tm)) =>
+      Just (MkEntry _ name ty (Fn tm) _) =>
         catchError (
             do
             debug $ \ _ =>  "app \{show name} to \{show sp}"
@@ -112,7 +112,7 @@ evalCase env mode sc@(VRef _ nm sp) (cc@(CaseCons name nms t) :: xs) = do
       debug $ \ _ =>  "ECase \{show nm} \{show sp} \{show nms} \{showTm t}"
       go env (sp <>> Nil) nms
     else case lookup nm top of
-      (Just (MkEntry _ str type (DCon _ k str1))) => evalCase env mode sc xs
+      (Just (MkEntry _ str type (DCon _ k str1) _)) => evalCase env mode sc xs
       -- bail for a stuck function
       _ => pure Nothing
   where

src/Lib/Parser.newt

@@ -528,7 +528,7 @@ parseDef = do
     startBlock $ manySame $ (parseSig <|> parseDef)
   let body = maybe body (\ decls => RWhere wfc decls body) w
   -- these get collected later
-  pure $ Def fc nm ((t, body) :: Nil) -- (MkClause fc Nil t body :: Nil)
+  pure $ FunDef fc nm ((t, body) :: Nil) -- (MkClause fc Nil t body :: Nil)
 
 
 parsePType : Parser Decl

src/Lib/ProcessDecl.newt

@@ -96,6 +96,13 @@ impTele tele = map foo tele
     foo (BI fc nm _ _ , ty) = (BI fc nm Implicit Zero, ty)
 
 
+checkAlreadyDef : FC → Name → M Unit
+checkAlreadyDef fc nm = do
+  top <- getTop
+  case lookupRaw nm top of
+    Nothing => pure MkUnit
+    Just entry => error fc "\{show nm} is already defined at \{show entry.fc}"
+
 
 processDecl : List String -> Decl -> M Unit
 
@@ -106,14 +113,12 @@ processTypeSig ns fc names tm = do
   top <- getTop
   mc <- readIORef top.metaCtx
   -- let mstart = length' mc.metas
-  for names $ \nm => do
+  traverse (checkAlreadyDef fc) names
-    let (Nothing) = lookupRaw nm top
-      | Just entry => error fc "\{show nm} is already defined at \{show entry.fc}"
-    pure MkUnit
   ty <- check (mkCtx fc) tm (VU fc)
   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
+  ignore $ for names $ \nm => setDef (QN ns nm) fc ty Axiom Nil
+
 
 
 processPrimType : List Name → FC → Name → Maybe Raw → M Unit
@@ -121,7 +126,7 @@ processPrimType ns fc nm ty = do
   top <- getTop
   ty' <- check (mkCtx fc) (maybe (RU fc) id ty) (VU fc)
   let arity = cast $ piArity ty'
-  setDef (QN ns nm) fc ty' (PrimTCon arity)
+  setDef (QN ns nm) fc ty' (PrimTCon arity) Nil
 
 
 processPrimFn : List String → FC → String → List String → Raw → String → M Unit
@@ -135,7 +140,7 @@ processPrimFn ns fc nm used ty src = do
     Nothing => error fc "\{name} not in scope"
     Just entry => pure entry.name
   let arity = piArity ty'
-  setDef (QN ns nm) fc ty' (PrimFn src arity used')
+  setDef (QN ns nm) fc ty' (PrimFn src arity used') Nil
 
 
 processDef : List String → FC → String → List (Raw × Raw) → M Unit
@@ -146,7 +151,7 @@ processDef ns fc nm clauses = do
   mc <- readIORef top.metaCtx
   let (Just entry) = lookupRaw nm top
     | Nothing => throwError $ E fc "No declaration for \{nm}"
-  let (MkEntry fc name ty Axiom) = entry
+  let (MkEntry fc name ty Axiom _) = entry
     | _ => throwError $ E fc "\{nm} already defined at \{show entry.fc}"
 
   log 1 $ \ _ => "check \{nm} at \{render 90 $ pprint Nil ty}"
@@ -216,7 +221,7 @@ processClass ns classFC nm tele decls = do
       let autoPat = foldl mkAutoApp (RVar classFC dcName) fields
       let lhs = makeLHS (RVar fc name) tele
       let lhs = RApp classFC lhs autoPat Auto
-      let decl = Def fc name ((lhs, (RVar fc name)) :: Nil)
+      let decl = FunDef fc name ((lhs, (RVar fc name)) :: Nil)
 
       log 1 $ \ _ => "\{name} : \{render 90 $ pretty funType}"
       log 1 $ \ _ => "\{render 90 $ pretty decl}"
@@ -264,17 +269,20 @@ processInstance ns instfc ty decls = do
     Just _ => pure MkUnit -- TODO check that the types match
     Nothing => processDecl ns sigDecl
 
+  setFlag (QN ns instname) instfc Hint
+  -- TODO add to hint dictionary
+
   let (Just decls) = collectDecl <$> decls
     | _ => do
       debug $ \ _ => "Forward declaration \{show sigDecl}"
 
   let (Ref _ tconName, args) = funArgs codomain
     | (tm, _) => error tyFC "\{render 90 $ pprint Nil codomain} doesn't appear to be a TCon application"
-  let (Just (MkEntry _ name type (TCon _ cons))) = lookup tconName top
+  let (Just (MkEntry _ name type (TCon _ cons) _)) = lookup tconName top
     | _ => error tyFC "\{show tconName} is not a type constructor"
   let (con :: Nil) = cons
     | _ => error tyFC "\{show tconName} has multiple constructors \{show cons}"
-  let (Just (MkEntry _ _ dcty (DCon _ _ _))) = lookup con top
+  let (Just (MkEntry _ _ dcty (DCon _ _ _) _)) = lookup con top
     | _ => error tyFC "can't find constructor \{show con}"
   vdcty@(VPi _ nm icit rig a b) <- eval Nil CBN dcty
     | x => error (getFC x) "dcty not Pi"
@@ -294,13 +302,14 @@ processInstance ns instfc ty decls = do
        let ty' = foldr (\ x acc => case the Binder x of (MkBinder fc nm' icit rig ty') => Pi fc nm' icit rig ty' acc) ty tele
        let nm' = "\{instname},\{nm}"
        -- we're working with a Tm, so we define directly instead of processDecl
-       let (Just (Def fc name xs)) = find (\x => case the Decl x of
+       let (Just (FunDef fc name xs)) = find (\x => case the Decl x of
-        (Def y name xs) => name == nm
+        (FunDef y name xs) => name == nm
         _ => False) decls
           | _ => error instfc "no definition for \{nm}"
 
-       setDef (QN ns nm') fc ty' Axiom
+       -- REVIEW if we want to Hint this
-       let decl = (Def fc nm' xs)
+       setDef (QN ns nm') fc ty' Axiom Nil
+       let decl = (FunDef fc nm' xs)
        log 1 $ \ _ => "***"
        log 1 $ \ _ => "«\{nm'}» : \{render 90 $ pprint Nil ty'}"
        log 1 $ \ _ => render 80 $ pretty decl
@@ -312,7 +321,7 @@ processInstance ns instfc ty decls = do
     debug $ \ _ => render 80 $ pretty decl
     processDecl ns decl
   let (QN _ con') = con
-  let decl = Def instfc instname ((RVar instfc instname, mkRHS instname conTele (RVar instfc con')) :: Nil)
+  let decl = FunDef instfc instname ((RVar instfc instname, mkRHS instname conTele (RVar instfc con')) :: Nil)
   log 1 $ \ _ => "SIGDECL"
   log 1 $ \ _ => "\{render 90 $ pretty sigDecl}"
   log 1 $ \ _ => render 80 $ pretty decl
@@ -388,20 +397,20 @@ populateConInfo entries =
   setInfo zero ZeroCon :: setInfo succ SuccCon :: Nil
   where
     setInfo : TopEntry → ConInfo → TopEntry
-    setInfo (MkEntry fc nm dty (DCon _ arity hn)) info = MkEntry fc nm dty (DCon info arity hn)
+    setInfo (MkEntry fc nm dty (DCon _ arity hn) flags) info = MkEntry fc nm dty (DCon info arity hn) flags
     setInfo x _ = x
 
     checkEnum : TopEntry → Maybe TopEntry
-    checkEnum (MkEntry fc nm dty (DCon _ 0 hn)) = Just $ MkEntry fc nm dty (DCon EnumCon 0 hn)
+    checkEnum (MkEntry fc nm dty (DCon _ 0 hn) flags) = Just $ MkEntry fc nm dty (DCon EnumCon 0 hn) flags
     checkEnum _ = Nothing
 
     isZero : TopEntry → Bool
-    isZero (MkEntry fc nm dty (DCon _ 0 hn)) = True
+    isZero (MkEntry fc nm dty (DCon _ 0 hn) flags) = True
     isZero _ = False
 
     -- TODO - handle indexes, etc
     isSucc : TopEntry → Bool
-    isSucc (MkEntry fc nm dty@(Pi _ _ _ _ (Ref _ a) (Ref _ b)) (DCon _ 1 hn)) = a == b
+    isSucc (MkEntry fc nm dty@(Pi _ _ _ _ (Ref _ a) (Ref _ b)) (DCon _ 1 hn) _) = a == b
     isSucc _ = False
 
 processData : List String → FC → String → Raw → List Decl → M Unit
@@ -412,14 +421,15 @@ processData ns fc nm ty cons = do
   mc <- readIORef top.metaCtx
   tyty <- check (mkCtx fc) ty (VU fc)
   case lookupRaw nm top of
-    Just (MkEntry _ name type Axiom) => do
+    Just (MkEntry _ name type Axiom _) => do
       tyty' <- eval Nil CBN tyty
       type' <- eval Nil CBN type
       unifyCatch fc (mkCtx fc) tyty' type'
-    Just (MkEntry _ name type _) => error fc "\{show nm} already declared"
+    Just _ => error fc "\{show nm} already declared"
-    Nothing => setDef (QN ns nm) fc tyty Axiom
+    Nothing => setDef (QN ns nm) fc tyty Axiom Nil
   entries <- join <$> (for cons $ \x => case x of
       (TypeSig fc names tm) => do
+          traverse (checkAlreadyDef fc) names
           debug $ \ _ => "check dcon \{show names} \{show tm}"
           dty <- check (mkCtx fc) tm (VU fc)
           debug $ \ _ => "dty \{show names} is \{render 90 $ pprint Nil dty}"
@@ -433,10 +443,10 @@ processData ns fc nm ty cons = do
             | (tm, _) => error (getFC tm) "expected \{nm} got \{render 90 $ pprint tnames tm}"
           when (hn /= QN ns nm) $ \ _ =>
             error (getFC codomain) "Constructor codomain is \{render 90 $ pprint tnames codomain} rather than \{nm}"
-          pure $ map (\ nm' => (MkEntry fc (QN ns nm') dty (DCon NormalCon (getArity dty) hn))) names
+          pure $ map (\ nm' => (MkEntry fc (QN ns nm') dty (DCon NormalCon (getArity dty) hn) Nil)) names
       decl => throwError $ E (getFC decl) "expected constructor declaration")
   let entries = populateConInfo entries
-  for entries $ \case (MkEntry name fc dty def) => setDef fc name dty def
+  for entries $ \case (MkEntry name fc dty def flags) => setDef fc name dty def flags
   let cnames = map (\x => x.name) entries
 
   log 1 $ \ _ => "setDef \{nm}  TCon \{show cnames}"
@@ -482,7 +492,7 @@ processRecord ns recordFC nm tele cname decls = do
       let pname = "." ++ name
       let lhs = foldl (\acc x => case the (BindInfo × Raw) x of (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc pname) tele
       let lhs = RApp recordFC lhs autoPat Explicit
-      let pdecl = Def fc pname ((lhs, (RVar fc name)) :: Nil)
+      let pdecl = FunDef fc pname ((lhs, (RVar fc name)) :: Nil)
       log 1 $ \ _ => "\{pname} : \{render 90 $ pretty funType}"
       log 1 $ \ _ => "\{render 90 $ pretty pdecl}"
       processDecl ns $ TypeSig fc (pname :: Nil) funType
@@ -494,7 +504,7 @@ processDecl ns (PMixFix _ _ _ _)  = pure MkUnit
 processDecl ns (TypeSig fc names tm) = processTypeSig ns fc names tm
 processDecl ns (PType fc nm ty) = processPrimType ns fc nm ty
 processDecl ns (PFunc fc nm used ty src) = processPrimFn ns fc nm used ty src
-processDecl ns (Def fc nm clauses) = processDef ns fc nm clauses
+processDecl ns (FunDef fc nm clauses) = processDef ns fc nm clauses
 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

src/Lib/Syntax.newt

@@ -107,7 +107,7 @@ Telescope = List (BindInfo × Raw)
 
 data Decl
   = TypeSig FC (List Name) Raw
-  | Def FC Name (List (Raw × Raw)) -- (List Clause)
+  | FunDef FC Name (List (Raw × Raw))
   | DCheck FC Raw Raw
   | Data FC Name Raw (List Decl)
   | ShortData FC Raw (List Raw)
@@ -121,7 +121,7 @@ data Decl
 
 instance HasFC Decl where
   getFC (TypeSig x strs tm) = x
-  getFC (Def x str xs) = x
+  getFC (FunDef x str xs) = x
   getFC (DCheck x tm tm1) = x
   getFC (Data x str tm xs) = x
   getFC (ShortData x _ _) = x
@@ -158,7 +158,7 @@ instance Show BindInfo where
 
 instance Show Decl where
   show (TypeSig _ str x) = foo ("TypeSig" :: show str :: show x :: Nil)
-  show (Def _ str clauses) = foo ("Def" :: show str :: show clauses :: Nil)
+  show (FunDef _ str clauses) = foo ("FunDef" :: show str :: show clauses :: Nil)
   show (Data _ str xs ys) = foo ("Data" :: show str :: show xs :: show ys :: Nil)
   show (DCheck _ x y) = foo ("DCheck" :: show x :: show y :: Nil)
   show (PType _ name ty) = foo ("PType" :: name :: show ty :: Nil)
@@ -267,7 +267,7 @@ pipeSep = folddoc (\a b => a <+/> text "|" <+> b)
 
 instance Pretty Decl where
   pretty (TypeSig _ nm ty) = spread (map text nm) <+> text ":" <+> nest 2 (pretty ty)
-  pretty (Def _ nm clauses) = stack $ map prettyPair clauses
+  pretty (FunDef _ nm clauses) = stack $ map prettyPair clauses
     where
       prettyPair : Raw × Raw → Doc
       prettyPair (a, b) = pretty a <+> text "=" <+> pretty b

src/Lib/TopContext.newt

@@ -47,25 +47,35 @@ emptyTop = do
   pure $ MkTop EmptyMap Nil Nil EmptyMap mcctx 0 errs EmptyMap
 
 
-setDef : QName -> FC -> Tm -> Def -> M Unit
+setFlag : QName → FC → EFlag → M Unit
-setDef name fc ty def = do
+setFlag name fc flag = do
   top <- getTop
-  let (Nothing) = lookupMap' name top.defs
+  let (Just (MkEntry fc nm ty def flags)) = lookupMap' name top.defs
-    | Just (MkEntry fc' nm' ty' def') => error fc "\{show name} is already defined at \{show fc'}"
+    | Nothing => error fc "\{show name} not declared"
   modifyTop $ \case
     MkTop mods imp ns defs metaCtx verbose errors ops =>
-      let defs = (updateMap name (MkEntry fc name ty def) top.defs) in
+      let defs = (updateMap name (MkEntry fc name ty def (flag :: flags)) defs) in
+      MkTop mods imp ns defs metaCtx verbose errors ops
+
+setDef : QName -> FC -> Tm -> Def → List EFlag -> M Unit
+setDef name fc ty def flags = do
+  top <- getTop
+  let (Nothing) = lookupMap' name top.defs
+    | Just (MkEntry fc' nm' ty' def' _) => error fc "\{show name} is already defined at \{show fc'}"
+  modifyTop $ \case
+    MkTop mods imp ns defs metaCtx verbose errors ops =>
+      let defs = (updateMap name (MkEntry fc name ty def flags) top.defs) in
       MkTop mods imp ns defs metaCtx verbose errors ops
 
 
 updateDef : QName -> FC -> Tm -> Def -> M Unit
 updateDef name fc ty def = do
   top <- getTop
-  let (Just (MkEntry fc' nm' ty' def')) = lookupMap' name top.defs
+  let (Just (MkEntry fc' nm' ty' def' flags)) = lookupMap' name top.defs
     | Nothing => error fc "\{show name} not declared"
   modifyTop $ \case
     MkTop mods imp ns defs metaCtx verbose errors ops =>
-      let defs = (updateMap name (MkEntry fc' name ty def) defs) in
+      let defs = (updateMap name (MkEntry fc' name ty def flags) defs) in
       MkTop mods imp ns defs metaCtx verbose errors ops
 
 addError : Error -> M Unit

src/Lib/Types.newt

@@ -328,17 +328,29 @@ instance Show Def where
 
 -- entry in the top level context
 
+data EFlag = Hint | Inline
+
+instance Show EFlag where
+  show Hint = "hint"
+  show Inline = "inline"
+
+instance Eq EFlag where
+  Hint == Hint = True
+  Inline == Inline = True
+  _ == _ = False
+
 record TopEntry where
   constructor MkEntry
   fc : FC
   name : QName
   type : Tm
   def : Def
+  eflags : List EFlag
 
 -- FIXME snoc
 
 instance Show TopEntry where
-  show (MkEntry fc name type def) = "\{show name} : \{show type} := \{show def}"
+  show (MkEntry fc name type def flags) = "\{show name} : \{show type} := \{show def} \{show flags}"
 
 record ModContext where
   constructor MkModCtx

src/Main.newt

@@ -32,7 +32,7 @@ jsonTopContext = do
   where
     jsonDef : TopEntry -> Json
     -- There is no FC here...
-    jsonDef (MkEntry fc (QN ns name) type def) = JsonObj
+    jsonDef (MkEntry fc (QN ns name) type def _) = JsonObj
       (  ("fc", toJson fc)
       :: ("name", toJson name)
       :: ("type", toJson (render 80 $ pprint Nil type) )

tests/TestMap.newt.golden

@@ -2,9 +2,9 @@
 []
 [(2, 3)]
 [(1, 3), (2, 0)]
-[(0, (MkUnit)), (1, (MkUnit)), (2, (MkUnit)), (3, (MkUnit)), (4, (MkUnit)), (5, (MkUnit)), (6, (MkUnit)), (7, (MkUnit)), (8, (MkUnit)), (9, (MkUnit)), (10, (MkUnit)), (11, (MkUnit)), (12, (MkUnit)), (13, (MkUnit)), (14, (MkUnit)), (16, (MkUnit)), (17, (MkUnit)), (20, (MkUnit))]
+[(0, "MkUnit"), (1, "MkUnit"), (2, "MkUnit"), (3, "MkUnit"), (4, "MkUnit"), (5, "MkUnit"), (6, "MkUnit"), (7, "MkUnit"), (8, "MkUnit"), (9, "MkUnit"), (10, "MkUnit"), (11, "MkUnit"), (12, "MkUnit"), (13, "MkUnit"), (14, "MkUnit"), (16, "MkUnit"), (17, "MkUnit"), (20, "MkUnit")]
-(Just _ (0, (MkUnit)))
+(Just _ (0, "MkUnit"))
-(Just _ (20, (MkUnit)))
+(Just _ (20, "MkUnit"))
 ohne 4
 [0, 1, 2, 3, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 17, 20]
 ohne 1