{-# OPTIONS_GHC -fglasgow-exts #-}

module HW6 where

import qualified Debug.Trace as D
import qualified Data.List as L
import qualified Data.Generics as G


--
-- Term datatype. Contains core term language and syntactic sugar
--   extensions.
--
data Term = Var String       
          | String :\ Term   
          | Term :$: Term

          | Con Integer
          | Term :+: Term
          | Term :-: Term

          | Count
          | Out Term

          | LetRec Decl Term

          | Term :*: Term
          | Fst Term
          | Snd Term

          | TT
          | FF
          | Not Term
          | Term :==: Term
          | If Term Term Term

          | Skip
          | Term :& Term

          | Term ::: Term
          | Nil 
          | LCase Term Term Term

          | MkRef Term
          | Read Term
          | Term := Term

          | Amb Term Term

          --
          -- Syntactic Sugar
          --
          | Let [Decl] Term 
            -- Let [x1 :=: e1, x2 :=: e2] e ==> (x1 :\ (x2 :\ e) :$: e2) :$: e1

          | LetRecs [Decl] Term 
            -- LetRecs [x1 :=: e1, x2 :=: e2] e ==> LetRec (x1 :=: e1) (LetRec (x2 :=: e2) e

          | While Term Term 
            -- While e1 e2 ==> LetRec (w :=: x :\ If e1 (e2 :& Var w :$: Skip) Skip) (Var w :$: Skip)
            -- where x and w are not in the free vars of e1 and e2

          | ReadV String
            -- ReadV x ==> Read (Var x)

          | String :!= Term
            -- x :!= e ==> Var x := e
 
  deriving (G.Data, G.Typeable, Show)


--
-- Declaration datatype (for use in core LetRec Term
-- construct). Second declaration form is syntactic sugar.
--
data Decl = String :=: Term 

          --
          -- Syntactic Sugar
          -- 
          | String :!=: Term 
            -- x :!=: e ==> x :=: MkRef e

  deriving (G.Data, G.Typeable, Show)


--
-- Fixity declarations
--
infix 1 :=:
infix 1 :!=:
infixr 2 :\
infixr 3 :&
infix 4 :!=
infix 4 :=
infixl 5 :$:
infixl 7 :+:
infixr 8 :::

--
-- The assignment: Fill in the definitions of the three functions below.
--

--
-- freeVars e produces a list of the free variables in e
--
-- Assume e contains no syntactic sugar.
--
-- Hint: you should use the Haskell library functions nub and (\\),
--   both of which are in the List module imported into this file.  
--
freeVars :: Term -> [String]

--
-- desugar e produces a desugared version of e
--
desugar :: Term -> Term

--
-- allClosed x checks to see if every Term occurring anywhere in the
--   given argument is closed.
--
-- Hint: Make use of freeVars and desugar from above; make desugar
--   applicable at all types (this is very easy to do).
--
allClosed :: G.GenericQ Bool

{--- Some examples of allClosed: 

  allClosed (Var "x") == False 

  allClosed [Let ["x" :=: Var "f"] (Var "x"), "x" :\ Var "x", Skip] == False

  allClosed (("x" :\ Var "x", 
              "z" :\ LetRecs ["x" :=: Con 1, 
                              "f" :=: "y" :\ If (Var "y") (Var "f" :$: Var "x") Skip
                             ] 
                             (Var "f" :$: Var "z")
             ),
             Skip
            )
     == True
---}