From d22f3844f6aa3e4f7a575a9dcecc5e23bc3a3e71 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 14 Dec 2024 19:58:52 -0800 Subject: [PATCH] At patterns on LHS --- TODO.md | 7 ++++++- aoc2023/Day1.newt | 4 ---- src/Lib/Elab.idr | 41 ++++++++++++++++++++++++++--------------- src/Lib/Parser.idr | 12 +++++++++++- src/Lib/Syntax.idr | 17 ++++++++++------- src/Lib/Tokenizer.idr | 4 ++-- src/Lib/Types.idr | 8 ++++++++ 7 files changed, 63 insertions(+), 30 deletions(-) diff --git a/TODO.md b/TODO.md index c3c4e7c..1d383bf 100644 --- a/TODO.md +++ b/TODO.md @@ -1,11 +1,16 @@ ## TODO +More comments in code! This is getting big enough that I need to re-find my bearings when fixing stuff. + +- [ ] Move on to next decl in case of error + - for parse error, seek to col 0 token - [ ] keymap for monaco - [x] SortedMap.newt issue in `where` - [x] fix "insufficient patterns", wire in M or Either String - [x] Matching _,_ when Maybe is expected should be an error - [ ] There are issues with matching inside do blocks, I think we need to guess scrutinee? I could imagine constraining metas too (e.g. if Just ... at ?m123 then ?m123 =?= Maybe ?m456) + - Also, the root cause is tough to track down if there is a type error (this happens with `do` in Idris, too). - [ ] error for non-linear pattern - [ ] typeclass dependencies - need to flag internal functions to not search (or flag functions for search). I need to decide on syntax for this. @@ -33,7 +38,7 @@ - [ ] `$` no longer works inside ≡⟨ ⟩ sort out how to support both that and `$ \ x => ...` (or don't bother) - We'd either need to blacklist all non-initial mixfix bits at the appropriate spots or always pass around a terminating token. - [ ] **Translate newt to newt** - - [ ] Support @ on the LHS + - [x] Support @ on the LHS - [x] if / then / else sugar - [ ] `data Foo = A | B` sugar - [ ] records diff --git a/aoc2023/Day1.newt b/aoc2023/Day1.newt index ebb2313..2fc2c65 100644 --- a/aoc2023/Day1.newt +++ b/aoc2023/Day1.newt @@ -10,10 +10,6 @@ digits1 (c :: cs) = let x = ord c in then x - 48 :: digits1 cs else digits1 cs -tail : {a : U} -> List a -> List a -tail Nil = Nil -tail (x :: xs) = xs - -- TODO I used @ patterns in Lean digits2 : List Char -> List Int digits2 xs = case xs of diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index a7e6cdf..84f247c 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -15,7 +15,6 @@ import Lib.Eval import Lib.TopContext import Lib.Syntax - ||| collectDecl collects multiple Def for one function into one export collectDecl : List Decl -> List Decl @@ -453,7 +452,7 @@ introClause nm icit (MkClause fc cons [] expr) = error fc "Clause size doesn't m 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 _ _ _ _ _) :: xs) = Just x findSplit (x@(nm, PatLit _ val) :: xs) = Just x findSplit (x :: xs) = findSplit xs @@ -580,7 +579,6 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do let (VRef _ sctynm _ _) = scty | _ => error (getFC scty) "case split on non-inductive \{show scty}" case lookupDef ctx scnm of - -- NOW this is S var7 Just val@(VRef fc nm y sp) => if nm /= dcName then do @@ -693,13 +691,15 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do then case y of PatVar _ _ s => pure $ Just $ c :: (xs ++ acc) PatWild _ _ => pure $ Just $ c :: (xs ++ acc) - -- FIXME why don't we hit this ('x' for Just x) + -- FIXME why don't we hit this (when user puts 'x' for Just 'x') PatLit fc lit => error fc "Literal \{show lit} in constructor split" - -- FIXME check type - PatCon fc _ nm ys => if nm == dcName - then pure $ Just $ !(makeConstr vars ys) ++ xs ++ acc - -- TODO can we check this when we make the PatCon? + PatCon fc icit nm ys as => if nm == dcName + then case as of + Nothing => pure $ Just $ !(makeConstr vars ys) ++ xs ++ acc + -- putting this in constraints causes it to be renamed scnm -> nm' when we check body. + Just nm' => pure $ Just $ (scnm, (PatVar fc icit nm')) :: !(makeConstr vars ys) ++ xs ++ acc else do + -- TODO can we check this when we make the PatCon? case lookup nm !get of (Just (MkEntry _ name type (DCon k tcname))) => if (tcname /= sctynm) @@ -721,12 +721,17 @@ splitArgs tm args = (tm, args) mkPat : TopContext -> (Raw, Icit) -> M Pattern +mkPat top (RAs fc as tm, icit) = + case !(mkPat top (tm, icit)) of + (PatCon fc icit nm args Nothing) => pure $ PatCon fc icit nm args (Just as) + (PatCon fc icit nm args Nothing) => error fc "Double as pattern \{show tm}" + t => error fc "Can't put as on non-constructor \{show tm}" mkPat top (tm, icit) = do case splitArgs tm [] of ((RVar fc nm), b) => case lookup nm top of (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) + pure $ PatCon fc icit nm !(traverse (mkPat top) b) Nothing -- 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 @@ -736,7 +741,7 @@ mkPat top (tm, icit) = do ((RImplicit fc), _) => error fc "implicit pat can't be applied to arguments" ((RLit fc lit), []) => pure $ PatLit fc lit ((RLit fc y), b) => error fc "lit cannot be applied to arguments" - (a,b) => error (getFC a) "expected pat var or constructor" + (a,b) => error (getFC a) "expected pat var or constructor, got \{show a}" export @@ -853,6 +858,7 @@ buildLitCase ctx prob fc scnm scty lit = do pure $ CaseLit lit tm where + -- FIXME - thread in M for errors -- replace constraint with constraints on parameters, or nothing if non-matching clause rewriteConstraint : List Constraint -> List Constraint -> Maybe (List Constraint) rewriteConstraint [] acc = Just acc @@ -862,7 +868,7 @@ buildLitCase ctx prob fc scnm scty lit = do PatVar _ _ s => Just $ c :: (xs ++ acc) PatWild _ _ => Just $ c :: (xs ++ acc) PatLit fc lit' => if lit' == lit then Just $ (xs ++ acc) else Nothing - PatCon _ _ str ys => Nothing -- error matching lit against constructor + PatCon _ _ str ys as => Nothing -- error matching lit against constructor else rewriteConstraint xs (c :: acc) rewriteClause : Clause -> Maybe Clause @@ -896,6 +902,13 @@ litTyName (LString str) = "String" litTyName (LInt i) = "Int" litTyName (LChar c) = "Char" +renameContext : String -> String -> Context -> Context +renameContext from to ctx = { types $= go } ctx + where + go : Vect n (String,Val) -> Vect n (String,Val) + go Nil = Nil + go ((a,b) :: types) = if a == from then (to,b) :: types else (a,b) :: go types + -- This process is similar to extendPi, but we need to stop -- if one clause is short on patterns. buildTree ctx (MkProb [] ty) = error emptyFC "no clauses" @@ -928,9 +941,8 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do -- REVIEW We probably need to know this is a VRef before we decide to split on this slot.. scty' <- unlet ctx.env scty >>= forceType ctx.env case pat of - PatCon _ _ _ _ => do + PatCon fc _ _ _ as => do -- expand vars that may be solved, eval top level functions - debug "EXP \{show scty} -> \{show scty'}" -- this is per the paper, but it would be nice to coalesce -- default cases @@ -939,7 +951,6 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do alts <- traverse (buildCase ctx prob scnm scty') cons debug "GOTALTS \{show alts}" when (length (catMaybes alts) == 0) $ error (fc) "no alts for \{show scty'}" - -- TODO check for empty somewhere? pure $ Case fc sctm (catMaybes alts) PatLit fc v => do let tyname = litTyName v @@ -1140,5 +1151,5 @@ infer ctx (RImplicit fc) = do infer ctx (RLit fc (LString str)) = pure (Lit fc (LString str), !(primType fc "String")) infer ctx (RLit fc (LInt i)) = pure (Lit fc (LInt i), !(primType fc "Int")) infer ctx (RLit fc (LChar c)) = pure (Lit fc (LChar c), !(primType fc "Char")) - +infer ctx (RAs fc _ _) = error fc "@ can only be used in patterns" infer ctx tm = error (getFC tm) "Implement infer \{show tm}" diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 2db6fda..31a45ad 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -74,10 +74,20 @@ export term : (Parser Raw) withPos : Parser a -> Parser (FC, a) withPos pa = (,) <$> getPos <*> pa +asAtom : Parser Raw +asAtom = do + fc <- getPos + nm <- ident + asPat <- optional $ keyword "@" *> parens typeExpr + case asPat of + Just exp => pure $ RAs fc nm exp + Nothing => pure $ RVar fc nm + -- the inside of Raw atom : Parser Raw atom = RU <$> getPos <* keyword "U" - <|> RVar <$> getPos <*> ident + -- <|> RVar <$> getPos <*> ident + <|> asAtom <|> RVar <$> getPos <*> uident <|> lit <|> RImplicit <$> getPos <* keyword "_" diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index f10a5e9..81da8e0 100644 --- a/src/Lib/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -12,7 +12,7 @@ data Raw : Type where public export data Pattern = PatVar FC Icit Name - | PatCon FC Icit Name (List Pattern) + | PatCon FC Icit Name (List Pattern) (Maybe Name) | PatWild FC Icit -- Not handling this yet, but we need to be able to work with numbers and strings... | PatLit FC Literal @@ -20,7 +20,7 @@ data Pattern export getIcit : Pattern -> Icit getIcit (PatVar x icit str) = icit -getIcit (PatCon x icit str xs) = icit +getIcit (PatCon x icit str xs as) = icit getIcit (PatWild x icit) = icit getIcit (PatLit fc lit) = Explicit @@ -28,7 +28,7 @@ getIcit (PatLit fc lit) = Explicit export HasFC Pattern where getFC (PatVar fc _ _) = fc - getFC (PatCon fc _ _ _) = fc + getFC (PatCon fc _ _ _ _) = fc getFC (PatWild fc _) = fc getFC (PatLit fc lit) = fc @@ -78,6 +78,7 @@ data Raw : Type where RDo : (fc : FC) -> List DoStmt -> Raw RIf : (fc : FC) -> Raw -> Raw -> Raw -> Raw RWhere : (fc : FC) -> (List Decl) -> Raw -> Raw + RAs : (fc : FC) -> Name -> Raw -> Raw %name Raw tm @@ -98,6 +99,7 @@ HasFC Raw where getFC (RDo fc stmts) = fc getFC (RIf fc _ _ _) = fc getFC (RWhere fc _ _) = fc + getFC (RAs fc _ _) = fc -- derive some stuff - I'd like json, eq, show, ... @@ -187,7 +189,7 @@ Show Module where export Show Pattern where 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 (PatCon _ icit str xs as) = foo ["PatCon", show icit, show str, assert_total $ show xs, show as] show (PatWild _ icit) = foo ["PatWild", show icit] show (PatLit _ lit) = foo ["PatLit", show lit] @@ -214,6 +216,7 @@ Show Raw where show (RU _) = "U" show (RIf _ x y z) = foo [ "If", show x, show y, show z] show (RWhere _ _ _) = foo [ "Where", "FIXME"] + show (RAs _ nm x) = foo [ "RAs", nm, show x] export Pretty Literal where @@ -225,12 +228,11 @@ export Pretty Pattern where -- FIXME - wrap Implicit with {} pretty (PatVar _ icit nm) = text nm - pretty (PatCon _ icit nm args) = text nm <+> spread (map pretty args) + pretty (PatCon _ icit nm args Nothing) = text nm <+> spread (map pretty args) + pretty (PatCon _ icit nm args (Just as)) = text as ++ "@(" ++ text nm <+> spread (map pretty args) ++ ")" pretty (PatWild _icit) = "_" pretty (PatLit _ lit) = pretty lit - - export Pretty Raw where pretty = asDoc 0 @@ -269,6 +271,7 @@ 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 asDoc p (RWhere _ dd b) = text "TODO pretty where" + asDoc p (RAs _ nm x) = text nm ++ "@(" ++ asDoc 0 x ++ ")" export Pretty Decl where diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr index 2fb5507..33e8f61 100644 --- a/src/Lib/Tokenizer.idr +++ b/src/Lib/Tokenizer.idr @@ -11,7 +11,7 @@ keywords = ["let", "in", "where", "case", "of", "data", "U", "do", "∀", "forall", "class", "instance", "if", "then", "else", - "$", "λ", "?", + "$", "λ", "?", "@", "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_", "|"] checkKW : String -> Token Kind @@ -27,7 +27,7 @@ identMore : Lexer identMore = alphaNum <|> exact "'" <|> exact "_" singleton : Lexer -singleton = oneOf "()\\{}[],." +singleton = oneOf "()\\{}[],.@" quo : Recognise True quo = is '"' diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 62f0d4a..b64a718 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -449,6 +449,14 @@ record Context where -- FC to use if we don't have a better option fc : 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 ||| add a binding to environment