diff --git a/TODO.md b/TODO.md index 719255d..a193579 100644 --- a/TODO.md +++ b/TODO.md @@ -13,9 +13,9 @@ I may be done with `U` - I keep typing `Type`. - [x] implicit patterns - [x] operators - [x] pair syntax (via comma operator) -- [ ] matching on operators +- [x] matching on operators - [x] top level - - [ ] case statements ******** + - [x] case statements - [x] SKIP list syntax - Agda doesn't have it, clashes with pair syntax - [ ] import diff --git a/newt/oper.newt b/newt/oper.newt index 4517ee9..90aef54 100644 --- a/newt/oper.newt +++ b/newt/oper.newt @@ -42,3 +42,7 @@ blah x y z = (x, y, z) curryPlus : Pair Int Int -> Int curryPlus (a, b) = a + b + +caseCurry : Pair Int Int -> Int +caseCurry x = case x of + (a,b) => a + b diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index 14ff404..345ed5f 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -430,6 +430,35 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do rewriteClause vars (MkClause fc cons pats expr) = pure $ MkClause fc !(rewriteCons vars cons []) pats expr +splitArgs : Raw -> List (Raw, Icit) -> (Raw, List (Raw, Icit)) +splitArgs (RApp fc t u icit) args = splitArgs t ((u, icit) :: args) +splitArgs tm args = (tm, args) + + +mkPat : TopContext -> (Raw, Icit) -> M Pattern +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) + Just _ => error (getFC tm) "not a data constructor" + Nothing => case b of + [] => pure $ PatVar fc icit nm + _ => error (getFC tm) "patvar applied to args" + ((RImplicit fc), []) => pure $ PatWild fc icit + ((RImplicit fc), _) => error fc "implicit pat can't be applied" + -- ((RLit x y), b) => ?rhs_19 + (a,b) => error (getFC a) "expected pat var or constructor" + + +export +makeClause : TopContext -> (Raw, Raw) -> M Clause +makeClause top (lhs, rhs) = do + let (nm, args) = splitArgs lhs [] + pats <- traverse (mkPat top) args + pure $ MkClause (getFC lhs) [] pats rhs + lookupName : Context -> String -> Maybe (Tm, Val) lookupName ctx name = go 0 ctx.types @@ -505,8 +534,9 @@ check ctx tm ty = case (tm, !(forceType ty)) of debug "SCTM/TY \{pprint (names ctx) sc} \{show scty}" let scnm = fresh "sc" + top <- get -- FIXME FC - let clauses = map (\(MkAlt pat rawRHS) =>MkClause fc [(scnm, pat)] [] rawRHS ) alts + clauses <- traverse (\(MkAlt pat rawRHS) => pure $ MkClause fc [(scnm, !(mkPat top (pat, Explicit)))] [] rawRHS ) alts -- buildCase expects scrutinee to be a name in the context because -- it's compared against the first part of Constraint. We could switch diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 06d93f6..4e9975d 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -171,7 +171,7 @@ pPattern = PatCon (!getPos) Explicit <$> (uident <|> token MixFix) <*> many patA caseAlt : Parser RCaseAlt caseAlt = do - pat <- pPattern + pat <- typeExpr keyword "=>" t <- term pure $ MkAlt pat t diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 6b1edc4..21d2599 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -27,33 +27,6 @@ collectDecl ((Def fc nm cl) :: rest@(Def _ nm' cl' :: xs)) = else (Def fc nm cl :: collectDecl rest) collectDecl (x :: xs) = x :: collectDecl xs -makeClause : TopContext -> (Raw, Raw) -> M Clause -makeClause top (lhs, rhs) = do - let (nm, args) = splitArgs lhs [] - pats <- traverse mkPat args - pure $ MkClause (getFC lhs) [] pats rhs - where - - splitArgs : Raw -> List (Raw, Icit) -> (Raw, List (Raw, Icit)) - splitArgs (RApp fc t u icit) args = splitArgs t ((u, icit) :: args) - splitArgs tm args = (tm, args) - - mkPat : (Raw, Icit) -> M Pattern - mkPat (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 b) - Just _ => error (getFC tm) "not a data constructor" - Nothing => case b of - [] => pure $ PatVar fc icit nm - _ => error (getFC tm) "patvar applied to args" - ((RImplicit fc), []) => pure $ PatWild fc icit - ((RImplicit fc), _) => error fc "implicit pat can't be applied" - -- ((RLit x y), b) => ?rhs_19 - (a,b) => error (getFC a) "expected pat var or constructor" - export processDecl : Decl -> M () diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index 7f26c46..b7a5fc0 100644 --- a/src/Lib/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -57,7 +57,7 @@ record Clause where -- could be a pair, but I suspect stuff will be added? public export -data RCaseAlt = MkAlt Pattern Raw +data RCaseAlt = MkAlt Raw Raw data Raw : Type where RVar : FC -> (nm : Name) -> Raw diff --git a/tests/black/oper.newt b/tests/black/oper.newt index 339aa6e..2a32747 100644 --- a/tests/black/oper.newt +++ b/tests/black/oper.newt @@ -39,3 +39,11 @@ data Pair : U -> U -> U where blah : Int -> Int -> Int -> Pair Int (Pair Int Int) blah x y z = (x , y, z) + +curryPlus : Pair Int Int -> Int +curryPlus (a, b) = a + b + +-- case is different path, so separate test +caseCurry : Pair Int Int -> Int +caseCurry x = case x of + (a, b) => a + b