/*---------------------------------------------------------------------------
  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<2703> : 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<$10257,$10258>)  : 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<$10267,$10268>) : 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<$10257,$10258>, y : marker<$10267,$10268>) -> bool(m1m1: marker<$10257,$10258>,m2m2: marker<$10267,$10268>)


// -------------------------------------------
// 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<$4031,$4029> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,a1a1: V>, yy: marker<$4032,$4030> : 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<$3325> : evvstd/core/hnd/evv: E -> V<e1e1: E>, evev: ev<$3327> : 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<$4077> : 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<$3385> : evvstd/core/hnd/evv: E -> V<ee: E>, evv1evv1: evv<$3385> : 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<$2628> : 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 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: ($3416) -> $3418 $3417 : 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: $4318 : aa: V, nextnext: ($4318) -> $4320 $4319 : aa: V -> ee: E bb: V )result: -> 4349 4348 : ee: E bb: V
  if yieldingstd/core/hnd/yielding: () -> $4320 bool() then yield-extendstd/core/hnd/yield-extend: (next : ($4318) -> $4320 $4319) -> $4320 $4319(nextnext: ($4318) -> $4320 $4319) else nextnext: ($4318) -> $4320 $4319(xx: $4318)

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: $10213 : aa: V, extendextend: ($10213) -> $10215 $10214 : aa: V -> ee: E bb: V, nextnext: ($10213) -> $10215 $10214 : aa: V -> ee: E bb: V )result: -> 10244 10243 : ee: E bb: V
  if yieldingstd/core/hnd/yielding: () -> $10215 bool() then yield-extendstd/core/hnd/yield-extend: (next : ($10213) -> $10215 $10214) -> $10215 $10214(extendextend: ($10213) -> $10215 $10214) else nextnext: ($10213) -> $10215 $10214(xx: $10213)

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) -> $3450 $3449, a) -> $3450 $3451 : 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<$3492,$3493>: 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<$3722,$3723> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>, clauseclause: ((resume-result<$3720,$3723>) -> $3722 $3723) -> $3722 $3723 : (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<$3530,$3531> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>, clauseclause: ((resume-result<$3528,$3531>) -> $3530 $3531) -> $3530 $3531 : (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<$6674,$6675> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>, clauseclause: ((resume-result<$6673,$6675>) -> $6674 $6675) -> $6674 $6675 : (resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> e1e1: E rr: V) -> e1e1: E rr: V )result: -> 6716 6715 : e1e1: E bb: V
  //val w0 = evv-get()
  val gg: () -> $6673 : () -> _b_b: V = yield-to-primstd/core/hnd/yield-to-prim: (m : marker<$6674,$6675>, clause : ((resume-result<$6673,$6675>) -> $6674 $6675) -> $6674 $6675) -> $6674 (() -> $6673)(mm: marker<$6674,$6675>, clauseclause: ((resume-result<$6673,$6675>) -> $6674 $6675) -> $6674 $6675)
  yield-extendstd/core/hnd/yield-extend: (next : (() -> $6674 $6673) -> $6674 $6673) -> $6674 $6673 fnfn: (f : () -> $6674 $6673) -> $6674 $6673(ff: () -> $6674 $6673)
    // val keep1 = guard(w0)  // check the evidence is correctly restored
    ff: () -> $6674 $6673()

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<$3403> : 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<$4360> : evvstd/core/hnd/evv: E -> V<e0e0: E>,  w1w1: evv<$4360> : evvstd/core/hnd/evv: E -> V<e0e0: E>, evev: ev<$4361> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, mm: marker<$4360,$4362> : markerstd/core/hnd/marker: (E, V) -> V<e0e0: E,rr: V>, retret: ($4359) -> $4360 $4362: aa: V -> e0e0: E rr: V, resultresult: $4359 : aa: V )result: -> 4690 4692 : e0e0: E rr: V
  guardstd/core/hnd/guard: (w : evv<$4360>) -> $4360 ()(w1w1: evv<$4360>)
  evv-setstd/core/hnd/evv-set: (w : evv<$4360>) -> $4360 ()(w0w0: evv<$4360>)  // restore the previous evidence vector
  match yield-promptstd/core/hnd/yield-prompt: (m : marker<$4360,$4362>) -> $4360 yld<$4360,$4359,$4362>(mm: marker<$4360,$4362>)
    Purestd/core/hnd/Pure: forall<e,a,b> yld<e,a,b> ->
      // returning
      retret: ($4359) -> $4360 $4362(resultresult: $4359)
    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: () -> $4360 $4362()
    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) -> $4360 $4359, a) -> $4360 $4362) -> $4360 $4362 fnfn: forall<a> (cont : (a) -> $4360 $4359, res : a) -> $4360 $4362(contcont: ($4421) -> $4360 $4359,resres: $4421)
        // we resume, continue under a fresh a prompt again
        val w0'w0': evv<$4360> = evv-getstd/core/hnd/evv-get: () -> $4360 evv<$4360>()  // if not using scoped resumptions, w0' may be different from w0
        val w1'w1': evv<$4360> = if (evv-eqstd/core/hnd/evv-eq: (evv0 : evv<$4360>, evv1 : evv<$4360>) -> $4360 bool(w0w0: evv<$4360>,w0'w0': evv<$4360>)) then w1w1: evv<$4360> else evv-insertstd/core/hnd/evv-insert: (evv : evv<$4360>, ev : ev<$4361>) -> $4360 evv<$4360>(w0'w0': evv<$4360>,evev: ev<$4361>)
        evv-setstd/core/hnd/evv-set: (w : evv<$4360>) -> $4360 ()(w1'w1': evv<$4360>)
        promptstd/core/hnd/prompt: (w0 : evv<$4360>, w1 : evv<$4360>, ev : ev<$4361>, m : marker<$4360,$4362>, ret : ($4359) -> $4360 $4362, result : $4359) -> $4360 $4362(w0'w0': evv<$4360>,w1'w1': evv<$4360>,evev: ev<$4361>,pretend-decreasingstd/core/undiv/pretend-decreasing: (x : marker<$4360,$4362>) -> $4360 marker<$4360,$4362>(mm: marker<$4360,$4362>),retret: ($4359) -> $4360 $4362,contcont: ($4421) -> $4360 $4359(resres: $4421));
    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<$4489,$4362>) -> $4360 $4362) -> $4360 $4362,contcont: (() -> $4489) -> $4360 $4359) ->
      // yielded to the operation `clause` in our handler
      fun resumeresume: (r : resume-result<$4489,$4362>) -> $4360 $4362(rr: resume-result<$4489,$4362>)result: -> $4360 $4362
        match(rr: resume-result<$4489,$4362>)
          Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(xx: $4489) ->
            val w0'w0': evv<$4360> = evv-getstd/core/hnd/evv-get: () -> $4360 evv<$4360>()  // if not using scoped resumptions, w0' may be different from w0
            val w1'w1': evv<$4360> = if evv-eqstd/core/hnd/evv-eq: (evv0 : evv<$4360>, evv1 : evv<$4360>) -> $4360 bool(w0w0: evv<$4360>,w0'w0': evv<$4360>) then w1w1: evv<$4360> else evv-insertstd/core/hnd/evv-insert: (evv : evv<$4360>, ev : ev<$4361>) -> $4360 evv<$4360>(w0'w0': evv<$4360>,evev: ev<$4361>)
            evv-setstd/core/hnd/evv-set: (w : evv<$4360>) -> $4360 ()(w1'w1': evv<$4360>)
            promptstd/core/hnd/prompt: (w0 : evv<$4360>, w1 : evv<$4360>, ev : ev<$4361>, m : marker<$4360,$4362>, ret : ($4359) -> $4360 $4362, result : $4359) -> $4360 $4362(w0'w0': evv<$4360>,w1'w1': evv<$4360>,evev: ev<$4361>,pretend-decreasingstd/core/undiv/pretend-decreasing: (x : marker<$4360,$4362>) -> $4360 marker<$4360,$4362>(mm: marker<$4360,$4362>),retret: ($4359) -> $4360 $4362,contcont: (() -> $4489) -> $4360 $4359({xx: $4489}))
          Shallowstd/core/hnd/Shallow: forall<a,b> (result : a) -> resume-result<a,b>(xx: $4489) ->
            yield-bindstd/core/hnd/yield-bind: (x : $4359, next : ($4359) -> $4360 $4362) -> $4360 $4362( contcont: (() -> $4489) -> $4360 $4359({xx: $4489}), fnfn: (y : $4359) -> $4360 $4362(yy: $4359) retret: ($4359) -> $4360 $4362(yy: $4359) )
          Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>(xx: $4362) ->
            val w0'w0': evv<$4360> = evv-getstd/core/hnd/evv-get: () -> $4360 evv<$4360>()  // if not using scoped resumptions, w0' may be different from w0
            val w1'w1': evv<$4360> = if evv-eqstd/core/hnd/evv-eq: (evv0 : evv<$4360>, evv1 : evv<$4360>) -> $4360 bool(w0w0: evv<$4360>,w0'w0': evv<$4360>) then w1w1: evv<$4360> else evv-insertstd/core/hnd/evv-insert: (evv : evv<$4360>, ev : ev<$4361>) -> $4360 evv<$4360>(w0'w0': evv<$4360>,evev: ev<$4361>)
            evv-setstd/core/hnd/evv-set: (w : evv<$4360>) -> $4360 ()(w1'w1': evv<$4360>)
            promptstd/core/hnd/prompt: (w0 : evv<$4360>, w1 : evv<$4360>, ev : ev<$4361>, m : marker<$4360,$4362>, ret : ($4359) -> $4360 $4362, result : $4359) -> $4360 $4362(w0'w0': evv<$4360>,w1'w1': evv<$4360>,evev: ev<$4361>,pretend-decreasingstd/core/undiv/pretend-decreasing: (x : marker<$4360,$4362>) -> $4360 marker<$4360,$4362>(mm: marker<$4360,$4362>),retret: ($4359) -> $4360 $4362,contcont: (() -> $4489) -> $4360 $4359({ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$4360,$4362>, clause : ((resume-result<$4489,$4362>) -> $4360 $4362) -> $4360 $4362) -> $4489(mm: marker<$4360,$4362>, fnfn: ((resume-result<$4489,$4362>) -> $4360 $4362) -> $4360 $4362(_k) xx: $4362) }))
      clauseclause: ((resume-result<$4489,$4362>) -> $4360 $4362) -> $4360 $4362(resumeresume: (r : resume-result<$4489,$4362>) -> $4360 $4362) // TODO: we should exit prompt first, and then execute clause to use constant stack space when resuming

pub noinline fun @hhandle( tagtag: htag<$4708>:htagstd/core/hnd/htag: ((E, V) -> V) -> V<hh: (E, V) -> V>, hh: $4708<$4706,$4709> : hh: (E, V) -> V<ee: E,rr: V>, retret: ($4705) -> $4706 $4709: aa: V -> ee: E rr: V, actionaction: () -> $4707 $4705 : () -> e1e1: E aa: V )result: -> 4802 4805 : ee: E rr: V
  // insert new evidence for our handler
  val w0w0: evv<$4706> = evv-getstd/core/hnd/evv-get: () -> $4706 evv<$4706>()
  val mm: marker<$4706,$4709>  = fresh-markerstd/core/hnd/fresh-marker: () -> $4706 marker<$4706,$4709>()
  val evev: ev<$4708> = 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<$4708>,mm: marker<$4706,$4709>,hh: $4708<$4706,$4709>,w0w0: evv<$4706>)
  val w1w1: evv<$4706> = evv-insertstd/core/hnd/evv-insert: (evv : evv<$4706>, ev : ev<$4708>) -> $4706 evv<$4706>(w0w0: evv<$4706>,evev: ev<$4708>)
  evv-setstd/core/hnd/evv-set: (w : evv<$4706>) -> $4706 ()(w1w1: evv<$4706>)
  // call action first (this may be yielding), then check the result
  promptstd/core/hnd/prompt: (w0 : evv<$4706>, w1 : evv<$4706>, ev : ev<$4708>, m : marker<$4706,$4709>, ret : ($4705) -> $4706 $4709, result : $4705) -> $4706 $4709(w0w0: evv<$4706>,w1w1: evv<$4706>,evev: ev<$4708>,mm: marker<$4706,$4709>,retret: ($4705) -> $4706 $4709,cast-ev0std/core/hnd/cast-ev0: (f : () -> $4707 $4705) -> $4706 (() -> $4706 $4705)(actionaction: () -> $4707 $4705)())

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

pub noinline fun @named-handle( tagtag: htag<$5033>:htagstd/core/hnd/htag: ((E, V) -> V) -> V<hh: (E, V) -> V>, hh: $5033<$5031,$5034> : hh: (E, V) -> V<ee: E,rr: V>, retret: ($5030) -> $5031 $5034: aa: V -> ee: E rr: V, actionaction: (ev<$5033>) -> $5032 $5030 : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V> -> e1e1: E aa: V )result: -> 5111 5114 : ee: E rr: V
  val mm: marker<$5031,$5034> = fresh-marker-namedstd/core/hnd/fresh-marker-named: () -> $5031 marker<$5031,$5034>()            // unique (negative) marker, but never gets inserted into the evidence vector
  val w0w0: evv<$5031> = evv-getstd/core/hnd/evv-get: () -> $5031 evv<$5031>()
  val evev: ev<$5033> = 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<$5033>,mm: marker<$5031,$5034>,hh: $5033<$5031,$5034>,w0w0: evv<$5031>)
  promptstd/core/hnd/prompt: (w0 : evv<$5031>, w1 : evv<$5031>, ev : ev<$5033>, m : marker<$5031,$5034>, ret : ($5030) -> $5031 $5034, result : $5030) -> $5031 $5034(w0w0: evv<$5031>,w0w0: evv<$5031>,evev: ev<$5033>,mm: marker<$5031,$5034>,retret: ($5030) -> $5031 $5034,cast-ev1std/core/hnd/cast-ev1: (f : (ev<$5033>) -> $5032 $5030) -> $5031 ((ev<$5033>) -> $5031 $5030)(actionaction: (ev<$5033>) -> $5032 $5030)(evev: ev<$5033>))


// -------------------------------------------
// 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: ($4821) -> $4823 $4822 : (aa: V) -> e1e1: E bb: V, xx: $4821 : aa: V )result: -> 4921 4919 : e2e2: E bb: V
  val w0w0: evv<_4830> = evv-swap-deletestd/core/hnd/evv-swap-delete: (i : ev-index, behind : bool) -> $4824 evv<_4830>(ii: ev-index,behindbehind: bool)
  val yy: $4822 = cast-ev1std/core/hnd/cast-ev1: (f : ($4821) -> $4823 $4822) -> $4824 (($4821) -> $4824 $4822)(actionaction: ($4821) -> $4823 $4822)(xx: $4821)
  evv-setstd/core/hnd/evv-set: (w : evv<_4830>) -> $4824 ()(w0w0: evv<_4830>)
  if yieldingstd/core/hnd/yielding: () -> $4824 bool() returnreturn: $4822 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $4824 $4822, a) -> $4824 $4822) -> $4824 $4822( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($4874) -> $4824 $4822,resres: $4874) mask-at1std/core/hnd/mask-at1: (i : ev-index, behind : bool, action : ($4874) -> $4824 $4822, x : $4874) -> $4824 $4822(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev-index) -> $4824 ev-index(ii: ev-index),behindbehind: bool,contcont: ($4874) -> $4824 $4822,resres: $4874) )std/core/types/Unit: ()
  yy: $4822

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: () -> $4935 $4934 : () -> e1e1: E aa: V )result: -> 5020 5018 : e2e2: E aa: V
  val w0w0: evv<_4942> = evv-swap-deletestd/core/hnd/evv-swap-delete: (i : ev-index, behind : bool) -> $4936 evv<_4942>(ii: ev-index,behindbehind: bool)
  val xx: $4934 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $4935 $4934) -> $4936 (() -> $4936 $4934)(actionaction: () -> $4935 $4934)()
  evv-setstd/core/hnd/evv-set: (w : evv<_4942>) -> $4936 ()(w0w0: evv<_4942>)
  if yieldingstd/core/hnd/yielding: () -> $4936 bool() returnreturn: $4934 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $4936 $4934, a) -> $4936 $4934) -> $4936 $4934( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($4982) -> $4936 $4934,resres: $4982) mask-at1std/core/hnd/mask-at1: (i : ev-index, behind : bool, action : ($4982) -> $4936 $4934, x : $4982) -> $4936 $4934(ii: ev-index,behindbehind: bool,contcont: ($4982) -> $4936 $4934,resres: $4982) )std/core/types/Unit: ()
  xx: $4934

// mask for builtin effects without a handler or evidence (like `:st` or `:local`)
pub fun @mask-builtin<aa: V,e1e1: E,e2e2: E>( actionaction: () -> $2657 $2656 : () -> e1e1: E aa: V )result: -> 2681 2679 : e2e2: E aa: V
  cast-ev0std/core/hnd/cast-ev0: (f : () -> $2657 $2656) -> $2658 (() -> $2658 $2656)(actionaction: () -> $2657 $2656)()


// -------------------------------------------
// 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<$9664,$9661>:local-varstd/core/types/local-var: (H, V) -> V<ss: H,aa: V>, resres: $9662 : bb: V  )result: -> <div,local<9758>|9757> 9756 : <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<$9664>|$9663> boolyieldingstd/core/hnd/yielding: () -> <div,local<$9664>|$9663> bool() returnreturn: $9662 resres: $9662;
  val vv: $9661 = locloc: $9661
  yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> <div,local<$9664>|$9663> $9662, a) -> <div,local<$9664>|$9663> $9662) -> <div,local<$9664>|$9663> $9662(fnfn: forall<a,e> (cont : (a) -> <div,local<$9664>|e> $9662, x : a) -> <div,local<$9664>|e> $9662(contcont: ($9710) -> <div,local<$9664>|$9663> $9662,xx: $9710){ locloc: local-var<$9664,$9661> :=std/core/types/local-set: (v : local-var<$9664,$9661>, assigned : $9661) -> <local<$9664>,div|$9663> () vv: $9661; prompt-local-varstd/core/hnd/prompt-local-var: (loc : local-var<$9664,$9661>, res : $9662) -> <div,local<$9664>|$9663> $9662(@byref(locloc: local-var<$9664,$9661>),contcont: ($9710) -> <div,local<$9664>|$9663> $9662(xx: $9710)) } )  // 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: $9789:aa: V, actionaction: (l : local-var<$9792,$9789>) -> <local<$9792>|$9791> $9790: (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<9857>|9856> 9855 : <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<$9792>|$9791> $9790) -> <local<$9792>|$9791> $9790
    val locloc: local-var<$9792,$9789> : local-varstd/core/types/local-var: (H, V) -> V<__w-l464-c25: H,__w-l464-c27: V> = local-newstd/core/types/local-new: (value : $9789) -> <local<$9792>,div|$9791> local-var<$9792,$9789>(initinit: $9789)
    val resres: $9790 = cast-ev1std/core/hnd/cast-ev1: (f : (local-var<$9792,$9789>) -> <local<$9792>|$9791> $9790) -> <div,local<$9792>|$9791> ((local-var<$9792,$9789>) -> <div,local<$9792>|$9791> $9790)(actionaction: (l : local-var<$9792,$9789>) -> <local<$9792>|$9791> $9790)(@byref(locloc: local-var<$9792,$9789>))
    prompt-local-varstd/core/hnd/prompt-local-var: (loc : local-var<$9792,$9789>, res : $9790) -> <div,local<$9792>|$9791> $9790(@byref(locloc: local-var<$9792,$9789>),resres: $9790)


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

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

fun finally-promptstd/core/hnd/finally-prompt: forall<a,e> (fin : () -> e (), res : a) -> e a(finfin: () -> $9294 () : () -> ee: E (std/core/types/unit: V)std/core/types/unit: V, resres: $9293 : aa: V )result: -> 9398 9397 : ee: E aa: V
  if !std/core/types/bool/(!): (b : bool) -> $9294 boolyieldingstd/core/hnd/yielding: () -> $9294 bool() then
    finfin: () -> $9294 ()()
    resres: $9293
  elif yielding-non-finalstd/core/hnd/yielding-non-final: () -> $9294 bool() then
    yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $9294 $9293, a) -> $9294 $9293) -> $9294 $9293(fnfn: forall<a> (cont : (a) -> $9294 $9293, x : a) -> $9294 $9293(contcont: ($9328) -> $9294 $9293,xx: $9328){ finally-promptstd/core/hnd/finally-prompt: (fin : () -> $9294 (), res : $9293) -> $9294 $9293(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : () -> $9294 ()) -> $9294 (() -> $9294 ())(finfin: () -> $9294 ()),contcont: ($9328) -> $9294 $9293(xx: $9328)) })
  else
    val yldyld: yield-info = yield-capturestd/core/hnd/yield-capture: () -> $9294 yield-info()
    finfin: () -> $9294 ()()
    if yieldingstd/core/hnd/yielding: () -> $9294 bool() returnreturn: $9293 yield-extendstd/core/hnd/yield-extend: (next : (_9366) -> $9294 $9293) -> $9294 $9293( fnfn: (_9366) -> $9294 $9293(_x) unsafe-reyieldstd/core/hnd/unsafe-reyield: (yld : yield-info) -> $9294 $9293(yldyld: yield-info) )std/core/types/Unit: ()
    unsafe-reyieldstd/core/hnd/unsafe-reyield: (yld : yield-info) -> $9294 $9293(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) -> $9608 () : (intstd/core/types/int: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V, actionaction: () -> $9608 $9607 : () -> ee: E aa: V )result: -> 9654 9653 : ee: E aa: V
  initinit: (int) -> $9608 ()(0literal: int
dec = 0
hex8 = 0x00
bit8 = 0b00000000
) if yieldingstd/core/hnd/yielding: () -> $9608 bool() returnreturn: $9607 yield-extendstd/core/hnd/yield-extend: (next : (()) -> $9608 $9607) -> $9608 $9607(fnfn: (()) -> $9608 $9607(_ret:(std/core/types/unit: V)std/core/types/unit: V) initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $9608 (), res : $9607) -> $9608 $9607(initinit: (int) -> $9608 (),actionaction: () -> $9608 $9607()) )std/core/types/Unit: () initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $9608 (), res : $9607) -> $9608 $9607(initinit: (int) -> $9608 (), actionaction: () -> $9608 $9607()
) fun initially-promptstd/core/hnd/initially-prompt: forall<a,e> (init : (int) -> e (), res : a) -> e a( initinit: (int) -> $9430 () : (intstd/core/types/int: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V, resres: $9429 : aa: V )result: -> 9600 9599 : ee: E aa: V if yielding-non-finalstd/core/hnd/yielding-non-final: () -> $9430 bool() then val countcount: ref<global,int> = unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$9430> ref<global,int>) -> $9430 (() -> $9430 ref<global,int>){refstd/core/types/ref: (value : int) -> <alloc<global>,read<global>,write<global>|$9430> ref<global,int>(0literal: int
dec = 0
hex8 = 0x00
bit8 = 0b00000000
)}() yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $9430 $9429, a) -> $9430 $9429) -> $9430 $9429(fnfn: forall<a> (cont : (a) -> $9430 $9429, x : a) -> $9430 $9429(contcont: ($9467) -> $9430 $9429,xx: $9467) val cntcnt: int = unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$9430> int) -> $9430 (() -> $9430 int){ !std/core/types/ref/(!): (ref : ref<global,int>) -> <read<global>,alloc<global>,write<global>|$9430> intcountcount: ref<global,int> }() // increase counter on every resumption unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$9430> ()) -> $9430 (() -> $9430 ()){ countcount: ref<global,int> :=std/core/types/set: (ref : ref<global,int>, assigned : int) -> <write<global>,alloc<global>,read<global>|$9430> () addstd/core/hnd/add: (i : int, j : int) -> <write<global>,alloc<global>,read<global>|$9430> int(cntcnt: int,1literal: int
dec = 1
hex8 = 0x01
bit8 = 0b00000001
) }() if eqstd/core/hnd/eq: (x : int, y : int) -> $9430 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) -> $9430 ()(cntcnt: int) if yieldingstd/core/hnd/yielding: () -> $9430 bool() then { yield-extendstd/core/hnd/yield-extend: (next : (_9546) -> $9430 $9429) -> $9430 $9429( fnfn: (_9546) -> $9430 $9429(_ret) initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $9430 (), res : $9429) -> $9430 $9429(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : (int) -> $9430 ()) -> $9430 ((int) -> $9430 ())(initinit: (int) -> $9430 ()), contcont: ($9467) -> $9430 $9429(xx: $9467)) ); (std/core/types/Unit: ())std/core/types/Unit: () }std/core/types/Unit: () initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $9430 (), res : $9429) -> $9430 $9429(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : (int) -> $9430 ()) -> $9430 ((int) -> $9430 ())(initinit: (int) -> $9430 ()), contcont: ($9467) -> $9430 $9429(xx: $9467)) ) else resres: $9429
// ------------------------------------------- // 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<2445,2448>) -> 2446 2448 : 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<$4161,$4162,$4163,$4164> : resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>, xx: $4161 : bb: V )result: -> 4201 4203 : ee: E rr: V (rr: resume-context<$4161,$4162,$4163,$4164>.kstd/core/hnd/resume-context/k: (resume-context<$4161,$4162,$4163,$4164>) -> $4162 ((resume-result<$4161,$4164>) -> $4162 $4164))(Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(xx: $4161)) 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<$4232,$4233,$4234,$4235> : resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>, xx: $4232 : bb: V )result: -> 4288 4289 : e0e0: E rr: V cast-ev1std/core/hnd/cast-ev1: (f : (resume-result<$4232,$4235>) -> $4233 $4235) -> $4234 ((resume-result<$4232,$4235>) -> $4234 $4235)(rr: resume-context<$4232,$4233,$4234,$4235>.kstd/core/hnd/resume-context/k: (resume-context<$4232,$4233,$4234,$4235>) -> $4234 ((resume-result<$4232,$4235>) -> $4233 $4235))(Shallowstd/core/hnd/Shallow: forall<a,b> (result : a) -> resume-result<a,b>(xx: $4232)) 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<$7102,$7103,$7104,$7105> : resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>, xx: $7105 : rr: V )result: -> 7142 7144 : ee: E rr: V //finalize(r.k,x) (rr: resume-context<$7102,$7103,$7104,$7105>.kstd/core/hnd/resume-context/k: (resume-context<$7102,$7103,$7104,$7105>) -> $7103 ((resume-result<$7102,$7105>) -> $7103 $7105))(Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>(xx: $7105)) // ------------------------------------------- // 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<$3133> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($3133<e,a>) -> clause1<$3131,$3132,$3133,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: $3131 : aa: V )result: -> 3201 3199 : ee: E bb: V match evev: ev<$3133> 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<$3137,$3138>,hh: $3133<$3137,$3138>,_w) -> match hh: $3133<$3137,$3138>.opop: ($3133<$3137,$3138>) -> $3134 clause1<$3131,$3132,$3133,$3137,$3138> 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<$3137,$3138>, ev<$3133>, $3131) -> $3137 $3132) -> cast-clause1std/core/hnd/cast-clause1: (f : (marker<$3137,$3138>, ev<$3133>, $3131) -> $3137 $3132) -> $3134 ((marker<$3137,$3138>, ev<$3133>, $3131) -> $3134 $3132)(ff: (marker<$3137,$3138>, ev<$3133>, $3131) -> $3137 $3132)(mm: marker<$3137,$3138>,evev: ev<$3133>,xx: $3131) fun evv-swap-withstd/core/hnd/evv-swap-with: forall<a,e> (ev : ev<a>) -> evv<e>(evev: ev<$3944> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>)result: -> total evv<8937> match(evev: ev<$3944>) 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<$3947>) -> evv-swapstd/core/hnd/evv-swap: (w : evv<$3947>) -> evv<_3964>(ww: evv<$3947>) inline fun under1std/core/hnd/under1: forall<a,b,e,c> (ev : ev<c>, op : (a) -> e b, x : a) -> e b( evev: ev<$8622> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($8619) -> $8621 $8620 : aa: V -> ee: E bb: V, xx: $8619 : aa: V )result: -> 8703 8702 : ee: E bb: V val w0w0: evv<_8630> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$8622>) -> $8621 evv<_8630>(evev: ev<$8622>) val yy: $8620 = opop: ($8619) -> $8621 $8620(xx: $8619) // evv-set(w0) // only needed before yielding for evidence expected check in prompt if yieldingstd/core/hnd/yielding: () -> $8621 bool() returnreturn: $8620 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $8621 $8620, a) -> $8621 $8620) -> $8621 $8620( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($8650) -> $8621 $8620,resres: $8650) under1xstd/core/hnd/under1x: (ev : ev<$8622>, op : ($8650) -> $8621 $8620, x : $8650) -> $8621 $8620(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev<$8622>) -> $8621 ev<$8622>(evev: ev<$8622>),contcont: ($8650) -> $8621 $8620,resres: $8650) )std/core/types/Unit: () evv-setstd/core/hnd/evv-set: (w : evv<_8630>) -> $8621 ()(w0w0: evv<_8630>) yy: $8620 // 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<$8524> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($8521) -> $8523 $8522 : aa: V -> ee: E bb: V, xx: $8521 : aa: V )result: -> 8605 8604 : ee: E bb: V val w0w0: evv<_8532> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$8524>) -> $8523 evv<_8532>(evev: ev<$8524>) val yy: $8522 = opop: ($8521) -> $8523 $8522(xx: $8521) // evv-set(w0) // only needed before yielding for evidence expected check in prompt if yieldingstd/core/hnd/yielding: () -> $8523 bool() returnreturn: $8522 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $8523 $8522, a) -> $8523 $8522) -> $8523 $8522( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($8552) -> $8523 $8522,resres: $8552) under1xstd/core/hnd/under1x: (ev : ev<$8524>, op : ($8552) -> $8523 $8522, x : $8552) -> $8523 $8522(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev<$8524>) -> $8523 ev<$8524>(evev: ev<$8524>),contcont: ($8552) -> $8523 $8522,resres: $8552) )std/core/types/Unit: () evv-setstd/core/hnd/evv-set: (w : evv<_8532>) -> $8523 ()(w0w0: evv<_8532>) yy: $8522 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 : $6810, r : resume-context<$6811,$6812,$6813,$6815>) -> $6812 $6815 : (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<6879,6880,6883,6881,6884> : 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<$6812,$6815>, ev<$6814>, x : $6810) -> $6812 $6811(mm: marker<$6812,$6815>,_ev,xx: $6810){ yield-tostd/core/hnd/yield-to: (m : marker<$6812,$6815>, clause : ((resume-result<$6811,$6815>) -> $6812 $6815) -> $6812 $6815) -> $6812 $6811(mm: marker<$6812,$6815>, fnfn: (k : (resume-result<$6811,$6815>) -> $6812 $6815) -> $6812 $6815(kk: (resume-result<$6811,$6815>) -> $6812 $6815){ opop: (x : $6810, r : resume-context<$6811,$6812,$6813,$6815>) -> $6812 $6815(xx: $6810,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<$6811,$6815>) -> $6812 $6815)) } ) } ) fun getstd/core/hnd/get: forall<a,h> (ref : ref<h,a>) -> <read<h>,div> a( refref: ref<$4130,$4129>: refstd/core/types/ref: (H, V) -> V<hh: H,aa: V>)result: -> <read<4153>,div> 4152 : <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<$4130,$4129>) -> <read<$4130>,div> $4129refref: ref<$4130,$4129> 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-checkstd/core/hnd/protect-check: 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<$7157,$7159>) -> $7158 $7159 : resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V, resres: $7159 : rr: V )result: -> 7224 7225 : ee: E rr: V val did-resumedid-resume: bool : boolstd/core/types/bool: V = (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$7158> bool) -> $7158 (() -> $7158 bool){ !std/core/types/ref/(!): (ref : ref<global,bool>) -> <read<global>,alloc<global>,write<global>|$7158> boolresumedresumed: ref<global,bool> })() if !std/core/types/bool/(!): (b : bool) -> $7158 booldid-resumedid-resume: bool then kk: (resume-result<$7157,$7159>) -> $7158 $7159(Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>(resres: $7159)) //finalize(k,res) else resres: $7159 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: $7235 : aa: V, clauseclause: (x : $7235, k : ($7236) -> $7237 $7238) -> $7237 $7238 : (x:aa: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V, kk: (resume-result<$7236,$7238>) -> $7237 $7238 : resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V )result: -> 7358 7359 : ee: E rr: V val resumedresumed: ref<global,bool> = (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$7237> ref<global,bool>) -> $7237 (() -> $7237 ref<global,bool>){refstd/core/types/ref: (value : bool) -> <alloc<global>,read<global>,write<global>|$7237> ref<global,bool>(Falsestd/core/types/False: bool)})() fun kprotectkprotect: (ret : $7236) -> $7237 $7238(retret: $7236)result: -> $7237 $7238 (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$7237> ()) -> $7237 (() -> $7237 ()){resumedresumed: ref<global,bool> :=std/core/types/set: (ref : ref<global,bool>, assigned : bool) -> <write<global>,alloc<global>,read<global>|$7237> () Truestd/core/types/True: bool})() kk: (resume-result<$7236,$7238>) -> $7237 $7238(Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(retret: $7236)) val resres: $7238 = clauseclause: (x : $7235, k : ($7236) -> $7237 $7238) -> $7237 $7238(xx: $7235,kprotectkprotect: (ret : $7236) -> $7237 $7238) if yieldingstd/core/hnd/yielding: () -> $7237 bool() returnreturn: $7238 yield-extendstd/core/hnd/yield-extend: (next : ($7238) -> $7237 $7238) -> $7237 $7238( fnfn: (xres : $7238) -> $7237 $7238(xresxres: $7238) protect-checkstd/core/hnd/protect-check: (resumed : ref<global,bool>, k : (resume-result<$7236,$7238>) -> $7237 $7238, res : $7238) -> $7237 $7238(resumedresumed: ref<global,bool>,kk: (resume-result<$7236,$7238>) -> $7237 $7238,xresxres: $7238) )std/core/types/Unit: () protect-checkstd/core/hnd/protect-check: (resumed : ref<global,bool>, k : (resume-result<$7236,$7238>) -> $7237 $7238, res : $7238) -> $7237 $7238(resumedresumed: ref<global,bool>,kk: (resume-result<$7236,$7238>) -> $7237 $7238,resres: $7238) /* 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 : $7449, k : ($7450) -> $7451 $7453) -> $7451 $7453 : (x:aa: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause1<7513,7514,7516,7515,7517> : 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<$7451,$7453>, ev<$7452>, x : $7449) -> $7451 $7450(mm: marker<$7451,$7453>,_ev,xx: $7449){ yield-tostd/core/hnd/yield-to: (m : marker<$7451,$7453>, clause : ((resume-result<$7450,$7453>) -> $7451 $7453) -> $7451 $7453) -> $7451 $7450(mm: marker<$7451,$7453>, fnfn: (k : (resume-result<$7450,$7453>) -> $7451 $7453) -> $7451 $7453(kk: (resume-result<$7450,$7453>) -> $7451 $7453) protectstd/core/hnd/protect: (x : $7449, clause : (x : $7449, k : ($7450) -> $7451 $7453) -> $7451 $7453, k : (resume-result<$7450,$7453>) -> $7451 $7453) -> $7451 $7453(xx: $7449,clauseclause: (x : $7449, k : ($7450) -> $7451 $7453) -> $7451 $7453,kk: (resume-result<$7450,$7453>) -> $7451 $7453) ) }) // 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: ($8863) -> $8860 $8864 : aa: V -> ee: E bb: V)result: -> total clause1<8915,8916,8914,8912,8913> : 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<$8860,$8861>, ev : ev<$8862>, x : $8863) -> $8860 $8864(_m,evev: ev<$8862>,xx: $8863){ under1std/core/hnd/under1: (ev : ev<$8862>, op : ($8863) -> $8860 $8864, x : $8863) -> $8860 $8864(evev: ev<$8862>,opop: ($8863) -> $8860 $8864,xx: $8863) }) // 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: ($3818) -> $3815 $3819 : aa: V -> ee: E bb: V)result: -> total clause1<3856,3857,3855,3853,3854> : 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<$3815,$3816>, ev<$3817>, x : $3818) -> $3815 $3819(_m,_ev,xx: $3818){ opop: ($3818) -> $3815 $3819(xx: $3818) }) // 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: ($8016) -> $8018 $8020 : aa: V -> ee: E rr: V )result: -> total clause1<8069,8070,8072,8071,8073> : 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<$8018,$8020>, ev<$8019>, x : $8016) -> $8018 $8017(mm: marker<$8018,$8020>,_ev,xx: $8016){ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$8018,$8020>, clause : ((resume-result<$8017,$8020>) -> $8018 $8020) -> $8018 $8020) -> $8018 $8017(mm: marker<$8018,$8020>, fnfn: ((resume-result<$8017,$8020>) -> $8018 $8020) -> $8018 $8020(_k) opop: ($8016) -> $8018 $8020(xx: $8016) ) }) //---------------------------------------------------------------- // 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<$3060> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($3060<e,a>) -> clause0<$3058,$3060,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: -> 3118 3117 : ee: E bb: V match evev: ev<$3060> 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<$3063,$3064>,hh: $3060<$3063,$3064>,_w) -> match hh: $3060<$3063,$3064>.opop: ($3060<$3063,$3064>) -> $3059 clause0<$3058,$3060,$3063,$3064> Clause0std/core/hnd/Clause0: forall<a,b,e,c> (clause : (marker<e,c>, ev<b>) -> e a) -> clause0<a,b,e,c>(ff: (marker<$3063,$3064>, ev<$3060>) -> $3063 $3058) -> cast-clause0std/core/hnd/cast-clause0: (f : (marker<$3063,$3064>, ev<$3060>) -> $3063 $3058) -> $3059 ((marker<$3063,$3064>, ev<$3060>) -> $3059 $3058)(ff: (marker<$3063,$3064>, ev<$3060>) -> $3063 $3058)(mm: marker<$3063,$3064>,evev: ev<$3060>) inline fun under0std/core/hnd/under0: forall<a,e,b> (ev : ev<b>, op : () -> e a) -> e a( evev: ev<$8719> : evstd/core/hnd/ev: ((E, V) -> V) -> V<ii: (E, V) -> V>, opop: () -> $8718 $8717 : () -> ee: E bb: V)result: -> 8790 8789 : ee: E bb: V val w0w0: evv<_8727> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$8719>) -> $8718 evv<_8727>(evev: ev<$8719>) val yy: $8717 = opop: () -> $8718 $8717() // evv-set(w0) // only needed before yielding for evidence expected check in prompt evv-setstd/core/hnd/evv-set: (w : evv<_8727>) -> $8718 ()(w0w0: evv<_8727>) if yieldingstd/core/hnd/yielding: () -> $8718 bool() returnreturn: $8717 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $8718 $8717, a) -> $8718 $8717) -> $8718 $8717( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($8754) -> $8718 $8717,resres: $8754) under1std/core/hnd/under1: (ev : ev<$8719>, op : ($8754) -> $8718 $8717, x : $8754) -> $8718 $8717(evev: ev<$8719>,contcont: ($8754) -> $8718 $8717,resres: $8754) )std/core/types/Unit: () yy: $8717 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<$6727,$6728,$6729,$6731>) -> $6728 $6731 : 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<6789,6792,6790,6793> : 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<$6728,$6731>, ev<$6730>) -> $6728 $6727(mm: marker<$6728,$6731>,_ev){ yield-tostd/core/hnd/yield-to: (m : marker<$6728,$6731>, clause : ((resume-result<$6727,$6731>) -> $6728 $6731) -> $6728 $6731) -> $6728 $6727(mm: marker<$6728,$6731>, fnfn: (k : (resume-result<$6727,$6731>) -> $6728 $6731) -> $6728 $6731(kk: (resume-result<$6727,$6731>) -> $6728 $6731){ opop: (resume-context<$6727,$6728,$6729,$6731>) -> $6728 $6731(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<$6727,$6731>) -> $6728 $6731)) } ) }) /* 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: (($7372) -> $7373 $7375) -> $7373 $7375 : (bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause0<7432,7434,7433,7435> : 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<$7373,$7375>, ev<$7374>) -> $7373 $7372(mm: marker<$7373,$7375>,_ev){ yield-tostd/core/hnd/yield-to: (m : marker<$7373,$7375>, clause : ((resume-result<$7372,$7375>) -> $7373 $7375) -> $7373 $7375) -> $7373 $7372(mm: marker<$7373,$7375>, fnfn: (k : (resume-result<$7372,$7375>) -> $7373 $7375) -> $7373 $7375(kk: (resume-result<$7372,$7375>) -> $7373 $7375){ protectstd/core/hnd/protect: (x : (), clause : (x : (), k : ($7372) -> $7373 $7375) -> $7373 $7375, k : (resume-result<$7372,$7375>) -> $7373 $7375) -> $7373 $7375((std/core/types/Unit: ())std/core/types/Unit: (),fnfn: ((), r : ($7372) -> $7373 $7375) -> $7373 $7375(_x,rr: ($7372) -> $7373 $7375){ opop: (($7372) -> $7373 $7375) -> $7373 $7375(rr: ($7372) -> $7373 $7375) }, kk: (resume-result<$7372,$7375>) -> $7373 $7375) }) }) 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: () -> $8801 $8804 : () -> ee: E bb: V)result: -> total clause0<8846,8845,8843,8844> : 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<$8801,$8802>, ev : ev<$8803>) -> $8801 $8804(_m,evev: ev<$8803>){ under0std/core/hnd/under0: (ev : ev<$8803>, op : () -> $8801 $8804) -> $8801 $8804(evev: ev<$8803>,opop: () -> $8801 $8804) }) 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: () -> $3767 $3770 : () -> ee: E bb: V)result: -> total clause0<3801,3800,3798,3799> : 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<$3767,$3768>, ev<$3769>) -> $3767 $3770(_m,_ev){ opop: () -> $3767 $3770() }) pub fun clause-valuestd/core/hnd/clause-value: forall<a,e,b,c> (v : a) -> clause0<a,b,e,c>(vv: $3981 : bb: V)result: -> total clause0<4012,4014,4013,4015> : 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<$3982,$3984>, ev<$3983>) -> $3982 $3981(_m,_ev){ vv: $3981 }) pub fun clause-never0std/core/hnd/clause-never0: forall<a,e,b,c> (op : () -> e c) -> clause0<a,b,e,c>( opop: () -> $7954 $7956 : () -> ee: E rr: V )result: -> total clause0<7999,8001,8000,8002> : 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<$7954,$7956>, ev<$7955>) -> $7954 $7953(mm: marker<$7954,$7956>,_ev){ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$7954,$7956>, clause : ((resume-result<$7953,$7956>) -> $7954 $7956) -> $7954 $7956) -> $7954 $7953(mm: marker<$7954,$7956>, fnfn: ((resume-result<$7953,$7956>) -> $7954 $7956) -> $7954 $7956(_k){ opop: () -> $7954 $7956() }) }) //---------------------------------------------------------------- // 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<$8937> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($8933, $8934) -> $8936 $8935 : (a1a1: V,a2a2: V) -> ee: E bb: V, x1x1: $8933 : a1a1: V, x2x2: $8934 : a2a2: V )result: -> 9016 9015 : ee: E bb: V val w0w0: evv<_8945> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$8937>) -> $8936 evv<_8945>(evev: ev<$8937>) val zz: $8935 = opop: ($8933, $8934) -> $8936 $8935(x1x1: $8933,x2x2: $8934) evv-setstd/core/hnd/evv-set: (w : evv<_8945>) -> $8936 ()(w0w0: evv<_8945>) if yieldingstd/core/hnd/yielding: () -> $8936 bool() returnreturn: $8935 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $8936 $8935, a) -> $8936 $8935) -> $8936 $8935( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($8974) -> $8936 $8935,resres: $8974) under1std/core/hnd/under1: (ev : ev<$8937>, op : ($8974) -> $8936 $8935, x : $8974) -> $8936 $8935(evev: ev<$8937>,contcont: ($8974) -> $8936 $8935,resres: $8974) )std/core/types/Unit: () zz: $8935 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: $7534 : a1a1: V, x2x2: $7535:a2a2: V, clauseclause: (x : $7534, x : $7535, k : ($7536) -> $7537 $7538) -> $7537 $7538 : (x:a1a1: V,x:a2a2: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V, kk: (resume-result<$7536,$7538>) -> $7537 $7538 : resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V )result: -> 7662 7663 : ee: E rr: V val resumedresumed: ref<global,bool> = (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$7537> ref<global,bool>) -> $7537 (() -> $7537 ref<global,bool>){refstd/core/types/ref: (value : bool) -> <alloc<global>,read<global>,write<global>|$7537> ref<global,bool>(Falsestd/core/types/False: bool)})() fun kprotectkprotect: (ret : $7536) -> $7537 $7538(retret: $7536)result: -> $7537 $7538 (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$7537> ()) -> $7537 (() -> $7537 ()){ resumedresumed: ref<global,bool> :=std/core/types/set: (ref : ref<global,bool>, assigned : bool) -> <write<global>,alloc<global>,read<global>|$7537> () Truestd/core/types/True: bool })() kk: (resume-result<$7536,$7538>) -> $7537 $7538(Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(retret: $7536)) val resres: $7538 = clauseclause: (x : $7534, x : $7535, k : ($7536) -> $7537 $7538) -> $7537 $7538(x1x1: $7534,x2x2: $7535,kprotectkprotect: (ret : $7536) -> $7537 $7538) if yieldingstd/core/hnd/yielding: () -> $7537 bool() returnreturn: $7538 yield-extendstd/core/hnd/yield-extend: (next : ($7538) -> $7537 $7538) -> $7537 $7538( fnfn: (xres : $7538) -> $7537 $7538(xresxres: $7538) protect-checkstd/core/hnd/protect-check: (resumed : ref<global,bool>, k : (resume-result<$7536,$7538>) -> $7537 $7538, res : $7538) -> $7537 $7538(resumedresumed: ref<global,bool>,kk: (resume-result<$7536,$7538>) -> $7537 $7538,xresxres: $7538) )std/core/types/Unit: () protect-checkstd/core/hnd/protect-check: (resumed : ref<global,bool>, k : (resume-result<$7536,$7538>) -> $7537 $7538, res : $7538) -> $7537 $7538(resumedresumed: ref<global,bool>,kk: (resume-result<$7536,$7538>) -> $7537 $7538,resres: $7538) 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 : $7679, x2 : $7680, k : ($7681) -> $7682 $7684) -> $7682 $7684 : (x1:a1a1: V, x2:a2a2: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause2<7753,7754,7755,7757,7756,7758> : 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<$7682,$7684>, ev<$7683>, x1 : $7679, x2 : $7680) -> $7682 $7681(mm: marker<$7682,$7684>,_ev,x1x1: $7679,x2x2: $7680){ yield-tostd/core/hnd/yield-to: (m : marker<$7682,$7684>, clause : ((resume-result<$7681,$7684>) -> $7682 $7684) -> $7682 $7684) -> $7682 $7681(mm: marker<$7682,$7684>, fnfn: (k : (resume-result<$7681,$7684>) -> $7682 $7684) -> $7682 $7684(kk: (resume-result<$7681,$7684>) -> $7682 $7684){ protect2std/core/hnd/protect2: (x1 : $7679, x2 : $7680, clause : (x : $7679, x : $7680, k : ($7681) -> $7682 $7684) -> $7682 $7684, k : (resume-result<$7681,$7684>) -> $7682 $7684) -> $7682 $7684(x1x1: $7679,x2x2: $7680,clauseclause: (x1 : $7679, x2 : $7680, k : ($7681) -> $7682 $7684) -> $7682 $7684,kk: (resume-result<$7681,$7684>) -> $7682 $7684) }) }) 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 : $6904, x2 : $6905, r : resume-context<$6906,$6907,$6908,$6910>) -> $6907 $6910 : (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<6980,6981,6982,6985,6983,6986> : 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<$6907,$6910>, ev<$6909>, x1 : $6904, x2 : $6905) -> $6907 $6906(mm: marker<$6907,$6910>,_ev,x1x1: $6904,x2x2: $6905){ yield-tostd/core/hnd/yield-to: (m : marker<$6907,$6910>, clause : ((resume-result<$6906,$6910>) -> $6907 $6910) -> $6907 $6910) -> $6907 $6906(mm: marker<$6907,$6910>, fnfn: (k : (resume-result<$6906,$6910>) -> $6907 $6910) -> $6907 $6910(kk: (resume-result<$6906,$6910>) -> $6907 $6910){ opop: (x1 : $6904, x2 : $6905, r : resume-context<$6906,$6907,$6908,$6910>) -> $6907 $6910(x1x1: $6904,x2x2: $6905,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<$6906,$6910>) -> $6907 $6910)) } ) }) 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: ($9036, $9037) -> $9033 $9038 : (a1a1: V,a2a2: V) -> ee: E bb: V)result: -> total clause2<9098,9099,9100,9097,9095,9096> : 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<$9033,$9034>, ev : ev<$9035>, x1 : $9036, x2 : $9037) -> $9033 $9038(mm: marker<$9033,$9034>,evev: ev<$9035>,x1x1: $9036,x2x2: $9037){ under2std/core/hnd/under2: (ev : ev<$9035>, op : ($9036, $9037) -> $9033 $9038, x1 : $9036, x2 : $9037) -> $9033 $9038(evev: ev<$9035>,opop: ($9036, $9037) -> $9033 $9038,x1x1: $9036,x2x2: $9037) }) 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: ($3877, $3878) -> $3874 $3879 : (a1a1: V,a2a2: V) -> ee: E bb: V)result: -> total clause2<3922,3923,3924,3921,3919,3920> : 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<$3874,$3875>, ev<$3876>, x1 : $3877, x2 : $3878) -> $3874 $3879(_m,_ev,x1x1: $3877,x2x2: $3878){ opop: ($3877, $3878) -> $3874 $3879(x1x1: $3877,x2x2: $3878) }) pub inline fun @perform2( evxevx: ev<$3220> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($3220<e,a>) -> clause2<$3216,$3217,$3218,$3220,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: $3216 : aa: V, yy: $3217 : bb: V )result: -> 3294 3293 : ee: E cc: V match evxevx: ev<$3220> 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<$3223,$3224>,hh: $3220<$3223,$3224>,_w) -> match hh: $3220<$3223,$3224>.opop: ($3220<$3223,$3224>) -> $3219 clause2<$3216,$3217,$3218,$3220,$3223,$3224> 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<$3223,$3224>, ev<$3220>, $3216, $3217) -> $3223 $3218) -> cast-clause2std/core/hnd/cast-clause2: (f : (marker<$3223,$3224>, ev<$3220>, $3216, $3217) -> $3223 $3218) -> $3219 ((marker<$3223,$3224>, ev<$3220>, $3216, $3217) -> $3219 $3218)(ff: (marker<$3223,$3224>, ev<$3220>, $3216, $3217) -> $3223 $3218)(mm: marker<$3223,$3224>,evxevx: ev<$3220>,xx: $3216,yy: $3217) 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: ($8090, $8091) -> $8093 $8095 : (a1a1: V,a2a2: V) -> ee: E rr: V )result: -> total clause2<8150,8151,8152,8154,8153,8155> : 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<$8093,$8095>, ev<$8094>, x1 : $8090, x2 : $8091) -> $8093 $8092(mm: marker<$8093,$8095>,_ev,x1x1: $8090,x2x2: $8091){ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$8093,$8095>, clause : ((resume-result<$8092,$8095>) -> $8093 $8095) -> $8093 $8095) -> $8093 $8092(mm: marker<$8093,$8095>, fnfn: ((resume-result<$8092,$8095>) -> $8093 $8095) -> $8093 $8095(_k){ opop: ($8090, $8091) -> $8093 $8095(x1x1: $8090,x2x2: $8091) }) }) //---------------------------------------------------------------- // 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<$3638> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($3638<e,a>) -> clause1<$3635,$3636,$3638,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: $3635 : aa: V )result: -> 3704 3703 : ee: E bb: V match evev: ev<$3638> 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<$3641,$3642>,hh: $3638<$3641,$3642>,_w) -> match hh: $3638<$3641,$3642>.opop: ($3638<$3641,$3642>) -> $3637 clause1<$3635,$3636,$3638,$3641,$3642> 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<$3641,$3642>, ev<$3638>, $3635) -> $3641 $3636) -> cast-clause1std/core/hnd/cast-clause1: (f : (marker<$3641,$3642>, ev<$3638>, $3635) -> $3641 $3636) -> $3637 ((marker<$3641,$3642>, ev<$3638>, $3635) -> $3637 $3636)(ff: (marker<$3641,$3642>, ev<$3638>, $3635) -> $3641 $3636)(mm: marker<$3641,$3642>,evev: ev<$3638>,xx: $3635) 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 : $7009, x2 : $7010, x3 : $7011, r : resume-context<$7012,$7013,$7014,$7016>) -> $7013 $7016 : (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<(7069, 7070, 7071),7072,7075,7073,7076> : 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 : ($7009, $7010, $7011), r : resume-context<$7012,$7013,$7014,$7016>) -> $7013 $7016) -> clause1<($7009, $7010, $7011),$7012,$7015,$7013,$7016>( fnfn: (($7009, $7010, $7011), r : resume-context<$7012,$7013,$7014,$7016>) -> $7013 $7016((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $7009,x2x2: $7010,x3x3: $7011)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c),rr: resume-context<$7012,$7013,$7014,$7016>){ opop: (x1 : $7009, x2 : $7010, x3 : $7011, r : resume-context<$7012,$7013,$7014,$7016>) -> $7013 $7016(x1x1: $7009,x2x2: $7010,x3x3: $7011,rr: resume-context<$7012,$7013,$7014,$7016>) } ) 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 : $7778, x2 : $7779, x3 : $7780, k : ($7781) -> $7782 $7784) -> $7782 $7784 : (x1:a1a1: V, x2:a2a2: V, x3:a3a3: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause1<(7832, 7833, 7834),7835,7837,7836,7838> : 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 : ($7778, $7779, $7780), k : ($7781) -> $7782 $7784) -> $7782 $7784) -> clause1<($7778, $7779, $7780),$7781,$7783,$7782,$7784>( fnfn: (($7778, $7779, $7780), k : ($7781) -> $7782 $7784) -> $7782 $7784((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $7778,x2x2: $7779,x3x3: $7780)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c),kk: ($7781) -> $7782 $7784){ opop: (x1 : $7778, x2 : $7779, x3 : $7780, k : ($7781) -> $7782 $7784) -> $7782 $7784(x1x1: $7778,x2x2: $7779,x3x3: $7780,kk: ($7781) -> $7782 $7784) } ) 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: ($9123, $9124, $9125) -> $9120 $9126 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E bb: V)result: -> total clause1<(9176, 9177, 9178),9179,9175,9173,9174> : 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 : (($9123, $9124, $9125)) -> $9120 $9126) -> clause1<($9123, $9124, $9125),$9126,$9122,$9120,$9121>( fnfn: (($9123, $9124, $9125)) -> $9120 $9126((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $9123,x2x2: $9124,x3x3: $9125)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) ){ opop: ($9123, $9124, $9125) -> $9120 $9126(x1x1: $9123,x2x2: $9124,x3x3: $9125) } ) 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: ($8351, $8352, $8353) -> $8348 $8354 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E bb: V)result: -> total clause1<(8404, 8405, 8406),8407,8403,8401,8402> : 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 : (($8351, $8352, $8353)) -> $8348 $8354) -> clause1<($8351, $8352, $8353),$8354,$8350,$8348,$8349>( fnfn: (($8351, $8352, $8353)) -> $8348 $8354((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8351,x2x2: $8352,x3x3: $8353)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)){ opop: ($8351, $8352, $8353) -> $8348 $8354(x1x1: $8351,x2x2: $8352,x3x3: $8353) } ) 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: ($8175, $8176, $8177) -> $8179 $8181 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E rr: V )result: -> total clause1<(8228, 8229, 8230),8231,8233,8232,8234> : 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 : (($8175, $8176, $8177)) -> $8179 $8181) -> clause1<($8175, $8176, $8177),$8178,$8180,$8179,$8181>(fnfn: (($8175, $8176, $8177)) -> $8179 $8181((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8175,x2x2: $8176,x3x3: $8177)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)){ opop: ($8175, $8176, $8177) -> $8179 $8181(x1x1: $8175,x2x2: $8176,x3x3: $8177) } ) pub fun @perform3( evev: ev<$6481> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($6481<e,a>) -> clause1<($6476, $6477, $6478),$6479,$6481,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: $6476 : a1a1: V, x2x2: $6477 : a2a2: V, x3x3: $6478 : a3a3: V )result: -> 6547 6546 : ee: E bb: V xperform1std/core/hnd/xperform1: (ev : ev<$6481>, op : forall<e,a> ($6481<e,a>) -> clause1<($6476, $6477, $6478),$6479,$6481,e,a>, x : ($6476, $6477, $6478)) -> $6480 $6479(evev: ev<$6481>,opop: forall<e,a> ($6481<e,a>) -> clause1<($6476, $6477, $6478),$6479,$6481,e,a>,(std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $6476,x2x2: $6477,x3x3: $6478)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<$9971> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($9966, $9967, $9968) -> $9970 $9969 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E bb: V, x1x1: $9966 : a1a1: V, x2x2: $9967 : a2a2: V, x3x3: $9968 : a3a3: V )result: -> 10054 10053 : ee: E bb: V val w0w0: evv<_9979> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$9971>) -> $9970 evv<_9979>(evev: ev<$9971>) val zz: $9969 = opop: ($9966, $9967, $9968) -> $9970 $9969(x1x1: $9966,x2x2: $9967,x3x3: $9968) evv-setstd/core/hnd/evv-set: (w : evv<_9979>) -> $9970 ()(w0w0: evv<_9979>) if yieldingstd/core/hnd/yielding: () -> $9970 bool() returnreturn: $9969 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $9970 $9969, a) -> $9970 $9969) -> $9970 $9969( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($10009) -> $9970 $9969,resres: $10009) under1std/core/hnd/under1: (ev : ev<$9971>, op : ($10009) -> $9970 $9969, x : $10009) -> $9970 $9969(evev: ev<$9971>,contcont: ($10009) -> $9970 $9969,resres: $10009) )std/core/types/Unit: () zz: $9969 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 : $7861, x2 : $7862, x3 : $7863, x4 : $7864, k : ($7865) -> $7866 $7868) -> $7866 $7868 : (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<(7920, 7921, 7922, 7923),7924,7926,7925,7927> : 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 : ($7861, $7862, $7863, $7864), k : ($7865) -> $7866 $7868) -> $7866 $7868) -> clause1<($7861, $7862, $7863, $7864),$7865,$7867,$7866,$7868>( fnfn: (($7861, $7862, $7863, $7864), k : ($7865) -> $7866 $7868) -> $7866 $7868((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $7861,x2x2: $7862,x3x3: $7863,x4x4: $7864)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d),kk: ($7865) -> $7866 $7868){ opop: (x1 : $7861, x2 : $7862, x3 : $7863, x4 : $7864, k : ($7865) -> $7866 $7868) -> $7866 $7868(x1x1: $7861,x2x2: $7862,x3x3: $7863,x4x4: $7864,kk: ($7865) -> $7866 $7868) } ) 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: ($9205, $9206, $9207, $9208) -> $9202 $9209 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E bb: V)result: -> total clause1<(9263, 9264, 9265, 9266),9267,9262,9260,9261> : 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 : (($9205, $9206, $9207, $9208)) -> $9202 $9209) -> clause1<($9205, $9206, $9207, $9208),$9209,$9204,$9202,$9203>( fnfn: (($9205, $9206, $9207, $9208)) -> $9202 $9209((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9205,x2x2: $9206,x3x3: $9207,x4x4: $9208)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)){ opop: ($9205, $9206, $9207, $9208) -> $9202 $9209(x1x1: $9205,x2x2: $9206,x3x3: $9207,x4x4: $9208) } ) 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: ($8433, $8434, $8435, $8436) -> $8430 $8437 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E bb: V)result: -> total clause1<(8491, 8492, 8493, 8494),8495,8490,8488,8489> : 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 : (($8433, $8434, $8435, $8436)) -> $8430 $8437) -> clause1<($8433, $8434, $8435, $8436),$8437,$8432,$8430,$8431>( fnfn: (($8433, $8434, $8435, $8436)) -> $8430 $8437((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $8433,x2x2: $8434,x3x3: $8435,x4x4: $8436)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)){ opop: ($8433, $8434, $8435, $8436) -> $8430 $8437(x1x1: $8433,x2x2: $8434,x3x3: $8435,x4x4: $8436) } ) 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: ($8257, $8258, $8259, $8260) -> $8262 $8264 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E rr: V )result: -> total clause1<(8315, 8316, 8317, 8318),8319,8321,8320,8322> : 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 : (($8257, $8258, $8259, $8260)) -> $8262 $8264) -> clause1<($8257, $8258, $8259, $8260),$8261,$8263,$8262,$8264>(fnfn: (($8257, $8258, $8259, $8260)) -> $8262 $8264((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $8257,x2x2: $8258,x3x3: $8259,x4x4: $8260)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)){ opop: ($8257, $8258, $8259, $8260) -> $8262 $8264(x1x1: $8257,x2x2: $8258,x3x3: $8259,x4x4: $8260) } ) pub fun @perform4( evev: ev<$6575> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($6575<e,a>) -> clause1<($6569, $6570, $6571, $6572),$6573,$6575,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: $6569 : a1a1: V, x2x2: $6570 : a2a2: V, x3x3: $6571 : a3a3: V, x4x4: $6572 : a4a4: V )result: -> 6648 6647 : ee: E bb: V xperform1std/core/hnd/xperform1: (ev : ev<$6575>, op : forall<e,a> ($6575<e,a>) -> clause1<($6569, $6570, $6571, $6572),$6573,$6575,e,a>, x : ($6569, $6570, $6571, $6572)) -> $6574 $6573(evev: ev<$6575>,opop: forall<e,a> ($6575<e,a>) -> clause1<($6569, $6570, $6571, $6572),$6573,$6575,e,a>,(std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $6569,x2x2: $6570,x3x3: $6571,x4x4: $6572)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<$10080> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($10074, $10075, $10076, $10077) -> $10079 $10078 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E bb: V, x1x1: $10074 : a1a1: V, x2x2: $10075 : a2a2: V, x3x3: $10076 : a3a3: V, x4x4: $10077 : a4a4: V )result: -> 10167 10166 : ee: E bb: V val w0w0: evv<_10088> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$10080>) -> $10079 evv<_10088>(evev: ev<$10080>) val zz: $10078 = opop: ($10074, $10075, $10076, $10077) -> $10079 $10078(x1x1: $10074,x2x2: $10075,x3x3: $10076,x4x4: $10077) evv-setstd/core/hnd/evv-set: (w : evv<_10088>) -> $10079 ()(w0w0: evv<_10088>) if yieldingstd/core/hnd/yielding: () -> $10079 bool() returnreturn: $10078 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10079 $10078, a) -> $10079 $10078) -> $10079 $10078( fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($10119) -> $10079 $10078,resres: $10119) under1std/core/hnd/under1: (ev : ev<$10080>, op : ($10119) -> $10079 $10078, x : $10119) -> $10079 $10078(evev: ev<$10080>,contcont: ($10119) -> $10079 $10078,resres: $10119) )std/core/types/Unit: () zz: $10078 // ------------------------------------------- // Open // ------------------------------------------- pub fun @open-none0<bb: V,e1e1: E,e2e2: E>( ff: () -> $2709 $2708 : () -> e1e1: E bb: V )result: -> 2746 2744 : e2e2: E bb: V val ww: evv<$2710> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $2710 evv<$2710>() val xx: $2708 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $2709 $2708) -> $2710 (() -> $2710 $2708)(ff: () -> $2709 $2708)() val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$2710>) -> $2710 ()(ww: evv<$2710>) xx: $2708 pub fun @open-none1<aa: V,bb: V,e1e1: E,e2e2: E>( ff: ($2756) -> $2758 $2757 : aa: V -> e1e1: E bb: V, x1x1: $2756 : aa: V )result: -> 2802 2800 : e2e2: E bb: V val ww: evv<$2759> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $2759 evv<$2759>() val xx: $2757 = cast-ev1std/core/hnd/cast-ev1: (f : ($2756) -> $2758 $2757) -> $2759 (($2756) -> $2759 $2757)(ff: ($2756) -> $2758 $2757)(x1x1: $2756) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$2759>) -> $2759 ()(ww: evv<$2759>) xx: $2757 pub fun @open-none2<a1a1: V,a2a2: V,bb: V,e1e1: E,e2e2: E>( ff: ($2815, $2816) -> $2818 $2817 : (a1a1: V,a2a2: V) -> e1e1: E bb: V, x1x1: $2815 : a1a1: V, x2x2: $2816 : a2a2: V )result: -> 2869 2867 : e2e2: E bb: V val ww: evv<$2819> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $2819 evv<$2819>() val xx: $2817 = cast-ev2std/core/hnd/cast-ev2: (f : ($2815, $2816) -> $2818 $2817) -> $2819 (($2815, $2816) -> $2819 $2817)(ff: ($2815, $2816) -> $2818 $2817)(x1x1: $2815,x2x2: $2816) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$2819>) -> $2819 ()(ww: evv<$2819>) xx: $2817 pub fun @open-none3<a1a1: V,a2a2: V,a3a3: V,bb: V,e1e1: E,e2e2: E>( ff: ($2885, $2886, $2887) -> $2889 $2888 : (a1a1: V,a2a2: V,a3a3: V) -> e1e1: E bb: V, x1x1: $2885 : a1a1: V, x2x2: $2886 : a2a2: V, x3x3: $2887 : a3a3: V )result: -> 2947 2945 : e2e2: E bb: V val ww: evv<$2890> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $2890 evv<$2890>() val xx: $2888 = cast-ev3std/core/hnd/cast-ev3: (f : ($2885, $2886, $2887) -> $2889 $2888) -> $2890 (($2885, $2886, $2887) -> $2890 $2888)(ff: ($2885, $2886, $2887) -> $2889 $2888)(x1x1: $2885,x2x2: $2886,x3x3: $2887) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$2890>) -> $2890 ()(ww: evv<$2890>) xx: $2888 pub fun @open-none4<a1a1: V,a2a2: V,a3a3: V,a4a4: V,bb: V,e1e1: E,e2e2: E>( ff: ($2966, $2967, $2968, $2969) -> $2971 $2970 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e1e1: E bb: V, x1x1: $2966 : a1a1: V, x2x2: $2967 : a2a2: V, x3x3: $2968 : a3a3: V, x4x4: $2969 : a4a4: V )result: -> 3036 3034 : e2e2: E bb: V val ww: evv<$2972> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $2972 evv<$2972>() val xx: $2970 = cast-ev4std/core/hnd/cast-ev4: (f : ($2966, $2967, $2968, $2969) -> $2971 $2970) -> $2972 (($2966, $2967, $2968, $2969) -> $2972 $2970)(ff: ($2966, $2967, $2968, $2969) -> $2971 $2970)(x1x1: $2966,x2x2: $2967,x3x3: $2968,x4x4: $2969) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$2972>) -> $2972 ()(ww: evv<$2972>) xx: $2970 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: ($5130) -> $5132 $5131 : aa: V -> e1e1: E bb: V, xx: $5130 : aa: V )result: -> 5225 5223 : e2e2: E bb: V val ww: evv<$5133> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $5133 evv<$5133>(ii: ev-index) val yy: $5131 = cast-ev1std/core/hnd/cast-ev1: (f : ($5130) -> $5132 $5131) -> $5133 (($5130) -> $5133 $5131)(ff: ($5130) -> $5132 $5131)(xx: $5130) evv-setstd/core/hnd/evv-set: (w : evv<$5133>) -> $5133 ()(ww: evv<$5133>) if yieldingstd/core/hnd/yielding: () -> $5133 bool() returnreturn: $5131 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5133 $5131, a) -> $5133 $5131) -> $5133 $5131(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($5179) -> $5133 $5131,resres: $5179){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($5179) -> $5133 $5131, x : $5179) -> $5133 $5131(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev-index) -> $5133 ev-index(ii: ev-index),contcont: ($5179) -> $5133 $5131,resres: $5179) })std/core/types/Unit: () yy: $5131 pub fun @open-at0<bb: V,e1e1: E,e2e2: E>( ii: ev-index: ev-indexstd/core/hnd/ev-index: V, ff: () -> $5239 $5238 : () -> e1e1: E bb: V )result: -> 5319 5317 : e2e2: E bb: V val ww: evv<$5240> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $5240 evv<$5240>(ii: ev-index) val yy: $5238 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $5239 $5238) -> $5240 (() -> $5240 $5238)(ff: () -> $5239 $5238)() evv-setstd/core/hnd/evv-set: (w : evv<$5240>) -> $5240 ()(ww: evv<$5240>) if yieldingstd/core/hnd/yielding: () -> $5240 bool() returnreturn: $5238 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5240 $5238, a) -> $5240 $5238) -> $5240 $5238(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($5282) -> $5240 $5238,resres: $5282){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($5282) -> $5240 $5238, x : $5282) -> $5240 $5238(ii: ev-index,contcont: ($5282) -> $5240 $5238,resres: $5282) })std/core/types/Unit: () yy: $5238 pub fun @open-at1<aa: V,bb: V,e1e1: E,e2e2: E>( ii: ev-index: ev-indexstd/core/hnd/ev-index: V, ff: ($5329) -> $5331 $5330 : aa: V -> e1e1: E bb: V, xx: $5329 : aa: V )result: -> 5418 5416 : e2e2: E bb: V val ww: evv<$5332> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $5332 evv<$5332>(ii: ev-index) val yy: $5330 = cast-ev1std/core/hnd/cast-ev1: (f : ($5329) -> $5331 $5330) -> $5332 (($5329) -> $5332 $5330)(ff: ($5329) -> $5331 $5330)(xx: $5329) evv-setstd/core/hnd/evv-set: (w : evv<$5332>) -> $5332 ()(ww: evv<$5332>) if yieldingstd/core/hnd/yielding: () -> $5332 bool() returnreturn: $5330 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5332 $5330, a) -> $5332 $5330) -> $5332 $5330(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($5378) -> $5332 $5330,resres: $5378){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($5378) -> $5332 $5330, x : $5378) -> $5332 $5330(ii: ev-index,contcont: ($5378) -> $5332 $5330,resres: $5378) })std/core/types/Unit: () yy: $5330 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: ($5431, $5432) -> $5434 $5433 : (a1a1: V,a2a2: V) -> e1e1: E bb: V, x1x1: $5431 : a1a1: V, x2x2: $5432 : a2a2: V )result: -> 5528 5526 : e2e2: E bb: V val ww: evv<$5435> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $5435 evv<$5435>(ii: ev-index) val yy: $5433 = cast-ev2std/core/hnd/cast-ev2: (f : ($5431, $5432) -> $5434 $5433) -> $5435 (($5431, $5432) -> $5435 $5433)(ff: ($5431, $5432) -> $5434 $5433)(x1x1: $5431,x2x2: $5432) evv-setstd/core/hnd/evv-set: (w : evv<$5435>) -> $5435 ()(ww: evv<$5435>) if yieldingstd/core/hnd/yielding: () -> $5435 bool() returnreturn: $5433 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5435 $5433, a) -> $5435 $5433) -> $5435 $5433(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($5485) -> $5435 $5433,resres: $5485){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($5485) -> $5435 $5433, x : $5485) -> $5435 $5433(ii: ev-index,contcont: ($5485) -> $5435 $5433,resres: $5485) })std/core/types/Unit: () yy: $5433 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: ($5544, $5545, $5546) -> $5548 $5547 : (a1a1: V,a2a2: V,a3a3: V) -> e1e1: E bb: V, x1x1: $5544 : a1a1: V, x2x2: $5545 : a2a2: V, x3x3: $5546 : a3a3: V )result: -> 5649 5647 : e2e2: E bb: V val ww: evv<$5549> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $5549 evv<$5549>(ii: ev-index) val yy: $5547 = cast-ev3std/core/hnd/cast-ev3: (f : ($5544, $5545, $5546) -> $5548 $5547) -> $5549 (($5544, $5545, $5546) -> $5549 $5547)(ff: ($5544, $5545, $5546) -> $5548 $5547)(x1x1: $5544,x2x2: $5545,x3x3: $5546) evv-setstd/core/hnd/evv-set: (w : evv<$5549>) -> $5549 ()(ww: evv<$5549>) if yieldingstd/core/hnd/yielding: () -> $5549 bool() returnreturn: $5547 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5549 $5547, a) -> $5549 $5547) -> $5549 $5547(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($5603) -> $5549 $5547,resres: $5603){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($5603) -> $5549 $5547, x : $5603) -> $5549 $5547(ii: ev-index,contcont: ($5603) -> $5549 $5547,resres: $5603) })std/core/types/Unit: () yy: $5547 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: ($5668, $5669, $5670, $5671) -> $5673 $5672 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e1e1: E bb: V, x1x1: $5668 : a1a1: V, x2x2: $5669 : a2a2: V, x3x3: $5670 : a3a3: V, x4x4: $5671 : a4a4: V )result: -> 5781 5779 : e2e2: E bb: V val ww: evv<$5674> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $5674 evv<$5674>(ii: ev-index) val yy: $5672 = cast-ev4std/core/hnd/cast-ev4: (f : ($5668, $5669, $5670, $5671) -> $5673 $5672) -> $5674 (($5668, $5669, $5670, $5671) -> $5674 $5672)(ff: ($5668, $5669, $5670, $5671) -> $5673 $5672)(x1x1: $5668,x2x2: $5669,x3x3: $5670,x4x4: $5671) evv-setstd/core/hnd/evv-set: (w : evv<$5674>) -> $5674 ()(ww: evv<$5674>) if yieldingstd/core/hnd/yielding: () -> $5674 bool() returnreturn: $5672 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5674 $5672, a) -> $5674 $5672) -> $5674 $5672(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($5732) -> $5674 $5672,resres: $5732){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($5732) -> $5674 $5672, x : $5732) -> $5674 $5672(ii: ev-index,contcont: ($5732) -> $5674 $5672,resres: $5732) })std/core/types/Unit: () yy: $5672 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: ($5803) -> $5805 $5804 : aa: V -> e1e1: E bb: V, xx: $5803 : aa: V )result: -> 5898 5896 : e2e2: E bb: V val ww: evv<$5806> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $5806 evv<$5806>(indicesindices: vector<ev-index>) val yy: $5804 = cast-ev1std/core/hnd/cast-ev1: (f : ($5803) -> $5805 $5804) -> $5806 (($5803) -> $5806 $5804)(ff: ($5803) -> $5805 $5804)(xx: $5803) evv-setstd/core/hnd/evv-set: (w : evv<$5806>) -> $5806 ()(ww: evv<$5806>) if yieldingstd/core/hnd/yielding: () -> $5806 bool() returnreturn: $5804 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5806 $5804, a) -> $5806 $5804) -> $5806 $5804(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($5852) -> $5806 $5804,resres: $5852){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($5852) -> $5806 $5804, x : $5852) -> $5806 $5804(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : vector<ev-index>) -> $5806 vector<ev-index>(indicesindices: vector<ev-index>),contcont: ($5852) -> $5806 $5804,resres: $5852) })std/core/types/Unit: () yy: $5804 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: () -> $5912 $5911 : () -> e1e1: E bb: V )result: -> 5992 5990 : e2e2: E bb: V val ww: evv<$5913> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $5913 evv<$5913>(indicesindices: vector<ev-index>) val yy: $5911 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $5912 $5911) -> $5913 (() -> $5913 $5911)(ff: () -> $5912 $5911)() evv-setstd/core/hnd/evv-set: (w : evv<$5913>) -> $5913 ()(ww: evv<$5913>) if yieldingstd/core/hnd/yielding: () -> $5913 bool() returnreturn: $5911 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5913 $5911, a) -> $5913 $5911) -> $5913 $5911(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($5955) -> $5913 $5911,resres: $5955){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($5955) -> $5913 $5911, x : $5955) -> $5913 $5911(indicesindices: vector<ev-index>,contcont: ($5955) -> $5913 $5911,resres: $5955) })std/core/types/Unit: () yy: $5911 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: ($6002) -> $6004 $6003 : aa: V -> e1e1: E bb: V, xx: $6002 : aa: V )result: -> 6091 6089 : e2e2: E bb: V val ww: evv<$6005> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $6005 evv<$6005>(indicesindices: vector<ev-index>) val yy: $6003 = cast-ev1std/core/hnd/cast-ev1: (f : ($6002) -> $6004 $6003) -> $6005 (($6002) -> $6005 $6003)(ff: ($6002) -> $6004 $6003)(xx: $6002) evv-setstd/core/hnd/evv-set: (w : evv<$6005>) -> $6005 ()(ww: evv<$6005>) if yieldingstd/core/hnd/yielding: () -> $6005 bool() returnreturn: $6003 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $6005 $6003, a) -> $6005 $6003) -> $6005 $6003(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($6051) -> $6005 $6003,resres: $6051){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($6051) -> $6005 $6003, x : $6051) -> $6005 $6003(indicesindices: vector<ev-index>,contcont: ($6051) -> $6005 $6003,resres: $6051) })std/core/types/Unit: () yy: $6003 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: ($6104, $6105) -> $6107 $6106 : (a1a1: V,a2a2: V) -> e1e1: E bb: V, x1x1: $6104 : a1a1: V, x2x2: $6105 : a2a2: V )result: -> 6201 6199 : e2e2: E bb: V val ww: evv<$6108> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $6108 evv<$6108>(indicesindices: vector<ev-index>) val yy: $6106 = cast-ev2std/core/hnd/cast-ev2: (f : ($6104, $6105) -> $6107 $6106) -> $6108 (($6104, $6105) -> $6108 $6106)(ff: ($6104, $6105) -> $6107 $6106)(x1x1: $6104,x2x2: $6105) evv-setstd/core/hnd/evv-set: (w : evv<$6108>) -> $6108 ()(ww: evv<$6108>) if yieldingstd/core/hnd/yielding: () -> $6108 bool() returnreturn: $6106 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $6108 $6106, a) -> $6108 $6106) -> $6108 $6106(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($6158) -> $6108 $6106,resres: $6158){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($6158) -> $6108 $6106, x : $6158) -> $6108 $6106(indicesindices: vector<ev-index>,contcont: ($6158) -> $6108 $6106,resres: $6158) })std/core/types/Unit: () yy: $6106 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: ($6217, $6218, $6219) -> $6221 $6220 : (a1a1: V,a2a2: V,a3a3: V) -> e1e1: E bb: V, x1x1: $6217 : a1a1: V, x2x2: $6218 : a2a2: V, x3x3: $6219 : a3a3: V )result: -> 6322 6320 : e2e2: E bb: V val ww: evv<$6222> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $6222 evv<$6222>(indicesindices: vector<ev-index>) val yy: $6220 = cast-ev3std/core/hnd/cast-ev3: (f : ($6217, $6218, $6219) -> $6221 $6220) -> $6222 (($6217, $6218, $6219) -> $6222 $6220)(ff: ($6217, $6218, $6219) -> $6221 $6220)(x1x1: $6217,x2x2: $6218,x3x3: $6219) evv-setstd/core/hnd/evv-set: (w : evv<$6222>) -> $6222 ()(ww: evv<$6222>) if yieldingstd/core/hnd/yielding: () -> $6222 bool() returnreturn: $6220 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $6222 $6220, a) -> $6222 $6220) -> $6222 $6220(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($6276) -> $6222 $6220,resres: $6276){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($6276) -> $6222 $6220, x : $6276) -> $6222 $6220(indicesindices: vector<ev-index>,contcont: ($6276) -> $6222 $6220,resres: $6276) })std/core/types/Unit: () yy: $6220 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: ($6341, $6342, $6343, $6344) -> $6346 $6345 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e1e1: E bb: V, x1x1: $6341 : a1a1: V, x2x2: $6342 : a2a2: V, x3x3: $6343 : a3a3: V, x4x4: $6344 : a4a4: V )result: -> 6454 6452 : e2e2: E bb: V val ww: evv<$6347> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $6347 evv<$6347>(indicesindices: vector<ev-index>) val yy: $6345 = cast-ev4std/core/hnd/cast-ev4: (f : ($6341, $6342, $6343, $6344) -> $6346 $6345) -> $6347 (($6341, $6342, $6343, $6344) -> $6347 $6345)(ff: ($6341, $6342, $6343, $6344) -> $6346 $6345)(x1x1: $6341,x2x2: $6342,x3x3: $6343,x4x4: $6344) evv-setstd/core/hnd/evv-set: (w : evv<$6347>) -> $6347 ()(ww: evv<$6347>) if yieldingstd/core/hnd/yielding: () -> $6347 bool() returnreturn: $6345 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $6347 $6345, a) -> $6347 $6345) -> $6347 $6345(fnfn: forall<a,b,e> (cont : (a) -> e b, res : a) -> e b(contcont: ($6405) -> $6347 $6345,resres: $6405){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($6405) -> $6347 $6345, x : $6405) -> $6347 $6345(indicesindices: vector<ev-index>,contcont: ($6405) -> $6347 $6345,resres: $6405) })std/core/types/Unit: () yy: $6345 // ------------------------------------------- // capture yields // ------------------------------------------- pub fun unsafe-try-finalizestd/core/hnd/unsafe-try-finalize: forall<a,e> (action : () -> e a) -> e either<yield-info,a>( actionaction: () -> $10191 $10190 : () -> ee: E aa: V )result: -> 10206 either<yield-info,10205> : 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 : $10190) -> $10191 either<yield-info,$10190>(actionaction: () -> $10191 $10190()); fun try-finalize-promptstd/core/hnd/try-finalize-prompt: forall<a,e> (res : a) -> e either<yield-info,a>( resres: $9870 : aa: V )result: -> 9959 either<yield-info,9958> : 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: () -> $9871 bool() returnreturn: either<yield-info,$9870> yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $9871 $9870, a) -> $9871 either<yield-info,$9870>) -> $9871 either<yield-info,$9870>(fnfn: forall<a,b,e> (cont : (a) -> e b, x : a) -> e either<yield-info,b>(contcont: ($9887) -> $9871 $9870,xx: $9887) try-finalize-promptstd/core/hnd/try-finalize-prompt: (res : $9870) -> $9871 either<yield-info,$9870>(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : $9870) -> $9871 $9870(contcont: ($9887) -> $9871 $9870(xx: $9887))) )std/core/types/Unit: () if !std/core/types/bool/(!): (b : bool) -> $9871 boolyieldingstd/core/hnd/yielding: () -> $9871 bool() then Rightstd/core/types/Right: forall<a,b> (right : b) -> either<a,b>(resres: $9870) else Leftstd/core/types/Left: forall<a,b> (left : a) -> either<a,b>(yield-capturestd/core/hnd/yield-capture: () -> $9871 yield-info())