Problems with TYPOL

[jperez@lsi.upc.es (Javier Perez)]

Hello

We are using TYPOL to implement a complex type checker. For us is unavoidable 
to have some kind of negation in order to save hundreds of lines of code.

Recently we have built an strategy to simulate negation taking advantadge of
the recovery rules. To make a predicate and its negation we make a predicate
that always succeeds and returns a value . If the predicate applies we
make the predicate return a 1, and if not a 0.

To do this we implement predicate with the same rules that would have normally,
and in these rules we return a one, then we put a recovery rule (the most 
general rule) that returns a 0. I have enclosed an example that will
show this more clearly.

The problem is that under certain circumstances this doesn't work, sometimes
the program stops in the half of the execution as if it would have finished
normally.

I have make a little test in which you can see this:

This is a little language to represent sets of integers:

---------------------- file test.metal ----------------------------------------

-- Test for the recovery rules.

definition of test is

   chapter LANGUAGE

   rules

   <axiom> ::= <set> ;
       <set>

   <set> ::= "[" "]" ;
       set_i-list(())
  
   <set> ::= "[" <int_nelist> "]" ;
       <int_nelist>

   <int_nelist> ::= <int> ;
       set_i-list((<int>))

   <int_nelist> ::= <int> "," <int_nelist> ;
       set_i-pre(<int>, <int_nelist>)

   <int> ::=%Integer ;
       int-atom(%Integer)

   abstract syntax

   set_i -> INT * ... ;
   int -> implemented as INTEGER;

   SET ::= set_i;
   INT ::= int;

   end chapter;

end definition

-----------------------------------------------------------------------------

This is the TYPOL rules that implement an equal operation on these sets, and
some simple tests:


------------------------ file testrec.ty ------------------------------------

program testrec is

use test;

-- Test for recovery rules.

import diff(_,_) from prolog;

export test_recovery(|- T : T2) as testrec(T) = T2;

set test_recovery is

judgement |- test : test;

equal_sets(|- set_i[int 4, int 5], set_i[int 5, int 4] : R1) &
equal_sets(|- set_i[int 4], set_i[int 5, int 4] : R2) &
equal_sets(|- set_i[int 4, int 5], set_i[int 5] : R3)
---------------
|- GLI : GLI;

end test_recovery;


set equal_sets is

judgement |- SET, SET : INT;

-- Returns 1 if both sets contain the same elements and 0 if not. 

includes_set(|- SET, SET2 : int 1) &
includes_set(|- SET2, SET : int 1)
----------------------------
|- SET, SET2 : int 1;

recovery 

|- X, Y : int 0;

end equal_sets;


set includes_set is

judgement |- SET, SET : INT;

-- Returns 1 if the first set is included by the second and 0 if not.

|- set_i[], SET2 : int 1;

belongs_set(|- ELT, SET2 : int 1) &
|- ELTR, SET2 : int 1
-------------------
|- set_i[ELT . ELTR], SET2 : int 1;

recovery 

|- X, Y : int 0;

end includes_set;


set belongs_set is

judgement |- INT, SET : INT;

-- Returns 1 if the element belongs to the set and 0 if not.

|-  ELT, set_i[ELT . ELTR] : int 1;

diff(ELT, ELT2) &
|- ELT, ELTR : int 1
---------------------
|- ELT, set_i[ELT2 . ELTR] : int 1;

recovery 

|- X, Y : int 0;

end belongs_set;

end testrec;


-----------------------------------------------------------------------

When we execute this example, the program stops in the second call to the
equal_sets predicate concretely: equal_sets(|- set_i[int 4], set_i[int 5, int 4
] : R2) . The program performs correctly the first call to includes_set,
the second call is executed and it fails, but before the program returns to 
the rule of the predicate equal_sets, the program ends.

However if we make a slight change to the equal_sets predicate:


set equal_sets is

judgement |- SET, SET : INT;

-- Returns 1 if both sets contain the same elements and 0 if not. 

includes_set(|- SET, SET2 : int 1) &
includes_set(|- SET2, SET : RES)
----------------------------
|- SET, SET2 : RES;

recovery 

|- X, Y : int 0;

end equal_sets;


Then the program runs correctly. Unfortunately we have found more complicate
situations where making this change is not possible, so it is not a valid
solution to perform just this change.

We don't know if this is a TYPOL bug, or if we are not using properly the
recovery rules.

Javier
 Perez