K-user mailing list

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

Hi there,

My message below is waiting for approval because it's larger than
128K. This is due to its PDF attachment. In case you know Ott, please
see the Ott source in the attachments instead. Hopefully, it won't be
a lot of hassle to read through the Ott source for it's aimed to be a
close ASCII transliteration of the operational semantics. I would
appreciate it if you could help me.

TIA,
--Hossein

On 23 February 2012 13:25, Seyed H. HAERI (Hossein)
<hossein.haeri AT gmail.com>
 wrote:
> 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/
> --------------------------------------------------------------------------------------------------------------



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

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.ott
Description: application/vnd.oasis.opendocument.text-template