Isabelle/HOL translation: records and named patterns

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