{-
    gulcii -- graphical untyped lambda calculus interpreter
    Copyright (C) 2011, 2013  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 Lambda (Term(..), pretty, isFreeIn, variablesIn, freeVariablesIn) where

import Data.List (nub)

import Evaluation (Strategy(..))

{-
Untyped lambda calculus terms.
-}

data Term
  = Variable String
  | Lambda Strategy String Term
  | Apply Term Term
  | Trace String Term Term
  deriving (Read, Show, Eq, Ord)

{-
Pretty-print a term.
-}

pretty :: Term -> String
pretty = unwords . pretty'

pretty' :: Term -> [String]
pretty' (Variable v) = [v]
pretty' (Lambda k v t) = ["(", "\\", v, pretty'' k] ++ pretty' t ++ [")"]
pretty' (Apply  s t) = ["("] ++ pretty' s ++ pretty' t ++ [")"]
pretty' (Trace k s t) = ["(", "{", k, ":"] ++ pretty' s ++ ["}"] ++ pretty' t ++ [")"]

pretty'' :: Strategy -> String
pretty'' Strict = "!"
pretty'' Lazy = "."
pretty'' Copy = "?"

{-
Check if a variable occurs free in a term.
-}

isFreeIn :: String -> Term -> Bool
isFreeIn n (Variable v)  = n == v
isFreeIn n (Lambda _ v t)  = if n == v then False else n `isFreeIn` t
isFreeIn n (Apply t t')  = n `isFreeIn` t || n `isFreeIn` t'
isFreeIn n (Trace _ t t')  = n `isFreeIn` t || n `isFreeIn` t'

{-
Get all variable names defined or referenced by a term.
-}

variablesIn :: Term -> [String]
variablesIn (Variable v)  = [v]
variablesIn (Lambda _ v t)  = nub $ v : variablesIn t
variablesIn (Apply t t')  = nub $ variablesIn t ++ variablesIn t'
variablesIn (Trace _ t t')  = nub $ variablesIn t ++ variablesIn t'

{-
Get all free variables referenced by a term.
-}

freeVariablesIn :: Term -> [String]
freeVariablesIn t = filter (`isFreeIn` t) (variablesIn t)