{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
-- * Demonstrating `non-compositional', context-sensitive processing
-- * The final style
-- * Flatten the additions
module FlatF where
import Intro2 hiding (main)
import PushNegF as Neg hiding (main,Ctx)
-- We are going to write flata as an interpreter.
-- After all, that's all we can do with an expression in a final form.
-- * The nested pattern-matching establishes a context:
-- * flata :: Exp -> Exp
-- * flata e@Lit{} = e
-- * flata e@Neg{} = e
-- * flata (Add (Add e1 e2) e3) = flata (Add e1 (Add e2 e3))
-- * flata (Add e1 e2) = Add e1 (flata e2)
-- The processing is slightly different from push_neg, because we repeatedly
-- process the transformed expression (the last-but one clause)
-- The nested pattern-match again betrays the context-sensitivity.
-- The context in question is expression being the left child of addition.
-- * //
-- So, we define the context
-- (LCA e) means that the context (Add [] e), being the left immediate
-- child of addition whose right child is e. NonLCA is any other context.
data Ctx e = LCA e | NonLCA
-- On other words, LCA e3 represents the context of adding e3 _to the right_ of
-- the expression in focus.
instance ExpSYM repr => ExpSYM (Ctx repr -> repr) where
lit n NonLCA = lit n
lit n (LCA e) = add (lit n) e
neg e NonLCA = neg (e NonLCA)
neg e (LCA e3) = add (neg (e NonLCA)) e3 -- assume only lits are negated
add e1 e2 ctx = e1 (LCA (e2 ctx))
-- The last clause expresses the reassociation-to-the-right
-- * C[Add e1 e2] -> Add e1 C[e2]
-- Recall that after the negations are pushed down, expressions are
-- described by the following grammar
-- * e ::= factor | add e e
-- * factor ::= int | neg int
-- That is, C ::= [] | Add [] e
-- Keep in mind the processing is done bottom-up!
-- A general approach is to use continuations (or monads),
-- or to encode the Ctx with zippers
-- (the defunctionalized continuations, in the present
-- case).
-- The Ctx data type above is tuned to the present example,
-- keeping only the data we need (e.g., we aren't interested
-- in the context of Neg or of the addition on the left,
-- and so we don't represent these cases in Ctx).
-- Exercise: there are several clauses where lit, neg, or add
-- appears on both sides of the definition.
-- In which clause add is being used recursively?
-- The `interpreter' for flattening
flata :: (Ctx repr -> repr) -> repr
flata e = e NonLCA
norm = flata . Neg.push_neg
-- Use our sample term
-- We make it a bit complex
tf3 = (add tf1 (neg (neg tf1)))
tf3_view = view tf3
-- "((8 + (-(1 + 2))) + (-(-(8 + (-(1 + 2))))))"
tf3_eval = eval tf3
-- 10
-- The normalized expression can be evaluated with any interpreter
tf3_norm = norm tf3
tf3_norm_view = view tf3_norm
-- "(8 + ((-1) + ((-2) + (8 + ((-1) + (-2))))))"
-- The result of the standard evaluation (the `meaning') is preserved
tf3_norm_eval = eval tf3_norm
-- 10
tf4 = add t (neg t) where t = (add (add (lit 1) (lit 2)) (lit 3))
tf4_view = view tf4
-- "(((1 + 2) + 3) + (-((1 + 2) + 3)))"
tf4_eval = eval tf4
-- 0
tf4_norm = norm tf4
tf4_norm_view = view tf4_norm
-- "(1 + (2 + (3 + ((-1) + ((-2) + (-3))))))"
-- The result of the standard evaluation (the `meaning') is preserved
tf4_norm_eval = eval tf4_norm
-- 0
main = do
print tf3_view
print tf3_eval
print tf3_norm_view
print tf3_norm_eval
if tf3_eval == tf3_norm_eval then return ()
else error "Normalization"
-- normalizing a normal form does not change it
if (view . norm $ tf3_norm) == tf3_norm_view then return ()
else error "Normalization"
print tf4_view
print tf4_eval
print tf4_norm_view
print tf4_norm_eval
if tf4_eval == tf4_norm_eval then return ()
else error "Normalization"
if (view . norm $ tf4_norm) == tf4_norm_view then return ()
else error "Normalization"