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
+data RecordDef = RecordDef
-  { _recordName :: Name,
+  { _recordDefName :: Name,
-    _recordParams :: [TypeVar],
+    _recordDefParams :: [TypeVar],
-    _recordFields :: [RecordField],
+    _recordDefFields :: [RecordField],
-    _recordDocComment :: Maybe Text
+    _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
+instance PrettyCode RecordDef where
-  ppCode Record {..} = do
+  ppCode RecordDef {..} = do
-    let comment = prettyTextComment _recordDocComment
+    let comment = prettyTextComment _recordDefDocComment
-    n <- ppCode _recordName
+    n <- ppCode _recordDefName
-    params <- ppParams _recordParams
+    params <- ppParams _recordDefParams
-    fields <- mapM ppCode _recordFields
+    fields <- mapM ppCode _recordDefFields
     return $ comment <> kwRecord <+> params <?+> n <+> "=" <> line <> indent' (vsep fields)
 
 instance PrettyCode RecordField where

src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs

@@ -2,6 +2,7 @@ module Juvix.Compiler.Backend.Isabelle.Translation.FromTyped where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
+import Data.List.NonEmpty.Extra qualified as NonEmpty
 import Data.Text qualified as T
 import Data.Text qualified as Text
 import Juvix.Compiler.Backend.Isabelle.Data.Result
@@ -21,12 +22,22 @@ newtype NameSet = NameSet
   }
 
 newtype NameMap = NameMap
-  { _nameMap :: HashMap Name Name
+  { _nameMap :: HashMap Name Expression
   }
 
 makeLenses ''NameSet
 makeLenses ''NameMap
 
+data Nested a = Nested
+  { _nestedElem :: a,
+    _nestedPatterns :: NestedPatterns
+  }
+  deriving stock (Functor)
+
+type NestedPatterns = [(Expression, Nested Pattern)]
+
+makeLenses ''Nested
+
 fromInternal ::
   forall r.
   (Members '[Error JuvixError, Reader EntryPoint, Reader ModuleTable, NameIdGen] r) =>
@@ -54,7 +65,7 @@ fromInternal Internal.InternalTypedResult {..} = do
 goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory
 goModule onlyTypes infoTable Internal.Module {..} =
   Theory
-    { _theoryName = over nameText toIsabelleName $ over namePretty toIsabelleName _moduleName,
+    { _theoryName = overNameText toIsabelleName _moduleName,
       _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
       _theoryStatements = case _modulePragmas ^. pragmasIsabelleIgnore of
         Just (PragmaIsabelleIgnore True) -> []
@@ -74,6 +85,24 @@ goModule onlyTypes infoTable Internal.Module {..} =
       StmtDatatype {} -> True
       StmtRecord {} -> True
 
+    mkExprCase :: Case -> Expression
+    mkExprCase c@Case {..} = case _caseValue of
+      ExprIden v ->
+        case _caseBranches of
+          CaseBranch {..} :| [] ->
+            case _caseBranchPattern of
+              PatVar v' -> substVar v' v _caseBranchBody
+              _ -> ExprCase c
+          _ -> ExprCase c
+      ExprTuple (Tuple (ExprIden v :| [])) ->
+        case _caseBranches of
+          CaseBranch {..} :| [] ->
+            case _caseBranchPattern of
+              PatTuple (Tuple (PatVar v' :| [])) -> substVar v' v _caseBranchBody
+              _ -> ExprCase c
+          _ -> ExprCase c
+      _ -> ExprCase c
+
     goMutualBlock :: Internal.MutualBlock -> [Statement]
     goMutualBlock Internal.MutualBlock {..} =
       filter (\stmt -> not onlyTypes || isTypeDef stmt) $
@@ -96,11 +125,11 @@ goModule onlyTypes infoTable Internal.Module {..} =
           && head' _inductiveConstructors ^. Internal.inductiveConstructorIsRecord =
           let tyargs = fst $ Internal.unfoldFunType $ head' _inductiveConstructors ^. Internal.inductiveConstructorType
            in StmtRecord
-                Record
+                RecordDef
-                  { _recordName = _inductiveName,
+                  { _recordDefName = _inductiveName,
-                    _recordParams = params,
+                    _recordDefParams = params,
-                    _recordFields = map goRecordField tyargs,
+                    _recordDefFields = map goRecordField tyargs,
-                    _recordDocComment = _inductiveDocComment
+                    _recordDefDocComment = _inductiveDocComment
                   }
       | otherwise =
           StmtDatatype
@@ -178,7 +207,7 @@ goModule onlyTypes infoTable Internal.Module {..} =
       -- We assume here that all clauses have the same number of patterns
       Just (Internal.ExpressionLambda Internal.Lambda {..})
         | not $ null $ filterTypeArgs 0 ty $ toList $ head _lambdaClauses ^. Internal.lambdaPatterns ->
-            fmap goClause _lambdaClauses
+            nonEmpty' $ goClauses $ toList _lambdaClauses
         | otherwise ->
             oneClause (goExpression'' nset (NameMap mempty) (head _lambdaClauses ^. Internal.lambdaBody))
       Just body -> oneClause (goExpression'' nset (NameMap mempty) body)
@@ -190,19 +219,113 @@ goModule onlyTypes infoTable Internal.Module {..} =
         oneClause expr =
           nonEmpty'
             [ Clause
-                { _clausePatterns = nonEmpty' $ map PatVar argnames,
+                { _clausePatterns = nonEmpty' (map PatVar argnames),
                   _clauseBody = expr
                 }
             ]
 
-        goClause :: Internal.LambdaClause -> Clause
+        goClauses :: [Internal.LambdaClause] -> [Clause]
-        goClause Internal.LambdaClause {..} =
+        goClauses = \case
-          Clause
+          Internal.LambdaClause {..} : cls ->
-            { _clausePatterns = nonEmpty' pats,
+            case npats0 of
-              _clauseBody = goExpression'' nset' nmap' _lambdaBody
+              Nested pats [] ->
+                Clause
+                  { _clausePatterns = nonEmpty' pats,
+                    _clauseBody = goExpression'' nset' nmap' _lambdaBody
+                  }
+                  : goClauses cls
+              Nested pats npats ->
+                let rhs = goExpression'' nset' nmap' _lambdaBody
+                    argnames' = fmap getPatternArgName _lambdaPatterns
+                    vnames =
+                      fmap
+                        ( \(idx :: Int, mname) ->
+                            maybe
+                              ( defaultName
+                                  ( disambiguate
+                                      (nset' ^. nameSet)
+                                      ("v_" <> show idx)
+                                  )
+                              )
+                              (overNameText (disambiguate (nset' ^. nameSet)))
+                              mname
+                        )
+                        (NonEmpty.zip (nonEmpty' [0 ..]) argnames')
+                    nset'' = foldl' (flip (over nameSet . HashSet.insert . (^. namePretty))) nset' vnames
+                    remainingBranches = goLambdaClauses'' nset'' nmap' cls
+                    valTuple = ExprTuple (Tuple (fmap ExprIden vnames))
+                    patTuple = PatTuple (Tuple (nonEmpty' pats))
+                    brs = goNestedBranches valTuple rhs remainingBranches patTuple (nonEmpty' npats)
+                 in [ Clause
+                        { _clausePatterns = fmap PatVar vnames,
+                          _clauseBody =
+                            mkExprCase
+                              Case
+                                { _caseValue = valTuple,
+                                  _caseBranches = brs
+                                }
+                        }
+                    ]
+            where
+              (npats0, nset', nmap') = goPatternArgsTop (filterTypeArgs 0 ty (toList _lambdaPatterns))
+          [] -> []
+
+    goNestedBranches :: Expression -> Expression -> [CaseBranch] -> Pattern -> NonEmpty (Expression, Nested Pattern) -> NonEmpty CaseBranch
+    goNestedBranches caseVal rhs remainingBranches pat npats =
+      let val = ExprTuple (Tuple (fmap fst npats))
+          pat' = PatTuple (Tuple (fmap ((^. nestedElem) . snd) npats))
+          npats' = concatMap ((^. nestedPatterns) . snd) npats
+          brs = goNestedBranches' rhs (mkDefaultBranch caseVal remainingBranches) (Nested pat' npats')
+          remainingBranches' = filter (not . subsumesPattern pat . (^. caseBranchPattern)) remainingBranches
+       in CaseBranch
+            { _caseBranchPattern = pat,
+              _caseBranchBody =
+                mkExprCase
+                  Case
+                    { _caseValue = val,
+                      _caseBranches = brs
+                    }
             }
-          where
+            :| remainingBranches'
-            (pats, nset', nmap') = goPatternArgs'' (filterTypeArgs 0 ty (toList _lambdaPatterns))
+
+    mkDefaultBranch :: Expression -> [CaseBranch] -> Maybe CaseBranch
+    mkDefaultBranch val remainingBranches = case remainingBranches of
+      [] -> Nothing
+      _ ->
+        Just $
+          CaseBranch
+            { _caseBranchPattern = PatVar (defaultName "_"),
+              _caseBranchBody =
+                mkExprCase
+                  Case
+                    { _caseValue = val,
+                      _caseBranches = nonEmpty' remainingBranches
+                    }
+            }
+
+    goNestedBranches' :: Expression -> Maybe CaseBranch -> Nested Pattern -> NonEmpty CaseBranch
+    goNestedBranches' rhs defaultBranch = \case
+      Nested pat [] ->
+        CaseBranch
+          { _caseBranchPattern = pat,
+            _caseBranchBody = rhs
+          }
+          :| toList defaultBranch
+      Nested pat npats -> do
+        let val = ExprTuple (Tuple (nonEmpty' (map fst npats)))
+            pat' = PatTuple (Tuple (nonEmpty' (map ((^. nestedElem) . snd) npats)))
+            npats' = concatMap ((^. nestedPatterns) . snd) npats
+            brs = goNestedBranches' rhs defaultBranch (Nested pat' npats')
+         in CaseBranch
+              { _caseBranchPattern = pat,
+                _caseBranchBody =
+                  mkExprCase
+                    Case
+                      { _caseValue = val,
+                        _caseBranches = brs
+                      }
+              }
+              :| toList defaultBranch
 
     goFunctionDef :: Internal.FunctionDef -> Statement
     goFunctionDef Internal.FunctionDef {..} = goDef _funDefName _funDefType _funDefArgsInfo (Just _funDefBody) _funDefDocComment
@@ -290,24 +413,30 @@ goModule onlyTypes infoTable Internal.Module {..} =
             _ -> overNameText quote name
         Nothing -> overNameText quote name
 
-    goFunName :: Name -> Name
+    getArgtys :: Internal.ConstructorInfo -> [Internal.FunctionParameter]
-    goFunName name =
+    getArgtys ctrInfo = fst $ Internal.unfoldFunType $ ctrInfo ^. Internal.constructorInfoType
-      case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of
-        Just funInfo ->
-          case funInfo ^. Internal.functionInfoPragmas . pragmasIsabelleFunction of
-            Just PragmaIsabelleFunction {..} -> setNameText _pragmaIsabelleFunctionName name
-            Nothing -> overNameText quote name
-        Nothing -> overNameText quote name
 
-    lookupName :: forall r. (Member (Reader NameMap) r) => Name -> Sem r Name
+    goFunName :: Expression -> Expression
+    goFunName = \case
+      ExprIden name ->
+        ExprIden $
+          case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of
+            Just funInfo ->
+              case funInfo ^. Internal.functionInfoPragmas . pragmasIsabelleFunction of
+                Just PragmaIsabelleFunction {..} -> setNameText _pragmaIsabelleFunctionName name
+                Nothing -> overNameText quote name
+            Nothing -> overNameText quote name
+      x -> x
+
+    lookupName :: forall r. (Member (Reader NameMap) r) => Name -> Sem r Expression
     lookupName name = do
       nmap <- asks (^. nameMap)
-      return $ fromMaybe name $ HashMap.lookup name nmap
+      return $ fromMaybe (ExprIden name) $ HashMap.lookup name nmap
 
     localName :: forall a r. (Members '[Reader NameSet, Reader NameMap] r) => Name -> Name -> Sem r a -> Sem r a
     localName v v' =
       local (over nameSet (HashSet.insert (v' ^. namePretty)))
-        . local (over nameMap (HashMap.insert v v'))
+        . local (over nameMap (HashMap.insert v (ExprIden v')))
 
     localNames :: forall a r. (Members '[Reader NameSet, Reader NameMap] r) => [(Name, Name)] -> Sem r a -> Sem r a
     localNames vs e = foldl' (flip (uncurry localName)) e vs
@@ -316,6 +445,11 @@ goModule onlyTypes infoTable Internal.Module {..} =
     withLocalNames nset nmap =
       local (const nset) . local (const nmap)
 
+    goRecordFields :: [Internal.FunctionParameter] -> [a] -> [(Name, a)]
+    goRecordFields argtys args = case (argtys, args) of
+      (ty : argtys', arg' : args') -> (fromMaybe (defaultName "_") (ty ^. Internal.paramName), arg') : goRecordFields argtys' args'
+      _ -> []
+
     goExpression' :: Internal.Expression -> Expression
     goExpression' = goExpression'' (NameSet mempty) (NameMap mempty)
 
@@ -340,8 +474,7 @@ goModule onlyTypes infoTable Internal.Module {..} =
         goIden :: Internal.Iden -> Sem r Expression
         goIden iden = case iden of
           Internal.IdenFunction name -> do
-            name' <- lookupName name
+            goFunName <$> lookupName name
-            return $ ExprIden (goFunName name')
           Internal.IdenConstructor name ->
             case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
               Just ctrInfo ->
@@ -350,8 +483,7 @@ goModule onlyTypes infoTable Internal.Module {..} =
                   _ -> return $ ExprIden (goConstrName name)
               Nothing -> return $ ExprIden (goConstrName name)
           Internal.IdenVar name -> do
-            name' <- lookupName name
+            lookupName name
-            return $ ExprIden name'
           Internal.IdenAxiom name -> return $ ExprIden (overNameText quote name)
           Internal.IdenInductive name -> return $ ExprIden (overNameText quote name)
 
@@ -388,6 +520,19 @@ goModule onlyTypes infoTable Internal.Module {..} =
               x' <- goExpression x
               y' <- goExpression y
               return $ ExprTuple (Tuple (x' :| [y']))
+          | Just (name, fields) <- getRecordCreation app = do
+              fields' <- mapM (secondM goExpression) fields
+              return $ ExprRecord (Record name fields')
+          | Just (indName, names, record, fields) <- getRecordUpdate app = do
+              record' <- goExpression record
+              let names' = map (qualifyRecordProjection indName) names
+              nset <- ask @NameSet
+              nmap <- ask @NameMap
+              let nset' = foldl' (flip (over nameSet . HashSet.insert . (^. namePretty))) nset names'
+                  exprs = map (\n -> ExprApp (Application (ExprIden n) record')) names'
+                  nmap' = foldl' (flip (over nameMap . uncurry HashMap.insert)) nmap (zipExact names exprs)
+              fields' <- mapM (secondM (withLocalNames nset' nmap' . goExpression)) fields
+              return $ ExprRecordUpdate (RecordUpdate record' (Record indName fields'))
           | Just (fn, args) <- getIdentApp app = do
               fn' <- goExpression fn
               args' <- mapM goExpression args
@@ -542,6 +687,47 @@ goModule onlyTypes infoTable Internal.Module {..} =
           where
             (fn, args) = Internal.unfoldApplication app
 
+        getRecordCreation :: Internal.Application -> Maybe (Name, [(Name, Internal.Expression)])
+        getRecordCreation app = case fn of
+          Internal.ExpressionIden (Internal.IdenConstructor name) ->
+            case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
+              Just ctrInfo
+                | ctrInfo ^. Internal.constructorInfoRecord ->
+                    Just (indName, goRecordFields (getArgtys ctrInfo) (toList args))
+                where
+                  indName = ctrInfo ^. Internal.constructorInfoInductive
+              _ -> Nothing
+          _ -> Nothing
+          where
+            (fn, args) = Internal.unfoldApplication app
+
+        getRecordUpdate :: Internal.Application -> Maybe (Name, [Name], Internal.Expression, [(Name, Internal.Expression)])
+        getRecordUpdate Internal.Application {..} = case _appLeft of
+          Internal.ExpressionLambda Internal.Lambda {..} -> case _lambdaClauses of
+            Internal.LambdaClause {..} :| [] -> case fmap (^. Internal.patternArgPattern) _lambdaPatterns of
+              Internal.PatternConstructorApp Internal.ConstructorApp {..} :| []
+                | all isPatternArgVar _constrAppParameters ->
+                    case _lambdaBody of
+                      Internal.ExpressionApplication app -> case fn of
+                        Internal.ExpressionIden (Internal.IdenConstructor name')
+                          | name' == _constrAppConstructor ->
+                              case HashMap.lookup name' (infoTable ^. Internal.infoConstructors) of
+                                Just ctrInfo
+                                  | ctrInfo ^. Internal.constructorInfoRecord ->
+                                      let names = map (fromJust . getPatternArgName) _constrAppParameters
+                                          fields = goRecordFields (getArgtys ctrInfo) (toList args)
+                                          fields' = zipWithExact (\n (n', e) -> (setNameText (n' ^. namePretty) n, e)) names fields
+                                          fields'' = filter (\(n, e) -> e /= Internal.ExpressionIden (Internal.IdenVar n)) fields'
+                                       in Just (ctrInfo ^. Internal.constructorInfoInductive, map fst fields', _appRight, fields'')
+                                _ -> Nothing
+                        _ -> Nothing
+                        where
+                          (fn, args) = Internal.unfoldApplication app
+                      _ -> Nothing
+              _ -> Nothing
+            _ -> Nothing
+          _ -> Nothing
+
         getIdentApp :: Internal.Application -> Maybe (Internal.Expression, [Internal.Expression])
         getIdentApp app = case mty of
           Just (ty, paramsNum) -> Just (fn, args')
@@ -581,7 +767,6 @@ goModule onlyTypes infoTable Internal.Module {..} =
         goInstanceHole :: Internal.InstanceHole -> Sem r Expression
         goInstanceHole _ = return ExprUndefined
 
-        -- TODO: binders
         goLet :: Internal.Let -> Sem r Expression
         goLet Internal.Let {..} = do
           let fdefs = concatMap toFunDefs (toList _letClauses)
@@ -632,10 +817,10 @@ goModule onlyTypes infoTable Internal.Module {..} =
 
         goLambda :: Internal.Lambda -> Sem r Expression
         goLambda Internal.Lambda {..}
-          | npats == 0 = goExpression (head _lambdaClauses ^. Internal.lambdaBody)
+          | patsNum == 0 = goExpression (head _lambdaClauses ^. Internal.lambdaBody)
           | otherwise = goLams vars
           where
-            npats =
+            patsNum =
               case _lambdaType of
                 Just ty ->
                   length
@@ -647,7 +832,7 @@ goModule onlyTypes infoTable Internal.Module {..} =
                     . filter ((/= Internal.Implicit) . (^. Internal.patternArgIsImplicit))
                     . toList
                     $ head _lambdaClauses ^. Internal.lambdaPatterns
-            vars = map (\i -> defaultName ("x" <> show i)) [0 .. npats - 1]
+            vars = map (\i -> defaultName ("x" <> show i)) [0 .. patsNum - 1]
 
             goLams :: [Name] -> Sem r Expression
             goLams = \case
@@ -668,128 +853,239 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 val <-
                   case vars of
                     [v] -> do
-                      v' <- lookupName v
+                      lookupName v
-                      return $ ExprIden v'
                     _ -> do
                       vars' <- mapM lookupName vars
                       return $
                         ExprTuple
                           Tuple
-                            { _tupleComponents = nonEmpty' $ map ExprIden vars'
+                            { _tupleComponents = nonEmpty' vars'
                             }
-                brs <- mapM goClause _lambdaClauses
+                brs <- goLambdaClauses (toList _lambdaClauses)
                 return $
-                  ExprCase
+                  mkExprCase
                     Case
                       { _caseValue = val,
-                        _caseBranches = brs
+                        _caseBranches = nonEmpty' brs
                       }
 
-            goClause :: Internal.LambdaClause -> Sem r CaseBranch
-            goClause Internal.LambdaClause {..} = do
-              (pat, nset, nmap) <- case _lambdaPatterns of
-                p :| [] -> goPatternArg' p
-                _ -> do
-                  (pats, nset, nmap) <- goPatternArgs' (toList _lambdaPatterns)
-                  let pat =
-                        PatTuple
-                          Tuple
-                            { _tupleComponents = nonEmpty' pats
-                            }
-                  return (pat, nset, nmap)
-              body <- withLocalNames nset nmap $ goExpression _lambdaBody
-              return $
-                CaseBranch
-                  { _caseBranchPattern = pat,
-                    _caseBranchBody = body
-                  }
-
         goCase :: Internal.Case -> Sem r Expression
         goCase Internal.Case {..} = do
           val <- goExpression _caseExpression
-          brs <- mapM goCaseBranch _caseBranches
+          brs <- goCaseBranches (toList _caseBranches)
           return $
-            ExprCase
+            mkExprCase
               Case
                 { _caseValue = val,
-                  _caseBranches = brs
+                  _caseBranches = nonEmpty' brs
                 }
 
-        goCaseBranch :: Internal.CaseBranch -> Sem r CaseBranch
+        goCaseBranches :: [Internal.CaseBranch] -> Sem r [CaseBranch]
-        goCaseBranch Internal.CaseBranch {..} = do
+        goCaseBranches = \case
-          (pat, nset, nmap) <- goPatternArg' _caseBranchPattern
+          Internal.CaseBranch {..} : brs -> do
-          rhs <- withLocalNames nset nmap $ goCaseBranchRhs _caseBranchRhs
+            (npat, nset, nmap) <- goPatternArgCase _caseBranchPattern
-          return $
+            case npat of
-            CaseBranch
+              Nested pat [] -> do
-              { _caseBranchPattern = pat,
+                rhs <- withLocalNames nset nmap $ goCaseBranchRhs _caseBranchRhs
-                _caseBranchBody = rhs
+                brs' <- goCaseBranches brs
-              }
+                return $
+                  CaseBranch
+                    { _caseBranchPattern = pat,
+                      _caseBranchBody = rhs
+                    }
+                    : brs'
+              Nested pat npats -> do
+                let vname = defaultName (disambiguate (nset ^. nameSet) "v")
+                    nset' = over nameSet (HashSet.insert (vname ^. namePretty)) nset
+                rhs <- withLocalNames nset' nmap $ goCaseBranchRhs _caseBranchRhs
+                remainingBranches <- withLocalNames nset' nmap $ goCaseBranches brs
+                let brs' = goNestedBranches (ExprIden vname) rhs remainingBranches pat (nonEmpty' npats)
+                return
+                  [ CaseBranch
+                      { _caseBranchPattern = PatVar vname,
+                        _caseBranchBody =
+                          mkExprCase
+                            Case
+                              { _caseValue = ExprIden vname,
+                                _caseBranches = brs'
+                              }
+                      }
+                  ]
+          [] -> return []
 
         goCaseBranchRhs :: Internal.CaseBranchRhs -> Sem r Expression
         goCaseBranchRhs = \case
           Internal.CaseBranchRhsExpression e -> goExpression e
           Internal.CaseBranchRhsIf {} -> error "unsupported: side conditions"
 
-    goPatternArgs'' :: [Internal.PatternArg] -> ([Pattern], NameSet, NameMap)
+    goLambdaClauses'' :: NameSet -> NameMap -> [Internal.LambdaClause] -> [CaseBranch]
-    goPatternArgs'' pats =
+    goLambdaClauses'' nset nmap cls =
-      (pats', nset, nmap)
+      run $ runReader nset $ runReader nmap $ goLambdaClauses cls
-      where
-        (nset, (nmap, pats')) = run $ runState (NameSet mempty) $ runState (NameMap mempty) $ goPatternArgs pats
 
-    goPatternArg' :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => Internal.PatternArg -> Sem r (Pattern, NameSet, NameMap)
+    goLambdaClauses :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => [Internal.LambdaClause] -> Sem r [CaseBranch]
-    goPatternArg' pat = do
+    goLambdaClauses = \case
+      Internal.LambdaClause {..} : cls -> do
+        (npat, nset, nmap) <- case _lambdaPatterns of
+          p :| [] -> goPatternArgCase p
+          _ -> do
+            (npats, nset, nmap) <- goPatternArgsCase (toList _lambdaPatterns)
+            let npat =
+                  fmap
+                    ( \pats ->
+                        PatTuple
+                          Tuple
+                            { _tupleComponents = nonEmpty' pats
+                            }
+                    )
+                    npats
+            return (npat, nset, nmap)
+        case npat of
+          Nested pat [] -> do
+            body <- withLocalNames nset nmap $ goExpression _lambdaBody
+            brs <- goLambdaClauses cls
+            return $
+              CaseBranch
+                { _caseBranchPattern = pat,
+                  _caseBranchBody = body
+                }
+                : brs
+          Nested pat npats -> do
+            let vname = defaultName (disambiguate (nset ^. nameSet) "v")
+                nset' = over nameSet (HashSet.insert (vname ^. namePretty)) nset
+            rhs <- withLocalNames nset' nmap $ goExpression _lambdaBody
+            remainingBranches <- withLocalNames nset' nmap $ goLambdaClauses cls
+            let brs' = goNestedBranches (ExprIden vname) rhs remainingBranches pat (nonEmpty' npats)
+            return
+              [ CaseBranch
+                  { _caseBranchPattern = PatVar vname,
+                    _caseBranchBody =
+                      mkExprCase
+                        Case
+                          { _caseValue = ExprIden vname,
+                            _caseBranches = brs'
+                          }
+                  }
+              ]
+      [] -> return []
+
+    isPatternArgVar :: Internal.PatternArg -> Bool
+    isPatternArgVar Internal.PatternArg {..} =
+      case _patternArgPattern of
+        Internal.PatternVariable {} -> True
+        _ -> False
+
+    getPatternArgName :: Internal.PatternArg -> Maybe Name
+    getPatternArgName Internal.PatternArg {..} =
+      case _patternArgPattern of
+        Internal.PatternVariable name -> Just name
+        _ -> _patternArgName
+
+    goPatternArgsTop :: [Internal.PatternArg] -> (Nested [Pattern], NameSet, NameMap)
+    goPatternArgsTop pats =
+      (Nested pats' npats, nset, nmap)
+      where
+        (npats, (nset, (nmap, pats'))) = run $ runOutputList $ runState (NameSet mempty) $ runState (NameMap mempty) $ goPatternArgs True pats
+
+    goPatternArgCase :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => Internal.PatternArg -> Sem r (Nested Pattern, NameSet, NameMap)
+    goPatternArgCase pat = do
       nset <- ask @NameSet
       nmap <- ask @NameMap
-      let (nmap', (nset', pat')) = run $ runState nmap $ runState nset $ goPatternArg pat
+      let (npats, (nmap', (nset', pat'))) = run $ runOutputList $ runState nmap $ runState nset $ goPatternArg False pat
-      return (pat', nset', nmap')
+      return (Nested pat' npats, nset', nmap')
 
-    goPatternArgs' :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => [Internal.PatternArg] -> Sem r ([Pattern], NameSet, NameMap)
+    goPatternArgsCase :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => [Internal.PatternArg] -> Sem r (Nested [Pattern], NameSet, NameMap)
-    goPatternArgs' pats = do
+    goPatternArgsCase pats = do
       nset <- ask @NameSet
       nmap <- ask @NameMap
-      let (nmap', (nset', pats')) = run $ runState nmap $ runState nset $ goPatternArgs pats
+      let (npats, (nmap', (nset', pats'))) = run $ runOutputList $ runState nmap $ runState nset $ goPatternArgs False pats
-      return (pats', nset', nmap')
+      return (Nested pats' npats, nset', nmap')
 
-    goPatternArgs :: forall r. (Members '[State NameSet, State NameMap] r) => [Internal.PatternArg] -> Sem r [Pattern]
+    goPatternArgs :: forall r. (Members '[State NameSet, State NameMap, Output (Expression, Nested Pattern)] r) => Bool -> [Internal.PatternArg] -> Sem r [Pattern]
-    goPatternArgs = mapM goPatternArg
+    goPatternArgs isTop = mapM (goPatternArg isTop)
 
-    -- TODO: named patterns (`_patternArgName`) are not handled properly
+    goPatternArg :: forall r. (Members '[State NameSet, State NameMap, Output (Expression, Nested Pattern)] r) => Bool -> Internal.PatternArg -> Sem r Pattern
-    goPatternArg :: forall r. (Members '[State NameSet, State NameMap] r) => Internal.PatternArg -> Sem r Pattern
+    goPatternArg isTop Internal.PatternArg {..}
-    goPatternArg Internal.PatternArg {..} =
+      | Just name <- _patternArgName = do
-      goPattern _patternArgPattern
+          binders <- gets (^. nameSet)
+          let name' = overNameText (disambiguate binders) name
+          modify' (over nameSet (HashSet.insert (name' ^. namePretty)))
+          modify' (over nameMap (HashMap.insert name (ExprIden name')))
+          npat <- goNestedPattern _patternArgPattern
+          output (ExprIden name', npat)
+          return $ PatVar name'
+      | otherwise =
+          goPattern isTop _patternArgPattern
+
+    goNestedPatternArg :: forall r. (Members '[State NameSet, State NameMap] r) => Internal.PatternArg -> Sem r (Nested Pattern)
+    goNestedPatternArg Internal.PatternArg {..}
+      | Just name <- _patternArgName = do
+          binders <- gets (^. nameSet)
+          let name' = overNameText (disambiguate binders) name
+          modify' (over nameSet (HashSet.insert (name' ^. namePretty)))
+          modify' (over nameMap (HashMap.insert name (ExprIden name')))
+          npat <- goNestedPattern _patternArgPattern
+          return $ Nested (PatVar name') [(ExprIden name', npat)]
+      | otherwise =
+          goNestedPattern _patternArgPattern
+
+    goNestedPattern :: forall r. (Members '[State NameSet, State NameMap] r) => Internal.Pattern -> Sem r (Nested Pattern)
+    goNestedPattern pat = do
+      (npats, pat') <- runOutputList $ goPattern False pat
+      return $ Nested pat' npats
+
+    goPattern :: forall r. (Members '[State NameSet, State NameMap, Output (Expression, Nested Pattern)] r) => Bool -> Internal.Pattern -> Sem r Pattern
+    goPattern isTop = \case
+      Internal.PatternVariable name -> do
+        binders <- gets (^. nameSet)
+        let name' = overNameText (disambiguate binders) name
+        modify' (over nameSet (HashSet.insert (name' ^. namePretty)))
+        modify' (over nameMap (HashMap.insert name (ExprIden name')))
+        return $ PatVar name'
+      Internal.PatternConstructorApp x -> goPatternConstructorApp x
+      Internal.PatternWildcardConstructor {} -> impossible
       where
-        goPattern :: Internal.Pattern -> Sem r Pattern
-        goPattern = \case
-          Internal.PatternVariable name -> do
-            binders <- gets (^. nameSet)
-            let name' = overNameText (disambiguate binders) name
-            modify' (over nameSet (HashSet.insert (name' ^. namePretty)))
-            modify' (over nameMap (HashMap.insert name name'))
-            return $ PatVar name'
-          Internal.PatternConstructorApp x -> goPatternConstructorApp x
-          Internal.PatternWildcardConstructor {} -> impossible
-
         goPatternConstructorApp :: Internal.ConstructorApp -> Sem r Pattern
         goPatternConstructorApp Internal.ConstructorApp {..}
           | Just lst <- getListPat _constrAppConstructor _constrAppParameters = do
-              pats <- goPatternArgs lst
+              pats <- goPatternArgs False lst
               return $ PatList (List pats)
           | Just (x, y) <- getConsPat _constrAppConstructor _constrAppParameters = do
-              x' <- goPatternArg x
+              x' <- goPatternArg False x
-              y' <- goPatternArg y
+              y' <- goPatternArg False y
               return $ PatCons (Cons x' y')
+          | Just (indName, fields) <- getRecordPat _constrAppConstructor _constrAppParameters =
+              if
+                  | isTop -> do
+                      fields' <- mapM (secondM (goPatternArg False)) fields
+                      return $ PatRecord (Record indName fields')
+                  | otherwise -> do
+                      binders <- gets (^. nameSet)
+                      let adjustName :: Name -> Expression
+                          adjustName name =
+                            let name' = qualifyRecordProjection indName name
+                             in ExprApp (Application (ExprIden name') (ExprIden vname))
+                          vname = defaultName (disambiguate binders "v")
+                          fieldsVars = map (second (fromJust . getPatternArgName)) $ map (first adjustName) $ filter (isPatternArgVar . snd) fields
+                          fieldsNonVars = map (first adjustName) $ filter (not . isPatternArgVar . snd) fields
+                      modify' (over nameSet (HashSet.insert (vname ^. namePretty)))
+                      forM fieldsVars $ \(e, fname) -> do
+                        modify' (over nameSet (HashSet.insert (fname ^. namePretty)))
+                        modify' (over nameMap (HashMap.insert fname e))
+                      fieldsNonVars' <- mapM (secondM goNestedPatternArg) fieldsNonVars
+                      forM fieldsNonVars' output
+                      return (PatVar vname)
           | Just (x, y) <- getPairPat _constrAppConstructor _constrAppParameters = do
-              x' <- goPatternArg x
+              x' <- goPatternArg False x
-              y' <- goPatternArg y
+              y' <- goPatternArg False y
               return $ PatTuple (Tuple (x' :| [y']))
           | Just p <- getNatPat _constrAppConstructor _constrAppParameters =
               case p of
                 Left zero -> return zero
                 Right arg -> do
-                  arg' <- goPatternArg arg
+                  arg' <- goPatternArg False arg
                   return (PatConstrApp (ConstrApp (goConstrName _constrAppConstructor) [arg']))
           | otherwise = do
-              args <- mapM goPatternArg _constrAppParameters
+              args <- mapM (goPatternArg False) _constrAppParameters
               return $
                 PatConstrApp
                   ConstrApp
@@ -824,6 +1120,16 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 _ -> Nothing
             Nothing -> Nothing
 
+        getRecordPat :: Name -> [Internal.PatternArg] -> Maybe (Name, [(Name, Internal.PatternArg)])
+        getRecordPat name args =
+          case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
+            Just ctrInfo
+              | ctrInfo ^. Internal.constructorInfoRecord ->
+                  Just (indName, goRecordFields (getArgtys ctrInfo) args)
+              where
+                indName = ctrInfo ^. Internal.constructorInfoInductive
+            _ -> Nothing
+
         getNatPat :: Name -> [Internal.PatternArg] -> Maybe (Either Pattern Internal.PatternArg)
         getNatPat name args =
           case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of
@@ -868,6 +1174,10 @@ goModule onlyTypes infoTable Internal.Module {..} =
               _nameIdModuleId = defaultModuleId
             }
 
+    qualifyRecordProjection :: Name -> Name -> Name
+    qualifyRecordProjection indName name =
+      setNameText (indName ^. namePretty <> "." <> name ^. namePretty) name
+
     setNameText :: Text -> Name -> Name
     setNameText txt name =
       set namePretty txt
@@ -881,39 +1191,39 @@ goModule onlyTypes infoTable Internal.Module {..} =
         $ name
 
     disambiguate :: HashSet Text -> Text -> Text
-    disambiguate binders = disambiguate' binders . quote
+    disambiguate binders = disambiguate' . quote
+      where
+        disambiguate' :: Text -> Text
+        disambiguate' name
+          | name == "?" || name == "" || name == "_" =
+              disambiguate' "X"
+          | HashSet.member name binders
+              || HashSet.member name names =
+              disambiguate' (prime name)
+          | otherwise =
+              name
 
-    disambiguate' :: HashSet Text -> Text -> Text
+        names :: HashSet Text
-    disambiguate' binders name
+        names =
-      | name == "?" || name == "" || name == "_" =
+          HashSet.fromList $
-          disambiguate' binders "X"
+            map quote $
-      | HashSet.member name binders
+              map (^. Internal.functionInfoName . namePretty) (filter (not . (^. Internal.functionInfoIsLocal)) (HashMap.elems (infoTable ^. Internal.infoFunctions)))
-          || HashSet.member name names =
+                ++ map (^. Internal.constructorInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoConstructors))
-          disambiguate' binders (prime name)
+                ++ map (^. Internal.inductiveInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoInductives))
-      | otherwise =
+                ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms))
-          name
-
-    names :: HashSet Text
-    names =
-      HashSet.fromList $
-        map quote $
-          map (^. Internal.functionInfoName . namePretty) (filter (not . (^. Internal.functionInfoIsLocal)) (HashMap.elems (infoTable ^. Internal.infoFunctions)))
-            ++ map (^. Internal.constructorInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoConstructors))
-            ++ map (^. Internal.inductiveInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoInductives))
-            ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms))
 
     quote :: Text -> Text
     quote = quote' . Text.filter isLatin1 . Text.filter (isLetter .||. isDigit .||. (== '_') .||. (== '\''))
-
+      where
-    quote' :: Text -> Text
+        quote' :: Text -> Text
-    quote' txt
+        quote' txt
-      | HashSet.member txt reservedNames = quote' (prime txt)
+          | HashSet.member txt reservedNames = quote' (prime txt)
-      | txt == "_" = "v"
+          | txt == "_" = "v"
-      | otherwise = case Text.uncons txt of
+          | otherwise = case Text.uncons txt of
-          Just (c, _) | not (isLetter c) -> quote' ("v_" <> txt)
+              Just (c, _) | not (isLetter c) -> quote' ("v_" <> txt)
-          _ -> case Text.unsnoc txt of
+              _ -> case Text.unsnoc txt of
-            Just (_, c) | not (isAlphaNum c || c == '\'') -> quote' (txt <> "'")
+                Just (_, c) | not (isAlphaNum c || c == '\'') -> quote' (txt <> "'")
-            _ -> txt
+                _ -> txt
 
     reservedNames :: HashSet Text
     reservedNames =

src/Juvix/Compiler/Internal/Data/InfoTable.hs

@@ -265,5 +265,6 @@ mkConstructorEntries d =
       (_constructorInfoBuiltin, c) <- zipExact builtins (d ^. inductiveConstructors),
       let _constructorInfoType = c ^. inductiveConstructorType,
       let _constructorInfoName = c ^. inductiveConstructorName,
-      let _constructorInfoTrait = d ^. inductiveTrait
+      let _constructorInfoTrait = d ^. inductiveTrait,
+      let _constructorInfoRecord = c ^. inductiveConstructorIsRecord
   ]

src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs

@@ -10,7 +10,8 @@ data ConstructorInfo = ConstructorInfo
     _constructorInfoInductive :: InductiveName,
     _constructorInfoName :: ConstructorName,
     _constructorInfoBuiltin :: Maybe BuiltinConstructor,
-    _constructorInfoTrait :: Bool
+    _constructorInfoTrait :: Bool,
+    _constructorInfoRecord :: Bool
   }
   deriving stock (Generic)
 

tests/positive/Isabelle/Program.juvix

@@ -98,11 +98,48 @@ type Either' A B :=
 -- Records
 
 {-# isabelle-ignore: true #-}
+type R' := mkR' {
+  r1' : Nat;
+  r2' : Nat;
+};
+
 type R := mkR {
   r1 : Nat;
   r2 : Nat;
 };
 
+r : R := mkR 0 1;
+v : Nat := 0;
+
+funR (r : R) : R :=
+  case r of
+  | mkR@{r1; r2} := r@R{r1 := r1 + r2};
+
+funRR : R -> R
+  | r@mkR@{r1; r2} := r@R{r1 := r1 + r2};
+
+funR' : R -> R
+  | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr1 + rr2; r2 := rr2};
+
+funR1 : R -> R
+  | mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2}
+  | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1};
+
+funR2 (r : R) : R :=
+  case r of
+  | mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2}
+  | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1};
+
+funR3 (er : Either' R R) : R :=
+  case er of
+  | Left' mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2}
+  | Left' mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1}
+  | Right' mkR@{r1; r2 := zero} := mkR@{r1 := 7; r2 := r1}
+  | Right' r@(mkR@{r1; r2}) := r@R{r1 := r2 + 2; r2 := r1 + 3};
+
+funR4 : R -> R
+  | r@mkR@{r1} := r@R{r2 := r1};
+
 -- Standard library
 
 bf (b1 b2 : Bool) : Bool := not (b1 && b2);

tests/positive/Isabelle/isabelle/Program.thy

@@ -58,10 +58,10 @@ datatype 'A Queue
   = queue "'A list" "'A list"
 
 fun qfst :: "'A Queue \<Rightarrow> 'A list" where
-  "qfst (queue x v) = x"
+  "qfst (queue x v') = x"
 
 fun qsnd :: "'A Queue \<Rightarrow> 'A list" where
-  "qsnd (queue v v') = v'"
+  "qsnd (queue v' v'0) = v'0"
 
 fun pop_front :: "'A Queue \<Rightarrow> 'A Queue" where
   "pop_front q =
@@ -69,7 +69,7 @@ fun pop_front :: "'A Queue \<Rightarrow> 'A Queue" where
        q' = queue (tl (qfst q)) (qsnd q)
      in case qfst q' of
           [] \<Rightarrow> queue (rev (qsnd q')) [] |
-          v \<Rightarrow> q')"
+          v' \<Rightarrow> q')"
 
 fun push_back :: "'A Queue \<Rightarrow> 'A \<Rightarrow> 'A Queue" where
   "push_back q x =
@@ -86,8 +86,8 @@ fun is_empty :: "'A Queue \<Rightarrow> bool" where
        [] \<Rightarrow>
          (case qsnd q of
             [] \<Rightarrow> True |
-            v \<Rightarrow> False) |
+            v' \<Rightarrow> False) |
-       v \<Rightarrow> False)"
+       v' \<Rightarrow> False)"
 
 definition empty :: "'A Queue" where
   "empty = queue [] []"
@@ -97,8 +97,7 @@ fun funkcja :: "nat \<Rightarrow> nat" where
     (let
        nat1 = 1;
        nat2 = 2;
-       plusOne = \<lambda> x0 . case x0 of
+       plusOne = \<lambda> x0 . x0 + 1
-                                  n' \<Rightarrow> n' + 1
      in plusOne n + nat1 + nat2)"
 
 text \<open>
@@ -110,6 +109,115 @@ datatype ('A, 'B) Either'
     (* Right constructor *)
     Right' 'B
 
+record R =
+  r1 :: nat
+  r2 :: nat
+
+fun r1 :: "R \<Rightarrow> nat" where
+  "r1 (| R.r1 = r1'0, R.r2 = r2'0 |) = r1'0"
+
+fun r2 :: "R \<Rightarrow> nat" where
+  "r2 (| R.r1 = r1'0, R.r2 = r2'0 |) = r2'0"
+
+definition r :: R where
+  "r = (| R.r1 = 0, R.r2 = 1 |)"
+
+definition v :: nat where
+  "v = 0"
+
+fun funR :: "R \<Rightarrow> R" where
+  "funR r' = (r' (| R.r1 := R.r1 r' + R.r2 r' |))"
+
+fun funRR :: "R \<Rightarrow> R" where
+  "funRR r'0 = (r'0 (| R.r1 := R.r1 r'0 + R.r2 r'0 |))"
+
+fun funR' :: "R \<Rightarrow> R" where
+  "funR' (| R.r1 = rr1, R.r2 = rr2 |) =
+    (let
+       r1'0 = rr1 + rr2;
+       r2'0 = rr2
+     in (| R.r1 = r1'0, R.r2 = r2'0 |))"
+
+fun funR1 :: "R \<Rightarrow> R" where
+  "funR1 (| R.r1 = 0, R.r2 = r2'0 |) =
+    (let
+       r1'0 = r2'0;
+       r2'1 = r2'0
+     in (| R.r1 = r1'0, R.r2 = r2'1 |))" |
+  "funR1 (| R.r1 = rr1, R.r2 = rr2 |) =
+    (let
+       r1'0 = rr2;
+       r2'0 = rr1
+     in (| R.r1 = r1'0, R.r2 = r2'0 |))"
+
+fun funR2 :: "R \<Rightarrow> R" where
+  "funR2 r' =
+    (case (R.r1 r') of
+       (0) \<Rightarrow>
+         let
+           r1'0 = R.r2 r';
+           r2'0 = R.r2 r'
+         in (| R.r1 = r1'0, R.r2 = r2'0 |) |
+       _ \<Rightarrow>
+         let
+           r1'0 = R.r2 r';
+           r2'0 = R.r1 r'
+         in (| R.r1 = r1'0, R.r2 = r2'0 |))"
+
+fun funR3 :: "(R, R) Either' \<Rightarrow> R" where
+  "funR3 er =
+    (case er of
+       (Left' v') \<Rightarrow>
+         (case (R.r1 v') of
+            (0) \<Rightarrow>
+              let
+                r1'0 = R.r2 v';
+                r2'0 = R.r2 v'
+              in (| R.r1 = r1'0, R.r2 = r2'0 |) |
+            _ \<Rightarrow>
+              (case er of
+                 (Left' v'1) \<Rightarrow>
+                   let
+                     r1'0 = R.r2 v'1;
+                     r2'0 = R.r1 v'1
+                   in (| R.r1 = r1'0, R.r2 = r2'0 |) |
+                 v'2 \<Rightarrow>
+                   (case v'2 of
+                      (Right' v'1) \<Rightarrow>
+                        (case (R.r2 v'1) of
+                           (0) \<Rightarrow>
+                             let
+                               r1'0 = 7;
+                               r2'0 = 7
+                             in (| R.r1 = r1'0, R.r2 = r2'0 |) |
+                           _ \<Rightarrow>
+                             (case v'2 of
+                                (Right' r') \<Rightarrow>
+                                  r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))) |
+                      v'4 \<Rightarrow>
+                        (case v'4 of
+                           (Right' r') \<Rightarrow>
+                             r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))) |
+       v'2 \<Rightarrow>
+         (case v'2 of
+            (Right' v'1) \<Rightarrow>
+              (case (R.r2 v'1) of
+                 (0) \<Rightarrow>
+                   let
+                     r1'0 = 7;
+                     r2'0 = 7
+                   in (| R.r1 = r1'0, R.r2 = r2'0 |) |
+                 _ \<Rightarrow>
+                   (case v'2 of
+                      (Right' r') \<Rightarrow>
+                        r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))) |
+            v'4 \<Rightarrow>
+              (case v'4 of
+                 (Right' r') \<Rightarrow> r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))"
+
+fun funR4 :: "R \<Rightarrow> R" where
+  "funR4 r'0 = (r'0 (| R.r2 := R.r1 r'0 |))"
+
 fun bf :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
   "bf b1 b2 = (\<not> (b1 \<and> b2))"