lives-group / APEG

2 stars 0 forks source link

Type System Madness ! #36

Open emcardoso opened 2 years ago

emcardoso commented 2 years ago

In our previous meetings, we discuss a problem with the type system, basically, we thought that there was something weird was going on with the constraint solver. To better summarize the problem here is a simplified example:

apeg Dispair;

rule1 [language l] returns x:   { x = (| 1 |) ; } ;

rule2 [language l] returns y:  { y = `w` ; } ;

rule3 [language l] returns z: 
   rule1<l,p> /
   rule2<l,q>
   {z = {| #q |}; 
    w = (| #q |); }
;  

And here is the type system output for the example:

_0=metaExpr
_1=metaPeg
_0=_3
_1=_4
_2=metaExpr

------ Environment ----- 
 rule3 |->     sig: (language) -> (metaExpr:_2)
    locals: 
    ------ Environment ----- 
     w |-> metaExpr
     l |-> language
     q |-> metaPeg:_4
     p |-> metaExpr:_3
     z |-> metaExpr

 rule2 |->     sig: (language) -> (metaPeg:_1)
    locals: 
    ------ Environment ----- 
     l |-> language
     y |-> metaPeg

 rule1 |->     sig: (language) -> (metaExpr:_0)
    locals: 
    ------ Environment ----- 
     x |-> metaExpr
     l |-> language

The problem here is that in the body of rule3 z and w are mere unquote of variable q, whose type is metaPeg. However, z and w have a different type (both are metaExpr) than q.

Out of curiosity, I make the type system print the name of the class of inner node unquote and it is :

   ==================== The type of N inner node is ============================== 
              apeg.ast.expr.MetaAttribute

Which is, of course, of type metaExpr. Fixing the node construction should solve this and reveal more problems!

tassilucas commented 2 years ago

Hello Elton, thanks for the issue.

We fixed the problem in the last meeting by exiting the meta level in the following line:

unquote_expr returns[Unquote unq, SymInfo si]:
{metaLevel}? t='#' {exitMeta();} primary {enterMeta();}
{$unq = factory.newUnquoteExpr(new SymInfo($t.line, $t.pos), $primary.exp);
$si = new SymInfo($t.line $t.pos); };

And then, we executed the following apeg file:

apeg bug_example;

pterm[language g] returns y: literalPEG<g, ret> '*' { y = {| #ret* |}; };

literalPEG[language g] returns `s`: '\'' s=(a..z)+ '\'';

Obtaining the output:

_1=_2
_2=meta
_2=metaPeg
_0=_2
_1=metaPeg

------ Environment ----- 
 pterm |->     sig: (language) -> (meta:_0)
    locals: 
    ------ Environment ----- 
     ret |-> meta:_2
     g |-> language
     y |-> meta:_2

 literalPEG |->     sig: (language) -> (metaPeg:_1)
    locals: 
    ------ Environment ----- 
     s |-> string
     g |-> language

which has a constraint of type meta. By disabling VTyMeta constraint creation, we fixed this problem.

emcardoso commented 2 years ago

Nice observation and solution Lucas. Rethink a little better I conclude that disabling the meta constraint creating wasn´t a good idea! The problem with this approach is that we should check whenever an unquote operation really has some meta-type. To this end, I made some modifications to the Constraint Machine (CTM) and added a pertinence test. This new constraint is equivalent to having a variable restricted to some possibilities! Here is what the constraints now look like on your example:

_1=_2
_2 in { metaExpr, metaPeg, metaType} 
_2=metaPeg
_0=_2
_1=metaPeg

------ Environment ----- 
 pterm |->     sig: (language) -> (metaPeg:_0)
    locals: 
    ------ Environment ----- 
     ret |-> metaPeg:_2
     g |-> language
     y |-> metaPeg:_2

 literalPEG |->     sig: (language) -> (metaPeg:_1)
    locals: 
    ------ Environment ----- 
     s |-> string
     g |-> language

Note que varible _2 now has a new constraint : _2 in { metaExpr, metaPeg, metaType} which means _2 must be one of the enumerated types !

tassilucas commented 2 years ago

Hmm thats interesting, Elton. This approach should be better than avoiding VTyMeta constraints.

By the way, I pushed my last commit e67598f so feel free to push these new changes :)

Thanks.