-
Notifications
You must be signed in to change notification settings - Fork 4
/
Copy pathPushNegFI.hs
88 lines (67 loc) · 2.45 KB
/
PushNegFI.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
{-# LANGUAGE NoMonomorphismRestriction #-}
-- * Demonstrating `non-compositional', context-sensitive processing
-- * The final style, via the intermediate data type.
-- This is cheating. But it does show the relationship between
-- initial and final. It also points out that everything we can
-- do with the data type, we can do in the final approach too -- albeit
-- with cheating in this case
module PushNegFI where
-- Explain the imports:
import Intro2 hiding (main) -- The final representation of Exp
import Intro1 (Exp(..)) -- import the Exp data type
import qualified PushNegI as I -- use the initial push_neg as it was
-- * //
-- We write the interpreter for final terms that produce initial, data type
-- terms
instance ExpSYM Exp where
lit = Lit -- nice symmetry between upper-and
neg = Neg -- lower case
add = Add
initialize :: Exp -> Exp
initialize = id
-- * //
-- We write an evaluator for data type that produces final representation
-- The analogy with fold must be patent.
finalize :: ExpSYM repr => Exp -> repr -- could have been inferred
finalize (Lit n) = lit n
finalize (Neg e) = neg (finalize e)
finalize (Add e1 e2) = add (finalize e1) (finalize e2)
-- * //
-- Now, push_neg in the final style is a mere composition
push_neg = finalize . I.push_neg . initialize
-- * Deforestation? Fusion laws?
-- Open research question: can the intermediate Exp data type be removed
-- by deforestation? Can we propose fusion laws to eliminate Exp?
-- * //
-- To remind, here is our sample term
tf1_view = view tf1
-- "(8 + (-(1 + 2)))"
tf1_norm = push_neg tf1
-- The new expression can be evaluated with any interpreter
tf1_norm_view = view tf1_norm
-- "(8 + ((-1) + (-2)))"
-- The result of the standard evaluation (the `meaning') is preserved
tf1_norm_eval = eval tf1_norm
-- 5
-- Add an extra negation
tf1n_norm = push_neg (neg tf1)
-- see the result
tf1n_norm_view = view tf1n_norm
-- "((-8) + (1 + 2))"
tf1n_norm_eval = eval tf1n_norm
-- -5
-- Negate the already negated term
tf1nn_norm = push_neg (neg tf1n_norm)
tf1nn_norm_view = view tf1nn_norm
-- "(8 + ((-1) + (-2)))"
main = do
print PushNegFI.tf1_view
print tf1_norm_view
print tf1n_norm_view
if tf1_norm_view == tf1nn_norm_view then return ()
else error "Double neg"
print tf1nn_norm_view
if eval tf1 == tf1_norm_eval then return ()
else error "Normalization"
if eval tf1 == - tf1n_norm_eval then return ()
else error "Normalization"