K-user mailing list

[Andrew Cann <shum AT canndrew.org>]

Thank you! This information helps a lot, particularly the wiki (which I didn't
know existed). Most of the info on the module system page still seems beyond 
my
level though. I think a good place to start would be to learn KORE, that way I
can understand how K actually works, then I can start using it in a more
syntactic-sugary way once I'm familiar with the fundamentals. Does that make
sense?

 - Andrew

On Mon, Dec 11, 2017 at 03:00:17PM +0200, Radu Mereuta wrote:
> Hi Andrew,
> 
> Can you provide a bit more info about your usage? (K version to be more
> specific)
> I tried to kompile with K4.0, and it failed at the final two rules.
> After I commented those, it passed. Then I tried to parse a file from the
> github link you provided, but that failed also.
> 
> So I will try to answer in general to a few of your concerns regarding
> parsing:
> - parsing programs: you can use `kompile` then `kast` on a program to see
> the AST. If you have an infinite loop, this is where you will see the stack
> trace you mentioned. You can play with different stack sizes by changing
> the JVM initial parameters (see /bin directory).
> 
> - parsing rules: K uses this mix of K syntax and user syntax to allow
> programmers more options in defining the semantics in the style of that
> language. But as you found out, there are some limitations. You can't use
> `Id` because it conflicts with metavariables, you can't use `=>` because it
> conflicts with the rewrite arrow. But there are workarounds this. You can
> use more modules and separate the problematic productions.
> Take a look at these:
> 
> https://github.com/kframework/k/wiki/!!!-Module-System#example-using-different-syntax-for-parsing-and-semantics
> 
> https://github.com/kframework/k/wiki/Separate-modules-for-parsing-and-semantics
> This way, you can define the complete syntax of your language and the
> program parser will have no issues, but when writing rules, you have to use
> the labeled form of that production.
> 
> Regarding type annotations: there are a few, defined as follows:
> syntax S ::= S ":S"    // force the inner term to have the sort S; can only
> be placed in a context that accepts sort S - this works at the semantic
> level also because it forces metavariables to check the sort at runtime
> syntax S ::= S "::S"   // same as above, but no runtime checks - this is
> only used by the parser for syntax disambiguation
> syntax S ::= K ":>S"  // syntactic only again, but can accept any term and
> force it to fit in a place where S is expected
> syntax K ::= S "<:S"  // the reverse
> 
> If I remember correctly, you can use ":" (semicolon) in rules, as long as
> you separate it by spaces so it doesn't conflict with type annotations.
> 
> If you have any more parsing issues, I will be glad to help.
> 
> Radu Mereuta
> 
> 
> 
> 
> On Sun, Dec 10, 2017 at 12:05 PM, Andrew Cann 
> <shum AT canndrew.org>
>  wrote:
> 
> > Hello K people.
> >
> > First off, I'm very excited to learn that K is thing that exists! I've 
> > been
> > trying to write my own languages for years - with the dream of having
> > verified
> > formal semantics aswell - but I've always ended up overwhelmed by the
> > amount of
> > work involved in even doing something simple like writing a parser. So
> > thanks
> > for making a programming language for writing programming languages, it's
> > very
> > cool!
> >
> > That said, I'm having problems kompiling and krunning my first toy example
> > language. For reference, I've pasted what I've written so far at the
> > bottom of
> > this email (though I'm not expecting or asking anyone to read the whole
> > thing).
> > Some of my probkems are:
> >
> > # Parsing
> >
> > I think the parser is going into an infinite loop. If i comment-out all 
> > the
> > rules and just leave the syntax definitions then krun still hangs forever
> > on
> > any input I've tried. How can I prevent or debug this? Can I, for example,
> > set
> > a recursion limit on the parser and have it fail with a backtrace of rules
> > it's
> > attempting to match when the limit gets hit?
> >
> > # Rules
> >
> > When writing rules there doesn't seem to be any way to deliniate between
> > the
> > syntax of my language and the syntax of K itself. For example, I want
> > lambdas
> > in my language to be written `(x => expr)` where `x` is a variable bound 
> > in
> > `expr`.  But the `=>` symbol here conflicts with the `=>` symbol used to
> > define
> > rules. Someone on github suggested I define my syntax in a seperate module
> > to
> > my rules. And this worked - it allowed me to define my own syntax using
> > `=>` -
> > but I don't understand why it worked. I also don't understand how K can
> > tell
> > which `=>` I'm refering to or even if it always can - I think the problems
> > I'm
> > having compiling my last two rules might be to do with it getting confused
> > over
> > this.
> >
> > Another example: in one of my rules I have `{(X:Id = H:Pat):AssPat, ...`,
> > but I don't want the parenthesis here ->     ^~~~~~~~~~~~~^
> > to be treated as part of my language.
> > They're just there so that I can apply `:AssPat` to a group of syntax, I
> > still
> > want `{some_id = some_pat, ...` (without parenthesis) to be matched by 
> > this
> > rule. Will this work? Is there a way to make it work or otherwise not 
> > work?
> >
> > A third example: I want to write type annotations in my language as `x:
> > Type`.
> > This doesn't seem at all possible since colons are already used by K to
> > define
> > metavariables.
> >
> > So my question here is: is there some general way to solve these problems?
> > When
> > I write syntax declarations there's no ambiguity because the parts that
> > are my
> > language are enclosed in quotes. However I tried using quote in rule
> > declarations and it didn't work. Is there some alternate syntax for
> > defining
> > rules which uses quotes (or something equivalent)? If not there *really*
> > needs
> > to be since jumpling the language and meta-language syntax together like
> > this
> > seems completely nuts (or maybe I just fundamentally don't understand how 
> > K
> > works).
> >
> > Anyway, hopefully someone can explain some of this to me. I would 
> > extremely
> > grateful since K seens completely awesome if it can do what I want it to
> > do.
> >
> > Regards
> >  - Andrew
> >
> > PS. The language I'm trying to define is this:
> > https://github.com/canndrew/malk-doc
> >
> > My work-in-progress malk.k file is pasted below:
> >
> > require "substitution.k"
> >
> > module MALK-SYNTAX
> >     syntax Val
> >       ::= Id.
> >         | Pat "->" Expr
> >         | Pat "=>" Expr
> >         | "{" "}"
> >         | "{" StructExpr "}"
> >         | "#{" "}"
> >         | "#{" StructType "}"
> >         | Expr "==" Expr
> >         | Expr "#=" Expr
> >         | "Type"
> >
> >     syntax Expr
> >       ::= Val
> >         | Expr Expr       [left, strict]
> >         | "(" Expr ")"    [brackets]
> >         | Expr ":" Expr
> >
> >     syntax StructExpr
> >       ::= AssExpr
> >         | AssExpr ","
> >         | AssExpr "," StructExpr
> >         | "..." Expr
> >
> >     syntax AssExpr
> >       ::= Expr
> >         | Id "=" Expr [binder]
> >
> >     syntax StructType
> >       ::= AssType
> >         | AssType ","
> >         | AssType "," StructType
> >         | "..." Expr
> >
> >     syntax AssType
> >       ::= Expr
> >         | Id ":" Expr [binder]
> >
> >     syntax Pat
> >       ::= Id
> >         | "(" Pat ")"     [brackets]
> >         | Pat ":" Expr
> >         | "{" "}"
> >         | "{" StructPat "}"
> >
> >     syntax StructPat
> >       ::= AssPat
> >         | AssPat ","
> >         | AssPat "," StructPat
> >         | "..." Pat
> >
> >     syntax AssPat
> >       ::= Pat
> >         | Id "=" Pat [binder]
> >
> > endmodule
> >
> > module MALK
> >     imports MALK-SYNTAX
> >     imports SUBSTITUTION
> >
> >     syntax KResult ::= Val
> >
> >     configuration <T> <k> $PGM:Expr </k> <state> .List </state> </T>
> >
> >     // structural rules
> >
> >     // expand struct terms (do these go the wrong direction? :/ )
> >     rule A:AssExpr:StructExpr => A , [structural]
> >     rule {H:AssExpr, T:StructExpr}:Expr => {H, ... {T}} [structural]
> >     rule {H:AssExpr,} => {H, ... {}} [structural]
> >     rule {... T:Expr}:Expr => T [structural]
> >
> >     // expand struct types (do these go the wrong direction? :/ )
> >     rule A:AssType:StructType => A , [structural]
> >     rule #{H:AssType, T:StructType}:Expr => #{H, ... #{T}} [structural]
> >     rule #{H:AssType,} => #{H, ... #{}} [structural]
> >     rule #{... T:Expr}:Expr => T [structural]
> >
> >     // expand struct terms (do these go the wrong direction? :/ )
> >     rule A:AssPat:StructPat => A , [structural]
> >     rule {H:AssPat, T:StructPat}:Pat => {H, ... {T}} [structural]
> >     rule {H:AssPat,} => {H, ... {}} [structural]
> >     rule {... T:Pat}:Pat => T [structural]
> >
> >
> >     // computational rules
> >     rule (X:Id:Pat => E:Expr):Val V:Val => E[V / X]
> >     rule ({} => E:Expr):Val {} => E
> >     rule (({H:Pat:AssPat, ... T:Pat}:Pat => E):Val {A:Expr:AssExpr, ...
> > B:Expr}:Expr) => ((H => (T => E):Expr):Expr A B)   [structural]
> >     rule (({(X:Id = H:Pat):AssPat, ... T:Pat}:Pat => E):Val {(X =
> > A:Expr):AssExpr, ... B:Expr}:Expr) => ((H => (T => E):Expr):Expr A B)
> >  [structural]
> >
> > endmodule
> >
> >

Attachment: signature.asc
Description: Digital signature