/*---------------------------------------------------------------------------
  Copyright 2012-2024, Microsoft Research, Daan Leijen.

  This is free software; you can redistribute it and/or modify it under the
  terms of the Apache License, Version 2.0. A copy of the License can be
  found in the LICENSE file at the root of this distribution.
---------------------------------------------------------------------------*/

/* Internal effect handler primitives.

  Internal primitives to implement evidence based algebraic
  effect handlers. These are emitted by the compiler during evidence
  translation and this module is always implicitly imported.

  This module is compiled _without monadic translation_ and
  thus we need to do this by hand in this module which allows us to implement
  most primitives directly in Koka keeping the external C/JavaScript/etc primitives
  to a minimum.

  The paper:

  > Ningning Xie, and Daan Leijen. _Generalized Evidence Passing for Effect Handlers_,
  > or _efficient compilation of effect handlers to C_.
  > Proceedings of the ACM International Conference on Functional Programming (ICFP'21),
  > August 2021, Vol 5: pp. 71, doi: 10.1145/3473576.
  > <https://www.microsoft.com/en-us/research/publication/generalized-evidence-passing-for-effect-handlers-or-efficient-compilation-of-effect-handlers-to-c/>

  describes precisely how the monadic evidence translation works on which this
  module is based. Read this first to understand how this module works.

  Another paper of interest is:

  > Ningning Xie, and Daan Leijen. _Effect Handlers in Haskell, Evidently_.
  > The 13th ACM SIGPLAN International Haskell Symposium, (Haskell'20),
  > August 2020. <https://www.microsoft.com/en-us/research/uploads/prod/2020/07/effev.pdf>

  which which explains the internal typing of handlers, evidence vectors, etc. in a simpler setting.

  ## Notes

  An effect _row_ has kind `::E`, while an atomic effect kind is `::X`.
  (We will see that `::X` is equal to the kind `::(E,V) -> V` ) (`::V` is for value kinds *)

  We use the term "answer" context to talk about the result type `:r` and effect type `:e` of
  (the context of) the handler in the stack. The `:e` does not include the effect `::X` of the handler.

  - `:marker<e,r>` : a unique integer corresponding to an answer context `:<e,r>`. This functions
    as a dependent type: when the integer matches at runtime, that will be the type of the answer context.

  - handlers `:h` are partially applied types with signature `h<e,r> :: (E,V)->V`
    for some answer context `:<e,r>`. The handlers contain all operations (much like a virtual method table).
    (these handler types are generated by the compiler for each effect type)

  - Evidence `ev<h :: (E,V)->V >` for a handler `:h` is an existential tuple
    `forall e r. Ev( marker: marker<e,r>, hnd: h<e,r> )` containing the marker and the actual handler (pointer)
    for some answer context `:<e,r>` -- we don't know the answer context exact type as it depends on where
    the handler was dynamically bound; we just have evidence that this handler `:h` exists in our context.

  - Actually, we use a quadruple for the evidence (corresponding to the evidence as formalized in the generalized evidence paper).
    We also add the handler effect tag (`:htag<h>`) (for dynamic lookup), and the evidence vector
    of the answer context where the handler was defind (`:evv<e,r>`)
    (so we can execute operations in-place using the evidence vector at the point where they were defined).

  - Each operation definition in a handler is called a _clause_. For a one argument operation, we have:
    ```
    abstract value type clause1<a,b,h,e::E,r>
      Clause1( clause: (marker<e,r>, ev<h>, a) -> e b )
    ```
    defining an operation `:a -> b` for some handler `:h` in an answer context `:<e,r>`.
    (these are generated by the compiler from a handler definition)

  - An operation is performed by a rank-2 function:
    `fun perform1( ev : ev<h>, select-op : (forall<e1,r> h<e1,r> -> clause1<a,b,h,e1,r>), x : a ) : e b`
    where we can call an operation given evidence for a handler `:ev<h>` together with a
    polymorphic field selection function that for any handler `h` in _any_ answer context, returns its clause.
    It is defined as:
    ```
      match ev
        Ev(_tag,m,h,_answ) -> match select-op(h)  // for an abstract `:<e1,r>`
          Clause1(f) -> f(m,ev,x)
    ```

  - Each clause _definition_ can now determine to fully yield to the handler, or be tail-resumptive etc.
    (that is, this is determined at the handler definition site, not the call site, and generated by the compiler)
    For example, we could be most general (`ctl`) and yield back to the marker (where the handler was defined in the call-stack)
    (with a function that receives the continuation/resumption `k`):
    ```
    Clause1( fn(m,ev,x) yield-to(m, fn(k) op(k,x) ))
    ```
    or be super efficient and directly call the (tail-resumptive) operation in-place (`fun`):
    ```
    Clause1( fn(m,ev,x) op(x) )
    ```
    and various variants in-between. The last definition is unsafe for example if the (user defined) `op` invokes
    operations itself as the evidence vector should be the one as defined at the handler site.
    So, we norally use instead:
    ```
    Clause1( fn(m,ev,x) under1(ev,op,x) )
    ```
    where `under1` uses the evidence vector (`hevv`) stored in the evidence `ev` to execute `op(x)` under.
    (this is also explained in detail in the generalized evidence paper).

*/
module std/core/hndstd/core/hnd

import std/core/typesstd/core/types
import std/core/undivstd/core/undiv

extern import
  c  file "inline/hnd"
  js file "inline/hnd.js"

// -------------------------------------------
// Internal types
// -------------------------------------------

// The tag of a handler identifies the type at runtime (e.g. `"exn/core/std"`).
abstract value type htagstd/core/hnd/htag: ((E, V) -> V) -> V<hh: (E, V) -> V::(E,V)->V>
  Htagstd/core/hnd/Htag: forall<a> (tagname : string) -> htag<a>(tagnamestd/core/hnd/htag/tagname: forall<a> (htag : htag<a>) -> string:stringstd/core/types/string: V)

// _Internal_ hidden constructor for creating handler tags
pub fun @new-htag( tagtag: string : stringstd/core/types/string: V )result: -> total htag<2786> : htagstd/core/hnd/htag: ((E, V) -> V) -> V<hh: (E, V) -> V>
  Htagstd/core/hnd/Htag: forall<a> (tagname : string) -> htag<a>(tagtag: string)

// Show a handler tag.
pub fun htag/showstd/core/hnd/htag/show: forall<a> (htag<a>) -> string( Htagstd/core/hnd/Htag: forall<a> (tagname : string) -> htag<a>(tagtag: string) : htagstd/core/hnd/htag: ((E, V) -> V) -> V<hh: (E, V) -> V> )result: -> total string : stringstd/core/types/string: V
  tagtag: string


// Effect handler evidence of a handler `:h` in the context.
abstract type evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>
  con Evstd/core/hnd/Ev: forall<a,e,b> (htag : htag<a>, marker : marker<e,b>, hnd : a<e,b>, hevv : evv<e>) -> ev<a><ee: E,rr: V>(htagstd/core/hnd/ev/htag: forall<a> (ev : ev<a>) -> htag<a>:htagstd/core/hnd/htag: ((E, V) -> V) -> V<hh: (E, V) -> V>, marker:markerstd/core/hnd/marker: (E, V) -> V<ee: E,rr: V>, hnd:hh: (E, V) -> V<ee: E,rr: V>, hevv:evvstd/core/hnd/evv: E -> V<ee: E>)

// Abstract type of Evidence vectors
type evvstd/core/hnd/evv: E -> V<ee: E::E>

// Index into an evidence vector
pub alias ev-indexstd/core/hnd/ev-index: V = ssize_tstd/core/types/ssize_t: V

// Evidence equality compares the markers.
pub fun ev/(==)std/core/hnd/ev/(==): forall<a> (ev<a>, ev<a>) -> bool( Evstd/core/hnd/Ev: forall<a,e,b> (htag : htag<a>, marker : marker<e,b>, hnd : a<e,b>, hevv : evv<e>) -> ev<a>(_,m1m1: marker<$2872,$2873>)  : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, Evstd/core/hnd/Ev: forall<a,e,b> (htag : htag<a>, marker : marker<e,b>, hnd : a<e,b>, hevv : evv<e>) -> ev<a>(_,m2m2: marker<$2885,$2886>) : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V> )result: -> total bool : boolstd/core/types/bool: V
  eq-markerstd/core/hnd/eq-marker: (x : marker<$2872,$2873>, y : marker<$2885,$2886>) -> bool(m1m1: marker<$2872,$2873>,m2m2: marker<$2885,$2886>)


// -------------------------------------------
// Internal Markers
// -------------------------------------------

// _Internal_. The type of handler markers (usually `:int32_t`).
// Needed for effect handlers in `module std/core/hnd`.
value type markerstd/core/hnd/marker: (E, V) -> V<ee: E::E,aa: V>

// Are two markers equal?
extern eq-markerstd/core/hnd/eq-marker: forall<a,b,e,e1> (x : marker<e,a>, y : marker<e1,b>) -> bool( xx: marker<$2812,$2810> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,a1a1: V>, yy: marker<$2813,$2811> : markerstd/core/hnd/marker: (E, V) -> V<e2e2: E,a2a2: V> ) : boolstd/core/types/bool: V
  inline "#1==#2"

extern fresh-markerstd/core/hnd/fresh-marker: forall<a,e> () -> marker<e,a>() : markerstd/core/hnd/marker: (E, V) -> V<ee: E,aa: V>
  c inline "kk_marker_unique(kk_context())"
  js inline "$marker_unique++"

extern fresh-marker-namedstd/core/hnd/fresh-marker-named: forall<a,e> () -> marker<e,a>() : markerstd/core/hnd/marker: (E, V) -> V<ee: E,aa: V>
  c inline  "-kk_marker_unique(kk_context())"
  js inline "-($marker_unique++)"



// -------------------------------------------
// Internal Evidence vectors
// The datatype is `:evv<e>` is internal for performance
// reasons and since different backends may have different
// requirements.
// -------------------------------------------

// Insert new evidence into the given evidence vector.
extern evv-insertstd/core/hnd/evv-insert: forall<e,e1,a> (evv : evv<e>, ev : ev<a>) -> e evv<e1>( evvevv: evv<$2987> : evvstd/core/hnd/evv: E -> V<e1e1: E>, evev: ev<$2989> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V> ) : e1e1: E evvstd/core/hnd/evv: E -> V<e2e2: E>
  c  "kk_evv_insert"
  js "_evv_insert"

// show evidence for debug purposes
extern evv-showstd/core/hnd/evv-show: forall<e> (evv : evv<e>) -> string( evvevv: evv<$3027> : evvstd/core/hnd/evv: E -> V<ee: E> ) : stringstd/core/types/string: V
  c  "kk_evv_show"
  js "_evv_show"

// Is an evidence vector unchanged? (i.e. as pointer equality).
// This is used to avoid copying in common cases.
extern evv-eqstd/core/hnd/evv-eq: forall<e> (evv0 : evv<e>, evv1 : evv<e>) -> bool(evv0evv0: evv<$3046> : evvstd/core/hnd/evv: E -> V<ee: E>, evv1evv1: evv<$3046> : evvstd/core/hnd/evv: E -> V<ee: E> ) : boolstd/core/types/bool: V
  c  "kk_evv_eq"
  js inline "(#1) === (#2)"


// -------------------------------------------
// Operations on the "current" evidence vector
// -------------------------------------------

// Return the evidence at index `i` in the current evidence vector.
pub inline extern @evv-at<e,h> ( i : ev-indexstd/core/hnd/ev-index: V ) : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>  // pretend total; don't simplify
  c  "kk_evv_at"
  js "$std_core_hnd._evv_at"

// (dynamically) find evidence insertion/deletion index in the evidence vector
// The compiler optimizes `@evv-index` to a static index when apparent from the effect type.
pub extern @evv-index<ee: E::E,hh: (E, V) -> V>( htaghtag: htag<$3067> : htagstd/core/hnd/htag: ((E, V) -> V) -> V<hh: (E, V) -> V> ) : ee: E ev-indexstd/core/hnd/ev-index: V
  c  "kk_evv_index"
  js "__evv_index"

// Get evidence at a mask level for duplicate labels.
pub inline extern @evv-index-mask( i : ev-indexstd/core/hnd/ev-index: V, mask-level : ev-indexstd/core/hnd/ev-index: V ) : ee: E ev-indexstd/core/hnd/ev-index: V
  inline "#1+#2"

// Get the current evidence vector.
extern evv-getstd/core/hnd/evv-get: forall<e> () -> e evv<e>() : ee: E evvstd/core/hnd/evv: E -> V<ee: E>
  c  "kk_evv_get"
  js "$std_core_hnd._evv_get"

// Set the current evidence vector.
inline extern evv-setstd/core/hnd/evv-set: forall<e,e1> (w : evv<e1>) -> e ()<e1,e>( w : evvstd/core/hnd/evv: E -> V<e1e1: E> ) : ee: E (std/core/types/unit: V)std/core/types/unit: V
  c  "kk_evv_set"
  js "$std_core_hnd._evv_set"

// Does the current evidence vector consist solely of affine handlers?
// This is called in backends that do not have context paths (like javascript)
// to optimize TRMC (where we can use faster update-in-place TRMC if we know the
// operations are all affine). As such, it is always safe to return `false`.
//
// control flow context:
//                 -1: none: bottom
//                   /          \
// 0: except: never resumes   1: linear: resumes exactly once
//                   \          /
//           2: affine: resumes never or once
//                        |
//     3: multi: resumes never, once, or multiple times
//
pub extern @evv-is-affine() : boolstd/core/types/bool: V
  c  inline "kk_evv_is_affine(kk_context())"
  js inline "$std_core_hnd._evv_is_affine_()"


// -----------------------------------------------------------------------------------
// Various swap variants.
// These are here just for improved performance (by avoiding dup/drop for example)
// -----------------------------------------------------------------------------------

// Swap the current evidence vector with `w`
inline extern evv-swapstd/core/hnd/evv-swap: forall<e,e1,e2> (w : evv<e1>) -> e evv<e2><e1,e2>( w : evvstd/core/hnd/evv: E -> V<e1e1: E> ) : ee: E evvstd/core/hnd/evv: E -> V<e2e2: E>
  c  "kk_evv_swap"
  js "$std_core_hnd._evv_swap"

// Remove evidence at index `i` of the current evidence vector, and return the old one.
// (used by `mask`)
extern evv-swap-deletestd/core/hnd/evv-swap-delete: forall<e,e1> (i : ev-index, behind : bool) -> e1 evv<e>( ii: ev-index : ev-indexstd/core/hnd/ev-index: V, behindbehind: bool : boolstd/core/types/bool: V ) : e1e1: E evvstd/core/hnd/evv: E -> V<ee: E>
  c  "kk_evv_swap_delete"
  js "_evv_swap_delete"

// Swap the current evidence vector with an empty vector.
// (this is used in open calls to switch to a total context)
inline extern evv-swap-create0std/core/hnd/evv-swap-create0: forall<e> () -> e evv<e>() : ee: E evvstd/core/hnd/evv: E -> V<ee: E>  //not quite the right effect type but avoids unbound effect types
  c  "kk_evv_swap_create0"
  js "$std_core_hnd._evv_swap_create0"

// Swap the current evidence vector with a singleton vector (with the evidence at current index `i`).
// (this is common in open calls to switch to a singleton effect context when calling operations)
inline extern evv-swap-create1std/core/hnd/evv-swap-create1: forall<e> (i : ev-index) -> e evv<e>( i : ev-indexstd/core/hnd/ev-index: V ) : ee: E evvstd/core/hnd/evv: E -> V<ee: E>  //not quite the right effect type but avoids unbound effect types
  c  "kk_evv_swap_create1"
  js "$std_core_hnd._evv_swap_create1"

// Swap the current evidence vector with a new vector consisting of evidence
// at indices `indices` in the current vector.
extern evv-swap-createstd/core/hnd/evv-swap-create: forall<e> (indices : vector<ev-index>) -> e evv<e>( indicesindices: vector<ev-index> : vectorstd/core/types/vector: V -> V<ev-indexstd/core/hnd/ev-index: V> ) : ee: E evvstd/core/hnd/evv: E -> V<ee: E>  //not quite the right effect type but avoids unbound effect types
  c  "kk_evv_swap_create"
  js "_evv_swap_create"



// -------------------------------------------
// Internal multi-prompt delimited control
// -------------------------------------------

pub inline extern yieldingstd/core/hnd/yielding: () -> bool() : boolstd/core/types/bool: V
  c  "kk_yielding"
  js "$std_core_hnd._yielding"

pub inline extern yielding-non-finalstd/core/hnd/yielding-non-final: () -> bool() : boolstd/core/types/bool: V
  c  "kk_yielding_non_final"
  js "$std_core_hnd._yielding_non_final"

pub noinline extern yield-extendstd/core/hnd/yield-extend: forall<a,b,e> (next : (a) -> e b) -> e b(nextnext: ($3156) -> $3158 $3157 : aa: V -> ee: E bb: V ) : ee: E bb: V
  c  "kk_yield_extend"
  js "_yield_extend"

pub inline fun yield-bindstd/core/hnd/yield-bind: forall<a,b,e> (x : a, next : (a) -> e b) -> e b( xx: $3195 : aa: V, nextnext: ($3195) -> $3197 $3196 : aa: V -> ee: E bb: V )result: -> 3232 3231 : ee: E bb: V
  if yieldingstd/core/hnd/yielding: () -> $3197 bool() then yield-extendstd/core/hnd/yield-extend: (next : ($3195) -> $3197 $3196) -> $3197 $3196(nextnext: ($3195) -> $3197 $3196) else nextnext: ($3195) -> $3197 $3196(xx: $3195)

pub inline fun yield-bind2std/core/hnd/yield-bind2: forall<a,b,e> (x : a, extend : (a) -> e b, next : (a) -> e b) -> e b( xx: $3242 : aa: V, extendextend: ($3242) -> $3244 $3243 : aa: V -> ee: E bb: V, nextnext: ($3242) -> $3244 $3243 : aa: V -> ee: E bb: V )result: -> 3279 3278 : ee: E bb: V
  if yieldingstd/core/hnd/yielding: () -> $3244 bool() then yield-extendstd/core/hnd/yield-extend: (next : ($3242) -> $3244 $3243) -> $3244 $3243(extendextend: ($3242) -> $3244 $3243) else nextnext: ($3242) -> $3244 $3243(xx: $3242)

extern yield-contstd/core/hnd/yield-cont: forall<a,e,b> (f : forall<c> ((c) -> e a, c) -> e b) -> e b(ff: forall<a> ((a) -> $3290 $3289, a) -> $3290 $3291 : forall<bb: V> (bb: V -> ee: E aa: V, bb: V) -> ee: E rr: V ) : ee: E rr: V  // make hidden pub?
  c  "kk_yield_cont"
  js "_yield_cont"

inline extern keep-yielding-finalstd/core/hnd/keep-yielding-final: forall<e,a> () -> e a() : ee: E rr: V
  c  "kk_box_any"
  js inline "undefined"

extern yield-promptstd/core/hnd/yield-prompt: forall<a,e,b> (m : marker<e,b>) -> yld<e,a,b>( mm: marker<$3338,$3339>: markerstd/core/hnd/marker: (E, V) -> V<ee: E,rr: V> ) : yldstd/core/hnd/yld: (E, V, V) -> V<ee: E,aa: V,rr: V>
  c  "kk_yield_prompt"
  js "_yield_prompt"

extern yield-to-primstd/core/hnd/yield-to-prim: forall<a,e,e1,b> (m : marker<e1,b>, clause : ((resume-result<a,b>) -> e1 b) -> e1 b) -> e (() -> a)( mm: marker<$3382,$3383> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>, clauseclause: ((resume-result<$3380,$3383>) -> $3382 $3383) -> $3382 $3383 : (resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> e1e1: E rr: V) -> e1e1: E rr: V ) : ee: E (() -> bstd/core/types/total: E)
  c  "kk_yield_to"
  js "$std_core_hnd._yield_to"

extern yield-to-finalstd/core/hnd/yield-to-final: forall<a,e,e1,b> (m : marker<e1,b>, clause : ((resume-result<a,b>) -> e1 b) -> e1 b) -> e a( mm: marker<$3437,$3438> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>, clauseclause: ((resume-result<$3435,$3438>) -> $3437 $3438) -> $3437 $3438 : (resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> e1e1: E rr: V) -> e1e1: E rr: V ) : ee: E bb: V
  c  "kk_yield_final"
  js "$std_core_hnd._yield_final"

noinline fun yield-tostd/core/hnd/yield-to: forall<a,e,b> (m : marker<e,b>, clause : ((resume-result<a,b>) -> e b) -> e b) -> e a( mm: marker<$3488,$3489> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>, clauseclause: ((resume-result<$3487,$3489>) -> $3488 $3489) -> $3488 $3489 : (resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> e1e1: E rr: V) -> e1e1: E rr: V )result: -> 3536 3535 : e1e1: E bb: V
  //val w0 = evv-get()
  val gg: () -> $3487 : () -> _b_b: V = yield-to-primstd/core/hnd/yield-to-prim: (m : marker<$3488,$3489>, clause : ((resume-result<$3487,$3489>) -> $3488 $3489) -> $3488 $3489) -> $3488 (() -> $3487)(mm: marker<$3488,$3489>, clauseclause: ((resume-result<$3487,$3489>) -> $3488 $3489) -> $3488 $3489)
  yield-extendstd/core/hnd/yield-extend: (next : (() -> $3488 $3487) -> $3488 $3487) -> $3488 $3487 fnfn: (f : () -> $3488 $3487) -> $3488 $3487(ff: () -> $3488 $3487)
    // val keep1 = guard(w0)  // check the evidence is correctly restored
    ff: () -> $3488 $3487()

pub type yield-infostd/core/hnd/yield-info: V

extern yield-capturestd/core/hnd/yield-capture: forall<e> () -> e yield-info() : ee: E yield-infostd/core/hnd/yield-info: V
  c "kk_yield_capture"
  js "_yield_capture"

pub extern unsafe-reyieldstd/core/hnd/unsafe-reyield: forall<a,e> (yld : yield-info) -> e a(yldyld: yield-info : yield-infostd/core/hnd/yield-info: V) : ee: E aa: V
  c "kk_yield_reyield"
  js "_reyield"


// -------------------------------------------
//
// -------------------------------------------

inline extern cast-ev0std/core/hnd/cast-ev0: forall<a,e,e1> (f : () -> e1 a) -> (() -> e a)( f:() -> e1e1: E bb: V) : ((std/core/types/total: E) -> e0e0: E bb: V)
  inline "#1"

inline extern cast-ev1std/core/hnd/cast-ev1: forall<a,b,e,e1> (f : (a) -> e1 b) -> ((a) -> e b)( f:(a1a1: V) -> e1e1: E bb: V) : ((std/core/types/total: Ea1a1: V) -> e0e0: E bb: V)
  inline "#1"

inline extern cast-ev2std/core/hnd/cast-ev2: forall<a,b,c,e,e1> (f : (a, b) -> e1 c) -> ((a, b) -> e c)( f:(a1a1: V,a2a2: V) -> e1e1: E bb: V) : ((std/core/types/total: Ea1a1: V,a2a2: V) -> e0e0: E bb: V)
  inline "#1"

inline extern cast-ev3std/core/hnd/cast-ev3: forall<a,b,c,d,e,e1> (f : (a, b, c) -> e1 d) -> ((a, b, c) -> e d)( f:(a1a1: V,a2a2: V,a3a3: V) -> e1e1: E bb: V) : ((std/core/types/total: Ea1a1: V,a2a2: V,a3a3: V) -> e0e0: E bb: V)
  inline "#1"

inline extern cast-ev4std/core/hnd/cast-ev4: forall<a,b,c,d,a1,e,e1> (f : (a, b, c, d) -> e1 a1) -> ((a, b, c, d) -> e a1)( f:(a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e1e1: E bb: V) : ((std/core/types/total: Ea1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e0e0: E bb: V)
  inline "#1"

inline extern cast-ev5std/core/hnd/cast-ev5: forall<a,b,c,d,a1,b1,e,e1> (f : (a, b, c, d, a1) -> e1 b1) -> ((a, b, c, d, a1) -> e b1)( f:(a1a1: V,a2a2: V,a3a3: V,a4a4: V,a5a5: V) -> e1e1: E bb: V) : ((std/core/types/total: Ea1a1: V,a2a2: V,a3a3: V,a4a4: V,a5a5: V) -> e0e0: E bb: V)
  inline "#1"

value type resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V>
  Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>( result: bb: V )
  Shallowstd/core/hnd/Shallow: forall<a,b> (result : a) -> resume-result<a,b>( result: bb: V )
  Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>( result : rr: V )

value type yldstd/core/hnd/yld: (E, V, V) -> V<ee: E,aa: V,rr: V>
  Purestd/core/hnd/Pure: forall<e,a,b> yld<e,a,b>
  YieldingFinalstd/core/hnd/YieldingFinal: forall<e,a,b> yld<e,a,b>
  Yieldingstd/core/hnd/Yielding: forall<e,a,b> yld<e,a,b>
  Yieldstd/core/hnd/Yield: forall<e,a,b,c> (clause : ((resume-result<c,b>) -> e b) -> e b, cont : (() -> c) -> e a) -> yld<e,a,b><bb: V>(clause : (resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V) -> ee: E rr: V, cont : (() -> bstd/core/types/total: E) -> ee: E aa: V)

extern guardstd/core/hnd/guard: forall<e> (w : evv<e>) -> e ()(ww: evv<$3588> : evvstd/core/hnd/evv: E -> V<ee: E> ) : ee: E (std/core/types/unit: V)std/core/types/unit: V
  c  inline "kk_evv_guard(#1,kk_context())"
  js "_guard"

extern resume-finalstd/core/hnd/resume-final: forall<a> () -> a() : astd/core/types/total: E
  c  inline "kk_fatal_resume_final(kk_context())"
  js "_throw_resume_final"

fun promptstd/core/hnd/prompt: forall<a,e,b,c> (w0 : evv<e>, w1 : evv<e>, ev : ev<b>, m : marker<e,c>, ret : (a) -> e c, result : a) -> e c( w0w0: evv<$3622> : evvstd/core/hnd/evv: E -> V<e0e0: E>,  w1w1: evv<$3622> : evvstd/core/hnd/evv: E -> V<e0e0: E>, evev: ev<$3623> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, mm: marker<$3622,$3624> : markerstd/core/hnd/marker: (E, V) -> V<e0e0: E,rr: V>, retret: ($3621) -> $3622 $3624: aa: V -> e0e0: E rr: V, resultresult: $3621 : aa: V )result: -> 3973 3975 : e0e0: E rr: V
  guardstd/core/hnd/guard: (w : evv<$3622>) -> $3622 ()(w1w1: evv<$3622>)
  evv-setstd/core/hnd/evv-set: (w : evv<$3622>) -> $3622 ()(w0w0: evv<$3622>)  // restore the previous evidence vector
  match yield-promptstd/core/hnd/yield-prompt: (m : marker<$3622,$3624>) -> $3622 yld<$3622,$3621,$3624>(mm: marker<$3622,$3624>)
    Purestd/core/hnd/Pure: forall<e,a,b> yld<e,a,b> ->
      // returning
      retret: ($3621) -> $3622 $3624(resultresult: $3621)
    YieldingFinalstd/core/hnd/YieldingFinal: forall<e,a,b> yld<e,a,b> ->
      // yielding final (exception), keep yielding
      keep-yielding-finalstd/core/hnd/keep-yielding-final: () -> $3622 $3624()
    Yieldingstd/core/hnd/Yielding: forall<e,a,b> yld<e,a,b> ->
      // regular yield, install a continuation
      yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $3622 $3621, a) -> $3622 $3624) -> $3622 $3624 fnfn: forall<a> (cont : (a) -> $3622 $3621, res : a) -> $3622 $3624(contcont: ($3683) -> $3622 $3621,resres: $3683)
        // we resume, continue under a fresh a prompt again
        val w0'w0': evv<$3622> = evv-getstd/core/hnd/evv-get: () -> $3622 evv<$3622>()  // if not using scoped resumptions, w0' may be different from w0
        val w1'w1': evv<$3622> = if (evv-eqstd/core/hnd/evv-eq: (evv0 : evv<$3622>, evv1 : evv<$3622>) -> $3622 bool(w0w0: evv<$3622>,w0'w0': evv<$3622>)) then w1w1: evv<$3622> else evv-insertstd/core/hnd/evv-insert: (evv : evv<$3622>, ev : ev<$3623>) -> $3622 evv<$3622>(w0'w0': evv<$3622>,evev: ev<$3623>)
        evv-setstd/core/hnd/evv-set: (w : evv<$3622>) -> $3622 ()(w1'w1': evv<$3622>)
        promptstd/core/hnd/prompt: (w0 : evv<$3622>, w1 : evv<$3622>, ev : ev<$3623>, m : marker<$3622,$3624>, ret : ($3621) -> $3622 $3624, result : $3621) -> $3622 $3624(w0'w0': evv<$3622>,w1'w1': evv<$3622>,evev: ev<$3623>,pretend-decreasingstd/core/undiv/pretend-decreasing: (x : marker<$3622,$3624>) -> $3622 marker<$3622,$3624>(mm: marker<$3622,$3624>),retret: ($3621) -> $3622 $3624,contcont: ($3683) -> $3622 $3621(resres: $3683));
    Yieldstd/core/hnd/Yield: forall<e,a,b,c> (clause : ((resume-result<c,b>) -> e b) -> e b, cont : (() -> c) -> e a) -> yld<e,a,b>(clauseclause: ((resume-result<$3757,$3624>) -> $3622 $3624) -> $3622 $3624,contcont: (() -> $3757) -> $3622 $3621) ->
      // yielded to the operation `clause` in our handler
      fun resumeresume: (r : resume-result<$3757,$3624>) -> $3622 $3624(rr: resume-result<$3757,$3624>)result: -> $3622 $3624
        match(rr: resume-result<$3757,$3624>)
          Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(xx: $3757) ->
            val w0'w0': evv<$3622> = evv-getstd/core/hnd/evv-get: () -> $3622 evv<$3622>()  // if not using scoped resumptions, w0' may be different from w0
            val w1'w1': evv<$3622> = if evv-eqstd/core/hnd/evv-eq: (evv0 : evv<$3622>, evv1 : evv<$3622>) -> $3622 bool(w0w0: evv<$3622>,w0'w0': evv<$3622>) then w1w1: evv<$3622> else evv-insertstd/core/hnd/evv-insert: (evv : evv<$3622>, ev : ev<$3623>) -> $3622 evv<$3622>(w0'w0': evv<$3622>,evev: ev<$3623>)
            evv-setstd/core/hnd/evv-set: (w : evv<$3622>) -> $3622 ()(w1'w1': evv<$3622>)
            promptstd/core/hnd/prompt: (w0 : evv<$3622>, w1 : evv<$3622>, ev : ev<$3623>, m : marker<$3622,$3624>, ret : ($3621) -> $3622 $3624, result : $3621) -> $3622 $3624(w0'w0': evv<$3622>,w1'w1': evv<$3622>,evev: ev<$3623>,pretend-decreasingstd/core/undiv/pretend-decreasing: (x : marker<$3622,$3624>) -> $3622 marker<$3622,$3624>(mm: marker<$3622,$3624>),retret: ($3621) -> $3622 $3624,contcont: (() -> $3757) -> $3622 $3621({xx: $3757}))
          Shallowstd/core/hnd/Shallow: forall<a,b> (result : a) -> resume-result<a,b>(xx: $3757) ->
            yield-bindstd/core/hnd/yield-bind: (x : $3621, next : ($3621) -> $3622 $3624) -> $3622 $3624( contcont: (() -> $3757) -> $3622 $3621({xx: $3757}), fnfn: (y : $3621) -> $3622 $3624(yy: $3621) retret: ($3621) -> $3622 $3624(yy: $3621) )
          Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>(xx: $3624) ->
            val w0'w0': evv<$3622> = evv-getstd/core/hnd/evv-get: () -> $3622 evv<$3622>()  // if not using scoped resumptions, w0' may be different from w0
            val w1'w1': evv<$3622> = if evv-eqstd/core/hnd/evv-eq: (evv0 : evv<$3622>, evv1 : evv<$3622>) -> $3622 bool(w0w0: evv<$3622>,w0'w0': evv<$3622>) then w1w1: evv<$3622> else evv-insertstd/core/hnd/evv-insert: (evv : evv<$3622>, ev : ev<$3623>) -> $3622 evv<$3622>(w0'w0': evv<$3622>,evev: ev<$3623>)
            evv-setstd/core/hnd/evv-set: (w : evv<$3622>) -> $3622 ()(w1'w1': evv<$3622>)
            promptstd/core/hnd/prompt: (w0 : evv<$3622>, w1 : evv<$3622>, ev : ev<$3623>, m : marker<$3622,$3624>, ret : ($3621) -> $3622 $3624, result : $3621) -> $3622 $3624(w0'w0': evv<$3622>,w1'w1': evv<$3622>,evev: ev<$3623>,pretend-decreasingstd/core/undiv/pretend-decreasing: (x : marker<$3622,$3624>) -> $3622 marker<$3622,$3624>(mm: marker<$3622,$3624>),retret: ($3621) -> $3622 $3624,contcont: (() -> $3757) -> $3622 $3621({ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$3622,$3624>, clause : ((resume-result<$3757,$3624>) -> $3622 $3624) -> $3622 $3624) -> $3757(mm: marker<$3622,$3624>, fnfn: ((resume-result<$3757,$3624>) -> $3622 $3624) -> $3622 $3624(_k) xx: $3624) }))
      clauseclause: ((resume-result<$3757,$3624>) -> $3622 $3624) -> $3622 $3624(resumeresume: (r : resume-result<$3757,$3624>) -> $3622 $3624) // TODO: we should exit prompt first, and then execute clause to use constant stack space when resuming

pub noinline fun @hhandle( tagtag: htag<$3991>:htagstd/core/hnd/htag: ((E, V) -> V) -> V<hh: (E, V) -> V>, hh: $3991<$3989,$3992> : hh: (E, V) -> V<ee: E,rr: V>, retret: ($3988) -> $3989 $3992: aa: V -> ee: E rr: V, actionaction: () -> $3990 $3988 : () -> e1e1: E aa: V )result: -> 4095 4098 : ee: E rr: V
  // insert new evidence for our handler
  val w0w0: evv<$3989> = evv-getstd/core/hnd/evv-get: () -> $3989 evv<$3989>()
  val mm: marker<$3989,$3992>  = fresh-markerstd/core/hnd/fresh-marker: () -> $3989 marker<$3989,$3992>()
  val evev: ev<$3991> = Evstd/core/hnd/Ev: forall<a,e,b> (htag : htag<a>, marker : marker<e,b>, hnd : a<e,b>, hevv : evv<e>) -> ev<a>(tagtag: htag<$3991>,mm: marker<$3989,$3992>,hh: $3991<$3989,$3992>,w0w0: evv<$3989>)
  val w1w1: evv<$3989> = evv-insertstd/core/hnd/evv-insert: (evv : evv<$3989>, ev : ev<$3991>) -> $3989 evv<$3989>(w0w0: evv<$3989>,evev: ev<$3991>)
  evv-setstd/core/hnd/evv-set: (w : evv<$3989>) -> $3989 ()(w1w1: evv<$3989>)
  // call action first (this may be yielding), then check the result
  promptstd/core/hnd/prompt: (w0 : evv<$3989>, w1 : evv<$3989>, ev : ev<$3991>, m : marker<$3989,$3992>, ret : ($3988) -> $3989 $3992, result : $3988) -> $3989 $3992(w0w0: evv<$3989>,w1w1: evv<$3989>,evev: ev<$3991>,mm: marker<$3989,$3992>,retret: ($3988) -> $3989 $3992,cast-ev0std/core/hnd/cast-ev0: (f : () -> $3990 $3988) -> $3989 (() -> $3989 $3988)(actionaction: () -> $3990 $3988)())

// -------------------------------------------
// named handler
// (which is not inserted into the evidence vector)
// -------------------------------------------

pub noinline fun @named-handle( tagtag: htag<$4117>:htagstd/core/hnd/htag: ((E, V) -> V) -> V<hh: (E, V) -> V>, hh: $4117<$4115,$4118> : hh: (E, V) -> V<ee: E,rr: V>, retret: ($4114) -> $4115 $4118: aa: V -> ee: E rr: V, actionaction: (ev<$4117>) -> $4116 $4114 : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V> -> e1e1: E aa: V )result: -> 4205 4208 : ee: E rr: V
  val mm: marker<$4115,$4118> = fresh-marker-namedstd/core/hnd/fresh-marker-named: () -> $4115 marker<$4115,$4118>()            // unique (negative) marker, but never gets inserted into the evidence vector
  val w0w0: evv<$4115> = evv-getstd/core/hnd/evv-get: () -> $4115 evv<$4115>()
  val evev: ev<$4117> = Evstd/core/hnd/Ev: forall<a,e,b> (htag : htag<a>, marker : marker<e,b>, hnd : a<e,b>, hevv : evv<e>) -> ev<a>(tagtag: htag<$4117>,mm: marker<$4115,$4118>,hh: $4117<$4115,$4118>,w0w0: evv<$4115>)
  promptstd/core/hnd/prompt: (w0 : evv<$4115>, w1 : evv<$4115>, ev : ev<$4117>, m : marker<$4115,$4118>, ret : ($4114) -> $4115 $4118, result : $4114) -> $4115 $4118(w0w0: evv<$4115>,w0w0: evv<$4115>,evev: ev<$4117>,mm: marker<$4115,$4118>,retret: ($4114) -> $4115 $4118,cast-ev1std/core/hnd/cast-ev1: (f : (ev<$4117>) -> $4116 $4114) -> $4115 ((ev<$4117>) -> $4115 $4114)(actionaction: (ev<$4117>) -> $4116 $4114)(evev: ev<$4117>))


// -------------------------------------------
// mask
// -------------------------------------------

fun mask-at1std/core/hnd/mask-at1: forall<a,b,e,e1> (i : ev-index, behind : bool, action : (a) -> e b, x : a) -> e1 b( ii: ev-index : ev-indexstd/core/hnd/ev-index: V, behindbehind: bool : boolstd/core/types/bool: V, actionaction: ($4224) -> $4226 $4225 : (aa: V) -> e1e1: E bb: V, xx: $4224 : aa: V )result: -> 4336 4334 : e2e2: E bb: V
  val w0w0: evv<_4233> = evv-swap-deletestd/core/hnd/evv-swap-delete: (i : ev-index, behind : bool) -> $4227 evv<_4233>(ii: ev-index,behindbehind: bool)
  val yy: $4225 = cast-ev1std/core/hnd/cast-ev1: (f : ($4224) -> $4226 $4225) -> $4227 (($4224) -> $4227 $4225)(actionaction: ($4224) -> $4226 $4225)(xx: $4224)
  evv-setstd/core/hnd/evv-set: (w : evv<_4233>) -> $4227 ()(w0w0: evv<_4233>)
  if yieldingstd/core/hnd/yielding: () -> $4227 bool() returnreturn: $4225 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $4227 $4225, a) -> $4227 $4225) -> $4227 $4225( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($4277) -> $4227 $4225,resres: $4277) mask-at1std/core/hnd/mask-at1: (i : ev-index, behind : bool, action : ($4277) -> $4227 $4225, x : $4277) -> $4227 $4225(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev-index) -> $4227 ev-index(ii: ev-index),behindbehind: bool,contcont: ($4277) -> $4227 $4225,resres: $4277) )std/core/types/Unit: ()
  yy: $4225

pub fun @mask-at<aa: V,e1e1: E,e2e2: E>( ii: ev-index : ev-indexstd/core/hnd/ev-index: V, behindbehind: bool : boolstd/core/types/bool: V, actionaction: () -> $4350 $4349 : () -> e1e1: E aa: V )result: -> 4445 4443 : e2e2: E aa: V
  val w0w0: evv<_4357> = evv-swap-deletestd/core/hnd/evv-swap-delete: (i : ev-index, behind : bool) -> $4351 evv<_4357>(ii: ev-index,behindbehind: bool)
  val xx: $4349 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $4350 $4349) -> $4351 (() -> $4351 $4349)(actionaction: () -> $4350 $4349)()
  evv-setstd/core/hnd/evv-set: (w : evv<_4357>) -> $4351 ()(w0w0: evv<_4357>)
  if yieldingstd/core/hnd/yielding: () -> $4351 bool() returnreturn: $4349 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $4351 $4349, a) -> $4351 $4349) -> $4351 $4349( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($4397) -> $4351 $4349,resres: $4397) mask-at1std/core/hnd/mask-at1: (i : ev-index, behind : bool, action : ($4397) -> $4351 $4349, x : $4397) -> $4351 $4349(ii: ev-index,behindbehind: bool,contcont: ($4397) -> $4351 $4349,resres: $4397) )std/core/types/Unit: ()
  xx: $4349

// mask for builtin effects without a handler or evidence (like `:st` or `:local`)
pub fun @mask-builtin<aa: V,e1e1: E,e2e2: E>( actionaction: () -> $4456 $4455 : () -> e1e1: E aa: V )result: -> 4486 4484 : e2e2: E aa: V
  cast-ev0std/core/hnd/cast-ev0: (f : () -> $4456 $4455) -> $4457 (() -> $4457 $4455)(actionaction: () -> $4456 $4455)()


// -------------------------------------------
// Local variables
// -------------------------------------------

fun prompt-local-varstd/core/hnd/prompt-local-var: forall<a,b,h> (loc : local-var<h,a>, res : b) -> <div,local<h>> b(locloc: local-var<$4499,$4496>:local-varstd/core/types/local-var: (H, V) -> V<ss: H,aa: V>, resres: $4497 : bb: V  )result: -> <div,local<4604>|4603> 4602 : <divstd/core/types/div: X,localstd/core/types/local: H -> X<ss: H>|std/core/types/effect-extend: (X, E) -> Eee: E> bb: V
  if !std/core/types/bool/(!): (b : bool) -> <div,local<$4499>|$4498> boolyieldingstd/core/hnd/yielding: () -> <div,local<$4499>|$4498> bool() returnreturn: $4497 resres: $4497;
  val vv: $4496 = locloc: $4496
  yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> <div,local<$4499>|$4498> $4497, a) -> <div,local<$4499>|$4498> $4497) -> <div,local<$4499>|$4498> $4497(fnfn: forall<a,e> (cont : (a) -> <div,local<$4499>|e> $4497, x : a) -> <div,local<$4499>|e> $4497(contcont: ($4545) -> <div,local<$4499>|$4498> $4497,xx: $4545){ locloc: local-var<$4499,$4496> :=std/core/types/local-set: (v : local-var<$4499,$4496>, assigned : $4496) -> <local<$4499>,div|$4498> () vv: $4496; prompt-local-varstd/core/hnd/prompt-local-var: (loc : local-var<$4499,$4496>, res : $4497) -> <div,local<$4499>|$4498> $4497(@byref(locloc: local-var<$4499,$4496>),contcont: ($4545) -> <div,local<$4499>|$4498> $4497(xx: $4545)) } )  // restore state early before the resume

pub inline fun local-varstd/core/hnd/local-var: forall<a,b,e,h> (init : a, action : (l : local-var<h,a>) -> <local<h>|e> b) -> <local<h>|e> b(initinit: $4638:aa: V, actionaction: (l : local-var<$4641,$4638>) -> <local<$4641>|$4640> $4639: (l:local-varstd/core/types/local-var: (H, V) -> V<ss: H,aa: V>) -> <localstd/core/types/local: H -> X<ss: H>|std/core/types/effect-extend: (X, E) -> Eee: E> bb: V )result: -> <local<4714>|4713> 4712 : <localstd/core/types/local: H -> X<ss: H>|std/core/types/effect-extend: (X, E) -> Eee: E> bb: V
  pretend-no-divstd/core/undiv/pretend-no-div: (action : () -> <div,local<$4641>|$4640> $4639) -> <local<$4641>|$4640> $4639
    val locloc: local-var<$4641,$4638> : local-varstd/core/types/local-var: (H, V) -> V<__w-l468-c25: H,__w-l468-c27: V> = local-newstd/core/types/local-new: (value : $4638) -> <local<$4641>,div|$4640> local-var<$4641,$4638>(initinit: $4638)
    val resres: $4639 = cast-ev1std/core/hnd/cast-ev1: (f : (local-var<$4641,$4638>) -> <local<$4641>|$4640> $4639) -> <div,local<$4641>|$4640> ((local-var<$4641,$4638>) -> <div,local<$4641>|$4640> $4639)(actionaction: (l : local-var<$4641,$4638>) -> <local<$4641>|$4640> $4639)(@byref(locloc: local-var<$4641,$4638>))
    prompt-local-varstd/core/hnd/prompt-local-var: (loc : local-var<$4641,$4638>, res : $4639) -> <div,local<$4641>|$4640> $4639(@byref(locloc: local-var<$4641,$4638>),resres: $4639)


// -------------------------------------------
// Finally
// -------------------------------------------

pub fun finallystd/core/hnd/finally: forall<a,e> (fin : () -> e (), action : () -> e a) -> e a( finfin: () -> $4846 () : () -> ee: E (std/core/types/unit: V)std/core/types/unit: V, actionaction: () -> $4846 $4845 : () -> ee: E aa: V )result: -> 4866 4865 : ee: E aa: V
  finally-promptstd/core/hnd/finally-prompt: (fin : () -> $4846 (), res : $4845) -> $4846 $4845(finfin: () -> $4846 (), actionaction: () -> $4846 $4845());

fun finally-promptstd/core/hnd/finally-prompt: forall<a,e> (fin : () -> e (), res : a) -> e a(finfin: () -> $4728 () : () -> ee: E (std/core/types/unit: V)std/core/types/unit: V, resres: $4727 : aa: V )result: -> 4838 4837 : ee: E aa: V
  if !std/core/types/bool/(!): (b : bool) -> $4728 boolyieldingstd/core/hnd/yielding: () -> $4728 bool() then
    finfin: () -> $4728 ()()
    resres: $4727
  elif yielding-non-finalstd/core/hnd/yielding-non-final: () -> $4728 bool() then
    yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $4728 $4727, a) -> $4728 $4727) -> $4728 $4727(fnfn: forall<a> (cont : (a) -> $4728 $4727, x : a) -> $4728 $4727(contcont: ($4762) -> $4728 $4727,xx: $4762){ finally-promptstd/core/hnd/finally-prompt: (fin : () -> $4728 (), res : $4727) -> $4728 $4727(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : () -> $4728 ()) -> $4728 (() -> $4728 ())(finfin: () -> $4728 ()),contcont: ($4762) -> $4728 $4727(xx: $4762)) })
  else
    val yldyld: yield-info = yield-capturestd/core/hnd/yield-capture: () -> $4728 yield-info()
    finfin: () -> $4728 ()()
    if yieldingstd/core/hnd/yielding: () -> $4728 bool() returnreturn: $4727 yield-extendstd/core/hnd/yield-extend: (next : (_4802) -> $4728 $4727) -> $4728 $4727( fnfn: (_4802) -> $4728 $4727(_x) unsafe-reyieldstd/core/hnd/unsafe-reyield: (yld : yield-info) -> $4728 $4727(yldyld: yield-info) )std/core/types/Unit: ()
    unsafe-reyieldstd/core/hnd/unsafe-reyield: (yld : yield-info) -> $4728 $4727(yldyld: yield-info)

/*
fun finalize(cont : (() -> b) -> e r, res : a) : e a
  val m : marker<_e,_r> = fresh-marker()
  val w = evv-get()
  prompt(w,w,ev-none(),m,id, yield-bind( cont({ yield-to-final(m,fn(_k) res) }), fn(_x) res ))  // TODO: special prompt that does not insert on resume?
*/

// -------------------------------------------
// Initially
// -------------------------------------------

// add integers
inline extern addstd/core/hnd/add: (i : int, j : int) -> int(i : intstd/core/types/int: V, j : intstd/core/types/int: V) : intstd/core/types/int: V
  c  "kk_integer_add"
  cs inline "(#1 + #2)"
  js inline "(#1 + #2)" // "$std_core_types._int_add"

// are two integers equal?
inline extern eqstd/core/hnd/eq: (x : int, y : int) -> bool( ^x : intstd/core/types/int: V, ^y : intstd/core/types/int: V) : boolstd/core/types/bool: V
  c  "kk_integer_eq_borrow"
  cs inline "(#1 == #2)"
  js inline "(#1 == #2)" // $std_core_types._int_eq"


pub fun initiallystd/core/hnd/initially: forall<a,e> (init : (int) -> e (), action : () -> e a) -> e a(initinit: (int) -> $5058 () : (intstd/core/types/int: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V, actionaction: () -> $5058 $5057 : () -> ee: E aa: V )result: -> 5108 5107 : ee: E aa: V
  initinit: (int) -> $5058 ()(0literal: int
dec = 0
hex8 = 0x00
bit8 = 0b00000000
) if yieldingstd/core/hnd/yielding: () -> $5058 bool() returnreturn: $5057 yield-extendstd/core/hnd/yield-extend: (next : (()) -> $5058 $5057) -> $5058 $5057(fnfn: (()) -> $5058 $5057(_ret:(std/core/types/unit: V)std/core/types/unit: V) initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $5058 (), res : $5057) -> $5058 $5057(initinit: (int) -> $5058 (),actionaction: () -> $5058 $5057()) )std/core/types/Unit: () initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $5058 (), res : $5057) -> $5058 $5057(initinit: (int) -> $5058 (), actionaction: () -> $5058 $5057()
) fun initially-promptstd/core/hnd/initially-prompt: forall<a,e> (init : (int) -> e (), res : a) -> e a( initinit: (int) -> $4874 () : (intstd/core/types/int: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V, resres: $4873 : aa: V )result: -> 5050 5049 : ee: E aa: V if yielding-non-finalstd/core/hnd/yielding-non-final: () -> $4874 bool() then val countcount: ref<global,int> = unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$4874> ref<global,int>) -> $4874 (() -> $4874 ref<global,int>){refstd/core/types/ref: (value : int) -> <alloc<global>,read<global>,write<global>|$4874> ref<global,int>(0literal: int
dec = 0
hex8 = 0x00
bit8 = 0b00000000
)}() yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $4874 $4873, a) -> $4874 $4873) -> $4874 $4873(fnfn: forall<a> (cont : (a) -> $4874 $4873, x : a) -> $4874 $4873(contcont: ($4911) -> $4874 $4873,xx: $4911) val cntcnt: int = unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$4874> int) -> $4874 (() -> $4874 int){ !std/core/types/ref/(!): (ref : ref<global,int>) -> <read<global>,alloc<global>,write<global>|$4874> intcountcount: ref<global,int> }() // increase counter on every resumption unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$4874> ()) -> $4874 (() -> $4874 ()){ countcount: ref<global,int> :=std/core/types/set: (ref : ref<global,int>, assigned : int) -> <write<global>,alloc<global>,read<global>|$4874> () addstd/core/hnd/add: (i : int, j : int) -> <write<global>,alloc<global>,read<global>|$4874> int(cntcnt: int,1literal: int
dec = 1
hex8 = 0x01
bit8 = 0b00000001
) }() if eqstd/core/hnd/eq: (x : int, y : int) -> $4874 bool(cntcnt: int,0literal: int
dec = 0
hex8 = 0x00
bit8 = 0b00000000
) then (std/core/types/Unit: ())std/core/types/Unit: () else // for every resume after the first, run the initializer val rr: () = initinit: (int) -> $4874 ()(cntcnt: int) if yieldingstd/core/hnd/yielding: () -> $4874 bool() then { yield-extendstd/core/hnd/yield-extend: (next : (_4990) -> $4874 $4873) -> $4874 $4873( fnfn: (_4990) -> $4874 $4873(_ret) initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $4874 (), res : $4873) -> $4874 $4873(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : (int) -> $4874 ()) -> $4874 ((int) -> $4874 ())(initinit: (int) -> $4874 ()), contcont: ($4911) -> $4874 $4873(xx: $4911)) ); (std/core/types/Unit: ())std/core/types/Unit: () }std/core/types/Unit: () initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $4874 (), res : $4873) -> $4874 $4873(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : (int) -> $4874 ()) -> $4874 ((int) -> $4874 ())(initinit: (int) -> $4874 ()), contcont: ($4911) -> $4874 $4873(xx: $4911)) ) else resres: $4873
// ------------------------------------------- // Resume context // ------------------------------------------- abstract value struct resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E::E,e0e0: E::E,rr: V>( kresult: -> total (resume-result<2565,2568>) -> 2566 2568 : resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V ) pub fun resumestd/core/hnd/resume: forall<a,e,e1,b> (r : resume-context<a,e,e1,b>, x : a) -> e b( rr: resume-context<$5115,$5116,$5117,$5118> : resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>, xx: $5115 : bb: V )result: -> 5163 5165 : ee: E rr: V (rr: resume-context<$5115,$5116,$5117,$5118>.kstd/core/hnd/resume-context/k: (resume-context<$5115,$5116,$5117,$5118>) -> $5116 ((resume-result<$5115,$5118>) -> $5116 $5118))(Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(xx: $5115)) pub fun resume-shallowstd/core/hnd/resume-shallow: forall<a,e,e1,b> (r : resume-context<a,e,e1,b>, x : a) -> e1 b( rr: resume-context<$5178,$5179,$5180,$5181> : resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>, xx: $5178 : bb: V )result: -> 5242 5243 : e0e0: E rr: V cast-ev1std/core/hnd/cast-ev1: (f : (resume-result<$5178,$5181>) -> $5179 $5181) -> $5180 ((resume-result<$5178,$5181>) -> $5180 $5181)(rr: resume-context<$5178,$5179,$5180,$5181>.kstd/core/hnd/resume-context/k: (resume-context<$5178,$5179,$5180,$5181>) -> $5180 ((resume-result<$5178,$5181>) -> $5179 $5181))(Shallowstd/core/hnd/Shallow: forall<a,b> (result : a) -> resume-result<a,b>(xx: $5178)) pub fun finalizestd/core/hnd/finalize: forall<a,e,e1,b> (r : resume-context<a,e,e1,b>, x : b) -> e b( rr: resume-context<$5256,$5257,$5258,$5259> : resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>, xx: $5259 : rr: V )result: -> 5304 5306 : ee: E rr: V //finalize(r.k,x) (rr: resume-context<$5256,$5257,$5258,$5259>.kstd/core/hnd/resume-context/k: (resume-context<$5256,$5257,$5258,$5259>) -> $5257 ((resume-result<$5256,$5259>) -> $5257 $5259))(Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>(xx: $5259)) // ------------------------------------------- // Clauses // ------------------------------------------- abstract value type clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<aa: V::V,bb: V::V,hh: (E, V) -> V::(E,V)->V,ee: E::E,rr: V::V> Clause1std/core/hnd/Clause1: forall<a,b,c,e,d> (clause : (marker<e,d>, ev<c>, a) -> e b) -> clause1<a,b,c,e,d>( clausestd/core/hnd/clause1/clause: forall<a,b,c,e,d> (clause1 : clause1<a,b,c,e,d>) -> ((marker<e,d>, ev<c>, a) -> e b): (markerstd/core/hnd/marker: (E, V) -> V<ee: E,rr: V>, evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, aa: V) -> ee: E bb: V ) inline extern cast-clause0std/core/hnd/cast-clause0: forall<a,e,e1,b,c> (f : (marker<e1,c>, ev<b>) -> e1 a) -> e ((marker<e1,c>, ev<b>) -> e a)( f : (markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>,evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>) -> e1e1: E bb: V) : ee: E ((markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>,evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>) -> ee: E bb: V) inline "#1" inline extern cast-clause1std/core/hnd/cast-clause1: forall<a,b,e,e1,c,d> (f : (marker<e1,d>, ev<c>, a) -> e1 b) -> e ((marker<e1,d>, ev<c>, a) -> e b)( f : (markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>,evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>,aa: V) -> e1e1: E bb: V) : ee: E ((markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>,evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>,aa: V) -> ee: E bb: V) inline "#1" inline extern cast-clause2std/core/hnd/cast-clause2: forall<a,b,c,e,e1,d,a1> (f : (marker<e1,a1>, ev<d>, a, b) -> e1 c) -> e ((marker<e1,a1>, ev<d>, a, b) -> e c)( f : (markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>,evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>,a1a1: V,a2a2: V) -> e1e1: E bb: V) : ee: E ((markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>,evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>,a1a1: V,a2a2: V) -> ee: E bb: V) inline "#1" pub inline fun @perform1<aa: V,bb: V,hh: (E, V) -> V>( evev: ev<$5321> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($5321<e,a>) -> clause1<$5319,$5320,$5321,e,a> : (forall<e1e1: E,rr: V> hh: (E, V) -> V<e1e1: E,rr: V> -> clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<aa: V,bb: V,hh: (E, V) -> V,e1e1: E,rr: V>), xx: $5319 : aa: V )result: -> 5407 5405 : ee: E bb: V match evev: ev<$5321> Evstd/core/hnd/Ev: forall<a,e,b> (htag : htag<a>, marker : marker<e,b>, hnd : a<e,b>, hevv : evv<e>) -> ev<a>(_tag,mm: marker<$5328,$5329>,hh: $5321<$5328,$5329>,_w) -> match hh: $5321<$5328,$5329>.opop: ($5321<$5328,$5329>) -> $5322 clause1<$5319,$5320,$5321,$5328,$5329> Clause1std/core/hnd/Clause1: forall<a,b,c,e,d> (clause : (marker<e,d>, ev<c>, a) -> e b) -> clause1<a,b,c,e,d>(ff: (marker<$5328,$5329>, ev<$5321>, $5319) -> $5328 $5320) -> cast-clause1std/core/hnd/cast-clause1: (f : (marker<$5328,$5329>, ev<$5321>, $5319) -> $5328 $5320) -> $5322 ((marker<$5328,$5329>, ev<$5321>, $5319) -> $5322 $5320)(ff: (marker<$5328,$5329>, ev<$5321>, $5319) -> $5328 $5320)(mm: marker<$5328,$5329>,evev: ev<$5321>,xx: $5319) fun evv-swap-withstd/core/hnd/evv-swap-with: forall<a,e> (ev : ev<a>) -> evv<e>(evev: ev<$5422> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>)result: -> total evv<5462> match(evev: ev<$5422>) Evstd/core/hnd/Ev: forall<a,e,b> (htag : htag<a>, marker : marker<e,b>, hnd : a<e,b>, hevv : evv<e>) -> ev<a>(_tag,_m,_h,ww: evv<$5428>) -> evv-swapstd/core/hnd/evv-swap: (w : evv<$5428>) -> evv<_5445>(ww: evv<$5428>) inline fun under1std/core/hnd/under1: forall<a,b,e,c> (ev : ev<c>, op : (a) -> e b, x : a) -> e b( evev: ev<$5583> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($5580) -> $5582 $5581 : aa: V -> ee: E bb: V, xx: $5580 : aa: V )result: -> 5676 5675 : ee: E bb: V val w0w0: evv<_5591> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$5583>) -> $5582 evv<_5591>(evev: ev<$5583>) val yy: $5581 = opop: ($5580) -> $5582 $5581(xx: $5580) // evv-set(w0) // only needed before yielding for evidence expected check in prompt if yieldingstd/core/hnd/yielding: () -> $5582 bool() returnreturn: $5581 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5582 $5581, a) -> $5582 $5581) -> $5582 $5581( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($5611) -> $5582 $5581,resres: $5611) under1xstd/core/hnd/under1x: (ev : ev<$5583>, op : ($5611) -> $5582 $5581, x : $5611) -> $5582 $5581(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev<$5583>) -> $5582 ev<$5583>(evev: ev<$5583>),contcont: ($5611) -> $5582 $5581,resres: $5611) )std/core/types/Unit: () evv-setstd/core/hnd/evv-set: (w : evv<_5591>) -> $5582 ()(w0w0: evv<_5591>) yy: $5581 // extra under1x to make under1 inlineable noinline fun under1xstd/core/hnd/under1x: forall<a,b,e,c> (ev : ev<c>, op : (a) -> e b, x : a) -> e b( evev: ev<$5473> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($5470) -> $5472 $5471 : aa: V -> ee: E bb: V, xx: $5470 : aa: V )result: -> 5566 5565 : ee: E bb: V val w0w0: evv<_5481> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$5473>) -> $5472 evv<_5481>(evev: ev<$5473>) val yy: $5471 = opop: ($5470) -> $5472 $5471(xx: $5470) // evv-set(w0) // only needed before yielding for evidence expected check in prompt if yieldingstd/core/hnd/yielding: () -> $5472 bool() returnreturn: $5471 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5472 $5471, a) -> $5472 $5471) -> $5472 $5471( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($5501) -> $5472 $5471,resres: $5501) under1xstd/core/hnd/under1x: (ev : ev<$5473>, op : ($5501) -> $5472 $5471, x : $5501) -> $5472 $5471(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev<$5473>) -> $5472 ev<$5473>(evev: ev<$5473>),contcont: ($5501) -> $5472 $5471,resres: $5501) )std/core/types/Unit: () evv-setstd/core/hnd/evv-set: (w : evv<_5481>) -> $5472 ()(w0w0: evv<_5481>) yy: $5471 pub fun clause-control-raw1std/core/hnd/clause-control-raw1: forall<a,b,e,e1,c,d> (op : (x : a, r : resume-context<b,e,e1,d>) -> e d) -> clause1<a,b,c,e,d>( opop: (x : $5690, r : resume-context<$5691,$5692,$5693,$5695>) -> $5692 $5695 : (x:aa: V, r: resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>) -> ee: E rr: V )result: -> total clause1<5771,5772,5775,5773,5776> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<aa: V,bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause1std/core/hnd/Clause1: forall<a,b,c,e,d> (clause : (marker<e,d>, ev<c>, a) -> e b) -> clause1<a,b,c,e,d>(fnfn: (m : marker<$5692,$5695>, ev<$5694>, x : $5690) -> $5692 $5691(mm: marker<$5692,$5695>,_ev,xx: $5690){ yield-tostd/core/hnd/yield-to: (m : marker<$5692,$5695>, clause : ((resume-result<$5691,$5695>) -> $5692 $5695) -> $5692 $5695) -> $5692 $5691(mm: marker<$5692,$5695>, fnfn: (k : (resume-result<$5691,$5695>) -> $5692 $5695) -> $5692 $5695(kk: (resume-result<$5691,$5695>) -> $5692 $5695){ opop: (x : $5690, r : resume-context<$5691,$5692,$5693,$5695>) -> $5692 $5695(xx: $5690,Resume-contextstd/core/hnd/Resume-context: forall<a,e,e1,b> (k : (resume-result<a,b>) -> e b) -> resume-context<a,e,e1,b>(kk: (resume-result<$5691,$5695>) -> $5692 $5695)) } ) } ) fun getstd/core/hnd/get: forall<a,h> (ref : ref<h,a>) -> <read<h>,div> a( refref: ref<$5797,$5796>: refstd/core/types/ref: (H, V) -> V<hh: H,aa: V>)result: -> <read<5824>,div> 5823 : <std/core/types/total: Ereadstd/core/types/read: H -> X<hh: H>,divstd/core/types/div: X> aa: V !std/core/types/ref/(!): (ref : ref<$5797,$5796>) -> <read<$5797>,div> $5796refref: ref<$5797,$5796> inline extern unsafe-ststd/core/hnd/unsafe-st: forall<a,e> (f : () -> <st<global>|e> a) -> (() -> e a)(f : () -> <ststd/core/types/st: H -> E<globalstd/core/types/global: H>|ee: E> aa: V ) : ((std/core/types/total: E) -> ee: E aa: V) inline "#1" fun protect-promptstd/core/hnd/protect-prompt: forall<a,e,b> (resumed : ref<global,bool>, k : (resume-result<a,b>) -> e b, res : b) -> e b( resumedresumed: ref<global,bool> : refstd/core/types/ref: (H, V) -> V<globalstd/core/types/global: H,boolstd/core/types/bool: V>, kk: (resume-result<$5832,$5834>) -> $5833 $5834 : resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V, resres: $5834 : rr: V )result: -> 6005 6006 : ee: E rr: V val did-resumedid-resume: bool : boolstd/core/types/bool: V = (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$5833> bool) -> $5833 (() -> $5833 bool){ !std/core/types/ref/(!): (ref : ref<global,bool>) -> <read<global>,alloc<global>,write<global>|$5833> boolresumedresumed: ref<global,bool> })() if did-resumedid-resume: bool then // if resumed, we no longer need to protect resres: $5834 elif !std/core/types/bool/(!): (b : bool) -> $5833 boolyieldingstd/core/hnd/yielding: () -> $5833 bool() then // otherwise, if we are not yielding, resume k with finalization (to run all finally clauses) kk: (resume-result<$5832,$5834>) -> $5833 $5834(Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>(resres: $5834)) elif yielding-non-finalstd/core/hnd/yielding-non-final: () -> $5833 bool() then // if we yield non-final to an operation, extend the continuation with this prompt (so we keep protecting after being resumed) yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5833 $5834, a) -> $5833 $5834) -> $5833 $5834( fnfn: forall<a> (cont : (a) -> $5833 $5834, x : a) -> $5833 $5834(contcont: ($5910) -> $5833 $5834,xx: $5910) protect-promptstd/core/hnd/protect-prompt: (resumed : ref<global,bool>, k : (resume-result<$5832,$5834>) -> $5833 $5834, res : $5834) -> $5833 $5834(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ref<global,bool>) -> $5833 ref<global,bool>(resumedresumed: ref<global,bool>),kk: (resume-result<$5832,$5834>) -> $5833 $5834,contcont: ($5910) -> $5833 $5834(xx: $5910)) ) else // if we are in a final yield, capture it, resume k with finalization, and reyield val yldyld: yield-info = yield-capturestd/core/hnd/yield-capture: () -> $5833 yield-info() kk: (resume-result<$5832,$5834>) -> $5833 $5834(Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>(resres: $5834)) if yieldingstd/core/hnd/yielding: () -> $5833 bool() returnreturn: $5834 yield-extendstd/core/hnd/yield-extend: (next : (_5964) -> $5833 $5834) -> $5833 $5834( fnfn: (_5964) -> $5833 $5834(_x) unsafe-reyieldstd/core/hnd/unsafe-reyield: (yld : yield-info) -> $5833 $5834(yldyld: yield-info) )std/core/types/Unit: () // yikes, a finally clause is itself yielding... unsafe-reyieldstd/core/hnd/unsafe-reyield: (yld : yield-info) -> $5833 $5834(yldyld: yield-info) fun protectstd/core/hnd/protect: forall<a,b,e,c> (x : a, clause : (x : a, k : (b) -> e c) -> e c, k : (resume-result<b,c>) -> e c) -> e c( xx: $6016 : aa: V, clauseclause: (x : $6016, k : ($6017) -> $6018 $6019) -> $6018 $6019 : (x:aa: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V, kk: (resume-result<$6017,$6019>) -> $6018 $6019 : resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V )result: -> 6115 6116 : ee: E rr: V val resumedresumed: ref<global,bool> = (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$6018> ref<global,bool>) -> $6018 (() -> $6018 ref<global,bool>){refstd/core/types/ref: (value : bool) -> <alloc<global>,read<global>,write<global>|$6018> ref<global,bool>(Falsestd/core/types/False: bool)})() fun kprotectkprotect: (ret : $6017) -> $6018 $6019(retret: $6017)result: -> $6018 $6019 (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$6018> ()) -> $6018 (() -> $6018 ()){resumedresumed: ref<global,bool> :=std/core/types/set: (ref : ref<global,bool>, assigned : bool) -> <write<global>,alloc<global>,read<global>|$6018> () Truestd/core/types/True: bool})() kk: (resume-result<$6017,$6019>) -> $6018 $6019(Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(retret: $6017)) val resres: $6019 = clauseclause: (x : $6016, k : ($6017) -> $6018 $6019) -> $6018 $6019(xx: $6016,kprotectkprotect: (ret : $6017) -> $6018 $6019) protect-promptstd/core/hnd/protect-prompt: (resumed : ref<global,bool>, k : (resume-result<$6017,$6019>) -> $6018 $6019, res : $6019) -> $6018 $6019(resumedresumed: ref<global,bool>,kk: (resume-result<$6017,$6019>) -> $6018 $6019,resres: $6019) /* pub fun clause-control1( clause : (x:a, k: b -> e r) -> e r ) : clause1<a,b,e,r> Clause1(fn(m,w,x){ yield-to(m, fn(k){ clause(x, fn(r){ k({r}) } ) }) }) */ // generic control clause pub fun clause-control1std/core/hnd/clause-control1: forall<a,b,e,c,d> (clause : (x : a, k : (b) -> e d) -> e d) -> clause1<a,b,c,e,d>( clauseclause: (x : $6129, k : ($6130) -> $6131 $6133) -> $6131 $6133 : (x:aa: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause1<6203,6204,6206,6205,6207> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<aa: V,bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause1std/core/hnd/Clause1: forall<a,b,c,e,d> (clause : (marker<e,d>, ev<c>, a) -> e b) -> clause1<a,b,c,e,d>(fnfn: (m : marker<$6131,$6133>, ev<$6132>, x : $6129) -> $6131 $6130(mm: marker<$6131,$6133>,_ev,xx: $6129){ yield-tostd/core/hnd/yield-to: (m : marker<$6131,$6133>, clause : ((resume-result<$6130,$6133>) -> $6131 $6133) -> $6131 $6133) -> $6131 $6130(mm: marker<$6131,$6133>, fnfn: (k : (resume-result<$6130,$6133>) -> $6131 $6133) -> $6131 $6133(kk: (resume-result<$6130,$6133>) -> $6131 $6133) protectstd/core/hnd/protect: (x : $6129, clause : (x : $6129, k : ($6130) -> $6131 $6133) -> $6131 $6133, k : (resume-result<$6130,$6133>) -> $6131 $6133) -> $6131 $6133(xx: $6129,clauseclause: (x : $6129, k : ($6130) -> $6131 $6133) -> $6131 $6133,kk: (resume-result<$6130,$6133>) -> $6131 $6133) ) }) // tail-resumptive clause: resumes exactly once at the end // (these can be executed 'in-place' without capturing a resumption) pub fun clause-tail1std/core/hnd/clause-tail1: forall<e,a,b,c,d> (op : (c) -> e d) -> clause1<c,d,b,e,a><ee: E,rr: V,hh: (E, V) -> V,aa: V,bb: V>(opop: ($6227) -> $6224 $6228 : aa: V -> ee: E bb: V)result: -> total clause1<6289,6290,6288,6286,6287> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<aa: V,bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause1std/core/hnd/Clause1: forall<a,b,c,e,d> (clause : (marker<e,d>, ev<c>, a) -> e b) -> clause1<a,b,c,e,d>(fnfn: (marker<$6224,$6225>, ev : ev<$6226>, x : $6227) -> $6224 $6228(_m,evev: ev<$6226>,xx: $6227){ under1std/core/hnd/under1: (ev : ev<$6226>, op : ($6227) -> $6224 $6228, x : $6227) -> $6224 $6228(evev: ev<$6226>,opop: ($6227) -> $6224 $6228,xx: $6227) }) // tail-resumptive clause that does not itself invoke operations // (these can be executed 'in-place' without setting the correct evidence vector) pub fun clause-tail-noop1std/core/hnd/clause-tail-noop1: forall<e,a,b,c,d> (op : (c) -> e d) -> clause1<c,d,b,e,a><ee: E,rr: V,hh: (E, V) -> V,aa: V,bb: V>(opop: ($6310) -> $6307 $6311 : aa: V -> ee: E bb: V)result: -> total clause1<6358,6359,6357,6355,6356> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<aa: V,bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause1std/core/hnd/Clause1: forall<a,b,c,e,d> (clause : (marker<e,d>, ev<c>, a) -> e b) -> clause1<a,b,c,e,d>(fnfn: (marker<$6307,$6308>, ev<$6309>, x : $6310) -> $6307 $6311(_m,_ev,xx: $6310){ opop: ($6310) -> $6307 $6311(xx: $6310) }) // clause that never resumes (e.g. an exception handler) // (these do not need to capture a resumption and execute finally clauses upfront) pub fun clause-never1std/core/hnd/clause-never1: forall<a,b,e,c,d> (op : (a) -> e d) -> clause1<a,b,c,e,d>( opop: ($6376) -> $6378 $6380 : aa: V -> ee: E rr: V )result: -> total clause1<6439,6440,6442,6441,6443> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<aa: V,bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause1std/core/hnd/Clause1: forall<a,b,c,e,d> (clause : (marker<e,d>, ev<c>, a) -> e b) -> clause1<a,b,c,e,d>(fnfn: (m : marker<$6378,$6380>, ev<$6379>, x : $6376) -> $6378 $6377(mm: marker<$6378,$6380>,_ev,xx: $6376){ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$6378,$6380>, clause : ((resume-result<$6377,$6380>) -> $6378 $6380) -> $6378 $6380) -> $6378 $6377(mm: marker<$6378,$6380>, fnfn: ((resume-result<$6377,$6380>) -> $6378 $6380) -> $6378 $6380(_k) opop: ($6376) -> $6378 $6380(xx: $6376) ) }) //---------------------------------------------------------------- // 0 arguments; reuse 1 argument Clauses //---------------------------------------------------------------- abstract value type clause0std/core/hnd/clause0: (V, (E, V) -> V, E, V) -> V<bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause0std/core/hnd/Clause0: forall<a,b,e,c> (clause : (marker<e,c>, ev<b>) -> e a) -> clause0<a,b,e,c>( clausestd/core/hnd/clause0/clause: forall<a,b,e,c> (clause0 : clause0<a,b,e,c>) -> ((marker<e,c>, ev<b>) -> e a): (markerstd/core/hnd/marker: (E, V) -> V<ee: E,rr: V>, evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>) -> ee: E bb: V ) //inline extern cast-hnd( h : h<e1,r> ) : e h<e,r> { inline "#1"//inline extern cast-marker( m : marker<e1,r> ) : e marker<e,r> { inline "#1" pub inline fun @perform0( evev: ev<$6462> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($6462<e,a>) -> clause0<$6460,$6462,e,a> : (forall<e1e1: E,rr: V> hh: (E, V) -> V<e1e1: E,rr: V> -> clause0std/core/hnd/clause0: (V, (E, V) -> V, E, V) -> V<bb: V,hh: (E, V) -> V,e1e1: E,rr: V>) )result: -> 6535 6534 : ee: E bb: V match evev: ev<$6462> Evstd/core/hnd/Ev: forall<a,e,b> (htag : htag<a>, marker : marker<e,b>, hnd : a<e,b>, hevv : evv<e>) -> ev<a>(_tag,mm: marker<$6468,$6469>,hh: $6462<$6468,$6469>,_w) -> match hh: $6462<$6468,$6469>.opop: ($6462<$6468,$6469>) -> $6461 clause0<$6460,$6462,$6468,$6469> Clause0std/core/hnd/Clause0: forall<a,b,e,c> (clause : (marker<e,c>, ev<b>) -> e a) -> clause0<a,b,e,c>(ff: (marker<$6468,$6469>, ev<$6462>) -> $6468 $6460) -> cast-clause0std/core/hnd/cast-clause0: (f : (marker<$6468,$6469>, ev<$6462>) -> $6468 $6460) -> $6461 ((marker<$6468,$6469>, ev<$6462>) -> $6461 $6460)(ff: (marker<$6468,$6469>, ev<$6462>) -> $6468 $6460)(mm: marker<$6468,$6469>,evev: ev<$6462>) inline fun under0std/core/hnd/under0: forall<a,e,b> (ev : ev<b>, op : () -> e a) -> e a( evev: ev<$6550> : evstd/core/hnd/ev: ((E, V) -> V) -> V<ii: (E, V) -> V>, opop: () -> $6549 $6548 : () -> ee: E bb: V)result: -> 6631 6630 : ee: E bb: V val w0w0: evv<_6558> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$6550>) -> $6549 evv<_6558>(evev: ev<$6550>) val yy: $6548 = opop: () -> $6549 $6548() // evv-set(w0) // only needed before yielding for evidence expected check in prompt evv-setstd/core/hnd/evv-set: (w : evv<_6558>) -> $6549 ()(w0w0: evv<_6558>) if yieldingstd/core/hnd/yielding: () -> $6549 bool() returnreturn: $6548 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $6549 $6548, a) -> $6549 $6548) -> $6549 $6548( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($6585) -> $6549 $6548,resres: $6585) under1std/core/hnd/under1: (ev : ev<$6550>, op : ($6585) -> $6549 $6548, x : $6585) -> $6549 $6548(evev: ev<$6550>,contcont: ($6585) -> $6549 $6548,resres: $6585) )std/core/types/Unit: () yy: $6548 pub fun clause-control-raw0std/core/hnd/clause-control-raw0: forall<a,e,e1,b,c> (op : (resume-context<a,e,e1,c>) -> e c) -> clause0<a,b,e,c>( opop: (resume-context<$6642,$6643,$6644,$6646>) -> $6643 $6646 : resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V> -> ee: E rr: V )result: -> total clause0<6714,6717,6715,6718> : clause0std/core/hnd/clause0: (V, (E, V) -> V, E, V) -> V<bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause0std/core/hnd/Clause0: forall<a,b,e,c> (clause : (marker<e,c>, ev<b>) -> e a) -> clause0<a,b,e,c>(fnfn: (m : marker<$6643,$6646>, ev<$6645>) -> $6643 $6642(mm: marker<$6643,$6646>,_ev){ yield-tostd/core/hnd/yield-to: (m : marker<$6643,$6646>, clause : ((resume-result<$6642,$6646>) -> $6643 $6646) -> $6643 $6646) -> $6643 $6642(mm: marker<$6643,$6646>, fnfn: (k : (resume-result<$6642,$6646>) -> $6643 $6646) -> $6643 $6646(kk: (resume-result<$6642,$6646>) -> $6643 $6646){ opop: (resume-context<$6642,$6643,$6644,$6646>) -> $6643 $6646(Resume-contextstd/core/hnd/Resume-context: forall<a,e,e1,b> (k : (resume-result<a,b>) -> e b) -> resume-context<a,e,e1,b>(kk: (resume-result<$6642,$6646>) -> $6643 $6646)) } ) }) /* pub fun clause-control0( op : (b -> e r) -> e r ) : clause0<b,e,r> Clause0(fn(m,w){ yield-to(m, fn(k){ op(fn(r){ k({r} )}) }) }) */ pub fun clause-control0std/core/hnd/clause-control0: forall<a,e,b,c> (op : ((a) -> e c) -> e c) -> clause0<a,b,e,c>( opop: (($6735) -> $6736 $6738) -> $6736 $6738 : (bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause0<6803,6805,6804,6806> : clause0std/core/hnd/clause0: (V, (E, V) -> V, E, V) -> V<bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause0std/core/hnd/Clause0: forall<a,b,e,c> (clause : (marker<e,c>, ev<b>) -> e a) -> clause0<a,b,e,c>(fnfn: (m : marker<$6736,$6738>, ev<$6737>) -> $6736 $6735(mm: marker<$6736,$6738>,_ev){ yield-tostd/core/hnd/yield-to: (m : marker<$6736,$6738>, clause : ((resume-result<$6735,$6738>) -> $6736 $6738) -> $6736 $6738) -> $6736 $6735(mm: marker<$6736,$6738>, fnfn: (k : (resume-result<$6735,$6738>) -> $6736 $6738) -> $6736 $6738(kk: (resume-result<$6735,$6738>) -> $6736 $6738){ protectstd/core/hnd/protect: (x : (), clause : (x : (), k : ($6735) -> $6736 $6738) -> $6736 $6738, k : (resume-result<$6735,$6738>) -> $6736 $6738) -> $6736 $6738((std/core/types/Unit: ())std/core/types/Unit: (),fnfn: ((), r : ($6735) -> $6736 $6738) -> $6736 $6738(_x,rr: ($6735) -> $6736 $6738){ opop: (($6735) -> $6736 $6738) -> $6736 $6738(rr: ($6735) -> $6736 $6738) }, kk: (resume-result<$6735,$6738>) -> $6736 $6738) }) }) pub fun clause-tail0std/core/hnd/clause-tail0: forall<e,a,b,c> (op : () -> e c) -> clause0<c,b,e,a><ee: E,rr: V,hh: (E, V) -> V,bb: V>(opop: () -> $6820 $6823 : () -> ee: E bb: V)result: -> total clause0<6873,6872,6870,6871> : clause0std/core/hnd/clause0: (V, (E, V) -> V, E, V) -> V<bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause0std/core/hnd/Clause0: forall<a,b,e,c> (clause : (marker<e,c>, ev<b>) -> e a) -> clause0<a,b,e,c>(fnfn: (marker<$6820,$6821>, ev : ev<$6822>) -> $6820 $6823(_m,evev: ev<$6822>){ under0std/core/hnd/under0: (ev : ev<$6822>, op : () -> $6820 $6823) -> $6820 $6823(evev: ev<$6822>,opop: () -> $6820 $6823) }) pub fun clause-tail-noop0std/core/hnd/clause-tail-noop0: forall<e,a,b,c> (op : () -> e c) -> clause0<c,b,e,a><ee: E,rr: V,hh: (E, V) -> V,bb: V>(opop: () -> $6887 $6890 : () -> ee: E bb: V)result: -> total clause0<6929,6928,6926,6927> : clause0std/core/hnd/clause0: (V, (E, V) -> V, E, V) -> V<bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause0std/core/hnd/Clause0: forall<a,b,e,c> (clause : (marker<e,c>, ev<b>) -> e a) -> clause0<a,b,e,c>(fnfn: (marker<$6887,$6888>, ev<$6889>) -> $6887 $6890(_m,_ev){ opop: () -> $6887 $6890() }) pub fun clause-valuestd/core/hnd/clause-value: forall<a,e,b,c> (v : a) -> clause0<a,b,e,c>(vv: $6943 : bb: V)result: -> total clause0<6982,6984,6983,6985> : clause0std/core/hnd/clause0: (V, (E, V) -> V, E, V) -> V<bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause0std/core/hnd/Clause0: forall<a,b,e,c> (clause : (marker<e,c>, ev<b>) -> e a) -> clause0<a,b,e,c>(fnfn: (marker<$6944,$6946>, ev<$6945>) -> $6944 $6943(_m,_ev){ vv: $6943 }) pub fun clause-never0std/core/hnd/clause-never0: forall<a,e,b,c> (op : () -> e c) -> clause0<a,b,e,c>( opop: () -> $7000 $7002 : () -> ee: E rr: V )result: -> total clause0<7053,7055,7054,7056> : clause0std/core/hnd/clause0: (V, (E, V) -> V, E, V) -> V<bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause0std/core/hnd/Clause0: forall<a,b,e,c> (clause : (marker<e,c>, ev<b>) -> e a) -> clause0<a,b,e,c>(fnfn: (m : marker<$7000,$7002>, ev<$7001>) -> $7000 $6999(mm: marker<$7000,$7002>,_ev){ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$7000,$7002>, clause : ((resume-result<$6999,$7002>) -> $7000 $7002) -> $7000 $7002) -> $7000 $6999(mm: marker<$7000,$7002>, fnfn: ((resume-result<$6999,$7002>) -> $7000 $7002) -> $7000 $7002(_k){ opop: () -> $7000 $7002() }) }) //---------------------------------------------------------------- // 2 arguments //---------------------------------------------------------------- abstract value type clause2std/core/hnd/clause2: (V, V, V, (E, V) -> V, E, V) -> V<a1a1: V,a2a2: V,bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause2std/core/hnd/Clause2: forall<a,b,c,d,e,a1> (clause : (marker<e,a1>, ev<d>, a, b) -> e c) -> clause2<a,b,c,d,e,a1>( clausestd/core/hnd/clause2/clause: forall<a,b,c,d,e,a1> (clause2 : clause2<a,b,c,d,e,a1>) -> ((marker<e,a1>, ev<d>, a, b) -> e c): (markerstd/core/hnd/marker: (E, V) -> V<ee: E,rr: V>, evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, a1a1: V, a2a2: V) -> ee: E bb: V ) fun under2std/core/hnd/under2: forall<a,b,c,e,d> (ev : ev<d>, op : (a, b) -> e c, x1 : a, x2 : b) -> e c( evev: ev<$7074> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($7070, $7071) -> $7073 $7072 : (a1a1: V,a2a2: V) -> ee: E bb: V, x1x1: $7070 : a1a1: V, x2x2: $7071 : a2a2: V )result: -> 7167 7166 : ee: E bb: V val w0w0: evv<_7082> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$7074>) -> $7073 evv<_7082>(evev: ev<$7074>) val zz: $7072 = opop: ($7070, $7071) -> $7073 $7072(x1x1: $7070,x2x2: $7071) evv-setstd/core/hnd/evv-set: (w : evv<_7082>) -> $7073 ()(w0w0: evv<_7082>) if yieldingstd/core/hnd/yielding: () -> $7073 bool() returnreturn: $7072 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $7073 $7072, a) -> $7073 $7072) -> $7073 $7072( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($7111) -> $7073 $7072,resres: $7111) under1std/core/hnd/under1: (ev : ev<$7074>, op : ($7111) -> $7073 $7072, x : $7111) -> $7073 $7072(evev: ev<$7074>,contcont: ($7111) -> $7073 $7072,resres: $7111) )std/core/types/Unit: () zz: $7072 fun protect2std/core/hnd/protect2: forall<a,b,c,e,d> (x1 : a, x2 : b, clause : (x : a, x : b, k : (c) -> e d) -> e d, k : (resume-result<c,d>) -> e d) -> e d( x1x1: $7184 : a1a1: V, x2x2: $7185:a2a2: V, clauseclause: (x : $7184, x : $7185, k : ($7186) -> $7187 $7188) -> $7187 $7188 : (x:a1a1: V,x:a2a2: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V, kk: (resume-result<$7186,$7188>) -> $7187 $7188 : resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V )result: -> 7290 7291 : ee: E rr: V val resumedresumed: ref<global,bool> = (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$7187> ref<global,bool>) -> $7187 (() -> $7187 ref<global,bool>){refstd/core/types/ref: (value : bool) -> <alloc<global>,read<global>,write<global>|$7187> ref<global,bool>(Falsestd/core/types/False: bool)})() fun kprotectkprotect: (ret : $7186) -> $7187 $7188(retret: $7186)result: -> $7187 $7188 (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$7187> ()) -> $7187 (() -> $7187 ()){ resumedresumed: ref<global,bool> :=std/core/types/set: (ref : ref<global,bool>, assigned : bool) -> <write<global>,alloc<global>,read<global>|$7187> () Truestd/core/types/True: bool })() kk: (resume-result<$7186,$7188>) -> $7187 $7188(Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(retret: $7186)) val resres: $7188 = clauseclause: (x : $7184, x : $7185, k : ($7186) -> $7187 $7188) -> $7187 $7188(x1x1: $7184,x2x2: $7185,kprotectkprotect: (ret : $7186) -> $7187 $7188) protect-promptstd/core/hnd/protect-prompt: (resumed : ref<global,bool>, k : (resume-result<$7186,$7188>) -> $7187 $7188, res : $7188) -> $7187 $7188(resumedresumed: ref<global,bool>,kk: (resume-result<$7186,$7188>) -> $7187 $7188,resres: $7188) pub fun clause-control2std/core/hnd/clause-control2: forall<a,b,c,e,d,a1> (clause : (x1 : a, x2 : b, k : (c) -> e a1) -> e a1) -> clause2<a,b,c,d,e,a1>( clauseclause: (x1 : $7307, x2 : $7308, k : ($7309) -> $7310 $7312) -> $7310 $7312 : (x1:a1a1: V, x2:a2a2: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause2<7393,7394,7395,7397,7396,7398> : clause2std/core/hnd/clause2: (V, V, V, (E, V) -> V, E, V) -> V<a1a1: V,a2a2: V,bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause2std/core/hnd/Clause2: forall<a,b,c,d,e,a1> (clause : (marker<e,a1>, ev<d>, a, b) -> e c) -> clause2<a,b,c,d,e,a1>(fnfn: (m : marker<$7310,$7312>, ev<$7311>, x1 : $7307, x2 : $7308) -> $7310 $7309(mm: marker<$7310,$7312>,_ev,x1x1: $7307,x2x2: $7308){ yield-tostd/core/hnd/yield-to: (m : marker<$7310,$7312>, clause : ((resume-result<$7309,$7312>) -> $7310 $7312) -> $7310 $7312) -> $7310 $7309(mm: marker<$7310,$7312>, fnfn: (k : (resume-result<$7309,$7312>) -> $7310 $7312) -> $7310 $7312(kk: (resume-result<$7309,$7312>) -> $7310 $7312){ protect2std/core/hnd/protect2: (x1 : $7307, x2 : $7308, clause : (x : $7307, x : $7308, k : ($7309) -> $7310 $7312) -> $7310 $7312, k : (resume-result<$7309,$7312>) -> $7310 $7312) -> $7310 $7312(x1x1: $7307,x2x2: $7308,clauseclause: (x1 : $7307, x2 : $7308, k : ($7309) -> $7310 $7312) -> $7310 $7312,kk: (resume-result<$7309,$7312>) -> $7310 $7312) }) }) pub fun clause-control-raw2std/core/hnd/clause-control-raw2: forall<a,b,c,e,e1,d,a1> (op : (x1 : a, x2 : b, r : resume-context<c,e,e1,a1>) -> e a1) -> clause2<a,b,c,d,e,a1>( opop: (x1 : $7418, x2 : $7419, r : resume-context<$7420,$7421,$7422,$7424>) -> $7421 $7424 : (x1:a1a1: V, x2:a2a2: V, r: resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>) -> ee: E rr: V )result: -> total clause2<7508,7509,7510,7513,7511,7514> : clause2std/core/hnd/clause2: (V, V, V, (E, V) -> V, E, V) -> V<a1a1: V,a2a2: V,bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause2std/core/hnd/Clause2: forall<a,b,c,d,e,a1> (clause : (marker<e,a1>, ev<d>, a, b) -> e c) -> clause2<a,b,c,d,e,a1>(fnfn: (m : marker<$7421,$7424>, ev<$7423>, x1 : $7418, x2 : $7419) -> $7421 $7420(mm: marker<$7421,$7424>,_ev,x1x1: $7418,x2x2: $7419){ yield-tostd/core/hnd/yield-to: (m : marker<$7421,$7424>, clause : ((resume-result<$7420,$7424>) -> $7421 $7424) -> $7421 $7424) -> $7421 $7420(mm: marker<$7421,$7424>, fnfn: (k : (resume-result<$7420,$7424>) -> $7421 $7424) -> $7421 $7424(kk: (resume-result<$7420,$7424>) -> $7421 $7424){ opop: (x1 : $7418, x2 : $7419, r : resume-context<$7420,$7421,$7422,$7424>) -> $7421 $7424(x1x1: $7418,x2x2: $7419,Resume-contextstd/core/hnd/Resume-context: forall<a,e,e1,b> (k : (resume-result<a,b>) -> e b) -> resume-context<a,e,e1,b>(kk: (resume-result<$7420,$7424>) -> $7421 $7424)) } ) }) pub fun clause-tail2std/core/hnd/clause-tail2: forall<e,a,b,c,d,a1> (op : (c, d) -> e a1) -> clause2<c,d,a1,b,e,a><ee: E,rr: V,hh: (E, V) -> V,a1a1: V,a2a2: V,bb: V>(opop: ($7540, $7541) -> $7537 $7542 : (a1a1: V,a2a2: V) -> ee: E bb: V)result: -> total clause2<7614,7615,7616,7613,7611,7612> : clause2std/core/hnd/clause2: (V, V, V, (E, V) -> V, E, V) -> V<a1a1: V,a2a2: V,bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause2std/core/hnd/Clause2: forall<a,b,c,d,e,a1> (clause : (marker<e,a1>, ev<d>, a, b) -> e c) -> clause2<a,b,c,d,e,a1>(fnfn: (m : marker<$7537,$7538>, ev : ev<$7539>, x1 : $7540, x2 : $7541) -> $7537 $7542(mm: marker<$7537,$7538>,evev: ev<$7539>,x1x1: $7540,x2x2: $7541){ under2std/core/hnd/under2: (ev : ev<$7539>, op : ($7540, $7541) -> $7537 $7542, x1 : $7540, x2 : $7541) -> $7537 $7542(evev: ev<$7539>,opop: ($7540, $7541) -> $7537 $7542,x1x1: $7540,x2x2: $7541) }) pub fun clause-tail-noop2std/core/hnd/clause-tail-noop2: forall<e,a,b,c,d,a1> (op : (c, d) -> e a1) -> clause2<c,d,a1,b,e,a><ee: E,rr: V,hh: (E, V) -> V,a1a1: V,a2a2: V,bb: V>(opop: ($7639, $7640) -> $7636 $7641 : (a1a1: V,a2a2: V) -> ee: E bb: V)result: -> total clause2<7696,7697,7698,7695,7693,7694> : clause2std/core/hnd/clause2: (V, V, V, (E, V) -> V, E, V) -> V<a1a1: V,a2a2: V,bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause2std/core/hnd/Clause2: forall<a,b,c,d,e,a1> (clause : (marker<e,a1>, ev<d>, a, b) -> e c) -> clause2<a,b,c,d,e,a1>(fnfn: (marker<$7636,$7637>, ev<$7638>, x1 : $7639, x2 : $7640) -> $7636 $7641(_m,_ev,x1x1: $7639,x2x2: $7640){ opop: ($7639, $7640) -> $7636 $7641(x1x1: $7639,x2x2: $7640) }) pub inline fun @perform2( evxevx: ev<$7722> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($7722<e,a>) -> clause2<$7718,$7719,$7720,$7722,e,a> : (forall<e1e1: E,rr: V> hh: (E, V) -> V<e1e1: E,rr: V> -> clause2std/core/hnd/clause2: (V, V, V, (E, V) -> V, E, V) -> V<aa: V,bb: V,cc: V,hh: (E, V) -> V,e1e1: E,rr: V>), xx: $7718 : aa: V, yy: $7719 : bb: V )result: -> 7817 7816 : ee: E cc: V match evxevx: ev<$7722> Evstd/core/hnd/Ev: forall<a,e,b> (htag : htag<a>, marker : marker<e,b>, hnd : a<e,b>, hevv : evv<e>) -> ev<a>(_tag,mm: marker<$7728,$7729>,hh: $7722<$7728,$7729>,_w) -> match hh: $7722<$7728,$7729>.opop: ($7722<$7728,$7729>) -> $7721 clause2<$7718,$7719,$7720,$7722,$7728,$7729> Clause2std/core/hnd/Clause2: forall<a,b,c,d,e,a1> (clause : (marker<e,a1>, ev<d>, a, b) -> e c) -> clause2<a,b,c,d,e,a1>(ff: (marker<$7728,$7729>, ev<$7722>, $7718, $7719) -> $7728 $7720) -> cast-clause2std/core/hnd/cast-clause2: (f : (marker<$7728,$7729>, ev<$7722>, $7718, $7719) -> $7728 $7720) -> $7721 ((marker<$7728,$7729>, ev<$7722>, $7718, $7719) -> $7721 $7720)(ff: (marker<$7728,$7729>, ev<$7722>, $7718, $7719) -> $7728 $7720)(mm: marker<$7728,$7729>,evxevx: ev<$7722>,xx: $7718,yy: $7719) pub fun clause-never2std/core/hnd/clause-never2: forall<a,b,c,e,d,a1> (op : (a, b) -> e a1) -> clause2<a,b,c,d,e,a1>( opop: ($7836, $7837) -> $7839 $7841 : (a1a1: V,a2a2: V) -> ee: E rr: V )result: -> total clause2<7908,7909,7910,7912,7911,7913> : clause2std/core/hnd/clause2: (V, V, V, (E, V) -> V, E, V) -> V<a1a1: V,a2a2: V,bb: V,hh: (E, V) -> V,ee: E,rr: V> Clause2std/core/hnd/Clause2: forall<a,b,c,d,e,a1> (clause : (marker<e,a1>, ev<d>, a, b) -> e c) -> clause2<a,b,c,d,e,a1>(fnfn: (m : marker<$7839,$7841>, ev<$7840>, x1 : $7836, x2 : $7837) -> $7839 $7838(mm: marker<$7839,$7841>,_ev,x1x1: $7836,x2x2: $7837){ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$7839,$7841>, clause : ((resume-result<$7838,$7841>) -> $7839 $7841) -> $7839 $7841) -> $7839 $7838(mm: marker<$7839,$7841>, fnfn: ((resume-result<$7838,$7841>) -> $7839 $7841) -> $7839 $7841(_k){ opop: ($7836, $7837) -> $7839 $7841(x1x1: $7836,x2x2: $7837) }) }) //---------------------------------------------------------------- // 3 arguments: reuse 1 argument clause. // Or should the compiler do tupling/untupling? //---------------------------------------------------------------- // For interal use fun xperform1std/core/hnd/xperform1: forall<a,b,e,c> (ev : ev<c>, op : forall<e1,d> (c<e1,d>) -> clause1<a,b,c,e1,d>, x : a) -> e b( evev: ev<$7936> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($7936<e,a>) -> clause1<$7933,$7934,$7936,e,a> : (forall<e1e1: E,rr: V> hh: (E, V) -> V<e1e1: E,rr: V> -> clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<aa: V,bb: V,hh: (E, V) -> V,e1e1: E,rr: V>), xx: $7933 : aa: V )result: -> 8020 8019 : ee: E bb: V match evev: ev<$7936> Evstd/core/hnd/Ev: forall<a,e,b> (htag : htag<a>, marker : marker<e,b>, hnd : a<e,b>, hevv : evv<e>) -> ev<a>(_tag,mm: marker<$7942,$7943>,hh: $7936<$7942,$7943>,_w) -> match hh: $7936<$7942,$7943>.opop: ($7936<$7942,$7943>) -> $7935 clause1<$7933,$7934,$7936,$7942,$7943> Clause1std/core/hnd/Clause1: forall<a,b,c,e,d> (clause : (marker<e,d>, ev<c>, a) -> e b) -> clause1<a,b,c,e,d>(ff: (marker<$7942,$7943>, ev<$7936>, $7933) -> $7942 $7934) -> cast-clause1std/core/hnd/cast-clause1: (f : (marker<$7942,$7943>, ev<$7936>, $7933) -> $7942 $7934) -> $7935 ((marker<$7942,$7943>, ev<$7936>, $7933) -> $7935 $7934)(ff: (marker<$7942,$7943>, ev<$7936>, $7933) -> $7942 $7934)(mm: marker<$7942,$7943>,evev: ev<$7936>,xx: $7933) pub fun clause-control-raw3std/core/hnd/clause-control-raw3: forall<a,b,c,d,e,e1,a1,b1> (op : (x1 : a, x2 : b, x3 : c, r : resume-context<d,e,e1,b1>) -> e b1) -> clause1<(a, b, c),d,a1,e,b1>( opop: (x1 : $8036, x2 : $8037, x3 : $8038, r : resume-context<$8039,$8040,$8041,$8043>) -> $8040 $8043 : (x1:a1a1: V, x2:a2a2: V, x3:a3a3: V, r: resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>) -> ee: E rr: V )result: -> total clause1<(8115, 8116, 8117),8118,8121,8119,8122> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(std/core/types/tuple3: (V, V, V) -> Va1a1: V,a2a2: V,a3a3: V),bb: V,hh: (E, V) -> V,ee: E,rr: V> clause-control-raw1std/core/hnd/clause-control-raw1: (op : (x : ($8036, $8037, $8038), r : resume-context<$8039,$8040,$8041,$8043>) -> $8040 $8043) -> clause1<($8036, $8037, $8038),$8039,$8042,$8040,$8043>( fnfn: (($8036, $8037, $8038), r : resume-context<$8039,$8040,$8041,$8043>) -> $8040 $8043((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8036,x2x2: $8037,x3x3: $8038)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c),rr: resume-context<$8039,$8040,$8041,$8043>){ opop: (x1 : $8036, x2 : $8037, x3 : $8038, r : resume-context<$8039,$8040,$8041,$8043>) -> $8040 $8043(x1x1: $8036,x2x2: $8037,x3x3: $8038,rr: resume-context<$8039,$8040,$8041,$8043>) } ) pub fun clause-control3std/core/hnd/clause-control3: forall<a,b,c,d,e,a1,b1> (op : (x1 : a, x2 : b, x3 : c, k : (d) -> e b1) -> e b1) -> clause1<(a, b, c),d,a1,e,b1>( opop: (x1 : $8148, x2 : $8149, x3 : $8150, k : ($8151) -> $8152 $8154) -> $8152 $8154 : (x1:a1a1: V, x2:a2a2: V, x3:a3a3: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause1<(8219, 8220, 8221),8222,8224,8223,8225> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(std/core/types/tuple3: (V, V, V) -> Va1a1: V,a2a2: V,a3a3: V),bb: V,hh: (E, V) -> V,ee: E,rr: V> clause-control1std/core/hnd/clause-control1: (clause : (x : ($8148, $8149, $8150), k : ($8151) -> $8152 $8154) -> $8152 $8154) -> clause1<($8148, $8149, $8150),$8151,$8153,$8152,$8154>( fnfn: (($8148, $8149, $8150), k : ($8151) -> $8152 $8154) -> $8152 $8154((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8148,x2x2: $8149,x3x3: $8150)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c),kk: ($8151) -> $8152 $8154){ opop: (x1 : $8148, x2 : $8149, x3 : $8150, k : ($8151) -> $8152 $8154) -> $8152 $8154(x1x1: $8148,x2x2: $8149,x3x3: $8150,kk: ($8151) -> $8152 $8154) } ) pub fun clause-tail3std/core/hnd/clause-tail3: forall<e,a,b,c,d,a1,b1> (op : (c, d, a1) -> e b1) -> clause1<(c, d, a1),b1,b,e,a><ee: E,rr: V,hh: (E, V) -> V,a1a1: V,a2a2: V,a3a3: V,bb: V>(opop: ($8251, $8252, $8253) -> $8248 $8254 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E bb: V)result: -> total clause1<(8321, 8322, 8323),8324,8320,8318,8319> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(std/core/types/tuple3: (V, V, V) -> Va1a1: V,a2a2: V,a3a3: V),bb: V,hh: (E, V) -> V,ee: E,rr: V> clause-tail1std/core/hnd/clause-tail1: (op : (($8251, $8252, $8253)) -> $8248 $8254) -> clause1<($8251, $8252, $8253),$8254,$8250,$8248,$8249>( fnfn: (($8251, $8252, $8253)) -> $8248 $8254((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8251,x2x2: $8252,x3x3: $8253)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) ){ opop: ($8251, $8252, $8253) -> $8248 $8254(x1x1: $8251,x2x2: $8252,x3x3: $8253) } ) pub fun clause-tail-noop3std/core/hnd/clause-tail-noop3: forall<e,a,b,c,d,a1,b1> (op : (c, d, a1) -> e b1) -> clause1<(c, d, a1),b1,b,e,a><ee: E,rr: V,hh: (E, V) -> V,a1a1: V,a2a2: V,a3a3: V,bb: V>(opop: ($8350, $8351, $8352) -> $8347 $8353 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E bb: V)result: -> total clause1<(8420, 8421, 8422),8423,8419,8417,8418> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(std/core/types/tuple3: (V, V, V) -> Va1a1: V,a2a2: V,a3a3: V),bb: V,hh: (E, V) -> V,ee: E,rr: V> clause-tail-noop1std/core/hnd/clause-tail-noop1: (op : (($8350, $8351, $8352)) -> $8347 $8353) -> clause1<($8350, $8351, $8352),$8353,$8349,$8347,$8348>( fnfn: (($8350, $8351, $8352)) -> $8347 $8353((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8350,x2x2: $8351,x3x3: $8352)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)){ opop: ($8350, $8351, $8352) -> $8347 $8353(x1x1: $8350,x2x2: $8351,x3x3: $8352) } ) pub fun clause-never3std/core/hnd/clause-never3: forall<a,b,c,d,e,a1,b1> (op : (a, b, c) -> e b1) -> clause1<(a, b, c),d,a1,e,b1>( opop: ($8446, $8447, $8448) -> $8450 $8452 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E rr: V )result: -> total clause1<(8516, 8517, 8518),8519,8521,8520,8522> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(std/core/types/tuple3: (V, V, V) -> Va1a1: V,a2a2: V,a3a3: V),bb: V,hh: (E, V) -> V,ee: E,rr: V> clause-never1std/core/hnd/clause-never1: (op : (($8446, $8447, $8448)) -> $8450 $8452) -> clause1<($8446, $8447, $8448),$8449,$8451,$8450,$8452>(fnfn: (($8446, $8447, $8448)) -> $8450 $8452((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8446,x2x2: $8447,x3x3: $8448)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)){ opop: ($8446, $8447, $8448) -> $8450 $8452(x1x1: $8446,x2x2: $8447,x3x3: $8448) } ) pub fun @perform3( evev: ev<$8550> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($8550<e,a>) -> clause1<($8545, $8546, $8547),$8548,$8550,e,a> : (forall<e1e1: E,rr: V> hh: (E, V) -> V<e1e1: E,rr: V> -> clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(std/core/types/tuple3: (V, V, V) -> Va1a1: V,a2a2: V,a3a3: V),bb: V,hh: (E, V) -> V,e1e1: E,rr: V>), x1x1: $8545 : a1a1: V, x2x2: $8546 : a2a2: V, x3x3: $8547 : a3a3: V )result: -> 8628 8627 : ee: E bb: V xperform1std/core/hnd/xperform1: (ev : ev<$8550>, op : forall<e,a> ($8550<e,a>) -> clause1<($8545, $8546, $8547),$8548,$8550,e,a>, x : ($8545, $8546, $8547)) -> $8549 $8548(evev: ev<$8550>,opop: forall<e,a> ($8550<e,a>) -> clause1<($8545, $8546, $8547),$8548,$8550,e,a>,(std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8545,x2x2: $8546,x3x3: $8547)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)) fun under3std/core/hnd/under3: forall<a,b,c,d,e,a1> (ev : ev<a1>, op : (a, b, c) -> e d, x1 : a, x2 : b, x3 : c) -> e d( evev: ev<$8655> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($8650, $8651, $8652) -> $8654 $8653 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E bb: V, x1x1: $8650 : a1a1: V, x2x2: $8651 : a2a2: V, x3x3: $8652 : a3a3: V )result: -> 8754 8753 : ee: E bb: V val w0w0: evv<_8663> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$8655>) -> $8654 evv<_8663>(evev: ev<$8655>) val zz: $8653 = opop: ($8650, $8651, $8652) -> $8654 $8653(x1x1: $8650,x2x2: $8651,x3x3: $8652) evv-setstd/core/hnd/evv-set: (w : evv<_8663>) -> $8654 ()(w0w0: evv<_8663>) if yieldingstd/core/hnd/yielding: () -> $8654 bool() returnreturn: $8653 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $8654 $8653, a) -> $8654 $8653) -> $8654 $8653( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($8693) -> $8654 $8653,resres: $8693) under1std/core/hnd/under1: (ev : ev<$8655>, op : ($8693) -> $8654 $8653, x : $8693) -> $8654 $8653(evev: ev<$8655>,contcont: ($8693) -> $8654 $8653,resres: $8693) )std/core/types/Unit: () zz: $8653 pub fun clause-control4std/core/hnd/clause-control4: forall<a,b,c,d,a1,e,b1,c1> (op : (x1 : a, x2 : b, x3 : c, x4 : d, k : (a1) -> e c1) -> e c1) -> clause1<(a, b, c, d),a1,b1,e,c1>( opop: (x1 : $8774, x2 : $8775, x3 : $8776, x4 : $8777, k : ($8778) -> $8779 $8781) -> $8779 $8781 : (x1:a1a1: V, x2:a2a2: V, x3:a3a3: V, x4:a4a4: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause1<(8853, 8854, 8855, 8856),8857,8859,8858,8860> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(std/core/types/tuple4: (V, V, V, V) -> Va1a1: V,a2a2: V,a3a3: V,a4a4: V),bb: V,hh: (E, V) -> V,ee: E,rr: V> clause-control1std/core/hnd/clause-control1: (clause : (x : ($8774, $8775, $8776, $8777), k : ($8778) -> $8779 $8781) -> $8779 $8781) -> clause1<($8774, $8775, $8776, $8777),$8778,$8780,$8779,$8781>( fnfn: (($8774, $8775, $8776, $8777), k : ($8778) -> $8779 $8781) -> $8779 $8781((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $8774,x2x2: $8775,x3x3: $8776,x4x4: $8777)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d),kk: ($8778) -> $8779 $8781){ opop: (x1 : $8774, x2 : $8775, x3 : $8776, x4 : $8777, k : ($8778) -> $8779 $8781) -> $8779 $8781(x1x1: $8774,x2x2: $8775,x3x3: $8776,x4x4: $8777,kk: ($8778) -> $8779 $8781) } ) pub fun clause-tail4std/core/hnd/clause-tail4: forall<e,a,b,c,d,a1,b1,c1> (op : (c, d, a1, b1) -> e c1) -> clause1<(c, d, a1, b1),c1,b,e,a><ee: E,rr: V,hh: (E, V) -> V,a1a1: V,a2a2: V,a3a3: V,a4a4: V,bb: V>(opop: ($8889, $8890, $8891, $8892) -> $8886 $8893 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E bb: V)result: -> total clause1<(8967, 8968, 8969, 8970),8971,8966,8964,8965> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(std/core/types/tuple4: (V, V, V, V) -> Va1a1: V,a2a2: V,a3a3: V,a4a4: V),bb: V,hh: (E, V) -> V,ee: E,rr: V> clause-tail1std/core/hnd/clause-tail1: (op : (($8889, $8890, $8891, $8892)) -> $8886 $8893) -> clause1<($8889, $8890, $8891, $8892),$8893,$8888,$8886,$8887>( fnfn: (($8889, $8890, $8891, $8892)) -> $8886 $8893((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $8889,x2x2: $8890,x3x3: $8891,x4x4: $8892)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)){ opop: ($8889, $8890, $8891, $8892) -> $8886 $8893(x1x1: $8889,x2x2: $8890,x3x3: $8891,x4x4: $8892) } ) pub fun clause-tail-noop4std/core/hnd/clause-tail-noop4: forall<e,a,b,c,d,a1,b1,c1> (op : (c, d, a1, b1) -> e c1) -> clause1<(c, d, a1, b1),c1,b,e,a><ee: E,rr: V,hh: (E, V) -> V,a1a1: V,a2a2: V,a3a3: V,a4a4: V,bb: V>(opop: ($9000, $9001, $9002, $9003) -> $8997 $9004 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E bb: V)result: -> total clause1<(9078, 9079, 9080, 9081),9082,9077,9075,9076> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(std/core/types/tuple4: (V, V, V, V) -> Va1a1: V,a2a2: V,a3a3: V,a4a4: V),bb: V,hh: (E, V) -> V,ee: E,rr: V> clause-tail-noop1std/core/hnd/clause-tail-noop1: (op : (($9000, $9001, $9002, $9003)) -> $8997 $9004) -> clause1<($9000, $9001, $9002, $9003),$9004,$8999,$8997,$8998>( fnfn: (($9000, $9001, $9002, $9003)) -> $8997 $9004((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9000,x2x2: $9001,x3x3: $9002,x4x4: $9003)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)){ opop: ($9000, $9001, $9002, $9003) -> $8997 $9004(x1x1: $9000,x2x2: $9001,x3x3: $9002,x4x4: $9003) } ) pub fun clause-never4std/core/hnd/clause-never4: forall<a,b,c,d,a1,e,b1,c1> (op : (a, b, c, d) -> e c1) -> clause1<(a, b, c, d),a1,b1,e,c1>( opop: ($9108, $9109, $9110, $9111) -> $9113 $9115 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E rr: V )result: -> total clause1<(9186, 9187, 9188, 9189),9190,9192,9191,9193> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(std/core/types/tuple4: (V, V, V, V) -> Va1a1: V,a2a2: V,a3a3: V,a4a4: V),bb: V,hh: (E, V) -> V,ee: E,rr: V> clause-never1std/core/hnd/clause-never1: (op : (($9108, $9109, $9110, $9111)) -> $9113 $9115) -> clause1<($9108, $9109, $9110, $9111),$9112,$9114,$9113,$9115>(fnfn: (($9108, $9109, $9110, $9111)) -> $9113 $9115((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9108,x2x2: $9109,x3x3: $9110,x4x4: $9111)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)){ opop: ($9108, $9109, $9110, $9111) -> $9113 $9115(x1x1: $9108,x2x2: $9109,x3x3: $9110,x4x4: $9111) } ) pub fun @perform4( evev: ev<$9225> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($9225<e,a>) -> clause1<($9219, $9220, $9221, $9222),$9223,$9225,e,a> : (forall<e1e1: E,rr: V> hh: (E, V) -> V<e1e1: E,rr: V> -> clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(std/core/types/tuple4: (V, V, V, V) -> Va1a1: V,a2a2: V,a3a3: V,a4a4: V),bb: V,hh: (E, V) -> V,e1e1: E,rr: V>), x1x1: $9219 : a1a1: V, x2x2: $9220 : a2a2: V, x3x3: $9221 : a3a3: V, x4x4: $9222 : a4a4: V )result: -> 9312 9311 : ee: E bb: V xperform1std/core/hnd/xperform1: (ev : ev<$9225>, op : forall<e,a> ($9225<e,a>) -> clause1<($9219, $9220, $9221, $9222),$9223,$9225,e,a>, x : ($9219, $9220, $9221, $9222)) -> $9224 $9223(evev: ev<$9225>,opop: forall<e,a> ($9225<e,a>) -> clause1<($9219, $9220, $9221, $9222),$9223,$9225,e,a>,(std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9219,x2x2: $9220,x3x3: $9221,x4x4: $9222)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)) fun under4std/core/hnd/under4: forall<a,b,c,d,a1,e,b1> (ev : ev<b1>, op : (a, b, c, d) -> e a1, x1 : a, x2 : b, x3 : c, x4 : d) -> e a1( evev: ev<$9343> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($9337, $9338, $9339, $9340) -> $9342 $9341 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E bb: V, x1x1: $9337 : a1a1: V, x2x2: $9338 : a2a2: V, x3x3: $9339 : a3a3: V, x4x4: $9340 : a4a4: V )result: -> 9448 9447 : ee: E bb: V val w0w0: evv<_9351> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$9343>) -> $9342 evv<_9351>(evev: ev<$9343>) val zz: $9341 = opop: ($9337, $9338, $9339, $9340) -> $9342 $9341(x1x1: $9337,x2x2: $9338,x3x3: $9339,x4x4: $9340) evv-setstd/core/hnd/evv-set: (w : evv<_9351>) -> $9342 ()(w0w0: evv<_9351>) if yieldingstd/core/hnd/yielding: () -> $9342 bool() returnreturn: $9341 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $9342 $9341, a) -> $9342 $9341) -> $9342 $9341( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($9382) -> $9342 $9341,resres: $9382) under1std/core/hnd/under1: (ev : ev<$9343>, op : ($9382) -> $9342 $9341, x : $9382) -> $9342 $9341(evev: ev<$9343>,contcont: ($9382) -> $9342 $9341,resres: $9382) )std/core/types/Unit: () zz: $9341 // ------------------------------------------- // Open // ------------------------------------------- pub fun @open-none0<bb: V,e1e1: E,e2e2: E>( ff: () -> $9472 $9471 : () -> e1e1: E bb: V )result: -> 9515 9513 : e2e2: E bb: V val ww: evv<$9473> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $9473 evv<$9473>() val xx: $9471 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $9472 $9471) -> $9473 (() -> $9473 $9471)(ff: () -> $9472 $9471)() val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$9473>) -> $9473 ()(ww: evv<$9473>) xx: $9471 pub fun @open-none1<aa: V,bb: V,e1e1: E,e2e2: E>( ff: ($9525) -> $9527 $9526 : aa: V -> e1e1: E bb: V, x1x1: $9525 : aa: V )result: -> 9579 9577 : e2e2: E bb: V val ww: evv<$9528> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $9528 evv<$9528>() val xx: $9526 = cast-ev1std/core/hnd/cast-ev1: (f : ($9525) -> $9527 $9526) -> $9528 (($9525) -> $9528 $9526)(ff: ($9525) -> $9527 $9526)(x1x1: $9525) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$9528>) -> $9528 ()(ww: evv<$9528>) xx: $9526 pub fun @open-none2<a1a1: V,a2a2: V,bb: V,e1e1: E,e2e2: E>( ff: ($9592, $9593) -> $9595 $9594 : (a1a1: V,a2a2: V) -> e1e1: E bb: V, x1x1: $9592 : a1a1: V, x2x2: $9593 : a2a2: V )result: -> 9656 9654 : e2e2: E bb: V val ww: evv<$9596> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $9596 evv<$9596>() val xx: $9594 = cast-ev2std/core/hnd/cast-ev2: (f : ($9592, $9593) -> $9595 $9594) -> $9596 (($9592, $9593) -> $9596 $9594)(ff: ($9592, $9593) -> $9595 $9594)(x1x1: $9592,x2x2: $9593) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$9596>) -> $9596 ()(ww: evv<$9596>) xx: $9594 pub fun @open-none3<a1a1: V,a2a2: V,a3a3: V,bb: V,e1e1: E,e2e2: E>( ff: ($9672, $9673, $9674) -> $9676 $9675 : (a1a1: V,a2a2: V,a3a3: V) -> e1e1: E bb: V, x1x1: $9672 : a1a1: V, x2x2: $9673 : a2a2: V, x3x3: $9674 : a3a3: V )result: -> 9746 9744 : e2e2: E bb: V val ww: evv<$9677> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $9677 evv<$9677>() val xx: $9675 = cast-ev3std/core/hnd/cast-ev3: (f : ($9672, $9673, $9674) -> $9676 $9675) -> $9677 (($9672, $9673, $9674) -> $9677 $9675)(ff: ($9672, $9673, $9674) -> $9676 $9675)(x1x1: $9672,x2x2: $9673,x3x3: $9674) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$9677>) -> $9677 ()(ww: evv<$9677>) xx: $9675 pub fun @open-none4<a1a1: V,a2a2: V,a3a3: V,a4a4: V,bb: V,e1e1: E,e2e2: E>( ff: ($9765, $9766, $9767, $9768) -> $9770 $9769 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e1e1: E bb: V, x1x1: $9765 : a1a1: V, x2x2: $9766 : a2a2: V, x3x3: $9767 : a3a3: V, x4x4: $9768 : a4a4: V )result: -> 9849 9847 : e2e2: E bb: V val ww: evv<$9771> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $9771 evv<$9771>() val xx: $9769 = cast-ev4std/core/hnd/cast-ev4: (f : ($9765, $9766, $9767, $9768) -> $9770 $9769) -> $9771 (($9765, $9766, $9767, $9768) -> $9771 $9769)(ff: ($9765, $9766, $9767, $9768) -> $9770 $9769)(x1x1: $9765,x2x2: $9766,x3x3: $9767,x4x4: $9768) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$9771>) -> $9771 ()(ww: evv<$9771>) xx: $9769 noinline fun open-at1std/core/hnd/open-at1: forall<a,b,e,e1> (i : ev-index, f : (a) -> e b, x : a) -> e1 b<aa: V,bb: V,e1e1: E,e2e2: E>( ii: ev-index: ev-indexstd/core/hnd/ev-index: V, ff: ($9871) -> $9873 $9872 : aa: V -> e1e1: E bb: V, xx: $9871 : aa: V )result: -> 9978 9976 : e2e2: E bb: V val ww: evv<$9874> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $9874 evv<$9874>(ii: ev-index) val yy: $9872 = cast-ev1std/core/hnd/cast-ev1: (f : ($9871) -> $9873 $9872) -> $9874 (($9871) -> $9874 $9872)(ff: ($9871) -> $9873 $9872)(xx: $9871) evv-setstd/core/hnd/evv-set: (w : evv<$9874>) -> $9874 ()(ww: evv<$9874>) if yieldingstd/core/hnd/yielding: () -> $9874 bool() returnreturn: $9872 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $9874 $9872, a) -> $9874 $9872) -> $9874 $9872(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($9920) -> $9874 $9872,resres: $9920){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($9920) -> $9874 $9872, x : $9920) -> $9874 $9872(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev-index) -> $9874 ev-index(ii: ev-index),contcont: ($9920) -> $9874 $9872,resres: $9920) })std/core/types/Unit: () yy: $9872 pub fun @open-at0<bb: V,e1e1: E,e2e2: E>( ii: ev-index: ev-indexstd/core/hnd/ev-index: V, ff: () -> $9992 $9991 : () -> e1e1: E bb: V )result: -> 10082 10080 : e2e2: E bb: V val ww: evv<$9993> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $9993 evv<$9993>(ii: ev-index) val yy: $9991 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $9992 $9991) -> $9993 (() -> $9993 $9991)(ff: () -> $9992 $9991)() evv-setstd/core/hnd/evv-set: (w : evv<$9993>) -> $9993 ()(ww: evv<$9993>) if yieldingstd/core/hnd/yielding: () -> $9993 bool() returnreturn: $9991 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $9993 $9991, a) -> $9993 $9991) -> $9993 $9991(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($10035) -> $9993 $9991,resres: $10035){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10035) -> $9993 $9991, x : $10035) -> $9993 $9991(ii: ev-index,contcont: ($10035) -> $9993 $9991,resres: $10035) })std/core/types/Unit: () yy: $9991 pub fun @open-at1<aa: V,bb: V,e1e1: E,e2e2: E>( ii: ev-index: ev-indexstd/core/hnd/ev-index: V, ff: ($10092) -> $10094 $10093 : aa: V -> e1e1: E bb: V, xx: $10092 : aa: V )result: -> 10193 10191 : e2e2: E bb: V val ww: evv<$10095> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10095 evv<$10095>(ii: ev-index) val yy: $10093 = cast-ev1std/core/hnd/cast-ev1: (f : ($10092) -> $10094 $10093) -> $10095 (($10092) -> $10095 $10093)(ff: ($10092) -> $10094 $10093)(xx: $10092) evv-setstd/core/hnd/evv-set: (w : evv<$10095>) -> $10095 ()(ww: evv<$10095>) if yieldingstd/core/hnd/yielding: () -> $10095 bool() returnreturn: $10093 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10095 $10093, a) -> $10095 $10093) -> $10095 $10093(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($10141) -> $10095 $10093,resres: $10141){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10141) -> $10095 $10093, x : $10141) -> $10095 $10093(ii: ev-index,contcont: ($10141) -> $10095 $10093,resres: $10141) })std/core/types/Unit: () yy: $10093 pub fun @open-at2<a1a1: V,a2a2: V,bb: V,e1e1: E,e2e2: E> ( ii: ev-index: ev-indexstd/core/hnd/ev-index: V, ff: ($10206, $10207) -> $10209 $10208 : (a1a1: V,a2a2: V) -> e1e1: E bb: V, x1x1: $10206 : a1a1: V, x2x2: $10207 : a2a2: V )result: -> 10317 10315 : e2e2: E bb: V val ww: evv<$10210> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10210 evv<$10210>(ii: ev-index) val yy: $10208 = cast-ev2std/core/hnd/cast-ev2: (f : ($10206, $10207) -> $10209 $10208) -> $10210 (($10206, $10207) -> $10210 $10208)(ff: ($10206, $10207) -> $10209 $10208)(x1x1: $10206,x2x2: $10207) evv-setstd/core/hnd/evv-set: (w : evv<$10210>) -> $10210 ()(ww: evv<$10210>) if yieldingstd/core/hnd/yielding: () -> $10210 bool() returnreturn: $10208 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10210 $10208, a) -> $10210 $10208) -> $10210 $10208(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($10260) -> $10210 $10208,resres: $10260){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10260) -> $10210 $10208, x : $10260) -> $10210 $10208(ii: ev-index,contcont: ($10260) -> $10210 $10208,resres: $10260) })std/core/types/Unit: () yy: $10208 pub fun @open-at3<a1a1: V,a2a2: V,a3a3: V,bb: V,e1e1: E,e2e2: E> ( ii: ev-index: ev-indexstd/core/hnd/ev-index: V, ff: ($10333, $10334, $10335) -> $10337 $10336 : (a1a1: V,a2a2: V,a3a3: V) -> e1e1: E bb: V, x1x1: $10333 : a1a1: V, x2x2: $10334 : a2a2: V, x3x3: $10335 : a3a3: V )result: -> 10454 10452 : e2e2: E bb: V val ww: evv<$10338> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10338 evv<$10338>(ii: ev-index) val yy: $10336 = cast-ev3std/core/hnd/cast-ev3: (f : ($10333, $10334, $10335) -> $10337 $10336) -> $10338 (($10333, $10334, $10335) -> $10338 $10336)(ff: ($10333, $10334, $10335) -> $10337 $10336)(x1x1: $10333,x2x2: $10334,x3x3: $10335) evv-setstd/core/hnd/evv-set: (w : evv<$10338>) -> $10338 ()(ww: evv<$10338>) if yieldingstd/core/hnd/yielding: () -> $10338 bool() returnreturn: $10336 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10338 $10336, a) -> $10338 $10336) -> $10338 $10336(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($10392) -> $10338 $10336,resres: $10392){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10392) -> $10338 $10336, x : $10392) -> $10338 $10336(ii: ev-index,contcont: ($10392) -> $10338 $10336,resres: $10392) })std/core/types/Unit: () yy: $10336 pub fun @open-at4<a1a1: V,a2a2: V,a3a3: V,a4a4: V,bb: V,e1e1: E,e2e2: E> ( ii: ev-index: ev-indexstd/core/hnd/ev-index: V, ff: ($10473, $10474, $10475, $10476) -> $10478 $10477 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e1e1: E bb: V, x1x1: $10473 : a1a1: V, x2x2: $10474 : a2a2: V, x3x3: $10475 : a3a3: V, x4x4: $10476 : a4a4: V )result: -> 10604 10602 : e2e2: E bb: V val ww: evv<$10479> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10479 evv<$10479>(ii: ev-index) val yy: $10477 = cast-ev4std/core/hnd/cast-ev4: (f : ($10473, $10474, $10475, $10476) -> $10478 $10477) -> $10479 (($10473, $10474, $10475, $10476) -> $10479 $10477)(ff: ($10473, $10474, $10475, $10476) -> $10478 $10477)(x1x1: $10473,x2x2: $10474,x3x3: $10475,x4x4: $10476) evv-setstd/core/hnd/evv-set: (w : evv<$10479>) -> $10479 ()(ww: evv<$10479>) if yieldingstd/core/hnd/yielding: () -> $10479 bool() returnreturn: $10477 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10479 $10477, a) -> $10479 $10477) -> $10479 $10477(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($10537) -> $10479 $10477,resres: $10537){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10537) -> $10479 $10477, x : $10537) -> $10479 $10477(ii: ev-index,contcont: ($10537) -> $10479 $10477,resres: $10537) })std/core/types/Unit: () yy: $10477 noinline fun open1std/core/hnd/open1: forall<a,b,e,e1> (indices : vector<ev-index>, f : (a) -> e b, x : a) -> e1 b<aa: V,bb: V,e1e1: E,e2e2: E>( indicesindices: vector<ev-index> : vectorstd/core/types/vector: V -> V<ev-indexstd/core/hnd/ev-index: V>, ff: ($10626) -> $10628 $10627 : aa: V -> e1e1: E bb: V, xx: $10626 : aa: V )result: -> 10733 10731 : e2e2: E bb: V val ww: evv<$10629> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $10629 evv<$10629>(indicesindices: vector<ev-index>) val yy: $10627 = cast-ev1std/core/hnd/cast-ev1: (f : ($10626) -> $10628 $10627) -> $10629 (($10626) -> $10629 $10627)(ff: ($10626) -> $10628 $10627)(xx: $10626) evv-setstd/core/hnd/evv-set: (w : evv<$10629>) -> $10629 ()(ww: evv<$10629>) if yieldingstd/core/hnd/yielding: () -> $10629 bool() returnreturn: $10627 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10629 $10627, a) -> $10629 $10627) -> $10629 $10627(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($10675) -> $10629 $10627,resres: $10675){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($10675) -> $10629 $10627, x : $10675) -> $10629 $10627(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : vector<ev-index>) -> $10629 vector<ev-index>(indicesindices: vector<ev-index>),contcont: ($10675) -> $10629 $10627,resres: $10675) })std/core/types/Unit: () yy: $10627 pub fun @open0<bb: V,e1e1: E,e2e2: E>( indicesindices: vector<ev-index> : vectorstd/core/types/vector: V -> V<ev-indexstd/core/hnd/ev-index: V>, ff: () -> $10747 $10746 : () -> e1e1: E bb: V )result: -> 10837 10835 : e2e2: E bb: V val ww: evv<$10748> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $10748 evv<$10748>(indicesindices: vector<ev-index>) val yy: $10746 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $10747 $10746) -> $10748 (() -> $10748 $10746)(ff: () -> $10747 $10746)() evv-setstd/core/hnd/evv-set: (w : evv<$10748>) -> $10748 ()(ww: evv<$10748>) if yieldingstd/core/hnd/yielding: () -> $10748 bool() returnreturn: $10746 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10748 $10746, a) -> $10748 $10746) -> $10748 $10746(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($10790) -> $10748 $10746,resres: $10790){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($10790) -> $10748 $10746, x : $10790) -> $10748 $10746(indicesindices: vector<ev-index>,contcont: ($10790) -> $10748 $10746,resres: $10790) })std/core/types/Unit: () yy: $10746 pub fun @open1<aa: V,bb: V,e1e1: E,e2e2: E>( indicesindices: vector<ev-index> : vectorstd/core/types/vector: V -> V<ev-indexstd/core/hnd/ev-index: V>, ff: ($10847) -> $10849 $10848 : aa: V -> e1e1: E bb: V, xx: $10847 : aa: V )result: -> 10948 10946 : e2e2: E bb: V val ww: evv<$10850> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $10850 evv<$10850>(indicesindices: vector<ev-index>) val yy: $10848 = cast-ev1std/core/hnd/cast-ev1: (f : ($10847) -> $10849 $10848) -> $10850 (($10847) -> $10850 $10848)(ff: ($10847) -> $10849 $10848)(xx: $10847) evv-setstd/core/hnd/evv-set: (w : evv<$10850>) -> $10850 ()(ww: evv<$10850>) if yieldingstd/core/hnd/yielding: () -> $10850 bool() returnreturn: $10848 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10850 $10848, a) -> $10850 $10848) -> $10850 $10848(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($10896) -> $10850 $10848,resres: $10896){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($10896) -> $10850 $10848, x : $10896) -> $10850 $10848(indicesindices: vector<ev-index>,contcont: ($10896) -> $10850 $10848,resres: $10896) })std/core/types/Unit: () yy: $10848 pub fun @open2<a1a1: V,a2a2: V,bb: V,e1e1: E,e2e2: E>( indicesindices: vector<ev-index> : vectorstd/core/types/vector: V -> V<ev-indexstd/core/hnd/ev-index: V>, ff: ($10961, $10962) -> $10964 $10963 : (a1a1: V,a2a2: V) -> e1e1: E bb: V, x1x1: $10961 : a1a1: V, x2x2: $10962 : a2a2: V )result: -> 11072 11070 : e2e2: E bb: V val ww: evv<$10965> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $10965 evv<$10965>(indicesindices: vector<ev-index>) val yy: $10963 = cast-ev2std/core/hnd/cast-ev2: (f : ($10961, $10962) -> $10964 $10963) -> $10965 (($10961, $10962) -> $10965 $10963)(ff: ($10961, $10962) -> $10964 $10963)(x1x1: $10961,x2x2: $10962) evv-setstd/core/hnd/evv-set: (w : evv<$10965>) -> $10965 ()(ww: evv<$10965>) if yieldingstd/core/hnd/yielding: () -> $10965 bool() returnreturn: $10963 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10965 $10963, a) -> $10965 $10963) -> $10965 $10963(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($11015) -> $10965 $10963,resres: $11015){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11015) -> $10965 $10963, x : $11015) -> $10965 $10963(indicesindices: vector<ev-index>,contcont: ($11015) -> $10965 $10963,resres: $11015) })std/core/types/Unit: () yy: $10963 pub fun @open3<a1a1: V,a2a2: V,a3a3: V,bb: V,e1e1: E,e2e2: E>( indicesindices: vector<ev-index> : vectorstd/core/types/vector: V -> V<ev-indexstd/core/hnd/ev-index: V>, ff: ($11088, $11089, $11090) -> $11092 $11091 : (a1a1: V,a2a2: V,a3a3: V) -> e1e1: E bb: V, x1x1: $11088 : a1a1: V, x2x2: $11089 : a2a2: V, x3x3: $11090 : a3a3: V )result: -> 11209 11207 : e2e2: E bb: V val ww: evv<$11093> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $11093 evv<$11093>(indicesindices: vector<ev-index>) val yy: $11091 = cast-ev3std/core/hnd/cast-ev3: (f : ($11088, $11089, $11090) -> $11092 $11091) -> $11093 (($11088, $11089, $11090) -> $11093 $11091)(ff: ($11088, $11089, $11090) -> $11092 $11091)(x1x1: $11088,x2x2: $11089,x3x3: $11090) evv-setstd/core/hnd/evv-set: (w : evv<$11093>) -> $11093 ()(ww: evv<$11093>) if yieldingstd/core/hnd/yielding: () -> $11093 bool() returnreturn: $11091 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11093 $11091, a) -> $11093 $11091) -> $11093 $11091(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($11147) -> $11093 $11091,resres: $11147){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11147) -> $11093 $11091, x : $11147) -> $11093 $11091(indicesindices: vector<ev-index>,contcont: ($11147) -> $11093 $11091,resres: $11147) })std/core/types/Unit: () yy: $11091 pub fun @open4<a1a1: V,a2a2: V,a3a3: V,a4a4: V,bb: V,e1e1: E,e2e2: E>( indicesindices: vector<ev-index> : vectorstd/core/types/vector: V -> V<ev-indexstd/core/hnd/ev-index: V>, ff: ($11228, $11229, $11230, $11231) -> $11233 $11232 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e1e1: E bb: V, x1x1: $11228 : a1a1: V, x2x2: $11229 : a2a2: V, x3x3: $11230 : a3a3: V, x4x4: $11231 : a4a4: V )result: -> 11359 11357 : e2e2: E bb: V val ww: evv<$11234> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $11234 evv<$11234>(indicesindices: vector<ev-index>) val yy: $11232 = cast-ev4std/core/hnd/cast-ev4: (f : ($11228, $11229, $11230, $11231) -> $11233 $11232) -> $11234 (($11228, $11229, $11230, $11231) -> $11234 $11232)(ff: ($11228, $11229, $11230, $11231) -> $11233 $11232)(x1x1: $11228,x2x2: $11229,x3x3: $11230,x4x4: $11231) evv-setstd/core/hnd/evv-set: (w : evv<$11234>) -> $11234 ()(ww: evv<$11234>) if yieldingstd/core/hnd/yielding: () -> $11234 bool() returnreturn: $11232 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11234 $11232, a) -> $11234 $11232) -> $11234 $11232(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($11292) -> $11234 $11232,resres: $11292){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11292) -> $11234 $11232, x : $11292) -> $11234 $11232(indicesindices: vector<ev-index>,contcont: ($11292) -> $11234 $11232,resres: $11292) })std/core/types/Unit: () yy: $11232 // ------------------------------------------- // capture yields // ------------------------------------------- pub fun unsafe-try-finalizestd/core/hnd/unsafe-try-finalize: forall<a,e> (action : () -> e a) -> e either<yield-info,a>( actionaction: () -> $11486 $11485 : () -> ee: E aa: V )result: -> 11505 either<yield-info,11504> : ee: E eitherstd/core/types/either: (V, V) -> V<yield-infostd/core/hnd/yield-info: V,aa: V> try-finalize-promptstd/core/hnd/try-finalize-prompt: (res : $11485) -> $11486 either<yield-info,$11485>(actionaction: () -> $11486 $11485()); fun try-finalize-promptstd/core/hnd/try-finalize-prompt: forall<a,e> (res : a) -> e either<yield-info,a>( resres: $11381 : aa: V )result: -> 11478 either<yield-info,11477> : ee: E eitherstd/core/types/either: (V, V) -> V<yield-infostd/core/hnd/yield-info: V,aa: V> if yielding-non-finalstd/core/hnd/yielding-non-final: () -> $11382 bool() returnreturn: either<yield-info,$11381> yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11382 $11381, a) -> $11382 either<yield-info,$11381>) -> $11382 either<yield-info,$11381>(fnfn: forall<a,b,e> (cont : (a) -> e b, x : a) -> e either<yield-info,b>(contcont: ($11398) -> $11382 $11381,xx: $11398) try-finalize-promptstd/core/hnd/try-finalize-prompt: (res : $11381) -> $11382 either<yield-info,$11381>(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : $11381) -> $11382 $11381(contcont: ($11398) -> $11382 $11381(xx: $11398))) )std/core/types/Unit: () if !std/core/types/bool/(!): (b : bool) -> $11382 boolyieldingstd/core/hnd/yielding: () -> $11382 bool() then Rightstd/core/types/Right: forall<a,b> (right : b) -> either<a,b>(resres: $11381) else Leftstd/core/types/Left: forall<a,b> (left : a) -> either<a,b>(yield-capturestd/core/hnd/yield-capture: () -> $11382 yield-info())