Refactor of typechecking and other checking processes (#1410)

* Refactor in progress

* Fixing imports and missing references

* Remove unnecessary import

app/Main.hs

@@ -6,24 +6,24 @@ import Commands.Internal.Termination as Termination
 import Control.Exception qualified as IO
 import Control.Monad.Extra
 import Data.HashMap.Strict qualified as HashMap
+import Juvix.Analysis.Scoping.Scoper qualified as Scoper
+import Juvix.Analysis.Termination qualified as Termination
+import Juvix.Analysis.TypeChecking qualified as MicroTyped
+import Juvix.Parsing.Parser qualified as Parser
 import Juvix.Pipeline
 import Juvix.Prelude hiding (Doc)
 import Juvix.Prelude.Pretty hiding (Doc)
 import Juvix.Syntax.Abstract.InfoTable qualified as Abstract
 import Juvix.Syntax.Abstract.Language qualified as Abstract
 import Juvix.Syntax.Abstract.Pretty qualified as Abstract
-import Juvix.Syntax.Concrete.Parser qualified as Parser
 import Juvix.Syntax.Concrete.Scoped.Highlight qualified as Highlight
 import Juvix.Syntax.Concrete.Scoped.InfoTable qualified as Scoper
 import Juvix.Syntax.Concrete.Scoped.Pretty qualified as Scoper
 import Juvix.Syntax.Concrete.Scoped.Pretty.Html
-import Juvix.Syntax.Concrete.Scoped.Scoper qualified as Scoper
 import Juvix.Syntax.MicroJuvix.MicroJuvixArityResult qualified as MicroArity
 import Juvix.Syntax.MicroJuvix.Pretty qualified as Micro
-import Juvix.Syntax.MicroJuvix.TypeChecker qualified as MicroTyped
 import Juvix.Syntax.MiniHaskell.Pretty qualified as MiniHaskell
 import Juvix.Syntax.MonoJuvix.Pretty qualified as Mono
-import Juvix.Termination qualified as Termination
 import Juvix.Translation.AbstractToMicroJuvix qualified as Micro
 import Juvix.Translation.MicroJuvixToMiniC qualified as MiniC
 import Juvix.Translation.MicroJuvixToMonoJuvix qualified as Mono

src/Juvix/Syntax/MicroJuvix/ArityChecker.hs → src/Juvix/Analysis/Arity.hs

@@ -1,15 +1,15 @@
-module Juvix.Syntax.MicroJuvix.ArityChecker
-  ( module Juvix.Syntax.MicroJuvix.ArityChecker,
+module Juvix.Analysis.Arity
+  ( module Juvix.Analysis.Arity,
     module Juvix.Syntax.MicroJuvix.MicroJuvixArityResult,
-    module Juvix.Syntax.MicroJuvix.ArityChecker.Error,
+    module Juvix.Analysis.Arity.Error,
   )
 where
 
+import Juvix.Analysis.Arity.Arity
+import Juvix.Analysis.Arity.Error
+import Juvix.Analysis.Arity.LocalVars
 import Juvix.Internal.NameIdGen
 import Juvix.Prelude hiding (fromEither)
-import Juvix.Syntax.MicroJuvix.ArityChecker.Arity
-import Juvix.Syntax.MicroJuvix.ArityChecker.Error
-import Juvix.Syntax.MicroJuvix.ArityChecker.LocalVars
 import Juvix.Syntax.MicroJuvix.InfoTable
 import Juvix.Syntax.MicroJuvix.Language.Extra
 import Juvix.Syntax.MicroJuvix.MicroJuvixArityResult

src/Juvix/Syntax/MicroJuvix/ArityChecker/Arity.hs → src/Juvix/Analysis/Arity/Arity.hs

@@ -1,4 +1,4 @@
-module Juvix.Syntax.MicroJuvix.ArityChecker.Arity where
+module Juvix.Analysis.Arity.Arity where
 
 import Juvix.Prelude
 

src/Juvix/Syntax/MicroJuvix/ArityChecker/Error.hs → src/Juvix/Analysis/Arity/Error.hs

@@ -1,11 +1,11 @@
-module Juvix.Syntax.MicroJuvix.ArityChecker.Error
-  ( module Juvix.Syntax.MicroJuvix.ArityChecker.Error,
-    module Juvix.Syntax.MicroJuvix.ArityChecker.Error.Types,
+module Juvix.Analysis.Arity.Error
+  ( module Juvix.Analysis.Arity.Error,
+    module Juvix.Analysis.Arity.Error.Types,
   )
 where
 
+import Juvix.Analysis.Arity.Error.Types
 import Juvix.Prelude
-import Juvix.Syntax.MicroJuvix.ArityChecker.Error.Types
 
 data ArityCheckerError
   = ErrWrongConstructorAppLength WrongConstructorAppLength

src/Juvix/Syntax/MicroJuvix/ArityChecker/Error/Types.hs → src/Juvix/Analysis/Arity/Error/Types.hs

@@ -1,4 +1,4 @@
-module Juvix.Syntax.MicroJuvix.ArityChecker.Error.Types where
+module Juvix.Analysis.Arity.Error.Types where
 
 -- import Juvix.Syntax.MicroJuvix.Error.Pretty
 import Juvix.Prelude

src/Juvix/Syntax/MicroJuvix/ArityChecker/LocalVars.hs → src/Juvix/Analysis/Arity/LocalVars.hs

@@ -1,8 +1,8 @@
-module Juvix.Syntax.MicroJuvix.ArityChecker.LocalVars where
+module Juvix.Analysis.Arity.LocalVars where
 
 import Data.HashMap.Strict qualified as HashMap
+import Juvix.Analysis.Arity.Arity
 import Juvix.Prelude
-import Juvix.Syntax.MicroJuvix.ArityChecker.Arity
 import Juvix.Syntax.MicroJuvix.Language
 
 newtype LocalVars = LocalVars

src/Juvix/Analysis/Positivity.hs

@@ -0,0 +1,6 @@
+module Juvix.Analysis.Positivity
+  ( module Juvix.Analysis.Positivity.Checker,
+  )
+where
+
+import Juvix.Analysis.Positivity.Checker

src/Juvix/Analysis/Positivity/Checker.hs

@@ -3,12 +3,12 @@ module Juvix.Analysis.Positivity.Checker where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
+import Juvix.Analysis.TypeChecking.Inference
 import Juvix.Pipeline.EntryPoint qualified as E
 import Juvix.Prelude hiding (fromEither)
 import Juvix.Syntax.MicroJuvix.Error
 import Juvix.Syntax.MicroJuvix.InfoTable
 import Juvix.Syntax.MicroJuvix.Language.Extra
-import Juvix.Syntax.MicroJuvix.TypeChecker.Inference
 
 type NegativeTypeParameters = HashSet VarName
 

src/Juvix/Analysis/Scoping.hs

@@ -0,0 +1,12 @@
+module Juvix.Analysis.Scoping
+  ( module Juvix.Analysis.Scoping.Scope,
+    module Juvix.Analysis.Scoping.Scoper,
+    module Juvix.Analysis.Scoping.InfoTableBuilder,
+    module Juvix.Analysis.Scoping.ScoperResult,
+  )
+where
+
+import Juvix.Analysis.Scoping.InfoTableBuilder
+import Juvix.Analysis.Scoping.Scope
+import Juvix.Analysis.Scoping.Scoper
+import Juvix.Analysis.Scoping.ScoperResult

src/Juvix/Syntax/Concrete/Scoped/Scoper/InfoTableBuilder.hs → src/Juvix/Analysis/Scoping/InfoTableBuilder.hs

@@ -1,10 +1,10 @@
-module Juvix.Syntax.Concrete.Scoped.Scoper.InfoTableBuilder where
+module Juvix.Analysis.Scoping.InfoTableBuilder where
 
 import Data.HashMap.Strict qualified as HashMap
+import Juvix.Analysis.Scoping.Scope
 import Juvix.Prelude
 import Juvix.Syntax.Concrete.Language
 import Juvix.Syntax.Concrete.Scoped.Name qualified as S
-import Juvix.Syntax.Concrete.Scoped.Scope
 
 data InfoTableBuilder m a where
   RegisterAxiom :: AxiomDef 'Scoped -> InfoTableBuilder m ()

src/Juvix/Syntax/Concrete/Scoped/Scope.hs → src/Juvix/Analysis/Scoping/Scope.hs

@@ -1,5 +1,5 @@
-module Juvix.Syntax.Concrete.Scoped.Scope
-  ( module Juvix.Syntax.Concrete.Scoped.Scope,
+module Juvix.Analysis.Scoping.Scope
+  ( module Juvix.Analysis.Scoping.Scope,
     module Juvix.Syntax.Concrete.Scoped.InfoTable,
   )
 where

src/Juvix/Syntax/Concrete/Scoped/Scoper.hs → src/Juvix/Analysis/Scoping/Scoper.hs

@@ -1,8 +1,8 @@
 -- | Limitations:
 -- 1. A symbol introduced by a type signature can only be used once per Module.
-module Juvix.Syntax.Concrete.Scoped.Scoper
-  ( module Juvix.Syntax.Concrete.Scoped.Scoper,
-    module Juvix.Syntax.Concrete.Scoped.Scoper.ScoperResult,
+module Juvix.Analysis.Scoping.Scoper
+  ( module Juvix.Analysis.Scoping.Scoper,
+    module Juvix.Analysis.Scoping.ScoperResult,
     module Juvix.Syntax.Concrete.Scoped.Error,
   )
 where
@@ -11,22 +11,22 @@ import Control.Monad.Combinators.Expr qualified as P
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
 import Data.List.NonEmpty qualified as NonEmpty
+import Juvix.Analysis.Scoping.InfoTableBuilder
+import Juvix.Analysis.Scoping.Scope
+import Juvix.Analysis.Scoping.ScoperResult
 import Juvix.Internal.NameIdGen
+import Juvix.Parsing.InfoTableBuilder (mergeTable)
+import Juvix.Parsing.InfoTableBuilder qualified as Parser
+import Juvix.Parsing.Parser (runModuleParser)
+import Juvix.Parsing.Parser qualified as Parser
+import Juvix.Parsing.ParserResult (ParserResult)
 import Juvix.Pipeline.EntryPoint
 import Juvix.Prelude
 import Juvix.Syntax.Concrete.Base qualified as P
 import Juvix.Syntax.Concrete.Language
 import Juvix.Syntax.Concrete.Name qualified as N
-import Juvix.Syntax.Concrete.Parser (runModuleParser)
-import Juvix.Syntax.Concrete.Parser qualified as Parser
-import Juvix.Syntax.Concrete.Parser.InfoTableBuilder (mergeTable)
-import Juvix.Syntax.Concrete.Parser.InfoTableBuilder qualified as Parser
-import Juvix.Syntax.Concrete.Parser.ParserResult (ParserResult)
 import Juvix.Syntax.Concrete.Scoped.Error
 import Juvix.Syntax.Concrete.Scoped.Name qualified as S
-import Juvix.Syntax.Concrete.Scoped.Scope
-import Juvix.Syntax.Concrete.Scoped.Scoper.InfoTableBuilder
-import Juvix.Syntax.Concrete.Scoped.Scoper.ScoperResult
 
 entryScoper ::
   Members '[Error ScoperError, Files, NameIdGen] r =>

src/Juvix/Syntax/Concrete/Scoped/Scoper/ScoperResult.hs → src/Juvix/Analysis/Scoping/ScoperResult.hs

@@ -1,8 +1,8 @@
-module Juvix.Syntax.Concrete.Scoped.Scoper.ScoperResult where
+module Juvix.Analysis.Scoping.ScoperResult where
 
+import Juvix.Parsing.Parser qualified as Parser
 import Juvix.Prelude
 import Juvix.Syntax.Concrete.Language
-import Juvix.Syntax.Concrete.Parser qualified as Parser
 import Juvix.Syntax.Concrete.Scoped.InfoTable qualified as Scoped
 
 data ScoperResult = ScoperResult

src/Juvix/Analysis/Termination.hs

@@ -0,0 +1,12 @@
+module Juvix.Analysis.Termination
+  ( module Juvix.Analysis.Termination.Checker,
+    module Juvix.Analysis.Termination.Types,
+    module Juvix.Analysis.Termination.Error,
+    module Juvix.Analysis.Termination.LexOrder,
+  )
+where
+
+import Juvix.Analysis.Termination.Checker
+import Juvix.Analysis.Termination.Error
+import Juvix.Analysis.Termination.LexOrder
+import Juvix.Analysis.Termination.Types

src/Juvix/Termination/Checker.hs → src/Juvix/Analysis/Termination/Checker.hs

@@ -1,18 +1,18 @@
-module Juvix.Termination.Checker
-  ( module Juvix.Termination.Checker,
-    module Juvix.Termination.FunctionCall,
-    module Juvix.Termination.Error,
+module Juvix.Analysis.Termination.Checker
+  ( module Juvix.Analysis.Termination.Checker,
+    module Juvix.Analysis.Termination.FunctionCall,
+    module Juvix.Analysis.Termination.Error,
   )
 where
 
 import Data.HashMap.Internal.Strict qualified as HashMap
+import Juvix.Analysis.Termination.Error
+import Juvix.Analysis.Termination.FunctionCall
+import Juvix.Analysis.Termination.LexOrder
+import Juvix.Analysis.Termination.Types
 import Juvix.Prelude
 import Juvix.Syntax.Abstract.InfoTable as Abstract
 import Juvix.Syntax.Abstract.Language as Abstract
-import Juvix.Termination.Error
-import Juvix.Termination.FunctionCall
-import Juvix.Termination.LexOrder
-import Juvix.Termination.Types
 
 checkTermination ::
   Members '[Error TerminationError] r =>

src/Juvix/Analysis/Termination/Error.hs

@@ -0,0 +1,19 @@
+module Juvix.Analysis.Termination.Error
+  ( module Juvix.Analysis.Termination.Error,
+    module Juvix.Analysis.Termination.Error.Pretty,
+    module Juvix.Analysis.Termination.Error.Types,
+  )
+where
+
+import Juvix.Analysis.Termination.Error.Pretty
+import Juvix.Analysis.Termination.Error.Types
+import Juvix.Prelude
+
+newtype TerminationError
+  = ErrNoLexOrder NoLexOrder
+  deriving stock (Show)
+
+instance ToGenericError TerminationError where
+  genericError :: TerminationError -> GenericError
+  genericError = \case
+    ErrNoLexOrder e -> genericError e

src/Juvix/Termination/Error/Pretty.hs → src/Juvix/Analysis/Termination/Error/Pretty.hs

@@ -1,13 +1,13 @@
-module Juvix.Termination.Error.Pretty
-  ( module Juvix.Termination.Error.Pretty,
-    module Juvix.Termination.Error.Pretty.Ann,
+module Juvix.Analysis.Termination.Error.Pretty
+  ( module Juvix.Analysis.Termination.Error.Pretty,
+    module Juvix.Analysis.Termination.Error.Pretty.Ann,
   )
 where
 
+import Juvix.Analysis.Termination.Error.Pretty.Ann
+import Juvix.Analysis.Termination.Error.Pretty.Ansi qualified as Ansi
 import Juvix.Prelude
 import Juvix.Prelude.Pretty
-import Juvix.Termination.Error.Pretty.Ann
-import Juvix.Termination.Error.Pretty.Ansi qualified as Ansi
 
 newtype PPOutput = PPOutput (Doc Eann)
 

src/Juvix/Termination/Error/Pretty/Ann.hs → src/Juvix/Analysis/Termination/Error/Pretty/Ann.hs

@@ -1,4 +1,4 @@
-module Juvix.Termination.Error.Pretty.Ann where
+module Juvix.Analysis.Termination.Error.Pretty.Ann where
 
 import Juvix.Syntax.Abstract.Pretty.Ann
 

src/Juvix/Termination/Error/Pretty/Ansi.hs → src/Juvix/Analysis/Termination/Error/Pretty/Ansi.hs

@@ -1,11 +1,11 @@
-module Juvix.Termination.Error.Pretty.Ansi
-  ( module Juvix.Termination.Error.Pretty.Ansi,
+module Juvix.Analysis.Termination.Error.Pretty.Ansi
+  ( module Juvix.Analysis.Termination.Error.Pretty.Ansi,
   )
 where
 
+import Juvix.Analysis.Termination.Error.Pretty.Ann
 import Juvix.Prelude
 import Juvix.Syntax.Abstract.Pretty.Ansi qualified as M
-import Juvix.Termination.Error.Pretty.Ann
 import Prettyprinter
 import Prettyprinter.Render.Terminal
 

src/Juvix/Termination/Error/Types.hs → src/Juvix/Analysis/Termination/Error/Types.hs

@@ -1,9 +1,9 @@
-module Juvix.Termination.Error.Types where
+module Juvix.Analysis.Termination.Error.Types where
 
+import Juvix.Analysis.Termination.Error.Pretty
 import Juvix.Prelude
 import Juvix.Prelude.Pretty
 import Juvix.Syntax.Abstract.Language
-import Juvix.Termination.Error.Pretty
 
 newtype NoLexOrder = NoLexOrder
   { _noLexOrderFun :: Name

src/Juvix/Termination/FunctionCall.hs → src/Juvix/Analysis/Termination/FunctionCall.hs

@@ -1,12 +1,12 @@
-module Juvix.Termination.FunctionCall
-  ( module Juvix.Termination.FunctionCall,
+module Juvix.Analysis.Termination.FunctionCall
+  ( module Juvix.Analysis.Termination.FunctionCall,
   )
 where
 
 import Data.HashMap.Strict qualified as HashMap
+import Juvix.Analysis.Termination.Types
 import Juvix.Prelude
 import Juvix.Syntax.Abstract.Language.Extra
-import Juvix.Termination.Types
 
 viewCall ::
   forall r.

src/Juvix/Termination/LexOrder.hs → src/Juvix/Analysis/Termination/LexOrder.hs

@@ -1,13 +1,13 @@
-module Juvix.Termination.LexOrder
-  ( module Juvix.Termination.LexOrder,
+module Juvix.Analysis.Termination.LexOrder
+  ( module Juvix.Analysis.Termination.LexOrder,
   )
 where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
+import Juvix.Analysis.Termination.Types
 import Juvix.Prelude
 import Juvix.Syntax.Abstract.Language.Extra
-import Juvix.Termination.Types
 
 fromEdgeList :: [Edge] -> Graph
 fromEdgeList l = HashMap.fromList [((e ^. edgeFrom, e ^. edgeTo), e) | e <- l]

src/Juvix/Analysis/Termination/Types.hs

@@ -0,0 +1,12 @@
+module Juvix.Analysis.Termination.Types
+  ( module Juvix.Analysis.Termination.Types.FunctionCall,
+    module Juvix.Analysis.Termination.Types.Graph,
+    module Juvix.Analysis.Termination.Types.SizeInfo,
+    module Juvix.Analysis.Termination.Types.SizeRelation,
+  )
+where
+
+import Juvix.Analysis.Termination.Types.FunctionCall
+import Juvix.Analysis.Termination.Types.Graph
+import Juvix.Analysis.Termination.Types.SizeInfo
+import Juvix.Analysis.Termination.Types.SizeRelation

src/Juvix/Termination/Types/FunctionCall.hs → src/Juvix/Analysis/Termination/Types/FunctionCall.hs

@@ -1,10 +1,10 @@
-module Juvix.Termination.Types.FunctionCall (module Juvix.Termination.Types.FunctionCall) where
+module Juvix.Analysis.Termination.Types.FunctionCall (module Juvix.Analysis.Termination.Types.FunctionCall) where
 
 import Data.HashMap.Strict qualified as HashMap
+import Juvix.Analysis.Termination.Types.SizeRelation
 import Juvix.Prelude
 import Juvix.Syntax.Abstract.Language
 import Juvix.Syntax.Abstract.Pretty.Base
-import Juvix.Termination.Types.SizeRelation
 import Prettyprinter as PP
 
 newtype CallMap = CallMap

src/Juvix/Termination/Types/Graph.hs → src/Juvix/Analysis/Termination/Types/Graph.hs

@@ -1,15 +1,15 @@
-module Juvix.Termination.Types.Graph
-  ( module Juvix.Termination.Types.Graph,
+module Juvix.Analysis.Termination.Types.Graph
+  ( module Juvix.Analysis.Termination.Types.Graph,
   )
 where
 
 import Data.HashSet qualified as HashSet
+import Juvix.Analysis.Termination.Types.FunctionCall
+import Juvix.Analysis.Termination.Types.SizeRelation
 import Juvix.Prelude
 import Juvix.Prelude.Pretty
 import Juvix.Syntax.Abstract.Language.Extra
 import Juvix.Syntax.Abstract.Pretty.Base
-import Juvix.Termination.Types.FunctionCall
-import Juvix.Termination.Types.SizeRelation
 import Prettyprinter as PP
 
 type Graph = HashMap (FunctionName, FunctionName) Edge

src/Juvix/Termination/Types/SizeInfo.hs → src/Juvix/Analysis/Termination/Types/SizeInfo.hs

@@ -1,4 +1,4 @@
-module Juvix.Termination.Types.SizeInfo where
+module Juvix.Analysis.Termination.Types.SizeInfo where
 
 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Prelude