219 lines
6.1 KiB
OCaml
219 lines
6.1 KiB
OCaml
(* https://github.com/kayceesrk/cs3100_f19/blob/cc71e59a081543257adc72a2428685e891bcd307/assignments/assignment1.ipynb *)
|
|
|
|
(* cond_dup: 'a list -> ('a -> bool) -> 'a list *)
|
|
let cond_dup l f =
|
|
List.fold_right
|
|
(fun a acc ->
|
|
(if f a then a :: a :: acc
|
|
else a :: acc))
|
|
l []
|
|
(* # cond_dup [3;4;5] (fun x -> x mod 2 = 1);; *)
|
|
(* - : int list = [3; 3; 4; 5; 5] *)
|
|
|
|
let rec n_times (f, n, v) =
|
|
if n <= 0 then v
|
|
else n_times (f, n-1, f v)
|
|
(* # n_times((fun x-> x+1), 50, 0);; *)
|
|
(* - : int = 50 *)
|
|
|
|
let rec range start stop =
|
|
if stop - start >= 0 then start :: (range (start+1) stop)
|
|
else []
|
|
(* # range 2 5;; *)
|
|
(* - : int list = [2; 3; 4; 5] *)
|
|
|
|
let rec zipwith f a b =
|
|
match a, b with
|
|
| [], _
|
|
| _, [] -> []
|
|
| a'::aa, b'::bb -> (f a' b') :: (zipWith f aa bb)
|
|
(* # zipwith (+) [1;2;3] [4;5];; *)
|
|
(* - : int list = [5; 7] *)
|
|
|
|
(* let rec flatten l = *)
|
|
(* match l with *)
|
|
(* | [] -> [] *)
|
|
(* | l :: ls -> l @ (flatten ls) *)
|
|
let rec flatten = function
|
|
| [] -> []
|
|
| l :: ls -> l @ (flatten ls)
|
|
(* # flatten ([[1;2];[3;4]]);; *)
|
|
(* - : int list = [1; 2; 3; 4] *)
|
|
|
|
let remove_stutter l = snd (List.fold_right
|
|
(fun x (prev, res) ->
|
|
match prev with
|
|
| None -> (Some x, x::res)
|
|
| Some prev' ->
|
|
if x=prev' then (prev, res)
|
|
else (Some x, x::res))
|
|
l (None, []))
|
|
(* # remove_stutter [1;2;2;3;1;1;1;4;4;2;2];; *)
|
|
(* - : int list = [1; 2; 3; 1; 4; 2] *)
|
|
|
|
|
|
(*********************************************************************)
|
|
|
|
|
|
(* https://github.com/kayceesrk/cs3100_f19/blob/cc71e59a081543257adc72a2428685e891bcd307/assignments/assignment2.zip *)
|
|
|
|
type expr
|
|
= Var of string
|
|
| App of expr * expr
|
|
| Lam of string * expr
|
|
|
|
(* prettify: expr -> string *)
|
|
let rec prettify e =
|
|
match e with
|
|
| Var v -> v
|
|
| App (e1, e2) -> "(" ^ (prettify e1) ^ " " ^ (prettify e2) ^ ")"
|
|
| Lam (v, e') -> "λ" ^ v ^ "." ^ (prettify e')
|
|
|
|
let mem v vars = List.exists (fun x -> x=v) vars
|
|
|
|
(* # mem "b" ["a";"b";"c"];; *)
|
|
(* - : bool = true *)
|
|
(* *)
|
|
(* # mem "x" ["a";"b";"c"];; *)
|
|
(* - : bool = false *)
|
|
|
|
let remove v vars = List.filter (fun x -> not (v=x)) vars
|
|
|
|
(* # remove "b" ["a";"b";"c"];; *)
|
|
(* - : string list = ["a"; "c"] *)
|
|
(* *)
|
|
(* # remove "x" ["a";"b";"c"];; *)
|
|
(* - : string list = ["a"; "b"; "c"] *)
|
|
|
|
(* union: string list -> string list -> string list *)
|
|
let union s1 s2 =
|
|
remove_stutter (List.sort String.compare (s1 @ s2))
|
|
|
|
(* # union ["a"; "c"; "b"] ["d"; "b"; "x"; "a"];; *)
|
|
(* - : String.t list = ["a"; "b"; "c"; "d"; "x"] *)
|
|
|
|
let add a l =
|
|
let l' =
|
|
(if List.exists (fun x -> x=a) l then l
|
|
else a::l) in
|
|
List.sort
|
|
(fun x y ->
|
|
if x < y then -1
|
|
else if x = y then 0
|
|
else 1) l'
|
|
|
|
(* # add "b" ["a";"c"];; *)
|
|
(* - : string list = ["a"; "b"; "c"] *)
|
|
(* *)
|
|
(* # add "a" ["c"; "a"];; *)
|
|
(* - : string list = ["a"; "c"] *)
|
|
|
|
let varcount = ref 0
|
|
let fresh s =
|
|
let v = !varcount in
|
|
s ^ (string_of_int v)
|
|
|
|
(* free_variables: expr -> string list *)
|
|
let rec free_variables = function
|
|
| Var v -> [v]
|
|
| App (e1, e2) ->
|
|
let fv1 = free_variables e1 in
|
|
let fv2 = free_variables e2 in
|
|
union fv1 fv2
|
|
| Lam (v, e') ->
|
|
let fv = free_variables e' in
|
|
remove v fv
|
|
|
|
(* # free_variables (Lam ("x", Var "x"));; *)
|
|
(* - : String.t list = [] *)
|
|
(* *)
|
|
(* # free_variables (Lam ("x", Var "y"));; *)
|
|
(* - : String.t list = ["y"] *)
|
|
|
|
(* substitute : expr -> string -> expr -> expr *)
|
|
(* substitute e1 var e2 means e1[e2/var] *)
|
|
let rec substitute e var repl =
|
|
match e with
|
|
| Var v -> repl
|
|
| App (e1, e2) -> App (substitute e1 var repl, substitute e2 var repl)
|
|
| Lam (v, body) ->
|
|
if v=var then
|
|
(* A bound variable. Can be interfered with only on a beta-reduction *)
|
|
e
|
|
else
|
|
let v' =
|
|
(* Avoid free variable capture *)
|
|
if mem v (free_variables repl) then fresh v
|
|
else v in
|
|
let body' = substitute body var repl in
|
|
Lam (v', body')
|
|
|
|
(* (λy.x)[(λz.z w)/x] is (λy.λz.z w) *)
|
|
(* # substitute (Lam ("y", Var "x")) "x" (Lam ("z", App (Var "z", (Var "w"))));; *)
|
|
(* - : expr = Lam ("y", Lam ("z", App (Var "z", Var "w"))) *)
|
|
(* *)
|
|
(* (λx.x)[y/x] is (λx.x) *)
|
|
(* # substitute (Lam ("x", Var "x")) "x" (Var "y");; *)
|
|
(* - : expr = Lam ("x", Var "x") *)
|
|
(* *)
|
|
(* (λx.y)[x/y] is (λx0. x) *)
|
|
(* # substitute (Lam ("x", Var "y")) "y" (Var "x");; *)
|
|
(* - : expr = Lam ("x0", Var "x") *)
|
|
|
|
|
|
(* reduce_cbv : expr -> expr * bool *)
|
|
let reduce_cbv e =
|
|
match e with
|
|
| App (e1, e2) ->
|
|
(match e1 with
|
|
| Lam (v, e') -> (substitute e' v e2, true)
|
|
| _ ->
|
|
(* Still got space to reduce *)
|
|
let (e1', flag) = reduce_cbv e1 in
|
|
(App (e1', e2), flag))
|
|
| _ -> (e, false)
|
|
|
|
(* # let e, flag = *)
|
|
(* reduce_cbv ( *)
|
|
(* App ( *)
|
|
(* App ( *)
|
|
(* Lam ("x", Var "x"), *)
|
|
(* Lam ("x", Var "x")), *)
|
|
(* Lam ("z", *)
|
|
(* App (Lam ("x", Var "x"), *)
|
|
(* Var "z")))) in (prettify e, flag);; *)
|
|
(* - : string * bool = ("(λx.x λz.(λx.x z))", true) *)
|
|
|
|
(* prettify ( *)
|
|
(* App ( *)
|
|
(* Lam ("x", Var "x), *)
|
|
(* Lam ("z", *)
|
|
(* App ( *)
|
|
(* Lam ("x", Var "x), *)
|
|
(* Var "z")))) *)
|
|
|
|
(* App (Lam ("z", *)
|
|
(* Lam ("x", Var "x")), *)
|
|
(* Var "z" *)
|
|
|
|
(* let expr, reduced = reduce_cbv (parse_string "(λx.x) (λz.(λx.x) z)") in *)
|
|
(* assert (reduced = true && *)
|
|
(* alpha_equiv expr (parse_string "λz.(λx.x) z")); *)
|
|
|
|
(* let expr, reduced = reduce_cbv (parse_string "λz.(λx.x) z") in *)
|
|
(* assert (reduced = false && *)
|
|
(* alpha_equiv expr (parse_string "λz.(λx.x) z")); *)
|
|
|
|
(* let expr, reduced = reduce_cbv (parse_string "(λx.y) ((λx.x x) (λx.x x))") in *)
|
|
(* assert (reduced = true && *)
|
|
(* alpha_equiv expr (parse_string "(λx.y) ((λx.x x) (λx.x x))")); *)
|
|
|
|
(* let expr, reduced = reduce_cbv (parse_string "x y z") in *)
|
|
(* assert (reduced = false && *)
|
|
(* alpha_equiv expr (parse_string "x y z")) *)
|
|
|
|
let rec reduce_normal e =
|
|
let e', flag = reduce_cbv e in
|
|
if flag then reduce_normal e'
|
|
else e'
|