blob: 1e85ca67ca8dd49e8f63e9973b78c07211abab39 (
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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
|
{-# LANGUAGE LambdaCase #-}
module Minilang.Lambda.DeBruijn where
import Data.List (elemIndex)
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
| 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
FNum n -> Eval.Num n
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' :: (Show ann, Eq ann) => 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 env 0 a body)
f' -> if f' /= f
then eval' env $ App f' a
else App f' a
eval' _ term = term
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 term -> term
Nothing -> FV x
FNum _ -> 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
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)
|
