reformat.expected

blah blah blah blah
  blah blah blah
  blah blah blah
  blah

constr. arg arg arg
  arg arg arg

x .fld .fld2 arg
  .fld3 arg arg arg
  arg

blah (blah blah)
  (blah (blah blah))
  (blah blah blah
     blah)

blah
  (blah blah blah
     blah blah blah
     blah) blah
  ((blah blah) blah
     (blah) blah)

x ↦ M

x ↦
blah blah blah blah
  blah blah blah
  blah blah

x x x x x x x x x x
  x x x x x x x ↦
M

x x x x x x x x x x
  x x x x x x x ↦
blah blah blah blah
  blah blah blah
  blah blah

M : A

M
: blah blah blah
    blah blah blah
    blah blah

blah blah blah blah
  blah blah blah
  blah
: A

blah blah blah
: blah blah blah

blah blah blah blah
  blah blah blah
  blah
: blah blah blah

blah blah blah
: blah blah blah
    blah blah blah
    blah

blah blah blah blah
  blah
: blah blah blah
    blah blah

blah blah blah blah
  blah blah blah
  blah
: blah blah blah
    blah blah blah
    blah blah

(x : A) → B

(x : A) (x : A) (x : A)
  (x : A) (x : A) (x : A)
  (x : A) (x : A) (x : A)
  (x : A)
  → C

(x : A) (x : A) (x : A)
  (x : A) (x : A) (x : A)
  (x : A) (x : A) (x : A)
  → C

(x : A)
  → blah blah blah blah blah
      blah blah blah blah
      blah blah

(x : A) → (x : A) → (x : A) → (x : A) → (x : A) → C

(x : A) → (x : A) → (x : A) → (x : A) → (x : A) → (x : A) → (x : A)
  → (x : A)
  → C

(x : A) → (x : A) → (x : A) → (x : A) → (x : A) → (x : A) → (x : A)
  → (x : A) → (x : A) → (x : A) → (x : A)
  → C

A → B

A → A → A → A → A → A → B

A → A → A → A → A → A → A → B

A → A → A → A → A → A → A → A
  → B

A → A → A → A → A → A → A → A
  → A
  → B

A → A → A → A → A → A → A → A
  → A → A
  → B

A → A → A → A → A → (x : A)
  → A
  → B

A → A → A → A → A → A → A → A
  → B

A → A → A → A → A → A → A → A
  → A → A
  → B

(x : A) → A → (x : A) → A
  → (x : A)
  → C

(x : A) (x : A) (x : A) → A
  → (x : A) (_ : A) 
  (x : A) (x : A) → (x : A)
  → C

A → A → A
  → blah blah blah blah blah
      blah blah blah → A → A
  → B

A → A → A
  → (x
     : blah blah blah blah
         blah blah blah blah)
  → A → A
  → B

(x : A) (x : A)
  (x
   : blah blah blah blah blah
       blah blah blah)
  (x : A) (x : A) (x : A)
  (x : A) (x : A) (x : A)
  → C

[> 1, 2, 3 >]

[> 1 >]

[> >]

[< 1, 2, 3 <]

[< 1 <]

[< <]

[>
  blah,
  blah,
  blah,
  blah,
  blah,
  blah,
  blah,
  blah,
  blah,
  blah,
  blah,
>]

[<
  blah,
  blah,
  blah,
  blah,
  blah,
  blah,
  blah,
  blah,
  blah,
  blah,
  blah,
<]

--------------------
Noncompactly
--------------------

let x ≔ y in z

let x ≔ y in
blah blah blah blah
  blah blah blah

let x ≔ y in
let z ≔ w in
u

let x ≔ y in let z ≔ w in u

let x
  ≔ blah blah blah
      blah blah
  in
blah blah blah blah
  blah blah

let x
  ≔ blah blah blah
      blah blah
  in
x

let x : w ≔ y in
let z : a ≔ w in
u

let x
  : boo boo boo boo
      boo boo boo
      boo boo
  ≔ blah blah blah
      blah blah
  in
blah blah blah blah
  blah blah

let x
  : boo boo boo boo
      boo boo boo
      boo boo
  ≔ blah blah blah
      blah blah
  in
x

let x
  : boo boo boo boo
      boo boo boo
      boo boo
  ≔ y
  in
blah blah blah blah
  blah blah

let x
  : boo boo boo boo
      boo boo boo
      boo boo
  ≔ y
  in
x

let x
  : a
  ≔ blah blah blah
      blah blah
  in
blah blah blah blah
  blah blah

let x
  : a
  ≔ blah blah blah
      blah blah
  in
x

(
  fst ≔ M,
  snd ≔ N,
)

f ( fst ≔ M, snd ≔ N )

(
  fst ≔
    blah blah blah blah blah
      blah,
  snd ≔
    blah blah blah blah blah
      blah blah blah,
)

(
  fst ≔
    blah blah blah blah blah
      blah,
  snd ≔ blah,
)

f
  (
    fst ≔
      blah blah blah blah
        blah blah,
    snd ≔
      blah blah blah blah
        blah blah blah blah,
  )

f
  (
    fst ≔
      blah blah blah blah
        blah blah,
    snd ≔ blah,
  )

(
  fst ≔ M,
  snd ≔ ( foo ≔ N, bar ≔ P ),
)

(
  fst ≔ M,
  snd ≔ ( foo ≔ N, bar ≔ P ),
)

f
  ( fst ≔ M, snd ≔ ( foo ≔ N, bar ≔ P ),
  )

[
  | .fst ↦
    blah blah blah blah blah
      blah 
  | .snd ↦
    blah blah blah blah blah
      blah blah blah 
]

[
  | .fst ↦ [
             | .foo ↦ bar 
             | .baz ↦ qux 
           ] 
  | .snd ↦ [
             | .poo ↦ [
                        | .bah ↦ bum 
                      ] 
           ] 
]

[
  | fst. ↦ [
             | foo. ↦ bar 
             | baz. ↦ qux 
           ] 
  | snd. ↦ [
             | poo. ↦ [
                        | bah. ↦ bum 
                      ] 
           ] 
]

match x [ 
  | con. a b ↦ blah blah 
  | str. u v ↦ bluh bluh 
]

match x [ 
  | con. a b ↦
    blah blah blah blah blah
      blah blah blah blah
      blah 
  | str. u v ↦ bluh bluh 
]

match x [ 
  | con. a a a a a a a a a a
      a a a a a a a a a a a a
      a ↦
    blah blah 
  | str. u v ↦ bluh bluh 
]

match x [ 
  | con. a a a a a a a a a a
      a a a a a a a a a a a a
      a ↦
    blah blah blah blah blah
      blah blah blah blah
      blah blah 
  | str. u v ↦ bluh bluh 
]

[
  | con. a b ↦ blah blah 
  | str. u v ↦ bluh bluh 
]

match x [ 
  | con. a b ↦
    match y [ 
      | foo. ↦
        ba ba baa ba baa baba
          ba ba baaba babba
          ba 
      | bar. u v w z w ↦ z 
    ] 
  | str. u v ↦ bluh bluh 
]

match x [ 
  | con. a b ↦
    [
      | .foo ↦
        ba ba baa ba baa baba
          ba ba baaba babba
          ba 
      | .bar ↦ z 
    ] 
  | str. u v ↦
    [
      | .flab ↦ boo boo 
      | .flub ↦
        zoo zo zoo zo zzo zo 
    ] 
]

[
  | con. a b ↦
    [
      | foo. x ↦ ba ba ba 
      | bar. y z ↦ y 
    ] 
  | str. u v ↦
    [
      | baz. ↦ bluh bluh 
    ] 
]

(match x [ 
   | poo. ↦ bah 
 ])

match x , y [ 
  | true. , false. ↦ 0 
  | true. , true. ↦ 1 
]

match x [ 
  | zero. ↦ 0 
  | suc. zero. ↦ 1 
  | suc. (suc. zero.) ↦ 2 
  | suc. (suc. (suc. n)) ↦ n 
]

codata [
| x .head : blah blah blah
              blah blah blah
              blah blah
| x .tail : Stream A
]

codata [
| x .head : blah blah blah
              blah blah blah
              blah blah
              → blah 
| x .tail
  : Stream A
]

sig (
  fst : blah blah blah blah
          blah blah blah blah,
  tail : Stream A,
  )

data [
| one.
  : blah blah blah blah blah
      blah blah blah blah
      → blah 
| two. : me ]


--------------------
Compactly
--------------------

let x ≔ y in z

let x ≔ y in
blah blah blah blah
  blah blah blah

let x ≔ y in
let z ≔ w in
u

let x ≔ y in let z ≔ w in u

let x
  ≔ blah blah blah
      blah blah in
blah blah blah blah
  blah blah

let x
  ≔ blah blah blah
      blah blah in
x

let x : w ≔ y in
let z : a ≔ w in
u

let x
  : boo boo boo boo
      boo boo boo
      boo boo
  ≔ blah blah blah
      blah blah in
blah blah blah blah
  blah blah

let x
  : boo boo boo boo
      boo boo boo
      boo boo
  ≔ blah blah blah
      blah blah in
x

let x
  : boo boo boo boo
      boo boo boo
      boo boo
  ≔ y in
blah blah blah blah
  blah blah

let x
  : boo boo boo boo
      boo boo boo
      boo boo
  ≔ y in
x

let x
  : a
  ≔ blah blah blah
      blah blah in
blah blah blah blah
  blah blah

let x
  : a
  ≔ blah blah blah
      blah blah in
x

( fst ≔ M,
  snd ≔ N )

f ( fst ≔ M, snd ≔ N )

( fst ≔
    blah blah blah blah blah
      blah,
  snd ≔
    blah blah blah blah blah
      blah blah blah )

( fst ≔
    blah blah blah blah blah
      blah,
  snd ≔ blah )

f
  ( fst ≔
      blah blah blah blah
        blah blah,
    snd ≔
      blah blah blah blah
        blah blah blah blah )

f
  ( fst ≔
      blah blah blah blah
        blah blah,
    snd ≔ blah )

( fst ≔ M,
  snd ≔ ( foo ≔ N, bar ≔ P ) )

( fst ≔ M,
  snd ≔ ( foo ≔ N, bar ≔ P ) )

f
  ( fst ≔ M,
    snd ≔ ( foo ≔ N, bar ≔ P ) )

[ | .fst ↦
    blah blah blah blah blah
      blah 
  | .snd ↦
    blah blah blah blah blah
      blah blah blah ]

[ | .fst ↦ [ | .foo ↦ bar | .baz ↦ qux ] 
  | .snd ↦ [ | .poo ↦ [ | .bah ↦ bum ] ] ]

[ | fst. ↦ [ | foo. ↦ bar 
             | baz. ↦ qux ] 
  | snd. ↦ [ | poo. ↦ [ | bah. ↦ bum ] ] ]

match x [ 
  | con. a b ↦ blah blah 
  | str. u v ↦ bluh bluh ]

match x [ 
  | con. a b ↦
    blah blah blah blah blah
      blah blah blah blah
      blah 
  | str. u v ↦ bluh bluh ]

match x [ 
  | con. a a a a a a a a a a
      a a a a a a a a a a a a
      a ↦
    blah blah 
  | str. u v ↦ bluh bluh ]

match x [ 
  | con. a a a a a a a a a a
      a a a a a a a a a a a a
      a ↦
    blah blah blah blah blah
      blah blah blah blah
      blah blah 
  | str. u v ↦ bluh bluh ]

[ | con. a b ↦ blah blah 
  | str. u v ↦ bluh bluh ]

match x [ 
  | con. a b ↦ match y [ 
    | foo. ↦
      ba ba baa ba baa baba
        ba ba baaba babba ba 
    | bar. u v w z w ↦ z ] 
  | str. u v ↦ bluh bluh ]

match x [ 
  | con. a b ↦ [ 
    | .foo ↦
      ba ba baa ba baa baba
        ba ba baaba babba ba 
    | .bar ↦ z ] 
  | str. u v ↦ [ 
    | .flab ↦ boo boo 
    | .flub ↦
      zoo zo zoo zo zzo zo ] ]

[ | con. a b ↦
    [ | foo. x ↦ ba ba ba 
      | bar. y z ↦ y ] 
  | str. u v ↦
    [ | baz. ↦ bluh bluh ] ]

(match x [ 
   | poo. ↦ bah ])

match x , y [ 
  | true. , false. ↦ 0 
  | true. , true. ↦ 1 ]

match x [ 
  | zero. ↦ 0 
  | suc. zero. ↦ 1 
  | suc. (suc. zero.) ↦ 2 
  | suc. (suc. (suc. n)) ↦ n ]

codata [
| x .head : blah blah blah
              blah blah blah
              blah blah
| x .tail : Stream A ]

codata [
| x .head : blah blah blah
              blah blah blah
              blah blah
              → blah 
| x .tail
  : Stream A ]

sig (
  fst : blah blah blah blah
          blah blah blah blah,
  tail : Stream A)

data [
| one.
  : blah blah blah blah blah
      blah blah blah blah
      → blah 
| two. : me ]