preparing for release
[maximus:gulcii.git] / src / Lambda.hs
1 {-
2     gulcii -- graphical untyped lambda calculus interpreter
3     Copyright (C) 2011, 2013  Claude Heiland-Allen
4
5     This program is free software; you can redistribute it and/or modify
6     it under the terms of the GNU General Public License as published by
7     the Free Software Foundation; either version 2 of the License, or
8     (at your option) any later version.
9
10     This program is distributed in the hope that it will be useful,
11     but WITHOUT ANY WARRANTY; without even the implied warranty of
12     MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
13     GNU General Public License for more details.
14
15     You should have received a copy of the GNU General Public License along
16     with this program; if not, write to the Free Software Foundation, Inc.,
17     51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
18 -}
19
20 module Lambda (Term(..), pretty, isFreeIn, variablesIn, freeVariablesIn) where
21
22 import Data.List (nub)
23
24 import Evaluation (Strategy(..))
25
26 {-
27 Untyped lambda calculus terms.
28 -}
29
30 data Term
31   = Variable String
32   | Lambda Strategy String Term
33   | Apply Term Term
34   | Trace String Term Term
35   deriving (Read, Show, Eq, Ord)
36
37 {-
38 Pretty-print a term.
39 -}
40
41 pretty :: Term -> String
42 pretty = unwords . pretty'
43
44 pretty' :: Term -> [String]
45 pretty' (Variable v) = [v]
46 pretty' (Lambda k v t) = ["(", "\\", v, pretty'' k] ++ pretty' t ++ [")"]
47 pretty' (Apply  s t) = ["("] ++ pretty' s ++ pretty' t ++ [")"]
48 pretty' (Trace k s t) = ["(", "{", k, ":"] ++ pretty' s ++ ["}"] ++ pretty' t ++ [")"]
49
50 pretty'' :: Strategy -> String
51 pretty'' Strict = "!"
52 pretty'' Lazy = "."
53 pretty'' Copy = "?"
54
55 {-
56 Check if a variable occurs free in a term.
57 -}
58
59 isFreeIn :: String -> Term -> Bool
60 isFreeIn n (Variable v)  = n == v
61 isFreeIn n (Lambda _ v t)  = if n == v then False else n `isFreeIn` t
62 isFreeIn n (Apply t t')  = n `isFreeIn` t || n `isFreeIn` t'
63 isFreeIn n (Trace _ t t')  = n `isFreeIn` t || n `isFreeIn` t'
64
65 {-
66 Get all variable names defined or referenced by a term.
67 -}
68
69 variablesIn :: Term -> [String]
70 variablesIn (Variable v)  = [v]
71 variablesIn (Lambda _ v t)  = nub $ v : variablesIn t
72 variablesIn (Apply t t')  = nub $ variablesIn t ++ variablesIn t'
73 variablesIn (Trace _ t t')  = nub $ variablesIn t ++ variablesIn t'
74
75 {-
76 Get all free variables referenced by a term.
77 -}
78
79 freeVariablesIn :: Term -> [String]
80 freeVariablesIn t = filter (`isFreeIn` t) (variablesIn t)