Merge branch 'main' into dev

app/Main.hs

@@ -61,7 +61,7 @@ data ParseOptions = ParseOptions
   { _parseInputFile :: FilePath,
     _parseNoPrettyShow :: Bool
   }
-
+  
 newtype HighlightOptions = HighlightOptions
   { _highlightInputFile :: FilePath
   }
@@ -182,6 +182,7 @@ parseCommand =
   <|> parseDisplayRoot
   <|> hsubparser
           (mconcat
+
             [ commandParse,
               commandScope,
               commandHtml,

src/MiniJuvix/Syntax/MicroJuvix/Error/Pretty/Base.hs

@@ -50,6 +50,7 @@ instance PrettyError WrongConstructorAppArgs where
       ctorName = ppCode (e ^. wrongCtorAppApp . constrAppConstructor)
       pat :: Int -> Doc ann
       pat n = pretty n <+> plural "pattern" "patterns" n
+
       funName :: Name
       funName = e ^. wrongCtorAppName
 

src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs

@@ -13,6 +13,7 @@ data WrongConstructorType = WrongConstructorType
   }
   deriving stock (Show)
 
+
 -- | the arguments of a constructor pattern do not match
 -- the expected arguments of the constructor
 data WrongConstructorAppArgs = WrongConstructorAppArgs
@@ -30,6 +31,7 @@ data WrongType = WrongType
   }
   deriving stock (Show)
 
+
 -- | The left hand expression of a function application is not
 -- a function type.
 data ExpectedFunctionType = ExpectedFunctionType
@@ -39,6 +41,7 @@ data ExpectedFunctionType = ExpectedFunctionType
   }
   deriving stock (Show)
 
+
 -- | A function definition clause matches too many arguments
 data TooManyPatterns = TooManyPatterns
   { _tooManyPatternsClause :: FunctionClause,

src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs

@@ -10,6 +10,7 @@ data ConstructorInfo = ConstructorInfo {
   _constructorInfoInductive :: InductiveName
   }
 
+
 newtype FunctionInfo = FunctionInfo {
   _functionInfoType :: Type
   }

src/MiniJuvix/Syntax/MicroJuvix/Language.hs

@@ -2,6 +2,7 @@ module MiniJuvix.Syntax.MicroJuvix.Language
   ( module MiniJuvix.Syntax.MicroJuvix.Language,
     module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
     module MiniJuvix.Syntax.Concrete.Scoped.Name,
+    module MiniJuvix.Syntax.Concrete.Literal,
   )
 where
 
@@ -15,6 +16,7 @@ import MiniJuvix.Syntax.Fixity
 import Prettyprinter
 import MiniJuvix.Syntax.Concrete.Language (HasLoc)
 
+
 type FunctionName = Name
 
 type AxiomName = Name

src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -20,6 +20,7 @@ checkModule m = run $ do
     (x : xs) -> Left (x :| xs)
 
 checkModule' :: Members '[Reader InfoTable, Output TypeCheckerError] r =>
+
   Module -> Sem r Module
 checkModule' Module {..} = do
   _moduleBody' <- checkModuleBody _moduleBody
@@ -28,6 +29,7 @@ checkModule' Module {..} = do
     ..
     }
 
+
 checkModuleBody :: Members '[Reader InfoTable, Output TypeCheckerError] r =>
   ModuleBody -> Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
@@ -66,6 +68,7 @@ checkExpression t e = do
                                            _wrongTypeInferredType = infTy,
                                            _wrongTypeExpectedType = t})
 
+
 inferExpression :: Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars] r =>
    Expression -> Sem r Expression
 inferExpression = fmap ExpressionTyped . inferExpression'

src/MiniJuvix/Translation/AbstractToMicroJuvix.hs

@@ -30,6 +30,7 @@ goSymbol s =
       _nameDefined = s ^. S.nameDefined,
       _nameLoc = s ^. S.nameConcrete . symbolLoc }
 
+
 unsupported :: Text -> a
 unsupported thing = error ("Abstract to MicroJuvix: Not yet supported: " <> thing)
 

test/TypeCheck/Negative.hs

@@ -13,6 +13,7 @@ data NegTest = NegTest
     file :: FilePath,
     checkErr :: [TypeCheckerError] -> Maybe FailMsg }
 
+
 testDescr :: NegTest -> TestDescr
 testDescr NegTest {..} = TestDescr {
   testName = name,
@@ -26,6 +27,7 @@ testDescr NegTest {..} = TestDescr {
 
       case result of
         Left es -> whenJust (checkErr (toList es)) assertFailure
+
         Right _ -> assertFailure "The type checker did not find an error."
   }
 

tests/positive/VP/SimpleFungibleToken.mjuvix

@@ -147,3 +147,4 @@ vp token keys-changed verifiers :=
   auxVP (foldl (check-keys verifiers) (MakePair 0 false) keys-changed);
 
 end;
+