feat: Provide grammar producing aterms with signature matching Chap 4

example.
This commit is contained in:
Glen Whitney 2020-12-15 21:58:07 -08:00
parent 79b9392173
commit 412bd679f1
4 changed files with 24 additions and 4 deletions

1
.gitignore vendored
View File

@ -9,3 +9,4 @@
/.factorypath /.factorypath
/.polyglot.metaborg.yaml /.polyglot.metaborg.yaml
*.aterm

View File

@ -8,7 +8,7 @@ imports
language language
table : target/metaborg/sdf.tbl table : target/metaborg/sdf.tbl
start symbols : Start start symbols : Prop
line comment : "//" line comment : "//"
block comment : "/*" * "*/" block comment : "/*" * "*/"

1
prop.spl Normal file
View File

@ -0,0 +1 @@
(1 -> 0) & 0 = p & 0

View File

@ -6,12 +6,30 @@ imports
context-free start-symbols context-free start-symbols
Start Prop
context-free sorts context-free sorts
Start Prop String
context-free syntax context-free syntax
Start.Empty = <> Prop.True = <1>
Prop.False = <0>
Prop.Atom = String
Prop.Not = <!<Prop>>
Prop.And = <<Prop> & <Prop>>
Prop.Or = <<Prop> | <Prop>>
Prop.Impl = [[Prop] -> [Prop]]
Prop.Eq = <<Prop> = <Prop>>
Prop = <(<Prop>)> {bracket}
String = ID
context-free priorities
Prop.Not
> Prop.And
> Prop.Or
> Prop.Impl
> Prop.Eq