{- 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 Bruijn (Term(..), bruijn, freeVariablesIn) where import Data.Maybe (listToMaybe) import Data.Set (Set, empty, singleton, union) import qualified Lambda as U import Evaluation (Strategy) data Term = Free String | Bound0 | Scope Term | Lambda Strategy Term | Apply Term Term deriving (Read, Show, Eq, Ord) bruijn :: U.Term -> Term bruijn = bruijn' [] bruijn' :: [String] -> U.Term -> Term bruijn' m (U.Apply s t) = Apply (bruijn' m s) (bruijn' m t) bruijn' m (U.Lambda k v t) = Lambda k (bruijn' (v : m) t) bruijn' m (U.Variable v) = case genericElemIndex v m of Nothing -> Free v Just i -> applyN i Scope Bound0 applyN :: Integer -> (a -> a) -> a -> a applyN n f | n == 0 = id | otherwise = f . applyN (n - 1) f freeVariablesIn :: Term -> Set String freeVariablesIn (Free v) = singleton v freeVariablesIn Bound0 = empty freeVariablesIn (Scope t) = freeVariablesIn t freeVariablesIn (Lambda _ t) = freeVariablesIn t freeVariablesIn (Apply s t) = freeVariablesIn s `union` freeVariablesIn t {- Generic list functions. -} genericElemIndex :: (Eq a, Enum b, Num b) => a -> [a] -> Maybe b genericElemIndex x = genericFindIndex (x ==) genericFindIndex :: (Enum b, Num b) => (a -> Bool) -> [a] -> Maybe b genericFindIndex p = listToMaybe . genericFindIndices p genericFindIndices :: (Enum b, Num b) => (a -> Bool) -> [a] -> [b] genericFindIndices p xs = [ i | (x, i) <- zip xs [0 ..], p x]