How to identify dynamic value such like bool?

gmhwxi · October 24, 2015, 12:34pm

r_rps is not a constructor and thus cannot be used as a pattern
(the compiler treats it as a variable that matches any value)

Try:

datatype rps(rps) = r_rps(r_rps) | p_rps(p_rps) | s_rps(s_rps)

Then you can use r_rps() as a pattern.On Saturday, October 24, 2015 at 5:53:18 AM UTC-4, Kiwamu Okabe wrote:

Hi all,

I’m trying to define type to learn static side of ATS language.
The code is a library for Rock-paper-scissors.

https://github.com/jats-ug/practice-ats/tree/ce6d2001867fa4a9db6c3dc9fb2044d5346bfc6f/static_rps

First, I define Rock-paper-scissors sort with emulate bool.

https://github.com/jats-ug/practice-ats/blob/ce6d2001867fa4a9db6c3dc9fb2044d5346bfc6f/static_rps/rps.sats
datasort rps = (* abstract *) 

stacst r_rps: rps (* Rock *) 
and    p_rps: rps (* Paper *) 
and    s_rps: rps (* Scissors *) 

abst@ype rps (rps) = int 
typedef rps = [x:rps] rps (x) 

val r_rps: rps (r_rps) = "mac#" 
val p_rps: rps (p_rps) = "mac#" 
val s_rps: rps (s_rps) = "mac#" 

%{ 
#define r_rps 0 
#define p_rps 1 
#define s_rps 2 
%} 
And try to define print function on rps.

https://github.com/jats-ug/practice-ats/blob/ce6d2001867fa4a9db6c3dc9fb2044d5346bfc6f/static_rps/rps.dats
implement{} 
print_rps (x) = let val s = case x of 
  | r_rps => "Rock" 
  | p_rps => "Paper" 
  | s_rps => "Scissors" 
in 
  print_string s 
end 
However the compiler can’t identify the rps value.
$ patscc main.dats -DATS_MEMALLOC_LIBC 
/home/kiwamu/src/practice-ats/static_rps/rps.dats: 95(line=6, offs=5) 
-- 111(line=6, offs=21): error(3): this pattern match clause is 
redundant. 
/home/kiwamu/src/practice-ats/static_rps/rps.dats: 116(line=7, offs=5) 
-- 135(line=7, offs=24): error(3): this pattern match clause is 
redundant. 
How to identify dynamic value such like bool?

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

john_skaller · October 24, 2015, 6:53pm

‘true’ and ‘false’ are constants. They are treated specially when
used as patterns.

That’s naughty! Here’s what I did:

Felix originally copied Ocaml in having constant (no argument)
constructors. However I hate Camelcase. So I made the user do this:

| Fred ?argument => …
| Joe => …
This is ugly, having to put ? before variables.
So I changed it. I copied ATS No constant constructors:

| Fred argument => …
| Joe () => …
Felix always had an abbreviation in expressions:

#f ==> f ()

Its a shorthand which is very useful because in Felix type classes
you cannot have constants, only functions. So you have to do

#zero[double]

for example, for the real number class zero, instance double.

Hence:

match … with
| #True => …
| #False => …
In fact the parser translates true and false, they’re treated “special”
in the parser NOT in pattern matches. Having special things in core
parts of the compiler add complexity.

—
john skaller
ska...@users.sourceforge.net
http://felix-lang.org

gmhwxi · October 24, 2015, 1:32pm

They are defined in ${PATSHOME}/prelude/basics_dyn.datsOn Saturday, October 24, 2015 at 9:23:02 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Sat, Oct 24, 2015 at 10:07 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

‘true’ and ‘false’ are constants. They are treated specially when
used as patterns.

On Saturday, October 24, 2015 at 8:58:22 AM UTC-4, Kiwamu Okabe wrote:

Where is the constructor of true and false?

‘true’ and ‘false’ are pre-defined constants?
I can’t find the definition in prelude?

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

gmhwxi · October 24, 2015, 12:44pm

See:

https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST20/test20.datsOn Saturday, October 24, 2015 at 8:34:55 AM UTC-4, gmhwxi wrote:

r_rps is not a constructor and thus cannot be used as a pattern
(the compiler treats it as a variable that matches any value)

Try:

datatype rps(rps) = r_rps(r_rps) | p_rps(p_rps) | s_rps(s_rps)

Then you can use r_rps() as a pattern.

On Saturday, October 24, 2015 at 5:53:18 AM UTC-4, Kiwamu Okabe wrote:
Hi all,

I’m trying to define type to learn static side of ATS language.
The code is a library for Rock-paper-scissors.

https://github.com/jats-ug/practice-ats/tree/ce6d2001867fa4a9db6c3dc9fb2044d5346bfc6f/static_rps

First, I define Rock-paper-scissors sort with emulate bool.

https://github.com/jats-ug/practice-ats/blob/ce6d2001867fa4a9db6c3dc9fb2044d5346bfc6f/static_rps/rps.sats
datasort rps = (* abstract *) 

stacst r_rps: rps (* Rock *) 
and    p_rps: rps (* Paper *) 
and    s_rps: rps (* Scissors *) 

abst@ype rps (rps) = int 
typedef rps = [x:rps] rps (x) 

val r_rps: rps (r_rps) = "mac#" 
val p_rps: rps (p_rps) = "mac#" 
val s_rps: rps (s_rps) = "mac#" 

%{ 
#define r_rps 0 
#define p_rps 1 
#define s_rps 2 
%} 
And try to define print function on rps.

https://github.com/jats-ug/practice-ats/blob/ce6d2001867fa4a9db6c3dc9fb2044d5346bfc6f/static_rps/rps.dats
implement{} 
print_rps (x) = let val s = case x of 
  | r_rps => "Rock" 
  | p_rps => "Paper" 
  | s_rps => "Scissors" 
in 
  print_string s 
end 
However the compiler can’t identify the rps value.
$ patscc main.dats -DATS_MEMALLOC_LIBC 
/home/kiwamu/src/practice-ats/static_rps/rps.dats: 95(line=6, offs=5) 
-- 111(line=6, offs=21): error(3): this pattern match clause is 
redundant. 
/home/kiwamu/src/practice-ats/static_rps/rps.dats: 116(line=7, offs=5) 
-- 135(line=7, offs=24): error(3): this pattern match clause is 
redundant. 
How to identify dynamic value such like bool?

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

john_skaller · October 24, 2015, 6:58pm

Correct.

You can use ‘_ when …’ instead:

For that I use another shorthand:

| (A, $constant) => …

translates to

| (A, synthvar) when synthvar == constant => …

—
john skaller
ska...@users.sourceforge.net
http://felix-lang.org

gmhwxi · October 24, 2015, 1:36pm

You can. You just cannot use them (r_rps, p_rps, s_rps)
as patterns. Note that ‘true’ and ‘false’ are treated specially when
used as patterns.On Saturday, October 24, 2015 at 9:32:32 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Sat, Oct 24, 2015 at 10:22 PM, Kiwamu Okabe <kiw…@debian.or.jp <javascript:>> wrote:

‘true’ and ‘false’ are pre-defined constants?
I can’t find the definition in prelude?

Following is the definition of true?

https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_dyn.sats#L59

Why my following code can’t define the constants of rps?

https://github.com/jats-ug/practice-ats/blob/ce6d2001867fa4a9db6c3dc9fb2044d5346bfc6f/static_rps/rps.sats#L10

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

gmhwxi · October 24, 2015, 1:50pm

Correct.

You can use ‘_ when …’ instead:

https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST20/test21.datsOn Saturday, October 24, 2015 at 9:40:34 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Sat, Oct 24, 2015 at 10:36 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

You can. You just cannot use them (r_rps, p_rps, s_rps)
as patterns. Note that ‘true’ and ‘false’ are treated specially when
used as patterns.

Hmm…

I can define constructors of rps.
I can use the constructors as patterns.
I can define constants of rps.
I can’t use the constants as patterns.

Correct?

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

gmhwxi · October 24, 2015, 1:07pm

‘true’ and ‘false’ are constants. They are treated specially when
used as patterns.On Saturday, October 24, 2015 at 8:58:22 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Sat, Oct 24, 2015 at 9:34 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

r_rps is not a constructor and thus cannot be used as a pattern
(the compiler treats it as a variable that matches any value)

Try:

datatype rps(rps) = r_rps(r_rps) | p_rps(p_rps) | s_rps(s_rps)

Then you can use r_rps() as a pattern.

Fixed my code.

Hongwei feedback · jats-ug/practice-ats@c2b7d57 · GitHub

Where is the constructor of true and false?

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

gmhwxi · October 25, 2015, 1:44am

The special treatment is kind of a vestige.
One can now implement bool as a datatype
while keeping the keywords ‘true’ and ‘false’
compatible with the 1/0 interpretation:

(* ****** ****** *)
//
// False is ahead of True because
// of the need to map False to 0 and True to 1
/
datatype
bool(bool) =
| False(false) | True(true)
typedef bool = [b:bool] bool(b)

(* ****** ****** *)

#define true True()
#define false False()

(* ****** ****** *)
//
fun
print_bool
(x: bool): void =
case+ x of
| true => print “true”
| false => print “false”
//

(* ****** ****** *)On Saturday, October 24, 2015 at 2:54:37 PM UTC-4, John Skaller wrote:

On 25 Oct 2015, at 00:07, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

‘true’ and ‘false’ are constants. They are treated specially when
used as patterns.

That’s naughty! Here’s what I did:
Felix originally copied Ocaml in having constant (no argument)
constructors. However I hate Camelcase. So I made the user do this:
| Fred ?argument => … 
| Joe => … 
This is ugly, having to put ? before variables.
So I changed it. I copied ATS No constant constructors:
 | Fred argument => … 
 | Joe () => … 
Felix always had an abbreviation in expressions:
 #f ==> f () 
Its a shorthand which is very useful because in Felix type classes
you cannot have constants, only functions. So you have to do
    #zero[double] 
for example, for the real number class zero, instance double.
Hence:
 match .. with 
 | #True => … 
 | #False => … 
In fact the parser translates true and false, they’re treated “special”
in the parser NOT in pattern matches. Having special things in core
parts of the compiler add complexity.
—
john skaller
ska...@users.sourceforge.net <javascript:>
http://felix-lang.org

Topic		Replies	Views
Rock-paper-scissors library to learn statics and proofs on ATS language Google Group	4	415	November 1, 2015
Unpacking a value of existential type Google Group	0	291	November 23, 2013
Obtaining the type of a dynamic constant Google Group	1	394	November 9, 2015
Dynamic checking Google Group	0	272	January 19, 2014
Pattern matching compile failure Google Group	3	492	September 27, 2015

How to identify dynamic value such like bool?

Thank’s,

Thank’s,

Thank’s,

Thank’s,

Thank’s,

Thank’s,

Related Topics