From 8f6eec4f643752c62b4fdbda11f4240d00cfe4ff Mon Sep 17 00:00:00 2001
From: Vilem Liepelt <17603372+buggymcbugfix@users.noreply.github.com>
Date: Thu, 2 Mar 2023 14:42:20 +0100
Subject: [PATCH 1/3] wip

---
 compiler/app/Language/Granule/Compiler.hs     |   7 +
 frontend/package.yaml                         |   8 +-
 .../src/Language/Granule/Checker/Checker.hs   | 153 +++++++++-------
 .../src/Language/Granule/Checker/Kinding.hs   |   1 -
 .../src/Language/Granule/Checker/Monad.hs     |  10 +-
 .../src/Language/Granule/Checker/NameClash.hs |   5 +-
 .../Language/Granule/Checker/Primitives.hs    |  38 ++--
 .../Language/Granule/Checker/Substitution.hs  |   3 +-
 .../Language/Granule/Checker/TypeAliases.hs   |  15 +-
 frontend/src/Language/Granule/Context.hs      |   6 +-
 frontend/src/Language/Granule/Syntax/Def.hs   |  39 ++--
 frontend/src/Language/Granule/Syntax/Parser.y | 169 +++++++++---------
 .../Language/Granule/Syntax/Preprocessor.hs   |  31 ++--
 .../Granule/Syntax/Preprocessor/Latex.hs      |   6 +-
 .../Granule/Syntax/Preprocessor/Markdown.hs   |  26 +--
 .../src/Language/Granule/Syntax/Pretty.hs     |  33 ++--
 .../src/Language/Granule/Syntax/Program.hs    | 111 ++++++++++++
 .../Language/Granule/Syntax/QuasiQuoter.hs    |  28 +++
 .../Language/Granule/Synthesis/Deriving.hs    |   1 -
 .../Language/Granule/Synthesis/Refactor.hs    |   3 +-
 frontend/src/Language/Granule/Utils.hs        |  30 +++-
 21 files changed, 469 insertions(+), 254 deletions(-)
 create mode 100644 frontend/src/Language/Granule/Syntax/Program.hs
 create mode 100644 frontend/src/Language/Granule/Syntax/QuasiQuoter.hs

diff --git a/compiler/app/Language/Granule/Compiler.hs b/compiler/app/Language/Granule/Compiler.hs
index e486511f0..6dda4facc 100644
--- a/compiler/app/Language/Granule/Compiler.hs
+++ b/compiler/app/Language/Granule/Compiler.hs
@@ -248,6 +248,13 @@ parseGrConfig = info (go <**> helper) $ briefDesc
             , show solverTimeoutMillis <> "ms."
             ]
 
+        globalsCachePath <-
+          optional $ strOption
+            $ long "cache-path"
+            <> help ("Path to the cache file. Defaults to "
+                    <> show cachePath)
+            <> metavar "PATH"
+
         globalsIncludePath <-
           optional $ strOption
             $ long "include-path"
diff --git a/frontend/package.yaml b/frontend/package.yaml
index 3c138597f..b36541ef5 100644
--- a/frontend/package.yaml
+++ b/frontend/package.yaml
@@ -23,10 +23,11 @@ ghc-options:
 
 default-extensions:
 - ImplicitParams
-- ViewPatterns
 - LambdaCase
-- TupleSections
 - NamedFieldPuns
+- ScopedTypeVariables
+- TupleSections
+- ViewPatterns
 
 library:
   source-dirs: src
@@ -88,7 +89,6 @@ library:
   - Glob
   - filepath
   - bifunctors
-  - raw-strings-qq
   - text-replace
   - directory
   - syb >=0.6
@@ -97,6 +97,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..5d97cc335 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,81 +62,102 @@ 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 () ()
-  -> 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
+  => Module
+  -> IO (Either (NonEmpty CheckerError) (AST () Type, ModuleSignature))
+check mod@Mod{ moduleAST = ast } =
+  case moduleSignature mod of
+    Just sig -> do
+  -- case moduleMetadata of
+  --   ModMeta
+  --     -- { moduleMetaFilePath = Just sourceFilePath
+  --     { moduleMetaFileModificationTime = Just sourceFileModificationTime
+  --     -- , moduleMetaSignatureFilePath = Just interfaceFilePath
+  --     , moduleMetaSignatureFileModificationTime = Just interfaceFileModificationTime
+  --     }
+  --     | interfaceFileModificationTime > sourceFileModificationTime
+  --     , Just sig <- moduleSignature mod
+
+
+  evalChecker (initState { allHiddenNames = moduleHiddenNames mod }) $ 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
+      defs <- runAll kindCheckDef (definitions ast)
       let defCtxt = map (\(Def _ name _ _ tys) -> (name, tys)) defs
       defs <- runAll (checkDef defCtxt) defs
       -- 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{ dataTypes = dataTypes ast, definitions = defs }, 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 +325,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 +2008,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..ce4048bd7
--- /dev/null
+++ b/frontend/src/Language/Granule/Syntax/Program.hs
@@ -0,0 +1,111 @@
+-- | 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)
+import System.FilePath ((<.>))
+import Control.Exception (try)
+
+-- | Invariants:
+-- * rootModule \in modules
+-- if a Module has a module signature, then it is assumed that type checking can be skipped
+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 ModuleName
+  , 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
+  , derivedDefinitions :: [Def () ()]
+  }
+
+type E = String
+
+readAndPreprocessGranuleProgram :: (?globals :: Globals)
+  => FilePath
+  -> IO (Either E GranuleProgram)
+readAndPreprocessGranuleProgram filePath = do
+  src <- preprocess filePath
+  rootModule <- parseModule src
+  let ?gloabals = ?globals { globalsRewriter = Nothing }
+  moduleImports rootModule
+
+
+goImports :: (?globals :: Globals)
+  => Module
+  -> Set ModuleName
+  -> IO (Either E [(ModuleName, ModuleName)])
+goImports rootModule imports = do
+  let (foo :: _) = traverse (try . readFile) [fp <.> ext | ext <- granuleFileTypes]
+  undefined
+
+granuleFileTypes = ["gr", "gr.md", "gr.tex", "gr.latex"]
+
+
+
+-- 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'
+--               )
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

From e0e0902b7e0769b5322f037530b4cbe1d431733d Mon Sep 17 00:00:00 2001
From: Vilem Liepelt <17603372+buggymcbugfix@users.noreply.github.com>
Date: Mon, 18 Dec 2023 17:20:46 +0100
Subject: [PATCH 2/3] wip

---
 StdLib/Either.gri                             |   7 +
 StdLib/Vec.gri                                | 187 ++++++++++++++++++
 examples/Capabilities.gr.output               |   1 +
 examples/hni.gr                               |   6 +
 examples/hni.gr.output                        |   1 +
 examples/nonDeterminism.gr.output             |   1 +
 examples/sensitivity.gr.output                |   1 +
 examples/test.gr                              |   5 +
 fix.gr                                        |   9 +
 frontend/package.yaml                         |   1 +
 .../src/Language/Granule/Checker/Checker.hs   |  56 +++---
 frontend/src/Language/Granule/Syntax/Parser.y | 121 ++++++++++--
 .../src/Language/Granule/Syntax/Pretty.hs     |  15 +-
 .../src/Language/Granule/Syntax/Program.hs    |  49 ++---
 test.gr                                       |   6 +
 work-in-progress/ref.gr                       |   9 +
 16 files changed, 405 insertions(+), 70 deletions(-)
 create mode 100644 StdLib/Either.gri
 create mode 100644 StdLib/Vec.gri
 create mode 100644 examples/Capabilities.gr.output
 create mode 100644 examples/hni.gr
 create mode 100644 examples/hni.gr.output
 create mode 100644 examples/nonDeterminism.gr.output
 create mode 100644 examples/sensitivity.gr.output
 create mode 100644 examples/test.gr
 create mode 100644 fix.gr
 create mode 100644 test.gr
 create mode 100644 work-in-progress/ref.gr

diff --git a/StdLib/Either.gri b/StdLib/Either.gri
new file mode 100644
index 000000000..12738c29c
--- /dev/null
+++ b/StdLib/Either.gri
@@ -0,0 +1,7 @@
+data Either a b where Left a | Right b
+
+pushEither : forall {a : Type, b : Type, c : Nat} . {c <= 1} =>
+             (Either a b) [c] -> Either (a [c]) (b [c])
+
+pullEither : forall {a : Type, b : Type, c : Nat}
+        . Either (a [c]) (b [c]) -> (Either a b) [c]
diff --git a/StdLib/Vec.gri b/StdLib/Vec.gri
new file mode 100644
index 000000000..8fc7f87b1
--- /dev/null
+++ b/StdLib/Vec.gri
@@ -0,0 +1,187 @@
+------
+--- Module: Vec
+--- Description: Base library for operations on type-indexed vectors
+--- Authors: Dominic Orchard, Vilem-Benjamin Liepelt
+--- License: BSD3
+--- Copyright: (c) Authors 2018
+--- Issue-tracking: https://github.com/dorchard/granule/issues
+--- Repository: https://github.com/dorchard/granule
+------
+
+-- # Operations on vectors
+
+import Nat
+import Fin
+
+data Vec (n : Nat) t where
+  Nil  : Vec 0 t;
+  Cons : t -> Vec n t -> Vec (n+1) t
+
+-- Length of an indexed vector into an indexed nat
+-- discarding the elements
+length
+  : forall {a : Type, n : Nat}
+  . Vec n (a [0]) -> N n
+length Nil = Z;
+length (Cons [_] xs) = S (length xs)
+
+-- Length of a `Vec` into an indexed `N`, preserving the elements
+length'
+  : forall {a : Type, n : Nat}
+  . Vec n a -> (N n, Vec n a)
+length' Nil = (Z, Nil);
+length' (Cons x xs) = let (n, xs) = length' xs in (S n, Cons x xs)
+
+--- Map function
+map
+  : forall {a b : Type, n : Nat}
+  . (a -> b) [n] -> Vec n a -> Vec n b
+map [_] Nil = Nil;
+map [f] (Cons x xs) = Cons (f x) (map [f] xs)
+
+-- Safe random-access indexing from a vector
+index : forall {a : Type, n m : Nat}
+     . {m > n} => N n -> (Vec m a) [0..1] -> a
+index Z     [Cons x _]   = x;
+index (S k) [Cons _ xs'] = index k [xs']
+
+-- Standard foldr on vectors
+foldr
+  : forall {a b : Type, n : Nat}
+  . (a -> b -> b) [n] -> b -> Vec n a -> b
+foldr [_] z Nil = z;
+foldr [f] z (Cons x xs) = f x (foldr [f] z xs)
+
+foldr1
+  : forall {a : Type, n : Nat}
+  . (a -> a -> a) [n] -> Vec (n + 1) a -> a
+foldr1 [_] (Cons x Nil) = x;
+foldr1 [mag] (Cons x (Cons x' xs)) = foldr1 [mag] (Cons (x `mag` x') xs)
+
+foldl
+  : forall {a b : Type, n : Nat}
+  . (b -> a -> b) [n] -> b -> Vec n a -> b
+foldl [_] acc Nil = acc;
+foldl [op] acc (Cons x xs) = foldl [op] (acc `op` x) xs
+
+-- Append two vectors
+append
+  : forall {a : Type, m n : Nat}
+  . Vec n a -> Vec m a -> Vec (n + m) a
+append Nil ys = ys;
+append (Cons x xs) ys = Cons x (append xs ys)
+
+drop
+  : forall {a : Type, m n : Nat}
+  . N m -> (Vec n a) [0..1] -> Vec (n - m) a
+drop Z [xs] = xs;
+drop (S n) [Nil] = drop n [Nil];
+drop (S n) [Cons _ xs] = drop n [xs]
+
+take
+  : forall {a : Type, m n : Nat}
+  . N m -> (Vec n a) [0..1] -> Vec (n + (m - n)) a
+take Z [xs] = xs;
+take (S k) [Cons x xs] = Cons x (take k [xs])
+
+--- Return the first item (head) of the vector
+--- NB: non-linear in the vector
+head
+  : forall {a : Type, n : Nat}
+  . (Vec (n + 1) a) [0..1] -> a
+head [Cons x _] = x
+
+--- Return the vector with the first item removed
+--- NB: non-linear in the vector
+tail
+  : forall {a : Type, n : Nat}
+  . (Vec (n + 1) a) [0..1] -> Vec n a
+tail [Cons _ xs] = xs
+
+--- Get the last item of a Vector
+--last : forall {a : Type, n : Nat}
+--     . (Vec (n + 1) a) [0..1] -> a
+--last [Cons x Nil] = x;
+--last [Cons _ xs] = last [xs]
+
+---
+--init : forall {a : Type, n : Nat}
+--     . (Vec (n + 1) a) [0..1] -> Vec n a
+--init [Cons _ Nil] = Nil;
+--init [Cons x xs] = Cons x (init [xs])
+
+uncons
+  : forall {a : Type, n : Nat}
+  . Vec (n + 1) a -> (a, Vec n a)
+uncons (Cons x xs) = (x,xs)
+
+--- Split a vector at position 'n'
+split
+  : forall {a : Type, m n : Nat}
+  . N n -> (Vec (n + m) a) -> (Vec n a, Vec m a)
+split Z xs = (Nil, xs);
+split (S n) (Cons x xs) = let (xs', ys') = split n xs in (Cons x xs', ys')
+
+--- Simple folds
+sum
+  : forall {n : Nat}
+  . Vec n Int -> Int
+sum = foldr [\(x : Int) -> \(y : Int) -> x + y] 0
+
+product
+  : forall {n : Nat}
+  . Vec n Int -> Int
+product = foldr [\(x : Int) -> \(y : Int) -> x * y] 1
+
+--- Replicate n x is a vector of length n with x the value of every element
+replicate
+  : forall {a : Type, n : Nat}
+  . N n -> a [n] -> Vec n a
+replicate Z [c] = Nil;
+replicate (S n) [c] = Cons c (replicate n [c])
+
+--- Make a vector of length n with all integers from 0 to n-1
+---     > range (S (S (S (S Z))))
+---     Cons 0 (Cons 1 (Cons 2 (Cons 3 Nil)))
+range
+  : forall {n : Nat}
+  . N n -> Vec n Int
+range n = range' n [0]
+
+--- Make a vector of length n with all integers from `start` up until `n + i - 1`
+---     > range' (S (S (S (S Z)))) [-6]
+---     Cons -6 (Cons -5 (Cons -4 (Cons -3 Nil)))
+range'
+  : forall {n : Nat}
+  . N n -> Int [n] -> Vec n Int
+range' Z [i] = Nil;
+range' (S n) [i] = Cons i (range' n [i + 1])
+
+--- pullVec pulls non linearity in elements into a non linearity on the whole vector
+pullVec : forall {a : Type, s : Semiring, k : s, n : Nat}
+  . Vec n (a [k]) -> (Vec n a) [k]
+pullVec = pull @Vec
+
+--- pushVec pushes in non linearity of vector into the elements
+pushVec : ∀ {a : Type, s : Semiring, k : s, n : Nat} . {(1 : s) <= k}
+      => (Vec n a) [k] → Vec n (a [k])
+pushVec = push @Vec
+
+copySpine
+  : forall {a : Type, n : Nat}
+  . Vec n a -> Vec n () × Vec n a
+copySpine Nil = (Nil, Nil);
+copySpine (Cons x xs) = let
+  (ss, xs) = copySpine xs
+  in (Cons () ss, Cons x xs)
+
+data VecX a where
+  VecX : ∀ {n : Nat} . Vec n a → VecX a
+
+import Maybe
+
+stringToVecX : String → VecX Char
+stringToVecX s = case stringUncons s of
+  None → VecX Nil;
+  Some (c, s) → let VecX v = stringToVecX s in VecX (Cons c v)
+
diff --git a/examples/Capabilities.gr.output b/examples/Capabilities.gr.output
new file mode 100644
index 000000000..dd626a0f3
--- /dev/null
+++ b/examples/Capabilities.gr.output
@@ -0,0 +1 @@
+()
\ No newline at end of file
diff --git a/examples/hni.gr b/examples/hni.gr
new file mode 100644
index 000000000..581283a3e
--- /dev/null
+++ b/examples/hni.gr
@@ -0,0 +1,6 @@
+main : Char <IO>
+main = let
+  h <- openHandle ReadMode "examples/hni.gr";
+  (h2, c) <- readChar h;
+  () <- closeHandle h2
+  in pure c
diff --git a/examples/hni.gr.output b/examples/hni.gr.output
new file mode 100644
index 000000000..dd1645aeb
--- /dev/null
+++ b/examples/hni.gr.output
@@ -0,0 +1 @@
+'m'
\ No newline at end of file
diff --git a/examples/nonDeterminism.gr.output b/examples/nonDeterminism.gr.output
new file mode 100644
index 000000000..4841526b0
--- /dev/null
+++ b/examples/nonDeterminism.gr.output
@@ -0,0 +1 @@
+Cons 2.0 (Cons -2.0 (Cons -2.0 (Cons 2.0 Nil)))
\ No newline at end of file
diff --git a/examples/sensitivity.gr.output b/examples/sensitivity.gr.output
new file mode 100644
index 000000000..6867f09e5
--- /dev/null
+++ b/examples/sensitivity.gr.output
@@ -0,0 +1 @@
+413.5
\ No newline at end of file
diff --git a/examples/test.gr b/examples/test.gr
new file mode 100644
index 000000000..c9c91d808
--- /dev/null
+++ b/examples/test.gr
@@ -0,0 +1,5 @@
+data Option a = None | Some a
+
+fromOption : forall a . a [] -> Option a -> a
+fromOption [d] None = d;
+fromOption [d] (Some x) = x
diff --git a/fix.gr b/fix.gr
new file mode 100644
index 000000000..624f4cf12
--- /dev/null
+++ b/fix.gr
@@ -0,0 +1,9 @@
+-- how often can we unroll the loop?
+fix : forall {a : Type, n : Nat} . (a -> a) [] -> a
+fix [f] = f (fix [f] x)
+
+-- go 0 = 0
+-- go n = n + go (n - 1)
+
+-- go_ 0 rec = 0
+-- go_ n rec = n + rec (n - 1)
diff --git a/frontend/package.yaml b/frontend/package.yaml
index b36541ef5..06e01e65c 100644
--- a/frontend/package.yaml
+++ b/frontend/package.yaml
@@ -99,6 +99,7 @@ library:
   - clock
   - algebraic-graphs
   - template-haskell
+  - extra
 
 tests:
   frontend-spec:
diff --git a/frontend/src/Language/Granule/Checker/Checker.hs b/frontend/src/Language/Granule/Checker/Checker.hs
index 5d97cc335..194c14ff4 100644
--- a/frontend/src/Language/Granule/Checker/Checker.hs
+++ b/frontend/src/Language/Granule/Checker/Checker.hs
@@ -67,12 +67,22 @@ import System.Directory (getModificationTime)
 import Control.Exception (try, SomeException)
 
 -- Checking (top-level)
+
+-- TODO: Return typed GranuleProgram
 check :: (?globals :: Globals)
-  => Module
-  -> IO (Either (NonEmpty CheckerError) (AST () Type, ModuleSignature))
-check mod@Mod{ moduleAST = ast } =
-  case moduleSignature mod of
-    Just sig -> do
+  => GranuleProgram
+  -> IO (Either (NonEmpty CheckerError) (AST () Type, [Def () ()]))
+check prog = do
+  topSort (dependencyGraph prog)
+
+
+-- checkModule :: (?globals :: Globals)
+--   => Module
+--   -> IO (Either (NonEmpty CheckerError) (AST () Type, ModuleSignature))
+-- checkModule mod@Mod{ moduleAST = ast } =
+--   case moduleSignature mod of
+--     Just sig -> do
+
   -- case moduleMetadata of
   --   ModMeta
   --     -- { moduleMetaFilePath = Just sourceFilePath
@@ -84,22 +94,22 @@ check mod@Mod{ moduleAST = ast } =
   --     , Just sig <- moduleSignature mod
 
 
-  evalChecker (initState { allHiddenNames = moduleHiddenNames mod }) $ do
-      ast <- return $ replaceTypeAliases ast
-      _    <- checkNameClashes ast
-      _    <- runAll checkTyCon (Primitives.dataTypes ++ dataTypes ast)
-      _    <- runAll checkDataCons (Primitives.dataTypes ++ dataTypes ast)
-      debugM "extensions" (show $ globalsExtensions ?globals)
-      debugM "check" "kindCheckDef"
-      defs <- runAll kindCheckDef (definitions ast)
-      let defCtxt = map (\(Def _ name _ _ tys) -> (name, tys)) defs
-      defs <- runAll (checkDef defCtxt) defs
-      -- Add on any definitions computed by the type checker (derived)
-      st <- get
-      let derivedDefs = map (snd . snd) (derivedDefinitions st)
-      -- traceM $ show $ AST dataDecls defs imports hidden name
-      -- traceM $ show derivedDefs
-      pure (AST{ dataTypes = dataTypes ast, definitions = defs }, derivedDefs)
+  -- evalChecker (initState { allHiddenNames = moduleHiddenNames mod }) $ do
+  --     ast <- return $ replaceTypeAliases ast
+  --     _    <- checkNameClashes ast
+  --     _    <- runAll checkTyCon (Primitives.dataTypes ++ dataTypes ast)
+  --     _    <- runAll checkDataCons (Primitives.dataTypes ++ dataTypes ast)
+  --     debugM "extensions" (show $ globalsExtensions ?globals)
+  --     debugM "check" "kindCheckDef"
+  --     defs <- runAll kindCheckDef (definitions ast)
+  --     let defCtxt = map (\(Def _ name _ _ tys) -> (name, tys)) defs
+  --     defs <- runAll (checkDef defCtxt) defs
+  --     -- Add on any definitions computed by the type checker (derived)
+  --     st <- get
+  --     let derivedDefs = map (snd . snd) (derivedDefinitions st)
+  --     -- traceM $ show $ AST dataDecls defs imports hidden name
+  --     -- traceM $ show derivedDefs
+  --     pure (AST{ dataTypes = dataTypes ast, definitions = defs }, derivedDefs)
 
 -- Synthing the type of a single expression in the context of a Module
 synthExprInIsolation :: (?globals :: Globals)
@@ -325,8 +335,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
+    -- 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)
diff --git a/frontend/src/Language/Granule/Syntax/Parser.y b/frontend/src/Language/Granule/Syntax/Parser.y
index 70b16f7e8..302735827 100644
--- a/frontend/src/Language/Granule/Syntax/Parser.y
+++ b/frontend/src/Language/Granule/Syntax/Parser.y
@@ -1,8 +1,9 @@
 {
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE TypeApplications #-}
 
 module Language.Granule.Syntax.Parser where
 
@@ -14,19 +15,26 @@ import Control.Monad.Trans.Class (lift)
 import Data.Char (isSpace)
 import Data.Foldable (toList)
 import Data.List (intercalate, nub, stripPrefix)
-import Data.Maybe (mapMaybe)
+import Data.Maybe (catMaybes, mapMaybe)
 import Data.Set (Set, (\\), fromList, insert, empty, singleton)
-import qualified Data.Map as M
+import qualified Data.Map as Map
 import Numeric
 import System.FilePath ((</>), takeBaseName)
 import System.Exit
 import System.Directory (doesFileExist)
 
+import Algebra.Graph as Graph
+import System.FilePath ((<.>))
+import Control.Exception (SomeException, try)
+import Data.Either.Extra (partitionEithers, eitherToMaybe)
+import qualified Data.Set as Set
+
 import Language.Granule.Syntax.Identifiers
 import Language.Granule.Syntax.Lexer
 import Language.Granule.Syntax.Def
 import Language.Granule.Syntax.Expr
 import Language.Granule.Syntax.Pattern
+import Language.Granule.Syntax.Preprocessor
 import Language.Granule.Syntax.Preprocessor.Markdown
 import Language.Granule.Syntax.Preprocessor.Latex
 import Language.Granule.Syntax.Span
@@ -37,6 +45,7 @@ import Language.Granule.Syntax.Program
 }
 
 %name topLevel TopLevel
+%name moduleSig ModuleSig
 %name expr Expr
 %name tscheme TypeScheme
 %tokentype { Token }
@@ -135,7 +144,7 @@ TopLevel :: { Module }
   | module CONSTR hiding '(' Ids ')' where  NL Defs
       { $9
         { moduleName = constrString $2
-        , moduleHiddenNames = M.fromList $ map (\id -> (id, constrString $2)) $5
+        , moduleHiddenNames = Map.fromList $ map (\id -> (id, constrString $2)) $5
         }
       }
 
@@ -156,9 +165,19 @@ 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) } }
+  | 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) } }
+
+ModuleSig :: { ModuleSignature }
+  : Sig
+      { let (name, tySch, _) = $1 in emptyModuleSignature{ modSigDefinitionContext = [(mkId name, tySch)] } }
+  | Sig NL ModuleSig
+      { let (name, tySch, _) = $1 in $3{ modSigDefinitionContext = (mkId name, tySch) : modSigDefinitionContext $3 } }
+  | DataDecl
+      { emptyModuleSignature{ modSigDataDeclarationContext = [(dataDeclId $1, $1)] } }
+  | DataDecl NL ModuleSig
+      { $3{ modSigDataDeclarationContext = (dataDeclId $1, $1) : modSigDataDeclarationContext $3 } }
 
 NL :: { () }
   : nl NL                     { }
@@ -458,7 +477,7 @@ Guarantee :: { Type }
 Expr :: { Expr () () }
   : let LetBind MultiLet
       {% let (_, pat, mt, expr) = $2
-      	in (mkSpan (getPos $1, getEnd $3)) >>=
+        in (mkSpan (getPos $1, getEnd $3)) >>=
            \sp -> return $ App sp () False
                    (Val (getSpan $3) () False (Abs () pat mt $3)) expr
       }
@@ -536,9 +555,9 @@ MultiLet
   : ';' LetBind MultiLet
     {% let (_, pat, mt, expr) = $2
 
-     	in (mkSpan (getPos $1, getEnd $3)) >>=
+       in (mkSpan (getPos $1, getEnd $3)) >>=
            \sp -> return $ App sp () False
-     	               (Val (getSpan $3) () False (Abs () pat mt $3)) expr }
+                      (Val (getSpan $3) () False (Abs () pat mt $3)) expr }
   | in Expr
     { $2 }
 
@@ -550,7 +569,7 @@ MultiLetEff :: { Expr () () }
 MultiLetEff
   : ';' LetBindEff MultiLetEff
       {% let (_, pat, mt, expr) = $2
-	      in (mkSpan (getPos $1, getEnd $3)) >>=
+        in (mkSpan (getPos $1, getEnd $3)) >>=
              \sp -> return $ LetDiamond sp () False pat mt expr $3
       }
   | in Expr                   { $2 }
@@ -653,6 +672,84 @@ parseError t = do
 parseModule :: FilePath -> String -> Either String Module
 parseModule file input = runReaderT (topLevel $ scanTokens input) file
 
+parseModuleSignature :: FilePath -> String -> Either String ModuleSignature
+parseModuleSignature file input = runReaderT (moduleSig $ scanTokens input) file
+
+type E = String
+
+-- | Given a root module path, discover a GranuleProgram on the filesystem
+readAndPreprocessGranuleProgram :: (?globals :: Globals)
+  => FilePath
+  -> IO (Either E GranuleProgram)
+readAndPreprocessGranuleProgram filePath = do
+  src <- preprocess filePath
+  case parseModule filePath src of
+    Left err -> pure $ Left err
+    Right rootModule -> do
+      let ?globals = ?globals{ globalsRewriter = Nothing }
+      eImports <- traverse tryReadModuleFromDisk (Set.toList $ moduleImports rootModule)
+      case partitionEithers eImports of
+        (errs@(_:_), _) -> pure $ Left "TODO"
+        ([], imports) -> do
+          let granulePrg = GranulePrg
+                { granulePrgRootModule = moduleName rootModule
+                , granulePrgModules = insertIntoModuleMap rootModule Map.empty
+                , granulePrgDependencyGraph = Graph.empty
+                }
+          crawlImportGraph (moduleName rootModule) imports granulePrg
+
+insertIntoModuleMap mod = Map.insert (moduleName mod) mod
+
+crawlImportGraph :: ModuleName -> [Module] -> GranuleProgram -> IO (Either E GranuleProgram)
+crawlImportGraph currentModule imports prg = undefined
+
+tryReadModuleFromDisk :: (?globals :: Globals)
+  => ModuleName
+  -> IO (Either E Module)
+tryReadModuleFromDisk moduleName = do
+  -- search for candidate source files, in the current working directory (TODO: is this always
+  -- well-defined?) or on include path
+  candidates <-
+    sequence
+      [ tryReadAndPreprocessGranuleSourceFile prefix ext
+      | prefix <- [moduleName, includePath </> moduleName], ext <- granuleFileExtensions
+      ]
+
+  case catMaybes candidates of
+    -- No modules found
+    [] -> pure $ Left "module not found"
+
+    -- More than one module found
+    srcs@(_:_:_) -> pure $ Left ("ambiguous module '" ++ moduleName ++ "'")
+
+    -- Exactly one module found
+    [(prefix, ext, src)] -> do
+      let fp = prefix <.> ext
+      let ?globals = ?globals{ globalsSourceFilePath = Just fp }
+      case parseModule fp src of
+        Left err -> pure $ Left err
+        Right mod -> do
+          eModuleSignatureSrc <- try @SomeException (readFile (prefix <.> granuleInterfaceFileExtension))
+          case eModuleSignatureSrc of
+            Left{} -> pure $ Right mod
+            Right moduleSignatureSrc ->
+              case parseModuleSignature fp moduleSignatureSrc of
+                Left{} -> error "TODO"
+                Right sig ->
+                  pure $ Right mod{ moduleSignature = Just sig }
+
+granuleFileExtensions :: [String]
+granuleFileExtensions = ["gr", "gr.md", "gr.tex", "gr.latex"]
+
+granuleInterfaceFileExtension :: String
+granuleInterfaceFileExtension = "gri"
+
+-- | Try to read and preprocess file @prefix@ with extension @ext@, returning @(prefix, ext, contents)@.
+tryReadAndPreprocessGranuleSourceFile :: (?globals :: Globals) => FilePath -> String -> IO (Maybe (FilePath, String, String))
+tryReadAndPreprocessGranuleSourceFile prefix ext = do
+  mbSrc <- eitherToMaybe <$> try @SomeException (preprocess =<< readFile (prefix <.> ext))
+  pure ((prefix, ext,) <$> mbSrc)
+
 -- parseAndDoImportsAndFreshenDefs :: (?globals :: Globals) => String -> IO (AST () (), [Extension])
 -- parseAndDoImportsAndFreshenDefs input = do
 --     (ast, extensions) <- parseDefsAndDoImports input
diff --git a/frontend/src/Language/Granule/Syntax/Pretty.hs b/frontend/src/Language/Granule/Syntax/Pretty.hs
index f273c227a..b67955e45 100644
--- a/frontend/src/Language/Granule/Syntax/Pretty.hs
+++ b/frontend/src/Language/Granule/Syntax/Pretty.hs
@@ -190,9 +190,18 @@ instance Pretty Module where
     <> (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
+
+pretty' :: (?globals :: Globals, Pretty l) => [l] -> String
+pretty' = intercalate "\n\n" . map pretty
+
+instance Pretty ModuleSignature where
+  pretty ModSig
+    { modSigDataDeclarationContext
+    , modSigDefinitionContext
+    , modSigDerivedDefinitions
+    } =
+        pretty' (map snd modSigDataDeclarationContext)
+        <> "\n\n" <> pretty' (map snd modSigDefinitionContext)
 
 instance Pretty v => Pretty (Def v a) where
     pretty (Def _ v _ eqs (Forall _ [] [] t))
diff --git a/frontend/src/Language/Granule/Syntax/Program.hs b/frontend/src/Language/Granule/Syntax/Program.hs
index ce4048bd7..21ba9aea0 100644
--- a/frontend/src/Language/Granule/Syntax/Program.hs
+++ b/frontend/src/Language/Granule/Syntax/Program.hs
@@ -9,26 +9,25 @@ 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.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)
-import System.FilePath ((<.>))
-import Control.Exception (try)
+
 
 -- | Invariants:
 -- * rootModule \in modules
 -- if a Module has a module signature, then it is assumed that type checking can be skipped
 data GranuleProgram = GranulePrg
-  { rootModule :: ModuleName
-  , modules :: Map ModuleName Module
-  , dependencyGraph :: AdjacencyMap ModuleName
+  { granulePrgRootModule :: ModuleName
+  , granulePrgModules :: Map ModuleName Module
+  , granulePrgDependencyGraph :: AdjacencyMap ModuleName
   }
+  deriving (Show, Eq)
 
 type ModuleName = String
 
@@ -41,6 +40,7 @@ data Module = Mod
   , moduleImports :: Set ModuleName
   , moduleHiddenNames :: Map Id ModuleName -- map from names to the module hiding them
   }
+  deriving (Show, Eq)
 
 emptyModule :: Module
 emptyModule = Mod
@@ -70,33 +70,18 @@ emptyModule = Mod
 --     }
 
 data ModuleSignature = ModSig
-  { dataDeclarationContext :: Ctxt DataDecl
-  , definitionContext :: Ctxt TypeScheme
-  , derivedDefinitions :: [Def () ()]
+  { modSigDataDeclarationContext :: Ctxt DataDecl
+  , modSigDefinitionContext :: Ctxt TypeScheme
+  , modSigDerivedDefinitions :: [Def () ()]
   }
+  deriving (Show, Eq)
 
-type E = String
-
-readAndPreprocessGranuleProgram :: (?globals :: Globals)
-  => FilePath
-  -> IO (Either E GranuleProgram)
-readAndPreprocessGranuleProgram filePath = do
-  src <- preprocess filePath
-  rootModule <- parseModule src
-  let ?gloabals = ?globals { globalsRewriter = Nothing }
-  moduleImports rootModule
-
-
-goImports :: (?globals :: Globals)
-  => Module
-  -> Set ModuleName
-  -> IO (Either E [(ModuleName, ModuleName)])
-goImports rootModule imports = do
-  let (foo :: _) = traverse (try . readFile) [fp <.> ext | ext <- granuleFileTypes]
-  undefined
-
-granuleFileTypes = ["gr", "gr.md", "gr.tex", "gr.latex"]
-
+emptyModuleSignature :: ModuleSignature
+emptyModuleSignature = ModSig
+  { modSigDataDeclarationContext = empty
+  , modSigDefinitionContext = empty
+  , modSigDerivedDefinitions = empty
+  }
 
 
 -- fileLocal <- doesFileExist i
diff --git a/test.gr b/test.gr
new file mode 100644
index 000000000..54d4118ed
--- /dev/null
+++ b/test.gr
@@ -0,0 +1,6 @@
+data Signal a = Tick a (Signal a)
+
+data Addr = A Int
+
+ram : Signal (Addr, Int) -> Signal (Addr, Int [])
+ram = ram
diff --git a/work-in-progress/ref.gr b/work-in-progress/ref.gr
new file mode 100644
index 000000000..e7d6c59ff
--- /dev/null
+++ b/work-in-progress/ref.gr
@@ -0,0 +1,9 @@
+
+-- Doubly linked list node
+data DLN a
+  = Node a (Ref (DLN a)) (Ref (DLN a))
+  | Null
+
+-- append : forall a. a -> DLN a -> DLN a
+-- append x (Node elem prev Null) = Node elem prev (alloc )
+-- append x (Node elem prev next) = Node elem prev (mapRef (append x) next);

From b0954f33751b6d7ac09dfb880bd93512d1cb0402 Mon Sep 17 00:00:00 2001
From: Vilem Liepelt <17603372+buggymcbugfix@users.noreply.github.com>
Date: Mon, 18 Dec 2023 17:24:27 +0100
Subject: [PATCH 3/3] moar wip

---
 .../src/Language/Granule/Checker/Checker.hs   |  4 +--
 .../Language/Granule/Syntax/Preprocessor.hs   | 15 ++++++-----
 .../src/Language/Granule/Interpreter.hs       | 27 ++++---------------
 test.gr                                       |  7 ++++-
 4 files changed, 22 insertions(+), 31 deletions(-)

diff --git a/frontend/src/Language/Granule/Checker/Checker.hs b/frontend/src/Language/Granule/Checker/Checker.hs
index 194c14ff4..a9bb002db 100644
--- a/frontend/src/Language/Granule/Checker/Checker.hs
+++ b/frontend/src/Language/Granule/Checker/Checker.hs
@@ -335,8 +335,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
+    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)
diff --git a/frontend/src/Language/Granule/Syntax/Preprocessor.hs b/frontend/src/Language/Granule/Syntax/Preprocessor.hs
index 87f0109fc..8c7ce45f5 100644
--- a/frontend/src/Language/Granule/Syntax/Preprocessor.hs
+++ b/frontend/src/Language/Granule/Syntax/Preprocessor.hs
@@ -36,9 +36,12 @@ preprocess filePath
     extension = reverse . takeWhile (/= '.') . reverse $ filePath
 
     -- (file extension, (stripNonGranule, destructivePreprocessor))
-    acceptedFormats =
-      [ ("gr",    (id,         id))
-      , ("md",    (unMarkdown, processGranuleMarkdown id literateEnvName))
-      , ("tex",   (unLatex,    processGranuleLatex id literateEnvName))
-      , ("latex", (unLatex,    processGranuleLatex id literateEnvName))
-      ]
+
+acceptedFormats =
+  [ ("gr",    (id,         id))
+  , ("md",    (unMarkdown, processGranuleMarkdown id literateEnvName))
+  , ("tex",   (unLatex,    processGranuleLatex id literateEnvName))
+  , ("latex", (unLatex,    processGranuleLatex id literateEnvName))
+  ]
+
+data GranuleFileExtension = Gr | GrMd | GrTex | GrLatex
diff --git a/interpreter/src/Language/Granule/Interpreter.hs b/interpreter/src/Language/Granule/Interpreter.hs
index dfe7171c9..7a1e6ae35 100755
--- a/interpreter/src/Language/Granule/Interpreter.hs
+++ b/interpreter/src/Language/Granule/Interpreter.hs
@@ -208,37 +208,21 @@ parseGrFlags
 
 
 data GrConfig = GrConfig
-  { grRewriter        :: Maybe (String -> String)
-  , grKeepBackup      :: Maybe Bool
-  , grLiterateEnvName :: Maybe String
-  , grShowVersion     :: Bool
+  { grShowVersion     :: Bool
   , grGlobals         :: Globals
   }
 
-rewriter :: GrConfig -> Maybe (String -> String)
-rewriter c = grRewriter c <|> Nothing
 
-keepBackup :: GrConfig -> Bool
-keepBackup = fromMaybe False . grKeepBackup
-
-literateEnvName :: GrConfig -> String
-literateEnvName = fromMaybe "granule" . grLiterateEnvName
 
 instance Semigroup GrConfig where
   c1 <> c2 = GrConfig
-    { grRewriter    = grRewriter    c1 <|> grRewriter  c2
-    , grKeepBackup      = grKeepBackup      c1 <|> grKeepBackup      c2
-    , grLiterateEnvName = grLiterateEnvName c1 <|> grLiterateEnvName c2
-    , grGlobals         = grGlobals         c1 <>  grGlobals         c2
+    { grGlobals         = grGlobals         c1 <>  grGlobals         c2
     , grShowVersion     = grShowVersion     c1 ||  grShowVersion     c2
     }
 
 instance Monoid GrConfig where
   mempty = GrConfig
-    { grRewriter    = Nothing
-    , grKeepBackup      = Nothing
-    , grLiterateEnvName = Nothing
-    , grGlobals         = mempty
+    { grGlobals         = mempty
     , grShowVersion     = False
     }
 
@@ -248,7 +232,6 @@ getGrConfig = do
     configHome <- readUserConfig (grGlobals configCLI)
     pure (globPatterns, configCLI <> configHome)
   where
-  -- TODO: UNIX specific
     readUserConfig :: Globals -> IO GrConfig
     readUserConfig globals = do
       let ?globals = globals
@@ -420,7 +403,7 @@ parseGrConfig = info (go <**> helper) $ briefDesc
             <> (help . unwords)
             [ "Index of synthesised programs"
             , "Defaults to"
-            , show synthIndex 
+            , show synthIndex
             ]
 
         grRewriter
@@ -518,4 +501,4 @@ instance UserMsg InterpreterError where
   msg (EvalError m) = m
   msg (FatalError m) = m
   msg NoEntryPoint = "Program entry point `" <> entryPoint <> "` not found. A different one can be specified with `--entry-point`."
-  msg (NoMatchingFiles p) = "The glob pattern `" <> p <> "` did not match any files."
\ No newline at end of file
+  msg (NoMatchingFiles p) = "The glob pattern `" <> p <> "` did not match any files."
diff --git a/test.gr b/test.gr
index 54d4118ed..43fe11c8c 100644
--- a/test.gr
+++ b/test.gr
@@ -1,6 +1,11 @@
 data Signal a = Tick a (Signal a)
 
-data Addr = A Int
+data Addr = Ad Int
 
 ram : Signal (Addr, Int) -> Signal (Addr, Int [])
 ram = ram
+
+system : Int
+system input =
+    let writePort = writePort in
+    let readPort = ram writePort in 1