{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
-- * Double-negation elimination
module B2Neg where
import BasicGates
import Prelude hiding (and,or)
import RR
-- * Our Constant Propagator was a partial _evaluator_, a fold.
-- * Can we use the approach for something that clearly is not
-- * a fold?
-- * Here we implement double-negation elimination
-- * (in electrical sense):
-- * neg (neg e) ---> e
-- * It is a context-sensitive re-writing, and so is not a fold,
-- * on the surface of it
-- 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.
-- * //
-- Interestingly, the approach we used in partial evaluation still
-- works:
-- * Annotate! with available static knowledge
-- * Here, annotate terms with the context in which they occur
-- * Each optimization has its own term type suitable for it.
-- Unk: no annotation,
data N2N repr a where
Unk :: repr a -> N2N repr a -- no annotation
Neg :: repr Bool -> N2N repr Bool -- it is a negation
instance Symantics repr => RR N2N repr where
bwd (Unk e) = e
bwd (Neg x) = neg x
fwd = Unk
instance Symantics repr => Symantics (N2N repr) where
lit = fwd . lit
neg (Unk e) = Neg e -- we statically know we negated
neg (Neg x) = Unk x
-- and e1 e2 = Unk $ and (bwd e1) (bwd e2)
and = map2 and
or = map2 or
instance SymInput repr => SymInput (N2N repr) where
wireX = fwd wireX
wireY = fwd wireY
wireZ = fwd wireZ
-- * Observe the result
-- A type-specific version of bwd
obsN2N :: Symantics repr => N2N repr a -> repr a
obsN2N = bwd
exnn = neg . neg $ and (neg (neg wireX)) wireY
_ = view exnn
_ = view (obsN2N exnn)
_ = view (obsN2N exaddXY1)
-- * QUIZ: There is double negation, but it is not eliminated. Why?