diff --git a/newt-vscode/syntaxes/newt.tmLanguage.json b/newt-vscode/syntaxes/newt.tmLanguage.json index 3bf6e6f..2d2c8c0 100644 --- a/newt-vscode/syntaxes/newt.tmLanguage.json +++ b/newt-vscode/syntaxes/newt.tmLanguage.json @@ -16,7 +16,7 @@ }, { "name": "keyword.newt", - "match": "\\b(data|where|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b" + "match": "\\b(data|where|class|instance|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b" }, { "name": "string.js", diff --git a/playground/src/monarch.ts b/playground/src/monarch.ts index 853040c..e97574b 100644 --- a/playground/src/monarch.ts +++ b/playground/src/monarch.ts @@ -79,6 +79,8 @@ export let newtTokens: monaco.languages.IMonarchLanguage = { "if", "then", "else", + "class", + "instance", "module", "infixl", "infixr", diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index a76ac6d..f0746fd 100644 --- a/src/Lib/Elab.idr +++ b/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 diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 77248d1..adc3a93 100644 --- a/src/Lib/Parser.idr +++ b/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 diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index d72ec74..be21fbb 100644 --- a/src/Lib/ProcessDecl.idr +++ b/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}" diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index 61e71c5..796e453 100644 --- a/src/Lib/Syntax.idr +++ b/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) diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr index 3e96341..7fd6611 100644 --- a/src/Lib/Tokenizer.idr +++ b/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", "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_"] diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 380eb12..4bbf4dc 100644 --- a/src/Lib/Types.idr +++ b/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