From b9d864123a1831ad198e305539bfcd83651987a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Mon, 2 Sep 2024 15:56:58 +0200 Subject: [PATCH] Isabelle/HOL translation: comments (#2974) * Closes #2962 * Depends on #2963 * In Isabelle/HOL comments cannot appear in internal syntax. All comments inside a Juvix definition are moved outside: to before the definition or before the earliest function clause. --------- Co-authored-by: Jan Mas Rovira --- app/Commands/Isabelle.hs | 5 +- .../Compiler/Backend/Isabelle/Data/Result.hs | 3 +- src/Juvix/Compiler/Backend/Isabelle/Extra.hs | 12 +- .../Compiler/Backend/Isabelle/Language.hs | 100 ++++++++++++++-- src/Juvix/Compiler/Backend/Isabelle/Pretty.hs | 20 ++-- .../Compiler/Backend/Isabelle/Pretty/Base.hs | 72 ++++++++---- .../Backend/Isabelle/Translation/FromTyped.hs | 111 +++++++++--------- src/Juvix/Compiler/Internal/Language.hs | 28 +++-- .../Translation/FromConcrete/Data/Context.hs | 3 + .../Analysis/TypeChecking/Data/Context.hs | 3 + src/Juvix/Data/Loc.hs | 5 +- src/Juvix/Prelude/Effects/Input.hs | 9 ++ test/Isabelle/Positive.hs | 3 +- tests/positive/Isabelle/Program.juvix | 8 +- tests/positive/Isabelle/isabelle/Program.thy | 13 ++ 15 files changed, 284 insertions(+), 111 deletions(-) diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs index c2731fc2a..410855d7c 100644 --- a/app/Commands/Isabelle.hs +++ b/app/Commands/Isabelle.hs @@ -14,10 +14,11 @@ runCommand opts = do let inputFile = opts ^. isabelleInputFile res <- runPipeline opts inputFile upToIsabelle let thy = res ^. resultTheory + comments = res ^. resultComments outputDir <- fromAppPathDir (opts ^. isabelleOutputDir) if | opts ^. isabelleStdout -> do - renderStdOut (ppOutDefault thy) + renderStdOut (ppOutDefault comments thy) putStrLn "" | otherwise -> do ensureDir outputDir @@ -29,4 +30,4 @@ runCommand opts = do ) absPath :: Path Abs File absPath = outputDir file - writeFileEnsureLn absPath (ppPrint thy <> "\n") + writeFileEnsureLn absPath (ppPrint comments thy <> "\n") diff --git a/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs b/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs index 3c13082b6..9818ff31b 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Data/Result.hs @@ -4,7 +4,8 @@ import Juvix.Compiler.Backend.Isabelle.Language data Result = Result { _resultTheory :: Theory, - _resultModuleId :: ModuleId + _resultModuleId :: ModuleId, + _resultComments :: [Comment] } makeLenses ''Result diff --git a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs b/src/Juvix/Compiler/Backend/Isabelle/Extra.hs index 6b398aee4..2d306bdb0 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Extra.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Extra.hs @@ -12,13 +12,13 @@ mkApp fn = \case subsumesPattern :: Pattern -> Pattern -> Bool subsumesPattern pat1 pat2 = case (pat1, pat2) of (PatVar _, _) -> True - (PatZero, PatZero) -> 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)) -> + (PatList (List _ p1), PatList (List _ p2)) -> length p1 == length p2 && all (uncurry subsumesPattern) (zipExact p1 p2) (PatCons (Cons c1 p1), PatCons (Cons c2 p2)) -> @@ -40,7 +40,7 @@ substVar var var' = go go :: Expression -> Expression go = \case ExprIden x -> goIden x - ExprUndefined -> ExprUndefined + ExprUndefined x -> ExprUndefined x ExprLiteral x -> ExprLiteral x ExprApp x -> goApplication x ExprBinop x -> goBinop x @@ -78,7 +78,7 @@ substVar var var' = go goTuple (Tuple xs) = ExprTuple (Tuple (fmap go xs)) goList :: List Expression -> Expression - goList (List xs) = ExprList (List (map go xs)) + goList (List loc xs) = ExprList (List loc (map go xs)) goCons :: Cons Expression -> Expression goCons (Cons h t) = ExprCons (Cons (go h) (go t)) @@ -111,10 +111,10 @@ substVar var var' = go goPattern :: Pattern -> Pattern goPattern = \case PatVar x -> PatVar (goName x) - PatZero -> PatZero + PatZero x -> PatZero x 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)) + PatList (List loc p) -> PatList (List loc (fmap goPattern p)) PatCons (Cons h t) -> PatCons (Cons (goPattern h) (goPattern t)) PatRecord (Record n r) -> PatRecord (Record n (map (second goPattern) r)) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs index 00fc381e4..7ce496be1 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Language.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Language.hs @@ -48,8 +48,8 @@ makeLenses ''IndApp data Expression = ExprIden Name - | ExprUndefined - | ExprLiteral Literal + | ExprUndefined Interval + | ExprLiteral (WithLoc Literal) | ExprApp Application | ExprBinop Binop | ExprTuple (Tuple Expression) @@ -117,7 +117,7 @@ data Lambda = Lambda data Pattern = PatVar Name - | PatZero + | PatZero Interval | PatConstrApp ConstrApp | PatTuple (Tuple Pattern) | PatList (List Pattern) @@ -128,8 +128,9 @@ newtype Tuple a = Tuple { _tupleComponents :: NonEmpty a } -newtype List a = List - { _listElements :: [a] +data List a = List + { _listLoc :: Interval, + _listElements :: [a] } data Cons a = Cons @@ -306,7 +307,7 @@ instance HasAtomicity Type where instance HasAtomicity Expression where atomicity = \case ExprIden {} -> Atom - ExprUndefined -> Atom + ExprUndefined {} -> Atom ExprLiteral {} -> Atom ExprApp {} -> Aggregate appFixity ExprBinop Binop {..} -> Aggregate _binopFixity @@ -323,7 +324,7 @@ instance HasAtomicity Expression where instance HasAtomicity Pattern where atomicity = \case PatVar {} -> Atom - PatZero -> Atom + PatZero {} -> Atom PatConstrApp ConstrApp {..} | null _constrAppArgs -> Atom | otherwise -> Aggregate appFixity @@ -331,3 +332,88 @@ instance HasAtomicity Pattern where PatList {} -> Atom PatCons {} -> Aggregate consFixity PatRecord {} -> Atom + +instance HasLoc Expression where + getLoc = \case + ExprIden n -> getLoc n + ExprUndefined x -> x + ExprLiteral x -> x ^. withLocInt + ExprApp x -> getLoc x + ExprBinop x -> getLoc x + ExprTuple x -> getLoc x + ExprList x -> getLoc x + ExprCons x -> getLoc x + ExprRecord x -> getLoc x + ExprRecordUpdate x -> getLoc x + ExprLet x -> getLoc x + ExprIf x -> getLoc x + ExprCase x -> getLoc x + ExprLambda x -> getLoc x + +instance HasLoc Application where + getLoc Application {..} = getLoc _appLeft <> getLoc _appRight + +instance HasLoc Binop where + getLoc Binop {..} = getLoc _binopLeft <> getLoc _binopRight + +instance (HasLoc a) => HasLoc (Tuple a) where + getLoc = getLocSpan . (^. tupleComponents) + +instance HasLoc (List a) where + getLoc = (^. listLoc) + +instance (HasLoc a) => HasLoc (Cons a) where + getLoc Cons {..} = getLoc _consHead <> getLoc _consTail + +instance HasLoc (Record a) where + getLoc Record {..} = + getLoc _recordName + <>? maybe Nothing (Just . getLocSpan) (nonEmpty (map fst _recordFields)) + +instance HasLoc RecordUpdate where + getLoc RecordUpdate {..} = getLoc _recordUpdateRecord <> getLoc _recordUpdateFields + +instance HasLoc RecordField where + getLoc RecordField {..} = getLoc _recordFieldName + +instance HasLoc Let where + getLoc Let {..} = getLocSpan _letClauses <> getLoc _letBody + +instance HasLoc LetClause where + getLoc LetClause {..} = getLoc _letClauseName <> getLoc _letClauseValue + +instance HasLoc If where + getLoc If {..} = getLoc _ifValue <> getLoc _ifBranchTrue <> getLoc _ifBranchFalse + +instance HasLoc Case where + getLoc Case {..} = getLoc _caseValue <> getLocSpan _caseBranches + +instance HasLoc Lambda where + getLoc Lambda {..} = getLoc _lambdaVar <> getLoc _lambdaBody + +instance HasLoc CaseBranch where + getLoc CaseBranch {..} = getLoc _caseBranchPattern <> getLoc _caseBranchBody + +instance HasLoc Pattern where + getLoc = \case + PatVar n -> getLoc n + PatZero x -> x + PatConstrApp x -> getLoc x + PatTuple x -> getLoc x + PatList x -> getLoc x + PatCons x -> getLoc x + PatRecord x -> getLoc x + +instance HasLoc ConstrApp where + getLoc ConstrApp {..} = getLoc _constrAppConstructor + +instance HasLoc Statement where + getLoc = \case + StmtDefinition Definition {..} -> getLoc _definitionName + StmtFunction Function {..} -> getLoc _functionName + StmtSynonym Synonym {..} -> getLoc _synonymName + StmtDatatype Datatype {..} -> getLoc _datatypeName + StmtRecord RecordDef {..} -> getLoc _recordDefName + +instance HasLoc Clause where + getLoc Clause {..} = getLocSpan _clausePatterns <> getLoc _clauseBody diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty.hs index b9989c184..203f90bc3 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Pretty.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty.hs @@ -6,17 +6,21 @@ import Juvix.Data.PPOutput import Juvix.Prelude import Prettyprinter.Render.Terminal qualified as Ansi -ppOutDefault :: (PrettyCode c) => c -> AnsiText -ppOutDefault = mkAnsiText . PPOutput . doc defaultOptions - -ppOut :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> AnsiText -ppOut o = mkAnsiText . PPOutput . doc (project o) +ppOutDefault :: (PrettyCode c) => [Comment] -> c -> AnsiText +ppOutDefault comments = + mkAnsiText + . PPOutput + . doc defaultOptions comments ppTrace' :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> Text -ppTrace' opts = Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLayoutOptions . doc (project opts) +ppTrace' opts = + Ansi.renderStrict + . reAnnotateS stylize + . layoutPretty defaultLayoutOptions + . doc (project opts) [] ppTrace :: (PrettyCode c) => c -> Text ppTrace = ppTrace' traceOptions -ppPrint :: (PrettyCode c) => c -> Text -ppPrint = show . ppOutDefault +ppPrint :: (PrettyCode c) => [Comment] -> c -> Text +ppPrint comments = show . ppOutDefault comments diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs index 22a1c016c..1d1a45c67 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs @@ -10,20 +10,24 @@ arrow :: Doc Ann arrow = "\\" class PrettyCode c where - ppCode :: (Member (Reader Options) r) => c -> Sem r (Doc Ann) + ppCode :: (Members '[Reader Options, Input Comment] r) => c -> Sem r (Doc Ann) -doc :: (PrettyCode c) => Options -> c -> Doc Ann -doc opts = run . runReader opts . ppCode +doc :: (PrettyCode c) => Options -> [Comment] -> c -> Doc Ann +doc opts comments = + run + . runReader opts + . runInputList comments + . ppCode -ppCodeQuoted :: (HasAtomicity c, PrettyCode c, Member (Reader Options) r) => c -> Sem r (Doc Ann) +ppCodeQuoted :: (HasAtomicity c, PrettyCode c, Members '[Reader Options, Input Comment] r) => c -> Sem r (Doc Ann) ppCodeQuoted c | atomicity c == Atom = ppCode c | otherwise = dquotes <$> ppCode c -ppTopCode :: (HasAtomicity c, PrettyCode c, Member (Reader Options) r) => c -> Sem r (Doc Ann) +ppTopCode :: (HasAtomicity c, PrettyCode c, Members '[Reader Options, Input Comment] r) => c -> Sem r (Doc Ann) ppTopCode c = parensIf (not (isAtomic c)) <$> ppCode c -ppParams :: (HasAtomicity c, PrettyCode c, Member (Reader Options) r) => [c] -> Sem r (Maybe (Doc Ann)) +ppParams :: (HasAtomicity c, PrettyCode c, Members '[Reader Options, Input Comment] r) => [c] -> Sem r (Maybe (Doc Ann)) ppParams = \case [] -> return Nothing [x] -> Just <$> ppRightExpression appFixity x @@ -31,6 +35,22 @@ ppParams = \case ps <- mapM ppCode params return $ Just $ parens (hsep (punctuate comma ps)) +ppComments :: (Member (Input Comment) r) => Interval -> Sem r (Doc Ann) +ppComments loc = do + comments <- inputWhile cmpLoc + return + . mconcatMap (\c -> annotate AnnComment $ "(*" <> pretty (c ^. commentText) <+> "*)" <> line) + $ comments + where + cmpLoc :: Comment -> Bool + cmpLoc c = c ^. commentInterval . intervalStart <= loc ^. intervalEnd + +ppCodeWithComments :: (PrettyCode a, HasLoc a, Members '[Reader Options, Input Comment] r) => a -> Sem r (Doc Ann, Doc Ann) +ppCodeWithComments a = do + comments <- ppComments (getLoc a) + res <- ppCode a + return (comments, res) + prettyTextComment :: Maybe Text -> Doc Ann prettyTextComment = \case Nothing -> "" @@ -95,8 +115,8 @@ instance PrettyCode IndApp where instance PrettyCode Expression where ppCode = \case ExprIden x -> ppCode x - ExprUndefined -> return kwUndefined - ExprLiteral x -> ppCode x + ExprUndefined {} -> return kwUndefined + ExprLiteral x -> ppCode (x ^. withLocParam) ExprApp x -> ppCode x ExprBinop x -> ppCode x ExprTuple x -> ppCode x @@ -175,7 +195,7 @@ instance (PrettyCode a) => PrettyCode (List a) where elems <- mapM ppCode _listElements return $ brackets $ hsep (punctuate comma elems) -ppRecord :: (PrettyCode a, Member (Reader Options) r) => Bool -> Record a -> Sem r (Doc Ann) +ppRecord :: (PrettyCode a, Members '[Reader Options, Input Comment] r) => Bool -> Record a -> Sem r (Doc Ann) ppRecord bUpdate Record {..} = do recName <- ppCode _recordName names <- mapM (ppCode . fst) _recordFields @@ -194,7 +214,7 @@ instance (PrettyCode a, HasAtomicity a) => PrettyCode (Cons a) where instance PrettyCode Pattern where ppCode = \case PatVar x -> ppCode x - PatZero -> return $ annotate AnnLiteralInteger (pretty (0 :: Int)) + PatZero {} -> return $ annotate AnnLiteralInteger (pretty (0 :: Int)) PatConstrApp x -> ppCode x PatTuple x -> ppCode x PatList x -> ppCode x @@ -220,12 +240,15 @@ instance PrettyCode Lambda where return $ "\\" <+> name <+?> ty <+> dot <+> body instance PrettyCode Statement where - ppCode = \case - StmtDefinition x -> ppCode x - StmtFunction x -> ppCode x - StmtSynonym x -> ppCode x - StmtDatatype x -> ppCode x - StmtRecord x -> ppCode x + ppCode stmt = do + comments <- ppComments (getLoc stmt) + stmt' <- case stmt of + StmtDefinition x -> ppCode x + StmtFunction x -> ppCode x + StmtSynonym x -> ppCode x + StmtDatatype x -> ppCode x + StmtRecord x -> ppCode x + return $ comments <> stmt' instance PrettyCode Definition where ppCode Definition {..} = do @@ -240,8 +263,9 @@ instance PrettyCode Function where let comment = prettyTextComment _functionDocComment n <- ppCode _functionName ty <- ppCodeQuoted _functionType - cls <- mapM ppCode _functionClauses - let cls' = punctuate (space <> kwPipe) $ map (dquotes . (n <+>)) (toList cls) + res <- mapM ppCodeWithComments _functionClauses + let cls = punctuate (space <> kwPipe) $ map (dquotes . (n <+>) . snd) (toList res) + cls' = zipWithExact (<>) (toList (fmap fst res)) cls return $ comment <> kwFun <+> n <+> "::" <+> ty <+> kwWhere <> line <> indent' (vsep cls') instance PrettyCode Clause where @@ -267,10 +291,11 @@ instance PrettyCode Datatype where instance PrettyCode Constructor where ppCode Constructor {..} = do + comments <- ppComments (getLoc _constructorName) let comment = prettyComment _constructorDocComment n <- ppCode _constructorName tys <- mapM ppCodeQuoted _constructorArgTypes - return $ comment <> hsep (n : tys) + return $ comments <> comment <> hsep (n : tys) instance PrettyCode RecordDef where ppCode RecordDef {..} = do @@ -282,10 +307,11 @@ instance PrettyCode RecordDef where instance PrettyCode RecordField where ppCode RecordField {..} = do + comments <- ppComments (getLoc _recordFieldName) let comment = prettyComment _recordFieldDocComment n <- ppCode _recordFieldName ty <- ppCodeQuoted _recordFieldType - return $ comment <> n <+> "::" <+> ty + return $ comments <> comment <> n <+> "::" <+> ty ppImports :: [Name] -> Sem r [Doc Ann] ppImports ns = @@ -312,21 +338,21 @@ instance PrettyCode Theory where <> kwEnd ppRightExpression :: - (PrettyCode a, HasAtomicity a, Member (Reader Options) r) => + (PrettyCode a, HasAtomicity a, Members '[Reader Options, Input Comment] r) => Fixity -> a -> Sem r (Doc Ann) ppRightExpression = ppLRExpression isRightAssoc ppLeftExpression :: - (PrettyCode a, HasAtomicity a, Member (Reader Options) r) => + (PrettyCode a, HasAtomicity a, Members '[Reader Options, Input Comment] r) => Fixity -> a -> Sem r (Doc Ann) ppLeftExpression = ppLRExpression isLeftAssoc ppLRExpression :: - (HasAtomicity a, PrettyCode a, Member (Reader Options) r) => + (HasAtomicity a, PrettyCode a, Members '[Reader Options, Input Comment] r) => (Fixity -> Bool) -> Fixity -> a -> diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index 0ffc72b22..87e48fb9c 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -15,7 +15,6 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Da import Juvix.Compiler.Pipeline.EntryPoint import Juvix.Compiler.Store.Extra import Juvix.Compiler.Store.Language -import Juvix.Extra.Paths qualified as P newtype NameSet = NameSet { _nameSet :: HashSet Text @@ -43,7 +42,7 @@ fromInternal :: (Members '[Error JuvixError, Reader EntryPoint, Reader ModuleTable, NameIdGen] r) => Internal.InternalTypedResult -> Sem r Result -fromInternal Internal.InternalTypedResult {..} = do +fromInternal res@Internal.InternalTypedResult {..} = do onlyTypes <- (^. entryPointIsabelleOnlyTypes) <$> ask itab <- getInternalModuleTable <$> ask let md :: Internal.InternalModule @@ -52,15 +51,20 @@ fromInternal Internal.InternalTypedResult {..} = do itab' = Internal.insertInternalModule itab md table :: Internal.InfoTable table = Internal.computeCombinedInfoTable itab' - go onlyTypes table _resultModule + comments :: [Comment] + comments = allComments (Internal.getInternalTypedResultComments res) + go onlyTypes comments table _resultModule where - go :: Bool -> Internal.InfoTable -> Internal.Module -> Sem r Result - go onlyTypes tab md = + go :: Bool -> [Comment] -> Internal.InfoTable -> Internal.Module -> Sem r Result + go onlyTypes comments tab md = return $ Result { _resultTheory = goModule onlyTypes tab md, - _resultModuleId = md ^. Internal.moduleId + _resultModuleId = md ^. Internal.moduleId, + _resultComments = filter (\c -> c ^. commentInterval . intervalFile == file) comments } + where + file = getLoc md ^. intervalFile goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory goModule onlyTypes infoTable Internal.Module {..} = @@ -146,9 +150,9 @@ goModule onlyTypes infoTable Internal.Module {..} = goInductiveParameter Internal.InductiveParameter {..} = TypeVar _inductiveParamName goRecordField :: Internal.FunctionParameter -> RecordField - goRecordField Internal.FunctionParameter {..} = + goRecordField param@Internal.FunctionParameter {..} = RecordField - { _recordFieldName = fromMaybe (defaultName "_") _paramName, + { _recordFieldName = fromMaybe (defaultName (getLoc param) "_") _paramName, _recordFieldType = goType _paramType, _recordFieldDocComment = Nothing } @@ -178,7 +182,7 @@ goModule onlyTypes infoTable Internal.Module {..} = Function { _functionName = name', _functionType = goType ty, - _functionClauses = goBody argnames ty body, + _functionClauses = goBody loc argnames ty body, _functionDocComment = comment } | otherwise -> @@ -186,13 +190,14 @@ goModule onlyTypes infoTable Internal.Module {..} = Definition { _definitionName = name', _definitionType = goType ty, - _definitionBody = maybe ExprUndefined goExpression' body, + _definitionBody = maybe (ExprUndefined loc) goExpression' body, _definitionDocComment = comment } where argnames = - map (overNameText quote) $ filterTypeArgs 0 ty $ map (fromMaybe (defaultName "_") . (^. Internal.argInfoName)) argsInfo + map (overNameText quote) $ filterTypeArgs 0 ty $ map (fromMaybe (defaultName (getLoc name) "_") . (^. Internal.argInfoName)) argsInfo name' = overNameText quote name + loc = getLoc name isFunction :: [Name] -> Internal.Expression -> Maybe Internal.Expression -> Bool isFunction argnames ty = \case @@ -201,9 +206,9 @@ goModule onlyTypes infoTable Internal.Module {..} = True _ -> not (null argnames) - goBody :: [Name] -> Internal.Expression -> Maybe Internal.Expression -> NonEmpty Clause - goBody argnames ty = \case - Nothing -> oneClause ExprUndefined + goBody :: Interval -> [Name] -> Internal.Expression -> Maybe Internal.Expression -> NonEmpty Clause + goBody defLoc argnames ty = \case + Nothing -> oneClause (ExprUndefined defLoc) -- 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 -> @@ -226,7 +231,7 @@ goModule onlyTypes infoTable Internal.Module {..} = goClauses :: [Internal.LambdaClause] -> [Clause] goClauses = \case - Internal.LambdaClause {..} : cls -> + cl@Internal.LambdaClause {..} : cls -> case npats0 of Nested pats [] -> Clause @@ -242,6 +247,7 @@ goModule onlyTypes infoTable Internal.Module {..} = ( \(idx :: Int, mname) -> maybe ( defaultName + (getLoc cl) ( disambiguate (nset' ^. nameSet) ("v_" <> show idx) @@ -255,7 +261,7 @@ goModule onlyTypes infoTable Internal.Module {..} = remainingBranches = goLambdaClauses'' nset'' nmap' cls valTuple = ExprTuple (Tuple (fmap ExprIden vnames)) patTuple = PatTuple (Tuple (nonEmpty' pats)) - brs = goNestedBranches valTuple rhs remainingBranches patTuple (nonEmpty' npats) + brs = goNestedBranches (getLoc cl) valTuple rhs remainingBranches patTuple (nonEmpty' npats) in [ Clause { _clausePatterns = fmap PatVar vnames, _clauseBody = @@ -270,12 +276,12 @@ goModule onlyTypes infoTable Internal.Module {..} = (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 = + goNestedBranches :: Interval -> Expression -> Expression -> [CaseBranch] -> Pattern -> NonEmpty (Expression, Nested Pattern) -> NonEmpty CaseBranch + goNestedBranches loc 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') + brs = goNestedBranches' rhs (mkDefaultBranch loc caseVal remainingBranches) (Nested pat' npats') remainingBranches' = filter (not . subsumesPattern pat . (^. caseBranchPattern)) remainingBranches in CaseBranch { _caseBranchPattern = pat, @@ -288,13 +294,13 @@ goModule onlyTypes infoTable Internal.Module {..} = } :| remainingBranches' - mkDefaultBranch :: Expression -> [CaseBranch] -> Maybe CaseBranch - mkDefaultBranch val remainingBranches = case remainingBranches of + mkDefaultBranch :: Interval -> Expression -> [CaseBranch] -> Maybe CaseBranch + mkDefaultBranch loc val remainingBranches = case remainingBranches of [] -> Nothing _ -> Just $ CaseBranch - { _caseBranchPattern = PatVar (defaultName "_"), + { _caseBranchPattern = PatVar (defaultName loc "_"), _caseBranchBody = mkExprCase Case @@ -447,7 +453,7 @@ goModule onlyTypes infoTable Internal.Module {..} = 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' + (ty : argtys', arg' : args') -> (fromMaybe (defaultName (getLoc ty) "_") (ty ^. Internal.paramName), arg') : goRecordFields argtys' args' _ -> [] goExpression' :: Internal.Expression -> Expression @@ -479,7 +485,7 @@ goModule onlyTypes infoTable Internal.Module {..} = case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of Just ctrInfo -> case ctrInfo ^. Internal.constructorInfoBuiltin of - Just Internal.BuiltinNatZero -> return $ ExprLiteral (LitNumeric 0) + Just Internal.BuiltinNatZero -> return $ ExprLiteral (WithLoc (getLoc name) (LitNumeric 0)) _ -> return $ ExprIden (goConstrName name) Nothing -> return $ ExprIden (goConstrName name) Internal.IdenVar name -> do @@ -490,12 +496,12 @@ goModule onlyTypes infoTable Internal.Module {..} = goApplication :: Internal.Application -> Sem r Expression goApplication app@Internal.Application {..} | Just (pragmas, arg1, arg2) <- getIsabelleOperator app = - mkIsabelleOperator pragmas arg1 arg2 + mkIsabelleOperator (getLoc app) pragmas arg1 arg2 | Just x <- getLiteral app = - return $ ExprLiteral $ LitNumeric x + return $ ExprLiteral $ WithLoc (getLoc app) (LitNumeric x) | Just xs <- getList app = do xs' <- mapM goExpression xs - return $ ExprList (List xs') + return $ ExprList (List (getLoc app) xs') | Just (arg1, arg2) <- getCons app = do arg1' <- goExpression arg1 arg2' <- goExpression arg2 @@ -542,14 +548,14 @@ goModule onlyTypes infoTable Internal.Module {..} = r <- goExpression _appRight return $ ExprApp (Application l r) - mkIsabelleOperator :: PragmaIsabelleOperator -> Internal.Expression -> Internal.Expression -> Sem r Expression - mkIsabelleOperator PragmaIsabelleOperator {..} arg1 arg2 = do + mkIsabelleOperator :: Interval -> PragmaIsabelleOperator -> Internal.Expression -> Internal.Expression -> Sem r Expression + mkIsabelleOperator loc PragmaIsabelleOperator {..} arg1 arg2 = do arg1' <- goExpression arg1 arg2' <- goExpression arg2 return $ ExprBinop Binop - { _binopOperator = defaultName _pragmaIsabelleOperatorName, + { _binopOperator = defaultName loc _pragmaIsabelleOperatorName, _binopLeft = arg1', _binopRight = arg2', _binopFixity = @@ -662,10 +668,10 @@ goModule onlyTypes infoTable Internal.Module {..} = case funInfo ^. Internal.functionInfoBuiltin of Just Internal.BuiltinBoolAnd | (arg1 :| [arg2]) <- args -> - Just (defaultName "\\", andFixity, arg1, arg2) + Just (defaultName (getLoc name) "\\", andFixity, arg1, arg2) Just Internal.BuiltinBoolOr | (arg1 :| [arg2]) <- args -> - Just (defaultName "\\", orFixity, arg1, arg2) + Just (defaultName (getLoc name) "\\", orFixity, arg1, arg2) _ -> Nothing Nothing -> Nothing _ -> Nothing @@ -752,20 +758,20 @@ goModule onlyTypes infoTable Internal.Module {..} = _ -> Nothing goFunType :: Internal.Function -> Sem r Expression - goFunType _ = return ExprUndefined + goFunType f = return (ExprUndefined (getLoc f)) goLiteral :: Internal.LiteralLoc -> Sem r Expression - goLiteral lit = return $ ExprLiteral $ case lit ^. withLocParam of + goLiteral lit = return $ ExprLiteral $ WithLoc (lit ^. withLocInt) $ case lit ^. withLocParam of Internal.LitString s -> LitString s Internal.LitNumeric n -> LitNumeric n Internal.LitInteger n -> LitNumeric n Internal.LitNatural n -> LitNumeric n goHole :: Internal.Hole -> Sem r Expression - goHole _ = return ExprUndefined + goHole h = return (ExprUndefined (getLoc h)) goInstanceHole :: Internal.InstanceHole -> Sem r Expression - goInstanceHole _ = return ExprUndefined + goInstanceHole h = return (ExprUndefined (getLoc h)) goLet :: Internal.Let -> Sem r Expression goLet Internal.Let {..} = do @@ -797,7 +803,7 @@ goModule onlyTypes infoTable Internal.Module {..} = } goUniverse :: Internal.SmallUniverse -> Sem r Expression - goUniverse _ = return ExprUndefined + goUniverse u = return (ExprUndefined (getLoc u)) goSimpleLambda :: Internal.SimpleLambda -> Sem r Expression goSimpleLambda Internal.SimpleLambda {..} = do @@ -816,7 +822,7 @@ goModule onlyTypes infoTable Internal.Module {..} = } goLambda :: Internal.Lambda -> Sem r Expression - goLambda Internal.Lambda {..} + goLambda lam@Internal.Lambda {..} | patsNum == 0 = goExpression (head _lambdaClauses ^. Internal.lambdaBody) | otherwise = goLams vars where @@ -832,7 +838,7 @@ goModule onlyTypes infoTable Internal.Module {..} = . filter ((/= Internal.Implicit) . (^. Internal.patternArgIsImplicit)) . toList $ head _lambdaClauses ^. Internal.lambdaPatterns - vars = map (\i -> defaultName ("x" <> show i)) [0 .. patsNum - 1] + vars = map (\i -> defaultName (getLoc lam) ("x" <> show i)) [0 .. patsNum - 1] goLams :: [Name] -> Sem r Expression goLams = \case @@ -882,7 +888,7 @@ goModule onlyTypes infoTable Internal.Module {..} = goCaseBranches :: [Internal.CaseBranch] -> Sem r [CaseBranch] goCaseBranches = \case - Internal.CaseBranch {..} : brs -> do + br@Internal.CaseBranch {..} : brs -> do (npat, nset, nmap) <- goPatternArgCase _caseBranchPattern case npat of Nested pat [] -> do @@ -895,11 +901,11 @@ goModule onlyTypes infoTable Internal.Module {..} = } : brs' Nested pat npats -> do - let vname = defaultName (disambiguate (nset ^. nameSet) "v") + let vname = defaultName (getLoc br) (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) + let brs' = goNestedBranches (getLoc vname) (ExprIden vname) rhs remainingBranches pat (nonEmpty' npats) return [ CaseBranch { _caseBranchPattern = PatVar vname, @@ -924,7 +930,7 @@ goModule onlyTypes infoTable Internal.Module {..} = goLambdaClauses :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => [Internal.LambdaClause] -> Sem r [CaseBranch] goLambdaClauses = \case - Internal.LambdaClause {..} : cls -> do + cl@Internal.LambdaClause {..} : cls -> do (npat, nset, nmap) <- case _lambdaPatterns of p :| [] -> goPatternArgCase p _ -> do @@ -950,11 +956,11 @@ goModule onlyTypes infoTable Internal.Module {..} = } : brs Nested pat npats -> do - let vname = defaultName (disambiguate (nset ^. nameSet) "v") + let vname = defaultName (getLoc cl) (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) + let brs' = goNestedBranches (getLoc vname) (ExprIden vname) rhs remainingBranches pat (nonEmpty' npats) return [ CaseBranch { _caseBranchPattern = PatVar vname, @@ -1045,10 +1051,10 @@ goModule onlyTypes infoTable Internal.Module {..} = Internal.PatternWildcardConstructor {} -> impossible where goPatternConstructorApp :: Internal.ConstructorApp -> Sem r Pattern - goPatternConstructorApp Internal.ConstructorApp {..} + goPatternConstructorApp app@Internal.ConstructorApp {..} | Just lst <- getListPat _constrAppConstructor _constrAppParameters = do pats <- goPatternArgs False lst - return $ PatList (List pats) + return $ PatList (List (getLoc app) pats) | Just (x, y) <- getConsPat _constrAppConstructor _constrAppParameters = do x' <- goPatternArg False x y' <- goPatternArg False y @@ -1064,7 +1070,7 @@ goModule onlyTypes infoTable Internal.Module {..} = adjustName name = let name' = qualifyRecordProjection indName name in ExprApp (Application (ExprIden name') (ExprIden vname)) - vname = defaultName (disambiguate binders "v") + vname = defaultName (getLoc app) (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))) @@ -1137,7 +1143,7 @@ goModule onlyTypes infoTable Internal.Module {..} = case funInfo ^. Internal.constructorInfoBuiltin of Just Internal.BuiltinNatZero | null args -> - Just $ Left PatZero + Just $ Left $ PatZero (getLoc name) Just Internal.BuiltinNatSuc | [arg] <- args -> Just $ Right arg @@ -1155,19 +1161,18 @@ goModule onlyTypes infoTable Internal.Module {..} = _ -> Nothing Nothing -> Nothing - defaultName :: Text -> Name - defaultName n = + defaultName :: Interval -> Text -> Name + defaultName loc n = Name { _nameText = n, _nameId = defaultId, _nameKind = KNameLocal, _nameKindPretty = KNameLocal, _namePretty = n, - _nameLoc = defaultLoc, + _nameLoc = loc, _nameFixity = Nothing } where - defaultLoc = singletonInterval $ mkInitialLoc P.noFile defaultId = NameId { _nameIdUid = 0, diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index ae0f83c2c..662c69151 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/src/Juvix/Compiler/Internal/Language.hs @@ -515,14 +515,6 @@ makeLenses ''ConstructorDef makeLenses ''ConstructorApp makeLenses ''NormalizedExpression -instance HasLoc InductiveDef where - getLoc d = - getLoc (d ^. inductiveName) - <>? (getLoc . (^. last1) <$> (nonEmpty (d ^. inductiveConstructors))) - -instance HasLoc NormalizedExpression where - getLoc = getLoc . (^. normalizedExpressionOriginal) - instance Eq ModuleIndex where (==) = (==) `on` (^. moduleIxModule . moduleName) @@ -589,6 +581,26 @@ instance HasAtomicity Pattern where PatternVariable {} -> Atom PatternWildcardConstructor {} -> Atom +instance HasLoc Module where + getLoc m = getLoc (m ^. moduleName) <>? maybe Nothing (Just . getLocSpan) (nonEmpty (m ^. moduleBody . moduleStatements)) + +instance HasLoc MutualBlock where + getLoc = getLocSpan . (^. mutualStatements) + +instance HasLoc MutualStatement where + getLoc = \case + StatementInductive i -> getLoc i + StatementFunction f -> getLoc f + StatementAxiom a -> getLoc a + +instance HasLoc InductiveDef where + getLoc d = + getLoc (d ^. inductiveName) + <>? (getLoc . (^. last1) <$> (nonEmpty (d ^. inductiveConstructors))) + +instance HasLoc NormalizedExpression where + getLoc = getLoc . (^. normalizedExpressionOriginal) + instance HasLoc AxiomDef where getLoc a = getLoc (a ^. axiomName) <> getLoc (a ^. axiomType) diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete/Data/Context.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete/Data/Context.hs index b21e3088e..b18654bfb 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete/Data/Context.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete/Data/Context.hs @@ -15,3 +15,6 @@ data InternalResult = InternalResult } makeLenses ''InternalResult + +getInternalResultComments :: InternalResult -> Comments +getInternalResultComments = Concrete.getScoperResultComments . (^. resultScoper) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs index ddd581b23..51a491592 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs @@ -36,3 +36,6 @@ data ImportContext = ImportContext makeLenses ''InternalTypedResult makeLenses ''ImportContext + +getInternalTypedResultComments :: InternalTypedResult -> Comments +getInternalTypedResultComments = Internal.getInternalResultComments . (^. resultInternal) diff --git a/src/Juvix/Data/Loc.hs b/src/Juvix/Data/Loc.hs index 812e44723..547fcb586 100644 --- a/src/Juvix/Data/Loc.hs +++ b/src/Juvix/Data/Loc.hs @@ -76,7 +76,7 @@ data Interval = Interval _intervalStart :: FileLoc, _intervalEnd :: FileLoc } - deriving stock (Show, Ord, Eq, Generic, Data, Lift) + deriving stock (Show, Eq, Generic, Data, Lift) instance Hashable Interval @@ -84,6 +84,9 @@ instance Serialize Interval instance NFData Interval +instance Ord Interval where + compare (Interval f s e) (Interval f' s' e') = compare (f, s, e) (f', s', e') + class HasLoc t where getLoc :: t -> Interval diff --git a/src/Juvix/Prelude/Effects/Input.hs b/src/Juvix/Prelude/Effects/Input.hs index 1fc78da6e..8cc4edf4a 100644 --- a/src/Juvix/Prelude/Effects/Input.hs +++ b/src/Juvix/Prelude/Effects/Input.hs @@ -2,6 +2,7 @@ module Juvix.Prelude.Effects.Input ( Input, input, inputJust, + inputWhile, peekInput, runInputList, ) @@ -26,6 +27,14 @@ input = Input [] -> (Nothing, Input []) Input (i : is) -> (Just i, Input is) +inputWhile :: (Member (Input i) r) => (i -> Bool) -> Sem r [i] +inputWhile c = + stateStaticRep $ + \case + Input l -> + let (sat, rest) = span c l + in (sat, Input rest) + peekInput :: (Member (Input i) r) => Sem r (Maybe i) peekInput = do Input l <- getStaticRep diff --git a/test/Isabelle/Positive.hs b/test/Isabelle/Positive.hs index b7d84652c..e3755db29 100644 --- a/test/Isabelle/Positive.hs +++ b/test/Isabelle/Positive.hs @@ -33,9 +33,10 @@ testDescr PosTest {..} = step "Translate" PipelineResult {..} <- snd <$> testRunIO entryPoint upToIsabelle let thy = _pipelineResult ^. resultTheory + comments = _pipelineResult ^. resultComments step "Checking against expected output file" expFile :: Text <- readFile _expectedFile - assertEqDiffText "Compare to expected output" (ppPrint thy <> "\n") expFile + assertEqDiffText "Compare to expected output" (ppPrint comments thy <> "\n") expFile } allTests :: TestTree diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index 1cf4a9b5f..7e7db6324 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -8,8 +8,10 @@ id1 : List Nat -> List Nat := id; id2 {A : Type} : A -> A := id; +-- Add one to each element in a list add_one : List Nat -> List Nat | [] := [] + -- hello! | (x :: xs) := (x + 1) :: add_one xs; sum : List Nat -> Nat @@ -26,12 +28,16 @@ g (x y : Nat) : Bool := inc (x : Nat) : Nat := suc x; +-- dec function dec : Nat -> Nat | zero := zero | (suc x) := x; +-- dec' function dec' (x : Nat) : Nat := - case x of zero := zero | suc y := y; + -- Do case switch + -- pattern match on x + case x of {- the zero case -} zero := {- return zero -} zero | {- the suc case -} suc y := y; optmap {A} (f : A -> A) : Maybe A -> Maybe A | nothing := nothing diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index 96ef8e48b..2d7324f43 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -11,8 +11,10 @@ definition id1 :: "nat list \ nat list" where definition id2 :: "'A \ 'A" where "id2 = id" +(* Add one to each element in a list *) fun add_one :: "nat list \ nat list" where "add_one [] = []" | + (* hello! *) "add_one (x # xs) = ((x + 1) # add_one xs)" fun sum :: "nat list \ nat" where @@ -28,11 +30,18 @@ fun g :: "nat \ nat \ bool" where fun inc :: "nat \ nat" where "inc x = (Suc x)" +(* dec function *) fun dec :: "nat \ nat" where "dec 0 = 0" | "dec (Suc x) = x" +(* dec' function *) fun dec' :: "nat \ nat" where + (* Do case switch *) + (* pattern match on x *) + (* the zero case *) + (* return zero *) + (* the suc case *) "dec' x = (case x of 0 \ 0 | @@ -51,6 +60,7 @@ fun bool_fun :: "bool \ bool \ bool \ bool" fun bool_fun' :: "bool \ bool \ bool \ bool" where "bool_fun' x y z = (x \ y \ z)" +(* Queues *) text \ A type of Queues \ @@ -92,6 +102,7 @@ fun is_empty :: "'A Queue \ bool" where definition empty :: "'A Queue" where "empty = queue [] []" +(* Multiple let expressions *) fun funkcja :: "nat \ nat" where "funkcja n = (let @@ -109,6 +120,7 @@ datatype ('A, 'B) Either' (* Right constructor *) Right' 'B +(* Records *) record R = r1 :: nat r2 :: nat @@ -218,6 +230,7 @@ fun funR3 :: "(R, R) Either' \ R" where fun funR4 :: "R \ R" where "funR4 r'0 = (r'0 (| R.r2 := R.r1 r'0 |))" +(* Standard library *) fun bf :: "bool \ bool \ bool" where "bf b1 b2 = (\ (b1 \ b2))"