K-user mailing list

["Seyed H. HAERI (Hossein)" <hossein.haeri AT gmail.com>]

Hi again,

OK, now I'm stuck for the same basic reason, on a more complicated
example. See the attached PDF for Ott's output of the famous
(big-step) operational semantics of Launchbury for lazy evaluation.
Here is my attempt to model that so far:

require /modules/substitution

module LAUNCHBURY-SYNTAX
  syntax Val ::= "\\" #Id "." Exp [binder prec 100 latex "\lambda{#1}.{#2}"]

  syntax Binding ::= #Id "=" Exp
  syntax Bindings ::= List{Binding, ","}

  syntax Exp ::= #Id
              | Val
              | Exp #Id [strict(1) gather (E e)]
              | "let" Bindings "in" Exp
end module

module LAUNCHBURY imports LAUNCHBURY-SYNTAX + SUBSTITUTION

  syntax KResult ::= Val

  configuration <k color = "green" multiplicity = "*"> $PGM:K </k>
<heap> .Map </heap>

  rule <k> (\ Y:#Id.E':Exp) X:#Id => E'[X/Y] ... </k>
  rule <k> X:#Id => Z:Val ... </k> <heap> ... X |-> (_ => Z) ... </heap>
end module

My very last rule above is my first unsuccessful attempt to model the
Var rule of the attached PDF. Upon kompilation of the above file,
Maude expresses its unhappiness about Z being used before being
introduced first. Whilst I think Maude is right, I don't seem to be
able to figure out how to tell K that: Z is what we get once we try
the evaluation of what X was bound to in the original heap with X's
binding removed. Here is another failed attempt:

  rule <k> X:#Id ... </k> <heap> ... X |-> E:Exp ... </heap> => <k> Z
... </k> <heap> D[X |-> Z] </heap>
       (<k> E ... </k> <heap> ... X |-> . ... </heap> => <k> Z:Val ...
</k> <heap> D:Map </heap>)

This one fails with an error message that I can't decrypt:

[ERROR]: Default terms accept open cells only for Bag cells.
 Term: <_>_</_>(heap,(.).Map,heap)
 Context:  -> __ -> _=>_ -> __ -> _=>_
Location:
/home/hossein/Documents/KFram/Teachup/Launchbury/launchbury.k:23-24
 Compilation phase: DEFAULT-TERMS
Aborting the compilation

So, how do you guys do that? And, moreover, what's the story about
"default terms" and "Bag cells" here?

TIA,
--Hossein

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

Seyed H. HAERI (Hossein)

Research Assistant
Institute for Software Systems (STS)
Technical University of Hamburg (TUHH)
Hamburg, Germany

ACCU - Professionalism in programming - http://www.accu.org/
--------------------------------------------------------------------------------------------------------------

Attachment: Launchbury.pdf
Description: Adobe PDF document