[in-progress] Imp manual strictness

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,23 +116,23 @@ 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))
 
-# 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))
+# 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()

sort-inf.k

@@ -0,0 +1,76 @@
+module SORT-INF
+  imports INT
+  imports BOOL
+  imports MAP
+
+  configuration <sortInf>
+                  <k> $PGM:Exp </k>
+                  <sortEnv> .Map </sortEnv>
+                </sortInf>
+
+  // 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 <k> X:Id => ?S:Sort ... </k>
+       <sortEnv> (.Map => (X |-> ?S)) RHO </sortEnv>
+    requires notBool(X in_keys(RHO))
+  rule <k> X:Id => S ... </k>
+       <sortEnv> ... X |-> S ... </sortEnv>
+
+  rule <k> int => exp ... </k>
+  rule <k> exp + exp => exp ... </k>
+  rule <k> int ie exp => int ... </k>
+  rule <k> int +i int => int ... </k>
+endmodule
+
+/*
+module SORT-INF
+  imports BOOL
+  imports MAP
+  imports STRING
+
+  configuration <sortInf>
+                  <k> #init ~> $PGM:Pattern </k>
+                  <sortEnv> .Map </sortEnv>
+                  <prods>
+                    <prodx multiplicity="*" type="Set"> ?_:Prod </prodx>
+                  </prods>
+                </sortInf>
+
+  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 <k> #init => appl2("+", x, y) ... </k>
+       <prods> _
+            => <prodx> prod("+", sort("exp"), sort("exp"), sort("exp")) </prodx>
+               <prodx> prod("+i", sort("int"), sort("int"), sort("int")) </prodx>
+       </prods>
+
+  syntax Pattern ::= Sort
+  syntax KResult ::= Sort
+
+  rule <k> X:Id => ?S:Sort ... </k>
+       <sortEnv> .Map => (X |-> ?S) ... </sortEnv>
+  rule <k> appl2(SYM, ARG1, ARG2) => RESULT ... </k>
+       <prodx> prod(SYM, RESULT, ARG1, ARG2) </prodx>
+endmodule
+*/

src/kink.md

@@ -35,14 +35,14 @@ module KINK-CONFIGURATION
   syntax DeclarationsCellFragment
   configuration <k> #parseCommandLine($COMMANDLINE:CommandLine, $PGM:Any) </k>
                 <definition>
-                   <defnAttrs format="[ %2 ]%n"> .Patterns </defnAttrs>
-                   <modules format="%2%n">
-                     <mod format="module %2%i%n%4%n%5%n%d%n %i%dendmodule %3%n%n"
+                   <defnAttrs format="[ %2 ]"> .Patterns </defnAttrs>
+                   <modules format="%2">
+                     <mod format="%nmodule %2%i%4%5%n%d%nendmodule %3%n"
                           multiplicity="*" type="Set">
                        <name format="%2"> #token("UNNAMED", "ModuleName"):ModuleName </name>
                        <attributes format="[ %2 ]"> .Patterns </attributes>
                        <declarations format="%2">
-                         <decl format="%2%n" multiplicity="*" type="Set"> nullDecl </decl>
+                         <decl format="%n%2" multiplicity="*" type="Set"> nullDecl </decl>
                        </declarations>
                        <grammar> .Set </grammar>
                      </mod>

t/expressions/expected.ekore

@@ -0,0 +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  ) ]
+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 {  } (  ) ]
+endmodule [  ]
+
+module D-K
+  import B-KSEQ [  ]
+  import C-INJ [  ]
+endmodule [  ]
+
+module EXPRESSIONS
+  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 ExpCell {  } [  ]
+  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 expCell {  } ( KCell {  } , ACell {  } ) : ExpCell {  } [ functional {  } (  ) , constructor {  } (  ) , injective {  } (  ) ]
+  symbol kCell {  } ( K {  } ) : KCell {  } [ functional {  } (  ) , constructor {  } (  ) , injective {  } (  ) ]
+  syntax ACell ::= "<a>" BExpResult "</a>" [ 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 ExpCell ::= "<exp>" KCell ACell "</exp>" [ functional , constructor , injective , klabel ( expCell ) ]
+  syntax KCell ::= "<k>" K "</k>" [ functional , constructor , injective , klabel ( kCell ) ]
+endmodule [  ]
+

t/expressions/expressions.ekore

@@ -0,0 +1,62 @@
+module A-BASIC-K
+  sort K{} []
+  sort KItem{} []
+endmodule [ ]
+
+module B-KSEQ
+  import A-BASIC-K []
+
+  syntax K ::= KItem "~>" K [klabel(kseq)]
+  syntax K ::= ".K" [klabel(dotk)]
+
+  symbol append{}(K{}, K{}) : K{} [function{}()]
+
+  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 [ sortInjection{}() ]
+
+  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 EXPRESSIONS
+  import D-K []
+
+  syntax ExpCell ::= "<exp>" KCell ACell "</exp>"  [klabel(expCell)]
+  syntax KCell ::= "<k>" K "</k>"                  [klabel(kCell)]
+  syntax ACell ::= "<a>" BExpResult  "</a>"        [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)]
+
+  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

t/expressions/expressions.k

@@ -0,0 +1,44 @@
+module EXPRESSIONS
+  syntax Layout ::= r"(/\\*([^\\*]|(\\*+([^\\*/])))*\\*+/|//[^\n\r]*|[\\ \n\r\t])*" [klabel(layout)]
+  syntax Pgm ::= ExpCell
+
+  syntax K ::= KItem "~>" K                             [klabel(kseq)]
+                 | ".K"                                 [klabel(dotk)]
+  syntax KItem ::= BExp                                 [klabel(inj)]
+
+  configuration <exp>
+                  <k> $PGM:K </k>
+                </exp>
+
+  syntax ExpCell ::= "<exp>" KCell "</exp>"             [klabel(expCell)]
+  syntax KCell ::= "<k>" K "</k>"                       [klabel(kCell)]
+
+  syntax BExpResult ::= "True"                          [klabel(True)]
+                      | "False"                         [klabel(False)]
+  syntax BExp ::= BExpResult                            [klabel(inj)]
+                | "(" BExp ")"                          [klabel(Bracket)]
+                | BExp "&&" BExp                        [klabel(And)]
+
+//  rule <k> True  && B:BExp  => B:BExp ... </k>
+//  rule <k> False && B:BExp  => False ... </k>
+//  rule <k> B1 && B2 => B1 ~> #hole && B2 ... </k>
+//  rule <k> ( B1 ) => B1 ... </k>
+//
+//  rule <exp>
+//         <k> B:BExpResult  ~> REST </k>
+//       </exp>
+//    => <exp>
+//         <k> REST </k>
+//       </exp>
+
+//      context HOLE:BExp && B:BExp
+//  =>  context <exp> <k> HOLE:BExp && B:BExp ... </k> </exp>
+//  =>  context <exp> <k> HOLE:BExp && B:BExp ... </k> </exp>
+//  =>  context <exp> <k> (HOLE:BExp => HOLE:BExp) && B:BExp ... </k> </exp>
+//  =>  context <exp> <k> (HOLE:BExp => HOLE:BExp) && B:BExp ... </k> </exp>
+//  =>  context <exp> <k> (HOLE:BExp => HOLE:BExp) && B:BExp ... </k> </exp>
+//  =>  context cooled = <exp> <k> HOLE:BExp && B:BExp ... </k> </exp>
+                frozen = FREEZER1&& B:BExp
+                heated = <exp> <k> HOLE:BExp ~> FREEZER1&& B:BExp ... </k> </exp>
+//              =>  <exp> <k> HOLE:BExp && B:BExp ... </k> </exp>
+endmodule

t/expressions/programs/conjunction.exp

@@ -0,0 +1,3 @@
+<exp>
+  <k> True && ( False && True ) ~> .K </k>
+</exp>

t/expressions/programs/conjunction.exp.expected

@@ -0,0 +1,3 @@
+expCell{}(
+    kCell{}(kseq{}(inj{BExpResult{}, KItem{}}(False{}()), dotk{}())),
+)

t/expressions/programs/conjunction.exp.kast

@@ -0,0 +1 @@
+expCell { } ( kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( And {  } ( inj { BExpResult {  } , BExp {  } } ( True {  } (  ) )  , Bracket { } ( And { } ( inj { BExpResult {  } , BExp {  } } ( False {  } (  ) )  , inj { BExpResult {  } , BExp {  } } ( True {  } (  ) ) ) ) ) )  , dotk {  } (  )  )  ) )