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 <janmasrovira@gmail.com>

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")

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

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))
 

src/Juvix/Compiler/Backend/Isabelle/Language.hs

@@ -48,8 +48,8 @@ makeLenses ''IndApp
 
 data Expression
   = ExprIden Name
-  | ExprUndefined
+  | ExprUndefined Interval
-  | ExprLiteral Literal
+  | 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
+data List a = List
-  { _listElements :: [a]
+  { _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

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 :: (PrettyCode c) => [Comment] -> c -> AnsiText
-ppOutDefault = mkAnsiText . PPOutput . doc defaultOptions
+ppOutDefault comments =
-
+  mkAnsiText
-ppOut :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> AnsiText
+    . PPOutput
-ppOut o = mkAnsiText . PPOutput . doc (project o)
+    . 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 :: (PrettyCode c) => [Comment] -> c -> Text
-ppPrint = show . ppOutDefault
+ppPrint comments = show . ppOutDefault comments

src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs

@@ -10,20 +10,24 @@ arrow :: Doc Ann
 arrow = "\\<Rightarrow>"
 
 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 :: (PrettyCode c) => Options -> [Comment] -> c -> Doc Ann
-doc opts = run . runReader opts . ppCode
+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
+    ExprUndefined {} -> return kwUndefined
-    ExprLiteral x -> ppCode x
+    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 $ "\\<lambda>" <+> name <+?> ty <+> dot <+> body
 
 instance PrettyCode Statement where
-  ppCode = \case
+  ppCode stmt = do
-    StmtDefinition x -> ppCode x
+    comments <- ppComments (getLoc stmt)
-    StmtFunction x -> ppCode x
+    stmt' <- case stmt of
-    StmtSynonym x -> ppCode x
+      StmtDefinition x -> ppCode x
-    StmtDatatype x -> ppCode x
+      StmtFunction x -> ppCode x
-    StmtRecord 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
+    res <- mapM ppCodeWithComments _functionClauses
-    let cls' = punctuate (space <> kwPipe) $ map (dquotes . (n <+>)) (toList cls)
+    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 ->

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 :: Bool -> [Comment] -> Internal.InfoTable -> Internal.Module -> Sem r Result
-    go onlyTypes tab md =
+    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 :: Interval -> [Name] -> Internal.Expression -> Maybe Internal.Expression -> NonEmpty Clause
-    goBody argnames ty = \case
+    goBody defLoc argnames ty = \case
-      Nothing -> oneClause ExprUndefined
+      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 :: Interval -> Expression -> Expression -> [CaseBranch] -> Pattern -> NonEmpty (Expression, Nested Pattern) -> NonEmpty CaseBranch
-    goNestedBranches caseVal rhs remainingBranches pat npats =
+    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 :: Interval -> Expression -> [CaseBranch] -> Maybe CaseBranch
-    mkDefaultBranch val remainingBranches = case remainingBranches of
+    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 :: Interval -> PragmaIsabelleOperator -> Internal.Expression -> Internal.Expression -> Sem r Expression
-        mkIsabelleOperator PragmaIsabelleOperator {..} arg1 arg2 = do
+        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 "\\<and>", andFixity, arg1, arg2)
+                        Just (defaultName (getLoc name) "\\<and>", andFixity, arg1, arg2)
                   Just Internal.BuiltinBoolOr
                     | (arg1 :| [arg2]) <- args ->
-                        Just (defaultName "\\<or>", orFixity, arg1, arg2)
+                        Just (defaultName (getLoc name) "\\<or>", 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 :: Interval -> Text -> Name
-    defaultName n =
+    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,

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)
 

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)

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)

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
 

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

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

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

tests/positive/Isabelle/isabelle/Program.thy

@@ -11,8 +11,10 @@ definition id1 :: "nat list \<Rightarrow> nat list" where
 definition id2 :: "'A \<Rightarrow> 'A" where
   "id2 = id"
 
+(* Add one to each element in a list *)
 fun add_one :: "nat list \<Rightarrow> nat list" where
   "add_one [] = []" |
+  (* hello! *)
   "add_one (x # xs) = ((x + 1) # add_one xs)"
 
 fun sum :: "nat list \<Rightarrow> nat" where
@@ -28,11 +30,18 @@ fun g :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
 fun inc :: "nat \<Rightarrow> nat" where
   "inc x = (Suc x)"
 
+(* dec function *)
 fun dec :: "nat \<Rightarrow> nat" where
   "dec 0 = 0" |
   "dec (Suc x) = x"
 
+(* dec' function *)
 fun dec' :: "nat \<Rightarrow> nat" where
+  (* Do case switch *)
+  (* pattern match on x *)
+  (* the zero case  *)
+  (* return zero  *)
+  (* the suc case  *)
   "dec' x =
     (case x of
        0 \<Rightarrow> 0 |
@@ -51,6 +60,7 @@ fun bool_fun :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
 fun bool_fun' :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool" where
   "bool_fun' x y z = (x \<and> y \<or> z)"
 
+(* Queues *)
 text \<open>
 A type of Queues
 \<close>
@@ -92,6 +102,7 @@ fun is_empty :: "'A Queue \<Rightarrow> bool" where
 definition empty :: "'A Queue" where
   "empty = queue [] []"
 
+(* Multiple let expressions *)
 fun funkcja :: "nat \<Rightarrow> 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' \<Rightarrow> R" where
 fun funR4 :: "R \<Rightarrow> R" where
   "funR4 r'0 = (r'0 (| R.r2 := R.r1 r'0 |))"
 
+(* Standard library *)
 fun bf :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
   "bf b1 b2 = (\<not> (b1 \<and> b2))"