Re: question

[td@trinidad.inria.fr (Thierry Despeyroux)]

In article <556@sophia.inria.fr>, rl@cs.unh.edu (Rongliang Li) writes:
=> Hi, here are some errors reported by TYPOL type-checking, I hope someone can
=> tell me why the incompatible types happened.
=> 	Error: The variable V is used with incompatible types (string, SMALL::IDENT).
=> 	Error: The variable N is used with incompatible types (string, SMALL::VALUE).
=> 
=> the errors came from the following typol rule:
=> 	judgement	PAIR_S |- I, BOOL , B : PAIR_S ;
=> 	pair_s[] |- ident V, false, num N: pair_s[pair(V, false, N)] ;
=> 
=> the corresponding parts of those in METAL file are:
=> 	pair_s  -> PAIR * ... ;
=>         pair    -> IDENT  BOOL VALUE ;
=> 
=>         PAIRS   ::= pair_s ;
=>         PAIR    ::= pair ;
=>         VALUE   ::= num true false d_fun d_proc ;
=> 
=>         <ident> ::= %ID ;
=>                 ident-atom(%ID)
=>         <num>   ::= %INT ;
=>                 num-atom(%INT)
=> 
=> 	ident   -> implemented as IDENTIFIER;
=>         num     -> implemented as STRING;
=> 
=> 	IDENT ::= ident;
=>         B ::= num;





Let's describe the abstract syntax in another way, and I hope
it will become clear:

pair  : IDENT x BOOL x VALUE  -> PAIR ;
ident : string -> IDENT ;
num   : string -> VALUE ;

In pair(V, B, N), V has type IDENT, N has type VALUE, and the all
expression is of type PAIR.

In ident V, V (the value of the atom) is of type string, and the all
expression is of type IDENT.

The same applies to num.

So the correct rule is

pair_s[] |- ident V, false, num N: pair_s[pair(ident V, false, num N)] ;

In fact, due to the judgement you have given, as the phylum IDENT
contains only one operator (ident), and the phylum B contains also one
operator (num) you may write:

judgement	PAIR_S |- I, BOOL , B : PAIR_S ;
pair_s[] |- V, false, N: pair_s[pair(V, false, N)] ;


Warning! In this rule, false is a variable. I think it may be an error,
since false may be an operator with arity 0. In this case you should
write false().



Thierry Despeyroux.