blob: 87d88597c86339ec24acc64dbe083e8e8e2e3e31 (
plain) (
blame)
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
|
module Reducer
( reduce
) where
import Helper
-- TODO: Research interaction nets and optimal reduction
-- TODO: Eta-reduction: [f 0] => f
-- (Abstraction f@_ (Bruijn 0)) = f
(<+>) :: Expression -> Int -> Expression
(<+>) (Bruijn x ) n = if x > n then Bruijn (pred x) else Bruijn x
(<+>) (Application e1 e2) n = Application (e1 <+> n) (e2 <+> n)
(<+>) (Abstraction e ) n = Abstraction $ e <+> (succ n)
(<+>) _ _ = error "invalid"
(<->) :: Expression -> Int -> Expression
(<->) (Bruijn x ) n = if x > n then Bruijn (succ x) else Bruijn x
(<->) (Application e1 e2) n = Application (e1 <-> n) (e2 <-> n)
(<->) (Abstraction e ) n = Abstraction $ e <-> (succ n)
(<->) _ _ = error "invalid"
bind :: Expression -> Expression -> Int -> Expression
bind e (Bruijn x ) n = if x == n then e else Bruijn x
bind e (Application e1 e2) n = Application (bind e e1 n) (bind e e2 n)
bind e (Abstraction exp' ) n = Abstraction (bind (e <-> (-1)) exp' (succ n))
bind _ _ _ = error "invalid"
step :: Expression -> Expression
step (Bruijn e) = Bruijn e
step (Application (Abstraction e) app) = (bind (app <-> (-1)) e 0) <+> 0
step (Application e1 e2) = Application (step e1) (step e2)
step (Abstraction e) = Abstraction (step e)
step _ = error "invalid"
reduceable :: Expression -> Bool
reduceable (Bruijn _) = False
reduceable (Variable _) = True
reduceable (Application (Abstraction _) _) = True
reduceable (Application e1 e2) = reduceable e1 || reduceable e2
reduceable (Abstraction e) = reduceable e
reduceable _ = error "invalid"
-- alpha conversion is not needed with de bruijn indexing
reduce :: Expression -> Expression
reduce = until (not . reduceable) step
|
