From f886716214834139aeeeb25747665048316a8db0 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Thu, 24 Apr 2025 22:03:44 +0300 Subject: [PATCH 01/50] add parser --- .../LambdaTermTests.fs | 4 +- .../LambdaInterpreter.fsproj | 6 + .../LambdaInterpreter/LambdaTerm.fs | 106 +++++++++--------- .../LambdaInterpreter/Parser.fs | 55 +++++++++ .../LambdaInterpreter/Syntax.fs | 22 ++++ 5 files changed, 140 insertions(+), 53 deletions(-) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter/Syntax.fs diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaTermTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaTermTests.fs index 5ff8ac6..a0b80af 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaTermTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaTermTests.fs @@ -1,8 +1,10 @@ -module LambdaTerm.Tests +module LambdaInterpreter.Tests open NUnit.Framework open FsUnit +open LambdaTerm + 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) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj index 60a9a0b..90af49b 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -7,6 +7,12 @@ + + + + + + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaTerm.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaTerm.fs index 3f424d3..67d6b76 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaTerm.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaTerm.fs @@ -1,58 +1,60 @@ -module LambdaTerm +namespace LambdaInterpreter -/// Use strings as variables in lambda terms. -type Variable = string +module LambdaTerm = -/// The definition of lambda term. -type LambdaTerm = - | Variable of Variable - | Abstraction of Variable * LambdaTerm - | Application of LambdaTerm * LambdaTerm + /// Use strings as variables in lambda terms. + type Variable = string -/// 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) + /// The definition of lambda term. + type LambdaTerm = + | Variable of Variable + | Abstraction of Variable * LambdaTerm + | Application of LambdaTerm * LambdaTerm -/// 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 + /// 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) -/// 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) + /// 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 -/// 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) + /// 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/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs new file mode 100644 index 0000000..ee1af25 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs @@ -0,0 +1,55 @@ +namespace LambdaInterpreter + +open FParsec + +module Parser = + + let whitespaceOpt = spaces + + let whitespace = spaces1 + + let ( ?< ) parser = whitespaceOpt >>. parser + + let ( ?> ) parser = parser .>> whitespaceOpt + + let ( !< ) parser = whitespace >>. parser + + let ( !> ) parser = parser .>> whitespace + + let lineEnd = (?<)(skipNewline <|> eof) + + let variable: Parser = + let isFirstVariableChar c = isLetter c + let isVariableChar c = isLetter c || isDigit c || c = '_' + + many1Satisfy2 isFirstVariableChar isVariableChar |>> Name + + let variables = variable .>>. many !> fun (h, t) -> h :: t + + let term, termRef = createParserForwardedToRef () + + let operand = + between ((?>)(pchar '(')) ((?<)(pchar ')')) term |>> Brackets + <|> (variable |>> Variable) + + let abstraction = between (pchar '\\') (pchar '.') variables .>>. term |>> Abstraction + + let applicationOpt, applicationOptRef = createParserForwardedToRef () + + applicationOptRef.Value <- + !>. applicationOpt |>> Apply + <|> preturn ApplicationOpt.Epsilon + + let application = operand .>>. applicationOpt |>> Application + + termRef.Value <- choice [application; abstraction] + + let declaration = pstring "let" >>. !declaration .>> pchar '=' .>>. !> Definition + + let expressionOpt = choice [definition; term |>> Result; preturn Epsilon] + + let expression = expressionOpt .>> lineEnd + + let program = many expression diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax.fs new file mode 100644 index 0000000..2369450 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax.fs @@ -0,0 +1,22 @@ +namespace LambdaInterpreter + +type Variable = Name of string + +type Variables = Variable list + +type Term = + | Application of Operand * ApplicationOpt + | Abstraction of Variables * Term +and ApplicationOpt = + | Apply of Operand * ApplicationOpt + | Epsilon +and Operand = + | Variable of Variable + | Brackets of Term + +type Expression = + | Definition of Variable * Term + | Result of Term + | Epsilon + +type Program = Expression list From 93efcdde244a673f02f91d6d30c6b4515a63f507 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Thu, 24 Apr 2025 23:25:30 +0300 Subject: [PATCH 02/50] refactor --- .../LambdaTermTests.fs | 139 +++++++++--------- .../LambdaInterpreter.fsproj | 5 +- .../LambdaInterpreter/Parser.fs | 20 +++ .../{LambdaTerm.fs => Reduction.fs} | 32 ++-- .../LambdaInterpreter/Syntax/AST.fs | 13 ++ .../{Syntax.fs => Syntax/Primary.fs} | 9 ++ 6 files changed, 128 insertions(+), 90 deletions(-) rename Tasks/LambdaInterpreter/LambdaInterpreter/{LambdaTerm.fs => Reduction.fs} (68%) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs rename Tasks/LambdaInterpreter/LambdaInterpreter/{Syntax.fs => Syntax/Primary.fs} (62%) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaTermTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaTermTests.fs index a0b80af..4ae5085 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaTermTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaTermTests.fs @@ -3,7 +3,8 @@ open NUnit.Framework open FsUnit -open LambdaTerm +open AST +open Reduction let id var = Abstraction (var, Variable var) let omega var = Abstraction (var, Application (Variable var, Variable var)) @@ -12,97 +13,97 @@ 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"; + Variable (Name "x"); + Application (Variable (Name "x"), Variable (Name "y")); + Abstraction (Name "x", Variable (Name "y")); + omega (Name "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"); + Application (omega (Name "x"), Variable (Name "y")); + Application (Abstraction (Name "x", Variable (Name "x")), Variable (Name "z")); + Application (Abstraction (Name "x", Application (Variable (Name "x"), Variable (Name "y"))), Variable (Name "z")); + Application (Abstraction (Name "x", Variable (Name "y")), Omega (Name "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")); + Abstraction (Name "a", Application + (Abstraction (Name "b", Application (Variable (Name "b"), Variable (Name "c"))), + Variable (Name "x"))); + Application (Variable (Name "x"), Application + (Abstraction (Name "a", omega (Name "y")), + Variable (Name "z"))); // Multiple variable substitution Application (Application - (Abstraction ("a", Abstraction ("b", Application (Variable "a", Variable "b"))), - Variable "x"), Variable "y"); + (Abstraction (Name "a", Abstraction (Name "b", Application (Variable (Name "a"), Variable (Name "b")))), + Variable (Name "x")), Variable (Name "y")); Application (Application (Application - (Abstraction ("a", Abstraction ("b", Abstraction ("c", Variable "x"))), - Variable "y"), Variable "y"), Variable "y"); + (Abstraction (Name "a", Abstraction (Name "b", Abstraction (Name "c", Variable (Name "x")))), + Variable (Name "y")), Variable (Name "y")), Variable (Name "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 (id (Name "x"), id (Name "y")); + Abstraction (Name "a", Application + (Abstraction (Name "b", Application (Variable (Name "a"), Variable (Name "b"))), + id (Name "x"))); + Application (id (Name "x"), Application (Variable (Name "x"), Variable (Name "y"))); Application - (Abstraction ("a", Abstraction ("b", Application (Variable "a", Variable "b"))), - id "x"); + (Abstraction (Name "a", Abstraction (Name "b", Application (Variable (Name "a"), Variable (Name "b")))), + id (Name "x")); // Irreducible redex - Omega "z"; - Application (Omega "x", Omega "y"); + Omega (Name "z"); + Application (Omega (Name "x"), Omega (Name "y")); // Alpha conversion required Application - (Abstraction ("x", Abstraction ("y", Application (Variable "x", Variable "y"))), - Variable "y"); + (Abstraction (Name "x", Abstraction (Name "y", Application (Variable (Name "x"), Variable (Name "y")))), + Variable (Name "y")); Application - (Abstraction ("z'", Abstraction ("z", Application (Variable "z", Variable "z'"))), - Variable "z"); + (Abstraction (Name "z'", Abstraction (Name "z", Application (Variable (Name "z"), Variable (Name "z'")))), + Variable (Name "z")); Application - (Abstraction ("x", Application - (Abstraction ("y", Application (Variable "x", Variable "y")), - Variable "x")), - Abstraction ("y", Application (Variable "x", Variable "y"))); + (Abstraction (Name "x", Application + (Abstraction (Name "y", Application (Variable (Name "x"), Variable (Name "y"))), + Variable (Name "x"))), + Abstraction (Name "y", Application (Variable (Name "x"), Variable (Name "y")))); Application - (Abstraction ("a", Abstraction ("b", - Abstraction ("c", Application (Variable "a", Variable "b")))), - Application (Variable "c", Variable "b")); + (Abstraction (Name "a", Abstraction (Name "b", + Abstraction (Name "c", Application (Variable (Name "a"), Variable (Name "b"))))), + Application (Variable (Name "c"), Variable (Name "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'"))); + Variable (Name "x"); + Application (Variable (Name "x"), Variable (Name "y")); + Abstraction (Name "x", Variable (Name "y")); + omega (Name "x"); + + Application (Variable (Name "y"), Variable (Name "y")); + Variable (Name "z"); + Application (Variable (Name "z"), Variable (Name "y")); + Variable (Name "y"); + + Abstraction (Name "a", Application (Variable (Name "x"), Variable (Name "c"))); + Application (Variable (Name "x"), omega (Name "y")); + + Application (Variable (Name "x"), Variable (Name "y")); + Variable (Name "x"); + + id (Name "y"); + Abstraction (Name "a", Application(Variable (Name "a"), id (Name "x"))); + Application (Variable (Name "x"), Variable (Name "y")); + id (Name "b"); + + Omega (Name "z"); + Application (Omega (Name "x"), Omega (Name "y")); + + Abstraction (Name "y'", Application (Variable (Name "y"), Variable (Name "y'"))); + Abstraction (Name "z''", Application (Variable (Name "z''"), Variable (Name "z"))); + Application (Variable (Name "x"), Abstraction (Name "y", Application (Variable (Name "x"), Variable (Name "y")))); + Abstraction (Name "b'", Abstraction (Name "c'", Application + (Application (Variable (Name "c"), Variable (Name "b")), + Variable (Name "b'")))); ] let testCases = List.zip terms reducedTerms |> List.map TestCaseData diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj index 90af49b..75e9632 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -6,9 +6,10 @@ - - + + + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs index ee1af25..8b389b0 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs @@ -2,54 +2,74 @@ namespace LambdaInterpreter open FParsec +/// Module dealing with the source text parsing. module Parser = + /// Accept 0 or more spaces. let whitespaceOpt = spaces + /// Accept 1 of more spaces. 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 the end of line with optional whitespace. let lineEnd = (?<)(skipNewline <|> eof) + /// Accept the variable name. let variable: Parser = let isFirstVariableChar c = isLetter c let isVariableChar c = isLetter c || isDigit c || c = '_' many1Satisfy2 isFirstVariableChar isVariableChar |>> Name + /// Accept one or more of variable names. let variables = variable .>>. many !> fun (h, t) -> h :: t + /// Accept a primary lambda term representation. let term, termRef = createParserForwardedToRef () + /// Accept an operand in lambda term application. let operand = between ((?>)(pchar '(')) ((?<)(pchar ')')) term |>> Brackets <|> (variable |>> Variable) + /// Accept a lambda abstraction. let abstraction = between (pchar '\\') (pchar '.') variables .>>. term |>> Abstraction + /// Accept an optional lambda term application. let applicationOpt, applicationOptRef = createParserForwardedToRef () applicationOptRef.Value <- !>. applicationOpt |>> Apply <|> preturn ApplicationOpt.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 "let" >>. !declaration .>> pchar '=' .>>. !> Definition + /// Accept an optional expression of a program. let expressionOpt = choice [definition; term |>> Result; preturn Epsilon] + /// Accept an expression of a program or a line break. let expression = expressionOpt .>> lineEnd + /// Accept a program as a list of expressions. let program = many expression diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaTerm.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reduction.fs similarity index 68% rename from Tasks/LambdaInterpreter/LambdaInterpreter/LambdaTerm.fs rename to Tasks/LambdaInterpreter/LambdaInterpreter/Reduction.fs index 67d6b76..a6210e6 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaTerm.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reduction.fs @@ -1,21 +1,15 @@ namespace LambdaInterpreter -module LambdaTerm = +open AST - /// 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 +/// Module dealing with lambda term reduction. +module Reduction = /// 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) + | Variable (Name v) -> set [v] + | Abstraction (Name v, term) -> Set.remove v (freeVars term) | Application (left, right) -> Set.union (freeVars left) (freeVars right) @@ -26,21 +20,21 @@ module LambdaTerm = /// Substitutes free occurrences of variable `var` in `term` with given term `sub`. /// Performs alpha-conversion if necessary. - let rec substitute term var sub = + let rec substitute term (Name var) sub = match term with - | Variable x when x = var -> sub + | Variable (Name x) when x = var -> sub | Variable _ as var -> var - | Abstraction (x, _) as abs when x = var -> abs - | Abstraction (x, term) -> + | Abstraction (Name x, _) as abs when x = var -> abs + | Abstraction (Name 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) + Abstraction (Name x, substitute term (Name var) sub) else - let y = nextFreeVar x (Set.union freeVarsS freeVarsT) - Abstraction (y, substitute (substitute term x (Variable y)) var sub) + let y = nextFreeVar x (Set.union freeVarsS freeVarsT) |> Name + Abstraction (y, substitute (substitute term (Name x) (Variable y)) (Name var) sub) | Application (left, right) -> - Application (substitute left var sub, substitute right var sub) + Application (substitute left (Name var) sub, substitute right (Name var) sub) /// Performs beta-reduction of the given lambda `term`. /// Performs alpha-conversion if necessary. diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs new file mode 100644 index 0000000..5ee74f9 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -0,0 +1,13 @@ +namespace LambdaInterpreter + +/// Module dealing with finalized syntax trees. +module AST = + + /// The definition of lambda term. + type LambdaTerm = + | Variable of Variable + | Abstraction of Variable * LambdaTerm + | Application of LambdaTerm * LambdaTerm + + /// The finalized variable definition. + type Definition = Variable * LambdaTerm diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs similarity index 62% rename from Tasks/LambdaInterpreter/LambdaInterpreter/Syntax.fs rename to Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs index 2369450..c2e9cf3 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs @@ -1,22 +1,31 @@ namespace LambdaInterpreter +/// A variable of specific name. type Variable = Name of string +/// A list of variables. type Variables = Variable list +/// A primary term representation. type Term = | Application of Operand * ApplicationOpt | Abstraction of Variables * Term + +/// Optional lambda term application. and ApplicationOpt = | Apply of Operand * ApplicationOpt | Epsilon + +/// An operand in lambda term application. and Operand = | Variable of Variable | Brackets of Term +/// An expression as a logical unit of the program. type Expression = | Definition of Variable * Term | Result of Term | Epsilon +/// Program as a list of expressions. type Program = Expression list From 279cfa00fd2a1d66b4e8862c7aac176cb3a3d4a2 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Fri, 25 Apr 2025 12:17:22 +0300 Subject: [PATCH 03/50] add AST conversions --- .../LambdaInterpreter/Parser.fs | 1 + .../LambdaInterpreter/Syntax/AST.fs | 54 ++++++++++++++++++- .../LambdaInterpreter/Syntax/Primary.fs | 49 +++++++++-------- 3 files changed, 79 insertions(+), 25 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs index 8b389b0..f290ce7 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs @@ -1,6 +1,7 @@ namespace LambdaInterpreter open FParsec +open Primary /// Module dealing with the source text parsing. module Parser = diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index 5ee74f9..a8e61cc 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -1,5 +1,8 @@ namespace LambdaInterpreter +open System +open Primary + /// Module dealing with finalized syntax trees. module AST = @@ -9,5 +12,52 @@ module AST = | Abstraction of Variable * LambdaTerm | Application of LambdaTerm * LambdaTerm - /// The finalized variable definition. - type Definition = Variable * LambdaTerm + /// The finalized expression representation. + type Expression = + | Definition of Variable * LambdaTerm + | Result of LambdaTerm + + /// The finalized program representation. + type Program = Expression seq + + /// Build AST of a lambda term using the `primary` representation. + let buildAST_Term: Primary.Term -> LambdaTerm = Unchecked.defaultof<_> + let buildAST_Term_Ref = ref buildAST_Term + + /// Convert `primary` operand representation to the lambda term. + let buildAST_Operand (primary: Primary.Operand) = + match primary with + | Primary.Variable var -> Variable var + | Brackets term -> buildAST_Term term + + /// Build AST of lambda term application using term on the `left` and the rest on `right`. + let rec buildAST_Application (left: LambdaTerm, right: Primary.ApplicationOpt) = + match right with + | Apply (operand, rest) -> + let right = buildAST_Operand operand + let partial = Application (left, right) + buildAST_Application (partial, rest) + | ApplicationOpt.Epsilon -> left + + buildAST_Term_Ref.Value <- fun primary -> + match primary with + | Primary.Application (operand, rest) -> + let operand = buildAST_Operand operand + buildAST_Application (operand, rest) + | Primary.Abstraction (head :: tail, term) -> + if tail.IsEmpty then Abstraction (head, buildAST_Term term) + else Abstraction (head, buildAST_Term (Primary.Abstraction (tail, term))) + | Primary.Abstraction ([], _) -> + raise (ArgumentException "Abstraction received empty variable list") + + /// Build a finalized program representation from the `primary` one. + let buildAST_Program (primary: Primary.Program) = + seq { + for expression in primary do + match expression with + | Primary.Definition (variable, term) -> + yield Definition (variable, buildAST_Term term) + | Primary.Result term -> + yield Result (buildAST_Term term) + | Epsilon -> () + } diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs index c2e9cf3..afd1d51 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs @@ -6,26 +6,29 @@ type Variable = Name of string /// A list of variables. type Variables = Variable list -/// A primary term representation. -type Term = - | Application of Operand * ApplicationOpt - | Abstraction of Variables * Term - -/// Optional lambda term application. -and ApplicationOpt = - | Apply of Operand * ApplicationOpt - | Epsilon - -/// An operand in lambda term application. -and Operand = - | Variable of Variable - | Brackets of Term - -/// An expression as a logical unit of the program. -type Expression = - | Definition of Variable * Term - | Result of Term - | Epsilon - -/// Program as a list of expressions. -type Program = Expression list +/// 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 = + | Apply of Operand * ApplicationOpt + | Epsilon + + /// An operand in lambda term application. + and Operand = + | Variable of Variable + | Brackets of Term + + /// An expression as a logical unit of the program. + type Expression = + | Definition of Variable * Term + | Result of Term + | Epsilon + + /// Program as a list of expressions. + type Program = Expression list From 0a967857bcae7f06eeaa800df3c05a22a4d74d96 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Fri, 25 Apr 2025 12:45:24 +0300 Subject: [PATCH 04/50] add lambda term to string transformation --- .../LambdaInterpreter/LambdaInterpreter.fsproj | 2 ++ Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs | 7 +++++++ Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs | 7 +++++++ 3 files changed, 16 insertions(+) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj index 75e9632..756a8dd 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -2,6 +2,7 @@ net9.0 + Exe true @@ -10,6 +11,7 @@ + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs new file mode 100644 index 0000000..a13dfcf --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -0,0 +1,7 @@ +namespace LambdaInterpreter + +open AST +open Parser +open Reduction + + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index a8e61cc..5466a94 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -61,3 +61,10 @@ module AST = yield Result (buildAST_Term term) | Epsilon -> () } + + /// Get a string representation of the given lambda `term`. + let rec toString (term: LambdaTerm) = + match term with + | Variable (Name var) -> var + | Application (left, right) -> $"{toString left} {toString right}" + | Abstraction (Name var, term) -> $"(\\{var}.{toString term})" From 4362d34420fac7f49b350e4c13de8d4bb5495e98 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Fri, 25 Apr 2025 16:39:56 +0300 Subject: [PATCH 05/50] add interpreter and program --- .../LambdaInterpreter/Interpreter.fs | 46 ++++++++++++++++ .../LambdaInterpreter.fsproj | 1 + .../LambdaInterpreter/Program.fs | 53 +++++++++++++++++-- .../LambdaInterpreter/Reduction.fs | 5 ++ .../LambdaInterpreter/Syntax/AST.fs | 20 ++++--- 5 files changed, 110 insertions(+), 15 deletions(-) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs new file mode 100644 index 0000000..cd3b5f8 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -0,0 +1,46 @@ +namespace LambdaInterpreter + +open System +open System.Text +open FParsec + +open AST +open Parser +open Reduction + +/// Module dealing with lambda term interpretation. +module Interpreter = + + /// Run the interpreter to the end of the given `stream`. + let runInterpreter (interactive: bool) (stream: CharStream<_>) = + let mutable vars = new Map ([]) + seq { + while not stream.IsEndOfStream do + if interactive then printf "-> " + let reply = expression stream + if reply.Status = Ok then + let expr = reply.Result |> buildAST_Expression + match expr with + | Definition (var, term) -> + vars <- vars.Add (var, substituteMany term vars) + | Result term -> + let result = substituteMany term vars |> reduce |> toString + if interactive then printfn "%s" result + yield Result.Ok result + | None -> () + else + let message = reply.Error.Head.ToString () + if interactive then printfn "%s" message + yield Result.Error message + } + + /// Run the interpreter on a source file at the given `path`. + let runInterpreterOnFile (path: string) = + use stream = new CharStream<_> (path, Encoding.UTF8) + runInterpreter false stream + + /// Interactively run the interpreter in the console. + let runInterpreterInConsole () = + use inputStream = Console.OpenStandardInput () + let stream = new CharStream<_> (inputStream, Encoding.UTF8) + runInterpreter true stream diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj index 756a8dd..1bb52d9 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -11,6 +11,7 @@ + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index a13dfcf..1beaba5 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -1,7 +1,52 @@ -namespace LambdaInterpreter +open System -open AST -open Parser -open Reduction +open LambdaInterpreter.Interpreter +let printInfo () = + printf " +Lambda Interpreter +------------------ +A simple interpreter of lambda term expressions. +For more info use -h option. +" + +let printHelp () = + printf " +Lambda Interpreter +------------------ +A simple interpreter of lambda term expressions. + +Usage: + LambdaInterpreter [options]\t\t Run interpreter interactively + LambdaInterpreter {path-to-file}\t Run interpreter on the given source file + +Options: + -h|--help\t\t Display help + +Syntax: + variable\t\t [letter][letter|digit|_]* + term\t\t {variable}|{abstraction}|{application}|({term}) + application\t\t {term} {term} + abstraction\t\t \\{variables}.{term} + definition\t\t let {variable} = {term} + +Examples: + let S = \\x y z.x z (y z) + let K = \\x y.x + S K K +" + +let args = Environment.GetCommandLineArgs () + +if Array.contains "-h" args || Array.contains "--help" args then + printHelp () + exit 0 + +printInfo () +let output = runInterpreterInConsole () + +let hasErrors = output |> Seq.exists (function | Error _ -> true | Ok _ -> false) +let exitCode = if hasErrors then 1 else 0 + +exit exitCode diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reduction.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reduction.fs index a6210e6..e30c678 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reduction.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reduction.fs @@ -36,6 +36,11 @@ module Reduction = | Application (left, right) -> Application (substitute left (Name var) sub, substitute right (Name var) sub) + /// Substitutes variables in `term` according to the `subs` mapping. + let substituteMany term (subs: Map) = + subs + |> Seq.fold (fun acc pair -> substitute acc pair.Key pair.Value) term + /// Performs beta-reduction of the given lambda `term`. /// Performs alpha-conversion if necessary. let rec reduce term = diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index 5466a94..1056665 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -16,6 +16,7 @@ module AST = type Expression = | Definition of Variable * LambdaTerm | Result of LambdaTerm + | None /// The finalized program representation. type Program = Expression seq @@ -50,17 +51,14 @@ module AST = | Primary.Abstraction ([], _) -> raise (ArgumentException "Abstraction received empty variable list") - /// Build a finalized program representation from the `primary` one. - let buildAST_Program (primary: Primary.Program) = - seq { - for expression in primary do - match expression with - | Primary.Definition (variable, term) -> - yield Definition (variable, buildAST_Term term) - | Primary.Result term -> - yield Result (buildAST_Term term) - | Epsilon -> () - } + /// Build a finalized expression representation from the `primary` one. + let buildAST_Expression (primary: Primary.Expression) = + match primary with + | Primary.Definition (variable, term) -> + Definition (variable, buildAST_Term term) + | Primary.Result term -> + Result (buildAST_Term term) + | Epsilon -> None /// Get a string representation of the given lambda `term`. let rec toString (term: LambdaTerm) = From 7e43c80fcc4ca34e8953075c1d890309491f26b4 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Fri, 25 Apr 2025 16:50:09 +0300 Subject: [PATCH 06/50] change naming --- .../LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj | 2 +- .../{LambdaTermTests.fs => ReductionTests.fs} | 0 Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs | 4 ++-- 3 files changed, 3 insertions(+), 3 deletions(-) rename Tasks/LambdaInterpreter/LambdaInterpreter.Tests/{LambdaTermTests.fs => ReductionTests.fs} (100%) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj index 382dfbf..8db0586 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj @@ -6,7 +6,7 @@ false - + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaTermTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReductionTests.fs similarity index 100% rename from Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaTermTests.fs rename to Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReductionTests.fs diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index 1beaba5..1d59dbe 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -3,7 +3,7 @@ open System open LambdaInterpreter.Interpreter let printInfo () = - printf " + printfn " Lambda Interpreter ------------------ A simple interpreter of lambda term expressions. @@ -12,7 +12,7 @@ For more info use -h option. " let printHelp () = - printf " + printfn " Lambda Interpreter ------------------ A simple interpreter of lambda term expressions. From 46a9a2d37442866b1ba4348b5ea38a9c6b8b279d Mon Sep 17 00:00:00 2001 From: bygu4 Date: Sat, 26 Apr 2025 00:59:50 +0300 Subject: [PATCH 07/50] add parser tests --- .../LambdaInterpreter.Tests.fsproj | 1 + .../LambdaInterpreter.Tests/ParserTests.fs | 164 ++++++++++++++++++ .../LambdaInterpreter.Tests/ReductionTests.fs | 3 +- .../LambdaInterpreter/Parser.fs | 2 +- 4 files changed, 168 insertions(+), 2 deletions(-) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj index 8db0586..da51ce7 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj @@ -6,6 +6,7 @@ false + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs new file mode 100644 index 0000000..71b953b --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs @@ -0,0 +1,164 @@ +module Parser.Tests + +open NUnit.Framework +open FsUnit +open FParsec + +open LambdaInterpreter +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; + " \n", whitespaceOpt, Some 4; + "", whitespace, None; + " ", whitespace, Some 1; + "\n", whitespace, Some 1; + "a1", whitespace, None; + ] |> runTest + +[] +let testParser_LineEnd () = + [ + "", lineEnd, Some 0; + " ", lineEnd, Some 5; + "\n", lineEnd, Some 1; + " \n", lineEnd, Some 4; + "a12", lineEnd, 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; + ] |> 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, None; + "1 2", variables, None; + " ololo ololo ", variables, None; + "first, second", variables, Some 5; + ] |> runTest + +[] +let testParser_Operand () = + [ + "var1", operand, Some 4; + "()", operand, None; + "(some_var)", operand, Some 10; + "_not_a_var", operand, None; + "A B", operand, Some 1; + "((var)", operand, None; + "(((ololo)))", operand, Some 11; + "\\x.y", operand, None; + "(first second)", operand, Some 14; + "(\\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 13; + "a1 a2 a3", application, Some 14; + "(_xyz)", application, None; + "(var1) 2var", application, None; + "(a b) c", application, Some 9; + "var (\\x.x z)", application, Some 12; + "((\\A1 B2 C3.A1) ololo) var1", application, Some 28; + ] |> 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; + ] |> runTest + +[] +let testParser_Term () = + [ + "var1", term, Some 4; + "((ololo))", term, Some 9; + "(\\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; + ] |> runTest + +[] +let testParser_Declaration () = + [ + "let VAR", declaration, Some 7; + "olet a", declaration, None; + " let xy", declaration, None; + "let tmp", declaration, Some 10; + "foo", declaration, None; + "bar ololo", declaration, None; + ] |> 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; + ] |> runTest + +[] +let testParser_Expression () = + [ + "let S = \\x y z.x z (y z)", expression, Some 24; + "let K = \\x y.x", expression, Some 14; + "S K K", expression, Some 5; + "\n", expression, Some 1; + " \n", expression, Some 8; + "_wewq", expression, None; + "123\n", expression, None; + "", expression, Some 0; + "variable", expression, Some 8; + ] |> runTest diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReductionTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReductionTests.fs index 4ae5085..e7d6b8e 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReductionTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReductionTests.fs @@ -1,8 +1,9 @@ -module LambdaInterpreter.Tests +module Reduction.Tests open NUnit.Framework open FsUnit +open LambdaInterpreter open AST open Reduction diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs index f290ce7..4d6bedd 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs @@ -28,7 +28,7 @@ module Parser = let lineEnd = (?<)(skipNewline <|> eof) /// Accept the variable name. - let variable: Parser = + let variable: Parser = let isFirstVariableChar c = isLetter c let isVariableChar c = isLetter c || isDigit c || c = '_' From ef7ee4499d44cc251dc883049ef3ff52b6614f11 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Sat, 26 Apr 2025 10:25:11 +0300 Subject: [PATCH 08/50] correct whitespace parsing --- .../LambdaInterpreter.Tests/ParserTests.fs | 23 +++++++++++-------- .../LambdaInterpreter/Parser.fs | 12 +++++----- 2 files changed, 19 insertions(+), 16 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs index 71b953b..03902a7 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs @@ -19,10 +19,12 @@ let testParser_WhiteSpace () = [ "", whitespaceOpt, Some 0; "\t", whitespaceOpt, Some 1; - " \n", whitespaceOpt, Some 4; + " \t\t ", whitespaceOpt, Some 6; + " \n", whitespaceOpt, Some 3; "", whitespace, None; " ", whitespace, Some 1; - "\n", whitespace, Some 1; + "\n", whitespace, None; + " \t\t a", whitespace, Some 8; "a1", whitespace, None; ] |> runTest @@ -70,12 +72,13 @@ 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 11; + "( ((ololo )) )", operand, Some 15; "\\x.y", operand, None; - "(first second)", operand, Some 14; + "(first second )", operand, Some 16; "(\\u v w.v)", operand, Some 10; "((\\x.x) i j)", operand, Some 12; ] |> runTest @@ -86,13 +89,13 @@ let testParser_Application () = "a", application, Some 1; "(var_1)", application, Some 7; "X Y", application, Some 3; - "(ololo) (abc)", application, Some 13; + "( ololo ) (abc)", application, Some 15; "a1 a2 a3", application, Some 14; "(_xyz)", application, None; - "(var1) 2var", 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 28; + "( (\\A1 B2 C3.A1) ololo) var1", application, Some 30; ] |> runTest [] @@ -113,7 +116,7 @@ let testParser_Abstraction () = let testParser_Term () = [ "var1", term, Some 4; - "((ololo))", term, Some 9; + "((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; @@ -152,9 +155,9 @@ let testParser_Definition () = [] let testParser_Expression () = [ - "let S = \\x y z.x z (y z)", expression, Some 24; + "let S = \\x y z.x z (y z)\n", expression, Some 25; "let K = \\x y.x", expression, Some 14; - "S K K", expression, Some 5; + "S K K \n", expression, Some 7; "\n", expression, Some 1; " \n", expression, Some 8; "_wewq", expression, None; diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs index 4d6bedd..7ca67f9 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs @@ -6,11 +6,11 @@ open Primary /// Module dealing with the source text parsing. module Parser = - /// Accept 0 or more spaces. - let whitespaceOpt = spaces + /// Accept 0 or more whitespaces. + let whitespaceOpt = skipMany (choice [pchar ' '; pchar '\t']) - /// Accept 1 of more spaces. - let whitespace = spaces1 + /// Accept 1 of more whitespaces. + let whitespace = skipMany1 (choice [pchar ' '; pchar '\t']) /// Accept optional whitespace on the left of the given `parser`. let ( ?< ) parser = whitespaceOpt >>. parser @@ -35,7 +35,7 @@ module Parser = many1Satisfy2 isFirstVariableChar isVariableChar |>> Name /// Accept one or more of variable names. - let variables = variable .>>. many !> fun (h, t) -> h :: t + let variables = sepBy1 variable whitespace /// Accept a primary lambda term representation. let term, termRef = createParserForwardedToRef () @@ -52,7 +52,7 @@ module Parser = let applicationOpt, applicationOptRef = createParserForwardedToRef () applicationOptRef.Value <- - !>. applicationOpt |>> Apply + attempt (!>. applicationOpt) |>> Apply <|> preturn ApplicationOpt.Epsilon /// Accept a lambda term application or a single operand. From ca4f7d77a47b2f6b5717d6aba4c9af3614a3940e Mon Sep 17 00:00:00 2001 From: bygu4 Date: Sat, 26 Apr 2025 15:27:19 +0300 Subject: [PATCH 09/50] refactor the interpreter, check for keywords and use regex during variable parsing --- .../LambdaInterpreter.Tests/ParserTests.fs | 30 ++++--- .../LambdaInterpreter/Interpreter.fs | 82 +++++++++++-------- .../LambdaInterpreter/Parser.fs | 49 ++++++----- .../LambdaInterpreter/Program.fs | 31 +++++-- .../LambdaInterpreter/Syntax/AST.fs | 15 ++-- .../LambdaInterpreter/Syntax/Primary.fs | 5 +- 6 files changed, 129 insertions(+), 83 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs index 03902a7..698d2de 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs @@ -20,22 +20,23 @@ let testParser_WhiteSpace () = "", whitespaceOpt, Some 0; "\t", whitespaceOpt, Some 1; " \t\t ", whitespaceOpt, Some 6; - " \n", whitespaceOpt, Some 3; + " \n", whitespaceOpt, Some 4; "", whitespace, None; " ", whitespace, Some 1; - "\n", whitespace, None; + "\n", whitespace, Some 1; " \t\t a", whitespace, Some 8; "a1", whitespace, None; ] |> runTest [] -let testParser_LineEnd () = +let testParser_InputEnd () = [ - "", lineEnd, Some 0; - " ", lineEnd, Some 5; - "\n", lineEnd, Some 1; - " \n", lineEnd, Some 4; - "a12", lineEnd, None; + "", inputEnd, Some 0; + " ", inputEnd, Some 5; + "\n", inputEnd, Some 1; + " \n", inputEnd, Some 4; + "a12", inputEnd, None; + " 1 ", inputEnd, None; ] |> runTest [] @@ -50,6 +51,10 @@ let testParser_Variable () = "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; ] |> runTest [] @@ -96,6 +101,7 @@ let testParser_Application () = "(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; ] |> runTest [] @@ -119,7 +125,7 @@ let testParser_Term () = "((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; + "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; @@ -131,11 +137,13 @@ let testParser_Term () = 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; ] |> runTest [] @@ -150,6 +158,7 @@ let testParser_Definition () = "foo bar = baz", definition, None; "let v1 = v2", definition, Some 16; "let term = ", definition, None; + "let let = X Y Z", definition, None; ] |> runTest [] @@ -157,11 +166,12 @@ let testParser_Expression () = [ "let S = \\x y z.x z (y z)\n", expression, Some 25; "let K = \\x y.x", expression, Some 14; - "S K K \n", expression, Some 7; + "S K K \t\n", expression, Some 8; "\n", expression, Some 1; " \n", expression, Some 8; "_wewq", expression, None; "123\n", expression, None; "", expression, Some 0; "variable", expression, Some 8; + "let test = (\\x.x) y, ", expression, None; ] |> runTest diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index cd3b5f8..1b07f88 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -1,46 +1,60 @@ namespace LambdaInterpreter open System -open System.Text +open System.IO open FParsec open AST open Parser open Reduction -/// Module dealing with lambda term interpretation. -module Interpreter = - - /// Run the interpreter to the end of the given `stream`. - let runInterpreter (interactive: bool) (stream: CharStream<_>) = - let mutable vars = new Map ([]) - seq { - while not stream.IsEndOfStream do - if interactive then printf "-> " - let reply = expression stream - if reply.Status = Ok then - let expr = reply.Result |> buildAST_Expression - match expr with - | Definition (var, term) -> - vars <- vars.Add (var, substituteMany term vars) - | Result term -> - let result = substituteMany term vars |> reduce |> toString - if interactive then printfn "%s" result - yield Result.Ok result - | None -> () - else - let message = reply.Error.Head.ToString () - if interactive then printfn "%s" message - yield Result.Error message +/// Class representing the lambda term interpreter. +type Interpreter (stream: Stream, ?interactive: bool) = + let reader = new StreamReader (stream) + let mutable vars = new Map ([]) + let mutable error = false + + /// Create interpreter for the standard console input. + new () = new Interpreter (Console.OpenStandardInput ()) + + /// Create interpreter for the source file at the given `path`. + new (path: string) = new Interpreter (File.OpenRead path) + + /// Whether the interpreter is interactive. + member _.IsInteractive: bool = defaultArg interactive false + + /// Whether the end of stream was reached by the interpreter. + member _.EndOfStream: bool = reader.EndOfStream + + /// Whether an error occurred during the interpretation. + member _.HadError: bool = error + + /// Analyze the next line in the stream and get the interpretation result. + member _.RunOnNextLineAsync (): Async> = + + /// Interpret the given `primary` expression representation. + let interpretExpression primary = + match buildAST_Expression primary with + | Definition (var, term) -> + vars <- vars.Add (var, substituteMany term vars) + Result.Ok String.Empty + | Result term -> + let result = substituteMany term vars |> reduce |> toString + Result.Ok result + | Empty -> Result.Ok String.Empty + + async { + let! line = reader.ReadLineAsync () |> Async.AwaitTask + let parserResult = line |> run expression + return + match parserResult with + | Success (expr, _, _) -> interpretExpression expr + | Failure (msg, _, _) -> + error <- true + Result.Error msg } - /// Run the interpreter on a source file at the given `path`. - let runInterpreterOnFile (path: string) = - use stream = new CharStream<_> (path, Encoding.UTF8) - runInterpreter false stream + interface IDisposable with - /// Interactively run the interpreter in the console. - let runInterpreterInConsole () = - use inputStream = Console.OpenStandardInput () - let stream = new CharStream<_> (inputStream, Encoding.UTF8) - runInterpreter true stream + /// Free resources used by the interpreter. + member _.Dispose () = reader.Dispose () diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs index 7ca67f9..485da82 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs @@ -6,11 +6,17 @@ open Primary /// Module dealing with the source text parsing. module Parser = + let variablePattern = @"[a-zA-Z][a-zA-Z0-9_]*" + let declarationKeyword = "let" + + let keywords = [declarationKeyword] + let isKeyword str = List.contains str keywords + /// Accept 0 or more whitespaces. - let whitespaceOpt = skipMany (choice [pchar ' '; pchar '\t']) + let whitespaceOpt = spaces - /// Accept 1 of more whitespaces. - let whitespace = skipMany1 (choice [pchar ' '; pchar '\t']) + /// Accept 1 or more whitespaces. + let whitespace = spaces1 /// Accept optional whitespace on the left of the given `parser`. let ( ?< ) parser = whitespaceOpt >>. parser @@ -24,15 +30,21 @@ module Parser = /// Accept whitespace on the right of the given `parser`. let ( !> ) parser = parser .>> whitespace - /// Accept the end of line with optional whitespace. - let lineEnd = (?<)(skipNewline <|> eof) + /// Accept optional whitespace followed by end of the input. + let inputEnd = (?<)eof - /// Accept the variable name. - let variable: Parser = - let isFirstVariableChar c = isLetter c - let isVariableChar c = isLetter c || isDigit c || c = '_' + /// Modifies the given parser `reply` to check whether the given `predicate` is not satisfied. + let except (predicate: 'a -> bool) (reply: Reply<'a>) = + if reply.Status = ReplyStatus.Ok then + if reply.Result |> predicate |> not then Reply reply.Result + else Reply ( + ReplyStatus.Error, + ErrorMessage.Unexpected $"Unexpected value: {reply.Result}" |> ErrorMessageList + ) + else reply - many1Satisfy2 isFirstVariableChar isVariableChar |>> Name + /// Accept the variable name. + let variable: Parser = regex variablePattern >> except isKeyword |>> Name /// Accept one or more of variable names. let variables = sepBy1 variable whitespace @@ -45,9 +57,6 @@ module Parser = between ((?>)(pchar '(')) ((?<)(pchar ')')) term |>> Brackets <|> (variable |>> Variable) - /// Accept a lambda abstraction. - let abstraction = between (pchar '\\') (pchar '.') variables .>>. term |>> Abstraction - /// Accept an optional lambda term application. let applicationOpt, applicationOptRef = createParserForwardedToRef () @@ -55,6 +64,9 @@ module Parser = attempt (!>. applicationOpt) |>> Apply <|> preturn ApplicationOpt.Epsilon + /// Accept a lambda abstraction. + let abstraction = between (pchar '\\') (pchar '.') variables .>>. term |>> Abstraction + /// Accept a lambda term application or a single operand. let application = operand .>>. applicationOpt |>> Application @@ -63,14 +75,11 @@ module Parser = /// Accept a variable declaration. let declaration = pstring "let" >>. !declaration .>> pchar '=' .>>. !> Definition - /// Accept an optional expression of a program. + /// Accept an expression or an empty string. let expressionOpt = choice [definition; term |>> Result; preturn Epsilon] - /// Accept an expression of a program or a line break. - let expression = expressionOpt .>> lineEnd - - /// Accept a program as a list of expressions. - let program = many expression + /// Accept an expression or an empty string followed by end of the input. + let expression = expressionOpt .>> inputEnd diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index 1d59dbe..ea40236 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -1,6 +1,6 @@ open System -open LambdaInterpreter.Interpreter +open LambdaInterpreter let printInfo () = printfn " @@ -37,6 +37,25 @@ Examples: S K K " +type ExitCode = + | Success = 0 + | Error = 1 + +/// Run the given `interpreter` to the end of stream. +let runInterpreter (interpreter: Interpreter) = + while not interpreter.EndOfStream do + async { + if interpreter.IsInteractive then printf "-> " + let! output = interpreter.RunOnNextLineAsync () + do + match output with + | Ok message | Error message -> printfn "%s" message + } |> Async.RunSynchronously + +let getExitCode (interpreter: Interpreter) = + if interpreter.IsInteractive || not interpreter.HadError then ExitCode.Success + else ExitCode.Error + let args = Environment.GetCommandLineArgs () if Array.contains "-h" args || Array.contains "--help" args then @@ -44,9 +63,11 @@ if Array.contains "-h" args || Array.contains "--help" args then exit 0 printInfo () -let output = runInterpreterInConsole () -let hasErrors = output |> Seq.exists (function | Error _ -> true | Ok _ -> false) -let exitCode = if hasErrors then 1 else 0 +let interpreter = + if args.Length = 1 then new Interpreter (args.[0]) + else new Interpreter () + +using interpreter runInterpreter -exit exitCode +getExitCode interpreter |> int |> exit diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index 1056665..679df47 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -6,7 +6,7 @@ open Primary /// Module dealing with finalized syntax trees. module AST = - /// The definition of lambda term. + /// Definition of the lambda term. type LambdaTerm = | Variable of Variable | Abstraction of Variable * LambdaTerm @@ -16,10 +16,7 @@ module AST = type Expression = | Definition of Variable * LambdaTerm | Result of LambdaTerm - | None - - /// The finalized program representation. - type Program = Expression seq + | Empty /// Build AST of a lambda term using the `primary` representation. let buildAST_Term: Primary.Term -> LambdaTerm = Unchecked.defaultof<_> @@ -54,11 +51,9 @@ module AST = /// Build a finalized expression representation from the `primary` one. let buildAST_Expression (primary: Primary.Expression) = match primary with - | Primary.Definition (variable, term) -> - Definition (variable, buildAST_Term term) - | Primary.Result term -> - Result (buildAST_Term term) - | Epsilon -> None + | Primary.Definition (variable, term) -> Definition (variable, buildAST_Term term) + | Primary.Result term -> Result (buildAST_Term term) + | Epsilon -> Empty /// Get a string representation of the given lambda `term`. let rec toString (term: LambdaTerm) = diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs index afd1d51..33c5291 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs @@ -24,11 +24,8 @@ module Primary = | Variable of Variable | Brackets of Term - /// An expression as a logical unit of the program. + /// An expression as a variable definition or a term result. type Expression = | Definition of Variable * Term | Result of Term | Epsilon - - /// Program as a list of expressions. - type Program = Expression list From 74d00b9fd243add908054c34321f87e548d52798 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Sat, 26 Apr 2025 18:50:12 +0300 Subject: [PATCH 10/50] refactor, move exit codes to separate file, correct interpreter --- .../LambdaInterpreter/ExitCode.fs | 20 ++++++ .../LambdaInterpreter/Interpreter.fs | 10 ++- .../LambdaInterpreter.fsproj | 3 +- .../LambdaInterpreter/Program.fs | 66 +++++++++++-------- .../LambdaInterpreter/Syntax/AST.fs | 34 +++++----- .../LambdaInterpreter/{ => Syntax}/Parser.fs | 13 ++-- 6 files changed, 92 insertions(+), 54 deletions(-) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter/ExitCode.fs rename Tasks/LambdaInterpreter/LambdaInterpreter/{ => Syntax}/Parser.fs (85%) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/ExitCode.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/ExitCode.fs new file mode 100644 index 0000000..df7537a --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/ExitCode.fs @@ -0,0 +1,20 @@ +namespace LambdaInterpreter + +/// Module containing utility regarding the exit code of the app. +module ExitCode = + + type ExitCode = + + /// The program execution was successful. + | Success = 0 + + /// An syntax error has occurred during source file interpretation. + | SyntaxError = 1 + + /// The given source file was not found. + | FileNotFound = 2 + + /// Get the exit code of the program according to the state of the given `interpreter`. + let getExitCode (interpreter: Interpreter) = + if interpreter.IsInteractive || not interpreter.HadError then ExitCode.Success + else ExitCode.SyntaxError diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index 1b07f88..b2cb5d6 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -15,7 +15,7 @@ type Interpreter (stream: Stream, ?interactive: bool) = let mutable error = false /// Create interpreter for the standard console input. - new () = new Interpreter (Console.OpenStandardInput ()) + new () = new Interpreter (Console.OpenStandardInput (), true) /// Create interpreter for the source file at the given `path`. new (path: string) = new Interpreter (File.OpenRead path) @@ -54,6 +54,14 @@ type Interpreter (stream: Stream, ?interactive: bool) = Result.Error msg } + /// Run the interpreter until the end of stream. + /// Yield interpretation result for each of the lines. + member self.RunToEnd (): Result seq = + seq { + while not self.EndOfStream do + yield Async.RunSynchronously <| self.RunOnNextLineAsync () + } + interface IDisposable with /// Free resources used by the interpreter. diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj index 1bb52d9..c22605f 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -9,9 +9,10 @@ - + + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index ea40236..57541d4 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -1,7 +1,10 @@ open System +open System.IO open LambdaInterpreter +open ExitCode +/// Print generic info about the app with a help suggestion. let printInfo () = printfn " Lambda Interpreter @@ -11,6 +14,7 @@ A simple interpreter of lambda term expressions. For more info use -h option. " +/// Print command line help. let printHelp () = printfn " Lambda Interpreter @@ -37,37 +41,45 @@ Examples: S K K " -type ExitCode = - | Success = 0 - | Error = 1 - -/// Run the given `interpreter` to the end of stream. -let runInterpreter (interpreter: Interpreter) = - while not interpreter.EndOfStream do - async { - if interpreter.IsInteractive then printf "-> " - let! output = interpreter.RunOnNextLineAsync () - do - match output with - | Ok message | Error message -> printfn "%s" message - } |> Async.RunSynchronously - -let getExitCode (interpreter: Interpreter) = - if interpreter.IsInteractive || not interpreter.HadError then ExitCode.Success - else ExitCode.Error +/// Print a pointer indicating the start of input when running the interactive interpreter. +let printInputPointer () = + printf "-> " + +/// 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`. +let handleOutput (output: Result) = + match output with + | Ok result -> + if result.Length > 0 then printMessage ConsoleColor.Green (result + "\n") + | Error message -> + printMessage ConsoleColor.Yellow message let args = Environment.GetCommandLineArgs () if Array.contains "-h" args || Array.contains "--help" args then printHelp () - exit 0 - -printInfo () - -let interpreter = - if args.Length = 1 then new Interpreter (args.[0]) - else new Interpreter () - -using interpreter runInterpreter + exit <| int ExitCode.Success + +let interpreter = + try + if args.Length = 2 then new Interpreter (args.[1]) + else new Interpreter () + with + | :? FileNotFoundException | :? DirectoryNotFoundException as ex -> + printMessage ConsoleColor.Red (ex.Message + "\n") + exit <| int ExitCode.FileNotFound + +if interpreter.IsInteractive then printInfo () ; printInputPointer () + +using interpreter (fun interpreter -> + for output in interpreter.RunToEnd () do + handleOutput output + if interpreter.IsInteractive then printInputPointer () +) getExitCode interpreter |> int |> exit diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index 679df47..6dae896 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -19,25 +19,23 @@ module AST = | Empty /// Build AST of a lambda term using the `primary` representation. - let buildAST_Term: Primary.Term -> LambdaTerm = Unchecked.defaultof<_> - let buildAST_Term_Ref = ref buildAST_Term + let rec buildAST_Term (primary: Primary.Term) = + + /// Convert `primary` operand representation to the lambda term. + let buildAST_Operand (primary: Primary.Operand) = + match primary with + | Primary.Variable var -> Variable var + | Brackets term -> buildAST_Term term + + /// Build AST of lambda term application using term on the `left` and the rest on `right`. + let rec buildAST_Application (left: LambdaTerm, right: Primary.ApplicationOpt) = + match right with + | Apply (operand, rest) -> + let right = buildAST_Operand operand + let partial = Application (left, right) + buildAST_Application (partial, rest) + | ApplicationOpt.Epsilon -> left - /// Convert `primary` operand representation to the lambda term. - let buildAST_Operand (primary: Primary.Operand) = - match primary with - | Primary.Variable var -> Variable var - | Brackets term -> buildAST_Term term - - /// Build AST of lambda term application using term on the `left` and the rest on `right`. - let rec buildAST_Application (left: LambdaTerm, right: Primary.ApplicationOpt) = - match right with - | Apply (operand, rest) -> - let right = buildAST_Operand operand - let partial = Application (left, right) - buildAST_Application (partial, rest) - | ApplicationOpt.Epsilon -> left - - buildAST_Term_Ref.Value <- fun primary -> match primary with | Primary.Application (operand, rest) -> let operand = buildAST_Operand operand diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs similarity index 85% rename from Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs rename to Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs index 485da82..926f6d1 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs @@ -33,18 +33,17 @@ module Parser = /// Accept optional whitespace followed by end of the input. let inputEnd = (?<)eof - /// Modifies the given parser `reply` to check whether the given `predicate` is not satisfied. - let except (predicate: 'a -> bool) (reply: Reply<'a>) = - if reply.Status = ReplyStatus.Ok then - if reply.Result |> predicate |> not then Reply reply.Result - else Reply ( + /// 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 $"Unexpected value: {reply.Result}" |> ErrorMessageList + ErrorMessage.Unexpected $"\"{reply.Result}\" is reserved as a keyword" |> ErrorMessageList ) else reply /// Accept the variable name. - let variable: Parser = regex variablePattern >> except isKeyword |>> Name + let variable: Parser = regex variablePattern >> exceptKeyword |>> Name /// Accept one or more of variable names. let variables = sepBy1 variable whitespace From 07526b5e03cc0476e3d1532e93fe6a199f1bbd2f Mon Sep 17 00:00:00 2001 From: bygu4 Date: Sat, 26 Apr 2025 19:13:22 +0300 Subject: [PATCH 11/50] update term to string transformation --- .../LambdaInterpreter/Syntax/AST.fs | 22 ++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index 6dae896..642e227 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -54,8 +54,20 @@ module AST = | Epsilon -> Empty /// Get a string representation of the given lambda `term`. - let rec toString (term: LambdaTerm) = - match term with - | Variable (Name var) -> var - | Application (left, right) -> $"{toString left} {toString right}" - | Abstraction (Name var, term) -> $"(\\{var}.{toString term})" + let toString (term: LambdaTerm) = + + /// Get a string representation of the given lambda `term`. + /// Add brackets if necessary for a proper operation priority. + let rec toStringInternal (term: LambdaTerm) (withBrackets: bool) = + match term with + | Variable (Name var) -> var + | Application (left, right) -> + let left = $"{toStringInternal left left.IsAbstraction}" + let right = $"{toStringInternal right right.IsApplication}" + let term = $"{left} {right}" + if withBrackets then $"({term})" else term + | Abstraction (Name var, term) -> + let term = $"\\{var}.{toStringInternal term false}" + if withBrackets then $"({term})" else term + + toStringInternal term false From 7078d15ad4b32cde803e2a7bfd2cfd26b588469c Mon Sep 17 00:00:00 2001 From: bygu4 Date: Sat, 26 Apr 2025 20:03:22 +0300 Subject: [PATCH 12/50] add ColorScheme module, refactor --- .../LambdaInterpreter/ColorScheme.fs | 20 +++++++++++++++++++ .../LambdaInterpreter/Interpreter.fs | 2 ++ .../LambdaInterpreter.fsproj | 1 + .../LambdaInterpreter/Program.fs | 20 ++++++++++--------- 4 files changed, 34 insertions(+), 9 deletions(-) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter/ColorScheme.fs diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/ColorScheme.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/ColorScheme.fs new file mode 100644 index 0000000..590e99e --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/ColorScheme.fs @@ -0,0 +1,20 @@ +namespace LambdaInterpreter + +open System + +/// 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 + + /// Definition of the color scheme of the console application. + type ColorScheme = SuccessColor * ErrorColor + + /// 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.White, Color ConsoleColor.Red diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index b2cb5d6..0f0568b 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -9,6 +9,8 @@ open Parser open Reduction /// Class representing the lambda term interpreter. +/// Create a parser instance to be run on the given `stream`. +/// Use `interactive` parameter if the interpreter is meant to be run in console. type Interpreter (stream: Stream, ?interactive: bool) = let reader = new StreamReader (stream) let mutable vars = new Map ([]) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj index c22605f..1075a01 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -13,6 +13,7 @@ + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index 57541d4..7ecae1f 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -3,6 +3,7 @@ open System.IO open LambdaInterpreter open ExitCode +open ColorScheme /// Print generic info about the app with a help suggestion. let printInfo () = @@ -51,13 +52,13 @@ let printMessage (color: ConsoleColor) (message: string) = printfn "%s" message Console.ResetColor () -/// Print the result of interpretation according to the given `output`. -let handleOutput (output: Result) = +/// 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 -> - if result.Length > 0 then printMessage ConsoleColor.Green (result + "\n") + if result.Length > 0 then printMessage success (result + "\n") | Error message -> - printMessage ConsoleColor.Yellow message + printMessage error message let args = Environment.GetCommandLineArgs () @@ -74,12 +75,13 @@ let interpreter = printMessage ConsoleColor.Red (ex.Message + "\n") exit <| int ExitCode.FileNotFound -if interpreter.IsInteractive then printInfo () ; printInputPointer () +using interpreter (fun interpreter -> + let colorScheme = getColorScheme interpreter + if interpreter.IsInteractive then printInfo () ; printInputPointer () -using interpreter (fun interpreter -> for output in interpreter.RunToEnd () do - handleOutput output + handleOutput colorScheme output if interpreter.IsInteractive then printInputPointer () -) -getExitCode interpreter |> int |> exit + getExitCode interpreter |> int |> exit +) From ae199ba2defafcef7ebf40225eab55b9b035d7d0 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Sun, 27 Apr 2025 01:03:20 +0300 Subject: [PATCH 13/50] add Console directory --- .../LambdaInterpreter/{ => Console}/ColorScheme.fs | 0 .../LambdaInterpreter/{ => Console}/ExitCode.fs | 0 .../LambdaInterpreter/LambdaInterpreter.fsproj | 4 ++-- Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs | 2 +- 4 files changed, 3 insertions(+), 3 deletions(-) rename Tasks/LambdaInterpreter/LambdaInterpreter/{ => Console}/ColorScheme.fs (100%) rename Tasks/LambdaInterpreter/LambdaInterpreter/{ => Console}/ExitCode.fs (100%) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/ColorScheme.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs similarity index 100% rename from Tasks/LambdaInterpreter/LambdaInterpreter/ColorScheme.fs rename to Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/ExitCode.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs similarity index 100% rename from Tasks/LambdaInterpreter/LambdaInterpreter/ExitCode.fs rename to Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj index 1075a01..afd9cad 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -12,8 +12,8 @@ - - + + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index 7ecae1f..5ec3560 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -2,8 +2,8 @@ open System open System.IO open LambdaInterpreter -open ExitCode open ColorScheme +open ExitCode /// Print generic info about the app with a help suggestion. let printInfo () = From 16fa87a8944bf0627a15c5a679a927d6d82968aa Mon Sep 17 00:00:00 2001 From: bygu4 Date: Sun, 27 Apr 2025 13:23:41 +0300 Subject: [PATCH 14/50] add special commands, refactor --- .../InterpreterTests.fs | 8 +++ .../LambdaInterpreter.Tests.fsproj | 6 ++ .../TestFiles/Successful/Test01.txt | 3 + .../TestFiles/Successful/Test02.txt | 0 .../LambdaInterpreter/Console/ExitCode.fs | 2 +- .../LambdaInterpreter/Interpreter.fs | 62 ++++++++++++++----- .../LambdaInterpreter.fsproj | 1 + .../LambdaInterpreter/Program.fs | 36 +++++------ .../LambdaInterpreter/Syntax/AST.fs | 2 + .../LambdaInterpreter/Syntax/Keywords.fs | 35 +++++++++++ .../LambdaInterpreter/Syntax/Parser.fs | 24 ++++--- .../LambdaInterpreter/Syntax/Primary.fs | 7 +++ 12 files changed, 141 insertions(+), 45 deletions(-) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test01.txt create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test02.txt create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs new file mode 100644 index 0000000..bb75ec4 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -0,0 +1,8 @@ +module Interpreter.Tests + +open NUnit.Framework +open FsUnit + +open LambdaInterpreter + + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj index da51ce7..6e2c999 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj @@ -8,6 +8,7 @@ + @@ -21,4 +22,9 @@ + + + Always + + \ No newline at end of file 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..788a0a5 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test01.txt @@ -0,0 +1,3 @@ +let S = \x y z.x z (y z) +let K = \x y.x +S K K \ 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..e69de29 diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs index df7537a..59c4cf6 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs @@ -16,5 +16,5 @@ module ExitCode = /// Get the exit code of the program according to the state of the given `interpreter`. let getExitCode (interpreter: Interpreter) = - if interpreter.IsInteractive || not interpreter.HadError then ExitCode.Success + if interpreter.IsInteractive || not interpreter.SyntaxError then ExitCode.Success else ExitCode.SyntaxError diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index 0f0568b..1c6ed5b 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -4,38 +4,68 @@ open System open System.IO open FParsec +open Keywords open AST open Parser open Reduction /// Class representing the lambda term interpreter. -/// Create a parser instance to be run on the given `stream`. -/// Use `interactive` parameter if the interpreter is meant to be run in console. -type Interpreter (stream: Stream, ?interactive: bool) = +type Interpreter private (stream: Stream, interactive: bool) = let reader = new StreamReader (stream) let mutable vars = new Map ([]) let mutable error = false - /// Create interpreter for the standard console input. - new () = new Interpreter (Console.OpenStandardInput (), true) + /// Print help info to the standard output. + static member PrintHelp () = 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}} - /// Create interpreter for the source file at the given `path`. - new (path: string) = new Interpreter (File.OpenRead path) +Examples: + -> {DeclarationKeyword} S = \\x y z.x z (y z) + -> {DeclarationKeyword} K = \\x y.x + -> S K K + \\z.z + +Commands: + {ClearKeyword}\t\t Clear the list of defined variables + {HelpKeyword}\t\t Display help + {ExitKeyword}\t\t Stop the execution and exit +" + + /// Create an interactive interpreter for the standard console input. + static member StartInteractive (): Interpreter = + new Interpreter (Console.OpenStandardInput (), true) + + /// Create an interpreter to run on source file at the given `path`. + static member StartOnFile (path: string): Interpreter = + new Interpreter (File.OpenRead path, false) /// Whether the interpreter is interactive. - member _.IsInteractive: bool = defaultArg interactive false + member _.IsInteractive: bool = interactive /// Whether the end of stream was reached by the interpreter. member _.EndOfStream: bool = reader.EndOfStream - /// Whether an error occurred during the interpretation. - member _.HadError: bool = error + /// Whether a syntax error occurred during the interpretation. + member _.SyntaxError: bool = error /// Analyze the next line in the stream and get the interpretation result. member _.RunOnNextLineAsync (): Async> = + /// Execute the given special interpreter `command`. + let runCommand (command: SpecialCommand) = + match command with + | Clear -> vars <- new Map ([]) + | Help -> if interactive then Interpreter.PrintHelp () + | Exit -> reader.Close () + Result.Ok String.Empty + /// Interpret the given `primary` expression representation. - let interpretExpression primary = + let interpretExpression (primary: Primary.Expression) = match buildAST_Expression primary with | Definition (var, term) -> vars <- vars.Add (var, substituteMany term vars) @@ -43,6 +73,7 @@ type Interpreter (stream: Stream, ?interactive: bool) = | Result term -> let result = substituteMany term vars |> reduce |> toString Result.Ok result + | Command command -> runCommand command | Empty -> Result.Ok String.Empty async { @@ -58,13 +89,16 @@ type Interpreter (stream: Stream, ?interactive: bool) = /// Run the interpreter until the end of stream. /// Yield interpretation result for each of the lines. - member self.RunToEnd (): Result seq = + member self.RunToEnd (): Async> seq = seq { - while not self.EndOfStream do - yield Async.RunSynchronously <| self.RunOnNextLineAsync () + while stream.CanRead do + yield self.RunOnNextLineAsync () } 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 afd9cad..901df02 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -7,6 +7,7 @@ + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index 5ec3560..2f61e5c 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -5,14 +5,14 @@ open LambdaInterpreter open ColorScheme open ExitCode -/// Print generic info about the app with a help suggestion. -let printInfo () = +/// Print header with general info about the app and a help suggestion. +let printHeader () = printfn " Lambda Interpreter ------------------ A simple interpreter of lambda term expressions. -For more info use -h option. +Type 'help' for more info. " /// Print command line help. @@ -21,6 +21,8 @@ let printHelp () = Lambda Interpreter ------------------ A simple interpreter of lambda term expressions. +It can either be run interactively using the standard input, +or on a specified source file. Usage: LambdaInterpreter [options]\t\t Run interpreter interactively @@ -28,19 +30,7 @@ Usage: Options: -h|--help\t\t Display help - -Syntax: - variable\t\t [letter][letter|digit|_]* - term\t\t {variable}|{abstraction}|{application}|({term}) - application\t\t {term} {term} - abstraction\t\t \\{variables}.{term} - definition\t\t let {variable} = {term} - -Examples: - let S = \\x y z.x z (y z) - let K = \\x y.x - S K K -" +" Interpreter.PrintHelp () /// Print a pointer indicating the start of input when running the interactive interpreter. let printInputPointer () = @@ -68,20 +58,22 @@ if Array.contains "-h" args || Array.contains "--help" args then let interpreter = try - if args.Length = 2 then new Interpreter (args.[1]) - else new Interpreter () + if args.Length = 2 then Interpreter.StartOnFile (args[1]) + else Interpreter.StartInteractive () with | :? FileNotFoundException | :? DirectoryNotFoundException as ex -> printMessage ConsoleColor.Red (ex.Message + "\n") exit <| int ExitCode.FileNotFound -using interpreter (fun interpreter -> +async { + use interpreter = interpreter let colorScheme = getColorScheme interpreter - if interpreter.IsInteractive then printInfo () ; printInputPointer () + if interpreter.IsInteractive then printHeader () ; printInputPointer () - for output in interpreter.RunToEnd () do + for nextLine in interpreter.RunToEnd () do + let! output = nextLine handleOutput colorScheme output if interpreter.IsInteractive then printInputPointer () getExitCode interpreter |> int |> exit -) +} |> Async.RunSynchronously diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index 642e227..f8f55f9 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -16,6 +16,7 @@ module AST = type Expression = | Definition of Variable * LambdaTerm | Result of LambdaTerm + | Command of SpecialCommand | Empty /// Build AST of a lambda term using the `primary` representation. @@ -51,6 +52,7 @@ module AST = match primary with | Primary.Definition (variable, term) -> Definition (variable, buildAST_Term term) | Primary.Result term -> Result (buildAST_Term term) + | Primary.Command command -> Command command | Epsilon -> Empty /// Get a string representation of the given lambda `term`. diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs new file mode 100644 index 0000000..805cf96 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs @@ -0,0 +1,35 @@ +namespace LambdaInterpreter + +/// 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 clearing the list of defined variables. + [] + let ClearKeyword = "clear" + + /// Keyword for displaying help info. + [] + let HelpKeyword = "help" + + /// Keyword for exiting the interpreter. + [] + let ExitKeyword = "exit" + + /// The list of defined keywords. + let keywords = [ + DeclarationKeyword; + ClearKeyword; + HelpKeyword; + 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 index 926f6d1..b2dc550 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs @@ -1,17 +1,13 @@ namespace LambdaInterpreter open FParsec + +open Keywords open Primary /// Module dealing with the source text parsing. module Parser = - let variablePattern = @"[a-zA-Z][a-zA-Z0-9_]*" - let declarationKeyword = "let" - - let keywords = [declarationKeyword] - let isKeyword str = List.contains str keywords - /// Accept 0 or more whitespaces. let whitespaceOpt = spaces @@ -43,7 +39,7 @@ module Parser = else reply /// Accept the variable name. - let variable: Parser = regex variablePattern >> exceptKeyword |>> Name + let variable: Parser = regex VariablePattern >> exceptKeyword |>> Name /// Accept one or more of variable names. let variables = sepBy1 variable whitespace @@ -77,8 +73,20 @@ module Parser = /// Accept a variable declaration with assignment. let definition = !>declaration .>> pchar '=' .>>. !> Definition + /// Accept a keyword for clearing the variable list. + let clear: Parser = pstring ClearKeyword >>. preturn (Command Clear) + + /// Accept a keyword for displaying help. + let help: Parser = pstring HelpKeyword >>. preturn (Command Help) + + /// Accept a keyword for exiting the interpreter. + let exit: Parser = pstring ExitKeyword >>. preturn (Command Exit) + + /// Accept a special interpreter command. + let command = choice [clear; help; exit] + /// Accept an expression or an empty string. - let expressionOpt = choice [definition; term |>> Result; preturn Epsilon] + let expressionOpt = choice [attempt term |>> Result; definition; command; preturn Epsilon] /// 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 index 33c5291..3fa77e0 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs @@ -6,6 +6,12 @@ type Variable = Name of string /// A list of variables. type Variables = Variable list +/// A special command for managing the interpreter execution. +type SpecialCommand = + | Clear + | Help + | Exit + /// Module defining primary syntax constructions. module Primary = @@ -28,4 +34,5 @@ module Primary = type Expression = | Definition of Variable * Term | Result of Term + | Command of SpecialCommand | Epsilon From 569718db14eb205e6be10a0394b085f280a98bfa Mon Sep 17 00:00:00 2001 From: bygu4 Date: Sun, 27 Apr 2025 14:01:09 +0300 Subject: [PATCH 15/50] update parser tests --- .../LambdaInterpreter.Tests/ParserTests.fs | 25 ++++++++++++++++++- .../LambdaInterpreter/Program.fs | 2 +- 2 files changed, 25 insertions(+), 2 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs index 698d2de..aedc2af 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs @@ -55,6 +55,7 @@ let testParser_Variable () = "let", variable, None; "letvar", variable, Some 6; "not_a_let", variable, Some 9; + "exit", variable, None; ] |> runTest [] @@ -144,6 +145,8 @@ let testParser_Declaration () = "foo", declaration, None; "bar ololo", declaration, None; "let let", declaration, None; + "let help", declaration, None; + "let exitCode", declaration, Some 12; ] |> runTest [] @@ -159,19 +162,39 @@ let testParser_Definition () = "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 () = + [ + "clear", command, Some 5; + "help", command, Some 4; + "exit", command, Some 4; + "not_help", command, None; + "exitCode", command, Some 4; + " clear", command, None; + "exit \t ", command, Some 4; ] |> runTest [] let testParser_Expression () = [ "let S = \\x y z.x z (y z)\n", expression, Some 25; - "let K = \\x y.x", expression, Some 14; + "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 vars", expression, None; + "let ololo_exit = (\\x.\\y.x ) z\n", expression, Some 30; + "a clear", expression, None; + "\n exit", expression, None; ] |> runTest diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index 2f61e5c..667996a 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -29,7 +29,7 @@ Usage: LambdaInterpreter {path-to-file}\t Run interpreter on the given source file Options: - -h|--help\t\t Display help + -h|--help\t\t Display help and exit " Interpreter.PrintHelp () /// Print a pointer indicating the start of input when running the interactive interpreter. From f02b0ab9d9e5cf395a7c1795d58bf5c2853fb03e Mon Sep 17 00:00:00 2001 From: bygu4 Date: Sun, 27 Apr 2025 14:24:51 +0300 Subject: [PATCH 16/50] refactor main --- Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index 667996a..1cd0eda 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -68,12 +68,12 @@ let interpreter = async { use interpreter = interpreter let colorScheme = getColorScheme interpreter - if interpreter.IsInteractive then printHeader () ; printInputPointer () + if interpreter.IsInteractive then printHeader () for nextLine in interpreter.RunToEnd () do + if interpreter.IsInteractive then printInputPointer () let! output = nextLine handleOutput colorScheme output - if interpreter.IsInteractive then printInputPointer () getExitCode interpreter |> int |> exit } |> Async.RunSynchronously From 0b6d810379c3f5bba310d1d870cc76335a9c024f Mon Sep 17 00:00:00 2001 From: bygu4 Date: Sun, 27 Apr 2025 15:27:29 +0300 Subject: [PATCH 17/50] rename keywords, add clear buffer keyword --- .../LambdaInterpreter.Tests/ParserTests.fs | 6 ++++-- .../LambdaInterpreter/Interpreter.fs | 6 ++++-- .../LambdaInterpreter/Syntax/Keywords.fs | 11 ++++++++--- .../LambdaInterpreter/Syntax/Parser.fs | 9 ++++++--- .../LambdaInterpreter/Syntax/Primary.fs | 3 ++- 5 files changed, 24 insertions(+), 11 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs index aedc2af..7b42992 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs @@ -168,13 +168,15 @@ let testParser_Definition () = [] let testParser_Command () = [ - "clear", command, Some 5; + "reset", command, Some 5; "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 [] @@ -193,7 +195,7 @@ let testParser_Expression () = "variable", expression, Some 8; "let test = (\\x.x) y, ", expression, None; "help \t", expression, Some 7; - "clear vars", expression, None; + "clear buff", expression, None; "let ololo_exit = (\\x.\\y.x ) z\n", expression, Some 30; "a clear", expression, None; "\n exit", expression, None; diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index 1c6ed5b..687bd93 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -31,8 +31,9 @@ Examples: \\z.z Commands: - {ClearKeyword}\t\t Clear the list of defined variables + {ResetKeyword}\t\t Reset defined variables {HelpKeyword}\t\t Display help + {ClearKeyword}\t\t Clear console buffer {ExitKeyword}\t\t Stop the execution and exit " @@ -59,8 +60,9 @@ Commands: /// Execute the given special interpreter `command`. let runCommand (command: SpecialCommand) = match command with - | Clear -> vars <- new Map ([]) + | Reset -> vars <- new Map ([]) | Help -> if interactive then Interpreter.PrintHelp () + | Clear -> if interactive then Console.Clear () | Exit -> reader.Close () Result.Ok String.Empty diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs index 805cf96..a98a446 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs @@ -11,14 +11,18 @@ module Keywords = [] let DeclarationKeyword = "let" - /// Keyword for clearing the list of defined variables. + /// Keyword for resetting defined variables. [] - let ClearKeyword = "clear" + let ResetKeyword = "reset" /// 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" @@ -26,8 +30,9 @@ module Keywords = /// The list of defined keywords. let keywords = [ DeclarationKeyword; - ClearKeyword; + ResetKeyword; HelpKeyword; + ClearKeyword; ExitKeyword; ] diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs index b2dc550..f1739c2 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs @@ -73,17 +73,20 @@ module Parser = /// Accept a variable declaration with assignment. let definition = !>declaration .>> pchar '=' .>>. !> Definition - /// Accept a keyword for clearing the variable list. - let clear: Parser = pstring ClearKeyword >>. preturn (Command Clear) + /// Accept a keyword for resetting defined variables. + let reset: Parser = pstring ResetKeyword >>. preturn (Command Reset) /// 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 [clear; help; exit] + let command = choice [reset; help; clear; exit] /// Accept an expression or an empty string. let expressionOpt = choice [attempt term |>> Result; definition; command; preturn Epsilon] diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs index 3fa77e0..75a1165 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs @@ -8,8 +8,9 @@ type Variables = Variable list /// A special command for managing the interpreter execution. type SpecialCommand = - | Clear + | Reset | Help + | Clear | Exit /// Module defining primary syntax constructions. From 6607308bdce0fa12262922c7759dc34cb6b6c7fe Mon Sep 17 00:00:00 2001 From: bygu4 Date: Mon, 28 Apr 2025 00:54:26 +0300 Subject: [PATCH 18/50] add tests for the interpreter class --- .../InterpreterTests.fs | 163 ++++++++++++++++++ .../LambdaInterpreter.Tests/ParserTests.fs | 2 + .../TestFiles/Successful/Test02.txt | 10 ++ .../TestFiles/Successful/Test03.txt | 10 ++ .../TestFiles/Successful/Test04.txt | 6 + .../TestFiles/Successful/Test05.txt | 8 + .../TestFiles/Successful/Test06.txt | 7 + .../TestFiles/Successful/Test07.txt | 11 ++ .../TestFiles/Unsuccessful/Test01.txt | 13 ++ .../TestFiles/Unsuccessful/Test02.txt | 11 ++ .../TestFiles/Unsuccessful/Test03.txt | 15 ++ .../LambdaInterpreter/Interpreter.fs | 17 +- .../LambdaInterpreter/Program.fs | 5 - .../LambdaInterpreter/Syntax/AST.fs | 2 +- 14 files changed, 268 insertions(+), 12 deletions(-) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test03.txt create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test04.txt create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test05.txt create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test06.txt create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test07.txt create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test01.txt create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test02.txt create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test03.txt diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index bb75ec4..080e734 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -2,7 +2,170 @@ 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 e; + Ok e; + Ok "\\z.z"; + ]; + [ // Test 2 + Ok e; + Ok e; + Ok e; + Ok "ololo"; + Ok e; + Ok e; + Ok "a"; + Ok e; + Ok "\\V1.\\V2.V2 (\\x.V2 x)"; + Ok "\\x.\\y.\\x.x"; + Ok e; + ]; + [ // Test 3 + Ok e; + Ok e; + Ok e; + Ok e; + Ok e; + Ok e; + Ok "second third (\\x.x first)"; + Ok e; + Ok e; + Ok "second third" + Ok e; + ]; + [ // Test 4 + Ok "x y"; + Ok e; + Ok e; + Ok "x"; + Ok e; + Ok "\\y'.y y'"; + ]; + [ // Test 5 + Ok e; + Ok e; + Ok e; + Ok "\\y.ololo"; + Ok e; + Ok e; + Ok "snd"; + Ok "res"; + ]; + [ // Test 6 + Ok e; + Ok "a"; + Ok e; + Ok e; + ]; + [ // Test 7 + Ok e; + Ok e; + Ok "var"; + Ok e; + Ok "\\x.x"; + Ok e; + Ok "exitCode"; + Ok "helpMe"; + Ok "toClear"; + Ok "reset_vars"; + Ok "no_exit_1"; + Ok e; + ]; +] + +let unsuccessfulCasesResults: Result list list = [ + [ // Test 1 + Error e; + Error e; + Error e; + Error e; + Ok e; + Error e; + Error e; + Error e; + Ok e; + Error e; + Error e; + Ok e; + Ok "res"; + ]; + [ // Test 2 + Error e; + Error e; + Error e; + Error e; + Error e; + Ok e; + Error e; + Error e; + Error e; + Error e; + Error e; + Ok e; + ]; + [ // Test 3 + Error e; + Error e; + Ok e; + Error e; + Error e; + Error e; + Error e; + Error e; + Error e; + Ok e; + Error e; + Error e; + Error e; + Error e; + Error e; + Ok e; + ]; +] + +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 getOutput (interpreter: Interpreter) = + interpreter.RunToEnd () + |> Seq.map Async.RunSynchronously + |> Seq.toList + +let outputsMatch (actual: Result list) (expected: Result list) = + 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 = getOutput interpreter + output |> outputsMatch expectedOutput |> should be True + interpreter.SyntaxError |> should equal shouldFail diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs index 7b42992..972e893 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs @@ -132,6 +132,7 @@ let testParser_Term () = "\\x.\\y", term, None; "_q", term, None; "a, b, c", term, Some 1; + "\\X Y Z.Z \\t.X Y", term, Some 9; ] |> runTest [] @@ -199,4 +200,5 @@ let testParser_Expression () = "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, None; ] |> runTest diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test02.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test02.txt index e69de29..c5be3eb 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test02.txt +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test02.txt @@ -0,0 +1,10 @@ + +let I = \x.x + +I ololo + +let var = I a +var + +\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..482745b --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test03.txt @@ -0,0 +1,10 @@ +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..e55c7cf --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test04.txt @@ -0,0 +1,6 @@ +x y + +let x = \z.x +x y + +(\x y.x y) y \ 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..716dcf3 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test05.txt @@ -0,0 +1,8 @@ +let fst = \x y.x +let snd = \fst.\snd.snd +let res = (snd a fst) ololo +res +reset + +snd +res \ 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..05c8ab8 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test06.txt @@ -0,0 +1,7 @@ +let I = \x.x +I a + +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/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..5d9a624 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test02.txt @@ -0,0 +1,11 @@ +let let = a +let reset = B +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 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/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index 687bd93..08f1328 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -37,6 +37,10 @@ Commands: {ExitKeyword}\t\t Stop the execution and exit " + /// Print a pointer indicating the start of input when running the interactive interpreter. + static member PrintInputPointer () = + printf "-> " + /// Create an interactive interpreter for the standard console input. static member StartInteractive (): Interpreter = new Interpreter (Console.OpenStandardInput (), true) @@ -45,11 +49,12 @@ Commands: static member StartOnFile (path: string): Interpreter = new Interpreter (File.OpenRead path, false) - /// Whether the interpreter is interactive. + /// Whether the interpreter is being run in console. member _.IsInteractive: bool = interactive - /// Whether the end of stream was reached by the interpreter. - member _.EndOfStream: bool = reader.EndOfStream + /// 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 = error @@ -78,6 +83,7 @@ Commands: | Command command -> runCommand command | Empty -> Result.Ok String.Empty + if interactive then Interpreter.PrintInputPointer () async { let! line = reader.ReadLineAsync () |> Async.AwaitTask let parserResult = line |> run expression @@ -89,11 +95,10 @@ Commands: Result.Error msg } - /// Run the interpreter until the end of stream. - /// Yield interpretation result for each of the lines. + /// Run the interpreter while possible and yield result for each of the lines. member self.RunToEnd (): Async> seq = seq { - while stream.CanRead do + while self.CanRun do yield self.RunOnNextLineAsync () } diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index 1cd0eda..a23313f 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -32,10 +32,6 @@ Options: -h|--help\t\t Display help and exit " Interpreter.PrintHelp () -/// Print a pointer indicating the start of input when running the interactive interpreter. -let printInputPointer () = - printf "-> " - /// Print the given `message` to the standard output with the given `color`. let printMessage (color: ConsoleColor) (message: string) = Console.ForegroundColor <- color @@ -71,7 +67,6 @@ async { if interpreter.IsInteractive then printHeader () for nextLine in interpreter.RunToEnd () do - if interpreter.IsInteractive then printInputPointer () let! output = nextLine handleOutput colorScheme output diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index f8f55f9..2de0288 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -65,7 +65,7 @@ module AST = | Variable (Name var) -> var | Application (left, right) -> let left = $"{toStringInternal left left.IsAbstraction}" - let right = $"{toStringInternal right right.IsApplication}" + let right = $"{toStringInternal right (right.IsAbstraction || right.IsApplication)}" let term = $"{left} {right}" if withBrackets then $"({term})" else term | Abstraction (Name var, term) -> From 3da4a8256f7a10d3e6423b71e7e3711a0157b6ef Mon Sep 17 00:00:00 2001 From: bygu4 Date: Mon, 28 Apr 2025 01:21:09 +0300 Subject: [PATCH 19/50] add optional whitespace for abstraction --- .../LambdaInterpreter.Tests/ParserTests.fs | 8 ++++++-- .../LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs | 6 +++--- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs index 972e893..2a66dee 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs @@ -66,10 +66,11 @@ let testParser_Variables () = "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, None; + "a _ b", variables, Some 2; "1 2", variables, None; - " ololo ololo ", variables, None; + " ololo ololo ", variables, Some 15; "first, second", variables, Some 5; + "fst snd thd \t\n", variables, Some 18; ] |> runTest [] @@ -117,6 +118,8 @@ let testParser_Abstraction () = "\\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 [] @@ -133,6 +136,7 @@ let testParser_Term () = "_q", term, None; "a, b, c", term, Some 1; "\\X Y Z.Z \\t.X Y", term, Some 9; + "( \\ a b . z)", term, Some 14; ] |> runTest [] diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs index f1739c2..a5c22bc 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs @@ -41,8 +41,8 @@ module Parser = /// Accept the variable name. let variable: Parser = regex VariablePattern >> exceptKeyword |>> Name - /// Accept one or more of variable names. - let variables = sepBy1 variable whitespace + /// 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 () @@ -60,7 +60,7 @@ module Parser = <|> preturn ApplicationOpt.Epsilon /// Accept a lambda abstraction. - let abstraction = between (pchar '\\') (pchar '.') variables .>>. term |>> Abstraction + let abstraction = between (pchar '\\') (pchar '.') variables .>>. (?<)term |>> Abstraction /// Accept a lambda term application or a single operand. let application = operand .>>. applicationOpt |>> Application From 49f9c03750c5753a71b7f4437bfe3a7b4e357315 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Mon, 28 Apr 2025 12:14:49 +0300 Subject: [PATCH 20/50] refactor, skip empty interpreter output --- .../InterpreterTests.fs | 67 +++++-------------- .../LambdaInterpreter.Tests.fsproj | 2 +- .../{ReductionTests.fs => ReducerTests.fs} | 4 +- .../TestFiles/Successful/Test03.txt | 5 ++ .../TestFiles/Successful/Test06.txt | 5 ++ .../TestFiles/Successful/Test08.txt | 0 .../TestFiles/Unsuccessful/Test04.txt | 15 +++++ .../LambdaInterpreter/Interpreter.fs | 58 ++++++++-------- .../LambdaInterpreter.fsproj | 2 +- .../LambdaInterpreter/Program.fs | 14 ++-- .../{Reduction.fs => Reducer.fs} | 33 ++++++--- 11 files changed, 105 insertions(+), 100 deletions(-) rename Tasks/LambdaInterpreter/LambdaInterpreter.Tests/{ReductionTests.fs => ReducerTests.fs} (95%) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test08.txt create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test04.txt rename Tasks/LambdaInterpreter/LambdaInterpreter/{Reduction.fs => Reducer.fs} (63%) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index 080e734..a48b8e3 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -18,73 +18,47 @@ let e = String.Empty let successfulCasesResults: Result list list = [ [ // Test 1 - Ok e; - Ok e; Ok "\\z.z"; ]; [ // Test 2 - Ok e; - Ok e; - Ok e; Ok "ololo"; - Ok e; - Ok e; Ok "a"; - Ok e; Ok "\\V1.\\V2.V2 (\\x.V2 x)"; Ok "\\x.\\y.\\x.x"; - Ok e; ]; [ // Test 3 - Ok e; - Ok e; - Ok e; - Ok e; - Ok e; - Ok e; + 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 e; - Ok e; - Ok "second third" - Ok e; + Ok "second third"; ]; [ // Test 4 Ok "x y"; - Ok e; - Ok e; Ok "x"; - Ok e; Ok "\\y'.y y'"; ]; [ // Test 5 - Ok e; - Ok e; - Ok e; Ok "\\y.ololo"; - Ok e; - Ok e; Ok "snd"; Ok "res"; ]; [ // Test 6 - Ok e; Ok "a"; - Ok e; - Ok e; + Ok "\\a.\\b.b a"; + Ok "baz bar"; ]; [ // Test 7 - Ok e; - Ok e; Ok "var"; - Ok e; Ok "\\x.x"; - Ok e; Ok "exitCode"; Ok "helpMe"; Ok "toClear"; Ok "reset_vars"; Ok "no_exit_1"; - Ok e; + ]; + [ // Test 8 ]; ] @@ -94,14 +68,11 @@ let unsuccessfulCasesResults: Result list list = [ Error e; Error e; Error e; - Ok e; Error e; Error e; Error e; - Ok e; Error e; Error e; - Ok e; Ok "res"; ]; [ // Test 2 @@ -110,31 +81,33 @@ let unsuccessfulCasesResults: Result list list = [ Error e; Error e; Error e; - Ok e; Error e; Error e; Error e; Error e; Error e; - Ok e; ]; [ // Test 3 Error e; Error e; - Ok e; Error e; Error e; Error e; Error e; Error e; Error e; - Ok e; Error e; Error e; Error e; Error e; Error e; - Ok e; + ]; + [ // Test 4 + Ok "\\x.\\y.x"; + Ok "\\x.\\y.x"; + Error "e"; + Ok "bar"; + Ok "foo bar"; ]; ] @@ -150,12 +123,8 @@ let unsuccessfulCases = let testCases = Seq.append successfulCases unsuccessfulCases |> Seq.map TestCaseData -let getOutput (interpreter: Interpreter) = - interpreter.RunToEnd () - |> Seq.map Async.RunSynchronously - |> Seq.toList - 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 @@ -166,6 +135,6 @@ let outputsMatch (actual: Result list) (expected: Result] let testInterpreter (sourceFile: string, expectedOutput: Result list, shouldFail: bool) = let interpreter = Interpreter.StartOnFile sourceFile - let output = getOutput interpreter + let output = interpreter.RunToEnd () |> Seq.toList output |> outputsMatch expectedOutput |> should be True interpreter.SyntaxError |> should equal shouldFail diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj index 6e2c999..b69b05c 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/LambdaInterpreter.Tests.fsproj @@ -7,7 +7,7 @@ - + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReductionTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs similarity index 95% rename from Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReductionTests.fs rename to Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs index e7d6b8e..8ce6e3c 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReductionTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs @@ -5,7 +5,6 @@ open FsUnit open LambdaInterpreter open AST -open Reduction let id var = Abstraction (var, Variable var) let omega var = Abstraction (var, Application (Variable var, Variable var)) @@ -111,4 +110,5 @@ let testCases = List.zip terms reducedTerms |> List.map TestCaseData [] let testReduce term reducedTerm = - reduce term |> should equal reducedTerm + let reducer = new Reducer () + reducer.Reduce term |> should equal reducedTerm diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test03.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test03.txt index 482745b..3f75ba1 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test03.txt +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test03.txt @@ -1,3 +1,8 @@ +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 diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test06.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test06.txt index 05c8ab8..e536b53 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test06.txt +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test06.txt @@ -1,5 +1,10 @@ let I = \x.x I a +let foo = \ a b . b (I a) +foo + +let temp = foo bar baz +temp exit 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/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/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index 08f1328..66b68eb 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -7,13 +7,12 @@ open FParsec open Keywords open AST open Parser -open Reduction /// Class representing the lambda term interpreter. -type Interpreter private (stream: Stream, interactive: bool) = +type Interpreter private (stream: Stream, interactive: bool, ?verbose: bool) = let reader = new StreamReader (stream) - let mutable vars = new Map ([]) - let mutable error = false + let reducer = new Reducer (?verbose=verbose) + let mutable syntaxError = false /// Print help info to the standard output. static member PrintHelp () = printfn $" @@ -42,12 +41,12 @@ Commands: printf "-> " /// Create an interactive interpreter for the standard console input. - static member StartInteractive (): Interpreter = - new Interpreter (Console.OpenStandardInput (), true) + static member StartInteractive (?verbose: bool): Interpreter = + new Interpreter (Console.OpenStandardInput (), true, ?verbose=verbose) - /// Create an interpreter to run on source file at the given `path`. - static member StartOnFile (path: string): Interpreter = - new Interpreter (File.OpenRead path, false) + /// Create an interpreter to run on a source file at the given `path`. + static member StartOnFile (path: string, ?verbose: bool): Interpreter = + new Interpreter (File.OpenRead path, false, ?verbose=verbose) /// Whether the interpreter is being run in console. member _.IsInteractive: bool = interactive @@ -57,49 +56,50 @@ Commands: else stream.CanRead && not reader.EndOfStream /// Whether a syntax error occurred during the interpretation. - member _.SyntaxError: bool = error + member _.SyntaxError: bool = syntaxError + + /// 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 _.RunOnNextLineAsync (): Async> = + member private _.RunOnNextLineAsync (): Async option> = /// Execute the given special interpreter `command`. let runCommand (command: SpecialCommand) = match command with - | Reset -> vars <- new Map ([]) + | Reset -> reducer.Reset () | Help -> if interactive then Interpreter.PrintHelp () | Clear -> if interactive then Console.Clear () | Exit -> reader.Close () - Result.Ok String.Empty + None /// Interpret the given `primary` expression representation. let interpretExpression (primary: Primary.Expression) = match buildAST_Expression primary with | Definition (var, term) -> - vars <- vars.Add (var, substituteMany term vars) - Result.Ok String.Empty - | Result term -> - let result = substituteMany term vars |> reduce |> toString - Result.Ok result + reducer.AddDefinition (var, term) + None + | Result term -> reducer.Reduce term |> toString |> Result.Ok |> Some | Command command -> runCommand command - | Empty -> Result.Ok String.Empty + | Empty -> None - if interactive then Interpreter.PrintInputPointer () async { + if interactive then Interpreter.PrintInputPointer () let! line = reader.ReadLineAsync () |> Async.AwaitTask let parserResult = line |> run expression return match parserResult with | Success (expr, _, _) -> interpretExpression expr | Failure (msg, _, _) -> - error <- true - Result.Error msg - } - - /// Run the interpreter while possible and yield result for each of the lines. - member self.RunToEnd (): Async> seq = - seq { - while self.CanRun do - yield self.RunOnNextLineAsync () + syntaxError <- true + msg |> Result.Error |> Some } interface IDisposable with diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj index 901df02..c478444 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -11,7 +11,7 @@ - + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index a23313f..eaa57de 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -41,10 +41,8 @@ let printMessage (color: ConsoleColor) (message: string) = /// 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 -> - if result.Length > 0 then printMessage success (result + "\n") - | Error message -> - printMessage error message + | Ok result -> printMessage success (result + "\n") + | Error message -> printMessage error message let args = Environment.GetCommandLineArgs () @@ -61,14 +59,12 @@ let interpreter = printMessage ConsoleColor.Red (ex.Message + "\n") exit <| int ExitCode.FileNotFound -async { - use interpreter = interpreter +using interpreter (fun interpreter -> let colorScheme = getColorScheme interpreter if interpreter.IsInteractive then printHeader () - for nextLine in interpreter.RunToEnd () do - let! output = nextLine + for output in interpreter.RunToEnd () do handleOutput colorScheme output getExitCode interpreter |> int |> exit -} |> Async.RunSynchronously +) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reduction.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs similarity index 63% rename from Tasks/LambdaInterpreter/LambdaInterpreter/Reduction.fs rename to Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index e30c678..d8efa01 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reduction.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -2,10 +2,12 @@ open AST -/// Module dealing with lambda term reduction. -module Reduction = +/// Class performing lambda term reduction. +type Reducer (?verbose: bool) = + let verbose = defaultArg verbose false + let mutable variables = new Map ([]) - /// Gets free variables of the given lambda `term`. + /// Get free variables of the given lambda `term`. let rec freeVars term = match term with | Variable (Name v) -> set [v] @@ -13,13 +15,13 @@ module Reduction = | Application (left, right) -> Set.union (freeVars left) (freeVars right) - /// Gets a variable, starting with `prefix`, that is not in `freeVars`. + /// Get 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. + /// Substitute free occurrences of variable `var` in `term` with given term `sub`. + /// Perform alpha-conversion if necessary. let rec substitute term (Name var) sub = match term with | Variable (Name x) when x = var -> sub @@ -36,13 +38,13 @@ module Reduction = | Application (left, right) -> Application (substitute left (Name var) sub, substitute right (Name var) sub) - /// Substitutes variables in `term` according to the `subs` mapping. + /// Substitute variables in `term` according to the `subs` mapping. let substituteMany term (subs: Map) = subs |> Seq.fold (fun acc pair -> substitute acc pair.Key pair.Value) term - /// Performs beta-reduction of the given lambda `term`. - /// Performs alpha-conversion if necessary. + /// Perform beta-reduction of the given lambda `term`. + /// Perform alpha-conversion if necessary. let rec reduce term = match term with | Variable _ as var -> var @@ -57,3 +59,16 @@ module Reduction = match left with | Abstraction _ -> reduce (Application (left, right)) | _ -> Application (left, right) + + /// Define a `var` to be substituted with the given `term`. + member _.AddDefinition (var: Variable, term: LambdaTerm) = + variables <- variables.Add (var, substituteMany term variables) + + /// Reset defined variables. + member _.Reset () = + variables <- new Map ([]) + + /// Perform beta-reduction of the given lambda `term` according to defined variables. + /// Perform alpha-conversion if necessary. + member _.Reduce (term: LambdaTerm): LambdaTerm = + variables |> substituteMany term |> reduce From a741d1a616c555f006fe40ba7ba6d7cf7679b4c6 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Mon, 28 Apr 2025 14:40:23 +0300 Subject: [PATCH 21/50] add Reducer logging --- .../InterpreterTests.fs | 2 +- .../LambdaInterpreter/Interpreter.fs | 10 +++-- .../LambdaInterpreter/Program.fs | 4 +- .../LambdaInterpreter/Reducer.fs | 39 ++++++++++++++++++- .../LambdaInterpreter/Syntax/AST.fs | 33 +++++++++------- 5 files changed, 65 insertions(+), 23 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index a48b8e3..27e7333 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -105,7 +105,7 @@ let unsuccessfulCasesResults: Result list list = [ [ // Test 4 Ok "\\x.\\y.x"; Ok "\\x.\\y.x"; - Error "e"; + Error e; Ok "bar"; Ok "foo bar"; ]; diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index 66b68eb..cd2287b 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -24,9 +24,9 @@ Syntax: definition\t\t {DeclarationKeyword} {{variable}} = {{term}} Examples: - -> {DeclarationKeyword} S = \\x y z.x z (y z) - -> {DeclarationKeyword} K = \\x y.x - -> S K K + >>> {DeclarationKeyword} S = \\x y z.x z (y z) + >>> {DeclarationKeyword} K = \\x y.x + >>> S K K \\z.z Commands: @@ -38,13 +38,15 @@ Commands: /// Print a pointer indicating the start of input when running the interactive interpreter. static member PrintInputPointer () = - printf "-> " + printf ">>> " /// Create an interactive interpreter for the standard console input. + /// Use `verbose` option for more detailed console output. 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 for more detailed console output. static member StartOnFile (path: string, ?verbose: bool): Interpreter = new Interpreter (File.OpenRead path, false, ?verbose=verbose) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index eaa57de..f33bdcf 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -52,8 +52,8 @@ if Array.contains "-h" args || Array.contains "--help" args then let interpreter = try - if args.Length = 2 then Interpreter.StartOnFile (args[1]) - else Interpreter.StartInteractive () + if args.Length = 2 then Interpreter.StartOnFile (args[1], true) + else Interpreter.StartInteractive true with | :? FileNotFoundException | :? DirectoryNotFoundException as ex -> printMessage ConsoleColor.Red (ex.Message + "\n") diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index d8efa01..ecbcce0 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -2,11 +2,38 @@ open AST +/// Log record of reducer execution. +type LogRecord = + | AlphaConversion of Variable * Variable + | BetaReduction of LambdaTerm * LambdaTerm * Variable * LambdaTerm + | Substitution of Variable * LambdaTerm + | StartedReducing of LambdaTerm + | Reducing of LambdaTerm + | AddingDefinition of Variable * LambdaTerm + | Resetting + /// Class performing lambda term reduction. +/// Use `verbose` option to print logs to the console. type Reducer (?verbose: bool) = let verbose = defaultArg verbose false let mutable variables = new Map ([]) + /// Print a log message from the given `record` according to verbosity. + let log record = + if verbose then + match record with + | AlphaConversion (Name x, Name y) -> + $" [alpha-conversion]: {x} -> {y}" + | BetaReduction (source, term, Name var, sub) -> + $" [beta-reduction]: {toString source} -> {toStringWithBrackets term}[{var} := {toString sub}]" + | Substitution (Name var, sub) -> + $" [substitution]: {var} -> {toString sub}" + | StartedReducing term -> toString term + | Reducing term -> $" reducing {toString term} ..." + | AddingDefinition (Name var, term) -> $"adding definition: {var} = {toString term} ..." + | Resetting -> "resetting defined variables ..." + |> printfn "%s" + /// Get free variables of the given lambda `term`. let rec freeVars term = match term with @@ -24,7 +51,9 @@ type Reducer (?verbose: bool) = /// Perform alpha-conversion if necessary. let rec substitute term (Name var) sub = match term with - | Variable (Name x) when x = var -> sub + | Variable (Name x) when x = var -> + log <| Substitution (Name var, sub) + sub | Variable _ as var -> var | Abstraction (Name x, _) as abs when x = var -> abs | Abstraction (Name x, term) -> @@ -34,6 +63,7 @@ type Reducer (?verbose: bool) = Abstraction (Name x, substitute term (Name var) sub) else let y = nextFreeVar x (Set.union freeVarsS freeVarsT) |> Name + log <| AlphaConversion (Name x, y) Abstraction (y, substitute (substitute term (Name x) (Variable y)) (Name var) sub) | Application (left, right) -> Application (substitute left (Name var) sub, substitute right (Name var) sub) @@ -46,10 +76,12 @@ type Reducer (?verbose: bool) = /// Perform beta-reduction of the given lambda `term`. /// Perform alpha-conversion if necessary. let rec reduce term = + log <| Reducing term match term with | Variable _ as var -> var | Abstraction (x, term) -> Abstraction (x, reduce term) | Application (Abstraction (var, term) as abs, sub) as source -> + log <| BetaReduction (source, term, var, sub) let term = substitute term var sub if term <> source then reduce term else Application (reduce abs, reduce sub) @@ -62,13 +94,18 @@ type Reducer (?verbose: bool) = /// Define a `var` to be substituted with the given `term`. member _.AddDefinition (var: Variable, term: LambdaTerm) = + log <| AddingDefinition (var, term) variables <- variables.Add (var, substituteMany term variables) + if verbose then printf "\n" /// Reset defined variables. member _.Reset () = + log <| Resetting variables <- new Map ([]) + if verbose then printf "\n" /// Perform beta-reduction of the given lambda `term` according to defined variables. /// Perform alpha-conversion if necessary. member _.Reduce (term: LambdaTerm): LambdaTerm = + log <| StartedReducing term variables |> substituteMany term |> reduce diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index 2de0288..ccd1b8b 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -56,20 +56,23 @@ module AST = | Epsilon -> Empty /// Get a string representation of the given lambda `term`. - let toString (term: LambdaTerm) = - - /// Get a string representation of the given lambda `term`. - /// Add brackets if necessary for a proper operation priority. - let rec toStringInternal (term: LambdaTerm) (withBrackets: bool) = - match term with - | Variable (Name var) -> var - | Application (left, right) -> - let left = $"{toStringInternal left left.IsAbstraction}" - let right = $"{toStringInternal right (right.IsAbstraction || right.IsApplication)}" - let term = $"{left} {right}" - if withBrackets then $"({term})" else term - | Abstraction (Name var, term) -> - let term = $"\\{var}.{toStringInternal term false}" - if withBrackets then $"({term})" else term + /// Add brackets if necessary for a proper operation priority. + let rec private toStringInternal (term: LambdaTerm) (withBrackets: bool) = + match term with + | Variable (Name var) -> var + | Application (left, right) -> + let left = $"{toStringInternal left left.IsAbstraction}" + let right = $"{toStringInternal right (right.IsAbstraction || right.IsApplication)}" + let term = $"{left} {right}" + if withBrackets then $"({term})" else term + | Abstraction (Name var, term) -> + let term = $"\\{var}.{toStringInternal term false}" + if withBrackets then $"({term})" else term + /// Get a string representation of the given lambda `term`. + let toString (term: LambdaTerm) = toStringInternal term false + + /// Get a string representation of the given lambda `term` and surround it with brackets if necessary. + let toStringWithBrackets (term: LambdaTerm) = + toStringInternal term true From d05288256826d3052d53ceac0f3954b699103fed Mon Sep 17 00:00:00 2001 From: bygu4 Date: Mon, 28 Apr 2025 19:26:06 +0300 Subject: [PATCH 22/50] add Options struct, add --verbose option --- .../LambdaInterpreter/Console/ExitCode.fs | 7 +++- .../LambdaInterpreter/Console/Options.fs | 40 +++++++++++++++++++ .../LambdaInterpreter/Interpreter.fs | 4 +- .../LambdaInterpreter.fsproj | 1 + .../LambdaInterpreter/Program.fs | 34 +++++++++------- .../LambdaInterpreter/Syntax/Parser.fs | 2 +- 6 files changed, 69 insertions(+), 19 deletions(-) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter/Console/Options.fs diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs index 59c4cf6..197f2ad 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs @@ -8,12 +8,15 @@ module ExitCode = /// The program execution was successful. | Success = 0 - /// An syntax error has occurred during source file interpretation. - | SyntaxError = 1 + /// The given command line arguments are invalid. + | BadArguments = 1 /// The given source file was not found. | FileNotFound = 2 + /// An syntax error has occurred during source file interpretation. + | SyntaxError = 3 + /// Get the exit code of the program according to the state of the given `interpreter`. let getExitCode (interpreter: Interpreter) = if interpreter.IsInteractive || not interpreter.SyntaxError then ExitCode.Success diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Options.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Options.fs new file mode 100644 index 0000000..e6deeec --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Options.fs @@ -0,0 +1,40 @@ +namespace LambdaInterpreter + +open System + +/// Struct for managing command line options. +type Options private (sourceFile: string option, help: bool, verbose: 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"|] + + /// 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 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 sourceFile = if args.Count = 1 then Some (Set.minElement args) else None + let error = args.Count > 1 + new Options (sourceFile, help, verbose, error) + end diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index cd2287b..14898ce 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -41,12 +41,12 @@ Commands: printf ">>> " /// Create an interactive interpreter for the standard console input. - /// Use `verbose` option for more detailed console output. + /// 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 for more detailed console output. + /// Use `verbose` option to print logs to the console. static member StartOnFile (path: string, ?verbose: bool): Interpreter = new Interpreter (File.OpenRead path, false, ?verbose=verbose) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj index c478444..21357b5 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -13,6 +13,7 @@ + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index f33bdcf..d2eeec1 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -17,20 +17,22 @@ Type 'help' for more info. /// Print command line help. let printHelp () = - printfn " + printfn $" Lambda Interpreter ------------------ A simple interpreter of lambda term expressions. It can either be run interactively using the standard input, or on a specified source file. -Usage: - LambdaInterpreter [options]\t\t Run interpreter interactively - LambdaInterpreter {path-to-file}\t Run interpreter on the given source file +Usage: LambdaInterpreter {{path-to-file?}} [options] Options: - -h|--help\t\t Display help and exit -" Interpreter.PrintHelp () + {String.Join ('|', Options.HelpArgs)}\t\t Display help and exit + {String.Join ('|', Options.VerboseArgs)}\t Use detailed output" + Interpreter.PrintHelp () + +/// Message to print when failed to interpret the given command line args. +let invalidArgsMessage = "Invalid command line arguments provided. For more info use '--help' option." /// Print the given `message` to the standard output with the given `color`. let printMessage (color: ConsoleColor) (message: string) = @@ -44,20 +46,24 @@ let handleOutput (Color success, Color error) (output: Result) = | Ok result -> printMessage success (result + "\n") | Error message -> printMessage error message -let args = Environment.GetCommandLineArgs () +let options = Options.GetFromArgs () -if Array.contains "-h" args || Array.contains "--help" args then +if options.Help then printHelp () exit <| int ExitCode.Success +if options.Error then + printMessage ConsoleColor.Red invalidArgsMessage + exit <| int ExitCode.BadArguments + let interpreter = - try - if args.Length = 2 then Interpreter.StartOnFile (args[1], true) - else Interpreter.StartInteractive true - with - | :? FileNotFoundException | :? DirectoryNotFoundException as ex -> - printMessage ConsoleColor.Red (ex.Message + "\n") + match options.SourceFile with + | Some path -> + try Interpreter.StartOnFile (path, options.Verbose) + with :? FileNotFoundException | :? DirectoryNotFoundException as ex -> + printMessage ConsoleColor.Red ex.Message exit <| int ExitCode.FileNotFound + | None -> Interpreter.StartInteractive options.Verbose using interpreter (fun interpreter -> let colorScheme = getColorScheme interpreter diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs index a5c22bc..40353f7 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs @@ -34,7 +34,7 @@ module Parser = if reply.Status = ReplyStatus.Ok && isKeyword reply.Result then Reply ( ReplyStatus.Error, - ErrorMessage.Unexpected $"\"{reply.Result}\" is reserved as a keyword" |> ErrorMessageList + ErrorMessage.Unexpected $"'{reply.Result}' is reserved as a keyword" |> ErrorMessageList ) else reply From 60d4bf2244e3091deb1f381f5e2a20a9ebcf2add Mon Sep 17 00:00:00 2001 From: bygu4 Date: Mon, 28 Apr 2025 19:43:03 +0300 Subject: [PATCH 23/50] correct output formatting --- Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs | 2 +- Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs | 2 -- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index d2eeec1..4ab7b59 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -43,7 +43,7 @@ let printMessage (color: ConsoleColor) (message: string) = /// 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 + "\n") + | Ok result -> printMessage success result | Error message -> printMessage error message let options = Options.GetFromArgs () diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index ecbcce0..b92d227 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -96,13 +96,11 @@ type Reducer (?verbose: bool) = member _.AddDefinition (var: Variable, term: LambdaTerm) = log <| AddingDefinition (var, term) variables <- variables.Add (var, substituteMany term variables) - if verbose then printf "\n" /// Reset defined variables. member _.Reset () = log <| Resetting variables <- new Map ([]) - if verbose then printf "\n" /// Perform beta-reduction of the given lambda `term` according to defined variables. /// Perform alpha-conversion if necessary. From 4f82792e7388f3f5ebe7be0cfd8fde809b1c100c Mon Sep 17 00:00:00 2001 From: bygu4 Date: Mon, 28 Apr 2025 20:07:10 +0300 Subject: [PATCH 24/50] use list instead of map to store definitions --- .../LambdaInterpreter.Tests/InterpreterTests.fs | 1 + .../TestFiles/Successful/Test01.txt | 7 ++++++- Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs | 10 +++++----- 3 files changed, 12 insertions(+), 6 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index 27e7333..2a42e99 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -19,6 +19,7 @@ let e = String.Empty let successfulCasesResults: Result list list = [ [ // Test 1 Ok "\\z.z"; + Ok "trololo"; ]; [ // Test 2 Ok "ololo"; diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test01.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test01.txt index 788a0a5..37954c8 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test01.txt +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test01.txt @@ -1,3 +1,8 @@ let S = \x y z.x z (y z) let K = \x y.x -S K K \ No newline at end of file +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/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index b92d227..91bc6b5 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -16,7 +16,7 @@ type LogRecord = /// Use `verbose` option to print logs to the console. type Reducer (?verbose: bool) = let verbose = defaultArg verbose false - let mutable variables = new Map ([]) + let mutable variables: (Variable * LambdaTerm) list = [] /// Print a log message from the given `record` according to verbosity. let log record = @@ -69,9 +69,9 @@ type Reducer (?verbose: bool) = Application (substitute left (Name var) sub, substitute right (Name var) sub) /// Substitute variables in `term` according to the `subs` mapping. - let substituteMany term (subs: Map) = + let substituteMany term subs = subs - |> Seq.fold (fun acc pair -> substitute acc pair.Key pair.Value) term + |> Seq.fold (fun acc (var, sub) -> substitute acc var sub) term /// Perform beta-reduction of the given lambda `term`. /// Perform alpha-conversion if necessary. @@ -95,12 +95,12 @@ type Reducer (?verbose: bool) = /// Define a `var` to be substituted with the given `term`. member _.AddDefinition (var: Variable, term: LambdaTerm) = log <| AddingDefinition (var, term) - variables <- variables.Add (var, substituteMany term variables) + variables <- (var, term) :: variables /// Reset defined variables. member _.Reset () = log <| Resetting - variables <- new Map ([]) + variables <- [] /// Perform beta-reduction of the given lambda `term` according to defined variables. /// Perform alpha-conversion if necessary. From a736f1d3b5bf821ca0ca15c9cdd86c569f92fa48 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Mon, 28 Apr 2025 22:40:09 +0300 Subject: [PATCH 25/50] add --line-number option --- .../LambdaInterpreter/Console/Options.fs | 15 ++++++-- .../LambdaInterpreter/Interpreter.fs | 34 +++++++++++++------ .../LambdaInterpreter/Program.fs | 5 +-- .../LambdaInterpreter/Reducer.fs | 2 +- 4 files changed, 41 insertions(+), 15 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Options.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Options.fs index e6deeec..b5e7125 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Options.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Options.fs @@ -3,7 +3,11 @@ namespace LambdaInterpreter open System /// Struct for managing command line options. -type Options private (sourceFile: string option, help: bool, verbose: bool, error: bool) = +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"|] @@ -11,6 +15,9 @@ type Options private (sourceFile: string option, help: bool, verbose: bool, erro /// 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 @@ -20,6 +27,9 @@ type Options private (sourceFile: string option, help: bool, verbose: bool, erro /// 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 @@ -34,7 +44,8 @@ type Options private (sourceFile: string option, help: bool, verbose: bool, erro 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, error) + new Options (sourceFile, help, verbose, lineNumber, error) end diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index 14898ce..a615da8 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -9,11 +9,22 @@ open AST open Parser /// Class representing the lambda term interpreter. -type Interpreter private (stream: Stream, interactive: bool, ?verbose: bool) = +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 + /// Print a pointer indicating the start of input when running an interactive interpreter. + let tryPrintInputPointer () = + if interactive then printf ">>> " + + /// 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 + /// Print help info to the standard output. static member PrintHelp () = printfn $" Syntax: @@ -36,10 +47,6 @@ Commands: {ExitKeyword}\t\t Stop the execution and exit " - /// Print a pointer indicating the start of input when running the interactive interpreter. - static member PrintInputPointer () = - printf ">>> " - /// Create an interactive interpreter for the standard console input. /// Use `verbose` option to print logs to the console. static member StartInteractive (?verbose: bool): Interpreter = @@ -47,8 +54,9 @@ Commands: /// Create an interpreter to run on a source file at the given `path`. /// Use `verbose` option to print logs to the console. - static member StartOnFile (path: string, ?verbose: bool): Interpreter = - new Interpreter (File.OpenRead path, false, ?verbose=verbose) + /// 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 @@ -88,12 +96,18 @@ Commands: | Definition (var, term) -> reducer.AddDefinition (var, term) None - | Result term -> reducer.Reduce term |> toString |> Result.Ok |> Some + | Result term -> + reducer.Reduce term + |> toString + |> tryAddCurrentLine + |> Result.Ok + |> Some | Command command -> runCommand command | Empty -> None async { - if interactive then Interpreter.PrintInputPointer () + currentLine <- currentLine + 1 + tryPrintInputPointer () let! line = reader.ReadLineAsync () |> Async.AwaitTask let parserResult = line |> run expression return @@ -101,7 +115,7 @@ Commands: | Success (expr, _, _) -> interpretExpression expr | Failure (msg, _, _) -> syntaxError <- true - msg |> Result.Error |> Some + msg |> tryAddCurrentLine |> Result.Error |> Some } interface IDisposable with diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index 4ab7b59..2195cab 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -28,7 +28,8 @@ Usage: LambdaInterpreter {{path-to-file?}} [options] Options: {String.Join ('|', Options.HelpArgs)}\t\t Display help and exit - {String.Join ('|', Options.VerboseArgs)}\t Use detailed output" + {String.Join ('|', Options.VerboseArgs)}\t Use detailed output + {String.Join ('|', Options.LineNumberArgs)}\t Print line number with output" Interpreter.PrintHelp () /// Message to print when failed to interpret the given command line args. @@ -59,7 +60,7 @@ if options.Error then let interpreter = match options.SourceFile with | Some path -> - try Interpreter.StartOnFile (path, options.Verbose) + try Interpreter.StartOnFile (path, options.Verbose, options.LineNumber) with :? FileNotFoundException | :? DirectoryNotFoundException as ex -> printMessage ConsoleColor.Red ex.Message exit <| int ExitCode.FileNotFound diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index 91bc6b5..bdcab68 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -68,7 +68,7 @@ type Reducer (?verbose: bool) = | Application (left, right) -> Application (substitute left (Name var) sub, substitute right (Name var) sub) - /// Substitute variables in `term` according to the `subs` mapping. + /// Substitute variables in `term` according to the given `subs` pair sequence. let substituteMany term subs = subs |> Seq.fold (fun acc (var, sub) -> substitute acc var sub) term From c9d66e97f460830b7f1a0052d6e5425f3307605a Mon Sep 17 00:00:00 2001 From: bygu4 Date: Mon, 28 Apr 2025 23:22:57 +0300 Subject: [PATCH 26/50] update main --- Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index 2195cab..6f56aff 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -10,7 +10,7 @@ let printHeader () = printfn " Lambda Interpreter ------------------ -A simple interpreter of lambda term expressions. +An interactive lambda term interpreter. Type 'help' for more info. " @@ -20,11 +20,11 @@ let printHelp () = printfn $" Lambda Interpreter ------------------ -A simple interpreter of lambda term expressions. +An interactive lambda term interpreter. It can either be run interactively using the standard input, or on a specified source file. -Usage: LambdaInterpreter {{path-to-file?}} [options] +Usage: LambdaInterpreter [path-to-file] [options] Options: {String.Join ('|', Options.HelpArgs)}\t\t Display help and exit From f58a61f92933c42c121778ee634c28f0a135e2a9 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Tue, 29 Apr 2025 01:17:49 +0300 Subject: [PATCH 27/50] update comments and exception handling --- .../LambdaInterpreter/Console/ColorScheme.fs | 2 +- .../LambdaInterpreter/Console/ExitCode.fs | 2 +- Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs | 12 +++++++----- .../LambdaInterpreter/Syntax/AST.fs | 2 +- 4 files changed, 10 insertions(+), 8 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs index 590e99e..a50c9e2 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs @@ -11,7 +11,7 @@ module ColorScheme = /// Color of messages signaling of error. type ErrorColor = Color of ConsoleColor - /// Definition of the color scheme of the console application. + /// Color scheme of the console application. type ColorScheme = SuccessColor * ErrorColor /// Get the color scheme of the app according to the state of the given `interpreter`. diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs index 197f2ad..6ec5538 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs @@ -14,7 +14,7 @@ module ExitCode = /// The given source file was not found. | FileNotFound = 2 - /// An syntax error has occurred during source file interpretation. + /// A syntax error has occurred during source file interpretation. | SyntaxError = 3 /// Get the exit code of the program according to the state of the given `interpreter`. diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index 6f56aff..4e616ef 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -2,17 +2,18 @@ open System open System.IO open LambdaInterpreter +open Keywords open ColorScheme open ExitCode /// Print header with general info about the app and a help suggestion. let printHeader () = - printfn " + printfn $" Lambda Interpreter ------------------ An interactive lambda term interpreter. -Type 'help' for more info. +Type '{HelpKeyword}' for more info. " /// Print command line help. @@ -28,12 +29,13 @@ Usage: LambdaInterpreter [path-to-file] [options] Options: {String.Join ('|', Options.HelpArgs)}\t\t Display help and exit - {String.Join ('|', Options.VerboseArgs)}\t Use detailed output + {String.Join ('|', Options.VerboseArgs)}\t Print detailed interpretation info {String.Join ('|', Options.LineNumberArgs)}\t Print line number with output" Interpreter.PrintHelp () /// Message to print when failed to interpret the given command line args. -let invalidArgsMessage = "Invalid command line arguments provided. For more info use '--help' option." +let invalidArgsMessage = + $"Invalid command line arguments provided. For more info use '{Array.last Options.HelpArgs}' option." /// Print the given `message` to the standard output with the given `color`. let printMessage (color: ConsoleColor) (message: string) = @@ -61,7 +63,7 @@ let interpreter = match options.SourceFile with | Some path -> try Interpreter.StartOnFile (path, options.Verbose, options.LineNumber) - with :? FileNotFoundException | :? DirectoryNotFoundException as ex -> + with :? IOException | :? UnauthorizedAccessException as ex -> printMessage ConsoleColor.Red ex.Message exit <| int ExitCode.FileNotFound | None -> Interpreter.StartInteractive options.Verbose diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index ccd1b8b..842ad0c 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -3,7 +3,7 @@ namespace LambdaInterpreter open System open Primary -/// Module dealing with finalized syntax trees. +/// Module dealing with finalized syntax trees of lambda expressions. module AST = /// Definition of the lambda term. From 2614394da1fdc8e25b07695f4891892946c6f8a5 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Tue, 29 Apr 2025 12:50:05 +0300 Subject: [PATCH 28/50] handle stack overflow during reduction, update logging --- .../InterpreterTests.fs | 6 +- .../TestFiles/Unsuccessful/Test05.txt | 6 ++ .../LambdaInterpreter/Console/ExitCode.fs | 11 +++- .../LambdaInterpreter/Interpreter.fs | 17 +++-- .../LambdaInterpreter/Reducer.fs | 66 ++++++++++++------- 5 files changed, 72 insertions(+), 34 deletions(-) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test05.txt diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index 2a42e99..7f68a39 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -110,6 +110,10 @@ let unsuccessfulCasesResults: Result list list = [ Ok "bar"; Ok "foo bar"; ]; + [ // Test 5 + Error e; + Ok "(\\x.x x) (\\x.x x)"; + ]; ] let successfulCases = @@ -138,4 +142,4 @@ let testInterpreter (sourceFile: string, expectedOutput: Result let interpreter = Interpreter.StartOnFile sourceFile let output = interpreter.RunToEnd () |> Seq.toList output |> outputsMatch expectedOutput |> should be True - interpreter.SyntaxError |> should equal shouldFail + (interpreter.SyntaxError || interpreter.StackOverflow) |> should equal shouldFail 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..4ea6b16 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test05.txt @@ -0,0 +1,6 @@ +let e = \x.x x x +\Z.e e + +let o = \x.x x +let O = o o +O diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs index 6ec5538..858f272 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs @@ -14,10 +14,15 @@ module ExitCode = /// The given source file was not found. | FileNotFound = 2 - /// A syntax error has occurred during source file interpretation. + /// A syntax error occurred during source file interpretation. | SyntaxError = 3 + /// A stack overflow occurred during the source file term reduction. + | StackOverflow = 4 + /// Get the exit code of the program according to the state of the given `interpreter`. let getExitCode (interpreter: Interpreter) = - if interpreter.IsInteractive || not interpreter.SyntaxError then ExitCode.Success - else ExitCode.SyntaxError + if interpreter.IsInteractive then ExitCode.Success else + if interpreter.SyntaxError then ExitCode.SyntaxError else + if interpreter.StackOverflow then ExitCode.StackOverflow else + ExitCode.Success diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index a615da8..66e195c 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -16,6 +16,7 @@ type Interpreter private (stream: Stream, interactive: bool, ?verbose: bool, ?li let mutable currentLine = 0 let mutable syntaxError = false + let mutable stackOverflow = false /// Print a pointer indicating the start of input when running an interactive interpreter. let tryPrintInputPointer () = @@ -68,6 +69,9 @@ Commands: /// Whether a syntax error occurred during the interpretation. member _.SyntaxError: bool = syntaxError + /// Whether a stack overflow occurred during the term reduction. + member _.StackOverflow: bool = stackOverflow + /// Run the interpreter while possible and yield the interpretation results. member self.RunToEnd (): Result seq = seq { @@ -97,11 +101,14 @@ Commands: reducer.AddDefinition (var, term) None | Result term -> - reducer.Reduce term - |> toString - |> tryAddCurrentLine - |> Result.Ok - |> Some + try reducer.Reduce term + |> toString + |> tryAddCurrentLine + |> Result.Ok + |> Some + with :? StackOverflowException as ex -> + stackOverflow <- true + ex.Message |> tryAddCurrentLine |> Result.Error |> Some | Command command -> runCommand command | Empty -> None diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index bdcab68..e4bf8b9 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -1,14 +1,15 @@ namespace LambdaInterpreter +open System open AST /// Log record of reducer execution. type LogRecord = + | StartedReducing of LambdaTerm + | Reducing of LambdaTerm | AlphaConversion of Variable * Variable | BetaReduction of LambdaTerm * LambdaTerm * Variable * LambdaTerm | Substitution of Variable * LambdaTerm - | StartedReducing of LambdaTerm - | Reducing of LambdaTerm | AddingDefinition of Variable * LambdaTerm | Resetting @@ -18,20 +19,32 @@ type Reducer (?verbose: bool) = let verbose = defaultArg verbose false let mutable variables: (Variable * LambdaTerm) list = [] + /// Max allowed depth of the recursion. + [] + let MaxRecursionDepth = 32000 + + /// Message to fail with in case of stack overflow. + [] + let StackOverflowMessage = "Error: max recursion depth exceeded during the reduction." + /// Print a log message from the given `record` according to verbosity. let log record = if verbose then match record with + | StartedReducing term -> + toString term + | Reducing term -> + $"| reducing {toString term} ..." | AlphaConversion (Name x, Name y) -> - $" [alpha-conversion]: {x} -> {y}" + $"| [alpha-conversion]: {x} -> {y}" | BetaReduction (source, term, Name var, sub) -> - $" [beta-reduction]: {toString source} -> {toStringWithBrackets term}[{var} := {toString sub}]" + $"| [beta-reduction]: {toString source} -> {toStringWithBrackets term}[{var} := {toString sub}]" | Substitution (Name var, sub) -> - $" [substitution]: {var} -> {toString sub}" - | StartedReducing term -> toString term - | Reducing term -> $" reducing {toString term} ..." - | AddingDefinition (Name var, term) -> $"adding definition: {var} = {toString term} ..." - | Resetting -> "resetting defined variables ..." + $"| [substitution]: {var} -> {toString sub}" + | AddingDefinition (Name var, term) -> + $"adding definition: {var} = {toString term} ..." + | Resetting -> + "resetting defined variables ..." |> printfn "%s" /// Get free variables of the given lambda `term`. @@ -75,22 +88,25 @@ type Reducer (?verbose: bool) = /// Perform beta-reduction of the given lambda `term`. /// Perform alpha-conversion if necessary. - let rec reduce term = - log <| Reducing term - match term with - | Variable _ as var -> var - | Abstraction (x, term) -> Abstraction (x, reduce term) - | Application (Abstraction (var, term) as abs, sub) as source -> - log <| BetaReduction (source, term, var, sub) - 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) + let reduce term = + let rec reduce term depth = + if depth > MaxRecursionDepth then raise <| StackOverflowException StackOverflowMessage + log <| Reducing term + match term with + | Variable _ as var -> var + | Abstraction (x, term) -> Abstraction (x, reduce term (depth + 1)) + | Application (Abstraction (var, term) as abs, sub) as source -> + log <| BetaReduction (source, term, var, sub) + let term = substitute term var sub + if term <> source then reduce term (depth + 1) + else Application (reduce abs (depth + 1), reduce sub (depth + 1)) + | Application (left, right) -> + let left = reduce left (depth + 1) + let right = reduce right (depth + 1) + match left with + | Abstraction _ -> reduce (Application (left, right)) (depth + 1) + | _ -> Application (left, right) + in reduce term 0 /// Define a `var` to be substituted with the given `term`. member _.AddDefinition (var: Variable, term: LambdaTerm) = From d4bfc42da52baa11c7445f5795e0aec78ac19b65 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Tue, 29 Apr 2025 13:24:51 +0300 Subject: [PATCH 29/50] adjust recursion limit --- Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index e4bf8b9..02e527e 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -19,9 +19,9 @@ type Reducer (?verbose: bool) = let verbose = defaultArg verbose false let mutable variables: (Variable * LambdaTerm) list = [] - /// Max allowed depth of the recursion. + /// Max allowed depth of recursion during the term reduction. [] - let MaxRecursionDepth = 32000 + let MaxRecursionDepth = 8192 /// Message to fail with in case of stack overflow. [] From e2c46e40c543f2a0654ebca44cee5cdf0343d8f3 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Tue, 29 Apr 2025 13:36:18 +0300 Subject: [PATCH 30/50] adjust recursion limit --- Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index 02e527e..7aade57 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -21,7 +21,7 @@ type Reducer (?verbose: bool) = /// Max allowed depth of recursion during the term reduction. [] - let MaxRecursionDepth = 8192 + let MaxRecursionDepth = 4096 /// Message to fail with in case of stack overflow. [] From 87a10a7741d966df7b9bfdd7eccced867f9295ff Mon Sep 17 00:00:00 2001 From: bygu4 Date: Tue, 29 Apr 2025 14:55:07 +0300 Subject: [PATCH 31/50] improve logging, change success output color --- .../LambdaInterpreter/Console/ColorScheme.fs | 2 +- .../LambdaInterpreter/Reducer.fs | 30 +++++++++++-------- 2 files changed, 19 insertions(+), 13 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs index a50c9e2..305216e 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs @@ -17,4 +17,4 @@ module ColorScheme = /// 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.White, Color ConsoleColor.Red + else Color ConsoleColor.Green, Color ConsoleColor.Red diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index 7aade57..a0763f8 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -6,12 +6,14 @@ 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 - | AddingDefinition of Variable * LambdaTerm - | Resetting + | UnableToReduce of LambdaTerm + | NewDefinition of Variable * LambdaTerm + | DefinitionsReset /// Class performing lambda term reduction. /// Use `verbose` option to print logs to the console. @@ -31,8 +33,8 @@ type Reducer (?verbose: bool) = let log record = if verbose then match record with - | StartedReducing term -> - toString term + | StartedReducing term -> $"{toString term}\n|" + | DoneReducing -> "V" | Reducing term -> $"| reducing {toString term} ..." | AlphaConversion (Name x, Name y) -> @@ -41,10 +43,10 @@ type Reducer (?verbose: bool) = $"| [beta-reduction]: {toString source} -> {toStringWithBrackets term}[{var} := {toString sub}]" | Substitution (Name var, sub) -> $"| [substitution]: {var} -> {toString sub}" - | AddingDefinition (Name var, term) -> - $"adding definition: {var} = {toString term} ..." - | Resetting -> - "resetting defined variables ..." + | 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" |> printfn "%s" /// Get free variables of the given lambda `term`. @@ -99,7 +101,9 @@ type Reducer (?verbose: bool) = log <| BetaReduction (source, term, var, sub) let term = substitute term var sub if term <> source then reduce term (depth + 1) - else Application (reduce abs (depth + 1), reduce sub (depth + 1)) + else + log <| UnableToReduce term + Application (reduce abs (depth + 1), reduce sub (depth + 1)) | Application (left, right) -> let left = reduce left (depth + 1) let right = reduce right (depth + 1) @@ -110,16 +114,18 @@ type Reducer (?verbose: bool) = /// Define a `var` to be substituted with the given `term`. member _.AddDefinition (var: Variable, term: LambdaTerm) = - log <| AddingDefinition (var, term) variables <- (var, term) :: variables + log <| NewDefinition (var, term) /// Reset defined variables. member _.Reset () = - log <| Resetting variables <- [] + log <| DefinitionsReset /// Perform beta-reduction of the given lambda `term` according to defined variables. /// Perform alpha-conversion if necessary. member _.Reduce (term: LambdaTerm): LambdaTerm = log <| StartedReducing term - variables |> substituteMany term |> reduce + let result = variables |> substituteMany term |> reduce + log <| DoneReducing + result From 49206ab7a71ec25006fc30fb0fc8ac65560edcc2 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Tue, 29 Apr 2025 16:41:44 +0300 Subject: [PATCH 32/50] add Help modules for managing console printing, refactor --- .../LambdaInterpreter.Tests/ParserTests.fs | 2 +- .../LambdaInterpreter.Tests/ReducerTests.fs | 1 + .../LambdaInterpreter/Console/ColorScheme.fs | 3 +- .../LambdaInterpreter/Console/ExitCode.fs | 6 ++- .../LambdaInterpreter/Console/Help.fs | 42 +++++++++++++++++ .../LambdaInterpreter/Console/Options.fs | 2 +- .../LambdaInterpreter/Interpreter.fs | 26 +---------- .../LambdaInterpreter.fsproj | 2 + .../LambdaInterpreter/Program.fs | 46 ++++++------------- .../LambdaInterpreter/Reducer.fs | 2 + .../LambdaInterpreter/Syntax/AST.fs | 2 +- .../LambdaInterpreter/Syntax/Help.fs | 28 +++++++++++ .../LambdaInterpreter/Syntax/Keywords.fs | 2 +- .../LambdaInterpreter/Syntax/Parser.fs | 2 +- .../LambdaInterpreter/Syntax/Primary.fs | 2 +- 15 files changed, 103 insertions(+), 65 deletions(-) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter/Console/Help.fs create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs index 2a66dee..99c4a60 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs @@ -4,7 +4,7 @@ open NUnit.Framework open FsUnit open FParsec -open LambdaInterpreter +open LambdaInterpreter.Syntax open Parser let runTest (testCases: (string * Parser<'a, unit> * int option) seq) = diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs index 8ce6e3c..879860d 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs @@ -4,6 +4,7 @@ open NUnit.Framework open FsUnit open LambdaInterpreter +open LambdaInterpreter.Syntax open AST let id var = Abstraction (var, Variable var) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs index 305216e..16399c7 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs @@ -1,6 +1,7 @@ -namespace LambdaInterpreter +namespace LambdaInterpreter.Console open System +open LambdaInterpreter /// Module containing utility regarding the console output color. module ColorScheme = diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs index 858f272..5843a04 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs @@ -1,4 +1,6 @@ -namespace LambdaInterpreter +namespace LambdaInterpreter.Console + +open LambdaInterpreter /// Module containing utility regarding the exit code of the app. module ExitCode = @@ -9,7 +11,7 @@ module ExitCode = | Success = 0 /// The given command line arguments are invalid. - | BadArguments = 1 + | InvalidArguments = 1 /// The given source file was not found. | FileNotFound = 2 diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Help.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Help.fs new file mode 100644 index 0000000..6e33654 --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Help.fs @@ -0,0 +1,42 @@ +namespace LambdaInterpreter.Console + +open System +open LambdaInterpreter.Syntax + +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 index b5e7125..e52ef3a 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Options.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Options.fs @@ -1,4 +1,4 @@ -namespace LambdaInterpreter +namespace LambdaInterpreter.Console open System diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index 66e195c..9514431 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -4,7 +4,7 @@ open System open System.IO open FParsec -open Keywords +open LambdaInterpreter.Syntax open AST open Parser @@ -26,28 +26,6 @@ type Interpreter private (stream: Stream, interactive: bool, ?verbose: bool, ?li let tryAddCurrentLine str = if lineNumber then $"[Line {currentLine}] {str}" else str - /// Print help info to the standard output. - static member PrintHelp () = 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: - >>> {DeclarationKeyword} S = \\x y z.x z (y z) - >>> {DeclarationKeyword} K = \\x y.x - >>> S K K - \\z.z - -Commands: - {ResetKeyword}\t\t Reset defined variables - {HelpKeyword}\t\t Display help - {ClearKeyword}\t\t Clear console buffer - {ExitKeyword}\t\t Stop the execution and exit -" - /// Create an interactive interpreter for the standard console input. /// Use `verbose` option to print logs to the console. static member StartInteractive (?verbose: bool): Interpreter = @@ -89,7 +67,7 @@ Commands: let runCommand (command: SpecialCommand) = match command with | Reset -> reducer.Reset () - | Help -> if interactive then Interpreter.PrintHelp () + | Help -> if interactive then Help.printSyntaxHelp () | Clear -> if interactive then Console.Clear () | Exit -> reader.Close () None diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj index 21357b5..af60fdd 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -11,11 +11,13 @@ + + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index 4e616ef..7afd065 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -2,40 +2,22 @@ open System open System.IO open LambdaInterpreter -open Keywords +open LambdaInterpreter.Console open ColorScheme open ExitCode +open Help /// Print header with general info about the app and a help suggestion. -let printHeader () = - printfn $" -Lambda Interpreter ------------------- -An interactive lambda term interpreter. +let printHeaderWithHelpSuggestion () = + printHeader () + printHelpSuggestion () -Type '{HelpKeyword}' for more info. -" - -/// Print command line help. -let printHelp () = - printfn $" -Lambda Interpreter ------------------- -An interactive lambda term interpreter. -It can either be run interactively using the standard input, -or on a specified source file. - -Usage: LambdaInterpreter [path-to-file] [options] - -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" - Interpreter.PrintHelp () - -/// Message to print when failed to interpret the given command line args. -let invalidArgsMessage = - $"Invalid command line arguments provided. For more info use '{Array.last Options.HelpArgs}' option." +/// 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) = @@ -52,12 +34,12 @@ let handleOutput (Color success, Color error) (output: Result) = let options = Options.GetFromArgs () if options.Help then - printHelp () + printHeaderWithHelp () exit <| int ExitCode.Success if options.Error then printMessage ConsoleColor.Red invalidArgsMessage - exit <| int ExitCode.BadArguments + exit <| int ExitCode.InvalidArguments let interpreter = match options.SourceFile with @@ -70,7 +52,7 @@ let interpreter = using interpreter (fun interpreter -> let colorScheme = getColorScheme interpreter - if interpreter.IsInteractive then printHeader () + if interpreter.IsInteractive then printHeaderWithHelpSuggestion () for output in interpreter.RunToEnd () do handleOutput colorScheme output diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index a0763f8..e7dc4e7 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -1,6 +1,8 @@ namespace LambdaInterpreter open System + +open LambdaInterpreter.Syntax open AST /// Log record of reducer execution. diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index 842ad0c..3923e9b 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -1,4 +1,4 @@ -namespace LambdaInterpreter +namespace LambdaInterpreter.Syntax open System open Primary diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs new file mode 100644 index 0000000..8c3332e --- /dev/null +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs @@ -0,0 +1,28 @@ +namespace LambdaInterpreter.Syntax + +open Keywords + +module Help = + + /// 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: + >>> {DeclarationKeyword} S = \\x y z.x z (y z) + >>> {DeclarationKeyword} K = \\x y.x + >>> S K K + \\z.z + +Commands: + {ResetKeyword}\t\t Reset defined variables + {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 index a98a446..f732255 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs @@ -1,4 +1,4 @@ -namespace LambdaInterpreter +namespace LambdaInterpreter.Syntax /// Module dealing with keyword definitions. module Keywords = diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs index 40353f7..bf905ca 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs @@ -1,4 +1,4 @@ -namespace LambdaInterpreter +namespace LambdaInterpreter.Syntax open FParsec diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs index 75a1165..f39010c 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs @@ -1,4 +1,4 @@ -namespace LambdaInterpreter +namespace LambdaInterpreter.Syntax /// A variable of specific name. type Variable = Name of string From 04968b28b3c8aa00ddbcf91eb78962ec270117e0 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Tue, 29 Apr 2025 19:06:45 +0300 Subject: [PATCH 33/50] add display command --- .../LambdaInterpreter.Tests/ParserTests.fs | 2 ++ .../LambdaInterpreter/Console/Help.fs | 1 + .../LambdaInterpreter/Interpreter.fs | 1 + .../LambdaInterpreter/Reducer.fs | 18 ++++++++++++++++++ .../LambdaInterpreter/Syntax/Help.fs | 2 ++ .../LambdaInterpreter/Syntax/Keywords.fs | 5 +++++ .../LambdaInterpreter/Syntax/Parser.fs | 5 ++++- .../LambdaInterpreter/Syntax/Primary.fs | 1 + 8 files changed, 34 insertions(+), 1 deletion(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs index 99c4a60..f1523bf 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs @@ -56,6 +56,7 @@ let testParser_Variable () = "letvar", variable, Some 6; "not_a_let", variable, Some 9; "exit", variable, None; + "display", variable, None; ] |> runTest [] @@ -174,6 +175,7 @@ let testParser_Definition () = let testParser_Command () = [ "reset", command, Some 5; + "display", command, Some 7; "help", command, Some 4; "clear", command, Some 5; "exit", command, Some 4; diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Help.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Help.fs index 6e33654..cac2fec 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Help.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/Help.fs @@ -3,6 +3,7 @@ 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. diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index 9514431..92be2c4 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -67,6 +67,7 @@ type Interpreter private (stream: Stream, interactive: bool, ?verbose: bool, ?li let runCommand (command: SpecialCommand) = match command with | Reset -> reducer.Reset () + | Display -> if interactive then reducer.Display () | Help -> if interactive then Help.printSyntaxHelp () | Clear -> if interactive then Console.Clear () | Exit -> reader.Close () diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index e7dc4e7..fd16e64 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -16,6 +16,8 @@ type LogRecord = | UnableToReduce of LambdaTerm | NewDefinition of Variable * LambdaTerm | DefinitionsReset + | DisplayingDefinitions + | NoVariablesDefined /// Class performing lambda term reduction. /// Use `verbose` option to print logs to the console. @@ -49,8 +51,14 @@ type Reducer (?verbose: bool) = $"| 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" + /// Print the given definition of `var` with `term` to the console. + let printDefinition (Name var, term) = + printfn $"- {var} := {toString term}" + /// Get free variables of the given lambda `term`. let rec freeVars term = match term with @@ -124,6 +132,16 @@ type Reducer (?verbose: bool) = variables <- [] log <| DefinitionsReset + /// Print defined variables to the console in order of addition. + member _.Display () = + log <| DisplayingDefinitions + if variables.IsEmpty then log <| NoVariablesDefined else + variables + |> List.rev + |> List.distinct + |> List.map printDefinition + |> ignore + /// Perform beta-reduction of the given lambda `term` according to defined variables. /// Perform alpha-conversion if necessary. member _.Reduce (term: LambdaTerm): LambdaTerm = diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs index 8c3332e..bde1595 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs @@ -2,6 +2,7 @@ namespace LambdaInterpreter.Syntax open Keywords +/// Module for displaying syntax help. module Help = /// Print syntax help to the standard output. @@ -22,6 +23,7 @@ Examples: 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 index f732255..838ad30 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Keywords.fs @@ -15,6 +15,10 @@ module Keywords = [] let ResetKeyword = "reset" + /// Keyword for displaying defined variables. + [] + let DisplayKeyword = "display" + /// Keyword for displaying help info. [] let HelpKeyword = "help" @@ -31,6 +35,7 @@ module Keywords = let keywords = [ DeclarationKeyword; ResetKeyword; + DisplayKeyword; HelpKeyword; ClearKeyword; ExitKeyword; diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs index bf905ca..d2d15ef 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs @@ -76,6 +76,9 @@ module Parser = /// 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) @@ -86,7 +89,7 @@ module Parser = let exit: Parser = pstring ExitKeyword >>. preturn (Command Exit) /// Accept a special interpreter command. - let command = choice [reset; help; clear; exit] + let command = choice [reset; display; help; clear; exit] /// Accept an expression or an empty string. let expressionOpt = choice [attempt term |>> Result; definition; command; preturn Epsilon] diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs index f39010c..6ad5efa 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs @@ -9,6 +9,7 @@ type Variables = Variable list /// A special command for managing the interpreter execution. type SpecialCommand = | Reset + | Display | Help | Clear | Exit From b1accccbad43ecb099a7cc9afe83140251cf2ae3 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Tue, 29 Apr 2025 20:15:13 +0300 Subject: [PATCH 34/50] add Logger class, refactor --- .../LambdaInterpreter.fsproj | 1 + .../LambdaInterpreter/Logger.fs | 45 ++++++++++++ .../LambdaInterpreter/Reducer.fs | 69 +++++-------------- 3 files changed, 63 insertions(+), 52 deletions(-) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter/Logger.fs diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj index af60fdd..23b185e 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -12,6 +12,7 @@ + diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Logger.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Logger.fs new file mode 100644 index 0000000..88c55d9 --- /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} -> {toStringWithBrackets 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/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index fd16e64..86f73d9 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -5,24 +5,10 @@ open System 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 performing lambda term reduction. /// Use `verbose` option to print logs to the console. type Reducer (?verbose: bool) = - let verbose = defaultArg verbose false + let logger = new Logger (?verbose=verbose) let mutable variables: (Variable * LambdaTerm) list = [] /// Max allowed depth of recursion during the term reduction. @@ -33,32 +19,6 @@ type Reducer (?verbose: bool) = [] let StackOverflowMessage = "Error: max recursion depth exceeded during the reduction." - /// Print a log message from the given `record` according to verbosity. - let log record = - 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} -> {toStringWithBrackets 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" - - /// Print the given definition of `var` with `term` to the console. - let printDefinition (Name var, term) = - printfn $"- {var} := {toString term}" - /// Get free variables of the given lambda `term`. let rec freeVars term = match term with @@ -77,7 +37,7 @@ type Reducer (?verbose: bool) = let rec substitute term (Name var) sub = match term with | Variable (Name x) when x = var -> - log <| Substitution (Name var, sub) + logger.Log <| Substitution (Name var, sub) sub | Variable _ as var -> var | Abstraction (Name x, _) as abs when x = var -> abs @@ -88,7 +48,7 @@ type Reducer (?verbose: bool) = Abstraction (Name x, substitute term (Name var) sub) else let y = nextFreeVar x (Set.union freeVarsS freeVarsT) |> Name - log <| AlphaConversion (Name x, y) + logger.Log <| AlphaConversion (Name x, y) Abstraction (y, substitute (substitute term (Name x) (Variable y)) (Name var) sub) | Application (left, right) -> Application (substitute left (Name var) sub, substitute right (Name var) sub) @@ -103,16 +63,16 @@ type Reducer (?verbose: bool) = let reduce term = let rec reduce term depth = if depth > MaxRecursionDepth then raise <| StackOverflowException StackOverflowMessage - log <| Reducing term + logger.Log <| Reducing term match term with | Variable _ as var -> var | Abstraction (x, term) -> Abstraction (x, reduce term (depth + 1)) | Application (Abstraction (var, term) as abs, sub) as source -> - log <| BetaReduction (source, term, var, sub) + logger.Log <| BetaReduction (source, term, var, sub) let term = substitute term var sub if term <> source then reduce term (depth + 1) else - log <| UnableToReduce term + logger.Log <| UnableToReduce term Application (reduce abs (depth + 1), reduce sub (depth + 1)) | Application (left, right) -> let left = reduce left (depth + 1) @@ -125,17 +85,22 @@ type Reducer (?verbose: bool) = /// Define a `var` to be substituted with the given `term`. member _.AddDefinition (var: Variable, term: LambdaTerm) = variables <- (var, term) :: variables - log <| NewDefinition (var, term) + logger.Log <| NewDefinition (var, term) /// Reset defined variables. member _.Reset () = variables <- [] - log <| DefinitionsReset + logger.Log <| DefinitionsReset /// Print defined variables to the console in order of addition. member _.Display () = - log <| DisplayingDefinitions - if variables.IsEmpty then log <| NoVariablesDefined else + + /// 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 @@ -145,7 +110,7 @@ type Reducer (?verbose: bool) = /// Perform beta-reduction of the given lambda `term` according to defined variables. /// Perform alpha-conversion if necessary. member _.Reduce (term: LambdaTerm): LambdaTerm = - log <| StartedReducing term + logger.Log <| StartedReducing term let result = variables |> substituteMany term |> reduce - log <| DoneReducing + logger.Log <| DoneReducing result From 1e4965b26d07a1690629e4cb04fd01f8014742e9 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Tue, 29 Apr 2025 20:18:15 +0300 Subject: [PATCH 35/50] update tests --- .../LambdaInterpreter.Tests/InterpreterTests.fs | 2 ++ .../LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test02.txt | 2 ++ 2 files changed, 4 insertions(+) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index 7f68a39..2f78d10 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -87,6 +87,8 @@ let unsuccessfulCasesResults: Result list list = [ Error e; Error e; Error e; + Error e; + Error e; ]; [ // Test 3 Error e; diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test02.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test02.txt index 5d9a624..eb07c8b 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test02.txt +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test02.txt @@ -1,5 +1,6 @@ let let = a let reset = B +let display = trololo let help = Q let clear = P let exit = ololo @@ -9,3 +10,4 @@ a help test let clear ( a b c) exit ooo +to display From 4c0ca5de8e285be8039fb3c18b0ca022466e778d Mon Sep 17 00:00:00 2001 From: bygu4 Date: Wed, 30 Apr 2025 00:17:17 +0300 Subject: [PATCH 36/50] correct application parsing with closing abstraction, update tests --- .../InterpreterTests.fs | 20 ++++++++++------ .../LambdaInterpreter.Tests/ParserTests.fs | 8 +++++-- .../TestFiles/Successful/Test02.txt | 3 +++ .../TestFiles/Successful/Test05.txt | 7 +++++- .../LambdaInterpreter/Syntax/AST.fs | 19 ++++++++++----- .../LambdaInterpreter/Syntax/Parser.fs | 23 +++++++++++-------- .../LambdaInterpreter/Syntax/Primary.fs | 7 +++--- 7 files changed, 59 insertions(+), 28 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index 2f78d10..23bc7f2 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -8,8 +8,8 @@ open System.IO open LambdaInterpreter let testFilesDir = "TestFiles" -let successfulCasesPath = Path.Join [| testFilesDir; "Successful" |] -let unsuccessfulCasesPath = Path.Join [| testFilesDir; "Unsuccessful" |] +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 @@ -24,15 +24,18 @@ let successfulCasesResults: Result list list = [ [ // 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 "\\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 "\\x.\\y.z \\x.y x"; + Ok "Mult (Sum \\P.P)"; + Ok "second third \\x.x first"; Ok "second third"; ]; [ // Test 4 @@ -44,6 +47,9 @@ let successfulCasesResults: Result list list = [ 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"; @@ -114,7 +120,7 @@ let unsuccessfulCasesResults: Result list list = [ ]; [ // Test 5 Error e; - Ok "(\\x.x x) (\\x.x x)"; + Ok "(\\x.x x) \\x.x x"; ]; ] diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs index f1523bf..6d98546 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ParserTests.fs @@ -105,6 +105,8 @@ let testParser_Application () = "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 [] @@ -136,8 +138,9 @@ let testParser_Term () = "\\x.\\y", term, None; "_q", term, None; "a, b, c", term, Some 1; - "\\X Y Z.Z \\t.X Y", term, Some 9; + "\\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 [] @@ -206,5 +209,6 @@ let testParser_Expression () = "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, 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/TestFiles/Successful/Test02.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test02.txt index c5be3eb..d6e238c 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test02.txt +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test02.txt @@ -6,5 +6,8 @@ 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/Test05.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test05.txt index 716dcf3..f63a210 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test05.txt +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test05.txt @@ -5,4 +5,9 @@ res reset snd -res \ No newline at end of file +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/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index 3923e9b..1e9bc9c 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -6,7 +6,7 @@ open Primary /// Module dealing with finalized syntax trees of lambda expressions. module AST = - /// Definition of the lambda term. + /// The finalized lambda term representation. type LambdaTerm = | Variable of Variable | Abstraction of Variable * LambdaTerm @@ -31,11 +31,12 @@ module AST = /// Build AST of lambda term application using term on the `left` and the rest on `right`. let rec buildAST_Application (left: LambdaTerm, right: Primary.ApplicationOpt) = match right with - | Apply (operand, rest) -> + | WithContinuation (operand, rest) -> let right = buildAST_Operand operand let partial = Application (left, right) buildAST_Application (partial, rest) - | ApplicationOpt.Epsilon -> left + | FinalAbstraction abs -> Application (left, buildAST_Term abs) + | Epsilon -> left match primary with | Primary.Application (operand, rest) -> @@ -53,16 +54,22 @@ module AST = | Primary.Definition (variable, term) -> Definition (variable, buildAST_Term term) | Primary.Result term -> Result (buildAST_Term term) | Primary.Command command -> Command command - | Epsilon -> Empty + | Primary.Empty -> Empty /// Get a string representation of the given lambda `term`. /// Add brackets if necessary for a proper operation priority. let rec private toStringInternal (term: LambdaTerm) (withBrackets: bool) = match term with | Variable (Name var) -> var + | Application (Application (left, (Abstraction _ as abs)), right) -> + let left = toStringInternal left left.IsAbstraction + let abs = toStringInternal abs true + let right = toStringInternal right right.IsApplication + let term = $"{left} {abs} {right}" + if withBrackets then $"({term})" else term | Application (left, right) -> - let left = $"{toStringInternal left left.IsAbstraction}" - let right = $"{toStringInternal right (right.IsAbstraction || right.IsApplication)}" + let left = toStringInternal left left.IsAbstraction + let right = toStringInternal right right.IsApplication let term = $"{left} {right}" if withBrackets then $"({term})" else term | Abstraction (Name var, term) -> diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs index d2d15ef..05396c9 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs @@ -47,20 +47,25 @@ module Parser = /// 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 = - between ((?>)(pchar '(')) ((?<)(pchar ')')) term |>> Brackets - <|> (variable |>> Variable) + 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 () - applicationOptRef.Value <- - attempt (!>. applicationOpt) |>> Apply - <|> preturn ApplicationOpt.Epsilon + /// Accept an operand application with continuation. + let applicationOpt' = attempt (!>. applicationOpt) |>> WithContinuation - /// Accept a lambda abstraction. - let abstraction = between (pchar '\\') (pchar '.') variables .>>. (?<)term |>> Abstraction + /// 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 @@ -92,7 +97,7 @@ module Parser = let command = choice [reset; display; help; clear; exit] /// Accept an expression or an empty string. - let expressionOpt = choice [attempt term |>> Result; definition; command; preturn Epsilon] + 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 index 6ad5efa..fd2d209 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Primary.fs @@ -24,7 +24,8 @@ module Primary = /// Optional lambda term application. and ApplicationOpt = - | Apply of Operand * ApplicationOpt + | WithContinuation of Operand * ApplicationOpt + | FinalAbstraction of Term | Epsilon /// An operand in lambda term application. @@ -32,9 +33,9 @@ module Primary = | Variable of Variable | Brackets of Term - /// An expression as a variable definition or a term result. + /// An expression to be interpreted. type Expression = | Definition of Variable * Term | Result of Term | Command of SpecialCommand - | Epsilon + | Empty From c6216ee735dbd97089d609028819c269dd8b2529 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Wed, 30 Apr 2025 00:42:47 +0300 Subject: [PATCH 37/50] minor refactoring --- .../LambdaInterpreter/LambdaInterpreter/Interpreter.fs | 2 +- .../LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs | 10 +++++++--- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index 92be2c4..d24e227 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -20,7 +20,7 @@ type Interpreter private (stream: Stream, interactive: bool, ?verbose: bool, ?li /// Print a pointer indicating the start of input when running an interactive interpreter. let tryPrintInputPointer () = - if interactive then printf ">>> " + if interactive then printf "%s" Help.InputPointer /// Add current line number to the given string when running on a source file. let tryAddCurrentLine str = diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs index bde1595..9aa9caf 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Help.fs @@ -5,6 +5,10 @@ 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 $" @@ -16,9 +20,9 @@ Syntax: definition\t\t {DeclarationKeyword} {{variable}} = {{term}} Examples: - >>> {DeclarationKeyword} S = \\x y z.x z (y z) - >>> {DeclarationKeyword} K = \\x y.x - >>> S K K + {InputPointer}{DeclarationKeyword} S = \\x y z.x z (y z) + {InputPointer}{DeclarationKeyword} K = \\x y.x + {InputPointer}S K K \\z.z Commands: From 48a12da4d3db9cdcf559444609f845898624a1d4 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Wed, 30 Apr 2025 00:48:59 +0300 Subject: [PATCH 38/50] update comments --- Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs | 1 + 1 file changed, 1 insertion(+) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs index 5843a04..568c93c 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs @@ -5,6 +5,7 @@ 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. From 672f7a125e3df4a185a1df1ff60ac286f8f58737 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Wed, 30 Apr 2025 01:14:36 +0300 Subject: [PATCH 39/50] simplify code in reducer --- .../LambdaInterpreter/LambdaInterpreter/Reducer.fs | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index 86f73d9..19521b7 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -34,7 +34,7 @@ type Reducer (?verbose: bool) = /// Substitute free occurrences of variable `var` in `term` with given term `sub`. /// Perform alpha-conversion if necessary. - let rec substitute term (Name var) sub = + let rec substitute term (Name var, sub) = match term with | Variable (Name x) when x = var -> logger.Log <| Substitution (Name var, sub) @@ -45,18 +45,17 @@ type Reducer (?verbose: bool) = let freeVarsS = freeVars sub let freeVarsT = freeVars term if not (Set.contains var freeVarsT && Set.contains x freeVarsS) then - Abstraction (Name x, substitute term (Name var) sub) + Abstraction (Name x, substitute term (Name var, sub)) else let y = nextFreeVar x (Set.union freeVarsS freeVarsT) |> Name logger.Log <| AlphaConversion (Name x, y) - Abstraction (y, substitute (substitute term (Name x) (Variable y)) (Name var) sub) + Abstraction (y, substitute (substitute term (Name x, Variable y)) (Name var, sub)) | Application (left, right) -> - Application (substitute left (Name var) sub, substitute right (Name var) sub) + Application (substitute left (Name var, sub), substitute right (Name var, sub)) /// Substitute variables in `term` according to the given `subs` pair sequence. let substituteMany term subs = - subs - |> Seq.fold (fun acc (var, sub) -> substitute acc var sub) term + subs |> Seq.fold substitute term /// Perform beta-reduction of the given lambda `term`. /// Perform alpha-conversion if necessary. @@ -69,7 +68,7 @@ type Reducer (?verbose: bool) = | Abstraction (x, term) -> Abstraction (x, reduce term (depth + 1)) | Application (Abstraction (var, term) as abs, sub) as source -> logger.Log <| BetaReduction (source, term, var, sub) - let term = substitute term var sub + let term = substitute term (var, sub) if term <> source then reduce term (depth + 1) else logger.Log <| UnableToReduce term From 35a5d13eca1f10f99d9814873da71a823ebc900b Mon Sep 17 00:00:00 2001 From: bygu4 Date: Wed, 30 Apr 2025 23:20:40 +0300 Subject: [PATCH 40/50] rewrite reduction in CPS, update naming --- .../InterpreterTests.fs | 2 +- .../LambdaInterpreter/Console/ColorScheme.fs | 3 + .../LambdaInterpreter/Console/ExitCode.fs | 6 +- .../LambdaInterpreter/Interpreter.fs | 12 ++-- .../LambdaInterpreter/Program.fs | 4 +- .../LambdaInterpreter/Reducer.fs | 55 +++++++++++++------ 6 files changed, 53 insertions(+), 29 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index 23bc7f2..bc47c1e 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -150,4 +150,4 @@ let testInterpreter (sourceFile: string, expectedOutput: Result let interpreter = Interpreter.StartOnFile sourceFile let output = interpreter.RunToEnd () |> Seq.toList output |> outputsMatch expectedOutput |> should be True - (interpreter.SyntaxError || interpreter.StackOverflow) |> should equal shouldFail + (interpreter.SyntaxError || interpreter.MaxDepthExceeded) |> should equal shouldFail diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs index 16399c7..41ab13b 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ColorScheme.fs @@ -15,6 +15,9 @@ module ColorScheme = /// 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 diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs index 568c93c..54c99a1 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Console/ExitCode.fs @@ -20,12 +20,12 @@ module ExitCode = /// A syntax error occurred during source file interpretation. | SyntaxError = 3 - /// A stack overflow occurred during the source file term reduction. - | StackOverflow = 4 + /// 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.StackOverflow then ExitCode.StackOverflow else + if interpreter.MaxDepthExceeded then ExitCode.MaxDepthExceeded else ExitCode.Success diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index d24e227..7bd343d 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -16,7 +16,7 @@ type Interpreter private (stream: Stream, interactive: bool, ?verbose: bool, ?li let mutable currentLine = 0 let mutable syntaxError = false - let mutable stackOverflow = false + let mutable maxDepthExceeded = false /// Print a pointer indicating the start of input when running an interactive interpreter. let tryPrintInputPointer () = @@ -47,8 +47,8 @@ type Interpreter private (stream: Stream, interactive: bool, ?verbose: bool, ?li /// Whether a syntax error occurred during the interpretation. member _.SyntaxError: bool = syntaxError - /// Whether a stack overflow occurred during the term reduction. - member _.StackOverflow: bool = stackOverflow + /// 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 = @@ -66,8 +66,8 @@ type Interpreter private (stream: Stream, interactive: bool, ?verbose: bool, ?li /// Execute the given special interpreter `command`. let runCommand (command: SpecialCommand) = match command with - | Reset -> reducer.Reset () - | Display -> if interactive then reducer.Display () + | Reset -> reducer.ResetDefinitions () + | Display -> if interactive then reducer.DisplayDefinitions () | Help -> if interactive then Help.printSyntaxHelp () | Clear -> if interactive then Console.Clear () | Exit -> reader.Close () @@ -86,7 +86,7 @@ type Interpreter private (stream: Stream, interactive: bool, ?verbose: bool, ?li |> Result.Ok |> Some with :? StackOverflowException as ex -> - stackOverflow <- true + maxDepthExceeded <- true ex.Message |> tryAddCurrentLine |> Result.Error |> Some | Command command -> runCommand command | Empty -> None diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs index 7afd065..49219ec 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Program.fs @@ -38,7 +38,7 @@ if options.Help then exit <| int ExitCode.Success if options.Error then - printMessage ConsoleColor.Red invalidArgsMessage + printMessage defaultErrorColor invalidArgsMessage exit <| int ExitCode.InvalidArguments let interpreter = @@ -46,7 +46,7 @@ let interpreter = | Some path -> try Interpreter.StartOnFile (path, options.Verbose, options.LineNumber) with :? IOException | :? UnauthorizedAccessException as ex -> - printMessage ConsoleColor.Red ex.Message + printMessage defaultErrorColor ex.Message exit <| int ExitCode.FileNotFound | None -> Interpreter.StartInteractive options.Verbose diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index 19521b7..d4aff90 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -13,11 +13,11 @@ type Reducer (?verbose: bool) = /// Max allowed depth of recursion during the term reduction. [] - let MaxRecursionDepth = 4096 + let MaxDepth = 1000000 - /// Message to fail with in case of stack overflow. + /// Message to fail with in case of max recursion depth exceeding. [] - let StackOverflowMessage = "Error: max recursion depth exceeded during the reduction." + let MaxDepthExceededMessage = "Error: max recursion depth exceeded during the reduction." /// Get free variables of the given lambda `term`. let rec freeVars term = @@ -60,26 +60,47 @@ type Reducer (?verbose: bool) = /// Perform beta-reduction of the given lambda `term`. /// Perform alpha-conversion if necessary. let reduce term = - let rec reduce term depth = - if depth > MaxRecursionDepth then raise <| StackOverflowException StackOverflowMessage + + /// Reduce `term` in CPS using the given `cont`. + /// Keep track of `depth` of the reduction and throw exception in case of exceeding. + let rec reduce term depth cont = + if depth > MaxDepth then raise <| StackOverflowException MaxDepthExceededMessage logger.Log <| Reducing term match term with - | Variable _ as var -> var - | Abstraction (x, term) -> Abstraction (x, reduce term (depth + 1)) + + // 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) -> + reduce term (depth + 1) ( + fun reducedTerm -> Abstraction (var, reducedTerm) |> cont + ) + + // Perform beta reduction and then 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) - if term <> source then reduce term (depth + 1) + if term <> source then reduce term depth cont else logger.Log <| UnableToReduce term - Application (reduce abs (depth + 1), reduce sub (depth + 1)) + reduce abs (depth + 1) (fun reducedAbs -> + reduce sub (depth + 1) (fun reducedSub -> + Application (reducedAbs, reducedSub) |> cont + ) + ) + + // Reduce both parts of the application and pass it to continuation. | Application (left, right) -> - let left = reduce left (depth + 1) - let right = reduce right (depth + 1) - match left with - | Abstraction _ -> reduce (Application (left, right)) (depth + 1) - | _ -> Application (left, right) - in reduce term 0 + reduce left (depth + 1) (fun reducedLeft -> + reduce right (depth + 1) (fun reducedRight -> + match reducedLeft with + | Abstraction _ -> reduce (Application (reducedLeft, reducedRight)) depth cont + | _ -> Application (reducedLeft, reducedRight) |> cont + ) + ) + + in reduce term 0 id /// Define a `var` to be substituted with the given `term`. member _.AddDefinition (var: Variable, term: LambdaTerm) = @@ -87,12 +108,12 @@ type Reducer (?verbose: bool) = logger.Log <| NewDefinition (var, term) /// Reset defined variables. - member _.Reset () = + member _.ResetDefinitions () = variables <- [] logger.Log <| DefinitionsReset /// Print defined variables to the console in order of addition. - member _.Display () = + member _.DisplayDefinitions () = /// Print the given definition of `var` with `term` to the console. let printDefinition (Name var, term) = From 9f3c1c7d7970a0982dfc7348296a9f174c1540c6 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Thu, 1 May 2025 00:39:51 +0300 Subject: [PATCH 41/50] rewrite substitution and free variable obtaining in CPS, refactor --- .../LambdaInterpreter/Reducer.fs | 108 ++++++++++++------ 1 file changed, 73 insertions(+), 35 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index d4aff90..c93f340 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -20,12 +20,24 @@ type Reducer (?verbose: bool) = let MaxDepthExceededMessage = "Error: max recursion depth exceeded during the reduction." /// Get free variables of the given lambda `term`. - let rec freeVars term = - match term with - | Variable (Name v) -> set [v] - | Abstraction (Name v, term) -> Set.remove v (freeVars term) - | Application (left, right) -> - Set.union (freeVars left) (freeVars right) + let freeVars term = + + /// Get free variables of the given lambda `term` using CPS with the given `cont`. + let rec freeVars term cont = + match term with + | Variable (Name v) -> set [v] |> cont + | Abstraction (Name v, term) -> + freeVars term (fun termVars -> + Set.remove v termVars |> cont + ) + | Application (left, right) -> + freeVars left (fun leftVars -> + freeVars right (fun rightVars -> + Set.union leftVars rightVars |> cont + ) + ) + + in freeVars term id /// Get a variable, starting with `prefix`, that is not in `freeVars`. let rec nextFreeVar prefix freeVars = @@ -34,24 +46,50 @@ type Reducer (?verbose: bool) = /// Substitute free occurrences of variable `var` in `term` with given term `sub`. /// Perform alpha-conversion if necessary. - let rec substitute term (Name var, sub) = - match term with - | Variable (Name x) when x = var -> - logger.Log <| Substitution (Name var, sub) - sub - | Variable _ as var -> var - | Abstraction (Name x, _) as abs when x = var -> abs - | Abstraction (Name x, term) -> - let freeVarsS = freeVars sub - let freeVarsT = freeVars term - if not (Set.contains var freeVarsT && Set.contains x freeVarsS) then - Abstraction (Name x, substitute term (Name var, sub)) - else - let y = nextFreeVar x (Set.union freeVarsS freeVarsT) |> Name - logger.Log <| AlphaConversion (Name x, y) - Abstraction (y, substitute (substitute term (Name x, Variable y)) (Name var, sub)) - | Application (left, right) -> - Application (substitute left (Name var, sub), substitute right (Name var, sub)) + let substitute term (Name var, sub) = + + /// Substitute free occurrences of variable `var` in `term` with given term `sub`. + /// Use CPS with the given `cont`. + let rec substitute 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 + + // Check free variables and perform alpha-conversion to avoid capturing. + | 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) + substitute term (Name x, Variable y) (fun converted -> + substitute converted (Name var, sub) (fun subsTerm -> + Abstraction (y, subsTerm) |> cont + ) + ) + else + substitute term (Name var, sub) (fun subsTerm -> + Abstraction (Name x, subsTerm) |> cont + ) + + // Make substitution in both parts of the application. + | Application (left, right) -> + substitute left (Name var, sub) (fun subsLeft -> + substitute right (Name var, sub) (fun subsRight -> + Application (subsLeft, subsRight) |> cont + ) + ) + + in substitute term (Name var, sub) id /// Substitute variables in `term` according to the given `subs` pair sequence. let substituteMany term subs = @@ -73,11 +111,11 @@ type Reducer (?verbose: bool) = // Reduce the right part of the abstraction and pass it to continuation. | Abstraction (var, term) -> - reduce term (depth + 1) ( - fun reducedTerm -> Abstraction (var, reducedTerm) |> cont + reduce term (depth + 1) (fun reducedTerm -> + Abstraction (var, reducedTerm) |> cont ) - // Perform beta reduction and then reduce the result. + // Perform beta-reduction and then 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) @@ -102,6 +140,14 @@ type Reducer (?verbose: bool) = in reduce term 0 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 @@ -126,11 +172,3 @@ type Reducer (?verbose: bool) = |> List.distinct |> List.map printDefinition |> ignore - - /// 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 From 929bd8528cb0e40ae50ffea040529bb8d3c217ee Mon Sep 17 00:00:00 2001 From: bygu4 Date: Thu, 1 May 2025 02:32:45 +0300 Subject: [PATCH 42/50] correct term to string transformation, update tests --- .../InterpreterTests.fs | 1 + .../TestFiles/Successful/Test04.txt | 6 ++++- .../LambdaInterpreter/Logger.fs | 2 +- .../LambdaInterpreter/Syntax/AST.fs | 25 ++++++++----------- .../LambdaInterpreter/Syntax/Parser.fs | 2 +- 5 files changed, 18 insertions(+), 18 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index bc47c1e..c8c5df8 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -42,6 +42,7 @@ let successfulCasesResults: Result list list = [ 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"; diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test04.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test04.txt index e55c7cf..72e2014 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test04.txt +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test04.txt @@ -3,4 +3,8 @@ x y let x = \z.x x y -(\x y.x y) y \ No newline at end of file +(\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/Logger.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Logger.fs index 88c55d9..58ea3fa 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Logger.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Logger.fs @@ -33,7 +33,7 @@ type Logger (?verbose: bool) = | AlphaConversion (Name x, Name y) -> $"| [alpha-conversion]: {x} -> {y}" | BetaReduction (source, term, Name var, sub) -> - $"| [beta-reduction]: {toString source} -> {toStringWithBrackets term}[{var} := {toString sub}]" + $"| [beta-reduction]: {toString source} -> {toStringParenthesized term}[{var} := {toString sub}]" | Substitution (Name var, sub) -> $"| [substitution]: {var} -> {toString sub}" | UnableToReduce term -> diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index 1e9bc9c..ea877e2 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -58,28 +58,23 @@ module AST = /// Get a string representation of the given lambda `term`. /// Add brackets if necessary for a proper operation priority. - let rec private toStringInternal (term: LambdaTerm) (withBrackets: bool) = + let rec private toStringInternal term parenthesized closing = match term with | Variable (Name var) -> var - | Application (Application (left, (Abstraction _ as abs)), right) -> - let left = toStringInternal left left.IsAbstraction - let abs = toStringInternal abs true - let right = toStringInternal right right.IsApplication - let term = $"{left} {abs} {right}" - if withBrackets then $"({term})" else term | Application (left, right) -> - let left = toStringInternal left left.IsAbstraction - let right = toStringInternal right right.IsApplication + let parenthesizedRight = right.IsApplication || right.IsAbstraction && not closing + let left = toStringInternal left left.IsAbstraction false + let right = toStringInternal right parenthesizedRight closing let term = $"{left} {right}" - if withBrackets then $"({term})" else term + if parenthesized then $"({term})" else term | Abstraction (Name var, term) -> - let term = $"\\{var}.{toStringInternal term false}" - if withBrackets then $"({term})" else term + let term = $"\\{var}.{toStringInternal term false true}" + if parenthesized then $"({term})" else term /// Get a string representation of the given lambda `term`. let toString (term: LambdaTerm) = - toStringInternal term false + toStringInternal term false true /// Get a string representation of the given lambda `term` and surround it with brackets if necessary. - let toStringWithBrackets (term: LambdaTerm) = - toStringInternal term true + let toStringParenthesized (term: LambdaTerm) = + toStringInternal term true true diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs index 05396c9..0139487 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/Parser.fs @@ -73,7 +73,7 @@ module Parser = termRef.Value <- choice [application; abstraction] /// Accept a variable declaration. - let declaration = pstring "let" >>. !>. !declaration .>> pchar '=' .>>. !> Definition From 54211a5b6637510d91b0c132a238784c9fc2585b Mon Sep 17 00:00:00 2001 From: bygu4 Date: Thu, 1 May 2025 15:49:22 +0300 Subject: [PATCH 43/50] add more tests, use TailCall attribute --- .../InterpreterTests.fs | 7 + .../TestFiles/Successful/Test09.txt | 12 ++ .../LambdaInterpreter/Reducer.fs | 201 +++++++++--------- 3 files changed, 119 insertions(+), 101 deletions(-) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test09.txt diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index c8c5df8..8735ae6 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -68,6 +68,13 @@ let successfulCasesResults: Result list list = [ ]; [ // Test 8 ]; + [ // Test 9 + Ok "U"; + Ok "V"; + Ok "\\f.f V U"; + Ok "V"; + Ok "U"; + ]; ] let unsuccessfulCasesResults: Result list list = [ 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/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index c93f340..d8afdd7 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -19,126 +19,125 @@ type Reducer (?verbose: bool) = [] let MaxDepthExceededMessage = "Error: max recursion depth exceeded during the reduction." - /// Get free variables of the given lambda `term`. - let freeVars term = - - /// Get free variables of the given lambda `term` using CPS with the given `cont`. - let rec freeVars term cont = - match term with - | Variable (Name v) -> set [v] |> cont - | Abstraction (Name v, term) -> - freeVars term (fun termVars -> - Set.remove v termVars |> cont - ) - | Application (left, right) -> - freeVars left (fun leftVars -> - freeVars right (fun rightVars -> - Set.union leftVars rightVars |> cont - ) + /// 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 ) + ) - in freeVars term id + /// 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 rec nextFreeVar prefix freeVars = - if not (Set.contains prefix freeVars) then prefix - else nextFreeVar (prefix + "'") 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`. - /// Perform alpha-conversion if necessary. - let substitute term (Name var, sub) = - - /// Substitute free occurrences of variable `var` in `term` with given term `sub`. - /// Use CPS with the given `cont`. - let rec substitute 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 - - // Check free variables and perform alpha-conversion to avoid capturing. - | 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) - substitute term (Name x, Variable y) (fun converted -> - substitute converted (Name var, sub) (fun subsTerm -> - Abstraction (y, subsTerm) |> cont - ) - ) - else - substitute term (Name var, sub) (fun subsTerm -> - Abstraction (Name x, subsTerm) |> cont + /// 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 + + // Check free variables and perform alpha-conversion to avoid capturing. + | 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) -> - substitute left (Name var, sub) (fun subsLeft -> - substitute right (Name var, sub) (fun subsRight -> - Application (subsLeft, subsRight) |> 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 ) + ) - in substitute term (Name var, sub) id + /// 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 - /// Perform beta-reduction of the given lambda `term`. - /// Perform alpha-conversion if necessary. - let reduce 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 reduce term depth 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) -> - reduce term (depth + 1) (fun reducedTerm -> - Abstraction (var, reducedTerm) |> cont - ) - - // Perform beta-reduction and then 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) - if term <> source then reduce term depth cont - else - logger.Log <| UnableToReduce term - reduce abs (depth + 1) (fun reducedAbs -> - reduce sub (depth + 1) (fun reducedSub -> - Application (reducedAbs, reducedSub) |> cont - ) + /// 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 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) (fun reducedTerm -> + Abstraction (var, reducedTerm) |> cont + ) + + // Perform beta-reduction and then 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) + if term <> source then reduceCPS term depth cont + else + logger.Log <| UnableToReduce term + reduceCPS abs (depth + 1) (fun reducedAbs -> + reduceCPS sub (depth + 1) (fun reducedSub -> + Application (reducedAbs, reducedSub) |> cont ) + ) - // Reduce both parts of the application and pass it to continuation. - | Application (left, right) -> - reduce left (depth + 1) (fun reducedLeft -> - reduce right (depth + 1) (fun reducedRight -> - match reducedLeft with - | Abstraction _ -> reduce (Application (reducedLeft, reducedRight)) depth cont - | _ -> Application (reducedLeft, reducedRight) |> cont - ) + // Reduce both parts of the application and pass it to continuation. + | Application (left, right) -> + reduceCPS left (depth + 1) (fun reducedLeft -> + reduceCPS right (depth + 1) (fun reducedRight -> + match reducedLeft with + | Abstraction _ -> reduceCPS (Application (reducedLeft, reducedRight)) depth cont + | _ -> Application (reducedLeft, reducedRight) |> cont ) + ) - in reduce term 0 id + /// Perform beta-reduction of the given lambda `term`. + /// Perform alpha-conversion if necessary. + let reduce term = reduceCPS term 0 id /// Perform beta-reduction of the given lambda `term` according to defined variables. /// Perform alpha-conversion if necessary. From beb6445db1e60324d6e52a57cf3e50249d83994f Mon Sep 17 00:00:00 2001 From: bygu4 Date: Thu, 1 May 2025 18:06:38 +0300 Subject: [PATCH 44/50] enable tail call optimization in props --- .../LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj | 1 + 1 file changed, 1 insertion(+) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj index 23b185e..2eb226f 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/LambdaInterpreter.fsproj @@ -4,6 +4,7 @@ net9.0 Exe true + true From 6fe9abaf70c789e6d585368f338b091a9c258595 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Thu, 1 May 2025 22:01:12 +0300 Subject: [PATCH 45/50] add arithmetic test --- .../InterpreterTests.fs | 10 +++++++++ .../TestFiles/Successful/Test10.txt | 21 +++++++++++++++++++ 2 files changed, 31 insertions(+) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test10.txt diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index 8735ae6..8bfc476 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -75,6 +75,16 @@ let successfulCasesResults: Result list list = [ 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)))))))"; + ]; ] let unsuccessfulCasesResults: Result list list = [ 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) From 1ba8ab7758dc0e7a00dc43375c29f80d5dfbd552 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Thu, 1 May 2025 23:37:55 +0300 Subject: [PATCH 46/50] rewrite AST conversions in CPS --- .../LambdaInterpreter/Interpreter.fs | 2 +- .../LambdaInterpreter/Syntax/AST.fs | 84 ++++++++++++------- 2 files changed, 56 insertions(+), 30 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs index 7bd343d..1545ecd 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Interpreter.fs @@ -75,7 +75,7 @@ type Interpreter private (stream: Stream, interactive: bool, ?verbose: bool, ?li /// Interpret the given `primary` expression representation. let interpretExpression (primary: Primary.Expression) = - match buildAST_Expression primary with + match buildExpressionAST primary with | Definition (var, term) -> reducer.AddDefinition (var, term) None diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index ea877e2..0c12f56 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -20,61 +20,87 @@ module AST = | Empty /// Build AST of a lambda term using the `primary` representation. - let rec buildAST_Term (primary: Primary.Term) = + /// Use CPS with the given `cont`. + [] + let rec private buildTermAST_CPS (primary: Primary.Term) cont = /// Convert `primary` operand representation to the lambda term. - let buildAST_Operand (primary: Primary.Operand) = + let buildOperandAST (primary: Primary.Operand) cont = match primary with - | Primary.Variable var -> Variable var - | Brackets term -> buildAST_Term term + | 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 buildAST_Application (left: LambdaTerm, right: Primary.ApplicationOpt) = + let rec buildApplicationAST (left: LambdaTerm) (right: Primary.ApplicationOpt) cont = match right with | WithContinuation (operand, rest) -> - let right = buildAST_Operand operand - let partial = Application (left, right) - buildAST_Application (partial, rest) - | FinalAbstraction abs -> Application (left, buildAST_Term abs) - | Epsilon -> left + 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) -> - let operand = buildAST_Operand operand - buildAST_Application (operand, rest) + buildOperandAST operand (fun operandAST -> + buildApplicationAST operandAST rest cont + ) | Primary.Abstraction (head :: tail, term) -> - if tail.IsEmpty then Abstraction (head, buildAST_Term term) - else Abstraction (head, buildAST_Term (Primary.Abstraction (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 buildAST_Expression (primary: Primary.Expression) = + let buildExpressionAST (primary: Primary.Expression) = match primary with - | Primary.Definition (variable, term) -> Definition (variable, buildAST_Term term) - | Primary.Result term -> Result (buildAST_Term term) + | 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`. - /// Add brackets if necessary for a proper operation priority. - let rec private toStringInternal term parenthesized closing = + /// 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) -> var + | Variable (Name var) -> cont var | Application (left, right) -> + let parenthesizedLeft = left.IsAbstraction let parenthesizedRight = right.IsApplication || right.IsAbstraction && not closing - let left = toStringInternal left left.IsAbstraction false - let right = toStringInternal right parenthesizedRight closing - let term = $"{left} {right}" - if parenthesized then $"({term})" else term + 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) -> - let term = $"\\{var}.{toStringInternal term false true}" - if parenthesized then $"({term})" else 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) = - toStringInternal term false true + toStringCPS term false true id - /// Get a string representation of the given lambda `term` and surround it with brackets if necessary. + /// Get a string representation of the given lambda `term` surrounded with brackets if it's not a variable. let toStringParenthesized (term: LambdaTerm) = - toStringInternal term true true + toStringCPS term true true id From cbf300d62ffc7c4329a4967189b032cb70d36e24 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Fri, 2 May 2025 00:14:10 +0300 Subject: [PATCH 47/50] correct parentheses in term to string conversion --- .../LambdaInterpreter.Tests/InterpreterTests.fs | 1 + .../LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test05.txt | 1 + Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs | 3 ++- 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index 8bfc476..65221fc 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -139,6 +139,7 @@ let unsuccessfulCasesResults: Result list list = [ [ // 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)"; ]; ] diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test05.txt b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test05.txt index 4ea6b16..d5223ce 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test05.txt +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Unsuccessful/Test05.txt @@ -4,3 +4,4 @@ let e = \x.x x x let o = \x.x x let O = o o O +O O O diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs index 0c12f56..c245ee7 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Syntax/AST.fs @@ -81,8 +81,9 @@ module AST = 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 closing + let parenthesizedRight = right.IsApplication || right.IsAbstraction && not closedAbstraction toStringCPS left parenthesizedLeft false (fun leftStr -> toStringCPS right parenthesizedRight closing (fun rightStr -> let termStr = $"{leftStr} {rightStr}" From 9e7731cd51367d50b7a24c62512f8df7ee174a59 Mon Sep 17 00:00:00 2001 From: bygu4 Date: Mon, 5 May 2025 23:26:52 +0300 Subject: [PATCH 48/50] correct the reduction in normal strategy, add factorial test --- .../InterpreterTests.fs | 7 +++ .../TestFiles/Successful/Test11.txt | 23 ++++++++++ .../LambdaInterpreter/Reducer.fs | 45 +++++++++++-------- 3 files changed, 56 insertions(+), 19 deletions(-) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test11.txt diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index 65221fc..e35c344 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -85,6 +85,13 @@ let successfulCasesResults: Result list list = [ 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)))))))))))))))))))))))"; + ]; ] let unsuccessfulCasesResults: Result list list = [ 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/Reducer.fs b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs index d8afdd7..eebfd0c 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter/Reducer.fs @@ -62,7 +62,8 @@ type Reducer (?verbose: bool) = // Our variable is bounded, call continuation. | Abstraction (Name x, _) as abs when x = var -> cont abs - // Check free variables and perform alpha-conversion to avoid capturing. + // 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 @@ -98,7 +99,7 @@ type Reducer (?verbose: bool) = /// 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 cont = + let rec reduceCPS term depth ret cont = if depth > MaxDepth then raise <| StackOverflowException MaxDepthExceededMessage logger.Log <| Reducing term match term with @@ -108,36 +109,42 @@ type Reducer (?verbose: bool) = // Reduce the right part of the abstraction and pass it to continuation. | Abstraction (var, term) -> - reduceCPS term (depth + 1) (fun reducedTerm -> + reduceCPS term (depth + 1) false (fun reducedTerm -> Abstraction (var, reducedTerm) |> cont ) - // Perform beta-reduction and then reduce the result. + // 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) - if term <> source then reduceCPS term depth cont - else - logger.Log <| UnableToReduce term - reduceCPS abs (depth + 1) (fun reducedAbs -> - reduceCPS sub (depth + 1) (fun reducedSub -> - Application (reducedAbs, reducedSub) |> cont + 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 both parts of the application and pass it to continuation. + // 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) (fun reducedLeft -> - reduceCPS right (depth + 1) (fun reducedRight -> - match reducedLeft with - | Abstraction _ -> reduceCPS (Application (reducedLeft, reducedRight)) depth cont - | _ -> Application (reducedLeft, reducedRight) |> cont - ) + 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 id + 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. From 8abf51c06e977ba2b68c86ba52a50d7b1799ce2e Mon Sep 17 00:00:00 2001 From: bygu4 Date: Mon, 5 May 2025 23:52:26 +0300 Subject: [PATCH 49/50] add fibonacci test --- .../InterpreterTests.fs | 8 ++++++ .../TestFiles/Successful/Test12.txt | 25 +++++++++++++++++++ 2 files changed, 33 insertions(+) create mode 100644 Tasks/LambdaInterpreter/LambdaInterpreter.Tests/TestFiles/Successful/Test12.txt diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs index e35c344..e22f859 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/InterpreterTests.fs @@ -92,6 +92,14 @@ let successfulCasesResults: Result list list = [ 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 = [ 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 From fbaab84cdfa6a25c6e8468f0d9d22b02560b9cff Mon Sep 17 00:00:00 2001 From: bygu4 Date: Tue, 6 May 2025 01:09:00 +0300 Subject: [PATCH 50/50] update reducer tests --- .../LambdaInterpreter.Tests/ReducerTests.fs | 171 +++++++++++------- 1 file changed, 101 insertions(+), 70 deletions(-) diff --git a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs index 879860d..6138b22 100644 --- a/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs +++ b/Tasks/LambdaInterpreter/LambdaInterpreter.Tests/ReducerTests.fs @@ -7,104 +7,135 @@ open LambdaInterpreter open LambdaInterpreter.Syntax open AST -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 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 - Variable (Name "x"); - Application (Variable (Name "x"), Variable (Name "y")); - Abstraction (Name "x", Variable (Name "y")); - omega (Name "x"); + var "x"; + Application (var "x", var "y"); + Abstraction (Name "x", var "y"); + omega; // Simple reduction - Application (omega (Name "x"), Variable (Name "y")); - Application (Abstraction (Name "x", Variable (Name "x")), Variable (Name "z")); - Application (Abstraction (Name "x", Application (Variable (Name "x"), Variable (Name "y"))), Variable (Name "z")); - Application (Abstraction (Name "x", Variable (Name "y")), Omega (Name "x")); + 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 (Variable (Name "b"), Variable (Name "c"))), - Variable (Name "x"))); - Application (Variable (Name "x"), Application - (Abstraction (Name "a", omega (Name "y")), - Variable (Name "z"))); + 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 (Variable (Name "a"), Variable (Name "b")))), - Variable (Name "x")), Variable (Name "y")); + (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 "a", Abstraction (Name "b", Abstraction (Name "c", Variable (Name "x")))), - Variable (Name "y")), Variable (Name "y")), Variable (Name "y")); + (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 (id (Name "x"), id (Name "y")); - Abstraction (Name "a", Application - (Abstraction (Name "b", Application (Variable (Name "a"), Variable (Name "b"))), - id (Name "x"))); - Application (id (Name "x"), Application (Variable (Name "x"), Variable (Name "y"))); - Application - (Abstraction (Name "a", Abstraction (Name "b", Application (Variable (Name "a"), Variable (Name "b")))), - id (Name "x")); + 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 (Name "z"); - Application (Omega (Name "x"), Omega (Name "y")); + Omega; + Application (Omega, Omega); // Alpha conversion required Application - (Abstraction (Name "x", Abstraction (Name "y", Application (Variable (Name "x"), Variable (Name "y")))), - Variable (Name "y")); + (Abstraction (Name "x", Abstraction (Name "y", Application (var "x", var "y"))), + var "y"); Application - (Abstraction (Name "z'", Abstraction (Name "z", Application (Variable (Name "z"), Variable (Name "z'")))), - Variable (Name "z")); + (Abstraction (Name "z'", Abstraction (Name "z", Application (var "z", var "z'"))), + var "z"); Application (Abstraction (Name "x", Application - (Abstraction (Name "y", Application (Variable (Name "x"), Variable (Name "y"))), - Variable (Name "x"))), - Abstraction (Name "y", Application (Variable (Name "x"), Variable (Name "y")))); + (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 (Variable (Name "a"), Variable (Name "b"))))), - Application (Variable (Name "c"), Variable (Name "b"))); + Abstraction (Name "c", Application (var "a", var "b")))), + Application (var "c", var "b")); ] let reducedTerms = [ - Variable (Name "x"); - Application (Variable (Name "x"), Variable (Name "y")); - Abstraction (Name "x", Variable (Name "y")); - omega (Name "x"); - - Application (Variable (Name "y"), Variable (Name "y")); - Variable (Name "z"); - Application (Variable (Name "z"), Variable (Name "y")); - Variable (Name "y"); - - Abstraction (Name "a", Application (Variable (Name "x"), Variable (Name "c"))); - Application (Variable (Name "x"), omega (Name "y")); - - Application (Variable (Name "x"), Variable (Name "y")); - Variable (Name "x"); - - id (Name "y"); - Abstraction (Name "a", Application(Variable (Name "a"), id (Name "x"))); - Application (Variable (Name "x"), Variable (Name "y")); - id (Name "b"); - - Omega (Name "z"); - Application (Omega (Name "x"), Omega (Name "y")); - - Abstraction (Name "y'", Application (Variable (Name "y"), Variable (Name "y'"))); - Abstraction (Name "z''", Application (Variable (Name "z''"), Variable (Name "z"))); - Application (Variable (Name "x"), Abstraction (Name "y", Application (Variable (Name "x"), Variable (Name "y")))); - Abstraction (Name "b'", Abstraction (Name "c'", Application - (Application (Variable (Name "c"), Variable (Name "b")), - Variable (Name "b'")))); + // 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