diff --git a/frontend/package.yaml b/frontend/package.yaml
index 3c138597f..ddc9fc1a3 100644
--- a/frontend/package.yaml
+++ b/frontend/package.yaml
@@ -88,7 +88,6 @@ library:
   - Glob
   - filepath
   - bifunctors
-  - raw-strings-qq
   - text-replace
   - directory
   - syb >=0.6
@@ -97,6 +96,8 @@ library:
   - split
   - logict >= 0.7.1.0
   - clock
+  - algebraic-graphs
+  - template-haskell
 
 tests:
   frontend-spec:
diff --git a/frontend/src/Language/Granule/Checker/Checker.hs b/frontend/src/Language/Granule/Checker/Checker.hs
index 06efa6386..fa252ff7e 100644
--- a/frontend/src/Language/Granule/Checker/Checker.hs
+++ b/frontend/src/Language/Granule/Checker/Checker.hs
@@ -7,6 +7,7 @@
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeApplications #-}
 
 {-# options_ghc -fno-warn-incomplete-uni-patterns -Wno-deprecations #-}
 
@@ -46,9 +47,9 @@ import Language.Granule.Checker.TypeAliases
 import Language.Granule.Checker.Variables
 import Language.Granule.Context
 
-import Language.Granule.Syntax.Identifiers
 import Language.Granule.Syntax.Helpers (freeVars, hasHole)
 import Language.Granule.Syntax.Def
+import Language.Granule.Syntax.Program
 import Language.Granule.Syntax.Expr
 import Language.Granule.Syntax.Pattern (Pattern(..))
 import Language.Granule.Syntax.Pretty
@@ -61,16 +62,20 @@ import qualified Language.Granule.Synthesis.Synth as Syn
 
 import Language.Granule.Utils
 
+import Debug.Trace
+import System.Directory (getModificationTime)
+import Control.Exception (try, SomeException)
+
 -- Checking (top-level)
 check :: (?globals :: Globals)
-  => AST () ()
+  => Module
   -> IO (Either (NonEmpty CheckerError) (AST () Type, [Def () ()]))
-check ast@(AST _ _ _ hidden _) = do
-  evalChecker (initState { allHiddenNames = hidden }) $ (do
-      ast@(AST dataDecls defs imports hidden name) <- return $ replaceTypeAliases ast
+check mod@Mod{ moduleAST = ast, moduleHiddenNames = hidden } = do
+  evalChecker (initState { allHiddenNames = hidden }) $ do
+      ast <- return $ replaceTypeAliases ast
       _    <- checkNameClashes ast
-      _    <- runAll checkTyCon (Primitives.dataTypes ++ dataDecls)
-      _    <- runAll checkDataCons (Primitives.dataTypes ++ dataDecls)
+      _    <- runAll checkTyCon (Primitives.dataTypes ++ dataTypes ast)
+      _    <- runAll checkDataCons (Primitives.dataTypes ++ dataTypes ast)
       debugM "extensions" (show $ globalsExtensions ?globals)
       debugM "check" "kindCheckDef"
       defs <- runAll kindCheckDef defs
@@ -79,63 +84,67 @@ check ast@(AST _ _ _ hidden _) = do
       -- Add on any definitions computed by the type checker (derived)
       st <- get
       let derivedDefs = map (snd . snd) (derivedDefinitions st)
-      pure $ (AST dataDecls defs imports hidden name, derivedDefs))
+      -- traceM $ show $ AST dataDecls defs imports hidden name
+      -- traceM $ show derivedDefs
+      pure (AST dataDecls defs imports hidden name, derivedDefs)
 
--- Synthing the type of a single expression in the context of an asy
+-- Synthing the type of a single expression in the context of a Module
 synthExprInIsolation :: (?globals :: Globals)
-  => AST () ()
+  => Module
   -> Expr () ()
   -> IO (Either (NonEmpty CheckerError) (Either (TypeScheme , [Def () ()]) Type))
-synthExprInIsolation ast@(AST dataDecls defs imports hidden name) expr =
-  evalChecker (initState { allHiddenNames = hidden }) $ do
-      _    <- checkNameClashes ast
-      _    <- runAll checkTyCon (Primitives.dataTypes ++ dataDecls)
-      _    <- runAll checkDataCons (Primitives.dataTypes ++ dataDecls)
-      defs <- runAll kindCheckDef defs
-
-      let defCtxt = map (\(Def _ name _ _ tys) -> (name, tys)) defs
-
-      -- also check the defs
-      defs <- runAll (checkDef defCtxt) defs
-
-      -- Since we need to return a type scheme, have a look first
-      -- for top-level identifiers with their schemes
-      case expr of
-        -- Lookup in data constructors
-        (Val s _ _ (Constr _ c [])) -> do
-          mConstructor <- lookupDataConstructor s c
-          case mConstructor of
-            Just (tySch, _) -> return $ Left (tySch, [])
-            Nothing -> do
-              st <- get
-              -- Or see if this is a kind constructors
-              case lookup c (typeConstructors st) of
-                Just (k, _, _) -> return $ Right k
-                Nothing -> throw UnboundDataConstructor{ errLoc = s, errId = c }
-
-        -- Lookup in definitions
-        (Val s _ _ (Var _ x)) -> do
-          case lookup x (defCtxt <> Primitives.builtins) of
-            Just tyScheme -> return $ Left (tyScheme, [])
-            Nothing -> throw UnboundVariableError{ errLoc = s, errId = x }
-
-        -- Otherwise, do synth
-        _ -> do
-          (ty, _, subst, _) <- synthExpr defCtxt [] Positive expr
-          --
-          -- Solve the generated constraints
-          checkerState <- get
-
-          let predicate = Conj $ predicateStack checkerState
-          predicate <- substitute subst predicate
-          solveConstraints predicate (getSpan expr) (mkId "grepl")
-
-
-          let derivedDefs = map (snd . snd) (derivedDefinitions checkerState)
-
-          -- Apply the outcoming substitution
-          ty' <- substitute subst ty
-          return $ Left (Forall nullSpanNoFile [] [] ty', derivedDefs)
+synthExprInIsolation
+  mod@Mod{ moduleAST = ast@AST{ dataTypes = dataDecls, definitions = defs } }
+  expr =
+    evalChecker (initState { allHiddenNames = moduleHiddenNames mod }) $ do
+        _    <- checkNameClashes ast
+        _    <- runAll checkTyCon (Primitives.dataTypes ++ dataDecls)
+        _    <- runAll checkDataCons (Primitives.dataTypes ++ dataDecls)
+        defs <- runAll kindCheckDef defs
+
+        let defCtxt = map (\(Def _ name _ _ tys) -> (name, tys)) defs
+
+        -- also check the defs
+        defs <- runAll (checkDef defCtxt) defs
+
+        -- Since we need to return a type scheme, have a look first
+        -- for top-level identifiers with their schemes
+        case expr of
+          -- Lookup in data constructors
+          (Val s _ _ (Constr _ c [])) -> do
+            mConstructor <- lookupDataConstructor s c
+            case mConstructor of
+              Just (tySch, _) -> return $ Left (tySch, [])
+              Nothing -> do
+                st <- get
+                -- Or see if this is a kind constructors
+                case lookup c (typeConstructors st) of
+                  Just (k, _, _) -> return $ Right k
+                  Nothing -> throw UnboundDataConstructor{ errLoc = s, errId = c }
+
+          -- Lookup in definitions
+          (Val s _ _ (Var _ x)) -> do
+            case lookup x (defCtxt <> Primitives.builtins) of
+              Just tyScheme -> return $ Left (tyScheme, [])
+              Nothing -> throw UnboundVariableError{ errLoc = s, errId = x }
+
+          -- Otherwise, do synth
+          _ -> do
+            (ty, _, subst, _) <- synthExpr defCtxt [] Positive expr
+            --
+            -- Solve the generated constraints
+            checkerState <- get
+
+            let predicate = Conj $ predicateStack checkerState
+            predicate <- substitute subst predicate
+            solveConstraints predicate (getSpan expr) (mkId "grepl")
+
+
+            let derivedDefs = map (snd . snd) (derivedDefinitions checkerState)
+
+            -- Apply the outcoming substitution
+            ty' <- substitute subst ty
+            return $ Left (Forall nullSpanNoFile [] [] ty', derivedDefs)
 
 -- TODO: we are checking for name clashes again here. Where is the best place
 -- to do this check?
@@ -303,6 +312,8 @@ checkDef defCtxt (Def s defName rf el@(EquationList _ _ _ equations)
     checkGuardsForImpossibility s defName
     checkGuardsForExhaustivity s defName ty equations
     let el' = el { equations = elaboratedEquations }
+    traceM "\n\n********\n"
+    traceM $ show $ Def s defName rf el' tys
     pure $ Def s defName rf el' tys
   where
     elaborateEquation :: Equation () () -> Checker (Equation () Type)
@@ -1984,6 +1995,11 @@ checkGuardsForImpossibility s name = do
     debugM "impossibility" $ "about to try" <> pretty thm
     -- Try to prove the theorem
     constructors <- allDataConstructorNames
+
+    -- traceM $ show (thm, tyVars, constructors)
+
+    _ <- liftIO $ try @SomeException $ getModificationTime ""
+
     (_, result) <- liftIO $ provePredicate thm tyVars constructors
 
     p <- simplifyPred thm
diff --git a/frontend/src/Language/Granule/Checker/Kinding.hs b/frontend/src/Language/Granule/Checker/Kinding.hs
index 5e34eb5e4..e23d76967 100644
--- a/frontend/src/Language/Granule/Checker/Kinding.hs
+++ b/frontend/src/Language/Granule/Checker/Kinding.hs
@@ -19,7 +19,6 @@ import Data.Maybe (fromMaybe)
 import Language.Granule.Context
 
 import Language.Granule.Syntax.Def
-import Language.Granule.Syntax.Identifiers
 import Language.Granule.Syntax.Pretty
 import Language.Granule.Syntax.Span
 import Language.Granule.Syntax.Type
diff --git a/frontend/src/Language/Granule/Checker/Monad.hs b/frontend/src/Language/Granule/Checker/Monad.hs
index beb11c750..6c4a77ef5 100644
--- a/frontend/src/Language/Granule/Checker/Monad.hs
+++ b/frontend/src/Language/Granule/Checker/Monad.hs
@@ -17,6 +17,7 @@ module Language.Granule.Checker.Monad where
 import Data.Maybe (mapMaybe)
 import Data.Either (partitionEithers)
 import Data.Foldable (toList)
+import Data.Functor ( ($>) )
 import Data.List (intercalate, transpose)
 import Data.List.NonEmpty (NonEmpty(..))
 import qualified Data.Map as M
@@ -32,10 +33,9 @@ import Language.Granule.Checker.Predicates
 import qualified Language.Granule.Checker.Primitives as Primitives
 import Language.Granule.Context
 
-import Language.Granule.Syntax.Def
+import Language.Granule.Syntax.Program
 import Language.Granule.Syntax.Expr (Operator, Expr)
 import Language.Granule.Syntax.Helpers (FreshenerState(..), freshen, Term(..))
-import Language.Granule.Syntax.Identifiers
 import Language.Granule.Syntax.Type
 import Language.Granule.Syntax.Pattern
 import Language.Granule.Syntax.Pretty
@@ -70,7 +70,7 @@ runAll f xs = do
   st <- get
   (results, st) <- liftIO $ runAllCheckers st (map f xs)
   case partitionEithers results of
-    ([], successes) -> put st *> pure successes
+    ([], successes) -> put st $> successes
     -- everything succeeded, so `put` the state and carry on
     (err:errs, _) -> throwError $ sconcat (err:|errs)
     -- combine all errors and fail
@@ -179,7 +179,7 @@ data CheckerState = CS
             , derivStack :: [Derivation]
 
             -- Names from modules which are hidden
-            , allHiddenNames :: M.Map Id Id
+            , allHiddenNames :: M.Map Id ModuleName
 
             -- The type of the current equation.
             , equationTy :: Maybe Type
@@ -230,7 +230,7 @@ lookupDataConstructor sp constrName = do
     Nothing -> return $ lookup constrName (dataConstructors st)
     Just mod ->
       -- If the constructor is hidden but we are inside that module...
-      if sourceName mod == takeBaseName (filename sp)
+      if mod == takeBaseName (filename sp)
         -- .. then its fine
         then return $ lookup constrName (dataConstructors st)
         -- Otheriwe this is truly hidden
diff --git a/frontend/src/Language/Granule/Checker/NameClash.hs b/frontend/src/Language/Granule/Checker/NameClash.hs
index e7dd060ae..8d73905ee 100644
--- a/frontend/src/Language/Granule/Checker/NameClash.hs
+++ b/frontend/src/Language/Granule/Checker/NameClash.hs
@@ -5,11 +5,10 @@ import Control.Monad.Except (throwError)
 import Data.List.NonEmpty (NonEmpty(..))
 import Language.Granule.Checker.Monad
 import Language.Granule.Syntax.Def
-import Language.Granule.Syntax.Identifiers
 import Language.Granule.Utils
 
 checkNameClashes :: AST () () -> Checker ()
-checkNameClashes (AST dataDecls defs _ _ _) =
+checkNameClashes AST{ dataTypes = dataDecls, definitions = defs } =
     case concat [typeConstructorErrs, dataConstructorErrs, defErrs] of
       [] -> pure ()
       (d:ds) -> throwError (d:|ds)
@@ -49,4 +48,4 @@ checkNameClashes (AST dataDecls defs _ _ _) =
           { errLoc = defSpan x2
           , errDef = x2
           , otherDefs = xs
-          }
\ No newline at end of file
+          }
diff --git a/frontend/src/Language/Granule/Checker/Primitives.hs b/frontend/src/Language/Granule/Checker/Primitives.hs
index cc5a9046b..552bf6fc5 100644
--- a/frontend/src/Language/Granule/Checker/Primitives.hs
+++ b/frontend/src/Language/Granule/Checker/Primitives.hs
@@ -9,11 +9,9 @@
 module Language.Granule.Checker.Primitives where
 
 import Data.List.NonEmpty (NonEmpty(..))
-import Text.RawString.QQ (r)
 
-import Language.Granule.Syntax.Def
-import Language.Granule.Syntax.Identifiers
-import Language.Granule.Syntax.Parser (parseDefs)
+import Language.Granule.Syntax.Def as Def
+import Language.Granule.Syntax.QuasiQuoter
 import Language.Granule.Syntax.Type
 import Language.Granule.Syntax.Span
 import Language.Granule.Syntax.Expr (Operator(..))
@@ -36,7 +34,7 @@ capabilities =
    [(mkId "Console", funTy (tyCon "String") (tyCon "()"))
   , (mkId "TimeDate", funTy (tyCon "()") (tyCon "String"))]
 
-    
+
 
 -- Associates type constuctors names to their:
 --    * kind
@@ -80,7 +78,7 @@ typeConstructors =
     , (mkId "One",      (tyCon "LNL", [], False))
     , (mkId "Many",     (tyCon "LNL", [], False))
     -- Security levels
-    
+
     -- Note that Private/Public can be members of Sec (and map to Hi/Lo) or if 'SecurityLevels' is
     -- turned on then they are part of the 'Level' semiring
     , (mkId "Private",  (extensionDependent [(SecurityLevels, tyCon "Level")] (tyCon "Sec"), [], False))
@@ -195,7 +193,7 @@ dataTypes =
           , dataConstrId = mkId "&"
           , dataConstrParams = [TyVar (mkId "a"), TyVar (mkId "b")]
          }]}
-    ] ++ builtinDataTypesParsed
+    ] ++ Def.dataTypes builtinAST
 
 binaryOperators :: Operator -> NonEmpty Type
 binaryOperators = \case
@@ -240,8 +238,8 @@ binaryOperators = \case
         , funTy (TyCon $ mkId "DFloat") (funTy (TyCon $ mkId "DFloat") (TyCon $ mkId "Bool"))]
 
 -- TODO make a proper quasi quoter that parses this at compile time
-builtinSrc :: String
-builtinSrc = [r|
+builtinAST :: AST () ()
+builtinAST = [gr|
 
 import Prelude
 
@@ -582,13 +580,13 @@ uniqueBind
   . (*a -> !b) -> !a -> !b
 uniqueBind = BUILTIN
 
-uniquePush 
-  : forall {a b : Type} 
+uniquePush
+  : forall {a b : Type}
   . *(a, b)  -> (*a, *b)
 uniquePush = BUILTIN
 
-uniquePull 
-  : forall {a b : Type} 
+uniquePull
+  : forall {a b : Type}
   . (*a, *b) -> *(a, b)
 uniquePull = BUILTIN
 
@@ -672,20 +670,12 @@ projR = BUILTIN
 
 |]
 
-
-builtinDataTypesParsed :: [DataDecl]
 builtins :: [(Id, TypeScheme)]
-(builtinDataTypesParsed, builtins) =
-  (types, map unDef defs)
-    where
-      AST types defs _ _ _ = case parseDefs "builtins" builtinSrc of
-        Right (ast, _) -> ast
-        Left err -> error err
+builtins = map unDef $ definitions builtinAST
 
-      unDef :: Def () () -> (Id, TypeScheme)
-      unDef (Def _ name _ _ (Forall _ bs cs t)) = (name, Forall nullSpanBuiltin bs cs t)
+unDef :: Def () () -> (Id, TypeScheme)
+unDef (Def _ name _ _ (Forall _ bs cs t)) = (name, Forall nullSpanBuiltin bs cs t)
 
 -- List of primitives that can't be promoted in CBV
 unpromotables :: [String]
 unpromotables = ["newFloatArray", "forkLinear", "forkLinear'", "forkMulticast", "forkReplicate", "forkReplicateExactly"]
-
diff --git a/frontend/src/Language/Granule/Checker/Substitution.hs b/frontend/src/Language/Granule/Checker/Substitution.hs
index 72b93d0bb..418e48bd9 100644
--- a/frontend/src/Language/Granule/Checker/Substitution.hs
+++ b/frontend/src/Language/Granule/Checker/Substitution.hs
@@ -30,7 +30,6 @@ import Language.Granule.Context
 import Language.Granule.Syntax.Def
 import Language.Granule.Syntax.Expr hiding (Substitutable)
 import Language.Granule.Syntax.Helpers hiding (freshIdentifierBase)
-import Language.Granule.Syntax.Identifiers
 import Language.Granule.Syntax.Pattern
 -- import Language.Granule.Syntax.Pretty
 import Language.Granule.Syntax.Span
@@ -371,7 +370,7 @@ substituteValue ctxt (PromoteF ty expr) =
 substituteValue ctxt (PureF ty expr) =
     do  ty' <- substitute ctxt ty
         return $ Pure ty' expr
-substituteValue ctxt (NecF ty expr) = 
+substituteValue ctxt (NecF ty expr) =
     do ty' <- substitute ctxt ty
        return $ Nec ty' expr
 substituteValue ctxt (ConstrF ty ident vs) =
diff --git a/frontend/src/Language/Granule/Checker/TypeAliases.hs b/frontend/src/Language/Granule/Checker/TypeAliases.hs
index 654535836..50e258c89 100644
--- a/frontend/src/Language/Granule/Checker/TypeAliases.hs
+++ b/frontend/src/Language/Granule/Checker/TypeAliases.hs
@@ -8,15 +8,12 @@ import Language.Granule.Checker.Primitives (typeAliases)
 import Data.Functor.Identity (runIdentity)
 
 replaceTypeAliases :: AST a b -> AST a b
-replaceTypeAliases (AST dataDecls defs imports hidden name) =
-  AST
-    (map replaceInDataDecl dataDecls)
-    (map replaceInDef defs)
-    imports hidden name
+replaceTypeAliases AST{ dataTypes = dtys, definitions = defs } =
+  AST{ dataTypes = map replaceInDataDecl dtys, definitions = map replaceInDef defs }
 
 replaceInDataDecl :: DataDecl -> DataDecl
 replaceInDataDecl (DataDecl s v tyVarContext kindAnn constrs) =
- DataDecl s v (map (\(id, t) -> (id, replaceInType t)) tyVarContext)
+ DataDecl s v (ctxtMap replaceInType tyVarContext)
    (replaceInMaybeType kindAnn)
    (map replaceInDataConstr constrs)
 
@@ -51,12 +48,12 @@ replaceInExpr (TryCatch s a b e1 p mt e2 e3) =
   TryCatch s a b (replaceInExpr e1) p (replaceInMaybeType mt) (replaceInExpr e2) (replaceInExpr e3)
 replaceInExpr (Val s a b v) = Val s a b v
 replaceInExpr (Case s a b e patsAndExprs) =
-  Case s a b (replaceInExpr e) (map (\(a, b) -> (a, replaceInExpr b)) patsAndExprs)
+  Case s a b (replaceInExpr e) (ctxtMap replaceInExpr patsAndExprs)
 replaceInExpr (Hole s a b ids) = Hole s a b ids
 
 replaceInTypeScheme :: TypeScheme -> TypeScheme
 replaceInTypeScheme (Forall s quants constraints t) =
-  Forall s (map (\(v, t) -> (v, replaceInType t)) quants)
+  Forall s (ctxtMap replaceInType quants)
     (map replaceInType constraints)
     (replaceInType t)
 
@@ -82,5 +79,3 @@ replaceInType =
       case lookup id typeAliases of
         Just ([], t)  -> t
         _             -> TyCon id
-
-
diff --git a/frontend/src/Language/Granule/Context.hs b/frontend/src/Language/Granule/Context.hs
index df4ed313e..6b3d43b73 100644
--- a/frontend/src/Language/Granule/Context.hs
+++ b/frontend/src/Language/Granule/Context.hs
@@ -6,6 +6,7 @@
 
 module Language.Granule.Context where
 
+import Control.Arrow ( Arrow(second) )
 import Data.Maybe (isJust)
 import Data.List (sortBy)
 import Language.Granule.Syntax.Identifiers (Id)
@@ -37,9 +38,8 @@ replace (x : ctxt) name v
   = x : replace ctxt name v
 
 -- | Map over the just elements of the context (and not the keys (identifiers))
-ctxtMap :: (a -> b) -> Ctxt a -> Ctxt b
-ctxtMap f [] = []
-ctxtMap f ((v, x):ctxt) = (v, f x) : ctxtMap f ctxt
+ctxtMap :: (b -> c) -> [(a, b)] -> [(a, c)]
+ctxtMap = map . second
 
 -- $setup
 -- >>> import Language.Granule.Syntax.Identifiers (mkId)
diff --git a/frontend/src/Language/Granule/Syntax/Def.hs b/frontend/src/Language/Granule/Syntax/Def.hs
index 97a3514a5..d9b0306af 100644
--- a/frontend/src/Language/Granule/Syntax/Def.hs
+++ b/frontend/src/Language/Granule/Syntax/Def.hs
@@ -8,24 +8,27 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE RecordWildCards #-}
 
-module Language.Granule.Syntax.Def where
+module Language.Granule.Syntax.Def
+  ( module Language.Granule.Syntax.Def
+  , module Reexport
+  )
+where
 
 import Data.List ((\\), delete)
-import Data.Set (Set)
-import qualified Data.Map as M
 import GHC.Generics (Generic)
 import Data.Data
 import qualified Text.Reprinter as Rp
 
-import Language.Granule.Context (Ctxt)
+import Language.Granule.Context as Reexport (Ctxt, ctxtMap)
 import Language.Granule.Syntax.FirstParameter
 import Language.Granule.Syntax.Helpers
-import Language.Granule.Syntax.Identifiers
+import Language.Granule.Syntax.Identifiers as Reexport
 import Language.Granule.Syntax.Span
 import Language.Granule.Syntax.Expr
 import Language.Granule.Syntax.Type
 import Language.Granule.Syntax.Pattern
 
+
 -- | Top-level ASTs
 -- | Comprise a list of data type declarations and a list
 -- | of expression definitions
@@ -34,11 +37,26 @@ data AST v a =
   AST
     { dataTypes :: [DataDecl]
     , definitions :: [Def v a]
-    , imports :: Set Import
-    , hiddenNames :: M.Map Id Id -- map from names to the module hiding them
-    , moduleName  :: Maybe Id
     }
 
+emptyAST :: AST v a
+emptyAST =
+  AST
+    { dataTypes = mempty
+    , definitions = mempty
+    }
+
+-- instance Semigroup (AST v a) where
+--   ast1 <> ast2 =
+--     AST
+--       { dataTypes = dataTypes ast1 <> dataTypes ast2
+--       , definitions = definitions ast1 <> definitions ast2
+--       , imports = mempty
+--       , hiddenNames = hiddenNames ast1 <> hiddenNames ast2
+--       , moduleName = moduleName ast1
+--       }
+
+
 extendASTWith :: [Def v a] -> AST v a -> AST v a
 extendASTWith defs ast = ast { definitions = defs ++ definitions ast }
 
@@ -169,9 +187,8 @@ instance FirstParameter DataConstr Span
 
 -- | Fresh a whole AST
 freshenAST :: AST v a -> AST v a
-freshenAST (AST dds defs imports hiddens name) =
-  AST dds' defs' imports hiddens name
-    where (dds', defs') = (map runFreshener dds, map runFreshener defs)
+freshenAST ast@AST{ dataTypes = dds, definitions = defs } =
+  ast{ dataTypes = map runFreshener dds, definitions = map runFreshener defs }
 
 instance Monad m => Freshenable m DataDecl where
   freshen (DataDecl s v tyVars kind ds) = do
diff --git a/frontend/src/Language/Granule/Syntax/Parser.y b/frontend/src/Language/Granule/Syntax/Parser.y
index 6b887f43c..70b16f7e8 100644
--- a/frontend/src/Language/Granule/Syntax/Parser.y
+++ b/frontend/src/Language/Granule/Syntax/Parser.y
@@ -32,6 +32,7 @@ import Language.Granule.Syntax.Preprocessor.Latex
 import Language.Granule.Syntax.Span
 import Language.Granule.Syntax.Type
 import Language.Granule.Utils hiding (mkSpan)
+import Language.Granule.Syntax.Program
 
 }
 
@@ -40,7 +41,7 @@ import Language.Granule.Utils hiding (mkSpan)
 %name tscheme TypeScheme
 %tokentype { Token }
 %error { parseError }
-%monad { StateT [Extension] (ReaderT String (Either String)) }
+%monad { ReaderT String (Either String) }
 
 %token
     nl    { TokenNL _ }
@@ -127,35 +128,37 @@ import Language.Granule.Utils hiding (mkSpan)
 %left '.'
 %%
 
-TopLevel :: { AST () () }
+TopLevel :: { Module }
   : module CONSTR where NL Defs
-            { $5 { moduleName = Just $ mkId $ constrString $2 } }
+      { $5 { moduleName = constrString $2 } }
 
   | module CONSTR hiding '(' Ids ')' where  NL Defs
-            { let modName = mkId $ constrString $2
-              in $9 { moduleName = Just modName, hiddenNames = $5 modName } }
-
-  | language CONSTR NL TopLevel                     {% case parseExtensions (constrString $2) of
-                                                    Just ext -> do
-                                                       -- modify (\st -> st { globalsExtensions = ext : globalsExtensions st })
-                                                       modify (\st -> ext : st)
-                                                       return $4
-                                                    Nothing -> error ("Unknown language extension " ++ symString $2)
-                                                }
-
-  | Defs                                        { $1 }
-
-Ids :: { Id -> M.Map Id Id }
- : CONSTR          { \modName -> M.insert (mkId $ constrString $1) modName M.empty }
- | CONSTR ',' Ids  { \modName -> M.insert (mkId $ constrString $1) modName ($3 modName) }
-
-Defs :: { AST () () }
-  : Def                       { AST [] [$1] mempty mempty Nothing }
-  | DataDecl                  { AST [$1] [] mempty mempty Nothing }
-  | Import                    { AST [] [] (singleton $1) mempty Nothing }
-  | DataDecl NL Defs          { $3 { dataTypes = $1 : dataTypes $3 } }
-  | Def NL Defs               { $3 { definitions = $1 : definitions $3 } }
-  | Import NL Defs            { $3 { imports = insert $1 (imports $3) } }
+      { $9
+        { moduleName = constrString $2
+        , moduleHiddenNames = M.fromList $ map (\id -> (id, constrString $2)) $5
+        }
+      }
+
+  | language CONSTR NL TopLevel
+      { case parseExtensions (constrString $2) of
+            Just ext -> $4 { moduleExtensions = insert ext (moduleExtensions $4) }
+            Nothing -> error ("Unknown language extension: " ++ symString $2)
+      }
+
+  | Defs
+      { $1 }
+
+Ids :: { [Id] }
+ : CONSTR          { [mkId $ constrString $1] }
+ | CONSTR ',' Ids  { (mkId $ constrString $1) : $3 }
+
+Defs :: { Module }
+  : Def                       { emptyModule{ moduleAST = emptyAST{ definitions = [$1] } } }
+  | DataDecl                  { emptyModule{ moduleAST = emptyAST{ dataTypes = [$1] } } }
+  | Import                    { emptyModule{ moduleImports = singleton $1 } }
+  | DataDecl NL Defs          { $3 { moduleAST = (moduleAST $3){ dataTypes = $1 : dataTypes (moduleAST $3) } } }
+  | Def NL Defs               { $3 { moduleAST = (moduleAST $3){ definitions = $1 : definitions (moduleAST $3) } } }
+  | Import NL Defs            { $3 { moduleImports = insert $1 (moduleImports $3) } }
 
 NL :: { () }
   : nl NL                     { }
@@ -163,7 +166,7 @@ NL :: { () }
 
 Import :: { Import }
   : import                    { let TokenImport _ ('i':'m':'p':'o':'r':'t':path) = $1
-                                in dropWhile isSpace path <> ".gr"
+                                in dropWhile isSpace $path
                               }
 
 Def :: { Def () () }
@@ -496,17 +499,17 @@ Expr :: { Expr () () }
                      (PConstr span3 () False (mkId "False") [], $6)] }
 
   | clone Expr as CopyBind in Expr
-    {% let t1 = $2; (_, pat, mt) = $4; t2 = $6 
+    {% let t1 = $2; (_, pat, mt) = $4; t2 = $6
       in (mkSpan (getPos $1, getEnd $6)) >>=
-        \sp -> return $ App sp () False (App sp () False 
-          (Val sp () False (Var () (mkId "uniqueBind"))) 
+        \sp -> return $ App sp () False (App sp () False
+          (Val sp () False (Var () (mkId "uniqueBind")))
           (Val sp () False (Abs () pat mt t2))) t1 }
 
   | endorse Expr as CopyBind in Expr
-    {% let t1 = $2; (_, pat, mt) = $4; t2 = $6 
+    {% let t1 = $2; (_, pat, mt) = $4; t2 = $6
       in (mkSpan (getPos $1, getEnd $6)) >>=
-        \sp -> return $ App sp () False (App sp () False 
-          (Val sp () False (Var () (mkId "trustedBind"))) 
+        \sp -> return $ App sp () False (App sp () False
+          (Val sp () False (Var () (mkId "trustedBind")))
           (Val sp () False (Abs () pat mt t2))) t1 }
 
   | Form
@@ -607,7 +610,7 @@ Atom :: { Expr () () }
                                     >>= \sp -> return $ Val sp () False $ Nec () (Val sp () False $ NumInt x) }
   | '#' FLOAT                 {% let (TokenFloat _ x) = $2
                                  in (mkSpan $ getPosToSpan $1)
-                                    >>= \sp -> return $ Val sp () False $ Nec () (Val sp () False $ NumFloat $ read x) }                                                                                           
+                                    >>= \sp -> return $ Val sp () False $ Nec () (Val sp () False $ NumFloat $ read x) }
   | CONSTR                    {% (mkSpan $ getPosToSpan $1)  >>= \sp -> return $ Val sp () False $ Constr () (mkId $ constrString $1) [] }
   | '#' CONSTR                {% (mkSpan $ getPosToSpan $2) >>= \sp -> return $ Val sp () False $ Nec () (Val sp () False $ Constr () (mkId $ constrString $2) [])}
   | '(' Expr ',' Expr ')'     {% do
@@ -629,64 +632,66 @@ Atom :: { Expr () () }
                                      case $2 of (TokenCharLiteral _ c) -> Nec () (Val sp () False $ CharLiteral c) }
   | '#' STRING                {% (mkSpan $ getPosToSpan $1) >>= \sp ->
                                   return $ Val sp () False $
-                                     case $2 of (TokenStringLiteral _ c) -> Nec () (Val sp () False $ StringLiteral c) }                              
+                                     case $2 of (TokenStringLiteral _ c) -> Nec () (Val sp () False $ StringLiteral c) }
   | Hole                      { $1 }
   | '&' Expr                  {% (mkSpan $ getPosToSpan $1) >>= \sp -> return $ App sp () False (Val sp () False (Var () (mkId "uniqueReturn"))) $2 }
 
 {
 
-mkSpan :: (Pos, Pos) -> StateT [Extension] (ReaderT String (Either String)) Span
+mkSpan :: (Pos, Pos) -> ReaderT String (Either String) Span
 mkSpan (start, end) = do
-  filename <- lift $ ask
+  filename <- ask
   return $ Span start end filename
 
-parseError :: [Token] -> StateT [Extension] (ReaderT String (Either String)) a
-parseError [] = lift $ lift $ Left "Premature end of file"
+parseError :: [Token] -> ReaderT String (Either String) a
+parseError [] = lift $ Left "Premature end of file"
 parseError t = do
-    file <- lift $ ask
-    lift $ lift $ Left $ file <> ":" <> show l <> ":" <> show c <> ": parse error"
+    file <- ask
+    lift $ Left $ file <> ":" <> show l <> ":" <> show c <> ": parse error"
   where (l, c) = getPos (head t)
 
-parseDefs :: FilePath -> String -> Either String (AST () (), [Extension])
-parseDefs file input = runReaderT (runStateT (topLevel $ scanTokens input) []) file
-
-parseAndDoImportsAndFreshenDefs :: (?globals :: Globals) => String -> IO (AST () (), [Extension])
-parseAndDoImportsAndFreshenDefs input = do
-    (ast, extensions) <- parseDefsAndDoImports input
-    return (freshenAST ast, extensions)
-
-parseAndFreshenDefs :: (?globals :: Globals) => String -> IO (AST () (), [Extension])
-parseAndFreshenDefs input = do
-  (ast, extensions) <- either failWithMsg return $ parseDefs sourceFilePath input
-  return (freshenAST ast, extensions)
-
-parseDefsAndDoImports :: (?globals :: Globals) => String -> IO (AST () (), [Extension])
-parseDefsAndDoImports input = do
-    (ast, extensions) <- either failWithMsg return $ parseDefs sourceFilePath input
-    case moduleName ast of
-      Nothing -> doImportsRecursively (imports ast) (ast { imports = empty }, extensions)
-      Just (Id name _) ->
-        if name == takeBaseName sourceFilePath
-          then doImportsRecursively (imports ast) (ast { imports = empty }, extensions)
-          else do
-            failWithMsg $ "Module name `" <> name <> "` does not match filename `" <> takeBaseName sourceFilePath <> "`"
-
-  where
-    -- Get all (transitive) dependencies. TODO: blows up when the file imports itself
-    doImportsRecursively :: Set Import -> (AST () (), [Extension]) -> IO (AST () (), [Extension])
-    doImportsRecursively todo (ast@(AST dds defs done hidden name), extensions) = do
-      case toList (todo \\ done) of
-        [] -> return (ast, extensions)
-        (i:todo) -> do
-          fileLocal <- doesFileExist i
-          let path = if fileLocal then i else includePath </> i
-          let ?globals = ?globals { globalsSourceFilePath = Just path } in do
-
-            src <- readFile path
-            (AST dds' defs' imports' hidden' _, extensions') <- either failWithMsg return $ parseDefs path src
-            doImportsRecursively
-              (fromList todo <> imports')
-              (AST (dds' <> dds) (defs' <> defs) (insert i done) (hidden `M.union` hidden') name, extensions ++ extensions')
+parseModule :: FilePath -> String -> Either String Module
+parseModule file input = runReaderT (topLevel $ scanTokens input) file
+
+-- parseAndDoImportsAndFreshenDefs :: (?globals :: Globals) => String -> IO (AST () (), [Extension])
+-- parseAndDoImportsAndFreshenDefs input = do
+--     (ast, extensions) <- parseDefsAndDoImports input
+--     return (freshenAST ast, extensions)
+
+-- parseAndFreshenDefs :: (?globals :: Globals) => String -> IO (AST () (), [Extension])
+-- parseAndFreshenDefs input = do
+--   (ast, extensions) <- either failWithMsg return $ parseDefs sourceFilePath input
+--   return (freshenAST ast, extensions)
+
+-- parseDefsAndDoImports :: (?globals :: Globals) => String -> IO (AST () (), [Extension])
+-- parseDefsAndDoImports input = do
+--     (ast, extensions) <- either failWithMsg return $ parseDefs sourceFilePath input
+--     case moduleName ast of
+--       Nothing -> doImportsRecursively (imports ast) (ast { imports = empty }, extensions)
+--       Just (Id name _) ->
+--         if name == takeBaseName sourceFilePath
+--           then doImportsRecursively (imports ast) (ast { imports = empty }, extensions)
+--           else do
+--             failWithMsg $ "Module name `" <> name <> "` does not match filename `" <> takeBaseName sourceFilePath <> "`"
+
+  -- where
+  --   -- Get all (transitive) dependencies. TODO: blows up when the file imports itself
+  --   doImportsRecursively :: Set Import -> (AST () (), [Extension]) -> IO (AST () (), [Extension])
+  --   doImportsRecursively todo (ast@(AST dds defs done hidden name), extensions) = do
+  --     case toList (todo \\ done) of
+  --       [] -> return (ast, extensions)
+  --       (i:todo) -> do
+  --         fileLocal <- doesFileExist i
+  --         let path = if fileLocal then i else includePath </> i
+  --         let ?globals = ?globals { globalsSourceFilePath = Just path } in do
+
+  --           src <- readFile path
+  --           (AST dds' defs' imports' hidden' _, extensions') <- either failWithMsg return $ parseDefs path src
+  --           doImportsRecursively
+  --             (fromList todo <> imports')
+  --             ( AST (dds' <> dds) (defs' <> defs) (insert i done) (hidden `M.union` hidden') name
+  --             , extensions ++ extensions'
+  --             )
 
 failWithMsg :: String -> IO a
 failWithMsg msg = putStrLn msg >> exitFailure
diff --git a/frontend/src/Language/Granule/Syntax/Preprocessor.hs b/frontend/src/Language/Granule/Syntax/Preprocessor.hs
index 43a012af4..87f0109fc 100644
--- a/frontend/src/Language/Granule/Syntax/Preprocessor.hs
+++ b/frontend/src/Language/Granule/Syntax/Preprocessor.hs
@@ -6,19 +6,23 @@ import Data.List (intercalate)
 
 import Language.Granule.Syntax.Preprocessor.Latex
 import Language.Granule.Syntax.Preprocessor.Markdown
+import Language.Granule.Syntax.Preprocessor.Ascii
 
 import Language.Granule.Utils
 
 -- | Preprocess the source file based on the file extension.
-preprocess :: Maybe (String -> String) -> Bool -> String -> FilePath -> IO String
-preprocess mbRewriter keepOldFile file env
+preprocess :: (?globals :: Globals) => FilePath -> IO String
+preprocess filePath
   = case lookup extension acceptedFormats of
-      Just (stripNonGranule, preprocessOnlyGranule) -> do
-        src <- readFile file
-        case mbRewriter of
+      Just (stripNonGranule, destructivePreprocessor) -> do
+        src <- readFile filePath
+        case rewriter of
           Just rewriter -> do
-            let processedSrc = preprocessOnlyGranule rewriter src
-            written <- writeSrcFile file keepOldFile processedSrc
+            let rewriterF = case rewriter of
+                  AsciiToUnicode -> asciiToUnicode
+                  UnicodeToAscii -> unicodeToAscii
+            let processedSrc = destructivePreprocessor rewriterF src
+            written <- writeSrcFile filePath keepBackupOfProcessedFile processedSrc
             return $ stripNonGranule written
           Nothing -> return $ stripNonGranule src
       Nothing -> error
@@ -28,12 +32,13 @@ preprocess mbRewriter keepOldFile file env
         <> intercalate ", " (map fst acceptedFormats)
         <> "."
   where
-    extension = reverse . takeWhile (/= '.') . reverse $ file
 
-    -- (file extension, (stripNonGranule, destructive preprocessor))
+    extension = reverse . takeWhile (/= '.') . reverse $ filePath
+
+    -- (file extension, (stripNonGranule, destructivePreprocessor))
     acceptedFormats =
-      [ ("gr",    (id,             id))
-      , ("md",    (unMarkdown env, processGranuleMarkdown id env))
-      , ("tex",   (unLatex env,    processGranuleLatex id env))
-      , ("latex", (unLatex env,    processGranuleLatex id env))
+      [ ("gr",    (id,         id))
+      , ("md",    (unMarkdown, processGranuleMarkdown id literateEnvName))
+      , ("tex",   (unLatex,    processGranuleLatex id literateEnvName))
+      , ("latex", (unLatex,    processGranuleLatex id literateEnvName))
       ]
diff --git a/frontend/src/Language/Granule/Syntax/Preprocessor/Latex.hs b/frontend/src/Language/Granule/Syntax/Preprocessor/Latex.hs
index bcbf35a62..cb26b81db 100644
--- a/frontend/src/Language/Granule/Syntax/Preprocessor/Latex.hs
+++ b/frontend/src/Language/Granule/Syntax/Preprocessor/Latex.hs
@@ -4,6 +4,8 @@ module Language.Granule.Syntax.Preprocessor.Latex
   )
   where
 
+import Language.Granule.Utils
+
 import Data.Char (isSpace)
 import Control.Arrow ((>>>))
 
@@ -14,8 +16,8 @@ data DocType
 -- | Extract @\begin{env}@ code blocks @\end{env}@ from tex files on a
 -- line-by-line basis, where @env@ is the name of the relevant environment. Maps
 -- other lines to the empty string, such that line numbers are preserved.
-unLatex :: String -> (String -> String)
-unLatex env = processGranuleLatex (const "") env id
+unLatex :: (?globals :: Globals) => (String -> String)
+unLatex = processGranuleLatex (const "") literateEnvName id
 
 -- | Transform the input by the given processing functions for Granule and Latex
 -- (currently operating on a line-by-line basis)
diff --git a/frontend/src/Language/Granule/Syntax/Preprocessor/Markdown.hs b/frontend/src/Language/Granule/Syntax/Preprocessor/Markdown.hs
index b0c177c2a..90cf96bba 100644
--- a/frontend/src/Language/Granule/Syntax/Preprocessor/Markdown.hs
+++ b/frontend/src/Language/Granule/Syntax/Preprocessor/Markdown.hs
@@ -7,6 +7,8 @@ module Language.Granule.Syntax.Preprocessor.Markdown
 import Data.Char (isSpace)
 import Control.Arrow ((>>>))
 
+import Language.Granule.Utils
+
 data DocType
   = Markdown
   | GranuleBlockTwiddle
@@ -15,8 +17,8 @@ data DocType
 -- | Extract fenced code blocks from markdown files on a
 -- line-by-line basis. Maps other lines to the empty string, such that line
 -- numbers are preserved.
-unMarkdown :: String -> (String -> String)
-unMarkdown env = processGranuleMarkdown (const "") env id
+unMarkdown :: (?globals :: Globals) => (String -> String)
+unMarkdown = processGranuleMarkdown (const "") literateEnvName id
 
 -- | Transform the input by the given processing functions for Granule and
 -- Markdown (currently operating on a line-by-line basis)
@@ -29,19 +31,19 @@ processGranuleMarkdown fMd env fGr = lines >>> (`zip` [1..]) >>> go Markdown >>>
   where
     go :: DocType -> [(String, Int)] -> [String]
     go Markdown ((line, lineNumber) : ls)
-      | strip line == "~~~" <> env <> "" || strip line == "~~~ " <> env <> ""
+      | strip line == "~~~" <> env || strip line == "~~~ " <> env
         = fMd line : go GranuleBlockTwiddle ls
-      | strip line == "```" <> env <> "" || strip line == "``` " <> env <> ""
+      | strip line == "```" <> env || strip line == "``` " <> env
         = fMd line : go GranuleBlockTick ls
       | otherwise
         = fMd line : go Markdown ls
     go GranuleBlockTwiddle ((line, lineNumber) : ls)
       | strip line == "~~~"
         = fMd line : go Markdown ls
-      | strip line == "~~~" <> env <> ""
-        || strip line == "~~~ " <> env <> ""
-        || strip line == "```" <> env <> ""
-        || strip line == "``` " <> env <> ""
+      | strip line == "~~~" <> env
+        || strip line == "~~~ " <> env
+        || strip line == "```" <> env
+        || strip line == "``` " <> env
           = error
             $ "Unexpected `"
             <> line
@@ -53,10 +55,10 @@ processGranuleMarkdown fMd env fGr = lines >>> (`zip` [1..]) >>> go Markdown >>>
     go GranuleBlockTick ((line, lineNumber) : ls)
       | strip line == "```"
         = fMd line : go Markdown ls
-      | strip line == "~~~" <> env <> ""
-        || strip line == "~~~ " <> env <> ""
-        || strip line == "```" <> env <> ""
-        || strip line == "``` " <> env <> ""
+      | strip line == "~~~" <> env
+        || strip line == "~~~ " <> env
+        || strip line == "```" <> env
+        || strip line == "``` " <> env
           = error
             $ "Unexpected `"
             <> line
diff --git a/frontend/src/Language/Granule/Syntax/Pretty.hs b/frontend/src/Language/Granule/Syntax/Pretty.hs
index 16e4dd860..f273c227a 100644
--- a/frontend/src/Language/Granule/Syntax/Pretty.hs
+++ b/frontend/src/Language/Granule/Syntax/Pretty.hs
@@ -9,6 +9,7 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE NamedFieldPuns #-}
 
 module Language.Granule.Syntax.Pretty where
 
@@ -20,8 +21,8 @@ import Language.Granule.Syntax.Pattern
 import Language.Granule.Syntax.Span
 import Language.Granule.Syntax.Def
 import Language.Granule.Syntax.Helpers
-import Language.Granule.Syntax.Identifiers
 import Language.Granule.Utils
+import Language.Granule.Syntax.Program
 
 -- Version of pretty that assumes the default Globals so as not to
 -- propagate globals information around
@@ -170,19 +171,25 @@ instance Pretty TypeOperator where
    TyOpInterval        -> ".."
    TyOpConverge        -> "#"
 
-instance Pretty v => Pretty (AST v a) where
-  pretty (AST dataDecls defs imprts hidden name) =
+instance Pretty Module where
+  pretty Mod
+    { moduleAST = AST { dataTypes, definitions }
+    , moduleName
+    , moduleExtensions
+    , moduleImports
+    , moduleHiddenNames } =
     -- Module header (if it exists)
-    (case name of
-        Nothing -> ""
-        Just name -> "module "
-                  <> pretty name
-                  <> " hiding ("
-                  <> (intercalate "," (map pretty (toList hidden)))
-                  <> ") where\n\n")
-    <> (unlines . map ("import " <>) . toList) imprts
-    <> "\n\n" <> pretty' dataDecls
-    <> "\n\n" <> pretty' defs
+    (case moduleName of
+        "" -> ""
+        _ -> "module "
+            <> moduleName
+            <> " hiding ("
+            <> (intercalate "," (map pretty (toList moduleHiddenNames)))
+            <> ") where\n\n"
+    )
+    <> (unlines . map ("import " <>) . toList) moduleImports
+    <> "\n\n" <> pretty' dataTypes
+    <> "\n\n" <> pretty' definitions
     where
       pretty' :: Pretty l => [l] -> String
       pretty' = intercalate "\n\n" . map pretty
diff --git a/frontend/src/Language/Granule/Syntax/Program.hs b/frontend/src/Language/Granule/Syntax/Program.hs
new file mode 100644
index 000000000..78e40353b
--- /dev/null
+++ b/frontend/src/Language/Granule/Syntax/Program.hs
@@ -0,0 +1,75 @@
+-- | How Granule programs are structured into Modules
+
+module Language.Granule.Syntax.Program
+  ( module Language.Granule.Syntax.Program
+  , module Reexport
+  )
+where
+
+import Language.Granule.Utils
+import Language.Granule.Syntax.Def as Reexport
+import Language.Granule.Syntax.Type
+import Language.Granule.Syntax.Preprocessor
+
+import Algebra.Graph.AdjacencyMap (AdjacencyMap)
+import Data.Time.Clock (UTCTime)
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Control.Applicative (empty)
+
+data GranuleProgram = GranulePrg
+  { rootModule :: ModuleName
+  , modules :: Map ModuleName Module
+  , dependencyGraph :: AdjacencyMap ModuleName
+  }
+
+type ModuleName = String
+
+data Module = Mod
+  { moduleAST :: AST () ()
+  , moduleName :: ModuleName
+  , moduleMetadata :: ModuleMetadata
+  , moduleExtensions :: Set Extension
+  , moduleSignature :: Maybe ModuleSignature
+  , moduleImports :: Set Import
+  , moduleHiddenNames :: Map Id ModuleName -- map from names to the module hiding them
+  }
+
+emptyModule :: Module
+emptyModule = Mod
+  { moduleAST = emptyAST
+  , moduleName = empty
+  , moduleMetadata = emptyModuleMetadata
+  , moduleExtensions = Set.empty
+  , moduleSignature = empty
+  , moduleImports = Set.empty
+  , moduleHiddenNames = Map.empty
+  }
+
+data ModuleMetadata = ModMeta
+  { moduleMetaFilePath :: Maybe FilePath -- a module might not have a filepath, or we might not even have a module source at all and just run the type checker on the signature (with --no-eval)
+  , moduleMetaFileModificationTime :: Maybe UTCTime
+  , moduleMetaSignatureFilePath :: Maybe FilePath
+  , moduleMetaSignatureFileModificationTime :: Maybe UTCTime
+  }
+
+emptyModuleMetadata :: ModuleMetadata
+emptyModuleMetadata =
+  ModMeta
+    { moduleMetaFilePath = empty
+    , moduleMetaFileModificationTime = empty
+    , moduleMetaSignatureFilePath = empty
+    , moduleMetaSignatureFileModificationTime = empty
+    }
+
+data ModuleSignature = ModSig
+  { dataDeclarationContext :: Ctxt DataDecl
+  , definitionContext :: Ctxt TypeScheme
+  }
+
+readAndPreprocessGranuleProgram :: (?globals :: Globals) => FilePath -> IO GranuleProgram
+readAndPreprocessGranuleProgram filePath = do
+  src <- preprocess filePath
+  undefined
diff --git a/frontend/src/Language/Granule/Syntax/QuasiQuoter.hs b/frontend/src/Language/Granule/Syntax/QuasiQuoter.hs
new file mode 100644
index 000000000..a6693eecf
--- /dev/null
+++ b/frontend/src/Language/Granule/Syntax/QuasiQuoter.hs
@@ -0,0 +1,28 @@
+-- | Write Granule in your Haskell files!
+--      [gr|
+--      drop : a [] -> ()
+--      drop _ = ()
+--      |]
+
+module Language.Granule.Syntax.QuasiQuoter
+  ( module Language.Granule.Syntax.QuasiQuoter
+  )
+where
+
+import Language.Granule.Syntax.Program
+import Language.Granule.Syntax.Parser
+
+import Language.Haskell.TH.Quote
+
+gr :: QuasiQuoter
+gr =
+  QuasiQuoter
+    { quoteExp =
+        \str ->
+            case parseModule "builtins" str of
+              Right mod -> dataToExpQ (const Nothing) (moduleAST mod)
+              Left err -> error err
+    , quotePat  = undefined
+    , quoteType = undefined
+    , quoteDec  = undefined
+    }
diff --git a/frontend/src/Language/Granule/Synthesis/Deriving.hs b/frontend/src/Language/Granule/Synthesis/Deriving.hs
index 3d5eb1408..6ec4c3593 100644
--- a/frontend/src/Language/Granule/Synthesis/Deriving.hs
+++ b/frontend/src/Language/Granule/Synthesis/Deriving.hs
@@ -8,7 +8,6 @@ import Language.Granule.Syntax.Type
 import Language.Granule.Syntax.Expr
 import Language.Granule.Syntax.Def
 import Language.Granule.Syntax.Span
-import Language.Granule.Context
 
 import Language.Granule.Checker.Predicates (Constraint(..))
 import Language.Granule.Checker.Kinding
diff --git a/frontend/src/Language/Granule/Synthesis/Refactor.hs b/frontend/src/Language/Granule/Synthesis/Refactor.hs
index ef4213839..03959de37 100644
--- a/frontend/src/Language/Granule/Synthesis/Refactor.hs
+++ b/frontend/src/Language/Granule/Synthesis/Refactor.hs
@@ -4,7 +4,6 @@ module Language.Granule.Synthesis.Refactor where
 import Language.Granule.Syntax.Def
 import Language.Granule.Syntax.Expr
 import Language.Granule.Syntax.Pattern
-import Language.Granule.Syntax.Identifiers
 
 -- Refactors an equation which contains abstractions in its equations
 -- by pushing these abstractions into equation patterns
@@ -79,4 +78,4 @@ refactorPattern p@PInt {} _ _ = p
 refactorPattern p@PFloat {} _ _ = p
 refactorPattern (PConstr sp a _ id ps) id' subpat =
   let ps' = map (\p -> refactorPattern p id' subpat) ps
-  in PConstr sp a (any patRefactored ps') id ps'
\ No newline at end of file
+  in PConstr sp a (any patRefactored ps') id ps'
diff --git a/frontend/src/Language/Granule/Utils.hs b/frontend/src/Language/Granule/Utils.hs
index b23d96e17..b379b1ff9 100644
--- a/frontend/src/Language/Granule/Utils.hs
+++ b/frontend/src/Language/Granule/Utils.hs
@@ -52,12 +52,18 @@ data Globals = Globals
   , globalsGradeOnRule         :: Maybe Bool
   , globalsSynthTimeoutMillis  :: Maybe Integer
   , globalsSynthIndex          :: Maybe Integer
-  , globalsExtensions           :: [Extension]
+  , globalsExtensions          :: [Extension]
+  , globalsRewriter            :: Maybe Rewriter
+  , globalsKeepBackupOfProcessedFile :: Maybe Bool
+  , globalsLiterateEnvName     :: Maybe String
   } deriving (Read, Show)
 
 -- | Allowed extensions
 data Extension = Base | CBN | NoTopLevelApprox | SecurityLevels
- deriving (Eq, Read, Show)
+ deriving (Eq, Ord, Read, Show)
+
+data Rewriter = AsciiToUnicode | UnicodeToAscii
+  deriving (Eq, Ord, Read, Show)
 
 -- | Given a map from `Extension`s to `a` pick the first
 -- | `a` that matches with an extension in scope. Otherwise
@@ -81,7 +87,9 @@ parseExtensions xs =
 
 -- | Accessors for global flags with default values
 debugging, noColors, alternativeColors, noEval, suppressInfos, suppressErrors,
-  timestamp, testing, ignoreHoles, benchmarking, benchmarkingRawData, subtractiveSynthesisMode, alternateSynthesisMode, altSynthStructuring, gradeOnRule :: (?globals :: Globals) => Bool
+  timestamp, testing, ignoreHoles, benchmarking, benchmarkingRawData, subtractiveSynthesisMode,
+  alternateSynthesisMode, altSynthStructuring, gradeOnRule, keepBackupOfProcessedFile
+  :: (?globals :: Globals) => Bool
 debugging         = fromMaybe False $ globalsDebugging ?globals
 noColors          = fromMaybe False $ globalsNoColors ?globals
 alternativeColors = fromMaybe False $ globalsAlternativeColors ?globals
@@ -97,7 +105,13 @@ subtractiveSynthesisMode = fromMaybe False $ globalsSubtractiveSynthesis ?global
 alternateSynthesisMode = fromMaybe False $ globalsAlternateSynthesisMode ?globals
 altSynthStructuring = fromMaybe False $ globalsAltSynthStructuring ?globals
 gradeOnRule = fromMaybe False $ globalsGradeOnRule ?globals
+keepBackupOfProcessedFile = fromMaybe True $ globalsKeepBackupOfProcessedFile ?globals
+
+rewriter :: (?globals :: Globals) => Maybe Rewriter
+rewriter = globalsRewriter ?globals
 
+literateEnvName :: (?globals :: Globals) => String
+literateEnvName = fromMaybe "granule" $ globalsLiterateEnvName ?globals
 
 -- | Accessor for the solver timeout with a default value
 solverTimeoutMillis :: (?globals :: Globals) => Integer
@@ -148,6 +162,9 @@ instance Semigroup Globals where
       , globalsSynthIndex = globalsSynthIndex g1 <|> globalsSynthIndex g2
       , globalsSynthTimeoutMillis = globalsSynthTimeoutMillis g1 <|> globalsSynthTimeoutMillis g2
       , globalsExtensions = nub (globalsExtensions g1 <> globalsExtensions g2)
+      , globalsRewriter = globalsRewriter g1 <|> globalsRewriter g2
+      , globalsKeepBackupOfProcessedFile = globalsKeepBackupOfProcessedFile g1 <|> globalsKeepBackupOfProcessedFile g2
+      , globalsLiterateEnvName = globalsLiterateEnvName g1 <|> globalsLiterateEnvName g2
       }
 
 instance Monoid Globals where
@@ -172,11 +189,14 @@ instance Monoid Globals where
     , globalsBenchmarkRaw        = Nothing
     , globalsSubtractiveSynthesis   = Nothing
     , globalsAlternateSynthesisMode = Nothing
-        , globalsAltSynthStructuring = Nothing
+    , globalsAltSynthStructuring = Nothing
     , globalsGradeOnRule = Nothing
     , globalsSynthTimeoutMillis  = Nothing
     , globalsSynthIndex  = Nothing
     , globalsExtensions = [Base]
+    , globalsRewriter = Nothing
+    , globalsKeepBackupOfProcessedFile = Nothing
+    , globalsLiterateEnvName = Nothing
     }
 
 -- | A class for messages that are shown to the user. TODO: make more general
@@ -375,4 +395,4 @@ snd3 :: (a, b, c) -> b
 snd3 (_, x, _) = x
 
 thd3 :: (a, b, c) -> c
-thd3 (_, _, x) = x
\ No newline at end of file
+thd3 (_, _, x) = x