disallowed function effects incurred: stropt_is_some

[Brandon Barker]

This is some ATS1 code I was trying to port to ATS2.

Given the following definitions in ./prelude/SATS/CODEGEN/string.sats:

fun{
} stropt_is_some {n:int} (x: stropt n): bool (n >= 0)


castfn
stropt_unsome {n:nat} (x: stropt n): string (n)


(* ****** ****** *)
//
symintr strlen
symintr string_length
//
fun{
} string0_length
  (x: NSH(string)):<> size_t
fun{
} string1_length
  {n:int} (x: NSH(string(n))):<> size_t (n)
//
overload strlen with string0_length of 0
overload strlen with string1_length of 10
overload string_length with string0_length of 0
overload string_length with string1_length of 10
//
(* ****** ****** *)

The following function typehecked in ATS1 (was considred pure). This seems reasonable, the the above functions defined in ATS2 are not considered pure. Syntactically this makes sense, since the default effect is <1> I believe. But I wonder if these should be defined to be pure functions in ATS2. 

fn stropt_is_GE1 {i:int} (stropt: stropt i):<> bool (i >= 1)
  = if stropt_is_some(stropt) then let
        val slen = string_length(stropt_unsome(stropt))
      in
        slen >= 1
      end
    else false


implement main0 () = ()

Error message when using <>:

patscc -tcats /home/brand_000/test_stropt.dats

exec(patsopt --typecheck --dynamic /home/brand_000/test_stropt.dats)

Hello from ATS2(ATS/Postiats)!

Loading [fixity.ats] starts!

Loading [fixity.ats] finishes!

Loading [basics_pre.sats] starts!

Loading [basics_pre.sats] finishes!

Loading [basics_sta.sats] starts!

Loading [basics_sta.sats] finishes!

Loading [basics_dyn.sats] starts!

Loading [basics_dyn.sats] finishes!

Loading [basics_gen.sats] starts!

Loading [basics_gen.sats] finishes!

The 1st translation (fixity) of [/home/brand_000/test_stropt.dats] is successfully completed!

The 2nd translation (binding) of [/home/brand_000/test_stropt.dats] is successfully completed!

/home/brand_000/test_stropt.dats: 71(line=3, offs=8) -- 92(line=3, offs=29): error(3): [/home/brand_000/ATS-Postiats/src/pats_trans3_env_effect.dats]: the_effenv_check_set: some disallowed effects may be incurred: 1

/home/brand_000/test_stropt.dats: 136(line=4, offs=34) -- 156(line=4, offs=54): error(3): [/home/brand_000/ATS-Postiats/src/pats_trans3_env_effect.dats]: the_effenv_check_set: some disallowed effects may be incurred: 1

TRANS3: there are [4] errors in total.

exit(ATS): uncaught exception: _2home_2brand_000_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorException(1025)

exec(patsopt --typecheck --dynamic /home/brand_000/test_stropt.dats) = 256

Compilation exited abnormally with code 1 at Sun Jan 19 11:41:45

[gmhwxi]

I have just make stropt_is_some and stropt_unsome effect-free.

By the way, stropt_is_GE1 should use the following function (of time-complexity O(min(n1,n2)):

fun{
} strintcmp
  {n1,n2:int | n2 >=0}
  (x1: string n1, n2: int n2):<> int(sgn(n1-n2))
// end of [strintcmp]

fn stropt_is_GE1
  {i:int} (stropt: stropt i):<> bool (i >= 1) =
  if stropt_is_some(stropt)

    then strintcmp (stropt_unsome(stropt), 1) >= 0 else false
  // end of [if]

[gmhwxi]

Effect-tracking is a feature in ATS mostly for theorem proving.
If you think that a function you implement should be pure but the
typechecker does not agree, you can use $effmask_all(...) to
mask out effects.