Add syntax highlighting for juvix code blocks in docs

.gitignore

@@ -88,3 +88,4 @@ examples/milestone/HelloWorld/HelloWorld
 hie.yaml
 /.shake/
 /.benchmark-results/
+docs/assets/**

Makefile

@@ -74,6 +74,7 @@ demo-example:
 .PHONY: docs
 docs:
 	@cp $(METAFILES) docs/
+	@cp -r assets/ docs/
 	@mdbook build
 
 .PHONY: serve-docs

app/AsmInterpreter.hs

@@ -17,7 +17,7 @@ runAsm bValidate tab =
         Nothing ->
           case tab ^. Asm.infoMainFunction of
             Just sym -> do
-              r <- doRun tab (Asm.getFunInfo tab sym)
+              r <- doRun tab (Asm.lookupFunInfo tab sym)
               case r of
                 Left err ->
                   exitJuvixError (JuvixError err)

app/Commands/Repl.hs

@@ -6,7 +6,6 @@ import Commands.Base hiding (command)
 import Commands.Repl.Options
 import Control.Exception (throwIO)
 import Control.Monad.State.Strict qualified as State
-import Data.HashMap.Strict qualified as HashMap
 import Data.String.Interpolate (i, __i)
 import Evaluator
 import Juvix.Compiler.Concrete.Data.Scope (scopePath)
@@ -376,7 +375,6 @@ runTransformations shouldDisambiguate ts n = runCoreInfoTableBuilderArtifacts $
                 _identifierSymbol = sym,
                 _identifierLocation = Nothing,
                 _identifierArgsNum = 0,
-                _identifierArgsInfo = [],
                 _identifierType = Core.mkDynamic',
                 _identifierIsExported = False,
                 _identifierBuiltin = Nothing
@@ -395,4 +393,4 @@ runTransformations shouldDisambiguate ts n = runCoreInfoTableBuilderArtifacts $
       Core.setInfoTable tab''
 
     getNode :: Core.Symbol -> Sem (Core.InfoTableBuilder ': r) Core.Node
-    getNode sym = HashMap.lookupDefault impossible sym . (^. Core.identContext) <$> Core.getInfoTable
+    getNode sym = fromMaybe impossible . flip Core.lookupIdentifierNode' sym <$> Core.getInfoTable

book.toml

@@ -28,8 +28,8 @@ macros = "theme/latex-macros.txt"
 default-theme = "light"
 preferred-dark-theme = "Ayu"
 copy-fonts = true
-additional-css = ["theme/pagetoc.css"]
-additional-js = ["theme/pagetoc.js","assets/images/tara-magicien.png", "assets/images/tara-seating.svg", "assets/images/tara-smiling.png", "assets/images/tara-smiling.svg", "assets/images/tara-teaching.png", "assets/images/tara-teaching.svg", "assets/js/highlight.js", "assets/js/tex-chtml.js" ]
+additional-css = ["theme/pagetoc.css", "theme/juvix.css"]
+additional-js = ["theme/pagetoc.js", "theme/juvix.js", "theme/pascal.js"]
 no-section-label = false
 git-repository-url = "https://github.com/anoma/juvix"
 git-repository-icon = "fa-github"

docs/reference/language/axioms.md

@@ -5,11 +5,12 @@ example, let us imagine one wants to write a program that assumes _A_ is
 a type, and there exists a term _x_ that inhabits _A_. Then the program
 would look like the following.
 
-    -- Example.juvix
+```juvix
     module Example;
      axiom A : Type;
      axiom x : A;
     end;
+```
 
 Terms introduced by the `axiom` keyword lack any computational content.
 Programs containing axioms not marked as builtins cannot be compiled to

docs/reference/language/comments.md

@@ -5,15 +5,14 @@ Juvix has no support for nested comments.
 
 - Inline Comment
 
-<!-- -->
-
+```juvix
     -- This is a comment!
+```
 
 - Region comment
 
-<!-- -->
-
+```juvix
     {-
         This is a comment!
-
     -}
+```

docs/reference/language/modules.md

@@ -60,6 +60,7 @@ module B;
     open A;
     x : Nat;
     x := zero;
+end;
 ```
 
 However, opening modules may create name collisions if you already have

docs/tutorials/learn.md

@@ -27,7 +27,7 @@ juvix repl
 
 The response should be similar to:
 
-```juvix
+```jrepl
 Juvix REPL version 0.3: https://juvix.org. Run :help for help
 OK loaded: ./.juvix-build/stdlib/Stdlib/Prelude.juvix
 Stdlib.Prelude>
@@ -41,7 +41,7 @@ commands type `:help`.
 
 You can try evaluating simple arithmetic expressions in the REPL:
 
-```juvix
+```jrepl
 Stdlib.Prelude> 3 + 4
 7
 Stdlib.Prelude> 1 + 3 * 7
@@ -62,7 +62,7 @@ natural number from a smaller one yields `0`.
 
 You can also try boolean expressions
 
-```juvix
+```jrepl
 Stdlib.Prelude> true
 true
 Stdlib.Prelude> not true
@@ -77,7 +77,7 @@ Stdlib.Prelude> if true 1 0
 
 and strings, pairs and lists:
 
-```juvix
+```jrepl
 Stdlib.Prelude> "Hello world!"
 "Hello world!"
 Stdlib.Prelude> (1, 2)
@@ -91,7 +91,7 @@ In fact, you can use all functions and types from the
 module of the [standard library](https://anoma.github.io/juvix-stdlib),
 which is preloaded by default.
 
-```juvix
+```jrepl
 Stdlib.Prelude> length (1 :: 2 :: nil)
 3
 Stdlib.Prelude> null (1 :: 2 :: nil)
@@ -136,7 +136,7 @@ evaluating `main`.
 
 To see the type of an expression, use the `:type` REPL command:
 
-```juvix
+```jrepl
 Stdlib.Prelude> :type 1
 Nat
 Stdlib.Prelude> :type true
@@ -300,7 +300,7 @@ It is not necessary to define a separate function to perform pattern
 matching. One can use the `case` syntax to pattern match an expression
 directly.
 
-```juvix
+```jrepl
 Stdlib.Prelude> case (1, 2) | (suc _, zero) := 0 | (suc _, suc x) := x | _ := 19
 1
 ```
@@ -365,7 +365,7 @@ even :=
     odd' zero := false;
     odd' (suc n) := even' n;
   in
-  even'
+  even';
 ```
 
 The functions `even'` and `odd'` are not visible outside `even`.
@@ -569,13 +569,16 @@ This is not acceptable if you care about performance. In an imperative
 language, one would use a simple loop going over the list without any
 memory allocation. In pseudocode:
 
-```juvix
-var sum : Nat := 0;
-while (lst /= nnil) {
+```pascal
+sum : Nat := 0;
+
+while (lst /= nil) do
+begin
   sum := sum + head lst;
   lst := tail lst;
-};
-return sum;
+end;
+
+result := sum;
 ```
 
 Fortunately, it is possible to rewrite this function to use _tail
@@ -613,16 +616,19 @@ imperative pseudocode for computing the nth Fibonacci number in linear
 time. The variables `cur` and `next` hold the last two computed
 Fibonacci numbers.
 
-```juvix
-var cur : Nat := 0;
-var next : Nat := 1;
-while (n /= 0) {
-  var tmp := next;
+```pascal
+cur : Nat := 0;
+next : Nat := 1;
+
+while (n /= 0) do
+begin
+  tmp := next;
   next := cur + next;
   cur := tmp;
   n := n - 1;
-};
-return cur;
+end;
+
+result := cur;
 ```
 
 An equivalent functional program is:
@@ -776,7 +782,7 @@ and the [Juvix program examples](../reference/examples.md).
     Analogously to the `map` function for lists, define a function
 
     ```juvix
-    tmap : (Nat -> Nat) -> Tree -> Tree
+    tmap : (Nat -> Nat) -> Tree -> Tree;
     ```
 
     which applies a function to all natural numbers stored in a tree.

src/Juvix/Compiler/Asm/Data/InfoTable.hs

@@ -5,6 +5,7 @@ module Juvix.Compiler.Asm.Data.InfoTable
   )
 where
 
+import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Asm.Language
 import Juvix.Compiler.Asm.Language.Rep
 import Juvix.Compiler.Asm.Language.Type
@@ -50,7 +51,7 @@ data InductiveInfo = InductiveInfo
     _inductiveLocation :: Maybe Location,
     _inductiveSymbol :: Symbol,
     _inductiveKind :: Type,
-    _inductiveConstructors :: [ConstructorInfo],
+    _inductiveConstructors :: [Tag],
     _inductiveRepresentation :: IndRep
   }
 
@@ -67,3 +68,12 @@ emptyInfoTable =
       _infoInductives = mempty,
       _infoMainFunction = Nothing
     }
+
+lookupFunInfo :: InfoTable -> Symbol -> FunctionInfo
+lookupFunInfo infoTable sym = fromMaybe (error "invalid function symbol") (HashMap.lookup sym (infoTable ^. infoFunctions))
+
+lookupConstrInfo :: InfoTable -> Tag -> ConstructorInfo
+lookupConstrInfo infoTable tag = fromMaybe (error "invalid constructor tag") (HashMap.lookup tag (infoTable ^. infoConstrs))
+
+lookupInductiveInfo :: InfoTable -> Symbol -> InductiveInfo
+lookupInductiveInfo infoTable sym = fromMaybe (error "invalid inductive symbol") (HashMap.lookup sym (infoTable ^. infoInductives))

src/Juvix/Compiler/Asm/Data/InfoTableBuilder.hs

@@ -2,7 +2,6 @@ module Juvix.Compiler.Asm.Data.InfoTableBuilder where
 
 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Asm.Data.InfoTable
-import Juvix.Compiler.Asm.Extra.Base
 import Juvix.Compiler.Asm.Language
 
 data IdentKind
@@ -76,4 +75,4 @@ runInfoTableBuilder =
         return $ HashMap.lookup txt (s ^. stateIdents)
       GetFunctionInfo sym -> do
         s <- get
-        return (getFunInfo (s ^. stateInfoTable) sym)
+        return (lookupFunInfo (s ^. stateInfoTable) sym)

src/Juvix/Compiler/Asm/Extra/Base.hs

@@ -1,6 +1,5 @@
 module Juvix.Compiler.Asm.Extra.Base where
 
-import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Language
 
@@ -16,15 +15,6 @@ mkInstr' loc = Instr . CmdInstr (CommandInfo loc)
 mkBinop' :: Maybe Location -> Opcode -> Command
 mkBinop' loc = mkInstr' loc . Binop
 
-getFunInfo :: InfoTable -> Symbol -> FunctionInfo
-getFunInfo infoTable sym = fromMaybe (error "invalid function symbol") (HashMap.lookup sym (infoTable ^. infoFunctions))
-
-getConstrInfo :: InfoTable -> Tag -> ConstructorInfo
-getConstrInfo infoTable tag = fromMaybe (error "invalid constructor tag") (HashMap.lookup tag (infoTable ^. infoConstrs))
-
-getInductiveInfo :: InfoTable -> Symbol -> InductiveInfo
-getInductiveInfo infoTable sym = fromMaybe (error "invalid inductive symbol") (HashMap.lookup sym (infoTable ^. infoInductives))
-
 isFinalInstr :: Instruction -> Bool
 isFinalInstr = \case
   Return -> True

src/Juvix/Compiler/Asm/Extra/Memory.hs

@@ -5,7 +5,6 @@ import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Data.Stack (Stack)
 import Juvix.Compiler.Asm.Data.Stack qualified as Stack
 import Juvix.Compiler.Asm.Error
-import Juvix.Compiler.Asm.Extra.Base
 import Juvix.Compiler.Asm.Extra.Type
 import Juvix.Compiler.Asm.Language
 import Juvix.Compiler.Asm.Pretty
@@ -91,7 +90,7 @@ getMemValueType :: InfoTable -> MemValue -> Memory -> Maybe Type
 getMemValueType tab val mem = case val of
   DRef dr -> getDirectRefType dr mem
   ConstrRef fld ->
-    let ci = getConstrInfo tab (fld ^. fieldTag)
+    let ci = lookupConstrInfo tab (fld ^. fieldTag)
         tyargs = typeArgs (ci ^. constructorType)
      in atMay tyargs (fld ^. fieldOffset)
 

src/Juvix/Compiler/Asm/Extra/Recursors.hs

@@ -123,7 +123,7 @@ recurse' sig = go True
             Prealloc {} ->
               return mem
             AllocConstr tag -> do
-              let ci = getConstrInfo (sig ^. recursorInfoTable) tag
+              let ci = lookupConstrInfo (sig ^. recursorInfoTable) tag
                   n = ci ^. constructorArgsNum
                   tyargs = typeArgs (ci ^. constructorType)
               checkValueStack' loc (sig ^. recursorInfoTable) tyargs mem
@@ -136,7 +136,7 @@ recurse' sig = go True
                 pushValueStack (mkTypeConstr (ci ^. constructorInductive) tag tys) $
                   popValueStack n mem
             AllocClosure InstrAllocClosure {..} -> do
-              let fi = getFunInfo (sig ^. recursorInfoTable) _allocClosureFunSymbol
+              let fi = lookupFunInfo (sig ^. recursorInfoTable) _allocClosureFunSymbol
                   (tyargs, tgt) = unfoldType (fi ^. functionType)
               checkValueStack' loc (sig ^. recursorInfoTable) (take _allocClosureArgsNum tyargs) mem
               return $
@@ -183,10 +183,10 @@ recurse' sig = go True
               AsmError loc "invalid call: not enough values on the stack"
           let ty = case _callType of
                 CallClosure -> topValueStack' 0 mem
-                CallFun sym -> getFunInfo (sig ^. recursorInfoTable) sym ^. functionType
+                CallFun sym -> lookupFunInfo (sig ^. recursorInfoTable) sym ^. functionType
           let argsNum = case _callType of
                 CallClosure -> length (typeArgs ty)
-                CallFun sym -> getFunInfo (sig ^. recursorInfoTable) sym ^. functionArgsNum
+                CallFun sym -> lookupFunInfo (sig ^. recursorInfoTable) sym ^. functionArgsNum
           when (argsNum /= 0) $
             checkFunType ty
           when (ty /= TyDynamic && argsNum /= _callArgsNum) $
@@ -375,7 +375,7 @@ recurseS' sig = go
             Prealloc {} ->
               return si
             AllocConstr tag -> do
-              let ci = getConstrInfo (sig ^. recursorInfoTable) tag
+              let ci = lookupConstrInfo (sig ^. recursorInfoTable) tag
                   n = ci ^. constructorArgsNum
               return $
                 stackInfoPopValueStack (n - 1) si

src/Juvix/Compiler/Asm/Interpreter.hs

@@ -128,7 +128,7 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
       Prealloc {} ->
         goCode cont
       AllocConstr tag -> do
-        let ci = getConstrInfo infoTable tag
+        let ci = lookupConstrInfo infoTable tag
         args <- replicateM (ci ^. constructorArgsNum) popValueStack
         pushValueStack (ValConstr (Constr tag args))
         goCode cont
@@ -240,7 +240,7 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
     getCallDetails :: (Member Runtime r) => Maybe Location -> InstrCall -> Sem r (Code, Frame)
     getCallDetails loc InstrCall {..} = case _callType of
       CallFun sym -> do
-        let fi = getFunInfo infoTable sym
+        let fi = lookupFunInfo infoTable sym
         when
           (_callArgsNum /= fi ^. functionArgsNum)
           (runtimeError "invalid direct call: supplied arguments number not equal to expected arguments number")
@@ -250,7 +250,7 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
         v <- popValueStack
         case v of
           ValClosure cl -> do
-            let fi = getFunInfo infoTable (cl ^. closureSymbol)
+            let fi = lookupFunInfo infoTable (cl ^. closureSymbol)
                 n = length (cl ^. closureArgs)
             when
               (n >= fi ^. functionArgsNum)
@@ -283,7 +283,7 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
       v <- popValueStack
       case v of
         ValClosure cl -> do
-          let fi = getFunInfo infoTable (cl ^. closureSymbol)
+          let fi = lookupFunInfo infoTable (cl ^. closureSymbol)
           let n = fi ^. functionArgsNum - length (cl ^. closureArgs)
           when
             (n < 0)