{-
    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)