-- ***************************************************

-- 6.820 - Program Analysis - Fall 2019
-- PROBLEM SET 1

-- ***************************************************


-- ---------------------------------------------------
-- Problem 1
-- ---------------------------------------------------

-- Just copying some code from the problem set into this file
-- to check that we can load it into ghci and work with it.

apply_n f n x =
  if n == 0 then x
  else apply_n f (n - 1) (f x)

plus a b = apply_n ((+) 1) b a
mult a b = apply_n ((+) a) b 0
expon a b = apply_n ((*) a) b 1


-- ---------------------------------------------------
-- Problem 2
-- ---------------------------------------------------

-- Don't know calculus, so...


-- ---------------------------------------------------
-- Problem 3 : Sets
-- ---------------------------------------------------

type IntSet = (Int -> Bool)

isMember :: IntSet -> Int -> Bool
isMember f x = f x


-- Part a : Simple Sets
-- ---------------------------------------------------

-- A "set" is a function from Int to Bool.
-- It checks if an integer is a member of the set.
-- An empty set has no members, so no matter what Int
-- you give it, it should return False.
emptySet :: IntSet -- IntSet == Int -> Bool
emptySet x = False

-- Check it:
-- isMember emptySet 3 == False
-- isMember emptySet 5 == False

-- The "allInts" set contains all integers.
-- So no matter which integer you give it, it should
-- return True.
allInts :: IntSet
allInts x = True

-- Check it:
-- isMember allInts 3 == True
-- isMember allInts 10 == True


-- Part b : Intervals
-- ---------------------------------------------------

-- interval x y contains all the integers in [x, y].
interval :: Int -> Int -> IntSet -- Int -> Int -> (Int -> Bool)
interval lBound uBound = \x -> lBound <= x && x <= uBound

-- Check it:
-- let range  = interval 5 10
--     range' = interval 3 7
--  in isMember range 7 == True
--     isMember range 13 == False
--     isMember range' 2 == False
--     isMember range' 5 == False


-- Part c : Primes
-- ---------------------------------------------------

-- Don't care right now...


-- Part d : Set Operators
-- ---------------------------------------------------

-- Boolean Operators

-- A "set" is a function that takes an Int and returns a Bool
-- indicating whether the Int is in the Set.
-- So to build the intersection of two "sets" f and g,
-- we build a function that takes an Int, and checks if
-- that Int is in both sets f and g.
setIntersection :: IntSet -> IntSet -> IntSet
setIntersection f g = \x -> f x && g x

-- Or in either sets f or g.
setUnion:: IntSet -> IntSet -> IntSet
setUnion f g = \x -> f x || g x

-- Or not in set f.
setComplement :: IntSet -> IntSet
setComplement f = \x -> not (f x)

-- Check it
-- let range  = interval 5 10
--     range' = interval 3 7
--     intersection range range'
--     union range range'
--     complement range
--  in isMember intersection 6 == True
--     isMember intersection 4 == False
--     isMember union 6 == True
--     isMember union 4 == True
--     isMember complement 3 == False


-- Part e : Equality
-- ---------------------------------------------------

-- Not sure. Maybe do set equality for a range, and check every Int in the range.


-- ---------------------------------------------------
-- Problem 4 : Using Lambda Combinators
-- ---------------------------------------------------

type LamVar = Char
type LamBool = LamVar -> LamVar -> LamVar

-- True is represented as a function that takes two arguments and returns the first.
true :: LamBool
true = \x -> \y -> x

-- False is represented as a function that takes two arguments and returns the second.
false :: LamBool
false = \x -> \y -> y

-- Cond is represented as a function that takes a condition and two other arguments.
-- If the condition is true, it returns the first argument, otherwise the second.
-- cond :: LamBool -> LamBool -> LamBool -> LamBool
-- cond = \c -> \e1 -> \e2 -> c e1 e2

-- Check it:
-- true 'x' 'y' == 'x'
-- false 'x' 'y' == 'y'
-- cond true 'x' 'y' == 'x'
-- cond false 'x' 'y' == 'y'

-- and :: (Char -> Char -> Char) -> (Char -> Char -> Char) -> (Char -> Char -> Char)
-- and = \e1 -> \e2 -> cond e1 e2 false

-- bnot = \b1 -> cond b1 false true





-- ---------------------------------------------------
-- Problem 6 : A Normal Order NF Interpreter
-- ---------------------------------------------------


-- Part c: Renaming Function in Haskell
-- ---------------------------------------------------

-- Expressions can have the form of variables, applications, or abstractions.
data Expr =
      Var Name -- a variable
    | App Expr Expr -- application
    | Lambda Name Expr -- lambda abstraction
  deriving
    (Eq, Show) -- use default compiler generated Eq and Show instances

-- A variable can have a string name.
type Name = String -- a variable name

-- @replaceVar ("x", y) z@ takes the expression @z@, and it replaces
-- all free occurrences of "x" with the expression @y@.
replaceVar :: (Name, Expr) -> Expr -> Expr
replaceVar (n, e) src =
  case src of
    -- Is the expression a variable?
    -- If so, replace the variable if it's the one we're looking to replace.
    Var n' ->
      case n == n' of
        True -> e -- If it matches @n@, replace it with @e@.
        False -> src -- Otherwise, there's no match to replace.

    -- Is the expression an application?
    -- If so, replace the variables in each of the subexpressions.
    App e1 e2 -> App (replaceVar (n, e) e1) (replaceVar (n, e) e2)

    -- Is the expression a lambda?
    Lambda n' e' ->
      case n == n' of
        True -> src -- @n@ is bound (not free) so we can't replace it.
        False -> Lambda n' (replaceVar (n, e) e') -- Replace @n@ in the body.
        -- Note that this last replacement is naive.
        -- It doesn't prevent variable capture.


-- Check it:
-- let x = Var "x"
-- let y = Var "y"
-- replaceVar ("x", y) x -- Returns: @Var "y"@ (it replaces "x" with y)
-- replaceVar ("y", y) x -- Returns @Var "x"< (there is no free "x", so it replaces nothing)
-- let a = App x y
-- let b = App y y
-- replaceVar ("x", y) a -- Returns @App (Var "y") (Var "y") (it replaces the first "x" with "y")
-- replaceVar ("x", y) b -- Returns @App (Var "y") (Var "y") (no "x" in either expression)
-- let z = Var "z"
-- let c = Lambda "x" z
-- let d = Lambda "y" z
-- replaceVar ("x", y) c -- Returns the expression unchanged, because "x" is bound.
-- replaceVar ("z", y) d -- Returns the body changed to "y". But now "y" is captured!


-- Part d: Doing a Single Step
-- ---------------------------------------------------

-- Do one step of reduction.
normNF_OneStep :: ([Name], Expr) -> Maybe ([Name], Expr)
normNF_OneStep (name:names, e) =
  case e of

    -- A var can't be reduced any further.
    Var _ -> Nothing

    -- If it's an abstraction, we can't reduce further.
    Lambda _ _ -> Nothing

    -- If there's an application, we might have a redex.
    App e1 e2 ->
      case e1 of

        -- If the first term is a var, we can't reduce further.
        Var _ -> Nothing

        -- If the first term is an application, we can't reduce further.
        App _ _ -> Nothing

        -- If the first term is an abstraction, we can apply it to the argument.
        Lambda n' e' ->
           -- Alpha rename the bound variables in the body, then do the reduction.
          let alpha_converted_e = replaceVar (n', Var name) e'
              reduced_e = replaceVar (name, e2) alpha_converted_e
           in Just (names, reduced_e)

-- Check it:
-- let x = Var "x"
-- let y = Var "y"
-- let z = Var "z"
-- let lxx = Lambda "x" x
-- let lxy = Lambda "x" y
-- let lxx_y = App lxx y
-- normNF_OneStep (["a", "b"], lxx) ==> Returns: Nothing
-- normNF_OneStep (["a", "b"], lxx_y) ==> Returns: Just (["b"],Var "y")


-- Part e: Repitition
-- ---------------------------------------------------

-- Do @n@ steps of reduction.
normNF_n :: Int -> ([Name], Expr) -> ([Name], Expr)
normNF_n gas (names, e) =
  case gas of
    0 -> (names, e)
    _ ->
      case normNF_OneStep (names, e) of
        Nothing -> (names, e)
        Just (names', e') -> normNF_n (gas - 1) (names', e')

-- Check it:
-- let x = Var "x"
-- let y = Var "y"
-- let z = Var "z"
-- let lxx = Lambda "x" x
-- let lxx_y = App lxx y
-- normNF_n 3 (["a", "b"], lxx_y) ==> Returns: (["b"],Var "y")
-- let lylxx_y_z = App (Lambda "y" (App lxx y)) z
-- normNF_n 3 (["a", "b", "c"], lylxx_y_z) ==> Returns: (["c"],Var "z")


-- Part f: Generating New Names
-- ---------------------------------------------------

-- A list of integers.
freshNames = [1..]

-- Gather all names used in an expression.
usedNames :: Expr -> [Name]
usedNames e =
  case e of
    Var n -> [n]
    App e1 e2 -> (usedNames e1) ++ (usedNames e2)
    Lambda n e' -> (n : usedNames e')

-- Check it:
-- let x = Var "x"
-- let y = Var "y"
-- let lxx = Lambda "x" x
-- let lxx_y = App lxx y
-- usedNames lxx_y ==> Returns: ["x", "x", "y"]


-- Part g: Finishing Up
-- ---------------------------------------------------

-- @normNF 3 (App (Lambda "x" (Var "x")) (Var "y"))@ performs 3 reductions.
normNF :: Int -> Expr -> Expr
normNF gas e =
  let taken_names = usedNames e
      num_names = length taken_names
      fresh_names = map show (take num_names freshNames)
      (fresh_names', e') = normNF_n gas (fresh_names, e)
   in e'

-- Check it:
-- let x = Var "x"
-- let y = Var "y"
-- let lxx = Lambda "x" x
-- let lxx_y = App lxx y
-- normNF 5 lxx_y ==> Returns: Var "y"