(* ****** ****** )
//
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
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.On Sunday, January 19, 2014 2:07:18 PM UTC-5, gmhwxi wrote:
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]
On Sunday, January 19, 2014 11:52:34 AM UTC-5, Brandon Barker wrote:
This is some ATS1 code I was trying to port to ATS2.
Given the following definitions in ./prelude/SATS/CODEGEN/string.sats:
(* ****** ****** )
//
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
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]On Sunday, January 19, 2014 11:52:34 AM UTC-5, Brandon Barker wrote:
This is some ATS1 code I was trying to port to ATS2.
Given the following definitions in ./prelude/SATS/CODEGEN/string.sats:
(* ****** ****** )
//
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