(* Boolean constant propagation *)
(* L
#load "basic_gates.cmo";;
*)
open Basic_gates
(* Previously we have dealt with evaluators
Can we write transformers?
*)
(* First, follow up on an earlier observation: *)
module type SYMO = sig
include SYM
type obs
val observe : repr -> obs
end
(* NNN combining two signatures, harmoniously (making them agree on repr) *)
module type SYMWO = sig
include SYMO
include SYMW with type repr := repr
end
(* In nand.ml, we already saw the distinction between the meaning of
a phrase (expression), which was a function Polarity -> string,
and the meaning for the whole program, which was string
In the classical denotational semantics, you also see the distinction
between \mathcal{E} and \mathcal{M}.
Let's extend the SYMO signature accordingly. We will soon see how
much it makes sense.
*)
(* The trivial transformer: it actually will prove useful later *)
module ID(I:SYMO) = struct
type repr = I.repr
let lit = I.lit
let neg = I.neg
let (&&) = I.(&&)
let (||) = I.(||)
let inj : I.repr -> repr = fun x -> x
let prj : repr -> I.repr = fun x -> x
type obs = I.obs
let observe = I.observe
end
(* A transformer is an interpreter (after all, writing interpreters is all
we can do in tagless-final).
It interprets SYM terms in terms of I terms (pretty much like the
NAND compiler did before.
So, a transformer of tagless-final expressions as transformer of
interpreters!
*)
(* A transformer relates two semantic domains: repr and I.repr.
We added two functions inj/prj, to also convert between the domains.
They are also commonly called inclusion/retraction,
embedding/projection or
(especially in PE literature), reflection/reification.
As the names imply, they are meant to be total, and prj . inj should
be the identity. However, generally, inj is not surjective and
prj is not injective, so inj . prj is not generally an identity.
The ID transformer is not too interesting, so we consider boolean
simplification.
*)
(* Task: propagating boolean constants
Neg True -> False, Neg False -> True
And True x -> x, And False x ->False
Or True x ->True, Or False x -> x
*)
(* // *)
(* Partial evaluation *)
(* Annotated expressions
* Now we annotate expressions with what is known about them statically
* Unk: nothing is known statically;
* Lit: statically known value
*
* inj attaches the unknown annotation and prj forgets the annotations
*)
module CP(I:SYMO) = struct
type repr = Lit of bool | Unk of I.repr
let lit : bool -> repr = fun x -> Lit x
let neg : repr -> repr = function
| Lit x -> Lit (not x)
| Unk e -> Unk (I.neg e)
let (&&) : repr -> repr -> repr = fun e1 e2 ->
match (e1,e2) with
| (Lit true,e) | (e,Lit true) -> e
| (Lit false,_) | (_,Lit false) -> Lit false
| (Unk e1, Unk e2) -> Unk I.(e1 && e2)
let (||) : repr -> repr -> repr = fun e1 e2 ->
match (e1,e2) with
| (Lit true,_) | (_,Lit true) -> Lit true
| (Lit false,e) | (e,Lit false) -> e
| (Unk e1, Unk e2) -> Unk I.(e1 || e2)
let inj : I.repr -> repr = fun x -> Unk x
let prj : repr -> I.repr = function
| Unk x -> x
| Lit x -> I.lit x
type obs = I.obs
let observe : repr -> obs = fun e -> I.observe @@ prj e
end
(* When do Unk things occur? *)
module CPW(I:SYMWO) = struct
include CP(I)
let wire_x = inj I.wire_x
let wire_y = inj I.wire_y
let wire_z = inj I.wire_z
end
(* QUIZ
We now have two algebras, I and CP(I), with inj and prj converting their
carriers.
Question: are inj and prj algebra homomorphisms?
*)
(*
inj is an algebra homomorhism: check that it preserves operations, for
example, lit false (constant) and neg (arity 1). The others are similar.
Intuitively, inj is a homomorphism because `it doesn't do anything'
OTH, prj is not a homomorphism (see for neg):
if e : CP(I).repr, then
I.neg (prj e) is not generally the same as prj (neg i)
Example: let e = Lit true and let I be S0
However, prj does become a homomorphism is we add equations (identities)
to the algebra -- which are exactly the identities that justify our
transformation!
*)
module SWO0 = struct
include SW0
type obs = string
let observe x = x
end
let _ = SWO0.observe @@ exadd_xy1(module SW0)
let _ = let module M = CPW(SWO0) in
M.observe @@ exadd_xy1(module M)
(*
Always can add no annotation (Unk), always can erase annotations
We now capture the pattern
*)