Show instances, fixed a bunch of bugs in parsing

- The case / let / indent stuff actually works
- Needed a bunch of defers
- Idris silently builds loops in immediate definitions

.editorconfig

@@ -0,0 +1,6 @@
+# https://editorconfig.org/
+[*]
+end_of_line = lf
+insert_final_newline = true
+indent_size = 2
+indent_style = space

.gitignore

@@ -0,0 +1,2 @@
+build/
+*.*~

newt.ipkg

@@ -13,7 +13,7 @@ authors = "Steve Dunham"
 -- langversion
 
 -- packages to add to search path
-depends = contrib
+depends = contrib, base
 
 -- modules to install
 -- modules =

src/Derive.idr

@@ -0,0 +1,46 @@
+module Derive
+
+import public Language.Reflection
+-- import public Language.Elab.Syntax
+-- import public Language.Elab.Types
+
+-- Is base not in scope?
+-- import public Deriving.Common
+
+%language ElabReflection
+
+getType1 : Name -> Elab (Name,TTImp)
+getType1 name = do
+  [rval] <- getType name 
+    | [] => fail "can't get fullname for \{show name}"
+    | _  => fail "ambiguous name \{show name}"
+  pure rval
+
+
+fullName : Name -> Elab Name
+fullName name = do
+  [(qname,_)] <- getType name 
+    | [] => fail "can't get fullname for \{show name}"
+    | _  => fail "ambiguous name \{show name}"
+  pure qname
+
+export
+deriveShow : Name -> Elab ()
+deriveShow name = do
+    myGoal <- goal
+    logMsg "foo" 1 $ "my goal is \{show myGoal}"
+    fname <- fullName name
+    logMsg "foo" 1 $ "woo \{show fname}"
+    cons <- getCons fname
+    logMsg "foo" 1 $ "cons \{show cons}"
+    for_ cons $ \name => do
+      logMsg "foo" 1 $ "getType1 \{show name}"
+      (_,type) <- getType1 name
+      logTerm "foo" 1 (show name) type
+      -- type doesn't really matter, we need the explicit arity and the base name
+      
+
+
+    pure ()
+
+

src/Lib/Parser.idr

@@ -4,6 +4,7 @@ module Lib.Parser
 import Lib.Token
 import Lib.Parser.Impl
 import Syntax
+import Data.List
 
 -- There is the whole core vs surface thing here.
 -- might be best to do core first/ Technically don't
@@ -19,27 +20,130 @@ import Syntax
 
 ident = token Ident
 
-term : Parser Term
 
+parens : Parser a -> Parser a
+parens pa = do
+  sym "("
+  t <- pa
+  sym ")"
+  pure t
+
+lit : Parser Term
+lit = do
+  t <- token Number
+  pure $ Lit (LInt (cast t))
+
+
+
+export
+term : (Parser Term)
+
+
+-- ( t : ty ), (t , u) (t)
+-- Or do we want (x : ty)  I think we may need to annotate any term
+parenThinger : Parser Term
+parenThinger = do
+  keyword "("
+  t <- term
+  -- And now we want ) : or ,
+  -- we could do this with backtracing, but it'd kinda suck?
+  fail "todo"
+
+-- the inside of term
+atom : Parser Term
+atom = lit 
+    <|> Var <$> ident
+    <|> parens term
+    -- <|> sym "(" *> term <* sym ")"
+
+--
+-- atom is lit or ident
+
+data Fixity = InfixL | InfixR | Infix
+
+-- starter pack, but we'll move some to prelude
+operators : List (String, Int, Fixity)
+operators = [
+  ("->", 1, InfixR),
+  ("=", 2, InfixL), -- REVIEW
+  ("+",4,InfixL),
+  ("-",4,InfixL),
+  ("*",5,InfixL),
+  ("/",5,InfixL)
+]
+parseApp : Parser Term
+parseApp = do
+  hd <- atom
+  rest <- many atom
+  pure $ foldl App hd rest
+  
+
+parseOp : Lazy (Parser Term)
+parseOp = parseApp >>= go 0
+  where
+    go : Int -> Term -> Parser Term
+    go prec left = 
+      do
+        op <- token Oper
+        let Just (p,fix) = lookup op operators
+         | Nothing => fail "expected operator"
+        -- if p >= prec then pure () else fail ""
+        guard $ p >= prec
+        -- commit
+        let pr = case fix of InfixR => p; _ => p + 1
+        -- commit?
+        right <- go pr !(parseApp)
+        go prec (App (App (Var op) left) right)
+      <|> pure left
+
+
+export
 letExpr : Parser Term
-letExpr = Let <$ keyword "let" <*> ident <* keyword "=" <*> term <* keyword "in" <*> term
+letExpr = do
+  keyword "let"
+  commit
+  alts <- startBlock $ someSame $ letAssign
+  keyword' "in"
+  scope <- term
+  pure $ Let alts scope
+  -- Let <$ keyword "let" <*> ident <* keyword "=" <*> term <* keyword "in" <*> term
 
-pattern : Parser Pattern
+  where
+    letAssign : Parser (Name,Term)
+    letAssign = do
+      name <- ident
+      keyword "="
+      t <- term
+      pure (name,t)
 
+pPattern : Parser Pattern
+pPattern
+   = PatWild <$ keyword "_"
+  <|> [| PatVar ident |]
+
+export
 lamExpr : Parser Term
 lamExpr = do
   keyword "\\"
   commit
-  name <- pattern
+  name <- pPattern
   keyword "."
   scope <- term
   pure $ Lam name scope
 
-caseAlt : Parser CaseAlt
 
+caseAlt : Parser CaseAlt
+caseAlt = do
+  pat <- pPattern -- Term and sort it out later?
+  keyword "=>"
+  commit
+  t <- term
+  pure $ MkAlt pat t
+
+export
 caseExpr : Parser Term
 caseExpr = do
-  _ <- keyword "case"
+  keyword "case"
   commit
   sc <- term
   keyword "of"
@@ -47,10 +151,10 @@ caseExpr = do
   pure $ Case sc alts
 
 
-
+term = defer $ \_ => 
--- TODO - get this up and running with a case expr to test it
+        caseExpr
-
+    <|> letExpr
-
+    <|> parseOp
 
 {-
 so lets say we wanted to do the indent, the hard way. 

src/Lib/Parser/Impl.idr

@@ -33,9 +33,19 @@ Functor Result where
 export
 data Parser a = P (TokenList -> Bool -> (lc : (Int,Int)) -> Result a)
 
+export
 runP : Parser a -> TokenList -> Bool -> (Int,Int) -> Result a
 runP (P f) = f
 
+export
+parse : Parser a -> TokenList -> Either String a
+parse pa toks = case runP pa toks False (0,0) of
+  Fail (E msg) toks com => Left "error: \{msg} next at: \{show toks}"
+  OK a [] _ => Right a
+  OK a ts _ => Left "Extra toks \{show ts}"
+
+
+export
 fail : String -> Parser a
 fail msg = P $ \toks,com,col => Fail (E msg) toks com
 
@@ -58,23 +68,24 @@ export
 Alternative Parser where
   empty = fail "empty"
   (P pa) <|> (P pb) = P $ \toks,com,col =>
-    case pa toks com col of
+    case pa toks False col of
-      f@(Fail _ _ com') => if com' then f else pb toks com col
+      OK a toks' _ => OK a toks' com
-      t => t
+      Fail err toks' True  => Fail err toks' com
+      Fail err toks' False => pb toks com col
 
 export
 Monad Parser where
   P pa >>= pab = P $ \toks,com,col =>
     case pa toks com col of
       (OK a toks com) => runP (pab a) toks com col
-      (Fail err xs x) => ?rhs_1
+      (Fail err xs x) => Fail err xs x
 
 
 -- do we need this?
 pred : (BTok -> Bool) -> String -> Parser String
 pred f msg = P $ \toks,com,col =>
   case toks of
-    (t :: ts) => if f t then OK (value t) ts com else Fail (E msg) toks com
+    (t :: ts) => if f t then OK (value t) ts com else Fail (E "\{msg} vt:\{value t}") toks com
     [] => Fail (E "eof") toks com
 
 export
@@ -82,18 +93,16 @@ commit : Parser ()
 commit = P $ \toks,com,col => OK () toks True
 
 export
-token : Kind -> Parser String
+defer : (() -> (Parser a)) -> Parser a
-token k = pred (\t => t.val.kind == k) "Expected a \{show k}"
+defer f = P $ \toks,com,col => runP (f ()) toks com col
 
 
-export
+mutual
-keyword : String -> Parser ()
-keyword kw = ignore $ pred (\t => t.val.text == kw) "Expected \{kw}"
   
+  export some : Parser a -> Parser (List a)
+  some p = defer $ \_ => [| p :: many p|] --(::) <$> p <*> many p)
   
-many : Parser a -> Parser (List a)
+  export many : Parser a -> Parser (List a)
-some : Parser a -> Parser (List a)
-some p = (::) <$> p <*> many p
   many p = some p <|> pure []
 
 -- sixty let has some weird CPS stuff, but essentially:
@@ -108,7 +117,7 @@ export
 startBlock : Parser a -> Parser a
 startBlock (P p) = P $ \toks,com,(l,c) => case toks of
   [] => p toks com (l,c)
-  (t :: ts) =>
+  (t :: _) =>
     let (tl,tc) = start t
     in p toks com (tl,tc)
 
@@ -118,7 +127,7 @@ export
 sameLevel : Parser a -> Parser a
 sameLevel (P p) = P $ \toks,com,(l,c) => case toks of
   [] => p toks com (l,c)
-  (t :: ts) => 
+  (t :: _) => 
     let (tl,tc) = start t 
     in if tc == c then p toks com (tl, c)
     else if c < tc then Fail (E "unexpected indent") toks com
@@ -126,14 +135,38 @@ sameLevel (P p) = P $ \toks,com,(l,c) => case toks of
 
 export
 someSame : Parser a -> Parser (List a)
-someSame = some . sameLevel
+someSame pa = some $ sameLevel pa
 
 ||| requires a token to be indented?
+export
 indented : Parser a -> Parser a
 indented (P p) = P $ \toks,com,(l,c) => case toks of
   [] => p toks com (l,c)
-  (t::ts) =>
+  (t::_) =>
     let (tl,tc) = start t
     in if tc > c || tl == l then p toks com (l,c)
     else Fail (E "unexpected outdent") toks com
 
+
+
+export
+token' : Kind -> Parser String
+token' k = pred (\t => t.val.kind == k) "Expected a \{show k}"
+
+
+export
+keyword' : String -> Parser ()
+keyword' kw = ignore $ pred (\t => t.val.text == kw) "Expected \{kw}"
+
+export
+token : Kind -> Parser String
+token = indented . token'
+
+export
+keyword : String -> Parser ()
+keyword kw = indented $ keyword' kw
+
+export
+sym : String -> Parser ()
+sym = keyword
+

src/Lib/Token.idr

@@ -9,8 +9,8 @@ data Kind
   | Oper 
   | Number 
   | Symbol
-  | Arrow
   | Space
+  -- not doing Layout.idr
   | LBrace
   | Semi
   | RBrace
@@ -22,7 +22,6 @@ Show Kind where
   show Oper    = "Oper"
   show Number  = "Number"
   show Symbol  = "Symbol"
-  show Arrow   = "Arrow"
   show Space  = "Space"
   show LBrace  = "LBrace"
   show Semi    = "Semi"
@@ -35,7 +34,6 @@ Eq Kind where
   Oper    == Oper = True
   Number  == Number = True
   Symbol  == Symbol = True
-  Arrow   == Arrow = True
   Space   == Space = True
   LBrace  == LBrace = True
   Semi    == Semi   = True

src/Lib/Tokenizer.idr

@@ -13,10 +13,6 @@ specialOps = ["->", ":"]
 checkKW : String -> Token Kind
 checkKW s = if elem s keywords then Tok Keyword s else Tok Ident s
 
-opkind : String -> Kind
-opkind "->" = Arrow
-opkind _    = Oper
-
 isOpChar : Char -> Bool
 isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")
 
@@ -28,7 +24,7 @@ opChar = pred isOpChar
 -- tmap = [
 --   (alpha <+> many alphaNum, checkKW),
 --   (some digit, Tok Number),
---   (some opChar, \s => Tok (opkind s) s),
+--   (some opChar, \s => Tok Oper s),
 --   (lineComment (exact "--"), Tok Space),
 --   (symbol, Tok Symbol),
 --   (spaces, Tok Space)
@@ -38,7 +34,7 @@ rawTokens : Tokenizer (Token Kind)
 rawTokens
    =  match (alpha <+> many alphaNum) checkKW
   <|> match (some digit) (Tok Number)
-  <|> match (some opChar) (\s => Tok (opkind s) s)
+  <|> match (some opChar) (\s => Tok Oper s)
   <|> match (lineComment (exact "--")) (Tok Space)
   <|> match symbol (Tok Symbol)
   <|> match spaces (Tok Space)

src/Main.idr

@@ -3,26 +3,33 @@ module Main
 import Lib.Tokenizer
 import Lib.Layout
 import Lib.Token
+import Lib.Parser.Impl
+import Lib.Parser
+import Syntax
 
-src = "let x = 1\n    y = 2\n in x + y"
+check : Show a => Parser a -> String -> IO ()
-
+check pa src = do
-check : String -> IO ()
+  _ <- putStrLn "--"
-check src = do
+  _ <- putStrLn $ src
-  putStrLn "--"
-  printLn $ src
   let toks = tokenise src
-  
   printLn $ toks
-  let toks2 = layout toks
+  let res = parse pa toks
+  printLn res
+  -- let toks2 = layout toks
+  -- printLn $ map value toks2
 
-  printLn $ map value toks2
+-- gotta fix up error messages. Show it with some source
 
 main : IO ()
 main = do
   -- this stuff is working with layout, should I bother with col.
   -- downside is that it will be somewhat picky about the indentation of `in`
   -- The sixty stuff looks promising.  I might want my own tokenizer though.
-  check "let x = 1\n    y = 2\n in x + y"
+  check letExpr "let x = 1\n    y = 2\n in x + y"
-  check "let x = 1 in x + 2"
+  check term "let x = 1 in x + 2"
-  check "case x of\n   True => something\n   False => let\n      x = 1\n      y = 2\n    in x + y"
+  printLn "BREAK"
-
+  check term "case x of\n   True => something\n   False => let\n      x = 1\n      y = 2\n    in x + y"
+  check term "x + y * z + w"
+  check term "y * z + w"
+  check term "x -> y -> z"
+  check term "x y z"

src/Syntax.idr

@@ -1,7 +1,16 @@
 module Syntax
 
+import Data.String
+import Derive
+
+
 -- Good enough start, lets parse
 -- This is informed by pi-forall and others and is somewhat low level
+-- %language ElabReflection
+-- %logging "foo" 19
+
+%hide Name
+%hide Decl
 
 Name = String
 
@@ -9,8 +18,11 @@ data Term : Type where
 
 TyTerm = Term
 
+public export
 data Literal = LString String | LInt Int | LBool Bool
+public export
 data RigCount = Rig0 | RigW
+public export
 data Plicity = Implicit | Explicit | Eq
 
 public export
@@ -20,6 +32,8 @@ data Pattern
   | PatWild
   | PatLit Literal
 
+-- %runElab deriveShow `{Pattern}
+
 -- could be a pair, but I suspect stuff will be added?
 public export
 data CaseAlt = MkAlt Pattern Term
@@ -29,7 +43,7 @@ data Term
   = Var Name
   | Ann Term TyTerm
   | Lit Literal
-  | Let Name Term Term
+  | Let (List (Name, Term)) Term
   | Pi Name Plicity Term Term
   | App Term Term
   | Lam Pattern Term
@@ -56,3 +70,47 @@ record Module where
   name : Name
   imports : List Name
   decls : List Decl
+
+foo : List String -> String
+foo ts = "(" ++ unwords ts ++ ")"
+
+mutual
+
+  Show RigCount where
+    show Rig0 = "Rig0"
+    show RigW = "RigW"
+
+  Show Pattern where
+    show (PatVar str) = foo ["PatVar", show str]
+    show (PatCon str xs) = foo ["PatCon", show str, assert_total $ show xs]
+    show PatWild = "PatWild"
+    show (PatLit x) = foo ["PatLit" , show x]
+
+
+  Show CaseAlt where
+    show (MkAlt x y)= foo ["MkAlt", show x, assert_total $ show y]
+
+  Show Plicity where
+    show Implicit = "Implicit"
+    show Explicit = "Explicit"
+    show Eq = "Eq"
+
+  Show Literal where
+    show (LString str) = foo [ "LString", show str]
+    show (LInt i) = foo [ "LInt", show i]
+    show (LBool x) = foo [ "LBool", show x]
+
+
+  export
+  Show Term where
+    show (Var name) = foo ["Var", show name]
+    show (Ann t ty) = foo [ "Ann", show t, show ty]
+    show (Lit x) = foo [ "Lit", show x]
+    show (Let alts y) = foo [ "Let", assert_total $ show alts, show y]
+    show (Pi str x y z) = foo [ "Pi", show str, show x, show y, show z]
+    show (App x y) = foo [ "App", show x, show y]
+    show (Lam x y) = foo [ "Lam", show x, show y]
+    show (Case x xs) = foo [ "Case", show x, show xs]
+    show Wildcard = "Wildcard"
+    show (ParseError str) = foo [ "ParseError", "str"]
+