mar18_tut.hs

module TutAssignment where

{-
introducing basic data types for A3
-}

-- First step: Notes have inductive definition of extended Lambda calculus

-- NOTE: Wrong, since it's typed
-- data BExp x
--   = BTrue
--   | BFalse
--   | Eq x x
--   | Le x x
--   | Ge x x
--   | Not (BExp x)
--   deriving (Show, Eq, Ord)

data Lambda
  = Var String
  | App Lambda Lambda
  | Abs String Lambda -- basic Lambda Term
  | Add Lambda Lambda
  | Sub Lambda Lambda
  | Mul Lambda Lambda
  | Num Int           -- arithmetic term
  | Cond Lambda Lambda Lambda -- main control flow, if
    | LTrue
    | LFalse
  deriving (Show, Eq)


-- switching to debruijn notation
-- \x.\y.xy -> \.\2.1

data DLambda
  = DVar Int
  | DApp DLambda DLambda
  | DAbs DLambda
  -- ... and the rest

type Prog = [SECDInstruction]
data SECDInstruction
  = CLO Prog -- push closure of code with current env to the stack
  | APP -- popp function closure and argument and perform application
  | ACCESS Int -- push nth val in the env to the stack
  | RET -- return the top value on the stack and jump to the next on the stack
  | CONST Int -- constant int val
  | ADD
  | MUL
  | LEQ
  | TRUE
  | FALSE
  | IF
  | CONS
  | NIL -- List
  | CASE Prog -- List
  | CLOS [SECDInstruction] [Int] -- closure operation? (which is what supposed to go on the stack?)
  deriving (Show, Eq)

translateToDeBruijn :: Lambda -> DLambda
-- use the same code as Robin's alpha renaming
-- for the counter, keep track of the the indices
-- write the DeBruijn index instead
translateToDeBruijn = undefined

compile :: DLambda -> Prog
compile x = case x of
  -- NOTE: TA had 
  -- (DAbs t) -> [CLO (compile t ++ [RET])] 
  -- which didnt work for me ??
  (DAbs term ) -> CLO (compile term) : [RET]
  (DApp t1 t2) -> compile t1 ++ compile t2 ++ [APP]
  (DVar n    ) -> [ACCESS n]
  -- ... more terms here
  _            -> undefined

-- code, env, stack
type SECDMachine = (Prog, [Int], Prog)

-- a function that does one step
step :: SECDMachine -> SECDMachine
-- fill in this table
-- note: some type issues here, idk why
step ((CLO c) : prog, env, stack) = (c, env, CLO ((c, env) : stack))

-- fixPoint :: (Eq a) => (a -> a) -> a -> a
-- fixPoint f x = if (x == ) -- ?