diff --git a/Delta-Lambda.cabal b/Delta-Lambda.cabal
new file mode 100644
--- /dev/null
+++ b/Delta-Lambda.cabal
@@ -0,0 +1,112 @@
+-- Initial Delta-Lambda.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+-- The name of the package.
+name:                Delta-Lambda
+
+-- The package version.  See the Haskell package versioning policy (PVP) 
+-- for standards guiding when and how versions should be incremented.
+-- http://www.haskell.org/haskellwiki/Package_versioning_policy
+-- PVP summary:      +-+------- breaking API changes
+--                   | | +----- non-breaking API additions
+--                   | | | +--- code changes with no API change
+version:             0.1.0.0
+
+-- A short (one-line) description of the package.
+synopsis:            A demonstration interpreter for type system delta-lambda (of N.G. De-bruijn)
+
+-- A longer description of the package.
+description:         A demonstration package for the type system delta-lambda (of N.G. De-bruijn)
+                     in ~1000 lines of haskell.
+                     this is at the moment exceptionally ALPHA level software.
+                     no tests for the validity of the type checker (only the
+                     type synthesizer), or the parser, or the repl, etc...
+                     there are dragons in here (soon to be tamed), and lots
+                     of them!
+
+                     todo: profiling, unit testing, formal verification of type correctness
+                           adequacy proof of the implemented type system.
+
+-- The license under which the package is released.
+license:             MIT
+
+-- The file containing the license text.
+license-file:        LICENSE
+
+-- The package author(s).
+author:              James M
+
+-- An email address to which users can send suggestions, bug reports, and 
+-- patches.
+maintainer:          listofoptions@gmail.com
+
+-- A copyright notice.
+-- copyright:           
+
+category:            Compilers/Interpreters
+
+build-type:          Simple
+
+-- Extra files to be distributed with the package, such as examples or a 
+-- README.
+-- extra-source-files:  
+
+-- Constraint on the version of Cabal needed to build this package.
+cabal-version:       >=1.10
+
+Flag Debug
+  Description:         Enable debugging
+  Default:             False
+                     
+
+executable Delta-Lambda
+  -- .hs or .lhs file containing the Main module.
+  main-is:             dl.hs
+  default-extensions:  OverloadedStrings,
+                       FlexibleContexts,
+                       TypeSynonymInstances,
+                       FlexibleInstances,
+                       MultiParamTypeClasses,
+                       DefaultSignatures,
+                       DeriveGeneric,
+                       ScopedTypeVariables
+
+
+  if !flag(debug)
+      ghc-options:     -threaded
+                       -with-rtsopts=-N
+                       -W
+                       -fno-warn-warnings-deprecations
+                       -fno-warn-orphans
+                       -fwarn-unused-binds
+  else
+     ghc-options:      -fprof-auto-calls
+                       -with-rtsopts=-pa
+                       
+                       
+  -- Modules included in this executable, other than Main.
+  -- other-modules:       
+  
+  -- LANGUAGE extensions used by modules in this package.
+  -- other-extensions:    
+  
+  -- Other library packages from which modules are imported.
+  build-depends:       base >=4.8 && <4.9,
+                       bytestring >= 0.10.6.0,
+                       cereal >=0.5 && <0.6,
+                       cpphs >=1.20,
+                       filepath >= 1.4.0.0,
+                       haskeline >=0.7 && <0.8,
+                       megaparsec >=5.0 && <5.1,
+                       mtl>=2.2 && <2.3,
+                       options >=1.2 && <1.3,
+                       parallel>=3.2 && <3.3,
+                       text >= 1.2.2.0,
+                       wl-pprint >= 1.2
+  
+  -- Directories containing source files.
+  -- hs-source-dirs:      
+  
+  -- Base language which the package is written in.
+  default-language:    Haskell2010
+  
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+Copyright (c) 2016 James M
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/dl.hs b/dl.hs
new file mode 100644
--- /dev/null
+++ b/dl.hs
@@ -0,0 +1,911 @@
+module Main( main ) where
+
+{- TODO:
+  profiling
+  write tests
+-}
+
+
+--import           Paths_Delta-Lambda (version)
+import           Data.Char                   (isSpace, isNumber)
+import           System.FilePath             hiding ((</>))
+import           Control.Applicative
+import           Control.Monad.Except
+import           Control.Monad.Reader
+import           Control.Parallel
+import           Data.ByteString             (writeFile, readFile)
+import           Data.Text                   (Text, pack, unpack, length)
+import           Data.Text.Encoding
+import           Data.Text.IO
+import           Data.Version
+import           Data.Word                   (Word64)
+import           GHC.Generics
+import           Prelude                     hiding (getContents, putStrLn)
+import           System.IO                   (Handle, IOMode (ReadMode, ReadWriteMode), withFile)
+
+import           Text.Megaparsec             hiding (space)
+import qualified Text.Megaparsec.Lexer       as Lexer
+import           Text.Megaparsec.Text
+
+import           Options
+
+import           Text.PrettyPrint.Leijen     hiding ((<$>))
+
+import           Language.Preprocessor.Cpphs
+
+import           System.Console.Haskeline
+
+import           Data.Serialize
+
+-- represent a term with variable name type v, and variable binding index type i
+-- that has metadata m associated to each node and leaf
+data Term m v i = Variable v i m
+                | Abstraction v m (Term m v i) (Term m v i)
+                | Application m (Term m v i) (Term m v i)
+                | Type m
+                deriving (Generic)
+
+data Kind m v i = Function v m (Term m v i) (Kind m v i)
+                | Kind m
+                deriving (Generic)
+
+data DecompiledFileHeader = DecompiledFileHeader
+  { compiledFileName   :: Text
+  , interpreterVersion :: Version
+  , extensionsUsed     :: [Text]
+  }
+
+data DecompiledFile m v i = DecompiledFile
+  { decompiledFileHeader :: DecompiledFileHeader
+  , decompiledTerm       :: Term m v i
+  }
+
+instance (Serialize m, Serialize v, Serialize i) => Serialize (Term m v i) where
+
+instance (Serialize m, Serialize v, Serialize i) => Serialize (Kind m v i) where
+
+  -- some orphan instances
+instance Serialize Version where
+  put = \vers -> putListOf (put :: Putter Int) (versionBranch vers)
+  get = do
+    branchList :: [Int] <- getListOf get
+    return Version { versionBranch = branchList
+                   , versionTags = []
+                   }
+
+instance Serialize Text where
+  put = \text' -> do
+    putWord64le (fromIntegral (Data.Text.length text') :: Word64)
+    put (encodeUtf8 text')
+  get = do
+    leng <- getWord64le
+    bs <- getByteString (fromIntegral leng :: Int)
+    return (decodeUtf8 bs)
+
+instance Serialize SourcePos where
+  put = \srcPos -> do
+    put (sourceName srcPos)
+    put (sourceLine srcPos)
+    put (sourceColumn srcPos)
+  get = do str :: String <- get
+           pos1 :: Pos <- get
+           pos2 :: Pos <- get
+           return $ SourcePos str pos1 pos2
+
+instance Serialize Pos where
+  put = \pos -> putWord64le (fromIntegral (unPos pos) :: Word64)
+  get = getWord64le >>= return . unsafePos . fromIntegral
+
+instance Serialize DecompiledFileHeader where
+  put = \decompHeader -> do
+    put (compiledFileName decompHeader)
+    put (interpreterVersion decompHeader)
+    put (extensionsUsed decompHeader)
+  get = do
+    fname :: Text <- get
+    iversion :: Version <- get
+    xtensions :: [Text] <- get
+    return DecompiledFileHeader
+      { compiledFileName = fname
+      , interpreterVersion = iversion
+      , extensionsUsed = xtensions
+      }
+
+instance (Serialize m, Serialize v, Serialize i) => Serialize (DecompiledFile m v i) where
+  put = \decomp -> do
+    put (decompiledFileHeader decomp)
+    put (decompiledTerm decomp)
+  get = do
+    fileHeader :: DecompiledFileHeader <- get
+    fileBody :: Term m v i <- get
+    return DecompiledFile
+      { decompiledFileHeader = fileHeader
+      , decompiledTerm = fileBody
+      }
+
+transpile :: (m -> m') -> (v -> v') -> (i -> i') -> DecompiledFile m v i -> DecompiledFile m' v' i'
+transpile fm fv fi decompFile@DecompiledFile{ decompiledTerm = fileBody } =
+  let transpile' t = case t of
+                    Type m -> Type (fm m)
+                    Variable v i m -> Variable (fv v) (fi i) (fm m)
+                    Application m a f ->
+                      Application (fm m) (transpile' a) (transpile' f)
+                    Abstraction v m t b ->
+                      Abstraction (fv v) (fm m) (transpile' t) (transpile' b)
+  in decompFile { decompiledTerm = transpile' fileBody }
+
+
+
+
+
+bindTerm :: (Eq v, Eq i, Enum i) => v -> i -> Term m v i -> Term m v i
+bindTerm variable index subject = case subject of
+  Type metadata -> Type metadata
+  Application metadata argument function ->
+    Application metadata (bindTerm variable index argument) (bindTerm variable index function)
+  Abstraction variable' metadata parameter body ->
+    Abstraction variable' metadata (bindTerm variable index parameter)
+                                  (bindTerm variable (succ index) body)
+  Variable variable' index' metadata
+    | variable == variable' && index' == toEnum 0 -> Variable variable' index metadata
+    | otherwise -> subject
+
+bindContext :: (Eq i, Enum i, Show i) => [Term m Text i] -> i -> Term m Text i -> Term m Text i
+bindContext context index term = case context of
+  [] -> term
+  _:rest -> bindContext rest (succ index) (bindTerm (pack ("$" ++ show index)) index term)
+
+updateTerm :: (Ord i, Enum i) => i -> i -> Term m v i -> Term m v i
+updateTerm i k subject = case subject of
+  Type metadata -> Type metadata
+  Application metadata argument function ->
+    Application metadata (updateTerm i k argument) (updateTerm i k function)
+  Abstraction variable metadata parameter body ->
+    Abstraction variable metadata (updateTerm i k parameter) (updateTerm i (succ k) body)
+  Variable variable index metadata
+    | index > k -> Variable variable (toEnum $ fromEnum index + fromEnum i - 1) metadata
+    | otherwise -> subject
+
+substituteTerm :: (Ord i, Enum i) => i -> Term m v i -> Term m v i -> Term m v i
+substituteTerm index replacement' subject =
+  case subject of
+    Type metadata -> Type metadata
+    Application metadata argument function ->
+      Application metadata (substituteTerm index replacement' argument)
+      (substituteTerm index replacement' function)
+    Abstraction variable metadata parameter body ->
+      Abstraction variable metadata (substituteTerm index replacement' parameter)
+      (substituteTerm (succ index) replacement' body)
+    Variable variable index' metadata
+      | index' >  index -> Variable variable (pred index') metadata
+      | index' == index -> updateTerm index (toEnum 0) replacement'
+      | index' <  index -> subject
+
+substituteKind :: (Ord i, Enum i) => i -> Term m v i -> Kind m v i -> Kind m v i
+substituteKind index replacement' subject = case subject of
+  Kind metadata -> Kind metadata
+  Function variable metadata parameter body ->
+    Function variable metadata (substituteTerm index replacement' parameter)
+                                           (substituteKind (succ index) replacement' body)
+
+whnf :: (Ord i, Enum i) => Term m v i -> Term m v i
+whnf reduct =
+  case reduct of
+    Application metadata argument function ->
+      case whnf function of
+        Abstraction _ _ _ body ->
+          whnf $ substituteTerm (toEnum 1) argument body
+        f@_ -> Application metadata argument f
+    reduct'@_ -> reduct'
+
+nfTerm :: (Enum i, Ord i) => Term m v i -> Term m v i
+nfTerm reduct =
+  case reduct of
+    Abstraction variable metadata parameter body ->
+      let parameter' = nfTerm parameter
+          body' = parameter' `par` nfTerm body
+      in Abstraction variable metadata parameter' body'
+    Application metadata argument function ->
+      case whnf function of
+        Abstraction _ _ _ body ->
+          let arg = nfTerm argument
+              bod = arg `seq` substituteTerm (toEnum 1) arg (nfTerm body)
+          in nfTerm bod
+        f@_ -> Application metadata (nfTerm argument) (nfTerm f)
+    _ -> reduct
+
+nfKind :: (Enum i, Ord i) => Kind m v i -> Kind m v i
+nfKind reduct =
+  case reduct of
+    Kind metadata -> Kind metadata
+    Function variable metadata parameter body ->
+      let param = nfTerm parameter
+          body' = param `par` nfKind body
+      in Function variable metadata param body'
+
+instance (Enum i, Ord i, Eq v) => Eq (Term m v i) where
+  Type _ == Type _ = True
+  Variable variable index _ == Variable variable' index' _ = variable == variable' && index == index'
+  Application _ argument function == Application _ argument' function' =
+    let ftest = function == function'
+        atest = ftest `par` argument == argument'
+    in ftest && atest
+  Abstraction variable metadata parameter body == Abstraction _ _ parameter' body' =
+    let ptest = parameter == parameter'
+        var   = Variable variable (toEnum 1) metadata
+        btest = ptest `par` body == substituteTerm (toEnum 1) var body'
+    in ptest && btest
+  _ == _ = False
+
+instance (Enum i, Ord i, Eq v, Eq i) => Eq (Kind m v i) where
+  Kind _ == Kind _ = True
+  Function variable metadata parameter body == Function _ _ parameter' body' =
+    let ptest = parameter == parameter'
+        var   = Variable variable (toEnum 1) metadata
+        btest = ptest `par` body == substituteKind (toEnum 1) var body'
+    in ptest && btest
+  _ == _ = False
+
+infix 4 ===
+class (Enum i, Ord i, Eq i, Eq v) => BetaEq t v i where
+  (===) :: (Enum i, Ord i, Eq i, Eq v) => t v i -> t v i -> Bool
+
+instance (Enum i, Ord i, Eq i, Eq v) => BetaEq (Term m) v i where
+  a === b = nfTerm a == nfTerm b
+
+instance (Enum i, Ord i, Eq i, Eq v) => BetaEq (Kind m) v i where
+  a === b = nfKind a == nfKind b
+
+instance (Enum i, Ord i, Eq i, Eq v) => BetaEq (PseudoTerm m) v i where
+  Term a === Term b = nfTerm a == nfTerm b
+  Kind' a === Kind' b = nfKind a == nfKind b
+  _ === _ = False
+
+
+
+
+data PseudoTerm m v i = Term (Term m v i)
+                    | Kind' (Kind m v i)
+
+type Context m v i = [Term m v i]
+
+type Judgement m v i a = ReaderT (Context m v i) (Either String) a
+
+typeSynth :: (Show v, Enum i) => Term SourcePos v i -> Judgement SourcePos v i (PseudoTerm SourcePos v i)
+typeSynth term' =
+  case term' of
+    Type metadata -> return $ Kind' (Kind metadata)
+    Variable variable index position -> do
+      context <- ask
+      if Prelude.length context <= fromEnum index - 1 then
+        throwError $ "invalid variable encountered during type synthesis: "
+          ++ show variable ++ "\nat " ++ show position
+        else return $ Term $ context !! (fromEnum index - 1)
+    Application position argument function -> do
+      function' <- typeSynth function
+      case function' of
+        Term f -> return $ Term $ Application position argument f
+        Kind' _ -> throwError $ "invalid kind constructed during type synthesis"
+          ++ "\nat "  ++ show position
+    Abstraction variable position parameter body -> do
+      body' <- local (parameter:) (typeSynth body)
+      case body' of
+        Term b -> return $ Term $ Abstraction variable position parameter b
+        Kind' b -> return $ Kind' $ Function variable position parameter b
+
+fTypeSynth :: (Show v, Enum i) => Term SourcePos v i -> Judgement SourcePos v i (PseudoTerm SourcePos v i)
+fTypeSynth t = do
+  typ <- typeSynth t
+  case typ of
+    Term t' -> fTypeSynth t'
+    Kind' _ -> return typ
+
+termCorrect :: (Enum i, Show v, BetaEq (PseudoTerm SourcePos) v i) => Term SourcePos v i -> Judgement SourcePos v i ()
+termCorrect t = case t of
+  Type _ -> return ()
+  Variable{} ->
+    void (typeSynth t)
+  Abstraction _ _ parameter body -> do
+    termCorrect parameter
+    local (parameter:) (termCorrect body)
+  Application pos argument function -> do
+    argType <- typeSynth argument
+    termCorrect argument
+    Term funType <- fTypeSynth function
+    case nfTerm funType of
+      Abstraction _ _ parameter body ->
+        if Term parameter === argType then
+          termCorrect (nfTerm $ substituteTerm (toEnum 1) argument body)
+        else
+          let argPosition = show $ getNodeMetadata (Term argument)
+              parPosition = show $ getNodeMetadata (Term parameter)
+          in throwError $ "argument type and function parameter do not match: \n"
+                ++ "at " ++ argPosition ++ " with argument type of:   " ++ show argType ++ "\n"
+                ++ "at " ++ parPosition ++ " with parameter value of: " ++ show parameter ++ "\n"
+      e@_ -> throwError $ "attempted application onto non function type at "
+                ++ show pos ++ "\nwith type: " ++ show e
+
+
+
+
+
+lineComment, blockComment, spaceToken :: Parser ()
+lineComment = Lexer.skipLineComment "--" <|> Lexer.skipLineComment "#"
+blockComment = Lexer.skipBlockComment "{-" "-}"
+spaceToken = Lexer.space (void spaceChar) lineComment blockComment
+
+lexeme :: Parser a -> Parser a
+lexeme = Lexer.lexeme spaceToken
+
+symbol :: String -> Parser String
+symbol = Lexer.symbol spaceToken
+
+variableToken :: Parser Text
+variableToken = lexeme =<<
+  return . pack <$> ((:) <$> (letterChar <|> Text.Megaparsec.char '$') <*> many alphaNumChar)
+
+commaToken, colonToken, typeToken :: Parser ()
+commaToken = void (symbol ",")
+colonToken = void (symbol ":")
+typeToken  = void (symbol "type")
+
+parensToken, bracketsToken :: Parser a -> Parser a
+parensToken   = between (symbol "(") (symbol ")")
+bracketsToken = between (symbol "[") (symbol "]")
+
+vector :: Parser [Term SourcePos Text Word64]
+vector = sepBy1 term commaToken
+
+telescope :: Parser [([(Text, SourcePos)], Term SourcePos Text Word64)]
+telescope = some ((,) <$> sepBy ((,) <$> variableToken <*> getPosition) commaToken <*> (colonToken >> term))
+
+term :: Parser (Term SourcePos Text Word64)
+term =   (Type <$> (typeToken >> getPosition) <?> "type")
+     <|> try (Variable <$> variableToken <*> return 0 <*> getPosition <?> "variable")
+     <|> (apply <$> parensToken vector <*> term <?> "application")
+     <|> (funct <$> bracketsToken telescope <*> term <?> "abstraction")
+
+apply :: [Term SourcePos v i] -> Term SourcePos v i -> Term SourcePos v i
+apply = flip $ foldl (\f a -> Application (getNodeMetadata (Term a)) a f)
+
+funct :: [([(Text, SourcePos)], Term SourcePos Text Word64)] -> Term SourcePos Text Word64 -> Term SourcePos Text Word64
+funct = flip $ foldr $ \(ns, typ) bod -> foldr (\(n, p) -> Abstraction n p typ . bindTerm n 1) bod ns
+
+parseString :: String -> Text -> Either String (Term SourcePos Text Word64)
+parseString filename' input = case parse term filename' input of
+  Left err -> Left $ show err
+  Right val -> Right val
+
+parseInput :: Text -> Either String (Term SourcePos Text Word64)
+parseInput = parseString "stdin"
+
+
+
+
+
+getNodeMetadata :: PseudoTerm m v i -> m
+getNodeMetadata node = case node of
+  Term term' -> case term' of
+    Type metadata -> metadata
+    Variable _ _ metadata -> metadata
+    Abstraction _ metadata _ _ -> metadata
+    Application metadata _ _ -> metadata
+  Kind' kind -> case kind of
+    Kind metadata -> metadata
+    Function _ metadata _ _ -> metadata
+
+prettyKind :: Show v => Kind m v i -> Doc
+prettyKind kind = case kind of
+  Kind _ -> text "kind"
+  Function variable _ parameter body ->
+    let (args, bod) = collectAbstr [(variable, parameter)] body
+        argsDoc = list $ fmap (\(n, t) -> text (show n) <> colon <+> prettyTerm t) args
+        funDoc = argsDoc `par` prettyKind bod
+
+        collectAbstr args' (Function v _ t b) = collectAbstr (args' ++ [(v, t)]) b
+        collectAbstr args' fun = (args', fun)
+    in argsDoc </> funDoc
+
+prettyTerm :: Show v => Term m v i -> Doc
+prettyTerm term' = case term' of
+  Type _ -> text "type"
+  Variable variable _ _ -> text $ show variable
+  Application _ arg fun ->
+    let (args, fun') = collectApply [arg] fun
+        argsDoc = tupled $ map prettyTerm args
+        funDoc = argsDoc `par` prettyTerm fun'
+
+        collectApply args' (Application _ arg' fun'') = collectApply (args' ++ [arg']) fun''
+        collectApply args' fun'' = (args', fun'')
+    in argsDoc </> funDoc
+  Abstraction var _ typ bod ->
+    let (args, bod') = collectAbstr [(var, typ)] bod
+        argsDoc = list $ fmap (\(n, t) -> text (show n) <> colon <+> prettyTerm t) args
+        funDoc = argsDoc `par` prettyTerm bod'
+
+        collectAbstr args' (Abstraction v _ t b) = collectAbstr (args' ++ [(v, t)]) b
+        collectAbstr args' fun = (args', fun)
+    in argsDoc </> funDoc
+
+instance Show v => Show (Term m v i) where
+  showsPrec _ term' = displayS $ renderPretty 0.4 100 $ prettyTerm term'
+
+instance Show v => Show (Kind m v i) where
+  showsPrec _ kind = displayS $ renderPretty 0.4 100 $ prettyKind kind
+
+instance (Show v) => Show (PseudoTerm m v i) where
+  show p = case p of
+    Term t -> show t
+    Kind' k -> show k
+
+
+
+data ReplOptions = ReplOptions
+  { interactive  :: Bool
+  , writeHistory :: Bool
+  , historyFileN :: String
+  , noHelpPrompt :: Bool
+  }
+
+data FileOptions = FileOptions
+  { usePreprocessor     :: Bool
+  , compileToByteCode   :: Bool
+  , saveMetadata        :: Bool
+  , preprocessorOptions :: [String]
+  }
+
+data MainOptions = MainOptions
+  { inFile              :: String
+  , echoType            :: Bool
+  , useExtension        :: [String]
+  , replOptions         :: ReplOptions
+  , fileOptions         :: FileOptions
+  }
+
+fileGroup :: Maybe Group
+fileGroup = Just $ Options.group "file" "file commands" "commands that only affect files"
+
+replGroup :: Maybe Group
+replGroup = Just $ Options.group "repl" "repl commands" "commands that only affect the repl"
+
+fileAndReplGroup :: Maybe Group
+fileAndReplGroup = Just $ Options.group "file-and-repl" "file and repl commands"
+  "commands that both the file compiler and the repl interpreter share"
+
+instance Options ReplOptions where
+  defineOptions = pure ReplOptions
+    <*> defineOption optionType_bool (\o -> o
+          { optionLongFlags = ["interactive"]
+          , optionDefault = False
+          , optionShortFlags = ['n']
+          , optionDescription = "start repl"
+          , optionGroup = replGroup
+          })
+    
+    <*> defineOption optionType_bool (\o -> o
+          { optionLongFlags = ["write-history"]
+          , optionDefault = True
+          , optionShortFlags = ['w']
+          , optionDescription = "enable writing to the history file"
+          , optionGroup = replGroup
+          })
+    
+    <*> defineOption optionType_string (\o -> o
+          { optionLongFlags = ["history-file"]
+          , optionDefault = "~/.delta-lambda"
+          , optionShortFlags = ['f']
+          , optionDescription = "set the history file name and location"
+          , optionGroup = replGroup
+          })
+
+    <*> defineOption optionType_bool (\o -> o
+          { optionLongFlags = ["no-help-prompt"]
+          , optionDefault = False
+          , optionShortFlags = ['k']
+          , optionDescription = "dont issue help prompt on initial repl load"
+          , optionGroup = replGroup
+          })
+
+instance Options FileOptions where
+  defineOptions = pure FileOptions
+    <*> defineOption optionType_bool (\o -> o
+          { optionLongFlags = ["use-preprocessor"]
+          , optionDefault = True
+          , optionShortFlags = ['p']
+          , optionDescription = "enable the preprocessor"
+          , optionGroup = fileGroup
+          })
+    <*> defineOption optionType_bool (\o -> o
+          { optionLongFlags = ["compile"]
+          , optionDefault = False
+          , optionShortFlags = ['o']
+          , optionDescription = "enable compilation to bytecode"
+          , optionGroup = fileGroup
+          })
+    <*> defineOption optionType_bool (\o -> o
+          { optionLongFlags = ["without-metadata"]
+          , optionDefault = False
+          , optionShortFlags = ['s']
+          , optionDescription = "save metadata during compilation to bytecode"
+          , optionGroup = fileGroup
+          })
+    <*> defineOption (optionType_list ',' optionType_string) (\o -> o
+          { optionLongFlags = ["preprocessor-flags"]
+          , optionDefault = []
+          , optionShortFlags = ['c']
+          , optionDescription = "passes the proceeding flags to the preprocessor"
+          , optionGroup = fileGroup
+          })
+
+instance Options MainOptions where
+  defineOptions = pure MainOptions
+    <*> defineOption optionType_string (\o -> o
+          { optionLongFlags = ["in-file"]
+          , optionDefault = "stdin"
+          , optionShortFlags = ['i']
+          , optionDescription =
+              "input file usable extension must be one of "
+              ++ "(*.dl, *.cdl). note that if the \"-n\""
+              ++ " or \"--interactive\" flags are not used"
+              ++ " in combination with this option, the compiler"
+              ++ " will not load the file."
+          , optionGroup = fileAndReplGroup
+          })
+    <*> defineOption optionType_bool (\o -> o
+          { optionLongFlags = ["echo-type"]
+          , optionDefault = True
+          , optionShortFlags = ['e']
+          , optionDescription = "enable echoing the type of a term after checking"
+          , optionGroup = fileAndReplGroup
+          })
+    <*> defineOption (optionType_list ',' optionType_string) (\o -> o
+          { optionLongFlags = ["use-extensions"]
+          , optionDefault = []
+          , optionShortFlags = ['x']
+          , optionDescription =
+              "enables a set of extensions"
+          , optionGroup = fileAndReplGroup
+          })
+    <*> defineOptions
+    <*> defineOptions
+    
+version :: Version
+version = Version
+  { versionBranch = [0,1,0,0]
+  , versionTags = [] -- depreciated, but showVersion throws an exception without it
+  }
+
+replPrompt :: Version -> String
+replPrompt vers = Prelude.unlines
+  [ "    /\\         /\\"
+  , "   /  \\       /  \\"
+  , "  / /\\ \\     / /\\ \\"
+  , " / /__\\ \\   / /  \\ \\"
+  , "/________\\ /_/    \\_\\"
+  , "Welcome to Delta-Lambda, the 1000 line[s of haskell] theorem prover!"
+  , "This is apha level software! no documentation currently, and dragons galore!"
+  , "version: " ++ showVersion vers
+  ]
+
+helpPrompt :: String
+helpPrompt = Prelude.unlines
+  [ "/-----------------------------------------------------------------------------\\"
+  , "| command | parameters | description                                          |"
+  , "| :c      | input term | check that the input term is correct                 |"
+  , "| :e      | posn, term | add a term to the context at the position            |"
+  , "| :f      | input term | provide the final type of the input term             |"
+  , "| :g      | position   | get the type of a term name (or position) in context |"
+  , "| :h      |            | display this table                                   |"
+  , "| :o      | file name  | open a file and load it                              |"
+  , "| :q      |            | quit this repl                                       |"
+  , "| :r      | input term | provide the normal form of the input term            |"
+  , "| :t      | input term | provide the type of the input term                   |"
+  , "| :s      | input flag | set a flag, restart the repl                         |"
+  , "| :?      |            | syntax and semantics tutorial (not implemented)      |"
+  , "\\-----------------------------------------------------------------------------/"
+  ]
+
+data ReplState = ReplState
+  { replContext :: Context SourcePos Text Word64
+  , replTerm    :: Maybe (Term SourcePos Text Word64)
+  , replOpts    :: MainOptions
+  }
+
+main :: IO ()
+main = runCommand $ \opts _ ->
+  if interactive $ replOptions opts then
+    repl opts
+  else
+    if takeExtension (inFile opts) == ".dl" then
+      withFile (inFile opts) ReadMode $ parseCheckAndType opts
+    else
+      if takeExtension (inFile opts) == ".cdl" then
+        putStrLn . pack $ "cannot open binary file in non interactive mode!"
+      else
+        putStrLn . pack $ "extension not recognized: " ++ takeExtension (inFile opts)
+
+preprocess :: MainOptions -> Text -> IO (Either String Text)
+preprocess options fileContents =
+  if usePreprocessor $ fileOptions options then
+    case Language.Preprocessor.Cpphs.parseOptions (preprocessorOptions $ fileOptions options) of
+      Left err -> return $ Left err
+      Right cpphsOpts -> do
+        fileContents' <- runCpphs cpphsOpts (inFile options) (unpack fileContents)
+        return $ Right $ pack fileContents'
+  else return $ Right fileContents
+
+compile :: (Serialize m , Serialize v, Serialize i) => Term m v i -> MainOptions -> IO ()
+compile val options
+  | not (saveMetadata $ fileOptions options) = Data.ByteString.writeFile compiledFilename (encode file)
+  | otherwise =  Data.ByteString.writeFile compiledFilename (encode cleaned)
+  where header = DecompiledFileHeader
+          { compiledFileName = pack $ inFile options
+          , interpreterVersion = version
+          , extensionsUsed = map pack $ useExtension options
+          }
+        
+        file = DecompiledFile
+          { decompiledFileHeader = header
+          , decompiledTerm = val
+          }
+
+        cleaned = transpile (const ()) id id file
+        
+        compiledFilename = dropExtension (inFile options) -<.> ".cdl"
+      
+
+checkAndType :: (Enum i, Show v, BetaEq (PseudoTerm SourcePos) v i) => Term SourcePos v i -> MainOptions -> Context SourcePos v i -> IO (Maybe ())
+checkAndType term options context =
+  case runReaderT (termCorrect term) context of
+    Left err -> do
+      putStrLn $ pack err
+      return Nothing
+    Right _
+      | echoType options ->
+        case runReaderT (typeSynth term) context of
+          Left err -> do
+            putStrLn $ pack err
+            return Nothing
+          Right val -> do
+            putStrLn . pack $ show val
+            return $ Just ()
+      | otherwise -> do
+          return $ Just ()
+
+parseCheckAndType :: MainOptions -> Handle -> IO ()
+parseCheckAndType options file = do
+  input <- Data.Text.IO.hGetContents file
+  input' <- preprocess options input
+  case input' of
+    Left pperr -> putStrLn $ pack pperr
+    Right ppval ->
+      case parseInput ppval of
+        Left perr -> putStrLn $ pack perr
+        Right pval -> do
+          checked <- checkAndType pval options []
+          case checked of
+            Nothing -> return ()
+            Just _ -> 
+              if compileToByteCode $ fileOptions options then
+                compile pval options
+              else
+                return ()
+
+repl :: MainOptions -> IO ()
+repl options = do
+  Data.Text.IO.putStr $ pack (replPrompt version)
+  when (not (noHelpPrompt (replOptions options))) $ Data.Text.IO.putStr (pack helpPrompt)
+  if inFile options == "stdin" then
+    runInputT replSettings $ loop (initReplState Nothing options)
+    else
+    if takeExtension (inFile options) == ".dl" then do
+      withFile (inFile options) ReadWriteMode $ \h -> do
+        input <- Data.Text.IO.hGetContents h
+        input' <- preprocess options input
+        case input' of
+          Left pperr -> putStrLn $ pack pperr
+          Right ppval ->
+            case parseInput ppval of
+              Left perr -> putStrLn $ pack perr
+              Right pval -> do
+                checked <- checkAndType pval options []
+                case checked of
+                  Nothing -> return ()
+                  Just _ -> runInputT replSettings $ loop (initReplState (Just pval) options)
+    else
+      if takeExtension (inFile options) == ".cdl" then do
+        fileCont <- Data.ByteString.readFile (inFile options)
+        case decode fileCont :: Either String (DecompiledFile SourcePos Text Word64) of
+          Left perr -> putStrLn $ pack perr
+          Right pval -> do
+            let fvers = interpreterVersion (decompiledFileHeader pval)
+            if fvers < version then
+              putStrLn . pack $ "cannot load file \"" ++ inFile options ++ "\n" ++
+              "compiler version of file:   " ++ showVersion fvers ++ "\n" ++
+              "compiler version of system: " ++ showVersion version
+              else do
+                let val = decompiledTerm pval
+                runInputT replSettings $ loop (initReplState (Just val) options)
+      else
+        putStrLn . pack $ "extension not recognized: " ++ takeExtension (inFile options)
+              
+  where replSettings = defaultSettings
+          { historyFile = Just $ historyFileN (replOptions options)
+          , autoAddHistory = writeHistory (replOptions options)
+          }
+
+initReplState term options = ReplState
+  { replContext = []
+  , replTerm = term
+  , replOpts = options
+  }
+
+loop :: ReplState -> InputT IO ()
+loop state = do
+  let count = Prelude.length (replContext state)
+  input <- getInputLine $ if count == 0 then "|- " else show count ++ " |- "
+  case input of
+    Nothing -> loop state
+    Just (':':'c':' ':rest) -> do
+      case parseInput (pack rest) of
+        Left perr -> do
+          outputStrLn perr
+          loop state
+        Right pval -> do
+          lift $ checkAndType pval (replOpts state) (replContext state)
+          loop state
+    Just (':':'e':' ':rest) -> do
+      let positionStr = takeWhile (\x -> not (isSpace x) && isNumber x) rest
+      let termStr = dropWhile (\x -> not (isSpace x) && isNumber x) rest
+      if null positionStr then do
+        outputStrLn "please enter a non-negative number"
+        loop state
+        else do
+          let position :: Int = read positionStr
+          case parseInput $ pack termStr of
+            Left perr -> do
+              outputStrLn perr
+              loop state
+            Right pval -> do
+              checked <- lift $ checkAndType pval (replOpts state) (replContext state)
+              case checked of
+                Nothing -> loop state
+                Just _ -> do
+                  let (before, after) = splitAt position (replContext state)
+                  let pval' = bindContext (replContext state) 1 pval
+                  loop (state { replContext = before ++ [pval'] ++ after })
+              
+    Just (':':'f':' ':rest) ->
+      case parseInput (pack rest) of
+        Left perr -> do
+          outputStrLn perr
+          loop state
+        Right pval -> do
+          checked <- lift $ checkAndType pval (replOpts state) (replContext state)
+          case checked of
+            Nothing -> loop state
+            Just _ ->
+              case runReaderT (fTypeSynth pval) (replContext state) of
+                Left err -> do
+                  outputStrLn err
+                  loop state
+                Right val -> do
+                  outputStrLn $ show val
+                  loop state
+    Just (':':'g':' ':rest) -> do
+      let positionStr = takeWhile (\x -> not (isSpace x) && isNumber x) rest
+      if null positionStr then do
+        outputStrLn "please enter a non-negative number"
+        loop state
+        else do
+          let position :: Int = read positionStr
+          if position > Prelude.length (replContext state) then do
+            outputStrLn "position of term in context cannot be outside of context"
+            loop state
+            else do
+            let term = (replContext state) !! (position - 1)
+            outputStrLn $ show term
+            loop state
+    Just (':':'h':       _) -> do
+      outputStrLn helpPrompt
+      loop state
+    Just (':':'o':' ':rest) -> do
+      if takeExtension rest == ".dl" then do
+        loaded <- lift $ withFile rest ReadWriteMode $ \h -> do
+          input <- Data.Text.IO.hGetContents h
+          input' <- preprocess (replOpts state) input
+          case input' of
+            Left pperr -> do
+              putStrLn $ pack pperr
+              return Nothing
+            Right ppval ->
+              case parseInput ppval of
+                Left perr -> do
+                  putStrLn $ pack perr
+                  return Nothing
+                Right pval -> do
+                  checked <- checkAndType pval (replOpts state) []
+                  case checked of
+                    Nothing -> return Nothing
+                    Just _ -> return $ Just pval
+        case loaded of
+          Nothing -> loop state
+          Just val -> loop (state{ replTerm = Just val, replContext = [] })
+        else
+        if takeExtension rest == ".cdl" then do
+          fileCont <- lift $ Data.ByteString.readFile rest
+          case decode fileCont :: Either String (DecompiledFile SourcePos Text Word64) of
+            Left perr -> do
+              outputStrLn perr
+              loop state
+            Right pval -> do
+              let fvers = interpreterVersion (decompiledFileHeader pval)
+              if fvers < version then do
+                outputStrLn $ "cannot load file \"" ++ rest ++ "\n" ++
+                  "compiler version of file:   " ++ showVersion fvers ++ "\n" ++
+                  "compiler version of system: " ++ showVersion version
+                loop state
+                else do
+                  let val = decompiledTerm pval
+                  loop (state { replTerm = Just val, replContext = [] })
+        else do
+          outputStrLn $ "extension not recognized: " ++ rest
+          loop state
+    Just (':':'q':       _) -> return ()    
+    Just (':':'r':' ':rest) ->
+      case parseInput (pack rest) of
+        Left perr -> do
+          outputStrLn perr
+          loop state
+        Right pval -> do
+          checked <- lift $ checkAndType pval (replOpts state) (replContext state)
+          case checked of
+            Nothing -> loop state
+            Just _ -> do
+              outputStrLn $ show . nfTerm $ pval
+              loop state
+    Just (':':'t':' ':rest) -> 
+      case parseInput (pack rest) of
+        Left perr -> do
+          outputStrLn perr
+          loop state
+        Right pval -> do
+          checked <- lift $ checkAndType pval (replOpts state) (replContext state)
+          case checked of
+            Nothing -> loop state
+            Just _ ->
+              case runReaderT (typeSynth pval) (replContext state) of
+                Left err -> do
+                  outputStrLn err
+                  loop state
+                Right val -> do
+                  outputStrLn $ show val
+                  loop state
+    Just (':':'s':' ':rest) -> do
+      let pOpts = Options.parseOptions (split rest " ")
+      case parsedOptions pOpts of
+        Nothing -> do
+          case parsedError pOpts of
+            Nothing -> do
+              outputStrLn $ "an unknow error occured during proccessing of the options: "
+                ++ "\n" ++ rest
+              loop state
+            Just err -> do
+              outputStrLn err
+              loop state
+        Just opts -> loop (state {replOpts = opts})
+    Just (':':'?':_) -> do
+      outputStrLn "the turorial is under construction!"
+      loop state
+    Just input -> do
+      outputStrLn $ "input : " ++ input ++ "\n not recognised"
+      loop state
+
+split :: String -> String -> [String]
+split str pat = helper str pat [] [] where 
+    helper :: String -> String -> String -> String -> [String]
+    helper [] _  n _ = [n] ++ []
+    helper xs [] n _ = [n] ++ (split xs pat)
+    helper (x:xs) (y:ys) n m
+        | x /= y = helper (xs) pat ((n++m)++[x]) m
+        | otherwise = helper xs ys n (m++[y])