fixes and changes for porting

- forward declaration of records
- fixes to projections
- drop record accessors (use projections instead)
- changes to names to disambiguate

TODO.md

@@ -3,6 +3,7 @@
 
 More comments in code! This is getting big enough that I need to re-find my bearings when fixing stuff.
 
+- [ ] report info in case of error
 - [x] tokenizer that can be ported to newt
 - [ ] Add default path for library, so we don't need symlinks everywhere and can write tests for the library
 - [ ] string interpolation?

aoc2023/Aoc.newt

@@ -9,19 +9,6 @@ nums' by s = map stringToInt $ filter (_/=_ "") $ split (trim s) by
 nums : String → List Int
 nums s = map stringToInt $ filter (_/=_ "") $ split (trim s) " "
 
-isDigit : Char -> Bool
-isDigit '0' = True
-isDigit '1' = True
-isDigit '2' = True
-isDigit '3' = True
-isDigit '4' = True
-isDigit '5' = True
-isDigit '6' = True
-isDigit '7' = True
-isDigit '8' = True
-isDigit '9' = True
-isDigit _ = False
-
 indexOf? : ∀ a. {{Eq a}} → a → List a → Maybe Nat
 indexOf? {a} z xs = go Z z xs
   where

newt-vscode/syntaxes/newt.tmLanguage.json

@@ -22,18 +22,15 @@
       "name": "string.js",
       "begin": "`",
       "end": "`",
-      "patterns": [
+      "patterns": [{ "include": "source.js" }]
-        { "include": "source.js" }
-      ]
     },
     {
-      "name": "string.newt",
+      "name": "string.single.newt",
       "match": "'(.|\\\\.)'"
     },
     {
-      "name": "string.newt",
+      "name": "string.double.newt",
-      "begin": "\"",
+      "match": "\"(.|\\\\.)\""
-      "end": "\""
     }
   ]
 }

newt/Prelude.newt

@@ -50,6 +50,10 @@ fromMaybe : ∀ a. a → Maybe a → a
 fromMaybe a Nothing = a
 fromMaybe _ (Just a) = a
 
+maybe : ∀ a b. b → (a → b) → Maybe a → b
+maybe def f (Just a) = f a
+maybe def f Nothing = def
+
 data Either a b = Left a | Right b
 
 infixr 7 _::_
@@ -163,6 +167,10 @@ const a b = a
 _<*_ : ∀ f a b. {{Applicative f}} → f a → f b → f a
 fa <* fb = return const <*> fa <*> fb
 
+_*>_ : ∀ f a b. {{Functor f}} {{Applicative f}} → f a → f b → f b
+a *> b = map (const id) a <*> b
+
+
 class Traversable (t : U → U) where
   traverse : ∀ f a b. {{Applicative f}} → (a → f b) → t a → f (t b)
 
@@ -772,6 +780,9 @@ snoc xs x = xs ++ (x :: Nil)
 instance ∀ a b. {{Show a}} {{Show b}} → Show (a × b) where
   show (a,b) = "(" ++ show a ++ "," ++ show b ++ ")"
 
+instance ∀ a. {{Show a}} → Show (List a) where
+  show xs = joinBy ", " $ map show xs
+
 -- For now, I'm not having the compiler do this automatically
 
 Lazy : U → U
@@ -783,3 +794,39 @@ force f = f MkUnit
 -- unlike Idris, user will have to write \ _ => ...
 when : ∀ f. {{Applicative f}} → Bool → Lazy (f Unit) → f Unit
 when b fa = if b then force fa else return MkUnit
+
+instance ∀ a. {{Ord a}} → Ord (List a) where
+  compare Nil Nil = EQ
+  compare Nil ys = LT
+  compare xs Nil = GT
+  compare (x :: xs) (y :: ys) = case compare x y of
+    EQ => compare xs ys
+    c => c
+
+isSpace : Char -> Bool
+isSpace ' '    = True
+isSpace '\n'   = True
+isSpace _      = False
+
+isDigit : Char -> Bool
+isDigit '0' = True
+isDigit '1' = True
+isDigit '2' = True
+isDigit '3' = True
+isDigit '4' = True
+isDigit '5' = True
+isDigit '6' = True
+isDigit '7' = True
+isDigit '8' = True
+isDigit '9' = True
+isDigit _ = False
+
+isUpper : Char → Bool
+isUpper c = let o = ord c in 64 < o && o < 91
+
+ignore : ∀ f a. {{Functor f}} → f a → f Unit
+ignore = map (const MkUnit)
+
+instance ∀ a. {{Show a}} → Show (Maybe a) where
+  show Nothing = "Nothing"
+  show (Just a) = "Just {show a}"

port/Prettier.newt

@@ -1,155 +0,0 @@
--- A prettier printer, Philip Wadler
--- https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf
-module Prettier
-
-import Prelude
-
--- `Doc` is a pretty printing document.  Constructors are private, use
--- methods below.  `Alt` in particular has some invariants on it, see paper
--- for details. (Something along the lines of "the first line of left is not
--- bigger than the first line of the right".)
-
-
--- data Doc = Empty | Line | Text String | Nest Nat Doc | Seq Doc Doc | Alt Doc Doc
-data Doc : U where
-  Empty Line : Doc
-  Text : String -> Doc
-  Nest : Int -> Doc -> Doc
-  Seq : Doc -> Doc -> Doc
-  Alt : Doc -> Doc -> Doc
-
-
--- The original paper had a List-like structure Doc (the above was DOC) which
--- had Empty and a tail on Text and Line.
--- data Item = TEXT String | LINE Nat
-data Item : U where
-  TEXT :  String -> Item
-  LINE : Int -> Item
-
-empty : Doc
-empty = Empty
-
-flatten : Doc -> Doc
-flatten Empty = Empty
-flatten (Seq x y) = Seq (flatten x) (flatten y)
-flatten (Nest i x) = flatten x
-flatten Line = Text " "
-flatten (Text str) = Text str
-flatten (Alt x y) = flatten x
-
-group : Doc -> Doc
-group x = Alt (flatten x) x
-
--- TODO - we can accumulate snoc and cat all at once
-layout : List Item -> SnocList String -> String
-layout Nil acc = fastConcat $ acc <>> Nil
-layout (LINE k :: x) acc = layout x (acc :< "\n" :< replicate (cast k) ' ')
-layout (TEXT str :: x) acc = layout x (acc :< str)
-
--- Whether a documents first line fits.
-fits : Int -> List Item -> Bool
-fits 0 x = False
-fits w ((TEXT s) :: xs) = fits (w - slen s) xs
-fits w _ = True
-
--- vs Wadler, we're collecting the left side as a SnocList to prevent
--- blowing out the stack on the Text case.  The original had DOC as
--- a Linked-List like structure (now List Item)
-
--- I've now added a `fit` boolean to indicate if we should cut when we hit the line length
--- Wadler was relying on laziness to stop the first branch before LINE if necessary
-be : Bool -> SnocList Item -> Int -> Int -> List (Int × Doc) -> Maybe (List Item)
-be fit acc w k Nil = Just (acc <>> Nil)
-be fit acc w k ((i, Empty) :: xs) = be fit acc w k xs
-be fit acc w k ((i, Line) :: xs) = (be False (acc :< LINE i) w i xs)
-be fit acc w k ((i, (Text s)) :: xs) =
-  case not fit || (k + slen s < w) of
-    True => (be fit (acc :< TEXT s) w (k + slen s) xs)
-    False => Nothing
-be fit acc w k ((i, (Nest j x)) :: xs) = be fit acc w k ((i + j, x):: xs)
-be fit acc w k ((i, (Seq x y)) :: xs) = be fit acc w k ((i,x) :: (i,y) :: xs)
-be fit acc w k ((i, (Alt x y)) :: xs) =
-  (_<>>_ acc) <$> (be True Lin w k ((i,x) :: xs) <|> be fit Lin w k ((i, y) :: xs))
-
-best : Int -> Int -> Doc -> List Item
-best w k x = fromMaybe Nil $ be False Lin w k ((0,x) :: Nil)
-
--- interface Pretty a where
---   pretty : a -> Doc
-
-data Pretty : U -> U where
-  MkPretty : {a} → (a → Doc) → Pretty a
-
-pretty : {a} {{Pretty a}} → a → Doc
-pretty {{MkPretty p}} x = p x
-
-render : Int -> Doc -> String
-render w x = layout (best w 0 x) Lin
-
-instance Semigroup Doc where
-  x <+> y = Seq x (Seq (Text " ") y)
-
--- Match System.File so we don't get warnings
-
-line : Doc
-line = Line
-
-text : String -> Doc
-text = Text
-
-nest : Int -> Doc -> Doc
-nest = Nest
-
-instance Concat Doc where
-  x ++ y = Seq x y
-
-infixl 5 _</>_
-_</>_ : Doc -> Doc -> Doc
-x </> y = x ++ line ++ y
-
--- fold, but doesn't emit extra nil
-folddoc : (Doc -> Doc -> Doc) -> List Doc -> Doc
-folddoc f Nil = Empty
-folddoc f (x :: Nil) = x
-folddoc f (x :: xs) = f x (folddoc f xs)
-
--- separate with space
-spread : List Doc -> Doc
-spread = folddoc _<+>_
-
--- separate with new lines
-stack : List Doc -> Doc
-stack = folddoc _</>_
-
--- bracket x with l and r, indenting contents on new line
-bracket : String -> Doc -> String -> Doc
-bracket l x r = group (text l ++ nest 2 (line ++ x) ++ line ++ text r)
-
-infixl 5 _<+/>_
-
--- Either space or newline
-
-_<+/>_ : Doc -> Doc -> Doc
-x <+/> y = x ++ Alt (text " ") line ++ y
-
--- Reformat some docs to fill. Not sure if I want this precise behavior or not.
-fill : List Doc -> Doc
-fill Nil = Empty
-fill (x :: Nil) = x
-fill (x :: y :: xs) = Alt (flatten x <+> fill (flatten y :: xs)) (x </> fill (y :: xs))
-
--- separate with comma
-commaSep : List Doc -> Doc
-commaSep = folddoc (\a b => a ++ text "," <+/> b)
-
-/-
-
-FromString Doc where
-  fromString = text
-
--- If we stick Doc into a String, try to avoid line-breaks via `flatten`
-
-Interpolation Doc where
-  interpolate = render 80 . flatten
-
--/

port/TestPrettier.newt

@@ -1,20 +0,0 @@
-module TestPrettier
-
-import Prettier
-
-five : Nat
-five = S (S (S (S (S Z))))
-
-fifty : Nat
-fifty = five * five * S (S Z)
-
-doc : Doc
-doc = text "x" <+> text "+" <+> text "y"
-
-foo : String
-foo = render fifty doc
-
-main : IO Unit
-main = do
-  putStrLn foo
-  putStrLn $ replicate five 'x'

scripts/translate.sh

@@ -11,16 +11,22 @@ find src -type f -name '*.idr' | while read -r file; do
   if [[ ! -f "$output_file" ]]; then
     echo "$file -> $output_file"
     perl -pe '
+      use strict;
+
       s/^%.*//;
       s/\bType\b/U/g;
       s/\binterface\b/class/g;
       s/import public/import/g;
-      s/^\s*covering//g;
+      s/\[\]/Nil/g;
+      s{\[([^<].*?)\]}{"(" . (join " ::", split /,/, $1) . " :: Nil)"}ge;
+      s/\bsym\b/symbol/g;
       s/^export//g;
+      s/^\s*covering//g;
       s/pure \(\)/pure MkUnit/;
       s/M \(\)/M Unit/;
       s/Parser \(\)/Parser Unit/;
       s/OK \(\)/OK MkUnit/;
+      s/ifThenElse/ite/;
       s/toks,\s*com,\s*ops,\s*col/toks com ops col/;
       s/\bNat\b/Int/g;
       s/(\s+when [^\$]+\$)(.*)/\1 \\ _ =>\2/;
@@ -30,16 +36,17 @@ find src -type f -name '*.idr' | while read -r file; do
       # maybe break down an add the sugar?
       # patterns would be another option, but
       # we would need to handle overlapping ones
-      s/\[\]/Nil/g;
+
       s/ \. / ∘ /g;
       s/\(([<>\/+]+)\)/_\1_/g;
       s/\{-/\/-/g;
       s/-\}/-\//g;
       s/\[<\]/Lin/g;
       s/\[<([^\],]+)\]/(Lin :< \1)/g;
-      s/\[([^\],]+)\]/(\1 :: Nil)/g;
+      # s/\[([^\],]+)\]/(\1 :: Nil)/g;
       s/^([A-Z].*where)/instance \1/g;
       s/^data (.*:\s*\w+)$/\1/g;
     ' "$file" > "$output_file"
   fi
 done
+rsync -av done/ port

src/Lib/Elab.idr

@@ -97,9 +97,9 @@ export
 updateMeta : Nat -> (MetaEntry -> M MetaEntry) -> M ()
 updateMeta ix f = do
   top <- get
-  mc <- readIORef top.metas
+  mc <- readIORef top.metaCtx
   metas <- go mc.metas
-  writeIORef top.metas $ {metas := metas} mc
+  writeIORef top.metaCtx $ {metas := metas} mc
   where
     go : List MetaEntry -> M (List MetaEntry)
     go [] = error' "Meta \{show ix} not found"
@@ -110,7 +110,7 @@ export
 addConstraint : Env -> Nat -> SnocList Val -> Val -> M ()
 addConstraint env ix sp tm = do
   top <- get
-  mc <- readIORef top.metas
+  mc <- readIORef top.metaCtx
   updateMeta ix $ \case
     (Unsolved pos k a b c cons) => do
       debug "Add constraint m\{show ix} \{show sp} =?= \{show tm}"
@@ -605,7 +605,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
         clauses <- mapMaybe id <$> traverse (rewriteClause sctynm vars) prob.clauses
         debug "and now:"
         for_ clauses $ (\x => debug "    \{show x}")
-        when (length clauses == 0) $ error ctx.fc "Missing case for \{dcName} splitting \{scnm}"
+        when (length clauses == 0) $ error ctx.ctxFC "Missing case for \{dcName} splitting \{scnm}"
         tm <- buildTree ctx' (MkProb clauses prob.ty)
         pure $ Just $ CaseCons dcName (map getName vars) tm
 
@@ -617,9 +617,9 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
 
         -- Constrain the scrutinee's variable to be dcon applied to args
         let Just x = findIndex ((==scnm) . fst) ctx'.types
-          | Nothing => error ctx.fc "\{scnm} not is scope?"
+          | Nothing => error ctx.ctxFC "\{scnm} not is scope?"
         let lvl = lvl2ix (length ctx'.env) (cast x)
-        let scon : (Nat, Val) = (lvl, VRef ctx.fc dcName (DCon arity dcName) sc)
+        let scon : (Nat, Val) = (lvl, VRef ctx.ctxFC dcName (DCon arity dcName) sc)
 
         debug "scty \{show scty}"
         debug "UNIFY results \{show res.constraints}"
@@ -643,7 +643,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
         clauses <- mapMaybe id <$> traverse (rewriteClause sctynm vars) prob.clauses
         debug "and now:"
         for_ clauses $ (\x => debug "    \{show x}")
-        when (length clauses == 0) $ error ctx.fc "Missing case for \{dcName} splitting \{scnm}"
+        when (length clauses == 0) $ error ctx.ctxFC "Missing case for \{dcName} splitting \{scnm}"
         tm <- buildTree ctx' (MkProb clauses prob.ty)
         pure $ Just $ CaseCons dcName (map getName vars) tm
   where
@@ -667,15 +667,15 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
     makeConstr : List Bind -> List Pattern -> M (List (String, Pattern))
     makeConstr [] [] = pure $ []
     -- would need M in here to throw, and I'm building stuff as I go, I suppose I could <$>
-    makeConstr [] (pat :: pats) = error ctx.fc "too many patterns"
+    makeConstr [] (pat :: pats) = error ctx.ctxFC "too many patterns"
     makeConstr ((MkBind nm Implicit x) :: xs) [] = pure $ (nm, PatWild emptyFC Implicit) :: !(makeConstr xs [])
     makeConstr ((MkBind nm Auto x) :: xs) [] = pure $ (nm, PatWild emptyFC Auto) :: !(makeConstr xs [])
     -- FIXME need a proper error, but requires wiring M three levels down
-    makeConstr ((MkBind nm Explicit x) :: xs) [] = error ctx.fc "not enough patterns"
+    makeConstr ((MkBind nm Explicit x) :: xs) [] = error ctx.ctxFC "not enough patterns"
     makeConstr ((MkBind nm Explicit x) :: xs) (pat :: pats) =
       if getIcit pat == Explicit
         then pure $ (nm, pat) :: !(makeConstr xs pats)
-        else error ctx.fc "mismatch between Explicit and \{show $ getIcit pat}"
+        else error ctx.ctxFC "mismatch between Explicit and \{show $ getIcit pat}"
     makeConstr ((MkBind nm icit x) :: xs) (pat :: pats) =
       if getIcit pat /= icit -- Implicit/Explicit Implicit/Auto, etc
         then pure $ (nm, PatWild (getFC pat) icit) :: !(makeConstr xs (pat :: pats))
@@ -778,7 +778,7 @@ checkWhere ctx decls body ty = do
   -- context could hold a Name -> Val (not Tm because levels) to help with that
   -- e.g. "go" -> (VApp ... (VApp (VRef "ns.go") ...)
   -- But I'll attempt letrec first
-  tm <- buildTree ({ fc := defFC} ctx') (MkProb clauses' vty)
+  tm <- buildTree ({ ctxFC := defFC} ctx') (MkProb clauses' vty)
   vtm <- eval ctx'.env CBN tm
   -- Should we run the rest with the definition in place?
   -- I'm wondering if switching from bind to define will mess with metas
@@ -845,13 +845,13 @@ buildLitCase ctx prob fc scnm scty lit = do
 
   -- Constrain the scrutinee's variable to be lit value
   let Just ix = findIndex ((==scnm) . fst) ctx.types
-    | Nothing => error ctx.fc "\{scnm} not is scope?"
+    | Nothing => error ctx.ctxFC "\{scnm} not is scope?"
   let lvl = lvl2ix (length ctx.env) (cast ix)
   let scon : (Nat, Val) = (lvl, VLit fc lit)
   ctx' <- updateContext ctx [scon]
   let clauses = mapMaybe rewriteClause prob.clauses
 
-  when (length clauses == 0) $ error ctx.fc "Missing case for \{show lit} splitting \{scnm}"
+  when (length clauses == 0) $ error ctx.ctxFC "Missing case for \{show lit} splitting \{scnm}"
   tm <- buildTree ctx' (MkProb clauses prob.ty)
   pure $ CaseLit lit tm
 

src/Lib/Erasure.idr

@@ -5,6 +5,8 @@ import Data.Maybe
 import Data.SnocList
 import Lib.TopContext
 
+public export
+EEnv : Type
 EEnv = List (String, Quant, Maybe Tm)
 
 -- TODO look into removing Nothing below, can we recover all of the types?
@@ -16,7 +18,7 @@ getType : Tm -> M (Maybe Tm)
 getType (Ref fc nm x) = do
   top <- get
   case lookup nm top of
-    Nothing => error fc "\{nm} not in scope"
+    Nothing => error fc "\{show nm} not in scope"
     (Just (MkEntry _ name type def)) => pure $ Just type
 getType tm = pure Nothing
 
@@ -44,8 +46,8 @@ doAlt : EEnv -> CaseAlt -> M CaseAlt
 doAlt env (CaseDefault t) = CaseDefault <$> erase env t []
 doAlt env (CaseCons name args t) = do
   top <- get
-  let Just (MkEntry _ str type def) = lookup name top
+  let (Just (MkEntry _ str type def)) = lookup name top
-    | _ => error emptyFC "\{name} dcon missing from context"
+    | _ => error emptyFC "\{show name} dcon missing from context"
   let env' = piEnv env type args
   CaseCons name args <$> erase env' t []
   where

src/Lib/Parser.idr

@@ -7,12 +7,14 @@ import Lib.Syntax
 import Lib.Token
 import Lib.Types
 
+ident : Parser String
 ident = token Ident <|> token MixFix
 
+uident : Parser String
 uident = token UIdent
 
-parens : Parser a -> Parser a
+parenWrap : Parser a -> Parser a
-parens pa = do
+parenWrap pa = do
   sym "("
   t <- pa
   sym ")"
@@ -53,7 +55,7 @@ interp = token StartInterp *> term <* token EndInterp
 
 interpString : Parser Raw
 interpString = do
-  fc <- getPos
+  -- fc <- getPos
   ignore $ token StartQuote
   part <- term
   parts <- many (stringLit <|> interp)
@@ -63,7 +65,7 @@ interpString = do
     append : Raw -> Raw -> Raw
     append t u =
       let fc = getFC t in
-      (RApp fc (RApp fc (RVar fc "_++_") t Explicit) u Explicit)
+      (RApp (getFC t) (RApp fc (RVar fc "_++_") t Explicit) u Explicit)
 
 intLit : Parser Raw
 intLit = do
@@ -91,7 +93,7 @@ asAtom : Parser Raw
 asAtom = do
   fc <- getPos
   nm <- ident
-  asPat <- optional $ keyword "@" *> parens typeExpr
+  asPat <- optional $ keyword "@" *> parenWrap typeExpr
   case asPat of
     Just exp => pure $ RAs fc nm exp
     Nothing  => pure $ RVar fc nm
@@ -106,7 +108,7 @@ atom = RU <$> getPos <* keyword "U"
     <|> lit
     <|> RImplicit <$> getPos <* keyword "_"
     <|> RHole <$> getPos <* keyword "?"
-    <|> parens typeExpr
+    <|> parenWrap typeExpr
 
 -- Argument to a Spine
 pArg : Parser (Icit,FC,Raw)
@@ -121,6 +123,7 @@ AppSpine = List (Icit,FC,Raw)
 pratt : Operators -> Int -> String -> Raw -> AppSpine -> Parser (Raw, AppSpine)
 pratt ops prec stop left spine = do
   (left, spine) <- runPrefix stop left spine
+  let (left, spine) = projectHead left spine
   let spine = runProject spine
   case spine of
     [] => pure (left, [])
@@ -138,6 +141,14 @@ pratt ops prec stop left spine = do
             else pratt ops prec stop (RApp (getFC left) left tm Explicit) rest
     ((icit, fc, tm) :: rest) => pratt ops prec stop (RApp (getFC left) left tm icit) rest
   where
+    projectHead : Raw -> AppSpine -> (Raw, AppSpine)
+    projectHead t sp@((Explicit, fc', RVar fc nm) :: rest) =
+      if isPrefixOf "." nm
+        then projectHead (RApp fc (RVar fc nm) t Explicit) rest
+        else (t,sp)
+    projectHead t sp = (t, sp)
+
+    -- we need to check left/AppSpine first
     -- we have a case above for when the next token is a projection, but
     -- we need this to make projection bind tighter than app
     runProject : AppSpine -> AppSpine
@@ -176,9 +187,12 @@ pratt ops prec stop left spine = do
            -- TODO False should be an error here
          Just (MkOp name p fix True rule) => do
             runRule p fix stop rule (RVar fc name) spine
-         _ => pure (left, spine)
+         _ =>
+          pure (left, spine)
     runPrefix stop left spine = pure (left, spine)
 
+
+
 parseOp : Parser Raw
 parseOp = do
   fc <- getPos
@@ -215,7 +229,7 @@ letExpr = do
 pLamArg : Parser (Icit, String, Maybe Raw)
 pLamArg = (Implicit,,) <$> braces (ident <|> uident) <*> optional (sym ":" >> typeExpr)
        <|> (Auto,,) <$> dbraces (ident <|> uident) <*> optional (sym ":" >> typeExpr)
-       <|> (Explicit,,) <$> parens (ident <|> uident) <*> optional (sym ":" >> typeExpr)
+       <|> (Explicit,,) <$> parenWrap (ident <|> uident) <*> optional (sym ":" >> typeExpr)
        <|> (Explicit,,Nothing) <$> (ident <|> uident)
        <|> (Explicit,"_",Nothing) <$ keyword "_"
 
@@ -473,7 +487,7 @@ parsePFunc = do
   fc <- getPos
   keyword "pfunc"
   nm <- ident
-  uses <- optional (keyword "uses" >> parens (many $ uident <|> ident <|> token MixFix))
+  uses <- optional (keyword "uses" >> parenWrap (many $ uident <|> ident <|> token MixFix))
   keyword ":"
   ty <- typeExpr
   keyword ":="
@@ -536,9 +550,11 @@ parseInstance = do
   fc <- getPos
   keyword "instance"
   ty <- typeExpr
-  keyword "where"
+  -- is it a forward declaration
+  (Just _) <- optional $ keyword "where"
+    | _ => pure $ Instance fc ty Nothing
   decls <- startBlock $ manySame $ parseDef
-  pure $ Instance fc ty decls
+  pure $ Instance fc ty (Just decls)
 
 -- Not sure what I want here.
 -- I can't get a Tm without a type, and then we're covered by the other stuff

src/Lib/Parser/Impl.idr

@@ -107,7 +107,7 @@ Applicative Parser where
 
 -- Second argument lazy so we don't have circular refs when defining parsers.
 export
-(<|>) : Parser a -> Lazy (Parser a) -> Parser a
+(<|>) : Parser a -> (Parser a) -> Parser a
 (P pa) <|> (P pb) = P $ \toks,com,ops,col =>
   case pa toks False ops col of
     OK a toks' _ ops => OK a toks' com ops
@@ -133,12 +133,11 @@ export
 commit : Parser ()
 commit = P $ \toks,com,ops,col => OK () toks True ops
 
-mutual
-  export some : Parser a -> Parser (List a)
-  some p = (::) <$> p <*> many p
 
-  export many : Parser a -> Parser (List a)
+export some : Parser a -> Parser (List a)
-  many p = some p <|> pure []
+export many : Parser a -> Parser (List a)
+some p = (::) <$> p <*> many p
+many p = some p <|> pure []
 
 -- one or more `a` seperated by `s`
 export
@@ -149,7 +148,7 @@ export
 getPos : Parser FC
 getPos = P $ \toks, com, ops, indent => case toks of
   [] => OK emptyFC toks com ops
-  (t :: ts) => OK (MkFC indent.file (start t)) toks com ops
+  (t :: ts) => OK (MkFC indent.file (getStart t)) toks com ops
 
 ||| Start an indented block and run parser in it
 export
@@ -158,7 +157,7 @@ startBlock (P p) = P $ \toks,com,ops,indent => case toks of
   [] => p toks com ops indent
   (t :: _) =>
     -- If next token is at or before the current level, we've got an empty block
-    let (tl,tc) = start t in
+    let (tl,tc) = getStart t in
     let (MkFC file (line,col)) = indent in
     p toks com ops (MkFC file (tl, ifThenElse (tc <= col) (col + 1) tc))
 
@@ -166,12 +165,12 @@ startBlock (P p) = P $ \toks,com,ops,indent => case toks of
 ||| checking column and then updating line to match the current
 export
 sameLevel : Parser a -> Parser a
-sameLevel (P p) = P $ \toks,com,ops,indent => case toks of
+sameLevel (P p) = P $ \toks, com, ops, indent => case toks of
   [] => p toks com ops indent
   (t :: _) =>
-    let (tl,tc) = start t
+    let (tl,tc) = getStart t in
-        (MkFC file (line,col)) = indent
+    let (MkFC file (line,col)) = indent in
-    in if tc == col then p toks com ops ({start := (tl, col)} indent)
+    if tc == col then p toks com ops (MkFC file (tl, col))
     else if col < tc then Fail False (error file toks "unexpected indent") toks com ops
     else Fail False (error file toks "unexpected indent") toks com ops
 
@@ -189,7 +188,7 @@ indented : Parser a -> Parser a
 indented (P p) = P $ \toks,com,ops,indent => case toks of
   [] => p toks com ops indent
   (t::_) =>
-    let (tl,tc) = start t
+    let (tl,tc) = getStart t
     in if tc > fcCol indent || tl == fcLine indent then p toks com ops indent
     else Fail False (error (file indent) toks "unexpected outdent") toks com ops
 

src/Lib/Prettier.idr

@@ -34,14 +34,13 @@ group x = Alt (flatten x) x
 
 -- TODO - we can accumulate snoc and cat all at once
 layout : List Item -> SnocList String -> String
-layout [] acc = fastConcat $ cast acc
+layout [] acc = fastConcat $ acc <>> []
 layout (LINE k :: x) acc = layout x (acc :< "\n" :< replicate k ' ')
 layout (TEXT str :: x) acc = layout x (acc :< str)
 
 ||| Whether a documents first line fits.
 fits : Nat -> List Item -> Bool
-fits 0 x = False
+fits w ((TEXT s) :: xs) = if length s < w then fits (w `minus` length s) xs else False
-fits w ((TEXT s) :: xs) = fits (w `minus` length s) xs
 fits w _ = True
 
 -- vs Wadler, we're collecting the left side as a SnocList to prevent

src/Lib/ProcessDecl.idr

@@ -35,7 +35,7 @@ findMatches ctx ty ((MkEntry _ name type def) :: xs) = do
   -- let ctx = mkCtx (getFC ty)
   -- FIXME we're restoring state, but the INFO logs have already been emitted
   -- Also redo this whole thing to run during elab, recheck constraints, etc.
-  mc <- readIORef top.metas
+  mc <- readIORef top.metaCtx
   catchError(do
       -- TODO sort out the FC here
       let fc = getFC ty
@@ -46,12 +46,12 @@ findMatches ctx ty ((MkEntry _ name type def) :: xs) = do
       let (QN ns nm) = name
       tm <- check ctx (RVar fc nm) ty
       debug "Found \{pprint [] tm} for \{show ty}"
-      mc' <- readIORef top.metas
+      mc' <- readIORef top.metaCtx
-      writeIORef top.metas mc
+      writeIORef top.metaCtx mc
       ((tm, mc') ::) <$> findMatches ctx ty xs)
     (\ err => do
       debug "No match \{show ty} \{pprint [] type} \{showError "" err}"
-      writeIORef top.metas mc
+      writeIORef top.metaCtx mc
       findMatches ctx ty xs)
 
 contextMatches : Context -> Val -> M (List (Tm, MetaContext))
@@ -63,17 +63,17 @@ contextMatches ctx ty = go (zip ctx.env (toList ctx.types))
       type <- quote ctx.lvl vty
       let True = isCandidate ty type | False => go xs
       top <- get
-      mc <- readIORef top.metas
+      mc <- readIORef top.metaCtx
       catchError(do
           debug "TRY context \{nm} : \{pprint (names ctx) type} for \{show ty}"
           unifyCatch (getFC ty) ctx ty vty
-          mc' <- readIORef top.metas
+          mc' <- readIORef top.metaCtx
-          writeIORef top.metas mc
+          writeIORef top.metaCtx mc
           tm <- quote ctx.lvl tm
           ((tm, mc') ::) <$> go xs)
         (\ err => do
           debug "No match \{show ty} \{pprint (names ctx) type} \{showError "" err}"
-          writeIORef top.metas mc
+          writeIORef top.metaCtx mc
           go xs)
 
 -- FIXME - decide if we want to count Zero here
@@ -110,12 +110,12 @@ solveAutos mstart ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
         | res => do
           debug "FAILED to solve \{show ty}, matches: \{commaSep $ map (pprint [] . fst) res}"
           solveAutos mstart es
-      writeIORef top.metas mc
+      writeIORef top.metaCtx mc
       val <- eval ctx.env CBN tm
       debug "SOLUTION \{pprint [] tm} evaled to \{show val}"
       let sp = makeSpine ctx.lvl ctx.bds
       solve ctx.env k sp val
-      mc <- readIORef top.metas
+      mc <- readIORef top.metaCtx
       let mlen = length mc.metas `minus` mstart
       solveAutos mstart (take mlen mc.metas)
 solveAutos mstart (_ :: es) = solveAutos mstart es
@@ -140,7 +140,7 @@ logMetas : Nat -> M ()
 logMetas mstart = do
   -- FIXME, now this isn't logged for Sig / Data.
   top <- get
-  mc <- readIORef top.metas
+  mc <- readIORef top.metaCtx
   let mlen = length mc.metas `minus` mstart
   for_ (reverse $ take mlen mc.metas) $ \case
     (Solved fc k soln) => do
@@ -205,7 +205,7 @@ processDecl ns  (TypeSig fc names tm) = do
   putStrLn "-----"
 
   top <- get
-  mc <- readIORef top.metas
+  mc <- readIORef top.metaCtx
   let mstart = length mc.metas
   for_ names $ \nm => do
     let Nothing := lookupRaw nm top
@@ -238,7 +238,7 @@ processDecl ns (Def fc nm clauses) = do
   putStrLn "-----"
   putStrLn "Def \{show nm}"
   top <- get
-  mc <- readIORef top.metas
+  mc <- readIORef top.metaCtx
   let mstart = length mc.metas
   let Just entry = lookupRaw nm top
     | Nothing => throwError $ E fc "No declaration for \{nm}"
@@ -256,7 +256,7 @@ processDecl ns (Def fc nm clauses) = do
   tm <- buildTree (mkCtx fc) (MkProb clauses' vty)
   -- putStrLn "Ok \{pprint [] tm}"
 
-  mc <- readIORef top.metas
+  mc <- readIORef top.metaCtx
   let mlen = length mc.metas `minus` mstart
   solveAutos mstart (take mlen mc.metas)
   -- TODO - make nf that expands all metas and drop zonk
@@ -323,7 +323,7 @@ processDecl ns (Class classFC nm tele decls) = do
 
 
 processDecl ns (Instance instfc ty decls) = do
-  let decls = collectDecl decls
+
   putStrLn "-----"
   putStrLn "Instance \{pretty ty}"
   top <- get
@@ -342,6 +342,16 @@ processDecl ns (Instance instfc ty decls) = do
   -- or use "Monad\{show $ length defs}"
   let instname = interpolate $ pprint [] codomain
   let sigDecl = TypeSig instfc [instname] ty
+  -- 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
+    Just _ => pure MkUnit -- TODO check that the types match
+    Nothing => processDecl ns sigDecl
+
+  let (Just decls) = collectDecl <$> decls
+    | _ => do
+      debug "Forward declaration \{show sigDecl}"
 
   let (Ref _ tconName _, args) := funArgs codomain
     | (tm, _) => error tyFC "\{pprint [] codomain} doesn't appear to be a TCon application"
@@ -378,10 +388,7 @@ processDecl ns (Instance instfc ty decls) = do
        putStrLn $ render 80 $ pretty decl
        pure $ Just decl
      _ => pure Nothing
-  -- 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
-  processDecl ns sigDecl
   for_ (mapMaybe id defs) $ \decl => do
     -- debug because already printed above, but nice to have it near processing
     debug $ render 80 $ pretty decl
@@ -442,7 +449,7 @@ processDecl ns (Data fc nm ty cons) = do
   putStrLn "-----"
   putStrLn "Data \{nm}"
   top <- get
-  mc <- readIORef top.metas
+  mc <- readIORef top.metaCtx
   tyty <- check (mkCtx fc) ty (VU fc)
   case lookupRaw nm top of
     Just (MkEntry _ name type Axiom) => do
@@ -502,13 +509,13 @@ processDecl ns (Record recordFC nm tele cname decls) = do
     let autoPat = foldl (\acc, (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar recordFC dcName) fields
 
     -- `fieldName` - consider dropping to keep namespace clean
-    let lhs = foldl (\acc, (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele
+    -- let lhs = foldl (\acc, (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele
-    let lhs = RApp recordFC lhs autoPat Explicit
+    -- let lhs = RApp recordFC lhs autoPat Explicit
-    let decl = Def fc name [(lhs, (RVar fc name))]
+    -- let decl = Def fc name [(lhs, (RVar fc name))]
-    putStrLn "\{name} : \{pretty funType}"
+    -- putStrLn "\{name} : \{pretty funType}"
-    putStrLn "\{pretty decl}"
+    -- putStrLn "\{pretty decl}"
-    processDecl ns $ TypeSig fc [name] funType
+    -- processDecl ns $ TypeSig fc [name] funType
-    processDecl ns decl
+    -- processDecl ns decl
 
     -- `.fieldName`
     let pname = "." ++ name

src/Lib/Syntax.idr

@@ -40,7 +40,7 @@ Constraint = (String, Pattern)
 public export
 record Clause where
   constructor MkClause
-  fc : FC
+  clauseFC : FC
   -- I'm including the type of the left, so we can check pats and get the list of possibilities
   -- But maybe rethink what happens on the left.
   -- It's a VVar k or possibly a pattern.
@@ -60,7 +60,7 @@ public export
 data DoStmt : Type where
   DoExpr : (fc : FC) -> Raw -> DoStmt
   DoLet : (fc : FC) -> String -> Raw -> DoStmt
-  DoArrow : (fc: FC) -> Raw -> Raw -> List RCaseAlt -> DoStmt
+  DoArrow : (fc : FC) -> Raw -> Raw -> List RCaseAlt -> DoStmt
 
 data Decl : Type
 data Raw : Type where
@@ -125,7 +125,7 @@ data Decl
   | PFunc FC Name (List String) Raw String
   | PMixFix FC (List Name) Nat Fixity
   | Class FC Name Telescope (List Decl)
-  | Instance FC Raw (List Decl)
+  | Instance FC Raw (Maybe (List Decl))
   | Record FC Name Telescope (Maybe Name) (List Decl)
 
 public export
@@ -145,7 +145,7 @@ HasFC Decl where
 public export
 record Module where
   constructor MkModule
-  name : Name
+  modname : Name
   imports : List Import
   decls : List Decl
 
@@ -166,7 +166,8 @@ implementation Show Decl
 
 export Show Pattern
 
-export covering
+export
+covering
 Show Clause where
   show (MkClause fc cons pats expr) = show (fc, cons, pats, expr)
 
@@ -187,8 +188,8 @@ Show Decl where
   show (ShortData _ lhs sigs) = foo ["ShortData", show lhs, show sigs]
   show (PFunc _ nm uses ty src) = foo ["PFunc", nm, show uses, show ty, show src]
   show (PMixFix _ nms prec fix) = foo ["PMixFix", show nms, show prec, show fix]
-  show (Class _ nm tele decls) = foo ["Class",  nm, "...", show $ map show decls]
+  show (Class _ nm tele decls) = foo ["Class",  nm, "...", (show $ map show decls)]
-  show (Instance _ nm decls) = foo ["Instance",  show nm, show $ map show decls]
+  show (Instance _ nm decls) = foo ["Instance",  show nm, (show $ map show decls)]
   show (Record _ nm tele nm1 decls) = foo ["Record", show nm, show tele, show nm1, show decls]
 
 export covering
@@ -196,15 +197,16 @@ Show Module where
   show (MkModule name imports decls) = foo ["MkModule", show name, show imports, show decls]
 
 export
+covering
 Show Pattern where
   show (PatVar _ icit str) = foo ["PatVar", show icit, show str]
-  show (PatCon _ icit str xs as) = foo ["PatCon", show icit, show str, assert_total $ show xs, show as]
+  show (PatCon _ icit str xs as) = foo ["PatCon", show icit, show str, show xs, show as]
   show (PatWild _ icit) = foo ["PatWild", show icit]
   show (PatLit _ lit) = foo ["PatLit", show lit]
 
 covering
 Show RCaseAlt where
-  show (MkAlt x y)= foo ["MkAlt", show x, assert_total $ show y]
+  show (MkAlt x y)= foo ["MkAlt", show x, show y]
 
 covering
 Show Raw where
@@ -236,7 +238,7 @@ Pretty Pattern where
   pretty (PatVar _ icit nm) = text nm
   pretty (PatCon _ icit nm args Nothing) = text (show nm) <+> spread (map pretty args)
   pretty (PatCon _ icit nm args (Just as)) = text as ++ text "@(" ++ text (show nm) <+> spread (map pretty args) ++ text ")"
-  pretty (PatWild _icit) = text "_"
+  pretty (PatWild _ icit) = text "_"
   pretty (PatLit _ lit) = pretty lit
 
 wrap : Icit -> Doc -> Doc

src/Lib/Token.idr

@@ -99,5 +99,5 @@ kind : BTok -> Kind
 kind (MkBounded (Tok k s) _) = k
 
 export
-start : BTok -> (Int, Int)
+getStart : BTok -> (Int, Int)
-start (MkBounded _ (MkBounds l c _ _)) = (l,c)
+getStart (MkBounded _ (MkBounds l c _ _)) = (l,c)

src/Lib/Tokenizer.idr

@@ -10,7 +10,7 @@ import Lib.Common
 import Data.String
 
 standalone : List Char
-standalone = unpack "()\\{}[],.@"
+standalone = unpack "()\\{}[,.@]"
 
 keywords : List String
 keywords = ["let", "in", "where", "case", "of", "data", "U", "do",
@@ -38,7 +38,7 @@ quoteTokenise ts@(TS el ec toks chars) startl startc acc = case chars of
   '"' :: cs => Right (TS el ec (toks :< stok) chars)
   '\\' :: '{' :: cs => do
     let tok = MkBounded (Tok StartInterp "\\{") (MkBounds el ec el (ec + 2))
-    (TS sl sc toks chars) <- rawTokenise $ TS el (ec + 2) (toks :< stok :< tok) cs
+    (TS el ec toks chars) <- rawTokenise $ TS el (ec + 2) (toks :< stok :< tok) cs
     case chars of
       '}' :: cs =>
         let tok = MkBounded (Tok EndInterp "}") (MkBounds el ec el (ec + 1))
@@ -94,7 +94,7 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of
     let ch = ifThenElse (c == 'n') '\n' c
     in rawTokenise (TS sl (sc + 4) (toks :< mktok False sl (sc + 4) Character (singleton ch)) cs)
   '\'' :: c :: '\'' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) Character (singleton c)) cs)
-  '#' :: cs => ?do_pragma -- we probably want to require at least one alpha?
+  '#' :: cs => doRest (TS sl (sc + 1) toks cs) Pragma isIdent (Lin :< '#')
   '-' :: '-' :: cs => lineComment (TS sl (sc + 2) toks cs)
   '/' :: '-' :: cs => blockComment (TS sl (sc + 2) toks cs)
   '`' :: cs => doBacktick (TS sl (sc + 1) toks cs) [<]
@@ -145,15 +145,6 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of
         let kind = if elem '_' acc then MixFix else kind in
         rawTokenise (TS l c (toks :< mktok True l (c - 1) kind (pack $ acc <>> [])) (ch :: cs))
 
-    doQuote : TState -> SnocList Char -> Either Error TState
-    -- should be an error..
-    doQuote (TS line col toks Nil) acc = ?missing_end_quote
-    doQuote (TS line col toks ('\\' :: 'n' :: cs)) acc = doQuote (TS line (col + 2) toks cs) (acc :< '\n')
-    doQuote (TS line col toks ('\\' :: c :: cs)) acc = doQuote (TS line (col + 2) toks cs) (acc :< c)
-    doQuote (TS line col toks ('\n' :: cs)) acc = ?error_newline_in_quote
-    doQuote (TS line col toks ('"' :: cs)) acc = rawTokenise (TS line (col + 1) (toks :< mktok False line (col + 1) StringKind (pack $ acc <>> [])) cs)
-    doQuote (TS line col toks (c :: cs)) acc = doQuote (TS line (col + 1) toks cs) (acc :< c)
-
     doChar : Char -> List Char ->  Either Error TState
     doChar c cs = if elem c standalone
       then rawTokenise (TS sl (sc + 1) (toks :< mktok True sl (sc + 1) Symbol (singleton c)) cs)

src/Lib/Types.idr

@@ -160,7 +160,7 @@ public export
 covering
 Show CaseAlt where
   show (CaseDefault tm) = "_ => \{show tm}"
-  show (CaseCons nm args tm) = "\{nm} \{unwords args} => \{show tm}"
+  show (CaseCons nm args tm) = "\{show nm} \{unwords args} => \{show tm}"
   show (CaseLit lit tm) = "\{show lit} => \{show tm}"
 
 public export
@@ -407,7 +407,7 @@ record TopContext where
   constructor MkTop
   -- We'll add a map later?
   defs : SortedMap QName TopEntry
-  metas : IORef MetaContext
+  metaCtx : IORef MetaContext
   verbose : Bool -- command line flag
   errors : IORef (List Error)
   ||| loaded modules
@@ -427,15 +427,7 @@ record Context where
   bds : Vect lvl BD          -- bound or defined
 
   -- FC to use if we don't have a better option
-  fc : FC
+  ctxFC : FC
-
-setName : Context -> Nat -> String -> Context
-setName ctx ix name = case natToFin ix ctx.lvl of
-  Just ix' => { types $= updateAt ix' go  } ctx
-  Nothing => ctx
-  where
-    go : (String,Val) -> (String, Val)
-    go (a,b) = (name,b)
 
 %name Context ctx
 
@@ -460,7 +452,7 @@ Show MetaEntry where
 
 export
 withPos : Context -> FC -> Context
-withPos ctx fc = { fc := fc } ctx
+withPos ctx fc = { ctxFC := fc } ctx
 
 export
 names : Context -> List String
@@ -584,9 +576,9 @@ export
 freshMeta : Context -> FC -> Val -> MetaKind -> M Tm
 freshMeta ctx fc ty kind = do
   top <- get
-  mc <- readIORef top.metas
+  mc <- readIORef top.metaCtx
   debug "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
-  writeIORef top.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty kind [] ::) } mc
+  writeIORef top.metaCtx $ { next $= S, metas $= (Unsolved fc mc.next ctx ty kind [] ::) } mc
   pure $ applyBDs 0 (Meta fc mc.next) ctx.bds
   where
     -- hope I got the right order here :)
@@ -599,8 +591,8 @@ freshMeta ctx fc ty kind = do
 export
 lookupMeta : Nat -> M MetaEntry
 lookupMeta ix = do
-  ctx <- get
+  top <- get
-  mc <- readIORef ctx.metas
+  mc <- readIORef top.metaCtx
   go mc.metas
   where
     go : List MetaEntry -> M MetaEntry

src/Lib/Util.idr

@@ -10,7 +10,6 @@ funArgs tm = go tm []
     go (App _ t u) args = go t (u :: args)
     go t args = (t, args)
 
-
 public export
 data Binder : Type where
   MkBind : FC -> String -> Icit -> Quant -> Tm -> Binder
@@ -20,9 +19,6 @@ export
 Show Binder where
   show (MkBind _ nm icit quant t) = "[\{show quant}\{nm} \{show icit} : ...]"
 
-data Foo : Type -> Type where
-  MkFoo : Nat -> Foo a
-
 export
 splitTele : Tm -> (Tm, List Binder)
 splitTele = go []

src/Main.idr

@@ -123,7 +123,7 @@ processModule importFC base stk qn@(QN ns nm) = do
     processModule fc base (name :: stk) qname
 
   top <- get
-  mc <- readIORef top.metas
+  mc <- readIORef top.metaCtx
   -- REVIEW suppressing unsolved and solved metas from previous files
   -- I may want to know about (or fail early on) unsolved
   let mstart = length mc.metas

test/src/Main.idr

@@ -24,13 +24,13 @@ testCase : M ()
 testCase = do
   -- need to get some defs in here
   top <- get
-  let ctx = mkCtx top.metas
+  let ctx = mkCtx top.metaCtx
   let e = emptyFC
   -- maybe easier to parse out this data.
   processDecl (Data e "Foo" (RU e) [])
 
   tree <- buildTree ctx (MkProb [] (VU emptyFC))
-  --ty <- check (mkCtx top.metas) tm (VU fc)
+  --ty <- check (mkCtx top.metaCtx) tm (VU fc)
   pure ()
 
 

tests/ForwardRecord.newt

@@ -0,0 +1,18 @@
+module ForwardRecord
+
+import Prelude
+
+record Point where
+  x : Int
+  y : Int
+
+instance Show Point
+
+
+instance Show Point where
+  show pt = show pt.x ++ "," ++ show pt.y
+
+
+main : IO Unit
+main = do
+  printLn $ MkPoint 1 2

tests/ForwardRecord.newt.golden

@@ -0,0 +1 @@
+1,2