K-user mailing list

[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

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
>