diff --git a/build b/build index e77e786..35a34d5 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,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() 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/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 diff --git a/t/expressions/expected.ekore b/t/expressions/expected.ekore new file mode 100644 index 0000000..dea2794 --- /dev/null +++ b/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 ::= "" 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 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 new file mode 100644 index 0000000..d9cd9b5 --- /dev/null +++ b/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 ::= "" KCell ACell "" [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)] + + 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 new file mode 100644 index 0000000..03e1244 --- /dev/null +++ b/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 + $PGM:K + + + syntax ExpCell ::= "" KCell "" [klabel(expCell)] + syntax KCell ::= "" K "" [klabel(kCell)] + + syntax BExpResult ::= "True" [klabel(True)] + | "False" [klabel(False)] + 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 ) => B1 ... +// +// rule +// B:BExpResult ~> REST +// +// => +// 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 diff --git a/t/expressions/programs/conjunction.exp b/t/expressions/programs/conjunction.exp new file mode 100644 index 0000000..7628614 --- /dev/null +++ b/t/expressions/programs/conjunction.exp @@ -0,0 +1,3 @@ + + True && ( False && True ) ~> .K + diff --git a/t/expressions/programs/conjunction.exp.expected b/t/expressions/programs/conjunction.exp.expected new file mode 100644 index 0000000..83cf6da --- /dev/null +++ b/t/expressions/programs/conjunction.exp.expected @@ -0,0 +1,3 @@ +expCell{}( + kCell{}(kseq{}(inj{BExpResult{}, KItem{}}(False{}()), dotk{}())), +) diff --git a/t/expressions/programs/conjunction.exp.kast b/t/expressions/programs/conjunction.exp.kast new file mode 100644 index 0000000..b6c5270 --- /dev/null +++ b/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 { } ( ) ) ) ) diff --git a/t/imp-simple/expected.ekore b/t/imp-simple/expected.ekore deleted file mode 100644 index 47ebf53..0000000 --- a/t/imp-simple/expected.ekore +++ /dev/null @@ -1,56 +0,0 @@ -[ ] - -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 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 { } ) ) ) ) [ ] - 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 deleted file mode 100644 index 2b1e81f..0000000 --- a/t/imp-simple/imp-simple.ekore +++ /dev/null @@ -1,54 +0,0 @@ -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 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{})),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{})) -endmodule diff --git a/t/imp-simple/imp-simple.k b/t/imp-simple/imp-simple.k deleted file mode 100644 index 65a21db..0000000 --- a/t/imp-simple/imp-simple.k +++ /dev/null @@ -1,15 +0,0 @@ -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 deleted file mode 100644 index 623fa12..0000000 --- a/t/imp-simple/programs/conjunction.imp +++ /dev/null @@ -1 +0,0 @@ - True && False ~> .K diff --git a/t/imp-simple/programs/conjunction.imp.expected b/t/imp-simple/programs/conjunction.imp.expected deleted file mode 100644 index 82aa1aa..0000000 --- a/t/imp-simple/programs/conjunction.imp.expected +++ /dev/null @@ -1 +0,0 @@ -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 deleted file mode 100644 index ebf5326..0000000 --- a/t/imp-simple/programs/conjunction.imp.kast +++ /dev/null @@ -1 +0,0 @@ -kCell { } ( kseq { } ( inj { BExp { } , KItem { } } ( And { } ( True { } ( ) , False { } ( ) ) ) , dotk { } ( ) ) ) 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]