pb with the Typol typechecker/Metal

[blazy@rubis.iie.cnam.fr (Sandrine BLAZY)]

Hi,
I have written a very simple Typol program :

program PROG is
use LG;
export |- FILE-> FILE' as PROG(FILE) = (FILE');
judgement |- FILE -> FILE  ;

INSTR ( |- Li -> Li')
----------------------------------------------------------------------
|- file[unit(H, LS, Li)] -> file[unit(H, LS, Li')];

set INSTR
judgement |- STMT -> STMT;
|- I -> I'
--------------------------------------------------
|- l_stat[I] -> l_stat[I'] ;

|- I -> I' &  |- Queue -> Queue'
----------------------------------------------------------------
|- l_stat[I.Queue] -> l_stat[I'.Queue'] ;

|- ass(name X, E) -> l_stat[] ;

|- struct_if(E, Li1, Li2) -> l_stat[Li1] ;
end INSTR;
end PROG;

>> When I typecheck it, I get the following messages in the Centaur messages 
window:

Info: prolog ( 1 ): type error in arg(1, user, term) 
Info: prolog ( 1 ): out of range in seek(toplevel_input, 228864) 
Info: prolog ( 1 ): out of range in seek(toplevel_input, 228864) 

Info: prolog ( 1 ): Fatal Error: problems with a formalism: $LG$real_cst
(string, LG, real_cst). 
Info: prolog ( 1 ): Aborting execution ... 
Info: prolog ( 1 ): Fatal Error: problems with a formalism: $LG$double_cst
(string, LG, double_cst). 
Info: prolog ( 1 ): Aborting execution ... 
Info: prolog ( 1 ): Fatal Error: problems with a formalism: $LG$logic_cst
(string, LG, logic_cst). 
Info: prolog ( 1 ): Aborting execution ... 
Info: prolog ( 1 ): Fatal Error: problems with a formalism: $LG$integer
(0, LG, integer). 
Info: prolog ( 1 ): Aborting execution ... 
Info: prolog ( 1 ): Fatal Error: problems with a formalism: $LG$real
(0, LG, real). 
Info: prolog ( 1 ): Aborting execution ... 
Info: prolog ( 1 ): yes. 
Info: prolog ( 1 ):     /home/local/centaur2/centaur/tables/typol/semantics/TY_N
TEST.sp 
Info: prolog ( 1 ): 
calling an undefined procedure /home/local/centaur2/centaur/tables/typol/seman
tics/TY_NTEST.sp / 0 in module eclipse 
Info: prolog ( 1 ): no (more) solution. 

>> The $LG$xxxxx are all the LG tokens that I have defined in the LG.metal file 
(their abstract syntax rules are xxxxxx -> implemented as ...).

>> I also have the following messages in the "errors on prog.ty" window:


Error: The type FILE is ambiguous (LG::FILE , LG::FILE).
Error: The type STMT is ambiguous (LG::STMT , LG::STMT).

I don't understand all these messages.
Does anyone could tell me why the Typol typechecker cheks for tokens I
haven't used 
in the Typol program?

Thanks for helping!

Sandrine Blazy
------------------------------------------------------
IIE-CNAM
18 allée Jean Rostand         ph.: +33 (1) 69 36 73 83
91 025 Evry cedex             fax: +33 (1) 69 36 73 05
France                        email: blazy@iie.cnam.fr
http://web.iie.cnam.fr/~blazy/home.html