Add more comments in the source code

src/Juvix/Compiler/Core/Data/IdentDependencyInfo.hs

@@ -38,7 +38,8 @@ createSymbolDependencyInfo tab = createDependencyInfo graph startVertices
     graph =
       fmap
         ( \IdentifierInfo {..} ->
-            getSymbols' tab (lookupTabIdentifierNode tab _identifierSymbol)
+            getSymbols' tab _identifierType
+              <> getSymbols' tab (lookupTabIdentifierNode tab _identifierSymbol)
         )
         (tab ^. infoIdentifiers)
         <> foldr

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -536,7 +536,7 @@ instance PrettyCode InfoTable where
 
       ppInductives :: [InductiveInfo] -> Sem r (Doc Ann)
       ppInductives inds = do
-        inds' <- mapM ppInductive (filter (isNothing . (^. inductiveBuiltin)) inds)
+        inds' <- mapM ppInductive (filter (shouldPrintInductive . (^. inductiveBuiltin)) inds)
         return (vsep inds')
         where
           ppInductive :: InductiveInfo -> Sem r (Doc Ann)
@@ -545,6 +545,20 @@ instance PrettyCode InfoTable where
             ctrs <- mapM (fmap (<> semi) . ppCode . lookupTabConstructorInfo tbl) (ii ^. inductiveConstructors)
             return (kwInductive <+> name <+> braces (line <> indent' (vsep ctrs) <> line) <> kwSemicolon)
 
+          shouldPrintInductive :: Maybe BuiltinType -> Bool
+          shouldPrintInductive = \case
+            Just (BuiltinTypeInductive i) -> case i of
+              BuiltinList -> True
+              BuiltinMaybe -> False
+              BuiltinPair -> True
+              BuiltinPoseidonState -> True
+              BuiltinEcPoint -> True
+              BuiltinNat -> False
+              BuiltinInt -> False
+              BuiltinBool -> False
+            Just _ -> False
+            Nothing -> True
+
 instance PrettyCode AxiomInfo where
   ppCode ii = do
     name <- ppName KNameAxiom (ii ^. axiomName)

src/Juvix/Compiler/Core/Transformation/MoveApps.hs

@@ -52,5 +52,29 @@ convertNode = dmap go
               _ -> node
       _ -> node
 
+-- | Move applications inside let bindings and case branches.
+--
+-- The translation from Core to Core.Stripped requires that only variables or
+-- function symbols be present at the head of an application.
+--
+-- We transform
+--
+-- `(let x := M in N) Q`
+--
+-- to
+--
+-- `let x := M in N Q`
+--
+-- and e.g.
+--
+-- `(case M of { c1 x := N1; c2 x y := N2 }) Q`
+--
+-- to
+--
+-- `case M of { c1 x := N1 Q; c2 x y := N2 Q }`
+--
+-- References:
+--  - https://github.com/anoma/juvix/issues/1654
+--  - https://github.com/anoma/juvix/pull/1659
 moveApps :: Module -> Module
 moveApps = mapT (const convertNode)

src/Juvix/Compiler/Core/Transformation/Optimize/CaseCallLifting.hs

@@ -131,5 +131,51 @@ convertNode md = umap go
                   _ -> node
           _ -> node
 
+-- | Lifts calls in case branches out of the case expression, for functions that
+-- are called exactly once in each branch.
+--
+-- Transforms, e.g.,
+--
+-- case M
+-- | C1 x y := R1 (f A1 A2)
+-- | C2 z := R2 (f B1 B2)
+--
+-- to
+--
+-- let m := M;
+--      r := f (case m | C1 x y := A1 | C2 z := B1) (case m | C1 x y := A2 | C2 z := B2);
+-- in
+-- case m
+-- | C1 x y := R1 r
+-- | C2 z := R2 r
+--
+-- This allows to compile more Juvix programs to VampIR by automatically
+-- translating a large class of non-linearly-recursive programs into
+-- linearly-recursive ones.
+--
+-- For example,
+--
+-- def power' : Int → Int → Int → Int :=
+--   λ(acc : Int) λ(a : Int) λ(b : Int)
+--     if = b 0 then
+--       acc
+--     else if = (% b 2) 0 then
+--       power' acc (* a a) (/ b 2)
+--     else
+--       power' (* acc a) (* a a) (/ b 2);
+--
+-- is transformed into
+--
+-- def power' : Int → Int → Int → Int :=
+--   λ(acc : Int) λ(a : Int) λ(b : Int)
+--     if = b 0 then
+--       acc
+--     else
+--       let _X : Bool := = (% b 2) 0
+--       in power' (if _X then acc else * acc a) (* a a) (/ b 2);
+--
+-- References:
+--  - https://github.com/anoma/juvix/issues/2200
+--  - https://github.com/anoma/juvix/pull/2218
 caseCallLifting :: Module -> Module
 caseCallLifting md = mapAllNodes (convertNode md) md

src/Juvix/Compiler/Core/Transformation/Optimize/CaseFolding.hs

@@ -28,5 +28,17 @@ convertNode = dmap go
       _ ->
         impossible
 
+-- | Fold constant cases, i.e., convert
+--
+-- case C a b
+-- | A := ..
+-- | B x := ..
+-- | C x y := M
+--
+-- to
+--
+-- let x := a;
+--     y := b;
+-- in M
 caseFolding :: Module -> Module
 caseFolding = mapAllNodes convertNode

src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs

@@ -71,6 +71,15 @@ constantFolding' opts nonRecSyms tab md =
     )
     md
 
+-- | Evaluates closed applications with value arguments when the result type is
+-- zero-order. For example, `3 + 4` is evaluated to `7`, and `id 3` is evaluated
+-- to `3`, but `id id` is not evaluated because the target type is not
+-- zero-order (it's a function type). This optimization is only applied to
+-- non-recursive symbols.
+--
+-- References:
+--  - https://github.com/anoma/juvix/pull/2450
+--  - https://github.com/anoma/juvix/issues/2154
 constantFolding :: (Member (Reader CoreOptions) r) => Module -> Sem r Module
 constantFolding md = do
   opts <- ask

src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs

@@ -155,6 +155,24 @@ convertInductive md ii =
 convertAxiom :: Module -> AxiomInfo -> AxiomInfo
 convertAxiom md = over axiomType (convertNode md)
 
+-- | Remove type arguments and type abstractions.
+--
+-- Also adjusts the types, removing quantification over types and replacing all
+-- type variables with the dynamic type.
+--
+-- For example,
+--
+-- `\\A : Type \\f : ((B : Type) -> A -> B -> Pair A B) \\x : A { f A x x }`
+--
+-- is transformed to
+--
+-- `\\f : (Any -> Any -> Pair Any Any) \\x : Any { f x x }`
+--
+-- References:
+--  - https://github.com/anoma/juvix/issues/1512
+--  - https://github.com/anoma/juvix/pull/1655
+--  - https://github.com/anoma/juvix/issues/1930
+--  - https://github.com/anoma/juvix/pull/1954
 removeTypeArgs :: Module -> Module
 removeTypeArgs md =
   filterOutTypeSynonyms $