From a4f3704f4ed2ca599d4d5535c07cb9220dd68fe9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Thu, 29 Aug 2024 16:15:58 +0200 Subject: [PATCH] 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 | 120 ++++ .../Compiler/Backend/Isabelle/Language.hs | 36 +- .../Compiler/Backend/Isabelle/Pretty/Base.hs | 33 +- .../Backend/Isabelle/Translation/FromTyped.hs | 588 +++++++++++++----- src/Juvix/Compiler/Internal/Data/InfoTable.hs | 3 +- .../Compiler/Store/Internal/Data/InfoTable.hs | 3 +- tests/positive/Isabelle/Program.juvix | 37 ++ tests/positive/Isabelle/isabelle/Program.thy | 122 +++- 8 files changed, 779 insertions(+), 163 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs b/src/Juvix/Compiler/Backend/Isabelle/Extra.hs index b0db4c823a..6b398aee43 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs +++ b/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 + } diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs index bac6820f44..00fc381e4d 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Language.hs +++ b/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 diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs index 543652d4ed..22a1c016cf 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs +++ b/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 diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index fb74a797de..0ffc72b221 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/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 - { _recordName = _inductiveName, - _recordParams = params, - _recordFields = map goRecordField tyargs, - _recordDocComment = _inductiveDocComment + RecordDef + { _recordDefName = _inductiveName, + _recordDefParams = params, + _recordDefFields = map goRecordField tyargs, + _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 - goClause Internal.LambdaClause {..} = - Clause - { _clausePatterns = nonEmpty' pats, - _clauseBody = goExpression'' nset' nmap' _lambdaBody + goClauses :: [Internal.LambdaClause] -> [Clause] + goClauses = \case + Internal.LambdaClause {..} : cls -> + case npats0 of + 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 - (pats, nset', nmap') = goPatternArgs'' (filterTypeArgs 0 ty (toList _lambdaPatterns)) + :| remainingBranches' + + 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 - goFunName name = - case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of - Just funInfo -> - case funInfo ^. Internal.functionInfoPragmas . pragmasIsabelleFunction of - Just PragmaIsabelleFunction {..} -> setNameText _pragmaIsabelleFunctionName name + getArgtys :: Internal.ConstructorInfo -> [Internal.FunctionParameter] + getArgtys ctrInfo = fst $ Internal.unfoldFunType $ ctrInfo ^. Internal.constructorInfoType + + 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 - Nothing -> overNameText quote name + x -> x - lookupName :: forall r. (Member (Reader NameMap) r) => Name -> Sem r Name + 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 - return $ ExprIden (goFunName name') + goFunName <$> lookupName 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 - return $ ExprIden name' + lookupName 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 - return $ ExprIden v' + lookupName 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 - goCaseBranch Internal.CaseBranch {..} = do - (pat, nset, nmap) <- goPatternArg' _caseBranchPattern - rhs <- withLocalNames nset nmap $ goCaseBranchRhs _caseBranchRhs - return $ - CaseBranch - { _caseBranchPattern = pat, - _caseBranchBody = rhs - } + goCaseBranches :: [Internal.CaseBranch] -> Sem r [CaseBranch] + goCaseBranches = \case + Internal.CaseBranch {..} : brs -> do + (npat, nset, nmap) <- goPatternArgCase _caseBranchPattern + case npat of + Nested pat [] -> do + rhs <- withLocalNames nset nmap $ goCaseBranchRhs _caseBranchRhs + 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) - goPatternArgs'' pats = - (pats', nset, nmap) + goLambdaClauses'' :: NameSet -> NameMap -> [Internal.LambdaClause] -> [CaseBranch] + goLambdaClauses'' nset nmap cls = + run $ runReader nset $ runReader nmap $ goLambdaClauses cls + + goLambdaClauses :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => [Internal.LambdaClause] -> Sem r [CaseBranch] + 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 - (nset, (nmap, pats')) = run $ runState (NameSet mempty) $ runState (NameMap mempty) $ goPatternArgs pats + (npats, (nset, (nmap, pats'))) = run $ runOutputList $ runState (NameSet mempty) $ runState (NameMap mempty) $ goPatternArgs True pats - goPatternArg' :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => Internal.PatternArg -> Sem r (Pattern, NameSet, NameMap) - goPatternArg' pat = do + 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 - return (pat', nset', nmap') + let (npats, (nmap', (nset', pat'))) = run $ runOutputList $ runState nmap $ runState nset $ goPatternArg False pat + return (Nested pat' npats, nset', nmap') - goPatternArgs' :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => [Internal.PatternArg] -> Sem r ([Pattern], NameSet, NameMap) - goPatternArgs' pats = do + goPatternArgsCase :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => [Internal.PatternArg] -> Sem r (Nested [Pattern], NameSet, NameMap) + goPatternArgsCase pats = do nset <- ask @NameSet nmap <- ask @NameMap - let (nmap', (nset', pats')) = run $ runState nmap $ runState nset $ goPatternArgs pats - return (pats', nset', nmap') - - goPatternArgs :: forall r. (Members '[State NameSet, State NameMap] r) => [Internal.PatternArg] -> Sem r [Pattern] - goPatternArgs = mapM goPatternArg - - -- TODO: named patterns (`_patternArgName`) are not handled properly - goPatternArg :: forall r. (Members '[State NameSet, State NameMap] r) => Internal.PatternArg -> Sem r Pattern - goPatternArg Internal.PatternArg {..} = - goPattern _patternArgPattern + let (npats, (nmap', (nset', pats'))) = run $ runOutputList $ runState nmap $ runState nset $ goPatternArgs False pats + return (Nested pats' npats, nset', nmap') + + goPatternArgs :: forall r. (Members '[State NameSet, State NameMap, Output (Expression, Nested Pattern)] r) => Bool -> [Internal.PatternArg] -> Sem r [Pattern] + goPatternArgs isTop = mapM (goPatternArg isTop) + + goPatternArg :: forall r. (Members '[State NameSet, State NameMap, Output (Expression, Nested Pattern)] r) => Bool -> Internal.PatternArg -> Sem r Pattern + goPatternArg isTop 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 + 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 - y' <- goPatternArg y + x' <- goPatternArg False x + 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 - y' <- goPatternArg y + x' <- goPatternArg False x + 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' :: HashSet Text -> Text -> Text - disambiguate' binders name - | name == "?" || name == "" || name == "_" = - disambiguate' binders "X" - | HashSet.member name binders - || HashSet.member name names = - disambiguate' binders (prime name) - | otherwise = - 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)) + 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 + + 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 .||. (== '_') .||. (== '\'')) - - quote' :: Text -> Text - quote' txt - | HashSet.member txt reservedNames = quote' (prime txt) - | txt == "_" = "v" - | otherwise = case Text.uncons txt of - Just (c, _) | not (isLetter c) -> quote' ("v_" <> txt) - _ -> case Text.unsnoc txt of - Just (_, c) | not (isAlphaNum c || c == '\'') -> quote' (txt <> "'") - _ -> txt + where + quote' :: Text -> Text + quote' txt + | HashSet.member txt reservedNames = quote' (prime txt) + | txt == "_" = "v" + | otherwise = case Text.uncons txt of + Just (c, _) | not (isLetter c) -> quote' ("v_" <> txt) + _ -> case Text.unsnoc txt of + Just (_, c) | not (isAlphaNum c || c == '\'') -> quote' (txt <> "'") + _ -> txt reservedNames :: HashSet Text reservedNames = diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index 5b04c73950..85c72ca5be 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/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 ] diff --git a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs index 6554e412cb..b55ea477cc 100644 --- a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs +++ b/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) diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index 2e865deda5..1cf4a9b5f5 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/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); diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index 3c846b64c4..96ef8e48b6 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -58,10 +58,10 @@ datatype 'A Queue = queue "'A list" "'A list" fun qfst :: "'A Queue \ 'A list" where - "qfst (queue x v) = x" + "qfst (queue x v') = x" fun qsnd :: "'A Queue \ 'A list" where - "qsnd (queue v v') = v'" + "qsnd (queue v' v'0) = v'0" fun pop_front :: "'A Queue \ 'A Queue" where "pop_front q = @@ -69,7 +69,7 @@ fun pop_front :: "'A Queue \ 'A Queue" where q' = queue (tl (qfst q)) (qsnd q) in case qfst q' of [] \ queue (rev (qsnd q')) [] | - v \ q')" + v' \ q')" fun push_back :: "'A Queue \ 'A \ 'A Queue" where "push_back q x = @@ -86,8 +86,8 @@ fun is_empty :: "'A Queue \ bool" where [] \ (case qsnd q of [] \ True | - v \ False) | - v \ False)" + v' \ False) | + v' \ False)" definition empty :: "'A Queue" where "empty = queue [] []" @@ -97,8 +97,7 @@ fun funkcja :: "nat \ nat" where (let nat1 = 1; nat2 = 2; - plusOne = \ x0 . case x0 of - n' \ n' + 1 + plusOne = \ x0 . x0 + 1 in plusOne n + nat1 + nat2)" text \ @@ -110,6 +109,115 @@ datatype ('A, 'B) Either' (* Right constructor *) Right' 'B +record R = + r1 :: nat + r2 :: nat + +fun r1 :: "R \ nat" where + "r1 (| R.r1 = r1'0, R.r2 = r2'0 |) = r1'0" + +fun r2 :: "R \ 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 \ R" where + "funR r' = (r' (| R.r1 := R.r1 r' + R.r2 r' |))" + +fun funRR :: "R \ R" where + "funRR r'0 = (r'0 (| R.r1 := R.r1 r'0 + R.r2 r'0 |))" + +fun funR' :: "R \ 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 \ 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 \ R" where + "funR2 r' = + (case (R.r1 r') of + (0) \ + let + r1'0 = R.r2 r'; + r2'0 = R.r2 r' + in (| R.r1 = r1'0, R.r2 = r2'0 |) | + _ \ + 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' \ R" where + "funR3 er = + (case er of + (Left' v') \ + (case (R.r1 v') of + (0) \ + let + r1'0 = R.r2 v'; + r2'0 = R.r2 v' + in (| R.r1 = r1'0, R.r2 = r2'0 |) | + _ \ + (case er of + (Left' v'1) \ + let + r1'0 = R.r2 v'1; + r2'0 = R.r1 v'1 + in (| R.r1 = r1'0, R.r2 = r2'0 |) | + v'2 \ + (case v'2 of + (Right' v'1) \ + (case (R.r2 v'1) of + (0) \ + let + r1'0 = 7; + r2'0 = 7 + in (| R.r1 = r1'0, R.r2 = r2'0 |) | + _ \ + (case v'2 of + (Right' r') \ + r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))) | + v'4 \ + (case v'4 of + (Right' r') \ + r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))) | + v'2 \ + (case v'2 of + (Right' v'1) \ + (case (R.r2 v'1) of + (0) \ + let + r1'0 = 7; + r2'0 = 7 + in (| R.r1 = r1'0, R.r2 = r2'0 |) | + _ \ + (case v'2 of + (Right' r') \ + r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))) | + v'4 \ + (case v'4 of + (Right' r') \ r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))" + +fun funR4 :: "R \ R" where + "funR4 r'0 = (r'0 (| R.r2 := R.r1 r'0 |))" + fun bf :: "bool \ bool \ bool" where "bf b1 b2 = (\ (b1 \ b2))"