diff --git a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs b/src/Juvix/Compiler/Backend/Isabelle/Extra.hs index b0db4c823a..6b398aee43 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Extra.hs @@ -1,8 +1,128 @@ module Juvix.Compiler.Backend.Isabelle.Extra where +import Data.List.NonEmpty.Extra qualified as NonEmpty import Juvix.Compiler.Backend.Isabelle.Language mkApp :: Expression -> [Expression] -> Expression mkApp fn = \case [] -> fn arg : args -> mkApp (ExprApp (Application fn arg)) args + +-- | Check if a pattern `pat1` subsumes another pattern `pat2`. +subsumesPattern :: Pattern -> Pattern -> Bool +subsumesPattern pat1 pat2 = case (pat1, pat2) of + (PatVar _, _) -> True + (PatZero, PatZero) -> True + (PatConstrApp (ConstrApp c1 p1), PatConstrApp (ConstrApp c2 p2)) -> + c1 == c2 && all (uncurry subsumesPattern) (zipExact p1 p2) + (PatTuple (Tuple p1), PatTuple (Tuple p2)) -> + length p1 == length p2 + && all (uncurry subsumesPattern) (NonEmpty.zip p1 p2) + (PatList (List p1), PatList (List p2)) -> + length p1 == length p2 + && all (uncurry subsumesPattern) (zipExact p1 p2) + (PatCons (Cons c1 p1), PatCons (Cons c2 p2)) -> + subsumesPattern c1 c2 && subsumesPattern p1 p2 + (PatRecord (Record n1 r1), PatRecord (Record n2 r2)) -> + n1 == n2 + && map ((^. nameText) . fst) r1' == map ((^. nameText) . fst) r2' + && all (uncurry subsumesPattern) (zipExact (map snd r1') (map snd r2')) + where + r1' = sortOn ((^. nameText) . fst) r1 + r2' = sortOn ((^. nameText) . fst) r2 + _ -> False + +-- | Rename all occurrences of a variable in an expression. Also renames bound +-- variables. +substVar :: Name -> Name -> Expression -> Expression +substVar var var' = go + where + go :: Expression -> Expression + go = \case + ExprIden x -> goIden x + ExprUndefined -> ExprUndefined + ExprLiteral x -> ExprLiteral x + ExprApp x -> goApplication x + ExprBinop x -> goBinop x + ExprTuple x -> goTuple x + ExprList x -> goList x + ExprCons x -> goCons x + ExprRecord x -> goRecord x + ExprRecordUpdate x -> goRecordUpdate x + ExprLet x -> goLet x + ExprIf x -> goIf x + ExprCase x -> goCase x + ExprLambda x -> goLambda x + + goName :: Name -> Name + goName x = if x ^. nameText == var ^. nameText then var' else x + + goIden :: Name -> Expression + goIden = ExprIden . goName + + goApplication :: Application -> Expression + goApplication (Application fn arg) = + ExprApp (Application (go fn) (go arg)) + + goBinop :: Binop -> Expression + goBinop Binop {..} = + ExprBinop + Binop + { _binopOperator, + _binopLeft = go _binopLeft, + _binopRight = go _binopRight, + _binopFixity + } + + goTuple :: Tuple Expression -> Expression + goTuple (Tuple xs) = ExprTuple (Tuple (fmap go xs)) + + goList :: List Expression -> Expression + goList (List xs) = ExprList (List (map go xs)) + + goCons :: Cons Expression -> Expression + goCons (Cons h t) = ExprCons (Cons (go h) (go t)) + + goRecord' :: Record Expression -> Record Expression + goRecord' (Record n r) = Record n (map (second go) r) + + goRecord :: Record Expression -> Expression + goRecord = ExprRecord . goRecord' + + goRecordUpdate :: RecordUpdate -> Expression + goRecordUpdate (RecordUpdate r f) = + ExprRecordUpdate (RecordUpdate (go r) (goRecord' f)) + + goLet :: Let -> Expression + goLet (Let cs e) = ExprLet (Let (fmap goLetClause cs) (go e)) + + goLetClause :: LetClause -> LetClause + goLetClause (LetClause n e) = LetClause (goName n) (go e) + + goIf :: If -> Expression + goIf (If v t f) = ExprIf (If (go v) (go t) (go f)) + + goCase :: Case -> Expression + goCase (Case v bs) = ExprCase (Case (go v) (fmap goCaseBranch bs)) + + goCaseBranch :: CaseBranch -> CaseBranch + goCaseBranch (CaseBranch p e) = CaseBranch (goPattern p) (go e) + + goPattern :: Pattern -> Pattern + goPattern = \case + PatVar x -> PatVar (goName x) + PatZero -> PatZero + PatConstrApp (ConstrApp c p) -> PatConstrApp (ConstrApp c (fmap goPattern p)) + PatTuple (Tuple p) -> PatTuple (Tuple (fmap goPattern p)) + PatList (List p) -> PatList (List (fmap goPattern p)) + PatCons (Cons h t) -> PatCons (Cons (goPattern h) (goPattern t)) + PatRecord (Record n r) -> PatRecord (Record n (map (second goPattern) r)) + + goLambda :: Lambda -> Expression + goLambda Lambda {..} = + ExprLambda + Lambda + { _lambdaVar = goName _lambdaVar, + _lambdaBody = go _lambdaBody, + _lambdaType + } diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs index bac6820f44..00fc381e4d 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Language.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Language.hs @@ -55,6 +55,8 @@ data Expression | ExprTuple (Tuple Expression) | ExprList (List Expression) | ExprCons (Cons Expression) + | ExprRecord (Record Expression) + | ExprRecordUpdate RecordUpdate | ExprLet Let | ExprIf If | ExprCase Case @@ -76,6 +78,11 @@ data Binop = Binop _binopFixity :: Fixity } +data RecordUpdate = RecordUpdate + { _recordUpdateRecord :: Expression, + _recordUpdateFields :: Record Expression + } + data Let = Let { _letClauses :: NonEmpty LetClause, _letBody :: Expression @@ -115,6 +122,7 @@ data Pattern | PatTuple (Tuple Pattern) | PatList (List Pattern) | PatCons (Cons Pattern) + | PatRecord (Record Pattern) newtype Tuple a = Tuple { _tupleComponents :: NonEmpty a @@ -129,6 +137,11 @@ data Cons a = Cons _consTail :: a } +data Record a = Record + { _recordName :: Name, + _recordFields :: [(Name, a)] + } + data ConstrApp = ConstrApp { _constrAppConstructor :: Name, _constrAppArgs :: [Pattern] @@ -143,13 +156,19 @@ makeLenses ''CaseBranch makeLenses ''Lambda makeLenses ''ConstrApp makeLenses ''Expression +makeLenses ''Binop +makeLenses ''RecordUpdate +makeLenses ''Tuple +makeLenses ''List +makeLenses ''Cons +makeLenses ''Record data Statement = StmtDefinition Definition | StmtFunction Function | StmtSynonym Synonym | StmtDatatype Datatype - | StmtRecord Record + | StmtRecord RecordDef data Definition = Definition { _definitionName :: Name, @@ -189,11 +208,11 @@ data Constructor = Constructor _constructorDocComment :: Maybe Text } -data Record = Record - { _recordName :: Name, - _recordParams :: [TypeVar], - _recordFields :: [RecordField], - _recordDocComment :: Maybe Text +data RecordDef = RecordDef + { _recordDefName :: Name, + _recordDefParams :: [TypeVar], + _recordDefFields :: [RecordField], + _recordDefDocComment :: Maybe Text } data RecordField = RecordField @@ -207,9 +226,7 @@ makeLenses ''Function makeLenses ''Synonym makeLenses ''Datatype makeLenses ''Constructor -makeLenses ''Record makeLenses ''RecordField -makeLenses ''Tuple data Theory = Theory { _theoryName :: Name, @@ -296,6 +313,8 @@ instance HasAtomicity Expression where ExprTuple {} -> Atom ExprList {} -> Atom ExprCons {} -> Aggregate consFixity + ExprRecord {} -> Aggregate appFixity + ExprRecordUpdate {} -> Aggregate appFixity ExprLet {} -> Aggregate letFixity ExprIf {} -> Aggregate ifFixity ExprCase {} -> Aggregate caseFixity @@ -311,3 +330,4 @@ instance HasAtomicity Pattern where PatTuple {} -> Atom PatList {} -> Atom PatCons {} -> Aggregate consFixity + PatRecord {} -> Atom diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs index 543652d4ed..22a1c016cf 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs @@ -102,6 +102,8 @@ instance PrettyCode Expression where ExprTuple x -> ppCode x ExprList x -> ppCode x ExprCons x -> ppCode x + ExprRecord x -> ppRecord False x + ExprRecordUpdate x -> ppCode x ExprLet x -> ppCode x ExprIf x -> ppCode x ExprCase x -> ppCode x @@ -125,6 +127,12 @@ instance PrettyCode Binop where r <- ppRightExpression _binopFixity _binopRight return $ l <+> op <+> r +instance PrettyCode RecordUpdate where + ppCode RecordUpdate {..} = do + r <- ppCode _recordUpdateRecord + fields <- ppRecord True _recordUpdateFields + return $ r <+> fields + instance PrettyCode LetClause where ppCode LetClause {..} = do name <- ppCode _letClauseName @@ -165,7 +173,17 @@ instance (PrettyCode a) => PrettyCode (Tuple a) where instance (PrettyCode a) => PrettyCode (List a) where ppCode List {..} = do elems <- mapM ppCode _listElements - return $ brackets $ hsep (punctuate comma (toList elems)) + return $ brackets $ hsep (punctuate comma elems) + +ppRecord :: (PrettyCode a, Member (Reader Options) r) => Bool -> Record a -> Sem r (Doc Ann) +ppRecord bUpdate Record {..} = do + recName <- ppCode _recordName + names <- mapM (ppCode . fst) _recordFields + elems <- mapM (ppCode . snd) _recordFields + let names' = map (\n -> recName <> "." <> n) names + eq = if bUpdate then ":=" else "=" + fields = zipWithExact (\n e -> n <+> eq <+> e) names' elems + return $ "(|" <+> hsep (punctuate comma fields) <+> "|)" instance (PrettyCode a, HasAtomicity a) => PrettyCode (Cons a) where ppCode Cons {..} = do @@ -181,6 +199,7 @@ instance PrettyCode Pattern where PatTuple x -> ppCode x PatList x -> ppCode x PatCons x -> ppCode x + PatRecord x -> ppRecord False x instance PrettyCode ConstrApp where ppCode ConstrApp {..} = do @@ -253,12 +272,12 @@ instance PrettyCode Constructor where tys <- mapM ppCodeQuoted _constructorArgTypes return $ comment <> hsep (n : tys) -instance PrettyCode Record where - ppCode Record {..} = do - let comment = prettyTextComment _recordDocComment - n <- ppCode _recordName - params <- ppParams _recordParams - fields <- mapM ppCode _recordFields +instance PrettyCode RecordDef where + ppCode RecordDef {..} = do + let comment = prettyTextComment _recordDefDocComment + n <- ppCode _recordDefName + params <- ppParams _recordDefParams + fields <- mapM ppCode _recordDefFields return $ comment <> kwRecord <+> params n <+> "=" <> line <> indent' (vsep fields) instance PrettyCode RecordField where diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index fb74a797de..0ffc72b221 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -2,6 +2,7 @@ module Juvix.Compiler.Backend.Isabelle.Translation.FromTyped where import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet +import Data.List.NonEmpty.Extra qualified as NonEmpty import Data.Text qualified as T import Data.Text qualified as Text import Juvix.Compiler.Backend.Isabelle.Data.Result @@ -21,12 +22,22 @@ newtype NameSet = NameSet } newtype NameMap = NameMap - { _nameMap :: HashMap Name Name + { _nameMap :: HashMap Name Expression } makeLenses ''NameSet makeLenses ''NameMap +data Nested a = Nested + { _nestedElem :: a, + _nestedPatterns :: NestedPatterns + } + deriving stock (Functor) + +type NestedPatterns = [(Expression, Nested Pattern)] + +makeLenses ''Nested + fromInternal :: forall r. (Members '[Error JuvixError, Reader EntryPoint, Reader ModuleTable, NameIdGen] r) => @@ -54,7 +65,7 @@ fromInternal Internal.InternalTypedResult {..} = do goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory goModule onlyTypes infoTable Internal.Module {..} = Theory - { _theoryName = over nameText toIsabelleName $ over namePretty toIsabelleName _moduleName, + { _theoryName = overNameText toIsabelleName _moduleName, _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports), _theoryStatements = case _modulePragmas ^. pragmasIsabelleIgnore of Just (PragmaIsabelleIgnore True) -> [] @@ -74,6 +85,24 @@ goModule onlyTypes infoTable Internal.Module {..} = StmtDatatype {} -> True StmtRecord {} -> True + mkExprCase :: Case -> Expression + mkExprCase c@Case {..} = case _caseValue of + ExprIden v -> + case _caseBranches of + CaseBranch {..} :| [] -> + case _caseBranchPattern of + PatVar v' -> substVar v' v _caseBranchBody + _ -> ExprCase c + _ -> ExprCase c + ExprTuple (Tuple (ExprIden v :| [])) -> + case _caseBranches of + CaseBranch {..} :| [] -> + case _caseBranchPattern of + PatTuple (Tuple (PatVar v' :| [])) -> substVar v' v _caseBranchBody + _ -> ExprCase c + _ -> ExprCase c + _ -> ExprCase c + goMutualBlock :: Internal.MutualBlock -> [Statement] goMutualBlock Internal.MutualBlock {..} = filter (\stmt -> not onlyTypes || isTypeDef stmt) $ @@ -96,11 +125,11 @@ goModule onlyTypes infoTable Internal.Module {..} = && head' _inductiveConstructors ^. Internal.inductiveConstructorIsRecord = let tyargs = fst $ Internal.unfoldFunType $ head' _inductiveConstructors ^. Internal.inductiveConstructorType in StmtRecord - Record - { _recordName = _inductiveName, - _recordParams = params, - _recordFields = map goRecordField tyargs, - _recordDocComment = _inductiveDocComment + RecordDef + { _recordDefName = _inductiveName, + _recordDefParams = params, + _recordDefFields = map goRecordField tyargs, + _recordDefDocComment = _inductiveDocComment } | otherwise = StmtDatatype @@ -178,7 +207,7 @@ goModule onlyTypes infoTable Internal.Module {..} = -- We assume here that all clauses have the same number of patterns Just (Internal.ExpressionLambda Internal.Lambda {..}) | not $ null $ filterTypeArgs 0 ty $ toList $ head _lambdaClauses ^. Internal.lambdaPatterns -> - fmap goClause _lambdaClauses + nonEmpty' $ goClauses $ toList _lambdaClauses | otherwise -> oneClause (goExpression'' nset (NameMap mempty) (head _lambdaClauses ^. Internal.lambdaBody)) Just body -> oneClause (goExpression'' nset (NameMap mempty) body) @@ -190,19 +219,113 @@ goModule onlyTypes infoTable Internal.Module {..} = oneClause expr = nonEmpty' [ Clause - { _clausePatterns = nonEmpty' $ map PatVar argnames, + { _clausePatterns = nonEmpty' (map PatVar argnames), _clauseBody = expr } ] - goClause :: Internal.LambdaClause -> Clause - goClause Internal.LambdaClause {..} = - Clause - { _clausePatterns = nonEmpty' pats, - _clauseBody = goExpression'' nset' nmap' _lambdaBody + goClauses :: [Internal.LambdaClause] -> [Clause] + goClauses = \case + Internal.LambdaClause {..} : cls -> + case npats0 of + Nested pats [] -> + Clause + { _clausePatterns = nonEmpty' pats, + _clauseBody = goExpression'' nset' nmap' _lambdaBody + } + : goClauses cls + Nested pats npats -> + let rhs = goExpression'' nset' nmap' _lambdaBody + argnames' = fmap getPatternArgName _lambdaPatterns + vnames = + fmap + ( \(idx :: Int, mname) -> + maybe + ( defaultName + ( disambiguate + (nset' ^. nameSet) + ("v_" <> show idx) + ) + ) + (overNameText (disambiguate (nset' ^. nameSet))) + mname + ) + (NonEmpty.zip (nonEmpty' [0 ..]) argnames') + nset'' = foldl' (flip (over nameSet . HashSet.insert . (^. namePretty))) nset' vnames + remainingBranches = goLambdaClauses'' nset'' nmap' cls + valTuple = ExprTuple (Tuple (fmap ExprIden vnames)) + patTuple = PatTuple (Tuple (nonEmpty' pats)) + brs = goNestedBranches valTuple rhs remainingBranches patTuple (nonEmpty' npats) + in [ Clause + { _clausePatterns = fmap PatVar vnames, + _clauseBody = + mkExprCase + Case + { _caseValue = valTuple, + _caseBranches = brs + } + } + ] + where + (npats0, nset', nmap') = goPatternArgsTop (filterTypeArgs 0 ty (toList _lambdaPatterns)) + [] -> [] + + goNestedBranches :: Expression -> Expression -> [CaseBranch] -> Pattern -> NonEmpty (Expression, Nested Pattern) -> NonEmpty CaseBranch + goNestedBranches caseVal rhs remainingBranches pat npats = + let val = ExprTuple (Tuple (fmap fst npats)) + pat' = PatTuple (Tuple (fmap ((^. nestedElem) . snd) npats)) + npats' = concatMap ((^. nestedPatterns) . snd) npats + brs = goNestedBranches' rhs (mkDefaultBranch caseVal remainingBranches) (Nested pat' npats') + remainingBranches' = filter (not . subsumesPattern pat . (^. caseBranchPattern)) remainingBranches + in CaseBranch + { _caseBranchPattern = pat, + _caseBranchBody = + mkExprCase + Case + { _caseValue = val, + _caseBranches = brs + } } - where - (pats, nset', nmap') = goPatternArgs'' (filterTypeArgs 0 ty (toList _lambdaPatterns)) + :| remainingBranches' + + mkDefaultBranch :: Expression -> [CaseBranch] -> Maybe CaseBranch + mkDefaultBranch val remainingBranches = case remainingBranches of + [] -> Nothing + _ -> + Just $ + CaseBranch + { _caseBranchPattern = PatVar (defaultName "_"), + _caseBranchBody = + mkExprCase + Case + { _caseValue = val, + _caseBranches = nonEmpty' remainingBranches + } + } + + goNestedBranches' :: Expression -> Maybe CaseBranch -> Nested Pattern -> NonEmpty CaseBranch + goNestedBranches' rhs defaultBranch = \case + Nested pat [] -> + CaseBranch + { _caseBranchPattern = pat, + _caseBranchBody = rhs + } + :| toList defaultBranch + Nested pat npats -> do + let val = ExprTuple (Tuple (nonEmpty' (map fst npats))) + pat' = PatTuple (Tuple (nonEmpty' (map ((^. nestedElem) . snd) npats))) + npats' = concatMap ((^. nestedPatterns) . snd) npats + brs = goNestedBranches' rhs defaultBranch (Nested pat' npats') + in CaseBranch + { _caseBranchPattern = pat, + _caseBranchBody = + mkExprCase + Case + { _caseValue = val, + _caseBranches = brs + } + } + :| toList defaultBranch goFunctionDef :: Internal.FunctionDef -> Statement goFunctionDef Internal.FunctionDef {..} = goDef _funDefName _funDefType _funDefArgsInfo (Just _funDefBody) _funDefDocComment @@ -290,24 +413,30 @@ goModule onlyTypes infoTable Internal.Module {..} = _ -> overNameText quote name Nothing -> overNameText quote name - goFunName :: Name -> Name - goFunName name = - case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of - Just funInfo -> - case funInfo ^. Internal.functionInfoPragmas . pragmasIsabelleFunction of - Just PragmaIsabelleFunction {..} -> setNameText _pragmaIsabelleFunctionName name + getArgtys :: Internal.ConstructorInfo -> [Internal.FunctionParameter] + getArgtys ctrInfo = fst $ Internal.unfoldFunType $ ctrInfo ^. Internal.constructorInfoType + + goFunName :: Expression -> Expression + goFunName = \case + ExprIden name -> + ExprIden $ + case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of + Just funInfo -> + case funInfo ^. Internal.functionInfoPragmas . pragmasIsabelleFunction of + Just PragmaIsabelleFunction {..} -> setNameText _pragmaIsabelleFunctionName name + Nothing -> overNameText quote name Nothing -> overNameText quote name - Nothing -> overNameText quote name + x -> x - lookupName :: forall r. (Member (Reader NameMap) r) => Name -> Sem r Name + lookupName :: forall r. (Member (Reader NameMap) r) => Name -> Sem r Expression lookupName name = do nmap <- asks (^. nameMap) - return $ fromMaybe name $ HashMap.lookup name nmap + return $ fromMaybe (ExprIden name) $ HashMap.lookup name nmap localName :: forall a r. (Members '[Reader NameSet, Reader NameMap] r) => Name -> Name -> Sem r a -> Sem r a localName v v' = local (over nameSet (HashSet.insert (v' ^. namePretty))) - . local (over nameMap (HashMap.insert v v')) + . local (over nameMap (HashMap.insert v (ExprIden v'))) localNames :: forall a r. (Members '[Reader NameSet, Reader NameMap] r) => [(Name, Name)] -> Sem r a -> Sem r a localNames vs e = foldl' (flip (uncurry localName)) e vs @@ -316,6 +445,11 @@ goModule onlyTypes infoTable Internal.Module {..} = withLocalNames nset nmap = local (const nset) . local (const nmap) + goRecordFields :: [Internal.FunctionParameter] -> [a] -> [(Name, a)] + goRecordFields argtys args = case (argtys, args) of + (ty : argtys', arg' : args') -> (fromMaybe (defaultName "_") (ty ^. Internal.paramName), arg') : goRecordFields argtys' args' + _ -> [] + goExpression' :: Internal.Expression -> Expression goExpression' = goExpression'' (NameSet mempty) (NameMap mempty) @@ -340,8 +474,7 @@ goModule onlyTypes infoTable Internal.Module {..} = goIden :: Internal.Iden -> Sem r Expression goIden iden = case iden of Internal.IdenFunction name -> do - name' <- lookupName name - return $ ExprIden (goFunName name') + goFunName <$> lookupName name Internal.IdenConstructor name -> case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of Just ctrInfo -> @@ -350,8 +483,7 @@ goModule onlyTypes infoTable Internal.Module {..} = _ -> return $ ExprIden (goConstrName name) Nothing -> return $ ExprIden (goConstrName name) Internal.IdenVar name -> do - name' <- lookupName name - return $ ExprIden name' + lookupName name Internal.IdenAxiom name -> return $ ExprIden (overNameText quote name) Internal.IdenInductive name -> return $ ExprIden (overNameText quote name) @@ -388,6 +520,19 @@ goModule onlyTypes infoTable Internal.Module {..} = x' <- goExpression x y' <- goExpression y return $ ExprTuple (Tuple (x' :| [y'])) + | Just (name, fields) <- getRecordCreation app = do + fields' <- mapM (secondM goExpression) fields + return $ ExprRecord (Record name fields') + | Just (indName, names, record, fields) <- getRecordUpdate app = do + record' <- goExpression record + let names' = map (qualifyRecordProjection indName) names + nset <- ask @NameSet + nmap <- ask @NameMap + let nset' = foldl' (flip (over nameSet . HashSet.insert . (^. namePretty))) nset names' + exprs = map (\n -> ExprApp (Application (ExprIden n) record')) names' + nmap' = foldl' (flip (over nameMap . uncurry HashMap.insert)) nmap (zipExact names exprs) + fields' <- mapM (secondM (withLocalNames nset' nmap' . goExpression)) fields + return $ ExprRecordUpdate (RecordUpdate record' (Record indName fields')) | Just (fn, args) <- getIdentApp app = do fn' <- goExpression fn args' <- mapM goExpression args @@ -542,6 +687,47 @@ goModule onlyTypes infoTable Internal.Module {..} = where (fn, args) = Internal.unfoldApplication app + getRecordCreation :: Internal.Application -> Maybe (Name, [(Name, Internal.Expression)]) + getRecordCreation app = case fn of + Internal.ExpressionIden (Internal.IdenConstructor name) -> + case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of + Just ctrInfo + | ctrInfo ^. Internal.constructorInfoRecord -> + Just (indName, goRecordFields (getArgtys ctrInfo) (toList args)) + where + indName = ctrInfo ^. Internal.constructorInfoInductive + _ -> Nothing + _ -> Nothing + where + (fn, args) = Internal.unfoldApplication app + + getRecordUpdate :: Internal.Application -> Maybe (Name, [Name], Internal.Expression, [(Name, Internal.Expression)]) + getRecordUpdate Internal.Application {..} = case _appLeft of + Internal.ExpressionLambda Internal.Lambda {..} -> case _lambdaClauses of + Internal.LambdaClause {..} :| [] -> case fmap (^. Internal.patternArgPattern) _lambdaPatterns of + Internal.PatternConstructorApp Internal.ConstructorApp {..} :| [] + | all isPatternArgVar _constrAppParameters -> + case _lambdaBody of + Internal.ExpressionApplication app -> case fn of + Internal.ExpressionIden (Internal.IdenConstructor name') + | name' == _constrAppConstructor -> + case HashMap.lookup name' (infoTable ^. Internal.infoConstructors) of + Just ctrInfo + | ctrInfo ^. Internal.constructorInfoRecord -> + let names = map (fromJust . getPatternArgName) _constrAppParameters + fields = goRecordFields (getArgtys ctrInfo) (toList args) + fields' = zipWithExact (\n (n', e) -> (setNameText (n' ^. namePretty) n, e)) names fields + fields'' = filter (\(n, e) -> e /= Internal.ExpressionIden (Internal.IdenVar n)) fields' + in Just (ctrInfo ^. Internal.constructorInfoInductive, map fst fields', _appRight, fields'') + _ -> Nothing + _ -> Nothing + where + (fn, args) = Internal.unfoldApplication app + _ -> Nothing + _ -> Nothing + _ -> Nothing + _ -> Nothing + getIdentApp :: Internal.Application -> Maybe (Internal.Expression, [Internal.Expression]) getIdentApp app = case mty of Just (ty, paramsNum) -> Just (fn, args') @@ -581,7 +767,6 @@ goModule onlyTypes infoTable Internal.Module {..} = goInstanceHole :: Internal.InstanceHole -> Sem r Expression goInstanceHole _ = return ExprUndefined - -- TODO: binders goLet :: Internal.Let -> Sem r Expression goLet Internal.Let {..} = do let fdefs = concatMap toFunDefs (toList _letClauses) @@ -632,10 +817,10 @@ goModule onlyTypes infoTable Internal.Module {..} = goLambda :: Internal.Lambda -> Sem r Expression goLambda Internal.Lambda {..} - | npats == 0 = goExpression (head _lambdaClauses ^. Internal.lambdaBody) + | patsNum == 0 = goExpression (head _lambdaClauses ^. Internal.lambdaBody) | otherwise = goLams vars where - npats = + patsNum = case _lambdaType of Just ty -> length @@ -647,7 +832,7 @@ goModule onlyTypes infoTable Internal.Module {..} = . filter ((/= Internal.Implicit) . (^. Internal.patternArgIsImplicit)) . toList $ head _lambdaClauses ^. Internal.lambdaPatterns - vars = map (\i -> defaultName ("x" <> show i)) [0 .. npats - 1] + vars = map (\i -> defaultName ("x" <> show i)) [0 .. patsNum - 1] goLams :: [Name] -> Sem r Expression goLams = \case @@ -668,128 +853,239 @@ goModule onlyTypes infoTable Internal.Module {..} = val <- case vars of [v] -> do - v' <- lookupName v - return $ ExprIden v' + lookupName v _ -> do vars' <- mapM lookupName vars return $ ExprTuple Tuple - { _tupleComponents = nonEmpty' $ map ExprIden vars' + { _tupleComponents = nonEmpty' vars' } - brs <- mapM goClause _lambdaClauses + brs <- goLambdaClauses (toList _lambdaClauses) return $ - ExprCase + mkExprCase Case { _caseValue = val, - _caseBranches = brs + _caseBranches = nonEmpty' brs } - goClause :: Internal.LambdaClause -> Sem r CaseBranch - goClause Internal.LambdaClause {..} = do - (pat, nset, nmap) <- case _lambdaPatterns of - p :| [] -> goPatternArg' p - _ -> do - (pats, nset, nmap) <- goPatternArgs' (toList _lambdaPatterns) - let pat = - PatTuple - Tuple - { _tupleComponents = nonEmpty' pats - } - return (pat, nset, nmap) - body <- withLocalNames nset nmap $ goExpression _lambdaBody - return $ - CaseBranch - { _caseBranchPattern = pat, - _caseBranchBody = body - } - goCase :: Internal.Case -> Sem r Expression goCase Internal.Case {..} = do val <- goExpression _caseExpression - brs <- mapM goCaseBranch _caseBranches + brs <- goCaseBranches (toList _caseBranches) return $ - ExprCase + mkExprCase Case { _caseValue = val, - _caseBranches = brs + _caseBranches = nonEmpty' brs } - goCaseBranch :: Internal.CaseBranch -> Sem r CaseBranch - goCaseBranch Internal.CaseBranch {..} = do - (pat, nset, nmap) <- goPatternArg' _caseBranchPattern - rhs <- withLocalNames nset nmap $ goCaseBranchRhs _caseBranchRhs - return $ - CaseBranch - { _caseBranchPattern = pat, - _caseBranchBody = rhs - } + goCaseBranches :: [Internal.CaseBranch] -> Sem r [CaseBranch] + goCaseBranches = \case + Internal.CaseBranch {..} : brs -> do + (npat, nset, nmap) <- goPatternArgCase _caseBranchPattern + case npat of + Nested pat [] -> do + rhs <- withLocalNames nset nmap $ goCaseBranchRhs _caseBranchRhs + brs' <- goCaseBranches brs + return $ + CaseBranch + { _caseBranchPattern = pat, + _caseBranchBody = rhs + } + : brs' + Nested pat npats -> do + let vname = defaultName (disambiguate (nset ^. nameSet) "v") + nset' = over nameSet (HashSet.insert (vname ^. namePretty)) nset + rhs <- withLocalNames nset' nmap $ goCaseBranchRhs _caseBranchRhs + remainingBranches <- withLocalNames nset' nmap $ goCaseBranches brs + let brs' = goNestedBranches (ExprIden vname) rhs remainingBranches pat (nonEmpty' npats) + return + [ CaseBranch + { _caseBranchPattern = PatVar vname, + _caseBranchBody = + mkExprCase + Case + { _caseValue = ExprIden vname, + _caseBranches = brs' + } + } + ] + [] -> return [] goCaseBranchRhs :: Internal.CaseBranchRhs -> Sem r Expression goCaseBranchRhs = \case Internal.CaseBranchRhsExpression e -> goExpression e Internal.CaseBranchRhsIf {} -> error "unsupported: side conditions" - goPatternArgs'' :: [Internal.PatternArg] -> ([Pattern], NameSet, NameMap) - goPatternArgs'' pats = - (pats', nset, nmap) + goLambdaClauses'' :: NameSet -> NameMap -> [Internal.LambdaClause] -> [CaseBranch] + goLambdaClauses'' nset nmap cls = + run $ runReader nset $ runReader nmap $ goLambdaClauses cls + + goLambdaClauses :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => [Internal.LambdaClause] -> Sem r [CaseBranch] + goLambdaClauses = \case + Internal.LambdaClause {..} : cls -> do + (npat, nset, nmap) <- case _lambdaPatterns of + p :| [] -> goPatternArgCase p + _ -> do + (npats, nset, nmap) <- goPatternArgsCase (toList _lambdaPatterns) + let npat = + fmap + ( \pats -> + PatTuple + Tuple + { _tupleComponents = nonEmpty' pats + } + ) + npats + return (npat, nset, nmap) + case npat of + Nested pat [] -> do + body <- withLocalNames nset nmap $ goExpression _lambdaBody + brs <- goLambdaClauses cls + return $ + CaseBranch + { _caseBranchPattern = pat, + _caseBranchBody = body + } + : brs + Nested pat npats -> do + let vname = defaultName (disambiguate (nset ^. nameSet) "v") + nset' = over nameSet (HashSet.insert (vname ^. namePretty)) nset + rhs <- withLocalNames nset' nmap $ goExpression _lambdaBody + remainingBranches <- withLocalNames nset' nmap $ goLambdaClauses cls + let brs' = goNestedBranches (ExprIden vname) rhs remainingBranches pat (nonEmpty' npats) + return + [ CaseBranch + { _caseBranchPattern = PatVar vname, + _caseBranchBody = + mkExprCase + Case + { _caseValue = ExprIden vname, + _caseBranches = brs' + } + } + ] + [] -> return [] + + isPatternArgVar :: Internal.PatternArg -> Bool + isPatternArgVar Internal.PatternArg {..} = + case _patternArgPattern of + Internal.PatternVariable {} -> True + _ -> False + + getPatternArgName :: Internal.PatternArg -> Maybe Name + getPatternArgName Internal.PatternArg {..} = + case _patternArgPattern of + Internal.PatternVariable name -> Just name + _ -> _patternArgName + + goPatternArgsTop :: [Internal.PatternArg] -> (Nested [Pattern], NameSet, NameMap) + goPatternArgsTop pats = + (Nested pats' npats, nset, nmap) where - (nset, (nmap, pats')) = run $ runState (NameSet mempty) $ runState (NameMap mempty) $ goPatternArgs pats + (npats, (nset, (nmap, pats'))) = run $ runOutputList $ runState (NameSet mempty) $ runState (NameMap mempty) $ goPatternArgs True pats - goPatternArg' :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => Internal.PatternArg -> Sem r (Pattern, NameSet, NameMap) - goPatternArg' pat = do + goPatternArgCase :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => Internal.PatternArg -> Sem r (Nested Pattern, NameSet, NameMap) + goPatternArgCase pat = do nset <- ask @NameSet nmap <- ask @NameMap - let (nmap', (nset', pat')) = run $ runState nmap $ runState nset $ goPatternArg pat - return (pat', nset', nmap') + let (npats, (nmap', (nset', pat'))) = run $ runOutputList $ runState nmap $ runState nset $ goPatternArg False pat + return (Nested pat' npats, nset', nmap') - goPatternArgs' :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => [Internal.PatternArg] -> Sem r ([Pattern], NameSet, NameMap) - goPatternArgs' pats = do + goPatternArgsCase :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => [Internal.PatternArg] -> Sem r (Nested [Pattern], NameSet, NameMap) + goPatternArgsCase pats = do nset <- ask @NameSet nmap <- ask @NameMap - let (nmap', (nset', pats')) = run $ runState nmap $ runState nset $ goPatternArgs pats - return (pats', nset', nmap') - - goPatternArgs :: forall r. (Members '[State NameSet, State NameMap] r) => [Internal.PatternArg] -> Sem r [Pattern] - goPatternArgs = mapM goPatternArg - - -- TODO: named patterns (`_patternArgName`) are not handled properly - goPatternArg :: forall r. (Members '[State NameSet, State NameMap] r) => Internal.PatternArg -> Sem r Pattern - goPatternArg Internal.PatternArg {..} = - goPattern _patternArgPattern + let (npats, (nmap', (nset', pats'))) = run $ runOutputList $ runState nmap $ runState nset $ goPatternArgs False pats + return (Nested pats' npats, nset', nmap') + + goPatternArgs :: forall r. (Members '[State NameSet, State NameMap, Output (Expression, Nested Pattern)] r) => Bool -> [Internal.PatternArg] -> Sem r [Pattern] + goPatternArgs isTop = mapM (goPatternArg isTop) + + goPatternArg :: forall r. (Members '[State NameSet, State NameMap, Output (Expression, Nested Pattern)] r) => Bool -> Internal.PatternArg -> Sem r Pattern + goPatternArg isTop Internal.PatternArg {..} + | Just name <- _patternArgName = do + binders <- gets (^. nameSet) + let name' = overNameText (disambiguate binders) name + modify' (over nameSet (HashSet.insert (name' ^. namePretty))) + modify' (over nameMap (HashMap.insert name (ExprIden name'))) + npat <- goNestedPattern _patternArgPattern + output (ExprIden name', npat) + return $ PatVar name' + | otherwise = + goPattern isTop _patternArgPattern + + goNestedPatternArg :: forall r. (Members '[State NameSet, State NameMap] r) => Internal.PatternArg -> Sem r (Nested Pattern) + goNestedPatternArg Internal.PatternArg {..} + | Just name <- _patternArgName = do + binders <- gets (^. nameSet) + let name' = overNameText (disambiguate binders) name + modify' (over nameSet (HashSet.insert (name' ^. namePretty))) + modify' (over nameMap (HashMap.insert name (ExprIden name'))) + npat <- goNestedPattern _patternArgPattern + return $ Nested (PatVar name') [(ExprIden name', npat)] + | otherwise = + goNestedPattern _patternArgPattern + + goNestedPattern :: forall r. (Members '[State NameSet, State NameMap] r) => Internal.Pattern -> Sem r (Nested Pattern) + goNestedPattern pat = do + (npats, pat') <- runOutputList $ goPattern False pat + return $ Nested pat' npats + + goPattern :: forall r. (Members '[State NameSet, State NameMap, Output (Expression, Nested Pattern)] r) => Bool -> Internal.Pattern -> Sem r Pattern + goPattern isTop = \case + Internal.PatternVariable name -> do + binders <- gets (^. nameSet) + let name' = overNameText (disambiguate binders) name + modify' (over nameSet (HashSet.insert (name' ^. namePretty))) + modify' (over nameMap (HashMap.insert name (ExprIden name'))) + return $ PatVar name' + Internal.PatternConstructorApp x -> goPatternConstructorApp x + Internal.PatternWildcardConstructor {} -> impossible where - goPattern :: Internal.Pattern -> Sem r Pattern - goPattern = \case - Internal.PatternVariable name -> do - binders <- gets (^. nameSet) - let name' = overNameText (disambiguate binders) name - modify' (over nameSet (HashSet.insert (name' ^. namePretty))) - modify' (over nameMap (HashMap.insert name name')) - return $ PatVar name' - Internal.PatternConstructorApp x -> goPatternConstructorApp x - Internal.PatternWildcardConstructor {} -> impossible - goPatternConstructorApp :: Internal.ConstructorApp -> Sem r Pattern goPatternConstructorApp Internal.ConstructorApp {..} | Just lst <- getListPat _constrAppConstructor _constrAppParameters = do - pats <- goPatternArgs lst + pats <- goPatternArgs False lst return $ PatList (List pats) | Just (x, y) <- getConsPat _constrAppConstructor _constrAppParameters = do - x' <- goPatternArg x - y' <- goPatternArg y + x' <- goPatternArg False x + y' <- goPatternArg False y return $ PatCons (Cons x' y') + | Just (indName, fields) <- getRecordPat _constrAppConstructor _constrAppParameters = + if + | isTop -> do + fields' <- mapM (secondM (goPatternArg False)) fields + return $ PatRecord (Record indName fields') + | otherwise -> do + binders <- gets (^. nameSet) + let adjustName :: Name -> Expression + adjustName name = + let name' = qualifyRecordProjection indName name + in ExprApp (Application (ExprIden name') (ExprIden vname)) + vname = defaultName (disambiguate binders "v") + fieldsVars = map (second (fromJust . getPatternArgName)) $ map (first adjustName) $ filter (isPatternArgVar . snd) fields + fieldsNonVars = map (first adjustName) $ filter (not . isPatternArgVar . snd) fields + modify' (over nameSet (HashSet.insert (vname ^. namePretty))) + forM fieldsVars $ \(e, fname) -> do + modify' (over nameSet (HashSet.insert (fname ^. namePretty))) + modify' (over nameMap (HashMap.insert fname e)) + fieldsNonVars' <- mapM (secondM goNestedPatternArg) fieldsNonVars + forM fieldsNonVars' output + return (PatVar vname) | Just (x, y) <- getPairPat _constrAppConstructor _constrAppParameters = do - x' <- goPatternArg x - y' <- goPatternArg y + x' <- goPatternArg False x + y' <- goPatternArg False y return $ PatTuple (Tuple (x' :| [y'])) | Just p <- getNatPat _constrAppConstructor _constrAppParameters = case p of Left zero -> return zero Right arg -> do - arg' <- goPatternArg arg + arg' <- goPatternArg False arg return (PatConstrApp (ConstrApp (goConstrName _constrAppConstructor) [arg'])) | otherwise = do - args <- mapM goPatternArg _constrAppParameters + args <- mapM (goPatternArg False) _constrAppParameters return $ PatConstrApp ConstrApp @@ -824,6 +1120,16 @@ goModule onlyTypes infoTable Internal.Module {..} = _ -> Nothing Nothing -> Nothing + getRecordPat :: Name -> [Internal.PatternArg] -> Maybe (Name, [(Name, Internal.PatternArg)]) + getRecordPat name args = + case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of + Just ctrInfo + | ctrInfo ^. Internal.constructorInfoRecord -> + Just (indName, goRecordFields (getArgtys ctrInfo) args) + where + indName = ctrInfo ^. Internal.constructorInfoInductive + _ -> Nothing + getNatPat :: Name -> [Internal.PatternArg] -> Maybe (Either Pattern Internal.PatternArg) getNatPat name args = case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of @@ -868,6 +1174,10 @@ goModule onlyTypes infoTable Internal.Module {..} = _nameIdModuleId = defaultModuleId } + qualifyRecordProjection :: Name -> Name -> Name + qualifyRecordProjection indName name = + setNameText (indName ^. namePretty <> "." <> name ^. namePretty) name + setNameText :: Text -> Name -> Name setNameText txt name = set namePretty txt @@ -881,39 +1191,39 @@ goModule onlyTypes infoTable Internal.Module {..} = $ name disambiguate :: HashSet Text -> Text -> Text - disambiguate binders = disambiguate' binders . quote - - disambiguate' :: HashSet Text -> Text -> Text - disambiguate' binders name - | name == "?" || name == "" || name == "_" = - disambiguate' binders "X" - | HashSet.member name binders - || HashSet.member name names = - disambiguate' binders (prime name) - | otherwise = - name - - names :: HashSet Text - names = - HashSet.fromList $ - map quote $ - map (^. Internal.functionInfoName . namePretty) (filter (not . (^. Internal.functionInfoIsLocal)) (HashMap.elems (infoTable ^. Internal.infoFunctions))) - ++ map (^. Internal.constructorInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoConstructors)) - ++ map (^. Internal.inductiveInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoInductives)) - ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms)) + disambiguate binders = disambiguate' . quote + where + disambiguate' :: Text -> Text + disambiguate' name + | name == "?" || name == "" || name == "_" = + disambiguate' "X" + | HashSet.member name binders + || HashSet.member name names = + disambiguate' (prime name) + | otherwise = + name + + names :: HashSet Text + names = + HashSet.fromList $ + map quote $ + map (^. Internal.functionInfoName . namePretty) (filter (not . (^. Internal.functionInfoIsLocal)) (HashMap.elems (infoTable ^. Internal.infoFunctions))) + ++ map (^. Internal.constructorInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoConstructors)) + ++ map (^. Internal.inductiveInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoInductives)) + ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms)) quote :: Text -> Text quote = quote' . Text.filter isLatin1 . Text.filter (isLetter .||. isDigit .||. (== '_') .||. (== '\'')) - - quote' :: Text -> Text - quote' txt - | HashSet.member txt reservedNames = quote' (prime txt) - | txt == "_" = "v" - | otherwise = case Text.uncons txt of - Just (c, _) | not (isLetter c) -> quote' ("v_" <> txt) - _ -> case Text.unsnoc txt of - Just (_, c) | not (isAlphaNum c || c == '\'') -> quote' (txt <> "'") - _ -> txt + where + quote' :: Text -> Text + quote' txt + | HashSet.member txt reservedNames = quote' (prime txt) + | txt == "_" = "v" + | otherwise = case Text.uncons txt of + Just (c, _) | not (isLetter c) -> quote' ("v_" <> txt) + _ -> case Text.unsnoc txt of + Just (_, c) | not (isAlphaNum c || c == '\'') -> quote' (txt <> "'") + _ -> txt reservedNames :: HashSet Text reservedNames = diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index 5b04c73950..85c72ca5be 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -265,5 +265,6 @@ mkConstructorEntries d = (_constructorInfoBuiltin, c) <- zipExact builtins (d ^. inductiveConstructors), let _constructorInfoType = c ^. inductiveConstructorType, let _constructorInfoName = c ^. inductiveConstructorName, - let _constructorInfoTrait = d ^. inductiveTrait + let _constructorInfoTrait = d ^. inductiveTrait, + let _constructorInfoRecord = c ^. inductiveConstructorIsRecord ] diff --git a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs index 6554e412cb..b55ea477cc 100644 --- a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs @@ -10,7 +10,8 @@ data ConstructorInfo = ConstructorInfo _constructorInfoInductive :: InductiveName, _constructorInfoName :: ConstructorName, _constructorInfoBuiltin :: Maybe BuiltinConstructor, - _constructorInfoTrait :: Bool + _constructorInfoTrait :: Bool, + _constructorInfoRecord :: Bool } deriving stock (Generic) diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index 2e865deda5..1cf4a9b5f5 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -98,11 +98,48 @@ type Either' A B := -- Records {-# isabelle-ignore: true #-} +type R' := mkR' { + r1' : Nat; + r2' : Nat; +}; + type R := mkR { r1 : Nat; r2 : Nat; }; +r : R := mkR 0 1; +v : Nat := 0; + +funR (r : R) : R := + case r of + | mkR@{r1; r2} := r@R{r1 := r1 + r2}; + +funRR : R -> R + | r@mkR@{r1; r2} := r@R{r1 := r1 + r2}; + +funR' : R -> R + | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr1 + rr2; r2 := rr2}; + +funR1 : R -> R + | mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2} + | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1}; + +funR2 (r : R) : R := + case r of + | mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2} + | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1}; + +funR3 (er : Either' R R) : R := + case er of + | Left' mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2} + | Left' mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1} + | Right' mkR@{r1; r2 := zero} := mkR@{r1 := 7; r2 := r1} + | Right' r@(mkR@{r1; r2}) := r@R{r1 := r2 + 2; r2 := r1 + 3}; + +funR4 : R -> R + | r@mkR@{r1} := r@R{r2 := r1}; + -- Standard library bf (b1 b2 : Bool) : Bool := not (b1 && b2); diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index 3c846b64c4..96ef8e48b6 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -58,10 +58,10 @@ datatype 'A Queue = queue "'A list" "'A list" fun qfst :: "'A Queue \ 'A list" where - "qfst (queue x v) = x" + "qfst (queue x v') = x" fun qsnd :: "'A Queue \ 'A list" where - "qsnd (queue v v') = v'" + "qsnd (queue v' v'0) = v'0" fun pop_front :: "'A Queue \ 'A Queue" where "pop_front q = @@ -69,7 +69,7 @@ fun pop_front :: "'A Queue \ 'A Queue" where q' = queue (tl (qfst q)) (qsnd q) in case qfst q' of [] \ queue (rev (qsnd q')) [] | - v \ q')" + v' \ q')" fun push_back :: "'A Queue \ 'A \ 'A Queue" where "push_back q x = @@ -86,8 +86,8 @@ fun is_empty :: "'A Queue \ bool" where [] \ (case qsnd q of [] \ True | - v \ False) | - v \ False)" + v' \ False) | + v' \ False)" definition empty :: "'A Queue" where "empty = queue [] []" @@ -97,8 +97,7 @@ fun funkcja :: "nat \ nat" where (let nat1 = 1; nat2 = 2; - plusOne = \ x0 . case x0 of - n' \ n' + 1 + plusOne = \ x0 . x0 + 1 in plusOne n + nat1 + nat2)" text \ @@ -110,6 +109,115 @@ datatype ('A, 'B) Either' (* Right constructor *) Right' 'B +record R = + r1 :: nat + r2 :: nat + +fun r1 :: "R \ nat" where + "r1 (| R.r1 = r1'0, R.r2 = r2'0 |) = r1'0" + +fun r2 :: "R \ nat" where + "r2 (| R.r1 = r1'0, R.r2 = r2'0 |) = r2'0" + +definition r :: R where + "r = (| R.r1 = 0, R.r2 = 1 |)" + +definition v :: nat where + "v = 0" + +fun funR :: "R \ R" where + "funR r' = (r' (| R.r1 := R.r1 r' + R.r2 r' |))" + +fun funRR :: "R \ R" where + "funRR r'0 = (r'0 (| R.r1 := R.r1 r'0 + R.r2 r'0 |))" + +fun funR' :: "R \ R" where + "funR' (| R.r1 = rr1, R.r2 = rr2 |) = + (let + r1'0 = rr1 + rr2; + r2'0 = rr2 + in (| R.r1 = r1'0, R.r2 = r2'0 |))" + +fun funR1 :: "R \ R" where + "funR1 (| R.r1 = 0, R.r2 = r2'0 |) = + (let + r1'0 = r2'0; + r2'1 = r2'0 + in (| R.r1 = r1'0, R.r2 = r2'1 |))" | + "funR1 (| R.r1 = rr1, R.r2 = rr2 |) = + (let + r1'0 = rr2; + r2'0 = rr1 + in (| R.r1 = r1'0, R.r2 = r2'0 |))" + +fun funR2 :: "R \ R" where + "funR2 r' = + (case (R.r1 r') of + (0) \ + let + r1'0 = R.r2 r'; + r2'0 = R.r2 r' + in (| R.r1 = r1'0, R.r2 = r2'0 |) | + _ \ + let + r1'0 = R.r2 r'; + r2'0 = R.r1 r' + in (| R.r1 = r1'0, R.r2 = r2'0 |))" + +fun funR3 :: "(R, R) Either' \ R" where + "funR3 er = + (case er of + (Left' v') \ + (case (R.r1 v') of + (0) \ + let + r1'0 = R.r2 v'; + r2'0 = R.r2 v' + in (| R.r1 = r1'0, R.r2 = r2'0 |) | + _ \ + (case er of + (Left' v'1) \ + let + r1'0 = R.r2 v'1; + r2'0 = R.r1 v'1 + in (| R.r1 = r1'0, R.r2 = r2'0 |) | + v'2 \ + (case v'2 of + (Right' v'1) \ + (case (R.r2 v'1) of + (0) \ + let + r1'0 = 7; + r2'0 = 7 + in (| R.r1 = r1'0, R.r2 = r2'0 |) | + _ \ + (case v'2 of + (Right' r') \ + r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))) | + v'4 \ + (case v'4 of + (Right' r') \ + r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))) | + v'2 \ + (case v'2 of + (Right' v'1) \ + (case (R.r2 v'1) of + (0) \ + let + r1'0 = 7; + r2'0 = 7 + in (| R.r1 = r1'0, R.r2 = r2'0 |) | + _ \ + (case v'2 of + (Right' r') \ + r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))) | + v'4 \ + (case v'4 of + (Right' r') \ r' (| R.r1 := R.r2 r' + 2, R.r2 := R.r1 r' + 3 |))))" + +fun funR4 :: "R \ R" where + "funR4 r'0 = (r'0 (| R.r2 := R.r1 r'0 |))" + fun bf :: "bool \ bool \ bool" where "bf b1 b2 = (\ (b1 \ b2))"