Remove old typechecker

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/Data/InfoTable.hs

@@ -4,6 +4,7 @@ module Juvix.Compiler.Internal.Data.InfoTable
     extendWithReplExpression,
     lookupConstructor,
     lookupConstructorArgTypes,
+    lookupFunctionMaybe,
     lookupFunction,
     lookupConstructorReturnType,
     lookupInductive,
@@ -169,7 +170,7 @@ lookupConstructor f = do
         $ "impossible: "
           <> ppTrace f
           <> " is not in the InfoTable\n"
-          <> "The registered constructors are: "
+          <> "\nThe registered constructors are: "
           <> ppTrace (HashMap.keys tbl)
 
 lookupConstructorArgTypes :: (Member (Reader InfoTable) r) => Name -> Sem r ([InductiveParameter], [Expression])
@@ -188,13 +189,16 @@ lookupInductive f = do
         $ "impossible: "
           <> ppTrace f
           <> " is not in the InfoTable\n"
-          <> "The registered inductives are: "
+          <> "\nThe registered inductives are: "
           <> ppTrace (HashMap.keys tbl)
 
+lookupFunctionMaybe :: forall r. (Member (Reader InfoTable) r) => Name -> Sem r (Maybe FunctionInfo)
+lookupFunctionMaybe f = HashMap.lookup f <$> asks (^. infoFunctions)
+
 lookupFunction :: forall r. (Member (Reader InfoTable) r) => Name -> Sem r FunctionInfo
 lookupFunction f = do
   err <- impossibleErr
-  HashMap.lookupDefault err f <$> asks (^. infoFunctions)
+  fromMaybe err <$> lookupFunctionMaybe f
   where
     impossibleErr :: Sem r a
     impossibleErr = do
@@ -205,7 +209,7 @@ lookupFunction f = do
           <> ppTrace f
           <> " is not in the InfoTable\n"
           <> ppTrace (getLoc f)
-          <> "The registered functions are: "
+          <> "\nThe registered functions are: "
           <> ppTrace (HashMap.keys tbl)
 
 lookupAxiom :: (Member (Reader InfoTable) r) => Name -> Sem r AxiomInfo

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

@@ -12,8 +12,6 @@ type Rename = HashMap VarName VarName
 
 type Subs = HashMap VarName Expression
 
-type VarMap = HashMap VarName VarName
-
 data ApplicationArg = ApplicationArg
   { _appArgIsImplicit :: IsImplicit,
     _appArg :: Expression
@@ -126,16 +124,33 @@ instance HasExpressions SimpleLambda where
     pure (SimpleLambda bi' b')
 
 instance HasExpressions FunctionParameter where
-  leafExpressions f (FunctionParameter m i e) = do
-    e' <- leafExpressions f e
-    pure (FunctionParameter m i e')
+  leafExpressions f FunctionParameter {..} = do
+    ty' <- leafExpressions f _paramType
+    pure
+      FunctionParameter
+        { _paramType = ty',
+          _paramName,
+          _paramImplicit
+        }
 
 instance HasExpressions Function where
   leafExpressions f (Function l r) = do
     l' <- leafExpressions f l
     r' <- leafExpressions f r
     pure (Function l' r')
 
+instance HasExpressions ApplicationArg where
+  leafExpressions f ApplicationArg {..} = do
+    arg' <- leafExpressions f _appArg
+    pure
+      ApplicationArg
+        { _appArg = arg',
+          _appArgIsImplicit
+        }
+
+instance (HasExpressions a) => HasExpressions (Maybe a) where
+  leafExpressions = _Just . leafExpressions
+
 instance HasExpressions Application where
   leafExpressions f (Application l r i) = do
     l' <- leafExpressions f l
@@ -292,16 +307,24 @@ inductiveTypeVarsAssoc def l
     vars :: [VarName]
     vars = def ^.. inductiveParameters . each . inductiveParamName
 
-substitutionApp :: forall r expr. (Member NameIdGen r, HasExpressions expr) => (Maybe Name, Expression) -> expr -> Sem r expr
+substitutionApp :: (Maybe Name, Expression) -> Subs
 substitutionApp (mv, ty) = case mv of
-  Nothing -> return
-  Just v -> substitutionE (HashMap.singleton v ty)
+  Nothing -> mempty
+  Just v -> HashMap.singleton v ty
 
 localsToSubsE :: LocalVars -> Subs
 localsToSubsE l = ExpressionIden . IdenVar <$> l ^. localTyMap
 
+subsKind :: [Name] -> NameKind -> Subs
+subsKind uids k =
+  HashMap.fromList
+    [ (s, toExpression s') | s <- uids, let s' = toExpression (set nameKind k s)
+    ]
+
 substitutionE :: forall r expr. (Member NameIdGen r, HasExpressions expr) => Subs -> expr -> Sem r expr
-substitutionE m = leafExpressions goLeaf
+substitutionE m
+  | null m = pure
+  | otherwise = leafExpressions goLeaf
   where
     goLeaf :: Expression -> Sem r Expression
     goLeaf = \case
@@ -382,6 +405,7 @@ foldApplication f args = case nonEmpty args of
 unfoldApplication' :: Application -> (Expression, NonEmpty ApplicationArg)
 unfoldApplication' (Application l' r' i') = second (|: (ApplicationArg i' r')) (unfoldExpressionApp l')
 
+-- TODO make it tail recursive
 unfoldExpressionApp :: Expression -> (Expression, [ApplicationArg])
 unfoldExpressionApp = \case
   ExpressionApplication (Application l r i) ->

src/Juvix/Compiler/Internal/Language.hs

@@ -391,7 +391,7 @@ instance HasAtomicity SimpleLambda where
   atomicity = const Atom
 
 instance HasAtomicity Let where
-  atomicity l = atomicity (l ^. letExpression)
+  atomicity = const (Aggregate letFixity)
 
 instance HasAtomicity Literal where
   atomicity = \case

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