K-user mailing list

[Andrew Cann <shum AT canndrew.org>]

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