Refactor Core datastructures (#1975)

* Closes #1972 * Introduces lookup functions for the InfoTable to avoid using HashMap explicitly and reduce code duplication
2024-11-24 08:45:51 +03:00 · 2023-04-04 18:58:05 +02:00 · 2023-04-04 18:58:05 +02:00 · 6d83ba597f
commit 6d83ba597f
parent 75d25a56bb
38 changed files with 172 additions and 225 deletions
--- a/app/AsmInterpreter.hs
+++ b/app/AsmInterpreter.hs
@ -17,7 +17,7 @@ runAsm bValidate tab =
        Nothing ->
          case tab ^. Asm.infoMainFunction of
            Just sym -> do
-              r <- doRun tab (Asm.getFunInfo tab sym)
+              r <- doRun tab (Asm.lookupFunInfo tab sym)
              case r of
                Left err ->
                  exitJuvixError (JuvixError err)
--- a/app/Commands/Repl.hs
+++ b/app/Commands/Repl.hs
@ -6,7 +6,6 @@ import Commands.Base hiding (command)
 import Commands.Repl.Options
 import Control.Exception (throwIO)
 import Control.Monad.State.Strict qualified as State
-import Data.HashMap.Strict qualified as HashMap
 import Data.String.Interpolate (i, __i)
 import Evaluator
 import Juvix.Compiler.Concrete.Data.Scope (scopePath)
@ -376,7 +375,6 @@ runTransformations shouldDisambiguate ts n = runCoreInfoTableBuilderArtifacts $
                _identifierSymbol = sym,
                _identifierLocation = Nothing,
                _identifierArgsNum = 0,
-                _identifierArgsInfo = [],
                _identifierType = Core.mkDynamic',
                _identifierIsExported = False,
                _identifierBuiltin = Nothing
@ -395,4 +393,4 @@ runTransformations shouldDisambiguate ts n = runCoreInfoTableBuilderArtifacts $
      Core.setInfoTable tab''

    getNode :: Core.Symbol -> Sem (Core.InfoTableBuilder ': r) Core.Node
-    getNode sym = HashMap.lookupDefault impossible sym . (^. Core.identContext) <$> Core.getInfoTable
+    getNode sym = fromMaybe impossible . flip Core.lookupIdentifierNode' sym <$> Core.getInfoTable
--- a/src/Juvix/Compiler/Asm/Data/InfoTable.hs
+++ b/src/Juvix/Compiler/Asm/Data/InfoTable.hs
@ -5,6 +5,7 @@ module Juvix.Compiler.Asm.Data.InfoTable
  )
 where

+import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Asm.Language
 import Juvix.Compiler.Asm.Language.Rep
 import Juvix.Compiler.Asm.Language.Type
@ -50,7 +51,7 @@ data InductiveInfo = InductiveInfo
    _inductiveLocation :: Maybe Location,
    _inductiveSymbol :: Symbol,
    _inductiveKind :: Type,
-    _inductiveConstructors :: [ConstructorInfo],
+    _inductiveConstructors :: [Tag],
    _inductiveRepresentation :: IndRep
  }

@ -67,3 +68,12 @@ emptyInfoTable =
      _infoInductives = mempty,
      _infoMainFunction = Nothing
    }
+
+lookupFunInfo :: InfoTable -> Symbol -> FunctionInfo
+lookupFunInfo infoTable sym = fromMaybe (error "invalid function symbol") (HashMap.lookup sym (infoTable ^. infoFunctions))
+
+lookupConstrInfo :: InfoTable -> Tag -> ConstructorInfo
+lookupConstrInfo infoTable tag = fromMaybe (error "invalid constructor tag") (HashMap.lookup tag (infoTable ^. infoConstrs))
+
+lookupInductiveInfo :: InfoTable -> Symbol -> InductiveInfo
+lookupInductiveInfo infoTable sym = fromMaybe (error "invalid inductive symbol") (HashMap.lookup sym (infoTable ^. infoInductives))
--- a/src/Juvix/Compiler/Asm/Data/InfoTableBuilder.hs
+++ b/src/Juvix/Compiler/Asm/Data/InfoTableBuilder.hs
@ -2,7 +2,6 @@ module Juvix.Compiler.Asm.Data.InfoTableBuilder where

 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Asm.Data.InfoTable
-import Juvix.Compiler.Asm.Extra.Base
 import Juvix.Compiler.Asm.Language

 data IdentKind
@ -76,4 +75,4 @@ runInfoTableBuilder =
        return $ HashMap.lookup txt (s ^. stateIdents)
      GetFunctionInfo sym -> do
        s <- get
-        return (getFunInfo (s ^. stateInfoTable) sym)
+        return (lookupFunInfo (s ^. stateInfoTable) sym)
--- a/src/Juvix/Compiler/Asm/Extra/Base.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Base.hs
@ -1,6 +1,5 @@
 module Juvix.Compiler.Asm.Extra.Base where

-import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Language

@ -16,15 +15,6 @@ mkInstr' loc = Instr . CmdInstr (CommandInfo loc)
 mkBinop' :: Maybe Location -> Opcode -> Command
 mkBinop' loc = mkInstr' loc . Binop

-getFunInfo :: InfoTable -> Symbol -> FunctionInfo
-getFunInfo infoTable sym = fromMaybe (error "invalid function symbol") (HashMap.lookup sym (infoTable ^. infoFunctions))
-
-getConstrInfo :: InfoTable -> Tag -> ConstructorInfo
-getConstrInfo infoTable tag = fromMaybe (error "invalid constructor tag") (HashMap.lookup tag (infoTable ^. infoConstrs))
-
-getInductiveInfo :: InfoTable -> Symbol -> InductiveInfo
-getInductiveInfo infoTable sym = fromMaybe (error "invalid inductive symbol") (HashMap.lookup sym (infoTable ^. infoInductives))
-
 isFinalInstr :: Instruction -> Bool
 isFinalInstr = \case
  Return -> True
--- a/src/Juvix/Compiler/Asm/Extra/Memory.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Memory.hs
@ -5,7 +5,6 @@ import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Data.Stack (Stack)
 import Juvix.Compiler.Asm.Data.Stack qualified as Stack
 import Juvix.Compiler.Asm.Error
-import Juvix.Compiler.Asm.Extra.Base
 import Juvix.Compiler.Asm.Extra.Type
 import Juvix.Compiler.Asm.Language
 import Juvix.Compiler.Asm.Pretty
@ -91,7 +90,7 @@ getMemValueType :: InfoTable -> MemValue -> Memory -> Maybe Type
 getMemValueType tab val mem = case val of
  DRef dr -> getDirectRefType dr mem
  ConstrRef fld ->
-    let ci = getConstrInfo tab (fld ^. fieldTag)
+    let ci = lookupConstrInfo tab (fld ^. fieldTag)
        tyargs = typeArgs (ci ^. constructorType)
     in atMay tyargs (fld ^. fieldOffset)

--- a/src/Juvix/Compiler/Asm/Extra/Recursors.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Recursors.hs
@ -123,7 +123,7 @@ recurse' sig = go True
            Prealloc {} ->
              return mem
            AllocConstr tag -> do
-              let ci = getConstrInfo (sig ^. recursorInfoTable) tag
+              let ci = lookupConstrInfo (sig ^. recursorInfoTable) tag
                  n = ci ^. constructorArgsNum
                  tyargs = typeArgs (ci ^. constructorType)
              checkValueStack' loc (sig ^. recursorInfoTable) tyargs mem
@ -136,7 +136,7 @@ recurse' sig = go True
                pushValueStack (mkTypeConstr (ci ^. constructorInductive) tag tys) $
                  popValueStack n mem
            AllocClosure InstrAllocClosure {..} -> do
-              let fi = getFunInfo (sig ^. recursorInfoTable) _allocClosureFunSymbol
+              let fi = lookupFunInfo (sig ^. recursorInfoTable) _allocClosureFunSymbol
                  (tyargs, tgt) = unfoldType (fi ^. functionType)
              checkValueStack' loc (sig ^. recursorInfoTable) (take _allocClosureArgsNum tyargs) mem
              return $
@ -183,10 +183,10 @@ recurse' sig = go True
              AsmError loc "invalid call: not enough values on the stack"
          let ty = case _callType of
                CallClosure -> topValueStack' 0 mem
-                CallFun sym -> getFunInfo (sig ^. recursorInfoTable) sym ^. functionType
+                CallFun sym -> lookupFunInfo (sig ^. recursorInfoTable) sym ^. functionType
          let argsNum = case _callType of
                CallClosure -> length (typeArgs ty)
-                CallFun sym -> getFunInfo (sig ^. recursorInfoTable) sym ^. functionArgsNum
+                CallFun sym -> lookupFunInfo (sig ^. recursorInfoTable) sym ^. functionArgsNum
          when (argsNum /= 0) $
            checkFunType ty
          when (ty /= TyDynamic && argsNum /= _callArgsNum) $
@ -375,7 +375,7 @@ recurseS' sig = go
            Prealloc {} ->
              return si
            AllocConstr tag -> do
-              let ci = getConstrInfo (sig ^. recursorInfoTable) tag
+              let ci = lookupConstrInfo (sig ^. recursorInfoTable) tag
                  n = ci ^. constructorArgsNum
              return $
                stackInfoPopValueStack (n - 1) si
--- a/src/Juvix/Compiler/Asm/Interpreter.hs
+++ b/src/Juvix/Compiler/Asm/Interpreter.hs
@ -128,7 +128,7 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
      Prealloc {} ->
        goCode cont
      AllocConstr tag -> do
-        let ci = getConstrInfo infoTable tag
+        let ci = lookupConstrInfo infoTable tag
        args <- replicateM (ci ^. constructorArgsNum) popValueStack
        pushValueStack (ValConstr (Constr tag args))
        goCode cont
@ -240,7 +240,7 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
    getCallDetails :: (Member Runtime r) => Maybe Location -> InstrCall -> Sem r (Code, Frame)
    getCallDetails loc InstrCall {..} = case _callType of
      CallFun sym -> do
-        let fi = getFunInfo infoTable sym
+        let fi = lookupFunInfo infoTable sym
        when
          (_callArgsNum /= fi ^. functionArgsNum)
          (runtimeError "invalid direct call: supplied arguments number not equal to expected arguments number")
@ -250,7 +250,7 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
        v <- popValueStack
        case v of
          ValClosure cl -> do
-            let fi = getFunInfo infoTable (cl ^. closureSymbol)
+            let fi = lookupFunInfo infoTable (cl ^. closureSymbol)
                n = length (cl ^. closureArgs)
            when
              (n >= fi ^. functionArgsNum)
@ -283,7 +283,7 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
      v <- popValueStack
      case v of
        ValClosure cl -> do
-          let fi = getFunInfo infoTable (cl ^. closureSymbol)
+          let fi = lookupFunInfo infoTable (cl ^. closureSymbol)
          let n = fi ^. functionArgsNum - length (cl ^. closureArgs)
          when
            (n < 0)
--- a/src/Juvix/Compiler/Asm/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Asm/Pretty/Base.hs
@ -10,7 +10,6 @@ import Data.List.NonEmpty qualified as NonEmpty
 import Data.Text qualified as Text
 import Juvix.Compiler.Abstract.Data.Name
 import Juvix.Compiler.Asm.Data.InfoTable
-import Juvix.Compiler.Asm.Extra.Base
 import Juvix.Compiler.Asm.Interpreter.Base
 import Juvix.Compiler.Asm.Interpreter.RuntimeState
 import Juvix.Compiler.Asm.Pretty.Options
@ -162,7 +161,7 @@ instance PrettyCode TypeInductive where
  ppCode :: (Member (Reader Options) r) => TypeInductive -> Sem r (Doc Ann)
  ppCode TypeInductive {..} = do
    opts <- ask
-    let ii = getInductiveInfo (opts ^. optInfoTable) _typeInductiveSymbol
+    let ii = lookupInductiveInfo (opts ^. optInfoTable) _typeInductiveSymbol
    return $ annotate (AnnKind KNameInductive) (pretty (ii ^. inductiveName))

 instance PrettyCode TypeConstr where
@ -170,9 +169,9 @@ instance PrettyCode TypeConstr where
  ppCode TypeConstr {..} = do
    opts <- ask
    let tab = opts ^. optInfoTable
-    let ii = getInductiveInfo tab _typeConstrInductive
+    let ii = lookupInductiveInfo tab _typeConstrInductive
    let iname = annotate (AnnKind KNameInductive) (pretty (ii ^. inductiveName))
-    let ci = getConstrInfo tab _typeConstrTag
+    let ci = lookupConstrInfo tab _typeConstrTag
    let cname = annotate (AnnKind KNameConstructor) (pretty (ci ^. constructorName))
    args <- mapM ppCode _typeConstrFields
    return $ iname <> kwColon <> cname <> encloseSep "(" ")" ", " args
@ -373,14 +372,14 @@ instance PrettyCode ConstructorInfo where
    ty <- ppCode _constructorType
    return $ annotate (AnnKind KNameConstructor) (pretty (quoteAsmName _constructorName)) <+> colon <+> ty

-instance PrettyCode InductiveInfo where
-  ppCode InductiveInfo {..} = do
-    ctrs <- mapM ppCode _inductiveConstructors
-    return $ kwInductive <+> annotate (AnnKind KNameInductive) (pretty (quoteAsmName _inductiveName)) <+> braces' (vcat (map (<> semi) ctrs))
+ppInductive :: Member (Reader Options) r => InfoTable -> InductiveInfo -> Sem r (Doc Ann)
+ppInductive tab InductiveInfo {..} = do
+  ctrs <- mapM (ppCode . lookupConstrInfo tab) _inductiveConstructors
+  return $ kwInductive <+> annotate (AnnKind KNameInductive) (pretty (quoteAsmName _inductiveName)) <+> braces' (vcat (map (<> semi) ctrs))

 instance PrettyCode InfoTable where
-  ppCode InfoTable {..} = do
-    inds <- mapM ppCode (HashMap.elems (filterOutBuiltins _infoInductives))
+  ppCode tab@InfoTable {..} = do
+    inds <- mapM (ppInductive tab) (HashMap.elems (filterOutBuiltins _infoInductives))
    funsigs <- mapM ppFunSig (HashMap.elems _infoFunctions)
    funs <- mapM ppCode (HashMap.elems _infoFunctions)
    return $ vcat (map (<> line) inds) <> line <> vcat funsigs <> line <> line <> vcat (map (<> line) funs)
@ -389,9 +388,8 @@ instance PrettyCode InfoTable where
      filterOutBuiltins =
        HashMap.filter
          ( \ii -> case ii ^. inductiveConstructors of
-              ci : _ -> case ci ^. constructorTag of
-                BuiltinTag _ -> False
-                UserTag _ -> True
+              BuiltinTag _ : _ -> False
+              UserTag _ : _ -> True
              [] -> True
          )

--- a/src/Juvix/Compiler/Asm/Transformation/Prealloc.hs
+++ b/src/Juvix/Compiler/Asm/Transformation/Prealloc.hs
@ -24,7 +24,7 @@ computeCodePrealloc tab code = prealloc <$> foldS sig code (0, [])
      AllocConstr tag ->
        return (k + size, cmd : c)
        where
-          ci = getConstrInfo tab tag
+          ci = lookupConstrInfo tab tag
          size = getConstrSize (ci ^. constructorRepresentation) (ci ^. constructorArgsNum)
      AllocClosure InstrAllocClosure {..} -> do
        opts <- ask
@ -106,7 +106,7 @@ checkCodePrealloc tab code = do
      AllocConstr tag ->
        return $ \k -> cont (k - size)
        where
-          ci = getConstrInfo tab tag
+          ci = lookupConstrInfo tab tag
          size = getConstrSize (ci ^. constructorRepresentation) (ci ^. constructorArgsNum)
      AllocClosure InstrAllocClosure {..} -> do
        opts <- ask
--- a/src/Juvix/Compiler/Asm/Translation/FromCore.hs
+++ b/src/Juvix/Compiler/Asm/Translation/FromCore.hs
@ -316,7 +316,7 @@ translateInductiveInfo ii =
      _inductiveLocation = ii ^. Core.inductiveLocation,
      _inductiveSymbol = ii ^. Core.inductiveSymbol,
      _inductiveKind = convertType 0 (ii ^. Core.inductiveKind),
-      _inductiveConstructors = map translateConstructorInfo (ii ^. Core.inductiveConstructors),
+      _inductiveConstructors = ii ^. Core.inductiveConstructors,
      _inductiveRepresentation = IndRepStandard
    }

--- a/src/Juvix/Compiler/Asm/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Asm/Translation/FromSource.hs
@ -65,7 +65,7 @@ declareBuiltins = do
            _inductiveSymbol = sym,
            _inductiveLocation = Just i,
            _inductiveKind = TyDynamic,
-            _inductiveConstructors = constrs,
+            _inductiveConstructors = map (^. constructorTag) constrs,
            _inductiveRepresentation = IndRepStandard
          }
      )
@ -155,7 +155,7 @@ statementInductive = do
          }
  lift $ registerInductive ii
  ctrs <- braces $ P.sepEndBy (constrDecl sym) (kw kwSemicolon)
-  lift $ registerInductive ii {_inductiveConstructors = ctrs}
+  lift $ registerInductive ii {_inductiveConstructors = map (^. constructorTag) ctrs}

 functionArguments ::
  (Member InfoTableBuilder r) =>
--- a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs
+++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs
@ -57,9 +57,9 @@ withSymbol sym a = do
 fromCore :: Core.InfoTable -> (Morphism, Object)
 fromCore tab = case tab ^. Core.infoMain of
  Just sym ->
-    let node = fromJust $ HashMap.lookup sym (tab ^. Core.identContext)
+    let node = Core.lookupIdentifierNode tab sym
        syms = reverse $ filter (/= sym) $ Core.createIdentDependencyInfo tab ^. Core.depInfoTopSort
-        idents = map (\s -> fromJust $ HashMap.lookup s (tab ^. Core.infoIdentifiers)) syms
+        idents = map (Core.lookupIdentifierInfo tab) syms
        morph = run . runReader emptyEnv $ goIdents node idents
        obj = convertType $ Info.getNodeType node
     in (morph, obj)
@ -106,7 +106,7 @@ fromCore tab = case tab ^. Core.infoMain of
              }
        where
          sym = ii ^. Core.identifierSymbol
-          fundef = fromJust $ HashMap.lookup sym (tab ^. Core.identContext)
+          fundef = Core.lookupIdentifierNode tab sym
          argty = convertType (Info.getNodeType fundef)
          mkLambda = do
            body <- withSymbol sym (goIdents node idents)
@ -290,18 +290,15 @@ fromCore tab = case tab ^. Core.infoMain of
        error "constructor tag out of range"
      return $ (constructors !! tagNum) args
      where
-        ci = fromJust $ HashMap.lookup _constrTag (tab ^. Core.infoConstructors)
+        ci = Core.lookupConstructorInfo tab _constrTag
        sym = ci ^. Core.constructorInductive
-        ctrs =
-          fromJust
-            (HashMap.lookup sym (tab ^. Core.infoInductives))
-            ^. Core.inductiveConstructors
+        ctrs = Core.lookupInductiveInfo tab sym ^. Core.inductiveConstructors
        tagNum =
          fromJust
            $ elemIndex
              _constrTag
              . sort
-            $ map (^. Core.constructorTag) ctrs
+            $ ctrs
        constructors = mkConstructors $ convertInductive sym

    mkConstructors :: Object -> [Morphism -> Morphism]
@ -428,7 +425,7 @@ fromCore tab = case tab ^. Core.infoMain of
              go indty val branches
      where
        indty = convertInductive _caseInductive
-        ii = fromJust $ HashMap.lookup _caseInductive (tab ^. Core.infoInductives)
+        ii = Core.lookupInductiveInfo tab _caseInductive
        missingCtrs =
          filter
            ( \x ->
@ -438,7 +435,7 @@ fromCore tab = case tab ^. Core.infoMain of
                      _caseBranches
                  )
            )
-            (ii ^. Core.inductiveConstructors)
+            (map (Core.lookupConstructorInfo tab) (ii ^. Core.inductiveConstructors))
        missingCtrsNum = length missingCtrs
        ctrBrs = map mkCtrBranch missingCtrs
        defaultNode = fromMaybe (error "not all cases covered") _caseDefault
@ -615,10 +612,9 @@ fromCore tab = case tab ^. Core.infoMain of
    convertInductive :: Symbol -> Object
    convertInductive sym = do
      let ctrs =
-            sortOn (^. Core.constructorTag) $
-              fromJust
-                (HashMap.lookup sym (tab ^. Core.infoInductives))
-                ^. Core.inductiveConstructors
+            map (Core.lookupConstructorInfo tab) $
+              sort $
+                Core.lookupInductiveInfo tab sym ^. Core.inductiveConstructors
      case reverse ctrs of
        ci : ctrs' -> do
          foldr
--- a/src/Juvix/Compiler/Core/Data/IdentDependencyInfo.hs
+++ b/src/Juvix/Compiler/Core/Data/IdentDependencyInfo.hs
@ -16,7 +16,7 @@ createIdentDependencyInfo tab = createDependencyInfo graph startVertices
      fmap
        ( \IdentifierInfo {..} ->
            HashSet.map (\Ident {..} -> _identSymbol) $
-              getIdents (fromJust $ HashMap.lookup _identifierSymbol (tab ^. identContext))
+              getIdents (lookupIdentifierNode tab _identifierSymbol)
        )
        (tab ^. infoIdentifiers)

--- a/src/Juvix/Compiler/Core/Data/InfoTable.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTable.hs
@ -58,25 +58,18 @@ data IdentifierInfo = IdentifierInfo
    _identifierLocation :: Maybe Location,
    _identifierSymbol :: Symbol,
    _identifierType :: Type,
+    -- | The number of lambdas in the identifier body
    _identifierArgsNum :: Int,
-    _identifierArgsInfo :: [ArgumentInfo],
    _identifierIsExported :: Bool,
    _identifierBuiltin :: Maybe BuiltinFunction
  }

-data ArgumentInfo = ArgumentInfo
-  { _argumentName :: Text,
-    _argumentLocation :: Maybe Location,
-    _argumentType :: Type,
-    _argumentIsImplicit :: IsImplicit
-  }
-
 data InductiveInfo = InductiveInfo
  { _inductiveName :: Text,
    _inductiveLocation :: Maybe Location,
    _inductiveSymbol :: Symbol,
    _inductiveKind :: Type,
-    _inductiveConstructors :: [ConstructorInfo],
+    _inductiveConstructors :: [Tag],
    _inductiveParams :: [ParameterInfo],
    _inductivePositive :: Bool,
    _inductiveBuiltin :: Maybe BuiltinType
@ -107,12 +100,35 @@ data AxiomInfo = AxiomInfo

 makeLenses ''InfoTable
 makeLenses ''IdentifierInfo
-makeLenses ''ArgumentInfo
 makeLenses ''InductiveInfo
 makeLenses ''ConstructorInfo
 makeLenses ''ParameterInfo
 makeLenses ''AxiomInfo

+lookupInductiveInfo' :: InfoTable -> Symbol -> Maybe InductiveInfo
+lookupInductiveInfo' tab sym = HashMap.lookup sym (tab ^. infoInductives)
+
+lookupConstructorInfo' :: InfoTable -> Tag -> Maybe ConstructorInfo
+lookupConstructorInfo' tab tag = HashMap.lookup tag (tab ^. infoConstructors)
+
+lookupIdentifierInfo' :: InfoTable -> Symbol -> Maybe IdentifierInfo
+lookupIdentifierInfo' tab sym = HashMap.lookup sym (tab ^. infoIdentifiers)
+
+lookupIdentifierNode' :: InfoTable -> Symbol -> Maybe Node
+lookupIdentifierNode' tab sym = HashMap.lookup sym (tab ^. identContext)
+
+lookupInductiveInfo :: InfoTable -> Symbol -> InductiveInfo
+lookupInductiveInfo tab sym = fromJust $ lookupInductiveInfo' tab sym
+
+lookupConstructorInfo :: InfoTable -> Tag -> ConstructorInfo
+lookupConstructorInfo tab tag = fromJust $ lookupConstructorInfo' tab tag
+
+lookupIdentifierInfo :: InfoTable -> Symbol -> IdentifierInfo
+lookupIdentifierInfo tab sym = fromJust $ lookupIdentifierInfo' tab sym
+
+lookupIdentifierNode :: InfoTable -> Symbol -> Node
+lookupIdentifierNode tab sym = fromJust $ lookupIdentifierNode' tab sym
+
 lookupBuiltinInductive :: InfoTable -> BuiltinInductive -> Maybe InductiveInfo
 lookupBuiltinInductive tab b = (HashMap.!) (tab ^. infoInductives) . indSym <$> idenKind
  where
@ -147,10 +163,10 @@ lookupBuiltinFunction tab b = (HashMap.!) (tab ^. infoIdentifiers) . funSym <$>
      _ -> error "core infotable: expected function identifier"

 identName :: InfoTable -> Symbol -> Text
-identName tab sym = fromJust (HashMap.lookup sym (tab ^. infoIdentifiers)) ^. identifierName
+identName tab sym = lookupIdentifierInfo tab sym ^. identifierName

 typeName :: InfoTable -> Symbol -> Text
-typeName tab sym = fromJust (HashMap.lookup sym (tab ^. infoInductives)) ^. inductiveName
+typeName tab sym = lookupInductiveInfo tab sym ^. inductiveName

 identNames :: InfoTable -> HashSet Text
 identNames tab =
--- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
@ -19,7 +19,7 @@ data InfoTableBuilder m a where
  RegisterIdentNode :: Symbol -> Node -> InfoTableBuilder m ()
  RegisterMain :: Symbol -> InfoTableBuilder m ()
  RemoveSymbol :: Symbol -> InfoTableBuilder m ()
-  OverIdentArgsInfo :: Symbol -> ([ArgumentInfo] -> [ArgumentInfo]) -> InfoTableBuilder m ()
+  OverIdentArgs :: Symbol -> ([Binder] -> [Binder]) -> InfoTableBuilder m ()
  GetIdent :: Text -> InfoTableBuilder m (Maybe IdentKind)
  GetInfoTable :: InfoTableBuilder m InfoTable
  SetInfoTable :: InfoTable -> InfoTableBuilder m ()
@ -27,19 +27,13 @@ data InfoTableBuilder m a where
 makeSem ''InfoTableBuilder

 getConstructorInfo :: (Member InfoTableBuilder r) => Tag -> Sem r ConstructorInfo
-getConstructorInfo tag = do
-  tab <- getInfoTable
-  return $ fromJust (HashMap.lookup tag (tab ^. infoConstructors))
+getConstructorInfo tag = flip lookupConstructorInfo tag <$> getInfoTable

 getInductiveInfo :: (Member InfoTableBuilder r) => Symbol -> Sem r InductiveInfo
-getInductiveInfo sym = do
-  tab <- getInfoTable
-  return $ fromJust (HashMap.lookup sym (tab ^. infoInductives))
+getInductiveInfo sym = flip lookupInductiveInfo sym <$> getInfoTable

 getIdentifierInfo :: (Member InfoTableBuilder r) => Symbol -> Sem r IdentifierInfo
-getIdentifierInfo sym = do
-  tab <- getInfoTable
-  return $ fromJust (HashMap.lookup sym (tab ^. infoIdentifiers))
+getIdentifierInfo sym = flip lookupIdentifierInfo sym <$> getInfoTable

 getBoolSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
 getBoolSymbol = do
@ -61,8 +55,8 @@ checkSymbolDefined sym = do
  tab <- getInfoTable
  return $ HashMap.member sym (tab ^. identContext)

-setIdentArgsInfo :: (Member InfoTableBuilder r) => Symbol -> [ArgumentInfo] -> Sem r ()
-setIdentArgsInfo sym = overIdentArgsInfo sym . const
+setIdentArgs :: (Member InfoTableBuilder r) => Symbol -> [Binder] -> Sem r ()
+setIdentArgs sym = overIdentArgs sym . const

 runInfoTableBuilder :: forall r a. InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
 runInfoTableBuilder tab =
@ -112,11 +106,10 @@ runInfoTableBuilder tab =
        modify' (over infoIdentifiers (HashMap.delete sym))
        modify' (over identContext (HashMap.delete sym))
        modify' (over infoInductives (HashMap.delete sym))
-      OverIdentArgsInfo sym f -> do
-        argsInfo <- f <$> gets (^. infoIdentifiers . at sym . _Just . identifierArgsInfo)
-        modify' (set (infoIdentifiers . at sym . _Just . identifierArgsInfo) argsInfo)
-        modify' (set (infoIdentifiers . at sym . _Just . identifierArgsNum) (length argsInfo))
-        modify' (over infoIdentifiers (HashMap.adjust (over identifierType (expandType (map (^. argumentType) argsInfo))) sym))
+      OverIdentArgs sym f -> do
+        args <- f <$> gets (^. identContext . at sym . _Just . to (map (^. piLhsBinder) . fst . unfoldPi))
+        modify' (set (infoIdentifiers . at sym . _Just . identifierArgsNum) (length args))
+        modify' (over infoIdentifiers (HashMap.adjust (over identifierType (expandType args)) sym))
      GetIdent txt -> do
        s <- get
        return $ HashMap.lookup txt (s ^. identMap)
@ -174,7 +167,7 @@ declareInductiveBuiltins indName blt ctrs = do
          _inductiveLocation = Nothing,
          _inductiveSymbol = sym,
          _inductiveKind = mkDynamic',
-          _inductiveConstructors = constrs,
+          _inductiveConstructors = map (^. constructorTag) constrs,
          _inductivePositive = True,
          _inductiveParams = [],
          _inductiveBuiltin = blt
--- a/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs
+++ b/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs
@ -1,5 +1,6 @@
 module Juvix.Compiler.Core.Data.Stripped.InfoTable where

+import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Language.Stripped

 data InfoTable = InfoTable
@ -34,7 +35,7 @@ data InductiveInfo = InductiveInfo
    _inductiveLocation :: Maybe Location,
    _inductiveSymbol :: Symbol,
    _inductiveKind :: Type,
-    _inductiveConstructors :: [ConstructorInfo],
+    _inductiveConstructors :: [Tag],
    _inductiveParams :: [ParameterInfo]
  }

@ -59,3 +60,6 @@ makeLenses ''ArgumentInfo
 makeLenses ''InductiveInfo
 makeLenses ''ConstructorInfo
 makeLenses ''ParameterInfo
+
+lookupConstructorInfo :: InfoTable -> Tag -> ConstructorInfo
+lookupConstructorInfo tab tag = fromJust $ HashMap.lookup tag (tab ^. infoConstructors)
--- a/src/Juvix/Compiler/Core/Data/TypeDependencyInfo.hs
+++ b/src/Juvix/Compiler/Core/Data/TypeDependencyInfo.hs
@ -16,8 +16,8 @@ createTypeDependencyInfo tab = createDependencyInfo graph startVertices
      HashSet.fromList . (^.. inductiveSymbols)
        <$> HashMap.filter (isNothing . (^. inductiveBuiltin)) (tab ^. infoInductives)

-    constructorTypes :: SimpleFold ConstructorInfo Type
-    constructorTypes = constructorType . to typeArgs . each
+    constructorTypes :: SimpleFold Tag Type
+    constructorTypes = to (lookupConstructorInfo tab) . constructorType . to typeArgs . each

    inductiveSymbols :: SimpleFold InductiveInfo Symbol
    inductiveSymbols = inductiveConstructors . each . constructorTypes . nodeInductives
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@ -217,14 +217,14 @@ isInductive _ = False
 -- | `expandType argtys ty` expands the dynamic target of `ty` to match the
 -- number of arguments with types specified by `argstys`. For example,
 -- `expandType [int, string] (int -> any) = int -> string -> any`.
-expandType :: [Type] -> Type -> Type
+expandType :: [Binder] -> Type -> Type
 expandType argtys ty =
  let (tyargs, target) = unfoldPi ty
   in if
          | length tyargs >= length argtys ->
              ty
          | isDynamic target ->
-              rePis tyargs (mkPis' (drop (length tyargs) argtys) target)
+              rePis tyargs (mkPis (drop (length tyargs) argtys) target)
          | otherwise ->
              impossible

--- a/src/Juvix/Compiler/Core/Extra/Utils.hs
+++ b/src/Juvix/Compiler/Core/Extra/Utils.hs
@ -36,7 +36,7 @@ isTypeConstr tab ty = case typeTarget ty of
  NUniv {} ->
    True
  NIdt Ident {..} ->
-    isTypeConstr tab (fromJust $ HashMap.lookup _identSymbol (tab ^. identContext))
+    isTypeConstr tab (lookupIdentifierNode tab _identSymbol)
  _ -> False

 getTypeParams :: InfoTable -> Type -> [Type]
@ -245,23 +245,6 @@ squashApps = dmap go
            NTyp (TypeConstr i sym args') -> mkTypeConstr i sym (args' ++ args)
            _ -> n

-binderFromArgumentInfo :: ArgumentInfo -> Binder
-binderFromArgumentInfo a =
-  Binder
-    { _binderName = a ^. argumentName,
-      _binderLocation = a ^. argumentLocation,
-      _binderType = a ^. argumentType
-    }
-
-argumentInfoFromBinder :: Binder -> ArgumentInfo
-argumentInfoFromBinder i =
-  ArgumentInfo
-    { _argumentName = i ^. binderName,
-      _argumentLocation = i ^. binderLocation,
-      _argumentType = i ^. binderType,
-      _argumentIsImplicit = Explicit
-    }
-
 patternType :: Pattern -> Node
 patternType = \case
  PatWildcard w -> w ^. patternWildcardBinder . binderType
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@ -427,7 +427,7 @@ instance PrettyCode InfoTable where
    tys <- ppInductives (toList (tbl ^. infoInductives))
    sigs <- ppSigs (sortOn (^. identifierSymbol) $ toList (tbl ^. infoIdentifiers))
    ctx' <- ppContext (tbl ^. identContext)
-    main <- maybe (return "") (\s -> (<> line) . (line <>) <$> ppName KNameFunction (fromJust (HashMap.lookup s (tbl ^. infoIdentifiers)) ^. identifierName)) (tbl ^. infoMain)
+    main <- maybe (return "") (\s -> (<> line) . (line <>) <$> ppName KNameFunction (identName tbl s)) (tbl ^. infoMain)
    return (tys <> line <> line <> sigs <> line <> ctx' <> line <> main)
    where
      ppSig :: Symbol -> Sem r (Maybe (Doc Ann))
@ -439,7 +439,7 @@ instance PrettyCode InfoTable where
        sym' <- ppName KNameFunction mname'
        let -- the identifier may be missing if we have filtered out some
            -- identifiers for printing purposes
-            mii = HashMap.lookup s (tbl ^. infoIdentifiers)
+            mii = lookupIdentifierInfo' tbl s
        case mii of
          Nothing -> return Nothing
          Just ii -> do
@ -481,7 +481,7 @@ instance PrettyCode InfoTable where
          ppInductive :: InductiveInfo -> Sem r (Doc Ann)
          ppInductive ii = do
            name <- ppName KNameInductive (ii ^. inductiveName)
-            ctrs <- mapM (fmap (<> semi) . ppCode) (ii ^. inductiveConstructors)
+            ctrs <- mapM (fmap (<> semi) . ppCode . lookupConstructorInfo tbl) (ii ^. inductiveConstructors)
            return (kwInductive <+> name <+> braces (line <> indent' (vsep ctrs) <> line) <> kwSemicolon)

 instance PrettyCode Stripped.ArgumentInfo where
@ -525,7 +525,7 @@ instance PrettyCode Stripped.InfoTable where
          ppInductive :: Stripped.InductiveInfo -> Sem r (Doc Ann)
          ppInductive ii = do
            name <- ppName KNameInductive (ii ^. Stripped.inductiveName)
-            ctrs <- mapM (fmap (<> semi) . ppCode) (ii ^. Stripped.inductiveConstructors)
+            ctrs <- mapM (fmap (<> semi) . ppCode . Stripped.lookupConstructorInfo tbl) (ii ^. Stripped.inductiveConstructors)
            return (kwInductive <+> name <+> braces (line <> indent' (vsep ctrs) <> line))

 instance (PrettyCode a) => PrettyCode (NonEmpty a) where
--- a/src/Juvix/Compiler/Core/Transformation/Base.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Base.hs
@ -31,7 +31,6 @@ mapAllNodesM f tab =
    >>= mapAxiomsM (overM axiomType f)
    >>= mapConstructorsM (overM constructorType f)
    >>= mapInductivesM (overM inductiveKind f)
-    >>= mapInductivesM (overM inductiveConstructors (mapM (overM constructorType f)))
    >>= mapIdentsM (overM identifierType f)

 mapIdents :: (IdentifierInfo -> IdentifierInfo) -> InfoTable -> InfoTable
@ -71,8 +70,7 @@ mapAllNodes f tab =
    convertIdent :: IdentifierInfo -> IdentifierInfo
    convertIdent ii =
      ii
-        { _identifierType = f (ii ^. identifierType),
-          _identifierArgsInfo = map (over argumentType f) (ii ^. identifierArgsInfo)
+        { _identifierType = f (ii ^. identifierType)
        }

    convertConstructor :: ConstructorInfo -> ConstructorInfo
@ -82,8 +80,7 @@ mapAllNodes f tab =
    convertInductive ii =
      ii
        { _inductiveKind = f (ii ^. inductiveKind),
-          _inductiveParams = map (over paramKind f) (ii ^. inductiveParams),
-          _inductiveConstructors = map convertConstructor (ii ^. inductiveConstructors)
+          _inductiveParams = map (over paramKind f) (ii ^. inductiveParams)
        }

    convertAxiom :: AxiomInfo -> AxiomInfo
--- a/src/Juvix/Compiler/Core/Transformation/CheckExec.hs
+++ b/src/Juvix/Compiler/Core/Transformation/CheckExec.hs
@ -1,6 +1,5 @@
 module Juvix.Compiler.Core.Transformation.CheckExec where

-import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Error
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Transformation.Base
@ -30,7 +29,7 @@ checkExec tab =
        _ ->
          return tab
      where
-        ii = fromJust $ HashMap.lookup sym (tab ^. infoIdentifiers)
+        ii = lookupIdentifierInfo tab sym
        loc = fromMaybe defaultLoc (ii ^. identifierLocation)

        mockFile :: Path Abs File
--- a/src/Juvix/Compiler/Core/Transformation/CheckGeb.hs
+++ b/src/Juvix/Compiler/Core/Transformation/CheckGeb.hs
@ -1,6 +1,5 @@
 module Juvix.Compiler.Core.Transformation.CheckGeb where

-import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Data.TypeDependencyInfo
 import Juvix.Compiler.Core.Error
 import Juvix.Compiler.Core.Extra
@ -22,7 +21,7 @@ checkGeb tab =
        go :: Node -> Sem r Node
        go node = case node of
          NIdt Ident {..}
-            | isDynamic (fromJust (HashMap.lookup _identSymbol (tab ^. infoIdentifiers)) ^. identifierType) ->
+            | isDynamic (lookupIdentifierInfo tab _identSymbol ^. identifierType) ->
                throw (dynamicTypeError node (getInfoLocation _identInfo))
          NLam Lambda {..}
            | isDynamic (_lambdaBinder ^. binderType) ->
--- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
+++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
@ -1,6 +1,5 @@
 module Juvix.Compiler.Core.Transformation.ComputeTypeInfo where

-import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Data.BinderList qualified as BL
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info.TypeInfo qualified as Info
@ -27,7 +26,7 @@ computeNodeTypeInfo tab = umapL go
      NVar Var {..} ->
        shift (_varIndex + 1) (BL.lookup _varIndex bl ^. binderType)
      NIdt Ident {..} ->
-        fromJust (HashMap.lookup _identSymbol (tab ^. infoIdentifiers)) ^. identifierType
+        lookupIdentifierInfo tab _identSymbol ^. identifierType
      NCst Constant {..} ->
        case _constantValue of
          ConstInteger {} -> mkTypeInteger'
@ -56,8 +55,8 @@ computeNodeTypeInfo tab = umapL go
            _ -> error "incorrect trace builtin application"
          OpFail -> Info.getNodeType node
      NCtr Constr {..} ->
-        let ci = fromJust $ HashMap.lookup _constrTag (tab ^. infoConstructors)
-            ii = fromJust $ HashMap.lookup (ci ^. constructorInductive) (tab ^. infoInductives)
+        let ci = lookupConstructorInfo tab _constrTag
+            ii = lookupInductiveInfo tab (ci ^. constructorInductive)
         in case ii ^. inductiveBuiltin of
              Just (BuiltinTypeInductive BuiltinBool) ->
                mkTypeBool'
--- a/src/Juvix/Compiler/Core/Transformation/Eta.hs
+++ b/src/Juvix/Compiler/Core/Transformation/Eta.hs
@ -4,7 +4,6 @@ module Juvix.Compiler.Core.Transformation.Eta
  )
 where

-import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Transformation.Base

@ -52,13 +51,13 @@ etaExpandApps tab =
  where
    constrArgtys :: Tag -> [Type]
    constrArgtys tag =
-      case HashMap.lookup tag (tab ^. infoConstructors) of
+      case lookupConstructorInfo' tab tag of
        Just ci -> typeArgs (ci ^. constructorType)
        Nothing -> []

    typeConstrArgtys :: Symbol -> [Type]
    typeConstrArgtys sym =
-      case HashMap.lookup sym (tab ^. infoInductives) of
+      case lookupInductiveInfo' tab sym of
        Just ci -> map (^. paramKind) (ci ^. inductiveParams)
        Nothing -> []

--- a/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs
@ -53,8 +53,8 @@ lambdaLiftNode aboveBl top =
              let (freevarsAssocs, fBody') = captureFreeVarsCtx bl l'
                  allfreevars :: [Var]
                  allfreevars = map fst freevarsAssocs
-                  argsInfo :: [ArgumentInfo]
-                  argsInfo = map (argumentInfoFromBinder . (^. lambdaLhsBinder)) (fst (unfoldLambdas fBody'))
+                  argsNum :: Int
+                  argsNum = length (fst (unfoldLambdas fBody'))
              f <- freshSymbol
              let name = uniqueName "lambda" f
              ty <- nodeType fBody'
@ -65,8 +65,7 @@ lambdaLiftNode aboveBl top =
                    _identifierName = name,
                    _identifierLocation = Nothing,
                    _identifierType = ty,
-                    _identifierArgsNum = length argsInfo,
-                    _identifierArgsInfo = argsInfo,
+                    _identifierArgsNum = argsNum,
                    _identifierIsExported = False,
                    _identifierBuiltin = Nothing
                  }
@ -127,9 +126,8 @@ lambdaLiftNode aboveBl top =
                            captureFreeVarsType
                              (map (first (^. varIndex)) recItemsFreeVars)
                              (b, bty)
-                          argsInfo :: [ArgumentInfo]
-                          argsInfo =
-                            map (argumentInfoFromBinder . (^. lambdaLhsBinder)) (fst (unfoldLambdas topBody))
+                          argsNum :: Int
+                          argsNum = length (fst (unfoldLambdas topBody))
                      registerIdentNode sym topBody
                      registerIdent
                        name
@ -138,8 +136,7 @@ lambdaLiftNode aboveBl top =
                            _identifierName = name,
                            _identifierLocation = itemBinder ^. binderLocation,
                            _identifierType = topTy,
-                            _identifierArgsNum = length argsInfo,
-                            _identifierArgsInfo = argsInfo,
+                            _identifierArgsNum = argsNum,
                            _identifierIsExported = False,
                            _identifierBuiltin = Nothing
                          }
--- a/src/Juvix/Compiler/Core/Transformation/MatchToCase.hs
+++ b/src/Juvix/Compiler/Core/Transformation/MatchToCase.hs
@ -1,6 +1,5 @@
 module Juvix.Compiler.Core.Transformation.MatchToCase where

-import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
 import Data.List qualified as List
 import Juvix.Compiler.Core.Error
@ -118,8 +117,8 @@ goMatchToCase recur node = case node of
                    compileDefault Nothing err bindersNum vs' col matrix'
                | otherwise -> do
                    -- Section 4, case 3(a)
-                    let ind = fromJust (HashMap.lookup (List.head tags) (tab ^. infoConstructors)) ^. constructorInductive
-                        ctrsNum = length (fromJust (HashMap.lookup ind (tab ^. infoInductives)) ^. inductiveConstructors)
+                    let ind = lookupConstructorInfo tab (List.head tags) ^. constructorInductive
+                        ctrsNum = length (lookupInductiveInfo tab ind ^. inductiveConstructors)
                    branches <- mapM (compileBranch err bindersNum vs' col matrix') tags
                    defaultBranch <-
                      if
@ -171,9 +170,9 @@ goMatchToCase recur node = case node of
        getPatTags pats

    missingTag :: InfoTable -> Symbol -> HashSet Tag -> Tag
-    missingTag tab ind tags = fromJust $ find (not . flip HashSet.member tags) (map (^. constructorTag) (ii ^. inductiveConstructors))
+    missingTag tab ind tags = fromJust $ find (not . flip HashSet.member tags) (ii ^. inductiveConstructors)
      where
-        ii = fromJust $ HashMap.lookup ind (tab ^. infoInductives)
+        ii = lookupInductiveInfo tab ind

    compileMatchingRow :: Level -> [Level] -> PatternRow -> Sem r Node
    compileMatchingRow bindersNum vs PatternRow {..} =
@ -202,7 +201,7 @@ goMatchToCase recur node = case node of
            Just tag ->
              err (parensIf (argsNum > 0) (hsep (annotate (AnnKind KNameConstructor) (pretty (ci ^. constructorName)) : replicate argsNum "_")) : args)
              where
-                ci = fromJust $ HashMap.lookup tag (tab ^. infoConstructors)
+                ci = lookupConstructorInfo tab tag
                paramsNum = getTypeParamsNum tab (ci ^. constructorType)
                argsNum = ci ^. constructorArgsNum - paramsNum
            Nothing ->
@ -214,7 +213,7 @@ goMatchToCase recur node = case node of
    compileBranch :: ([Doc Ann] -> Doc Ann) -> Level -> [Level] -> [Pattern] -> PatternMatrix -> Tag -> Sem r CaseBranch
    compileBranch err bindersNum vs col matrix tag = do
      tab <- ask
-      let ci = fromJust $ HashMap.lookup tag (tab ^. infoConstructors)
+      let ci = lookupConstructorInfo tab tag
          paramsNum = getTypeParamsNum tab (ci ^. constructorType)
          argsNum = length (typeArgs (ci ^. constructorType))
          bindersNum' = bindersNum + argsNum
@ -260,7 +259,7 @@ goMatchToCase recur node = case node of
    getBranchMatrix :: [Pattern] -> PatternMatrix -> Tag -> Sem r PatternMatrix
    getBranchMatrix col matrix tag = do
      tab <- ask
-      let ci = fromJust $ HashMap.lookup tag (tab ^. infoConstructors)
+      let ci = lookupConstructorInfo tab tag
          argtys = typeArgs (ci ^. constructorType)
          argsNum = length argtys
          helper :: PatternRow -> Pattern -> Maybe PatternRow
--- a/src/Juvix/Compiler/Core/Transformation/NatToInt.hs
+++ b/src/Juvix/Compiler/Core/Transformation/NatToInt.hs
@ -41,7 +41,7 @@ convertNode tab = rmap go
            )
            _identSymbol
      NCtr (Constr {..}) ->
-        let ci = fromJust $ HashMap.lookup _constrTag (tab ^. infoConstructors)
+        let ci = lookupConstructorInfo tab _constrTag
         in case ci ^. constructorBuiltin of
              Just BuiltinNatZero ->
                mkConstant _constrInfo (ConstInteger 0)
@ -49,7 +49,7 @@ convertNode tab = rmap go
                recur [] $ mkBuiltinApp _constrInfo OpIntAdd (_constrArgs ++ [mkConstant' (ConstInteger 1)])
              _ -> recur [] node
      NCase (Case {..}) ->
-        let ii = fromJust $ HashMap.lookup _caseInductive (tab ^. infoInductives)
+        let ii = lookupInductiveInfo tab _caseInductive
         in case ii ^. inductiveBuiltin of
              Just (BuiltinTypeInductive BuiltinNat) ->
                case _caseBranches of
@ -68,7 +68,7 @@ convertNode tab = rmap go
        where
          makeIf :: CaseBranch -> Node -> Node
          makeIf CaseBranch {..} br =
-            let ci = fromJust $ HashMap.lookup (BuiltinTag TagTrue) (tab ^. infoConstructors)
+            let ci = lookupConstructorInfo tab (BuiltinTag TagTrue)
                sym = ci ^. constructorInductive
             in case _caseBranchBindersNum of
                  0 ->
@ -98,7 +98,7 @@ convertNode tab = rmap go

    convertIdentApp :: Node -> ((Info -> Node -> Node -> Node) -> Node) -> Symbol -> Node
    convertIdentApp node f sym =
-      let ii = fromJust $ HashMap.lookup sym (tab ^. infoIdentifiers)
+      let ii = lookupIdentifierInfo tab sym
       in case ii ^. identifierBuiltin of
            Just BuiltinNatPlus -> f (\info x y -> mkBuiltinApp info OpIntAdd [x, y])
            Just BuiltinNatSub ->
@ -113,7 +113,7 @@ convertNode tab = rmap go
                )
              where
                boolSymbol =
-                  fromJust (HashMap.lookup (BuiltinTag TagTrue) (tab ^. infoConstructors)) ^. constructorInductive
+                  lookupConstructorInfo tab (BuiltinTag TagTrue) ^. constructorInductive
            Just BuiltinNatMul -> f (\info x y -> mkBuiltinApp info OpIntMul [x, y])
            Just BuiltinNatUDiv ->
              f
--- a/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs
+++ b/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs
@ -29,10 +29,10 @@ convertNode tab = convert mempty
        where
          k = length (filter (isTypeConstr tab . (^. binderType)) (take _varIndex (toList vars)))
      NIdt Ident {..} ->
-        let fi = fromJust $ HashMap.lookup _identSymbol (tab ^. infoIdentifiers)
+        let fi = lookupIdentifierInfo tab _identSymbol
         in if
                | isTypeConstr tab (fi ^. identifierType) ->
-                    Recur (fromJust $ HashMap.lookup _identSymbol (tab ^. identContext))
+                    Recur (lookupIdentifierNode tab _identSymbol)
                | otherwise ->
                    Recur node
      NApp App {..} ->
@ -42,7 +42,7 @@ convertNode tab = convert mempty
                NVar (Var {..}) ->
                  BL.lookup _varIndex vars ^. binderType
                NIdt (Ident {..}) ->
-                  let fi = fromJust $ HashMap.lookup _identSymbol (tab ^. infoIdentifiers)
+                  let fi = lookupIdentifierInfo tab _identSymbol
                   in fi ^. identifierType
                _ -> unsupported node
            args' = filterArgs snd ty args
@ -54,7 +54,7 @@ convertNode tab = convert mempty
                | otherwise ->
                    End (mkApps (convert vars h) (map (second (convert vars)) args'))
      NCtr (Constr {..}) ->
-        let ci = fromJust $ HashMap.lookup _constrTag (tab ^. infoConstructors)
+        let ci = lookupConstructorInfo tab _constrTag
            ty = ci ^. constructorType
            args' = filterArgs id ty _constrArgs
         in End (mkConstr _constrInfo _constrTag (map (convert vars) args'))
@ -117,15 +117,9 @@ convertIdent :: InfoTable -> IdentifierInfo -> IdentifierInfo
 convertIdent tab ii =
  ii
    { _identifierType = ty',
-      _identifierArgsInfo =
-        map (uncurry (set argumentType)) $
-          zipExact tyargs' $
-            map fst $
-              filter (not . isTypeConstr tab . snd) (zipExact (ii ^. identifierArgsInfo) tyargs),
      _identifierArgsNum = length tyargs'
    }
  where
-    tyargs = typeArgs (ii ^. identifierType)
    ty' = convertNode tab (ii ^. identifierType)
    tyargs' = typeArgs ty'

@ -142,8 +136,7 @@ convertInductive :: InfoTable -> InductiveInfo -> InductiveInfo
 convertInductive tab ii =
  ii
    { _inductiveKind = ty',
-      _inductiveParams = map (over paramKind (convertNode tab) . fst) $ filter (not . isTypeConstr tab . snd) (zipExact (ii ^. inductiveParams) tyargs),
-      _inductiveConstructors = map (convertConstructor tab) (ii ^. inductiveConstructors)
+      _inductiveParams = map (over paramKind (convertNode tab) . fst) $ filter (not . isTypeConstr tab . snd) (zipExact (ii ^. inductiveParams) tyargs)
    }
  where
    tyargs = typeArgs (ii ^. inductiveKind)
--- a/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
+++ b/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs
@ -21,18 +21,9 @@ topEtaExpand info = run (mapT' go info)
          (_ : as) -> case node of
            NLam l -> NLam <$> traverseOf lambdaBody (skipLambdas as) l
            _ -> do
-              let newArgsInfo :: [ArgumentInfo]
-                  newArgsInfo = map toArgumentInfo args
-              overIdentArgsInfo sym (++ newArgsInfo)
+              let binders = map (^. piLhsBinder) args
+              overIdentArgs sym (++ binders)
              return (expand node args)
-        toArgumentInfo :: PiLhs -> ArgumentInfo
-        toArgumentInfo pi =
-          ArgumentInfo
-            { _argumentName = pi ^. piLhsBinder . binderName,
-              _argumentLocation = pi ^. piLhsBinder . binderLocation,
-              _argumentType = pi ^. piLhsBinder . binderType,
-              _argumentIsImplicit = Explicit
-            }
        expand :: Node -> [PiLhs] -> Node
        expand n lhs = reLambdas (map lambdaFromPi lhs) body'
          where
--- a/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs
+++ b/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs
@ -62,7 +62,7 @@ unrollRecursion tab = do
          forM_ [0 .. unrollLimit] goUnroll
          removeSymbol sym
          where
-            ii = fromJust $ HashMap.lookup sym (tab ^. infoIdentifiers)
+            ii = lookupIdentifierInfo tab sym

            goUnroll :: Int -> Sem r ()
            goUnroll limit = do
@ -77,7 +77,7 @@ unrollRecursion tab = do
                    | limit == 0 =
                        etaExpand (typeArgs (ii ^. identifierType)) failNode
                    | otherwise =
-                        umap (go limit) (fromJust $ HashMap.lookup sym (tab ^. identContext))
+                        umap (go limit) (lookupIdentifierNode tab sym)
              registerIdentNode sym' node

            go :: Int -> Node -> Node
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@ -66,15 +66,7 @@ fromInternal i = do
              _identifierName = freshIdentName tab "intToNat",
              _identifierLocation = Nothing,
              _identifierArgsNum = 1,
-              _identifierArgsInfo =
-                [ ArgumentInfo
-                    { _argumentName = "x",
-                      _argumentLocation = Nothing,
-                      _argumentType = mkTypePrim' (PrimInteger $ PrimIntegerInfo Nothing Nothing),
-                      _argumentIsImplicit = Explicit
-                    }
-                ],
-              _identifierType = mkPi' mkTypeInteger' targetType,
+              _identifierType = mkPi mempty (Binder "x" Nothing mkTypeInteger') targetType,
              _identifierIsExported = False,
              _identifierBuiltin = Nothing
            }
@ -177,7 +169,7 @@ goInductiveDef i = do
  -- because their types refer to the inductive
  registerInductive idx info
  ctorInfos <- mapM (goConstructor sym) (i ^. Internal.inductiveConstructors)
-  registerInductive idx info {_inductiveConstructors = ctorInfos}
+  registerInductive idx info {_inductiveConstructors = map (^. constructorTag) ctorInfos}

 goConstructor ::
  forall r.
@ -276,7 +268,6 @@ goFunctionDefIden (f, sym) = do
            -- _identiferArgsNum needs to match the number of lambdas in the
            -- body. This needs to be filled in later (in goFunctionDef).
            _identifierArgsNum = 0,
-            _identifierArgsInfo = [],
            _identifierIsExported = False,
            _identifierBuiltin = f ^. Internal.funDefBuiltin
          }
@ -314,7 +305,7 @@ goFunctionDef ((f, sym), ty) = do
    setIdentArgsInfo' :: Node -> Sem r ()
    setIdentArgsInfo' node = do
      let (is, _) = unfoldLambdas node
-      setIdentArgsInfo sym (map (argumentInfoFromBinder . (^. lambdaLhsBinder)) is)
+      setIdentArgs sym (map (^. lambdaLhsBinder) is)

 mkFunBody ::
  forall r.
@ -525,7 +516,7 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
              { _inductiveLocation = Just $ a ^. Internal.axiomName . nameLoc,
                _inductiveSymbol = sym,
                _inductiveKind = mkSmallUniv,
-                _inductiveConstructors = ctrs',
+                _inductiveConstructors = map (^. constructorTag) ctrs',
                _inductiveParams = [],
                _inductivePositive = False,
                _inductiveBuiltin = BuiltinTypeAxiom <$> ax,
@ -555,7 +546,6 @@ goAxiomDef a = do
                _identifierSymbol = sym,
                _identifierType = ty,
                _identifierArgsNum = 0,
-                _identifierArgsInfo = [],
                _identifierIsExported = False,
                _identifierBuiltin = Nothing,
                _identifierName
@ -563,7 +553,7 @@ goAxiomDef a = do
      registerIdent (mkIdentIndex (a ^. Internal.axiomName)) info
      registerIdentNode sym body
      let (is, _) = unfoldLambdas body
-      setIdentArgsInfo sym (map (argumentInfoFromBinder . (^. lambdaLhsBinder)) is)
+      setIdentArgs sym (map (^. lambdaLhsBinder) is)
    Nothing -> return ()
  where
    builtinBody :: Symbol -> Symbol -> Text -> Internal.BuiltinAxiom -> Maybe Node
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@ -55,7 +55,6 @@ setupMainFunction tab node =
          _identifierLocation = Nothing,
          _identifierSymbol = sym,
          _identifierArgsNum = 0,
-          _identifierArgsInfo = [],
          _identifierType = mkDynamic',
          _identifierBuiltin = Nothing,
          _identifierIsExported = True
@ -153,7 +152,6 @@ statementDef = do
                _identifierSymbol = sym,
                _identifierType = ty,
                _identifierArgsNum = 0,
-                _identifierArgsInfo = [],
                _identifierIsExported = False,
                _identifierBuiltin = Nothing
              }
@ -177,7 +175,7 @@ parseDefinition sym ty = do
        && not (isDynamic (typeTarget ty))
    )
    $ parseFailure off "type mismatch: too many lambdas"
-  lift $ setIdentArgsInfo sym (map (argumentInfoFromBinder . (^. lambdaLhsBinder)) is)
+  lift $ setIdentArgs sym (map (^. lambdaLhsBinder) is)

 statementInductive ::
  (Member InfoTableBuilder r) =>
@ -204,7 +202,7 @@ statementInductive = do
          }
  lift $ registerInductive txt ii
  ctrs <- braces $ P.sepEndBy (constrDecl sym) (kw kwSemicolon)
-  lift $ registerInductive txt ii {_inductiveConstructors = ctrs}
+  lift $ registerInductive txt ii {_inductiveConstructors = map (^. constructorTag) ctrs}

 constrDecl ::
  (Member InfoTableBuilder r) =>
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
@ -30,26 +30,27 @@ fromCore tab =

 translateFunctionInfo :: InfoTable -> IdentifierInfo -> Stripped.FunctionInfo
 translateFunctionInfo tab IdentifierInfo {..} =
-  Stripped.FunctionInfo
-    { _functionName = _identifierName,
-      _functionLocation = _identifierLocation,
-      _functionSymbol = _identifierSymbol,
-      _functionBody =
-        translateFunction
-          _identifierArgsNum
-          (fromJust $ HashMap.lookup _identifierSymbol (tab ^. identContext)),
-      _functionType = translateType _identifierType,
-      _functionArgsNum = _identifierArgsNum,
-      _functionArgsInfo = map translateArgInfo _identifierArgsInfo,
-      _functionIsExported = _identifierIsExported
-    }
+  assert (length (typeArgsBinders _identifierType) == _identifierArgsNum) $
+    Stripped.FunctionInfo
+      { _functionName = _identifierName,
+        _functionLocation = _identifierLocation,
+        _functionSymbol = _identifierSymbol,
+        _functionBody =
+          translateFunction
+            _identifierArgsNum
+            (fromJust $ HashMap.lookup _identifierSymbol (tab ^. identContext)),
+        _functionType = translateType _identifierType,
+        _functionArgsNum = _identifierArgsNum,
+        _functionArgsInfo = map translateArgInfo (typeArgsBinders _identifierType),
+        _functionIsExported = _identifierIsExported
+      }

-translateArgInfo :: ArgumentInfo -> Stripped.ArgumentInfo
-translateArgInfo ArgumentInfo {..} =
+translateArgInfo :: Binder -> Stripped.ArgumentInfo
+translateArgInfo Binder {..} =
  Stripped.ArgumentInfo
-    { _argumentName = _argumentName,
-      _argumentLocation = _argumentLocation,
-      _argumentType = translateType _argumentType
+    { _argumentName = _binderName,
+      _argumentLocation = _binderLocation,
+      _argumentType = translateType _binderType
    }

 translateInductiveInfo :: InductiveInfo -> Stripped.InductiveInfo
@ -59,7 +60,7 @@ translateInductiveInfo InductiveInfo {..} =
      _inductiveLocation = _inductiveLocation,
      _inductiveSymbol = _inductiveSymbol,
      _inductiveKind = translateType _inductiveKind,
-      _inductiveConstructors = map translateConstructorInfo _inductiveConstructors,
+      _inductiveConstructors = _inductiveConstructors,
      _inductiveParams = map translateParamInfo _inductiveParams
    }

--- a/src/Juvix/Compiler/Reg/Data/InfoTable.hs
+++ b/src/Juvix/Compiler/Reg/Data/InfoTable.hs
@ -32,7 +32,7 @@ data InductiveInfo = InductiveInfo
  { _inductiveName :: Text,
    _inductiveLocation :: Maybe Location,
    _inductiveSymbol :: Symbol,
-    _inductiveConstructors :: [ConstructorInfo],
+    _inductiveConstructors :: [Tag],
    _inductiveRepresentation :: IndRep
  }

--- a/src/Juvix/Compiler/Reg/Translation/FromAsm.hs
+++ b/src/Juvix/Compiler/Reg/Translation/FromAsm.hs
@ -46,7 +46,7 @@ fromAsm tab =
        { _inductiveName = ii ^. Asm.inductiveName,
          _inductiveLocation = ii ^. Asm.inductiveLocation,
          _inductiveSymbol = ii ^. Asm.inductiveSymbol,
-          _inductiveConstructors = map convertConstr (ii ^. Asm.inductiveConstructors),
+          _inductiveConstructors = ii ^. Asm.inductiveConstructors,
          _inductiveRepresentation = ii ^. Asm.inductiveRepresentation
        }

--- a/test/Asm/Run/Base.hs
+++ b/test/Asm/Run/Base.hs
@ -4,7 +4,6 @@ import Base
 import Data.Text.IO qualified as TIO
 import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Error
-import Juvix.Compiler.Asm.Extra
 import Juvix.Compiler.Asm.Interpreter
 import Juvix.Compiler.Asm.Pretty
 import Juvix.Compiler.Asm.Transformation.Validate
@ -24,7 +23,7 @@ asmRunAssertion' tab expectedFile step = do
                let outputFile = dirPath <//> $(mkRelFile "out.out")
                hout <- openFile (toFilePath outputFile) WriteMode
                step "Interpret"
-                r' <- doRun hout tab (getFunInfo tab sym)
+                r' <- doRun hout tab (lookupFunInfo tab sym)
                case r' of
                  Left err -> do
                    hClose hout
@ -72,7 +71,7 @@ asmRunErrorAssertion mainFile step = do
                    let outputFile = dirPath <//> $(mkRelFile "out.out")
                    hout <- openFile (toFilePath outputFile) WriteMode
                    step "Interpret"
-                    r' <- doRun hout tab (getFunInfo tab sym)
+                    r' <- doRun hout tab (lookupFunInfo tab sym)
                    hClose hout
                    case r' of
                      Left _ -> assertBool "" True