K-user mailing list

[Radu Mereuta <headness13 AT gmail.com>]

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