(* Basic gates and circuits *)
(* The tagless-final style is designed around a compositional mapping of
terms of the embedded DSL to the values in some |repr| domain -- i.e.,
denotational semantics.
*)
(*
* Define the syntax of circuits (in the form close to BNF)
* Read ``repr'' as a wire
We have constant wires (grounded or connected to the power supply),
we can invert a wire, we can connect two wires to the AND
gate and get an output wire in return.
*)
module type SYM = sig
type repr
val lit : bool -> repr
val neg : repr -> repr
val (&&) : repr -> repr -> repr
val (||) : repr -> repr -> repr
end
(* NNN
Module, aka struct: a collection of type declaration and definitions
Module type, aka signature: a collection of type declarations and types of
the defined symbols
Modules have a lot in common with records or objects (sans declarations),
or namespaces
and module types -- with virtual/abstract classes
*)
(* BNF view
The signature |SYM| can be read as the context-free grammar of the language:
|repr| is the start symbol and |lit|, |neg|, etc. are the
terminals. In the conventional CFG notation it would look as:
repr -> "lit" "true" | "lit" "false"
repr -> "neg" repr
repr -> repr "&&" repr
repr -> repr "||" repr
This grammar derives, for example, |lit true && lit false|.
*)
(* OCaml programmer's view *)
(*
OCaml programmers might look at |SYM| as defining a set of OCaml
functions to construct terms of the embedded calculus. All such terms
are represented as OCaml values of the abstract type |repr|. Thus |lit true|
is the term for the literal `true' of the DSL,
and |&&| is the OCaml function that constructs the conjunction of DSL terms
received as arguments. Thus |lit true && lit false|
is the OCaml expression that evaluates to the value of the type |repr| that
represents the contradictory conjunction.
*)
(* Example
NNN module, parameterized module (functor), open, let definition
*)
module Ex1(I:SYM) = struct
open I
let wire = lit true && (neg (lit false))
end
(* without parentheses: |lit true && neg @@ lit false| *)
(*
Since we use OCaml expressions to construct DSL terms, we
follow OCaml syntactic conventions regarding fixity, parentheses,
application operation associativity and precedence,
etc. We can write this expression without
parentheses, using |@@|~-- the right-associative OCaml application operator of
low precedence~-- as |lit true && neg @@ lit false|.
*)
(* A different way of writing Ex1, that may appeal to some people
It emphasizes that modules are essentially `records'
*)
(* Treat the module SYM as if it were a record
{lit: bool -> 'a; neg: 'a -> 'a; ...}
*)
type 'a symmod = (module SYM with type repr = 'a)
let ex1 : type a. a symmod -> a = function (module I) ->
I.(&&) (I.lit true) (I.neg (I.lit false))
let ex1 : type a. a symmod -> a = function (module I) ->
I.(lit true && (neg (lit false)))
let ex1 : type a. a symmod -> a = function (module I) -> let open I in
lit true && (neg (lit false))
(* An alternative
`Object algebras' (although it was presented at SSGIP in 2010,
two years before object algebras)
class virtual ['repr] sym = object
method virtual lit : bool -> 'repr
method virtual neg : 'repr -> 'repr
method virtual an_ : 'repr -> 'repr -> 'repr
method virtual or_ : 'repr -> 'repr -> 'repr
end
*)
(* Boring: all constants.
Need some inputs. So we extend the language
*)
module type SYMW = sig
include SYM
val wire_x : repr
val wire_y : repr
val wire_z : repr
end
type 'a symwmod = (module SYMW with type repr = 'a)
(* the alternative
class virtual ['repr] symw = object
inherit ['repr] sym
method virtual wire_x : 'repr
method virtual wire_y : 'repr
method virtual wire_z : 'repr
end
*)
let ex2 : type a. a symwmod -> a = function (module I) -> let open I in
lit true && neg wire_x
(* How to get xor? Extend the language again?
This is like a _macro_ (we see later)
We will also see a simpler way of writing the code below
*)
module XOR(I:SYM) = struct
open I
let xor x y = (x || y) && (neg (x && y))
end
(* Simple adder
* (soon we could do just "let open XOR(I) in ...")
*)
let exadd2 : type a. a symwmod -> a = function (module I) ->
let module X = XOR(I) in let open X in let open I in
xor wire_x wire_y
let exadd3 : type a. a symwmod -> a = function (module I) ->
let module X = XOR(I) in let open X in let open I in
xor (xor wire_x wire_y) wire_z
let exadd_xy1 : type a. a symwmod -> a = function (module I) ->
let module X = XOR(I) in let open X in let open I in
xor wire_x (xor wire_y (lit true))
(* So far, what we wrote are phrases in our DSL: well-formed phrases
What do they mean?
*)
(* // *)
(* To understand what a phrase means we first have to figure out what
words may mean. We need to implement the |SYM| signature.
An implementation, such as
|R| below, tells what |repr| is, concretely~--
and how exactly |lit|, |neg| etc. operations construct the
|repr| values that represent the boolean literal, the negation,
etc. terms. In other words, an implementation of |SYM| tells how
to compute the meaning, or, the |repr| value, of each term from the
|repr| values of its immediate subterms. An
implementation of |SYM| thus specifies a denotational semantics
of the calculus (compositional, as it should be).
*)
(* Specifically, |R| maps SYM terms to OCaml booleans *)
module R = struct
type repr = bool
let lit x = x
let neg = not
let (&&) = Stdlib.(&&)
let (||) = Stdlib.(||)
end
(* Recall,
module Ex1(I:SYM) = struct
open I
let wire = lit true && (neg (lit false))
end
*)
(* NNN
Functor application
It doesn't have to be local, but why pollute the namespace
*)
let _ = let module M=Ex1(R) in M.wire
(* Recall,
type 'a symmod = (module SYM with type repr = 'a)
let ex1 : type a. a symmod -> a = function (module I) -> let open I in
lit true && (neg (lit false))
*)
(* NNN This is just passing to a function a record object *)
let _ = ex1(module R)
(* This is a good place to look at the alternative: the familiar,
`deep' encoding of the SYM language as an ADT
*)
type symd =
| Lit of bool
| Neg of symd
| And of symd * symd
| Or of symd * symd
let exd = Neg(And (Lit true,Neg (Lit false)))
(* See how everything is upper case? And lots of required parentheses?
In fact, to make deep encoding convenient in OCaml, one nearly
has to introduce smart constructors:
let lit x = Lit x
let (&&) x y = And(x,y)
etc
from which to tagless final is one small step. (Once smart constructors
are introduced, especially in a module, than ADT become unnecessary).
*)
(* Here is the analogue of the R interpreter *)
let rec evalR : symd -> bool = function
| Lit x -> x
| Neg e -> Stdlib.not @@ evalR e
| And (e1,e2) -> Stdlib.(evalR e1 && evalR e2)
| Or (e1,e2) -> Stdlib.(evalR e1 || evalR e2)
(* QUIZ
How come evalR is recursive (structurally inductive, to be precise),
but module R has no recursive operations?
*)
(* Extensibility
Another difference between the ADT and the tagless final encoding is
extensibility. In many languages (say, Haskell), data types are not
extensible: one cannot add a new variant later on. In OCaml, data types
are extensible. However, functions are not extensible. Even if we can
add WireX, etc, variants to something like symd (we should have defined in
differently though for it to be extensible), we can't add new clauses
to evalR. But we can very easily extend module R: see below.
*)
(* To run ex2, we need an instance of SYMW *)
(* This is a model of SYMW, with the interpretation function *)
module RW = struct
include R
let wire_x = true
let wire_y = false
let wire_z = true
end
(* What if we use a wrong interpreter
let _ = exadd2 (module R)
*)
let _ = exadd2 (module RW)
(* We can't interpret exadd2 with R but we can interpret ex1 with RW.
More bindings don't hurt *)
let _ = ex1 (module RW)
(* QUIZ
The RW module defined one particular interpretation of wire_x,
wire_y and wire_z
What if we want a different interpretation?
Discuss in OCaml or your favorite language
*)
(* This is one answer, in OCaml. Many answers exist, even in OCaml *)
let _ = exadd2 (module struct include RW let wire_x = false end)
(* abstracting wire_x value *)
let exadd2_eval' x = exadd2 (module struct include RW let wire_x = x end)
(* // *)
(* Another interpreter, to show the circuit *)
(*
|R| is but one implementation of |SYM|. Another
implementation, called |S|, maps each term to a string, the
pretty-printed representation of the term. The reader may want
to write this implementation on their own (and then compare to the one
in the accompanying code).
*)
(* Interpret |repr| as a string *)
module S0 = struct
type repr = string
let paren : string -> string = fun x -> "(" ^ x ^ ")"
let lit x = if x then "tt" else "ff"
let neg x = "~" ^ x
let (&&) x y = paren @@ x ^ " && " ^ y
let (||) x y = paren @@ x ^ " || " ^ y
end
(* Explicit signature assignment
Why we need "with type repr = string"?
Note that paren is now `hidden'
*)
module SW0 : (SYMW with type repr = string) = struct
include S0
let wire_x = "X"
let wire_y = "Y"
let wire_z = "Z"
end
let exadd2_view = exadd2 (module SW0)
let exadd3_view = exadd3 (module SW0)
(* Is it clear that xor was a macro? *)
(* QUIZ: How to avoid too many parenthesis?
Write a precedence printer
*)
(* The need for the observe function *)
(*
module S = struct
type prec = int
type repr = prec -> string
let paren = function
| true -> fun x -> "(" ^ x ^ ")"
| _ -> fun x -> x
let lit x = fun p -> if x then "tt" else "ff"
let neg x = fun p -> paren (p>10) @@ "~" ^ (x 11)
let (&&) x y = fun p -> paren (p>4) @@ x 4 ^ " && " ^ y 4
let (||) x y = fun p -> paren (p>3) @@ x 3 ^ " || " ^ y 3
let observe x = x 0
end
module SW = struct
include S
let wire_x = fun _ -> "X"
let wire_y = fun _ -> "Y"
let wire_z = fun _ -> "Z"
end
let _ = SW.observe @@ exadd2 (module SW)
*)
(* Simplification is in order! *)
(* QUIZ *)
(* write an interpreter to draw the circuit as a diagram *)
(* QUIZ *)
(* write an interpreter to compute the latency (circuit switching delay) *)