(* Demonstrating `non-compositional', context-sensitive processing
One step of normalization: pushing negation towards literals
*)
(*
* When I first mentioned the initial and final styles in passing
* in July 2009 in Oxford, one Oxford professor said:
* ``Isn't it bloody obvious that you can't pattern-match in the final
* style?''
* The answer: it isn't bloody and it isn't obvious and it is not
* impossible to pattern-match in the final style.
*)
(* L
#load "basic_gates.cmo";;
*)
open Basic_gates;;
(* Suppose we have implemented SYM as a data type (so-called `deep embedding')
Then we can push negation down as the following transformation
*)
type symdata =
| Lit of bool
| WireX (* and there should be more... *)
| Neg of symdata
| And of symdata * symdata
| Or of symdata * symdata
(* See how everything is upper case? And lots of required parentheses? *)
let exd = Neg(And (Lit true,Neg WireX))
let rec neg_down : symdata -> symdata = function
| Neg (Lit true) -> Lit false
| Neg (Lit false) -> Lit true
| Neg (Neg x) -> neg_down x
| Neg (And (x,y)) -> Or (neg_down (Neg x), neg_down (Neg y))
| Neg (Or (x,y)) -> And (neg_down (Neg x), neg_down (Neg y))
| And (x,y) -> And (neg_down x, neg_down y)
| Or (x,y) -> Or (neg_down x, neg_down y)
| e -> e
let _ = neg_down exd
(* Nested pattern match: *context-sensitive* transformation *)
(* // *)
(*
* So, we define the context
*)
(* Tagless transformer
* We transform one interpreter into another
*)
module TNegDown(I:SYM) = struct
type ctx = Pos | Neg
type repr = ctx -> I.repr
let lit x = function
| Pos -> I.lit x
| Neg -> I.lit (not x)
let neg e = function
| Pos -> e Neg
| Neg -> e Pos
let (&&) e1 e2 = function
| Pos -> I.(e1 Pos && e2 Pos) (* homomorhism *)
| Neg -> I.(e1 Neg || e2 Neg)
let (||) e1 e2 = function
| Pos -> I.(e1 Pos || e2 Pos) (* homomorhism *)
| Neg -> I.(e1 Neg && e2 Neg)
end
(* When writing neg_down, we were thinking of the structure of the data
* When writing TNegDown, we were thinking about the meaning
* of lit, neg, etc., in each context
*)
(* QUIZ
* How to prove correctness?
*)
module TNegDownW(I:SYMW) = struct
include TNegDown(I)
let wire_x = function
| Pos -> I.wire_x
| Neg -> I.neg I.wire_x
let wire_y = function
| Pos -> I.wire_y
| Neg -> I.neg I.wire_y
let wire_z = function
| Pos -> I.wire_z
| Neg -> I.neg I.wire_z
end
let exd : type a. a symwmod -> a = function (module I) -> let open I in
neg @@ (lit true && neg wire_x)
let _ = exd(module SW0)
let _ = let module M = TNegDownW(SW0) in exd(module M)
let _ = let module M = TNegDownW(SW0) in exd (module M) M.Pos
(* The need to pass M.Pos at the end indicates that propably we need an
observation function, for the meaning of a program (as distinct from
a meaning of a (sub)expression
We should have gotten this indication already from the S interpreter
(left as en exercise)
*)
(* Spot-check test *)
let _ = exd(module RW)
let _ = let module M = TNegDownW(RW) in exd (module M) M.Pos
let exd3 : type a. a symwmod -> a = function (module I) -> let open I in
neg (exadd3 (module I))
let _ = exd3(module RW)
let _ = let module M = TNegDownW(RW) in exd3 (module M) M.Pos
let _ = exd3(module SW0)
let _ = let module M = TNegDownW(SW0) in exd3 (module M) M.Pos
;;