/*---------------------------------------------------------------------------
  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.
---------------------------------------------------------------------------*/

/* Primitive types and functions.

   This module is implicitly imported and all functions and types
   are always available.
   These types are required to be defined for the compiler
   to work correctly (i.e. types like `:int` or `:div`)

   The _kinds_ of types are all builtin:

   * `V`   value types (i.e. the star kind)
   * `E`   effect rows (`<div,exn|e>`)
   * `X`   a single effect (`div`, `exn`, `parse`, etc.), also called atomic effect
   * `H`   heap types (always a phantom type without actual values)
   * `HX`  a short-hand for user defined effect handlers of kind `(E,V) -> V`

*/
module std/core/typesstd/core/types

pub infixr 80  (^)
pub infixl 70  (*), (%), (/), cdiv, cmod
pub infixr 60  (++)
pub infixl 60  (+), (-)
pub infixr 55  (++.)
pub infix  40  (!=), (==), (<=), (>=), (<), (>)
pub infixr 30  (&&)
pub infixr 20  (||)
// prefix     (!), (-)


// build: 139

// ----------------------------------------------------------------------------
// Core types
// ----------------------------------------------------------------------------

// An arbitrary precision signed integer.
// See `module std/core/int` for integer operations.
pub type intstd/core/types/int: V

// A 64-bit IEEE 754 double precision floating point value.
// See `module std/num/float64` for operations on `:float64`s.
pub value type float64std/core/types/float64: V

// A unicode character.
// Characters are unicode _codepoint_\/s.
// This is different from a unicode _grapheme_ which represents a single displayed
// symbol and can consists of multiple codepoints due to combining characters and marks.
// (see also `module std/core/char` and the `module std/text/unicode` module).
pub value type charstd/core/types/char: V

// A string is a sequence of unicode character points (`char`).
// The encoding of a string is internal and there
// is no constant-time indexing of characters in a string.
// Use the `:sslice` type for efficient matching and retrieving
// sub-strings from string. See `module std/core/string` and
// `module std/core/sslice` for string operations.
pub type stringstd/core/types/string: V

// A 8-bit signed integer (represented in two's complement).
// Provides no operations and used only for storage and interaction with external code.
pub value type int8std/core/types/int8: V

// A 16-bit signed integer (represented in two's complement).
// Provides no operations and used only for storage and interaction with external code.
pub value type int16std/core/types/int16: V

// A 32-bit signed integer (represented in two's complement).
// See the `module std/num/int32` module for operations on 32-bit integers.
pub value type int32std/core/types/int32: V

// A 64-bit signed integer (represented in two's complement).
// See the `module std/num/int64` module for operations on 64-bit integers.
pub value type int64std/core/types/int64: V

// A signed two's complement integer equal to a signed `size_t` in C, i.e.
// it can hold the byte size of any object, in particular the maximum possible
// byte size of a vector or string.
// Provides no operations but is used mostly for interaction with external code.
// The Javascript backend uses `int32` for this.
pub value type ssize_tstd/core/types/ssize_t: V

// A signed two's complement integer equal to an `intptr_t` in C, i.e.
// it has the same bit-size as a native pointer (`void*`).
// Provides no operations but is used mostly for interaction with external code.
// The Javascript backend uses `int64` for this.
pub value type intptr_tstd/core/types/intptr_t: V

// A 32-bit IEEE 754 single precision floating point value.
// Provides currently no operations and currently only used for storage and for interaction with external code.
pub value type float32std/core/types/float32: V

// The type of immutable polymorphic arrays is called `:vector`.
// See `module std/core/vector` for vector operations.
pub type vectorstd/core/types/vector: V -> V<aa: V>

// An any type. Used for external calls.
pub type anystd/core/types/any: V

// Internal type used for in-place update of unique pattern matches.
pub type @reuse

pub extern @no-reuse() : @reusestd/core/types/total: E
  c inline  "NULL"
  js inline "null"


// The _total_ effect represents the absence of any effect.
// Usually written as `<>`
pub type totalstd/core/types/total: E :: E

// The effect constructor extends an effect row with another effect.
// Usually written as `<_|_>`
pub type effect-extendstd/core/types/effect-extend: (X, E) -> E :: (X,E) -> E

// The divergence effect: a divergent function may not terminate.
pub type divstd/core/types/div: X :: X

// The non-determinism effect.
pub type ndetstd/core/types/ndet: X :: X

// The alloc effect signifies a function may allocate in a heap `:h`
pub type allocstd/core/types/alloc: H -> X :: H -> X

// The read effect: signifies that a function may read from from heap `:h`.
pub type readstd/core/types/read: H -> X :: H -> X

// The write effect: signifies that a function may write to heap `:h`.
pub type writestd/core/types/write: H -> X :: H -> X

// Stateful functions can manipulate heap `:h` using allocations, reads and writes.
pub alias ststd/core/types/st: H -> E<hh: H> = <std/core/types/total: Ereadstd/core/types/read: H -> X<hh: H>, writestd/core/types/write: H -> X<hh: H>, allocstd/core/types/alloc: H -> X<hh: H>>

// The `:global` heap is a special heap constant to denote the global shared heap
pub type globalstd/core/types/global: H :: H

// Handled effects are lifted to an atomic effect using the `:handled` type constructor
// All user defined effects are `:handled` since they require a handler to be dismissed.
// In contrast, some built-in effects, like `:div` or `:st` do not require a handler
// as these are handled by the system.
// In particular, the runtime evidence vector only contains `:handled` (and `:handled1`) effects.
pub type handledstd/core/types/handled: ((E, V) -> V) -> X    :: HX -> X;

// Linear effects are lifted to an atomic effect using the `:handled1` type constructor
pub type handled1std/core/types/handled1: ((E, V) -> V) -> X   :: HX -> X;

// Named effects are lifted to an atomic effect with the `:nhandled` type constructor.
// In contrast to `:handled` effects, these effects are not passed in the evidence vector.
pub type nhandledstd/core/types/nhandled: ((E, V) -> V) -> X    :: HX -> X;

// Linear named effects are lifted to an atomic effect using the `:nhandled1` type constructor
pub type nhandled1std/core/types/nhandled1: ((E, V) -> V) -> X   :: HX -> X;


// ----------------------------------------------------------------------------
// Standard Data types
// ----------------------------------------------------------------------------

// The `:void` type is empty and has no constructors.
// See also the `:unit` unit type and the `:bool` type.
pub type voidstd/core/types/void: V

// The type of booleans has two inhabitants: `True` and `False`.
pub type boolstd/core/types/bool: V
  con Falsestd/core/types/False: bool
  con Truestd/core/types/True: bool

// The unit type `:unit` is inhabited by just a single value, namely `Unit`.
// Usually the type and constructor are written as `()`.
// See also the `:void` type and the `:bool` type.
pub struct unitstd/core/types/unit: V

// A pair of values `:a` and `:b`. Usually written as `(x,y)` (for types and terms)
pub value struct tuple2std/core/types/tuple2: (V, V) -> V<aa: V,bb: V>(fststd/core/types/tuple2/fst: forall<a,b> (tuple2 : (a, b)) -> a:aa: V,sndstd/core/types/tuple2/snd: forall<a,b> (tuple2 : (a, b)) -> b:bb: V)

// A triple of values. Usually written as `(x,y,z)` (for types and terms)
pub value struct tuple3std/core/types/tuple3: (V, V, V) -> V<aa: V,bb: V,cc: V>(fststd/core/types/tuple3/fst: forall<a,b,c> (tuple3 : (a, b, c)) -> a:aa: V,sndstd/core/types/tuple3/snd: forall<a,b,c> (tuple3 : (a, b, c)) -> b:bb: V,thdstd/core/types/tuple3/thd: forall<a,b,c> (tuple3 : (a, b, c)) -> c:cc: V)

// A quadruple of values. Usually written as `(a,b,c,d)` (for types and terms)
pub struct tuple4std/core/types/tuple4: (V, V, V, V) -> V<aa: V,bb: V,cc: V,dd: V>(fststd/core/types/tuple4/fst: forall<a,b,c,d> (tuple4 : (a, b, c, d)) -> a:aa: V,sndstd/core/types/tuple4/snd: forall<a,b,c,d> (tuple4 : (a, b, c, d)) -> b:bb: V,thdstd/core/types/tuple4/thd: forall<a,b,c,d> (tuple4 : (a, b, c, d)) -> c:cc: V,field4std/core/types/tuple4/field4: forall<a,b,c,d> (tuple4 : (a, b, c, d)) -> d:dd: V)

// A quintuple of values. Usually written as `(a,b,c,d,e)` (for types and terms)
pub struct tuple5std/core/types/tuple5: (V, V, V, V, V) -> V<aa: V,bb: V,cc: V,dd: V,ee: V>(fststd/core/types/tuple5/fst: forall<a,b,c,d,a1> (tuple5 : (a, b, c, d, a1)) -> a:aa: V,sndstd/core/types/tuple5/snd: forall<a,b,c,d,a1> (tuple5 : (a, b, c, d, a1)) -> b:bb: V,thdstd/core/types/tuple5/thd: forall<a,b,c,d,a1> (tuple5 : (a, b, c, d, a1)) -> c:cc: V,field4std/core/types/tuple5/field4: forall<a,b,c,d,a1> (tuple5 : (a, b, c, d, a1)) -> d:dd: V,field5std/core/types/tuple5/field5: forall<a,b,c,d,a1> (tuple5 : (a, b, c, d, a1)) -> a1:ee: V)

// The `:maybe` type is used to represent either a value (`Just(x)`) or `Nothing`.
// This type is often used to represent values that can be _null_.
// See also `module std/core/maybe`.
pub value type maybestd/core/types/maybe: V -> V<aa: V>
  // No result
  con Nothingstd/core/types/Nothing: forall<a> maybe<a>
  // A single result
  con Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>( value : aa: V )

// The choice type represents one of two possible types `:a` or `:b`.
// See also `module std/core/either`.
pub value type eitherstd/core/types/either: (V, V) -> V<aa: V,bb: V>
  // Left result, usually used for errors.
  con Leftstd/core/types/Left: forall<a,b> (left : a) -> either<a,b>( left : aa: V )
  // Right result, usually used for success.
  con Rightstd/core/types/Right: forall<a,b> (right : b) -> either<a,b>( right : bb: V )

// An enumeration to represent order: `Lt`, `Eq`, or `Gt`.
// See also `module std/core/order`.
pub type orderstd/core/types/order: V
  // lower-than
  Ltstd/core/types/Lt: order
  // equal
  Eqstd/core/types/Eq: order
  // greater-than
  Gtstd/core/types/Gt: order

// Represent two elements in ascending order. This is used to
// allow comparison on elements to be used linearly for `fip` functions.
// See also `module std/core/order`
pub value type order2std/core/types/order2: V -> V<aa: V>
  // The elements compared lower-than, with `lt < gt`.
  Lt2std/core/types/Lt2: forall<a> (lt : a, gt : a) -> order2<a>( lt: aa: V, gt : aa: V )
  // The elements compared equal (with value `eq`).
  Eq2std/core/types/Eq2: forall<a> (eq : a) -> order2<a>( eq: aa: V )
  // The elements compared greater-than, with `lt < gt`.
  Gt2std/core/types/Gt2: forall<a> (lt : a, gt : a) -> order2<a>( lt: aa: V, gt : aa: V )


// The type of lists, which can be either empty (`Nil`) or an element followed
// by a list (`Cons`).
// See `module std/core/list` for operations on lists.
pub type liststd/core/types/list: V -> V<aa: V>
  // The empty list.
  con Nilstd/core/types/Nil: forall<a> list<a>                  // note: must come first; see Core/Core.hs
  // A ``head``  element followed by the ``tail``  of the list.
  con Consstd/core/types/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(head:aa: V, tail : liststd/core/types/list: V -> V<aa: V> )


// Explicitly box values using the `Box` constructor.
pub value type boxstd/core/types/box: V -> V<aa: V>
  con Boxstd/core/types/Box: forall<a> (unbox : a) -> box<a>( unboxstd/core/types/box/unbox: forall<a> (box : box<a>) -> a : aa: V )

// A padding type `pad`.
// This is sometimes used for fbip programming to match up the size of constructors for reuse.
pub reference type padstd/core/types/pad: V
  Padstd/core/types/Pad: pad

// Prevent inlining an expression by passing it to `keep` (which is a non-inlineable identity function)
pub noinline fip fun keepstd/core/types/keep: forall<a> (x : a) -> a( xx: $2088 : aa: V )result: -> total 2096 : astd/core/types/total: E
  xx: $2088

// ----------------------------------------------------------------------------
// Standard functions
// ----------------------------------------------------------------------------

// The identity function returns its argument unchanged
pub fip fun idstd/core/types/id: forall<a> (x : a) -> a(xx: $2101 : aa: V)result: -> total 2109 : astd/core/types/total: E
  xx: $2101

// Logical conjunction. This is compiled specially avoid evaluating the second argument if `x==False`.
pub fip fun (&&)std/core/types/(&&): (x : bool, y : bool) -> bool( xx: bool : boolstd/core/types/bool: V, yy: bool : boolstd/core/types/bool: V)result: -> total bool : boolstd/core/types/bool: V   // inlined in the compiler for short-circuit evaluation
  if xx: bool then yy: bool else Falsestd/core/types/False: bool

// Logical disjunction. This is compiled specially avoid evaluating the second argument if `x==True`.
pub fip fun (||)std/core/types/(||): (x : bool, y : bool) -> bool( xx: bool : boolstd/core/types/bool: V, yy: bool : boolstd/core/types/bool: V)result: -> total bool : boolstd/core/types/bool: V  // inlined in the compiler for short-circuit evaluation
  if xx: bool then Truestd/core/types/True: bool else yy: bool

// Logical negation
pub fip fun bool/(!)std/core/types/bool/(!): (b : bool) -> bool( bb: bool : boolstd/core/types/bool: V )result: -> total bool : boolstd/core/types/bool: V
  if bb: bool then Falsestd/core/types/False: bool else Truestd/core/types/True: bool

// Logical negation
pub fip fun notstd/core/types/not: (b : bool) -> bool( bb: bool : boolstd/core/types/bool: V )result: -> total bool : boolstd/core/types/bool: V
  if bb: bool then Falsestd/core/types/False: bool else Truestd/core/types/True: bool


extern import
  js file "inline/types.js"

// Convert an integer to an `:int32`. The number is _clamped_ to the maximal or minimum `:int32`
// value if it is outside the range of an `:int32`.
// Needed for control flow contexts in `module std/core/hnd`
pub inline fip extern @make-int32( i : intstd/core/types/int: V) : int32std/core/types/int32: V
  c  "kk_integer_clamp32"
  cs "Primitive.IntToInt32"
  js "$std_core_types._int_clamp32"


// Convert an integer to an `:ssize_t`. The number is _clamped_ to the maximal or minimum `:ssize_t`
// value if it is outside the range of an `:ssize_t`.
// Needed for evidence indices in `module std/core/hnd`
pub fip extern @make-ssize_t( ii: int : intstd/core/types/int: V) : ssize_tstd/core/types/ssize_t: V
  c  "kk_integer_clamp_ssize_t"
  cs "Primitive.IntToInt32"
  js "$std_core_types._int_clamp32"


// Append two strings
pub extern (++)std/core/types/(++): (x : string, y : string) -> string(xx: string : stringstd/core/types/string: V, yy: string : stringstd/core/types/string: V) : stringstd/core/types/string: V
  c "kk_string_cat"
  inline "(#1 + #2)"


// _Internal_: generated by type inference and later refined into one of the `open` variants in `std/core/hnd`.
pub noinline extern @open<e1e1: E::E,e2e2: E::E,aa: V,bb: V>( xx: $2167 : aa: V ) : e2e2: E bb: V
  inline "#1"


// ----------------------------------------------------------------------------
// References
// ----------------------------------------------------------------------------

// The predicate `:hdiv<h,a,e>` signifies that if the type `:a` contains a reference to `:h`,
// then the effect `:e` must contain the divergent effect (`:div`). This constraint is generated
// when reading from the heap (see `(!)`) and is necessary to catch cases where code can diverge
// by storing self referential functions in the heap.
pub type hdivstd/core/types/hdiv: (H, V, E) -> P :: (H,V,E) -> P

// The predicate `:ediv<x,a,e>` signifies that if the type `:a` contains a reference to effect constant `:x",
// then the effect `:e` must contain the divergent effect (`:div`). This constraint is generated
// for operations on first-class effects where code can diverge through operations.
pub type edivstd/core/types/ediv: (X, V, E) -> P :: (X,V,E) -> P


// A reference `:ref<h,a>` points to a value of type `:a` in heap `:h`.
pub type refstd/core/types/ref: (H, V) -> V :: (H,V) -> V

// Allocate a fresh reference with an initial value.
pub inline extern refstd/core/types/ref: forall<a,h> (value : a) -> (alloc<h>) ref<h,a>( value : aa: V) : allocstd/core/types/alloc: H -> X<hh: H> refstd/core/types/ref: (H, V) -> V<hh: H,aa: V>
  c  "kk_ref_alloc"
  cs inline "new Ref<##1,##2>(#1)"
  js inline "{ value: #1 }"

// Assign a new value to a reference.
pub inline extern setstd/core/types/set: forall<a,h> (ref : ref<h,a>, assigned : a) -> (write<h>) ()( ^ref : refstd/core/types/ref: (H, V) -> V<hh: H,aa: V>, assigned : aa: V) : <std/core/types/total: Ewritestd/core/types/write: H -> X<hh: H>> (std/core/types/unit: V)std/core/types/unit: V
  c  "kk_ref_set_borrow"
  cs inline "#1.Set(#2)"
  js inline "((#1).value = #2)"

// Read the value of a reference.
pub inline extern ref/(!)std/core/types/ref/(!): forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e> : forall<hh: H,aa: V,ee: E> ( ref : refstd/core/types/ref: (H, V) -> V<hh: H,aa: V>) -> <readstd/core/types/read: H -> X<hh: H>|std/core/types/effect-extend: (X, E) -> Eee: E> aa: V with(hdivstd/core/types/hdiv: (H, V, E) -> P<hh: H,aa: V,ee: E>)
  c  "kk_ref_get"
  cs inline "#1.Value"
  js inline "#1.value"

// Modify the value of a reference.
// This is especially useful when the reference contains a vector, because
// getting the vector into a local variable and then setting it back into the reference later
// would mean that we hold on to a copy (and we can't update the vector in place then!).
// In contrast, this function passes the ownership to the given function.
pub inline extern modifystd/core/types/modify: forall<h,a,b,e> (ref : ref<h,a>, f : forall<h1> (local-var<h1,a>) -> <local<h1>|e> b) -> <read<h>,write<h>|e> b with hdiv<h,a,e> : forall<hh: H,aa: V,bb: V,ee: E> ( ref : refstd/core/types/ref: (H, V) -> V<hh: H,aa: V>, f : forall<ss: H> 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) -> <readstd/core/types/read: H -> X<hh: H>,writestd/core/types/write: H -> X<hh: H>|std/core/types/effect-extend: (X, E) -> Eee: E> bb: V with(hdivstd/core/types/hdiv: (H, V, E) -> P<hh: H,aa: V,ee: E>)
  c  "kk_ref_modify"
  js inline "((#2)(#1))"

// If a heap effect is unobservable, the heap effect can be erased by using the `run` fun.
// See also: _State in Haskell, by Simon Peyton Jones and John Launchbury_.
pub extern runstd/core/types/run: forall<e,a> (action : forall<h> () -> <alloc<h>,read<h>,write<h>|e> a) -> e a : forall<ee: E,aa: V> ( action : forall<hh: H> () -> <allocstd/core/types/alloc: H -> X<hh: H>,readstd/core/types/read: H -> X<hh: H>,writestd/core/types/write: H -> X<hh: H> |std/core/types/effect-extend: (X, E) -> E ee: E> aa: V ) -> ee: E aa: V
  c  inline "(kk_function_call(kk_box_t,(kk_function_t,kk_context_t*),#1,(#1,kk_context()),kk_context()))"
  cs inline "Primitive.Run<##2>(#1)"
  js inline "((#1)())"


// Mask the state effect. This is more convenient than masking each `:read`, `:write`, and `:alloc` effect separately.
pub inline extern mask-ststd/core/types/mask-st: forall<a,h,e> (() -> e a) -> (() -> <st<h>|e> a) : forall<aa: V,hh: H,ee: E> (() -> ee: E aa: V) -> totalstd/core/types/total: E (() -> <ststd/core/types/st: H -> E<hh: H>|ee: E> aa: V)
  inline "#1"

/*
// Inject the local effect into a function effect.
pub inline extern inject-local<a,h,e>( action : () -> e a ) : total (() -> <local<h>|e> a)
  inline "#1"
*/

// ----------------------------------------------------------------------------
// Local Variables
// ----------------------------------------------------------------------------

// A local heap effect.
pub type localstd/core/types/local: H -> X :: (H) -> X

// A local variable `:local-var<s,a>` points to a value of type `:a` in local scope `:s`.
pub type local-varstd/core/types/local-var: (H, V) -> V :: (H,V) -> V

// Allocate a fresh local with an initial value.
pub inline extern local-newstd/core/types/local-new: forall<a,e,h> (value : a) -> <local<h>|e> local-var<h,a><a,s,e>(value:aa: V) : <localstd/core/types/local: H -> X<ss: H>|std/core/types/effect-extend: (X, E) -> Eee: E> local-varstd/core/types/local-var: (H, V) -> V<ss: H,aa: V>
  c  "kk_ref_alloc"
  cs inline "new Ref<##1,##2>(#1)"
  js inline "{ value: #1 }"

// Assign a new value to a local variable
pub inline extern local-setstd/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> ()<a,s,e>( ^v: local-varstd/core/types/local-var: (H, V) -> V<ss: H,aa: V>, assigned: aa: V) : <localstd/core/types/local: H -> X<ss: H>|std/core/types/effect-extend: (X, E) -> Eee: E> (std/core/types/unit: V)std/core/types/unit: V
  c  "kk_ref_set_borrow"
  cs inline "#1.Set(#2)";
  js inline "((#1).value = #2)"

// Read the value of a local variable.
pub inline extern local-getstd/core/types/local-get: forall<a,h,e> (v : local-var<h,a>) -> <local<h>|e> a with hdiv<h,a,e> : forall<aa: V,ss: H,ee: E> (v: 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> aa: V with(hdivstd/core/types/hdiv: (H, V, E) -> P<ss: H,aa: V,ee: E>)
  c  "kk_ref_get"
  cs inline "#1.Value";
  js inline "((#1).value)";

// _Internal_: if local mutation is unobservable, the `:local` effect can be erased by using the `local-scope` function.
// See also: _State in Haskell, by Simon Peyton Jones and John Launchbury_.
pub inline fun local-scopestd/core/types/local-scope: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> e a<aa: V,ee: E>( actionaction: forall<h> () -> <local<h>|$2248> $2247 : forall<hh: H> () -> <localstd/core/types/local: H -> X<hh: H> |std/core/types/effect-extend: (X, E) -> E ee: E> aa: V)result: -> 2277 2276 : ee: E aa: V
  unsafe-no-local-caststd/core/types/unsafe-no-local-cast: (action : forall<h> () -> <local<h>|$2248> $2247) -> $2248 (() -> $2248 $2247)(actionaction: forall<h> () -> <local<h>|$2248> $2247)()

inline extern unsafe-no-local-caststd/core/types/unsafe-no-local-cast: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> (() -> e a) : forall<aa: V,ee: E> ( action : forall<hh: H> () -> <localstd/core/types/local: H -> X<hh: H>|std/core/types/effect-extend: (X, E) -> Eee: E> aa: V ) -> ((std/core/types/total: E) -> ee: E aa: V)
  inline "#1"

/*
inline extern local-scope : forall<e,a> ( action : forall<h> () -> <local<h> | e> a) -> e a
  c  "(kk_function_call(kk_box_t,(kk_function_t,kk_context_t*),#1,(#1,kk_context())))"
  cs inline "Primitive.Run<##2>(#1)";
  js inline "((#1)())";
*/

// _Internal_: used to pass locals by reference.
pub inline extern @byref(loc : aa: V) : astd/core/types/total: E
  inline "#1"


// ----------------------------------------------------------------------------
// Used during codegen
// ----------------------------------------------------------------------------

// Magic casting to the `:any` type.
pub inline extern @toany( x : aa: V ) : anystd/core/types/any: V
  inline "#1"
  cs inline "(object)(#1)"

// Internal: used for value effects
pub type @valueop<ee: E::E,aa: V::V>
  con @Valueop


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

// _Internal_: Optional is used by the compiler to pass optional arguments.
// It is usually displayed as `: ? tp` for some type `:tp`.
pub value type @optional<aa: V>
  // The `Optional` constructor is used when an optional argument is given.
  con @Optional( value : aa: V )
  // `None` is used when an optional argument is not provided.
  con @None   // note: must come second; see Core/Core.hs


// ----------------------------------------------------------------------------
// First-class constructor contexts.
// These primitives are used by the compiler for
// _tail recursion module cons_ (TRMC) optimization.
// ----------------------------------------------------------------------------

extern import
  c header-end-file "inline/types-cctx.h"
  js file "inline/types-cctx.js"

extern import
  c file "inline/types-cctx.c"

// _Internal_. Internal type for constructor contexts.
// Holds the address to a field of type `:a` in a constructor.
pub type @field-addr<aa: V>

// _Internal_. Internal function name for field addresses.
pub fip extern @field-addr-of( xx: $2285 : aa: V, connameconname: string : stringstd/core/types/string: V, fieldnamefieldname: string : stringstd/core/types/string: V ) : @field-addrstd/core/types/total: E<aa: V>
  c inline "kk_field_addr_null()"
  inline ""  // compiled specially

// First-class constructor context (for _tail recursion modulo cons_ (TRMC) optimization).
// See also ``samples/learn/contexts`` for further examples.
abstract value type cctxstd/core/types/cctx: (V, V) -> V<aa: V,bb: V>
  con @Cctx( resstd/core/types/cctx/res: forall<a,b> (cctx : cctx<a,b>) -> a : aa: V, holeptrstd/core/types/cctx/holeptr: forall<a,b> (cctx : cctx<a,b>) -> @field-addr<b> : @field-addr<bb: V> )

// A first-class constructor context where the hole is of the same type as the root of the structure.
pub alias ctxstd/core/types/ctx: V -> V<aa: V> = cctxstd/core/types/cctx: (V, V) -> V<aa: V,aa: V>

// _Internal_. Create a hole for a context
pub inline fip extern @cctx-hole-create() : astd/core/types/total: E
  c  inline "kk_cctx_hole()"
  js inline "undefined"

// _Internal_. Create an initial non-empty context.
pub inline fip extern @cctx-create( x : aa: V, xhole : @field-addr<bb: V> ) : cctxstd/core/types/cctx: (V, V) -> V<aa: V,bb: V>
  c   "kk_cctx_create"
  js  "$std_core_types._cctx_create"

// _Internal_. Extend a constructor context with a guaranteed non-empty context
pub inline fip extern @cctx-extend( c : cctxstd/core/types/cctx: (V, V) -> V<aa: V,bb: V>, x : bb: V, xhole : @field-addr<cc: V> ) : cctxstd/core/types/cctx: (V, V) -> V<aa: V,cc: V>
  c inline "kk_cctx_extend(#1,#2,#3,kk_context())"
  js "$std_core_types._cctx_extend"

// _Internal_. Compose a constructor context with a guaranteed non-empty context
pub inline fip extern @cctx-compose-extend( c1 : cctxstd/core/types/cctx: (V, V) -> V<aa: V,bb: V>, c2 : cctxstd/core/types/cctx: (V, V) -> V<bb: V,cc: V> ) : cctxstd/core/types/cctx: (V, V) -> V<aa: V,cc: V>
  c inline "kk_cctx_extend(#1,#2.res,#2.holeptr,kk_context())"
  js "$std_core_types._cctx_compose"

// Apply a constructor context to its final value (of type `:b`), which is
// put into the hole of the context, and returns the root of the resulting structure `:a`.
// This is a constant time operation for unique contexts.
//
// `(ctx Cons(1,_)) ++ (ctx Cons(_,Nil)) ++. 3 == [1,3]`
pub inline fip extern cctx/(++.)std/core/types/cctx/(++.): forall<a,b> (c : cctx<a,b>, x : b) -> a( c : cctxstd/core/types/cctx: (V, V) -> V<aa: V,bb: V>, x : bb: V ) : astd/core/types/total: E
  c inline "kk_cctx_apply(#1,#2,kk_context())"
  js "$std_core_types._cctx_apply"

// Compose two constructor contexts.
// This is a constant time operation for unique contexts.
//
// `(ctx Cons(1,_)) ++ (ctx Cons(2,_)) ++. Nil == [1,2]`
pub inline fip extern cctx/(++)std/core/types/cctx/(++): forall<a,b,c> (c1 : cctx<a,b>, c2 : cctx<b,c>) -> cctx<a,c>( c1 : cctxstd/core/types/cctx: (V, V) -> V<aa: V,bb: V>, c2 : cctxstd/core/types/cctx: (V, V) -> V<bb: V,cc: V> ) : cctxstd/core/types/cctx: (V, V) -> V<aa: V,cc: V>
  c inline "kk_cctx_compose(#1,#2,kk_context())"
  js "$std_core_types._cctx_compose"

// Create an empty context. Usually written directly as an empty context `ctx _`.
pub inline fip extern cctx/emptystd/core/types/cctx/empty: forall<a> () -> cctx<a,a>() : cctxstd/core/types/cctx: (V, V) -> V<aa: V,aa: V>
  c  "kk_cctx_empty"
  js "$std_core_types._cctx_empty"