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

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

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

// An arbitrary precision signed integer.
type intstd/core/types/int: 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 also the [``std/text/string``](std_text_string.html) module.
type stringstd/core/types/string: V

// A 64-bit IEEE 754 floating point value.
// See also `std/num/double` for more operations on `:double`s.
value type doublestd/core/types/double: V

// A 32-bit signed integer (represented in two's complement).
// See the `module std/num/int32` module for operations on 32-bit integers.
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.
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.
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.
value type intptr_tstd/core/types/intptr_t: V

// A 8-bit unsigned integer.
// Provides no operations but is used mostly for interaction with external code.
value type bytestd/core/types/byte: V

// A 32-bit IEEE 754 floating point value.
// Not supported by the Javascript backend
// Provides no operations but is used mostly for interaction with external code.
value type float32std/core/types/float32: V




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

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

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

// 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 [``std/text/unicode``](std_text_unicode.html) module.)
value type charstd/core/types/char: V

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

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

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


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

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

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

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

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

// Stateful funs can manipulate heap `:h` using allocations, reads and writes.
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
type globalstd/core/types/global: H :: H


// ----------------------------------------------------------------------------
// 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`.
type boolstd/core/types/bool: V {
  con Falsebool: bool
  con Truebool: bool
}

// The unit type `:()` is inhabited by just a single value, namely `()`.
// See also the `:void` type and the `:bool` type.
struct (std/core/types/(): V)std/core/types/(): V

// A pair of values `:a` and `:b`.
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.
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.
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.
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_.
type maybestd/core/types/maybe: V -> V<aa: V> {
  con Nothingmaybe: maybe<_2184>
  con Justmaybe: maybe<_2195>( valuevalue: 105 : aa: V )
}

// The choice type represents one of two possible types `:a` or `:b`.
type eitherstd/core/types/either: (V, V) -> V<aa: V,bb: V> {
  con Lefteither: either<_2077,_2078>( leftleft: 72 : aa: V )
  con Righteither: either<_2090,_2091>( rightright: 73 : bb: V )
}

// An enumeration to represent order
type orderstd/core/types/order: V {
  Ltorder: order
  Eqorder: order
  Gtorder: order
}

// Explicitly box values using the `Box` constructor.
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.
reference type hboxstd/core/types/hbox: V -> V<aa: V> {
  con Hboxstd/core/types/Hbox: forall<a> (unhbox : a) -> hbox<a>( unhboxunhbox: 84 : aa: V )
}

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

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

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

fun idstd/core/types/id: forall<a> (x : a) -> a(xx: $2302 : aa: V) : astd/core/types/(<>): E {
  xx: $2302
}

// Logical conjuction
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 (std/core/types/True: boolxx: bool) then yy: bool else Falsestd/core/types/False: bool
}

// Logical disjunction
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 (std/core/types/True: boolxx: bool) then Truestd/core/types/True: bool else yy: bool
}


// inline extern (&&) : (bool,bool) -> bool  { inline "(#1 && #2)" }
// inline extern (||) : (bool,bool) -> bool  { inline "(#1 || #2)" }

fun (!)std/core/types/(!).1: (b : bool) -> bool( bb: bool : boolstd/core/types/bool: V ) : boolstd/core/types/bool: V 
  if (std/core/types/True: boolbb: bool) then Falsestd/core/types/False: bool else Truestd/core/types/True: bool

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

//inline extern not  : (bool) -> bool  { inline "!(#1)" }
//inline extern (!)  : (bool) -> bool  { inline "!(#1)" }

// needed for markers in `std/core/hnd`.
inline extern zero32std/core/types/zero32: () -> int32() : int32std/core/types/int32: V { inline "0" }


// Generated by type inference and later refined into one of the `open` variants in `std/core/hnd`.
public noinline extern ".open"<e1e1: E::E,e2e2: E::E,aa: V,bb: V>( xx: $2258 : 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.
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.
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`.
type refstd/core/types/ref: (H, V) -> V :: (H,V) -> V

// Allocate a fresh reference with an initial value.
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 inline "kk_ref_alloc(#1,kk_context())"
  cs inline "new Ref<##1,##2>(#1)"
  js inline "{ value: #1 }"
}

// Assign a new value to a reference.
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 inline "kk_ref_set_borrow(#1,#2,kk_context())"
  cs inline "#1.Set(#2)"
  js inline "((#1).value = #2)"
}

// Read the value of a reference.
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 inline "kk_ref_get(#1,kk_context())"
  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 will pass its ownership to the given function.
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  inline "kk_ref_modify(#1, #2, kk_context())"
  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_.
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`
type localstd/core/types/local: H -> X :: (H) -> X
type local-varstd/core/types/local-var: (H, V) -> V :: (H,V) -> V

// Allocate a fresh local with an initial value.
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 inline "kk_ref_alloc(#1,kk_context())"
  cs inline "new Ref<##1,##2>(#1)"
  js inline "{ value: #1 }"
}

// Assign a new value to a local variable
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 inline "(kk_ref_set_borrow(#1,#2,kk_context()))"
  cs inline "#1.Set(#2)";
  js inline "((#1).value = #2)"
}

// Read the value of a local variable.
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 inline "(kk_ref_get(#1,kk_context()))"
  cs inline "#1.Value";
  js inline "((#1).value)";
}

private 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" }

// 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_.
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>|$2317> $2316 : 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>|$2317> $2316)()
}

/*
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)())";
}
*/

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`).
inline extern unsafe-decreasingstd/core/types/unsafe-decreasing: forall<a> (x : a) -> a( x : aa: V ) : astd/core/types/(<>): E { inline "#1" }

private 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.
fun unsafe-totalstd/core/types/unsafe-total: forall<a,e> (action : () -> e a) -> a( actionaction: () -> $2396 $2395 : () -> ee: E aa: V ) : astd/core/types/(<>): E {
  unsafe-total-caststd/core/types/unsafe-total-cast: forall<e,a> (action : () -> e a) -> (() -> a)( actionaction: () -> $2396 $2395 )()
}

// _Unsafe_. This function pretends the give action was deterministic
fun unsafe-no-ndetstd/core/types/unsafe-no-ndet: forall<a,e> (action : () -> <ndet|e> a) -> e a( actionaction: () -> <ndet|$2380> $2379 : () -> <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|$2380> $2379 )()
}

// _Unsafe_. This function pretends the give action is terminating
fun unsafe-no-divstd/core/types/unsafe-no-div: forall<a,e> (action : () -> <div|e> a) -> e a( actionaction: () -> <div|$2364> $2363 : () -> <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|$2364> $2363 )()
}

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

// Optional is used internally by the compiler to pass optional arguments.
// It is usually displayed as `:?a` for some type `:a`.
type optionalstd/core/types/optional: V -> V<aa: V> {
  // The `Optional` constructor is used when an optional argument is given.
  con Optionaloptional: ?_2207( valuevalue: 110 : aa: V )
  // `None` is used when an optional argument is not provided.
  con Noneoptional: ?_2219
}

// Handled effects are lifted to an atomic effect using the `:handled` type constructor
type handledstd/core/types/handled: HX -> X    :: HX -> X;

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



// ----------------------------------------------------------------------------
// 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.
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: 60 : aa: V, holehole: cfield<60> : cfieldstd/core/types/cfield: V -> V<aa: V> )

/*
// address of a field in a constructor (this is implemented in the compiler backend)
inline extern ".cfield-of"( obj : a, conname : string, fieldname : string ) : cfield<a> { } 

// create 'hole' of a certain type that is to be filled in later by ctail-link/ctail-resolve
// implemented in the compiler backend as it needs to by typed correctly (and should not be unboxed)
inline extern ".cfield-hole"() : a { }

// initial accumulator (generated in the Core/CTail.hs)
inline extern ".ctail-nil"() : ctail<a> {
  c inline "kk_ctail_nil()"
}

// accumulate (generated in the Core/CTail.hs)
inline extern ".ctail-link"( acc : ctail<a>, res : a, field : cfield<a> ) : ctail<a> {
  c inline "kk_ctail_link(#1,#2,#3)"
}

// resolve to final result (generated in the Core/CTail.hs)
inline extern ".ctail-resolve"( acc : ctail<a>, res : a ) : ctail<a> {
  c inline "kk_ctail_resolve(#1,#2)"
}
*/