K-user mailing list

[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