{-
gulcii -- graphical untyped lambda calculus interpreter
Copyright (C) 2011, 2013, 2017 Claude Heiland-Allen
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License along
with this program; if not, write to the Free Software Foundation, Inc.,
51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
-}
module Graph (Term(..), Definitions, References, graph, pretty) where
import Data.Map.Strict (Map)
import qualified Bruijn as B
import Evaluation (Strategy(..))
data Term
= Free !String
| Bound0
| Scope !Term
| Lambda !Strategy !Term
| Apply !Term !Term
| Reference !Integer
deriving (Read, Show, Eq, Ord)
pretty :: Term -> String
pretty = concat . pretty'
pretty' :: Term -> [String]
pretty' (Free s) = [s]
pretty' (Bound0) = ["0"]
pretty' (Scope t) = ["S"] ++ pretty' t
pretty' (Reference i) = ['#':show i]
pretty' (Lambda k t) = ["(", "\\", pretty'' k] ++ pretty' t ++ [")"]
pretty' (Apply s t) = ["("] ++ pretty' s ++ [" "] ++ pretty' t ++ [")"]
pretty'' :: Strategy -> String
pretty'' Strict = "!"
pretty'' Lazy = "."
pretty'' Copy = "?"
type Definitions = Map String Term
type References = Map Integer Term
graph :: B.Term -> Term
graph (B.Free v) = Free v
graph (B.Bound0) = Bound0
graph (B.Scope t) = Scope (graph t)
graph (B.Lambda k t) = Lambda k (graph t)
graph (B.Apply s t) = Apply (graph s) (graph t)