K-user mailing list

[Traian Florin Șerbănuță <traian.serbanuta AT info.uaic.ro>]

Hi Ömer,

This indeed was a tricky and rare issue.  

Shortly, the reason it is failing is because of the side effects introduced by the overloading of the application operator: The IdList syntax declaration generates a constructor which in the internal AST representation looks identical to the one generated by the application constructor.  

Explanation: this overloading creates (undesired) confusion at the level of the execution engine between function applications and lists. This is further complicated by the fact that a list is considered a value when all its elements are values which leads to the behavior you have experienced.  This danger of confusion is why overloading of operators is not  supported by K (although it is sometimes used in definitions)

Solution for you:  One way to distinguish the two constructors in the internal representation would be to change the klabel used for the application, adding something like klabel(apply) to the list of tags:

               | Exp Exp                                [left, strict, klabel(apply)]

Solution for us:  We should probably issue hard warnings when user overload operation, especially on incompatible types.

Thanks again for reporting and sorry for the trouble with it.

best wishes,

Traiann Serbanuta

2013/8/20 Ömer Sinan Ağacan <omeragacan AT gmail.com>

Hi all,

I'm already frustrated by debugging my K programs. Is there a way to
see why a rule doesn't apply? It would be great if there was an option
in debugger that tries to apply a rule(for instance, with "apply
rule123" command), and if it fails prints an explanation of the reason
why it doesn't apply.


My K file is this:


module STAGED-SYNTAX

  syntax IdList ::= List{Id, " "}

  syntax Exp ::= Id
               | Int
               | "(" Exp ")"                            [bracket]
               | Exp Exp                                [left, strict]
               > Exp "+" Exp                            [left, strict]
               > "fun" Id "->" Exp

  syntax Val ::= Int | closure(Map, Id, Exp)

  syntax Exp ::= Val

endmodule

module STAGED
  imports STAGED-SYNTAX

  configuration
    <k> $PGM:Exp </k>
    <env> .Map </env>

  syntax KResult ::= Val

  rule <k> fun I -> E => closure(Env, I, E) ... </k>
       <env> Env </env>                                 [lambda]

  rule <k> I:Id => V ... </k>
       <env> ... I |-> V:Val ... </env>                 [lookup1]

  syntax K ::= env(Map)

  rule <k> closure(Closure, ArgId, Body) Arg:Val => Body ~> env(OldEnv) ... </k>
       <env> OldEnv => OldEnv[Arg/ArgId] </env>         [application]

  rule <k> V:Val ~> env(M) => V ... </k>
       <env> _ => M </env>                              [restore-env]

  rule <k> I1:Int + I2:Int => I1 +Int I2 ... </k>       [addition]

endmodule

Now this _expression_ works fine: (fun n -> n) (fun n -> n) -- which
ends with <k> closure ( .Map , n , n ) </k>

but this fails: (fun n -> n) (fun n -> n) (fun n -> n) -- ends with
((closure ( .Map , n , n )) (closure ( .Map , n , n ))) (closure (
.Map , n , n )) .

Why application rule doesn't apply here? Can anyone help me with this?

Thanks,


---
Ömer Sinan Ağacan
http://osa1.net

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user