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

// Unsafe primitives to dismiss effects.
module std/core/unsafestd/core/unsafe

import std/core/typesstd/core/types

// _Unsafe_. This function calls a function and pretends it did not have any effect at all.
// Use with utmost care as it should not be used to dismiss user-defined effects that need
// a handler and can cause a segfault at runtime in such cases!
//
// You can use `unsafe-total` to dismiss built-in effects without handlers which include:
//
// - behavioral: `:div` (non-termination/divergence), `:ndet` (non-determinism)
// - state: `:alloc`, `:read`, `:write`, `:st`
// - external: `:ui`, `:fsys`, `:net`, `:blocking`
// - combinations: `:ioc-total` and `:ioc`
//
// Do _not_ dismiss `:io` since it has the `:exn` effect that should be handled (and an evidence
// vector should be passed in).
//
// Try to avoid using `unsafe-total` to initialize global values that have a side-effect, but
// use `std/core/delayed/delay` instead:
// ```
// val myglobal = delay( fn() initialize() )
// fun get-global() : e int
//   myglobal.force
// ```
pub fun unsafe-totalstd/core/unsafe/unsafe-total: forall<a,e> (action : () -> e a) -> a( actionaction: () -> $51 $50 : () -> ee: E aa: V )result: -> total 75 : astd/core/types/total: E
  unsafe-total-caststd/core/unsafe/unsafe-total-cast: (action : () -> $51 $50) -> (() -> $50)( actionaction: () -> $51 $50 )()

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

// _Unsafe_. This function pretends the given `action` is deterministic
pub fun pretend-no-ndetstd/core/unsafe/pretend-no-ndet: forall<a,e> (action : () -> <ndet|e> a) -> e a( actionaction: () -> <ndet|$85> $84 : () -> <ndetstd/core/types/ndet: X|std/core/types/effect-extend: (X, E) -> Eee: E> aa: V )result: -> 108 107 : ee: E aa: V
  // unsafe-total-cast( action )()  // this can segfault as it drops the e which can contain handled effects
  unsafe-no-ndet-caststd/core/unsafe/unsafe-no-ndet-cast: (() -> <ndet|$85> $84) -> $85 (() -> $85 $84)(actionaction: () -> <ndet|$85> $84)()

inline fip extern unsafe-no-ndet-caststd/core/unsafe/unsafe-no-ndet-cast: forall<a,e> (() -> <ndet|e> a) -> (() -> e a): forall<aa: V,ee: E> (() -> <ndetstd/core/types/ndet: X|std/core/types/effect-extend: (X, E) -> Eee: E> aa: V) -> ((std/core/types/total: E) -> ee: E aa: V)
  inline "#1"

// Collapse multiple ndet effects into one (this is safe).
pub fun collapse-ndetstd/core/unsafe/collapse-ndet: forall<a,e> (action : () -> <ndet,ndet|e> a) -> <ndet|e> a( actionaction: () -> <ndet,ndet|$116> $115 : () -> <ndetstd/core/types/ndet: X,ndetstd/core/types/ndet: X|std/core/types/effect-extend: (X, E) -> Eee: E> aa: V )result: -> <ndet|138> 137 : <ndetstd/core/types/ndet: X|std/core/types/effect-extend: (X, E) -> Eee: E> aa: V
  pretend-no-ndetstd/core/unsafe/pretend-no-ndet: (action : () -> <ndet,ndet|$116> $115) -> <ndet|$116> $115(actionaction: () -> <ndet,ndet|$116> $115)


// _Unsafe_. This function checks if two objects have the same address in the heap.
// The results may vary on the backend or compiler optimizations but the function pretends to be `:total`.
// Note also that value types always compare unequal since each value will be boxed fresh in the heap
// when calling this function.
pub inline extern unsafe-ptr-eqstd/core/unsafe/unsafe-ptr-eq: forall<a> (x : a, y : a) -> bool( ^x : aa: V, ^y : aa: V ) : boolstd/core/types/bool: V
  c  inline "kk_box_eq(#1,#2)"
  cs inline "Object.ReferenceEquals(#1,#2)"
  js inline "Object.is(#1,#2)"