Skip to Content.
Sympa Menu

k-user - Re: [K-user] Ocaml and LLVM definitions are now available under kframework

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [K-user] Ocaml and LLVM definitions are now available under kframework


Chronological Thread 
  • From: "Rosu, Grigore" <grosu AT illinois.edu>
  • To: Andrei Stefanescu <andreistef AT gmail.com>, Ömer Sinan Ağacan <omeragacan AT gmail.com>
  • Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
  • Subject: Re: [K-user] Ocaml and LLVM definitions are now available under kframework
  • Date: Thu, 12 Sep 2013 22:08:17 +0000
  • Accept-language: en-US
  • List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
  • List-id: <k-user.cs.uiuc.edu>

superheat is still working.  Not needed for execution, but needed for search.  So for the beginning you can comment the superheat attributes out and focus on execution, but eventually we'll have to reconsider them.

 

Grigore
 
 

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Andrei Stefanescu [andreistef AT gmail.com]
Sent: Thursday, September 12, 2013 4:30 PM
To: Ömer Sinan Ağacan
Cc: k-user AT cs.uiuc.edu
Subject: Re: [K-user] Ocaml and LLVM definitions are now available under kframework

* I think that hybrid is deprecated (lists are automatically hybrid), but I don't know about superheat...
* define is deprecated; make sure the operator being defined has the "[function]" attribute, and use rule instead
* List{K} has been replaced by KList.

Hope this helps,

Andrei



On Thu, Sep 12, 2013 at 3:32 PM, Ömer Sinan Ağacan <omeragacan AT gmail.com> wrote:
They don't work under latest version, I tried to fix some syntactic
problems but there are other kinds of problems too.

What I fixed but still couldn't run it:

  * `module Name is Contents end module` syntax is changed to `module
Name Contents endmodule`

  * superheat and hybrid keywords are apparently removed (are those
unnecessary now? or simply replaced by something else?)

  * ` character before terminals doesn't work

  * define keyword is also removed

  * List{K} syntax doesn't work (I think the problem is that we now
have to specify the separator, in that case what separator should I
add to make it work with no other changes?)


---
Ömer Sinan Ağacan
http://osa1.net


2013/9/10 Dorel Lucanu <dlucanu AT info.uaic.ro>:
> Congratulations!
> Ocaml definition is a surprise for me, I knew that you are developing the
> Haskel definition.
> But, of course, they have lot in common ...
> Dorel
>
>
> On 9/10/13 7:17 PM, David Lazar wrote:
>>
>> Hello K users,
>>
>> The OCaml definition and LLVM definition I co-developed with Chucky
>> Ellison are now available under the kframework Github project:
>>
>> https://github.com/kframework/ocaml-semantics
>>
>> https://github.com/kframework/llvm-semantics
>>
>> There are publications lurking in both of these projects but I don't
>> have time to take the lead on them. If you want to take the lead, let
>> me know and I can help you get started.
>>
>> Cheers,
>> David
>> _______________________________________________
>> k-user mailing list
>> k-user AT cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>
>
> _______________________________________________
> k-user mailing list
> k-user AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/k-user

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user




Archive powered by MHonArc 2.6.16.

Top of Page