Add back Symbol typeclass
This commit is contained in:
Joscha
parent
2bacb8f9d6
commit
cf0ed21144
1 changed files with 98 additions and 109 deletions
207
lambda.hs
207
lambda.hs
|
|
@ -1,24 +1,45 @@
|
|||
|
||||
import Data.List
|
||||
import Data.Maybe
|
||||
|
||||
-- A symbol denoting a variable; consists of a textual name and some (or no) apostrophes to ensure uniqueness
|
||||
data Symbol = Symbol { symBase :: String -- lowercase a to z
|
||||
, symLen :: Int -- nonnegative
|
||||
}
|
||||
class (Eq s) => Symbol s where
|
||||
-- Present symbols (not including symbol to change) -> symbol to change ->
|
||||
-- simplest unique symbol
|
||||
findName :: [s] -> s -> s
|
||||
|
||||
-- Symbol that appends apostrophes to become unique
|
||||
data SymApostrophe = SymApostrophe { symApoBase :: String -- lowercase a to z
|
||||
, symApoLen :: Int -- nonnegative
|
||||
}
|
||||
deriving (Eq)
|
||||
|
||||
instance Show Symbol where
|
||||
show (Symbol s n) = s ++ (replicate n '\'')
|
||||
instance Show SymApostrophe where
|
||||
show (SymApostrophe s n) = s ++ (replicate n '\'')
|
||||
|
||||
instance Symbol SymApostrophe where
|
||||
findName other (SymApostrophe base n) =
|
||||
let sameBase = filter ((base ==) . symApoBase) other
|
||||
lengths = map symApoLen sameBase
|
||||
freeLengths = [0..] \\ (nub lengths)
|
||||
in SymApostrophe base (head freeLengths) -- [0..] is infinite
|
||||
|
||||
-- Symbol that changes to another letter in the alphabet to become unique
|
||||
data SymLetter = SymLetter {symLetBase :: String } -- lowercase a to z, aa to zz, ...
|
||||
deriving (Eq)
|
||||
|
||||
instance Show SymLetter where
|
||||
show (SymLetter l) = l
|
||||
|
||||
instance Symbol SymLetter where
|
||||
findName other _ =
|
||||
let bases = map symLetBase other
|
||||
freeBases = names \\ (nub bases)
|
||||
in SymLetter (head freeBases)
|
||||
where letters = ['a'..'z']
|
||||
namesN 0 = [""]
|
||||
namesN n = [n ++ [l] | n <- namesN (n - 1), l <- letters]
|
||||
names = concatMap namesN [1..]
|
||||
|
||||
-- Present symbols (not including symbol to change) -> symbol to change ->
|
||||
-- unique symbol with same base and minimal amount of apostrophes
|
||||
findName :: [Symbol] -> Symbol -> Symbol
|
||||
findName other (Symbol base n) =
|
||||
let sameBase = filter ((base ==) . symBase) other
|
||||
lengths = map symLen sameBase
|
||||
freeLengths = [0..] \\ (nub lengths)
|
||||
in Symbol base (head freeLengths) -- [0..] is infinite
|
||||
|
||||
-- An expression. Can be a mere symbol, a lambda application, or a lambda abstraction.
|
||||
data Expression s = ESymbol s
|
||||
|
|
@ -36,6 +57,9 @@ showTopLevel :: (Show s) => Expression s -> String
|
|||
showTopLevel e@(EExpr _ _) = tail . init . show $ e
|
||||
showTopLevel e = show e
|
||||
|
||||
printTopLevel :: (Show s) => Expression s -> IO ()
|
||||
printTopLevel = putStrLn . showTopLevel
|
||||
|
||||
{-
|
||||
Apply a function
|
||||
Insert an expression into another expression:
|
||||
|
|
@ -43,7 +67,7 @@ Insert an expression into another expression:
|
|||
change all symbols within that expression to be unique in the expression's new context
|
||||
simplify all symbols
|
||||
-}
|
||||
simplifyExpr :: [(Symbol, Symbol)] -> [Symbol] -> Expression Symbol -> Expression Symbol
|
||||
simplifyExpr :: (Symbol s) => [(s, s)] -> [s] -> Expression s -> Expression s
|
||||
simplifyExpr mapping context (ESymbol s) = ESymbol $ fromMaybe (findName context s) $ lookup s mapping
|
||||
simplifyExpr mapping context (EExpr a b) = EExpr (simplifyExpr mapping context a) (simplifyExpr mapping context b)
|
||||
simplifyExpr mapping context (ELambda l e) =
|
||||
|
|
@ -52,135 +76,100 @@ simplifyExpr mapping context (ELambda l e) =
|
|||
newcontext = newl : context
|
||||
in ELambda newl (simplifyExpr newmapping newcontext e)
|
||||
|
||||
makeUnique :: [Symbol] -> Expression Symbol -> Expression Symbol
|
||||
makeUnique :: (Symbol s) => [s] -> Expression s -> Expression s
|
||||
makeUnique = simplifyExpr []
|
||||
|
||||
simplify :: Expression Symbol -> Expression Symbol
|
||||
simplify :: (Symbol s) => Expression s -> Expression s
|
||||
simplify = makeUnique []
|
||||
|
||||
insertExpr :: Symbol -> Expression Symbol -> [Symbol] -> Expression Symbol -> Expression Symbol
|
||||
insertExpr :: (Symbol s) => s -> Expression s -> [s] -> Expression s -> Expression s
|
||||
insertExpr r new context old@(ESymbol s)
|
||||
| r == s = makeUnique context new
|
||||
| otherwise = old
|
||||
insertExpr r new context (EExpr a b) = EExpr (insertExpr r new context a) (insertExpr r new context b)
|
||||
insertExpr r new context (ELambda l e) = ELambda l (insertExpr r new (l : context) e)
|
||||
|
||||
apply :: Expression Symbol -> Expression Symbol
|
||||
apply :: (Symbol s) => Expression s -> Expression s
|
||||
apply (EExpr (ELambda s l) b) = insertExpr s b [] l -- [], not [s]
|
||||
apply (EExpr a@(EExpr _ _) b) = EExpr (apply a) b
|
||||
apply e = e
|
||||
|
||||
step :: (Symbol s) => Expression s -> Expression s
|
||||
step = simplify . apply
|
||||
|
||||
-- EXPERIMENT ZONE START --
|
||||
letters = ['a'..'z']
|
||||
namesN :: Int -> [String]
|
||||
namesN 0 = [""]
|
||||
namesN n = [n ++ [l] | n <- namesN (n-1), l <- letters]
|
||||
names :: [String]
|
||||
names = concatMap namesN [1..]
|
||||
findNewName :: [Symbol] -> Symbol
|
||||
findNewName other =
|
||||
let bases = map symBase other
|
||||
freeBases = names \\ (nub bases)
|
||||
in Symbol (head freeBases) 0
|
||||
simplifyExpr_ :: [(Symbol, Symbol)] -> [Symbol] -> Expression Symbol -> Expression Symbol
|
||||
simplifyExpr_ mapping context (ESymbol s) = ESymbol $ fromMaybe (findNewName context) $ lookup s mapping
|
||||
simplifyExpr_ mapping context (EExpr a b) = EExpr (simplifyExpr_ mapping context a) (simplifyExpr_ mapping context b)
|
||||
simplifyExpr_ mapping context (ELambda l e) =
|
||||
let newl = findNewName context
|
||||
newmapping = (l, newl) : mapping
|
||||
newcontext = newl : context
|
||||
in ELambda newl (simplifyExpr_ newmapping newcontext e)
|
||||
makeUnique_ :: [Symbol] -> Expression Symbol -> Expression Symbol
|
||||
makeUnique_ = simplifyExpr_ []
|
||||
simplify_ :: Expression Symbol -> Expression Symbol
|
||||
simplify_ = makeUnique_ []
|
||||
insertExpr_ :: Symbol -> Expression Symbol -> [Symbol] -> Expression Symbol -> Expression Symbol
|
||||
insertExpr_ r new context old@(ESymbol s)
|
||||
| r == s = makeUnique_ context new
|
||||
| otherwise = old
|
||||
insertExpr_ r new context (EExpr a b) = EExpr (insertExpr_ r new context a) (insertExpr_ r new context b)
|
||||
insertExpr_ r new context (ELambda l e) = ELambda l (insertExpr_ r new (l : context) e)
|
||||
apply_ :: Expression Symbol -> Expression Symbol
|
||||
apply_ (EExpr (ELambda s l) b) = insertExpr_ s b [] l -- [], not [s]
|
||||
apply_ (EExpr a@(EExpr _ _) b) = EExpr (apply_ a) b
|
||||
apply_ e = e
|
||||
step_ = simplify_ . apply_
|
||||
-- EXPERIMENT ZONE END --
|
||||
|
||||
_s :: String -> Expression Symbol
|
||||
_s s = ESymbol $ _ss s
|
||||
|
||||
_ss :: String -> Symbol
|
||||
_ss s = Symbol s 0
|
||||
_sa = flip SymApostrophe 0
|
||||
_sl = SymLetter
|
||||
_ea s = ESymbol $ _sa s
|
||||
_el s = ESymbol $ _sl s
|
||||
|
||||
main = do
|
||||
putStrLn "Testing: Showing expressions"
|
||||
print (EExpr (_s "a") (EExpr (_s "b") (_s "c")))
|
||||
print (EExpr (_s "a") (EExpr (_s "b") (EExpr (_s "c") (_s "d"))))
|
||||
print (EExpr (EExpr (_s "a") (_s "b")) (_s "c"))
|
||||
print (EExpr (EExpr (EExpr (_s "a") (_s "b")) (_s "c")) (_s "d"))
|
||||
print (EExpr (EExpr (_s "a") (EExpr (_s "b") (_s "c"))) (_s "d"))
|
||||
print (ELambda (Symbol "a" 0) (_s "a"))
|
||||
print (ELambda (Symbol "a" 0) (EExpr (EExpr (_s "a") (EExpr (_s "b") (_s "c"))) (_s "d")))
|
||||
print (EExpr (_ea "a") (EExpr (_ea "b") (_ea "c")))
|
||||
print (EExpr (_ea "a") (EExpr (_ea "b") (EExpr (_ea "c") (_ea "d"))))
|
||||
print (EExpr (EExpr (_ea "a") (_ea "b")) (_ea "c"))
|
||||
print (EExpr (EExpr (EExpr (_ea "a") (_ea "b")) (_ea "c")) (_ea "d"))
|
||||
print (EExpr (EExpr (_ea "a") (EExpr (_ea "b") (_ea "c"))) (_ea "d"))
|
||||
print (ELambda (_sa "a") (_ea "a"))
|
||||
print (ELambda (_sa "a") (EExpr (EExpr (_ea "a") (EExpr (_ea "b") (_ea "c"))) (_ea "d")))
|
||||
putStrLn ""
|
||||
|
||||
-- test of findName (seems to be working) ~G
|
||||
putStrLn "Testing: Finding new symbols"
|
||||
print $ findName [(Symbol "a" 0), (Symbol "b" 0), (Symbol "a" 1)] (Symbol "a" 4)
|
||||
print $ findName [(Symbol "a" 0), (Symbol "b" 0), (Symbol "a" 1)] (Symbol "b" 3)
|
||||
print $ findName [(Symbol "a" 0), (Symbol "b" 0), (Symbol "a" 1)] (Symbol "c" 2)
|
||||
print $ findName [(Symbol "a" 1), (Symbol "a" 3), (Symbol "a" 0)] (Symbol "a" 1)
|
||||
-- EXPERIMENT ZONE START --
|
||||
print $ findNewName [(Symbol "a" 0), (Symbol "b" 0), (Symbol "a" 1)]
|
||||
print $ findNewName [(Symbol "a" 0), (Symbol "b" 0), (Symbol "a" 1)]
|
||||
print $ findNewName [(Symbol "a" 0), (Symbol "b" 0), (Symbol "a" 1)]
|
||||
print $ findNewName [(Symbol "a" 1), (Symbol "a" 3), (Symbol "a" 0)]
|
||||
-- EXPERIMENT ZONE END --
|
||||
putStrLn "SymApostrophe"
|
||||
print $ findName [(SymApostrophe "a" 0), (SymApostrophe "b" 0), (SymApostrophe "a" 1)] (SymApostrophe "a" 4)
|
||||
print $ findName [(SymApostrophe "a" 0), (SymApostrophe "b" 0), (SymApostrophe "a" 1)] (SymApostrophe "b" 3)
|
||||
print $ findName [(SymApostrophe "a" 0), (SymApostrophe "b" 0), (SymApostrophe "a" 1)] (SymApostrophe "c" 2)
|
||||
print $ findName [(SymApostrophe "a" 1), (SymApostrophe "a" 3), (SymApostrophe "a" 0)] (SymApostrophe "a" 1)
|
||||
putStrLn "SymLetter"
|
||||
print $ findName [(_sl "a"), (_sl "b"), (_sl "a")] (_sl "a")
|
||||
print $ findName [(_sl "a"), (_sl "b"), (_sl "d")] (_sl "b")
|
||||
print $ findName [(_sl "a"), (_sl "d"), (_sl "c")] (_sl "c")
|
||||
print $ findName [(_sl "b"), (_sl "a"), (_sl "c")] (_sl "d")
|
||||
putStrLn ""
|
||||
|
||||
putStrLn "Testing: Applying expressions"
|
||||
let t = (ELambda (_ss "a") (ELambda (_ss "b") (ESymbol (_ss "a"))))
|
||||
f = (ELambda (_ss "a") (ELambda (_ss "b") (ESymbol (_ss "b"))))
|
||||
n = (ELambda (_ss "a") (EExpr (EExpr (ESymbol (_ss "a")) (makeUnique [(_ss "a")] f)) (makeUnique [(_ss "a")] t)))
|
||||
-- EXPERIMENT ZONE START --
|
||||
n_ = (ELambda (_ss "a") (EExpr (EExpr (ESymbol (_ss "a")) (makeUnique_ [(_ss "a")] f)) (makeUnique_ [(_ss "a")] t)))
|
||||
-- EXPERIMENT ZONE END --
|
||||
print t
|
||||
print f
|
||||
print n
|
||||
print $ simplify $ (ELambda (Symbol "a" 1) (ESymbol (Symbol "a" 1)))
|
||||
print (EExpr n f)
|
||||
putStrLn $ showTopLevel (EExpr n f)
|
||||
let ta = (ELambda (_sa "a") (ELambda (_sa "b") (_ea "a")))
|
||||
fa = (ELambda (_sa "a") (ELambda (_sa "b") (_ea "b")))
|
||||
na = (ELambda (_sa "a") (EExpr (EExpr (_ea "a") (makeUnique [(_sa "a")] fa)) (makeUnique [(_sa "a")] ta)))
|
||||
tl = (ELambda (_sl "a") (ELambda (_sl "b") (_el "a")))
|
||||
fl = (ELambda (_sl "a") (ELambda (_sl "b") (_el "b")))
|
||||
nl = (ELambda (_sl "a") (EExpr (EExpr (_el "a") (makeUnique [(_sl "a")] fl)) (makeUnique [(_sl "a")] tl)))
|
||||
print ta
|
||||
print fa
|
||||
print na
|
||||
print tl
|
||||
print fl
|
||||
print nl
|
||||
print $ simplify $ (ELambda (SymApostrophe "a" 1) (ESymbol (SymApostrophe "a" 1)))
|
||||
print $ simplify $ (ELambda (_sl "b") (ESymbol (_sl "b")))
|
||||
putStrLn $ showTopLevel (EExpr na fa)
|
||||
putStrLn $ showTopLevel (EExpr nl fl)
|
||||
putStrLn ""
|
||||
|
||||
putStrLn "Replacing symbols: apostrophe"
|
||||
putStrLn "Running: not false"
|
||||
print (EExpr n f)
|
||||
print . step $ (EExpr n f)
|
||||
print . step . step $ (EExpr n f)
|
||||
print . step . step . step $ (EExpr n f)
|
||||
printTopLevel (EExpr na fa)
|
||||
printTopLevel . step $ (EExpr na fa)
|
||||
printTopLevel . step . step $ (EExpr na fa)
|
||||
printTopLevel . step . step . step $ (EExpr na fa)
|
||||
|
||||
putStrLn "Running: not true"
|
||||
print (EExpr n t)
|
||||
print . step $ (EExpr n t)
|
||||
print . step . step $ (EExpr n t)
|
||||
print . step . step . step $ (EExpr n t)
|
||||
printTopLevel (EExpr na ta)
|
||||
printTopLevel . step $ (EExpr na ta)
|
||||
printTopLevel . step . step $ (EExpr na ta)
|
||||
printTopLevel . step . step . step $ (EExpr na ta)
|
||||
putStrLn ""
|
||||
|
||||
-- EXPERIMENT ZONE START --
|
||||
putStrLn "Replacing symbols: new base"
|
||||
putStrLn "Replacing symbols: letter"
|
||||
putStrLn "Running: not false"
|
||||
print (EExpr n_ f)
|
||||
print . step_ $ (EExpr n_ f)
|
||||
print . step_ . step_ $ (EExpr n_ f)
|
||||
print . step_ . step_ . step_ $ (EExpr n_ f)
|
||||
printTopLevel (EExpr nl fl)
|
||||
printTopLevel . step $ (EExpr nl fl)
|
||||
printTopLevel . step . step $ (EExpr nl fl)
|
||||
printTopLevel . step . step . step $ (EExpr nl fl)
|
||||
|
||||
putStrLn "Running: not true"
|
||||
print (EExpr n_ t)
|
||||
print . step_ $ (EExpr n_ t)
|
||||
print . step_ . step_ $ (EExpr n_ t)
|
||||
print . step_ . step_ . step_ $ (EExpr n_ t)
|
||||
printTopLevel (EExpr nl tl)
|
||||
printTopLevel . step $ (EExpr nl tl)
|
||||
printTopLevel . step . step $ (EExpr nl tl)
|
||||
printTopLevel . step . step . step $ (EExpr nl tl)
|
||||
putStrLn ""
|
||||
-- EXPERIMENT ZONE END --
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue