K-user mailing list

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

Hi again,

Here is an update: Using the information you guys kindly gave me over
other threads, I came up with the following code:

  rule <k> X:#Id => Z ... </k> <heap> GPlus:Map => DMinus[Z/X] </heap>
       (<k> GPlus(X) </k> <heap> GPlus[undef/X] </heap> => <k> Z:Val
</k> <heap> DMinus:Map </heap>)

which unfortunately doesn't work either. Here is the frightening and
cryptic error message I get:

Advisory: could not find an operator R`{_`,_`,_`} with appropriate
domain in meta-module COMPILE-LOOP when trying to interprete metaterm
'R`{_`,_`,_`}['_`[_`][''__.Sort,'_`,_['_`[_`][''_=>_.Sort,'_`,_['_`[_`][''__.Sort,'_`,_['_`[_`][''<_>_</_>.Sort,'_`,_[''k.CellLabel.Constant,'_`[_`][''_`(_`).Sort,'_`,_[''GPlus:Map.Variable,'_`[_`][''_`(_`).Sort,'_`,_['_`[_`][''#_.Sort,''X:#Id.Variable],''.List`{K`}.List`{K`}.Constant]]]],''k.CellLabel.Constant]],'_`[_`][''<_>_</_>.Sort,'_`,_[''heap.CellLabel.Constant,'_`[_`][''_`[undef/_`].Qid,'_`,_[''GPlus:Map.Variable,'_`[_`][''_`(_`).Sort,'_`,_['_`[_`][''#_.Sort,''X:#Id.Variable],''.List`{K`}.List`{K`}.Constant]]]],''heap.CellLabel.Constant]]]],'_`[_`][''__.Sort,'_`,_['_`[_`][''<_>_</_>.Sort,'_`,_[''k.CellLabel.Constant,''Z:KItem.Variable,''k.CellLabel.Constant]],'_`[_`][''<_>_</_>.Sort,'_`,_[''heap.CellLabel.Constant,''DMinus:Map.Variable,''heap.CellLabel.Constant]]]]]],'_`[_`][''<_>_...</_>.Constant,'_`,_[''k.CellLabel.Constant,'_`[_`][''_=>_.Sort,'_`,_['_`[_`][''_`(_`).Sort,'_`,_['_`[_`][''#_.Sort,''X:#Id.Variable],''.List`{K`}.List`{K`}.Constant]],''Z:KItem.Variable]],''k.CellLabel.Constant]],'_`[_`][''<_>_</_>.Sort,'_`,_[''heap.CellLabel.Constant,'_`[_`][''_=>_.Sort,'_`,_[''GPlus:Map.Variable,'_`[_`][''_`[_/_`].Qid,'_`,_[''DMinus:Map.Variable,''Z:KItem.Variable,'_`[_`][''_`(_`).Sort,'_`,_['_`[_`][''#_.Sort,''X:#Id.Variable],''.List`{K`}.List`{K`}.Constant]]]]]],''heap.CellLabel.Constant]]]],'_`[_`][''_`(_`).Sort,'_`,_[''isVal.KLabel.Constant,''Z:KItem.Variable]],'klocation['"/home/hossein/Documents/KFram/Teachup/Launchbury/launchbury.k:34-35".String]].

And, in case you had difficulties finding the Ott rule I'm after
K'ification of, here it is:

  G : e --> D : z
  ------------------------------------------- :: var
  ( G , x |-> e ) : x --> ( D , x |-> z ) : z

Any idea now?

TIA,
--Hossein

P.S. As a heavy C++ metaprogrammer, for once when I saw the above
error message, I said to myself: Wow! So, there are tougher guys in
this world than C++? ;)

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



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

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/
--------------------------------------------------------------------------------------------------------------