unison/unison-src/transcripts/fix2049.output.md

id x = x

structural ability Stream a where
  emit : a -> ()

Stream.foldl : (x ->{g} a ->{g} x) -> x -> '{g, Stream a} r -> '{g} x
Stream.foldl f z str _ =
  h acc = cases
    { emit x -> k } -> handle !k with h (f acc x)
    { _ } -> acc
  handle !str with h z

Stream.range : Nat -> Nat -> '{Stream Nat} ()
Stream.range m n = do
  f : Nat ->{Stream Nat} ()
  f k = if k < n then emit k ; f (k+1) else ()
  f m

unique type Fold' g a b x = Fold' (x -> {g} a -> {g} x) x (x -> {g} b)

unique type Fold g a b = Fold (∀ g2 r. (∀ x. Fold' g a b x -> {g2} r) -> {g2} r)

Fold.fromFold' : Fold' g a b x -> Fold g a b
Fold.fromFold' fold = Fold.Fold (f -> f fold)

Fold.mkFold : (t -> {g} a -> {g} t) -> t -> (t -> {g} b) -> Fold g a b
Fold.mkFold step init extract =
  Fold.fromFold' (Fold'.Fold' step init extract)

folds.all : (a -> {g} Boolean) -> Fold g a Boolean
folds.all predicate =
  Fold.mkFold (b -> a -> b && (predicate a)) true id

Fold.Stream.fold : Fold g a b -> '{g, Stream a} r -> '{g} b
Fold.Stream.fold =
  run: Fold' g a b x -> '{g, Stream a} r -> '{g} b
  run =
    cases Fold'.Fold' step init extract ->
      stream -> _ -> extract !(foldl step init stream)
  cases
    Fold f -> stream -> f (f' -> run f' stream)

> folds.all.tests.stream =
    pred = n -> (Nat.gt n 2)
    res : 'Boolean
    res = Fold.Stream.fold (folds.all pred) (Stream.range 1 5)
    !res Universal.== false

  Loading changes detected in scratch.u.

  I found and typechecked these definitions in scratch.u. If you
  do an `add` or `update`, here's how your codebase would
  change:
  
    ⍟ These new definitions are ok to `add`:
    
      type Fold g a b
      type Fold' g a b x
      structural ability Stream a
      Fold.Stream.fold : Fold g a b
                         -> '{g, Stream a} r
                         -> '{g} b
      Fold.fromFold'   : Fold' g a b x -> Fold g a b
      Fold.mkFold      : (t ->{g} a ->{g} t)
                         -> t
                         -> (t ->{g} b)
                         -> Fold g a b
      Stream.foldl     : (x ->{g} a ->{g} x)
                         -> x
                         -> '{g, Stream a} r
                         -> '{g} x
      Stream.range     : Nat -> Nat -> '{Stream Nat} ()
      folds.all        : (a ->{g} Boolean) -> Fold g a Boolean
      id               : x -> x
  
  Now evaluating any watch expressions (lines starting with
  `>`)... Ctrl+C cancels.

    44 |     pred = n -> (Nat.gt n 2)
           ⧩
           true

Tests some capabilities for catching runtime exceptions.

catcher : '{IO} () ->{IO} Result
catcher act =
  handle tryEval act with cases
    { raise _ -> _ } -> Ok "caught"
    { _ } -> Fail "nothing to catch"

tests _ =
  [ catcher do
      _ = 1/0
      ()
  , catcher '(bug "testing")
  , handle tryEval (do 1+1) with cases
      { raise _ -> _ } -> Fail "1+1 failed"
      { 2 } -> Ok "got the right answer"
      { _ } -> Fail "got the wrong answer"
  ]

  Loading changes detected in scratch.u.

  I found and typechecked these definitions in scratch.u. If you
  do an `add` or `update`, here's how your codebase would
  change:
  
    ⍟ These new definitions are ok to `add`:
    
      catcher : '{IO} () ->{IO} Result
      tests   : ∀ _. _ ->{IO} [Result]

scratch/main> add

  ⍟ I've added these definitions:
  
    catcher : '{IO} () ->{IO} Result
    tests   : ∀ _. _ ->{IO} [Result]

scratch/main> io.test tests

    New test results:
  
    1. tests   ◉ caught
               ◉ caught
               ◉ got the right answer
  
  ✅ 3 test(s) passing
  
  Tip: Use view 1 to view the source of a test.