juvix/tests/positive/Format.juvix

{-- This is Judoc block comment --}
module -- Declaring a top module of name:
Format;

------------ many --- in comment

import Stdlib.Prelude -- Import a module of name:
open -- Bring all names into scope but..
hiding -- Hide some names
{-- like this
,; -- don't want , here
-- Bool either
Bool; true; false; mkShow; module Show};

-- Lorem ipsum dolor sit amet, consectetur adipiscing elit
terminating
-- Comment between terminating and type sig
go : Nat → Nat → Nat
  | n s := ite (s < n) (go (sub n 1) s) (go n (sub s n) + go (sub n 1) s);

module {- local module -}
M;
  syntax -- syntax in local modules
  operator , pair;
  axiom , : String → String → String;
end;

-- case with single branch
case1 (n : Nat) : Nat := case n of x := zero;

-- case with multiple branches
case2 (n : Nat) : Nat :=
  case n of
    | zero := zero
    | _ := zero;

-- case on nested case
case3 (n : Nat) : Nat :=
  case case n of {_ := zero} of
    | zero := zero
    | _ := zero;

-- case on nested case expression
case4 (n : Nat) : Nat :=
  case n of
    | zero := case n of {x := zero}
    | _ := zero;

-- -- case with application subject
case5 (n : Nat) : Nat := case id n of x := zero;

-- qualified commas
t4 : String := "a" M., "b" M., "c" M., "d";

open M;

-- mix qualified and unqualified commas
t5 : String := "a" M., "b" M., "c", "d";

-- comma chain fits in a line
t2 : String := "a", "b", "c", "d";

-- comma chain does not fit in a line
t3 : String :=
  "a"
    , "b"
    , "c"
    , "d"
    , "e"
    , "f"
    , "g"
    , "h"
    , "i"
    , "j"
    , "k"
    , "1234"
    , "1234"
    , "1234"
    , "1234"
    , "1234"
    , "1234"
    , "1234"
    , "1234";

-- escaping in String literals
e1 : String := "\"\n";

module Integers;
  binary : Nat := 0b1010101;

  octal : Nat := 0o3076101;

  decimal : Nat := 9076191;

  hexadecimal : Nat := 0x9076191aaff;

  neghexadecimal : Int := -0x9076191aaff;
end;

syntax fixity l1 := binary {assoc := left; below := [pair]};
syntax fixity r3 := binary {assoc := right; above := [pair]};
syntax fixity l6 := binary {assoc := left; above := [r3]};
syntax fixity r6 := binary {assoc := right; same := l6};
syntax fixity l7 := binary {assoc := left; above := [l6]};

syntax operator +l7 l7;
axiom +l7 : String → String → String;

syntax operator +r3 r3;
axiom +r3 : String → String → String;

syntax operator +l1 l1;
axiom +l1 : String → String → String;

syntax operator +l6 l6;
axiom +l6 : String → String → String;

syntax operator +r6 r6;
axiom +r6 : String → String → String;

-- nesting of chains
t : String :=
  "Hellooooooooo"
    +l1 "Hellooooooooo"
    +l1 "Hellooooooooo"
        +l6 "Hellooooooooo"
        +l6 ("Hellooooooooo" +r6 "Hellooooooooo" +r6 "Hellooooooooo")
        +l6 "Hellooooooooo"
        +l6 "Hellooooooooo" +l7 "Hellooooooooo" +l7 "Hellooooooooo" +l7 "Hellooooooooo"
      , "hi"
      , "hi";

-- function with single wildcard parameter
g : (_ : Type) -> Nat
  | _ := 1;

-- grouping of type arguments
exampleFunction1
  : {A : Type}
    -> List A
    -> List A
    -> List A
    -> List A
    -> List A
    -> List A
    -> List A
    -> List A
    -> List A
    -> List A
    -> Nat
  | _ _ _ _ _ _ _ _ _ _ := 1;

axiom undefined : {A : Type} -> A;

-- 200 in the body is indented with respect to the start of the chain
-- (at {A : Type})
exampleFunction2
  : {A : Type}
    -> List A
    -> List A
    -> List A
    -> List A
    -> List A
    -> List A
    -> List A
    -> List A
    -> List A
    -> List A
    -> Nat :=
  λ {_ _ _ _ _ _ _ _ _ _ :=
    undefined
      -- comment after first
      + undefined
      -- comment after second
      + undefined
      + undefined
      + undefined
      + undefined
      + undefined
      + undefined
      + undefined
      + undefined
      + undefined};

positive
type T0 (A : Type) := c0 : (A -> T0 A) -> T0 A;

-- Single Lambda clause
idLambda : {A : Type} -> A -> A := λ {x := x};

-- Lambda clauses
f : Nat -> Nat :=
  \ {
    -- comment before lambda pipe
    | zero :=
      let
        foo : Nat := 1;
      in foo
    | _ -- comment before lambda :=
    := 1
  };

module Patterns;

  syntax operator × functor;
  syntax operator , pair;
  type × (A : Type) (B : Type) := , : A → B → A × B;

  f : Nat × Nat × Nat × Nat -> Nat
    | (a, b, c, d) := a;

end;

module UnicodeStrings;
  a : String := "λ";
end;

module Comments;

  axiom a1 : Type;
  -- attached to a1

  -- attached to a2
  axiom a2 : Type;

  -- attached to nothing

  axiom a3 -- comment before axiom :
  : Type;

  num
    -- comment before type sig :
    : -- comment after type sig :
    Nat :=
    -- comment before clause :=
    -- comment after clause :=
    123;

  -- attached to nothing
  -- attached to nothing 2

  -- attached to nothing 3

  axiom a4 : -- before open pi brace
    {-- after open pi brace
    a -- before pi :
    : Type}
    -> Type;

  id2 : {A : Type} -> A -> Nat -> A
    | -- before patternarg braces
    {A} a -- before open patternarg parens
    (suc b) :=
      idLambda
        -- before implicit app
        {-- inside implicit arg
        A}
        -- before closing implicit arg
        a
    | a _ := a;

  type color : Type :=
    -- comment before pipe
    | black : color
    | white : color
    | red : color
    -- comment before pipe
    | blue : color;

  axiom a5 : Type;

  open Patterns -- before using
  using -- before brace
  {-- before first f
  f; f};

  type list (A : Type) : Type := cons A (list A);
end;

module EmptyRecords;
  import Stdlib.Data.Bool.Base open;

  type T := mkT {};

  x : T := mkT@{};

  isZero : Nat -> Bool
    | zero := true
    | suc@{} := false;
end;

--- Traits
module Traits;
  import Stdlib.Prelude open hiding {Show; mkShow; module Show};

  trait
  type Show A := mkShow {show : A → String};

  instance
  showStringI : Show String :=
    mkShow@{
      show := id
    };

  instance
  showBoolI : Show Bool :=
    mkShow@{
      show := λ {x := ite x "true" "false"}
    };

  instance
  showNatI : Show Nat :=
    mkShow@{
      show := natToString
    };

  showList {A} : {{Show A}} → List A → String
    | nil := "nil"
    | (h :: t) := Show.show h ++str " :: " ++str showList t;

  g : {A : Type} → {{Show A}} → Nat := 5;

  instance
  showListI {A} {{Show A}} : Show (List A) :=
    mkShow@{
      show := showList
    };

  showMaybe {A} {{Show A}} : Maybe A → String
    | (just x) := "just (" ++str Show.show x ++str ")"
    | nothing := "nothing";

  instance
  showMaybeI {A} {{Show A}} : Show (Maybe A) :=
    mkShow@{
      show := showMaybe
    };

  f {A} {{Show A}} : A → String
    | x := Show.show x;

  f' {A} : {{Show A}} → A → String
    | {{mkShow s}} x := s x;

  f'' {A} : {{Show A}} → A → String
    | {{M}} x := Show.show {{M}} x;

  f'3 {A} {{M : Show A}} : A → String := Show.show {{M}};

  f'4 {A} {{_ : Show A}} : A → String := Show.show;

end;

module OperatorRecord;
  trait
  type Natural A :=
    myNatural {
      syntax operator + additive;
      + : A -> A -> A;

      syntax operator * multiplicative;
      * : A -> A -> A
    };

  open Natural;

  calc {A : Type} {{Natural A}} (n m : A) : A :=
    let
      open Natural;
    in n + m * m;
end;

module RecordFieldPragmas;
  type Pr (A B : Type) :=
    mkPr {
      --- Judoc for A
      {-# inline: false #-}
      pfst : A;
      {-# inline: false #-}
      psnd : B
    };
end;

longLongLongArg : Int := 0;

longLongLongListArg : List Int := [];

l1 : List Int :=
  [ 1
  ; 2
  ; longLongLongArg
  ; longLongLongArg
  ; longLongLongArg
  ; longLongLongArg
  ; longLongLongArg
  ; longLongLongArg
  ];

l2 : List Int := [1; 2; 3];

l3 : List (List Int) :=
  [ [1; 2; 3]
  ; longLongLongListArg
  ; longLongLongListArg
  ; longLongLongListArg
  ; longLongLongListArg
  ; longLongLongListArg
  ];

l4 : List (List Int) :=
  [ [1; 2; 3]
  ; longLongLongListArg
  ; [ longLongLongArg
    ; longLongLongArg
    ; longLongLongArg
    ; longLongLongArg
    ; longLongLongArg
    ; longLongLongArg
    ]
  ; longLongLongListArg
  ];

-- Format as-pattern interacting with implicit args.

implicitWithInnerParens : {_ : Nat} -> Nat
  | {A@(suc B@(suc x))} := x
  | {B@(suc x)} := B
  | {_} := zero;

i2479' : {_ : Nat} -> Nat
  | {suc (suc x)} := x
  | {suc x} := x
  | {_} := zero;

-- formatting arguments that do not fit in a line
fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
  {f : List Nat} : Nat := zero;

-- formatting arguments that do not fit in a line
fff
  {f : List Nat}
  {f0 : List Nat}
  {f1 : List Nat}
  {f2 : List Nat}
  {f3 : List Nat}
  {f4 : List Nat}
  {f5 : List Nat}
  {f6 : List Nat}
  {f7 : List Nat}
  : Nat := zero;

module SideIfConditions;
  singleCaseBr : Nat :=
    case 12 of
      _
        | if 0 < 0 := 3
        | else := 4;

  multiCaseBr : Nat :=
    case 12 of
      | zero
        | if 0 < 0 := 3
        | if 0 > 0 := 6
        | else := 4
      | suc (suc n)
        | if 0 < 0 := 3
        | else := n
      | suc n if 0 < 0 := 3
      | suc zero := 5;
end;

module MultiIf;
  x : Nat :=
    if
      | 0 == 1 := 1
      | 1 == 1 := 1
      | else := 2;
end;

module PublicImports;

  module Inner;
    import Stdlib.Prelude as X.Y.Z using {Nat} public;
  end;

  axiom a : Inner.X.Y.Z.Nat;
end;

-- Comment at the end of a module