Created
May 14, 2021 15:54
-
-
Save pema99/d17ece0d58663765f1c46550f5a8a21a to your computer and use it in GitHub Desktop.
Lambda calculus parsing and reduction - Using my own parsing combinator lib
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module LambdaCalc | |
open Combinator | |
open Common | |
open Util | |
// Lambda calc AST | |
type Expr = | |
| Id of string | |
| Abs of string * Expr | |
| App of Expr * Expr | |
let rec prettyPrint expr = | |
match expr with | |
| Id id -> sprintf "%s" id | |
| Abs (id, e) -> sprintf "(\\%s. %s)" id (prettyPrint e) | |
| App (l, r) -> sprintf "%s %s" (prettyPrint l) (prettyPrint r) | |
// Parsing | |
let whitespace = | |
many (oneOf [' '; '\r'; '\n'; '\t']) *> just () | |
let isAlpha c = | |
(c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') | |
let isAlphaNumeric c = | |
isAlpha c || (c >= '0' && c <= '9') | |
let identP = | |
whitespace *> | |
(eatWhile1 isAlphaNumeric |>> List.toArray |>> System.String) | |
<* whitespace | |
let exprP, exprPImpl = declParser() | |
let varP = | |
identP |>> Id | |
let sigP = | |
whitespace *> (one '\\' *> identP <* one '.') <* whitespace | |
let absP = | |
(sigP <+> exprP) |>> Abs | |
let nonAppP = | |
between (one '(') exprP (one ')') | |
<|> absP | |
<|> varP | |
exprPImpl := | |
whitespace *> | |
(chainL1 (whitespace *> nonAppP) (just (curry App))) | |
<* whitespace | |
// Reduction | |
let rec freeVars expr = | |
match expr with | |
| Id id -> [ id ] | |
| Abs (x, t) -> List.filter ((<>) x) (freeVars t) | |
| App (t, s) -> freeVars t @ freeVars s | |
let rec subst expr x r = | |
match expr with | |
| Id _ -> | |
if expr = x then r | |
else expr | |
| App (t, s) -> | |
App (subst t x r, subst s x r) | |
| Abs (id, t) -> | |
let stale = List.exists ((=) id) (freeVars r) | |
if Id id = x || stale then expr | |
else Abs (id, subst t x r) | |
let rec beta expr = | |
match expr with | |
| App (Abs (x, t), s) -> subst t (Id x) s | |
| App (t, s) -> App (beta t, beta s) | |
| Abs (x, t) -> Abs (x, beta t) | |
| a -> a | |
let rec reduce expr = | |
let redex = beta expr | |
if redex = expr then redex | |
else reduce redex | |
// CLI | |
while true do | |
printf "Input expression: " | |
let dataSrc = mkMultiLineParser (System.Console.ReadLine()) | |
let result, state = exprP dataSrc | |
let expr = | |
match result with | |
| Success v -> v | |
| _ -> failwith (sprintf "Parsing failure. State: %A" state) | |
printfn "Reduced: %s" (prettyPrint (reduce expr)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment