K-user mailing list

[Stephen Chang <stchang AT ccs.neu.edu>]

2011/11/16 Traian Florin Șerbănuță 
<tserban2 AT illinois.edu>:
> Hi Stephen,
>
> Sorry abut that;  the agent definition on K seems outdated.  please
> update using either svn up  in the trunk or alternatively run the
> ./k-update script

Thanks, it seems to be working now! I think I asked this already, but
how does one see the result of running a program? All the programs
seem to be generating the same output (see below). Also, is there a
way to view/log each rewrite step?


<T>
  <barrier>
    true
  </barrier>
  <nextAgent>
    1
  </nextAgent>
  <IO>
    <in>
      .
    </in>
    <out>
      .
    </out>
  </IO>
  <messages>
    .
  </messages>
  <waiting>
    .
  </waiting>
  <world>
    .
  </world>
</T>











>
> best wishes,
> - traian
>
>
>
>
> 2011/11/16 Stephen Chang 
> <stchang AT ccs.neu.edu>:
>> Running on the virtual machine now :)
>>
>> Trying to run a program with the agent example language, but still
>> getting some errors. Adding --search doesn't seem to help either. Any
>> ideas?
>>
>>
>> k@KVM:~/k-shared/k-examples/languages/research/agent$
>>  krun programs/p1
>> Warning: kast reported errors or warnings:
>> Warning: "programCompile.maude", line 3 (mod
>> TEST-DO-NOT-USE-THIS-NAME): module AGENT-SYNTAX does not exist.
>> Warning: "programCompile.maude", line 9: bad token +.
>> Warning: "programCompile.maude", line 9: no parse for term.
>> Can't call method "getChildNodes" on an undefined value at
>> /home/k/k-framework/core/perl/ast.pl line 23.
>>
>> Error:
>> Fatal: kast returned a non-zero exit code: ExitFailure 9
>> Attempted command:
>> kast --k-definition ./agent --main-module AGENT --syntax-module
>> AGENT-SYNTAX 
>> /home/k/k-shared/k-examples/languages/research/agent/.k/krun_tmp/pgm1890.in
>>
>> k@KVM:~/k-shared/k-examples/languages/research/agent$
>>  krun --search programs/p1
>> Warning: kast reported errors or warnings:
>> Warning: "programCompile.maude", line 3 (mod
>> TEST-DO-NOT-USE-THIS-NAME): module AGENT-SYNTAX does not exist.
>> Warning: "programCompile.maude", line 9: bad token +.
>> Warning: "programCompile.maude", line 9: no parse for term.
>> Can't call method "getChildNodes" on an undefined value at
>> /home/k/k-framework/core/perl/ast.pl line 23.
>>
>> Error:
>> Fatal: kast returned a non-zero exit code: ExitFailure 9
>> Attempted command:
>> kast --k-definition ./agent --main-module AGENT --syntax-module
>> AGENT-SYNTAX 
>> /home/k/k-shared/k-examples/languages/research/agent/.k/krun_tmp/pgm1894.in
>>
>>
>>
>>
>>
>> On Tue, Nov 15, 2011 at 6:22 PM, Rosu, Grigore 
>> <grosu AT illinois.edu>
>>  wrote:
>>> We have in plan to incorporate in the tool a generic means to generate 
>>> fresh
>>> names that will automatically add the nextid cell for you.  Unfortunately,
>>> for the time being it needs to be added manually.
>>>
>>> Grigore
>>>
>>> -----Original message-----
>>>
>>> From: Chucky Ellison 
>>> <celliso2 AT illinois.edu>
>>> To: Stephen Chang 
>>> <stchang AT ccs.neu.edu>
>>> Cc: 
>>> "k-user AT cs.uiuc.edu"
>>>  
>>> <k-user AT cs.uiuc.edu>
>>> Sent: Tue, Nov 15, 2011 23:12:56 GMT+00:00
>>> Subject: Re: [K-user] untyped lambda calculi examples missing?
>>>
>>> It's a little weird why you need to do this, but it will work if you say:
>>> configuration  <T> <k>$PGM:K</k> <nextId> 0 </nextId> </T>
>>>
>>> The nextId cell is needed for the generic substitution.
>>>
>>> On Tue, Nov 15, 2011 at 4:02 PM, Stephen Chang 
>>> <stchang AT ccs.neu.edu>
>>>  wrote:
>>>> Thank you very much for the pointers everyone. I appreciate all the
>>>> assistance I've received from this list. I'm sorry to be so slow to
>>>> figure things out.
>>>>
>>>>
>>>> So it seems like this should be sufficient to get a call-by-value
>>>> lambda calculus:
>>>>
>>>>
>>>> (in file cbv.k)
>>>>
>>>> require /modules/lambda
>>>>
>>>> module CBV imports LAMBDA
>>>>
>>>>  configuration  <T> <k>$PGM:K</k> </T>
>>>>
>>>> end module
>>>>
>>>>
>>>>
>>>>
>>>> but when I try to compile, I get this error:
>>>>
>>>> stchang@caprica:~/NEU_Research/betaneed/K$
>>>>  kompile cbv.k
>>>> [ERROR] Error: /home/stchang/k-framework/modules/substitution.k:25-28
>>>> Compilation phase: CONTEXT-TRANSFORMERS Reason: Cell nextId is not at
>>>> the right level in the configuration. Check the initial configuration
>>>> for the definition matches the rule.  Trm:
>>>>
>>>> <_>_</_>(nextId,_=>_(_`(_`)(#_(N:#Nat),.List`{K`}),_`(_`)(#_(sNat_(N:#Nat)),.List`{K`})),nextId)
>>>>        Context:
>>>>
>>>> __(<_>_...</_>(k,_=>_(_`(_`)(beta`[_/_`](K:K,Y:#Id),_`(_`)('`[_`]_,_`,`,_(_`(_`)(#_(X:#Id),.List`{K`}),K':K))),_`(_`)(visitedL`(_`)('`[_`]_),_`(_`)('_visitedL`(`,`,`)_,_`,`,_(_`(_`)('visitedK_,_`(_`)(kList("wklist_"),_`(_`)(#_(id_(N:#Nat)),.List`{K`}))),_`(_`)('eval_`,then`apply`[_/_`],_`,`,_(_`(_`)('beta_`[_/_`],_`,`,_(K':K,_`,`,_(_`(_`)(#_(id_(N:#Nat)),.List`{K`}),_`(_`)(#_(X:#Id),.List`{K`})))),_`,`,_(K:K,_`(_`)(#_(Y:#Id),.List`{K`})))))))),k),<_>_</_>(nextId,_=>_(_`(_`)(#_(N:#Nat),.List`{K`}),_`(_`)(#_(sNat_(N:#Nat)),.List`{K`})),nextId))
>>>> Check .k/kompile_errYT_kvKadNY.txt to find all errors.
>>>> Aborting the compilation
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> 2011/11/15 Traian Florin Șerbănuță 
>>>> <tserban2 AT illinois.edu>:
>>>>> I think Agent is updated to the last version, yes.
>>>>>
>>>>> Stephen, you can take a look at AGENT in
>>>>> examples/languages/research/agent
>>>>>
>>>>> Agent is built from small pieces, which are all under the `modules'
>>>>> directory from the trunk.  I think the lambda and mu modules can give
>>>>> you an idea about how we use substitution, but you can use AGENT as an
>>>>> example of a non-trivial substitution based language.
>>>>>
>>>>> best wishes,
>>>>> - traian
>>>>>
>>>>>
>>>>> 2011/11/15 Rosu, Grigore 
>>>>> <grosu AT illinois.edu>:
>>>>>>
>>>>>> You can also take a look at Agent.  Traian, is Agent updated to the
>>>>>> latest
>>>>>> version of the tool?
>>>>>>
>>>>>> Grigore
>>>>>>
>>>>>> -----Original message-----
>>>>>>
>>>>>> From: Stephen Chang 
>>>>>> <stchang AT ccs.neu.edu>
>>>>>> To: "Lazar, David" 
>>>>>> <lazar6 AT illinois.edu>
>>>>>> Cc: 
>>>>>> "k-user AT cs.uiuc.edu"
>>>>>>  
>>>>>> <k-user AT cs.uiuc.edu>
>>>>>> Sent: Tue, Nov 15, 2011 20:53:37 GMT+00:00
>>>>>> Subject: Re: [K-user] untyped lambda calculi examples missing?
>>>>>>
>>>>>> On Tue, Nov 15, 2011 at 3:51 PM, David Lazar 
>>>>>> <lazar6 AT illinois.edu>
>>>>>> wrote:
>>>>>>> We provide substitution as a module you can just import, so you don't
>>>>>>> need to write all of those rules yourself. This module is located in
>>>>>>> modules/substitution.k.
>>>>>>>
>>>>>>> The simply-typed definition doesn't take advantage of this module
>>>>>>> (although it should).
>>>>>>>
>>>>>>> The lambda module (located in modules/lambda.k) does take advantage of
>>>>>>> the substitution module. You can copy the (fairly clear) code in
>>>>>>> modules/lambda.k to add lambda to your definition.
>>>>>>
>>>>>> Cool, thanks! I will check it out.
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>>
>>>>>>> Cheers,
>>>>>>> David
>>>>>>>
>>>>>>> On Tue, Nov 15, 2011 at 2:37 PM, Stephen Chang 
>>>>>>> <stchang AT ccs.neu.edu>
>>>>>>> wrote:
>>>>>>>> On Tue, Nov 15, 2011 at 3:22 PM, David Lazar 
>>>>>>>> <lazar6 AT illinois.edu>
>>>>>>>> wrote:
>>>>>>>>> Stephen,
>>>>>>>>>
>>>>>>>>> This is accidental. I think someone created the directory but forgot
>>>>>>>>> to add a definition :-).
>>>>>>>>>
>>>>>>>>> PCF is perhaps the closest thing we have to untyped lambda calculus.
>>>>>>>>> The PCF definition is located in
>>>>>>>>> examples/languages/classic/pcf/untyped. Note that this definition is
>>>>>>>>> environment-based. If you want to create a substitution-based
>>>>>>>>> definition, take a look at simply-typed lambda calculus and
>>>>>>>>> modules/lambda.k.
>>>>>>>>
>>>>>>>> I'm looking for a substitution-based definition. I looked at the
>>>>>>>> simply-typed example, but couldnt understand the substitution 
>>>>>>>> function
>>>>>>>> :)
>>>>>>>>
>>>>>>>> Is there any documentation that you recommend looking at? I've read
>>>>>>>> the JLAP paper and looked through Grigore's PL textbook draft but are
>>>>>>>> there any more-basic guides for just the tool itself?
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>>
>>>>>>>>> Hope this helps.
>>>>>>>>>
>>>>>>>>> Cheers,
>>>>>>>>> David
>>>>>>>>>
>>>>>>>>> On Tue, Nov 15, 2011 at 2:11 PM, Stephen Chang 
>>>>>>>>> <stchang AT ccs.neu.edu>
>>>>>>>>> wrote:
>>>>>>>>>> I noticed that the directory
>>>>>>>>>> examples/languages/classic/lambda/untyped
>>
>> _______________________________________________
>> k-user mailing list
>> k-user AT cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>>
>