From afda78c985d393400d2bc370a6ffcceb2e5f1e63 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Sun, 23 Jun 2019 20:32:53 +0530 Subject: [PATCH 01/15] t/imp/programs/two-plus-two: Remove unused program --- t/imp/programs/two-plus-two.imp | 4 ---- 1 file changed, 4 deletions(-) delete mode 100644 t/imp/programs/two-plus-two.imp diff --git a/t/imp/programs/two-plus-two.imp b/t/imp/programs/two-plus-two.imp deleted file mode 100644 index c63dc8f..0000000 --- a/t/imp/programs/two-plus-two.imp +++ /dev/null @@ -1,4 +0,0 @@ -bool a, b, c; -a = true; -b = false; -c = a & b; From 536096f1b310d0e760982ab70fa683918fac8127 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 25 Jun 2019 16:37:03 +0530 Subject: [PATCH 02/15] ekore: Combine two productions for Attr, by subsorting EKoreKString < TagContent --- src/ekore.md | 4 +--- src/parser-util.md | 2 -- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/src/ekore.md b/src/ekore.md index 639e5ab..653d238 100644 --- a/src/ekore.md +++ b/src/ekore.md @@ -237,7 +237,7 @@ module ATTRIBUTES-COMMON syntax KAttributesDeclaration ::= "[" AttrList "]" [klabel(kAttributesDeclaration)] syntax OptionalAttributes ::= KAttributesDeclaration - syntax TagContent ::= UpperName | LowerName | Numbers + syntax TagContent ::= UpperName | LowerName | Numbers | EKoreKString syntax TagContents syntax KEY ::= LowerName @@ -247,7 +247,6 @@ module ATTRIBUTES-ABSTRACT imports ATTRIBUTES-COMMON syntax Attr ::= tagSimple(KEY) [klabel(tagSimple), format(%3)] | KEY "(" TagContents ")" [klabel(tagContent)] - | KEY "(" EKoreKString ")" [klabel(tagString)] syntax AttrList ::= Attr "," AttrList [klabel(consAttrList), format(%1 %2 %3)] | ".AttrList" [klabel(dotAttrList)] @@ -263,7 +262,6 @@ module ATTRIBUTES-SYNTAX syntax Attr ::= KEY [klabel(tagSimple)] | KEY "(" TagContents ")" [klabel(tagContent)] - | KEY "(" EKoreKString ")" [klabel(tagString)] syntax EmptyAttrList ::= "" [klabel(dotAttrList )] syntax NeAttrList ::= Attr "," NeAttrList [klabel(consAttrList)] | Attr EmptyAttrList [klabel(consAttrList)] diff --git a/src/parser-util.md b/src/parser-util.md index 6e350a3..808ec34 100644 --- a/src/parser-util.md +++ b/src/parser-util.md @@ -147,8 +147,6 @@ module PARSER-UTIL => tokenToString(KEY) rule AttrToString(KEY:KEY(CONTENTS:TagContents)) => tokenToString(KEY) +String "(" +String tokenToString(CONTENTS) +String ")" - rule AttrToString(KEY:KEY(CONTENTS:EKoreKString)) - => tokenToString(KEY) +String "(" +String tokenToString(CONTENTS) +String ")" syntax String ::= TagContentsToString(TagContents) [function] rule TagContentsToString(tagContents(TC, TCs)) From 5de430ffb160ab98007dd41f356512dd9c449ed2 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 25 Jun 2019 16:46:57 +0530 Subject: [PATCH 03/15] Extract helpers for AttrList: #keyInAttributes, #getAttributeContent --- src/kink.md | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/src/kink.md b/src/kink.md index f83b779..ef40e58 100644 --- a/src/kink.md +++ b/src/kink.md @@ -148,6 +148,22 @@ module META-ACCESSORS syntax LowerName ::= "function" [token] ``` +```k + syntax Bool ::= #keyInAttributes(KEY, AttrList) [function] + rule #keyInAttributes(_, .AttrList) => false + rule #keyInAttributes(KEY, (tagSimple(KEY), _)) => true + rule #keyInAttributes(KEY, (tagContent(KEY, _), _)) => true + rule #keyInAttributes(KEY, (_ , REST)) + => #keyInAttributes(KEY, REST) [owise] + + syntax TagContents ::= #getAttributeContent(KEY, AttrList) [function] +// rule #getAttributeContent(_, .AttrList) => undefined +// rule #getAttributeContent(KEY, (tagSimple(KEY) , _)) => undefined + rule #getAttributeContent(KEY, (tagContent(KEY, CONTENT), _)) => CONTENT + rule #getAttributeContent(KEY, (_ , REST)) + => #getAttributeContent(KEY, REST) [owise] +``` + ```k endmodule ``` @@ -445,16 +461,8 @@ module PRODUCTIONS-TO-SYMBOL-DECLARATIONS ```k syntax LowerName ::= "klabel" [token] syntax SymbolName ::= #symbolNameFromAttrList(AttrList) [function] - rule #symbolNameFromAttrList - ( consAttrList - ( tagContent(klabel, SNAME:TagContents) - , ATTRS - ) - ) - // TODO: We need to handle errors - => {parseSymbolName(tokenToString(SNAME))}:>SymbolName - rule #symbolNameFromAttrList(consAttrList(_, ATTRS)) - => #symbolNameFromAttrList(ATTRS) [owise] + rule #symbolNameFromAttrList(ATTRS) + => {parseSymbolName(tokenToString(#getAttributeContent(klabel, ATTRS)))}:>SymbolName syntax Patterns ::= #removeKlabelAttr(AttrList) [function] rule #removeKlabelAttr(consAttrList(tagContent(klabel, _), ATTRS)) From 719b40e6e168daf864f501e5d7a06be5fb89999e Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 25 Jun 2019 16:54:45 +0530 Subject: [PATCH 04/15] kore: Add klabels for various pattern productions KLight needs them --- src/kore.md | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/kore.md b/src/kore.md index 8cc31ee..1ffee32 100644 --- a/src/kore.md +++ b/src/kore.md @@ -41,22 +41,22 @@ module KORE-COMMON syntax Pattern ::= Variable // | String | Symbol "(" Patterns ")" [klabel(application)] - | "\\and" "{" Sort "}" "(" Pattern "," Pattern ")" - | "\\not" "{" Sort "}" "(" Pattern ")" - | "\\or" "{" Sort "}" "(" Pattern "," Pattern ")" - | "\\implies" "{" Sort "}" "(" Pattern "," Pattern ")" - | "\\iff" "{" Sort "}" "(" Pattern "," Pattern ")" - | "\\forall" "{" Sort "}" "(" Variable "," Pattern ")" - | "\\exists" "{" Sort "}" "(" Variable "," Pattern ")" - | "\\ceil" "{" Sort "," Sort "}" "(" Pattern ")" - | "\\floor" "{" Sort "," Sort "}" "(" Pattern ")" - | "\\equals" "{" Sort "," Sort "}" "(" Pattern "," Pattern ")" [klabel(equals)] - | "\\in" "{" Sort "," Sort "}" "(" Pattern "," Pattern ")" - | "\\top" "{" Sort "}" "(" ")" - | "\\bottom" "{" Sort "}" "(" ")" - | "\\next" "{" Sort "}" "(" Pattern ")" - // | "\\rewrites" "{" Sort "}" "(" Pattern "," Pattern ")" // commented so it makes visiting easier - | "\\dv" "{" Sort "}" "(" Pattern ")" + | "\\and" "{" Sort "}" "(" Pattern "," Pattern ")" [klabel(and)] + | "\\not" "{" Sort "}" "(" Pattern ")" [klabel(not)] + | "\\or" "{" Sort "}" "(" Pattern "," Pattern ")" [klabel(or)] + | "\\implies" "{" Sort "}" "(" Pattern "," Pattern ")" [klabel(implies)] + | "\\iff" "{" Sort "}" "(" Pattern "," Pattern ")" [klabel(iff)] + | "\\forall" "{" Sort "}" "(" Variable "," Pattern ")" [klabel(forall)] + | "\\exists" "{" Sort "}" "(" Variable "," Pattern ")" [klabel(exists)] + | "\\ceil" "{" Sort "," Sort "}" "(" Pattern ")" [klabel(ceil)] + | "\\floor" "{" Sort "," Sort "}" "(" Pattern ")" [klabel(floor)] + | "\\equals" "{" Sort "," Sort "}" "(" Pattern "," Pattern ")" [klabel(equals)] + | "\\in" "{" Sort "," Sort "}" "(" Pattern "," Pattern ")" [klabel(in)] + | "\\top" "{" Sort "}" "(" ")" [klabel(top)] + | "\\bottom" "{" Sort "}" "(" ")" [klabel(bottom)] + | "\\next" "{" Sort "}" "(" Pattern ")" [klabel(next)] + | "\\rewrites" "{" Sort "}" "(" Pattern "," Pattern ")" [klabel(rewrites)] + | "\\dv" "{" Sort "}" "(" Pattern ")" [klabel(dv)] syntax Patterns syntax Attribute ::= "[" Patterns "]" [klabel(koreAttributes)] From b073816e56530aa22ba795b61e3ee6fc830bfd88 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 25 Jun 2019 16:56:00 +0530 Subject: [PATCH 05/15] Move LowerName tokens used in rules to a kore.k --- src/kink.md | 2 -- src/kore.md | 9 +++++++-- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/kink.md b/src/kink.md index ef40e58..16eecf9 100644 --- a/src/kink.md +++ b/src/kink.md @@ -145,7 +145,6 @@ module META-ACCESSORS symbol SNAME { .Sorts } ( _ ) : SORT [ ATTRS ] [owise] - syntax LowerName ::= "function" [token] ``` ```k @@ -459,7 +458,6 @@ module PRODUCTIONS-TO-SYMBOL-DECLARATIONS `#symbolNameFromAttrList` extracts the Name to be used for a symbol from the ```k - syntax LowerName ::= "klabel" [token] syntax SymbolName ::= #symbolNameFromAttrList(AttrList) [function] rule #symbolNameFromAttrList(ATTRS) => {parseSymbolName(tokenToString(#getAttributeContent(klabel, ATTRS)))}:>SymbolName diff --git a/src/kore.md b/src/kore.md index 1ffee32..17002ba 100644 --- a/src/kore.md +++ b/src/kore.md @@ -20,8 +20,8 @@ endmodule module TOKENS-SYNTAX imports TOKENS - syntax UpperName ::= r"[A-Z][A-Za-z\\-0-9'\\#]*" [token] - syntax LowerName ::= r"[a-z][A-Za-z\\-0-9'\\#]*" [token] + syntax UpperName ::= r"[A-Z][A-Za-z\\-0-9'\\#]*" [token, autoReject] + syntax LowerName ::= r"[a-z][A-Za-z\\-0-9'\\#]*" [token, autoReject] | "left" [token] // ^ I have no idea why I need to redeclare 'left', // but it gives a parsing error otherwise @@ -32,6 +32,11 @@ endmodule module KORE-COMMON imports TOKENS + syntax LowerName ::= "function" [token] + | "functional" [token] + | "constructor" [token] + | "injective" [token] + | "klabel" [token] syntax Sort ::= SortName | SortName "{" Sorts "}" [klabel(nameParam)] syntax Sorts From 31ae9242df4114a71e1aedec279ef09b2f46d8b5 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 25 Jun 2019 17:59:05 +0530 Subject: [PATCH 06/15] Add constructor, and related attributes for non-function productions --- src/command-line.md | 2 ++ src/kink.md | 30 ++++++++++++++++++++++++++++++ t/foobar/expected.ekore | 12 ++++++------ t/foobar/foobar.ekore | 4 ++-- t/peano/expected.ekore | 14 +++++++------- t/peano/peano.ekore | 8 ++++---- 6 files changed, 51 insertions(+), 19 deletions(-) diff --git a/src/command-line.md b/src/command-line.md index 871de29..e5a6c90 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -23,6 +23,7 @@ module COMMAND-LINE imports FRONTEND-MODULES-TO-KORE-MODULES imports FLATTEN-PRODUCTIONS imports OUTER-ABSTRACT + imports NON-FUNCTIONAL-PRODUCTIONS-TO-CONSTRUCTORS imports PRODUCTIONS-TO-SORT-DECLARATIONS imports PRODUCTIONS-TO-SYMBOL-DECLARATIONS imports TRANSLATE-FUNCTION-RULES @@ -81,6 +82,7 @@ High-level pipeline steps => #parseToEKore ~> #defnToConfig ~> #flattenProductions + ~> #nonFunctionProductionsToConstructors ~> #productionsToSortDeclarations ~> #productionsToSymbolDeclarations ~> #translateFunctionRules diff --git a/src/kink.md b/src/kink.md index 16eecf9..1105fa6 100644 --- a/src/kink.md +++ b/src/kink.md @@ -422,6 +422,36 @@ endmodule Once this module is defined, we import it into the main `KINK` module and add it to the pipeline. +Make non function productions constructors +------------------------------------------ + +If productions are not marked as functions, we consider them constructors. + +```k +module NON-FUNCTIONAL-PRODUCTIONS-TO-CONSTRUCTORS + imports META-ACCESSORS + syntax KItem ::= "#nonFunctionProductionsToConstructors" + rule #nonFunctionProductionsToConstructors ... + MNAME + + kSyntaxProduction(SORT, kProductionWAttr(PROD, [ ATTRS + => (tagSimple(functional) + , tagSimple(constructor) + , tagSimple(injective) + , ATTRS + ) + ] + )) + + ... + + requires notBool #keyInAttributes(constructor, ATTRS) + andBool notBool #keyInAttributes(function, ATTRS) + rule #nonFunctionProductionsToConstructors => .K ... + #STUCK() => .K ... +endmodule +``` + Extract symbols from productions -------------------------------- diff --git a/t/foobar/expected.ekore b/t/foobar/expected.ekore index 594f19e..14b3961 100644 --- a/t/foobar/expected.ekore +++ b/t/foobar/expected.ekore @@ -10,8 +10,8 @@ module B-KSEQ axiom { R } \equals { K { } , R } ( append { } ( kseq { } ( K1 : KItem { } , K2 : K { } ) , K3 : K { } ) , kseq { } ( K1 : KItem { } , append { } ( K2 : K { } , K3 : K { } ) ) ) [ ] import A-BASIC-K [ ] symbol append { } ( K { } , K { } ) : K { } [ function { } ( ) ] - symbol dotk { } ( ) : K { } [ ] - symbol kseq { } ( KItem { } , K { } ) : K { } [ ] + symbol dotk { } ( ) : K { } [ functional { } ( ), constructor { } ( ), injective { } ( ) ] + symbol kseq { } ( KItem { } , K { } ) : K { } [ functional { } ( ), constructor { } ( ), injective { } ( ) ] endmodule [ ] module C-INJ @@ -30,9 +30,9 @@ module FOOBAR sort Fizz { } [ ] sort Foo { } [ ] symbol bar { } ( ) : Foo { } [ function { } ( ) ] - symbol buzz2 { } ( ) : Foo { } [ ] - symbol foobar { } ( ) : Fizz { } [ ] - syntax Fizz ::= "foobar" [ klabel ( foobar ) ] + symbol buzz2 { } ( ) : Foo { } [ functional { } ( ), constructor { } ( ), injective { } ( ) ] + symbol foobar { } ( ) : Fizz { } [ functional { } ( ), constructor { } ( ), injective { } ( ) ] + syntax Fizz ::= "foobar" [ functional , constructor , injective , klabel ( foobar ) ] syntax Foo ::= "bar" [ klabel ( bar ) , function ] - syntax Foo ::= "buzz" [ klabel ( buzz2 ) ] + syntax Foo ::= "buzz" [ functional , constructor , injective , klabel ( buzz2 ) ] endmodule [ ] diff --git a/t/foobar/foobar.ekore b/t/foobar/foobar.ekore index e1529fc..7b4f4af 100644 --- a/t/foobar/foobar.ekore +++ b/t/foobar/foobar.ekore @@ -6,9 +6,9 @@ endmodule [ ] module B-KSEQ import A-BASIC-K [] - symbol kseq{}(KItem{}, K{}) : K{} [] + symbol kseq{}(KItem{}, K{}) : K{} [functional{}(), constructor{}(), injective{}()] symbol append{}(K{}, K{}) : K{} [function{}()] - symbol dotk{}() : K{} [] + symbol dotk{}() : K{} [functional{}(), constructor{}(), injective{}()] axiom{ R } \equals{K{},R}( diff --git a/t/peano/expected.ekore b/t/peano/expected.ekore index 69ebca8..c3e3c25 100644 --- a/t/peano/expected.ekore +++ b/t/peano/expected.ekore @@ -10,8 +10,8 @@ module B-KSEQ axiom { R } \equals { K { } , R } ( append { } ( kseq { } ( K1 : KItem { } , K2 : K { } ) , K3 : K { } ) , kseq { } ( K1 : KItem { } , append { } ( K2 : K { } , K3 : K { } ) ) ) [ ] import A-BASIC-K [ ] symbol append { } ( K { } , K { } ) : K { } [ function { } ( ) ] - symbol dotk { } ( ) : K { } [ ] - symbol kseq { } ( KItem { } , K { } ) : K { } [ ] + symbol dotk { } ( ) : K { } [ functional { } ( ), constructor { } ( ), injective { } ( ) ] + symbol kseq { } ( KItem { } , K { } ) : K { } [ functional { } ( ), constructor { } ( ), injective { } ( ) ] endmodule [ ] module C-INJ @@ -30,11 +30,11 @@ module PEANO import D-K [ ] sort Nat { } [ ] symbol plus { } ( Nat { } , Nat { } ) : Nat { } [ function { } ( ) ] - symbol succ { } ( Nat { } ) : Nat { } [ constructor { } ( ) , functional { } ( ) ] - symbol zero { } ( ) : Nat { } [ constructor { } ( ) , functional { } ( ) ] - syntax Nat ::= "plus" "(" Nat "," Nat ")" [ klabel ( plus ) , function ] - syntax Nat ::= "succ" "(" Nat ")" [ klabel ( succ ) , constructor , functional ] - syntax Nat ::= "zero" [ klabel ( zero ) , constructor , functional ] + symbol succ { } ( Nat { } ) : Nat { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] + symbol zero { } ( ) : Nat { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] + syntax Nat ::= "plus" "(" Nat "," Nat ")" [ klabel ( plus ), function ] + syntax Nat ::= "succ" "(" Nat ")" [ functional , constructor , injective , klabel ( succ ) ] + syntax Nat ::= "zero" [ functional , constructor , injective , klabel ( zero ) ] endmodule [ ] diff --git a/t/peano/peano.ekore b/t/peano/peano.ekore index 548b473..c93618e 100644 --- a/t/peano/peano.ekore +++ b/t/peano/peano.ekore @@ -5,9 +5,9 @@ endmodule [ ] module B-KSEQ import A-BASIC-K [] - symbol kseq{}(KItem{},K{}) : K{} [] symbol append{}(K{}, K{}) : K{} [function{}()] - symbol dotk{}() : K{} [] + symbol dotk { } ( ) : K { } [ functional { } ( ), constructor { } ( ), injective { } ( ) ] + symbol kseq { } ( KItem { } , K { } ) : K { } [ functional { } ( ), constructor { } ( ), injective { } ( ) ] axiom { R } \equals { K { }, R } ( append { } ( dotk { } ( ) , K2:K { } ) , K2 : K { } ) [ ] axiom { R } \equals { K { }, R } ( append { } ( kseq { } ( K1 : KItem { } , K2 : K { } ) , K3 : K { } ) , kseq { } ( K1 : KItem { } , append { } (K2 : K { } , K3 : K { } ) ) ) [ ] endmodule [ ] @@ -26,8 +26,8 @@ module PEANO import D-K [] syntax Nat ::= - "zero" [ klabel ( zero ), constructor, functional ] - | "succ" "(" Nat ")" [ klabel ( succ ), constructor, functional ] + "zero" [ klabel ( zero ) ] + | "succ" "(" Nat ")" [ klabel ( succ ) ] | "plus" "(" Nat "," Nat ")" [ klabel ( plus ), function ] rule plus{}(zero{}(), Y:Nat{}) => Y:Nat{} rule plus{}(succ{}(X:Nat{}), Y:Nat{}) => succ{}(plus{}(X:Nat{}, Y:Nat{})) From d1934fd6d78addae7cfd62181a536ee107be05e6 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 25 Jun 2019 18:00:28 +0530 Subject: [PATCH 07/15] Minor formatting and remove out of date comment --- src/kink.md | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/kink.md b/src/kink.md index 1105fa6..ddcce5d 100644 --- a/src/kink.md +++ b/src/kink.md @@ -467,7 +467,7 @@ module PRODUCTIONS-TO-SYMBOL-DECLARATIONS imports ID imports PARSER-UTIL - syntax MapTransform ::= "#productionsToSymbolDeclarations" + syntax KItem ::= "#productionsToSymbolDeclarations" rule #productionsToSymbolDeclarations ... MNAME @@ -481,7 +481,7 @@ module PRODUCTIONS-TO-SYMBOL-DECLARATIONS ... requires notBool #isSymbolDeclared(MNAME, #symbolNameFromAttrList(ATTRS)) - rule #productionsToSymbolDeclarations => .K ... + rule #productionsToSymbolDeclarations => .K ... #STUCK() => .K ... ``` @@ -504,13 +504,10 @@ module PRODUCTIONS-TO-SYMBOL-DECLARATIONS ```k syntax Pattern ::= #attr2Pattern(Attr) [function] - rule #attr2Pattern(tagSimple(KEY:LowerName)) => KEY { .Sorts } ( .Patterns ) syntax Patterns ::= #attrList2Patterns(AttrList) [function] - - // TODO: This reverses the pattern list rule #attrList2Patterns(ATTR, ATTRS) => #attr2Pattern(ATTR), #attrList2Patterns(ATTRS) rule #attrList2Patterns(.AttrList) => .Patterns ``` From 723f7688abda863d99488745948eda9fb518334f Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Thu, 27 Jun 2019 14:24:15 +0530 Subject: [PATCH 08/15] README: kink script is now in bin/ --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 09cddf8..398cc28 100644 --- a/README.md +++ b/README.md @@ -16,12 +16,12 @@ Running First, build K-in-K with `./build kink`. Then: -* to kompile an ekore definition, use `./kink kompile -- foo.ekore` -* to parse a program, use `./kink kast program.foo -- foo.k` +* to kompile an ekore definition, use `./bin/kink kompile -- foo.ekore` +* to parse a program, use `./bin/kink kast program.foo -- foo.k` Note that the `foo.k/ekore` files are arguments to KRun, whereas `kompile` and `kast program.foo` are arguments to the K-in-K definition. See -[src/command-line.md](src/command-line.md) and [./kink](./kink) for details. +[src/command-line.md](src/command-line.md) and [./bin/kink](./bin/kink) for details. Testing ======= From 790af06cf47774c9d16c530bb955b84a28efc2b9 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Thu, 27 Jun 2019 14:25:04 +0530 Subject: [PATCH 09/15] Set the right extensions for test output files --- build | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build b/build index 8e1ce5c..0a1c226 100755 --- a/build +++ b/build @@ -64,7 +64,7 @@ kink = proj.definition( backend = 'ocaml' ) def pipeline(commandline, extension): - return kink.krun().variables( + return kink.krun().ext(extension).variables( flags = "-cCOMMANDLINE='%s' -cKINKDEPLOYEDDIR=%s" % (commandline, kink.directory())) From 2d139c472653fe6f32e70915982c569aa53f24ff Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Thu, 27 Jun 2019 14:31:28 +0530 Subject: [PATCH 10/15] ekore: Simplify KProductionWAttr --- src/ekore.md | 6 +++--- src/parser-util.md | 11 ++--------- 2 files changed, 5 insertions(+), 12 deletions(-) diff --git a/src/ekore.md b/src/ekore.md index 653d238..0992a02 100644 --- a/src/ekore.md +++ b/src/ekore.md @@ -120,9 +120,7 @@ module K-PRODUCTION-COMMON syntax KSortList ::= KSortList "," KSort [klabel(kSortList)] | KSort syntax KProductionWAttr ::= KProduction OptionalAttributes [klabel(kProductionWAttr)] - | Tag "(" KSortList ")" OptionalAttributes [klabel(kFuncProductionWAttr)] - | "(" KSortList ")" OptionalAttributes [klabel(kTupleProductionWAttr)] - syntax KPrioritySeq ::= KPrioritySeq ">" KNeTagSet [klabel(kPrioritySeq)] + syntax KPrioritySeq ::= KPrioritySeq ">" KNeTagSet [klabel(kPrioritySeq)] | KNeTagSet syntax ProdBlock ::= ProdBlock "|" KProductionWAttr [klabel(prodBlock), format(%1%n%2 %3)] | KProductionWAttr @@ -132,6 +130,8 @@ module K-PRODUCTION-COMMON syntax KProductionItem syntax KProduction ::= KProductionItem | KProductionItem KProduction [klabel(kProduction), unit(emptyKProduction)] + | Tag "(" KSortList ")" [klabel(kFuncProduction)] + | "(" KSortList ")" [klabel(kTupleProduction)] syntax SyntaxDeclaration ::= "syntax" KSort OptionalAttributes [klabel(kSyntaxSort)] diff --git a/src/parser-util.md b/src/parser-util.md index 808ec34..b6f5d06 100644 --- a/src/parser-util.md +++ b/src/parser-util.md @@ -107,15 +107,6 @@ module PARSER-UTIL +String OptionalAttributesToString(ATTRS) +String "\n" +String grammarToString(DECLS) - rule grammarToString(SetItem(kSyntaxProduction(S, TAG:Tag(KSORTLIST:KSortList) ATTRS)) - DECLS - ) - => "syntax " +String tokenToString(S) +String " ::= " - +String tokenToString(TAG) - +String "(" +String KSortListToString(KSORTLIST) +String ")" +String " " - +String OptionalAttributesToString(ATTRS) - +String "\n" - +String grammarToString(DECLS) syntax String ::= KSortListToString(KSortList) [function] rule KSortListToString(S:KSort) => tokenToString(S) @@ -126,6 +117,8 @@ module PARSER-UTIL => KProductionItemToString(PI) rule KProductionToString(kProduction(PI, PIs)) => KProductionItemToString(PI) +String "\n" +String KProductionToString(PIs) + rule KProductionToString(TAG:Tag(KSORTLIST:KSortList)) + => tokenToString(TAG) +String "(" +String KSortListToString(KSORTLIST) +String ")" syntax String ::= KProductionItemToString(KProductionItem) [function] rule KProductionItemToString(nonTerminal(N)) => tokenToString(N) From ec86dbe1f44e804611af1c62f7311c945a42ddb3 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Thu, 27 Jun 2019 14:35:01 +0530 Subject: [PATCH 11/15] Add k-in-k prefix to temp files --- src/parser-util.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parser-util.md b/src/parser-util.md index b6f5d06..e17414c 100644 --- a/src/parser-util.md +++ b/src/parser-util.md @@ -61,7 +61,7 @@ module PARSER-UTIL | "parseHelper2" "(" KItem ")" [function] rule parseHelper(module = MOD, grammarFile = GRAMMAR, start = START, input = INPUT:String, output = OUTPUT) => parseHelper1( module = MOD, grammarFile = GRAMMAR - , start = START, inputFile = saveToTempFile(INPUT, "", "") + , start = START, inputFile = saveToTempFile(INPUT, "k-in-k", "") , output = OUTPUT ) rule parseHelper1(module = _, grammarFile = _, start = _, inputFile = E:IOError, output = _) From 60093e62428f262fefa5e60d374206813e011d26 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Thu, 27 Jun 2019 14:36:14 +0530 Subject: [PATCH 12/15] kink: Use #as to simplify rule --- src/kink.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/kink.md b/src/kink.md index ddcce5d..559350b 100644 --- a/src/kink.md +++ b/src/kink.md @@ -209,9 +209,9 @@ module PARSE-PROGRAM GRAMMAR rule #collectGrammar ... - kSyntaxProduction(SORT, PROD) - (.Set => SetItem(kSyntaxProduction(SORT, PROD))) REST - requires notBool(kSyntaxProduction(SORT, PROD) in REST) + kSyntaxProduction(SORT, PROD) #as SYNTAXDECL + ( .Set => SetItem(SYNTAXDECL) ) REST + requires notBool(SYNTAXDECL in REST) rule #collectGrammar => .K ... #STUCK() => .K ... endmodule From 4e2dcf7fde3fcd6d37d2afdc0b629be8f3716ed2 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Thu, 27 Jun 2019 14:47:50 +0530 Subject: [PATCH 13/15] #translateFunctionRules => #translateRules: extend to work for rewrite rules Add tests for imp --- build | 8 +++ src/command-line.md | 2 +- src/kink.md | 32 +++++++---- src/parser-util.md | 4 +- t/imp-simple/expected.ekore | 54 +++++++++++++++++++ t/imp-simple/imp-simple.ekore | 53 ++++++++++++++++++ t/imp-simple/imp-simple.k | 15 ++++++ t/imp-simple/programs/conjunction.imp | 1 + .../programs/conjunction.imp.expected | 1 + t/imp-simple/programs/conjunction.imp.kast | 1 + 10 files changed, 159 insertions(+), 12 deletions(-) create mode 100644 t/imp-simple/expected.ekore create mode 100644 t/imp-simple/imp-simple.ekore create mode 100644 t/imp-simple/imp-simple.k create mode 100644 t/imp-simple/programs/conjunction.imp create mode 100644 t/imp-simple/programs/conjunction.imp.expected create mode 100644 t/imp-simple/programs/conjunction.imp.kast diff --git a/build b/build index 0a1c226..67b0a9d 100755 --- a/build +++ b/build @@ -127,4 +127,12 @@ peano_tests += [ lang_test('t/peano', 'PEANO', 'two-plus-two.peano') ] peano_tests += [ parse_test('t/peano', 'peano.k', 'two-plus-two.peano') ] proj.build('t/peano', 'phony', inputs = Target.to_paths(peano_tests)) +# Imp +imp_tests = [] +imp_tests += [ ekore_test('t/imp-simple', 'imp-simple.ekore') ] +imp_tests += [ ekore_test('t/imp-simple', 'expected.ekore') ] +imp_tests += [ lang_test('t/imp-simple', 'IMP-SIMPLE', 'conjunction.imp') ] +imp_tests += [ parse_test('t/imp-simple', 'imp-simple.k', 'conjunction.imp') ] +proj.build('t/imp', 'phony', inputs = Target.to_paths(imp_tests)) + proj.main() diff --git a/src/command-line.md b/src/command-line.md index e5a6c90..824f497 100644 --- a/src/command-line.md +++ b/src/command-line.md @@ -85,7 +85,7 @@ High-level pipeline steps ~> #nonFunctionProductionsToConstructors ~> #productionsToSortDeclarations ~> #productionsToSymbolDeclarations - ~> #translateFunctionRules + ~> #translateRules ``` ```k diff --git a/src/kink.md b/src/kink.md index 559350b..7f5ed9f 100644 --- a/src/kink.md +++ b/src/kink.md @@ -534,27 +534,41 @@ endmodule Translate Function Rules ------------------------ -`#translateFunctionRules` generates new kore axioms for rewrite rules over -function symbols. Rules whose LHS is not a kore symbol with the function -attribute should be ignored. Since the rewrite rule carries no additional -information over the kore axiom, it can be discarded. +`#translateRules` generates new kore axioms for rules. When the left-hand-side +of the rule is a function symbol, we generate an axiom that uses equalities. +Otherwise, if it has a constructor attribute, we generate one with rewrites. We +do not handle `requires` and `ensures` clauses yet. ```k module TRANSLATE-FUNCTION-RULES imports KINK-CONFIGURATION imports META-ACCESSORS - syntax KItem ::= "#translateFunctionRules" - rule #translateFunctionRules ... + syntax KItem ::= "#translateRules" + rule #translateRules ... MNAME - kRule(noAttrs(krewrite( SYMBOL { .Sorts } ( ARG_PATTERNS ) , RHS))) + kRule(noAttrs(krewrite( SYMBOL { .Sorts } ( ARG_PATTERNS ) #as LHS, RHS))) => axiom { #token("R", "UpperName") , .Sorts } \equals { #getReturnSort(MNAME, SYMBOL), #token("R", "UpperName") } - ( SYMBOL { .Sorts } ( ARG_PATTERNS ) , RHS ) + ( LHS , RHS ) [ .Patterns ] requires #isFunctionSymbol(MNAME, SYMBOL) - rule #translateFunctionRules => .K ... + + rule #translateRules ... + MNAME + kRule(noAttrs(krewrite( SYMBOL { .Sorts } ( ARG_PATTERNS ) #as LHS , RHS))) + => #fun( RETSORT + => axiom { .Sorts } \rewrites { RETSORT } + ( \and { RETSORT } (\top{ RETSORT }(), LHS) + , \and { RETSORT } (\top{ RETSORT }(), RHS) + ) + [ .Patterns ] + ) (#getReturnSort(MNAME, SYMBOL)) + + requires notBool #isFunctionSymbol(MNAME, SYMBOL) + + rule #translateRules => .K ... #STUCK() => .K ... endmodule ``` diff --git a/src/parser-util.md b/src/parser-util.md index e17414c..ca13d4f 100644 --- a/src/parser-util.md +++ b/src/parser-util.md @@ -33,8 +33,8 @@ module PARSER-UTIL syntax KItem ::= parseSymbolName(String) [function, impure] rule [[ parseSymbolName(S) - => doParseKAST(parseHelper( module = "KORE-SYNTAX" - , grammarFile = DEPLOY_DIR +String "/src/kore.k" + => doParseKAST(parseHelper( module = "EKORE-SYNTAX" + , grammarFile = DEPLOY_DIR +String "/src/ekore.k" , start = "SymbolName" , input = S , output = "kast" diff --git a/t/imp-simple/expected.ekore b/t/imp-simple/expected.ekore new file mode 100644 index 0000000..1a05192 --- /dev/null +++ b/t/imp-simple/expected.ekore @@ -0,0 +1,54 @@ +[ ] + +module A-BASIC-K + + sort K { } [ ] + sort KItem { } [ ] + +endmodule [ ] + +module B-KSEQ + + axiom { R } \equals { K { } , R } ( append { } ( dotk { } ( ) , K2 : K { } ) , K2 : K { } ) [ ] + axiom { R } \equals { K { } , R } ( append { } ( kseq { } ( K1 : KItem { } , K2 : K { } ) , K3 : K { } ) , kseq { } ( K1 : KItem { } , append { } ( K2 : K { } , K3 : K { } ) ) ) [ ] + import A-BASIC-K [ ] + symbol append { } ( K { } , K { } ) : K { } [ function { } ( ) ] + symbol dotk { } ( ) : K { } [ ] + symbol kseq { } ( KItem { } , K { } ) : K { } [ ] + +endmodule [ ] + +module C-INJ + + axiom { S1 , S2 , S3 , R } \equals { S3 , R } ( inj { S2 , S3 } ( inj { S1 , S2 } ( T : S1 ) ) , inj { S1 , S3 } ( T : S1 ) ) [ ] + symbol inj { From , To } ( From ) : To [ ] + +endmodule [ ] + +module D-K + + import B-KSEQ [ ] + import C-INJ [ ] + +endmodule [ ] + +module IMP-SIMPLE + + axiom { } \rewrites { KCell { } } ( \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( False { } ( ) , VarB : BExp { } ) ) , dotk { } ( ) ) ) ) , \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( False { } ( ) ) , dotk { } ( ) ) ) ) ) [ ] + axiom { } \rewrites { KCell { } } ( \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( True { } ( ) , VarB : BExp { } ) ) , dotk { } ( ) ) ) ) , \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , dotk { } ( ) ) ) ) ) [ ] + import D-K [ ] + sort BExp { } [ ] + sort KCell { } [ ] + symbol And { } ( BExp { } , BExp { } ) : BExp { } [ functional { } (), constructor { } (), injective { } () ] + symbol False { } ( ) : BExp { } [ functional { } (), constructor { } (), injective { } () ] + symbol True { } ( ) : BExp { } [ functional { } (), constructor { } (), injective { } () ] + symbol kCell { } ( K { } ) : KCell { } [ functional { } (), constructor { } (), injective { } () ] + syntax BExp ::= "False" [ functional , constructor , injective , klabel ( False ) ] + syntax BExp ::= "True" [ functional , constructor , injective , klabel ( True ) ] + syntax BExp ::= BExp "&&" BExp [ functional , constructor , injective , klabel ( And ) ] + syntax KCell ::= "kCell" "(" K ")" [ functional , constructor , injective , klabel ( kCell ) ] + +endmodule [ ] + + + diff --git a/t/imp-simple/imp-simple.ekore b/t/imp-simple/imp-simple.ekore new file mode 100644 index 0000000..c1be661 --- /dev/null +++ b/t/imp-simple/imp-simple.ekore @@ -0,0 +1,53 @@ +module A-BASIC-K + sort K{} [] + sort KItem{} [] +endmodule [ ] + +module B-KSEQ + import A-BASIC-K [] + + symbol kseq{}(KItem{}, K{}) : K{} [] + symbol append{}(K{}, K{}) : K{} [function{}()] + symbol dotk{}() : K{} [] + + axiom{ R } + \equals{K{},R}( + append{}(dotk{}(),K2:K{}), + K2:K{}) + [] + + axiom{R} + \equals{K{},R}( + append{}(kseq{}(K1:KItem{},K2:K{}),K3:K{}), + kseq{}(K1:KItem{},append{}(K2:K{},K3:K{}))) + [] +endmodule [ ] + +module C-INJ + symbol inj{From,To}(From) : To [] + + axiom{S1,S2,S3,R} + \equals{S3,R}( + inj{S2,S3}(inj{S1,S2}(T:S1)), + inj{S1,S3}(T:S1)) + [] +endmodule + +module D-K + import B-KSEQ [] + import C-INJ [] +endmodule + +module IMP-SIMPLE + import D-K [] + + syntax BExp ::= "True" [klabel(True)] + | "False" [klabel(False)] + | BExp "&&" BExp [klabel(And)] + syntax KCell ::= "kCell" "(" K ")" [klabel(kCell)] + + rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(True{}(),VarB:BExp{})),dotk{}())) + => kCell{}(kseq{}(inj{BExp{}, KItem{}}(VarB:BExp{}),dotk{}())) + rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(False{}(),VarB:BExp{})),dotk{}())) + => kCell{}(kseq{}(inj{BExp{}, KItem{}}(False{}()),dotk{}())) +endmodule diff --git a/t/imp-simple/imp-simple.k b/t/imp-simple/imp-simple.k new file mode 100644 index 0000000..65a21db --- /dev/null +++ b/t/imp-simple/imp-simple.k @@ -0,0 +1,15 @@ +module IMP-SIMPLE + syntax Layout ::= r"(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" [klabel(layout)] + syntax Pgm ::= KCell + + syntax KCell ::= "" KList "" [klabel(kCell)] + syntax KList ::= KItem "~>" KList [klabel(kseq)] + | ".K" [klabel(dotk)] + syntax KItem ::= BExp [klabel(inj)] + + syntax BExp ::= "True" [klabel(True)] + | "False" [klabel(False)] + | BExp "&&" BExp [klabel(And)] + rule True && B:BExp => B:BExp + rule False && B:BExp => False +endmodule diff --git a/t/imp-simple/programs/conjunction.imp b/t/imp-simple/programs/conjunction.imp new file mode 100644 index 0000000..623fa12 --- /dev/null +++ b/t/imp-simple/programs/conjunction.imp @@ -0,0 +1 @@ + True && False ~> .K diff --git a/t/imp-simple/programs/conjunction.imp.expected b/t/imp-simple/programs/conjunction.imp.expected new file mode 100644 index 0000000..82aa1aa --- /dev/null +++ b/t/imp-simple/programs/conjunction.imp.expected @@ -0,0 +1 @@ +kCell { } ( kseq { }(inj{BExp{}, KItem{}}(False{}()), dotk{}())) diff --git a/t/imp-simple/programs/conjunction.imp.kast b/t/imp-simple/programs/conjunction.imp.kast new file mode 100644 index 0000000..ebf5326 --- /dev/null +++ b/t/imp-simple/programs/conjunction.imp.kast @@ -0,0 +1 @@ +kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( True { } ( ) , False { } ( ) ) ) , dotk { } ( ) ) ) From 5e3f0d4a1bfa0c82e9ba8db5c18dbc972e48188a Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Fri, 28 Jun 2019 14:40:02 +0530 Subject: [PATCH 14/15] Jenkinsfile: Separate stage for t/imp/; simplification --- Jenkinsfile | 38 ++++++++++---------------------------- 1 file changed, 10 insertions(+), 28 deletions(-) diff --git a/Jenkinsfile b/Jenkinsfile index e8e6313..68c5620 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -4,6 +4,9 @@ pipeline { additionalBuildArgs '--build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)' } } + options { + ansiColor('xterm') + } stages { stage("Init title") { when { changeRequest() } @@ -17,37 +20,16 @@ pipeline { steps { ansiColor('xterm') { sh '''#!/bin/bash - (cd ext/k-light/ && mvn package -DskipTests) && ./build kink - ''' - } - } - } - stage('t/foobar') { - steps { - ansiColor('xterm') { - sh '''#!/bin/bash - ./build t/foobar - ''' - } - } - } - stage('t/peano') { - steps { - ansiColor('xterm') { - sh '''#!/bin/bash - ./build t/foobar - ''' - } - } - } - stage('t/*') { - steps { - ansiColor('xterm') { - sh '''#!/bin/bash - ./build + (cd ext/k-light/ && mvn package -DskipTests) && ./build kink .build/kbackend-haskell ''' } } } + stage('t/foobar') { steps { sh '''./build t/foobar''' } } + stage('t/peano') { steps { sh '''./build t/peano''' } } + stage('t/imp') { steps { sh '''./build t/imp''' } } + + // Catch-all for anything left out + stage('t/*') { steps { sh '''./build''' } } } } From 5c8494ad6f026adf371f105e5c5ba78fabb51eb8 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Fri, 28 Jun 2019 15:29:16 +0530 Subject: [PATCH 15/15] build: when extracting the k/kore-cell fails print the input file --- build | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/build b/build index 67b0a9d..155fa41 100755 --- a/build +++ b/build @@ -19,12 +19,12 @@ proj = KProject() kore_from_config = proj.rule( 'kore-from-config' , description = 'kore-from-config: $in' - , command = 'lib/kore-from-config "$in" "$out"' + , command = 'lib/kore-from-config "$in" "$out" || (cat "$in" ; false)' , ext = 'kore' ) k_from_config = proj.rule( 'k-from-config' , description = 'k-from-config' - , command = 'lib/k-from-config "$in" "$out"' + , command = 'lib/k-from-config "$in" "$out" || (cat "$in" ; false)' , ext = 'kore' ) def kore_exec(kore, ext = 'kore-exec'):