From 7a681e5239d0ec50c3c5d7371a865565f9247bd9 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 11 Sep 2024 21:16:01 -0700 Subject: [PATCH] implicit patterns --- TODO.md | 7 +++++-- newt/typeclass.newt | 9 +++++++++ src/Lib/Check.idr | 34 ++++++++++++++++++---------------- src/Lib/Parser.idr | 23 +++++++++++++---------- src/Lib/Syntax.idr | 33 ++++++++++++++++++++------------- 5 files changed, 65 insertions(+), 41 deletions(-) diff --git a/TODO.md b/TODO.md index 4d88831..8014025 100644 --- a/TODO.md +++ b/TODO.md @@ -1,15 +1,18 @@ ## TODO +- [ ] there is some zero argument application in generated code + - possibly the fancy "apply arity then curry the rest" bit - [x] inline metas. Maybe zonk after TC/elab -- [ ] implicit patterns +- [x] implicit patterns - [ ] pair syntax - [ ] list syntax - [ ] operators - [ ] import - [ ] add {{ }} and solving autos + - considering various solutions. Perhaps marking the data type as solvable, if we had types on metas. - [ ] do blocks -- [ ] some solution for + (classes? ambiguity?) +- [ ] some solution for `+` (classes? ambiguity?) - [ ] show compiler failure in the editor (exit code != 0) - [ ] write js files into `out` directory - [ ] detect extra clauses in case statements diff --git a/newt/typeclass.newt b/newt/typeclass.newt index f70e67e..fd1677d 100644 --- a/newt/typeclass.newt +++ b/newt/typeclass.newt @@ -28,3 +28,12 @@ MaybeMonad = MkMonad {Maybe} (\ {A} ma amb => Just a => amb a) -- so if we added {{ }} and search... +-- second arg will be {{}} +-- add implicit patterns first + +-- I need a way to tag `x : Monad m` as auto. I could do {{}}, but maybe I should tag the `data` for search? +-- It should be a record, but I don't have records yet + +bind : {m : U -> U} -> {x : Monad m} -> {a b : U} -> (m a) -> (a -> m b) -> m b +bind {m} {MkMonad bind'} = bind' + diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index 0183bde..9529105 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -261,10 +261,13 @@ export buildTree : Context -> Problem -> M Tm introClause : String -> Icit -> Clause -> M Clause --- I don't think this makes a difference? -introClause nm Implicit (MkClause fc cons pats expr) = pure $ MkClause fc ((nm, PatWild fc) :: cons) pats expr +introClause nm icit (MkClause fc cons (pat :: pats) expr) = + if icit == getIcit pat then pure $ MkClause fc ((nm, pat) :: cons) pats expr + else if icit == Implicit then pure $ MkClause fc ((nm, PatWild fc Implicit) :: cons) (pat :: pats) expr + else error fc "Explicit arg and implicit pattern \{show nm} \{show icit} \{show pat}" +-- handle implicts at end? +introClause nm Implicit (MkClause fc cons [] expr) = pure $ MkClause fc ((nm, PatWild fc Implicit) :: cons) [] expr introClause nm icit (MkClause fc cons [] expr) = error fc "Clause size doesn't match" -introClause nm icit (MkClause fc cons (pat :: pats) expr) = pure $ MkClause fc ((nm, pat) :: cons) pats expr -- A split candidate looks like x /? Con ... -- we need a type here. I pulled if off of the @@ -273,7 +276,7 @@ introClause nm icit (MkClause fc cons (pat :: pats) expr) = pure $ MkClause fc ( findSplit : List Constraint -> Maybe Constraint findSplit [] = Nothing -- FIXME look up type, ensure it's a constructor -findSplit (x@(nm, PatCon _ cnm pats) :: xs) = Just x +findSplit (x@(nm, PatCon _ _ cnm pats) :: xs) = Just x findSplit (_ :: xs) = findSplit xs @@ -399,17 +402,16 @@ buildCase ctx prob scnm scty (dcName, _, ty) = do -- We get a list of clauses back (a Problem) and then solve that -- If they all fail, we have a coverage issue. (Assuming the constructor is valid) - - -- we'll want implicit patterns at some point, for now we wildcard implicits because - -- we don't have them makeConst : List Bind -> List Pattern -> List (String, Pattern) makeConst [] [] = [] - -- need M in here to throw. + -- would need M in here to throw, and I'm building stuff as I go, I suppose I could <$> makeConst [] (pat :: pats) = ?extra_patterns - -- - makeConst ((MkBind nm Implicit x) :: xs) [] = (nm, PatWild emptyFC) :: makeConst xs [] + makeConst ((MkBind nm Implicit x) :: xs) [] = (nm, PatWild emptyFC Implicit) :: makeConst xs [] makeConst ((MkBind nm Explicit x) :: xs) [] = ?extra_binders_2 - makeConst ((MkBind nm Implicit x) :: xs) (pat :: pats) = (nm, PatWild (getFC pat)) :: makeConst xs (pat :: pats) + makeConst ((MkBind nm Implicit x) :: xs) (pat :: pats) = + if getIcit pat == Explicit + then (nm, PatWild (getFC pat) Implicit) :: makeConst xs (pat :: pats) + else (nm, pat) :: makeConst xs pats makeConst ((MkBind nm Explicit x) :: xs) (pat :: pats) = (nm, pat) :: makeConst xs pats rewriteCons : List Bind -> List Constraint -> List Constraint -> Maybe (List Constraint) @@ -417,9 +419,9 @@ buildCase ctx prob scnm scty (dcName, _, ty) = do rewriteCons vars (c@(nm, y) :: xs) acc = if nm == scnm then case y of - PatVar _ s => Just $ c :: (xs ++ acc) - PatWild _ => Just $ c :: (xs ++ acc) - PatCon _ str ys => if str == dcName + PatVar _ _ s => Just $ c :: (xs ++ acc) + PatWild _ _ => Just $ c :: (xs ++ acc) + PatCon _ _ str ys => if str == dcName then Just $ (makeConst vars ys) ++ xs ++ acc else Nothing else rewriteCons vars xs (c :: acc) @@ -451,8 +453,8 @@ checkDone ctx [] body ty = do got <- check ctx body ty debug "DONE<- got \{pprint (names ctx) got}" pure got -checkDone ctx ((x, PatWild _) :: xs) body ty = checkDone ctx xs body ty -checkDone ctx ((nm, (PatVar _ nm')) :: xs) body ty = checkDone ({ types $= rename } ctx) xs body ty +checkDone ctx ((x, PatWild _ _) :: xs) body ty = checkDone ctx xs body ty +checkDone ctx ((nm, (PatVar _ _ nm')) :: xs) body ty = checkDone ({ types $= rename } ctx) xs body ty where rename : Vect n (String, Val) -> Vect n (String, Val) rename [] = [] diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index b60cf8e..5361756 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -165,20 +165,23 @@ lamExpr = do -- We may need to look up names at some point to see if they're constructors. -- so, we can do the capital letter thing here or push that bit down and collect single/double -pPattern' : Parser Pattern pPattern : Parser Pattern -pPattern - = PatWild <$ keyword "_" <*> getPos - <|> PatVar <$> getPos <*> ident - <|> PatCon <$> getPos <*> uident <*> pure [] - <|> parens pPattern' +patAtom : Parser Pattern +patAtom = do + fc <- getPos + PatWild fc Explicit <$ keyword "_" + <|> PatVar fc Explicit <$> ident + <|> PatCon fc Explicit <$> uident <*> pure [] + <|> braces (PatVar fc Implicit <$> ident) + <|> braces (PatWild fc Implicit <$ keyword "_") + <|> braces (PatCon fc Implicit <$> uident <*> many patAtom) + <|> parens pPattern -pPattern' = PatCon <$> getPos <*> uident <*> many pPattern <|> pPattern +pPattern = PatCon (!getPos) Explicit <$> uident <*> many patAtom <|> patAtom caseAlt : Parser RCaseAlt caseAlt = do - -- pat <- parseOp -- pPattern -- term and sort it out later? - pat <- pPattern' + pat <- pPattern keyword "=>" commit t <- term @@ -264,7 +267,7 @@ parseDef : Parser Decl parseDef = do fc <- getPos nm <- ident <|> uident - pats <- many pPattern + pats <- many patAtom keyword "=" body <- mustWork typeExpr -- these get collected later diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index d8bed89..6b7feb0 100644 --- a/src/Lib/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -16,17 +16,24 @@ data RigCount = Rig0 | RigW public export data Pattern - = PatVar FC Name - | PatCon FC Name (List Pattern) - | PatWild FC + = PatVar FC Icit Name + | PatCon FC Icit Name (List Pattern) + | PatWild FC Icit -- Not handling this yet, but we need to be able to work with numbers and strings... -- | PatLit Literal +export +getIcit : Pattern -> Icit +getIcit (PatVar x icit str) = icit +getIcit (PatCon x icit str xs) = icit +getIcit (PatWild x icit) = icit + + export HasFC Pattern where - getFC (PatVar fc str) = fc - getFC (PatCon fc str xs) = fc - getFC (PatWild fc) = fc + getFC (PatVar fc _ _) = fc + getFC (PatCon fc _ _ _) = fc + getFC (PatWild fc _) = fc -- %runElab deriveShow `{Pattern} public export @@ -147,10 +154,9 @@ Show RigCount where export 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 (PatVar _ icit str) = foo ["PatVar", show icit, show str] + show (PatCon _ icit str xs) = foo ["PatCon", show icit, show str, assert_total $ show xs] + show (PatWild _ icit) = foo ["PatWild", show icit] covering Show RCaseAlt where @@ -173,9 +179,10 @@ Show Raw where export Pretty Pattern where - pretty (PatVar _ nm) = text nm - pretty (PatCon _ nm args) = text nm <+> spread (map pretty args) - pretty (PatWild _)= "_" + -- FIXME - wrap Implicit with {} + pretty (PatVar _ icit nm) = text nm + pretty (PatCon _ icit nm args) = text nm <+> spread (map pretty args) + pretty (PatWild _icit)= "_"