[ app ] add --version flag and fixed warnings and formatting

2024-11-22 23:23:06 +03:00 · 2022-03-25 00:52:30 +01:00 · 2022-03-25 00:52:30 +01:00 · 17a0577ee7
commit 17a0577ee7
parent 02474c837f
47 changed files with 198 additions and 3192 deletions
--- a/app/Commands/Extra.hs
+++ b/app/Commands/Extra.hs
@ -1,12 +1,12 @@
 module Commands.Extra where

-import Options.Applicative
 import MiniJuvix.Prelude hiding (Doc)
+import Options.Applicative

 parseInputFile :: Parser FilePath
 parseInputFile =
- argument
-      str
-      ( metavar "MINIJUVIX_FILE"
-          <> help "Path to a .mjuvix file"
-      )
+  argument
+    str
+    ( metavar "MINIJUVIX_FILE"
+        <> help "Path to a .mjuvix file"
+    )
--- a/app/Commands/MicroJuvix.hs
+++ b/app/Commands/MicroJuvix.hs
@ -1,9 +1,10 @@
 {-# LANGUAGE ApplicativeDo #-}
+
 module Commands.MicroJuvix where

 import Commands.Extra
-import Options.Applicative
 import MiniJuvix.Prelude hiding (Doc)
+import Options.Applicative

 newtype MicroJuvixOptions = MicroJuvixOptions
  { _mjuvixInputFile :: FilePath
--- a/app/Commands/MiniHaskell.hs
+++ b/app/Commands/MiniHaskell.hs
@ -1,9 +1,10 @@
 {-# LANGUAGE ApplicativeDo #-}
+
 module Commands.MiniHaskell where

 import Commands.Extra
-import Options.Applicative
 import MiniJuvix.Prelude hiding (Doc)
+import Options.Applicative

 newtype MiniHaskellOptions = MiniHaskellOptions
  { _mhaskellInputFile :: FilePath
--- a/app/Commands/Termination.hs
+++ b/app/Commands/Termination.hs
@ -1,15 +1,16 @@
 {-# LANGUAGE ApplicativeDo #-}
+
 module Commands.Termination where

 import Commands.Extra
-import qualified Data.Text as Text
 import Control.Monad.Extra
-import Options.Applicative
-import qualified MiniJuvix.Syntax.Abstract.Pretty.Base as A
+import qualified Data.Text as Text
 import MiniJuvix.Prelude hiding (Doc)
+import qualified MiniJuvix.Syntax.Abstract.Pretty.Base as A
+import Options.Applicative

-data TerminationCommand =
-  Calls CallsOptions
+data TerminationCommand
+  = Calls CallsOptions
  | CallGraph CallGraphOptions

 data CallsOptions = CallsOptions
@ -33,14 +34,18 @@ parseCalls = do
          <> help "Show the unique number of each identifier"
      )
  _callsFunctionNameFilter <-
-    fmap msum . optional $ nonEmpty . Text.words <$> option str
-      ( long "function"
-          <> short 'f'
-          <> metavar "fun1 fun2 ..."
-          <> help "Only shows the specified functions"
-      )
+    fmap msum . optional $
+      nonEmpty . Text.words
+        <$> option
+          str
+          ( long "function"
+              <> short 'f'
+              <> metavar "fun1 fun2 ..."
+              <> help "Only shows the specified functions"
+          )
  _callsShowDecreasingArgs <-
-    option decrArgsParser
+    option
+      decrArgsParser
      ( long "show-decreasing-args"
          <> short 'd'
          <> value A.ArgRel
@ -48,24 +53,26 @@ parseCalls = do
      )
  pure CallsOptions {..}
  where
-  decrArgsParser :: ReadM A.ShowDecrArgs
-  decrArgsParser = eitherReader $ \s ->
-    case map toLower s of
-      "argument" -> return A.OnlyArg
-      "relation" -> return A.OnlyRel
-      "both" -> return A.ArgRel
-      _ -> Left "bad argument"
-
+    decrArgsParser :: ReadM A.ShowDecrArgs
+    decrArgsParser = eitherReader $ \s ->
+      case map toLower s of
+        "argument" -> return A.OnlyArg
+        "relation" -> return A.OnlyRel
+        "both" -> return A.ArgRel
+        _ -> Left "bad argument"

 parseCallGraph :: Parser CallGraphOptions
 parseCallGraph = do
  _graphInputFile <- parseInputFile
  _graphFunctionNameFilter <-
-    fmap msum . optional $ nonEmpty . Text.words <$> option str
-      ( long "function"
-          <> short 'f'
-          <> help "Only shows the specified function"
-      )
+    fmap msum . optional $
+      nonEmpty . Text.words
+        <$> option
+          str
+          ( long "function"
+              <> short 'f'
+              <> help "Only shows the specified function"
+          )
  pure CallGraphOptions {..}

 parseTerminationCommand :: Parser TerminationCommand
--- a/app/Main.hs
+++ b/app/Main.hs
@ -1,30 +1,35 @@
 {-# LANGUAGE ApplicativeDo #-}
+
 module Main (main) where

+--------------------------------------------------------------------------------
+
+import Commands.Extra
+import Commands.MicroJuvix
+import Commands.MiniHaskell
+import Commands.Termination as T
 import Control.Monad.Extra
+import MiniJuvix.Prelude hiding (Doc)
+import qualified MiniJuvix.Syntax.Abstract.Pretty.Ansi as A
 import qualified MiniJuvix.Syntax.Concrete.Language as M
 import qualified MiniJuvix.Syntax.Concrete.Parser as M
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ansi as M
+import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base (defaultOptions)
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as M
+import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Text as T
+import qualified MiniJuvix.Syntax.Concrete.Scoped.Scoper as M
 import qualified MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi as Micro
 import qualified MiniJuvix.Termination as T
-import qualified MiniJuvix.Translation.ScopedToAbstract as A
-import qualified MiniJuvix.Translation.AbstractToMicroJuvix as Micro
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as M
 import qualified MiniJuvix.Termination.CallGraph as A
-import qualified MiniJuvix.Syntax.Abstract.Pretty.Base as A
-import qualified MiniJuvix.Syntax.Concrete.Scoped.Scoper as M
-import MiniJuvix.Prelude hiding (Doc)
+import qualified MiniJuvix.Translation.AbstractToMicroJuvix as Micro
+import qualified MiniJuvix.Translation.ScopedToAbstract as A
+import MiniJuvix.Utils.Version (runDisplayVersion)
 import Options.Applicative
 import Options.Applicative.Help.Pretty
 import Text.Show.Pretty hiding (Html)
-import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Html
-import MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base (defaultOptions)
-import qualified MiniJuvix.Syntax.Abstract.Pretty.Ansi as A
-import Commands.Extra
-import Commands.Termination as T
-import Commands.MiniHaskell
-import Commands.MicroJuvix
+
+--------------------------------------------------------------------------------

 data Command
  = Scope ScopeOptions
@ -33,6 +38,7 @@ data Command
  | Termination TerminationCommand
  | MiniHaskell MiniHaskellOptions
  | MicroJuvix MicroJuvixOptions
+  | DisplayVersion

 data ScopeOptions = ScopeOptions
  { _scopeRootDir :: FilePath,
@ -61,21 +67,22 @@ parseHtml = do
      ( long "recursive"
          <> help "export imported modules recursively"
      )
-  _htmlTheme <- option (eitherReader parseTheme)
+  _htmlTheme <-
+    option
+      (eitherReader parseTheme)
      ( long "theme"
          <> metavar "THEME"
-          <> value Nord
+          <> value Ayu
          <> showDefault
          <> help "selects a theme: ayu (light); nord (dark)"
      )
  pure HtmlOptions {..}
  where
-  parseTheme :: String -> Either String Theme
-  parseTheme s = case s of
-    "nord" -> Right Nord
-    "ayu" -> Right Ayu
-    _ -> Left $ "unrecognised theme: " <> s
-
+    parseTheme :: String -> Either String Theme
+    parseTheme s = case s of
+      "nord" -> Right Nord
+      "ayu" -> Right Ayu
+      _ -> Left $ "unrecognised theme: " <> s

 parseParse :: Parser ParseOptions
 parseParse = do
@ -99,11 +106,12 @@ parseScope = do
          <> help "Root directory"
      )
  _scopeInputFiles <-
-    some $ argument
-      str
-      ( metavar "MINIJUVIX_FILE(s)"
-          <> help "Path to one ore more .mjuvix files"
-      )
+    some $
+      argument
+        str
+        ( metavar "MINIJUVIX_FILE(s)"
+            <> help "Path to one ore more MiniJuvix files"
+        )
  _scopeShowIds <-
    switch
      ( long "show-name-ids"
@ -117,10 +125,16 @@ parseScope = do
  _scopeNoColors <-
    switch
      ( long "no-colors"
-          <> help "Disable ansi formatting"
+          <> help "Disable ANSI formatting"
      )
  pure ScopeOptions {..}

+parseDisplayVersion :: Parser Command
+parseDisplayVersion =
+  flag'
+    DisplayVersion
+    (long "version" <> short 'v' <> help "Print the version and exit")
+
 descr :: ParserInfo Command
 descr =
  info
@ -133,20 +147,23 @@ descr =
  where
    headDoc :: Doc
    headDoc = dullblue $ bold $ underline "MiniJuvix help"
+
    foot :: Doc
-    foot = bold "maintainers: " <> "jan@heliax.dev; jonathan@heliax.dev"
+    foot = bold "maintainers: " <> "The MiniJuvix Team"

 parseCommand :: Parser Command
 parseCommand =
-  hsubparser $
-    mconcat
-      [ commandParse,
-        commandScope,
-        commandHtml,
-        commandTermination,
-        commandMicroJuvix,
-        commandMiniHaskell
-      ]
+  parseDisplayVersion
+    <|> ( hsubparser $
+            mconcat
+              [ commandParse,
+                commandScope,
+                commandHtml,
+                commandTermination,
+                commandMicroJuvix,
+                commandMiniHaskell
+              ]
+        )
  where
    commandMicroJuvix :: Mod CommandFields Command
    commandMicroJuvix = command "microjuvix" minfo
@ -155,7 +172,7 @@ parseCommand =
        minfo =
          info
            (MicroJuvix <$> parseMicroJuvix)
-            (progDesc "Translate a .mjuvix file to MicroJuvix")
+            (progDesc "Translate a MiniJuvix file to MicroJuvix")

    commandMiniHaskell :: Mod CommandFields Command
    commandMiniHaskell = command "minihaskell" minfo
@ -164,7 +181,7 @@ parseCommand =
        minfo =
          info
            (MiniHaskell <$> parseMiniHaskell)
-            (progDesc "Translate a .mjuvix file to MiniHaskell")
+            (progDesc "Translate a MiniJuvix file to MiniHaskell")

    commandParse :: Mod CommandFields Command
    commandParse = command "parse" minfo
@ -173,7 +190,7 @@ parseCommand =
        minfo =
          info
            (Parse <$> parseParse)
-            (progDesc "Parse a .mjuvix file")
+            (progDesc "Parse a MiniJuvix file")

    commandHtml :: Mod CommandFields Command
    commandHtml = command "html" minfo
@ -182,7 +199,8 @@ parseCommand =
        minfo =
          info
            (Html <$> parseHtml)
-            (progDesc "Generate html for a .mjuvix file")
+            (progDesc "Generate HTML for a MiniJuvix file")
+
    commandScope :: Mod CommandFields Command
    commandScope = command "scope" minfo
      where
@ -190,7 +208,8 @@ parseCommand =
        minfo =
          info
            (Scope <$> parseScope)
-            (progDesc "Parse and scope a .mjuvix file")
+            (progDesc "Parse and scope a MiniJuvix file")
+
    commandTermination :: Mod CommandFields Command
    commandTermination = command "termination" minfo
      where
@ -200,41 +219,31 @@ parseCommand =
            (Termination <$> parseTerminationCommand)
            (progDesc "Subcommands related to termination checking")

-
 mkScopePrettyOptions :: ScopeOptions -> M.Options
 mkScopePrettyOptions ScopeOptions {..} =
  M.defaultOptions
    { M._optShowNameId = _scopeShowIds,
      M._optInlineImports = _scopeInlineImports
-
    }

 parseModuleIO :: FilePath -> IO (M.Module 'M.Parsed 'M.ModuleTop)
 parseModuleIO = fromRightIO id . M.runModuleParserIO

-fromRightIO' :: (e -> IO ()) -> IO (Either e r) -> IO r
-fromRightIO' pp = do
-  eitherM ifLeft return
-  where
-  ifLeft e = pp e >> exitFailure
-
-fromRightIO :: (e -> Text) -> IO (Either e r) -> IO r
-fromRightIO pp = fromRightIO' (putStrLn . pp)
-
 go :: Command -> IO ()
 go c = do
  root <- getCurrentDirectory
  case c of
+    DisplayVersion -> runDisplayVersion
    Scope opts@ScopeOptions {..} -> do
      forM_ _scopeInputFiles $ \scopeInputFile -> do
        m <- parseModuleIO scopeInputFile
        s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
        printer (mkScopePrettyOptions opts) s
-        where
-          printer
-            | not _scopeNoColors = M.printPrettyCode
-            | otherwise = T.printPrettyCode
-
+      where
+        printer :: M.Options -> M.Module 'M.Scoped 'M.ModuleTop -> IO ()
+        printer
+          | not _scopeNoColors = M.printPrettyCode
+          | otherwise = T.printPrettyCode
    Parse ParseOptions {..} -> do
      m <- parseModuleIO _parseInputFile
      if _parseNoPrettyShow then print m else pPrint m
@ -261,7 +270,7 @@ go c = do
      m <- parseModuleIO _callsInputFile
      s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
      a <- fromRightIO' putStrLn (return $ A.translateModule s)
-      let callMap0 =  T.buildCallMap a
+      let callMap0 = T.buildCallMap a
          callMap = case _callsFunctionNameFilter of
            Nothing -> callMap0
            Just f -> T.filterCallMap f callMap0
--- a/lab/Core.agda
+++ b/lab/Core.agda
@ -1,359 +0,0 @@
-{-
-This module exposes the Internal syntax. A term is either checkable or
-inferable. As the name indicates, a term of type CheckableTerm is a
-term we must check. Similarly, a term of type InferableTerm, it is a
-term we can infer.
-}
-
-module MiniJuvix.Syntax.Core 
-  where
-
--------------------------------------------------------------------------------
-
-open import Haskell.Prelude
-open import Agda.Builtin.Equality
-
--------------------------------------------------------------------------------
-- Haskell stuff 
--------------------------------------------------------------------------------
-
-{-# FOREIGN AGDA2HS
-{-# OPTIONS_GHC -fno-warn-missing-export-lists #-}
-{-# OPTIONS_GHC -fno-warn-unused-matches #-}
-{-# OPTIONS_GHC -fno-warn-unused-imports #-}
-#-}
-
-{-# FOREIGN AGDA2HS
--------------------------------------------------------------------------------
-
-import MiniJuvix.Prelude
-
--------------------------------------------------------------------------------
-- Quantity (a.k.a. Usage)
--------------------------------------------------------------------------------
-#-}
-
-data Quantity : Set where
-  Zero One Many : Quantity
-{-# COMPILE AGDA2HS Quantity #-}
-
-instance
-  QuantityEq : Eq Quantity
-  QuantityEq ._==_ Zero Zero = true
-  QuantityEq ._==_ One  One  = true
-  QuantityEq ._==_ Many Many = true
-  QuantityEq ._==_ _    _    = false
-{-# COMPILE AGDA2HS QuantityEq #-}
- 
-compareQuantity : Quantity -> Quantity -> Ordering
-compareQuantity Zero  Zero = EQ
-compareQuantity Zero  _    = LT
-compareQuantity _    Zero  = GT
-compareQuantity One  One   = EQ
-compareQuantity One  _     = LT
-compareQuantity _    One   = GT
-compareQuantity Many Many  = EQ
-{-# COMPILE AGDA2HS compareQuantity #-}
-
-instance
-  QuantityOrd : Ord Quantity
-  QuantityOrd .compare  = compareQuantity 
-  QuantityOrd ._<_  x y = compareQuantity x y == LT
-  QuantityOrd ._>_  x y = compareQuantity x y == GT
-  QuantityOrd ._<=_ x y = compareQuantity x y /= GT
-  QuantityOrd ._>=_ x y = compareQuantity x y /= LT
-  QuantityOrd .max  x y = if compareQuantity x y == LT then y else x
-  QuantityOrd .min  x y = if compareQuantity x y == GT then y else x
-  -- Using ordFromCompare didnn' work, I might need to open an issue
-  -- for this in agda2hs, Idk.
-
-- The type of usages forms an ordered semiring.
-
-instance
-  QuantitySemigroup : Semigroup Quantity
-  QuantitySemigroup ._<>_ Zero _ = Zero
-  QuantitySemigroup ._<>_ One m = m
-  QuantitySemigroup ._<>_ Many Zero = Zero
-  QuantitySemigroup ._<>_ Many One = Many
-  QuantitySemigroup ._<>_ Many Many = Many
-
-  QuantityMon : Monoid Quantity
-  QuantityMon .mempty = Zero
-
-  QuantitySemiring : Semiring Quantity
-  QuantitySemiring .one = One
-  QuantitySemiring .times Zero _ = Zero
-  QuantitySemiring .times One m = m
-  QuantitySemiring .times Many Zero = Zero
-  QuantitySemiring .times Many One = Many
-  QuantitySemiring .times Many Many = Many
-
-{-# COMPILE AGDA2HS QuantityOrd #-}
-{-# COMPILE AGDA2HS QuantitySemigroup #-}
-{-# COMPILE AGDA2HS QuantityMon #-}
-{-# COMPILE AGDA2HS QuantitySemiring #-}
-
--------------------------------------------------------------------------------
-- Being relevant for a term is to have non zero quantity.
-
-data Relevance : Set where
-  Relevant   : Relevance  -- terms to compute.
-  Irrelevant : Relevance  -- terms to contemplate (for type formation).
-{-# COMPILE AGDA2HS Relevance #-}
-{-# FOREIGN AGDA2HS
-deriving stock instance Eq Relevance
-deriving stock instance Ord Relevance
-#-}
-
-relevancy : Quantity → Relevance
-relevancy Zero = Irrelevant
-relevancy _    = Relevant
-{-# COMPILE AGDA2HS relevancy #-}
-
--------------------------------------------------------------------------------
-- Variables. Relevant on the following design is the separation for a
-- variable between Bound and Free as a data constructr, due to
-- McBride and McKinna in "Functional Pearl: I am not a Number—I am a
-- Free Variable". 
--------------------------------------------------------------------------------
-
-- DeBruijn index.
-Index : Set
-Index = Nat
-{-# COMPILE AGDA2HS Index #-}
-
-- A variable can be "bound", "binding bound", or simply free. For
-- example, consider  the term "x(λy.y)". The variable x is free, the
-- first y is a binding bound variable, and the latter y is bound.
-
-BindingName : Set
-BindingName = String
-{-# COMPILE AGDA2HS BindingName #-}
-
-- A named variable can be in a local or global enviroment. In the
-- lambda term above, for example, the second occurrence of y is
-- globally bound. However, inside the the body of the lambda, the
-- variable is local free.
-
-data Name : Set where
-  -- the variable has zero binding 
-  Global : String → Name
-  -- the variable has a binding in its scope.
-  Local : BindingName → Index → Name
-{-# COMPILE AGDA2HS Name #-}
-
-instance
-  nameEq : Eq Name
-  nameEq ._==_ (Global x) (Global y) = x == y
-  nameEq ._==_ (Local x1 y1) (Local x2 y2) = x1 == x2 && y1 == y2
-  nameEq ._==_ _ _ = false
-{-# COMPILE AGDA2HS nameEq #-}
-
-- A variable is then a number indicating its DeBruijn index.
-- Otherwise, it is free, with an identifier as a name, or
-- inside 
-data Variable : Set where
-  Bound : Index → Variable
-  Free  : Name → Variable
-{-# COMPILE AGDA2HS Variable #-}
-
-instance
-  variableEq : Eq Variable 
-  variableEq ._==_ (Bound x) (Bound y) = x == y
-  variableEq ._==_ (Free x) (Free y) = x == y
-  variableEq ._==_ _ _ = false
-{-# COMPILE AGDA2HS variableEq #-}
-
-- TODO: May I want to have Instances of Ord, Functor, Applicative, Monad?
-
-{-# FOREIGN AGDA2HS
--------------------------------------------------------------------------------
-#-}
-
-{- 
-Core syntax follows the pattern design for bidirectional typing
-algorithmgs in [Dunfield and Krishnaswami, 2019]. Pfenning's principle
-is one of such criterion and stated as follows.
-
-1. If the rule is an introduction rule, make the principal judgement
-   "checking", and 
-2. if the rule is an elimination rule, make the principal judgement
-   "synthesising".
-   
-Jargon:
- Principal connective of a rule:
-  - for an introduction rule is the connective that is being
-    introduced.
-  - for a elimination rule is the connective that is eliminated.
- Principal Judgement of a rule is the judgment that contains the
-  principal connective.
-}
-
-{-# FOREIGN AGDA2HS
--------------------------------------------------------------------------------
-- Type-checkable terms.
--------------------------------------------------------------------------------
-#-}
-
-data CheckableTerm : Set
-data InferableTerm : Set
-
-data CheckableTerm where
-  {- Universe types. 
-  See the typing rule Univ⇐.
-  -}
-  UniverseType : CheckableTerm
-  {- Dependent function types. 
-  See the typing rules →F⇐ and →I⇐.
-    1. (Π[ x :ρ S ] P x) : U
-    2. (λ x. t) : Π[ x :ρ S ] P x
-  -}
-  PiType : Quantity → BindingName → CheckableTerm → CheckableTerm → CheckableTerm
-  Lam : BindingName → CheckableTerm → CheckableTerm
-  {- Dependent tensor product types. 
-  See the typing rules ⊗-F-⇐,  ⊗-I₀⇐, and ⊗-I₁⇐.
-    1. * S ⊗ T : U
-    2. (M , N) : S ⊗ T
-  -}
-  TensorType : Quantity → BindingName → CheckableTerm → CheckableTerm → CheckableTerm
-  TensorIntro : CheckableTerm → CheckableTerm → CheckableTerm
-  {- Unit types. 
-  See the typing rule 1-F-⇐ and 1-I-⇐.
-    1. 𝟙 : U
-    2. ⋆ : 𝟙
-  -}
-  UnitType : CheckableTerm
-  Unit : CheckableTerm
-  {- Disjoint sum types.
-  See the typing rules
-    1. S + T : U
-    2. inl x : S + T
-    3. inr x : S + T
-  -}
-  SumType : CheckableTerm → CheckableTerm → CheckableTerm
-  Inl : CheckableTerm → CheckableTerm
-  Inr : CheckableTerm → CheckableTerm
-  -- Inferrable terms are clearly checkable, see typing rule Inf⇐.
-  Inferred : InferableTerm → CheckableTerm
-
-{-# COMPILE AGDA2HS CheckableTerm #-}
-
-{-# FOREIGN AGDA2HS
--------------------------------------------------------------------------------
-- Type-inferable terms (a.k.a terms that synthesise)
--------------------------------------------------------------------------------
-#-}
-
-data InferableTerm where
-  -- | Variables, typing rule Var⇒. 
-  Var : Variable → InferableTerm
-  -- | Annotations, typing rule Ann⇒.
-  {- Maybe, I want to have the rules here like this:
-  
-    OΓ ⊢ S ⇐0 𝕌     Γ ⊢ M ⇐0 𝕌
-    ────────────────────────────── Ann⇒
-           Γ ⊢ (M : S) ⇒ S
-  -}
-  Ann : CheckableTerm → CheckableTerm → InferableTerm
-  -- |  Application (eliminator).
-  App : InferableTerm → CheckableTerm → InferableTerm
-  -- | Dependent Tensor product eliminator. See section 2.1.3 in Atkey 2018.
-  -- let z@(u, v) = M in N :^q (a ⊗ b))
-  TensorTypeElim
-    : Quantity       -- q is the multiplicity of the eliminated pair.
-    → BindingName          -- z is the name of the variable binding the pair in the
-                     -- type annotation of the result of elimination.
-    → BindingName          -- u is the name of the variable binding the first element.
-    → BindingName          -- v is the name of the variable binding the second element.
-    → InferableTerm  -- (u,v) is the eliminated pair.
-    → CheckableTerm  -- Result of the elimination.
-    → CheckableTerm  -- Type annotation of the result of elimination.
-    → InferableTerm
-  -- | Sum type eliminator (a.k.a. case)
-  -- let (z : S + T) in (case z of {(inl u) ↦ r1; (inr v) ↦ r2}  :^q  T) 
-  SumTypeElim        -- Case
-    :  Quantity      -- Multiplicity of the sum contents.
-    →  BindingName         -- Name of the variable binding the sum in the type
-                     -- annotation of the result of elimination.
-    → InferableTerm  -- The eliminated sum.
-    → BindingName          -- u is the name of the variable binding the left element.
-    → CheckableTerm  -- r1 is the result of the elimination in case the sum contains
-                     -- the left element.
-    → BindingName          -- v is the name of the variable binding the right element.
-    → CheckableTerm  -- r2 is the result of the elimination in case the sum contains
-                     -- the right element.
-    → CheckableTerm  -- Type annotation of the result of the elimination.
-    → InferableTerm
-{-# COMPILE AGDA2HS InferableTerm #-}
-
-{-# FOREIGN AGDA2HS
--------------------------------------------------------------------------------
-- Term Equality
--------------------------------------------------------------------------------
-#-}
-
-checkEq : CheckableTerm → CheckableTerm → Bool
-inferEq : InferableTerm → InferableTerm → Bool
-
-- We below explicitly use `checkEq` and `inferEq` to have a more
-- reliable Haskell output using Agda2HS. The traditional way gives an
-- extraneous instance definitions.
-
-checkEq UniverseType UniverseType = true
-checkEq (PiType q₁ _ a₁ b₁) (PiType q₂ _ a₂ b₂) 
-  = q₁ == q₂ && checkEq a₁ a₂ && checkEq b₁ b₂
-checkEq (TensorType q₁ _ a₁ b₁) (TensorType q₂ _ a₂ b₂)
-   = q₁ == q₂ && checkEq a₁ a₂ &&  checkEq b₁ b₂
-checkEq (TensorIntro x₁ y₁) (TensorIntro x₂ y₂) = checkEq x₁ x₂ && checkEq y₁ y₂
-checkEq UnitType UnitType = true
-checkEq Unit Unit = true
-checkEq (SumType x₁ y₁) (SumType x₂ y₂) = checkEq x₁ x₂ && checkEq y₁ y₂
-checkEq (Inl x) (Inl y) = checkEq  x y
-checkEq (Inr x) (Inr y) = checkEq  x y
-checkEq (Inferred x) (Inferred y) = inferEq x y
-checkEq _ _ = false
-{-# COMPILE AGDA2HS checkEq #-}
-
-inferEq (Var x) (Var y) = x == y
-inferEq (Ann x₁ y₁) (Ann x₂ y₂) = checkEq x₁ x₂ &&  checkEq y₁ y₂
-inferEq (App x₁ y₁) (App x₂ y₂) =  inferEq x₁ x₂ &&  checkEq y₁ y₂
-inferEq (TensorTypeElim q₁ _ _ _ a₁ b₁ c₁) (TensorTypeElim q₂ _ _ _ a₂ b₂ c₂) 
-  = q₁ == q₂ &&  inferEq a₁ a₂ &&  checkEq b₁ b₂ &&  checkEq c₁ c₂
-inferEq (SumTypeElim q₁ _ x₁ _ a₁ _ b₁ c₁) 
-      (SumTypeElim q₂ _ x₂ _ a₂ _ b₂ c₂)
-  = q₁ == q₂ &&  inferEq x₁ x₂ && checkEq a₁ a₂ &&  checkEq b₁ b₂ &&  checkEq c₁ c₂
-inferEq _ _ = false
-{-# COMPILE AGDA2HS inferEq #-}
-
-instance
-  CheckableTermEq : Eq CheckableTerm
-  CheckableTermEq ._==_ = checkEq
-{-# COMPILE AGDA2HS CheckableTermEq #-}
-
-instance
-  InferableTermEq : Eq InferableTerm
-  InferableTermEq ._==_ = inferEq
-{-# COMPILE AGDA2HS InferableTermEq #-}
-
-data Term : Set where
-  Checkable : CheckableTerm → Term  -- terms with a type checkable.
-  Inferable : InferableTerm → Term  -- terms that which types can be inferred.
-{-# COMPILE AGDA2HS Term #-}
-
-termEq : Term → Term → Bool
-termEq (Checkable (Inferred x))  (Inferable y) = x == y
-termEq (Checkable x) (Checkable y) = x == y
-termEq (Inferable x) (Checkable (Inferred y)) = x == y
-termEq (Inferable x) (Inferable y) = x == y
-termEq _ _ = false
-{-# COMPILE AGDA2HS termEq #-}
-
-instance 
-  TermEq : Eq Term 
-  TermEq ._==_ = termEq
-
-{-# COMPILE AGDA2HS TermEq #-}   
-
--------------------------------------------------------------------------------
-- Other Instances
--------------------------------------------------------------------------------
--- a/lab/Core.hs
+++ b/lab/Core.hs
@ -1,200 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-missing-export-lists #-}
-{-# OPTIONS_GHC -fno-warn-unused-imports #-}
-{-# OPTIONS_GHC -fno-warn-unused-matches #-}
-
-module MiniJuvix.Syntax.Core where
-
--------------------------------------------------------------------------------
-
-- import Algebra.Graph.Label (Semiring (..))
-import MiniJuvix.Prelude hiding (Local)
-import Numeric.Natural (Natural)
-
--------------------------------------------------------------------------------
-- Quantity (a.k.a. Usage)
--------------------------------------------------------------------------------
-
-data Quantity
-  = Zero
-  | One
-  | Many
-
-instance Eq Quantity where
-  Zero == Zero = True
-  One == One = True
-  Many == Many = True
-  _ == _ = False
-
-compareQuantity :: Quantity -> Quantity -> Ordering
-compareQuantity Zero Zero = EQ
-compareQuantity Zero _ = LT
-compareQuantity _ Zero = GT
-compareQuantity One One = EQ
-compareQuantity One _ = LT
-compareQuantity _ One = GT
-compareQuantity Many Many = EQ
-
-instance Ord Quantity where
-  compare = compareQuantity
-  x < y = compareQuantity x y == LT
-  x > y = compareQuantity x y == GT
-  x <= y = compareQuantity x y /= GT
-  x >= y = compareQuantity x y /= LT
-  max x y = if compareQuantity x y == LT then y else x
-  min x y = if compareQuantity x y == GT then y else x
-
-instance Semigroup Quantity where
-  Zero <> _ = Zero
-  One <> m = m
-  Many <> Zero = Zero
-  Many <> One = Many
-  Many <> Many = Many
-
-instance Monoid Quantity where
-  mempty = Zero
-
-instance Semiring Quantity where
-  one = One
-  (<.>) Zero _ = Zero
-  (<.>) One m = m
-  (<.>) Many Zero = Zero
-  (<.>) Many One = Many
-  (<.>) Many Many = Many
-
-data Relevance
-  = Relevant
-  | Irrelevant
-
-deriving stock instance Eq Relevance
-
-deriving stock instance Ord Relevance
-
-relevancy :: Quantity -> Relevance
-relevancy Zero = Irrelevant
-relevancy _ = Relevant
-
-type Index = Natural
-
-type BindingName = String
-
-data Name
-  = Global String
-  | Local BindingName Index
-
-instance Eq Name where
-  Global x == Global y = x == y
-  Local x1 y1 == Local x2 y2 = x1 == x2 && y1 == y2
-  _ == _ = False
-
-data Variable
-  = Bound Index
-  | Free Name
-
-instance Eq Variable where
-  Bound x == Bound y = x == y
-  Free x == Free y = x == y
-  _ == _ = False
-
--------------------------------------------------------------------------------
-
--------------------------------------------------------------------------------
-- Type-checkable terms.
--------------------------------------------------------------------------------
-
-data CheckableTerm
-  = UniverseType
-  | PiType Quantity BindingName CheckableTerm CheckableTerm
-  | Lam BindingName CheckableTerm
-  | TensorType Quantity BindingName CheckableTerm CheckableTerm
-  | TensorIntro CheckableTerm CheckableTerm
-  | UnitType
-  | Unit
-  | SumType CheckableTerm CheckableTerm
-  | Inl CheckableTerm
-  | Inr CheckableTerm
-  | Inferred InferableTerm
-
-data InferableTerm
-  = Var Variable
-  | Ann CheckableTerm CheckableTerm
-  | App InferableTerm CheckableTerm
-  | TensorTypeElim
-      Quantity
-      BindingName
-      BindingName
-      BindingName
-      InferableTerm
-      CheckableTerm
-      CheckableTerm
-  | SumTypeElim
-      Quantity
-      BindingName
-      InferableTerm
-      BindingName
-      CheckableTerm
-      BindingName
-      CheckableTerm
-      CheckableTerm
-
--------------------------------------------------------------------------------
-- Type-inferable terms (a.k.a terms that synthesise)
--------------------------------------------------------------------------------
-
--------------------------------------------------------------------------------
-- Term Equality
--------------------------------------------------------------------------------
-
-checkEq :: CheckableTerm -> CheckableTerm -> Bool
-checkEq UniverseType UniverseType = True
-checkEq (PiType q₁ _ a₁ b₁) (PiType q₂ _ a₂ b₂) =
-  q₁ == q₂ && checkEq a₁ a₂ && checkEq b₁ b₂
-checkEq (TensorType q₁ _ a₁ b₁) (TensorType q₂ _ a₂ b₂) =
-  q₁ == q₂ && checkEq a₁ a₂ && checkEq b₁ b₂
-checkEq (TensorIntro x₁ y₁) (TensorIntro x₂ y₂) =
-  checkEq x₁ x₂ && checkEq y₁ y₂
-checkEq UnitType UnitType = True
-checkEq Unit Unit = True
-checkEq (SumType x₁ y₁) (SumType x₂ y₂) =
-  checkEq x₁ x₂ && checkEq y₁ y₂
-checkEq (Inl x) (Inl y) = checkEq x y
-checkEq (Inr x) (Inr y) = checkEq x y
-checkEq (Inferred x) (Inferred y) = inferEq x y
-checkEq _ _ = False
-
-inferEq :: InferableTerm -> InferableTerm -> Bool
-inferEq (Var x) (Var y) = x == y
-inferEq (Ann x₁ y₁) (Ann x₂ y₂) = checkEq x₁ x₂ && checkEq y₁ y₂
-inferEq (App x₁ y₁) (App x₂ y₂) = inferEq x₁ x₂ && checkEq y₁ y₂
-inferEq
-  (TensorTypeElim q₁ _ _ _ a₁ b₁ c₁)
-  (TensorTypeElim q₂ _ _ _ a₂ b₂ c₂) =
-    q₁ == q₂ && inferEq a₁ a₂ && checkEq b₁ b₂ && checkEq c₁ c₂
-inferEq
-  (SumTypeElim q₁ _ x₁ _ a₁ _ b₁ c₁)
-  (SumTypeElim q₂ _ x₂ _ a₂ _ b₂ c₂) =
-    q₁ == q₂
-      && inferEq x₁ x₂
-      && checkEq a₁ a₂
-      && checkEq b₁ b₂
-      && checkEq c₁ c₂
-inferEq _ _ = False
-
-instance Eq CheckableTerm where
-  (==) = checkEq
-
-instance Eq InferableTerm where
-  (==) = inferEq
-
-data Term
-  = Checkable CheckableTerm
-  | Inferable InferableTerm
-
-termEq :: Term -> Term -> Bool
-termEq (Checkable (Inferred x)) (Inferable y) = x == y
-termEq (Checkable x) (Checkable y) = x == y
-termEq (Inferable x) (Checkable (Inferred y)) = x == y
-termEq (Inferable x) (Inferable y) = x == y
-termEq _ _ = False
-
-instance Eq Term where
-  (==) = termEq
--- a/lab/Eval.agda
+++ b/lab/Eval.agda
@ -1,187 +0,0 @@
-module MiniJuvix.Syntax.Eval where
-
--------------------------------------------------------------------------------
-
-open import Haskell.Prelude
-open import Agda.Builtin.Equality
-
-open import MiniJuvix.Syntax.Core
-
--------------------------------------------------------------------------------
-- Haskell stuff
--------------------------------------------------------------------------------
-
-{-# FOREIGN AGDA2HS
-{-# OPTIONS_GHC -fno-warn-missing-export-lists -fno-warn-unused-matches #-}
-#-}
-
-{-# FOREIGN AGDA2HS
-import MiniJuvix.Syntax.Core
-import MiniJuvix.Prelude
-#-}
-
-{-# FOREIGN AGDA2HS
--------------------------------------------------------------------------------
-- Values and neutral terms
--------------------------------------------------------------------------------
-#-}
-
-{-
-  We are interested in a normal form for posibbly open terms. This
-  means that a term may have free variables. Therefore, we must
-  consider two kind of reduced terms: values and neutral terms. A term
-  that do not longer beta-reduce (i.e. that it contains an evaluation
-  answer) is called a value. A term is neutral whenever its futher
-  beta-reduction depends on a free variable. Terms in normal form are
-  then defined by mutual recursion with neutral terms.
-}
-
-{- Since Agda2HS does not support indexed data types, we have to
-  repeat ourselves with syntax for values and neutral terms based on
-  Core syntax. The following is ideally for formal verification, but
-  not doable.
-}
-
-{-
-data Value : Term → Set
-data Neutral : Term → Set
-
-data Value where
-  IsUniverse : Value (Checkable UniverseType)
-  IsNeutral : (t : Term) → Neutral t → Value t
-  IsUnit : Value (Checkable Unit)
-  IsUnitType : Value (Checkable UnitType)
-  ...
-
-data Neutral where
-  IsFree : (b : Name) → Neutral (Inferable (Free b))
-  ...
-}
-
-{-# NO_POSITIVITY_CHECK #-}
-data Value : Set
-data Neutral : Set
-
-data Value where
-  IsUniverse : Value
-  IsPiType : Quantity → BindingName → Value → (Value -> Value) -> Value
-  IsLam : BindingName → (Value -> Value) -> Value
-  IsTensorType : Quantity → BindingName → Value → (Value -> Value) -> Value
-  IsTensorIntro : Value → Value -> Value
-  IsUnitType : Value
-  IsUnit : Value
-  IsSumType : Value → Value -> Value
-  IsInl : Value -> Value
-  IsInr : Value -> Value
-  IsNeutral : Neutral -> Value
-
-{-# COMPILE AGDA2HS Value #-}
-
-data Neutral where
-  IsFree : Name → Neutral
-  IsApp : Neutral → Value → Neutral
-  IsTensorTypeElim :
-    Quantity → BindingName → BindingName → BindingName
-    → Neutral
-    → (Value -> Value -> Value)
-    → (Value -> Value)
-    → Neutral
-  NSumElim :
-    Quantity
-    → BindingName
-    → Neutral
-    → BindingName
-    → (Value -> Value)
-    → BindingName
-    → (Value -> Value)
-    → (Value -> Value)
-    → Neutral
-
-{-# COMPILE AGDA2HS Neutral #-}
-
-- We can have an embedding from values to terms as a sort of quoting.
-- Usages: we can check for value equality by defining term equality.
-
-valueToTerm : Value → Term
-valueToTerm v = Checkable Unit -- TODO
-{-# COMPILE AGDA2HS valueToTerm #-}
-
--------------------------------------------------------------------------------
-- Substitution of bound variables. Recall a bound variable is
-- constructed using Bound and a natural number. The following is one
-- special case of substitution. See a relevant discussion on
-- ekmett/bound-making-de-bruijn-succ-less. For QTT, see Def. 12 in
-- Conor's paper.
--------------------------------------------------------------------------------
-
-substCheckableTerm
-  : CheckableTerm    -- Term N
-  → Index            -- Bound variable x
-  -> InferableTerm   -- M
-  -> CheckableTerm   -- N[x := M]
-
-substInferableTerm
-  : InferableTerm    -- Term N
-  →  Index           -- bound variable x
-  -> InferableTerm   -- inferable term M
-  -> InferableTerm   -- N[x := M]
-
-substCheckableTerm UniverseType x m = UniverseType
-substCheckableTerm (PiType q y a b) x m
-  = PiType q y
-      (substCheckableTerm a x m)
-      (substCheckableTerm b (x + 1) m)
-substCheckableTerm (Lam y n) x m
-  = Lam y (substCheckableTerm n (x + 1) m)
-substCheckableTerm (TensorType q y s t) x m
-  = TensorType q y
-      (substCheckableTerm s x m)
-      (substCheckableTerm t (x + 1) m)
-substCheckableTerm (TensorIntro p1 p2) x m
-  = TensorIntro
-      (substCheckableTerm p1 x m)
-      (substCheckableTerm p2 x m)
-substCheckableTerm UnitType x m = UnitType
-substCheckableTerm Unit x m = Unit
-substCheckableTerm (SumType a b) x m
-  = SumType
-      (substCheckableTerm a x m)
-      (substCheckableTerm b x m)
-substCheckableTerm (Inl n) x m = Inl (substCheckableTerm n x m)
-substCheckableTerm (Inr n) x m = Inr (substCheckableTerm n x m)
-substCheckableTerm (Inferred n) x m
-  = Inferred (substInferableTerm n x m)
-{-# COMPILE AGDA2HS substCheckableTerm #-}
-
-- Variable substitution.
-substInferableTerm (Var (Bound y)) x m = if x == y then m else Var (Bound y)
-substInferableTerm (Var (Free y)) x m  = Var (Free y)
-- we subst. checkable parts.
-substInferableTerm (Ann y a) x m
-  = Ann (substCheckableTerm y x m)
-        (substCheckableTerm a x m)
-substInferableTerm (App f t) x m
-  = App (substInferableTerm f x m)
-        (substCheckableTerm t x m)
-substInferableTerm (TensorTypeElim q z u v n a b) x m
-  = TensorTypeElim q z u v
-      (substInferableTerm n x m)
-      (substCheckableTerm a (x + 2) m)
-      (substCheckableTerm b (x + 1) m)
-substInferableTerm (SumTypeElim q z esum u r1 v r2 ann) x m
-  = SumTypeElim q z
-    (substInferableTerm esum x m)
-    u (substCheckableTerm r1 (x + 1) m)
-    v (substCheckableTerm r2 (x + 1) m)
-    (substCheckableTerm ann (x + 1) m)
-{-# COMPILE AGDA2HS substInferableTerm #-}
-
-{-- Substitution, denoted by (N[x := M]) is defined by mutual
-  recursion and by induction on N, and replace all the ocurrences of
-  'x' by M in the term N. Recall that N is a term of type either
-  CheckableTerm or InferableTerm.
-}
-
-substTerm : Term → Nat → InferableTerm → Term
-substTerm (Checkable n) x m = Checkable (substCheckableTerm n x m)
-substTerm (Inferable n) x m = Inferable (substInferableTerm n x m)
--- a/lab/Eval.hs
+++ b/lab/Eval.hs
@ -1,106 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-missing-export-lists -fno-warn-unused-matches #-}
-
-module MiniJuvix.Syntax.Eval where
-
-import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Core
-
--------------------------------------------------------------------------------
-- Values and neutral terms
--------------------------------------------------------------------------------
-
-data Value
-  = IsUniverse
-  | IsPiType Quantity BindingName Value (Value -> Value)
-  | IsLam BindingName (Value -> Value)
-  | IsTensorType Quantity BindingName Value (Value -> Value)
-  | IsTensorIntro Value Value
-  | IsUnitType
-  | IsUnit
-  | IsSumType Value Value
-  | IsInl Value
-  | IsInr Value
-  | IsNeutral Neutral
-
-data Neutral
-  = IsFree Name
-  | IsApp Neutral Value
-  | IsTensorTypeElim
-      Quantity
-      BindingName
-      BindingName
-      BindingName
-      Neutral
-      (Value -> Value -> Value)
-      (Value -> Value)
-  | NSumElim
-      Quantity
-      BindingName
-      Neutral
-      BindingName
-      (Value -> Value)
-      BindingName
-      (Value -> Value)
-      (Value -> Value)
-
-valueToTerm :: Value -> Term
-valueToTerm v = Checkable Unit
-
-substCheckableTerm ::
-  CheckableTerm -> Index -> InferableTerm -> CheckableTerm
-substCheckableTerm UniverseType x m = UniverseType
-substCheckableTerm (PiType q y a b) x m =
-  PiType
-    q
-    y
-    (substCheckableTerm a x m)
-    (substCheckableTerm b (x + 1) m)
-substCheckableTerm (Lam y n) x m =
-  Lam y (substCheckableTerm n (x + 1) m)
-substCheckableTerm (TensorType q y s t) x m =
-  TensorType
-    q
-    y
-    (substCheckableTerm s x m)
-    (substCheckableTerm t (x + 1) m)
-substCheckableTerm (TensorIntro p1 p2) x m =
-  TensorIntro
-    (substCheckableTerm p1 x m)
-    (substCheckableTerm p2 x m)
-substCheckableTerm UnitType x m = UnitType
-substCheckableTerm Unit x m = Unit
-substCheckableTerm (SumType a b) x m =
-  SumType (substCheckableTerm a x m) (substCheckableTerm b x m)
-substCheckableTerm (Inl n) x m = Inl (substCheckableTerm n x m)
-substCheckableTerm (Inr n) x m = Inr (substCheckableTerm n x m)
-substCheckableTerm (Inferred n) x m =
-  Inferred (substInferableTerm n x m)
-
-substInferableTerm ::
-  InferableTerm -> Index -> InferableTerm -> InferableTerm
-substInferableTerm (Var (Bound y)) x m =
-  if x == y then m else Var (Bound y)
-substInferableTerm (Var (Free y)) x m = Var (Free y)
-substInferableTerm (Ann y a) x m =
-  Ann (substCheckableTerm y x m) (substCheckableTerm a x m)
-substInferableTerm (App f t) x m =
-  App (substInferableTerm f x m) (substCheckableTerm t x m)
-substInferableTerm (TensorTypeElim q z u v n a b) x m =
-  TensorTypeElim
-    q
-    z
-    u
-    v
-    (substInferableTerm n x m)
-    (substCheckableTerm a (x + 2) m)
-    (substCheckableTerm b (x + 1) m)
-substInferableTerm (SumTypeElim q z esum u r1 v r2 ann) x m =
-  SumTypeElim
-    q
-    z
-    (substInferableTerm esum x m)
-    u
-    (substCheckableTerm r1 (x + 1) m)
-    v
-    (substCheckableTerm r2 (x + 1) m)
-    (substCheckableTerm ann (x + 1) m)
--- a/lab/agda-proofs/minijuvix-proofs.agda-lib
+++ b/lab/agda-proofs/minijuvix-proofs.agda-lib
@ -1,4 +0,0 @@
-name: minijuvix-proofs
-depend: standard-library
-include: proofs
-flags:
--- a/lab/agda-proofs/proofs/Algebra/Structures/StarSemiring.agda
+++ b/lab/agda-proofs/proofs/Algebra/Structures/StarSemiring.agda
@ -1,16 +0,0 @@
-open import Relation.Binary using (Rel)
-
-module Algebra.Structures.StarSemiring
-  {a ℓ} {A : Set a}  -- The underlying set
-  (_≈_ : Rel A ℓ)    -- The underlying equality relation
-  where
-
-open import Base
-open import Algebra.Structures {A = A} _≡_
-
-
-record IsStarSemiring (_+_ _*_ : Op₂ A) (★ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
-  field
-    isSemiring : IsSemiring _+_ _*_ 0# 1#
-    ★-cond-1 : ∀ a → ★ a ≈ (1# + (a * ★ a))
-    ★-cond-2 : ∀ a → ★ a ≈ (1# + (★ a * a))
--- a/lab/agda-proofs/proofs/Base.agda
+++ b/lab/agda-proofs/proofs/Base.agda
@ -1,6 +0,0 @@
-module Base where
-
-open import Level using (Level; _⊔_) renaming (suc to lsuc; zero to lzero) public
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; trans; sym; cong) public
-open import Algebra.Core public
-open import Data.Product public
--- a/lab/agda-proofs/proofs/Termination/FunctionCall.agda
+++ b/lab/agda-proofs/proofs/Termination/FunctionCall.agda
@ -1,328 +0,0 @@
-module Termination.FunctionCall where
-
-open import Base
-open import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Data.Product.Properties
-open import Data.Product
-import Termination.SizeRelation as S
-open S using (S)
-import Termination.SizeRelation.Properties as S
-open import Data.Nat using (ℕ)
-open import Axiom.Extensionality.Propositional
-
-module Matrix where
-  open import Data.Fin using (Fin; zero; suc; inject₁; fromℕ; _≟_)
-  open import Data.Nat using (ℕ)
-  open import Data.Vec using (Vec; tabulate)
-  open import Function.Base using (case_of_)
-  open import Relation.Nullary
-
-  -- Square matrix
-  Matrix : (A : Set) → ℕ → Set
-  Matrix A n = Vec (Vec A n) n
-
-  diagonal : {A : Set} → (zero diag : A) → (n : ℕ) → Matrix A n
-  diagonal z diag n = tabulate (λ i → tabulate (λ j →
-    case i ≟ j of λ {(yes _) → diag; (no _) → z}))
-
-
-module Square (n : ℕ) where
-  open import Data.Fin using (Fin; zero; suc; inject₁; fromℕ)
-  open import Data.Vec
-  open Matrix
-
-  -- All calls are assumed to be of arity n
-  Call : Set
-  Call = Vec S n
-
-  -- All edges are assumed to have n calls
-  Edge : Set
-  Edge = Matrix S n
-
-  Call-⁇ : Call
-  Call-⁇ = replicate S.⁇
-
-  -- Call-∼ : Call
-  -- Call-∼ = replicate S.∼
-
-  ⁇ : Edge
-  ⁇ = replicate (replicate S.⁇)
-
-  ∼ : Edge
-  ∼ = diagonal S.⁇ S.∼ n
-
-  infixl 6 _+_
-  infixl 7 _*_
-
-  sumRow : Call → S
-  sumRow = foldr _ S._+_ S.⁇
-
-  _*_ : Op₂ Edge
-  _*_ a b = tabulate (λ i → tabulate (λ j → sumRow (zipWith S._*_ (lookup a i) (lookup (transpose b) j))))
-
-  -- pointwise
-  _+_ : Op₂ Edge
-  (a + b) = tabulate (λ i → tabulate (λ j → lookup (lookup a i) j S.+ lookup (lookup b i) j))
-
-  -- ★ : Op₁ Edge
-  -- ★ a = tabulate (λ i → tabulate (λ j → S.★ (lookup (lookup a i) j)))
-
-
-module 2by2 where
-  open Square 2
-  open import Data.Vec
-  open S.★1 renaming (★ to S★)
-
-  ★ : Op₁ Edge
-  ★ ((b ∷ c ∷ []) ∷ (d ∷ e ∷ []) ∷ []) =
-    let ★b = S★ b
-        Δ = e S.+ (d S.* ★b S.* c)
-        ★Δ = S★ Δ
-
-        b' = ★b S.+ ★b S.* c S.* ★Δ S.* d S.* ★b
-        b'' = S★ (b S.+ c S.* S★ e S.* d)
-        c' = ★b S.* c S.* ★Δ
-        d' = ★Δ S.* d S.* ★b
-        e' = ★Δ
-    in ((b'' ∷ c' ∷ []) ∷
-        (d' ∷ e' ∷ [])
-        ∷ [])
-
-  -- TODO See definition of Call matrix!
-  ★-condition-1 : (a : Edge) → ★ a ≡ ∼ + a * ★ a
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.⁇ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.≺ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.⁇ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.≺ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.⁇ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.≺ ∷ S.∼ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.⁇ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.≺ ∷ []) ∷ []) = refl
-  ★-condition-1 ((S.∼ ∷ S.∼ ∷ []) ∷ (S.∼ ∷ S.∼ ∷ []) ∷ []) = refl
-
-
-
-- Simplified version
-module SingleCall where
-  open S.★1 renaming (★ to S★)
-
-  -- All calls have exactly 2 arguments
-  Call₂ : Set
-  Call₂ = S × S
-
-  -- An edge is a single function call
-  Edge₁ : Set
-  Edge₁ = Call₂
-
-  ⁇ : Edge₁
-  ⁇ = S.⁇ , S.⁇
-
-  ∼ : Edge₁
-  ∼ = S.∼ , S.∼
-
-  infixl 6 _+_
-  infixl 7 _*_
-
-  _*_ : Op₂ Edge₁
-  _*_ (a , b) (a' , b') = a S.* a' , b S.* b'
-
-  _+_ : Op₂ Edge₁
-  (a , b) + (a' , b') = a S.+ a' , b S.+ b'
-
-  open import Algebra.Structures {A = Call₂} _≡_
-  open import Algebra.Definitions {A = Call₂} _≡_
-  open import Algebra.Structures.StarSemiring {A = Call₂} _≡_
-
-  ×-≡,≡→≡ : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → {p₁@(a₁ , b₁) p₂@(a₂ , b₂) : A × B} → (a₁ ≡ a₂ × b₁ ≡ b₂) → p₁ ≡ p₂
-  ×-≡,≡→≡ (refl , refl) = refl
-
-  +-Commutative : Commutative _+_
-  +-Commutative a b = ×-≡,≡→≡
-    (S.+-Commutative (proj₁ a) (proj₁ b)
-    , S.+-Commutative (proj₂ a) (proj₂ b))
-
-  +-Associative : Associative _+_
-  +-Associative a b c = ×-≡,≡→≡
-     (S.+-Associative (proj₁ a) _ _
-     , S.+-Associative (proj₂ a) _ _)
-
-  +-IsMagma : IsMagma _+_
-  +-IsMagma = record
-    { isEquivalence = ≡.isEquivalence ;
-    ∙-cong = λ { refl refl → refl }}
-
-  +-IsSemigroup : IsSemigroup _+_
-  +-IsSemigroup = record { isMagma = +-IsMagma ; assoc = +-Associative }
-
-  +-Identityˡ : LeftIdentity ⁇ _+_
-  +-Identityˡ _ = refl
-
-  +-Identityʳ : RightIdentity ⁇ _+_
-  +-Identityʳ (fst , snd) = ×-≡,≡→≡ (S.+-Identityʳ _ , S.+-Identityʳ _)
-
-  +-Identity : Identity ⁇ _+_
-  +-Identity = +-Identityˡ , +-Identityʳ
-
-  +-IsMonoid : IsMonoid _+_ ⁇
-  +-IsMonoid = record { isSemigroup = +-IsSemigroup ; identity = +-Identity }
-
-  +-IsCommutativeMonoid : IsCommutativeMonoid _+_ ⁇
-  +-IsCommutativeMonoid = record
-    { isMonoid = +-IsMonoid ;
-    comm = +-Commutative }
-
-  -- Proofs on _*_
-
-  *-Associative : Associative _*_
-  *-Associative a b c = ×-≡,≡→≡
-     (S.*-Associative (proj₁ a) _ _
-     , S.*-Associative (proj₂ a) _ _)
-
-  *-Identityˡ : LeftIdentity ∼ _*_
-  *-Identityˡ _ = refl
-
-  *-Identityʳ : RightIdentity ∼ _*_
-  *-Identityʳ (fst , snd) = ×-≡,≡→≡ (S.*-Identityʳ _ , S.*-Identityʳ _)
-
-  *-Identity : Identity ∼ _*_
-  *-Identity = *-Identityˡ , *-Identityʳ
-
-  -- Proofs on + and *
-
-  *-DistributesOverˡ-+ : _*_ DistributesOverˡ _+_
-  *-DistributesOverˡ-+ a b c = ×-≡,≡→≡
-   (S.*-DistributesOverˡ-+ (proj₁ a) _ _
-   , S.*-DistributesOverˡ-+ (proj₂ a) _ _)
-
-  *-DistributesOverʳ-+ : _*_ DistributesOverʳ _+_
-  *-DistributesOverʳ-+ a b c = ×-≡,≡→≡
-   (S.*-DistributesOverʳ-+ (proj₁ a) (proj₁ b) _
-   , S.*-DistributesOverʳ-+ (proj₂ a) (proj₂ b) _)
-
-  *-DistributesOver-+ : _*_ DistributesOver _+_
-  *-DistributesOver-+ = *-DistributesOverˡ-+ , *-DistributesOverʳ-+
-
-  *-IsMagma : IsMagma _*_
-  *-IsMagma = record
-   { isEquivalence = ≡.isEquivalence
-    ; ∙-cong = λ {refl refl → refl }}
-
-  *-IsSemigroup : IsSemigroup _*_
-  *-IsSemigroup = record { isMagma = *-IsMagma ; assoc = *-Associative }
-
-  *-IsMonoid : IsMonoid _*_ ∼
-  *-IsMonoid = record { isSemigroup = *-IsSemigroup ; identity = *-Identity }
-
-  +-*-IsSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _+_ _*_ ⁇ ∼
-  +-*-IsSemiringWithoutAnnihilatingZero = record
-    { +-isCommutativeMonoid = +-IsCommutativeMonoid
-    ; *-isMonoid = *-IsMonoid
-    ; distrib = *-DistributesOver-+
-    }
-
-  *-LeftZero : LeftZero ⁇ _*_
-  *-LeftZero _ = refl
-
-  *-RightZero : RightZero ⁇ _*_
-  *-RightZero x = ×-≡,≡→≡
-    (S.*-RightZero (proj₁ x)
-    , S.*-RightZero (proj₂ x))
-
-  *-Zero : Zero ⁇ _*_
-  *-Zero = *-LeftZero , *-RightZero
-
-  +-*-IsSemiring : IsSemiring _+_ _*_ ⁇ ∼
-  +-*-IsSemiring = record
-    { isSemiringWithoutAnnihilatingZero = +-*-IsSemiringWithoutAnnihilatingZero
-    ; zero = *-Zero }
-
-  ★ : Op₁ Edge₁
-  ★ (a , b) = S★ a , S★ b
-
-  ★-condition-1 : (a : Edge₁) → ★ a ≡ ∼ + a * ★ a
-  ★-condition-1 a = ×-≡,≡→≡
-    (S.★-condition-1 (proj₁ a)
-    , S.★-condition-1 (proj₂ a))
-
-  ★-condition-2 : (a : Edge₁) → ★ a ≡ ∼ + ★ a * a
-  ★-condition-2 a = ×-≡,≡→≡
-    (S.★-condition-2 (proj₁ a)
-    , S.★-condition-2 (proj₂ a))
-
-  +-*-★-IsStarSemiring : IsStarSemiring _+_ _*_ ★ ⁇ ∼
-  +-*-★-IsStarSemiring = record
-    { isSemiring = +-*-IsSemiring
-    ; ★-cond-1 = ★-condition-1
-    ; ★-cond-2 = ★-condition-2 }
--- a/lab/agda-proofs/proofs/Termination/SizeRelation.agda
+++ b/lab/agda-proofs/proofs/Termination/SizeRelation.agda
@ -1,60 +0,0 @@
-module Termination.SizeRelation where
-
-open import Base
-open import Relation.Binary.PropositionalEquality.Properties as ≡
-
-data S : Set where
-  ⁇ : S
-  ≺ : S
-  ∼ : S
-
-infixl 6 _+_
-infixl 7 _*_
-
-_*_ : Op₂ S
-⁇ * _ = ⁇
-∼ * a = a
-≺ * ⁇ = ⁇
-≺ * ∼ = ≺
-≺ * ≺ = ≺
-
-_+_ : Op₂ S
-≺ + _ = ≺
-∼ + ≺ = ≺
-∼ + ∼ = ∼
-∼ + ⁇ = ∼
-⁇ + b = b
-
-module ★1 where
-  ★ : Op₁ S
-  ★ ⁇ = ∼
-  ★ ≺ = ≺
-  ★ ∼ = ∼
-
-  private
-    ★-condition-1 : (a : S) → ★ a ≡ ∼ + a * ★ a
-    ★-condition-1 ⁇ = refl
-    ★-condition-1 ≺ = refl
-    ★-condition-1 ∼ = refl
-
-    ★-condition-2 : (a : S) → ★ a ≡ ∼ + ★ a * a
-    ★-condition-2 ⁇ = refl
-    ★-condition-2 ≺ = refl
-    ★-condition-2 ∼ = refl
-
-module ★2 where
-  ★ : Op₁ S
-  ★ ⁇ = ∼
-  ★ ≺ = ≺
-  ★ ∼ = ≺
-
-  private
-    ★-condition-1 : (a : S) → ★ a ≡ ∼ + a * ★ a
-    ★-condition-1 ⁇ = refl
-    ★-condition-1 ≺ = refl
-    ★-condition-1 ∼ = refl
-
-    ★-condition-2 : (a : S) → ★ a ≡ ∼ + ★ a * a
-    ★-condition-2 ⁇ = refl
-    ★-condition-2 ≺ = refl
-    ★-condition-2 ∼ = refl
--- a/lab/agda-proofs/proofs/Termination/SizeRelation/Properties.agda
+++ b/lab/agda-proofs/proofs/Termination/SizeRelation/Properties.agda
@ -1,185 +0,0 @@
-module Termination.SizeRelation.Properties where
-
-open import Base
-open import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Termination.SizeRelation
-
-open import Algebra.Structures {A = S} _≡_
-open import Algebra.Definitions {A = S} _≡_
-open import Algebra.Structures.StarSemiring {A = S} _≡_
-
-- Proofs on _+_
-
-+-Commutative : Commutative _+_
-+-Commutative ⁇ ⁇ = refl
-+-Commutative ⁇ ≺ = refl
-+-Commutative ⁇ ∼ = refl
-+-Commutative ≺ ⁇ = refl
-+-Commutative ≺ ≺ = refl
-+-Commutative ≺ ∼ = refl
-+-Commutative ∼ ⁇ = refl
-+-Commutative ∼ ≺ = refl
-+-Commutative ∼ ∼ = refl
-
-+-Associative : Associative _+_
-+-Associative ⁇ _ _ = refl
-+-Associative ≺ _ _ = refl
-+-Associative ∼ ⁇ _ = refl
-+-Associative ∼ ≺ _ = refl
-+-Associative ∼ ∼ ⁇ = refl
-+-Associative ∼ ∼ ≺ = refl
-+-Associative ∼ ∼ ∼ = refl
-
-+-IsMagma : IsMagma _+_
-+-IsMagma = record
-  { isEquivalence = ≡.isEquivalence ;
-  ∙-cong = λ { refl refl → refl }}
-
-+-IsSemigroup : IsSemigroup _+_
-+-IsSemigroup = record { isMagma = +-IsMagma ; assoc = +-Associative }
-
-+-Identityˡ : LeftIdentity ⁇ _+_
-+-Identityˡ _ = refl
-
-+-Identityʳ : RightIdentity ⁇ _+_
-+-Identityʳ ⁇ = refl
-+-Identityʳ ≺ = refl
-+-Identityʳ ∼ = refl
-
-+-Identity : Identity ⁇ _+_
-+-Identity = +-Identityˡ , +-Identityʳ
-
-+-IsMonoid : IsMonoid _+_ ⁇
-+-IsMonoid = record { isSemigroup = +-IsSemigroup ; identity = +-Identity }
-
-+-IsCommutativeMonoid : IsCommutativeMonoid _+_ ⁇
-+-IsCommutativeMonoid = record
-  { isMonoid = +-IsMonoid ;
-   comm = +-Commutative }
-
-- Proofs on _*_
-
-*-Associative : Associative _*_
-*-Associative ⁇ _ _ = refl
-*-Associative ≺ ⁇ _ = refl
-*-Associative ≺ ≺ ⁇ = refl
-*-Associative ≺ ≺ ≺ = refl
-*-Associative ≺ ≺ ∼ = refl
-*-Associative ≺ ∼ _ = refl
-*-Associative ∼ _ _ = refl
-
-*-Commutative : Commutative _*_
-*-Commutative ⁇ ⁇ = refl
-*-Commutative ⁇ ≺ = refl
-*-Commutative ⁇ ∼ = refl
-*-Commutative ≺ ⁇ = refl
-*-Commutative ≺ ≺ = refl
-*-Commutative ≺ ∼ = refl
-*-Commutative ∼ ⁇ = refl
-*-Commutative ∼ ≺ = refl
-*-Commutative ∼ ∼ = refl
-
-*-Identityˡ : LeftIdentity ∼ _*_
-*-Identityˡ _ = refl
-
-*-Identityʳ : RightIdentity ∼ _*_
-*-Identityʳ ⁇ = refl
-*-Identityʳ ≺ = refl
-*-Identityʳ ∼ = refl
-
-*-Identity : Identity ∼ _*_
-*-Identity = *-Identityˡ , *-Identityʳ
-
-- Proofs on + and *
-
-*-DistributesOverˡ-+ : _*_ DistributesOverˡ _+_
-*-DistributesOverˡ-+ ⁇ _ _ = refl
-*-DistributesOverˡ-+ ≺ ⁇ _ = refl
-*-DistributesOverˡ-+ ≺ ≺ _ = refl
-*-DistributesOverˡ-+ ≺ ∼ ⁇ = refl
-*-DistributesOverˡ-+ ≺ ∼ ≺ = refl
-*-DistributesOverˡ-+ ≺ ∼ ∼ = refl
-*-DistributesOverˡ-+ ∼ _ _ = refl
-
-*-DistributesOverʳ-+ : _*_ DistributesOverʳ _+_
-*-DistributesOverʳ-+ ⁇ ⁇ _ = refl
-*-DistributesOverʳ-+ ⁇ ≺ ⁇ = refl
-*-DistributesOverʳ-+ ⁇ ≺ ≺ = refl
-*-DistributesOverʳ-+ ⁇ ≺ ∼ = refl
-*-DistributesOverʳ-+ ⁇ ∼ ⁇ = refl
-*-DistributesOverʳ-+ ⁇ ∼ ≺ = refl
-*-DistributesOverʳ-+ ⁇ ∼ ∼ = refl
-*-DistributesOverʳ-+ ≺ ⁇ _ = refl
-*-DistributesOverʳ-+ ≺ ≺ _ = refl
-*-DistributesOverʳ-+ ≺ ∼ ⁇ = refl
-*-DistributesOverʳ-+ ≺ ∼ ≺ = refl
-*-DistributesOverʳ-+ ≺ ∼ ∼ = refl
-*-DistributesOverʳ-+ ∼ ⁇ _ = refl
-*-DistributesOverʳ-+ ∼ ≺ _ = refl
-*-DistributesOverʳ-+ ∼ ∼ ⁇ = refl
-*-DistributesOverʳ-+ ∼ ∼ ≺ = refl
-*-DistributesOverʳ-+ ∼ ∼ ∼ = refl
-
-*-DistributesOver-+ : _*_ DistributesOver _+_
-*-DistributesOver-+ = *-DistributesOverˡ-+ , *-DistributesOverʳ-+
-
-*-IsMagma : IsMagma _*_
-*-IsMagma = record
-  { isEquivalence = ≡.isEquivalence
-   ; ∙-cong = λ {refl refl → refl }}
-
-*-IsSemigroup : IsSemigroup _*_
-*-IsSemigroup = record { isMagma = *-IsMagma
-  ; assoc = *-Associative }
-
-*-IsMonoid : IsMonoid _*_ ∼
-*-IsMonoid = record
-   { isSemigroup = *-IsSemigroup
-   ; identity = *-Identity }
-
-+-*-IsSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _+_ _*_ ⁇ ∼
-+-*-IsSemiringWithoutAnnihilatingZero = record
-  { +-isCommutativeMonoid = +-IsCommutativeMonoid
-  ; *-isMonoid = *-IsMonoid
-  ; distrib = *-DistributesOver-+
-  }
-
-*-LeftZero : LeftZero ⁇ _*_
-*-LeftZero _ = refl
-
-*-RightZero : RightZero ⁇ _*_
-*-RightZero ⁇ = refl
-*-RightZero ≺ = refl
-*-RightZero ∼ = refl
-
-*-Zero : Zero ⁇ _*_
-*-Zero = *-LeftZero , *-RightZero
-
-+-*-IsSemiring : IsSemiring _+_ _*_ ⁇ ∼
-+-*-IsSemiring = record
-  { isSemiringWithoutAnnihilatingZero = +-*-IsSemiringWithoutAnnihilatingZero
-  ; zero = *-Zero }
-
-+-*-IsCommutativeSemiring : IsCommutativeSemiring _+_ _*_ ⁇ ∼
-+-*-IsCommutativeSemiring =
-  record { isSemiring = +-*-IsSemiring
-  ; *-comm = *-Commutative }
-
-- Proofs on ★
-open ★1
-
-★-condition-1 : (a : S) → ★ a ≡ ∼ + a * ★ a
-★-condition-1 ⁇ = refl
-★-condition-1 ≺ = refl
-★-condition-1 ∼ = refl
-
-★-condition-2 : (a : S) → ★ a ≡ ∼ + ★ a * a
-★-condition-2 ⁇ = refl
-★-condition-2 ≺ = refl
-★-condition-2 ∼ = refl
-
-+-*-★-IsStarSemiring : IsStarSemiring _+_ _*_ ★ ⁇ ∼
-+-*-★-IsStarSemiring = record
-   { isSemiring = +-*-IsSemiring
-   ; ★-cond-1 = ★-condition-1
-   ; ★-cond-2 = ★-condition-2 }
--- a/lab/examples/Example1.mjuvix
+++ b/lab/examples/Example1.mjuvix
@ -1,223 +0,0 @@
-- Comments as in Haskell.
--This is another comment
------ This is another comment
-- This is another comment --possible text-- 
-  -- This is a comment, as it is not indent
-  -- sensitive. It should be fine.
-
-- reserved symbols (with their Unicode counterpart):
-- , ; : { } -> |-> := === @ _ \
-- reserved words:
-- module close open axiom inductive record options
-- where let in
-
-- Options to check/run this file.
-options { 
-debug   := INFO;
-phase   := { parsing , check };
-backend := none; -- llvm.
-};
-
-module Example1;
-
-module M;
-- This creates a module called M,
-- which it must be closed with:
-end M;
-
-open M;  -- comments can follow after ;
-close M;
-
-- import moduleName {names} hiding {names};
-import Primitives;       -- imports all the public names.
-import Backend {LLVM};   -- imports to local scope a var. called LLVM.
-import Prelude hiding {Nat, Vec, Empty, Unit};
-	-- same as before, but without the names inside `hiding`
-
-- Judgement decl. 
-- `x : M;`
-
-- Nonindexed inductive type declaration:
-inductive Nat
-{ zero : Nat ;
-	suc : Nat -> Nat ;
-};
-
-- Term definition uses := instead of =.
-- = is not a reserved name.
-- == is not a reserved name.
-- === is a reserved symbol for def. equality.
-zero' : Nat;
-zero'                 
-:= zero; 
-
-- Axioms/definitions.
-axiom A : Type;
-axiom a a' : A; 
-
-f : Nat -> A;
-f := \x -> match x
-{
-	zero |-> a  ;
-	suc  |-> a' ;
-}; 
-
-g : Nat -> A;
-g Nat.zero    := a;
-g (Nat.suc t) := a';
-
-- Qualified names for pattern-matching seems convenient.
-- For example, if we define a function without a type sig.
-- that also matches on inductive type with constructor names
-- appearing in another type, e.g. Nat and Fin.
-
-inductive Fin (n : Nat) {
-	zero : Fin Nat.zero;
-	suc  : (n : Nat) -> Fin (Nat.suc n);
-};
-
-infixl 10 _+_ ; -- fixity notation as in Agda or Haskell.
-_+_ : Nat → Nat → Nat ;
-_+_ Nat.zero m    := m;
-_+_ (Nat.suc n) m := Nat.suc (n + m) ;
-
-- Unicode is possible.
-ℕ : Type;
-ℕ := Nat;
-- Maybe consider alises for types and data constructors:
-- `alias ℕ := Nat` ;
-
-- The function `g` should be transformed to
-- a function of the form f. (aka. case-tree compilation)
-
-- Examples we must have to make things interesting:
-- Recall ; goes after any declarations.
-
-inductive Unit { tt : Unit;};
-
-- Indexed inductive type declarations:
-inductive Vec (n : Nat) (A : Type)
-{
-	zero : Vec Nat.zero A;
-	succ : A -> Vec n A -> Vec (Nat.succ n) A;
-};
-
-Vec' : Nat -> Type -> Type;
-Vec' Nat.zero A      := Unit;
-Vec' (Vec'.suc n) A := A -> Vec' n A;
-
-inductive Empty{};
-
-exfalso : (A : Type) -> Empty -> A;
-exfalso A e := match e {};
-
-neg : Type -> Type;
-neg := A -> Empty;
-
-- Record
-record Person {
-	name : String;
-	age: Nat;
-};
-
-h : Person -> Nat;
-h := \x -> match x {
-	{name = s , age = n} |-> n;
-};
-
-h' : Person -> Nat;
-h' {name = s , age = n} := n;
-
-- projecting fields values.
-h'' : Person -> String;
-h'' p := Person.name p;
-
-- maybe, harder to support but very convenient.
-h''' : Person -> String;
-h''' p := p.name;
-
-- So far, we haven't used quantites, here is some examples.
-- We mark a type judgment `x : M` of quantity n as `x :n M`. 
-- If the quantity n is not explicit, then the judgement
-- is `x :Any M`.
-
-- The following says that the term z of type A has quantity 0.
-axiom z :0 A;
-axiom B : (x :1 A) -> Type;   -- type family
-axiom T : [ A ] B;            -- Tensor product type. usages Any
-axiom T' : [ x :1 A ] B;      -- Tensor product type.
-axiom em : (x :1 A) -> B;  
-
-- Tensor product type.
-f' : [ x :1 A ] -> B;
-f' x := em x;
-
-- Pattern-matching on tensor pairs;
-
-g' : ([ A -> B ] A) -> B;  -- it should be the same as `[ A -> B ] A -> B` 
-g' (k , a) = k a; 			   
-
-g'' : ([ A -> B ] A) -> B;
-g'' = \p -> match p {
-	(k , a) |-> k a;
-};
-
-axiom C : Type;
-axiom D : Type;
-
-- A quantity can annotate a field name in a record type.
-record P (A : Type) (B : A -> Type) {
-	proj1 : C;
-	proj2 :0 D;
-} 
-eta-equality, constructor prop;  -- extra options.
-
-- More inductive types.
-inductive Id (A : Type) (x : A)
-{
-	refl : Id A x;
-};
-
-
-a-is-a : a = a;
-a-is-a := refl;
-
-- Where
-
-a-is-a' : a = a;
-a-is-a' := helper
-where helper := a-is-a;
-
-a-is-a'' : a = a;
-a-is-a'' := helper
-where {
-helper : a = a;
-helper := a-is-a';
-}
-
-- `Let` can appear in type level definition
-- but also in term definitions.
-
-a-is-a-3 : a = a;
-a-is-a-3 := let { helper : a = a; helper := a-is-a;} in helper;
-
-a-is-a-4 : let {
-typeId : (M : Type) -> (x : M) -> Type;
-typeId M x := x = x;
-} in typeId A a;
-a-is-a-4 := a-is-a;
-
-end Example1;
-
-- future:
-- module M' (X : Type);
-- x-is-x : (x : X) -> x = x;
-- x-is-x x := refl;
-- end M';
-- open M' A;
-- a-is-a-5 := a = a;
-- a-is-a-5 = x-is-x a;
-- Also, for debugging:
-
-- print e; print out the internal representation for e, without normalising it.
-- eval e;  compute e and print it out;
--- a/lab/examples/Example2.mjuvix
+++ b/lab/examples/Example2.mjuvix
@ -1,44 +0,0 @@
-- Based on example2.ju in anoma/juvix
-
-module Example2;
-
-import Prelude hiding {Bool, True, False};
-
-record Account {
-   balance : Nat;
-   name    : String;
-};
-
-record Transaction {
-  sender   : Account;
-  receiver : Account;
-};
-
-record Storage { trans : Transaction; };
-
-inductive TrustLevel {
-  Trusted    : Nat -> TrustLevel;
-  NotTrusted : TrustLevel
-};
-
-determine-trust-level : String -> TrustLevel;
-determine-trust-level s :=
-  if s === "bob"  then (Trusted 30)
-  else if s === "maria" then (Trusted 50)
-  else NotTrusted;
-
-inductive Bool {
-True : Bool;
-False : Bool;
-};
-
-accept-withdraws-from : Storage -> Storage -> Bool;
-accept-withdraws-from initial final := 
-  let { trusted? := determine-trust-level initial.trans.receiver.name; }
-  in match trusted? {
-     Trusted funds |-> 
-          funds.maximum-withdraw >=final.trans.sender.balance - initial.trans.sender.balance;
-     NotTrusted |-> False;
-  };
-
-end Example2;
--- a/lab/examples/Example3.mjuvix
+++ b/lab/examples/Example3.mjuvix
@ -1,32 +0,0 @@
-- Based on example3.ju in anoma/juvix
-
-module Example3;
-
-import Prelude;
-
-record Account {
-   balance : Nat;
-   name    : String;
-};
-
-record Transaction {
-  sender   : Account;
-  receiver : Account;
-};
-
-record Storage { trans : Transaction; };
-
-determine-maximum-withdraw : String -> Nat;
-determine-maximum-withdraw s := 
-  if s === "bob" then 30
-  else if s === "maria" then 50
-  else 0;
-
-accept-withdraws-from : Storage -> Storage -> Bool;
-accept-withdraws-from initial final :=
-  let { withdrawl-amount :=
-    determine-maximum-withdraw initial.trans.receiver.name;
-  } in 
-  withdrawl-amount >= final.trans.sender.balance - initial.trans.sender.balance;
-
-end Example3;
--- a/lab/examples/FirstMilestone.mjuvix
+++ b/lab/examples/FirstMilestone.mjuvix
@ -1,243 +0,0 @@
-module FirstMilestone;
-
--------------------------------------------------------------------------------
-- Module declaration
--------------------------------------------------------------------------------
-
-module M;  -- This creates a module called M.
-end;       -- This closes the current module in scope.
-
--------------------------------------------------------------------------------
-- Import definitions from existing modules
--------------------------------------------------------------------------------
-
-import Primitives;
-
-{- The line above will import to the local scope all the
-   public names qualified in the module called
-   Primitives.
-}
-
-open Primitives;
-
-{- The line above will import to the local scope all the
-   public names unqualified in the module called
-   Prelude.
-}
-
-import Backend;
-
-- Additionally, one can only import unqualified names by means of
-- the keyword "using".
-open Backend using { LLVM };  -- this imports to the local scope only the
-                              -- variable called LLVM.
-- One can use ---in combination with `using`--- the keyword `hiding`
-- to avoid importing undesirable names.
-
-import Prelude;
-open Prelude hiding { Nat ; Unit ; Empty } ;
-
--------------------------------------------------------------------------------
-- Inductive type declarations
--------------------------------------------------------------------------------
-
-- An inductive type named Empty without data constructors.
-inductive Empty {};
-
-- An inductive type named Unit with only one constructor.
-inductive Unit { tt : Unit; };
-
-inductive Nat' : Type
-{ zero : Nat' ;
-  suc : Nat' -> Nat' ;
-};
-
-- The use of the type `Type` below is optional.
-- The following declaration is equivalent to Nat'.
-
-inductive Nat {
-  zero : Nat ;
-  suc : Nat -> Nat ;
-};
-
-- A term definition uses the symbol (:=) instead of the traditional
-- symbol (=). The symbol (===) is reserved for def. equality. The
-- symbols (=) and (==) are not reserved.
-
-zero' : Nat;
-zero' := zero;
-
-
-- * Inductive type declarations with paramenters.
-
-- The n-point type.
-inductive Fin (n : Nat) {
-  zero : Fin zero;
-  suc  : (n : Nat) -> Fin (suc n);
-};
-
-- The type of sized vectors.
-inductive Vec (n : Nat) (A : Type)
-{
-  zero : Vec Nat.zero A;
-  succ : A -> Vec n A -> Vec (Nat.succ n) A;
-};
-
-- * Indexed inductive type declarations.
-
-- A very interesting data type.
-inductive Id (A : Type) (x : A) : A -> Type
-{
-  refl : Id A x x;
-};
-
--------------------------------------------------------------------------------
-- Unicode, whitespaces, newlines
--------------------------------------------------------------------------------
-
-- Unicode symbols are permitted.
-ℕ : Type;
-ℕ := Nat;
-
-- Whitespaces and newlines are optional. The following term
-- declaration is equivalent to the previous one.
-ℕ'
-  : Type;
-ℕ'
-:=
-  Nat;
-
-- Again, whitespaces are optional in declarations. For example,
-- `keyword nameID { content ; x := something; };` is equivalent to
-- `keyword nameID{content;x:=something;};`. However, we must strive
-- for readability and therefore, the former expression is better.
-
--------------------------------------------------------------------------------
-- Axioms/definitions
--------------------------------------------------------------------------------
-
-axiom A : Type;
-axiom a : A;
-axiom a' : A;
-
--------------------------------------------------------------------------------
-- Pattern-matching
--------------------------------------------------------------------------------
-
-f : Nat -> A;
-f := \x -> match x  -- \x  or λ x to denote a lambda abstraction.
-  {
-    zero ↦ a   ; -- case declaration uses the mapsto symbol or the normal arrow.
-    suc  -> a' ;
-  };
-
-- We can use qualified names to disambiguate names for
-- pattern-matching. For example, imagine the case where there are
-- distinct matches of the same constructor name for different
-- inductive types (e.g. zero in Nat and Fin), AND the function type
-- signature is missing.
-
-g : Nat -> A;
-g Nat.zero    := a;
-g (Nat.suc t) := a';
-
-- For pattern-matching, the symbol `_` is the wildcard pattern as in
-- Haskell or Agda. The following function definition is equivalent to
-- the former.
-
-g' : Nat -> A;
-g' zero := a;
-g' _    := a';
-
-- Note that the function `g` will be transformed to a function equal
-- to the function f above in the case-tree compilation phase.
-
-- The absurd case for patterns.
-
-exfalso : (A : Type) -> Empty -> A;
-exfalso A e := match e {};
-
-neg : Type -> Type;
-neg := A -> Empty;
-
-- An equivalent type for sized vectors.
-
-Vec' : Nat -> Type -> Type;
-Vec' Nat.zero A    := Unit;
-Vec' (Nat.suc n) A := A -> Vec' n A;
-
--------------------------------------------------------------------------------
-- Fixity notation similarly as in Agda or Haskell.
--------------------------------------------------------------------------------
-
-infixl 10 + ;
-+ : Nat → Nat → Nat ;
-+ Nat.zero m    := m;
-+ (Nat.suc n) m := Nat.suc (n + m) ;
-
--------------------------------------------------------------------------------
-- Quantities for variables.
--------------------------------------------------------------------------------
-
-- A quantity for a variable in MiniJuvix can be either 0,1, or Any.
-- If the quantity n is not explicit, then it is Any.
-
-- The type of functions that uses once its input of type A to produce a number.
-axiom funs : (x :1 A) -> Nat;
-
-axiom B : (x :1 A) -> Type;   -- B is a type family.
-axiom em : (x :1 A) -> B;
-
--------------------------------------------------------------------------------
-- Where
--------------------------------------------------------------------------------
-
-a-is-a : Id A a a;
-a-is-a := refl;
-
-a-is-a' : Id A a a;
-a-is-a' := helper
-  where {
-    open somemodule;
-    helper : Id A a a;
-    helper := a-is-a;
-    };
-
--------------------------------------------------------------------------------
-- Let
--------------------------------------------------------------------------------
-
-- `let` can appear in term and type level definitions.
-
-a-is-a'' : Id A a a;
-a-is-a'' := let { helper : Id A a a;
-                  helper := a-is-a; }
-            in helper;
-
-a-is-a''' : let { typeId : (M : Type) -> (x : M) -> Type;
-                  typeId M x := Id M x x;
-                } in typeId A a;
-a-is-a''' := a-is-a;
-
--------------------------------------------------------------------------------
-- Debugging
--------------------------------------------------------------------------------
-
-e : Nat;
-e : suc zero + suc zero;
-
-two : Nat;
-two := suc (suc zero);
-
-e-is-two : Id Nat e two;
-e-is-two := refl;
-
-- print out the internal representation for e without normalising it.
-print e;
-
-- compute e and print e.
-eval e;
-
--------------------------------------------------------------------------------
-
-end;
--- a/lab/examples/declarations/module/Makefile
+++ b/lab/examples/declarations/module/Makefile
@ -1,6 +0,0 @@
-
-all:
-	- make test
-
-test :
-	shelltest fail succeed -c --execdir -h --all
--- a/lab/examples/declarations/module/examples/A.mjuvix
+++ b/lab/examples/declarations/module/examples/A.mjuvix
@ -1,4 +0,0 @@
-module A;
-  module B;
-  end;
-end;
--- a/lab/examples/declarations/module/examples/AA.mjuvix
+++ b/lab/examples/declarations/module/examples/AA.mjuvix
@ -1,4 +0,0 @@
-module A;
-  module A;
-  end;
-end;
--- a/lab/examples/declarations/module/examples/E0.mjuvix
+++ b/lab/examples/declarations/module/examples/E0.mjuvix
--- a/lab/examples/declarations/module/examples/E1.mjuvix
+++ b/lab/examples/declarations/module/examples/E1.mjuvix
@ -1 +0,0 @@
-module Top;
--- a/lab/examples/declarations/module/examples/E2.mjuvix
+++ b/lab/examples/declarations/module/examples/E2.mjuvix
@ -1,8 +0,0 @@
-module Top;
-  module A;
-    module O; end;
-  end;
-  module B;
-    module O; end;
-  end;
-end;
--- a/lab/examples/declarations/module/examples/E3.mjuvix
+++ b/lab/examples/declarations/module/examples/E3.mjuvix
@ -1,4 +0,0 @@
-module Top;
-  module A; end;
-  module A; end;
-end;
--- a/lab/examples/declarations/module/examples/T.mjuvix
+++ b/lab/examples/declarations/module/examples/T.mjuvix
@ -1,6 +0,0 @@
-module Top;
-  module A;
-    module P; end;
-  end;
-  import A;
-end;
--- a/lab/examples/declarations/module/fail/E0.test
+++ b/lab/examples/declarations/module/fail/E0.test
@ -1,11 +0,0 @@
-# An empty file is not valid
-$ stack -- exec minijuvix parse ./../examples/E0.mjuvix
->2
-minijuvix: user error (./../examples/E0.mjuvix:1:1:
-  |
-1 | <empty line>
-  | ^
-unexpected end of input
-expecting "module"
-)
->= 1
--- a/lab/examples/declarations/module/fail/E1.test
+++ b/lab/examples/declarations/module/fail/E1.test
@ -1,23 +0,0 @@
-# Every module declaration ends with 'end;'
-$ stack -- exec minijuvix parse ./../examples/E1.mjuvix
->2
-minijuvix: user error (./../examples/E1.mjuvix:3:1:
-  |
-3 | <empty line>
-  | ^
-unexpected end of input
-expecting "axiom", "end", "eval", "import", "inductive", "infix", "infixl", "infixr", "module", "open", "postfix", "prefix", or "print"
-)
->= 1
-
-
-$ stack -- exec minijuvix scope ./../examples/E1.mjuvix
->2
-minijuvix: user error (./../examples/E1.mjuvix:3:1:
-  |
-3 | <empty line>
-  | ^
-unexpected end of input
-expecting "axiom", "end", "eval", "import", "inductive", "infix", "infixl", "infixr", "module", "open", "postfix", "prefix", or "print"
-)
->= 1
--- a/lab/examples/declarations/module/fail/E2.test
+++ b/lab/examples/declarations/module/fail/E2.test
@ -1,34 +0,0 @@
-<
-$ stack -- exec minijuvix parse ./../examples/E2.mjuvix
->
-Module
-  { modulePath =
-      TopModulePath
-        { modulePathDir = Path { pathParts = [] }
-        , modulePathName = Sym "Top"
-        }
-  , moduleBody =
-      [ StatementModule
-          Module
-            { modulePath = Sym "A"
-            , moduleBody =
-                [ StatementModule Module { modulePath = Sym "O" , moduleBody = [] }
-                ]
-            }
-      , StatementModule
-          Module
-            { modulePath = Sym "B"
-            , moduleBody =
-                [ StatementModule Module { modulePath = Sym "O" , moduleBody = [] }
-                ]
-            }
-      ]
-  }
->= 0
-
-
-<
-$ stack -- exec minijuvix scope ./../examples/E2.mjuvix
->2
-minijuvix: user error (ErrAlreadyDefined (Sym "O"))
->= 1
--- a/lab/examples/declarations/module/fail/E3.test
+++ b/lab/examples/declarations/module/fail/E3.test
@ -1,22 +0,0 @@
-<
-$ stack -- exec minijuvix parse ./../examples/E3.mjuvix
->
-Module
-  { modulePath =
-      TopModulePath
-        { modulePathDir = Path { pathParts = [] }
-        , modulePathName = Sym "Top"
-        }
-  , moduleBody =
-      [ StatementModule Module { modulePath = Sym "A" , moduleBody = [] }
-      , StatementModule Module { modulePath = Sym "A" , moduleBody = [] }
-      ]
-  }
->= 0
-
-
-<
-$ stack -- exec minijuvix scope ./../examples/E3.mjuvix
->2
-minijuvix: user error (ErrAlreadyDefined (Sym "A"))
->= 1
--- a/lab/examples/declarations/module/fail/T.test
+++ b/lab/examples/declarations/module/fail/T.test
@ -1,4 +0,0 @@
-$ stack -- exec minijuvix scope ./../examples/T.mjuvix
->2
-minijuvix: examples/T.mjuvix/A.mjuvix: openFile: inappropriate type (Not a directory)
->= 1
--- a/lab/examples/declarations/module/succeed/A.test
+++ b/lab/examples/declarations/module/succeed/A.test
@ -1,30 +0,0 @@
-$ cat ./../examples/A.mjuvix
->
-module A;
-  module B;
-  end;
-end;
->= 0
-
-$ stack -- exec minijuvix parse ./../examples/A.mjuvix
->
-Module
-  { modulePath =
-      TopModulePath
-        { modulePathDir = Path { pathParts = [] }
-        , modulePathName = Sym "A"
-        }
-  , moduleBody =
-      [ StatementModule Module { modulePath = Sym "B" , moduleBody = [] }
-      ]
-  }
->= 0
-
-
-$ stack -- exec minijuvix scope ./../examples/A.mjuvix -- --show-name-ids
->
-module A;
-  module B@0;
-  end;
-end;
->= 0
--- a/lab/examples/declarations/module/succeed/T.test
+++ b/lab/examples/declarations/module/succeed/T.test
@ -1,27 +0,0 @@
-$ stack -- exec minijuvix parse ./../examples/T.mjuvix
->
-Module
-  { modulePath =
-      TopModulePath
-        { modulePathDir = Path { pathParts = [] }
-        , modulePathName = Sym "Top"
-        }
-  , moduleBody =
-      [ StatementModule
-          Module
-            { modulePath = Sym "A"
-            , moduleBody =
-                [ StatementModule Module { modulePath = Sym "P" , moduleBody = [] }
-                ]
-            }
-      , StatementImport
-          Import
-            { importModule =
-                TopModulePath
-                  { modulePathDir = Path { pathParts = [] }
-                  , modulePathName = Sym "A"
-                  }
-            }
-      ]
-  }
->= 0
--- a/lab/examples/syntax.miniju
+++ b/lab/examples/syntax.miniju
@ -1,51 +0,0 @@
-- The syntax is very similar to that of Agda. However, we need some extra ';'
-module Example where
-
-   -- The natural numbers can be inductively defined thus:
-   data ℕ : Type 0 ;
-      | zero : ℕ
-      | suc : ℕ → ℕ ;
-
-   -- A list of elements with typed size:
-   data Vec (A : Type) : ℕ → Type 0 ;
-     | nil : A → Vec A zero
-     | cons : (n : ℕ) → A → Vec A n → Vec A (suc n) ;
-
-   module ℕ-Ops where
-     infixl 6 + ;
-     + : ℕ → ℕ → ℕ ;
-     + zero b = b ;
-     + (suc a) b = suc (a + b) ;
-
-     infixl 7 * ;
-     * : ℕ → ℕ → ℕ ;
-     * zero b = zero ;
-     * (suc a) b = b + a * b ;
-   end
-
-   module M1 (A : Type 0) where
-      aVec : ℕ → Type 0 ;
-      aVec = Vec A ;
-   end
-
-   module Bot where
-      data ⊥ : Type 0 ;
-   end
-
-   open module M1 ℕ ;
-
-   two : ℕ ;
-   two = suc (suc zero) ;
-
-   id : (A : Type) → A → A ;
-   id _ = λ x → x ;
-
-   natVec : aVec (cons zero) ;
-   natVec = cons (two * two + one) nil ;
-     -- The 'where' part belongs to the clause
-     where
-     open module ℕ-Ops ;
-     one : ℕ ;
-     one = suc zero ;
-
-end
--- a/lab/examples/token.mjuvix
+++ b/lab/examples/token.mjuvix
@ -1,417 +0,0 @@
-module Token;
-
-import Data.Nat;
-open Data.Nat using {<=};
-
-import Data.String;
-open Data.String using {compare};
-
--------------------------------------------------------------------------------
-- Boiler plate taken from previous code
--------------------------------------------------------------------------------
-
-{-
-total_order : (a:eqtype) (f: (a -> a -> Tot Bool)) =
-   (forall a1 a2. (f a1 a2 /\ f a2 a1)  ==> a1 = a2)  (* anti-symmetry *)
- /\ (forall a1 a2 a3. f a1 a2 /\ f a2 a3 ==> f a1 a3)  (* transitivity  *)
- /\ (forall a1 a2. f a1 a2 \/ f a2 a1)                (* totality      *)
-
-string_cmp' s1 s2 =  String.compare s1 s2 <= 0
-
-(* The F* defn just calls down to OCaml, since we know comparison in OCaml is total
- * just admit it
- *)
-
-string_cmpTotal : unit -> Lemma (total_order string string_cmp')
-string_cmpTotal () = admit ()
-
-// hack function so, the data structure doesn't forget the proof!
-string_cmp : Map.cmp string
-string_cmp = string_cmpTotal (); string_cmp'
-
-}
-
--------------------------------------------------------------------------------
-- Type definitions
--------------------------------------------------------------------------------
-
-Address : Type;
-Address := String;
-
-- Accounts : Map.ordmap Address Nat string_cmp
-
-inductive Account {
-  mkAccount : Nat -> SortedMap Address Nat -> Account;
-}
-
-balance : Account -> Nat;
-balance (mkAccount n _) := n;
-
-allowances : Account -> SortedMap Address Nat ;
-allowances (mkAccount _ s) := s;
-
-
-add_account_values_acc : Accounts → Nat -> Nat
-add_account_values_acc Accounts n  =
- MapProp.fold (fun _key (v : Nat) (acc : Nat) -> v + acc) Accounts n
-
-// we have to specify they are Nats :(
-add_account_values : Accounts -> Nat
-add_account_values Accounts =
- MapProp.fold (fun _key (v : Nat) (acc : Nat) -> v + acc) Accounts 0
-
-inductive Storage {
-  mkStorage : Nat -> Accounts
-  total-supply : Nat;
-  Accounts : a : Accounts { total-supply = add_account_values a };
-}
-
-empty-storage : storage
-empty-storage = {
-  total-supply = 0;
-  Accounts = Map.empty;
-}
-
-inductive Token {
-  mkToken :
-    Storage ->   -- storage
-    Nat ->       -- version
-    String ->    -- name
-    Char ->      -- symbol
-    Address ->   -- owner
-    Token
-}
-
-storage : Token -> Storage;
-storage (mkToken s _ _ _ _ _) := s;
-
-version : Token -> Nat;
-version (mkToken _ n _ _ _ _) := n;
-
-name    : Token -> String;
-name    (mkToken _ _ n _ _ _) := n;
-
-symbol  : Token -> Char;
-symbol  (mkToken _ _ _ s _ _) := s;
-
-owner   : Token -> Address;
-owner   (mkToken _ _ _ _ _ a) := a;
-
-
-type txTransfer = {
-  from_account    : Address;
-  to_account      : Address;
-  transfer_amount : Nat
-}
-
-type tx_mint = {
-  mint_amount     : Nat;
-  mintTo_account : Address
-}
-
-type tx_burn = {
-  burn_amount       : Nat;
-  burn_from_account : Address
-}
-
-inductive txData {
-  transfer : txTransfer -> txData;
-  mint     : txMint -> txData;
-  burn     : txBurn -> txData;
-  }
-
-type tx = {
-  tx_data               : tx_data;
-  tx_authroized_account : Address;
-}
-
--------------------------------------------------------------------------------
-- Begin Functions On Accounts
--------------------------------------------------------------------------------
-
-has_n : Accounts -> Address -> Nat -> Bool
-has_n accounts add toTransfer :=
-  match Map.select add Accounts {
-   (Some n) -> toTransfer <= n;
-   None     -> false;
-  }
-
-account-sub :
-  (acc : Accounts) ->
-  (add : Address) ->
-  (num : Nat {has_n acc add num}) ->
-  Accounts
-account-sub Accounts add number =
-  match Map.select add Accounts with
-   { Some balance -> Map.update add (balance - number) Accounts };
-
-
-// No feedback given, so don't know next move :(
-transfer-sub : 
-  (acc : Accounts) ->
-  (add : Address) ->
-  (num : Nat) ->
-  Lemma ->
-  (requires (has_n acc add num)) ->
-  (ensures (  add_account_values acc - num
-           == add_account_values (account-sub acc add num)))
-transfer-sub acc add num :=
-  match Map.select add acc {
-   Some balance ->;
-    remaining : Nat = balance - num in
-    admit ()
-  };
-
-account_add : acc : Accounts
-                -> add : Address
-                -> num : Nat
-                -> Accounts
-account_add acc add num =
-  match Map.select add acc with
-   Some b' -> Map.update add (b' + num) acc;
-   None    -> Map.update add num        acc;
-
--------------------------------------------------------------------------------
-(**** Experimental Proofs on Transfer *)
--------------------------------------------------------------------------------
-
-transfer_add_lemma : acc : Accounts
-                       -> add : Address
-                       -> num : Nat
-                       -> Lemma
-                       (ensures
-                         (i =
-                           match Map.select add acc with
-                            None   -> 0;
-                            Some v -> v;
-                          in i + num = Some?.v (Map.select add (account_add acc add num))))
-transfer_add_lemma acc add num = ()
-
-transfer_add_unaffect : acc : Accounts
-                          -> add : Address
-                          -> num : Nat
-                          -> Lemma
-                          (ensures
-                            (forall x. Map.contains x acc /\ x <> add
-                              ==> Map.select x acc = Map.select x (account_add acc add num)))
-transfer_add_unaffect acc add num = ()
-
-
-transfer-same_when_remove : acc : Accounts
-                              -> add : Address
-                              -> num : Nat
-                              -> Lemma
-                              (ensures
-                                (new_account = account_add acc add num in
-                                    add_account_values (Map.remove add acc)
-                                 == add_account_values (Map.remove add new_account)))
-transfer-same_when_remove acc add num =
-  new_account = account_add acc add num in
-  assert (Map.equal (Map.remove add acc) (Map.remove add new_account))
-
-// Useful stepping stone to the real answer!
-// sadly admitted for now
-transfer_acc_behavior : acc : Accounts
-                          -> add : Address
-                          -> Lemma
-                            (ensures
-                              (i =
-                                match Map.select add acc with
-                                 None   -> 0;
-                                 Some v -> v;
-                                in add_account_values_acc (Map.remove add acc) i
-                                  == add_account_values acc))
-transfer_acc_behavior acc add =
-  admit ()
-
-// No feedback given, so don't know next move :(
-transfer_add : acc : Accounts
-                 -> add : Address
-                 -> num : Nat
-                 -> Lemma
-                  (ensures ( add_account_values acc + num
-                           == add_account_values (account_add acc add num)))
-transfer_add acc add num =
-  admit ();
-  transfer-same_when_remove acc add num;
-  transfer_add_unaffect acc add num;
-  transfer_add_lemma acc add num
-
--------------------------------------------------------------------------------
-(**** Failed Experimental Proofs Over *)
--------------------------------------------------------------------------------
-
-
-transfer_acc : acc     : Accounts
-                -> add_from : Address
-                -> addTo   : Address
-                -> num      : Nat {has_n acc add_from num}
-                -> Accounts
-transfer_acc Accounts add_from addTo number =
-  new_Accounts = account-sub Accounts add_from number in
-  account_add new_Accounts addTo number
-
-transfer_maintains-supply
-  : acc      : Accounts
-  -> add_from : Address
-  -> addTo   : Address
-  -> num      : Nat
-  -> Lemma
-    (requires (has_n acc add_from num))
-    (ensures (add_account_values acc
-              == add_account_values (transfer_acc acc add_from addTo num)))
-transfer_maintains-supply acc add_from addTo num =
-  transfer-sub acc add_from num;
-  transfer_add (account-sub acc add_from num) addTo num
-
-transfer-stor
-  : stor     : storage
-  -> add_from : Address
-  -> addTo   : Address
-  -> num      : Nat {has_n stor.Accounts add_from num}
-  -> storage
-transfer-stor stor add_from addTo num =
-  new_acc = account_add (account-sub stor.Accounts add_from num) addTo num in
-  transfer_maintains-supply stor.Accounts add_from addTo num;
-  { total-supply = stor.total-supply;
-    Accounts     = new_acc
-  }
-
-
--------------------------------------------------------------------------------
-(* End Type Definitions *)
-(**** Begin Validations On Tokens *)
--------------------------------------------------------------------------------
-
-
-validTransfer : token -> tx -> Bool
-validTransfer token tx =
-  match tx.tx_data with
-   Transfer {from_account; transfer_amount} ->;
-    has_n token.storage.Accounts from_account transfer_amount
-    && tx.tx_authroized_account = from_account
-   Mint _  Burn _ ->;
-    false
-
-valid_mint : token -> tx -> Bool
-valid_mint token tx =
-  match tx.tx_data with
-   Mint mint           -> token.owner = tx.tx_authroized_account;
-   Transfer _  Burn _ -> false;
-
-valid_burn : token -> tx -> Bool
-valid_burn token tx =
-  match tx.tx_data with
-   Burn {burn_from_account; burn_amount} ->;
-    has_n token.storage.Accounts burn_from_account burn_amount
-    && tx.tx_authroized_account = burn_from_account
-   Transfer _  Mint _ ->;
-    false
-
-
--------------------------------------------------------------------------------
-(* End validations on tokens *)
-(**** Begin Functions On Tokens *)
--------------------------------------------------------------------------------
-
-tokenTransaction : (token -> tx -> Bool) -> Type0
-tokenTransaction f =
-  tok : token -> tx : tx { f tok tx } -> token
-
-transfer : tokenTransaction validTransfer
-transfer token transaction =
-  match transaction.tx_data with
-   Transfer {from_account; to_account; transfer_amount} ->;
-    { token
-      with storage = transfer-stor token.storage
-                                   from_account
-                                   to_account
-                                   transfer_amount
-    }
-
-mint : tokenTransaction valid_mint
-mint token transaction =
-  match transaction.tx_data with
-   Mint {mint_amount; mintTo_account} ->;
-    transfer_add token.storage.Accounts mintTo_account mint_amount;
-    { token
-      with storage = {
-        total-supply = token.storage.total-supply + mint_amount;
-        Accounts     = account_add token.storage.Accounts mintTo_account mint_amount
-      }}
-
-burn : tokenTransaction valid_burn
-burn token transaction =
-  match transaction.tx_data with
-   Burn {burn_from_account; burn_amount} ->;
-    transfer-sub token.storage.Accounts burn_from_account burn_amount;
-    { token
-      with storage = {
-        total-supply = token.storage.total-supply - burn_amount;
-        Accounts     = account-sub token.storage.Accounts burn_from_account burn_amount
-      }}
-
-type transaction_error =
-   Not_enough_funds;
-   Not-same_account;
-   Not_ownerToken;
-   Not_enoughTokens;
-
-executeTransaction : token -> tx -> c_or transaction_error token
-executeTransaction token tx =
-  match tx.tx_data with
-   Transfer _ ->;
-    if validTransfer token tx
-    then Right (transfer token tx)
-    else Left Not_enough_funds // todo determine what the error is
-   Mint _ ->;
-    if valid_mint token tx
-    then Right (mint token tx)
-    else Left Not_ownerToken
-   Burn _ ->;
-    if valid_burn token tx
-    then Right (burn token tx)
-    else Left Not_enoughTokens
-
-validTransferTransaction
-  : tok : token
-  -> tx  : tx
-  -> Lemma (requires (validTransfer tok tx))
-          (ensures (
-            Right newTok = executeTransaction tok tx in
-            tok.storage.total-supply == newTok.storage.total-supply))
-validTransferTransaction tok tx = ()
-
-
-valid_mintTransaction
-  : tok : token
-  -> tx  : tx
-  -> Lemma (requires (valid_mint tok tx))
-          (ensures (
-            Right newTok = executeTransaction tok tx in
-            Mint {mint_amount} = tx.tx_data in
-            tok.storage.total-supply + mint_amount == newTok.storage.total-supply))
-valid_mintTransaction tok tx = ()
-
-valid_burnTransaction
-  : tok : token
-  -> tx  : tx
-  -> Lemma (requires (valid_burn tok tx))
-          (ensures (
-            Right newTok = executeTransaction tok tx in
-            Burn {burn_amount} = tx.tx_data in
-            tok.storage.total-supply - burn_amount == newTok.storage.total-supply))
-valid_burnTransaction tok tx = ()
-
-isLeft = function
-   Left _  -> true;
-   Right _ -> false;
-
-non_validTransaction
-  : tok : token
-  -> tx  : tx
-  -> Lemma (requires (not (valid_burn tok tx)
-                   /\ not (valid_mint tok tx)
-                   /\ not (validTransfer tok tx)))
-          (ensures (isLeft (executeTransaction tok tx)))
-non_validTransaction tok tx = ()
--- a/lab/minijuvix.agda-lib
+++ b/lab/minijuvix.agda-lib
@ -1,3 +0,0 @@
-name: MiniJuvix
-include: src
-depend: agda2hs
--- a/lab/notes/Example.agda
+++ b/lab/notes/Example.agda
@ -1,100 +0,0 @@
-- testing
-module MiniJuvix.Syntax.Core where
-
-open import Haskell.Prelude
-open import Agda.Builtin.Equality
-
-- language extensions
-{-# FOREIGN AGDA2HS
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE FlexibleInstances #-}
-#-}
-
-{-# FOREIGN AGDA2HS
-{-
-M , N := x
-    | λ x . M
-    | M N
-    | ⊤
-    | ⊥
-    | if_then_else
-    | x : M
-where
-    variables x.
-    M := Bool | M -> M
-}
-#-}
-
-VarType : Set
-VarType = String
-
-------------------------------------------------------------------------------
-- Types
-------------------------------------------------------------------------------
-
-data Type : Set where
-  BoolType : Type
-  ArrowType : Type → Type → Type
-
-{-# COMPILE AGDA2HS Type deriving (Show, Eq) #-}
-
-------------------------------------------------------------------------------
-- Terms
-------------------------------------------------------------------------------
-
-data Term : Set where
-  Var : VarType → Term
-  TT : Term
-  FF : Term
-  Abs : VarType → Term → Term
-  App : Term → Term → Term
-  If : Term → Term → Term → Term
-  Jud : Term → Type → Term
-
-
-{-# COMPILE AGDA2HS Term deriving (Show, Eq) #-}
-
-------------------------------------------------------------------------------
-- Context
-------------------------------------------------------------------------------
-
-Context : Set
-Context = List (VarType × Type)
-
-{-# COMPILE AGDA2HS Context #-}
-
-------------------------------------------------------------------------------
-
-- | Bidirectional type-checking algorithm:
-- defined by mutual recursion:
-
-- type inference (a.k.a. type synthesis).
-infer : Context → Term → Maybe Type
-- type checking.
-check : Context → Term → Type → Maybe Type
-
-
-codomain : Type → Maybe Type
-codomain BoolType = Nothing
-codomain (ArrowType a b) = Just b
-
-helper : Context → Term →  Maybe Type → Maybe Type
-helper γ x (Just (ArrowType _ tB)) = check γ x tB
-helper _ _ _ = Nothing
-
-{-# COMPILE AGDA2HS helper #-}
-
-- http://cdwifi.cz/#/
-
-infer γ (Var x) = lookup x γ
-infer γ TT = pure BoolType
-infer γ FF = pure BoolType
-infer γ (Abs x t) = pure BoolType -- TODO
-infer γ (App f x) = case (infer γ f) of helper γ x
-infer γ (If a t f) = pure BoolType
-infer γ (Jud x m) = check γ x m
-
-check γ x T = {!!}
-
-{-# COMPILE AGDA2HS infer #-}
-{-# COMPILE AGDA2HS check #-}
--- a/lab/notes/forTesting.md
+++ b/lab/notes/forTesting.md
@ -1,2 +0,0 @@
-
-Examples to test the typechecker:
--- a/lab/notes/module-scoping.org
+++ b/lab/notes/module-scoping.org
@ -1,35 +0,0 @@
-* Module scoping
-  This document contains some notes on how the implementation of module scoping
-  is supposed to work.
-
-** Import statements
-   What happens when we see:
-   #+begin_example
-   import Data.Nat
-   #+end_example
-   All symbols *defined* in =Data.Nat= become available in the current module
-   through qualified names. I.e. =Data.Nat.zero=.
-
-** Open statements
-   What happens when we see:
-   #+begin_example
-   open Data.Nat
-   #+end_example
-   All symbols *defined* in =Data.Nat= become available in the current module
-   through unqualified names. I.e. =zero=.
-
- =using= and =hiding= modifiers are handled in the expected way.
-
-** Nested modules
-   What happens when we see:
-   #+begin_example
-   module Local;
-   ...
-   end;
-   #+end_example
-   We need to answer two questions.
-   1. What happens after =module Local;=. Inside =Local= *all* symbols that were
-      in scope, continue to be in scope.
-   2. What happens after =end;=. All symbols *defined in* =Local= are in scope
-      through qualified names. One can think of this as the same as importing
- =Local= if it was a top module.
--- a/lab/notes/tooling.md
+++ b/lab/notes/tooling.md
@ -1,72 +0,0 @@
-Tools used so far:
-
- cabal-edit
- hlint and checkout
-  https://github.com/kowainik/relude/blob/main/.hlint.yaml for a
-  complex configuration and better hints.
- stan
- summoner
- ghcup
- `implicit-hie` generates `hie.yaml`.
-
- For a good prelude, I tried with Protolude, but it seems a bit
-  abandoned, and it doesn't have support the new Haskell versions.
-  Relude just offered the same, and it is better documented. Let us
-  give it a shot. NoImplicitPrelude plus base-noprelude.
-  https://kowainik.github.io/projects/relude
-
- For Pretty printer, we will use the package
-  https://hackage.haskell.org/package/prettyprinter, which supports
-  nice annotations and colors using Ansi-terminal subpackage:
-    `cabal-edit add prettyprinter-ansi-terminal`.
-
- Two options for the kind of container we can use for Context. Using
-  the package container and for performance, unordered-containers. The
-  latter seems to have the same API naming than the former. So, in
-  principle, it doesn't matter which we use.
-
-
- See
-  [gluedeval](https://gist.github.com/AndrasKovacs/a0e0938113b193d6b9c1c0620d853784).
-  During elaboration different kind of evaluation strategies may be
-  needed.
-    - top vs. local scope. 
- On equality type-checking, see
-  [abstract](https://github.com/anjapetkovic/anjapetkovic.github.io/blob/master/talks/2021-06-17-TYPES2021/abstract.pdf)
- To document the code, see
-  https://kowainik.github.io/posts/haddock-tips
-
-Initial task order for Minijuvix indicated between parenthesis:
-1. Parser (3.)
-2. Typechecker   (1.)
-3. Compiler (2.)
-4. Interpreter (4.)
-
- On deriving stuff using Standalone Der.
-See https://kowainik.github.io/posts/deriving.
- To avoid boilerplate in the cabal file, one could use [common
-  stanzas](https://vrom911.github.io/blog/common-stanzas). At the
-  moment, I'm using cabal-edit to keep the bounds and this tool does
-  not support stanzas. So be it.
-
- Using MultiParamTypeClasses to allow me deriving multi instances in one line. 
-
- TODO: make a `ref.bib` listing all the repositories and the
-  source-code from where I took code, inspiration, whatever thing.
-
- The haskell library https://hackage.haskell.org/package/capability
-  seems to be a right choice. Still, I need to check the details. I
-  will use Juvix Prelude.
-
- Let us use qualified imports to prevent namespace pollution,
-  as much as possible. Checkout:
-  - https://www.haskell.org/onlinereport/haskell2010/haskellch5.html
-  - https://ro-che.info/articles/2019-01-26-haskell-module-system-p2
-  - https://mmhaskell.com/blog/2017/5/8/4-steps-to-a-better-imports-list.
-
- TODO: https://kowainik.github.io/posts/2018-09-09-dhall-to-hlint So
-  far, I have proposed a hlint file, it's clean, but for refactoring,
-  seems to me, the link above shows a better approach.
-
- Let us use the Safe pragma.
-  https://stackoverflow.com/questions/61655158/haskell-safe-and-trustworthy-extensions
--- a/package.yaml
+++ b/package.yaml
@ -28,6 +28,7 @@ dependencies:
 - edit-distance == 0.2.*
 - extra == 1.7.*
 - filepath == 1.4.*
+- gitrev == 1.3.*
 - hashable == 1.4.*
 - megaparsec == 9.2.*
 - microlens-platform == 0.4.*
--- a/src/MiniJuvix/Prelude/Base.hs
+++ b/src/MiniJuvix/Prelude/Base.hs
@ -238,3 +238,12 @@ minimumMaybe l = if null l then Nothing else Just (minimum l)

 fromText :: IsString a => Text -> a
 fromText = fromString . unpack
+
+fromRightIO' :: (e -> IO ()) -> IO (Either e r) -> IO r
+fromRightIO' pp = do
+  eitherM ifLeft return
+  where
+    ifLeft e = pp e >> exitFailure
+
+fromRightIO :: (e -> Text) -> IO (Either e r) -> IO r
+fromRightIO pp = fromRightIO' (putStrLn . pp)
--- a/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs
@ -55,9 +55,13 @@ kwArrow = keyword Str.toAscii
 kwForeign :: Doc Ann
 kwForeign = keyword Str.foreign_

+kwAgda :: Doc Ann
+kwAgda = keyword Str.agda
+
 kwGhc :: Doc Ann
 kwGhc = keyword Str.ghc

+
 kwData :: Doc Ann
 kwData = keyword Str.data_

@ -136,7 +140,8 @@ instance PrettyCode FunctionDef where

 instance PrettyCode Backend where
  ppCode = \case
-    BackendGhc -> return kwGhc
+    BackendGhc  -> return kwGhc
+    BackendAgda -> return kwAgda

 instance PrettyCode ForeignBlock where
  ppCode ForeignBlock {..} = do
--- a/src/MiniJuvix/Termination/CallGraphOld.hs
+++ b/src/MiniJuvix/Termination/CallGraphOld.hs
@ -1,210 +0,0 @@
-module MiniJuvix.Termination.CallGraphOld
-  ( module MiniJuvix.Termination.Types,
-    module MiniJuvix.Termination.CallGraphOld,
-  )
-where
-
-import qualified Data.HashMap.Strict as HashMap
-import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Abstract.Language.Extra
-import MiniJuvix.Syntax.Abstract.Pretty.Base
-import MiniJuvix.Termination.Types
-import Prettyprinter as PP
-
-type Edges = HashMap (FunctionName, FunctionName) Edge
-
-data Edge = Edge
-  { _edgeFrom :: FunctionName,
-    _edgeTo :: FunctionName,
-    _edgeMatrices :: [CallMatrix]
-  }
-
-newtype CompleteCallGraph = CompleteCallGraph Edges
-
-data ReflexiveEdge = ReflexiveEdge
-  { _redgeFun :: FunctionName,
-    _redgeMatrices :: [CallMatrix]
-  }
-
-data RecursiveBehaviour = RecursiveBehaviour
-  { _recBehaviourFunction :: FunctionName,
-    _recBehaviourMatrix :: [[Rel]]
-  }
-
-makeLenses ''RecursiveBehaviour
-makeLenses ''Edge
-makeLenses ''ReflexiveEdge
-
-multiply :: CallMatrix -> CallMatrix -> CallMatrix
-multiply a b = map sumProdRow a
-  where
-    rowB :: Int -> CallRow
-    rowB i = CallRow $ case b !? i of
-      Just (CallRow (Just c)) -> Just c
-      _ -> Nothing
-    sumProdRow :: CallRow -> CallRow
-    sumProdRow (CallRow mr) = CallRow $ do
-      (ki, ra) <- mr
-      (j, rb) <- _callRow (rowB ki)
-      return (j, mul' ra rb)
-
-multiplyMany :: [CallMatrix] -> [CallMatrix] -> [CallMatrix]
-multiplyMany r s = [multiply a b | a <- r, b <- s]
-
-composeEdge :: Edge -> Edge -> Maybe Edge
-composeEdge a b = do
-  guard (a ^. edgeTo == b ^. edgeFrom)
-  return
-    Edge
-      { _edgeFrom = a ^. edgeFrom,
-        _edgeTo = b ^. edgeTo,
-        _edgeMatrices = multiplyMany (a ^. edgeMatrices) (b ^. edgeMatrices)
-      }
-
-fromFunCall :: FunctionName -> FunCall -> Call
-fromFunCall caller fc =
-  Call
-    { _callFrom = caller,
-      _callTo = fc ^. callName,
-      _callMatrix = map fst (fc ^. callArgs)
-    }
-
-completeCallGraph :: CallMap -> CompleteCallGraph
-completeCallGraph cm = CompleteCallGraph (go startingEdges)
-  where
-    startingEdges :: Edges
-    startingEdges = foldr insertCall mempty allCalls
-      where
-        insertCall :: Call -> Edges -> Edges
-        insertCall Call {..} = HashMap.alter (Just . aux) (_callFrom, _callTo)
-          where
-            aux :: Maybe Edge -> Edge
-            aux me = case me of
-              Nothing -> Edge _callFrom _callTo [_callMatrix]
-              Just e -> over edgeMatrices (_callMatrix :) e
-    allCalls :: [Call]
-    allCalls =
-      [ fromFunCall caller funCall
-        | (caller, callerMap) <- HashMap.toList (cm ^. callMap),
-          (_, funCalls) <- HashMap.toList callerMap,
-          funCall <- funCalls
-      ]
-
-    go :: Edges -> Edges
-    go m
-      | edgesCount m == edgesCount m' = m
-      | otherwise = go m'
-      where
-        m' = step m
-
-    step :: Edges -> Edges
-    step s = edgesUnion (edgesCompose s startingEdges) s
-
-    fromEdgeList :: [Edge] -> Edges
-    fromEdgeList l = HashMap.fromList [((e ^. edgeFrom, e ^. edgeTo), e) | e <- l]
-
-    edgesCompose :: Edges -> Edges -> Edges
-    edgesCompose a b =
-      fromEdgeList $
-        catMaybes
-          [composeEdge ea eb | ea <- toList a, eb <- toList b]
-    edgesUnion :: Edges -> Edges -> Edges
-    edgesUnion = HashMap.union
-    edgesCount :: Edges -> Int
-    edgesCount = HashMap.size
-
-reflexiveEdges :: CompleteCallGraph -> [ReflexiveEdge]
-reflexiveEdges (CompleteCallGraph es) = mapMaybe reflexive (toList es)
-  where
-    reflexive :: Edge -> Maybe ReflexiveEdge
-    reflexive e
-      | e ^. edgeFrom == e ^. edgeTo =
-        Just $ ReflexiveEdge (e ^. edgeFrom) (e ^. edgeMatrices)
-      | otherwise = Nothing
-
-callMatrixDiag :: CallMatrix -> [Rel]
-callMatrixDiag m = [col i r | (i, r) <- zip [0 :: Int ..] m]
-  where
-    col :: Int -> CallRow -> Rel
-    col i (CallRow row) = case row of
-      Nothing -> RNothing
-      Just (j, r')
-        | i == j -> RJust r'
-        | otherwise -> RNothing
-
-recursiveBehaviour :: ReflexiveEdge -> RecursiveBehaviour
-recursiveBehaviour re =
-  RecursiveBehaviour
-    (re ^. redgeFun)
-    (map callMatrixDiag (re ^. redgeMatrices))
-
-findOrder :: RecursiveBehaviour -> Maybe LexOrder
-findOrder rb = LexOrder <$> listToMaybe (mapMaybe (isLexOrder >=> nonEmpty) allPerms)
-  where
-    b0 :: [[Rel]]
-    b0 = rb ^. recBehaviourMatrix
-    indexed = map (zip [0 :: Int ..] . take minLength) b0
-      where
-        minLength = minimum (map length b0)
-
-    startB = removeUselessColumns indexed
-
-    -- removes columns that don't have at least one ≺ in them
-    removeUselessColumns :: [[(Int, Rel)]] -> [[(Int, Rel)]]
-    removeUselessColumns = transpose . filter (any (isLess . snd)) . transpose
-
-    isLexOrder :: [Int] -> Maybe [Int]
-    isLexOrder = go startB
-      where
-        go :: [[(Int, Rel)]] -> [Int] -> Maybe [Int]
-        go [] _ = Just []
-        go b perm = case perm of
-          [] -> error "The permutation should have one element at least!"
-          (p0 : ptail)
-            | Just r <- find (isLess . snd . (!! p0)) b,
-              all (notNothing . snd . (!! p0)) b,
-              Just perm' <- go (b' p0) (map pred ptail) ->
-              Just (fst (r !! p0) : perm')
-            | otherwise -> Nothing
-          where
-            b' i = map r' (filter (not . isLess . snd . (!! i)) b)
-              where
-                r' r = case splitAt i r of
-                  (x, y) -> x ++ drop 1 y
-
-    notNothing = (RNothing /=)
-    isLess = (RJust RLe ==)
-
-    allPerms :: [[Int]]
-    allPerms = case nonEmpty startB of
-      Nothing -> []
-      Just s -> permutations [0 .. length (head s) - 1]
-
-instance PrettyCode Edge where
-  ppCode Edge {..} = do
-    fromFun <- ppSCode _edgeFrom
-    toFun <- ppSCode _edgeTo
-    matrices <- indent 2 . ppMatrices . zip [0 :: Int ..] <$> mapM ppCode _edgeMatrices
-    return $
-      pretty ("Edge" :: Text) <+> fromFun <+> waveFun <+> toFun <> line
-        <> matrices
-    where
-      ppMatrices = vsep2 . map ppMatrix
-      ppMatrix (i, t) =
-        pretty ("Matrix" :: Text) <+> pretty i <> colon <> line
-          <> t
-
-instance PrettyCode CompleteCallGraph where
-  ppCode :: forall r. Members '[Reader Options] r => CompleteCallGraph -> Sem r (Doc Ann)
-  ppCode (CompleteCallGraph edges) = do
-    es <- vsep2 <$> mapM ppCode (toList edges)
-    return $ pretty ("Complete Call Graph:" :: Text) <> line <> es
-
-instance PrettyCode RecursiveBehaviour where
-  ppCode :: forall r. Members '[Reader Options] r => RecursiveBehaviour -> Sem r (Doc Ann)
-  ppCode (RecursiveBehaviour f m) = do
-    f' <- ppSCode f
-    let m' = vsep (map (PP.list . map pretty) m)
-    return $
-      pretty ("Recursive behaviour of " :: Text) <> f' <> colon <> line
-        <> indent 2 (align m')
--- a/src/MiniJuvix/Utils/Version.hs
+++ b/src/MiniJuvix/Utils/Version.hs
@ -1,40 +1,78 @@
-module MiniJuvix.Utils.Version (getVersion) where
+module MiniJuvix.Utils.Version
+  ( branch,
+    commit,
+    commitDate,
+    infoVersionRepo,
+    progName,
+    progNameVersion,
+    progNameVersionTag,
+    runDisplayVersion,
+    shortHash,
+    versionDoc,
+    versionTag,
+)
+where

 ------------------------------------------------------------------------------

-import Control.Exception (IOException)
-import qualified Control.Exception as Exception
-import qualified Data.List as List
-import Data.Version (Version (versionTags))
-import MiniJuvix.Prelude
-import System.Exit
-import System.Process (readProcessWithExitCode)
+import Data.Version (showVersion)
+import Development.GitRev (gitBranch, gitCommitDate, gitHash)
+import MiniJuvix.Prelude hiding (Doc)
+import qualified Paths_minijuvix
+import Prettyprinter as PP
+import Prettyprinter.Render.Text (renderIO)
+import System.Environment (getProgName)

 ------------------------------------------------------------------------------

-tryIO :: IO a -> IO (Either IOException a)
-tryIO = Exception.try
+versionDoc :: Doc Text
+versionDoc = PP.pretty (showVersion Paths_minijuvix.version)

-commitInfo :: IO (Maybe String)
-commitInfo = do
-  res <-
-    tryIO $
-      readProcessWithExitCode "git" ["log", "--format=%h", "-n", "1"] ""
-  case res of
-    Right (ExitSuccess, hash, _) -> do
-      (_, _, _) <- readProcessWithExitCode "git" ["diff", "--quiet"] ""
-      return $ Just (List.init hash)
-    _ -> return Nothing
+branch :: Doc Text
+branch = PP.pretty (pack $(gitBranch))

-gitVersion :: Version -> String -> Version
-gitVersion version hash = version {versionTags = [take 7 hash]}
+commit :: Doc Text
+commit = PP.pretty (pack $(gitHash))

-- | If inside a `git` repository, then @'getVersion' x@ will return
-- @x@ plus the hash of the top commit used for
-- compilation. Otherwise, only @x@ will be returned.
-getVersion :: Version -> IO Version
-getVersion version = do
-  commit <- commitInfo
-  case commit of
-    Nothing -> return version
-    Just rev -> return $ gitVersion version rev
+commitDate :: Doc Text
+commitDate = PP.pretty (pack $(gitCommitDate))
+
+shortHash :: Doc Text
+shortHash = PP.pretty (pack (take 7 $(gitHash)))
+
+versionTag :: Doc Text
+versionTag = versionDoc <> "-" <> shortHash
+
+progName :: IO (Doc Text)
+progName = PP.pretty . pack . toUpperFirst <$> getProgName
+
+progNameVersion :: IO (Doc Text)
+progNameVersion = do
+  pName <- progName
+  pure (pName <+> "version" <+> versionDoc)
+
+progNameVersionTag :: IO (Doc Text)
+progNameVersionTag = do
+  progNameV <- progNameVersion
+  pure (progNameV <> "-" <> shortHash)
+
+infoVersionRepo :: IO (Doc Text)
+infoVersionRepo = do
+  pNameTag <- progNameVersionTag
+  pure
+    ( pNameTag <> line
+        <> "Branch"
+        <> colon <+> branch
+        <> line
+        <> "Commit"
+        <> colon <+> commit
+        <> line
+        <> "Date"
+        <> colon <+> commitDate
+        <> line
+    )
+
+runDisplayVersion :: IO ()
+runDisplayVersion = do
+  v <- layoutPretty defaultLayoutOptions <$> infoVersionRepo
+  renderIO stdout v
--- a/stack.yaml
+++ b/stack.yaml
@ -1,2 +1,4 @@
+ghc-options:
+  "$locals": -optP-Wno-nonportable-include-path
 resolver: nightly-2022-03-23
-extra-deps: []
+extra-deps: []