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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
{-# LANGUAGE LambdaCase #-}
module Minilang.Lambda.DeBruijn where
import Data.List (elemIndex)
import qualified Data.Map.Strict as Map
import Data.Text (Text)
import qualified Data.Text
import Minilang.Lambda.Eval (Term)
import qualified Minilang.Lambda.Eval as Eval
data DeBruijn ann
= FV Text
| FNum Int
| FBuiltin Text -- ^ a fully-applied or partial built-in operator
| Var ann Int
| Lam ann (DeBruijn ann)
| App (DeBruijn ann) (DeBruijn ann)
deriving (Show, Read, Eq)
type Env ann = [(Text, DeBruijn ann)]
newEnv :: Env ann
newEnv = []
-- | An environment pre-seeded with every built-in operator name.
-- Each entry maps the name to an 'FBuiltin' node so that 'eval\'' can
-- recognise and reduce applications of those names.
builtinDeBruijnEnv :: Env ann
builtinDeBruijnEnv =
map (\name -> (name, FBuiltin name)) (Map.keys Eval.builtinArity)
fromDeBruijn :: DeBruijn Text -> Term
fromDeBruijn = \case
FV x -> Eval.Var x
FNum n -> Eval.Num n
FBuiltin b -> Eval.Var b -- reads back as a Var; eval recognises it
Var s _ -> Eval.Var s
Lam s body -> Eval.Lam s (fromDeBruijn body)
App f a -> Eval.App (fromDeBruijn f) (fromDeBruijn a)
-- Convert a term with named variables to De Bruijn indices
toDeBruijn :: Term -> DeBruijn Text
toDeBruijn term = go term []
where
go (Eval.Var x) env =
case elemIndex x env of
Just idx -> Var x idx
Nothing -> FV x
go (Eval.Lam x body) env =
Lam x (go body (x : env))
go (Eval.App f a) env =
App (go f env) (go a env)
go (Eval.Num n) _env =
FNum n
eval :: DeBruijn ann -> DeBruijn ann
eval (App f a) =
case eval f of
Lam _ body -> eval (substitute [] 0 a body)
f' -> App f' a
eval term = term
eval' :: Env Text -> DeBruijn Text -> DeBruijn Text
eval' env = \case
FV v -> case lookup v env of
Just term -> term
Nothing -> FV v
FBuiltin b -> FBuiltin b
App f a ->
let f' = eval' env f
a' = eval' env a
in case f' of
-- Beta-reduction
Lam _ body -> eval' env (substitute env 0 a' body)
-- Built-in: collect arguments and reduce when saturated
FBuiltin b -> evalBuiltin env b [a']
-- Left-spine is itself a partial builtin application
App g arg ->
case collectBuiltin (App g arg) of
Just (b, accumulated) -> evalBuiltin env b (accumulated ++ [a'])
Nothing ->
let applied = App f' a'
in if applied /= App f a
then eval' env applied
else applied
f'' ->
let applied = App f'' a'
in if applied /= App f a
then eval' env applied
else applied
term -> term
-- | Walk a left-spine of 'App' nodes and check whether the root is an
-- 'FBuiltin'. If so, return the builtin name and the already-accumulated
-- arguments (left-to-right order).
collectBuiltin :: DeBruijn Text -> Maybe (Text, [DeBruijn Text])
collectBuiltin = go []
where
go acc (App f arg) = go (arg : acc) f
go acc (FBuiltin b) = Just (b, acc)
go _ _ = Nothing
-- | Attempt to reduce a built-in application once all required arguments
-- are present. Falls back to a neutral 'App' spine when the arity has not
-- been reached yet or when the arguments are not integer literals.
evalBuiltin :: Env Text -> Text -> [DeBruijn Text] -> DeBruijn Text
evalBuiltin env b args =
case Map.lookup b Eval.builtinArity of
Nothing -> rebuild (FBuiltin b) args -- unknown builtin; leave as-is
Just ar
| length args < ar ->
-- Still partial: return the spine as-is for now
rebuild (FBuiltin b) args
| length args == ar ->
case tryReduce b args of
Just result -> result
Nothing -> rebuild (FBuiltin b) args
| otherwise ->
-- Over-applied: reduce with exactly `ar` args then apply the rest
let (sat, extra) = splitAt ar args
in case tryReduce b sat of
Just reduced -> foldl (\acc x -> eval' env (App acc x)) reduced extra
Nothing -> rebuild (FBuiltin b) args
-- | Church-encoded True as a DeBruijn term: lam f -> lam t -> t
churchTrue :: DeBruijn Text
churchTrue = Lam "f" (Lam "t" (Var "t" 0))
-- | Church-encoded False as a DeBruijn term: lam f -> lam t -> f
churchFalse :: DeBruijn Text
churchFalse = Lam "f" (Lam "t" (Var "f" 1))
-- | Attempt a numeric reduction. Returns 'Nothing' when either argument is
-- not an 'FNum' (e.g. it is still a free variable).
-- Comparison operators return Church booleans rather than integer flags.
tryReduce :: Text -> [DeBruijn Text] -> Maybe (DeBruijn Text)
tryReduce name args = case (name, args) of
("+", [FNum x, FNum y]) -> Just $ FNum (x + y)
("-", [FNum x, FNum y]) -> Just $ FNum (x - y)
("*", [FNum x, FNum y]) -> Just $ FNum (x * y)
("div", [FNum x, FNum y]) | y /= 0 -> Just $ FNum (x `div` y)
("mod", [FNum x, FNum y]) | y /= 0 -> Just $ FNum (x `mod` y)
("=", [FNum x, FNum y]) -> Just $ if x == y then churchTrue else churchFalse
("<", [FNum x, FNum y]) -> Just $ if x < y then churchTrue else churchFalse
("neg", [FNum x]) -> Just $ FNum (negate x)
_ -> Nothing
-- | Rebuild a left-spine application from a head and a list of arguments.
rebuild :: DeBruijn Text -> [DeBruijn Text] -> DeBruijn Text
rebuild = foldl App
substitute :: Env ann -> Int -> DeBruijn ann -> DeBruijn ann -> DeBruijn ann
substitute env n arg term = case term of
FV x -> case lookup x env of
Just t -> t
Nothing -> FV x
FNum _ -> term
FBuiltin _ -> term
Var t x
| x == n -> arg
| otherwise -> Var t x
Lam x body -> Lam x (substitute env (n + 1) arg body)
App f a -> App (substitute env n arg f) (substitute env n arg a)
pretty :: DeBruijn Text -> Text
pretty = \case
FV x -> x
FNum n -> showNum n
FBuiltin b -> b
Var s _ -> s
Lam s body -> "(lam (" <> s <> ") " <> pretty body <> ")"
App f a -> "(" <> pretty f <> " " <> pretty a <> ")"
-- | Render an integer, using no space between '-' and digits for negative numbers.
showNum :: Int -> Text
showNum n
| n < 0 = "-" <> Data.Text.pack (show (abs n))
| otherwise = Data.Text.pack (show n)
|
