From 994228dc943212b717b3a59970c3ba6153e163f4 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 19 Aug 2024 20:13:55 +0200 Subject: [PATCH 01/13] records: language & printing --- .../Compiler/Backend/Isabelle/Language.hs | 33 +++++++++++++++---- .../Compiler/Backend/Isabelle/Pretty/Base.hs | 28 ++++++++++++---- .../Backend/Isabelle/Translation/FromTyped.hs | 8 ++--- tests/positive/Isabelle/Program.juvix | 5 +++ 4 files changed, 57 insertions(+), 17 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs index a0e130c1e0..04b528734f 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,10 @@ data Cons a = Cons _consTail :: a } +newtype Record a = Record + { _recordFields :: [(Name, a)] + } + data ConstrApp = ConstrApp { _constrAppConstructor :: Name, _constrAppArgs :: [Pattern] @@ -143,13 +155,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, @@ -184,10 +202,10 @@ data Constructor = Constructor _constructorArgTypes :: [Type] } -data Record = Record - { _recordName :: Name, - _recordParams :: [TypeVar], - _recordFields :: [RecordField] +data RecordDef = RecordDef + { _recordDefName :: Name, + _recordDefParams :: [TypeVar], + _recordDefFields :: [RecordField] } data RecordField = RecordField @@ -200,9 +218,7 @@ makeLenses ''Function makeLenses ''Synonym makeLenses ''Datatype makeLenses ''Constructor -makeLenses ''Record makeLenses ''RecordField -makeLenses ''Tuple data Theory = Theory { _theoryName :: Name, @@ -289,6 +305,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 @@ -304,3 +322,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 6e58abaa40..a4c09a6bd4 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs @@ -82,6 +82,8 @@ instance PrettyCode Expression where ExprTuple x -> ppCode x ExprList x -> ppCode x ExprCons x -> ppCode x + ExprRecord x -> ppCode x + ExprRecordUpdate x -> ppCode x ExprLet x -> ppCode x ExprIf x -> ppCode x ExprCase x -> ppCode x @@ -105,6 +107,12 @@ instance PrettyCode Binop where r <- ppRightExpression _binopFixity _binopRight return $ l <+> op <+> r +instance PrettyCode RecordUpdate where + ppCode RecordUpdate {..} = do + r <- ppCode _recordUpdateRecord + fields <- ppCode _recordUpdateFields + return $ r <+> fields + instance PrettyCode LetClause where ppCode LetClause {..} = do name <- ppCode _letClauseName @@ -145,7 +153,14 @@ 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) + +instance (PrettyCode a) => PrettyCode (Record a) where + ppCode Record {..} = do + names <- mapM (ppCode . fst) _recordFields + elems <- mapM (ppCode . snd) _recordFields + let fields = zipWithExact (\n e -> n <+> "=" <+> e) names elems + return $ "(|" <+> hsep (punctuate comma fields) <+> "|)" instance (PrettyCode a, HasAtomicity a) => PrettyCode (Cons a) where ppCode Cons {..} = do @@ -161,6 +176,7 @@ instance PrettyCode Pattern where PatTuple x -> ppCode x PatList x -> ppCode x PatCons x -> ppCode x + PatRecord x -> ppCode x instance PrettyCode ConstrApp where ppCode ConstrApp {..} = do @@ -228,11 +244,11 @@ instance PrettyCode Constructor where tys <- mapM ppCodeQuoted _constructorArgTypes return $ hsep (n : tys) -instance PrettyCode Record where - ppCode Record {..} = do - n <- ppCode _recordName - params <- ppParams _recordParams - fields <- mapM ppCode _recordFields +instance PrettyCode RecordDef where + ppCode RecordDef {..} = do + n <- ppCode _recordDefName + params <- ppParams _recordDefParams + fields <- mapM ppCode _recordDefFields return $ 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 9ed35142d5..9a9ae97af5 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -96,10 +96,10 @@ 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 + RecordDef + { _recordDefName = _inductiveName, + _recordDefParams = params, + _recordDefFields = map goRecordField tyargs } | otherwise = StmtDatatype diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index 0cd881bc34..e2e53bd1a3 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -92,6 +92,11 @@ type Either' A B := Left' A | Right' B; -- Records {-# isabelle-ignore: true #-} +type R' := mkR' { + r1' : Nat; + r2' : Nat; +}; + type R := mkR { r1 : Nat; r2 : Nat; From a7721c1018f4d18727c1ef5f871c2ee743712b54 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 19 Aug 2024 22:06:16 +0200 Subject: [PATCH 02/13] translate records (wip) --- .../Backend/Isabelle/Translation/FromTyped.hs | 33 ++++++++++++++++++- src/Juvix/Compiler/Internal/Data/InfoTable.hs | 3 +- .../Compiler/Store/Internal/Data/InfoTable.hs | 3 +- tests/positive/Isabelle/Program.juvix | 7 ++++ tests/positive/Isabelle/isabelle/Program.thy | 12 +++++++ 5 files changed, 55 insertions(+), 3 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index 9a9ae97af5..75a22b3f14 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -283,6 +283,9 @@ goModule onlyTypes infoTable Internal.Module {..} = _ -> overNameText quote name Nothing -> overNameText quote name + getArgtys :: Internal.ConstructorInfo -> [Internal.FunctionParameter] + getArgtys ctrInfo = fst $ Internal.unfoldFunType $ ctrInfo ^. Internal.constructorInfoType + goFunName :: Name -> Name goFunName name = case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of @@ -309,6 +312,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) @@ -381,6 +389,9 @@ goModule onlyTypes infoTable Internal.Module {..} = x' <- goExpression x y' <- goExpression y return $ ExprTuple (Tuple (x' :| [y'])) + | Just fields <- getRecordCreation app = do + fields' <- mapM (secondM goExpression) fields + return $ ExprRecord (Record fields') | Just (fn, args) <- getIdentApp app = do fn' <- goExpression fn args' <- mapM goExpression args @@ -535,6 +546,17 @@ goModule onlyTypes infoTable Internal.Module {..} = where (fn, args) = Internal.unfoldApplication app + getRecordCreation :: Internal.Application -> Maybe [(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 (goRecordFields (getArgtys ctrInfo) (toList args)) + _ -> Nothing + _ -> Nothing + where + (fn, args) = Internal.unfoldApplication app + getIdentApp :: Internal.Application -> Maybe (Internal.Expression, [Internal.Expression]) getIdentApp app = case mty of Just (ty, paramsNum) -> Just (fn, args') @@ -574,7 +596,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) @@ -771,6 +792,9 @@ goModule onlyTypes infoTable Internal.Module {..} = x' <- goPatternArg x y' <- goPatternArg y return $ PatCons (Cons x' y') + | Just fields <- getRecordPat _constrAppConstructor _constrAppParameters = do + fields' <- mapM (secondM goPatternArg) fields + return $ PatRecord (Record fields') | Just (x, y) <- getPairPat _constrAppConstructor _constrAppParameters = do x' <- goPatternArg x y' <- goPatternArg y @@ -817,6 +841,13 @@ goModule onlyTypes infoTable Internal.Module {..} = _ -> Nothing Nothing -> Nothing + getRecordPat :: Name -> [Internal.PatternArg] -> Maybe [(Name, Internal.PatternArg)] + getRecordPat name args = + case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of + Just ctrInfo + | ctrInfo ^. Internal.constructorInfoRecord -> Just (goRecordFields (getArgtys ctrInfo) args) + _ -> Nothing + getNatPat :: Name -> [Internal.PatternArg] -> Maybe (Either Pattern Internal.PatternArg) getNatPat name args = case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of 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 e2e53bd1a3..ff98e1cb10 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -102,6 +102,13 @@ type R := mkR { r2 : Nat; }; +funR (r : R) : R := + case r of + | mkR@{r1; r2} := r@R{r1 := r1 + r2}; + +funR' : R -> R + | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr1 + rr2; r2 := rr2}; + -- 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 e9c72431aa..061cf0a701 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -99,6 +99,18 @@ datatype ('A, 'B) Either' = Left' 'A | Right' 'B +record R = + r1 :: nat + r2 :: nat + +fun r1 :: "R \ nat" where + "r1 \ r1 = r1', r2 = _ \ = r1'" + +fun funR :: "R \ R" where + "funR r = + (case r of + _ \ r\r1 := R.r1 r + R.r2 r\)" + fun bf :: "bool \ bool \ bool" where "bf b1 b2 = (\ (b1 \ b2))" From de505a72acb50fc34935d4f6467199ac5798bc5e Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 20 Aug 2024 20:32:01 +0200 Subject: [PATCH 03/13] record pattern matching --- .../Compiler/Backend/Isabelle/Language.hs | 5 +- .../Compiler/Backend/Isabelle/Pretty/Base.hs | 4 +- .../Backend/Isabelle/Translation/FromTyped.hs | 77 +++++++++++-------- tests/positive/Isabelle/isabelle/Program.thy | 18 ++++- 4 files changed, 65 insertions(+), 39 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs index 04b528734f..5e3d2f2fe1 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Language.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Language.hs @@ -137,8 +137,9 @@ data Cons a = Cons _consTail :: a } -newtype Record a = Record - { _recordFields :: [(Name, a)] +data Record a = Record + { _recordName :: Name, + _recordFields :: [(Name, a)] } data ConstrApp = ConstrApp diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs index a4c09a6bd4..a06a5fae85 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs @@ -157,9 +157,11 @@ instance (PrettyCode a) => PrettyCode (List a) where instance (PrettyCode a) => PrettyCode (Record a) where ppCode Record {..} = do + recName <- ppCode _recordName names <- mapM (ppCode . fst) _recordFields elems <- mapM (ppCode . snd) _recordFields - let fields = zipWithExact (\n e -> n <+> "=" <+> e) names elems + let names' = map (\n -> recName <> "." <> n) names + fields = zipWithExact (\n e -> n <+> "=" <+> e) names' elems return $ "(|" <+> hsep (punctuate comma fields) <+> "|)" instance (PrettyCode a, HasAtomicity a) => PrettyCode (Cons a) where diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index 75a22b3f14..11b0859e63 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -195,7 +195,7 @@ goModule onlyTypes infoTable Internal.Module {..} = _clauseBody = goExpression'' nset' nmap' _lambdaBody } where - (pats, nset', nmap') = goPatternArgs'' (filterTypeArgs 0 ty (toList _lambdaPatterns)) + (pats, nset', nmap') = goPatternArgsTop (filterTypeArgs 0 ty (toList _lambdaPatterns)) goFunctionDef :: Internal.FunctionDef -> Statement goFunctionDef Internal.FunctionDef {..} = goDef _funDefName _funDefType _funDefArgsInfo (Just _funDefBody) @@ -389,9 +389,9 @@ goModule onlyTypes infoTable Internal.Module {..} = x' <- goExpression x y' <- goExpression y return $ ExprTuple (Tuple (x' :| [y'])) - | Just fields <- getRecordCreation app = do + | Just (name, fields) <- getRecordCreation app = do fields' <- mapM (secondM goExpression) fields - return $ ExprRecord (Record fields') + return $ ExprRecord (Record name fields') | Just (fn, args) <- getIdentApp app = do fn' <- goExpression fn args' <- mapM goExpression args @@ -546,12 +546,15 @@ goModule onlyTypes infoTable Internal.Module {..} = where (fn, args) = Internal.unfoldApplication app - getRecordCreation :: Internal.Application -> Maybe [(Name, Internal.Expression)] + 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 (goRecordFields (getArgtys ctrInfo) (toList args)) + | ctrInfo ^. Internal.constructorInfoRecord -> + Just (indName, goRecordFields (getArgtys ctrInfo) (toList args)) + where + indName = ctrInfo ^. Internal.constructorInfoInductive _ -> Nothing _ -> Nothing where @@ -702,9 +705,9 @@ goModule onlyTypes infoTable Internal.Module {..} = goClause :: Internal.LambdaClause -> Sem r CaseBranch goClause Internal.LambdaClause {..} = do (pat, nset, nmap) <- case _lambdaPatterns of - p :| [] -> goPatternArg' p + p :| [] -> goPatternArgCase p _ -> do - (pats, nset, nmap) <- goPatternArgs' (toList _lambdaPatterns) + (pats, nset, nmap) <- goPatternArgsCase (toList _lambdaPatterns) let pat = PatTuple Tuple @@ -731,7 +734,7 @@ goModule onlyTypes infoTable Internal.Module {..} = goCaseBranch :: Internal.CaseBranch -> Sem r CaseBranch goCaseBranch Internal.CaseBranch {..} = do - (pat, nset, nmap) <- goPatternArg' _caseBranchPattern + (pat, nset, nmap) <- goPatternArgCase _caseBranchPattern rhs <- withLocalNames nset nmap $ goCaseBranchRhs _caseBranchRhs return $ CaseBranch @@ -744,32 +747,32 @@ goModule onlyTypes infoTable Internal.Module {..} = Internal.CaseBranchRhsExpression e -> goExpression e Internal.CaseBranchRhsIf {} -> error "unsupported: side conditions" - goPatternArgs'' :: [Internal.PatternArg] -> ([Pattern], NameSet, NameMap) - goPatternArgs'' pats = + goPatternArgsTop :: [Internal.PatternArg] -> ([Pattern], NameSet, NameMap) + goPatternArgsTop pats = (pats', nset, nmap) where - (nset, (nmap, pats')) = run $ runState (NameSet mempty) $ runState (NameMap mempty) $ goPatternArgs pats + (nset, (nmap, pats')) = run $ 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 (Pattern, NameSet, NameMap) + goPatternArgCase pat = do nset <- ask @NameSet nmap <- ask @NameMap - let (nmap', (nset', pat')) = run $ runState nmap $ runState nset $ goPatternArg pat + let (nmap', (nset', pat')) = run $ runState nmap $ runState nset $ goPatternArg False pat return (pat', 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 ([Pattern], NameSet, NameMap) + goPatternArgsCase pats = do nset <- ask @NameSet nmap <- ask @NameMap - let (nmap', (nset', pats')) = run $ runState nmap $ runState nset $ goPatternArgs pats + let (nmap', (nset', pats')) = run $ runState nmap $ runState nset $ goPatternArgs False pats return (pats', nset', nmap') - goPatternArgs :: forall r. (Members '[State NameSet, State NameMap] r) => [Internal.PatternArg] -> Sem r [Pattern] - goPatternArgs = mapM goPatternArg + goPatternArgs :: forall r. (Members '[State NameSet, State NameMap] r) => Bool -> [Internal.PatternArg] -> Sem r [Pattern] + goPatternArgs isTop = mapM (goPatternArg isTop) -- 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 {..} = + goPatternArg :: forall r. (Members '[State NameSet, State NameMap] r) => Bool -> Internal.PatternArg -> Sem r Pattern + goPatternArg isTop Internal.PatternArg {..} = goPattern _patternArgPattern where goPattern :: Internal.Pattern -> Sem r Pattern @@ -786,27 +789,32 @@ goModule onlyTypes infoTable Internal.Module {..} = 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 fields <- getRecordPat _constrAppConstructor _constrAppParameters = do - fields' <- mapM (secondM goPatternArg) fields - return $ PatRecord (Record fields') + | Just (name, fields) <- getRecordPat _constrAppConstructor _constrAppParameters = + if + | isTop -> do + fields' <- mapM (secondM (goPatternArg False)) fields + return $ PatRecord (Record name fields') + | otherwise -> + -- TODO: record patterns are not supported in non-top-level patterns + return $ PatVar (defaultName "_") | 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 @@ -841,11 +849,14 @@ goModule onlyTypes infoTable Internal.Module {..} = _ -> Nothing Nothing -> Nothing - getRecordPat :: Name -> [Internal.PatternArg] -> Maybe [(Name, Internal.PatternArg)] + 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 (goRecordFields (getArgtys ctrInfo) args) + | ctrInfo ^. Internal.constructorInfoRecord -> + Just (indName, goRecordFields (getArgtys ctrInfo) args) + where + indName = ctrInfo ^. Internal.constructorInfoInductive _ -> Nothing getNatPat :: Name -> [Internal.PatternArg] -> Maybe (Either Pattern Internal.PatternArg) diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index 061cf0a701..f2d343d45c 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -103,13 +103,25 @@ record R = r1 :: nat r2 :: nat -fun r1 :: "R \ nat" where - "r1 \ r1 = r1', r2 = _ \ = r1'" +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" fun funR :: "R \ R" where "funR r = (case r of - _ \ r\r1 := R.r1 r + R.r2 r\)" + _ \ + (\ x0 . case x0 of + _ \ (| R.r1 = r1 + r2, R.r2 = r2 |)) r)" + +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 bf :: "bool \ bool \ bool" where "bf b1 b2 = (\ (b1 \ b2))" From 3cf4ba5031e0173c49167d98d26feb3c1883b2a0 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 21 Aug 2024 20:20:46 +0200 Subject: [PATCH 04/13] nested patterns wip --- .../Backend/Isabelle/Translation/FromTyped.hs | 294 ++++++++++++------ tests/positive/Isabelle/isabelle/Program.thy | 8 +- 2 files changed, 206 insertions(+), 96 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index 11b0859e63..016db290bd 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -21,12 +21,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) => @@ -171,7 +181,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) @@ -188,14 +198,20 @@ goModule onlyTypes infoTable Internal.Module {..} = } ] - goClause :: Internal.LambdaClause -> Clause - goClause Internal.LambdaClause {..} = - Clause - { _clausePatterns = nonEmpty' pats, - _clauseBody = goExpression'' nset' nmap' _lambdaBody - } - where - (pats, nset', nmap') = goPatternArgsTop (filterTypeArgs 0 ty (toList _lambdaPatterns)) + 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 -> undefined + where + (npats0, nset', nmap') = goPatternArgsTop (filterTypeArgs 0 ty (toList _lambdaPatterns)) + [] -> [] goFunctionDef :: Internal.FunctionDef -> Statement goFunctionDef Internal.FunctionDef {..} = goDef _funDefName _funDefType _funDefArgsInfo (Just _funDefBody) @@ -286,24 +302,27 @@ goModule onlyTypes infoTable Internal.Module {..} = getArgtys :: Internal.ConstructorInfo -> [Internal.FunctionParameter] getArgtys ctrInfo = fst $ Internal.unfoldFunType $ ctrInfo ^. Internal.constructorInfoType - 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 + 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 @@ -341,8 +360,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 -> @@ -351,8 +369,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) @@ -649,10 +666,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 @@ -664,7 +681,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 @@ -685,107 +702,178 @@ 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 <- goClauses (toList _lambdaClauses) return $ ExprCase 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 :| [] -> goPatternArgCase p - _ -> do - (pats, nset, nmap) <- goPatternArgsCase (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 - } + goClauses :: [Internal.LambdaClause] -> Sem r [CaseBranch] + goClauses = \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 <- goClauses cls + return $ + CaseBranch + { _caseBranchPattern = pat, + _caseBranchBody = body + } + : brs + Nested pat npats -> undefined + [] -> return [] goCase :: Internal.Case -> Sem r Expression goCase Internal.Case {..} = do val <- goExpression _caseExpression - brs <- mapM goCaseBranch _caseBranches + brs <- goCaseBranches (toList _caseBranches) return $ ExprCase Case { _caseValue = val, - _caseBranches = brs + _caseBranches = nonEmpty' brs } - goCaseBranch :: Internal.CaseBranch -> Sem r CaseBranch - goCaseBranch Internal.CaseBranch {..} = do - (pat, nset, nmap) <- goPatternArgCase _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 name = defaultName (disambiguate (nset ^. nameSet) "v") + rhs <- withLocalNames nset nmap $ goCaseBranchRhs _caseBranchRhs + brs' <- goCaseBranches brs + let defaultBranch = + case nonEmpty brs' of + Just brs'' -> + [ CaseBranch + { _caseBranchPattern = PatVar name, + _caseBranchBody = + ExprCase + Case + { _caseValue = ExprIden name, + _caseBranches = brs'' + } + } + ] + Nothing -> [] + toList <$> goNestedCaseBranches rhs defaultBranch (Nested pat npats) + [] -> return [] + + goNestedCaseBranches :: Expression -> [CaseBranch] -> Nested Pattern -> Sem r (NonEmpty CaseBranch) + goNestedCaseBranches rhs defaultBranch = \case + Nested pat [] -> + return $ + CaseBranch + { _caseBranchPattern = pat, + _caseBranchBody = rhs + } + :| 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 <- goNestedCaseBranches rhs defaultBranch (Nested pat' npats') + return $ + CaseBranch + { _caseBranchPattern = pat, + _caseBranchBody = + ExprCase + Case + { _caseValue = val, + _caseBranches = brs + } + } + :| defaultBranch goCaseBranchRhs :: Internal.CaseBranchRhs -> Sem r Expression goCaseBranchRhs = \case Internal.CaseBranchRhsExpression e -> goExpression e Internal.CaseBranchRhsIf {} -> error "unsupported: side conditions" - goPatternArgsTop :: [Internal.PatternArg] -> ([Pattern], NameSet, NameMap) + goPatternArgsTop :: [Internal.PatternArg] -> (Nested [Pattern], NameSet, NameMap) goPatternArgsTop pats = - (pats', nset, nmap) + (Nested pats' npats, nset, nmap) where - (nset, (nmap, pats')) = run $ runState (NameSet mempty) $ runState (NameMap mempty) $ goPatternArgs True pats + (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 (Pattern, NameSet, NameMap) + 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 False 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') - goPatternArgsCase :: 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) goPatternArgsCase pats = do nset <- ask @NameSet nmap <- ask @NameMap - let (nmap', (nset', pats')) = run $ runState nmap $ runState nset $ goPatternArgs False pats - return (pats', nset', nmap') + 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] r) => Bool -> [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 isTop = mapM (goPatternArg isTop) - -- TODO: named patterns (`_patternArgName`) are not handled properly - goPatternArg :: forall r. (Members '[State NameSet, State NameMap] r) => Bool -> Internal.PatternArg -> Sem r Pattern + goPatternArg :: forall r. (Members '[State NameSet, State NameMap, Output (Expression, Nested Pattern)] r) => Bool -> Internal.PatternArg -> Sem r Pattern goPatternArg isTop Internal.PatternArg {..} = - goPattern _patternArgPattern + -- TODO: named patterns + goPattern isTop _patternArgPattern + + goNestedPatternArg :: forall r. (Members '[State NameSet, State NameMap, Output (Expression, Nested Pattern)] r) => Bool -> Internal.PatternArg -> Sem r (Nested Pattern) + goNestedPatternArg isTop Internal.PatternArg {..} = + -- TODO: named patterns + goNestedPattern isTop _patternArgPattern + + goNestedPattern :: forall r. (Members '[State NameSet, State NameMap, Output (Expression, Nested Pattern)] r) => Bool -> Internal.Pattern -> Sem r (Nested Pattern) + goNestedPattern isTop pat = do + (npats, pat') <- runOutputList $ goPattern isTop 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 @@ -795,14 +883,27 @@ goModule onlyTypes infoTable Internal.Module {..} = x' <- goPatternArg False x y' <- goPatternArg False y return $ PatCons (Cons x' y') - | Just (name, fields) <- getRecordPat _constrAppConstructor _constrAppParameters = + | Just (indName, fields) <- getRecordPat _constrAppConstructor _constrAppParameters = if | isTop -> do fields' <- mapM (secondM (goPatternArg False)) fields - return $ PatRecord (Record name fields') - | otherwise -> - -- TODO: record patterns are not supported in non-top-level patterns - return $ PatVar (defaultName "_") + return $ PatRecord (Record indName fields') + | otherwise -> do + binders <- gets (^. nameSet) + let adjustName :: Name -> Expression + adjustName name = + let name' = overNameText (\n -> indName ^. nameText <> "." <> n) name + in ExprApp (Application (ExprIden name') (ExprIden vname)) + vname = defaultName (disambiguate binders "v") + fieldsVars = map (second getPatternArgVar) $ 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 False)) fieldsNonVars + forM fieldsNonVars' output + return (PatVar vname) | Just (x, y) <- getPairPat _constrAppConstructor _constrAppParameters = do x' <- goPatternArg False x y' <- goPatternArg False y @@ -822,6 +923,19 @@ goModule onlyTypes infoTable Internal.Module {..} = _constrAppArgs = args } + isPatternArgVar :: Internal.PatternArg -> Bool + isPatternArgVar Internal.PatternArg {..} = + isNothing _patternArgName + && case _patternArgPattern of + Internal.PatternVariable {} -> True + _ -> False + + getPatternArgVar :: Internal.PatternArg -> Name + getPatternArgVar Internal.PatternArg {..} = + case _patternArgPattern of + Internal.PatternVariable name -> name + _ -> impossible + -- This function cannot be simply merged with `getList` because in patterns -- the constructors don't get the type arguments. getListPat :: Name -> [Internal.PatternArg] -> Maybe [Internal.PatternArg] diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index f2d343d45c..8b69ff927a 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -109,12 +109,8 @@ fun r1 :: "R \ nat" where fun r2 :: "R \ nat" where "r2 (| R.r1 = r1'0, R.r2 = r2'0 |) = r2'0" -fun funR :: "R \ R" where - "funR r = - (case r of - _ \ - (\ x0 . case x0 of - _ \ (| R.r1 = r1 + r2, R.r2 = r2 |)) r)" +fun funR :: "R \ nat" where + "funR r = R.r1 r" fun funR' :: "R \ R" where "funR' (| R.r1 = rr1, R.r2 = rr2 |) = From f4946176a3093ed33d48455a3d5eb0ee41678501 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 22 Aug 2024 17:58:24 +0200 Subject: [PATCH 05/13] nested record patterns --- .../Backend/Isabelle/Translation/FromTyped.hs | 210 ++++++++++++------ tests/positive/Isabelle/Program.juvix | 12 + tests/positive/Isabelle/isabelle/Program.thy | 50 ++++- 3 files changed, 197 insertions(+), 75 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index 016db290bd..077330bb9d 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -208,11 +208,83 @@ goModule onlyTypes infoTable Internal.Module {..} = _clauseBody = goExpression'' nset' nmap' _lambdaBody } : goClauses cls - Nested pats npats -> undefined + Nested pats npats -> + let rhs = goExpression'' nset' nmap' _lambdaBody + vnames = map (overNameText (disambiguate (nset' ^. nameSet))) argnames + nset'' = foldl' (flip (over nameSet . HashSet.insert . (^. namePretty))) nset' vnames + remainingBranches = goLambdaClauses'' nset'' nmap' cls + valTuple = ExprTuple (Tuple (nonEmpty' (map ExprIden vnames))) + brs = goNestedBranches valTuple rhs remainingBranches (PatTuple (Tuple (nonEmpty' pats))) (nonEmpty' npats) + in [ Clause + { _clausePatterns = nonEmpty' $ map PatVar vnames, + _clauseBody = + ExprCase + 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') + in CaseBranch + { _caseBranchPattern = pat, + _caseBranchBody = + ExprCase + Case + { _caseValue = val, + _caseBranches = brs + } + } + :| remainingBranches + + mkDefaultBranch :: Expression -> [CaseBranch] -> Maybe CaseBranch + mkDefaultBranch val remainingBranches = case remainingBranches of + [] -> Nothing + _ -> + Just $ + CaseBranch + { _caseBranchPattern = PatVar (defaultName "_"), + _caseBranchBody = + ExprCase + 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 = + ExprCase + Case + { _caseValue = val, + _caseBranches = brs + } + } + :| toList defaultBranch + goFunctionDef :: Internal.FunctionDef -> Statement goFunctionDef Internal.FunctionDef {..} = goDef _funDefName _funDefType _funDefArgsInfo (Just _funDefBody) @@ -710,7 +782,7 @@ goModule onlyTypes infoTable Internal.Module {..} = Tuple { _tupleComponents = nonEmpty' vars' } - brs <- goClauses (toList _lambdaClauses) + brs <- goLambdaClauses (toList _lambdaClauses) return $ ExprCase Case @@ -718,36 +790,6 @@ goModule onlyTypes infoTable Internal.Module {..} = _caseBranches = nonEmpty' brs } - goClauses :: [Internal.LambdaClause] -> Sem r [CaseBranch] - goClauses = \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 <- goClauses cls - return $ - CaseBranch - { _caseBranchPattern = pat, - _caseBranchBody = body - } - : brs - Nested pat npats -> undefined - [] -> return [] - goCase :: Internal.Case -> Sem r Expression goCase Internal.Case {..} = do val <- goExpression _caseExpression @@ -774,56 +816,78 @@ goModule onlyTypes infoTable Internal.Module {..} = } : brs' Nested pat npats -> do - let name = defaultName (disambiguate (nset ^. nameSet) "v") rhs <- withLocalNames nset nmap $ goCaseBranchRhs _caseBranchRhs - brs' <- goCaseBranches brs - let defaultBranch = - case nonEmpty brs' of - Just brs'' -> - [ CaseBranch - { _caseBranchPattern = PatVar name, - _caseBranchBody = - ExprCase - Case - { _caseValue = ExprIden name, - _caseBranches = brs'' - } + let vname = defaultName (disambiguate (nset ^. nameSet) "v") + nset' = over nameSet (HashSet.insert (vname ^. namePretty)) nset + remainingBranches <- withLocalNames nset' nmap $ goCaseBranches brs + let brs' = goNestedBranches (ExprIden vname) rhs remainingBranches pat (nonEmpty' npats) + return + [ CaseBranch + { _caseBranchPattern = PatVar vname, + _caseBranchBody = + ExprCase + Case + { _caseValue = ExprIden vname, + _caseBranches = brs' } - ] - Nothing -> [] - toList <$> goNestedCaseBranches rhs defaultBranch (Nested pat npats) + } + ] [] -> return [] - goNestedCaseBranches :: Expression -> [CaseBranch] -> Nested Pattern -> Sem r (NonEmpty CaseBranch) - goNestedCaseBranches rhs defaultBranch = \case - Nested pat [] -> + goCaseBranchRhs :: Internal.CaseBranchRhs -> Sem r Expression + goCaseBranchRhs = \case + Internal.CaseBranchRhsExpression e -> goExpression e + Internal.CaseBranchRhsIf {} -> error "unsupported: side conditions" + + 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 = rhs + _caseBranchBody = body } - :| defaultBranch + : brs 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 <- goNestedCaseBranches rhs defaultBranch (Nested pat' npats') - return $ - CaseBranch - { _caseBranchPattern = pat, - _caseBranchBody = - ExprCase - Case - { _caseValue = val, - _caseBranches = brs - } - } - :| defaultBranch - - goCaseBranchRhs :: Internal.CaseBranchRhs -> Sem r Expression - goCaseBranchRhs = \case - Internal.CaseBranchRhsExpression e -> goExpression e - Internal.CaseBranchRhsIf {} -> error "unsupported: side conditions" + rhs <- withLocalNames nset nmap $ goExpression _lambdaBody + let vname = defaultName (disambiguate (nset ^. nameSet) "v") + nset' = over nameSet (HashSet.insert (vname ^. namePretty)) nset + remainingBranches <- withLocalNames nset' nmap $ goLambdaClauses cls + let brs' = goNestedBranches (ExprIden vname) rhs remainingBranches pat (nonEmpty' npats) + return + [ CaseBranch + { _caseBranchPattern = PatVar vname, + _caseBranchBody = + ExprCase + Case + { _caseValue = ExprIden vname, + _caseBranches = brs' + } + } + ] + [] -> return [] goPatternArgsTop :: [Internal.PatternArg] -> (Nested [Pattern], NameSet, NameMap) goPatternArgsTop pats = diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index ff98e1cb10..8e7535c9db 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -106,9 +106,21 @@ 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}; + -- 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 8b69ff927a..0afabfa42b 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -109,8 +109,17 @@ fun r1 :: "R \ nat" where fun r2 :: "R \ nat" where "r2 (| R.r1 = r1'0, R.r2 = r2'0 |) = r2'0" -fun funR :: "R \ nat" where - "funR r = R.r1 r" +fun funR :: "R \ R" where + "funR r = + (case r of + v \ + (\ x0 . case x0 of + v' \ (| R.r1 = R.r1 v' + R.r2 v', R.r2 = R.r2 v' |)) r)" + +fun funRR :: "R \ R" where + "funRR (| R.r1 = r1'0, R.r2 = r2'0 |) = + ((\ x0 . case x0 of + v \ (| R.r1 = R.r1 v + R.r2 v, R.r2 = R.r2 v |)) r)" fun funR' :: "R \ R" where "funR' (| R.r1 = rr1, R.r2 = rr2 |) = @@ -119,6 +128,43 @@ fun funR' :: "R \ R" where 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 of + v' \ + (case v' of + 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 v' of + v'0 \ + let + r1'0 = R.r2 v'0; + r2'0 = R.r1 v'0 + in (| R.r1 = r1'0, R.r2 = r2'0 |))) | + v'0 \ + let + r1'0 = R.r2 v'0; + r2'0 = R.r1 v'0 + in (| R.r1 = r1'0, R.r2 = r2'0 |)))" + fun bf :: "bool \ bool \ bool" where "bf b1 b2 = (\ (b1 \ b2))" From 0e4581a729e487a34146062dc5bbbec6c92bee3b Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 22 Aug 2024 18:38:33 +0200 Subject: [PATCH 06/13] remove redundant clauses --- src/Juvix/Compiler/Backend/Isabelle/Extra.hs | 25 ++++++++ .../Backend/Isabelle/Translation/FromTyped.hs | 63 ++++++++++--------- tests/positive/Isabelle/Program.juvix | 6 ++ tests/positive/Isabelle/isabelle/Program.thy | 33 ++++++++-- 4 files changed, 90 insertions(+), 37 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs b/src/Juvix/Compiler/Backend/Isabelle/Extra.hs index b0db4c823a..60e51bd81d 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Extra.hs @@ -1,8 +1,33 @@ 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 fst r1' == map fst r2' + && all (uncurry subsumesPattern) (zipExact (map snd r1') (map snd r2')) + where + r1' = sortOn fst r1 + r2' = sortOn fst r2 + _ -> False diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index 077330bb9d..52ba24e008 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -235,6 +235,7 @@ goModule onlyTypes infoTable Internal.Module {..} = 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 = @@ -244,7 +245,7 @@ goModule onlyTypes infoTable Internal.Module {..} = _caseBranches = brs } } - :| remainingBranches + :| remainingBranches' mkDefaultBranch :: Expression -> [CaseBranch] -> Maybe CaseBranch mkDefaultBranch val remainingBranches = case remainingBranches of @@ -1094,39 +1095,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/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index 8e7535c9db..f816c7cb97 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -121,6 +121,12 @@ funR2 (r : R) : R := | 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' r := r@R{r1 := 2}; + -- 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 0afabfa42b..86fe06954f 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -158,12 +158,33 @@ fun funR2 :: "R \ R" where let r1'0 = R.r2 v'0; r2'0 = R.r1 v'0 - in (| R.r1 = r1'0, R.r2 = r2'0 |))) | - v'0 \ - let - r1'0 = R.r2 v'0; - r2'0 = R.r1 v'0 - in (| R.r1 = r1'0, R.r2 = r2'0 |)))" + in (| R.r1 = r1'0, R.r2 = r2'0 |)))))" + +fun funR3 :: "(R, R) Either' \ R" where + "funR3 er = + (case er of + v' \ + (case v' 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 v' of + (Left' v'0) \ + let + r1'0 = R.r2 v'0; + r2'0 = R.r1 v'0 + in (| R.r1 = r1'0, R.r2 = r2'0 |) | + (Right' r) \ + (\ x0 . case x0 of + v'0 \ (| R.r1 = 2, R.r2 = R.r2 v'0 |)) r)) | + (Right' r) \ + (\ x0 . case x0 of + v'0 \ (| R.r1 = 2, R.r2 = R.r2 v'0 |)) r))" fun bf :: "bool \ bool \ bool" where "bf b1 b2 = (\ (b1 \ b2))" From 0759a454b3bab97f11d2cd07896befb38300dd3a Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 22 Aug 2024 20:08:04 +0200 Subject: [PATCH 07/13] named patterns --- .../Backend/Isabelle/Translation/FromTyped.hs | 94 ++++++++++++------- tests/positive/Isabelle/Program.juvix | 3 + tests/positive/Isabelle/isabelle/Program.thy | 87 +++++++++-------- 3 files changed, 114 insertions(+), 70 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index 52ba24e008..2c1349bc0d 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 @@ -193,7 +194,7 @@ goModule onlyTypes infoTable Internal.Module {..} = oneClause expr = nonEmpty' [ Clause - { _clausePatterns = nonEmpty' $ map PatVar argnames, + { _clausePatterns = nonEmpty' (map PatVar argnames), _clauseBody = expr } ] @@ -210,13 +211,28 @@ goModule onlyTypes infoTable Internal.Module {..} = : goClauses cls Nested pats npats -> let rhs = goExpression'' nset' nmap' _lambdaBody - vnames = map (overNameText (disambiguate (nset' ^. nameSet))) argnames + 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 (nonEmpty' (map ExprIden vnames))) - brs = goNestedBranches valTuple rhs remainingBranches (PatTuple (Tuple (nonEmpty' pats))) (nonEmpty' npats) + valTuple = ExprTuple (Tuple (fmap ExprIden vnames)) + patTuple = PatTuple (Tuple (nonEmpty' pats)) + brs = goNestedBranches valTuple rhs remainingBranches patTuple (nonEmpty' npats) in [ Clause - { _clausePatterns = nonEmpty' $ map PatVar vnames, + { _clausePatterns = fmap PatVar vnames, _clauseBody = ExprCase Case @@ -890,6 +906,18 @@ goModule onlyTypes infoTable Internal.Module {..} = ] [] -> 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) @@ -914,18 +942,33 @@ goModule onlyTypes infoTable Internal.Module {..} = 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 {..} = - -- TODO: named patterns - goPattern isTop _patternArgPattern - - goNestedPatternArg :: forall r. (Members '[State NameSet, State NameMap, Output (Expression, Nested Pattern)] r) => Bool -> Internal.PatternArg -> Sem r (Nested Pattern) - goNestedPatternArg isTop Internal.PatternArg {..} = - -- TODO: named patterns - goNestedPattern isTop _patternArgPattern - - goNestedPattern :: forall r. (Members '[State NameSet, State NameMap, Output (Expression, Nested Pattern)] r) => Bool -> Internal.Pattern -> Sem r (Nested Pattern) - goNestedPattern isTop pat = do - (npats, pat') <- runOutputList $ goPattern isTop pat + 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 @@ -960,13 +1003,13 @@ goModule onlyTypes infoTable Internal.Module {..} = let name' = overNameText (\n -> indName ^. nameText <> "." <> n) name in ExprApp (Application (ExprIden name') (ExprIden vname)) vname = defaultName (disambiguate binders "v") - fieldsVars = map (second getPatternArgVar) $ map (first adjustName) $ filter (isPatternArgVar . snd) fields + 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 False)) fieldsNonVars + fieldsNonVars' <- mapM (secondM goNestedPatternArg) fieldsNonVars forM fieldsNonVars' output return (PatVar vname) | Just (x, y) <- getPairPat _constrAppConstructor _constrAppParameters = do @@ -988,19 +1031,6 @@ goModule onlyTypes infoTable Internal.Module {..} = _constrAppArgs = args } - isPatternArgVar :: Internal.PatternArg -> Bool - isPatternArgVar Internal.PatternArg {..} = - isNothing _patternArgName - && case _patternArgPattern of - Internal.PatternVariable {} -> True - _ -> False - - getPatternArgVar :: Internal.PatternArg -> Name - getPatternArgVar Internal.PatternArg {..} = - case _patternArgPattern of - Internal.PatternVariable name -> name - _ -> impossible - -- This function cannot be simply merged with `getList` because in patterns -- the constructors don't get the type arguments. getListPat :: Name -> [Internal.PatternArg] -> Maybe [Internal.PatternArg] diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index f816c7cb97..ca9945a9c5 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -102,6 +102,9 @@ type R := mkR { 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}; diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index 86fe06954f..6a80198de9 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -55,10 +55,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 = @@ -66,7 +66,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 = @@ -80,8 +80,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 [] []" @@ -109,17 +109,28 @@ fun r1 :: "R \ nat" where 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 = - (case r of - v \ + "funR r' = + (case r' of + v' \ (\ x0 . case x0 of - v' \ (| R.r1 = R.r1 v' + R.r2 v', R.r2 = R.r2 v' |)) r)" + v'0 \ (| R.r1 = R.r1 v'0 + R.r2 v'0, R.r2 = R.r2 v'0 |)) r')" fun funRR :: "R \ R" where - "funRR (| R.r1 = r1'0, R.r2 = r2'0 |) = - ((\ x0 . case x0 of - v \ (| R.r1 = R.r1 v + R.r2 v, R.r2 = R.r2 v |)) r)" + "funRR r'0 = + (case (r'0) of + (r') \ + (case (r') of + (v') \ + (\ x0 . case x0 of + v'0 \ + (| R.r1 = R.r1 v'0 + R.r2 v'0, R.r2 = R.r2 v'0 |)) r'))" fun funR' :: "R \ R" where "funR' (| R.r1 = rr1, R.r2 = rr2 |) = @@ -141,50 +152,50 @@ fun funR1 :: "R \ R" where in (| R.r1 = r1'0, R.r2 = r2'0 |))" fun funR2 :: "R \ R" where - "funR2 r = - (case r of - v' \ - (case v' of - v \ - (case (R.r1 v) of + "funR2 r' = + (case r' of + v'0 \ + (case v'0 of + v' \ + (case (R.r1 v') of (0) \ let - r1'0 = R.r2 v; - r2'0 = R.r2 v + r1'0 = R.r2 v'; + r2'0 = R.r2 v' in (| R.r1 = r1'0, R.r2 = r2'0 |) | _ \ - (case v' of - v'0 \ + (case v'0 of + v'1 \ let - r1'0 = R.r2 v'0; - r2'0 = R.r1 v'0 + r1'0 = R.r2 v'1; + r2'0 = R.r1 v'1 in (| R.r1 = r1'0, R.r2 = r2'0 |)))))" fun funR3 :: "(R, R) Either' \ R" where "funR3 er = (case er of - v' \ - (case v' of - (Left' v) \ - (case (R.r1 v) of + v'0 \ + (case v'0 of + (Left' v') \ + (case (R.r1 v') of (0) \ let - r1'0 = R.r2 v; - r2'0 = R.r2 v + r1'0 = R.r2 v'; + r2'0 = R.r2 v' in (| R.r1 = r1'0, R.r2 = r2'0 |) | _ \ - (case v' of - (Left' v'0) \ + (case v'0 of + (Left' v'1) \ let - r1'0 = R.r2 v'0; - r2'0 = R.r1 v'0 + r1'0 = R.r2 v'1; + r2'0 = R.r1 v'1 in (| R.r1 = r1'0, R.r2 = r2'0 |) | - (Right' r) \ + (Right' r') \ (\ x0 . case x0 of - v'0 \ (| R.r1 = 2, R.r2 = R.r2 v'0 |)) r)) | - (Right' r) \ + v'1 \ (| R.r1 = 2, R.r2 = R.r2 v'1 |)) r')) | + (Right' r') \ (\ x0 . case x0 of - v'0 \ (| R.r1 = 2, R.r2 = R.r2 v'0 |)) r))" + v'1 \ (| R.r1 = 2, R.r2 = R.r2 v'1 |)) r'))" fun bf :: "bool \ bool \ bool" where "bf b1 b2 = (\ (b1 \ b2))" From 07f4337dea4ff59d08fd82d73cca651aa71c3f53 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 22 Aug 2024 20:22:56 +0200 Subject: [PATCH 08/13] fix name disambiguation --- .../Backend/Isabelle/Translation/FromTyped.hs | 4 +- tests/positive/Isabelle/Program.juvix | 7 ++- tests/positive/Isabelle/isabelle/Program.thy | 58 +++++++++++++++++-- 3 files changed, 59 insertions(+), 10 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index 2c1349bc0d..a16de79dad 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -833,9 +833,9 @@ goModule onlyTypes infoTable Internal.Module {..} = } : brs' Nested pat npats -> do - rhs <- withLocalNames nset nmap $ goCaseBranchRhs _caseBranchRhs 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 @@ -888,9 +888,9 @@ goModule onlyTypes infoTable Internal.Module {..} = } : brs Nested pat npats -> do - rhs <- withLocalNames nset nmap $ goExpression _lambdaBody 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 diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index ca9945a9c5..ffc3b2d62b 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -126,9 +126,10 @@ funR2 (r : R) : R := 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' r := r@R{r1 := 2}; + | 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}; -- Standard library diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index 6a80198de9..a911d4ed5f 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -190,12 +190,60 @@ fun funR3 :: "(R, R) Either' \ R" where 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 + v'4 \ + (case v'4 of + (Right' r') \ + (case (r') of + (v'3) \ + (\ x0 . case x0 of + v'5 \ + (| R.r1 = R.r2 v'5 + 2, R.r2 = R.r1 v'5 + 3 |)) r')))) | + v'4 \ + (case v'4 of + (Right' r') \ + (case (r') of + (v'3) \ + (\ x0 . case x0 of + v'5 \ + (| R.r1 = R.r2 v'5 + 2, R.r2 = R.r1 v'5 + 3 |)) r'))))) | + 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 + v'4 \ + (case v'4 of + (Right' r') \ + (case (r') of + (v'3) \ + (\ x0 . case x0 of + v'5 \ + (| R.r1 = R.r2 v'5 + 2, R.r2 = R.r1 v'5 + 3 |)) r')))) | + v'4 \ + (case v'4 of (Right' r') \ - (\ x0 . case x0 of - v'1 \ (| R.r1 = 2, R.r2 = R.r2 v'1 |)) r')) | - (Right' r') \ - (\ x0 . case x0 of - v'1 \ (| R.r1 = 2, R.r2 = R.r2 v'1 |)) r'))" + (case (r') of + (v'3) \ + (\ x0 . case x0 of + v'5 \ + (| R.r1 = R.r2 v'5 + 2, R.r2 = R.r1 v'5 + 3 |)) r')))))" fun bf :: "bool \ bool \ bool" where "bf b1 b2 = (\ (b1 \ b2))" From 7298271acaf95ecb79211e61038c5b2644c20622 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 22 Aug 2024 21:36:05 +0200 Subject: [PATCH 09/13] record update translation --- .../Backend/Isabelle/Translation/FromTyped.hs | 45 ++++++++++++++++++- tests/positive/Isabelle/Program.juvix | 3 ++ tests/positive/Isabelle/isabelle/Program.thy | 33 ++++++-------- 3 files changed, 59 insertions(+), 22 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index a16de79dad..26d8c5f965 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -65,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) -> [] @@ -498,6 +498,16 @@ goModule onlyTypes infoTable Internal.Module {..} = | 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 @@ -666,6 +676,33 @@ goModule onlyTypes infoTable Internal.Module {..} = 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') @@ -1000,7 +1037,7 @@ goModule onlyTypes infoTable Internal.Module {..} = binders <- gets (^. nameSet) let adjustName :: Name -> Expression adjustName name = - let name' = overNameText (\n -> indName ^. nameText <> "." <> n) 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 @@ -1112,6 +1149,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 diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index ffc3b2d62b..31dafdd1ca 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -131,6 +131,9 @@ funR3 (er : Either' R R) : R := | 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 a911d4ed5f..6a539b1707 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -118,19 +118,14 @@ definition v :: nat where fun funR :: "R \ R" where "funR r' = (case r' of - v' \ - (\ x0 . case x0 of - v'0 \ (| R.r1 = R.r1 v'0 + R.r2 v'0, R.r2 = R.r2 v'0 |)) r')" + v' \ r' (| R.r1 := R.r1 r' + R.r2 r' |))" fun funRR :: "R \ R" where "funRR r'0 = (case (r'0) of (r') \ (case (r') of - (v') \ - (\ x0 . case x0 of - v'0 \ - (| R.r1 = R.r1 v'0 + R.r2 v'0, R.r2 = R.r2 v'0 |)) r'))" + (v') \ r' (| R.r1 := R.r1 r' + R.r2 r' |)))" fun funR' :: "R \ R" where "funR' (| R.r1 = rr1, R.r2 = rr2 |) = @@ -206,17 +201,13 @@ fun funR3 :: "(R, R) Either' \ R" where (Right' r') \ (case (r') of (v'3) \ - (\ x0 . case x0 of - v'5 \ - (| R.r1 = R.r2 v'5 + 2, R.r2 = R.r1 v'5 + 3 |)) r')))) | + r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))) | v'4 \ (case v'4 of (Right' r') \ (case (r') of (v'3) \ - (\ x0 . case x0 of - v'5 \ - (| R.r1 = R.r2 v'5 + 2, R.r2 = R.r1 v'5 + 3 |)) r'))))) | + r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |)))))) | v'2 \ (case v'2 of (Right' v'1) \ @@ -233,17 +224,19 @@ fun funR3 :: "(R, R) Either' \ R" where (Right' r') \ (case (r') of (v'3) \ - (\ x0 . case x0 of - v'5 \ - (| R.r1 = R.r2 v'5 + 2, R.r2 = R.r1 v'5 + 3 |)) r')))) | + r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))) | v'4 \ (case v'4 of (Right' r') \ (case (r') of - (v'3) \ - (\ x0 . case x0 of - v'5 \ - (| R.r1 = R.r2 v'5 + 2, R.r2 = R.r1 v'5 + 3 |)) r')))))" + (v'3) \ r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))))" + +fun funR4 :: "R \ R" where + "funR4 r'0 = + (case (r'0) of + (r') \ + (case (r') of + (v') \ r' (| R.r2 := R.r1 r' |)))" fun bf :: "bool \ bool \ bool" where "bf b1 b2 = (\ (b1 \ b2))" From 13babbf157feeb8f1afcdd9e3296a6626e38a57d Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 22 Aug 2024 21:42:14 +0200 Subject: [PATCH 10/13] fix record update printing --- .../Compiler/Backend/Isabelle/Pretty/Base.hs | 23 ++++++++++--------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs index a06a5fae85..3136d6858b 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs @@ -82,7 +82,7 @@ instance PrettyCode Expression where ExprTuple x -> ppCode x ExprList x -> ppCode x ExprCons x -> ppCode x - ExprRecord x -> ppCode x + ExprRecord x -> ppRecord False x ExprRecordUpdate x -> ppCode x ExprLet x -> ppCode x ExprIf x -> ppCode x @@ -110,7 +110,7 @@ instance PrettyCode Binop where instance PrettyCode RecordUpdate where ppCode RecordUpdate {..} = do r <- ppCode _recordUpdateRecord - fields <- ppCode _recordUpdateFields + fields <- ppRecord True _recordUpdateFields return $ r <+> fields instance PrettyCode LetClause where @@ -155,14 +155,15 @@ instance (PrettyCode a) => PrettyCode (List a) where elems <- mapM ppCode _listElements return $ brackets $ hsep (punctuate comma elems) -instance (PrettyCode a) => PrettyCode (Record a) where - ppCode Record {..} = do - recName <- ppCode _recordName - names <- mapM (ppCode . fst) _recordFields - elems <- mapM (ppCode . snd) _recordFields - let names' = map (\n -> recName <> "." <> n) names - fields = zipWithExact (\n e -> n <+> "=" <+> e) names' elems - return $ "(|" <+> hsep (punctuate comma fields) <+> "|)" +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 @@ -178,7 +179,7 @@ instance PrettyCode Pattern where PatTuple x -> ppCode x PatList x -> ppCode x PatCons x -> ppCode x - PatRecord x -> ppCode x + PatRecord x -> ppRecord False x instance PrettyCode ConstrApp where ppCode ConstrApp {..} = do From ee27806e723ad9b80c07b50ddb74f841bc6c9f48 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 23 Aug 2024 12:06:10 +0200 Subject: [PATCH 11/13] remove spurious pattern matches --- src/Juvix/Compiler/Backend/Isabelle/Extra.hs | 101 +++++++++++- .../Backend/Isabelle/Translation/FromTyped.hs | 34 +++- tests/positive/Isabelle/isabelle/Program.thy | 145 +++++++----------- 3 files changed, 181 insertions(+), 99 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs b/src/Juvix/Compiler/Backend/Isabelle/Extra.hs index 60e51bd81d..e6483aa755 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Extra.hs @@ -25,9 +25,104 @@ subsumesPattern pat1 pat2 = case (pat1, pat2) of subsumesPattern c1 c2 && subsumesPattern p1 p2 (PatRecord (Record n1 r1), PatRecord (Record n2 r2)) -> n1 == n2 - && map fst r1' == map fst r2' + && map ((^. nameText) . fst) r1' == map ((^. nameText) . fst) r2' && all (uncurry subsumesPattern) (zipExact (map snd r1') (map snd r2')) where - r1' = sortOn fst r1 - r2' = sortOn fst r2 + 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/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index 26d8c5f965..29897e3fa7 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -85,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) $ @@ -234,7 +252,7 @@ goModule onlyTypes infoTable Internal.Module {..} = in [ Clause { _clausePatterns = fmap PatVar vnames, _clauseBody = - ExprCase + mkExprCase Case { _caseValue = valTuple, _caseBranches = brs @@ -255,7 +273,7 @@ goModule onlyTypes infoTable Internal.Module {..} = in CaseBranch { _caseBranchPattern = pat, _caseBranchBody = - ExprCase + mkExprCase Case { _caseValue = val, _caseBranches = brs @@ -271,7 +289,7 @@ goModule onlyTypes infoTable Internal.Module {..} = CaseBranch { _caseBranchPattern = PatVar (defaultName "_"), _caseBranchBody = - ExprCase + mkExprCase Case { _caseValue = val, _caseBranches = nonEmpty' remainingBranches @@ -294,7 +312,7 @@ goModule onlyTypes infoTable Internal.Module {..} = in CaseBranch { _caseBranchPattern = pat, _caseBranchBody = - ExprCase + mkExprCase Case { _caseValue = val, _caseBranches = brs @@ -838,7 +856,7 @@ goModule onlyTypes infoTable Internal.Module {..} = } brs <- goLambdaClauses (toList _lambdaClauses) return $ - ExprCase + mkExprCase Case { _caseValue = val, _caseBranches = nonEmpty' brs @@ -849,7 +867,7 @@ goModule onlyTypes infoTable Internal.Module {..} = val <- goExpression _caseExpression brs <- goCaseBranches (toList _caseBranches) return $ - ExprCase + mkExprCase Case { _caseValue = val, _caseBranches = nonEmpty' brs @@ -879,7 +897,7 @@ goModule onlyTypes infoTable Internal.Module {..} = [ CaseBranch { _caseBranchPattern = PatVar vname, _caseBranchBody = - ExprCase + mkExprCase Case { _caseValue = ExprIden vname, _caseBranches = brs' @@ -934,7 +952,7 @@ goModule onlyTypes infoTable Internal.Module {..} = [ CaseBranch { _caseBranchPattern = PatVar vname, _caseBranchBody = - ExprCase + mkExprCase Case { _caseValue = ExprIden vname, _caseBranches = brs' diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index 6a539b1707..cd1d253f4f 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -91,8 +91,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)" datatype ('A, 'B) Either' @@ -116,16 +115,10 @@ definition v :: nat where "v = 0" fun funR :: "R \ R" where - "funR r' = - (case r' of - v' \ r' (| R.r1 := R.r1 r' + R.r2 r' |))" + "funR r' = (r' (| R.r1 := R.r1 r' + R.r2 r' |))" fun funRR :: "R \ R" where - "funRR r'0 = - (case (r'0) of - (r') \ - (case (r') of - (v') \ r' (| R.r1 := R.r1 r' + R.r2 r' |)))" + "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 |) = @@ -148,95 +141,71 @@ fun funR1 :: "R \ R" where fun funR2 :: "R \ R" where "funR2 r' = - (case r' of - v'0 \ - (case v'0 of - 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 v'0 of - v'1 \ - let - r1'0 = R.r2 v'1; - r2'0 = R.r1 v'1 - in (| R.r1 = r1'0, R.r2 = r2'0 |)))))" + (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 - v'0 \ - (case v'0 of - (Left' v') \ - (case (R.r1 v') 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 = R.r2 v'; - r2'0 = R.r2 v' + r1'0 = 7; + r2'0 = 7 in (| R.r1 = r1'0, R.r2 = r2'0 |) | _ \ - (case v'0 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 - v'4 \ - (case v'4 of - (Right' r') \ - (case (r') of - (v'3) \ - r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))) | - v'4 \ - (case v'4 of - (Right' r') \ - (case (r') of - (v'3) \ - 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 - v'4 \ - (case v'4 of - (Right' r') \ - (case (r') of - (v'3) \ - r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))) | - v'4 \ - (case v'4 of + (case v'2 of (Right' r') \ - (case (r') of - (v'3) \ r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))))" + 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 = - (case (r'0) of - (r') \ - (case (r') of - (v') \ r' (| R.r2 := R.r1 r' |)))" + "funR4 r'0 = (r'0 (| R.r2 := R.r1 r'0 |))" fun bf :: "bool \ bool \ bool" where "bf b1 b2 = (\ (b1 \ b2))" From 7fd84c512fc47a81b46c9aaf0726b2a91a6992b9 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 12:22:57 +0200 Subject: [PATCH 12/13] Update src/Juvix/Compiler/Backend/Isabelle/Extra.hs Co-authored-by: Jan Mas Rovira --- src/Juvix/Compiler/Backend/Isabelle/Extra.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs b/src/Juvix/Compiler/Backend/Isabelle/Extra.hs index e6483aa755..cda612cd5f 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Extra.hs @@ -65,7 +65,7 @@ substVar var var' = go ExprApp (Application (go fn) (go arg)) goBinop :: Binop -> Expression - goBinop (Binop {..}) = + goBinop Binop {..} = ExprBinop Binop { _binopOperator, From 745f0dbdd2b302f35c1cf2f19f3d0c48a3bb3cad 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 12:23:03 +0200 Subject: [PATCH 13/13] Update src/Juvix/Compiler/Backend/Isabelle/Extra.hs Co-authored-by: Jan Mas Rovira --- src/Juvix/Compiler/Backend/Isabelle/Extra.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs b/src/Juvix/Compiler/Backend/Isabelle/Extra.hs index cda612cd5f..6b398aee43 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Extra.hs @@ -119,7 +119,7 @@ substVar var var' = go PatRecord (Record n r) -> PatRecord (Record n (map (second goPattern) r)) goLambda :: Lambda -> Expression - goLambda (Lambda {..}) = + goLambda Lambda {..} = ExprLambda Lambda { _lambdaVar = goName _lambdaVar,