add sugar for typeclass

src/Lib/Elab.idr

@@ -666,8 +666,9 @@ mkPat top (tm, icit) = do
                 (Just (MkEntry name type (DCon k str))) =>
                   -- TODO check arity, also figure out why we need reverse
                   pure $ PatCon fc icit nm !(traverse (mkPat top) b)
-                Just _ => error (getFC tm) "not a data constructor"
-                Nothing => case b of
+                -- This fires when a global is shadowed by a pattern var
+                -- Just _ => error (getFC tm) "\{show nm} is not a data constructor"
+                _ => case b of
                                 [] => pure $ PatVar fc icit nm
                                 _ => error (getFC tm) "patvar applied to args"
     ((RImplicit fc), []) => pure $ PatWild fc icit

src/Lib/Parser.idr

@@ -262,7 +262,7 @@ term =  caseExpr
 varname : Parser String
 varname = (ident <|> uident <|> keyword "_" *> pure "_")
 
-ebind : Parser (List (FC, String, Icit, Raw))
+ebind : Parser Telescope
 ebind = do
   -- don't commit until we see the ":"
   sym "("
@@ -271,7 +271,7 @@ ebind = do
   sym ")"
   pure $ map (\(pos, name) => (pos, name, Explicit, ty)) names
 
-ibind : Parser (List (FC, String, Icit, Raw))
+ibind : Parser Telescope
 ibind = do
   -- I've gone back and forth on this, but I think {m a b} is more useful than {Nat}
   sym "{"
@@ -280,7 +280,7 @@ ibind = do
   sym "}"
   pure $ map (\(pos,name) => (pos, name, Implicit, fromMaybe (RImplicit pos) ty)) names
 
-abind : Parser (List (FC, String, Icit, Raw))
+abind : Parser Telescope
 abind = do
   -- for this, however, it would be nice to allow {{Monad A}}
   sym "{{"
@@ -403,6 +403,22 @@ parseData = do
   decls <- startBlock $ manySame $ parseSig
   pure $ Data fc name ty decls
 
+nakedBind : Parser Telescope
+nakedBind = do
+  names <- some (withPos varname)
+  pure $ map (\(pos,name) => (pos, name, Implicit,  RImplicit pos)) names
+
+export
+parseClass : Parser Decl
+parseClass = do
+  fc <- getPos
+  keyword "class"
+  name <- uident
+  teles <- many $ ebind <|> nakedBind
+  keyword "where"
+  decls <- startBlock $ manySame $ parseSig
+  pure $ Class fc name (join teles) 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
 parseNorm : Parser Decl
@@ -410,7 +426,8 @@ parseNorm = DCheck <$> getPos <* keyword "#check" <*> typeExpr <* keyword ":" <*
 
 export
 parseDecl : Parser Decl
-parseDecl = parseMixfix <|> parsePType <|> parsePFunc <|> parseNorm <|> parseData <|> parseSig <|> parseDef
+parseDecl = parseMixfix <|> parsePType <|> parsePFunc
+  <|> parseNorm <|> parseData <|> parseSig <|> parseDef <|> parseClass
 
 
 export

src/Lib/ProcessDecl.idr

@@ -3,6 +3,7 @@ module Lib.ProcessDecl
 import Data.IORef
 import Data.String
 import Data.Vect
+import Data.Maybe
 
 import Lib.Elab
 import Lib.Parser
@@ -241,6 +242,51 @@ processDecl (DCheck fc tm ty) = do
   norm <- nfv [] res
   putStrLn "  NFV \{pprint [] norm}"
 
+processDecl (Class classFC nm tele decls) = do
+  putStrLn "-----"
+  putStrLn "Class \{nm}"
+  let fields = getSigs decls
+  -- We'll need names for the telescope
+  let dcName = "Mk\{nm}"
+  let tcType = teleToPi tele (RU classFC)
+  let tail = foldl (\ acc, (fc, nm, icit, _) => RApp fc acc (RVar fc nm) icit) (RVar classFC nm) tele
+  let dcType = teleToPi impTele $
+    foldr (\(fc, nm, ty), acc =>  RPi fc (Just nm) Explicit ty acc  ) tail fields
+
+  putStrLn "tcon type \{pretty tcType}"
+  putStrLn "dcon type \{pretty dcType}"
+  let decl = Data classFC nm tcType [TypeSig classFC [dcName] dcType]
+  putStrLn "Decl:"
+  putStrLn $ render 90 $ pretty decl
+  processDecl decl
+  for_ fields $ \ (fc,name,ty) => do
+      let funType = teleToPi impTele $ RPi fc Nothing Auto tail ty
+
+      putStrLn "\{name} : \{pretty funType}"
+      processDecl $ TypeSig fc [name] funType
+
+      let autoPat = foldl (\acc, (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar classFC dcName) fields
+      putStrLn "\{pretty autoPat}"
+      let lhs = foldl (\acc, (fc', nm, _, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele
+      let lhs = RApp classFC lhs autoPat Auto
+      let decl = Def fc name [(lhs, (RVar fc name))]
+      putStrLn "\{pretty decl}"
+      processDecl decl
+  where
+
+    getSigs : List Decl -> List (FC, String, Raw)
+    getSigs [] = []
+    getSigs ((TypeSig _ [] _) :: xs) = getSigs xs
+    getSigs ((TypeSig fc (nm :: nms) ty) :: xs) = (fc, nm, ty) :: getSigs xs
+    getSigs (_:: xs) = getSigs xs
+
+    impTele : Telescope
+    impTele = map (\(fc, nm, _, ty) => (fc, nm, Implicit, ty)) tele
+
+    teleToPi : Telescope -> Raw -> Raw
+    teleToPi [] end = end
+    teleToPi ((fc, nm, icit, ty) :: tele) end = RPi fc (Just nm) icit ty (teleToPi tele end)
+
 processDecl (Data fc nm ty cons) = do
   putStrLn "-----"
   putStrLn "Data \{nm}"

src/Lib/Syntax.idr

@@ -106,7 +106,11 @@ HasFC Raw where
 public export
 data Import = MkImport FC Name
 
--- FIXME - I think I don't want "where" here, but the parser has an issue
+
+public export
+Telescope : Type
+Telescope = (List (FC, String, Icit, Raw))
+
 public export
 data Decl
   = TypeSig FC (List Name) Raw
@@ -116,6 +120,7 @@ data Decl
   | PType FC Name (Maybe Raw)
   | PFunc FC Name Raw String
   | PMixFix FC (List Name) Nat Fixity
+  | Class FC Name Telescope (List Decl)
 
 
 public export
@@ -158,6 +163,7 @@ Show Decl where
   show (PType _ name ty) = foo ["PType", name, show ty]
   show (PFunc _ nm ty src) = foo ["PFunc", nm, show ty, show src]
   show (PMixFix _ nms prec fix) = foo ["PMixFix", show nms, show prec, show fix]
+  show (Class _ nm _ _) = foo ["Class", "FIXME"]
 
 export covering
 Show Module where
@@ -215,7 +221,7 @@ Pretty Raw where
   pretty = asDoc 0
     where
     wrap : Icit -> Doc -> Doc
-    wrap Explicit x = x
+    wrap Explicit x = text "(" ++ x ++ text ")"
     wrap Implicit x = text "{" ++ x ++ text "}"
     wrap Auto x = text "{{" ++ x ++ text "}}"
 
@@ -246,22 +252,24 @@ Pretty Raw where
     asDoc p (RDo _ stmts) = text "TODO - RDo"
     asDoc p (RIf _ x y z) = par p 0 $ text "if" <+> asDoc 0 x <+/> "then" <+> asDoc 0 y <+/> "else" <+> asDoc 0 z
 
+export
+Pretty Decl where
+  pretty (TypeSig _ nm ty) = spread (map text nm) <+> text ":" <+> nest 2 (pretty ty)
+  pretty (Def _ nm clauses) = stack $ map (\(a,b) => pretty a <+> "=" <+> pretty b) clauses
+  pretty (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map pretty xs))
+  pretty (DCheck _ x y) = text "#check" <+> pretty x <+> ":" <+> pretty y
+  pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => ":" <+> pretty ty) ty)
+  pretty (PFunc _ nm ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src))
+  pretty (PMixFix _ names prec fix) = text (show fix) <+> text (show prec) <+> spread (map text names)
+  pretty (Class _ _ _ _) = text "TODO pretty PClass"
+
 export
 Pretty Module where
   pretty (MkModule name imports decls) =
     text "module" <+> text name
       </> stack (map doImport imports)
-      </> stack (map doDecl decls)
+      </> stack (map pretty decls)
       where
         doImport : Import -> Doc
         doImport (MkImport _ nm) = text "import" <+> text nm ++ line
 
-        doDecl : Decl -> Doc
-        doDecl (TypeSig _ nm ty) = spread (map text nm) <+> text ":" <+> nest 2 (pretty ty)
-        doDecl (Def _ nm clauses) = stack $ map (\(a,b) => pretty a <+> "=" <+> pretty b) clauses
-        -- the behavior of nest is kinda weird, I have to do the nest before/around the </>.
-        doDecl (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+>  pretty x <+> (nest 2 $ text "where" </> stack (map doDecl xs))
-        doDecl (DCheck _ x y) = text "#check" <+> pretty x <+> ":" <+> pretty y
-        doDecl (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => ":" <+> pretty ty) ty)
-        doDecl (PFunc _ nm ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src))
-        doDecl (PMixFix _ names prec fix) = text (show fix) <+> text (show prec) <+> spread (map text names)

src/Lib/Tokenizer.idr

@@ -9,6 +9,7 @@ keywords : List String
 keywords = ["let", "in", "where", "case", "of", "data", "U", "do",
             "ptype", "pfunc", "module", "infixl", "infixr", "infix",
             "∀", "forall",
+            "class", "instance",
             "if", "then", "else",
              "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_"]
 

src/Lib/Types.idr

@@ -282,18 +282,6 @@ Show Val where
   show (VLit _ lit) = show lit
   show (VLet _ nm a b) = "(%let \{show nm} = \{show a} in \{show b}"
 
--- Not used - I was going to change context to have a List Binder
--- instead of env, types, bds
--- But when we get down into eval, we don't have types to put into the env
--- It looks like Idris has a separate LocalEnv in eval, Kovacs peels off
--- env from context and extends it.
-data Binder : Type where
-  Bind : (nm : String) -> (bd : BD) -> (val : Val) -> (ty : Val) -> Binder
-
-covering
-Show Binder where
-  show (Bind nm bd val ty) = "(\{show bd} \{show nm} \{show val} : \{show ty})"
-
 public export
 Env : Type
 Env = List Val