translate comments to Isabelle

anoma · Aug 14, 2024 · e4a254b · e4a254b
1 parent 0c6d8a6
commit e4a254b
Show file tree

Hide file tree

Showing 6 changed files with 36 additions and 20 deletions.
diff --git a/src/Juvix/Compiler/Backend/Isabelle/Language.hs b/src/Juvix/Compiler/Backend/Isabelle/Language.hs
@@ -154,13 +154,15 @@ data Statement
 data Definition = Definition
   { _definitionName :: Name,
     _definitionType :: Type,
-    _definitionBody :: Expression
+    _definitionBody :: Expression,
+    _definitionComment :: Maybe Text
   }
 
 data Function = Function
   { _functionName :: Name,
     _functionType :: Type,
-    _functionClauses :: NonEmpty Clause
+    _functionClauses :: NonEmpty Clause,
+    _functionComment :: Maybe Text
   }
 
 data Clause = Clause
@@ -176,23 +178,27 @@ data Synonym = Synonym
 data Datatype = Datatype
   { _datatypeName :: Name,
     _datatypeParams :: [TypeVar],
-    _datatypeConstructors :: [Constructor]
+    _datatypeConstructors :: [Constructor],
+    _datatypeComment :: Maybe Text
   }
 
 data Constructor = Constructor
   { _constructorName :: Name,
-    _constructorArgTypes :: [Type]
+    _constructorArgTypes :: [Type],
+    _constructorComment :: Maybe Text
   }
 
 data Record = Record
   { _recordName :: Name,
     _recordParams :: [TypeVar],
-    _recordFields :: [RecordField]
+    _recordFields :: [RecordField],
+    _recordComment :: Maybe Text
   }
 
 data RecordField = RecordField
   { _recordFieldName :: Name,
-    _recordFieldType :: Type
+    _recordFieldType :: Type,
+    _recordFieldComment :: Maybe Text
   }
 
 makeLenses ''Definition

diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -92,14 +92,16 @@ goModule onlyTypes infoTable Internal.Module {..} =
                 Record
                   { _recordName = _inductiveName,
                     _recordParams = params,
-                    _recordFields = map goRecordField tyargs
+                    _recordFields = map goRecordField tyargs,
+                    _recordComment = _inductiveComment
                   }
       | otherwise =
           StmtDatatype
             Datatype
               { _datatypeName = _inductiveName,
                 _datatypeParams = params,
-                _datatypeConstructors = map goConstructorDef _inductiveConstructors
+                _datatypeConstructors = map goConstructorDef _inductiveConstructors,
+                _datatypeComment = _inductiveComment
               }
       where
         params = map goInductiveParameter _inductiveParameters
@@ -111,20 +113,22 @@ goModule onlyTypes infoTable Internal.Module {..} =
     goRecordField Internal.FunctionParameter {..} =
       RecordField
         { _recordFieldName = fromMaybe (defaultName "_") _paramName,
-          _recordFieldType = goType _paramType
+          _recordFieldType = goType _paramType,
+          _recordFieldComment = Nothing
         }
 
     goConstructorDef :: Internal.ConstructorDef -> Constructor
     goConstructorDef Internal.ConstructorDef {..} =
       Constructor
         { _constructorName = _inductiveConstructorName,
-          _constructorArgTypes = tyargs
+          _constructorArgTypes = tyargs,
+          _constructorComment = _inductiveConstructorComment
         }
       where
         tyargs = map (goType . (^. Internal.paramType)) (fst $ Internal.unfoldFunType _inductiveConstructorType)
 
-    goDef :: Name -> Internal.Expression -> [Internal.ArgInfo] -> Maybe Internal.Expression -> Statement
-    goDef name ty argsInfo body = case ty of
+    goDef :: Name -> Internal.Expression -> [Internal.ArgInfo] -> Maybe Internal.Expression -> Maybe Text -> Statement
+    goDef name ty argsInfo body comment = case ty of
       Internal.ExpressionUniverse {} ->
         StmtSynonym
           Synonym
@@ -137,14 +141,16 @@ goModule onlyTypes infoTable Internal.Module {..} =
               Function
                 { _functionName = name',
                   _functionType = goType ty,
-                  _functionClauses = goBody argnames ty body
+                  _functionClauses = goBody argnames ty body,
+                  _functionComment = comment
                 }
         | otherwise ->
             StmtDefinition
               Definition
                 { _definitionName = name',
                   _definitionType = goType ty,
-                  _definitionBody = maybe ExprUndefined goExpression' body
+                  _definitionBody = maybe ExprUndefined goExpression' body,
+                  _definitionComment = comment
                 }
       where
         argnames =
@@ -191,10 +197,10 @@ goModule onlyTypes infoTable Internal.Module {..} =
             (pats, nset', nmap') = goPatternArgs'' (filterTypeArgs 0 ty (toList _lambdaPatterns))
 
     goFunctionDef :: Internal.FunctionDef -> Statement
-    goFunctionDef Internal.FunctionDef {..} = goDef _funDefName _funDefType _funDefArgsInfo (Just _funDefBody)
+    goFunctionDef Internal.FunctionDef {..} = goDef _funDefName _funDefType _funDefArgsInfo (Just _funDefBody) _funDefComment
 
     goAxiomDef :: Internal.AxiomDef -> Statement
-    goAxiomDef Internal.AxiomDef {..} = goDef _axiomName _axiomType [] Nothing
+    goAxiomDef Internal.AxiomDef {..} = goDef _axiomName _axiomType [] Nothing _axiomComment
 
     goType :: Internal.Expression -> Type
     goType ty = case ty of

diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs
@@ -288,7 +288,8 @@ instance HasExpressions ConstructorDef where
         { _inductiveConstructorType = ty',
           _inductiveConstructorName,
           _inductiveConstructorIsRecord,
-          _inductiveConstructorPragmas
+          _inductiveConstructorPragmas,
+          _inductiveConstructorComment
         }
 
 typeAbstraction :: IsImplicit -> Name -> FunctionParameter

diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs
@@ -413,7 +413,8 @@ data ConstructorDef = ConstructorDef
   { _inductiveConstructorName :: ConstrName,
     _inductiveConstructorType :: Expression,
     _inductiveConstructorIsRecord :: Bool,
-    _inductiveConstructorPragmas :: Pragmas
+    _inductiveConstructorPragmas :: Pragmas,
+    _inductiveConstructorComment :: Maybe Text
   }
   deriving stock (Data)
 

diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -647,7 +647,8 @@ goConstructorDef retTy ConstructorDef {..} = do
       { _inductiveConstructorType = ty',
         _inductiveConstructorName = goSymbol _constructorName,
         _inductiveConstructorIsRecord = isRhsRecord _constructorRhs,
-        _inductiveConstructorPragmas = pragmas'
+        _inductiveConstructorPragmas = pragmas',
+        _inductiveConstructorComment = fmap ppPrint _constructorDoc
       }
   where
     goAdtType :: Concrete.RhsAdt 'Scoped -> Sem r Internal.Expression

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
@@ -230,7 +230,8 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do
               { _inductiveConstructorType = cty',
                 _inductiveConstructorName,
                 _inductiveConstructorIsRecord,
-                _inductiveConstructorPragmas
+                _inductiveConstructorPragmas,
+                _inductiveConstructorComment
               }
       registerConstructor c'
       return c'