Small changes for the presentation (#1456)

assets/linuwial.css

@@ -837,6 +837,10 @@ table.info {
   padding-left: 1em;
 }
 
+p.directory {
+  font-style: italic;
+}
+
 #module-list ul {
   list-style: none;
   margin: 0 0 0 2em;

examples/milestone/TicTacToe/CLI/TicTacToe.juvix

@@ -11,8 +11,6 @@ open import Stdlib.Data.Nat.Ord;
 open import Stdlib.Prelude;
 open import Logic.Game;
 
--- IO Utils
-
 axiom readline : String;
 compile readline {
   c ↦ "readline()";
@@ -24,17 +22,18 @@ compile parsePositiveInt {
   c ↦ "parsePositiveInt";
 };
 
--- IO
-
+-- | Reads a ;ℕ; from stdin
 getMove : Maybe ℕ;
 getMove ≔ validMove (parsePositiveInt (readline));
 
 do : IO × GameState -> GameState;
 do (_ , s) ≔ playMove getMove s;
 
+-- | A ;String; that prompts the user for their input
 prompt : GameState → String;
 prompt x ≔ "\n" ++str (showGameState x) ++str "\nPlayer " ++str showSymbol (player x) ++str ": ";
 
+-- | Main loop
 terminating
 run : (IO × GameState → GameState) → GameState → IO;
 run _ (state b p (terminate msg)) ≔ putStrLn ("\n" ++str (showGameState (state b p noError)) ++str "\n" ++str msg);

examples/milestone/TicTacToe/Logic/Board.juvix

@@ -0,0 +1,39 @@
+module Logic.Board;
+
+open import Stdlib.Prelude;
+open import Logic.Square public;
+open import Logic.Symbol public;
+open import Logic.Extra;
+
+--- A 3x3 grid of ;Square;s
+inductive Board {
+  board : List (List Square) → Board;
+};
+
+--- Returns the list of numbers corresponding to the empty ;Square;s
+possibleMoves : List Square → List ℕ;
+possibleMoves nil ≔ nil;
+possibleMoves ((empty n) ∷ xs) ≔ n ∷ possibleMoves xs;
+possibleMoves (_ ∷ xs) ≔ possibleMoves xs;
+
+--- ;true; if all the ;Square;s in the list are equal
+full : List Square → Bool;
+full (a ∷ b ∷ c ∷ nil) ≔ (==Square a b) && (==Square b c);
+
+diagonals : List (List Square) → List (List Square);
+diagonals ((a1 ∷ _ ∷ b1 ∷ nil) ∷ (_ ∷ c ∷ _ ∷ nil) ∷ (b2 ∷ _ ∷ a2 ∷ nil) ∷ nil) ≔ (a1 ∷ c ∷ a2 ∷ nil) ∷ (b1 ∷ c ∷ b2 ∷ nil) ∷ nil;
+
+columns : List (List Square) → List (List Square);
+columns ≔ transpose;
+
+rows : List (List Square) → List (List Square);
+rows ≔ id;
+
+--- Textual representation of a ;List Square;
+showRow : List Square → String;
+showRow xs ≔ concat (surround "|" (map showSquare xs));
+
+showBoard : Board → String;
+showBoard (board squares) ≔ unlines (surround "+---+---+---+" (map showRow squares));
+
+end;

examples/milestone/TicTacToe/Logic/Extra.juvix

@@ -0,0 +1,32 @@
+--- Some generic helper definitions.
+module Logic.Extra;
+
+open import Stdlib.Data.Nat.Ord;
+open import Stdlib.Prelude;
+
+infixr 5 ++str;
+--- Primitive concatenation of ;String;s
+axiom ++str : String → String → String;
+compile ++str {
+  c ↦ "concat";
+};
+
+--- Concatenates a list of strings
+---
+--- ;concat (("a" ∷ nil) ∷ ("b" ∷ nil)); evaluates to ;"a" ∷ "b" ∷ nil;
+concat : List String → String;
+concat ≔ foldl (++str) "";
+
+--- It inserts the first ;String; at the beginning, in between, and at the end of the second list
+surround : String → List String → List String;
+surround x xs ≔ (x ∷ intersperse x xs) ++ (x ∷ nil);
+
+--- It inserts the first ;String; in between the ;String;s in the second list and concatenates the result
+intercalate : String → List String → String;
+intercalate sep xs ≔ concat (intersperse sep xs);
+
+--- Joins a list of strings with the newline character
+unlines : List String → String;
+unlines ≔ intercalate "\n";
+
+end;

examples/milestone/TicTacToe/Logic/Game.juvix

@@ -8,166 +8,11 @@ module Logic.Game;
 
 open import Stdlib.Data.Nat.Ord;
 open import Stdlib.Prelude;
+open import Logic.Extra public;
+open import Logic.Board public;
+open import Logic.GameState public;
 
--- Render Utils
-
-infixr 5 ++str;
---- Concatenation of ;String;s
-axiom ++str : String → String → String;
-compile ++str {
-  c ↦ "concat";
-};
-
---- Concatenates a list of strings
----
---- ;concat (("a" ∷ nil) ∷ ("b" ∷ nil)); evaluates to ;"a" ∷ "b" ∷ nil;
-concat : List String → String;
-concat ≔ foldl (++str) "";
-
-surround : String → List String → List String;
-surround x xs ≔ (x ∷ intersperse x xs) ++ (x ∷ nil);
-
-intercalate : String → List String → String;
-intercalate sep xs ≔ concat (intersperse sep xs);
-
---- Joins a list of strings with the newline character
-unlines : List String → String;
-unlines ≔ intercalate "\n";
-
--- Symbol
-
---- A symbol represents a token that can be placed in a square
-inductive Symbol {
---- The circle token
-  O : Symbol;
---- The cross token
-  X : Symbol;
-};
-
---- Equality for ;Symbol;s
-==Symbol : Symbol → Symbol → Bool;
-==Symbol O O ≔ true;
-==Symbol X X ≔ true;
-==Symbol _ _ ≔ false;
-
---- Turns ;O; into ;X; and ;X; into ;O;
-switch : Symbol → Symbol;
-switch O ≔ X;
-switch X ≔ O;
-
---- Textual representation of a ;Symbol;
-showSymbol : Symbol → String;
-showSymbol O ≔ "O";
-showSymbol X ≔ "X";
-
--- Square
---- A square is each of the holes in a board
-inductive Square {
-  --- An empty square has a ;ℕ; that uniquely identifies it
-  empty : ℕ → Square;
-  --- An occupied square has a ;Symbol; in it
-  occupied : Symbol → Square;
-};
-
--- --- A row in a board implemented as ;List Square;
--- ---
--- --- >>> Row;
--- Row : Type;
--- Row ≔ List Square;
-
--- A column in a board implemented as ;List Square;
--- Column : Type;
--- Column ≔ Row;
-
---- Equality for ;Square;s
-==Square : Square → Square → Bool;
-==Square (empty m) (empty n) ≔ m == n;
-==Square (occupied s) (occupied t) ≔ ==Symbol s t;
-==Square _ _ ≔ false;
-
---- Textual representation of a ;Square;
-showSquare : Square → String;
-showSquare (empty n) ≔ " " ++str natToStr n ++str " ";
-showSquare (occupied s) ≔ " " ++str showSymbol s ++str " ";
-
--- TODO use a type alias?
---- A grid of squares
-inductive Board {
-  board : List (List Square) → Board;
-};
-
---- Returns the list of numbers corresponding to the empty ;Square;s
-possibleMoves : List Square → List ℕ;
-possibleMoves nil ≔ nil;
-possibleMoves ((empty n) ∷ xs) ≔ n ∷ possibleMoves xs;
-possibleMoves (_ ∷ xs) ≔ possibleMoves xs;
-
---- ;true; if all the ;Square;s in the list are equal
-full : List Square → Bool;
-full (a ∷ b ∷ c ∷ nil) ≔ (==Square a b) && (==Square b c);
-
-diagonals : List (List Square) → List (List Square);
-diagonals ((a1 ∷ _ ∷ b1 ∷ nil) ∷ (_ ∷ c ∷ _ ∷ nil) ∷ (b2 ∷ _ ∷ a2 ∷ nil) ∷ nil) ≔ (a1 ∷ c ∷ a2 ∷ nil) ∷ (b1 ∷ c ∷ b2 ∷ nil) ∷ nil;
-
-columns : List (List Square) → List (List Square);
-columns ≔ transpose;
-
-rows : List (List Square) → List (List Square);
-rows ≔ id;
-
---- Textual representation of a ;(List Square);
-showRow : (List Square) → String;
-showRow xs ≔ concat (surround "|" (map showSquare xs));
-
-showBoard : Board → String;
-showBoard (board squares) ≔ unlines (surround "+---+---+---+" (map showRow squares));
-
--- Error
-
-inductive Error {
---- no error occurred
-  noError : Error;
---- a non-fatal error occurred
-  continue : String → Error;
---- a fatal occurred
-  terminate : String → Error;
-};
-
--- GameState
-
-inductive GameState {
-  state : Board → Symbol → Error → GameState;
-};
-
---- Textual representation of a ;GameState;
-showGameState : GameState → String;
-showGameState (state b _ _) ≔ showBoard b;
-
---- Projects the player
-player : GameState → Symbol;
-player (state _ p _) ≔ p;
-
---- initial ;GameState;
-beginState : GameState;
-beginState ≔ state
-     (board (map (map empty) ((one ∷ two ∷ three ∷ nil) ∷ (four ∷ five ∷ six ∷ nil) ∷ (seven ∷ eight ∷ nine ∷ nil) ∷ nil)))
-     X
-     noError;
-
---- ;true; if some player has won the game
-won : GameState → Bool;
-won (state (board squares) _ _) ≔ any full (diagonals squares ++ rows squares ++ columns squares);
-
---- ;true; if there is a draw
-draw : GameState → Bool;
-draw (state (board squares) _ _) ≔ null (possibleMoves (flatten squares));
-
--- Move
-
-replace : Symbol → ℕ → Square → Square;
-replace player k (empty n) ≔ if (n Stdlib.Data.Nat.Ord.== k) (occupied player) (empty n);
-replace _ _ s ≔ s;
-
+--- Checks if we reached the end of the game.
 checkState : GameState → GameState;
 checkState (state b p e) ≔
   if (won (state b p e))
@@ -176,6 +21,7 @@ checkState (state b p e) ≔
          (state b p (terminate "It's a draw!"))
          (state b p e));
 
+--- Given a player attempted move, updates the state accordingly.
 playMove : Maybe ℕ → GameState → GameState;
 playMove nothing (state b p _) ≔
     state b p (continue "\nInvalid number, try again\n");
@@ -186,6 +32,7 @@ playMove (just k) (state (board s) player e) ≔
                            (switch player)
                            noError));
 
+--- Returns ;just; if the given ;ℕ; is in range of 1..9
 validMove : ℕ → Maybe ℕ;
 validMove n ≔ if ((n <= nine) && (n >= one)) (just n) nothing;
 

examples/milestone/TicTacToe/Logic/GameState.juvix

@@ -0,0 +1,43 @@
+module Logic.GameState;
+
+open import Stdlib.Prelude;
+open import Logic.Extra;
+open import Logic.Board;
+
+inductive Error {
+--- no error occurred
+  noError : Error;
+--- a non-fatal error occurred
+  continue : String → Error;
+--- a fatal occurred
+  terminate : String → Error;
+};
+
+inductive GameState {
+  state : Board → Symbol → Error → GameState;
+};
+
+--- Textual representation of a ;GameState;
+showGameState : GameState → String;
+showGameState (state b _ _) ≔ showBoard b;
+
+--- Projects the player
+player : GameState → Symbol;
+player (state _ p _) ≔ p;
+
+--- initial ;GameState;
+beginState : GameState;
+beginState ≔ state
+     (board (map (map empty) ((one ∷ two ∷ three ∷ nil) ∷ (four ∷ five ∷ six ∷ nil) ∷ (seven ∷ eight ∷ nine ∷ nil) ∷ nil)))
+     X
+     noError;
+
+--- ;true; if some player has won the game
+won : GameState → Bool;
+won (state (board squares) _ _) ≔ any full (diagonals squares ++ rows squares ++ columns squares);
+
+--- ;true; if there is a draw
+draw : GameState → Bool;
+draw (state (board squares) _ _) ≔ null (possibleMoves (flatten squares));
+
+end;

examples/milestone/TicTacToe/Logic/Square.juvix

@@ -0,0 +1,32 @@
+module Logic.Square;
+
+open import Stdlib.Prelude;
+open import Logic.Symbol;
+open import Stdlib.Data.Nat.Ord;
+open import Logic.Extra;
+
+--- A square is each of the holes in a board
+inductive Square {
+  --- An empty square has a ;ℕ; that uniquely identifies it
+  empty : ℕ → Square;
+  --- An occupied square has a ;Symbol; in it
+  occupied : Symbol → Square;
+};
+
+--- Equality for ;Square;s
+==Square : Square → Square → Bool;
+==Square (empty m) (empty n) ≔ m == n;
+==Square (occupied s) (occupied t) ≔ ==Symbol s t;
+==Square _ _ ≔ false;
+
+--- Textual representation of a ;Square;
+showSquare : Square → String;
+showSquare (empty n) ≔ " " ++str natToStr n ++str " ";
+showSquare (occupied s) ≔ " " ++str showSymbol s ++str " ";
+
+replace : Symbol → ℕ → Square → Square;
+replace player k (empty n) ≔ if (n Stdlib.Data.Nat.Ord.== k) (occupied player) (empty n);
+replace _ _ s ≔ s;
+
+
+end;

examples/milestone/TicTacToe/Logic/Symbol.juvix

@@ -0,0 +1,30 @@
+--- This module defines the ;Symbol; type and some helper functions.
+module Logic.Symbol;
+
+open import Stdlib.Prelude;
+
+--- A symbol represents a token that can be placed in a square
+inductive Symbol {
+--- The circle token
+  O : Symbol;
+--- The cross token
+  X : Symbol;
+};
+
+--- Equality for ;Symbol;s
+==Symbol : Symbol → Symbol → Bool;
+==Symbol O O ≔ true;
+==Symbol X X ≔ true;
+==Symbol _ _ ≔ false;
+
+--- Turns ;O; into ;X; and ;X; into ;O;
+switch : Symbol → Symbol;
+switch O ≔ X;
+switch X ≔ O;
+
+--- Textual representation of a ;Symbol;
+showSymbol : Symbol → String;
+showSymbol O ≔ "O";
+showSymbol X ≔ "X";
+
+end;

examples/milestone/TicTacToe/TicTacToe.juvix

@@ -0,0 +1,6 @@
+module TicTacToe;
+
+import CLI.TicTacToe;
+import Web.TicTacToe;
+
+end;

examples/milestone/TicTacToe/juvix.yaml

@@ -0,0 +1,2 @@
+name: tic-tac-toe
+version: 1.0.0

src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs

@@ -98,7 +98,7 @@ createIndexFile ps = do
         nodeRow = case lbl of
           Nothing ->
             return $
-              Html.span ! Attr.class_ attrBare $
+              Html.p ! Attr.class_ attrBare $
                 toHtml (prettyText s)
           Just lbl' -> do
             lnk <- nameIdAttrRef lbl' Nothing
@@ -106,9 +106,9 @@ createIndexFile ps = do
               Html.span ! Attr.class_ attrBare $
                 (a ! Attr.href lnk $ toHtml (prettyText lbl'))
         attrBase :: Html.AttributeValue
-        attrBase = "details-toggle-control details-toggle collapser"
+        attrBase = "details-toggle-control details-toggle"
         attrBare :: Html.AttributeValue
-        attrBare = attrBase <> "module"
+        attrBare = attrBase <> " directory"
         node :: Sem r Html
         node = do
           row' <- nodeRow
@@ -386,7 +386,7 @@ goOpen op
 goAxiom :: forall r. Members '[Reader HtmlOptions, Reader NormalizedTable] r => AxiomDef 'Scoped -> Sem r Html
 goAxiom axiom = do
   header' <- axiomHeader
-  defHeader tmp uid header' Nothing
+  defHeader tmp uid header' (axiom ^. axiomDoc)
   where
     uid :: NameId
     uid = axiom ^. axiomName . S.nameId

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

@@ -402,7 +402,7 @@ instance SingI s => PrettyCode (JudocParagraphLine s) where
   ppCode (JudocParagraphLine atoms) = do
     atoms' <- mconcatMap ppCode atoms
     let prefix = pretty (Str.judocStart :: Text) :: Doc Ann
-    return (prefix <> atoms' <> line)
+    return (prefix <+> atoms' <> line)
 
 instance SingI s => PrettyCode (Judoc s) where
   ppCode :: forall r. Members '[Reader Options] r => Judoc s -> Sem r (Doc Ann)

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs

@@ -574,14 +574,6 @@ inferExpression' e = case e of
           ExpressionFunction (Function (FunctionParameter paraName ifun funL) funR) -> do
             r' <- checkExpression funL r
             unless (iapp == ifun) (error "implicitness mismatch")
-            -- case l' ^. typedExpression of
-            --   ExpressionLambda (Lambda lamVar _ lamBody) ->
-            --     return
-            --       TypedExpression
-            --         { _typedExpression = substitutionE (HashMap.singleton lamVar r') lamBody,
-            --           _typedType = substitutionApp (paraName, r') funR
-            --         }
-            --   _ ->
             return
               TypedExpression
                 { _typedExpression =