Skip to content

Instantly share code, notes, and snippets.

@wkwkes

wkwkes/basic_fc.ml

Last active Dec 19, 2017
Embed
What would you like to do?
ML Advend Clendar 2017
(** basic definition **)
module type ExpSYM = sig
type repr
val lit : int -> repr
val neg : repr -> repr
val add : repr -> repr -> repr
end
module ExpSYMInt : ExpSYM with type repr = int = struct
type repr = int
let lit n = n
let neg e = - e
let add e1 e2 = e1 + e2
end
module ExpSYMString : ExpSYM with type repr = string = struct
type repr = string
let lit n = string_of_int n
let neg e = "-" ^ e
let add e1 e2 = "(" ^ e1 ^ "+" ^ e2 ^ ")"
end
(* let tf1 (type a) (module S : ExpSYM with type repr = a) =
let open S in
add (lit 8) (neg (add (lit 1) (lit 2))) *)
let tf1 (type a) (module S : ExpSYM with type repr = a) =
let open S in
add (lit 8) (neg (add (lit 1) (lit 2)))
module ModuleStyle (S : ExpSYM) = struct
let tf1 = S.(add (lit 8) (neg (add (lit 1) (lit 2))))
end
let tf1_1 = let module M = ModuleStyle(ExpSYMInt) in M.tf1
let tf12 : type a. (module ExpSYM with type repr = a) -> a =
fun (module S : ExpSYM with type repr = a) ->
let open S in
add (lit 8) (neg (add (lit 1) (lit 2)))
(* utop # tf1 (module ExpSYMInt);;
- : int = 5 *)
(* utop # tf1 (module ExpSYMString);;
- : string = "(8+-(1+2))" *)
(** extension with mul **)
module type MulSYM = sig
type repr
val mul : repr -> repr -> repr
end
module MulSYMInt : MulSYM with type repr = int = struct
type repr = int
let mul e1 e2 = e1 * e2
end
module MulSYMString : MulSYM with type repr = string = struct
type repr = string
let mul e1 e2 = "(" ^ e1 ^ "*" ^ e2 ^ ")"
end
let tfm1 (type a) (module S1 : ExpSYM with type repr = a) (module S2 : MulSYM with type repr = a) =
let open S1 in
let open S2 in
add (lit 7) (neg (mul (lit 1) (lit 2)))
(* utop # tfm1 (module ExpSYMInt) (module MulSYMInt);;
- : int = 5 *)
(* utop # tfm1 (module ExpSYMString) (module MulSYMString);;
- : string = "(7+-(1*2))" *)
(** serialization **)
type tree = Leaf of string | Node of string * (tree list)
module ExpSYMTree : ExpSYM with type repr = tree = struct
type repr = tree
let lit n = Node ("Lit", [Leaf (string_of_int n)])
let neg e = Node ("Neg", [e])
let add e1 e2 = Node ("Add", [e1; e2])
end
(* utop # tf1 (module ExpSYMTree);;
- : tree =
Node ("Add",
[Node ("Lit", [Leaf "8"]);
Node ("Neg",
[Node ("Add", [Node ("Lit", [Leaf "1"]); Node ("Lit", [Leaf "2"])])])])
*)
module MulSYMTree : MulSYM with type repr = tree = struct
type repr = tree
let mul e1 e2 = Node ("Mul", [e1; e2])
end
(*
# tfm1 (module ExpSYMTree) (module MulSYMTree);;
- : tree =
Node ("Add",
[Node ("Lit", [Leaf "7"]);
Node ("Neg",
[Node ("Mul", [Node ("Lit", [Leaf "1"]); Node ("Lit", [Leaf "2"])])])])
*)
(* let safeRead s= match s with
| [(x, "")] -> Right x
| _ -> Left ("Read error: " ^ s) *)
type ctx = Pos | Neg
module ExpSYMneg (S : ExpSYM) : (ExpSYM with type repr = ctx -> S.repr) = struct
type repr = ctx -> S.repr
let lit n = function Pos -> S.lit n | Neg -> S.neg (S.lit n)
let neg e = function Pos -> e Neg | Neg -> e Pos
let add e1 e2 ctx = S.add (e1 ctx) (e2 ctx)
end
(** relation between initial and final expressions **)
type exp = Lit of int | Neg of exp | Add of exp * exp
module ExpSYMExp : ExpSYM with type repr = exp = struct
type repr = exp
let lit n = Lit n
let neg e = Neg e
let add e1 e2 = Add (e1, e2)
end
let rec finalize : type a. (module ExpSYM with type repr = a) -> exp -> a =
fun (module S : ExpSYM with type repr = a) x ->
let open S in match x with
| Lit n -> lit n
| Neg e -> neg (finalize (module S : ExpSYM with type repr = a) e)
| Add (e1, e2) -> add (finalize (module S : ExpSYM with type repr = a) e1) (finalize (module S : ExpSYM with type repr = a) e2)
(*
utop # tf1 (module ExpSYMExp) |> finalize (module ExpSYMInt);;
- : int = 5
utop # tf1 (module ExpSYMExp) |> finalize (module ExpSYMString);;
- : bytes = "(8+-(1+2))"
*)
(** basic definition **)
module type ExpSYM = sig
type repr
val lit : int -> repr
val neg : repr -> repr
val add : repr -> repr -> repr
end
implicit module ExpSYMInt : ExpSYM with type repr = int = struct
type repr = int
let lit n = n
let neg e = - e
let add e1 e2 = e1 + e2
end
implicit module ExpSYMString : ExpSYM with type repr = string = struct
type repr = string
let lit n = string_of_int n
let neg e = "-" ^ e
let add e1 e2 = "(" ^ e1 ^ "+" ^ e2 ^ ")"
end
let eval : int -> int = fun x -> x
let show : string -> string = fun x -> x
let tf1 {S : ExpSYM} ctx =
let open S in
add (lit 8) (neg (add (lit 1) (lit 2)))
|> ctx
(*
# tf1 eval;;
- : int = 5
# tf1 show;;
- : string = "(8+-(1+2))"
*)
(** extension with mul **)
module type MulSYM = sig
type repr
val mul : repr -> repr -> repr
end
implicit module MulSYMInt : MulSYM with type repr = int = struct
type repr = int
let mul e1 e2 = e1 * e2
end
implicit module MulSYMString : MulSYM with type repr = string = struct
type repr = string
let mul e1 e2 = "(" ^ e1 ^ "*" ^ e2 ^ ")"
end
let tfm1 (type a) {S1 : ExpSYM with type repr = a} {S2 : MulSYM with type repr = a} (ctx : a -> a) =
let open S1 in
let open S2 in
add (lit 7) (neg (mul (lit 1) (lit 2)))
|> ctx
(*
# tfm1 eval;;
- : int = 5
# tfm1 show;;
- : string = "(7+-(1*2))"
*)
(** serialization **)
type tree = Leaf of string | Node of string * (tree list)
implicit module ExpSYMTree : ExpSYM with type repr = tree = struct
type repr = tree
let lit n = Node ("Lit", [Leaf (string_of_int n)])
let neg e = Node ("Neg", [e])
let add e1 e2 = Node ("Add", [e1; e2])
end
let toTree : tree -> tree = fun x -> x
(*
# tf1 toTree;;
- : tree =
Node ("Add",
[Node ("Lit", [Leaf "8"]);
Node ("Neg",
[Node ("Add", [Node ("Lit", [Leaf "1"]); Node ("Lit", [Leaf "2"])])])
*)
implicit module MulSYMTree : MulSYM with type repr = tree = struct
type repr = tree
let mul e1 e2 = Node ("Mul", [e1; e2])
end
(*
# tfm1 toTree;;
- : tree =
Node ("Add",
[Node ("Lit", [Leaf "7"]);
Node ("Neg",
[Node ("Mul", [Node ("Lit", [Leaf "1"]); Node ("Lit", [Leaf "2"])])])])
*)
(** pattern-matching **)
type ctx = Pos | Neg
implicit module ExpSYMneg {S : ExpSYM} : (ExpSYM with type repr = ctx -> S.repr) = struct
type repr = ctx -> S.repr
let lit n = function Pos -> S.lit n | Neg -> S.neg (S.lit n)
let neg e = function Pos -> e Neg | Neg -> e Pos
let add e1 e2 ctx = S.add (e1 ctx) (e2 ctx)
end
let push_neg (type a) (f : a -> a) : (ctx -> a) -> (ctx -> a) = fun e -> e
(*
# tf1 (push_neg eval) Pos;;
- : int = 5
# tf1 (push_neg show) Pos;;
- : string = "(8+(-1+-2))"
*)
implicit module MulSYMneg {S : MulSYM} : (MulSYM with type repr = ctx -> S.repr) = struct
type repr = ctx -> S.repr
let mul e1 e2 ctx = S.mul (e1 ctx) (e2 ctx)
end
(*
# tfm1 (push_neg show) Pos;;
- : string = "(7+(-1*-2))"
# tfm1 (push_neg eval) Pos;;a
- : int = 9
*)
(** relation **)
type exp = Lit of int | Neg of exp | Add of exp * exp
implicit module ExpSYMExp : ExpSYM with type repr = exp = struct
type repr = exp
let lit n = Lit n
let neg e = Neg e
let add e1 e2 = Add (e1, e2)
end
let initialize : exp -> exp = fun e -> e
let rec finalize : type a. {S : ExpSYM with type repr = a} -> exp -> a =
fun {S : ExpSYM with type repr = a} x ->
let open S in match x with
| Lit n -> lit n
| Neg e -> neg (finalize e)
| Add (e1, e2) -> add (finalize e1) (finalize e2)
let finalize : type a. {S : ExpSYM with type repr = a} -> (a -> a) -> exp -> a = fun {S : ExpSYM with type repr = a} f x ->
let rec aux : type a. {S : ExpSYM with type repr = a} -> exp -> a =
fun {S : ExpSYM with type repr = a} x ->
let open S in match x with
| Lit n -> lit n
| Neg e -> neg (aux e)
| Add (e1, e2) -> add (aux e1) (aux e2) in
aux x |> f
(*
# tf1 initialize;;
- : exp = Add (Lit 8, Neg (Add (Lit 1, Lit 2)))
*)
(*
# tf1 initialize |> (finalize eval);;
- : int = 5
# tf1 initialize |> (finalize show);;
- : string = "(8+-(1+2))"
# tf1 initialize |> (finalize toTree);;
- : tree =
Node ("Add",
[Node ("Lit", [Leaf "8"]);
Node ("Neg",
[Node ("Add", [Node ("Lit", [Leaf "1"]); Node ("Lit", [Leaf "2"])])])])
*)
(** tagless final with hoas **)
module type Symantics = sig
type 'a repr
val int : int -> int repr
val add : int repr -> int repr -> int repr
val lam : ('a repr -> 'b repr) -> ('a -> 'b) repr
val app : ('a -> 'b) repr -> 'a repr -> 'b repr
end
type 'a r = R of 'a
let unR = function R x -> x
implicit module SymanticR : Symantics with type 'a repr = 'a r = struct
type 'a repr = 'a r
let int x = R x
let add e1 e2 = R (unR e1 + unR e2)
let lam f = R (fun x -> R x |> f |> unR)
let app e1 e2 = R (unR e1 (unR e2))
end
(* type varCounter = int *)
(* type 'a s = S of (varCounter -> string) *)
type 'a s = S of (int -> string)
let unS = function S x -> x
implicit module SymanticS : Symantics with type 'a repr = 'a s = struct
type 'a repr = 'a s
let int x = S (fun _ -> string_of_int x)
let add e1 e2 = S (fun h -> "(" ^ unS e1 h ^ "+" ^ unS e2 h ^ ")")
let lam e = S (fun h -> let x = "x" ^ string_of_int h in
"("^x^" -> "^ (unS (e (S (fun _ ->x)))) (h+1) ^")")
let app e1 e2 = S (fun h -> "(" ^ unS e1 h ^ " " ^ unS e2 h ^ ")")
end
let th1 {M : Symantics} f =
M.(app (lam (fun x -> add x x)) (int 21)) |> f
let eval = unR
let show x = unS x 0
(*
# th1 eval;;
- : int = 42
# th1 show;;
- : string = "((x0 -> (x0+x0)) 21)"
*)
(** tagless final **)
module type Symantics = sig
type ('a, 'b) repr
val int : int -> ('h, int) repr
val add : ('h, int) repr -> ('h, int) repr -> ('h, int) repr
val z : (('a * 'h), 'a) repr
val s : ('h, 'a) repr -> ('any * 'h, 'a) repr
val lam : ('a * 'h, 'b) repr -> ('h, 'a -> 'b) repr
val app : ('h, 'a -> 'b) repr -> ('h, 'a) repr -> ('h, 'b) repr
end
type ('h, 'a) r = R of ('h -> 'a)
let unR = function R f -> f
implicit module SymanticsR : Symantics with type ('a, 'b) repr = ('a, 'b) r = struct
type ('a, 'b) repr = ('a, 'b) r
let int x = R (fun _ -> x)
let add e1 e2 = R (fun h -> unR e1 h + unR e2 h)
let z = R (fun (x, _) -> x)
let s v = R (fun (_, h) -> unR v h)
let lam e = R (fun h x -> unR e (x, h))
let app e1 e2 = R (fun h -> (unR e1 h) (unR e2 h))
end
type ('h, 'a) s = S of (int -> string)
let unS = function S f -> f
implicit module SymanticsS : Symantics with type ('a, 'b) repr = ('a, 'b) s = struct
type ('a, 'b) repr = ('a, 'b) s
let int x = S (fun _ -> string_of_int x)
let add e1 e2 = S (fun h -> "(" ^ unS e1 h ^ "+" ^ unS e2 h ^ ")")
let z = S (fun h -> "x" ^ string_of_int (h-1))
let s v = S (fun h -> unS v (h-1))
let lam e = S (fun h ->
let x = "x" ^ string_of_int h in
"(\\" ^ x ^ " -> " ^ unS e (h+1) ^ ")")
let app e1 e2 = S (fun h -> "(" ^ unS e1 h ^ " " ^ unS e2 h ^ ")")
end
let th1 {M : Symantics} f =
M.(app (lam (add z z)) (int 21)) |> f
let eval x = unR x ()
let show x = unS x 0
(*
# th1 eval;;
- : int = 42
# th1 show;;
- : string = "((\\x0 -> (x0+x0)) 21)"
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment