K-user mailing list

[Ö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