/*---------------------------------------------------------------------------
  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 divergence.
module std/core/undivstd/core/undiv

import std/core/typesstd/core/types

// _Unsafe_. Mark a function parameter as decreasing to suppress the non-termination effect (`:div`).
// The compiler has a very limited termination analysis, only recognizing direct recursion on
// inductive datatypes. When it is clear a function has a decreasing parameter but it is not recognized
// as such by the compiler, you can wrap the arguments in `pretend-decreasing` to inform the
// termination analysis to consider that parameter decreasing on a recursive call. Use with care
// to not accidentally allow actual divergence (without having that reflected in the effect type).
pub inline fip extern pretend-decreasingstd/core/undiv/pretend-decreasing: forall<a> (x : a) -> a( x : aa: V ) : astd/core/types/total: E
  inline "#1"

// _Unsafe_. This function pretends that the given action is terminating.
pub fun pretend-no-divstd/core/undiv/pretend-no-div: forall<a,e> (action : () -> <div|e> a) -> e a( actionaction: () -> <div|$38> $37 : () -> <divstd/core/types/div: X|std/core/types/effect-extend: (X, E) -> Eee: E> aa: V )result: -> 61 60 : ee: E aa: V
  pretend-nodiv-caststd/core/undiv/pretend-nodiv-cast: (action : () -> <div|$38> $37) -> $38 (() -> $38 $37)( actionaction: () -> <div|$38> $37 )()

inline fip extern pretend-nodiv-caststd/core/undiv/pretend-nodiv-cast: forall<e,a> (action : () -> <div|e> a) -> (() -> e a) : forall<ee: E,aa: V> ( action : () -> <divstd/core/types/div: 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 div effects into one (this is safe).
pub fun collapse-divstd/core/undiv/collapse-div: forall<a,e> (action : () -> <div,div|e> a) -> <div|e> a( actionaction: () -> <div,div|$69> $68 : () -> <divstd/core/types/div: X,divstd/core/types/div: X|std/core/types/effect-extend: (X, E) -> Eee: E> aa: V )result: -> <div|91> 90 : <divstd/core/types/div: X|std/core/types/effect-extend: (X, E) -> Eee: E> aa: V
  pretend-no-divstd/core/undiv/pretend-no-div: (action : () -> <div,div|$69> $68) -> <div|$69> $68(actionaction: () -> <div,div|$69> $68)