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

// Standard output to the console.
module std/core/consolestd/core/console

import std/core/typesstd/core/types
import std/core/unsafestd/core/unsafe
import std/core/hndstd/core/hnd
import std/core/stringstd/core/string
import std/core/showstd/core/show

extern import
  js file "inline/console.js"


// The console effect signifies that a function may write to the console.
pub type consolestd/core/console/console: X :: X


// ----------------------------------------------------------------------------
// Print to the console
// ----------------------------------------------------------------------------

noinline val redirectstd/core/console/redirect: ref<global,maybe<(string) -> console ()>> : refstd/core/types/ref: (H, V) -> V<globalstd/core/types/global: H,maybestd/core/types/maybe: V -> V<(stringstd/core/types/string: V) -> consolestd/core/console/console: X (std/core/types/unit: V)std/core/types/unit: V>> =
  unsafe-totalstd/core/unsafe/unsafe-total: (action : () -> <alloc<global>|_68> ref<global,maybe<(string) -> console ()>>) -> ref<global,maybe<(string) -> console ()>> { refstd/core/types/ref: (value : maybe<(string) -> console ()>) -> <alloc<global>|_68> ref<global,maybe<(string) -> console ()>>(Nothingstd/core/types/Nothing: forall<a> maybe<a>) }

// Redirect `print` and `println` calls to a specified function.
noinline fun print-redirectstd/core/console/print-redirect: (print : (msg : string) -> console ()) -> <st<global>,console,ndet> ()( printprint: (msg : string) -> console () : (msg : stringstd/core/types/string: V) -> consolestd/core/console/console: X (std/core/types/unit: V)std/core/types/unit: V )result: -> <st<global>,console,ndet> () : <std/core/types/total: Endetstd/core/types/ndet: X,consolestd/core/console/console: X,ststd/core/types/st: H -> E<globalstd/core/types/global: H>> (std/core/types/unit: V)std/core/types/unit: V
  redirectstd/core/console/redirect: ref<global,maybe<(string) -> console ()>> :=std/core/types/set: (ref : ref<global,maybe<(string) -> console ()>>, assigned : maybe<(string) -> console ()>) -> <write<global>,alloc<global>,console,ndet,read<global>> () Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(printprint: (msg : string) -> console ())

// Print a string to the console, including a final newline character.
extern xprintslnstd/core/console/xprintsln: (s : string) -> console ()(ss: string : stringstd/core/types/string: V) : consolestd/core/console/console: X (std/core/types/unit: V)std/core/types/unit: V
  c  "kk_println"
  cs "Console.WriteLine"
  js "_println"

// Print a string to the console
extern xprintsstd/core/console/xprints: (s : string) -> console ()( ss: string : stringstd/core/types/string: V) : consolestd/core/console/console: X (std/core/types/unit: V)std/core/types/unit: V
  c  "kk_print"
  cs "Console.Write"
  js "_print"

// _Unsafe_. This function removes the state effect from the effect of an action
inline extern unsafe-nostatestd/core/console/unsafe-nostate: forall<a,h> (action : () -> <st<h>,console> a) -> (() -> console a)( action : () -> <std/core/types/total: Eststd/core/types/st: H -> E<hh: H>,consolestd/core/console/console: X> aa: V ) : ((std/core/types/total: E) -> consolestd/core/console/console: X aa: V)
  inline "#1"

noinline fun printsstd/core/console/prints: (s : string) -> console ()( ss: string : stringstd/core/types/string: V )result: -> console () : consolestd/core/console/console: X (std/core/types/unit: V)std/core/types/unit: V
  (unsafe-nostatestd/core/console/unsafe-nostate: (action : () -> <st<global>,console> ()) -> console (() -> console ())
    match !std/core/types/ref/(!): (ref : ref<global,maybe<(string) -> console ()>>) -> <read<global>,console,alloc<_94>,write<global>> maybe<(string) -> console ()>redirectstd/core/console/redirect: ref<global,maybe<(string) -> console ()>>
      Nothingstd/core/types/Nothing: forall<a> maybe<a> -> xprintsstd/core/console/xprints: (s : string) -> <console,read<global>,alloc<_94>,write<global>> ()(ss: string)
      Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(ff: (string) -> console ()) -> ff: (string) -> <console,read<global>,alloc<_94>,write<global>> ()(ss: string)
  )()

noinline fun printslnstd/core/console/printsln: (s : string) -> console ()( ss: string : stringstd/core/types/string: V )result: -> console () : consolestd/core/console/console: X (std/core/types/unit: V)std/core/types/unit: V
  (unsafe-nostatestd/core/console/unsafe-nostate: (action : () -> <st<global>,console> ()) -> console (() -> console ())
    match !std/core/types/ref/(!): (ref : ref<global,maybe<(string) -> console ()>>) -> <read<global>,console,alloc<_195>,write<global>> maybe<(string) -> console ()>redirectstd/core/console/redirect: ref<global,maybe<(string) -> console ()>>
      Nothingstd/core/types/Nothing: forall<a> maybe<a> -> xprintslnstd/core/console/xprintsln: (s : string) -> <console,read<global>,alloc<_195>,write<global>> ()(ss: string)
      Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(ff: (string) -> console ()) -> { ff: (string) -> <console,read<global>,alloc<_195>,write<global>> ()(ss: string ++std/core/types/(++): (x : string, y : string) -> <console,read<global>,alloc<_195>,write<global>> string "\n"literal: string
count= 1
) } )(
) // Print a string to the console. pub fun string/printstd/core/console/string/print: (s : string) -> console ()(ss: string : stringstd/core/types/string: V)result: -> console () printsstd/core/console/prints: (s : string) -> console ()(ss: string) // Print a value that has a `show` function pub fun show/printstd/core/console/show/print: forall<a> (x : a, @implicit/show : (a) -> string) -> console ()( xx: $138 : aa: V, @implicit/show?show: ($138) -> string : aa: V -> stringstd/core/types/string: V )result: -> console () : consolestd/core/console/console: X (std/core/types/unit: V)std/core/types/unit: V printsstd/core/console/prints: (s : string) -> console ()(xx: $138.show?show: ($138) -> console string) // Print a string to the console, including a final newline character. pub fun string/printlnstd/core/console/string/println: (s : string) -> console ()(ss: string : stringstd/core/types/string: V)result: -> console () : consolestd/core/console/console: X (std/core/types/unit: V)std/core/types/unit: V printslnstd/core/console/printsln: (s : string) -> console ()(ss: string) // Print a value that has a `show` function, including a final newline character. pub fun show/printlnstd/core/console/show/println: forall<a> (x : a, @implicit/show : (a) -> string) -> console ()( xx: $250 : aa: V, @implicit/show?show: ($250) -> string : aa: V -> stringstd/core/types/string: V )result: -> console () : consolestd/core/console/console: X (std/core/types/unit: V)std/core/types/unit: V printslnstd/core/console/printsln: (s : string) -> console ()(xx: $250.show?show: ($250) -> console string)