blob: 6b5b7a2381817fff8970f1a366bbd35f7f175390 (
plain)
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
|
module Minilang.Lambda.DeBruijn where
import Data.List (elemIndex)
import Data.Text (Text)
import Minilang.Lambda.Eval (Term)
import qualified Minilang.Lambda.Eval as Eval
data DeBruijn
= FV Text
| Var Int
| Lam DeBruijn
| App DeBruijn DeBruijn
deriving (Show, Read, Eq)
-- Convert a term with named variables to De Bruijn indices
toDeBruijn :: Term -> DeBruijn
toDeBruijn term = go term []
where
go (Eval.Var x) env =
case elemIndex x env of
Just idx -> Var idx
Nothing -> FV x
go (Eval.Lam x body) env =
Lam (go body (x : env))
go (Eval.App f a) env =
App (go f env) (go a env)
eval :: DeBruijn -> DeBruijn
eval (App f a) =
case eval f of
Lam body -> eval (substitute 0 a body)
f' -> App f' a
eval term = term
substitute :: Int -> DeBruijn -> DeBruijn -> DeBruijn
substitute n arg term = case term of
FV x -> FV x
Var x
| x == n -> arg
| otherwise -> Var x
Lam body -> Lam (substitute (n + 1) arg body)
App f a -> App (substitute n arg f) (substitute n arg a)
|
