{-
    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.
-}

{-

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(Applicative, Alternative, (<|>), (<$>), (<$), (<*>), (<*), 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]
  | Trace String Term 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 "]")
      <|> (Trace <$ sym "{" <*> name <* sym ":" <*> parse <* sym "}" <*> parse)

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
desugar (Trace k s t) = U.Trace k <$> desugar s <*> desugar t

lam :: String -> U.Term -> U.Term
lam = U.Lambda Lazy