operators in case patterns

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

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

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

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

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 ()
 

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

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