blob: de709f1f412091690533bda722fe3cb9dc060572 (
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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
-- MIT License, Copyright (c) 2024 Marvin Borner
module Data.Mili
( Term(..)
, Nat(..)
, fold
, shift
) where
import Data.Functor.Identity ( runIdentity )
import Prelude hiding ( abs
, min
)
data Nat = Z | S Term
data Term = Abs Int Term -- | Abstraction with level
| App Term Term -- | Application
| Lvl Int -- | de Bruijn level
| Num Nat -- | Peano numeral
| Rec Term Term Term Term Term -- | Unbounded iteration
instance Show Nat where
show Z = "Z"
show (S t) = "S(" <> show t <> ")"
instance Show Term where
showsPrec _ (Abs l m) =
showString "(\\" . shows l . showString "." . shows m . showString ")"
showsPrec _ (App m n) =
showString "(" . shows m . showString " " . shows n . showString ")"
showsPrec _ (Lvl i) = shows i
showsPrec _ (Num n) = shows n
showsPrec _ (Rec t1 t2 u v w) =
showString "REC ("
. shows t1
. showString ", "
. shows t2
. showString "), "
. shows u
. showString ", "
. shows v
. showString ", "
. shows w
fold
:: (Int -> Term -> Term)
-> (Term -> Term -> Term)
-> (Int -> Term)
-> (Nat -> Term)
-> (Term -> Term -> Term -> Term -> Term -> Term)
-> Term
-> Term
fold abs app lvl num rec (Abs l m) = abs l $ fold abs app lvl num rec m
fold abs app lvl num rec (App a b) =
app (fold abs app lvl num rec a) (fold abs app lvl num rec b)
fold _ _ lvl _ _ (Lvl n ) = lvl n
fold _ _ _ num _ (Num Z ) = num Z
fold abs app lvl num rec (Num (S t)) = num $ S $ fold abs app lvl num rec t
fold abs app lvl num rec (Rec t1 t2 u v w) = rec
(fold abs app lvl num rec t1)
(fold abs app lvl num rec t2)
(fold abs app lvl num rec u)
(fold abs app lvl num rec v)
(fold abs app lvl num rec w)
shift :: Int -> Term -> Term
shift 0 = id
shift n = fold (\l m -> Abs (l + n) m) App (\l -> Lvl $ l + n) Num Rec
|
