Isabelle/HOL translation: records and named patterns (#2963)

* Closes #2894 
* Closes #2895
* The translation of pattern matching on records is a bit tricky because
one cannot pattern match on records in Isabelle, except in top patterns
of function clauses. We thus need to translate into nested pattern
matching and record projections. Named patterns can be translated with a
similar technique and are also handled in this PR.

Checklist
---------
- [x] record creation
- [x] record projections
- [x] record update
- [x] top-level record patterns
- [x] nested record patterns
- [x] named patterns
- [x] remove redundant pattern matching clauses
- [x] remove redundant single-branch pattern matches

src/Juvix/Compiler/Backend/Isabelle/Extra.hs

@@ -1,8 +1,128 @@
 module Juvix.Compiler.Backend.Isabelle.Extra where
 
+import Data.List.NonEmpty.Extra qualified as NonEmpty
 import Juvix.Compiler.Backend.Isabelle.Language
 
 mkApp :: Expression -> [Expression] -> Expression
 mkApp fn = \case
   [] -> fn
   arg : args -> mkApp (ExprApp (Application fn arg)) args
+
+-- | Check if a pattern `pat1` subsumes another pattern `pat2`.
+subsumesPattern :: Pattern -> Pattern -> Bool
+subsumesPattern pat1 pat2 = case (pat1, pat2) of
+  (PatVar _, _) -> True
+  (PatZero, PatZero) -> True
+  (PatConstrApp (ConstrApp c1 p1), PatConstrApp (ConstrApp c2 p2)) ->
+    c1 == c2 && all (uncurry subsumesPattern) (zipExact p1 p2)
+  (PatTuple (Tuple p1), PatTuple (Tuple p2)) ->
+    length p1 == length p2
+      && all (uncurry subsumesPattern) (NonEmpty.zip p1 p2)
+  (PatList (List p1), PatList (List p2)) ->
+    length p1 == length p2
+      && all (uncurry subsumesPattern) (zipExact p1 p2)
+  (PatCons (Cons c1 p1), PatCons (Cons c2 p2)) ->
+    subsumesPattern c1 c2 && subsumesPattern p1 p2
+  (PatRecord (Record n1 r1), PatRecord (Record n2 r2)) ->
+    n1 == n2
+      && map ((^. nameText) . fst) r1' == map ((^. nameText) . fst) r2'
+      && all (uncurry subsumesPattern) (zipExact (map snd r1') (map snd r2'))
+    where
+      r1' = sortOn ((^. nameText) . fst) r1
+      r2' = sortOn ((^. nameText) . fst) r2
+  _ -> False
+
+-- | Rename all occurrences of a variable in an expression. Also renames bound
+-- variables.
+substVar :: Name -> Name -> Expression -> Expression
+substVar var var' = go
+  where
+    go :: Expression -> Expression
+    go = \case
+      ExprIden x -> goIden x
+      ExprUndefined -> ExprUndefined
+      ExprLiteral x -> ExprLiteral x
+      ExprApp x -> goApplication x
+      ExprBinop x -> goBinop x
+      ExprTuple x -> goTuple x
+      ExprList x -> goList x
+      ExprCons x -> goCons x
+      ExprRecord x -> goRecord x
+      ExprRecordUpdate x -> goRecordUpdate x
+      ExprLet x -> goLet x
+      ExprIf x -> goIf x
+      ExprCase x -> goCase x
+      ExprLambda x -> goLambda x
+
+    goName :: Name -> Name
+    goName x = if x ^. nameText == var ^. nameText then var' else x
+
+    goIden :: Name -> Expression
+    goIden = ExprIden . goName
+
+    goApplication :: Application -> Expression
+    goApplication (Application fn arg) =
+      ExprApp (Application (go fn) (go arg))
+
+    goBinop :: Binop -> Expression
+    goBinop Binop {..} =
+      ExprBinop
+        Binop
+          { _binopOperator,
+            _binopLeft = go _binopLeft,
+            _binopRight = go _binopRight,
+            _binopFixity
+          }
+
+    goTuple :: Tuple Expression -> Expression
+    goTuple (Tuple xs) = ExprTuple (Tuple (fmap go xs))
+
+    goList :: List Expression -> Expression
+    goList (List xs) = ExprList (List (map go xs))
+
+    goCons :: Cons Expression -> Expression
+    goCons (Cons h t) = ExprCons (Cons (go h) (go t))
+
+    goRecord' :: Record Expression -> Record Expression
+    goRecord' (Record n r) = Record n (map (second go) r)
+
+    goRecord :: Record Expression -> Expression
+    goRecord = ExprRecord . goRecord'
+
+    goRecordUpdate :: RecordUpdate -> Expression
+    goRecordUpdate (RecordUpdate r f) =
+      ExprRecordUpdate (RecordUpdate (go r) (goRecord' f))
+
+    goLet :: Let -> Expression
+    goLet (Let cs e) = ExprLet (Let (fmap goLetClause cs) (go e))
+
+    goLetClause :: LetClause -> LetClause
+    goLetClause (LetClause n e) = LetClause (goName n) (go e)
+
+    goIf :: If -> Expression
+    goIf (If v t f) = ExprIf (If (go v) (go t) (go f))
+
+    goCase :: Case -> Expression
+    goCase (Case v bs) = ExprCase (Case (go v) (fmap goCaseBranch bs))
+
+    goCaseBranch :: CaseBranch -> CaseBranch
+    goCaseBranch (CaseBranch p e) = CaseBranch (goPattern p) (go e)
+
+    goPattern :: Pattern -> Pattern
+    goPattern = \case
+      PatVar x -> PatVar (goName x)
+      PatZero -> PatZero
+      PatConstrApp (ConstrApp c p) -> PatConstrApp (ConstrApp c (fmap goPattern p))
+      PatTuple (Tuple p) -> PatTuple (Tuple (fmap goPattern p))
+      PatList (List p) -> PatList (List (fmap goPattern p))
+      PatCons (Cons h t) -> PatCons (Cons (goPattern h) (goPattern t))
+      PatRecord (Record n r) -> PatRecord (Record n (map (second goPattern) r))
+
+    goLambda :: Lambda -> Expression
+    goLambda Lambda {..} =
+      ExprLambda
+        Lambda
+          { _lambdaVar = goName _lambdaVar,
+            _lambdaBody = go _lambdaBody,
+            _lambdaType
+          }

src/Juvix/Compiler/Backend/Isabelle/Language.hs

@@ -55,6 +55,8 @@ data Expression
   | ExprTuple (Tuple Expression)
   | ExprList (List Expression)
   | ExprCons (Cons Expression)
+  | ExprRecord (Record Expression)
+  | ExprRecordUpdate RecordUpdate
   | ExprLet Let
   | ExprIf If
   | ExprCase Case
@@ -76,6 +78,11 @@ data Binop = Binop
     _binopFixity :: Fixity
   }
 
+data RecordUpdate = RecordUpdate
+  { _recordUpdateRecord :: Expression,
+    _recordUpdateFields :: Record Expression
+  }
+
 data Let = Let
   { _letClauses :: NonEmpty LetClause,
     _letBody :: Expression
@@ -115,6 +122,7 @@ data Pattern
   | PatTuple (Tuple Pattern)
   | PatList (List Pattern)
   | PatCons (Cons Pattern)
+  | PatRecord (Record Pattern)
 
 newtype Tuple a = Tuple
   { _tupleComponents :: NonEmpty a
@@ -129,6 +137,11 @@ data Cons a = Cons
     _consTail :: a
   }
 
+data Record a = Record
+  { _recordName :: Name,
+    _recordFields :: [(Name, a)]
+  }
+
 data ConstrApp = ConstrApp
   { _constrAppConstructor :: Name,
     _constrAppArgs :: [Pattern]
@@ -143,13 +156,19 @@ makeLenses ''CaseBranch
 makeLenses ''Lambda
 makeLenses ''ConstrApp
 makeLenses ''Expression
+makeLenses ''Binop
+makeLenses ''RecordUpdate
+makeLenses ''Tuple
+makeLenses ''List
+makeLenses ''Cons
+makeLenses ''Record
 
 data Statement
   = StmtDefinition Definition
   | StmtFunction Function
   | StmtSynonym Synonym
   | StmtDatatype Datatype
-  | StmtRecord Record
+  | StmtRecord RecordDef
 
 data Definition = Definition
   { _definitionName :: Name,
@@ -189,11 +208,11 @@ data Constructor = Constructor
     _constructorDocComment :: Maybe Text
   }
 
-data Record = Record
-  { _recordName :: Name,
-    _recordParams :: [TypeVar],
-    _recordFields :: [RecordField],
-    _recordDocComment :: Maybe Text
+data RecordDef = RecordDef
+  { _recordDefName :: Name,
+    _recordDefParams :: [TypeVar],
+    _recordDefFields :: [RecordField],
+    _recordDefDocComment :: Maybe Text
   }
 
 data RecordField = RecordField
@@ -207,9 +226,7 @@ makeLenses ''Function
 makeLenses ''Synonym
 makeLenses ''Datatype
 makeLenses ''Constructor
-makeLenses ''Record
 makeLenses ''RecordField
-makeLenses ''Tuple
 
 data Theory = Theory
   { _theoryName :: Name,
@@ -296,6 +313,8 @@ instance HasAtomicity Expression where
     ExprTuple {} -> Atom
     ExprList {} -> Atom
     ExprCons {} -> Aggregate consFixity
+    ExprRecord {} -> Aggregate appFixity
+    ExprRecordUpdate {} -> Aggregate appFixity
     ExprLet {} -> Aggregate letFixity
     ExprIf {} -> Aggregate ifFixity
     ExprCase {} -> Aggregate caseFixity
@@ -311,3 +330,4 @@ instance HasAtomicity Pattern where
     PatTuple {} -> Atom
     PatList {} -> Atom
     PatCons {} -> Aggregate consFixity
+    PatRecord {} -> Atom

src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs

@@ -102,6 +102,8 @@ instance PrettyCode Expression where
     ExprTuple x -> ppCode x
     ExprList x -> ppCode x
     ExprCons x -> ppCode x
+    ExprRecord x -> ppRecord False x
+    ExprRecordUpdate x -> ppCode x
     ExprLet x -> ppCode x
     ExprIf x -> ppCode x
     ExprCase x -> ppCode x
@@ -125,6 +127,12 @@ instance PrettyCode Binop where
     r <- ppRightExpression _binopFixity _binopRight
     return $ l <+> op <+> r
 
+instance PrettyCode RecordUpdate where
+  ppCode RecordUpdate {..} = do
+    r <- ppCode _recordUpdateRecord
+    fields <- ppRecord True _recordUpdateFields
+    return $ r <+> fields
+
 instance PrettyCode LetClause where
   ppCode LetClause {..} = do
     name <- ppCode _letClauseName
@@ -165,7 +173,17 @@ instance (PrettyCode a) => PrettyCode (Tuple a) where
 instance (PrettyCode a) => PrettyCode (List a) where
   ppCode List {..} = do
     elems <- mapM ppCode _listElements
-    return $ brackets $ hsep (punctuate comma (toList elems))
+    return $ brackets $ hsep (punctuate comma elems)
+
+ppRecord :: (PrettyCode a, Member (Reader Options) r) => Bool -> Record a -> Sem r (Doc Ann)
+ppRecord bUpdate Record {..} = do
+  recName <- ppCode _recordName
+  names <- mapM (ppCode . fst) _recordFields
+  elems <- mapM (ppCode . snd) _recordFields
+  let names' = map (\n -> recName <> "." <> n) names
+      eq = if bUpdate then ":=" else "="
+      fields = zipWithExact (\n e -> n <+> eq <+> e) names' elems
+  return $ "(|" <+> hsep (punctuate comma fields) <+> "|)"
 
 instance (PrettyCode a, HasAtomicity a) => PrettyCode (Cons a) where
   ppCode Cons {..} = do
@@ -181,6 +199,7 @@ instance PrettyCode Pattern where
     PatTuple x -> ppCode x
     PatList x -> ppCode x
     PatCons x -> ppCode x
+    PatRecord x -> ppRecord False x
 
 instance PrettyCode ConstrApp where
   ppCode ConstrApp {..} = do
@@ -253,12 +272,12 @@ instance PrettyCode Constructor where
     tys <- mapM ppCodeQuoted _constructorArgTypes
     return $ comment <> hsep (n : tys)
 
-instance PrettyCode Record where
-  ppCode Record {..} = do
-    let comment = prettyTextComment _recordDocComment
-    n <- ppCode _recordName
-    params <- ppParams _recordParams
-    fields <- mapM ppCode _recordFields
+instance PrettyCode RecordDef where
+  ppCode RecordDef {..} = do
+    let comment = prettyTextComment _recordDefDocComment
+    n <- ppCode _recordDefName
+    params <- ppParams _recordDefParams
+    fields <- mapM ppCode _recordDefFields
     return $ comment <> kwRecord <+> params <?+> n <+> "=" <> line <> indent' (vsep fields)
 
 instance PrettyCode RecordField where