Remove old typechecker (#2545)

app/Commands/Dev/Internal.hs

@@ -1,7 +1,6 @@
 module Commands.Dev.Internal where
 
 import Commands.Base
-import Commands.Dev.Internal.Arity qualified as Arity
 import Commands.Dev.Internal.Options
 import Commands.Dev.Internal.Pretty qualified as Pretty
 import Commands.Dev.Internal.Reachability qualified as Reachability
@@ -10,6 +9,5 @@ import Commands.Dev.Internal.Typecheck qualified as Typecheck
 runCommand :: (Members '[Embed IO, App] r) => InternalCommand -> Sem r ()
 runCommand = \case
   Pretty opts -> Pretty.runCommand opts
-  Arity opts -> Arity.runCommand opts
   TypeCheck opts -> Typecheck.runCommand opts
   Reachability opts -> Reachability.runCommand opts

app/Commands/Dev/Internal/Options.hs

@@ -1,6 +1,5 @@
 module Commands.Dev.Internal.Options where
 
-import Commands.Dev.Internal.Arity.Options
 import Commands.Dev.Internal.Pretty.Options
 import Commands.Dev.Internal.Reachability.Options
 import Commands.Dev.Internal.Typecheck.Options
@@ -9,7 +8,6 @@ import CommonOptions
 data InternalCommand
   = Pretty InternalPrettyOptions
   | TypeCheck InternalTypeOptions
-  | Arity InternalArityOptions
   | Reachability InternalReachabilityOptions
   deriving stock (Data)
 
@@ -18,14 +16,10 @@ parseInternalCommand =
   hsubparser $
     mconcat
       [ commandPretty,
-        commandArity,
         commandTypeCheck,
         commandReachability
       ]
   where
-    commandArity :: Mod CommandFields InternalCommand
-    commandArity = command "arity" arityInfo
-
     commandPretty :: Mod CommandFields InternalCommand
     commandPretty = command "pretty" prettyInfo
 
@@ -35,12 +29,6 @@ parseInternalCommand =
     commandReachability :: Mod CommandFields InternalCommand
     commandReachability = command "reachability" reachabilityInfo
 
-    arityInfo :: ParserInfo InternalCommand
-    arityInfo =
-      info
-        (Arity <$> parseInternalArity)
-        (progDesc "Translate a Juvix file to Internal and insert holes")
-
     prettyInfo :: ParserInfo InternalCommand
     prettyInfo =
       info

app/GlobalOptions.hs

@@ -20,8 +20,7 @@ data GlobalOptions = GlobalOptions
     _globalNoCoverage :: Bool,
     _globalNoStdlib :: Bool,
     _globalUnrollLimit :: Int,
-    _globalOffline :: Bool,
-    _globalNewTypecheckingAlgorithm :: Bool
+    _globalOffline :: Bool
   }
   deriving stock (Eq, Show)
 
@@ -61,8 +60,7 @@ defaultGlobalOptions =
       _globalNoCoverage = False,
       _globalNoStdlib = False,
       _globalUnrollLimit = defaultUnrollLimit,
-      _globalOffline = False,
-      _globalNewTypecheckingAlgorithm = False
+      _globalOffline = False
     }
 
 -- | Get a parser for global flags which can be hidden or not depending on
@@ -128,11 +126,6 @@ parseGlobalFlags = do
       ( long "show-name-ids"
           <> help "[DEV] Show the unique number of each identifier when pretty printing"
       )
-  _globalNewTypecheckingAlgorithm <-
-    switch
-      ( long "new-typechecker"
-          <> help "[DEV] Use the new experimental typechecker"
-      )
   return GlobalOptions {..}
 
 parseBuildDir :: Mod OptionFields (Prepath Dir) -> Parser (AppPath Dir)
@@ -165,8 +158,7 @@ entryPointFromGlobalOptions root mainFile opts = do
         _entryPointUnrollLimit = opts ^. globalUnrollLimit,
         _entryPointGenericOptions = project opts,
         _entryPointBuildDir = maybe (def ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir,
-        _entryPointOffline = opts ^. globalOffline,
-        _entryPointNewTypeCheckingAlgorithm = opts ^. globalNewTypecheckingAlgorithm
+        _entryPointOffline = opts ^. globalOffline
       }
   where
     optBuildDir :: Maybe (Prepath Dir)

src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs

@@ -18,7 +18,6 @@ import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Print
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoped
 import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as InternalArity
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qualified as InternalTyped
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
 import Juvix.Compiler.Pipeline.EntryPoint
@@ -166,8 +165,7 @@ genJudocHtml JudocArgs {..} =
     cs :: Comments
     cs =
       _judocArgsCtx
-        ^. resultInternalArityResult
-          . InternalArity.resultInternalResult
+        ^. resultInternalResult
           . Internal.resultScoper
           . Scoped.comments
 
@@ -180,8 +178,7 @@ genJudocHtml JudocArgs {..} =
     mainMod :: Module 'Scoped 'ModuleTop
     mainMod =
       _judocArgsCtx
-        ^. InternalTyped.resultInternalArityResult
-          . InternalArity.resultInternalResult
+        ^. InternalTyped.resultInternalResult
           . Internal.resultScoper
           . Scoped.mainModule
 

src/Juvix/Compiler/Internal/Pretty/Base.hs

@@ -11,10 +11,8 @@ import Juvix.Compiler.Internal.Data.InstanceInfo (instanceInfoResult, instanceTa
 import Juvix.Compiler.Internal.Data.LocalVars
 import Juvix.Compiler.Internal.Data.NameDependencyInfo
 import Juvix.Compiler.Internal.Data.TypedHole
-import Juvix.Compiler.Internal.Extra.Base
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Pretty.Options
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types (Arity)
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity qualified as New
 import Juvix.Data.CodeAnn
 import Juvix.Prelude
@@ -113,13 +111,6 @@ ppMutual l = do
       return (braces (line <> indent' b' <> line))
   return (kwMutual <+> defs')
 
-instance PrettyCode Arity where
-  ppCode = return . pretty
-
-instance PrettyCode ApplicationArg where
-  ppCode ApplicationArg {..} =
-    implicitDelim _appArgIsImplicit <$> ppCode _appArg
-
 instance PrettyCode LetClause where
   ppCode :: forall r. (Member (Reader Options) r) => LetClause -> Sem r (Doc Ann)
   ppCode = \case

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -503,19 +503,6 @@ goInductiveParameters ::
   Sem r [Internal.InductiveParameter]
 goInductiveParameters params@InductiveParameters {..} = do
   paramType' <- goRhs _inductiveParametersRhs
-  newAlgo <- asks (^. entryPointNewTypeCheckingAlgorithm)
-  case paramType' of
-    Internal.ExpressionUniverse {} -> return ()
-    Internal.ExpressionHole {} -> return ()
-    _ ->
-      unless newAlgo
-        . throw
-        $ ErrUnsupported
-          Unsupported
-            { _unsupportedMsg = "only type variables of small types are allowed",
-              _unsupportedLoc = getLoc params
-            }
-
   let goInductiveParameter :: S.Symbol -> Internal.InductiveParameter
       goInductiveParameter var =
         Internal.InductiveParameter

src/Juvix/Compiler/Internal/Translation/FromInternal.hs

@@ -1,12 +1,9 @@
 module Juvix.Compiler.Internal.Translation.FromInternal
   ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability,
-    arityChecking,
     typeChecking,
     typeCheckingNew,
     typeCheckExpression,
     typeCheckExpressionType,
-    arityCheckExpression,
-    arityCheckImport,
     typeCheckImport,
   )
 where
@@ -17,60 +14,14 @@ import Juvix.Compiler.Concrete.Data.Highlight.Input
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Pretty
 import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context as Internal
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as ArityChecking
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context (InternalArityResult (InternalArityResult))
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking
-import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew qualified as New
 import Juvix.Compiler.Pipeline.Artifacts
 import Juvix.Compiler.Pipeline.EntryPoint
 import Juvix.Data.Effect.NameIdGen
 import Juvix.Prelude hiding (fromEither)
 
-arityChecking ::
-  (Members '[Error JuvixError, NameIdGen] r) =>
-  InternalResult ->
-  Sem r ArityChecking.InternalArityResult
-arityChecking res@InternalResult {..} =
-  mapError (JuvixError @ArityChecking.ArityCheckerError) $ do
-    r <-
-      runReader table
-        . evalCacheEmpty ArityChecking.checkModuleIndexNoCache
-        $ mapM ArityChecking.checkModule _resultModules
-    return
-      ArityChecking.InternalArityResult
-        { _resultInternalResult = res,
-          _resultModules = r
-        }
-  where
-    table :: InfoTable
-    table = buildTable _resultModules
-
-arityCheckExpression ::
-  (Members '[Error JuvixError, State Artifacts] r) =>
-  Expression ->
-  Sem r Expression
-arityCheckExpression exp = do
-  table <- extendedTableReplArtifacts exp
-  mapError (JuvixError @ArityChecking.ArityCheckerError)
-    . runReader table
-    . runNameIdGenArtifacts
-    $ ArityChecking.inferReplExpression exp
-
-arityCheckImport ::
-  (Members '[Error JuvixError, State Artifacts] r) =>
-  Import ->
-  Sem r Import
-arityCheckImport i = do
-  artiTable <- gets (^. artifactInternalTypedTable)
-  let table = buildTable [i ^. importModule . moduleIxModule] <> artiTable
-  mapError (JuvixError @ArityChecking.ArityCheckerError)
-    . runReader table
-    . runNameIdGenArtifacts
-    . evalCacheEmpty ArityChecking.checkModuleIndexNoCache
-    $ ArityChecking.checkImport i
-
 typeCheckExpressionType ::
   forall r.
   (Members '[Error JuvixError, State Artifacts, Termination] r) =>
@@ -85,7 +36,8 @@ typeCheckExpressionType exp = do
     . runNameIdGenArtifacts
     . runReader table
     . ignoreOutput @Example
-    . withEmptyVars
+    . withEmptyLocalVars
+    . withEmptyInsertedArgsStack
     . mapError (JuvixError @TypeCheckerError)
     . runInferenceDef
     $ inferExpression Nothing exp
@@ -113,24 +65,24 @@ typeCheckImport i = do
     . runNameIdGenArtifacts
     . ignoreOutput @Example
     . runReader table
-    . withEmptyVars
+    . withEmptyLocalVars
     -- TODO Store cache in Artifacts and use it here
     . evalCacheEmpty checkModuleNoCache
     $ checkTable >> checkImport i
 
 typeChecking ::
   forall r.
   (Members '[HighlightBuilder, Error JuvixError, Builtins, NameIdGen] r) =>
-  Sem (Termination ': r) ArityChecking.InternalArityResult ->
+  Sem (Termination ': r) Internal.InternalResult ->
   Sem r InternalTypedResult
 typeChecking a = do
   (termin, (res, table, (normalized, (idens, (funs, r))))) <- runTermination iniTerminationState $ do
     res <- a
     let table :: InfoTable
-        table = buildTable (res ^. ArityChecking.resultModules)
+        table = buildTable (res ^. Internal.resultModules)
 
         entryPoint :: EntryPoint
-        entryPoint = res ^. ArityChecking.internalArityResultEntryPoint
+        entryPoint = res ^. Internal.internalResultEntryPoint
     fmap (res,table,)
       . runOutputList
       . runReader entryPoint
@@ -139,10 +91,10 @@ typeChecking a = do
       . runReader table
       . mapError (JuvixError @TypeCheckerError)
       . evalCacheEmpty checkModuleNoCache
-      $ checkTable >> mapM checkModule (res ^. ArityChecking.resultModules)
+      $ checkTable >> mapM checkModule (res ^. Internal.resultModules)
   return
     InternalTypedResult
-      { _resultInternalArityResult = res,
+      { _resultInternalResult = res,
         _resultModules = r,
         _resultTermination = termin,
         _resultNormalized = HashMap.fromList [(e ^. exampleId, e ^. exampleExpression) | e <- normalized],
@@ -171,17 +123,11 @@ typeCheckingNew a = do
       . runState (mempty :: FunctionsTable)
       . runReader table
       . mapError (JuvixError @TypeCheckerError)
-      . evalCacheEmpty New.checkModuleNoCache
-      $ checkTable >> mapM New.checkModule (res ^. Internal.resultModules)
-  let ariRes :: InternalArityResult
-      ariRes =
-        InternalArityResult
-          { _resultInternalResult = res,
-            _resultModules = res ^. Internal.resultModules
-          }
+      . evalCacheEmpty checkModuleNoCache
+      $ checkTable >> mapM checkModule (res ^. Internal.resultModules)
   return
     InternalTypedResult
-      { _resultInternalArityResult = ariRes,
+      { _resultInternalResult = res,
         _resultModules = r,
         _resultTermination = termin,
         _resultNormalized = HashMap.fromList [(e ^. exampleId, e ^. exampleExpression) | e <- normalized],