/*---------------------------------------------------------------------------
  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 defined (`: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 normally 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<1921> : 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<$2095,$2096>)  : 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<$2108,$2109>) : 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<$2095,$2096>, y : marker<$2108,$2109>) -> bool(m1m1: marker<$2095,$2096>,m2m2: marker<$2108,$2109>)


// -------------------------------------------
// 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<$2034,$2032> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,a1a1: V>, yy: marker<$2035,$2033> : 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<$2213> : evvstd/core/hnd/evv: E -> V<e1e1: E>, evev: ev<$2215> : 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<$2254> : 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<$2274> : evvstd/core/hnd/evv: E -> V<ee: E>, evv1evv1: evv<$2274> : 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<$2296> : htagstd/core/hnd/htag: ((E, V) -> V) -> V<hh: (E, V) -> V> ) : ee: E ev-indexstd/core/hnd/ev-index: V
  c  "kk_evv_index"
  js "__evv_index"

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

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

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

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


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

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

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

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

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

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



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

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

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

pub noinline extern yield-extendstd/core/hnd/yield-extend: forall<a,b,e> (next : (a) -> e b) -> e b(nextnext: ($2390) -> $2392 $2391 : 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: $2430 : aa: V, nextnext: ($2430) -> $2432 $2431 : aa: V -> ee: E bb: V )result: -> 2470 2469 : ee: E bb: V
  if yieldingstd/core/hnd/yielding: () -> $2432 bool() then yield-extendstd/core/hnd/yield-extend: (next : ($2430) -> $2432 $2431) -> $2432 $2431(nextnext: ($2430) -> $2432 $2431) else nextnext: ($2430) -> $2432 $2431(xx: $2430)

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: $2480 : aa: V, extendextend: ($2480) -> $2482 $2481 : aa: V -> ee: E bb: V, nextnext: ($2480) -> $2482 $2481 : aa: V -> ee: E bb: V )result: -> 2520 2519 : ee: E bb: V
  if yieldingstd/core/hnd/yielding: () -> $2482 bool() then yield-extendstd/core/hnd/yield-extend: (next : ($2480) -> $2482 $2481) -> $2482 $2481(extendextend: ($2480) -> $2482 $2481) else nextnext: ($2480) -> $2482 $2481(xx: $2480)

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) -> $2531 $2530, a) -> $2531 $2532 : 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<$2580,$2581>: 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<$2625,$2626> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>, clauseclause: ((resume-result<$2623,$2626>) -> $2625 $2626) -> $2625 $2626 : (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<$2681,$2682> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>, clauseclause: ((resume-result<$2679,$2682>) -> $2681 $2682) -> $2681 $2682 : (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<$2733,$2734> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>, clauseclause: ((resume-result<$2732,$2734>) -> $2733 $2734) -> $2733 $2734 : (resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> e1e1: E rr: V) -> e1e1: E rr: V )result: -> 2786 2785 : e1e1: E bb: V
  //val w0 = evv-get()
  val gg: () -> $2732 : () -> _b_b: V = yield-to-primstd/core/hnd/yield-to-prim: (m : marker<$2733,$2734>, clause : ((resume-result<$2732,$2734>) -> $2733 $2734) -> $2733 $2734) -> $2733 (() -> $2732)(mm: marker<$2733,$2734>, clauseclause: ((resume-result<$2732,$2734>) -> $2733 $2734) -> $2733 $2734)
  yield-extendstd/core/hnd/yield-extend: (next : (() -> $2733 $2732) -> $2733 $2732) -> $2733 $2732 fnfn: (f : () -> $2733 $2732) -> $2733 $2732(ff: () -> $2733 $2732)
    // val keep1 = guard(w0)  // check the evidence is correctly restored
    ff: () -> $2733 $2732()

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

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

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

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


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

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

// mask for builtin effects without a handler or evidence (like `:st` or `:local`)
pub fun @mask-builtin<aa: V,e1e1: E,e2e2: E>( actionaction: () -> $3987 $3986 : () -> e1e1: E aa: V )result: -> 4019 4017 : e2e2: E aa: V
  cast-ev0std/core/hnd/cast-ev0: (f : () -> $3987 $3986) -> $3988 (() -> $3988 $3986)(actionaction: () -> $3987 $3986)()


// -------------------------------------------
// 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<aa: V,bb: V,ss: H,ee: E>(locloc: local-var<$4031,$4029>:local-varstd/core/types/local-var: (H, V) -> V<ss: H,aa: V>, resres: $4030 : bb: V  )result: -> <div,local<4141>|4142> 4140 : <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<$4031>|$4032> boolyieldingstd/core/hnd/yielding: () -> <div,local<$4031>|$4032> bool() returnreturn: $4030 resres: $4030;
  val vv: $4029 = locloc: $4029
?hdiv=iev@4057
yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> <div,local<$4031>|$4032> $4030, a) -> <div,local<$4031>|$4032> $4030) -> <div,local<$4031>|$4032> $4030(fnfn: forall<a> (cont : (a) -> <div,local<$4031>|$4032> $4030, x : a) -> <div,local<$4031>|$4032> $4030(contcont: ($4080) -> <div,local<$4031>|$4032> $4030,xx: $4080){ locloc: local-var<$4031,$4029> :=std/core/types/local-set: (v : local-var<$4031,$4029>, assigned : $4029) -> <local<$4031>,div|$4032> () vv: $4029; prompt-local-varstd/core/hnd/prompt-local-var: (loc : local-var<$4031,$4029>, res : $4030) -> <div,local<$4031>|$4032> $4030(@byref(locloc: local-var<$4031,$4029>),contcont: ($4080) -> <div,local<$4031>|$4032> $4030(xx: $4080)) }
) // restore state early before the resume pub inline fun local-varstd/core/hnd/local-var: forall<a,b,e,h> (init : a, action : (local-var<h,a>) -> <local<h>|e> b) -> <local<h>|e> b(initinit: $4176:aa: V, actionaction: (local-var<$4179,$4176>) -> <local<$4179>|$4178> $4177: (@local-var: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<4257>|4256> 4255 : <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<$4179>|$4178> $4177) -> <local<$4179>|$4178> $4177 val locloc: local-var<$4179,$4176> : local-varstd/core/types/local-var: (H, V) -> V<__w-l468-c25: H,__w-l468-c27: V> = local-newstd/core/types/local-new: (value : $4176) -> <local<$4179>,div|$4178> local-var<$4179,$4176>(initinit: $4176) val resres: $4177 = cast-ev1std/core/hnd/cast-ev1: (f : (local-var<$4179,$4176>) -> <local<$4179>|$4178> $4177) -> <div,local<$4179>|$4178> ((local-var<$4179,$4176>) -> <div,local<$4179>|$4178> $4177)(actionaction: (local-var<$4179,$4176>) -> <local<$4179>|$4178> $4177)(@byref(locloc: local-var<$4179,$4176>)) prompt-local-varstd/core/hnd/prompt-local-var: (loc : local-var<$4179,$4176>, res : $4177) -> <div,local<$4179>|$4178> $4177(@byref(locloc: local-var<$4179,$4176>),resres: $4177) // ------------------------------------------- // Finally // ------------------------------------------- pub fun finallystd/core/hnd/finally: forall<a,e> (fin : () -> e (), action : () -> e a) -> e a( finfin: () -> $4403 () : () -> ee: E (std/core/types/unit: V)std/core/types/unit: V, actionaction: () -> $4403 $4402 : () -> ee: E aa: V )result: -> 4425 4424 : ee: E aa: V finally-promptstd/core/hnd/finally-prompt: (fin : () -> $4403 (), res : $4402) -> $4403 $4402(finfin: () -> $4403 (), actionaction: () -> $4403 $4402()); fun finally-promptstd/core/hnd/finally-prompt: forall<a,e> (fin : () -> e (), res : a) -> e a(finfin: () -> $4271 () : () -> ee: E (std/core/types/unit: V)std/core/types/unit: V, resres: $4270 : aa: V )result: -> 4395 4394 : ee: E aa: V if !std/core/types/bool/(!): (b : bool) -> $4271 boolyieldingstd/core/hnd/yielding: () -> $4271 bool() then finfin: () -> $4271 ()() resres: $4270 elif yielding-non-finalstd/core/hnd/yielding-non-final: () -> $4271 bool() then yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $4271 $4270, a) -> $4271 $4270) -> $4271 $4270(fnfn: forall<a> (cont : (a) -> $4271 $4270, x : a) -> $4271 $4270(contcont: ($4309) -> $4271 $4270,xx: $4309){ finally-promptstd/core/hnd/finally-prompt: (fin : () -> $4271 (), res : $4270) -> $4271 $4270(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : () -> $4271 ()) -> $4271 (() -> $4271 ())(finfin: () -> $4271 ()),contcont: ($4309) -> $4271 $4270(xx: $4309)) }) else val yldyld: yield-info = yield-capturestd/core/hnd/yield-capture: () -> $4271 yield-info() finfin: () -> $4271 ()() if yieldingstd/core/hnd/yielding: () -> $4271 bool() returnreturn: $4270 yield-extendstd/core/hnd/yield-extend: (next : (_4355) -> $4271 $4270) -> $4271 $4270( fnfn: (_4355) -> $4271 $4270(_x) unsafe-reyieldstd/core/hnd/unsafe-reyield: (yld : yield-info) -> $4271 $4270(yldyld: yield-info) )std/core/types/Unit: () unsafe-reyieldstd/core/hnd/unsafe-reyield: (yld : yield-info) -> $4271 $4270(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) -> $4638 () : (intstd/core/types/int: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V, actionaction: () -> $4638 $4637 : () -> ee: E aa: V )result: -> 4695 4694 : ee: E aa: V initinit: (int) -> $4638 ()(0literal: int
dec = 0
hex8 = 0x00
bit8 = 0b00000000
) if yieldingstd/core/hnd/yielding: () -> $4638 bool() returnreturn: $4637 yield-extendstd/core/hnd/yield-extend: (next : (()) -> $4638 $4637) -> $4638 $4637(fnfn: (()) -> $4638 $4637(_ret:(std/core/types/unit: V)std/core/types/unit: V) initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $4638 (), res : $4637) -> $4638 $4637(initinit: (int) -> $4638 (),actionaction: () -> $4638 $4637()) )std/core/types/Unit: () initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $4638 (), res : $4637) -> $4638 $4637(initinit: (int) -> $4638 (), actionaction: () -> $4638 $4637()
) fun initially-promptstd/core/hnd/initially-prompt: forall<a,e> (init : (int) -> e (), res : a) -> e a( initinit: (int) -> $4433 () : (intstd/core/types/int: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V, resres: $4432 : aa: V )result: -> 4630 4629 : ee: E aa: V if yielding-non-finalstd/core/hnd/yielding-non-final: () -> $4433 bool() then val countcount: ref<global,int> = unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$4433> ref<global,int>) -> $4433 (() -> $4433 ref<global,int>){refstd/core/types/ref: (value : int) -> <alloc<global>,read<global>,write<global>|$4433> ref<global,int>(0literal: int
dec = 0
hex8 = 0x00
bit8 = 0b00000000
)}() yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $4433 $4432, a) -> $4433 $4432) -> $4433 $4432(fnfn: forall<a> (cont : (a) -> $4433 $4432, x : a) -> $4433 $4432(contcont: ($4475) -> $4433 $4432,xx: $4475) val cntcnt: int = unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$4433> int) -> $4433 (() -> $4433 int){ !std/core/types/ref/(!): (ref : ref<global,int>, @implicit/hdiv : hdiv<global,int,<alloc<global>,write<global>|$4433>>) -> <read<global>,alloc<global>,write<global>|$4433> int
?hdiv=iev@4494
countcount: ref<global,int> }() // increase counter on every resumption unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$4433> ()) -> $4433 (() -> $4433 ()){ countcount: ref<global,int> :=std/core/types/set: (ref : ref<global,int>, assigned : int) -> <write<global>,alloc<global>,read<global>|$4433> () addstd/core/hnd/add: (i : int, j : int) -> <write<global>,alloc<global>,read<global>|$4433> int(cntcnt: int,1literal: int
dec = 1
hex8 = 0x01
bit8 = 0b00000001
) }() if eqstd/core/hnd/eq: (x : int, y : int) -> $4433 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) -> $4433 ()(cntcnt: int) if yieldingstd/core/hnd/yielding: () -> $4433 bool() then { yield-extendstd/core/hnd/yield-extend: (next : (_4563) -> $4433 $4432) -> $4433 $4432( fnfn: (_4563) -> $4433 $4432(_ret) initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $4433 (), res : $4432) -> $4433 $4432(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : (int) -> $4433 ()) -> $4433 ((int) -> $4433 ())(initinit: (int) -> $4433 ()), contcont: ($4475) -> $4433 $4432(xx: $4475)) ); (std/core/types/Unit: ())std/core/types/Unit: () }std/core/types/Unit: () initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $4433 (), res : $4432) -> $4433 $4432(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : (int) -> $4433 ()) -> $4433 ((int) -> $4433 ())(initinit: (int) -> $4433 ()), contcont: ($4475) -> $4433 $4432(xx: $4475)) ) else resres: $4432
// ------------------------------------------- // 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<4737,4740>) -> 4738 4740 : 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<$4830,$4831,$4832,$4833> : resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>, xx: $4830 : bb: V )result: -> 4881 4883 : ee: E rr: V (rr: resume-context<$4830,$4831,$4832,$4833>.kstd/core/hnd/resume-context/k: (resume-context<$4830,$4831,$4832,$4833>) -> $4831 ((resume-result<$4830,$4833>) -> $4831 $4833))(Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(xx: $4830)) 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<$4896,$4897,$4898,$4899> : resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>, xx: $4896 : bb: V )result: -> 4964 4965 : e0e0: E rr: V cast-ev1std/core/hnd/cast-ev1: (f : (resume-result<$4896,$4899>) -> $4897 $4899) -> $4898 ((resume-result<$4896,$4899>) -> $4898 $4899)(rr: resume-context<$4896,$4897,$4898,$4899>.kstd/core/hnd/resume-context/k: (resume-context<$4896,$4897,$4898,$4899>) -> $4898 ((resume-result<$4896,$4899>) -> $4897 $4899))(Shallowstd/core/hnd/Shallow: forall<a,b> (result : a) -> resume-result<a,b>(xx: $4896)) 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<$4978,$4979,$4980,$4981> : resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>, xx: $4981 : rr: V )result: -> 5029 5031 : ee: E rr: V //finalize(r.k,x) (rr: resume-context<$4978,$4979,$4980,$4981>.kstd/core/hnd/resume-context/k: (resume-context<$4978,$4979,$4980,$4981>) -> $4979 ((resume-result<$4978,$4981>) -> $4979 $4981))(Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>(xx: $4981)) // ------------------------------------------- // 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<$5200> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($5200<e,a>) -> clause1<$5198,$5199,$5200,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: $5198 : aa: V )result: -> 5289 5287 : ee: E bb: V match evev: ev<$5200> 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<$5207,$5208>,hh: $5200<$5207,$5208>,_w) -> match hh: $5200<$5207,$5208>.opop: ($5200<$5207,$5208>) -> $5201 clause1<$5198,$5199,$5200,$5207,$5208> 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<$5207,$5208>, ev<$5200>, $5198) -> $5207 $5199) -> cast-clause1std/core/hnd/cast-clause1: (f : (marker<$5207,$5208>, ev<$5200>, $5198) -> $5207 $5199) -> $5201 ((marker<$5207,$5208>, ev<$5200>, $5198) -> $5201 $5199)(ff: (marker<$5207,$5208>, ev<$5200>, $5198) -> $5207 $5199)(mm: marker<$5207,$5208>,evev: ev<$5200>,xx: $5198) fun evv-swap-withstd/core/hnd/evv-swap-with: forall<a,e> (ev : ev<a>) -> evv<e>(evev: ev<$5304> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>)result: -> total evv<5345> match(evev: ev<$5304>) 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<$5310>) -> evv-swapstd/core/hnd/evv-swap: (w : evv<$5310>) -> evv<_5327>(ww: evv<$5310>) inline fun under1std/core/hnd/under1: forall<a,b,e,c> (ev : ev<c>, op : (a) -> e b, x : a) -> e b( evev: ev<$5469> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($5466) -> $5468 $5467 : aa: V -> ee: E bb: V, xx: $5466 : aa: V )result: -> 5565 5564 : ee: E bb: V val w0w0: evv<_5477> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$5469>) -> $5468 evv<_5477>(evev: ev<$5469>) val yy: $5467 = opop: ($5466) -> $5468 $5467(xx: $5466) // evv-set(w0) // only needed before yielding for evidence expected check in prompt if yieldingstd/core/hnd/yielding: () -> $5468 bool() returnreturn: $5467 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5468 $5467, a) -> $5468 $5467) -> $5468 $5467( fnfn: forall<a> (cont : (a) -> $5468 $5467, res : a) -> $5468 $5467(contcont: ($5501) -> $5468 $5467,resres: $5501) under1xstd/core/hnd/under1x: (ev : ev<$5469>, op : ($5501) -> $5468 $5467, x : $5501) -> $5468 $5467(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev<$5469>) -> $5468 ev<$5469>(evev: ev<$5469>),contcont: ($5501) -> $5468 $5467,resres: $5501) )std/core/types/Unit: () evv-setstd/core/hnd/evv-set: (w : evv<_5477>) -> $5468 ()(w0w0: evv<_5477>) yy: $5467 // 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<$5356> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($5353) -> $5355 $5354 : aa: V -> ee: E bb: V, xx: $5353 : aa: V )result: -> 5452 5451 : ee: E bb: V val w0w0: evv<_5364> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$5356>) -> $5355 evv<_5364>(evev: ev<$5356>) val yy: $5354 = opop: ($5353) -> $5355 $5354(xx: $5353) // evv-set(w0) // only needed before yielding for evidence expected check in prompt if yieldingstd/core/hnd/yielding: () -> $5355 bool() returnreturn: $5354 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5355 $5354, a) -> $5355 $5354) -> $5355 $5354( fnfn: forall<a> (cont : (a) -> $5355 $5354, res : a) -> $5355 $5354(contcont: ($5388) -> $5355 $5354,resres: $5388) under1xstd/core/hnd/under1x: (ev : ev<$5356>, op : ($5388) -> $5355 $5354, x : $5388) -> $5355 $5354(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev<$5356>) -> $5355 ev<$5356>(evev: ev<$5356>),contcont: ($5388) -> $5355 $5354,resres: $5388) )std/core/types/Unit: () evv-setstd/core/hnd/evv-set: (w : evv<_5364>) -> $5355 ()(w0w0: evv<_5364>) yy: $5354 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 : $5579, r : resume-context<$5580,$5581,$5582,$5584>) -> $5581 $5584 : (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<5664,5665,5668,5666,5669> : 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<$5581,$5584>, ev<$5583>, x : $5579) -> $5581 $5580(mm: marker<$5581,$5584>,_ev,xx: $5579){ yield-tostd/core/hnd/yield-to: (m : marker<$5581,$5584>, clause : ((resume-result<$5580,$5584>) -> $5581 $5584) -> $5581 $5584) -> $5581 $5580(mm: marker<$5581,$5584>, fnfn: (k : (resume-result<$5580,$5584>) -> $5581 $5584) -> $5581 $5584(kk: (resume-result<$5580,$5584>) -> $5581 $5584){ opop: (x : $5579, r : resume-context<$5580,$5581,$5582,$5584>) -> $5581 $5584(xx: $5579,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<$5580,$5584>) -> $5581 $5584)) } ) } ) fun getstd/core/hnd/get: forall<a,h> (ref : ref<h,a>) -> <read<h>,div> a( refref: ref<$5690,$5689>: refstd/core/types/ref: (H, V) -> V<hh: H,aa: V>)result: -> <read<5718>,div> 5717 : <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<$5690,$5689>, @implicit/hdiv : hdiv<$5690,$5689,div>) -> <read<$5690>,div> $5689
?hdiv=iev@5694
refref: ref<$5690,$5689>
inline extern unsafe-ststd/core/hnd/unsafe-st: forall<a,e> (f : () -> <st<global>|e> a) -> (() -> e a)(f : () -> <ststd/core/types/st: H -> E<globalstd/core/types/global: H>|ee: E> aa: V ) : ((std/core/types/total: E) -> ee: E aa: V) inline "#1" fun protect-promptstd/core/hnd/protect-prompt: forall<a,e,b> (resumed : ref<global,bool>, k : (resume-result<a,b>) -> e b, res : b) -> e b( resumedresumed: ref<global,bool> : refstd/core/types/ref: (H, V) -> V<globalstd/core/types/global: H,boolstd/core/types/bool: V>, kk: (resume-result<$5726,$5728>) -> $5727 $5728 : resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V, resres: $5728 : rr: V )result: -> 5917 5918 : ee: E rr: V val did-resumedid-resume: bool : boolstd/core/types/bool: V = (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$5727> bool) -> $5727 (() -> $5727 bool){ !std/core/types/ref/(!): (ref : ref<global,bool>, @implicit/hdiv : hdiv<global,bool,<alloc<global>,write<global>|$5727>>) -> <read<global>,alloc<global>,write<global>|$5727> bool
?hdiv=iev@5747
resumedresumed: ref<global,bool> })() if did-resumedid-resume: bool then // if resumed, we no longer need to protect resres: $5728 elif !std/core/types/bool/(!): (b : bool) -> $5727 boolyieldingstd/core/hnd/yielding: () -> $5727 bool() then // otherwise, if we are not yielding, resume k with finalization (to run all finally clauses) kk: (resume-result<$5726,$5728>) -> $5727 $5728(Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>(resres: $5728)) elif yielding-non-finalstd/core/hnd/yielding-non-final: () -> $5727 bool() then // if we yield non-final to an operation, extend the continuation with this prompt (so we keep protecting after being resumed) yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5727 $5728, a) -> $5727 $5728) -> $5727 $5728( fnfn: forall<a> (cont : (a) -> $5727 $5728, x : a) -> $5727 $5728(contcont: ($5811) -> $5727 $5728,xx: $5811) protect-promptstd/core/hnd/protect-prompt: (resumed : ref<global,bool>, k : (resume-result<$5726,$5728>) -> $5727 $5728, res : $5728) -> $5727 $5728(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ref<global,bool>) -> $5727 ref<global,bool>(resumedresumed: ref<global,bool>),kk: (resume-result<$5726,$5728>) -> $5727 $5728,contcont: ($5811) -> $5727 $5728(xx: $5811)) ) else // if we are in a final yield, capture it, resume k with finalization, and reyield val yldyld: yield-info = yield-capturestd/core/hnd/yield-capture: () -> $5727 yield-info() kk: (resume-result<$5726,$5728>) -> $5727 $5728(Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>(resres: $5728)) if yieldingstd/core/hnd/yielding: () -> $5727 bool() returnreturn: $5728 yield-extendstd/core/hnd/yield-extend: (next : (_5872) -> $5727 $5728) -> $5727 $5728( fnfn: (_5872) -> $5727 $5728(_x) unsafe-reyieldstd/core/hnd/unsafe-reyield: (yld : yield-info) -> $5727 $5728(yldyld: yield-info) )std/core/types/Unit: () // yikes, a finally clause is itself yielding... unsafe-reyieldstd/core/hnd/unsafe-reyield: (yld : yield-info) -> $5727 $5728(yldyld: yield-info
) fun protectstd/core/hnd/protect: forall<a,b,e,c> (x : a, clause : (x : a, k : (b) -> e c) -> e c, k : (resume-result<b,c>) -> e c) -> e c( xx: $5928 : aa: V, clauseclause: (x : $5928, k : ($5929) -> $5930 $5931) -> $5930 $5931 : (x:aa: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V, kk: (resume-result<$5929,$5931>) -> $5930 $5931 : resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V )result: -> 6037 6038 : ee: E rr: V val resumedresumed: ref<global,bool> = (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$5930> ref<global,bool>) -> $5930 (() -> $5930 ref<global,bool>){refstd/core/types/ref: (value : bool) -> <alloc<global>,read<global>,write<global>|$5930> ref<global,bool>(Falsestd/core/types/False: bool)})() fun kprotectkprotect: (ret : $5929) -> $5930 $5931(retret: $5929)result: -> $5930 $5931 (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$5930> ()) -> $5930 (() -> $5930 ()){resumedresumed: ref<global,bool> :=std/core/types/set: (ref : ref<global,bool>, assigned : bool) -> <write<global>,alloc<global>,read<global>|$5930> () Truestd/core/types/True: bool})() kk: (resume-result<$5929,$5931>) -> $5930 $5931(Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(retret: $5929)) val resres: $5931 = clauseclause: (x : $5928, k : ($5929) -> $5930 $5931) -> $5930 $5931(xx: $5928,kprotectkprotect: (ret : $5929) -> $5930 $5931) protect-promptstd/core/hnd/protect-prompt: (resumed : ref<global,bool>, k : (resume-result<$5929,$5931>) -> $5930 $5931, res : $5931) -> $5930 $5931(resumedresumed: ref<global,bool>,kk: (resume-result<$5929,$5931>) -> $5930 $5931,resres: $5931) /* 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 : $6051, k : ($6052) -> $6053 $6055) -> $6053 $6055 : (x:aa: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause1<6128,6129,6131,6130,6132> : 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<$6053,$6055>, ev<$6054>, x : $6051) -> $6053 $6052(mm: marker<$6053,$6055>,_ev,xx: $6051){ yield-tostd/core/hnd/yield-to: (m : marker<$6053,$6055>, clause : ((resume-result<$6052,$6055>) -> $6053 $6055) -> $6053 $6055) -> $6053 $6052(mm: marker<$6053,$6055>, fnfn: (k : (resume-result<$6052,$6055>) -> $6053 $6055) -> $6053 $6055(kk: (resume-result<$6052,$6055>) -> $6053 $6055) protectstd/core/hnd/protect: (x : $6051, clause : (x : $6051, k : ($6052) -> $6053 $6055) -> $6053 $6055, k : (resume-result<$6052,$6055>) -> $6053 $6055) -> $6053 $6055(xx: $6051,clauseclause: (x : $6051, k : ($6052) -> $6053 $6055) -> $6053 $6055,kk: (resume-result<$6052,$6055>) -> $6053 $6055) ) }) // 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: ($6152) -> $6149 $6153 : aa: V -> ee: E bb: V)result: -> total clause1<6216,6217,6215,6213,6214> : 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<$6149,$6150>, ev : ev<$6151>, x : $6152) -> $6149 $6153(_m,evev: ev<$6151>,xx: $6152){ under1std/core/hnd/under1: (ev : ev<$6151>, op : ($6152) -> $6149 $6153, x : $6152) -> $6149 $6153(evev: ev<$6151>,opop: ($6152) -> $6149 $6153,xx: $6152) }) // 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: ($6237) -> $6234 $6238 : aa: V -> ee: E bb: V)result: -> total clause1<6287,6288,6286,6284,6285> : 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<$6234,$6235>, ev<$6236>, x : $6237) -> $6234 $6238(_m,_ev,xx: $6237){ opop: ($6237) -> $6234 $6238(xx: $6237) }) // 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: ($6305) -> $6307 $6309 : aa: V -> ee: E rr: V )result: -> total clause1<6371,6372,6374,6373,6375> : 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<$6307,$6309>, ev<$6308>, x : $6305) -> $6307 $6306(mm: marker<$6307,$6309>,_ev,xx: $6305){ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$6307,$6309>, clause : ((resume-result<$6306,$6309>) -> $6307 $6309) -> $6307 $6309) -> $6307 $6306(mm: marker<$6307,$6309>, fnfn: ((resume-result<$6306,$6309>) -> $6307 $6309) -> $6307 $6309(_k) opop: ($6305) -> $6307 $6309(xx: $6305) ) }) //---------------------------------------------------------------- // 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<$6522> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($6522<e,a>) -> clause0<$6520,$6522,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: -> 6598 6597 : ee: E bb: V match evev: ev<$6522> 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<$6528,$6529>,hh: $6522<$6528,$6529>,_w) -> match hh: $6522<$6528,$6529>.opop: ($6522<$6528,$6529>) -> $6521 clause0<$6520,$6522,$6528,$6529> Clause0std/core/hnd/Clause0: forall<a,b,e,c> (clause : (marker<e,c>, ev<b>) -> e a) -> clause0<a,b,e,c>(ff: (marker<$6528,$6529>, ev<$6522>) -> $6528 $6520) -> cast-clause0std/core/hnd/cast-clause0: (f : (marker<$6528,$6529>, ev<$6522>) -> $6528 $6520) -> $6521 ((marker<$6528,$6529>, ev<$6522>) -> $6521 $6520)(ff: (marker<$6528,$6529>, ev<$6522>) -> $6528 $6520)(mm: marker<$6528,$6529>,evev: ev<$6522>) inline fun under0std/core/hnd/under0: forall<a,e,b> (ev : ev<b>, op : () -> e a) -> e a( evev: ev<$6613> : evstd/core/hnd/ev: ((E, V) -> V) -> V<ii: (E, V) -> V>, opop: () -> $6612 $6611 : () -> ee: E bb: V)result: -> 6696 6695 : ee: E bb: V val w0w0: evv<_6621> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$6613>) -> $6612 evv<_6621>(evev: ev<$6613>) val yy: $6611 = opop: () -> $6612 $6611() // evv-set(w0) // only needed before yielding for evidence expected check in prompt evv-setstd/core/hnd/evv-set: (w : evv<_6621>) -> $6612 ()(w0w0: evv<_6621>) if yieldingstd/core/hnd/yielding: () -> $6612 bool() returnreturn: $6611 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $6612 $6611, a) -> $6612 $6611) -> $6612 $6611( fnfn: forall<a> (cont : (a) -> $6612 $6611, res : a) -> $6612 $6611(contcont: ($6653) -> $6612 $6611,resres: $6653) under1std/core/hnd/under1: (ev : ev<$6613>, op : ($6653) -> $6612 $6611, x : $6653) -> $6612 $6611(evev: ev<$6613>,contcont: ($6653) -> $6612 $6611,resres: $6653) )std/core/types/Unit: () yy: $6611 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<$6707,$6708,$6709,$6711>) -> $6708 $6711 : 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<6783,6786,6784,6787> : 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<$6708,$6711>, ev<$6710>) -> $6708 $6707(mm: marker<$6708,$6711>,_ev){ yield-tostd/core/hnd/yield-to: (m : marker<$6708,$6711>, clause : ((resume-result<$6707,$6711>) -> $6708 $6711) -> $6708 $6711) -> $6708 $6707(mm: marker<$6708,$6711>, fnfn: (k : (resume-result<$6707,$6711>) -> $6708 $6711) -> $6708 $6711(kk: (resume-result<$6707,$6711>) -> $6708 $6711){ opop: (resume-context<$6707,$6708,$6709,$6711>) -> $6708 $6711(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<$6707,$6711>) -> $6708 $6711)) } ) }) /* 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: (($6804) -> $6805 $6807) -> $6805 $6807 : (bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause0<6876,6878,6877,6879> : 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<$6805,$6807>, ev<$6806>) -> $6805 $6804(mm: marker<$6805,$6807>,_ev){ yield-tostd/core/hnd/yield-to: (m : marker<$6805,$6807>, clause : ((resume-result<$6804,$6807>) -> $6805 $6807) -> $6805 $6807) -> $6805 $6804(mm: marker<$6805,$6807>, fnfn: (k : (resume-result<$6804,$6807>) -> $6805 $6807) -> $6805 $6807(kk: (resume-result<$6804,$6807>) -> $6805 $6807){ protectstd/core/hnd/protect: (x : (), clause : (x : (), k : ($6804) -> $6805 $6807) -> $6805 $6807, k : (resume-result<$6804,$6807>) -> $6805 $6807) -> $6805 $6807((std/core/types/Unit: ())std/core/types/Unit: (),fnfn: ((), r : ($6804) -> $6805 $6807) -> $6805 $6807(_x,rr: ($6804) -> $6805 $6807){ opop: (($6804) -> $6805 $6807) -> $6805 $6807(rr: ($6804) -> $6805 $6807) }, kk: (resume-result<$6804,$6807>) -> $6805 $6807) }) }) 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: () -> $6893 $6896 : () -> ee: E bb: V)result: -> total clause0<6948,6947,6945,6946> : 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<$6893,$6894>, ev : ev<$6895>) -> $6893 $6896(_m,evev: ev<$6895>){ under0std/core/hnd/under0: (ev : ev<$6895>, op : () -> $6893 $6896) -> $6893 $6896(evev: ev<$6895>,opop: () -> $6893 $6896) }) 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: () -> $6962 $6965 : () -> ee: E bb: V)result: -> total clause0<7006,7005,7003,7004> : 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<$6962,$6963>, ev<$6964>) -> $6962 $6965(_m,_ev){ opop: () -> $6962 $6965() }) pub fun clause-valuestd/core/hnd/clause-value: forall<a,e,b,c> (v : a) -> clause0<a,b,e,c>(vv: $7020 : bb: V)result: -> total clause0<7060,7062,7061,7063> : 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<$7021,$7023>, ev<$7022>) -> $7021 $7020(_m,_ev){ vv: $7020 }) pub fun clause-never0std/core/hnd/clause-never0: forall<a,e,b,c> (op : () -> e c) -> clause0<a,b,e,c>( opop: () -> $7078 $7080 : () -> ee: E rr: V )result: -> total clause0<7134,7136,7135,7137> : 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<$7078,$7080>, ev<$7079>) -> $7078 $7077(mm: marker<$7078,$7080>,_ev){ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$7078,$7080>, clause : ((resume-result<$7077,$7080>) -> $7078 $7080) -> $7078 $7080) -> $7078 $7077(mm: marker<$7078,$7080>, fnfn: ((resume-result<$7077,$7080>) -> $7078 $7080) -> $7078 $7080(_k){ opop: () -> $7078 $7080() }) }) //---------------------------------------------------------------- // 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<$7335> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($7331, $7332) -> $7334 $7333 : (a1a1: V,a2a2: V) -> ee: E bb: V, x1x1: $7331 : a1a1: V, x2x2: $7332 : a2a2: V )result: -> 7430 7429 : ee: E bb: V val w0w0: evv<_7343> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$7335>) -> $7334 evv<_7343>(evev: ev<$7335>) val zz: $7333 = opop: ($7331, $7332) -> $7334 $7333(x1x1: $7331,x2x2: $7332) evv-setstd/core/hnd/evv-set: (w : evv<_7343>) -> $7334 ()(w0w0: evv<_7343>) if yieldingstd/core/hnd/yielding: () -> $7334 bool() returnreturn: $7333 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $7334 $7333, a) -> $7334 $7333) -> $7334 $7333( fnfn: forall<a> (cont : (a) -> $7334 $7333, res : a) -> $7334 $7333(contcont: ($7377) -> $7334 $7333,resres: $7377) under1std/core/hnd/under1: (ev : ev<$7335>, op : ($7377) -> $7334 $7333, x : $7377) -> $7334 $7333(evev: ev<$7335>,contcont: ($7377) -> $7334 $7333,resres: $7377) )std/core/types/Unit: () zz: $7333 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: $7447 : a1a1: V, x2x2: $7448:a2a2: V, clauseclause: (x : $7447, x : $7448, k : ($7449) -> $7450 $7451) -> $7450 $7451 : (x:a1a1: V,x:a2a2: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V, kk: (resume-result<$7449,$7451>) -> $7450 $7451 : resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V )result: -> 7563 7564 : ee: E rr: V val resumedresumed: ref<global,bool> = (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$7450> ref<global,bool>) -> $7450 (() -> $7450 ref<global,bool>){refstd/core/types/ref: (value : bool) -> <alloc<global>,read<global>,write<global>|$7450> ref<global,bool>(Falsestd/core/types/False: bool)})() fun kprotectkprotect: (ret : $7449) -> $7450 $7451(retret: $7449)result: -> $7450 $7451 (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$7450> ()) -> $7450 (() -> $7450 ()){ resumedresumed: ref<global,bool> :=std/core/types/set: (ref : ref<global,bool>, assigned : bool) -> <write<global>,alloc<global>,read<global>|$7450> () Truestd/core/types/True: bool })() kk: (resume-result<$7449,$7451>) -> $7450 $7451(Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(retret: $7449)) val resres: $7451 = clauseclause: (x : $7447, x : $7448, k : ($7449) -> $7450 $7451) -> $7450 $7451(x1x1: $7447,x2x2: $7448,kprotectkprotect: (ret : $7449) -> $7450 $7451) protect-promptstd/core/hnd/protect-prompt: (resumed : ref<global,bool>, k : (resume-result<$7449,$7451>) -> $7450 $7451, res : $7451) -> $7450 $7451(resumedresumed: ref<global,bool>,kk: (resume-result<$7449,$7451>) -> $7450 $7451,resres: $7451) 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 : $7580, x2 : $7581, k : ($7582) -> $7583 $7585) -> $7583 $7585 : (x1:a1a1: V, x2:a2a2: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause2<7669,7670,7671,7673,7672,7674> : 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<$7583,$7585>, ev<$7584>, x1 : $7580, x2 : $7581) -> $7583 $7582(mm: marker<$7583,$7585>,_ev,x1x1: $7580,x2x2: $7581){ yield-tostd/core/hnd/yield-to: (m : marker<$7583,$7585>, clause : ((resume-result<$7582,$7585>) -> $7583 $7585) -> $7583 $7585) -> $7583 $7582(mm: marker<$7583,$7585>, fnfn: (k : (resume-result<$7582,$7585>) -> $7583 $7585) -> $7583 $7585(kk: (resume-result<$7582,$7585>) -> $7583 $7585){ protect2std/core/hnd/protect2: (x1 : $7580, x2 : $7581, clause : (x : $7580, x : $7581, k : ($7582) -> $7583 $7585) -> $7583 $7585, k : (resume-result<$7582,$7585>) -> $7583 $7585) -> $7583 $7585(x1x1: $7580,x2x2: $7581,clauseclause: (x1 : $7580, x2 : $7581, k : ($7582) -> $7583 $7585) -> $7583 $7585,kk: (resume-result<$7582,$7585>) -> $7583 $7585) }) }) 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 : $7694, x2 : $7695, r : resume-context<$7696,$7697,$7698,$7700>) -> $7697 $7700 : (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<7788,7789,7790,7793,7791,7794> : 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<$7697,$7700>, ev<$7699>, x1 : $7694, x2 : $7695) -> $7697 $7696(mm: marker<$7697,$7700>,_ev,x1x1: $7694,x2x2: $7695){ yield-tostd/core/hnd/yield-to: (m : marker<$7697,$7700>, clause : ((resume-result<$7696,$7700>) -> $7697 $7700) -> $7697 $7700) -> $7697 $7696(mm: marker<$7697,$7700>, fnfn: (k : (resume-result<$7696,$7700>) -> $7697 $7700) -> $7697 $7700(kk: (resume-result<$7696,$7700>) -> $7697 $7700){ opop: (x1 : $7694, x2 : $7695, r : resume-context<$7696,$7697,$7698,$7700>) -> $7697 $7700(x1x1: $7694,x2x2: $7695,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<$7696,$7700>) -> $7697 $7700)) } ) }) 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: ($7820, $7821) -> $7817 $7822 : (a1a1: V,a2a2: V) -> ee: E bb: V)result: -> total clause2<7896,7897,7898,7895,7893,7894> : 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<$7817,$7818>, ev : ev<$7819>, x1 : $7820, x2 : $7821) -> $7817 $7822(mm: marker<$7817,$7818>,evev: ev<$7819>,x1x1: $7820,x2x2: $7821){ under2std/core/hnd/under2: (ev : ev<$7819>, op : ($7820, $7821) -> $7817 $7822, x1 : $7820, x2 : $7821) -> $7817 $7822(evev: ev<$7819>,opop: ($7820, $7821) -> $7817 $7822,x1x1: $7820,x2x2: $7821) }) 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: ($7921, $7922) -> $7918 $7923 : (a1a1: V,a2a2: V) -> ee: E bb: V)result: -> total clause2<7980,7981,7982,7979,7977,7978> : 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<$7918,$7919>, ev<$7920>, x1 : $7921, x2 : $7922) -> $7918 $7923(_m,_ev,x1x1: $7921,x2x2: $7922){ opop: ($7921, $7922) -> $7918 $7923(x1x1: $7921,x2x2: $7922) }) pub inline fun @perform2( evxevx: ev<$8006> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($8006<e,a>) -> clause2<$8002,$8003,$8004,$8006,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: $8002 : aa: V, yy: $8003 : bb: V )result: -> 8104 8103 : ee: E cc: V match evxevx: ev<$8006> 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<$8012,$8013>,hh: $8006<$8012,$8013>,_w) -> match hh: $8006<$8012,$8013>.opop: ($8006<$8012,$8013>) -> $8005 clause2<$8002,$8003,$8004,$8006,$8012,$8013> 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<$8012,$8013>, ev<$8006>, $8002, $8003) -> $8012 $8004) -> cast-clause2std/core/hnd/cast-clause2: (f : (marker<$8012,$8013>, ev<$8006>, $8002, $8003) -> $8012 $8004) -> $8005 ((marker<$8012,$8013>, ev<$8006>, $8002, $8003) -> $8005 $8004)(ff: (marker<$8012,$8013>, ev<$8006>, $8002, $8003) -> $8012 $8004)(mm: marker<$8012,$8013>,evxevx: ev<$8006>,xx: $8002,yy: $8003) 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: ($8123, $8124) -> $8126 $8128 : (a1a1: V,a2a2: V) -> ee: E rr: V )result: -> total clause2<8198,8199,8200,8202,8201,8203> : 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<$8126,$8128>, ev<$8127>, x1 : $8123, x2 : $8124) -> $8126 $8125(mm: marker<$8126,$8128>,_ev,x1x1: $8123,x2x2: $8124){ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$8126,$8128>, clause : ((resume-result<$8125,$8128>) -> $8126 $8128) -> $8126 $8128) -> $8126 $8125(mm: marker<$8126,$8128>, fnfn: ((resume-result<$8125,$8128>) -> $8126 $8128) -> $8126 $8128(_k){ opop: ($8123, $8124) -> $8126 $8128(x1x1: $8123,x2x2: $8124) }) }) //---------------------------------------------------------------- // 3 arguments: reuse 1 argument clause. // Or should the compiler do tupling/untupling? //---------------------------------------------------------------- // For internal 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<$8226> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($8226<e,a>) -> clause1<$8223,$8224,$8226,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: $8223 : aa: V )result: -> 8313 8312 : ee: E bb: V match evev: ev<$8226> 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<$8232,$8233>,hh: $8226<$8232,$8233>,_w) -> match hh: $8226<$8232,$8233>.opop: ($8226<$8232,$8233>) -> $8225 clause1<$8223,$8224,$8226,$8232,$8233> 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<$8232,$8233>, ev<$8226>, $8223) -> $8232 $8224) -> cast-clause1std/core/hnd/cast-clause1: (f : (marker<$8232,$8233>, ev<$8226>, $8223) -> $8232 $8224) -> $8225 ((marker<$8232,$8233>, ev<$8226>, $8223) -> $8225 $8224)(ff: (marker<$8232,$8233>, ev<$8226>, $8223) -> $8232 $8224)(mm: marker<$8232,$8233>,evev: ev<$8226>,xx: $8223) 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 : $8329, x2 : $8330, x3 : $8331, r : resume-context<$8332,$8333,$8334,$8336>) -> $8333 $8336 : (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<(8410, 8411, 8412),8413,8416,8414,8417> : 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 : ($8329, $8330, $8331), r : resume-context<$8332,$8333,$8334,$8336>) -> $8333 $8336) -> clause1<($8329, $8330, $8331),$8332,$8335,$8333,$8336>( fnfn: (($8329, $8330, $8331), r : resume-context<$8332,$8333,$8334,$8336>) -> $8333 $8336((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8329,x2x2: $8330,x3x3: $8331)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c),rr: resume-context<$8332,$8333,$8334,$8336>){ opop: (x1 : $8329, x2 : $8330, x3 : $8331, r : resume-context<$8332,$8333,$8334,$8336>) -> $8333 $8336(x1x1: $8329,x2x2: $8330,x3x3: $8331,rr: resume-context<$8332,$8333,$8334,$8336>) } ) 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 : $8443, x2 : $8444, x3 : $8445, k : ($8446) -> $8447 $8449) -> $8447 $8449 : (x1:a1a1: V, x2:a2a2: V, x3:a3a3: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause1<(8516, 8517, 8518),8519,8521,8520,8522> : clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<(std/core/types/tuple3: (V, V, V) -> Va1a1: V,a2a2: V,a3a3: V),bb: V,hh: (E, V) -> V,ee: E,rr: V> clause-control1std/core/hnd/clause-control1: (clause : (x : ($8443, $8444, $8445), k : ($8446) -> $8447 $8449) -> $8447 $8449) -> clause1<($8443, $8444, $8445),$8446,$8448,$8447,$8449>( fnfn: (($8443, $8444, $8445), k : ($8446) -> $8447 $8449) -> $8447 $8449((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8443,x2x2: $8444,x3x3: $8445)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c),kk: ($8446) -> $8447 $8449){ opop: (x1 : $8443, x2 : $8444, x3 : $8445, k : ($8446) -> $8447 $8449) -> $8447 $8449(x1x1: $8443,x2x2: $8444,x3x3: $8445,kk: ($8446) -> $8447 $8449) } ) 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: ($8548, $8549, $8550) -> $8545 $8551 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E bb: V)result: -> total clause1<(8620, 8621, 8622),8623,8619,8617,8618> : 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 : (($8548, $8549, $8550)) -> $8545 $8551) -> clause1<($8548, $8549, $8550),$8551,$8547,$8545,$8546>( fnfn: (($8548, $8549, $8550)) -> $8545 $8551((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8548,x2x2: $8549,x3x3: $8550)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) ){ opop: ($8548, $8549, $8550) -> $8545 $8551(x1x1: $8548,x2x2: $8549,x3x3: $8550) } ) 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: ($8649, $8650, $8651) -> $8646 $8652 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E bb: V)result: -> total clause1<(8721, 8722, 8723),8724,8720,8718,8719> : 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 : (($8649, $8650, $8651)) -> $8646 $8652) -> clause1<($8649, $8650, $8651),$8652,$8648,$8646,$8647>( fnfn: (($8649, $8650, $8651)) -> $8646 $8652((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8649,x2x2: $8650,x3x3: $8651)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)){ opop: ($8649, $8650, $8651) -> $8646 $8652(x1x1: $8649,x2x2: $8650,x3x3: $8651) } ) 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: ($8747, $8748, $8749) -> $8751 $8753 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E rr: V )result: -> total clause1<(8819, 8820, 8821),8822,8824,8823,8825> : 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 : (($8747, $8748, $8749)) -> $8751 $8753) -> clause1<($8747, $8748, $8749),$8750,$8752,$8751,$8753>(fnfn: (($8747, $8748, $8749)) -> $8751 $8753((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8747,x2x2: $8748,x3x3: $8749)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)){ opop: ($8747, $8748, $8749) -> $8751 $8753(x1x1: $8747,x2x2: $8748,x3x3: $8749) } ) pub fun @perform3( evev: ev<$8853> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($8853<e,a>) -> clause1<($8848, $8849, $8850),$8851,$8853,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: $8848 : a1a1: V, x2x2: $8849 : a2a2: V, x3x3: $8850 : a3a3: V )result: -> 8933 8932 : ee: E bb: V xperform1std/core/hnd/xperform1: (ev : ev<$8853>, op : forall<e,a> ($8853<e,a>) -> clause1<($8848, $8849, $8850),$8851,$8853,e,a>, x : ($8848, $8849, $8850)) -> $8852 $8851(evev: ev<$8853>,opop: forall<e,a> ($8853<e,a>) -> clause1<($8848, $8849, $8850),$8851,$8853,e,a>,(std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8848,x2x2: $8849,x3x3: $8850)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<$8960> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($8955, $8956, $8957) -> $8959 $8958 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E bb: V, x1x1: $8955 : a1a1: V, x2x2: $8956 : a2a2: V, x3x3: $8957 : a3a3: V )result: -> 9061 9060 : ee: E bb: V val w0w0: evv<_8968> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$8960>) -> $8959 evv<_8968>(evev: ev<$8960>) val zz: $8958 = opop: ($8955, $8956, $8957) -> $8959 $8958(x1x1: $8955,x2x2: $8956,x3x3: $8957) evv-setstd/core/hnd/evv-set: (w : evv<_8968>) -> $8959 ()(w0w0: evv<_8968>) if yieldingstd/core/hnd/yielding: () -> $8959 bool() returnreturn: $8958 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $8959 $8958, a) -> $8959 $8958) -> $8959 $8958( fnfn: forall<a> (cont : (a) -> $8959 $8958, res : a) -> $8959 $8958(contcont: ($9003) -> $8959 $8958,resres: $9003) under1std/core/hnd/under1: (ev : ev<$8960>, op : ($9003) -> $8959 $8958, x : $9003) -> $8959 $8958(evev: ev<$8960>,contcont: ($9003) -> $8959 $8958,resres: $9003) )std/core/types/Unit: () zz: $8958 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 : $9081, x2 : $9082, x3 : $9083, x4 : $9084, k : ($9085) -> $9086 $9088) -> $9086 $9088 : (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<(9162, 9163, 9164, 9165),9166,9168,9167,9169> : 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 : ($9081, $9082, $9083, $9084), k : ($9085) -> $9086 $9088) -> $9086 $9088) -> clause1<($9081, $9082, $9083, $9084),$9085,$9087,$9086,$9088>( fnfn: (($9081, $9082, $9083, $9084), k : ($9085) -> $9086 $9088) -> $9086 $9088((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9081,x2x2: $9082,x3x3: $9083,x4x4: $9084)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d),kk: ($9085) -> $9086 $9088){ opop: (x1 : $9081, x2 : $9082, x3 : $9083, x4 : $9084, k : ($9085) -> $9086 $9088) -> $9086 $9088(x1x1: $9081,x2x2: $9082,x3x3: $9083,x4x4: $9084,kk: ($9085) -> $9086 $9088) } ) 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: ($9198, $9199, $9200, $9201) -> $9195 $9202 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E bb: V)result: -> total clause1<(9278, 9279, 9280, 9281),9282,9277,9275,9276> : 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 : (($9198, $9199, $9200, $9201)) -> $9195 $9202) -> clause1<($9198, $9199, $9200, $9201),$9202,$9197,$9195,$9196>( fnfn: (($9198, $9199, $9200, $9201)) -> $9195 $9202((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9198,x2x2: $9199,x3x3: $9200,x4x4: $9201)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)){ opop: ($9198, $9199, $9200, $9201) -> $9195 $9202(x1x1: $9198,x2x2: $9199,x3x3: $9200,x4x4: $9201) } ) 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: ($9311, $9312, $9313, $9314) -> $9308 $9315 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E bb: V)result: -> total clause1<(9391, 9392, 9393, 9394),9395,9390,9388,9389> : 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 : (($9311, $9312, $9313, $9314)) -> $9308 $9315) -> clause1<($9311, $9312, $9313, $9314),$9315,$9310,$9308,$9309>( fnfn: (($9311, $9312, $9313, $9314)) -> $9308 $9315((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9311,x2x2: $9312,x3x3: $9313,x4x4: $9314)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)){ opop: ($9311, $9312, $9313, $9314) -> $9308 $9315(x1x1: $9311,x2x2: $9312,x3x3: $9313,x4x4: $9314) } ) 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: ($9421, $9422, $9423, $9424) -> $9426 $9428 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E rr: V )result: -> total clause1<(9501, 9502, 9503, 9504),9505,9507,9506,9508> : 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 : (($9421, $9422, $9423, $9424)) -> $9426 $9428) -> clause1<($9421, $9422, $9423, $9424),$9425,$9427,$9426,$9428>(fnfn: (($9421, $9422, $9423, $9424)) -> $9426 $9428((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9421,x2x2: $9422,x3x3: $9423,x4x4: $9424)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)){ opop: ($9421, $9422, $9423, $9424) -> $9426 $9428(x1x1: $9421,x2x2: $9422,x3x3: $9423,x4x4: $9424) } ) pub fun @perform4( evev: ev<$9540> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($9540<e,a>) -> clause1<($9534, $9535, $9536, $9537),$9538,$9540,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: $9534 : a1a1: V, x2x2: $9535 : a2a2: V, x3x3: $9536 : a3a3: V, x4x4: $9537 : a4a4: V )result: -> 9629 9628 : ee: E bb: V xperform1std/core/hnd/xperform1: (ev : ev<$9540>, op : forall<e,a> ($9540<e,a>) -> clause1<($9534, $9535, $9536, $9537),$9538,$9540,e,a>, x : ($9534, $9535, $9536, $9537)) -> $9539 $9538(evev: ev<$9540>,opop: forall<e,a> ($9540<e,a>) -> clause1<($9534, $9535, $9536, $9537),$9538,$9540,e,a>,(std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9534,x2x2: $9535,x3x3: $9536,x4x4: $9537)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<$9660> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($9654, $9655, $9656, $9657) -> $9659 $9658 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E bb: V, x1x1: $9654 : a1a1: V, x2x2: $9655 : a2a2: V, x3x3: $9656 : a3a3: V, x4x4: $9657 : a4a4: V )result: -> 9767 9766 : ee: E bb: V val w0w0: evv<_9668> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$9660>) -> $9659 evv<_9668>(evev: ev<$9660>) val zz: $9658 = opop: ($9654, $9655, $9656, $9657) -> $9659 $9658(x1x1: $9654,x2x2: $9655,x3x3: $9656,x4x4: $9657) evv-setstd/core/hnd/evv-set: (w : evv<_9668>) -> $9659 ()(w0w0: evv<_9668>) if yieldingstd/core/hnd/yielding: () -> $9659 bool() returnreturn: $9658 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $9659 $9658, a) -> $9659 $9658) -> $9659 $9658( fnfn: forall<a> (cont : (a) -> $9659 $9658, res : a) -> $9659 $9658(contcont: ($9704) -> $9659 $9658,resres: $9704) under1std/core/hnd/under1: (ev : ev<$9660>, op : ($9704) -> $9659 $9658, x : $9704) -> $9659 $9658(evev: ev<$9660>,contcont: ($9704) -> $9659 $9658,resres: $9704) )std/core/types/Unit: () zz: $9658 // ------------------------------------------- // Open // ------------------------------------------- pub fun @open-none0<bb: V,e1e1: E,e2e2: E>( ff: () -> $9791 $9790 : () -> e1e1: E bb: V )result: -> 9838 9836 : e2e2: E bb: V val ww: evv<$9792> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $9792 evv<$9792>() val xx: $9790 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $9791 $9790) -> $9792 (() -> $9792 $9790)(ff: () -> $9791 $9790)() val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$9792>) -> $9792 ()(ww: evv<$9792>) xx: $9790 pub fun @open-none1<aa: V,bb: V,e1e1: E,e2e2: E>( ff: ($9848) -> $9850 $9849 : aa: V -> e1e1: E bb: V, x1x1: $9848 : aa: V )result: -> 9906 9904 : e2e2: E bb: V val ww: evv<$9851> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $9851 evv<$9851>() val xx: $9849 = cast-ev1std/core/hnd/cast-ev1: (f : ($9848) -> $9850 $9849) -> $9851 (($9848) -> $9851 $9849)(ff: ($9848) -> $9850 $9849)(x1x1: $9848) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$9851>) -> $9851 ()(ww: evv<$9851>) xx: $9849 pub fun @open-none2<a1a1: V,a2a2: V,bb: V,e1e1: E,e2e2: E>( ff: ($9919, $9920) -> $9922 $9921 : (a1a1: V,a2a2: V) -> e1e1: E bb: V, x1x1: $9919 : a1a1: V, x2x2: $9920 : a2a2: V )result: -> 9987 9985 : e2e2: E bb: V val ww: evv<$9923> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $9923 evv<$9923>() val xx: $9921 = cast-ev2std/core/hnd/cast-ev2: (f : ($9919, $9920) -> $9922 $9921) -> $9923 (($9919, $9920) -> $9923 $9921)(ff: ($9919, $9920) -> $9922 $9921)(x1x1: $9919,x2x2: $9920) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$9923>) -> $9923 ()(ww: evv<$9923>) xx: $9921 pub fun @open-none3<a1a1: V,a2a2: V,a3a3: V,bb: V,e1e1: E,e2e2: E>( ff: ($10003, $10004, $10005) -> $10007 $10006 : (a1a1: V,a2a2: V,a3a3: V) -> e1e1: E bb: V, x1x1: $10003 : a1a1: V, x2x2: $10004 : a2a2: V, x3x3: $10005 : a3a3: V )result: -> 10081 10079 : e2e2: E bb: V val ww: evv<$10008> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $10008 evv<$10008>() val xx: $10006 = cast-ev3std/core/hnd/cast-ev3: (f : ($10003, $10004, $10005) -> $10007 $10006) -> $10008 (($10003, $10004, $10005) -> $10008 $10006)(ff: ($10003, $10004, $10005) -> $10007 $10006)(x1x1: $10003,x2x2: $10004,x3x3: $10005) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$10008>) -> $10008 ()(ww: evv<$10008>) xx: $10006 pub fun @open-none4<a1a1: V,a2a2: V,a3a3: V,a4a4: V,bb: V,e1e1: E,e2e2: E>( ff: ($10100, $10101, $10102, $10103) -> $10105 $10104 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e1e1: E bb: V, x1x1: $10100 : a1a1: V, x2x2: $10101 : a2a2: V, x3x3: $10102 : a3a3: V, x4x4: $10103 : a4a4: V )result: -> 10188 10186 : e2e2: E bb: V val ww: evv<$10106> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $10106 evv<$10106>() val xx: $10104 = cast-ev4std/core/hnd/cast-ev4: (f : ($10100, $10101, $10102, $10103) -> $10105 $10104) -> $10106 (($10100, $10101, $10102, $10103) -> $10106 $10104)(ff: ($10100, $10101, $10102, $10103) -> $10105 $10104)(x1x1: $10100,x2x2: $10101,x3x3: $10102,x4x4: $10103) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$10106>) -> $10106 ()(ww: evv<$10106>) xx: $10104 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: ($10210) -> $10212 $10211 : aa: V -> e1e1: E bb: V, xx: $10210 : aa: V )result: -> 10321 10319 : e2e2: E bb: V val ww: evv<$10213> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10213 evv<$10213>(ii: ev-index) val yy: $10211 = cast-ev1std/core/hnd/cast-ev1: (f : ($10210) -> $10212 $10211) -> $10213 (($10210) -> $10213 $10211)(ff: ($10210) -> $10212 $10211)(xx: $10210) evv-setstd/core/hnd/evv-set: (w : evv<$10213>) -> $10213 ()(ww: evv<$10213>) if yieldingstd/core/hnd/yielding: () -> $10213 bool() returnreturn: $10211 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10213 $10211, a) -> $10213 $10211) -> $10213 $10211(fnfn: forall<a> (cont : (a) -> $10213 $10211, res : a) -> $10213 $10211(contcont: ($10265) -> $10213 $10211,resres: $10265){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10265) -> $10213 $10211, x : $10265) -> $10213 $10211(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev-index) -> $10213 ev-index(ii: ev-index),contcont: ($10265) -> $10213 $10211,resres: $10265) })std/core/types/Unit: () yy: $10211 pub fun @open-at0<bb: V,e1e1: E,e2e2: E>( ii: ev-index: ev-indexstd/core/hnd/ev-index: V, ff: () -> $10335 $10334 : () -> e1e1: E bb: V )result: -> 10428 10426 : e2e2: E bb: V val ww: evv<$10336> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10336 evv<$10336>(ii: ev-index) val yy: $10334 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $10335 $10334) -> $10336 (() -> $10336 $10334)(ff: () -> $10335 $10334)() evv-setstd/core/hnd/evv-set: (w : evv<$10336>) -> $10336 ()(ww: evv<$10336>) if yieldingstd/core/hnd/yielding: () -> $10336 bool() returnreturn: $10334 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10336 $10334, a) -> $10336 $10334) -> $10336 $10334(fnfn: forall<a> (cont : (a) -> $10336 $10334, res : a) -> $10336 $10334(contcont: ($10384) -> $10336 $10334,resres: $10384){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10384) -> $10336 $10334, x : $10384) -> $10336 $10334(ii: ev-index,contcont: ($10384) -> $10336 $10334,resres: $10384) })std/core/types/Unit: () yy: $10334 pub fun @open-at1<aa: V,bb: V,e1e1: E,e2e2: E>( ii: ev-index: ev-indexstd/core/hnd/ev-index: V, ff: ($10438) -> $10440 $10439 : aa: V -> e1e1: E bb: V, xx: $10438 : aa: V )result: -> 10542 10540 : e2e2: E bb: V val ww: evv<$10441> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10441 evv<$10441>(ii: ev-index) val yy: $10439 = cast-ev1std/core/hnd/cast-ev1: (f : ($10438) -> $10440 $10439) -> $10441 (($10438) -> $10441 $10439)(ff: ($10438) -> $10440 $10439)(xx: $10438) evv-setstd/core/hnd/evv-set: (w : evv<$10441>) -> $10441 ()(ww: evv<$10441>) if yieldingstd/core/hnd/yielding: () -> $10441 bool() returnreturn: $10439 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10441 $10439, a) -> $10441 $10439) -> $10441 $10439(fnfn: forall<a> (cont : (a) -> $10441 $10439, res : a) -> $10441 $10439(contcont: ($10493) -> $10441 $10439,resres: $10493){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10493) -> $10441 $10439, x : $10493) -> $10441 $10439(ii: ev-index,contcont: ($10493) -> $10441 $10439,resres: $10493) })std/core/types/Unit: () yy: $10439 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: ($10555, $10556) -> $10558 $10557 : (a1a1: V,a2a2: V) -> e1e1: E bb: V, x1x1: $10555 : a1a1: V, x2x2: $10556 : a2a2: V )result: -> 10669 10667 : e2e2: E bb: V val ww: evv<$10559> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10559 evv<$10559>(ii: ev-index) val yy: $10557 = cast-ev2std/core/hnd/cast-ev2: (f : ($10555, $10556) -> $10558 $10557) -> $10559 (($10555, $10556) -> $10559 $10557)(ff: ($10555, $10556) -> $10558 $10557)(x1x1: $10555,x2x2: $10556) evv-setstd/core/hnd/evv-set: (w : evv<$10559>) -> $10559 ()(ww: evv<$10559>) if yieldingstd/core/hnd/yielding: () -> $10559 bool() returnreturn: $10557 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10559 $10557, a) -> $10559 $10557) -> $10559 $10557(fnfn: forall<a> (cont : (a) -> $10559 $10557, res : a) -> $10559 $10557(contcont: ($10615) -> $10559 $10557,resres: $10615){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10615) -> $10559 $10557, x : $10615) -> $10559 $10557(ii: ev-index,contcont: ($10615) -> $10559 $10557,resres: $10615) })std/core/types/Unit: () yy: $10557 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: ($10685, $10686, $10687) -> $10689 $10688 : (a1a1: V,a2a2: V,a3a3: V) -> e1e1: E bb: V, x1x1: $10685 : a1a1: V, x2x2: $10686 : a2a2: V, x3x3: $10687 : a3a3: V )result: -> 10809 10807 : e2e2: E bb: V val ww: evv<$10690> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10690 evv<$10690>(ii: ev-index) val yy: $10688 = cast-ev3std/core/hnd/cast-ev3: (f : ($10685, $10686, $10687) -> $10689 $10688) -> $10690 (($10685, $10686, $10687) -> $10690 $10688)(ff: ($10685, $10686, $10687) -> $10689 $10688)(x1x1: $10685,x2x2: $10686,x3x3: $10687) evv-setstd/core/hnd/evv-set: (w : evv<$10690>) -> $10690 ()(ww: evv<$10690>) if yieldingstd/core/hnd/yielding: () -> $10690 bool() returnreturn: $10688 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10690 $10688, a) -> $10690 $10688) -> $10690 $10688(fnfn: forall<a> (cont : (a) -> $10690 $10688, res : a) -> $10690 $10688(contcont: ($10750) -> $10690 $10688,resres: $10750){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10750) -> $10690 $10688, x : $10750) -> $10690 $10688(ii: ev-index,contcont: ($10750) -> $10690 $10688,resres: $10750) })std/core/types/Unit: () yy: $10688 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: ($10828, $10829, $10830, $10831) -> $10833 $10832 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e1e1: E bb: V, x1x1: $10828 : a1a1: V, x2x2: $10829 : a2a2: V, x3x3: $10830 : a3a3: V, x4x4: $10831 : a4a4: V )result: -> 10962 10960 : e2e2: E bb: V val ww: evv<$10834> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10834 evv<$10834>(ii: ev-index) val yy: $10832 = cast-ev4std/core/hnd/cast-ev4: (f : ($10828, $10829, $10830, $10831) -> $10833 $10832) -> $10834 (($10828, $10829, $10830, $10831) -> $10834 $10832)(ff: ($10828, $10829, $10830, $10831) -> $10833 $10832)(x1x1: $10828,x2x2: $10829,x3x3: $10830,x4x4: $10831) evv-setstd/core/hnd/evv-set: (w : evv<$10834>) -> $10834 ()(ww: evv<$10834>) if yieldingstd/core/hnd/yielding: () -> $10834 bool() returnreturn: $10832 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10834 $10832, a) -> $10834 $10832) -> $10834 $10832(fnfn: forall<a> (cont : (a) -> $10834 $10832, res : a) -> $10834 $10832(contcont: ($10898) -> $10834 $10832,resres: $10898){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10898) -> $10834 $10832, x : $10898) -> $10834 $10832(ii: ev-index,contcont: ($10898) -> $10834 $10832,resres: $10898) })std/core/types/Unit: () yy: $10832 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: ($10984) -> $10986 $10985 : aa: V -> e1e1: E bb: V, xx: $10984 : aa: V )result: -> 11095 11093 : e2e2: E bb: V val ww: evv<$10987> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $10987 evv<$10987>(indicesindices: vector<ev-index>) val yy: $10985 = cast-ev1std/core/hnd/cast-ev1: (f : ($10984) -> $10986 $10985) -> $10987 (($10984) -> $10987 $10985)(ff: ($10984) -> $10986 $10985)(xx: $10984) evv-setstd/core/hnd/evv-set: (w : evv<$10987>) -> $10987 ()(ww: evv<$10987>) if yieldingstd/core/hnd/yielding: () -> $10987 bool() returnreturn: $10985 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10987 $10985, a) -> $10987 $10985) -> $10987 $10985(fnfn: forall<a> (cont : (a) -> $10987 $10985, res : a) -> $10987 $10985(contcont: ($11039) -> $10987 $10985,resres: $11039){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11039) -> $10987 $10985, x : $11039) -> $10987 $10985(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : vector<ev-index>) -> $10987 vector<ev-index>(indicesindices: vector<ev-index>),contcont: ($11039) -> $10987 $10985,resres: $11039) })std/core/types/Unit: () yy: $10985 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: () -> $11109 $11108 : () -> e1e1: E bb: V )result: -> 11202 11200 : e2e2: E bb: V val ww: evv<$11110> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $11110 evv<$11110>(indicesindices: vector<ev-index>) val yy: $11108 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $11109 $11108) -> $11110 (() -> $11110 $11108)(ff: () -> $11109 $11108)() evv-setstd/core/hnd/evv-set: (w : evv<$11110>) -> $11110 ()(ww: evv<$11110>) if yieldingstd/core/hnd/yielding: () -> $11110 bool() returnreturn: $11108 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11110 $11108, a) -> $11110 $11108) -> $11110 $11108(fnfn: forall<a> (cont : (a) -> $11110 $11108, res : a) -> $11110 $11108(contcont: ($11158) -> $11110 $11108,resres: $11158){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11158) -> $11110 $11108, x : $11158) -> $11110 $11108(indicesindices: vector<ev-index>,contcont: ($11158) -> $11110 $11108,resres: $11158) })std/core/types/Unit: () yy: $11108 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: ($11212) -> $11214 $11213 : aa: V -> e1e1: E bb: V, xx: $11212 : aa: V )result: -> 11316 11314 : e2e2: E bb: V val ww: evv<$11215> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $11215 evv<$11215>(indicesindices: vector<ev-index>) val yy: $11213 = cast-ev1std/core/hnd/cast-ev1: (f : ($11212) -> $11214 $11213) -> $11215 (($11212) -> $11215 $11213)(ff: ($11212) -> $11214 $11213)(xx: $11212) evv-setstd/core/hnd/evv-set: (w : evv<$11215>) -> $11215 ()(ww: evv<$11215>) if yieldingstd/core/hnd/yielding: () -> $11215 bool() returnreturn: $11213 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11215 $11213, a) -> $11215 $11213) -> $11215 $11213(fnfn: forall<a> (cont : (a) -> $11215 $11213, res : a) -> $11215 $11213(contcont: ($11267) -> $11215 $11213,resres: $11267){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11267) -> $11215 $11213, x : $11267) -> $11215 $11213(indicesindices: vector<ev-index>,contcont: ($11267) -> $11215 $11213,resres: $11267) })std/core/types/Unit: () yy: $11213 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: ($11329, $11330) -> $11332 $11331 : (a1a1: V,a2a2: V) -> e1e1: E bb: V, x1x1: $11329 : a1a1: V, x2x2: $11330 : a2a2: V )result: -> 11443 11441 : e2e2: E bb: V val ww: evv<$11333> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $11333 evv<$11333>(indicesindices: vector<ev-index>) val yy: $11331 = cast-ev2std/core/hnd/cast-ev2: (f : ($11329, $11330) -> $11332 $11331) -> $11333 (($11329, $11330) -> $11333 $11331)(ff: ($11329, $11330) -> $11332 $11331)(x1x1: $11329,x2x2: $11330) evv-setstd/core/hnd/evv-set: (w : evv<$11333>) -> $11333 ()(ww: evv<$11333>) if yieldingstd/core/hnd/yielding: () -> $11333 bool() returnreturn: $11331 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11333 $11331, a) -> $11333 $11331) -> $11333 $11331(fnfn: forall<a> (cont : (a) -> $11333 $11331, res : a) -> $11333 $11331(contcont: ($11389) -> $11333 $11331,resres: $11389){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11389) -> $11333 $11331, x : $11389) -> $11333 $11331(indicesindices: vector<ev-index>,contcont: ($11389) -> $11333 $11331,resres: $11389) })std/core/types/Unit: () yy: $11331 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: ($11459, $11460, $11461) -> $11463 $11462 : (a1a1: V,a2a2: V,a3a3: V) -> e1e1: E bb: V, x1x1: $11459 : a1a1: V, x2x2: $11460 : a2a2: V, x3x3: $11461 : a3a3: V )result: -> 11583 11581 : e2e2: E bb: V val ww: evv<$11464> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $11464 evv<$11464>(indicesindices: vector<ev-index>) val yy: $11462 = cast-ev3std/core/hnd/cast-ev3: (f : ($11459, $11460, $11461) -> $11463 $11462) -> $11464 (($11459, $11460, $11461) -> $11464 $11462)(ff: ($11459, $11460, $11461) -> $11463 $11462)(x1x1: $11459,x2x2: $11460,x3x3: $11461) evv-setstd/core/hnd/evv-set: (w : evv<$11464>) -> $11464 ()(ww: evv<$11464>) if yieldingstd/core/hnd/yielding: () -> $11464 bool() returnreturn: $11462 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11464 $11462, a) -> $11464 $11462) -> $11464 $11462(fnfn: forall<a> (cont : (a) -> $11464 $11462, res : a) -> $11464 $11462(contcont: ($11524) -> $11464 $11462,resres: $11524){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11524) -> $11464 $11462, x : $11524) -> $11464 $11462(indicesindices: vector<ev-index>,contcont: ($11524) -> $11464 $11462,resres: $11524) })std/core/types/Unit: () yy: $11462 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: ($11602, $11603, $11604, $11605) -> $11607 $11606 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e1e1: E bb: V, x1x1: $11602 : a1a1: V, x2x2: $11603 : a2a2: V, x3x3: $11604 : a3a3: V, x4x4: $11605 : a4a4: V )result: -> 11736 11734 : e2e2: E bb: V val ww: evv<$11608> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $11608 evv<$11608>(indicesindices: vector<ev-index>) val yy: $11606 = cast-ev4std/core/hnd/cast-ev4: (f : ($11602, $11603, $11604, $11605) -> $11607 $11606) -> $11608 (($11602, $11603, $11604, $11605) -> $11608 $11606)(ff: ($11602, $11603, $11604, $11605) -> $11607 $11606)(x1x1: $11602,x2x2: $11603,x3x3: $11604,x4x4: $11605) evv-setstd/core/hnd/evv-set: (w : evv<$11608>) -> $11608 ()(ww: evv<$11608>) if yieldingstd/core/hnd/yielding: () -> $11608 bool() returnreturn: $11606 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11608 $11606, a) -> $11608 $11606) -> $11608 $11606(fnfn: forall<a> (cont : (a) -> $11608 $11606, res : a) -> $11608 $11606(contcont: ($11672) -> $11608 $11606,resres: $11672){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11672) -> $11608 $11606, x : $11672) -> $11608 $11606(indicesindices: vector<ev-index>,contcont: ($11672) -> $11608 $11606,resres: $11672) })std/core/types/Unit: () yy: $11606 // ------------------------------------------- // capture yields // ------------------------------------------- pub fun unsafe-try-finalizestd/core/hnd/unsafe-try-finalize: forall<a,e> (action : () -> e a) -> e either<yield-info,a>( actionaction: () -> $11869 $11868 : () -> ee: E aa: V )result: -> 11890 either<yield-info,11889> : 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 : $11868) -> $11869 either<yield-info,$11868>(actionaction: () -> $11869 $11868()); fun try-finalize-promptstd/core/hnd/try-finalize-prompt: forall<a,e> (res : a) -> e either<yield-info,a>( resres: $11758 : aa: V )result: -> 11861 either<yield-info,11860> : 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: () -> $11759 bool() returnreturn: either<yield-info,$11758> yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11759 $11758, a) -> $11759 either<yield-info,$11758>) -> $11759 either<yield-info,$11758>(fnfn: forall<a> (cont : (a) -> $11759 $11758, x : a) -> $11759 either<yield-info,$11758>(contcont: ($11777) -> $11759 $11758,xx: $11777) try-finalize-promptstd/core/hnd/try-finalize-prompt: (res : $11758) -> $11759 either<yield-info,$11758>(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : $11758) -> $11759 $11758(contcont: ($11777) -> $11759 $11758(xx: $11777))) )std/core/types/Unit: () if !std/core/types/bool/(!): (b : bool) -> $11759 boolyieldingstd/core/hnd/yielding: () -> $11759 bool() then Rightstd/core/types/Right: forall<a,b> (right : b) -> either<a,b>(resres: $11758) else Leftstd/core/types/Left: forall<a,b> (left : a) -> either<a,b>(yield-capturestd/core/hnd/yield-capture: () -> $11759 yield-info())