{-
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.
-}
{-
Sugared term parser
===================
Grammar
-------
T ::= v | '\\' v+ ('.' | '!' | '?') T | T+ | '(' T ')' | n | '[' (T (, T)*)? ']' | '{' v ':' T '}' T
-}
module Sugar(Term(..), parse, desugar) where
import Control.Applicative((<|>), (<$>), (<$), (<*>), (<*), some, liftA2)
import Data.List ((\\))
import Parse
import qualified Lambda as U
import Evaluation (Strategy(..))
data Term
= Variable String
| Lambda Strategy [String] Term
| Apply [Term]
| Group Term
| Natural Integer
| List [Term]
deriving (Read, Show, Eq, Ord)
parse :: Parser String Term
parse = Apply <$> some parse'
parse' :: Parser String Term
parse' = (flip Lambda <$ sym "\\" <*> some name <*> strategy <*> parse)
<|> (Group <$ sym "(" <*> parse <* sym ")")
<|> (Variable <$> name)
<|> (Natural <$> integer)
<|> (List <$ sym "[" <*> manySep (sym ",") parse <* sym "]")
strategy :: Parser String Strategy
strategy = (Strict <$ sym "!") <|> (Lazy <$ sym ".") <|> (Copy <$ sym "?")
{-
A list of all possible legal variable names, need to generate fresh
variables (ie, names guaranteed to be unused in a given term).
-}
variables :: [String]
variables = [ v:vs | vs <- [] : variables, v <- ['a'..'z'] ]
{-
Desugar according to the following conventions:
Outermost parentheses are dropped:
M N means of (M N)
Applications are left associative:
M N P means (M N) P
The body of an abstraction extends as far right as possible
\x.M N means \x.(M N) and not (\x.M) N
A sequence of abstractions are contracted:
\x.\y.\z.N is abbreviated as \x y z.N
Desugar naturals with their Scott-encoding:
0 -> \s z . z
(1+n) -> \s z . s (desugar n)
Desugar lists with their Scott-encoding:
[] -> \ c n . n
(x:xs) -> \ c n . c (desugar x) (desugar xs)
-}
desugar :: Term -> Maybe U.Term
desugar (Variable v) = Just $ U.Variable v
desugar (Lambda _ [] _) = Nothing
desugar (Lambda k [v] t) = fmap (U.Lambda k v) $ desugar t
desugar (Lambda k (v:vs) t) = fmap (U.Lambda k v) $ desugar (Lambda k vs t)
desugar (Apply []) = Nothing
desugar (Apply ts) = foldl1 (liftA2 U.Apply) (map desugar ts)
desugar (Group t) = desugar t
desugar (Natural 0) = Just $ lam "s" (lam "z" (U.Variable "z"))
desugar (Natural n) =
let Just nn = desugar (Natural (n - 1))
(s:z:_) = variables \\ U.freeVariablesIn nn
in Just $ lam s (lam z (U.Apply (U.Variable s) nn))
desugar (List []) = Just $ lam "c" (lam "n" (U.Variable "n"))
desugar (List (l:ls)) =
let t = desugar l
ts = desugar (List ls)
in case (t,ts) of
(Just t', Just ts') ->
let (c:n:_) = (variables \\ U.freeVariablesIn t') \\ U.freeVariablesIn ts'
in Just $ lam c (lam n (U.Apply (U.Apply (U.Variable c) t') ts'))
_ -> Nothing
lam :: String -> U.Term -> U.Term
lam = U.Lambda Lazy