Utils Code Snippet
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
module Util = struct
type (α,β) result =
| Ok of α
| Err of β
let success : α → (α,β) result = λ x → Ok x
let failure : β → (α,β) result = λ x → Err x
let fmap : (α → β) → (α,γ) result → (β,γ) result = λ f →
function
| Ok x → Ok (f x)
| Err e → Err e
let (<$>) : (α → β) → (α,γ) result → (β,γ) result = fmap
let liftM : (α,γ) result → (α → (β,γ) result) → (β,γ) result = λ m f →
match m with
| Ok x → f x
| Err e → Err e
let (>>=) : (α,γ) result → (α → (β,γ) result) → (β,γ) result = liftM
let compose_left : (α → β) → (β → γ) → α → γ = λ f g x → g(f x)
let (>>) : (α → β) → (β → γ) → α → γ = compose_left
let safe_find : (α → bool) → α list → α option = λ f xs →
let rec aux = function
| [ ] → None
| x::xs →
if f x then
Some x
else
aux xs
in
aux xs
let string_to_chars : string → char list = λ x →
let rec aux acc = function
| 0 → acc
| i → aux (x.[i-1] :: acc) (i-1)
in aux [] (String.length x)
end
Utils Code output:
module Util :
sig
type ('a, 'b) result = Ok of 'a | Err of 'b
val success : 'a -> ('a, 'b) result
val failure : 'b -> ('a, 'b) result
val fmap : ('a -> 'b) -> ('a, 'c) result -> ('b, 'c) result
val ( <$> ) : ('a -> 'b) -> ('a, 'c) result -> ('b, 'c) result
val liftM : ('a, 'c) result -> ('a -> ('b, 'c) result) -> ('b, 'c) result
val ( >>= ) :
('a, 'c) result -> ('a -> ('b, 'c) result) -> ('b, 'c) result
val compose_left : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
val ( >> ) : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
val safe_find : ('a -> bool) -> 'a list -> 'a option
val string_to_chars : string -> char list
endLambda Calculus Code Snippet
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
module LambdaCalculus = struct
open Printf
open Util
type error =
| InvalidToken
| NoClojureParse
| InvalidParse
| UnboundVariable
| NoClojureEval
type expr =
| Var of name
| Lam of name * body
| App of expr * expr
and name = char
and body = expr
type token =
| ParLeft
| ParRight
| Lambda
| Dot
| Variable of char
type env = (char * expr) list
let alphabet =
[
'a';'b';'c';'d';'e';'f';'g';'h';'i';'j';'k';'l';'m';
'n';'o';'p';'q';'r';'s';'t';'u';'v';'w';'x';'y';'z';
]
let rec tokenize : char list → (token list,error) result = function
| [ ] → [ ] |> success
| ' ' :: xs → tokenize xs
| '(' :: xs → tokenize xs >>= λ ys → ParLeft :: ys |> success
| ')' :: xs → tokenize xs >>= λ ys → ParRight :: ys |> success
| '^' :: xs → tokenize xs >>= λ ys → Lambda :: ys |> success
| '.' :: xs → tokenize xs >>= λ ys → Dot :: ys |> success
| var :: xs →
if List.mem var alphabet
then tokenize xs >>= λ ys → Variable var :: ys |> success
else InvalidToken |> failure
let rec parse_aux : token list → (expr * token list,error) result = function
| Variable var :: xs → (Var var, xs) |> success
| Lambda :: Variable var :: Dot :: xs →
parse_aux xs >>=
λ (body,tokens) → (Lam (var,body), tokens) |> success
| ParLeft :: xs →
parse_aux xs >>=
(λ (func,ys) →
parse_aux ys >>=
(λ (value,zs) →
match zs with
| ParRight :: tokens → (App (func,value), tokens) |> success
| __________________ → NoClojureParse |> failure
)
)
| _________________________________ → InvalidParse |> failure
let parse : token list → (expr,error) result = λ xs →
fst <$> parse_aux xs
let rec eval_aux : env → expr → (env * expr,error) result = λ env →
function
| Var var →
let result =
match safe_find (λ (v,t) → var = v) env with
| Some (_,expr) → ([],expr) |> success
| None → UnboundVariable |> failure
in result
| Lam (var, body) →
(env, Lam (var, body)) |> success
| App (func, value) →
eval_aux env func >>= function
| closed_env, Lam (var, body) →
eval_aux env value >>= λ (_,eval_value) →
eval_aux ((var,eval_value) :: closed_env) body
| ___________________________ → NoClojureEval |> failure
let eval : expr → (expr,error) result = λ xs →
snd <$> eval_aux [] xs
let rec pretty_printer : expr → (string,error) result = function
| Var var →
sprintf "%c" var |> success
| Lam (var,body) →
pretty_printer body >>= λ x →
sprintf "^%c.%s" var x |> success
| App (func,value) →
pretty_printer func >>= λ x →
pretty_printer value >>= λ y →
sprintf "(%s %s)" x y |> success
let interpret : string → (string,error) result = λ x →
string_to_chars x |> success
>>= tokenize
>>= parse
>>= eval
>>= pretty_printer
end
Lambda Calculus Code output:
module LambdaCalculus :
sig
type error =
InvalidToken
| NoClojureParse
| InvalidParse
| UnboundVariable
| NoClojureEval
type expr = Var of name | Lam of name * body | App of expr * expr
and name = char
and body = expr
type token = ParLeft | ParRight | Lambda | Dot | Variable of char
type env = (char * expr) list
val alphabet : char list
val tokenize : char list -> (token list, error) Util.result
val parse_aux : token list -> (body * token list, error) Util.result
val parse : token list -> (expr, error) Util.result
val eval_aux : env -> body -> (env * expr, error) Util.result
val eval : expr -> (expr, error) Util.result
val pretty_printer : body -> (string, error) Util.result
val interpret : string -> (string, error) Util.result
endAssertions Code Snippet
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
module AssertLambdaCalculus = struct
open Util
let simple : bool =
LambdaCalculus.interpret "^x.x" =
Ok "^x.x"
let complex : bool =
LambdaCalculus.interpret "((^x.^y.x ^a.(a a)) ^b.b)" =
Ok "^a.(a a)"
(* let omega : bool =
LambdaCalculus.interpret "(^x.(x x) ^x.(x x))" =
Ok "Infinte loop, never terminates" *)
end
Assertions Code output:
module AssertLambdaCalculus :
sig
val simple : bool
val complex : bool
end
AssertLambdaCalculus.simple;;
- : bool = true
AssertLambdaCalculus.complex;;
- : bool = true