From c33cd1a827863c28136c9cb20c747cb5111a0336 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 2 Jul 2019 17:26:37 +0530 Subject: [PATCH 01/10] !!! incomplete: Extend imp to do heating and cooling --- t/imp-simple/expected.ekore | 20 +++++++++++-------- t/imp-simple/imp-simple.ekore | 17 +++++++++------- t/imp-simple/imp-simple.k | 17 +++++++++++----- .../programs/conjunction.imp.expected | 2 +- t/imp-simple/programs/conjunction.imp.kast | 2 +- 5 files changed, 36 insertions(+), 22 deletions(-) diff --git a/t/imp-simple/expected.ekore b/t/imp-simple/expected.ekore index 47ebf53..a04d5c1 100644 --- a/t/imp-simple/expected.ekore +++ b/t/imp-simple/expected.ekore @@ -36,18 +36,22 @@ endmodule [ ] module IMP-SIMPLE - axiom { } \rewrites { KCell { } } ( \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( False { } ( ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) ) , \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( False { } ( ) ) , DOTVAR : K { } ) ) ) ) [ ] - axiom { } \rewrites { KCell { } } ( \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( True { } ( ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) ) , \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) ) ) [ ] + axiom { } \rewrites { KCell { } } ( \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( False { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) ) , \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExpResult { } , KItem { } } ( False { } ( ) ) , DOTVAR : K { } ) ) ) ) [ ] + axiom { } \rewrites { KCell { } } ( \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) ) , \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) ) ) [ ] import D-K [ ] sort BExp { } [ ] + sort BExpResult { } [ ] 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 ) ] + symbol And { } ( BExp { } , BExp { } ) : BExp { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] + symbol False { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] + symbol HOLE { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] + symbol True { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] + symbol kCell { } ( K { } ) : KCell { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] syntax BExp ::= BExp "&&" BExp [ functional , constructor , injective , klabel ( And ) ] + syntax BExp ::= BExpResult [ functional , constructor , injective , klabel ( inj ) ] + syntax BExpResult ::= "#hole" [ functional , constructor , injective , klabel ( HOLE ) ] + syntax BExpResult ::= "False" [ functional , constructor , injective , klabel ( False ) ] + syntax BExpResult ::= "True" [ functional , constructor , injective , klabel ( True ) ] 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 index 2b1e81f..5374b58 100644 --- a/t/imp-simple/imp-simple.ekore +++ b/t/imp-simple/imp-simple.ekore @@ -42,13 +42,16 @@ 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)] + syntax KCell ::= "kCell" "(" K ")" [klabel(kCell)] - rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(True{}(),VarB:BExp{})),DOTVAR:K{})) + syntax BExpResult ::= "True" [klabel(True)] + | "False" [klabel(False)] + | "#hole" [klabel(HOLE)] + syntax BExp ::= BExpResult [klabel(inj)] + | BExp "&&" BExp [klabel(And)] + + rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(True{}()),VarB:BExp{})),DOTVAR:K{})) => kCell{}(kseq{}(inj{BExp{}, KItem{}}(VarB:BExp{}),DOTVAR:K{})) - rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(False{}(),VarB:BExp{})),DOTVAR:K{})) - => kCell{}(kseq{}(inj{BExp{}, KItem{}}(False{}()),DOTVAR:K{})) + rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(False{}()),VarB:BExp{})),DOTVAR:K{})) + => kCell{}(kseq{}(inj{BExpResult{}, KItem{}}(False{}()),DOTVAR:K{})) endmodule diff --git a/t/imp-simple/imp-simple.k b/t/imp-simple/imp-simple.k index 65a21db..4e9cca0 100644 --- a/t/imp-simple/imp-simple.k +++ b/t/imp-simple/imp-simple.k @@ -7,9 +7,16 @@ module IMP-SIMPLE | ".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 + syntax BExpResult ::= "True" [klabel(True)] + | "False" [klabel(False)] + | "#hole" [klabel(HOLE)] + syntax BExp ::= BExpResult [klabel(inj)] + | BExp "&&" BExp [klabel(And)] + + rule True && B:BExp => B:BExp ... + rule False && B:BExp => False ... + rule B1 && B2 + => B1 ~> HOLE && B2 + ... + endmodule diff --git a/t/imp-simple/programs/conjunction.imp.expected b/t/imp-simple/programs/conjunction.imp.expected index 82aa1aa..da22986 100644 --- a/t/imp-simple/programs/conjunction.imp.expected +++ b/t/imp-simple/programs/conjunction.imp.expected @@ -1 +1 @@ -kCell { } ( kseq { }(inj{BExp{}, KItem{}}(False{}()), dotk{}())) +kCell { } ( kseq { }(inj{BExpResult{}, KItem{}}(False{}()), dotk{}())) diff --git a/t/imp-simple/programs/conjunction.imp.kast b/t/imp-simple/programs/conjunction.imp.kast index ebf5326..92bbca0 100644 --- a/t/imp-simple/programs/conjunction.imp.kast +++ b/t/imp-simple/programs/conjunction.imp.kast @@ -1 +1 @@ -kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( True { } ( ) , False { } ( ) ) ) , dotk { } ( ) ) ) +kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , inj { BExpResult { } , BExp { } } ( False { } ( ) ) ) ) , dotk { } ( ) ) ) From 7ad29b1da9b54b8d25b4b8707a6b6f6ed5a19a0b Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 23 Jul 2019 00:46:13 +0530 Subject: [PATCH 02/10] imp: Add Brackets to allow unambigious expressions with more that two terms --- t/imp-simple/expected.ekore | 3 +++ t/imp-simple/imp-simple.ekore | 3 +++ t/imp-simple/imp-simple.k | 7 +++---- t/imp-simple/programs/conjunction.imp | 2 +- t/imp-simple/programs/conjunction.imp.kast | 2 +- 5 files changed, 11 insertions(+), 6 deletions(-) diff --git a/t/imp-simple/expected.ekore b/t/imp-simple/expected.ekore index a04d5c1..5a12239 100644 --- a/t/imp-simple/expected.ekore +++ b/t/imp-simple/expected.ekore @@ -38,15 +38,18 @@ module IMP-SIMPLE axiom { } \rewrites { KCell { } } ( \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( False { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) ) , \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExpResult { } , KItem { } } ( False { } ( ) ) , DOTVAR : K { } ) ) ) ) [ ] axiom { } \rewrites { KCell { } } ( \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) ) , \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) ) ) [ ] + axiom { } \rewrites { KCell { } } ( \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( Bracket { } ( VarB : BExp { } ) ) , DOTVAR : K { } ) ) ) , \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) ) ) [ ] import D-K [ ] sort BExp { } [ ] sort BExpResult { } [ ] sort KCell { } [ ] symbol And { } ( BExp { } , BExp { } ) : BExp { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] + symbol Bracket { } ( BExp { } ) : BExp { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] symbol False { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] symbol HOLE { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] symbol True { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] symbol kCell { } ( K { } ) : KCell { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] + syntax BExp ::= "(" BExp ")" [ functional , constructor , injective , klabel ( Bracket ) ] syntax BExp ::= BExp "&&" BExp [ functional , constructor , injective , klabel ( And ) ] syntax BExp ::= BExpResult [ functional , constructor , injective , klabel ( inj ) ] syntax BExpResult ::= "#hole" [ functional , constructor , injective , klabel ( HOLE ) ] diff --git a/t/imp-simple/imp-simple.ekore b/t/imp-simple/imp-simple.ekore index 5374b58..131ab56 100644 --- a/t/imp-simple/imp-simple.ekore +++ b/t/imp-simple/imp-simple.ekore @@ -48,10 +48,13 @@ module IMP-SIMPLE | "False" [klabel(False)] | "#hole" [klabel(HOLE)] syntax BExp ::= BExpResult [klabel(inj)] + | "(" BExp ")" [klabel(Bracket)] | BExp "&&" BExp [klabel(And)] rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(True{}()),VarB:BExp{})),DOTVAR:K{})) => kCell{}(kseq{}(inj{BExp{}, KItem{}}(VarB:BExp{}),DOTVAR:K{})) rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(False{}()),VarB:BExp{})),DOTVAR:K{})) => kCell{}(kseq{}(inj{BExpResult{}, KItem{}}(False{}()),DOTVAR:K{})) + rule kCell{}(kseq{}(inj{BExp{}, KItem{}} (Bracket{}(VarB:BExp{})), DOTVAR:K {})) + => kCell{}(kseq{}(inj{BExp{}, KItem{}} (VarB:BExp{}), DOTVAR:K {})) endmodule diff --git a/t/imp-simple/imp-simple.k b/t/imp-simple/imp-simple.k index 4e9cca0..d8d68d3 100644 --- a/t/imp-simple/imp-simple.k +++ b/t/imp-simple/imp-simple.k @@ -11,12 +11,11 @@ module IMP-SIMPLE | "False" [klabel(False)] | "#hole" [klabel(HOLE)] syntax BExp ::= BExpResult [klabel(inj)] + | "(" BExp ")" [klabel(Bracket)] | BExp "&&" BExp [klabel(And)] rule True && B:BExp => B:BExp ... rule False && B:BExp => False ... - rule B1 && B2 - => B1 ~> HOLE && B2 - ... - + rule B1 && B2 => B1 ~> HOLE && B2 ... + rule ( B1 ) => B1 ... endmodule diff --git a/t/imp-simple/programs/conjunction.imp b/t/imp-simple/programs/conjunction.imp index 623fa12..1cb41c1 100644 --- a/t/imp-simple/programs/conjunction.imp +++ b/t/imp-simple/programs/conjunction.imp @@ -1 +1 @@ - True && False ~> .K + True && ( False && True ) ~> .K diff --git a/t/imp-simple/programs/conjunction.imp.kast b/t/imp-simple/programs/conjunction.imp.kast index 92bbca0..6a570bf 100644 --- a/t/imp-simple/programs/conjunction.imp.kast +++ b/t/imp-simple/programs/conjunction.imp.kast @@ -1 +1 @@ -kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , inj { BExpResult { } , BExp { } } ( False { } ( ) ) ) ) , dotk { } ( ) ) ) +kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , Bracket { } ( And { } ( inj { BExpResult { } , BExp { } } ( False { } ( ) ) , inj { BExpResult { } , BExp { } } ( True { } ( ) ) ) ) ) ) , dotk { } ( ) ) ) From 9225bede1793f8a46440c86dce9d2d252a2ab019 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 23 Jul 2019 03:47:16 +0530 Subject: [PATCH 03/10] build: Fix alias `t/imp` => `t/imp-simple` --- build | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build b/build index e77e786..2f521ec 100755 --- a/build +++ b/build @@ -133,6 +133,6 @@ 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.build('t/imp-simple', 'phony', inputs = Target.to_paths(imp_tests)) proj.main() From c59f0fbe491ed56a0266709a8889edae69a55733 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 23 Jul 2019 03:48:00 +0530 Subject: [PATCH 04/10] !!! Assign statement --- t/imp-simple/expected.ekore | 48 ++++++++---------- t/imp-simple/imp-simple.ekore | 16 +++--- t/imp-simple/imp-simple.k | 49 +++++++++++++------ t/imp-simple/programs/conjunction.imp | 5 +- .../programs/conjunction.imp.expected | 5 +- t/imp-simple/programs/conjunction.imp.kast | 2 +- 6 files changed, 73 insertions(+), 52 deletions(-) diff --git a/t/imp-simple/expected.ekore b/t/imp-simple/expected.ekore index 5a12239..ee95699 100644 --- a/t/imp-simple/expected.ekore +++ b/t/imp-simple/expected.ekore @@ -1,63 +1,57 @@ [ ] 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 { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] - symbol kseq { } ( KItem { } , K { } ) : K { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] - syntax K ::= ".K" [ functional , constructor , injective , klabel ( dotk ) ] - syntax K ::= KItem "~>" K [ functional , constructor , injective , klabel ( kseq ) ] - + symbol dotk { } ( ) : K { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] + symbol kseq { } ( KItem { } , K { } ) : K { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] + syntax K ::= ".K" [ functional , constructor , injective , klabel ( dotk ) ] + syntax K ::= KItem "~>" K [ functional , constructor , injective , klabel ( kseq ) ] 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 [ sortInjection{}() ] - + symbol inj { From , To } ( From ) : To [ sortInjection { } ( ) ] 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 { } ( inj { BExpResult { } , BExp { } } ( False { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) ) , \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExpResult { } , KItem { } } ( False { } ( ) ) , DOTVAR : K { } ) ) ) ) [ ] - axiom { } \rewrites { KCell { } } ( \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) ) , \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) ) ) [ ] - axiom { } \rewrites { KCell { } } ( \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( Bracket { } ( VarB : BExp { } ) ) , DOTVAR : K { } ) ) ) , \and { KCell { } } ( \top { KCell { } } ( ) , kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) ) ) [ ] + axiom { } \rewrites { ImpCell { } } ( \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( False { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) , \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExpResult { } , KItem { } } ( False { } ( ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) ) [ ] + axiom { } \rewrites { ImpCell { } } ( \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) , \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) ) [ ] + axiom { } \rewrites { ImpCell { } } ( \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( Bracket { } ( VarB : BExp { } ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) , \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) ) [ ] import D-K [ ] + sort ACell { } [ ] sort BExp { } [ ] sort BExpResult { } [ ] + sort ImpCell { } [ ] sort KCell { } [ ] symbol And { } ( BExp { } , BExp { } ) : BExp { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] symbol Bracket { } ( BExp { } ) : BExp { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] symbol False { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] symbol HOLE { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] symbol True { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] + symbol aCell { } ( BExpResult { } ) : ACell { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] + symbol impCell { } ( KCell { } , ACell { } ) : ImpCell { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] symbol kCell { } ( K { } ) : KCell { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] - syntax BExp ::= "(" BExp ")" [ functional , constructor , injective , klabel ( Bracket ) ] - syntax BExp ::= BExp "&&" BExp [ functional , constructor , injective , klabel ( And ) ] - syntax BExp ::= BExpResult [ functional , constructor , injective , klabel ( inj ) ] - syntax BExpResult ::= "#hole" [ functional , constructor , injective , klabel ( HOLE ) ] - syntax BExpResult ::= "False" [ functional , constructor , injective , klabel ( False ) ] - syntax BExpResult ::= "True" [ functional , constructor , injective , klabel ( True ) ] - syntax KCell ::= "kCell" "(" K ")" [ functional , constructor , injective , klabel ( kCell ) ] - + syntax ACell ::= "" BExpResult "" [ functional , constructor , injective , klabel ( aCell ) ] + syntax BExp ::= "(" BExp ")" [ functional , constructor , injective , klabel ( Bracket ) ] + syntax BExp ::= BExp "&&" BExp [ functional , constructor , injective , klabel ( And ) ] + syntax BExp ::= BExpResult [ functional , constructor , injective , klabel ( inj ) ] + syntax BExpResult ::= "#hole" [ functional , constructor , injective , klabel ( HOLE ) ] + syntax BExpResult ::= "False" [ functional , constructor , injective , klabel ( False ) ] + syntax BExpResult ::= "True" [ functional , constructor , injective , klabel ( True ) ] + syntax ImpCell ::= "" KCell ACell "" [ functional , constructor , injective , klabel ( impCell ) ] + syntax KCell ::= "" K "" [ functional , constructor , injective , klabel ( kCell ) ] endmodule [ ] - - diff --git a/t/imp-simple/imp-simple.ekore b/t/imp-simple/imp-simple.ekore index 131ab56..5b63280 100644 --- a/t/imp-simple/imp-simple.ekore +++ b/t/imp-simple/imp-simple.ekore @@ -42,7 +42,9 @@ endmodule module IMP-SIMPLE import D-K [] - syntax KCell ::= "kCell" "(" K ")" [klabel(kCell)] + syntax ImpCell ::= "" KCell ACell "" [klabel(impCell)] + syntax KCell ::= "" K "" [klabel(kCell)] + syntax ACell ::= "" BExpResult "" [klabel(aCell)] syntax BExpResult ::= "True" [klabel(True)] | "False" [klabel(False)] @@ -51,10 +53,10 @@ module IMP-SIMPLE | "(" BExp ")" [klabel(Bracket)] | BExp "&&" BExp [klabel(And)] - rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(True{}()),VarB:BExp{})),DOTVAR:K{})) - => kCell{}(kseq{}(inj{BExp{}, KItem{}}(VarB:BExp{}),DOTVAR:K{})) - rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(False{}()),VarB:BExp{})),DOTVAR:K{})) - => kCell{}(kseq{}(inj{BExpResult{}, KItem{}}(False{}()),DOTVAR:K{})) - rule kCell{}(kseq{}(inj{BExp{}, KItem{}} (Bracket{}(VarB:BExp{})), DOTVAR:K {})) - => kCell{}(kseq{}(inj{BExp{}, KItem{}} (VarB:BExp{}), DOTVAR:K {})) + rule impCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(True{}()),VarB:BExp{})),DOTVAR:K{})), aCell {} ( AVal:BExpResult {})) + => impCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}}(VarB:BExp{}),DOTVAR:K{})), aCell {} ( AVal:BExpResult {})) + rule impCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(False{}()),VarB:BExp{})),DOTVAR:K{})), aCell {} ( AVal:BExpResult {})) + => impCell{}(kCell{}(kseq{}(inj{BExpResult{}, KItem{}}(False{}()),DOTVAR:K{})), aCell {} ( AVal:BExpResult {})) + rule impCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}} (Bracket{}(VarB:BExp{})), DOTVAR:K {})), aCell {} ( AVal:BExpResult {})) + => impCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}} (VarB:BExp{}), DOTVAR:K {})), aCell {} ( AVal:BExpResult {})) endmodule diff --git a/t/imp-simple/imp-simple.k b/t/imp-simple/imp-simple.k index d8d68d3..11b1677 100644 --- a/t/imp-simple/imp-simple.k +++ b/t/imp-simple/imp-simple.k @@ -1,21 +1,40 @@ module IMP-SIMPLE syntax Layout ::= r"(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" [klabel(layout)] - syntax Pgm ::= KCell + syntax Pgm ::= ImpCell + + syntax K ::= KItem "~>" K [klabel(kseq)] + | ".K" [klabel(dotk)] + syntax KItem ::= BExp [klabel(inj)] - syntax KCell ::= "" KList "" [klabel(kCell)] - syntax KList ::= KItem "~>" KList [klabel(kseq)] - | ".K" [klabel(dotk)] - syntax KItem ::= BExp [klabel(inj)] + configuration + $PGM:K + False:BExpResult + - syntax BExpResult ::= "True" [klabel(True)] - | "False" [klabel(False)] - | "#hole" [klabel(HOLE)] - syntax BExp ::= BExpResult [klabel(inj)] - | "(" BExp ")" [klabel(Bracket)] - | BExp "&&" BExp [klabel(And)] + syntax ImpCell ::= "" KCell ACell "" [klabel(impCell)] + syntax KCell ::= "" K "" [klabel(kCell)] + syntax ACell ::= "" BExpResult "" [klabel(aCell)] - rule True && B:BExp => B:BExp ... - rule False && B:BExp => False ... - rule B1 && B2 => B1 ~> HOLE && B2 ... - rule ( B1 ) => B1 ... + syntax BExpResult ::= "True" [klabel(True)] + | "False" [klabel(False)] + | "#hole" [klabel(HOLE)] + syntax BExp ::= BExpResult [klabel(inj)] + | "(" BExp ")" [klabel(Bracket)] + | BExp "&&" BExp [klabel(And)] + + syntax Statement ::= "a" ":=" BExp [klabel(assignToA)] + +// rule True && B:BExp => B:BExp ... +// rule False && B:BExp => False ... +// rule B1 && B2 => B1 ~> #hole && B2 ... +// rule ( B1 ) => B1 ... +// +// rule +// a := B:BExpResult ~> REST +// _:BExpResult +// +// => +// REST +// B:BExpResult +// endmodule diff --git a/t/imp-simple/programs/conjunction.imp b/t/imp-simple/programs/conjunction.imp index 1cb41c1..12348a7 100644 --- a/t/imp-simple/programs/conjunction.imp +++ b/t/imp-simple/programs/conjunction.imp @@ -1 +1,4 @@ - True && ( False && True ) ~> .K + + True && ( False && True ) ~> .K + False + diff --git a/t/imp-simple/programs/conjunction.imp.expected b/t/imp-simple/programs/conjunction.imp.expected index da22986..f4148dd 100644 --- a/t/imp-simple/programs/conjunction.imp.expected +++ b/t/imp-simple/programs/conjunction.imp.expected @@ -1 +1,4 @@ -kCell { } ( kseq { }(inj{BExpResult{}, KItem{}}(False{}()), dotk{}())) +impCell{}( + kCell{}(kseq{}(inj{BExpResult{}, KItem{}}(False{}()), dotk{}())), + aCell{}(False{}()) +) \ No newline at end of file diff --git a/t/imp-simple/programs/conjunction.imp.kast b/t/imp-simple/programs/conjunction.imp.kast index 6a570bf..cefe3b2 100644 --- a/t/imp-simple/programs/conjunction.imp.kast +++ b/t/imp-simple/programs/conjunction.imp.kast @@ -1 +1 @@ -kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , Bracket { } ( And { } ( inj { BExpResult { } , BExp { } } ( False { } ( ) ) , inj { BExpResult { } , BExp { } } ( True { } ( ) ) ) ) ) ) , dotk { } ( ) ) ) +impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , Bracket { } ( And { } ( inj { BExpResult { } , BExp { } } ( False { } ( ) ) , inj { BExpResult { } , BExp { } } ( True { } ( ) ) ) ) ) ) , dotk { } ( ) ) ) , aCell { } ( False { } ( ) ) ) From a2d51818dc03acb9896c29943168a90db37a16c0 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Thu, 15 Aug 2019 23:40:10 +0530 Subject: [PATCH 05/10] build: Rename lang_test to exec_test --- build | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/build b/build index 2f521ec..28566e0 100755 --- a/build +++ b/build @@ -93,7 +93,7 @@ def parse_test(base_dir, def_file, input_program): .variables(flags = '--ignore-all-space --ignore-blank-lines')) \ .default() -def lang_test(base_dir, module, program): +def exec_test(base_dir, module, program): language_kore = path.join(base_dir, 'expected.ekore') program_pattern = path.join(base_dir, 'programs', program + '.kast') expected_pattern = path.join(base_dir, 'programs', program + '.expected') @@ -116,14 +116,14 @@ foobar_tests = [] foobar_tests += [ ekore_test('t/foobar', 'foobar.ekore') ] foobar_tests += [ ekore_test('t/foobar', 'expected.ekore') ] foobar_tests += [ parse_test('t/foobar', 'foobar.k', 'bar.foobar') ] -foobar_tests += [ lang_test('t/foobar', 'FOOBAR', 'bar.foobar') ] +foobar_tests += [ exec_test('t/foobar', 'FOOBAR', 'bar.foobar') ] proj.build('t/foobar', 'phony', inputs = Target.to_paths(foobar_tests)) # Peano peano_tests = [] peano_tests += [ ekore_test('t/peano', 'peano.ekore') ] peano_tests += [ ekore_test('t/peano', 'expected.ekore') ] -peano_tests += [ lang_test('t/peano', 'PEANO', 'two-plus-two.peano') ] +peano_tests += [ exec_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)) @@ -131,7 +131,7 @@ proj.build('t/peano', 'phony', inputs = Target.to_paths(peano_tests)) 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 += [ exec_test('t/imp-simple', 'IMP-SIMPLE', 'conjunction.imp') ] imp_tests += [ parse_test('t/imp-simple', 'imp-simple.k', 'conjunction.imp') ] proj.build('t/imp-simple', 'phony', inputs = Target.to_paths(imp_tests)) From e2b760abd9993939f3b4246638abeac2b3a99b65 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Thu, 15 Aug 2019 23:41:31 +0530 Subject: [PATCH 06/10] configuration: improve formatting --- src/kink.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/kink.md b/src/kink.md index 6607f88..df02fa5 100644 --- a/src/kink.md +++ b/src/kink.md @@ -35,14 +35,14 @@ module KINK-CONFIGURATION syntax DeclarationsCellFragment configuration #parseCommandLine($COMMANDLINE:CommandLine, $PGM:Any) - .Patterns - - .Patterns + + #token("UNNAMED", "ModuleName"):ModuleName .Patterns - nullDecl + nullDecl .Set From 3d44cef3ad09689d4b86630f52c81e6d4a5909e2 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Thu, 15 Aug 2019 23:50:17 +0530 Subject: [PATCH 07/10] Rename imp-simple to expressions --- build | 14 +++++++------- t/{imp-simple => expressions}/expected.ekore | 2 +- .../expressions.ekore} | 2 +- .../imp-simple.k => expressions/expressions.k} | 2 +- .../programs/conjunction.exp} | 0 .../programs/conjunction.exp.expected} | 0 .../programs/conjunction.exp.kast} | 0 7 files changed, 10 insertions(+), 10 deletions(-) rename t/{imp-simple => expressions}/expected.ekore (99%) rename t/{imp-simple/imp-simple.ekore => expressions/expressions.ekore} (99%) rename t/{imp-simple/imp-simple.k => expressions/expressions.k} (98%) rename t/{imp-simple/programs/conjunction.imp => expressions/programs/conjunction.exp} (100%) rename t/{imp-simple/programs/conjunction.imp.expected => expressions/programs/conjunction.exp.expected} (100%) rename t/{imp-simple/programs/conjunction.imp.kast => expressions/programs/conjunction.exp.kast} (100%) diff --git a/build b/build index 28566e0..35a34d5 100755 --- a/build +++ b/build @@ -127,12 +127,12 @@ peano_tests += [ exec_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 += [ exec_test('t/imp-simple', 'IMP-SIMPLE', 'conjunction.imp') ] -imp_tests += [ parse_test('t/imp-simple', 'imp-simple.k', 'conjunction.imp') ] -proj.build('t/imp-simple', 'phony', inputs = Target.to_paths(imp_tests)) +# Expressions +exp_tests = [] +exp_tests += [ ekore_test('t/expressions', 'expressions.ekore') ] +exp_tests += [ ekore_test('t/expressions', 'expected.ekore') ] +exp_tests += [ exec_test('t/expressions', 'EXPRESSIONS', 'conjunction.exp') ] +exp_tests += [ parse_test('t/expressions', 'expressions.k', 'conjunction.exp') ] +proj.build('t/expressions', 'phony', inputs = Target.to_paths(exp_tests)) proj.main() diff --git a/t/imp-simple/expected.ekore b/t/expressions/expected.ekore similarity index 99% rename from t/imp-simple/expected.ekore rename to t/expressions/expected.ekore index ee95699..6c5aa15 100644 --- a/t/imp-simple/expected.ekore +++ b/t/expressions/expected.ekore @@ -26,7 +26,7 @@ module D-K import C-INJ [ ] endmodule [ ] -module IMP-SIMPLE +module EXPRESSIONS axiom { } \rewrites { ImpCell { } } ( \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( False { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) , \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExpResult { } , KItem { } } ( False { } ( ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) ) [ ] axiom { } \rewrites { ImpCell { } } ( \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) , \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) ) [ ] axiom { } \rewrites { ImpCell { } } ( \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( Bracket { } ( VarB : BExp { } ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) , \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) ) [ ] diff --git a/t/imp-simple/imp-simple.ekore b/t/expressions/expressions.ekore similarity index 99% rename from t/imp-simple/imp-simple.ekore rename to t/expressions/expressions.ekore index 5b63280..a93ac7e 100644 --- a/t/imp-simple/imp-simple.ekore +++ b/t/expressions/expressions.ekore @@ -39,7 +39,7 @@ module D-K import C-INJ [] endmodule -module IMP-SIMPLE +module EXPRESSIONS import D-K [] syntax ImpCell ::= "" KCell ACell "" [klabel(impCell)] diff --git a/t/imp-simple/imp-simple.k b/t/expressions/expressions.k similarity index 98% rename from t/imp-simple/imp-simple.k rename to t/expressions/expressions.k index 11b1677..998b73f 100644 --- a/t/imp-simple/imp-simple.k +++ b/t/expressions/expressions.k @@ -1,4 +1,4 @@ -module IMP-SIMPLE +module EXPRESSIONS syntax Layout ::= r"(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" [klabel(layout)] syntax Pgm ::= ImpCell diff --git a/t/imp-simple/programs/conjunction.imp b/t/expressions/programs/conjunction.exp similarity index 100% rename from t/imp-simple/programs/conjunction.imp rename to t/expressions/programs/conjunction.exp diff --git a/t/imp-simple/programs/conjunction.imp.expected b/t/expressions/programs/conjunction.exp.expected similarity index 100% rename from t/imp-simple/programs/conjunction.imp.expected rename to t/expressions/programs/conjunction.exp.expected diff --git a/t/imp-simple/programs/conjunction.imp.kast b/t/expressions/programs/conjunction.exp.kast similarity index 100% rename from t/imp-simple/programs/conjunction.imp.kast rename to t/expressions/programs/conjunction.exp.kast From 751df60755c6854bd87cc9a024a43ad393c6f260 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Fri, 16 Aug 2019 01:21:27 +0530 Subject: [PATCH 08/10] Imp => Exp --- t/expressions/expected.ekore | 12 ++++----- t/expressions/expressions.ekore | 14 +++++------ t/expressions/expressions.k | 25 +++++++------------ t/expressions/programs/conjunction.exp | 5 ++-- .../programs/conjunction.exp.expected | 5 ++-- t/expressions/programs/conjunction.exp.kast | 2 +- 6 files changed, 27 insertions(+), 36 deletions(-) diff --git a/t/expressions/expected.ekore b/t/expressions/expected.ekore index 6c5aa15..dea2794 100644 --- a/t/expressions/expected.ekore +++ b/t/expressions/expected.ekore @@ -27,14 +27,14 @@ module D-K endmodule [ ] module EXPRESSIONS - axiom { } \rewrites { ImpCell { } } ( \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( False { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) , \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExpResult { } , KItem { } } ( False { } ( ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) ) [ ] - axiom { } \rewrites { ImpCell { } } ( \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) , \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) ) [ ] - axiom { } \rewrites { ImpCell { } } ( \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( Bracket { } ( VarB : BExp { } ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) , \and { ImpCell { } } ( \top { ImpCell { } } ( ) , impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) ) [ ] + axiom { } \rewrites { ExpCell { } } ( \and { ExpCell { } } ( \top { ExpCell { } } ( ) , expCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( False { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) , \and { ExpCell { } } ( \top { ExpCell { } } ( ) , expCell { } ( kCell { } ( kseq { } ( inj { BExpResult { } , KItem { } } ( False { } ( ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) ) [ ] + axiom { } \rewrites { ExpCell { } } ( \and { ExpCell { } } ( \top { ExpCell { } } ( ) , expCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , VarB : BExp { } ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) , \and { ExpCell { } } ( \top { ExpCell { } } ( ) , expCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) ) [ ] + axiom { } \rewrites { ExpCell { } } ( \and { ExpCell { } } ( \top { ExpCell { } } ( ) , expCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( Bracket { } ( VarB : BExp { } ) ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) , \and { ExpCell { } } ( \top { ExpCell { } } ( ) , expCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( VarB : BExp { } ) , DOTVAR : K { } ) ) , aCell { } ( AVal : BExpResult { } ) ) ) ) [ ] import D-K [ ] sort ACell { } [ ] sort BExp { } [ ] sort BExpResult { } [ ] - sort ImpCell { } [ ] + sort ExpCell { } [ ] sort KCell { } [ ] symbol And { } ( BExp { } , BExp { } ) : BExp { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] symbol Bracket { } ( BExp { } ) : BExp { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] @@ -42,7 +42,7 @@ module EXPRESSIONS symbol HOLE { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] symbol True { } ( ) : BExpResult { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] symbol aCell { } ( BExpResult { } ) : ACell { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] - symbol impCell { } ( KCell { } , ACell { } ) : ImpCell { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] + symbol expCell { } ( KCell { } , ACell { } ) : ExpCell { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] symbol kCell { } ( K { } ) : KCell { } [ functional { } ( ) , constructor { } ( ) , injective { } ( ) ] syntax ACell ::= "" BExpResult "" [ functional , constructor , injective , klabel ( aCell ) ] syntax BExp ::= "(" BExp ")" [ functional , constructor , injective , klabel ( Bracket ) ] @@ -51,7 +51,7 @@ module EXPRESSIONS syntax BExpResult ::= "#hole" [ functional , constructor , injective , klabel ( HOLE ) ] syntax BExpResult ::= "False" [ functional , constructor , injective , klabel ( False ) ] syntax BExpResult ::= "True" [ functional , constructor , injective , klabel ( True ) ] - syntax ImpCell ::= "" KCell ACell "" [ functional , constructor , injective , klabel ( impCell ) ] + syntax ExpCell ::= "" KCell ACell "" [ functional , constructor , injective , klabel ( expCell ) ] syntax KCell ::= "" K "" [ functional , constructor , injective , klabel ( kCell ) ] endmodule [ ] diff --git a/t/expressions/expressions.ekore b/t/expressions/expressions.ekore index a93ac7e..d9cd9b5 100644 --- a/t/expressions/expressions.ekore +++ b/t/expressions/expressions.ekore @@ -42,7 +42,7 @@ endmodule module EXPRESSIONS import D-K [] - syntax ImpCell ::= "" KCell ACell "" [klabel(impCell)] + syntax ExpCell ::= "" KCell ACell "" [klabel(expCell)] syntax KCell ::= "" K "" [klabel(kCell)] syntax ACell ::= "" BExpResult "" [klabel(aCell)] @@ -53,10 +53,10 @@ module EXPRESSIONS | "(" BExp ")" [klabel(Bracket)] | BExp "&&" BExp [klabel(And)] - rule impCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(True{}()),VarB:BExp{})),DOTVAR:K{})), aCell {} ( AVal:BExpResult {})) - => impCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}}(VarB:BExp{}),DOTVAR:K{})), aCell {} ( AVal:BExpResult {})) - rule impCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(False{}()),VarB:BExp{})),DOTVAR:K{})), aCell {} ( AVal:BExpResult {})) - => impCell{}(kCell{}(kseq{}(inj{BExpResult{}, KItem{}}(False{}()),DOTVAR:K{})), aCell {} ( AVal:BExpResult {})) - rule impCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}} (Bracket{}(VarB:BExp{})), DOTVAR:K {})), aCell {} ( AVal:BExpResult {})) - => impCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}} (VarB:BExp{}), DOTVAR:K {})), aCell {} ( AVal:BExpResult {})) + rule expCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(True{}()),VarB:BExp{})),DOTVAR:K{})), aCell {} ( AVal:BExpResult {})) + => expCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}}(VarB:BExp{}),DOTVAR:K{})), aCell {} ( AVal:BExpResult {})) + rule expCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(inj{BExpResult{},BExp{}}(False{}()),VarB:BExp{})),DOTVAR:K{})), aCell {} ( AVal:BExpResult {})) + => expCell{}(kCell{}(kseq{}(inj{BExpResult{}, KItem{}}(False{}()),DOTVAR:K{})), aCell {} ( AVal:BExpResult {})) + rule expCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}} (Bracket{}(VarB:BExp{})), DOTVAR:K {})), aCell {} ( AVal:BExpResult {})) + => expCell{}(kCell{}(kseq{}(inj{BExp{}, KItem{}} (VarB:BExp{}), DOTVAR:K {})), aCell {} ( AVal:BExpResult {})) endmodule diff --git a/t/expressions/expressions.k b/t/expressions/expressions.k index 998b73f..060123f 100644 --- a/t/expressions/expressions.k +++ b/t/expressions/expressions.k @@ -1,40 +1,33 @@ module EXPRESSIONS syntax Layout ::= r"(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" [klabel(layout)] - syntax Pgm ::= ImpCell + syntax Pgm ::= ExpCell syntax K ::= KItem "~>" K [klabel(kseq)] | ".K" [klabel(dotk)] syntax KItem ::= BExp [klabel(inj)] - configuration + configuration $PGM:K - False:BExpResult - + - syntax ImpCell ::= "" KCell ACell "" [klabel(impCell)] + syntax ExpCell ::= "" KCell "" [klabel(expCell)] syntax KCell ::= "" K "" [klabel(kCell)] - syntax ACell ::= "" BExpResult "" [klabel(aCell)] syntax BExpResult ::= "True" [klabel(True)] | "False" [klabel(False)] - | "#hole" [klabel(HOLE)] syntax BExp ::= BExpResult [klabel(inj)] | "(" BExp ")" [klabel(Bracket)] | BExp "&&" BExp [klabel(And)] - syntax Statement ::= "a" ":=" BExp [klabel(assignToA)] - // rule True && B:BExp => B:BExp ... // rule False && B:BExp => False ... // rule B1 && B2 => B1 ~> #hole && B2 ... // rule ( B1 ) => B1 ... // -// rule -// a := B:BExpResult ~> REST -// _:BExpResult -// -// => +// rule +// B:BExpResult ~> REST +// +// => // REST -// B:BExpResult -// +// endmodule diff --git a/t/expressions/programs/conjunction.exp b/t/expressions/programs/conjunction.exp index 12348a7..7628614 100644 --- a/t/expressions/programs/conjunction.exp +++ b/t/expressions/programs/conjunction.exp @@ -1,4 +1,3 @@ - + True && ( False && True ) ~> .K - False - + diff --git a/t/expressions/programs/conjunction.exp.expected b/t/expressions/programs/conjunction.exp.expected index f4148dd..83cf6da 100644 --- a/t/expressions/programs/conjunction.exp.expected +++ b/t/expressions/programs/conjunction.exp.expected @@ -1,4 +1,3 @@ -impCell{}( +expCell{}( kCell{}(kseq{}(inj{BExpResult{}, KItem{}}(False{}()), dotk{}())), - aCell{}(False{}()) -) \ No newline at end of file +) diff --git a/t/expressions/programs/conjunction.exp.kast b/t/expressions/programs/conjunction.exp.kast index cefe3b2..b6c5270 100644 --- a/t/expressions/programs/conjunction.exp.kast +++ b/t/expressions/programs/conjunction.exp.kast @@ -1 +1 @@ -impCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , Bracket { } ( And { } ( inj { BExpResult { } , BExp { } } ( False { } ( ) ) , inj { BExpResult { } , BExp { } } ( True { } ( ) ) ) ) ) ) , dotk { } ( ) ) ) , aCell { } ( False { } ( ) ) ) +expCell { } ( kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( inj { BExpResult { } , BExp { } } ( True { } ( ) ) , Bracket { } ( And { } ( inj { BExpResult { } , BExp { } } ( False { } ( ) ) , inj { BExpResult { } , BExp { } } ( True { } ( ) ) ) ) ) ) , dotk { } ( ) ) ) ) From 97c08e93310f1f983c17e93a51928bd04ddccb78 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 28 Aug 2019 20:09:28 +0530 Subject: [PATCH 09/10] !!! t/expressions --- t/expressions/expressions.k | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/t/expressions/expressions.k b/t/expressions/expressions.k index 060123f..03e1244 100644 --- a/t/expressions/expressions.k +++ b/t/expressions/expressions.k @@ -30,4 +30,15 @@ module EXPRESSIONS // => // REST // + +// context HOLE:BExp && B:BExp +// => context HOLE:BExp && B:BExp ... +// => context HOLE:BExp && B:BExp ... +// => context (HOLE:BExp => HOLE:BExp) && B:BExp ... +// => context (HOLE:BExp => HOLE:BExp) && B:BExp ... +// => context (HOLE:BExp => HOLE:BExp) && B:BExp ... +// => context cooled = HOLE:BExp && B:BExp ... + frozen = FREEZER1&& B:BExp + heated = HOLE:BExp ~> FREEZER1&& B:BExp ... +// => HOLE:BExp && B:BExp ... endmodule From 0f79e725b55667a0b6d749e337a225ca73baefe1 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Wed, 28 Aug 2019 22:16:27 +0530 Subject: [PATCH 10/10] Minimal example for sort inference with subsorting --- sort-inf.k | 76 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ test | 31 ++++++++++++++++++++++ 2 files changed, 107 insertions(+) create mode 100644 sort-inf.k create mode 100644 test diff --git a/sort-inf.k b/sort-inf.k new file mode 100644 index 0000000..2ead7a3 --- /dev/null +++ b/sort-inf.k @@ -0,0 +1,76 @@ +module SORT-INF + imports INT + imports BOOL + imports MAP + + configuration + $PGM:Exp + .Map + + + // base syntax + syntax Sort ::= "int" | "exp" + + syntax Id ::= "x" | "y" + syntax Exp ::= Id | Int + | Exp "+" Exp [seqstrict] + | Exp "+i" Exp [seqstrict] + | Exp "ie" Exp [seqstrict] + + // Since we are evaluating expressions to their sorts: + syntax KResult ::= Sort + syntax Exp ::= Sort + + rule X:Id => ?S:Sort ... + (.Map => (X |-> ?S)) RHO + requires notBool(X in_keys(RHO)) + rule X:Id => S ... + ... X |-> S ... + + rule int => exp ... + rule exp + exp => exp ... + rule int ie exp => int ... + rule int +i int => int ... +endmodule + +/* +module SORT-INF + imports BOOL + imports MAP + imports STRING + + configuration + #init ~> $PGM:Pattern + .Map + + ?_:Prod + + + + syntax Sort ::= sort(String) + syntax Prod ::= inj(Sort, Sort) + | prod(String, Sort) + | prod(String, Sort, Sort) + | prod(String, Sort, Sort, Sort) + + syntax Id ::= "x" | "y" + syntax Pattern ::= Id + | appl1(String, Pattern) [seqstrict(2)] + | appl2(String, Pattern, Pattern) [seqstrict(2, 3)] + + syntax KItem ::= "#init" + rule #init => appl2("+", x, y) ... + _ + => prod("+", sort("exp"), sort("exp"), sort("exp")) + prod("+i", sort("int"), sort("int"), sort("int")) + + + syntax Pattern ::= Sort + syntax KResult ::= Sort + + rule X:Id => ?S:Sort ... + .Map => (X |-> ?S) ... + rule appl2(SYM, ARG1, ARG2) => RESULT ... + prod(SYM, RESULT, ARG1, ARG2) +endmodule +*/ diff --git a/test b/test new file mode 100644 index 0000000..d4046c8 --- /dev/null +++ b/test @@ -0,0 +1,31 @@ +//x + +x ie x +// x +i y +//x + y +//x < y +//appl2("+", x, y) + + + + x ie x +-> x ~> # ie x +-> ?S ~> # ie x + x |-> ?S +-> ?S ie x + x |-> ?S +-> x ~> ?S ie # + x |-> ?S + +// narrow with: int => exp +-> exp ~> int ie # + x |-> int + +-> int ie exp + x |-> int + +~> int + x |-> int [1] + +~> exp + x |-> int [2]