blob: 8b24f8b5c82ff81505f04ef2e460bb5040673a73 (
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
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
|
{-# LANGUAGE LambdaCase #-}
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 ann
= FV Text
| 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 = []
fromDeBruijn :: DeBruijn Text -> Term
fromDeBruijn = \case
FV x -> Eval.Var x
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)
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 ann -> DeBruijn ann -> DeBruijn ann
eval' env (FV v) = case lookup v env of
Just term -> term
Nothing -> FV v
eval' env (App f a) =
case eval' env f of
Lam _ body -> eval' env (substitute 0 a body)
f' -> App f' a
eval' _ term = term
substitute :: Int -> DeBruijn ann -> DeBruijn ann -> DeBruijn ann
substitute n arg term = case term of
FV x -> FV x
Var t x
| x == n -> arg
| otherwise -> Var t x
Lam x body -> Lam x (substitute (n + 1) arg body)
App f a -> App (substitute n arg f) (substitute n arg a)
pretty :: DeBruijn Text -> Text
pretty = \case
FV x -> x
Var s _ -> s
Lam s body -> "(lam (" <> s <> ") " <> pretty body <> ")"
App f a -> "(" <> pretty f <> " " <> pretty a <> ")"
|
