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 <[email protected]>
anoma · Sep 2, 2024 · b9d8641 · b9d8641
1 parent 9d2a2b5
commit b9d8641
Show file tree

Hide file tree

Showing 15 changed files with 284 additions and 111 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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,11 +324,96 @@ instance HasAtomicity Expression where
 instance HasAtomicity Pattern where
   atomicity = \case
     PatVar {} -> Atom
-    PatZero -> Atom
+    PatZero {} -> Atom
     PatConstrApp ConstrApp {..}
       | null _constrAppArgs -> Atom
       | otherwise -> Aggregate appFixity
     PatTuple {} -> Atom
     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
@@ -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