diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs new file mode 100644 index 0000000..e22f859 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -0,0 +1,187 @@ +module Interpreter.Tests + +open NUnit.Framework +open FsUnit +open System +open System.IO + +open LambdaInterpreter + +let testFilesDir = "TestFiles" +let successfulCasesPath = Path.Join [|testFilesDir; "Successful"|] +let unsuccessfulCasesPath = Path.Join [|testFilesDir; "Unsuccessful"|] + +let successfulCasesSources = Directory.EnumerateFiles successfulCasesPath |> seq |> Seq.sort +let unsuccessfulCasesSources = Directory.EnumerateFiles unsuccessfulCasesPath |> seq |> Seq.sort + +let e = String.Empty + +let successfulCasesResults: Result list list = [ + [ // Test 1 + Ok "\\z.z"; + Ok "trololo"; + ]; + [ // Test 2 + Ok "ololo"; + Ok "a"; + Ok "\\V1.\\V2.V2 \\x.V2 x"; + Ok "\\V1.\\V2.V2 \\x.V2 x"; + Ok "\\V1.\\V2.V2 (\\x.V2) x"; + Ok "\\V1.\\V2.V2 (\\x.V2) x"; + Ok "\\x.\\y.\\x.x"; + ]; + [ // Test 3 + Ok "qwerty"; + Ok "ololo (A_ B_)"; + Ok "\\x.\\y.z \\x.y x"; + Ok "Mult (Sum \\P.P)"; + Ok "second third \\x.x first"; + Ok "second third"; + ]; + [ // Test 4 + Ok "x y"; + Ok "x"; + Ok "\\y'.y y'"; + Ok "(\\x.x x) (\\x.x x) (\\x.x x) \\x.x x"; + ]; + [ // Test 5 + Ok "\\y.ololo"; + Ok "snd"; + Ok "res"; + Ok "\\U.\\V.V \\x.U"; + Ok "\\left.\\right.left (\\x.x) right"; + Ok "\\x.\\y.\\z.z (z y x)"; + ]; + [ // Test 6 + Ok "a"; + Ok "\\a.\\b.b a"; + Ok "baz bar"; + ]; + [ // Test 7 + Ok "var"; + Ok "\\x.x"; + Ok "exitCode"; + Ok "helpMe"; + Ok "toClear"; + Ok "reset_vars"; + Ok "no_exit_1"; + ]; + [ // Test 8 + ]; + [ // Test 9 + Ok "U"; + Ok "V"; + Ok "\\f.f V U"; + Ok "V"; + Ok "U"; + ]; + [ // Test 10 + Ok "\\f.\\x.f (f x)"; + Ok "\\f.\\x.f (f (f x))"; + Ok "\\f.\\x.f (f (f x))"; + Ok "\\f.\\x.x"; + Ok "\\f.\\x.f (f (f (f (f x))))"; + Ok "\\f.\\x.f (f (f (f (f (f x)))))"; + Ok "\\f.\\x.x"; + Ok "\\f.\\x.f (f (f (f (f (f (f (f x)))))))"; + ]; + [ // Test 11 + Ok "\\f.\\x.f x"; + Ok "\\f.\\x.f x"; + Ok "\\f.\\x.f (f x)"; + Ok "\\f.\\x.f (f (f (f (f (f x)))))"; + Ok "\\f.\\x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))))))))))"; + ]; + [ // Test 12 + Ok "\\f.\\x.f x"; + Ok "\\f.\\x.f x"; + Ok "\\f.\\x.f (f x)"; + Ok "\\f.\\x.f (f (f x))"; + Ok "\\f.\\x.f (f (f (f (f x))))"; + Ok "\\f.\\x.f (f (f (f (f (f (f (f x)))))))"; + ]; +] + +let unsuccessfulCasesResults: Result list list = [ + [ // Test 1 + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Ok "res"; + ]; + [ // Test 2 + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + ]; + [ // Test 3 + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + ]; + [ // Test 4 + Ok "\\x.\\y.x"; + Ok "\\x.\\y.x"; + Error e; + Ok "bar"; + Ok "foo bar"; + ]; + [ // Test 5 + Error e; + Ok "(\\x.x x) \\x.x x"; + Ok "(\\x.x x) (\\x.x x) ((\\x.x x) \\x.x x) ((\\x.x x) \\x.x x)"; + ]; +] + +let successfulCases = + successfulCasesResults + |> Seq.zip successfulCasesSources + |> Seq.map (fun (file, res) -> file, res, false) + +let unsuccessfulCases = + unsuccessfulCasesResults + |> Seq.zip unsuccessfulCasesSources + |> Seq.map (fun (file, res) -> file, res, true) + +let testCases = Seq.append successfulCases unsuccessfulCases |> Seq.map TestCaseData + +let outputsMatch (actual: Result list) (expected: Result list) = + actual.Length = expected.Length && + Seq.zip actual expected + |> Seq.map (function + | Ok res1, Ok res2 -> res1 = res2 + | Error _, Error _ -> true + | Ok _, Error _ | Error _, Ok _ -> false + ) |> Seq.forall (( = ) true) + +[] +let testInterpreter (sourceFile: string, expectedOutput: Result list, shouldFail: bool) = + let interpreter = Interpreter.StartOnFile sourceFile + let output = interpreter.RunToEnd () |> Seq.toList + output |> outputsMatch expectedOutput |> should be True + (interpreter.SyntaxError || interpreter.MaxDepthExceeded) |> should equal shouldFail diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj index 382dfbf..b69b05c 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj @@ -6,7 +6,9 @@ false - + + + @@ -20,4 +22,9 @@ + + + Always + + \ No newline at end of file diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaTermTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaTermTests.fs deleted file mode 100644 index 5ff8ac6..0000000 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaTermTests.fs +++ /dev/null @@ -1,110 +0,0 @@ -module LambdaTerm.Tests - -open NUnit.Framework -open FsUnit - -let id var = Abstraction (var, Variable var) -let omega var = Abstraction (var, Application (Variable var, Variable var)) -let Omega var = Application (omega var, omega var) - -let terms = - [ - // No redexes - Variable "x"; - Application (Variable "x", Variable "y"); - Abstraction ("x", Variable "y"); - omega "x"; - - // Simple reduction - Application (omega "x", Variable "y"); - Application (Abstraction ("x", Variable "x"), Variable "z"); - Application (Abstraction ("x", Application (Variable "x", Variable "y")), Variable "z"); - Application (Abstraction ("x", Variable "y"), Omega "x"); - - // Inner reduction - Abstraction ("a", Application - (Abstraction ("b", Application (Variable "b", Variable "c")), - Variable "x")); - Application (Variable "x", Application - (Abstraction ("a", omega "y"), - Variable "z")); - - // Multiple variable substitution - Application (Application - (Abstraction ("a", Abstraction ("b", Application (Variable "a", Variable "b"))), - Variable "x"), Variable "y"); - Application (Application (Application - (Abstraction ("a", Abstraction ("b", Abstraction ("c", Variable "x"))), - Variable "y"), Variable "y"), Variable "y"); - - // Term substitution - Application (id "x", id "y"); - Abstraction ("a", Application - (Abstraction ("b", Application (Variable "a", Variable "b")), - id "x")); - Application (id "x", Application (Variable "x", Variable "y")); - Application - (Abstraction ("a", Abstraction ("b", Application (Variable "a", Variable "b"))), - id "x"); - - // Irreducible redex - Omega "z"; - Application (Omega "x", Omega "y"); - - // Alpha conversion required - Application - (Abstraction ("x", Abstraction ("y", Application (Variable "x", Variable "y"))), - Variable "y"); - Application - (Abstraction ("z'", Abstraction ("z", Application (Variable "z", Variable "z'"))), - Variable "z"); - Application - (Abstraction ("x", Application - (Abstraction ("y", Application (Variable "x", Variable "y")), - Variable "x")), - Abstraction ("y", Application (Variable "x", Variable "y"))); - Application - (Abstraction ("a", Abstraction ("b", - Abstraction ("c", Application (Variable "a", Variable "b")))), - Application (Variable "c", Variable "b")); - ] - -let reducedTerms = - [ - Variable "x"; - Application (Variable "x", Variable "y"); - Abstraction ("x", Variable "y"); - omega "x"; - - Application (Variable "y", Variable "y"); - Variable "z"; - Application (Variable "z", Variable "y"); - Variable "y"; - - Abstraction ("a", Application (Variable "x", Variable "c")); - Application (Variable "x", omega "y"); - - Application (Variable "x", Variable "y"); - Variable "x"; - - id "y"; - Abstraction ("a", Application(Variable "a", id "x")); - Application (Variable "x", Variable "y"); - id "b"; - - Omega "z"; - Application (Omega "x", Omega "y"); - - Abstraction ("y'", Application (Variable "y", Variable "y'")); - Abstraction ("z''", Application (Variable "z''", Variable "z")); - Application (Variable "x", Abstraction ("y", Application (Variable "x", Variable "y"))); - Abstraction ("b'", Abstraction ("c'", Application - (Application (Variable "c", Variable "b"), - Variable "b'"))); - ] - -let testCases = List.zip terms reducedTerms |> List.map TestCaseData - -[] -let testReduce term reducedTerm = - reduce term |> should equal reducedTerm diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs new file mode 100644 index 0000000..6d98546 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs @@ -0,0 +1,214 @@ +module Parser.Tests + +open NUnit.Framework +open FsUnit +open FParsec + +open LambdaInterpreter.Syntax +open Parser + +let runTest (testCases: (string * Parser<'a, unit> * int option) seq) = + for input, parser, expectedPos in testCases do + let result = input |> run parser + match result with + | Success (_, _, pos) -> pos.Index |> should equal expectedPos.Value + | _ -> expectedPos |> _.IsNone |> should be True + +[] +let testParser_WhiteSpace () = + [ + "", whitespaceOpt, Some 0; + "\t", whitespaceOpt, Some 1; + " \t\t ", whitespaceOpt, Some 6; + " \n", whitespaceOpt, Some 4; + "", whitespace, None; + " ", whitespace, Some 1; + "\n", whitespace, Some 1; + " \t\t a", whitespace, Some 8; + "a1", whitespace, None; + ] |> runTest + +[] +let testParser_InputEnd () = + [ + "", inputEnd, Some 0; + " ", inputEnd, Some 5; + "\n", inputEnd, Some 1; + " \n", inputEnd, Some 4; + "a12", inputEnd, None; + " 1 ", inputEnd, None; + ] |> runTest + +[] +let testParser_Variable () = + [ + "x", variable, Some 1; + "ab", variable, Some 2; + "RE0", variable, Some 3; + "ab_123", variable, Some 6; + "p33_", variable, Some 4; + "_nm", variable, None; + "100qwe", variable, None; + "ololo%", variable, Some 5; + " , ", variable, None; + "@test", variable, None; + "let", variable, None; + "letvar", variable, Some 6; + "not_a_let", variable, Some 9; + "exit", variable, None; + "display", variable, None; + ] |> runTest + +[] +let testParser_Variables () = + [ + "", variables, None; + "a", variables, Some 1; + "X Y Z", variables, Some 5; + "x1 x2 x3 x4", variables, Some 11; + "v_1 v_2 x_3", variables, Some 15; + "a _ b", variables, Some 2; + "1 2", variables, None; + " ololo ololo ", variables, Some 15; + "first, second", variables, Some 5; + "fst snd thd \t\n", variables, Some 18; + ] |> runTest + +[] +let testParser_Operand () = + [ + "var1", operand, Some 4; + "()", operand, None; + "(some_var)", operand, Some 10; + "( XYZ )", operand, Some 9; + "_not_a_var", operand, None; + "A B", operand, Some 1; + "((var)", operand, None; + "( ((ololo )) )", operand, Some 15; + "\\x.y", operand, None; + "(first second )", operand, Some 16; + "(\\u v w.v)", operand, Some 10; + "((\\x.x) i j)", operand, Some 12; + ] |> runTest + +[] +let testParser_Application () = + [ + "a", application, Some 1; + "(var_1)", application, Some 7; + "X Y", application, Some 3; + "( ololo ) (abc)", application, Some 15; + "a1 a2 a3", application, Some 14; + "(_xyz)", application, None; + "(var1) 2var", application, Some 6; + "(a b) c", application, Some 9; + "var (\\x.x z)", application, Some 12; + "( (\\A1 B2 C3.A1) ololo) var1", application, Some 30; + "var1 (var2) var3 \t ", application, Some 19; + "( \\x.x )", application, Some 8; + "left \\x.right ", application, Some 13; + ] |> runTest + +[] +let testParser_Abstraction () = + [ + "\\x.x", abstraction, Some 4; + "\\a b c.d", abstraction, Some 8; + "\\var1 var2.(var3)", abstraction, Some 20; + "\\_a.b", abstraction, None; + "abc.d", abstraction, None; + "\\x y z (k)", abstraction, None; + "\\x.\\y.\\z.x", abstraction, Some 10; + "\\first second.\\var.first second", abstraction, Some 31; + "\\x y z.x y z", abstraction, Some 12; + "\\ A B C. \t B (C A)", abstraction, Some 20; + "\\ u v . \\x. x v", abstraction, Some 19; + ] |> runTest + +[] +let testParser_Term () = + [ + "var1", term, Some 4; + "((ololo) )", term, Some 10; + "(\\x y.x)", term, Some 8; + "\\x y z.x z (y z)", term, Some 16; + "S K K ", term, Some 7; + "((\\a.a) tmp) (\\x.\\y.\\z.y z x)", term, Some 32; + "(term))", term, Some 6; + "\\x.\\y", term, None; + "_q", term, None; + "a, b, c", term, Some 1; + "\\X Y Z.Z \\t.X Y", term, Some 16; + "( \\ a b . z)", term, Some 14; + "\\U. U (\\x.x) V", term, Some 14; + ] |> runTest + +[] +let testParser_Declaration () = + [ + "let VAR", declaration, Some 7; + "let", declaration, None; + "olet a", declaration, None; + " let xy", declaration, None; + "let tmp", declaration, Some 10; + "foo", declaration, None; + "bar ololo", declaration, None; + "let let", declaration, None; + "let help", declaration, None; + "let exitCode", declaration, Some 12; + ] |> runTest + +[] +let testParser_Definition () = + [ + "let a = b", definition, Some 9; + "let tmp = x y z", definition, Some 17; + "let ololo", definition, None; + " let var1 = var2", definition, None; + "let A B", definition, None; + "let x != y", definition, None; + "foo bar = baz", definition, None; + "let v1 = v2", definition, Some 16; + "let term = ", definition, None; + "let let = X Y Z", definition, None; + "let clear = I x x", definition, None; + ] |> runTest + +[] +let testParser_Command () = + [ + "reset", command, Some 5; + "display", command, Some 7; + "help", command, Some 4; + "clear", command, Some 5; + "exit", command, Some 4; + "not_help", command, None; + "exitCode", command, Some 4; + " clear", command, None; + "exit \t ", command, Some 4; + "reset vars", command, Some 5; + ] |> runTest + +[] +let testParser_Expression () = + [ + "let S = \\x y z.x z (y z)\n", expression, Some 25; + "let K = \\x y.x", expression, Some 15; + "S K K \t\n", expression, Some 8; + "let tmp = (\\x y z.some ( \\k.y z) x ) var", expression, Some 42; + "\n", expression, Some 1; + " \n", expression, Some 8; + " let I = \\x.x", expression, None; + "_wewq", expression, None; + "123\n", expression, None; + "", expression, Some 0; + "variable", expression, Some 8; + "let test = (\\x.x) y, ", expression, None; + "help \t", expression, Some 7; + "clear buff", expression, None; + "let ololo_exit = (\\x.\\y.x ) z\n", expression, Some 30; + "a clear", expression, None; + "\n exit", expression, None; + "let var = \\x.x \\y.y", expression, Some 20; + "\\A B.A \\x.B \t", expression, Some 14; + ] |> runTest diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs new file mode 100644 index 0000000..6138b22 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs @@ -0,0 +1,146 @@ +module Reduction.Tests + +open NUnit.Framework +open FsUnit + +open LambdaInterpreter +open LambdaInterpreter.Syntax +open AST + +let var = Name >> Variable + +let I = Abstraction (Name "x", var "x") +let omega = Abstraction (Name "x", Application (var "x", var "x")) +let Omega = Application (omega, omega) +let T = Abstraction (Name "x", Abstraction (Name "y", var "x")) +let F = Abstraction (Name "x", Abstraction (Name "y", var "y")) +let y = Abstraction (Name "x", Application (var "f", Application (var "x", var "x"))) +let Y = Abstraction (Name "f", Application (y, y)); + +let terms = + [ + // No redexes + var "x"; + Application (var "x", var "y"); + Abstraction (Name "x", var "y"); + omega; + + // Simple reduction + Application (omega, var "y"); + Application (Abstraction (Name "x", var "x"), var "z"); + Application (Abstraction (Name "x", Application (var "x", var "y")), var "z"); + Application (Abstraction (Name "x", var "y"), Omega); + + // Inner reduction + Abstraction (Name "a", Application (Abstraction (Name "b", Application (var "b", var "c")), var "x")); + Application (var "x", Application (Abstraction (Name "a", omega), var "z")); + + // Multiple variable substitution + Application (Application + (Abstraction (Name "a", Abstraction (Name "b", Application (var "a", var "b"))), + var "x"), + var "y"); + Application (Application (Application + (Abstraction (Name "a", Abstraction (Name "b", Abstraction (Name "c", var "x"))), + var "y"), + var "y"), + var "y"); + Application (Application (Application + (Abstraction (Name "U", Abstraction (Name "V", Abstraction (Name "W", + Abstraction (Name "H", Abstraction (Name "K", var "W"))))), + var "a"), + var "b"), + var "c"); + Application (var "trololo", + Application (Application + (Abstraction (Name "x", Abstraction (Name "y", var "x")), + var "A"), + var "B")); + + // Term substitution + Application (I, I); + Abstraction (Name "a", Application (Abstraction (Name "b", Application (var "a", var "b")), I)); + Application (I, Application (var "x", var "y")); + Application (Abstraction (Name "a", Abstraction (Name "b", Application (var "a", var "b"))), I); + + // Nested redex + Application (Application (I, Abstraction (Name "x", var "z")), Y); + Application (Y, F); + Application (var "S", Application (Application (Application (T, var "a"), var "b"), var "S")); + Application (Application (I, Application (Application (F, var "x"), I)), var "y"); + + // Irreducible redex + Omega; + Application (Omega, Omega); + + // Alpha conversion required + Application + (Abstraction (Name "x", Abstraction (Name "y", Application (var "x", var "y"))), + var "y"); + Application + (Abstraction (Name "z'", Abstraction (Name "z", Application (var "z", var "z'"))), + var "z"); + Application + (Abstraction (Name "x", Application + (Abstraction (Name "y", Application (var "x", var "y")), + var "x")), + Abstraction (Name "y", Application (var "x", var "y"))); + Application + (Abstraction (Name "a", Abstraction (Name "b", + Abstraction (Name "c", Application (var "a", var "b")))), + Application (var "c", var "b")); + ] + +let reducedTerms = + [ + // No redexes + var "x"; + Application (var "x", var "y"); + Abstraction (Name "x", var "y"); + omega; + + // Simple reduction + Application (var "y", var "y"); + var "z"; + Application (var "z", var "y"); + var "y"; + + // Inner reduction + Abstraction (Name "a", Application (var "x", var "c")); + Application (var "x", omega); + + // Multiple variable substitution + Application (var "x", var "y"); + var "x"; + Abstraction (Name "H", Abstraction (Name "K", var "c")); + Application (var "trololo", var "A"); + + // Term substitution + I; + Abstraction (Name "a", Application (var "a", I)); + Application (var "x", var "y"); + Abstraction (Name "b", var "b"); + + // Nested redex + var "z"; + Abstraction (Name "y", var "y"); + Application (var "S", Application (var "a", var "S")); + var "y"; + + // Irreducible redex + Omega; + Application (Omega, Omega); + + // Alpha conversion required + Abstraction (Name "y'", Application (var "y", var "y'")); + Abstraction (Name "z''", Application (var "z''", var "z")); + Application (var "x", Abstraction (Name "y", Application (var "x", var "y"))); + Abstraction (Name "b'", Abstraction (Name "c'", Application (Application (var "c", var "b"), var "b'"))); + ] + +let testCases = List.zip terms reducedTerms |> List.map TestCaseData + +[] +let testReduce term reducedTerm = + let reducer = new Reducer () + reducer.Reduce term |> should equal reducedTerm diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test01.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test01.txt new file mode 100644 index 0000000..37954c8 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test01.txt @@ -0,0 +1,8 @@ +let S = \x y z.x z (y z) +let K = \x y.x +S K K + +let z = trololo +let tmp = \x.z +let z = a +tmp z \ No newline at end of file diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test02.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test02.txt new file mode 100644 index 0000000..d6e238c --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test02.txt @@ -0,0 +1,13 @@ + +let I = \x.x + +I ololo + +let var = I a +var + +\V1 V2.V2 \x.V2 x +\V1 V2.V2 (\x.V2 x) +\V1 V2.(V2 \x.V2) x +\V1 V2.V2 (\x.V2) x +\x.\y.\x.x diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test03.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test03.txt new file mode 100644 index 0000000..3f75ba1 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test03.txt @@ -0,0 +1,15 @@ +qwerty +ololo (A_ B_) +\x.\y. z (\x.y x) +Mult (Sum (\P.P) ) + +let foo = \A B C.B C (\x.x A ) +let td = \a1 a2 a3.a3 + +let a1 = first +let a2 = second +let a3 = third +foo a1 a2 a3 + +let bar = td foo a1 a2 a3 +bar diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test04.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test04.txt new file mode 100644 index 0000000..72e2014 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test04.txt @@ -0,0 +1,10 @@ +x y + +let x = \z.x +x y + +(\x y.x y) y + +let o = \x. x x +let E = \ y. y y y y +E o \ No newline at end of file diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test05.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test05.txt new file mode 100644 index 0000000..f63a210 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test05.txt @@ -0,0 +1,13 @@ +let fst = \x y.x +let snd = \fst.\snd.snd +let res = (snd a fst) ololo +res +reset + +snd +res + +let baz = \ U V. V \x. U +baz +\left right. left (\x.x) right +\ x y z . (\t.z) (\t.x) ((z y ) x) \ No newline at end of file diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test06.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test06.txt new file mode 100644 index 0000000..e536b53 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test06.txt @@ -0,0 +1,12 @@ +let I = \x.x +I a +let foo = \ a b . b (I a) +foo + +let temp = foo bar baz +temp + +exit + +( a b) c d +I diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test07.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test07.txt new file mode 100644 index 0000000..36db00e --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test07.txt @@ -0,0 +1,11 @@ +help +clear +var +reset +\x.x + +exitCode +helpMe +toClear +reset_vars +no_exit_1 diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test08.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test08.txt new file mode 100644 index 0000000..e69de29 diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test09.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test09.txt new file mode 100644 index 0000000..7843805 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test09.txt @@ -0,0 +1,12 @@ +let pair = \a b f.f a b +let T = \ x . \ y . x +let F = \ x . \ y . y +let fst = \p.p T +let snd = \p.p F +let swap = \p.pair (snd p) (fst p) + +fst (pair U V) +snd (pair U V) +swap (pair U V) +fst (swap (pair U V)) +snd (swap (pair U V)) \ No newline at end of file diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test10.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test10.txt new file mode 100644 index 0000000..0e6a371 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test10.txt @@ -0,0 +1,21 @@ +let NUM_0 = \f.\x.x +let NUM_1 = \f.\x.f x +let NUM_2 = \f.\x.f (f x) +let NUM_3 = \f.\x.f (f (f x)) +let NUM_4 = \f.\x.f (f (f (f x))) + +let SUCC = \n f x.f (n f x) +let PRED = \n f x.n (\g h.h (g f)) (\u.x) \u.u + +let SUM = \m n f x.m f (n f x) +let MUL = \m n f.m (n f) + +SUCC NUM_1 +SUCC NUM_2 +PRED NUM_4 +PRED NUM_0 + +SUM NUM_2 NUM_3 +SUM (SUCC NUM_2) (PRED NUM_4) +MUL NUM_0 NUM_3 +MUL NUM_2 (SUCC NUM_3) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test11.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test11.txt new file mode 100644 index 0000000..40699b8 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test11.txt @@ -0,0 +1,23 @@ +let TRUE = \x y.x +let FALSE = \x y.y +let IF = \b t f.b t f + +let ZERO = \f.\x.x +let ONE = \f.\x.f x +let TWO = \f.\x.f (f x) +let THREE = \f.\x.f (f (f x)) +let FOUR = \f.\x.f (f (f (f x))) + +let IS_ZERO = \f.f (\t.FALSE) TRUE +let PRED = \n f x.n (\g h.h (g f)) (\u.x) \u.u +let MUL = \m n f.m (n f) + +let Y = \f.(\x.f (x x)) (\x.f (x x)) +let STEP = \f n.IF (IS_ZERO n) ONE (MUL n (f (PRED n))) +let FACT = Y STEP + +FACT ZERO +FACT ONE +FACT TWO +FACT THREE +FACT FOUR diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test12.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test12.txt new file mode 100644 index 0000000..adb5915 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test12.txt @@ -0,0 +1,25 @@ +let zero = \f x. x +let one = \f x. f x +let two = \f x. f (f x) +let three = \f x. f (f (f x)) +let four = \f x. f (f (f (f x))) +let five = \f x. f (f (f (f (f x)))) + +let true = \x y. x +let false = \x y. y +let if = \b t f. b t f + +let is_zero = \n. n (\t.false) true +let pred = \n f x. n (\g h. h (g f)) (\u. x) \u. u +let sum = \m n f x. m f (n f x) + +let Y = \f. (\x. f (x x)) (\x. f (x x)) +let step = \f n. if (is_zero n) one (if (is_zero (pred n)) one (sum (f (pred n)) (f (pred (pred n))))) +let fib = Y step + +fib zero +fib one +fib two +fib three +fib four +fib five diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test01.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test01.txt new file mode 100644 index 0000000..2527c4d --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test01.txt @@ -0,0 +1,13 @@ +\x y z u v +a1 b2 c3.a1 +\ .x y +\.Z + +let = ololo +let var = +let + +tmp = X Y +let U V = W + +res \ No newline at end of file diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test02.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test02.txt new file mode 100644 index 0000000..eb07c8b --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test02.txt @@ -0,0 +1,13 @@ +let let = a +let reset = B +let display = trololo +let help = Q +let clear = P +let exit = ololo + +\x y.\z.y (exit z) +a help +test let +clear ( a b c) +exit ooo +to display diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test03.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test03.txt new file mode 100644 index 0000000..9013f1b --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test03.txt @@ -0,0 +1,15 @@ + let x = y + A1 B2 C3 + +_a +42_ +some^var +*ololo +let err = (\x.x 123) +let J = U V _W + +let qwerty = () + exit +((var) +(a)()(b)(c) +(test)))) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test04.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test04.txt new file mode 100644 index 0000000..0449951 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test04.txt @@ -0,0 +1,15 @@ +let fst = \ x y . x +let I = \ x. x +I fst +(fst) + +let foo = fst I ololo + +() + +foo bar + +clear +reset + +foo bar diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test05.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test05.txt new file mode 100644 index 0000000..d5223ce --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test05.txt @@ -0,0 +1,7 @@ +let e = \x.x x x +\Z.e e + +let o = \x.x x +let O = o o +O +O O O diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs new file mode 100644 index 0000000..41ab13b --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs @@ -0,0 +1,24 @@ +namespace LambdaInterpreter.Console + +open System +open LambdaInterpreter + +/// Module containing utility regarding the console output color. +module ColorScheme = + + /// Color of messages signaling of success. + type SuccessColor = Color of ConsoleColor + + /// Color of messages signaling of error. + type ErrorColor = Color of ConsoleColor + + /// Color scheme of the console application. + type ColorScheme = SuccessColor * ErrorColor + + /// Default color of messages signaling of error. + let defaultErrorColor = ConsoleColor.Red + + /// Get the color scheme of the app according to the state of the given `interpreter`. + let getColorScheme (interpreter: Interpreter) = + if interpreter.IsInteractive then Color ConsoleColor.Green, Color ConsoleColor.Yellow + else Color ConsoleColor.Green, Color ConsoleColor.Red diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs new file mode 100644 index 0000000..54c99a1 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs @@ -0,0 +1,31 @@ +namespace LambdaInterpreter.Console + +open LambdaInterpreter + +/// Module containing utility regarding the exit code of the app. +module ExitCode = + + /// Enum representing the exit code of the app. + type ExitCode = + + /// The program execution was successful. + | Success = 0 + + /// The given command line arguments are invalid. + | InvalidArguments = 1 + + /// The given source file was not found. + | FileNotFound = 2 + + /// A syntax error occurred during source file interpretation. + | SyntaxError = 3 + + /// Max allowed depth of recursion exceeded during the source file term reduction. + | MaxDepthExceeded = 4 + + /// Get the exit code of the program according to the state of the given `interpreter`. + let getExitCode (interpreter: Interpreter) = + if interpreter.IsInteractive then ExitCode.Success else + if interpreter.SyntaxError then ExitCode.SyntaxError else + if interpreter.MaxDepthExceeded then ExitCode.MaxDepthExceeded else + ExitCode.Success diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Help.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Help.fs new file mode 100644 index 0000000..cac2fec --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Help.fs @@ -0,0 +1,43 @@ +namespace LambdaInterpreter.Console + +open System +open LambdaInterpreter.Syntax + +/// Module for displaying command line help. +module Help = + + /// Message to print when failed to interpret the given command line arguments. + let invalidArgsMessage = + $"Invalid command line arguments provided. For more info use '{Array.last Options.HelpArgs}' option." + + /// Print header with general info about the app. + let printHeader () = + printfn " +Lambda Interpreter +------------------ +An interactive lambda term interpreter." + + /// Print help suggestion with a corresponding command to the console. + let printHelpSuggestion () = + printfn $" +Type '{Keywords.HelpKeyword}' for more info. +" + + /// Print command line usage help to the console. + let printUsageHelp () = + printfn " +It can either be run interactively using the standard input, +or on a specified source file. + +Usage: LambdaInterpreter [path-to-file] [options]" + + /// Print command line options help to the console. + let printOptionsHelp () = + printfn $" +Options: + {String.Join ('|', Options.HelpArgs)}\t\t Display help and exit + {String.Join ('|', Options.VerboseArgs)}\t Print detailed interpretation info + {String.Join ('|', Options.LineNumberArgs)}\t Print line number with output" + + /// Print syntax help to the console. + let printSyntaxHelp () = Help.printSyntaxHelp () diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Options.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Options.fs new file mode 100644 index 0000000..e52ef3a --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Options.fs @@ -0,0 +1,51 @@ +namespace LambdaInterpreter.Console + +open System + +/// Struct for managing command line options. +type Options private (sourceFile: string option, + help: bool, + verbose: bool, + lineNumber: bool, + error: bool) = + struct + /// Command line arguments for displaying help. + static member HelpArgs: string array = [|"-h"; "--help"|] + + /// Command line arguments for printing detailed output to the console. + static member VerboseArgs: string array = [|"-v"; "--verbose"|] + + /// Command line arguments for printing source file line number with output. + static member LineNumberArgs: string array = [|"-n"; "--line-number"|] + + /// A path of the source file to run the interpreter on. + member _.SourceFile: string option = sourceFile + + /// Whether to display command line help. + member _.Help: bool = help + + /// Whether to print detailed output to the console. + member _.Verbose: bool = verbose + + /// Whether to print source file line number with output. + member _.LineNumber: bool = lineNumber + + /// Whether the given command line arguments are invalid. + member _.Error: bool = error + + /// Get options from command line arguments. + static member GetFromArgs (): Options = + + /// Get difference of `source` with `target` with a value indicating their intersection. + let removeMany source target = + let result = target |> Set |> Set.difference source + result, result <> source + + let args = Environment.GetCommandLineArgs () |> Array.removeAt 0 |> Set + let args, help = removeMany args Options.HelpArgs + let args, verbose = removeMany args Options.VerboseArgs + let args, lineNumber = removeMany args Options.LineNumberArgs + let sourceFile = if args.Count = 1 then Some (Set.minElement args) else None + let error = args.Count > 1 + new Options (sourceFile, help, verbose, lineNumber, error) + end diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs new file mode 100644 index 0000000..1545ecd --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -0,0 +1,113 @@ +namespace LambdaInterpreter + +open System +open System.IO +open FParsec + +open LambdaInterpreter.Syntax +open AST +open Parser + +/// Class representing the lambda term interpreter. +type Interpreter private (stream: Stream, interactive: bool, ?verbose: bool, ?lineNumber: bool) = + let reader = new StreamReader (stream) + let reducer = new Reducer (?verbose=verbose) + let lineNumber = defaultArg lineNumber false + + let mutable currentLine = 0 + let mutable syntaxError = false + let mutable maxDepthExceeded = false + + /// Print a pointer indicating the start of input when running an interactive interpreter. + let tryPrintInputPointer () = + if interactive then printf "%s" Help.InputPointer + + /// Add current line number to the given string when running on a source file. + let tryAddCurrentLine str = + if lineNumber then $"[Line {currentLine}] {str}" else str + + /// Create an interactive interpreter for the standard console input. + /// Use `verbose` option to print logs to the console. + static member StartInteractive (?verbose: bool): Interpreter = + new Interpreter (Console.OpenStandardInput (), true, ?verbose=verbose) + + /// Create an interpreter to run on a source file at the given `path`. + /// Use `verbose` option to print logs to the console. + /// Use `lineNumber` option to add line number to the output. + static member StartOnFile (path: string, ?verbose: bool, ?lineNumber: bool): Interpreter = + new Interpreter (File.OpenRead path, false, ?verbose=verbose, ?lineNumber=lineNumber) + + /// Whether the interpreter is being run in console. + member _.IsInteractive: bool = interactive + + /// Whether the current state of the interpreter supports running. + member _.CanRun: bool = if interactive then stream.CanRead + else stream.CanRead && not reader.EndOfStream + + /// Whether a syntax error occurred during the interpretation. + member _.SyntaxError: bool = syntaxError + + /// Whether max allowed depth of recursion exceeded during the term reduction. + member _.MaxDepthExceeded: bool = maxDepthExceeded + + /// Run the interpreter while possible and yield the interpretation results. + member self.RunToEnd (): Result seq = + seq { + while self.CanRun do + let result = self.RunOnNextLineAsync () |> Async.RunSynchronously + match result with + | Some output -> yield output + | None -> () + } + + /// Analyze the next line in the stream and get the interpretation result. + member private _.RunOnNextLineAsync (): Async option> = + + /// Execute the given special interpreter `command`. + let runCommand (command: SpecialCommand) = + match command with + | Reset -> reducer.ResetDefinitions () + | Display -> if interactive then reducer.DisplayDefinitions () + | Help -> if interactive then Help.printSyntaxHelp () + | Clear -> if interactive then Console.Clear () + | Exit -> reader.Close () + None + + /// Interpret the given `primary` expression representation. + let interpretExpression (primary: Primary.Expression) = + match buildExpressionAST primary with + | Definition (var, term) -> + reducer.AddDefinition (var, term) + None + | Result term -> + try reducer.Reduce term + |> toString + |> tryAddCurrentLine + |> Result.Ok + |> Some + with :? StackOverflowException as ex -> + maxDepthExceeded <- true + ex.Message |> tryAddCurrentLine |> Result.Error |> Some + | Command command -> runCommand command + | Empty -> None + + async { + currentLine <- currentLine + 1 + tryPrintInputPointer () + let! line = reader.ReadLineAsync () |> Async.AwaitTask + let parserResult = line |> run expression + return + match parserResult with + | Success (expr, _, _) -> interpretExpression expr + | Failure (msg, _, _) -> + syntaxError <- true + msg |> tryAddCurrentLine |> Result.Error |> Some + } + + interface IDisposable with + + /// Free resources used by the interpreter. + member _.Dispose () = reader.Dispose () + + /// Free resources used by the interpreter. + member _.Dispose () = reader.Dispose () diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj index 60a9a0b..2eb226f 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -2,11 +2,29 @@ net9.0 + Exe true + true - + + + + + + + + + + + + + + + + + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaTerm.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaTerm.fs deleted file mode 100644 index 3f424d3..0000000 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaTerm.fs +++ /dev/null @@ -1,58 +0,0 @@ -module LambdaTerm - -/// Use strings as variables in lambda terms. -type Variable = string - -/// The definition of lambda term. -type LambdaTerm = - | Variable of Variable - | Abstraction of Variable * LambdaTerm - | Application of LambdaTerm * LambdaTerm - -/// Gets free variables of the given lambda `term`. -let rec freeVars term = - match term with - | Variable v -> set [v] - | Abstraction (v, term) -> Set.remove v (freeVars term) - | Application (left, right) -> - Set.union (freeVars left) (freeVars right) - -/// Gets a variable, starting with `prefix`, that is not in `freeVars`. -let rec nextFreeVar prefix freeVars = - if not (Set.contains prefix freeVars) then prefix - else nextFreeVar (prefix + "'") freeVars - -/// Substitutes free occurrences of variable `var` in `term` with given term `sub`. -/// Performs alpha-conversion if necessary. -let rec substitute term var sub = - match term with - | Variable x when x = var -> sub - | Variable _ as var -> var - | Abstraction (x, _) as abs when x = var -> abs - | Abstraction (x, term) -> - let freeVarsS = freeVars sub - let freeVarsT = freeVars term - if not (Set.contains var freeVarsT && Set.contains x freeVarsS) then - Abstraction (x, substitute term var sub) - else - let y = nextFreeVar x (Set.union freeVarsS freeVarsT) - Abstraction (y, substitute (substitute term x (Variable y)) var sub) - | Application (left, right) -> - Application (substitute left var sub, substitute right var sub) - -/// Performs beta-reduction of the given lambda `term`. -/// Performs alpha-conversion if necessary. -let rec reduce term = - match term with - | Variable _ as var -> var - | Abstraction (x, term) -> Abstraction (x, reduce term) - | Application (Abstraction (var, term) as abs, sub) as source -> - let term = substitute term var sub - if term <> source then reduce term - else Application (reduce abs, reduce sub) - | Application (left, right) -> - let left = reduce left - let right = reduce right - match left with - | Abstraction _ -> reduce (Application (left, right)) - | _ -> Application (left, right) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Logger.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Logger.fs new file mode 100644 index 0000000..58ea3fa --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Logger.fs @@ -0,0 +1,45 @@ +namespace LambdaInterpreter + +open LambdaInterpreter.Syntax +open AST + +/// Log record of reducer execution. +type LogRecord = + | StartedReducing of LambdaTerm + | DoneReducing + | Reducing of LambdaTerm + | AlphaConversion of Variable * Variable + | BetaReduction of LambdaTerm * LambdaTerm * Variable * LambdaTerm + | Substitution of Variable * LambdaTerm + | UnableToReduce of LambdaTerm + | NewDefinition of Variable * LambdaTerm + | DefinitionsReset + | DisplayingDefinitions + | NoVariablesDefined + +/// Class for managing execution logs. +/// Use `verbose` option to print logs to the console. +type Logger (?verbose: bool) = + let verbose = defaultArg verbose false + + /// Print a log message using the given `record` according to verbosity. + member _.Log (record: LogRecord) = + if verbose then + match record with + | StartedReducing term -> $"{toString term}\n|" + | DoneReducing -> "V" + | Reducing term -> + $"| reducing {toString term} ..." + | AlphaConversion (Name x, Name y) -> + $"| [alpha-conversion]: {x} -> {y}" + | BetaReduction (source, term, Name var, sub) -> + $"| [beta-reduction]: {toString source} -> {toStringParenthesized term}[{var} := {toString sub}]" + | Substitution (Name var, sub) -> + $"| [substitution]: {var} -> {toString sub}" + | UnableToReduce term -> + $"| unable to reduce {toString term}\n| term didn't change after beta-reduction" + | NewDefinition (Name var, term) -> $"(!) definition: {var} = {toString term}" + | DefinitionsReset -> "(!) definitions were reset" + | DisplayingDefinitions -> "Defined variables in order:" + | NoVariablesDefined -> "- no variables were defined yet" + |> printfn "%s" diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs new file mode 100644 index 0000000..49219ec --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -0,0 +1,61 @@ +open System +open System.IO + +open LambdaInterpreter +open LambdaInterpreter.Console +open ColorScheme +open ExitCode +open Help + +/// Print header with general info about the app and a help suggestion. +let printHeaderWithHelpSuggestion () = + printHeader () + printHelpSuggestion () + +/// Print header with general info about the app followed by command line and interpreter usage help. +let printHeaderWithHelp () = + printHeader () + printUsageHelp () + printOptionsHelp () + printSyntaxHelp () + +/// Print the given `message` to the standard output with the given `color`. +let printMessage (color: ConsoleColor) (message: string) = + Console.ForegroundColor <- color + printfn "%s" message + Console.ResetColor () + +/// Print the result of interpretation according to the given `output` using the given color `scheme`. +let handleOutput (Color success, Color error) (output: Result) = + match output with + | Ok result -> printMessage success result + | Error message -> printMessage error message + +let options = Options.GetFromArgs () + +if options.Help then + printHeaderWithHelp () + exit <| int ExitCode.Success + +if options.Error then + printMessage defaultErrorColor invalidArgsMessage + exit <| int ExitCode.InvalidArguments + +let interpreter = + match options.SourceFile with + | Some path -> + try Interpreter.StartOnFile (path, options.Verbose, options.LineNumber) + with :? IOException | :? UnauthorizedAccessException as ex -> + printMessage defaultErrorColor ex.Message + exit <| int ExitCode.FileNotFound + | None -> Interpreter.StartInteractive options.Verbose + +using interpreter (fun interpreter -> + let colorScheme = getColorScheme interpreter + if interpreter.IsInteractive then printHeaderWithHelpSuggestion () + + for output in interpreter.RunToEnd () do + handleOutput colorScheme output + + getExitCode interpreter |> int |> exit +) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs new file mode 100644 index 0000000..eebfd0c --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -0,0 +1,180 @@ +namespace LambdaInterpreter + +open System + +open LambdaInterpreter.Syntax +open AST + +/// Class performing lambda term reduction. +/// Use `verbose` option to print logs to the console. +type Reducer (?verbose: bool) = + let logger = new Logger (?verbose=verbose) + let mutable variables: (Variable * LambdaTerm) list = [] + + /// Max allowed depth of recursion during the term reduction. + [] + let MaxDepth = 1000000 + + /// Message to fail with in case of max recursion depth exceeding. + [] + let MaxDepthExceededMessage = "Error: max recursion depth exceeded during the reduction." + + /// Get free variables of the given lambda `term` using CPS with the given `cont`. + [] + let rec freeVarsCPS term cont = + match term with + | Variable (Name v) -> set [v] |> cont + | Abstraction (Name v, term) -> + freeVarsCPS term (fun termVars -> + Set.remove v termVars |> cont + ) + | Application (left, right) -> + freeVarsCPS left (fun leftVars -> + freeVarsCPS right (fun rightVars -> + Set.union leftVars rightVars |> cont + ) + ) + + /// Get free variables of the given lambda `term`. + let freeVars term = freeVarsCPS term id + + /// Get a variable, starting with `prefix`, that is not in `freeVars`. + let nextFreeVar prefix freeVars = + let rec nextFreeVar prefix freeVars = + if not (Set.contains prefix freeVars) then prefix + else nextFreeVar (prefix + "'") freeVars + in nextFreeVar prefix freeVars + + /// Substitute free occurrences of variable `var` in `term` with given term `sub`. + /// Use CPS with the given `cont`. + [] + let rec substituteCPS term (Name var, sub) cont = + match term with + + // Substitute free occurrence of a matching variable. + | Variable (Name x) when x = var -> + logger.Log <| Substitution (Name var, sub) + cont sub + + // Nothing to substitute, call continuation. + | Variable _ as var -> cont var + + // Our variable is bounded, call continuation. + | Abstraction (Name x, _) as abs when x = var -> cont abs + + // Obtain free variables of term to make substitution in and term to substitute with. + // Perform alpha-conversion if necessary to avoid capturing, then make a substitution. + | Abstraction (Name x, term) -> + let freeVarsT = freeVars term + let freeVarsS = freeVars sub + if Set.contains var freeVarsT && Set.contains x freeVarsS then + let y = nextFreeVar x (Set.union freeVarsT freeVarsS) |> Name + logger.Log <| AlphaConversion (Name x, y) + substituteCPS term (Name x, Variable y) (fun converted -> + substituteCPS converted (Name var, sub) (fun subsTerm -> + Abstraction (y, subsTerm) |> cont + ) + ) + else + substituteCPS term (Name var, sub) (fun subsTerm -> + Abstraction (Name x, subsTerm) |> cont + ) + + // Make substitution in both parts of the application. + | Application (left, right) -> + substituteCPS left (Name var, sub) (fun subsLeft -> + substituteCPS right (Name var, sub) (fun subsRight -> + Application (subsLeft, subsRight) |> cont + ) + ) + + /// Substitute free occurrences of variable `var` in `term` with given term `sub`. + /// Perform alpha-conversion if necessary. + let substitute term (Name var, sub) = substituteCPS term (Name var, sub) id + + /// Substitute variables in `term` according to the given `subs` pair sequence. + let substituteMany term subs = + subs |> Seq.fold substitute term + + /// Reduce `term` in CPS using the given `cont`. + /// Keep track of `depth` of the reduction and throw exception in case of exceeding. + [] + let rec reduceCPS term depth ret cont = + if depth > MaxDepth then raise <| StackOverflowException MaxDepthExceededMessage + logger.Log <| Reducing term + match term with + + // Nothing to reduce, call continuation. + | Variable _ as var -> cont var + + // Reduce the right part of the abstraction and pass it to continuation. + | Abstraction (var, term) -> + reduceCPS term (depth + 1) false (fun reducedTerm -> + Abstraction (var, reducedTerm) |> cont + ) + + // Perform beta-reduction, then check whether the resulting term is an abstraction. + // Return if necessary to reduce the outermost redex, otherwise reduce the result. + | Application (Abstraction (var, term) as abs, sub) as source -> + logger.Log <| BetaReduction (source, term, var, sub) + let term = substitute term (var, sub) + match term with + | Abstraction _ when ret -> cont term + | _ -> + if term <> source then reduceCPS term depth ret cont + else + logger.Log <| UnableToReduce term + reduceCPS abs (depth + 1) false (fun reducedAbs -> + reduceCPS sub (depth + 1) false (fun reducedSub -> + Application (reducedAbs, reducedSub) |> cont + ) + ) + + // Reduce left part of the application first, then check for redex. + // Perform beta-reduction if left part was reduced to an abstraction, otherwise reduce the right part. + | Application (left, right) -> + reduceCPS left (depth + 1) true (fun reducedLeft -> + match reducedLeft with + | Abstraction _ -> reduceCPS (Application (reducedLeft, right)) depth ret cont + | _ -> + reduceCPS right (depth + 1) false (fun reducedRight -> + Application (reducedLeft, reducedRight) |> cont + ) + ) + + /// Perform beta-reduction of the given lambda `term`. + /// Perform alpha-conversion if necessary. + let reduce term = reduceCPS term 0 false id + + /// Perform beta-reduction of the given lambda `term` according to defined variables. + /// Perform alpha-conversion if necessary. + member _.Reduce (term: LambdaTerm): LambdaTerm = + logger.Log <| StartedReducing term + let result = variables |> substituteMany term |> reduce + logger.Log <| DoneReducing + result + + /// Define a `var` to be substituted with the given `term`. + member _.AddDefinition (var: Variable, term: LambdaTerm) = + variables <- (var, term) :: variables + logger.Log <| NewDefinition (var, term) + + /// Reset defined variables. + member _.ResetDefinitions () = + variables <- [] + logger.Log <| DefinitionsReset + + /// Print defined variables to the console in order of addition. + member _.DisplayDefinitions () = + + /// Print the given definition of `var` with `term` to the console. + let printDefinition (Name var, term) = + printfn $"- {var} := {toString term}" + + logger.Log <| DisplayingDefinitions + if variables.IsEmpty then logger.Log <| NoVariablesDefined else + variables + |> List.rev + |> List.distinct + |> List.map printDefinition + |> ignore diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs new file mode 100644 index 0000000..c245ee7 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -0,0 +1,107 @@ +namespace LambdaInterpreter.Syntax + +open System +open Primary + +/// Module dealing with finalized syntax trees of lambda expressions. +module AST = + + /// The finalized lambda term representation. + type LambdaTerm = + | Variable of Variable + | Abstraction of Variable * LambdaTerm + | Application of LambdaTerm * LambdaTerm + + /// The finalized expression representation. + type Expression = + | Definition of Variable * LambdaTerm + | Result of LambdaTerm + | Command of SpecialCommand + | Empty + + /// Build AST of a lambda term using the `primary` representation. + /// Use CPS with the given `cont`. + [] + let rec private buildTermAST_CPS (primary: Primary.Term) cont = + + /// Convert `primary` operand representation to the lambda term. + let buildOperandAST (primary: Primary.Operand) cont = + match primary with + | Primary.Variable var -> Variable var |> cont + | Brackets term -> buildTermAST_CPS term cont + + /// Build AST of lambda term application using term on the `left` and the rest on `right`. + let rec buildApplicationAST (left: LambdaTerm) (right: Primary.ApplicationOpt) cont = + match right with + | WithContinuation (operand, rest) -> + buildOperandAST operand (fun right -> + let partial = Application (left, right) + buildApplicationAST partial rest cont + ) + | FinalAbstraction abs -> + buildTermAST_CPS abs (fun right -> + Application (left, right) |> cont + ) + | Epsilon -> cont left + + match primary with + | Primary.Application (operand, rest) -> + buildOperandAST operand (fun operandAST -> + buildApplicationAST operandAST rest cont + ) + | Primary.Abstraction (head :: tail, term) -> + if tail.IsEmpty then + buildTermAST_CPS term (fun termAST -> + Abstraction (head, termAST) |> cont + ) + else + buildTermAST_CPS (Primary.Abstraction (tail, term)) (fun termAST -> + Abstraction (head, termAST) |> cont + ) + | Primary.Abstraction ([], _) -> + raise (ArgumentException "Abstraction received empty variable list") + + /// Build AST of a lambda term using the `primary` representation. + let buildTermAST (primary: Primary.Term) = buildTermAST_CPS primary id + + /// Build a finalized expression representation from the `primary` one. + let buildExpressionAST (primary: Primary.Expression) = + match primary with + | Primary.Definition (variable, term) -> Definition (variable, buildTermAST term) + | Primary.Result term -> Result (buildTermAST term) + | Primary.Command command -> Command command + | Primary.Empty -> Empty + + /// Get a string representation of the given lambda `term`. + /// Use `parenthesized` to surround term with brackets if it's not a variable. + /// Use `closing` to indicate that term is last in the application sequence. + /// Use CPS with the given `cont`. + [] + let rec private toStringCPS term parenthesized closing cont = + match term with + | Variable (Name var) -> cont var + | Application (left, right) -> + let closedAbstraction = parenthesized || closing + let parenthesizedLeft = left.IsAbstraction + let parenthesizedRight = right.IsApplication || right.IsAbstraction && not closedAbstraction + toStringCPS left parenthesizedLeft false (fun leftStr -> + toStringCPS right parenthesizedRight closing (fun rightStr -> + let termStr = $"{leftStr} {rightStr}" + if parenthesized then $"({termStr})" else termStr + |> cont + ) + ) + | Abstraction (Name var, term) -> + toStringCPS term false true (fun termStr -> + let termStr = $"\\{var}.{termStr}" + if parenthesized then $"({termStr})" else termStr + |> cont + ) + + /// Get a string representation of the given lambda `term`. + let toString (term: LambdaTerm) = + toStringCPS term false true id + + /// Get a string representation of the given lambda `term` surrounded with brackets if it's not a variable. + let toStringParenthesized (term: LambdaTerm) = + toStringCPS term true true id diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs new file mode 100644 index 0000000..9aa9caf --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs @@ -0,0 +1,34 @@ +namespace LambdaInterpreter.Syntax + +open Keywords + +/// Module for displaying syntax help. +module Help = + + /// A pointer indicating the start of input for the interpreter. + [] + let InputPointer = ">>> " + + /// Print syntax help to the standard output. + let printSyntaxHelp () = + printfn $" +Syntax: + variable\t\t {VariablePattern} + term\t\t {{variable}}|{{abstraction}}|{{application}}|({{term}}) + application\t\t {{term}} {{term}} + abstraction\t\t \\{{variables}}.{{term}} + definition\t\t {DeclarationKeyword} {{variable}} = {{term}} + +Examples: + {InputPointer}{DeclarationKeyword} S = \\x y z.x z (y z) + {InputPointer}{DeclarationKeyword} K = \\x y.x + {InputPointer}S K K + \\z.z + +Commands: + {ResetKeyword}\t\t Reset defined variables + {DisplayKeyword}\t\t Display definitions in order of addition + {HelpKeyword}\t\t Display help + {ClearKeyword}\t\t Clear console buffer + {ExitKeyword}\t\t Stop the execution and exit +" diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs new file mode 100644 index 0000000..838ad30 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs @@ -0,0 +1,45 @@ +namespace LambdaInterpreter.Syntax + +/// Module dealing with keyword definitions. +module Keywords = + + /// A regex pattern representing the variable name. + [] + let VariablePattern = @"[a-zA-Z][a-zA-Z0-9_]*" + + /// Keyword for variable declaration. + [] + let DeclarationKeyword = "let" + + /// Keyword for resetting defined variables. + [] + let ResetKeyword = "reset" + + /// Keyword for displaying defined variables. + [] + let DisplayKeyword = "display" + + /// Keyword for displaying help info. + [] + let HelpKeyword = "help" + + /// Keyword for clearing the console buffer. + [] + let ClearKeyword = "clear" + + /// Keyword for exiting the interpreter. + [] + let ExitKeyword = "exit" + + /// The list of defined keywords. + let keywords = [ + DeclarationKeyword; + ResetKeyword; + DisplayKeyword; + HelpKeyword; + ClearKeyword; + ExitKeyword; + ] + + /// Whether the given `str` is reserved as a keyword. + let isKeyword str = List.contains str keywords diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs new file mode 100644 index 0000000..0139487 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs @@ -0,0 +1,103 @@ +namespace LambdaInterpreter.Syntax + +open FParsec + +open Keywords +open Primary + +/// Module dealing with the source text parsing. +module Parser = + + /// Accept 0 or more whitespaces. + let whitespaceOpt = spaces + + /// Accept 1 or more whitespaces. + let whitespace = spaces1 + + /// Accept optional whitespace on the left of the given `parser`. + let ( ?< ) parser = whitespaceOpt >>. parser + + /// Accept optional whitespace on the right of the given `parser`. + let ( ?> ) parser = parser .>> whitespaceOpt + + /// Accept whitespace on the left of the given `parser`. + let ( !< ) parser = whitespace >>. parser + + /// Accept whitespace on the right of the given `parser`. + let ( !> ) parser = parser .>> whitespace + + /// Accept optional whitespace followed by end of the input. + let inputEnd = (?<)eof + + /// Modifies the given `reply` to check that its result is not a keyword. + let exceptKeyword (reply: Reply) = + if reply.Status = ReplyStatus.Ok && isKeyword reply.Result then + Reply ( + ReplyStatus.Error, + ErrorMessage.Unexpected $"'{reply.Result}' is reserved as a keyword" |> ErrorMessageList + ) + else reply + + /// Accept the variable name. + let variable: Parser = regex VariablePattern >> exceptKeyword |>> Name + + /// Accept one or more of variable names, separated and optionally surrounded by whitespace. + let variables = (?<)(sepEndBy1 variable whitespace) + + /// Accept a primary lambda term representation. + let term, termRef = createParserForwardedToRef () + + /// Accept a parenthesized lambda term. + let termPar = between ((?>)(pchar '(')) ((?<)(pchar ')')) term + + /// Accept an operand in lambda term application. + let operand = choice [variable |>> Variable; termPar |>> Brackets] + + /// Accept a lambda abstraction. + let abstraction = between (pchar '\\') (pchar '.') variables .>>. (?<)term |>> Abstraction + + /// Accept an optional lambda term application. + let applicationOpt, applicationOptRef = createParserForwardedToRef () + + /// Accept an operand application with continuation. + let applicationOpt' = attempt (!>. applicationOpt) |>> WithContinuation + + /// Accept a final abstraction in the application sequence. + let applicationOpt'' = attempt !> FinalAbstraction + + applicationOptRef.Value <- choice [applicationOpt'; applicationOpt''; preturn Epsilon] + + /// Accept a lambda term application or a single operand. + let application = operand .>>. applicationOpt |>> Application + + termRef.Value <- choice [application; abstraction] + + /// Accept a variable declaration. + let declaration = pstring DeclarationKeyword >>. !declaration .>> pchar '=' .>>. !> Definition + + /// Accept a keyword for resetting defined variables. + let reset: Parser = pstring ResetKeyword >>. preturn (Command Reset) + + /// Accept a keyword for displaying defined variables. + let display: Parser = pstring DisplayKeyword >>. preturn (Command Display) + + /// Accept a keyword for displaying help. + let help: Parser = pstring HelpKeyword >>. preturn (Command Help) + + /// Accept a keyword for clearing the console buffer. + let clear: Parser = pstring ClearKeyword >>. preturn (Command Clear) + + /// Accept a keyword for exiting the interpreter. + let exit: Parser = pstring ExitKeyword >>. preturn (Command Exit) + + /// Accept a special interpreter command. + let command = choice [reset; display; help; clear; exit] + + /// Accept an expression or an empty string. + let expressionOpt = choice [attempt term |>> Result; definition; command; preturn Empty] + + /// Accept an expression or an empty string followed by end of the input. + let expression = expressionOpt .>> inputEnd diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs new file mode 100644 index 0000000..fd2d209 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs @@ -0,0 +1,41 @@ +namespace LambdaInterpreter.Syntax + +/// A variable of specific name. +type Variable = Name of string + +/// A list of variables. +type Variables = Variable list + +/// A special command for managing the interpreter execution. +type SpecialCommand = + | Reset + | Display + | Help + | Clear + | Exit + +/// Module defining primary syntax constructions. +module Primary = + + /// A primary term representation. + type Term = + | Application of Operand * ApplicationOpt + | Abstraction of Variables * Term + + /// Optional lambda term application. + and ApplicationOpt = + | WithContinuation of Operand * ApplicationOpt + | FinalAbstraction of Term + | Epsilon + + /// An operand in lambda term application. + and Operand = + | Variable of Variable + | Brackets of Term + + /// An expression to be interpreted. + type Expression = + | Definition of Variable * Term + | Result of Term + | Command of SpecialCommand + | Empty