/*---------------------------------------------------------------------------
  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<1949> : 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<$2123,$2124>)  : 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<$2136,$2137>) : 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<$2123,$2124>, y : marker<$2136,$2137>) -> bool(m1m1: marker<$2123,$2124>,m2m2: marker<$2136,$2137>)


// -------------------------------------------
// 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<$2062,$2060> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,a1a1: V>, yy: marker<$2063,$2061> : markerstd/core/hnd/marker: (E, V) -> V<e2e2: E,a2a2: V> ) : boolstd/core/types/bool: V
  js inline "#1===#2"
  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<$2241> : evvstd/core/hnd/evv: E -> V<e1e1: E>, evev: ev<$2243> : 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<$2282> : 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<$2302> : evvstd/core/hnd/evv: E -> V<ee: E>, evv1evv1: evv<$2302> : 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<$2324> : 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: ($2418) -> $2420 $2419 : 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: $2458 : aa: V, nextnext: ($2458) -> $2460 $2459 : aa: V -> ee: E bb: V )result: -> 2498 2497 : ee: E bb: V
  if yieldingstd/core/hnd/yielding: () -> $2460 bool() then yield-extendstd/core/hnd/yield-extend: (next : ($2458) -> $2460 $2459) -> $2460 $2459(nextnext: ($2458) -> $2460 $2459) else nextnext: ($2458) -> $2460 $2459(xx: $2458)

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: $2508 : aa: V, extendextend: ($2508) -> $2510 $2509 : aa: V -> ee: E bb: V, nextnext: ($2508) -> $2510 $2509 : aa: V -> ee: E bb: V )result: -> 2548 2547 : ee: E bb: V
  if yieldingstd/core/hnd/yielding: () -> $2510 bool() then yield-extendstd/core/hnd/yield-extend: (next : ($2508) -> $2510 $2509) -> $2510 $2509(extendextend: ($2508) -> $2510 $2509) else nextnext: ($2508) -> $2510 $2509(xx: $2508)

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) -> $2559 $2558, a) -> $2559 $2560 : 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<$2608,$2609>: 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<$2653,$2654> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>, clauseclause: ((resume-result<$2651,$2654>) -> $2653 $2654) -> $2653 $2654 : (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<$2709,$2710> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>, clauseclause: ((resume-result<$2707,$2710>) -> $2709 $2710) -> $2709 $2710 : (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<$2761,$2762> : markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>, clauseclause: ((resume-result<$2760,$2762>) -> $2761 $2762) -> $2761 $2762 : (resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> e1e1: E rr: V) -> e1e1: E rr: V )result: -> 2814 2813 : e1e1: E bb: V
  //val w0 = evv-get()
  val gg: () -> $2760 : () -> _b_b: V = yield-to-primstd/core/hnd/yield-to-prim: (m : marker<$2761,$2762>, clause : ((resume-result<$2760,$2762>) -> $2761 $2762) -> $2761 $2762) -> $2761 (() -> $2760)(mm: marker<$2761,$2762>, clauseclause: ((resume-result<$2760,$2762>) -> $2761 $2762) -> $2761 $2762)
  yield-extendstd/core/hnd/yield-extend: (next : (() -> $2761 $2760) -> $2761 $2760) -> $2761 $2760 fnfn: (f : () -> $2761 $2760) -> $2761 $2760(ff: () -> $2761 $2760)
    // val keep1 = guard(w0)  // check the evidence is correctly restored
    ff: () -> $2761 $2760()

abstract struct yield-contextstd/core/hnd/yield-context: V( yldstd/core/hnd/yield-context/yld: (yield-context) -> any : anystd/core/types/any: V )

extern yield-capture-primstd/core/hnd/yield-capture-prim: forall<e> () -> e any() : ee: E anystd/core/types/any: V
  c "kk_yield_capture"
  js "_yield_capture"

extern unsafe-reyield-primstd/core/hnd/unsafe-reyield-prim: forall<a,e> (yld : any) -> e a(yldyld: any : anystd/core/types/any: V) : ee: E aa: V
  c "kk_yield_reyield"
  js "_reyield"

pub fun yield-capturestd/core/hnd/yield-capture: forall<e> () -> e yield-context()result: -> 2907 yield-context : ee: E yield-contextstd/core/hnd/yield-context: V
  Yield-contextstd/core/hnd/Yield-context: (yld : any) -> yield-context(yield-capture-primstd/core/hnd/yield-capture-prim: () -> $2892 any())

pub fun unsafe-reyieldstd/core/hnd/unsafe-reyield: forall<a,e> (yield-context) -> e a(Yield-contextstd/core/hnd/Yield-context: (yld : any) -> yield-context(yldyld: any) : yield-contextstd/core/hnd/yield-context: V )result: -> 2936 2935 : ee: E aa: V
  unsafe-reyield-primstd/core/hnd/unsafe-reyield-prim: (yld : any) -> $2912 $2911(yldyld: any)



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

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

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

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

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


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

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

// mask for builtin effects without a handler or evidence (like `:st` or `:local`)
pub fun @mask-builtin<aa: V,e1e1: E,e2e2: E>( actionaction: () -> $4090 $4089 : () -> e1e1: E aa: V )result: -> 4122 4120 : e2e2: E aa: V
  cast-ev0std/core/hnd/cast-ev0: (f : () -> $4090 $4089) -> $4091 (() -> $4091 $4089)(actionaction: () -> $4090 $4089)()


// -------------------------------------------
// 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<$4134,$4132>:local-varstd/core/types/local-var: (H, V) -> V<ss: H,aa: V>, resres: $4133 : bb: V  )result: -> <div,local<4243>|4244> 4242 : <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<$4134>|$4135> boolyieldingstd/core/hnd/yielding: () -> <div,local<$4134>|$4135> bool() returnreturn: $4133 resres: $4133;
  val vv: $4132 = locloc: $4132
?hdiv=iev@4160
yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> <div,local<$4134>|$4135> $4133, a) -> <div,local<$4134>|$4135> $4133) -> <div,local<$4134>|$4135> $4133(fnfn: forall<a> (cont : (a) -> <div,local<$4134>|$4135> $4133, x : a) -> <div,local<$4134>|$4135> $4133(contcont: ($4183) -> <div,local<$4134>|$4135> $4133,xx: $4183){ locloc: local-var<$4134,$4132> :=std/core/types/local-set: (v : local-var<$4134,$4132>, assigned : $4132) -> <div,local<$4134>|$4135> () vv: $4132; prompt-local-varstd/core/hnd/prompt-local-var: (loc : local-var<$4134,$4132>, res : $4133) -> <div,local<$4134>|$4135> $4133(@byref(locloc: local-var<$4134,$4132>),contcont: ($4183) -> <div,local<$4134>|$4135> $4133(xx: $4183)) }
) // 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: $4278:aa: V, actionaction: (local-var<$4281,$4278>) -> <local<$4281>|$4280> $4279: (@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<4359>|4358> 4357 : <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<$4281>|$4280> $4279) -> <local<$4281>|$4280> $4279 val locloc: local-var<$4281,$4278> : local-varstd/core/types/local-var: (H, V) -> V<__w-l476-c25: H,__w-l476-c27: V> = local-newstd/core/types/local-new: (value : $4278) -> <div,local<$4281>|$4280> local-var<$4281,$4278>(initinit: $4278) val resres: $4279 = cast-ev1std/core/hnd/cast-ev1: (f : (local-var<$4281,$4278>) -> <local<$4281>|$4280> $4279) -> <div,local<$4281>|$4280> ((local-var<$4281,$4278>) -> <div,local<$4281>|$4280> $4279)(actionaction: (local-var<$4281,$4278>) -> <local<$4281>|$4280> $4279)(@byref(locloc: local-var<$4281,$4278>)) prompt-local-varstd/core/hnd/prompt-local-var: (loc : local-var<$4281,$4278>, res : $4279) -> <div,local<$4281>|$4280> $4279(@byref(locloc: local-var<$4281,$4278>),resres: $4279) // ------------------------------------------- // Finally // ------------------------------------------- pub fun finallystd/core/hnd/finally: forall<a,e> (fin : () -> e (), action : () -> e a) -> e a( finfin: () -> $4524 () : () -> ee: E (std/core/types/unit: V)std/core/types/unit: V, actionaction: () -> $4524 $4523 : () -> ee: E aa: V )result: -> 4546 4545 : ee: E aa: V finally-promptstd/core/hnd/finally-prompt: (fin : () -> $4524 (), res : $4523) -> $4524 $4523(finfin: () -> $4524 (), actionaction: () -> $4524 $4523()); fun finally-promptstd/core/hnd/finally-prompt: forall<a,e> (fin : () -> e (), res : a) -> e a(finfin: () -> $4373 () : () -> ee: E (std/core/types/unit: V)std/core/types/unit: V, resres: $4372 : aa: V )result: -> 4516 4515 : ee: E aa: V if !std/core/types/bool/(!): (b : bool) -> $4373 boolyieldingstd/core/hnd/yielding: () -> $4373 bool() then finfin: () -> $4373 ()() if yieldingstd/core/hnd/yielding: () -> $4373 bool() then yield-extendstd/core/hnd/yield-extend: (next : (_4404) -> $4373 $4372) -> $4373 $4372(fnfn: (_4404) -> $4373 $4372(_) resres: $4372) else resres: $4372 elif yielding-non-finalstd/core/hnd/yielding-non-final: () -> $4373 bool() then yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $4373 $4372, a) -> $4373 $4372) -> $4373 $4372(fnfn: forall<a> (cont : (a) -> $4373 $4372, x : a) -> $4373 $4372(contcont: ($4431) -> $4373 $4372,xx: $4431){ finally-promptstd/core/hnd/finally-prompt: (fin : () -> $4373 (), res : $4372) -> $4373 $4372(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : () -> $4373 ()) -> $4373 (() -> $4373 ())(finfin: () -> $4373 ()),contcont: ($4431) -> $4373 $4372(xx: $4431)) }) else val yldyld: yield-context = yield-capturestd/core/hnd/yield-capture: () -> $4373 yield-context() finfin: () -> $4373 ()() if yieldingstd/core/hnd/yielding: () -> $4373 bool() returnreturn: $4372 yield-extendstd/core/hnd/yield-extend: (next : (_4477) -> $4373 $4372) -> $4373 $4372( fnfn: (_4477) -> $4373 $4372(_x) unsafe-reyieldstd/core/hnd/unsafe-reyield: (yield-context) -> $4373 $4372(yldyld: yield-context) )std/core/types/Unit: () unsafe-reyieldstd/core/hnd/unsafe-reyield: (yield-context) -> $4373 $4372(yldyld: yield-context) /* 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) -> $4759 () : (intstd/core/types/int: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V, actionaction: () -> $4759 $4758 : () -> ee: E aa: V )result: -> 4816 4815 : ee: E aa: V initinit: (int) -> $4759 ()(0literal: int
dec = 0
hex8 = 0x00
bit8 = 0b00000000
) if yieldingstd/core/hnd/yielding: () -> $4759 bool() returnreturn: $4758 yield-extendstd/core/hnd/yield-extend: (next : (()) -> $4759 $4758) -> $4759 $4758(fnfn: (()) -> $4759 $4758(_ret:(std/core/types/unit: V)std/core/types/unit: V) initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $4759 (), res : $4758) -> $4759 $4758(initinit: (int) -> $4759 (),actionaction: () -> $4759 $4758()) )std/core/types/Unit: () initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $4759 (), res : $4758) -> $4759 $4758(initinit: (int) -> $4759 (), actionaction: () -> $4759 $4758()
) fun initially-promptstd/core/hnd/initially-prompt: forall<a,e> (init : (int) -> e (), res : a) -> e a( initinit: (int) -> $4554 () : (intstd/core/types/int: V) -> ee: E (std/core/types/unit: V)std/core/types/unit: V, resres: $4553 : aa: V )result: -> 4751 4750 : ee: E aa: V if yielding-non-finalstd/core/hnd/yielding-non-final: () -> $4554 bool() then val countcount: ref<global,int> = unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$4554> ref<global,int>) -> $4554 (() -> $4554 ref<global,int>){refstd/core/types/ref: (value : int) -> <st<global>|$4554> ref<global,int>(0literal: int
dec = 0
hex8 = 0x00
bit8 = 0b00000000
)}() yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $4554 $4553, a) -> $4554 $4553) -> $4554 $4553(fnfn: forall<a> (cont : (a) -> $4554 $4553, x : a) -> $4554 $4553(contcont: ($4596) -> $4554 $4553,xx: $4596) val cntcnt: int = unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$4554> int) -> $4554 (() -> $4554 int){ !std/core/types/ref/(!): (ref : ref<global,int>, @implicit/hdiv : hdiv<global,int,<alloc<global>,write<global>|$4554>>) -> <st<global>|$4554> int
?hdiv=iev@4615
countcount: ref<global,int> }() // increase counter on every resumption unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$4554> ()) -> $4554 (() -> $4554 ()){ countcount: ref<global,int> :=std/core/types/set: (ref : ref<global,int>, assigned : int) -> <st<global>|$4554> () addstd/core/hnd/add: (i : int, j : int) -> <st<global>|$4554> int(cntcnt: int,1literal: int
dec = 1
hex8 = 0x01
bit8 = 0b00000001
) }() if eqstd/core/hnd/eq: (x : int, y : int) -> $4554 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) -> $4554 ()(cntcnt: int) if yieldingstd/core/hnd/yielding: () -> $4554 bool() then { yield-extendstd/core/hnd/yield-extend: (next : (_4684) -> $4554 $4553) -> $4554 $4553( fnfn: (_4684) -> $4554 $4553(_ret) initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $4554 (), res : $4553) -> $4554 $4553(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : (int) -> $4554 ()) -> $4554 ((int) -> $4554 ())(initinit: (int) -> $4554 ()), contcont: ($4596) -> $4554 $4553(xx: $4596)) ); (std/core/types/Unit: ())std/core/types/Unit: () }std/core/types/Unit: () initially-promptstd/core/hnd/initially-prompt: (init : (int) -> $4554 (), res : $4553) -> $4554 $4553(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : (int) -> $4554 ()) -> $4554 ((int) -> $4554 ())(initinit: (int) -> $4554 ()), contcont: ($4596) -> $4554 $4553(xx: $4596)) ) else resres: $4553
// ------------------------------------------- // 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<4858,4861>) -> 4859 4861 : 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<$4951,$4952,$4953,$4954> : resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>, xx: $4951 : bb: V )result: -> 5002 5004 : ee: E rr: V (rr: resume-context<$4951,$4952,$4953,$4954>.kstd/core/hnd/resume-context/k: (resume-context<$4951,$4952,$4953,$4954>) -> $4952 ((resume-result<$4951,$4954>) -> $4952 $4954))(Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(xx: $4951)) 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<$5017,$5018,$5019,$5020> : resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>, xx: $5017 : bb: V )result: -> 5085 5086 : e0e0: E rr: V cast-ev1std/core/hnd/cast-ev1: (f : (resume-result<$5017,$5020>) -> $5018 $5020) -> $5019 ((resume-result<$5017,$5020>) -> $5019 $5020)(rr: resume-context<$5017,$5018,$5019,$5020>.kstd/core/hnd/resume-context/k: (resume-context<$5017,$5018,$5019,$5020>) -> $5019 ((resume-result<$5017,$5020>) -> $5018 $5020))(Shallowstd/core/hnd/Shallow: forall<a,b> (result : a) -> resume-result<a,b>(xx: $5017)) 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<$5099,$5100,$5101,$5102> : resume-contextstd/core/hnd/resume-context: (V, E, E, V) -> V<bb: V,ee: E,e0e0: E,rr: V>, xx: $5102 : rr: V )result: -> 5150 5152 : ee: E rr: V //finalize(r.k,x) (rr: resume-context<$5099,$5100,$5101,$5102>.kstd/core/hnd/resume-context/k: (resume-context<$5099,$5100,$5101,$5102>) -> $5100 ((resume-result<$5099,$5102>) -> $5100 $5102))(Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>(xx: $5102)) // ------------------------------------------- // Clauses // ------------------------------------------- abstract value type clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<aa: V::V,bb: V::V,hh: (E, V) -> V::(E,V)->V,ee: E::E,rr: V::V> Clause1std/core/hnd/Clause1: forall<a,b,c,e,d> (clause : (marker<e,d>, ev<c>, a) -> e b) -> clause1<a,b,c,e,d>( clausestd/core/hnd/clause1/clause: forall<a,b,c,e,d> (clause1 : clause1<a,b,c,e,d>) -> ((marker<e,d>, ev<c>, a) -> e b): (markerstd/core/hnd/marker: (E, V) -> V<ee: E,rr: V>, evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, aa: V) -> ee: E bb: V ) inline extern cast-clause0std/core/hnd/cast-clause0: forall<a,e,e1,b,c> (f : (marker<e1,c>, ev<b>) -> e1 a) -> e ((marker<e1,c>, ev<b>) -> e a)( f : (markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>,evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>) -> e1e1: E bb: V) : ee: E ((markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>,evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>) -> ee: E bb: V) inline "#1" inline extern cast-clause1std/core/hnd/cast-clause1: forall<a,b,e,e1,c,d> (f : (marker<e1,d>, ev<c>, a) -> e1 b) -> e ((marker<e1,d>, ev<c>, a) -> e b)( f : (markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>,evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>,aa: V) -> e1e1: E bb: V) : ee: E ((markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>,evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>,aa: V) -> ee: E bb: V) inline "#1" inline extern cast-clause2std/core/hnd/cast-clause2: forall<a,b,c,e,e1,d,a1> (f : (marker<e1,a1>, ev<d>, a, b) -> e1 c) -> e ((marker<e1,a1>, ev<d>, a, b) -> e c)( f : (markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>,evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>,a1a1: V,a2a2: V) -> e1e1: E bb: V) : ee: E ((markerstd/core/hnd/marker: (E, V) -> V<e1e1: E,rr: V>,evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>,a1a1: V,a2a2: V) -> ee: E bb: V) inline "#1" pub inline fun @perform1<aa: V,bb: V,hh: (E, V) -> V>( evev: ev<$5321> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($5321<e,a>) -> clause1<$5319,$5320,$5321,e,a> : (forall<e1e1: E,rr: V> hh: (E, V) -> V<e1e1: E,rr: V> -> clause1std/core/hnd/clause1: (V, V, (E, V) -> V, E, V) -> V<aa: V,bb: V,hh: (E, V) -> V,e1e1: E,rr: V>), xx: $5319 : aa: V )result: -> 5410 5408 : ee: E bb: V match evev: ev<$5321> Evstd/core/hnd/Ev: forall<a,e,b> (htag : htag<a>, marker : marker<e,b>, hnd : a<e,b>, hevv : evv<e>) -> ev<a>(_tag,mm: marker<$5328,$5329>,hh: $5321<$5328,$5329>,_w) -> match hh: $5321<$5328,$5329>.opop: ($5321<$5328,$5329>) -> $5322 clause1<$5319,$5320,$5321,$5328,$5329> Clause1std/core/hnd/Clause1: forall<a,b,c,e,d> (clause : (marker<e,d>, ev<c>, a) -> e b) -> clause1<a,b,c,e,d>(ff: (marker<$5328,$5329>, ev<$5321>, $5319) -> $5328 $5320) -> cast-clause1std/core/hnd/cast-clause1: (f : (marker<$5328,$5329>, ev<$5321>, $5319) -> $5328 $5320) -> $5322 ((marker<$5328,$5329>, ev<$5321>, $5319) -> $5322 $5320)(ff: (marker<$5328,$5329>, ev<$5321>, $5319) -> $5328 $5320)(mm: marker<$5328,$5329>,evev: ev<$5321>,xx: $5319) fun evv-swap-withstd/core/hnd/evv-swap-with: forall<a,e> (ev : ev<a>) -> evv<e>(evev: ev<$5425> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>)result: -> total evv<5466> match(evev: ev<$5425>) 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<$5431>) -> evv-swapstd/core/hnd/evv-swap: (w : evv<$5431>) -> evv<_5448>(ww: evv<$5431>) inline fun under1std/core/hnd/under1: forall<a,b,e,c> (ev : ev<c>, op : (a) -> e b, x : a) -> e b( evev: ev<$5590> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($5587) -> $5589 $5588 : aa: V -> ee: E bb: V, xx: $5587 : aa: V )result: -> 5686 5685 : ee: E bb: V val w0w0: evv<_5598> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$5590>) -> $5589 evv<_5598>(evev: ev<$5590>) val yy: $5588 = opop: ($5587) -> $5589 $5588(xx: $5587) // evv-set(w0) // only needed before yielding for evidence expected check in prompt if yieldingstd/core/hnd/yielding: () -> $5589 bool() returnreturn: $5588 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5589 $5588, a) -> $5589 $5588) -> $5589 $5588( fnfn: forall<a> (cont : (a) -> $5589 $5588, res : a) -> $5589 $5588(contcont: ($5622) -> $5589 $5588,resres: $5622) under1xstd/core/hnd/under1x: (ev : ev<$5590>, op : ($5622) -> $5589 $5588, x : $5622) -> $5589 $5588(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev<$5590>) -> $5589 ev<$5590>(evev: ev<$5590>),contcont: ($5622) -> $5589 $5588,resres: $5622) )std/core/types/Unit: () evv-setstd/core/hnd/evv-set: (w : evv<_5598>) -> $5589 ()(w0w0: evv<_5598>) yy: $5588 // 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<$5477> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($5474) -> $5476 $5475 : aa: V -> ee: E bb: V, xx: $5474 : aa: V )result: -> 5573 5572 : ee: E bb: V val w0w0: evv<_5485> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$5477>) -> $5476 evv<_5485>(evev: ev<$5477>) val yy: $5475 = opop: ($5474) -> $5476 $5475(xx: $5474) // evv-set(w0) // only needed before yielding for evidence expected check in prompt if yieldingstd/core/hnd/yielding: () -> $5476 bool() returnreturn: $5475 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $5476 $5475, a) -> $5476 $5475) -> $5476 $5475( fnfn: forall<a> (cont : (a) -> $5476 $5475, res : a) -> $5476 $5475(contcont: ($5509) -> $5476 $5475,resres: $5509) under1xstd/core/hnd/under1x: (ev : ev<$5477>, op : ($5509) -> $5476 $5475, x : $5509) -> $5476 $5475(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev<$5477>) -> $5476 ev<$5477>(evev: ev<$5477>),contcont: ($5509) -> $5476 $5475,resres: $5509) )std/core/types/Unit: () evv-setstd/core/hnd/evv-set: (w : evv<_5485>) -> $5476 ()(w0w0: evv<_5485>) yy: $5475 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 : $5700, r : resume-context<$5701,$5702,$5703,$5705>) -> $5702 $5705 : (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<5785,5786,5789,5787,5790> : 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<$5702,$5705>, ev<$5704>, x : $5700) -> $5702 $5701(mm: marker<$5702,$5705>,_ev,xx: $5700){ yield-tostd/core/hnd/yield-to: (m : marker<$5702,$5705>, clause : ((resume-result<$5701,$5705>) -> $5702 $5705) -> $5702 $5705) -> $5702 $5701(mm: marker<$5702,$5705>, fnfn: (k : (resume-result<$5701,$5705>) -> $5702 $5705) -> $5702 $5705(kk: (resume-result<$5701,$5705>) -> $5702 $5705){ opop: (x : $5700, r : resume-context<$5701,$5702,$5703,$5705>) -> $5702 $5705(xx: $5700,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<$5701,$5705>) -> $5702 $5705)) } ) } ) fun getstd/core/hnd/get: forall<a,h> (ref : ref<h,a>) -> <div,read<h>> a( refref: ref<$5811,$5810>: refstd/core/types/ref: (H, V) -> V<hh: H,aa: V>)result: -> <read<5839>,div> 5838 : <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<$5811,$5810>, @implicit/hdiv : hdiv<$5811,$5810,div>) -> <div,read<$5811>> $5810
?hdiv=iev@5815
refref: ref<$5811,$5810>
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" type protect-statestd/core/hnd/protect-state: (V, V, E) -> V<bb: V,rr: V,ee: E> NeedsFinalizationstd/core/hnd/NeedsFinalization: forall<a,b,e> (k : (resume-result<a,b>) -> e b) -> protect-state<a,b,e>(k : resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V) NoFinalizationstd/core/hnd/NoFinalization: forall<a,b,e> protect-state<a,b,e> fun protect-promptstd/core/hnd/protect-prompt: forall<a,e,b> (resumed : ref<global,protect-state<a,b,e>>, res : b) -> e b( resumedresumed: ref<global,protect-state<$5909,$5911,$5910>> : refstd/core/types/ref: (H, V) -> V<globalstd/core/types/global: H,protect-statestd/core/hnd/protect-state: (V, V, E) -> V<bb: V,rr: V,ee: E>>, resres: $5911 : rr: V)result: -> 6121 6122 : ee: E rr: V // `@Hnodiv` is consumed by the divergence checker via implicit parameters: // because `resumed` lives in `global` state we'd otherwise be flagged as // potentially divergent through self-reference; binding `@Hnodiv` here // satisfies the checker that this prompt does not introduce divergence. val hdivhdiv: hdiv<global,protect-state<$5909,$5911,$5910>,<alloc<global>,write<global>|$5910>>=@Hnodiv val did-resumedid-resume: protect-state<$5909,$5911,$5910> : some<bb: V,rr: V,ee: E> protect-statestd/core/hnd/protect-state: (V, V, E) -> V<bb: V,rr: V,ee: E> = (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$5910> protect-state<$5909,$5911,$5910>) -> $5910 (() -> $5910 protect-state<$5909,$5911,$5910>){ !std/core/types/ref/(!): (ref : ref<global,protect-state<$5909,$5911,$5910>>, @implicit/hdiv : hdiv<global,protect-state<$5909,$5911,$5910>,<alloc<global>,write<global>|$5910>>) -> <st<global>|$5910> protect-state<$5909,$5911,$5910>
?hdiv=hdiv
resumedresumed: ref<global,protect-state<$5909,$5911,$5910>> })() match did-resumedid-resume: protect-state<$5909,$5911,$5910> NoFinalizationstd/core/hnd/NoFinalization: forall<a,b,e> protect-state<a,b,e> -> // resumed already, no need to protect resres: $5911 NeedsFinalizationstd/core/hnd/NeedsFinalization: forall<a,b,e> (k : (resume-result<a,b>) -> e b) -> protect-state<a,b,e>(kk: (resume-result<$5909,$5911>) -> $5910 $5911) -> if !std/core/types/bool/(!): (b : bool) -> $5910 boolyieldingstd/core/hnd/yielding: () -> $5910 bool() then // otherwise, if we are not yielding, resume k with finalization (to run all finally clauses) kk: (resume-result<$5909,$5911>) -> $5910 $5911(Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>(resres: $5911)) elif yielding-non-finalstd/core/hnd/yielding-non-final: () -> $5910 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) -> $5910 $5911, a) -> $5910 $5911) -> $5910 $5911( fnfn: forall<a> (cont : (a) -> $5910 $5911, x : a) -> $5910 $5911(contcont: ($6017) -> $5910 $5911,xx: $6017) protect-promptstd/core/hnd/protect-prompt: (resumed : ref<global,protect-state<$5909,$5911,$5910>>, res : $5911) -> $5910 $5911(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ref<global,protect-state<$5909,$5911,$5910>>) -> $5910 ref<global,protect-state<$5909,$5911,$5910>>(resumedresumed: ref<global,protect-state<$5909,$5911,$5910>>),contcont: ($6017) -> $5910 $5911(xx: $6017)) ) else // if we are in a final yield, capture it, resume k with finalization, and reyield val yldyld: yield-context = yield-capturestd/core/hnd/yield-capture: () -> $5910 yield-context() kk: (resume-result<$5909,$5911>) -> $5910 $5911(Finalizestd/core/hnd/Finalize: forall<a,b> (result : b) -> resume-result<a,b>(resres: $5911)) if yieldingstd/core/hnd/yielding: () -> $5910 bool() returnreturn: $5911 yield-extendstd/core/hnd/yield-extend: (next : (_6077) -> $5910 $5911) -> $5910 $5911( fnfn: (_6077) -> $5910 $5911(_x) unsafe-reyieldstd/core/hnd/unsafe-reyield: (yield-context) -> $5910 $5911(yldyld: yield-context) )std/core/types/Unit: () // yikes, a finally clause is itself yielding... unsafe-reyieldstd/core/hnd/unsafe-reyield: (yield-context) -> $5910 $5911(yldyld: yield-context
) 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: $6132 : aa: V, clauseclause: (x : $6132, k : ($6133) -> $6134 $6135) -> $6134 $6135 : (x:aa: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V, kk: (resume-result<$6133,$6135>) -> $6134 $6135 : resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V )result: -> 6259 6260 : ee: E rr: V val resumedresumed: ref<global,protect-state<$6133,$6135,$6134>> = (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$6134> ref<global,protect-state<$6133,$6135,$6134>>) -> $6134 (() -> $6134 ref<global,protect-state<$6133,$6135,$6134>>){refstd/core/types/ref: (value : protect-state<$6133,$6135,$6134>) -> <st<global>|$6134> ref<global,protect-state<$6133,$6135,$6134>>(NeedsFinalizationstd/core/hnd/NeedsFinalization: forall<a,b,e> (k : (resume-result<a,b>) -> e b) -> protect-state<a,b,e>(kk: (resume-result<$6133,$6135>) -> $6134 $6135))})() fun kprotectkprotect: (ret : $6133) -> $6134 $6135(retret: $6133)result: -> $6134 $6135 (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$6134> ()) -> $6134 (() -> $6134 ()){resumedresumed: ref<global,protect-state<$6133,$6135,$6134>> :=std/core/types/set: (ref : ref<global,protect-state<$6133,$6135,$6134>>, assigned : protect-state<$6133,$6135,$6134>) -> <st<global>|$6134> () NoFinalizationstd/core/hnd/NoFinalization: forall<a,b,e> protect-state<a,b,e>})() kk: (resume-result<$6133,$6135>) -> $6134 $6135(Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(retret: $6133)) val resres: $6135 = clauseclause: (x : $6132, k : ($6133) -> $6134 $6135) -> $6134 $6135(xx: $6132,kprotectkprotect: (ret : $6133) -> $6134 $6135) protect-promptstd/core/hnd/protect-prompt: (resumed : ref<global,protect-state<$6133,$6135,$6134>>, res : $6135) -> $6134 $6135(resumedresumed: ref<global,protect-state<$6133,$6135,$6134>>,resres: $6135) /* 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 : $6273, k : ($6274) -> $6275 $6277) -> $6275 $6277 : (x:aa: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause1<6350,6351,6353,6352,6354> : 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<$6275,$6277>, ev<$6276>, x : $6273) -> $6275 $6274(mm: marker<$6275,$6277>,_ev,xx: $6273){ yield-tostd/core/hnd/yield-to: (m : marker<$6275,$6277>, clause : ((resume-result<$6274,$6277>) -> $6275 $6277) -> $6275 $6277) -> $6275 $6274(mm: marker<$6275,$6277>, fnfn: (k : (resume-result<$6274,$6277>) -> $6275 $6277) -> $6275 $6277(kk: (resume-result<$6274,$6277>) -> $6275 $6277) protectstd/core/hnd/protect: (x : $6273, clause : (x : $6273, k : ($6274) -> $6275 $6277) -> $6275 $6277, k : (resume-result<$6274,$6277>) -> $6275 $6277) -> $6275 $6277(xx: $6273,clauseclause: (x : $6273, k : ($6274) -> $6275 $6277) -> $6275 $6277,kk: (resume-result<$6274,$6277>) -> $6275 $6277) ) }) // 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: ($6374) -> $6371 $6375 : aa: V -> ee: E bb: V)result: -> total clause1<6438,6439,6437,6435,6436> : 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<$6371,$6372>, ev : ev<$6373>, x : $6374) -> $6371 $6375(_m,evev: ev<$6373>,xx: $6374){ under1std/core/hnd/under1: (ev : ev<$6373>, op : ($6374) -> $6371 $6375, x : $6374) -> $6371 $6375(evev: ev<$6373>,opop: ($6374) -> $6371 $6375,xx: $6374) }) // 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: ($6459) -> $6456 $6460 : aa: V -> ee: E bb: V)result: -> total clause1<6509,6510,6508,6506,6507> : 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<$6456,$6457>, ev<$6458>, x : $6459) -> $6456 $6460(_m,_ev,xx: $6459){ opop: ($6459) -> $6456 $6460(xx: $6459) }) // 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: ($6527) -> $6529 $6531 : aa: V -> ee: E rr: V )result: -> total clause1<6593,6594,6596,6595,6597> : 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<$6529,$6531>, ev<$6530>, x : $6527) -> $6529 $6528(mm: marker<$6529,$6531>,_ev,xx: $6527){ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$6529,$6531>, clause : ((resume-result<$6528,$6531>) -> $6529 $6531) -> $6529 $6531) -> $6529 $6528(mm: marker<$6529,$6531>, fnfn: ((resume-result<$6528,$6531>) -> $6529 $6531) -> $6529 $6531(_k) opop: ($6527) -> $6529 $6531(xx: $6527) ) }) //---------------------------------------------------------------- // 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<$6744> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($6744<e,a>) -> clause0<$6742,$6744,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: -> 6820 6819 : ee: E bb: V match evev: ev<$6744> 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<$6750,$6751>,hh: $6744<$6750,$6751>,_w) -> match hh: $6744<$6750,$6751>.opop: ($6744<$6750,$6751>) -> $6743 clause0<$6742,$6744,$6750,$6751> Clause0std/core/hnd/Clause0: forall<a,b,e,c> (clause : (marker<e,c>, ev<b>) -> e a) -> clause0<a,b,e,c>(ff: (marker<$6750,$6751>, ev<$6744>) -> $6750 $6742) -> cast-clause0std/core/hnd/cast-clause0: (f : (marker<$6750,$6751>, ev<$6744>) -> $6750 $6742) -> $6743 ((marker<$6750,$6751>, ev<$6744>) -> $6743 $6742)(ff: (marker<$6750,$6751>, ev<$6744>) -> $6750 $6742)(mm: marker<$6750,$6751>,evev: ev<$6744>) inline fun under0std/core/hnd/under0: forall<a,e,b> (ev : ev<b>, op : () -> e a) -> e a( evev: ev<$6835> : evstd/core/hnd/ev: ((E, V) -> V) -> V<ii: (E, V) -> V>, opop: () -> $6834 $6833 : () -> ee: E bb: V)result: -> 6918 6917 : ee: E bb: V val w0w0: evv<_6843> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$6835>) -> $6834 evv<_6843>(evev: ev<$6835>) val yy: $6833 = opop: () -> $6834 $6833() // evv-set(w0) // only needed before yielding for evidence expected check in prompt evv-setstd/core/hnd/evv-set: (w : evv<_6843>) -> $6834 ()(w0w0: evv<_6843>) if yieldingstd/core/hnd/yielding: () -> $6834 bool() returnreturn: $6833 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $6834 $6833, a) -> $6834 $6833) -> $6834 $6833( fnfn: forall<a> (cont : (a) -> $6834 $6833, res : a) -> $6834 $6833(contcont: ($6875) -> $6834 $6833,resres: $6875) under1std/core/hnd/under1: (ev : ev<$6835>, op : ($6875) -> $6834 $6833, x : $6875) -> $6834 $6833(evev: ev<$6835>,contcont: ($6875) -> $6834 $6833,resres: $6875) )std/core/types/Unit: () yy: $6833 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<$6929,$6930,$6931,$6933>) -> $6930 $6933 : 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<7005,7008,7006,7009> : 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<$6930,$6933>, ev<$6932>) -> $6930 $6929(mm: marker<$6930,$6933>,_ev){ yield-tostd/core/hnd/yield-to: (m : marker<$6930,$6933>, clause : ((resume-result<$6929,$6933>) -> $6930 $6933) -> $6930 $6933) -> $6930 $6929(mm: marker<$6930,$6933>, fnfn: (k : (resume-result<$6929,$6933>) -> $6930 $6933) -> $6930 $6933(kk: (resume-result<$6929,$6933>) -> $6930 $6933){ opop: (resume-context<$6929,$6930,$6931,$6933>) -> $6930 $6933(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<$6929,$6933>) -> $6930 $6933)) } ) }) /* 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: (($7026) -> $7027 $7029) -> $7027 $7029 : (bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause0<7098,7100,7099,7101> : 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<$7027,$7029>, ev<$7028>) -> $7027 $7026(mm: marker<$7027,$7029>,_ev){ yield-tostd/core/hnd/yield-to: (m : marker<$7027,$7029>, clause : ((resume-result<$7026,$7029>) -> $7027 $7029) -> $7027 $7029) -> $7027 $7026(mm: marker<$7027,$7029>, fnfn: (k : (resume-result<$7026,$7029>) -> $7027 $7029) -> $7027 $7029(kk: (resume-result<$7026,$7029>) -> $7027 $7029){ protectstd/core/hnd/protect: (x : (), clause : (x : (), k : ($7026) -> $7027 $7029) -> $7027 $7029, k : (resume-result<$7026,$7029>) -> $7027 $7029) -> $7027 $7029((std/core/types/Unit: ())std/core/types/Unit: (),fnfn: ((), r : ($7026) -> $7027 $7029) -> $7027 $7029(_x,rr: ($7026) -> $7027 $7029){ opop: (($7026) -> $7027 $7029) -> $7027 $7029(rr: ($7026) -> $7027 $7029) }, kk: (resume-result<$7026,$7029>) -> $7027 $7029) }) }) 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: () -> $7115 $7118 : () -> ee: E bb: V)result: -> total clause0<7170,7169,7167,7168> : 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<$7115,$7116>, ev : ev<$7117>) -> $7115 $7118(_m,evev: ev<$7117>){ under0std/core/hnd/under0: (ev : ev<$7117>, op : () -> $7115 $7118) -> $7115 $7118(evev: ev<$7117>,opop: () -> $7115 $7118) }) 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: () -> $7184 $7187 : () -> ee: E bb: V)result: -> total clause0<7228,7227,7225,7226> : 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<$7184,$7185>, ev<$7186>) -> $7184 $7187(_m,_ev){ opop: () -> $7184 $7187() }) pub fun clause-valuestd/core/hnd/clause-value: forall<a,e,b,c> (v : a) -> clause0<a,b,e,c>(vv: $7242 : bb: V)result: -> total clause0<7282,7284,7283,7285> : 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<$7243,$7245>, ev<$7244>) -> $7243 $7242(_m,_ev){ vv: $7242 }) pub fun clause-never0std/core/hnd/clause-never0: forall<a,e,b,c> (op : () -> e c) -> clause0<a,b,e,c>( opop: () -> $7300 $7302 : () -> ee: E rr: V )result: -> total clause0<7356,7358,7357,7359> : 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<$7300,$7302>, ev<$7301>) -> $7300 $7299(mm: marker<$7300,$7302>,_ev){ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$7300,$7302>, clause : ((resume-result<$7299,$7302>) -> $7300 $7302) -> $7300 $7302) -> $7300 $7299(mm: marker<$7300,$7302>, fnfn: ((resume-result<$7299,$7302>) -> $7300 $7302) -> $7300 $7302(_k){ opop: () -> $7300 $7302() }) }) //---------------------------------------------------------------- // 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<$7557> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($7553, $7554) -> $7556 $7555 : (a1a1: V,a2a2: V) -> ee: E bb: V, x1x1: $7553 : a1a1: V, x2x2: $7554 : a2a2: V )result: -> 7652 7651 : ee: E bb: V val w0w0: evv<_7565> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$7557>) -> $7556 evv<_7565>(evev: ev<$7557>) val zz: $7555 = opop: ($7553, $7554) -> $7556 $7555(x1x1: $7553,x2x2: $7554) evv-setstd/core/hnd/evv-set: (w : evv<_7565>) -> $7556 ()(w0w0: evv<_7565>) if yieldingstd/core/hnd/yielding: () -> $7556 bool() returnreturn: $7555 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $7556 $7555, a) -> $7556 $7555) -> $7556 $7555( fnfn: forall<a> (cont : (a) -> $7556 $7555, res : a) -> $7556 $7555(contcont: ($7599) -> $7556 $7555,resres: $7599) under1std/core/hnd/under1: (ev : ev<$7557>, op : ($7599) -> $7556 $7555, x : $7599) -> $7556 $7555(evev: ev<$7557>,contcont: ($7599) -> $7556 $7555,resres: $7599) )std/core/types/Unit: () zz: $7555 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: $7669 : a1a1: V, x2x2: $7670:a2a2: V, clauseclause: (x : $7669, x : $7670, k : ($7671) -> $7672 $7673) -> $7672 $7673 : (x:a1a1: V,x:a2a2: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V, kk: (resume-result<$7671,$7673>) -> $7672 $7673 : resume-resultstd/core/hnd/resume-result: (V, V) -> V<bb: V,rr: V> -> ee: E rr: V )result: -> 7803 7804 : ee: E rr: V val resumedresumed: ref<global,protect-state<$7671,$7673,$7672>> = (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$7672> ref<global,protect-state<$7671,$7673,$7672>>) -> $7672 (() -> $7672 ref<global,protect-state<$7671,$7673,$7672>>){refstd/core/types/ref: (value : protect-state<$7671,$7673,$7672>) -> <st<global>|$7672> ref<global,protect-state<$7671,$7673,$7672>>(NeedsFinalizationstd/core/hnd/NeedsFinalization: forall<a,b,e> (k : (resume-result<a,b>) -> e b) -> protect-state<a,b,e>(kk: (resume-result<$7671,$7673>) -> $7672 $7673))})() fun kprotectkprotect: (ret : $7671) -> $7672 $7673(retret: $7671)result: -> $7672 $7673 (unsafe-ststd/core/hnd/unsafe-st: (f : () -> <st<global>|$7672> ()) -> $7672 (() -> $7672 ()){ resumedresumed: ref<global,protect-state<$7671,$7673,$7672>> :=std/core/types/set: (ref : ref<global,protect-state<$7671,$7673,$7672>>, assigned : protect-state<$7671,$7673,$7672>) -> <st<global>|$7672> () NoFinalizationstd/core/hnd/NoFinalization: forall<a,b,e> protect-state<a,b,e> })() kk: (resume-result<$7671,$7673>) -> $7672 $7673(Deepstd/core/hnd/Deep: forall<a,b> (result : a) -> resume-result<a,b>(retret: $7671)) val resres: $7673 = clauseclause: (x : $7669, x : $7670, k : ($7671) -> $7672 $7673) -> $7672 $7673(x1x1: $7669,x2x2: $7670,kprotectkprotect: (ret : $7671) -> $7672 $7673) protect-promptstd/core/hnd/protect-prompt: (resumed : ref<global,protect-state<$7671,$7673,$7672>>, res : $7673) -> $7672 $7673(resumedresumed: ref<global,protect-state<$7671,$7673,$7672>>,resres: $7673) 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 : $7820, x2 : $7821, k : ($7822) -> $7823 $7825) -> $7823 $7825 : (x1:a1a1: V, x2:a2a2: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause2<7909,7910,7911,7913,7912,7914> : 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<$7823,$7825>, ev<$7824>, x1 : $7820, x2 : $7821) -> $7823 $7822(mm: marker<$7823,$7825>,_ev,x1x1: $7820,x2x2: $7821){ yield-tostd/core/hnd/yield-to: (m : marker<$7823,$7825>, clause : ((resume-result<$7822,$7825>) -> $7823 $7825) -> $7823 $7825) -> $7823 $7822(mm: marker<$7823,$7825>, fnfn: (k : (resume-result<$7822,$7825>) -> $7823 $7825) -> $7823 $7825(kk: (resume-result<$7822,$7825>) -> $7823 $7825){ protect2std/core/hnd/protect2: (x1 : $7820, x2 : $7821, clause : (x : $7820, x : $7821, k : ($7822) -> $7823 $7825) -> $7823 $7825, k : (resume-result<$7822,$7825>) -> $7823 $7825) -> $7823 $7825(x1x1: $7820,x2x2: $7821,clauseclause: (x1 : $7820, x2 : $7821, k : ($7822) -> $7823 $7825) -> $7823 $7825,kk: (resume-result<$7822,$7825>) -> $7823 $7825) }) }) 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 : $7934, x2 : $7935, r : resume-context<$7936,$7937,$7938,$7940>) -> $7937 $7940 : (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<8028,8029,8030,8033,8031,8034> : 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<$7937,$7940>, ev<$7939>, x1 : $7934, x2 : $7935) -> $7937 $7936(mm: marker<$7937,$7940>,_ev,x1x1: $7934,x2x2: $7935){ yield-tostd/core/hnd/yield-to: (m : marker<$7937,$7940>, clause : ((resume-result<$7936,$7940>) -> $7937 $7940) -> $7937 $7940) -> $7937 $7936(mm: marker<$7937,$7940>, fnfn: (k : (resume-result<$7936,$7940>) -> $7937 $7940) -> $7937 $7940(kk: (resume-result<$7936,$7940>) -> $7937 $7940){ opop: (x1 : $7934, x2 : $7935, r : resume-context<$7936,$7937,$7938,$7940>) -> $7937 $7940(x1x1: $7934,x2x2: $7935,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<$7936,$7940>) -> $7937 $7940)) } ) }) 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: ($8060, $8061) -> $8057 $8062 : (a1a1: V,a2a2: V) -> ee: E bb: V)result: -> total clause2<8136,8137,8138,8135,8133,8134> : 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<$8057,$8058>, ev : ev<$8059>, x1 : $8060, x2 : $8061) -> $8057 $8062(mm: marker<$8057,$8058>,evev: ev<$8059>,x1x1: $8060,x2x2: $8061){ under2std/core/hnd/under2: (ev : ev<$8059>, op : ($8060, $8061) -> $8057 $8062, x1 : $8060, x2 : $8061) -> $8057 $8062(evev: ev<$8059>,opop: ($8060, $8061) -> $8057 $8062,x1x1: $8060,x2x2: $8061) }) 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: ($8161, $8162) -> $8158 $8163 : (a1a1: V,a2a2: V) -> ee: E bb: V)result: -> total clause2<8220,8221,8222,8219,8217,8218> : 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<$8158,$8159>, ev<$8160>, x1 : $8161, x2 : $8162) -> $8158 $8163(_m,_ev,x1x1: $8161,x2x2: $8162){ opop: ($8161, $8162) -> $8158 $8163(x1x1: $8161,x2x2: $8162) }) pub inline fun @perform2( evxevx: ev<$8246> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($8246<e,a>) -> clause2<$8242,$8243,$8244,$8246,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: $8242 : aa: V, yy: $8243 : bb: V )result: -> 8344 8343 : ee: E cc: V match evxevx: ev<$8246> 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<$8252,$8253>,hh: $8246<$8252,$8253>,_w) -> match hh: $8246<$8252,$8253>.opop: ($8246<$8252,$8253>) -> $8245 clause2<$8242,$8243,$8244,$8246,$8252,$8253> 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<$8252,$8253>, ev<$8246>, $8242, $8243) -> $8252 $8244) -> cast-clause2std/core/hnd/cast-clause2: (f : (marker<$8252,$8253>, ev<$8246>, $8242, $8243) -> $8252 $8244) -> $8245 ((marker<$8252,$8253>, ev<$8246>, $8242, $8243) -> $8245 $8244)(ff: (marker<$8252,$8253>, ev<$8246>, $8242, $8243) -> $8252 $8244)(mm: marker<$8252,$8253>,evxevx: ev<$8246>,xx: $8242,yy: $8243) 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: ($8363, $8364) -> $8366 $8368 : (a1a1: V,a2a2: V) -> ee: E rr: V )result: -> total clause2<8438,8439,8440,8442,8441,8443> : 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<$8366,$8368>, ev<$8367>, x1 : $8363, x2 : $8364) -> $8366 $8365(mm: marker<$8366,$8368>,_ev,x1x1: $8363,x2x2: $8364){ yield-to-finalstd/core/hnd/yield-to-final: (m : marker<$8366,$8368>, clause : ((resume-result<$8365,$8368>) -> $8366 $8368) -> $8366 $8368) -> $8366 $8365(mm: marker<$8366,$8368>, fnfn: ((resume-result<$8365,$8368>) -> $8366 $8368) -> $8366 $8368(_k){ opop: ($8363, $8364) -> $8366 $8368(x1x1: $8363,x2x2: $8364) }) }) //---------------------------------------------------------------- // 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<$8466> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($8466<e,a>) -> clause1<$8463,$8464,$8466,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: $8463 : aa: V )result: -> 8553 8552 : ee: E bb: V match evev: ev<$8466> 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<$8472,$8473>,hh: $8466<$8472,$8473>,_w) -> match hh: $8466<$8472,$8473>.opop: ($8466<$8472,$8473>) -> $8465 clause1<$8463,$8464,$8466,$8472,$8473> 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<$8472,$8473>, ev<$8466>, $8463) -> $8472 $8464) -> cast-clause1std/core/hnd/cast-clause1: (f : (marker<$8472,$8473>, ev<$8466>, $8463) -> $8472 $8464) -> $8465 ((marker<$8472,$8473>, ev<$8466>, $8463) -> $8465 $8464)(ff: (marker<$8472,$8473>, ev<$8466>, $8463) -> $8472 $8464)(mm: marker<$8472,$8473>,evev: ev<$8466>,xx: $8463) 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 : $8569, x2 : $8570, x3 : $8571, r : resume-context<$8572,$8573,$8574,$8576>) -> $8573 $8576 : (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<(8650, 8651, 8652),8653,8656,8654,8657> : 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 : ($8569, $8570, $8571), r : resume-context<$8572,$8573,$8574,$8576>) -> $8573 $8576) -> clause1<($8569, $8570, $8571),$8572,$8575,$8573,$8576>( fnfn: (($8569, $8570, $8571), r : resume-context<$8572,$8573,$8574,$8576>) -> $8573 $8576((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8569,x2x2: $8570,x3x3: $8571)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c),rr: resume-context<$8572,$8573,$8574,$8576>){ opop: (x1 : $8569, x2 : $8570, x3 : $8571, r : resume-context<$8572,$8573,$8574,$8576>) -> $8573 $8576(x1x1: $8569,x2x2: $8570,x3x3: $8571,rr: resume-context<$8572,$8573,$8574,$8576>) } ) 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 : $8683, x2 : $8684, x3 : $8685, k : ($8686) -> $8687 $8689) -> $8687 $8689 : (x1:a1a1: V, x2:a2a2: V, x3:a3a3: V, k: bb: V -> ee: E rr: V) -> ee: E rr: V )result: -> total clause1<(8756, 8757, 8758),8759,8761,8760,8762> : 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 : ($8683, $8684, $8685), k : ($8686) -> $8687 $8689) -> $8687 $8689) -> clause1<($8683, $8684, $8685),$8686,$8688,$8687,$8689>( fnfn: (($8683, $8684, $8685), k : ($8686) -> $8687 $8689) -> $8687 $8689((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8683,x2x2: $8684,x3x3: $8685)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c),kk: ($8686) -> $8687 $8689){ opop: (x1 : $8683, x2 : $8684, x3 : $8685, k : ($8686) -> $8687 $8689) -> $8687 $8689(x1x1: $8683,x2x2: $8684,x3x3: $8685,kk: ($8686) -> $8687 $8689) } ) 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: ($8788, $8789, $8790) -> $8785 $8791 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E bb: V)result: -> total clause1<(8860, 8861, 8862),8863,8859,8857,8858> : 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 : (($8788, $8789, $8790)) -> $8785 $8791) -> clause1<($8788, $8789, $8790),$8791,$8787,$8785,$8786>( fnfn: (($8788, $8789, $8790)) -> $8785 $8791((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8788,x2x2: $8789,x3x3: $8790)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) ){ opop: ($8788, $8789, $8790) -> $8785 $8791(x1x1: $8788,x2x2: $8789,x3x3: $8790) } ) 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: ($8889, $8890, $8891) -> $8886 $8892 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E bb: V)result: -> total clause1<(8961, 8962, 8963),8964,8960,8958,8959> : 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 : (($8889, $8890, $8891)) -> $8886 $8892) -> clause1<($8889, $8890, $8891),$8892,$8888,$8886,$8887>( fnfn: (($8889, $8890, $8891)) -> $8886 $8892((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8889,x2x2: $8890,x3x3: $8891)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)){ opop: ($8889, $8890, $8891) -> $8886 $8892(x1x1: $8889,x2x2: $8890,x3x3: $8891) } ) 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: ($8987, $8988, $8989) -> $8991 $8993 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E rr: V )result: -> total clause1<(9059, 9060, 9061),9062,9064,9063,9065> : 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 : (($8987, $8988, $8989)) -> $8991 $8993) -> clause1<($8987, $8988, $8989),$8990,$8992,$8991,$8993>(fnfn: (($8987, $8988, $8989)) -> $8991 $8993((std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $8987,x2x2: $8988,x3x3: $8989)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)){ opop: ($8987, $8988, $8989) -> $8991 $8993(x1x1: $8987,x2x2: $8988,x3x3: $8989) } ) pub fun @perform3( evev: ev<$9093> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($9093<e,a>) -> clause1<($9088, $9089, $9090),$9091,$9093,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: $9088 : a1a1: V, x2x2: $9089 : a2a2: V, x3x3: $9090 : a3a3: V )result: -> 9173 9172 : ee: E bb: V xperform1std/core/hnd/xperform1: (ev : ev<$9093>, op : forall<e,a> ($9093<e,a>) -> clause1<($9088, $9089, $9090),$9091,$9093,e,a>, x : ($9088, $9089, $9090)) -> $9092 $9091(evev: ev<$9093>,opop: forall<e,a> ($9093<e,a>) -> clause1<($9088, $9089, $9090),$9091,$9093,e,a>,(std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)x1x1: $9088,x2x2: $9089,x3x3: $9090)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<$9200> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($9195, $9196, $9197) -> $9199 $9198 : (a1a1: V,a2a2: V,a3a3: V) -> ee: E bb: V, x1x1: $9195 : a1a1: V, x2x2: $9196 : a2a2: V, x3x3: $9197 : a3a3: V )result: -> 9301 9300 : ee: E bb: V val w0w0: evv<_9208> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$9200>) -> $9199 evv<_9208>(evev: ev<$9200>) val zz: $9198 = opop: ($9195, $9196, $9197) -> $9199 $9198(x1x1: $9195,x2x2: $9196,x3x3: $9197) evv-setstd/core/hnd/evv-set: (w : evv<_9208>) -> $9199 ()(w0w0: evv<_9208>) if yieldingstd/core/hnd/yielding: () -> $9199 bool() returnreturn: $9198 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $9199 $9198, a) -> $9199 $9198) -> $9199 $9198( fnfn: forall<a> (cont : (a) -> $9199 $9198, res : a) -> $9199 $9198(contcont: ($9243) -> $9199 $9198,resres: $9243) under1std/core/hnd/under1: (ev : ev<$9200>, op : ($9243) -> $9199 $9198, x : $9243) -> $9199 $9198(evev: ev<$9200>,contcont: ($9243) -> $9199 $9198,resres: $9243) )std/core/types/Unit: () zz: $9198 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 : $9321, x2 : $9322, x3 : $9323, x4 : $9324, k : ($9325) -> $9326 $9328) -> $9326 $9328 : (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<(9402, 9403, 9404, 9405),9406,9408,9407,9409> : 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 : ($9321, $9322, $9323, $9324), k : ($9325) -> $9326 $9328) -> $9326 $9328) -> clause1<($9321, $9322, $9323, $9324),$9325,$9327,$9326,$9328>( fnfn: (($9321, $9322, $9323, $9324), k : ($9325) -> $9326 $9328) -> $9326 $9328((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9321,x2x2: $9322,x3x3: $9323,x4x4: $9324)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d),kk: ($9325) -> $9326 $9328){ opop: (x1 : $9321, x2 : $9322, x3 : $9323, x4 : $9324, k : ($9325) -> $9326 $9328) -> $9326 $9328(x1x1: $9321,x2x2: $9322,x3x3: $9323,x4x4: $9324,kk: ($9325) -> $9326 $9328) } ) 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: ($9438, $9439, $9440, $9441) -> $9435 $9442 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E bb: V)result: -> total clause1<(9518, 9519, 9520, 9521),9522,9517,9515,9516> : 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 : (($9438, $9439, $9440, $9441)) -> $9435 $9442) -> clause1<($9438, $9439, $9440, $9441),$9442,$9437,$9435,$9436>( fnfn: (($9438, $9439, $9440, $9441)) -> $9435 $9442((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9438,x2x2: $9439,x3x3: $9440,x4x4: $9441)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)){ opop: ($9438, $9439, $9440, $9441) -> $9435 $9442(x1x1: $9438,x2x2: $9439,x3x3: $9440,x4x4: $9441) } ) 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: ($9551, $9552, $9553, $9554) -> $9548 $9555 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E bb: V)result: -> total clause1<(9631, 9632, 9633, 9634),9635,9630,9628,9629> : 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 : (($9551, $9552, $9553, $9554)) -> $9548 $9555) -> clause1<($9551, $9552, $9553, $9554),$9555,$9550,$9548,$9549>( fnfn: (($9551, $9552, $9553, $9554)) -> $9548 $9555((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9551,x2x2: $9552,x3x3: $9553,x4x4: $9554)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)){ opop: ($9551, $9552, $9553, $9554) -> $9548 $9555(x1x1: $9551,x2x2: $9552,x3x3: $9553,x4x4: $9554) } ) 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: ($9661, $9662, $9663, $9664) -> $9666 $9668 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E rr: V )result: -> total clause1<(9741, 9742, 9743, 9744),9745,9747,9746,9748> : 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 : (($9661, $9662, $9663, $9664)) -> $9666 $9668) -> clause1<($9661, $9662, $9663, $9664),$9665,$9667,$9666,$9668>(fnfn: (($9661, $9662, $9663, $9664)) -> $9666 $9668((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9661,x2x2: $9662,x3x3: $9663,x4x4: $9664)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)){ opop: ($9661, $9662, $9663, $9664) -> $9666 $9668(x1x1: $9661,x2x2: $9662,x3x3: $9663,x4x4: $9664) } ) pub fun @perform4( evev: ev<$9780> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: forall<e,a> ($9780<e,a>) -> clause1<($9774, $9775, $9776, $9777),$9778,$9780,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: $9774 : a1a1: V, x2x2: $9775 : a2a2: V, x3x3: $9776 : a3a3: V, x4x4: $9777 : a4a4: V )result: -> 9869 9868 : ee: E bb: V xperform1std/core/hnd/xperform1: (ev : ev<$9780>, op : forall<e,a> ($9780<e,a>) -> clause1<($9774, $9775, $9776, $9777),$9778,$9780,e,a>, x : ($9774, $9775, $9776, $9777)) -> $9779 $9778(evev: ev<$9780>,opop: forall<e,a> ($9780<e,a>) -> clause1<($9774, $9775, $9776, $9777),$9778,$9780,e,a>,(std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)x1x1: $9774,x2x2: $9775,x3x3: $9776,x4x4: $9777)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<$9900> : evstd/core/hnd/ev: ((E, V) -> V) -> V<hh: (E, V) -> V>, opop: ($9894, $9895, $9896, $9897) -> $9899 $9898 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> ee: E bb: V, x1x1: $9894 : a1a1: V, x2x2: $9895 : a2a2: V, x3x3: $9896 : a3a3: V, x4x4: $9897 : a4a4: V )result: -> 10007 10006 : ee: E bb: V val w0w0: evv<_9908> = evv-swap-withstd/core/hnd/evv-swap-with: (ev : ev<$9900>) -> $9899 evv<_9908>(evev: ev<$9900>) val zz: $9898 = opop: ($9894, $9895, $9896, $9897) -> $9899 $9898(x1x1: $9894,x2x2: $9895,x3x3: $9896,x4x4: $9897) evv-setstd/core/hnd/evv-set: (w : evv<_9908>) -> $9899 ()(w0w0: evv<_9908>) if yieldingstd/core/hnd/yielding: () -> $9899 bool() returnreturn: $9898 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $9899 $9898, a) -> $9899 $9898) -> $9899 $9898( fnfn: forall<a> (cont : (a) -> $9899 $9898, res : a) -> $9899 $9898(contcont: ($9944) -> $9899 $9898,resres: $9944) under1std/core/hnd/under1: (ev : ev<$9900>, op : ($9944) -> $9899 $9898, x : $9944) -> $9899 $9898(evev: ev<$9900>,contcont: ($9944) -> $9899 $9898,resres: $9944) )std/core/types/Unit: () zz: $9898 // ------------------------------------------- // Open // ------------------------------------------- pub fun @open-none0<bb: V,e1e1: E,e2e2: E>( ff: () -> $10031 $10030 : () -> e1e1: E bb: V )result: -> 10078 10076 : e2e2: E bb: V val ww: evv<$10032> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $10032 evv<$10032>() val xx: $10030 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $10031 $10030) -> $10032 (() -> $10032 $10030)(ff: () -> $10031 $10030)() val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$10032>) -> $10032 ()(ww: evv<$10032>) xx: $10030 pub fun @open-none1<aa: V,bb: V,e1e1: E,e2e2: E>( ff: ($10088) -> $10090 $10089 : aa: V -> e1e1: E bb: V, x1x1: $10088 : aa: V )result: -> 10146 10144 : e2e2: E bb: V val ww: evv<$10091> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $10091 evv<$10091>() val xx: $10089 = cast-ev1std/core/hnd/cast-ev1: (f : ($10088) -> $10090 $10089) -> $10091 (($10088) -> $10091 $10089)(ff: ($10088) -> $10090 $10089)(x1x1: $10088) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$10091>) -> $10091 ()(ww: evv<$10091>) xx: $10089 pub fun @open-none2<a1a1: V,a2a2: V,bb: V,e1e1: E,e2e2: E>( ff: ($10159, $10160) -> $10162 $10161 : (a1a1: V,a2a2: V) -> e1e1: E bb: V, x1x1: $10159 : a1a1: V, x2x2: $10160 : a2a2: V )result: -> 10227 10225 : e2e2: E bb: V val ww: evv<$10163> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $10163 evv<$10163>() val xx: $10161 = cast-ev2std/core/hnd/cast-ev2: (f : ($10159, $10160) -> $10162 $10161) -> $10163 (($10159, $10160) -> $10163 $10161)(ff: ($10159, $10160) -> $10162 $10161)(x1x1: $10159,x2x2: $10160) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$10163>) -> $10163 ()(ww: evv<$10163>) xx: $10161 pub fun @open-none3<a1a1: V,a2a2: V,a3a3: V,bb: V,e1e1: E,e2e2: E>( ff: ($10243, $10244, $10245) -> $10247 $10246 : (a1a1: V,a2a2: V,a3a3: V) -> e1e1: E bb: V, x1x1: $10243 : a1a1: V, x2x2: $10244 : a2a2: V, x3x3: $10245 : a3a3: V )result: -> 10321 10319 : e2e2: E bb: V val ww: evv<$10248> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $10248 evv<$10248>() val xx: $10246 = cast-ev3std/core/hnd/cast-ev3: (f : ($10243, $10244, $10245) -> $10247 $10246) -> $10248 (($10243, $10244, $10245) -> $10248 $10246)(ff: ($10243, $10244, $10245) -> $10247 $10246)(x1x1: $10243,x2x2: $10244,x3x3: $10245) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$10248>) -> $10248 ()(ww: evv<$10248>) xx: $10246 pub fun @open-none4<a1a1: V,a2a2: V,a3a3: V,a4a4: V,bb: V,e1e1: E,e2e2: E>( ff: ($10340, $10341, $10342, $10343) -> $10345 $10344 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e1e1: E bb: V, x1x1: $10340 : a1a1: V, x2x2: $10341 : a2a2: V, x3x3: $10342 : a3a3: V, x4x4: $10343 : a4a4: V )result: -> 10428 10426 : e2e2: E bb: V val ww: evv<$10346> = evv-swap-create0std/core/hnd/evv-swap-create0: () -> $10346 evv<$10346>() val xx: $10344 = cast-ev4std/core/hnd/cast-ev4: (f : ($10340, $10341, $10342, $10343) -> $10345 $10344) -> $10346 (($10340, $10341, $10342, $10343) -> $10346 $10344)(ff: ($10340, $10341, $10342, $10343) -> $10345 $10344)(x1x1: $10340,x2x2: $10341,x3x3: $10342,x4x4: $10343) val keepkeep: () = evv-setstd/core/hnd/evv-set: (w : evv<$10346>) -> $10346 ()(ww: evv<$10346>) xx: $10344 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: ($10450) -> $10452 $10451 : aa: V -> e1e1: E bb: V, xx: $10450 : aa: V )result: -> 10561 10559 : e2e2: E bb: V val ww: evv<$10453> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10453 evv<$10453>(ii: ev-index) val yy: $10451 = cast-ev1std/core/hnd/cast-ev1: (f : ($10450) -> $10452 $10451) -> $10453 (($10450) -> $10453 $10451)(ff: ($10450) -> $10452 $10451)(xx: $10450) evv-setstd/core/hnd/evv-set: (w : evv<$10453>) -> $10453 ()(ww: evv<$10453>) if yieldingstd/core/hnd/yielding: () -> $10453 bool() returnreturn: $10451 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10453 $10451, a) -> $10453 $10451) -> $10453 $10451(fnfn: forall<a> (cont : (a) -> $10453 $10451, res : a) -> $10453 $10451(contcont: ($10505) -> $10453 $10451,resres: $10505){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10505) -> $10453 $10451, x : $10505) -> $10453 $10451(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : ev-index) -> $10453 ev-index(ii: ev-index),contcont: ($10505) -> $10453 $10451,resres: $10505) })std/core/types/Unit: () yy: $10451 pub fun @open-at0<bb: V,e1e1: E,e2e2: E>( ii: ev-index: ev-indexstd/core/hnd/ev-index: V, ff: () -> $10575 $10574 : () -> e1e1: E bb: V )result: -> 10668 10666 : e2e2: E bb: V val ww: evv<$10576> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10576 evv<$10576>(ii: ev-index) val yy: $10574 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $10575 $10574) -> $10576 (() -> $10576 $10574)(ff: () -> $10575 $10574)() evv-setstd/core/hnd/evv-set: (w : evv<$10576>) -> $10576 ()(ww: evv<$10576>) if yieldingstd/core/hnd/yielding: () -> $10576 bool() returnreturn: $10574 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10576 $10574, a) -> $10576 $10574) -> $10576 $10574(fnfn: forall<a> (cont : (a) -> $10576 $10574, res : a) -> $10576 $10574(contcont: ($10624) -> $10576 $10574,resres: $10624){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10624) -> $10576 $10574, x : $10624) -> $10576 $10574(ii: ev-index,contcont: ($10624) -> $10576 $10574,resres: $10624) })std/core/types/Unit: () yy: $10574 pub fun @open-at1<aa: V,bb: V,e1e1: E,e2e2: E>( ii: ev-index: ev-indexstd/core/hnd/ev-index: V, ff: ($10678) -> $10680 $10679 : aa: V -> e1e1: E bb: V, xx: $10678 : aa: V )result: -> 10782 10780 : e2e2: E bb: V val ww: evv<$10681> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10681 evv<$10681>(ii: ev-index) val yy: $10679 = cast-ev1std/core/hnd/cast-ev1: (f : ($10678) -> $10680 $10679) -> $10681 (($10678) -> $10681 $10679)(ff: ($10678) -> $10680 $10679)(xx: $10678) evv-setstd/core/hnd/evv-set: (w : evv<$10681>) -> $10681 ()(ww: evv<$10681>) if yieldingstd/core/hnd/yielding: () -> $10681 bool() returnreturn: $10679 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10681 $10679, a) -> $10681 $10679) -> $10681 $10679(fnfn: forall<a> (cont : (a) -> $10681 $10679, res : a) -> $10681 $10679(contcont: ($10733) -> $10681 $10679,resres: $10733){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10733) -> $10681 $10679, x : $10733) -> $10681 $10679(ii: ev-index,contcont: ($10733) -> $10681 $10679,resres: $10733) })std/core/types/Unit: () yy: $10679 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: ($10795, $10796) -> $10798 $10797 : (a1a1: V,a2a2: V) -> e1e1: E bb: V, x1x1: $10795 : a1a1: V, x2x2: $10796 : a2a2: V )result: -> 10909 10907 : e2e2: E bb: V val ww: evv<$10799> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10799 evv<$10799>(ii: ev-index) val yy: $10797 = cast-ev2std/core/hnd/cast-ev2: (f : ($10795, $10796) -> $10798 $10797) -> $10799 (($10795, $10796) -> $10799 $10797)(ff: ($10795, $10796) -> $10798 $10797)(x1x1: $10795,x2x2: $10796) evv-setstd/core/hnd/evv-set: (w : evv<$10799>) -> $10799 ()(ww: evv<$10799>) if yieldingstd/core/hnd/yielding: () -> $10799 bool() returnreturn: $10797 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10799 $10797, a) -> $10799 $10797) -> $10799 $10797(fnfn: forall<a> (cont : (a) -> $10799 $10797, res : a) -> $10799 $10797(contcont: ($10855) -> $10799 $10797,resres: $10855){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10855) -> $10799 $10797, x : $10855) -> $10799 $10797(ii: ev-index,contcont: ($10855) -> $10799 $10797,resres: $10855) })std/core/types/Unit: () yy: $10797 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: ($10925, $10926, $10927) -> $10929 $10928 : (a1a1: V,a2a2: V,a3a3: V) -> e1e1: E bb: V, x1x1: $10925 : a1a1: V, x2x2: $10926 : a2a2: V, x3x3: $10927 : a3a3: V )result: -> 11049 11047 : e2e2: E bb: V val ww: evv<$10930> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $10930 evv<$10930>(ii: ev-index) val yy: $10928 = cast-ev3std/core/hnd/cast-ev3: (f : ($10925, $10926, $10927) -> $10929 $10928) -> $10930 (($10925, $10926, $10927) -> $10930 $10928)(ff: ($10925, $10926, $10927) -> $10929 $10928)(x1x1: $10925,x2x2: $10926,x3x3: $10927) evv-setstd/core/hnd/evv-set: (w : evv<$10930>) -> $10930 ()(ww: evv<$10930>) if yieldingstd/core/hnd/yielding: () -> $10930 bool() returnreturn: $10928 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $10930 $10928, a) -> $10930 $10928) -> $10930 $10928(fnfn: forall<a> (cont : (a) -> $10930 $10928, res : a) -> $10930 $10928(contcont: ($10990) -> $10930 $10928,resres: $10990){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($10990) -> $10930 $10928, x : $10990) -> $10930 $10928(ii: ev-index,contcont: ($10990) -> $10930 $10928,resres: $10990) })std/core/types/Unit: () yy: $10928 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: ($11068, $11069, $11070, $11071) -> $11073 $11072 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e1e1: E bb: V, x1x1: $11068 : a1a1: V, x2x2: $11069 : a2a2: V, x3x3: $11070 : a3a3: V, x4x4: $11071 : a4a4: V )result: -> 11202 11200 : e2e2: E bb: V val ww: evv<$11074> = evv-swap-create1std/core/hnd/evv-swap-create1: (i : ev-index) -> $11074 evv<$11074>(ii: ev-index) val yy: $11072 = cast-ev4std/core/hnd/cast-ev4: (f : ($11068, $11069, $11070, $11071) -> $11073 $11072) -> $11074 (($11068, $11069, $11070, $11071) -> $11074 $11072)(ff: ($11068, $11069, $11070, $11071) -> $11073 $11072)(x1x1: $11068,x2x2: $11069,x3x3: $11070,x4x4: $11071) evv-setstd/core/hnd/evv-set: (w : evv<$11074>) -> $11074 ()(ww: evv<$11074>) if yieldingstd/core/hnd/yielding: () -> $11074 bool() returnreturn: $11072 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11074 $11072, a) -> $11074 $11072) -> $11074 $11072(fnfn: forall<a> (cont : (a) -> $11074 $11072, res : a) -> $11074 $11072(contcont: ($11138) -> $11074 $11072,resres: $11138){ open-at1std/core/hnd/open-at1: (i : ev-index, f : ($11138) -> $11074 $11072, x : $11138) -> $11074 $11072(ii: ev-index,contcont: ($11138) -> $11074 $11072,resres: $11138) })std/core/types/Unit: () yy: $11072 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: ($11224) -> $11226 $11225 : aa: V -> e1e1: E bb: V, xx: $11224 : aa: V )result: -> 11335 11333 : e2e2: E bb: V val ww: evv<$11227> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $11227 evv<$11227>(indicesindices: vector<ev-index>) val yy: $11225 = cast-ev1std/core/hnd/cast-ev1: (f : ($11224) -> $11226 $11225) -> $11227 (($11224) -> $11227 $11225)(ff: ($11224) -> $11226 $11225)(xx: $11224) evv-setstd/core/hnd/evv-set: (w : evv<$11227>) -> $11227 ()(ww: evv<$11227>) if yieldingstd/core/hnd/yielding: () -> $11227 bool() returnreturn: $11225 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11227 $11225, a) -> $11227 $11225) -> $11227 $11225(fnfn: forall<a> (cont : (a) -> $11227 $11225, res : a) -> $11227 $11225(contcont: ($11279) -> $11227 $11225,resres: $11279){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11279) -> $11227 $11225, x : $11279) -> $11227 $11225(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : vector<ev-index>) -> $11227 vector<ev-index>(indicesindices: vector<ev-index>),contcont: ($11279) -> $11227 $11225,resres: $11279) })std/core/types/Unit: () yy: $11225 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: () -> $11349 $11348 : () -> e1e1: E bb: V )result: -> 11442 11440 : e2e2: E bb: V val ww: evv<$11350> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $11350 evv<$11350>(indicesindices: vector<ev-index>) val yy: $11348 = cast-ev0std/core/hnd/cast-ev0: (f : () -> $11349 $11348) -> $11350 (() -> $11350 $11348)(ff: () -> $11349 $11348)() evv-setstd/core/hnd/evv-set: (w : evv<$11350>) -> $11350 ()(ww: evv<$11350>) if yieldingstd/core/hnd/yielding: () -> $11350 bool() returnreturn: $11348 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11350 $11348, a) -> $11350 $11348) -> $11350 $11348(fnfn: forall<a> (cont : (a) -> $11350 $11348, res : a) -> $11350 $11348(contcont: ($11398) -> $11350 $11348,resres: $11398){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11398) -> $11350 $11348, x : $11398) -> $11350 $11348(indicesindices: vector<ev-index>,contcont: ($11398) -> $11350 $11348,resres: $11398) })std/core/types/Unit: () yy: $11348 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: ($11452) -> $11454 $11453 : aa: V -> e1e1: E bb: V, xx: $11452 : aa: V )result: -> 11556 11554 : e2e2: E bb: V val ww: evv<$11455> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $11455 evv<$11455>(indicesindices: vector<ev-index>) val yy: $11453 = cast-ev1std/core/hnd/cast-ev1: (f : ($11452) -> $11454 $11453) -> $11455 (($11452) -> $11455 $11453)(ff: ($11452) -> $11454 $11453)(xx: $11452) evv-setstd/core/hnd/evv-set: (w : evv<$11455>) -> $11455 ()(ww: evv<$11455>) if yieldingstd/core/hnd/yielding: () -> $11455 bool() returnreturn: $11453 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11455 $11453, a) -> $11455 $11453) -> $11455 $11453(fnfn: forall<a> (cont : (a) -> $11455 $11453, res : a) -> $11455 $11453(contcont: ($11507) -> $11455 $11453,resres: $11507){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11507) -> $11455 $11453, x : $11507) -> $11455 $11453(indicesindices: vector<ev-index>,contcont: ($11507) -> $11455 $11453,resres: $11507) })std/core/types/Unit: () yy: $11453 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: ($11569, $11570) -> $11572 $11571 : (a1a1: V,a2a2: V) -> e1e1: E bb: V, x1x1: $11569 : a1a1: V, x2x2: $11570 : a2a2: V )result: -> 11683 11681 : e2e2: E bb: V val ww: evv<$11573> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $11573 evv<$11573>(indicesindices: vector<ev-index>) val yy: $11571 = cast-ev2std/core/hnd/cast-ev2: (f : ($11569, $11570) -> $11572 $11571) -> $11573 (($11569, $11570) -> $11573 $11571)(ff: ($11569, $11570) -> $11572 $11571)(x1x1: $11569,x2x2: $11570) evv-setstd/core/hnd/evv-set: (w : evv<$11573>) -> $11573 ()(ww: evv<$11573>) if yieldingstd/core/hnd/yielding: () -> $11573 bool() returnreturn: $11571 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11573 $11571, a) -> $11573 $11571) -> $11573 $11571(fnfn: forall<a> (cont : (a) -> $11573 $11571, res : a) -> $11573 $11571(contcont: ($11629) -> $11573 $11571,resres: $11629){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11629) -> $11573 $11571, x : $11629) -> $11573 $11571(indicesindices: vector<ev-index>,contcont: ($11629) -> $11573 $11571,resres: $11629) })std/core/types/Unit: () yy: $11571 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: ($11699, $11700, $11701) -> $11703 $11702 : (a1a1: V,a2a2: V,a3a3: V) -> e1e1: E bb: V, x1x1: $11699 : a1a1: V, x2x2: $11700 : a2a2: V, x3x3: $11701 : a3a3: V )result: -> 11823 11821 : e2e2: E bb: V val ww: evv<$11704> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $11704 evv<$11704>(indicesindices: vector<ev-index>) val yy: $11702 = cast-ev3std/core/hnd/cast-ev3: (f : ($11699, $11700, $11701) -> $11703 $11702) -> $11704 (($11699, $11700, $11701) -> $11704 $11702)(ff: ($11699, $11700, $11701) -> $11703 $11702)(x1x1: $11699,x2x2: $11700,x3x3: $11701) evv-setstd/core/hnd/evv-set: (w : evv<$11704>) -> $11704 ()(ww: evv<$11704>) if yieldingstd/core/hnd/yielding: () -> $11704 bool() returnreturn: $11702 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11704 $11702, a) -> $11704 $11702) -> $11704 $11702(fnfn: forall<a> (cont : (a) -> $11704 $11702, res : a) -> $11704 $11702(contcont: ($11764) -> $11704 $11702,resres: $11764){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11764) -> $11704 $11702, x : $11764) -> $11704 $11702(indicesindices: vector<ev-index>,contcont: ($11764) -> $11704 $11702,resres: $11764) })std/core/types/Unit: () yy: $11702 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: ($11842, $11843, $11844, $11845) -> $11847 $11846 : (a1a1: V,a2a2: V,a3a3: V,a4a4: V) -> e1e1: E bb: V, x1x1: $11842 : a1a1: V, x2x2: $11843 : a2a2: V, x3x3: $11844 : a3a3: V, x4x4: $11845 : a4a4: V )result: -> 11976 11974 : e2e2: E bb: V val ww: evv<$11848> = evv-swap-createstd/core/hnd/evv-swap-create: (indices : vector<ev-index>) -> $11848 evv<$11848>(indicesindices: vector<ev-index>) val yy: $11846 = cast-ev4std/core/hnd/cast-ev4: (f : ($11842, $11843, $11844, $11845) -> $11847 $11846) -> $11848 (($11842, $11843, $11844, $11845) -> $11848 $11846)(ff: ($11842, $11843, $11844, $11845) -> $11847 $11846)(x1x1: $11842,x2x2: $11843,x3x3: $11844,x4x4: $11845) evv-setstd/core/hnd/evv-set: (w : evv<$11848>) -> $11848 ()(ww: evv<$11848>) if yieldingstd/core/hnd/yielding: () -> $11848 bool() returnreturn: $11846 yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11848 $11846, a) -> $11848 $11846) -> $11848 $11846(fnfn: forall<a> (cont : (a) -> $11848 $11846, res : a) -> $11848 $11846(contcont: ($11912) -> $11848 $11846,resres: $11912){ open1std/core/hnd/open1: (indices : vector<ev-index>, f : ($11912) -> $11848 $11846, x : $11912) -> $11848 $11846(indicesindices: vector<ev-index>,contcont: ($11912) -> $11848 $11846,resres: $11912) })std/core/types/Unit: () yy: $11846 // ------------------------------------------- // capture yields // ------------------------------------------- // catch finalization and return the current yield state pub noinline fun unsafe-unfinalizestd/core/hnd/unsafe-unfinalize: forall<a,e> (action : () -> e a) -> e either<yield-context,a>( actionaction: () -> $12106 $12105 : () -> ee: E aa: V )result: -> 12127 either<yield-context,12126> : ee: E eitherstd/core/types/either: (V, V) -> V<yield-contextstd/core/hnd/yield-context: V,aa: V> unfinalize-promptstd/core/hnd/unfinalize-prompt: (res : $12105) -> $12106 either<yield-context,$12105>(actionaction: () -> $12106 $12105()); fun unfinalize-promptstd/core/hnd/unfinalize-prompt: forall<a,e> (res : a) -> e either<yield-context,a>( resres: $11998 : aa: V )result: -> 12098 either<yield-context,12097> : ee: E eitherstd/core/types/either: (V, V) -> V<yield-contextstd/core/hnd/yield-context: V,aa: V> if yielding-non-finalstd/core/hnd/yielding-non-final: () -> $11999 bool() then yield-contstd/core/hnd/yield-cont: (f : forall<a> ((a) -> $11999 $11998, a) -> $11999 either<yield-context,$11998>) -> $11999 either<yield-context,$11998>(fnfn: forall<a> (cont : (a) -> $11999 $11998, x : a) -> $11999 either<yield-context,$11998>(contcont: ($12017) -> $11999 $11998,xx: $12017) unfinalize-promptstd/core/hnd/unfinalize-prompt: (res : $11998) -> $11999 either<yield-context,$11998>(pretend-decreasingstd/core/undiv/pretend-decreasing: (x : $11998) -> $11999 $11998(contcont: ($12017) -> $11999 $11998(xx: $12017))) ) elif !std/core/types/bool/(!): (b : bool) -> $11999 boolyieldingstd/core/hnd/yielding: () -> $11999 bool() then Rightstd/core/types/Right: forall<a,b> (right : b) -> either<a,b>(resres: $11998) else Leftstd/core/types/Left: forall<a,b> (left : a) -> either<a,b>(yield-capturestd/core/hnd/yield-capture: () -> $11999 yield-context())