/*---------------------------------------------------------------------------
  Copyright 2012-2021, 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.
---------------------------------------------------------------------------*/

/* Core types.

   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`)
*/
module types

pub infixr 30  (&&)
pub infixr 20  (||)

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

// An arbitrary precision signed integer.
pub type intstd/core/types/int: V

// A 64-bit IEEE 754 double precision floating point value.
// See also `module std/num/float64` for more 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 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.
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

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

// Internal type used for in-place update of unique pattern matches
pub type reusestd/core/types/reuse: V

pub extern no-reusestd/core/types/no-reuse: () -> reuse() : reusestd/core/types/reuse: V
  c inline  "NULL"
  js inline "null"


// The _total_ effect represents the absence of any effect.
pub type <std/core/types/(<>): E> :: E

// The effect constructor extends an effect with another effect.
pub type <std/core/types/(<|>): (X, E) -> E|> :: (X,E) -> E

// The type of immutable arrays is called `:vector`.
pub type vectorstd/core/types/vector: V -> V<aa: V>


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

// The non-determism 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/(<>): 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
pub type handledstd/core/types/handled: HX -> X    :: HX -> X;

// Linear effects are lifted to an atomic effect using the `:handled1` type constructor
pub type handled1std/core/types/handled1: HX1 -> X   :: HX1 -> X;


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

// The `:void` type is empty and has no constructors.
// See also the `:()` unit type and the `:bool` type.
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 `:()` is inhabited by just a single value, namely `()`.
// See also the `:void` type and the `:bool` type.
pub struct (std/core/types/(): V)std/core/types/(): V

// A pair of values `:a` and `:b`.
pub struct (std/core/types/(,): (V, V) -> V,)std/core/types/(,): (V, V) -> V<aa: V,bb: V>(fstfst: 6:aa: V,sndsnd: 7:bb: V)

// A triple of values.
pub struct (std/core/types/(,,): (V, V, V) -> V,,)std/core/types/(,,): (V, V, V) -> V<aa: V,bb: V,cc: V>(fstfst: 13:aa: V,sndsnd: 14:bb: V,thdthd: 15:cc: V)

// A quadruple of values.
pub struct (std/core/types/(,,,): (V, V, V, V) -> V,,,)std/core/types/(,,,): (V, V, V, V) -> V<aa: V,bb: V,cc: V,dd: V>(fstfst: 22:aa: V,sndsnd: 23:bb: V,thdthd: 24:cc: V,field4field4: 25:dd: V)

// A quintuple of values.
pub struct (std/core/types/(,,,,): (V, V, V, V, V) -> V,,,,)std/core/types/(,,,,): (V, V, V, V, V) -> V<aa: V,bb: V,cc: V,dd: V,ee: V>(fstfst: 33:aa: V,sndsnd: 34:bb: V,thdthd: 35:cc: V,field4field4: 36:dd: V,field5field5: 37: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_.
pub type maybestd/core/types/maybe: V -> V<aa: V>
  con Nothingstd/core/types/Nothing: forall<a> maybe<a>
  con Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>( valuevalue: 107 : aa: V )

// The choice type represents one of two possible types `:a` or `:b`.
pub type eitherstd/core/types/either: (V, V) -> V<aa: V,bb: V>
  con Leftstd/core/types/Left: forall<a,b> (left : a) -> either<a,b>( leftleft: 68 : aa: V )
  con Rightstd/core/types/Right: forall<a,b> (right : b) -> either<a,b>( rightright: 69 : bb: V )

// An enumeration to represent order
pub type orderstd/core/types/order: V
  Ltstd/core/types/Lt: order
  Eqstd/core/types/Eq: order
  Gtstd/core/types/Gt: order

// 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>( unboxunbox: 47 : aa: V )

// Explicitly heap allocate using the `Hbox` constructor.
pub reference type hboxstd/core/types/hbox: V -> V<aa: V>
  con Hboxstd/core/types/Hbox: forall<a> (unhbox : a) -> hbox<a>( unhboxunhbox: 82 : aa: V )

pub fun hboxstd/core/types/hbox: forall<a> (x : a) -> hbox<a>( xx: $2421 : aa: V ) : hboxstd/core/types/hbox: V -> V<aa: V>
  Hboxstd/core/types/Hbox: forall<a> (unhbox : a) -> hbox<a>(xx: $2421)

pub noinline fun keepstd/core/types/keep: forall<a> (x : a) -> a( xx: $2311 : aa: V ) : astd/core/types/(<>): E
  xx: $2311

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

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

// Logical conjuction
pub fun (&&)std/core/types/(&&): (x : bool, y : bool) -> bool( xx: bool : boolstd/core/types/bool: V, yy: bool : boolstd/core/types/bool: V) : 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
pub fun (||)std/core/types/(||): (x : bool, y : bool) -> bool( xx: bool : boolstd/core/types/bool: V, yy: bool : boolstd/core/types/bool: V) : 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 fun (!)std/core/types/(!).1: (b : bool) -> bool( bb: bool : boolstd/core/types/bool: V ) : boolstd/core/types/bool: V 
  if bb: bool then Falsestd/core/types/False: bool else Truestd/core/types/True: bool

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

// _Internal_: 32-bit zero, needed for markers in `std/core/hnd`.
pub inline extern zero32std/core/types/zero32: () -> int32() : int32std/core/types/int32: V  
  inline "0"

// _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: $2260 : 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/(<>): Ewritestd/core/types/write: H -> X<hh: H>> (std/core/types/(): V)std/core/types/(): 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 (!)std/core/types/(!): 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/(<|>): (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/(<|>): (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/(<|>): (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/(<|>): (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())))"
  cs inline "Primitive.Run<##2>(#1)"
  js inline "((#1)())"


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

// A local variable `:var<s,a>` points to a value of type `:a` in local scope `:s`
pub type localstd/core/types/local: H -> X :: (H) -> X
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/(<|>): (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/(<|>): (X, E) -> Eee: E> (std/core/types/(): V)std/core/types/(): 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/(<|>): (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)";


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/(<|>): (X, E) -> Eee: E> aa: V ) -> ((std/core/types/(<>): E) -> ee: E aa: V) 
  inline "#1"

// _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>|$2319> $2318 : forall<hh: H> () -> <localstd/core/types/local: H -> X<hh: H> |std/core/types/(<|>): (X, E) -> E ee: E> aa: V) : ee: E aa: V
  unsafe-no-local-caststd/core/types/unsafe-no-local-cast: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> (() -> e a)(actionaction: forall<h> () -> <local<h>|$2319> $2318)()

/*
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 byrefstd/core/types/byref: forall<a> (loc : a) -> a(loc : aa: V) : astd/core/types/(<>): E 
  inline "#1"

// ----------------------------------------------------------------------------
// Unsafe: todo: move to separate module
// ----------------------------------------------------------------------------

// _Unsafe_. Mark a function parameter as decreasing to suppress the non-termination effect (`:div`).
pub inline extern unsafe-decreasingstd/core/types/unsafe-decreasing: forall<a> (x : a) -> a( x : aa: V ) : astd/core/types/(<>): E 
  inline "#1"

inline extern unsafe-total-caststd/core/types/unsafe-total-cast: forall<e,a> (action : () -> e a) -> (() -> a) : forall<ee: E,aa: V> ( action : () -> ee: E aa: V ) -> ((std/core/types/(<>): E) -> astd/core/types/(<>): E) 
  inline "#1"

// _Unsafe_. This function calls a function and pretends it did not have any effect at all.
pub fun unsafe-totalstd/core/types/unsafe-total: forall<a,e> (action : () -> e a) -> a( actionaction: () -> $2398 $2397 : () -> ee: E aa: V ) : astd/core/types/(<>): E
  unsafe-total-caststd/core/types/unsafe-total-cast: forall<e,a> (action : () -> e a) -> (() -> a)( actionaction: () -> $2398 $2397 )()

// _Unsafe_. This function pretends the give action was deterministic
pub fun unsafe-no-ndetstd/core/types/unsafe-no-ndet: forall<a,e> (action : () -> <ndet|e> a) -> e a( actionaction: () -> <ndet|$2382> $2381 : () -> <ndetstd/core/types/ndet: X|std/core/types/(<|>): (X, E) -> Eee: E> aa: V ) : ee: E aa: V
  unsafe-total-caststd/core/types/unsafe-total-cast: forall<e,a> (action : () -> e a) -> (() -> a)( actionaction: () -> <ndet|$2382> $2381 )()

// _Unsafe_. This function pretends the give action is terminating
pub fun unsafe-no-divstd/core/types/unsafe-no-div: forall<a,e> (action : () -> <div|e> a) -> e a( actionaction: () -> <div|$2366> $2365 : () -> <divstd/core/types/div: X|std/core/types/(<|>): (X, E) -> Eee: E> aa: V ) : ee: E aa: V
  unsafe-total-caststd/core/types/unsafe-total-cast: forall<e,a> (action : () -> e a) -> (() -> a)( actionaction: () -> <div|$2366> $2365 )()


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

// _Internal_: Optional is used by the compiler to pass optional arguments.
// It is usually displayed as `:?a` for some type `:a`.
pub value type optionalstd/core/types/optional: V -> V<aa: V>
  // The `Optional` constructor is used when an optional argument is given.
  con Optionalstd/core/types/Optional: forall<a> (value : a) -> ?a( valuevalue: 112 : aa: V )
  // `None` is used when an optional argument is not provided.
  con Nonestd/core/types/None: forall<a> ?a



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

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


// _Internal_. Internal type for _tail recursion module cons_ (TRMC) optimization.
// Holds the address to a field of type `:a` in a constructor.
pub value type cfieldstd/core/types/cfield: V -> V<aa: V>

// _Internal_. Internal type for _tail recursion module cons_ (TRMC) optimization.
abstract value type ctailstd/core/types/ctail: V -> V<aa: V>
  ".CTail"( resres: 58 : aa: V, holehole: cfield<58> : cfieldstd/core/types/cfield: V -> V<aa: V> )