Add pattern matching for character literals (#322)

* Added pattern matching for character literals, plus a few tests for character literal patterns in function definitions and case statements

* Fixed CBV pattern-matching for characters

Author: DeSevilla

compiler/src/Language/Granule/Compiler/HSCodegen.hs

@@ -104,6 +104,8 @@ cgPat (GrPat.PInt _ _ _ n) =
   return $ PLit () (Signless ()) $ Int () (fromIntegral n) (show n)
 cgPat (GrPat.PFloat _ _ _ n) =
   return $ PLit () (Signless ()) $ Frac () (toRational n) (show n)
+cgPat (GrPat.PChar _ _ _ ch) =
+  return $ PLit () (Signless ()) $ Char () ch (show ch)
 cgPat (GrPat.PConstr _ _ _ i _ l_pt)
   | i == Id "," ","  = do
       pts <- mapM cgPat l_pt

frontend/src/Language/Granule/Checker/Patterns.hs

@@ -162,6 +162,13 @@ ctxtFromTypedPattern' outerCoeff s pos ty@(TyCon c) (PFloat s' _ rf n) _
     let elabP = PFloat s' ty rf n
     return ([], [], [], elabP, Full)
 
+ctxtFromTypedPattern' outerCoeff s pos ty@(TyCon c) (PChar s' _ rf ch) _
+  | internalName c == "Char" = do
+    definiteUnification s pos outerCoeff ty
+
+    let elabP = PChar s' ty rf ch
+    return ([], [], [], elabP, Full)
+
 -- Pattern match on a modal box
 ctxtFromTypedPattern' outerCoeffAndTy s pos t@(Box coeff ty) (PBox sp _ rf p) _ = do
     (innerCoeffTy, subst0, _) <- synthKind s coeff
@@ -476,4 +483,5 @@ duplicateBinderCheck s ps = case duplicateBinders of
       (\_ _ _ bs -> bs)
       (\_ _ _ _ -> [])
       (\_ _ _ _ -> [])
+      (\_ _ _ _ -> [])
       (\_ _ _ _ _ bss -> concat bss)

frontend/src/Language/Granule/Checker/Substitution.hs

@@ -433,6 +433,9 @@ instance Substitutable a => Substitutable (Pattern a) where
       (\sp ann rf doub -> do
           ann' <- substitute ctxt ann
           return $ PFloat sp ann' rf doub)
+      (\sp ann rf char -> do
+          ann' <- substitute ctxt ann
+          return $ PChar sp ann' rf char)
       (\sp ann rf nm tyVarBindsRequested pats -> do
           ann' <- substitute ctxt ann
           return $ PConstr sp ann' rf nm tyVarBindsRequested pats)

frontend/src/Language/Granule/Syntax/Parser.y

@@ -310,6 +310,9 @@ PAtom :: { Pattern () }
   | FLOAT
        {% (mkSpan $ getPosToSpan $1) >>= \sp -> return $ let TokenFloat _ x = $1 in PFloat sp () False $ read x }
 
+  | CHAR
+       {% (mkSpan $ getPosToSpan $1) >>= \sp -> return $ let TokenCharLiteral _ x = $1 in PChar sp () False x }
+
   | CONSTR
        {% (mkSpan $ getPosToSpan $1) >>= \sp -> return $ let TokenConstr _ x = $1 in PConstr sp () False (mkId x) [] [] }
 

frontend/src/Language/Granule/Syntax/Pattern.hs

@@ -26,6 +26,7 @@ data Pattern a
   | PWild Span a Bool                  -- ^ Wildcard (underscore) pattern
   | PBox Span a Bool (Pattern a)       -- ^ Box patterns
   | PInt Span a Bool Int               -- ^ Numeric patterns
+  | PChar Span a Bool Char
   | PFloat Span a Bool Double          -- ^ Float pattern
   | PConstr Span a Bool Id [Id] [Pattern a] -- ^ Constructor pattern
   deriving (Eq, Show, Generic, Functor, Typeable, Data)
@@ -50,17 +51,19 @@ patternFold
   -> (Span -> ann -> Bool -> b -> b)
   -> (Span -> ann -> Bool -> Int -> b)
   -> (Span -> ann -> Bool -> Double -> b)
+  -> (Span -> ann -> Bool -> Char -> b)
   -> (Span -> ann -> Bool -> Id -> [Id] -> [b] -> b)
   -> Pattern ann
   -> b
-patternFold v w b i f c = go
+patternFold v w b i f ch c = go
   where
     go = \case
       PVar sp ann rf nm -> v sp ann rf nm
       PWild sp ann rf  -> w sp ann rf
       PBox sp ann rf pat -> b sp ann rf (go pat)
       PInt sp ann rf int -> i sp ann rf int
       PFloat sp ann rf doub -> f sp ann rf doub
+      PChar sp ann rf char -> ch sp ann rf char
       PConstr sp ann rf nm tyVarBindsRequested pats -> c sp ann rf nm tyVarBindsRequested (go <$> pats)
 
 patternFoldM
@@ -70,10 +73,11 @@ patternFoldM
   -> (Span -> ann -> Bool -> b -> m b)
   -> (Span -> ann -> Bool -> Int -> m b)
   -> (Span -> ann -> Bool -> Double -> m b)
+  -> (Span -> ann -> Bool -> Char -> m b)
   -> (Span -> ann -> Bool -> Id -> [Id] -> [b] -> m b)
   -> Pattern ann
   -> m b
-patternFoldM v w b i f c = go
+patternFoldM v w b i f ch c = go
   where
     go = \case
       PVar sp ann rf nm -> v sp ann rf nm
@@ -84,6 +88,7 @@ patternFoldM v w b i f c = go
             b sp ann rf pat'
       PInt sp ann rf int -> i sp ann rf int
       PFloat sp ann rf doub -> f sp ann rf doub
+      PChar sp ann rf char -> ch sp ann rf char
       PConstr sp ann rf nm tyVarBindsRequested pats ->
         do
             pats' <- mapM go pats
@@ -96,16 +101,18 @@ boundVars PWild {}       = []
 boundVars (PBox _ _ _ p)     = boundVars p
 boundVars PInt {}        = []
 boundVars PFloat {}      = []
+boundVars PChar {}       = []
 boundVars (PConstr _ _ _ _ _ ps) = concatMap boundVars ps
 
 boundVarsAndAnnotations :: Pattern a -> [(a, Id)]
 boundVarsAndAnnotations =
-    patternFold var wild box int flt cstr
+    patternFold var wild box int flt char cstr
     where var _ ty _ ident  = [(ty, ident)]
           wild _ _ _        = []
           box _ _ _ pat     = pat
           int _ _ _ _       = []
           flt _ _ _ _       = []
+          char _ _ _ _      = []
           cstr _ _ _ _ _    = concat
 
 ppair :: Span
@@ -138,13 +145,15 @@ instance Freshenable m (Pattern a) where
   freshen p@PWild {} = return p
   freshen p@PInt {} = return p
   freshen p@PFloat {} = return p
+  freshen p@PChar {} = return p
 
 patRefactored :: Pattern a -> Bool
 patRefactored (PVar _ _ rf _) = rf
 patRefactored (PWild _ _ rf) = rf
 patRefactored (PBox _ _ rf _) = rf
 patRefactored (PInt _ _ rf _) = rf
 patRefactored (PFloat _ _ rf _) = rf
+patRefactored (PChar _ _ rf _) = rf
 patRefactored (PConstr _ _ rf _ _ _) = rf
 
 instance Rp.Refactorable (Pattern a) where

frontend/src/Language/Granule/Syntax/Pretty.hs

@@ -346,6 +346,7 @@ instance Pretty (Pattern a) where
     wlpretty (PBox _ _ _ p)     = P.brackets $ prettyNestedNew p
     wlpretty (PInt _ _ _ n)     = P.pretty (show n)
     wlpretty (PFloat _ _ _ n)   = P.pretty (show n)
+    wlpretty (PChar _ _ _ n)    = P.pretty (show n)
     wlpretty (PConstr _ _ _ name _ args) | internalName name == "," = P.parens $ mconcat $ P.punctuate ", " (map prettyNestedNew args)
     wlpretty (PConstr _ _ _ name tyVarBindsRequested args) =
       P.sep (wlpretty name : (map tyvarbinds tyVarBindsRequested ++ map prettyNestedNew args))

frontend/src/Language/Granule/Synthesis/LinearHaskell.hs

@@ -569,6 +569,7 @@ patternToHaskell (GrPat.PWild{})        = PWildCard noSrcSpan
 patternToHaskell (GrPat.PBox _ _ _ pt)  = patternToHaskell pt
 patternToHaskell (GrPat.PInt _ _ _ n)   = PLit noSrcSpan (Signless noSrcSpan) $ Int noSrcSpan (fromIntegral n) (show n)
 patternToHaskell (GrPat.PFloat _ _ _ n) = PLit noSrcSpan (Signless noSrcSpan) $ Frac noSrcSpan (toRational n) (show n)
+patternToHaskell (GrPat.PChar _ _ _ ch)  = PLit noSrcSpan (Signless noSrcSpan) $ Char noSrcSpan ch (show ch)
 patternToHaskell (GrPat.PConstr _ _ _ id@(GrId.Id _ i) _ l_pt)
   | ',' `elem` i = PTuple noSrcSpan Boxed $ map patternToHaskell (reverse l_pt)
   | otherwise = PApp noSrcSpan (UnQual noSrcSpan $ idToHaskell id) $ map patternToHaskell (reverse l_pt)

frontend/src/Language/Granule/Synthesis/Refactor.hs

@@ -96,6 +96,7 @@ refactorPattern (PBox sp a b p) id' subpat =
    in PBox sp a (patRefactored p') p'
 refactorPattern p@PInt {} _ _ = p
 refactorPattern p@PFloat {} _ _ = p
+refactorPattern p@PChar {} _ _ = p
 refactorPattern (PConstr sp a _ id names ps) id' subpat =
   let ps' = map (\p -> refactorPattern p id' subpat) ps
   in PConstr sp a (any patRefactored ps') id names ps'

frontend/src/Language/Granule/Synthesis/Synth.hs

@@ -341,6 +341,7 @@ synthesiseLinearBase hints index unrComps rComps defId ctxt constructors goalTy
       unannotatePat (PBox s a rf p)          = PBox s () rf $ unannotatePat p
       unannotatePat (PInt s a rf int)        = PInt s () rf int
       unannotatePat (PFloat s a rf doub)     = PFloat s () rf doub
+      unannotatePat (PChar s a rf ch)        = PChar s () rf ch
       unannotatePat (PConstr s a rf nm names pats) = PConstr s () rf nm names $ map unannotatePat pats
 
 

frontend/tests/cases/positive/simple/charcase.gr

@@ -0,0 +1,13 @@
+import Bool 
+-- Small example of case expressions in Granule
+constId : Int → Int
+constId x = case 'a' of 'a' → x
+
+constId2 : Int → Int
+constId2 x =
+    case '\n' of
+      '\n' → x;
+      '\t' → x
+
+main : Int
+main = constId 10 + constId2 20