Add Bottom node (#2112)

- Closes #2056 
- Depends on #2103 

I am not sure about the implementation of `isType` for `NBot`. (solved).

The `Eq` instance returns `True` for every two `Bottom` terms,
regardless of their type.

---------

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>

src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs

@@ -138,6 +138,7 @@ fromCore tab = case tab ^. Core.infoMain of
       Core.NTyp {} -> unsupported
       Core.NPrim {} -> unsupported
       Core.NDyn {} -> unsupported
+      Core.NBot {} -> unsupported
       Core.Closure {} -> unsupported
 
     insertedBinders :: Level -> [Level] -> Index -> Int

src/Juvix/Compiler/Core/Error.hs

@@ -29,9 +29,9 @@ instance ToGenericError CoreError where
             Nothing -> e ^. coreErrorMsg
 
 instance Pretty CoreError where
-  pretty (CoreError {..}) = case _coreErrorNode of
+  pretty CoreError {..} = case _coreErrorNode of
     Just node -> pretty _coreErrorMsg <> colon <> space <> pretty (ppTrace node)
     Nothing -> pretty _coreErrorMsg
 
 instance HasLoc CoreError where
-  getLoc (CoreError {..}) = _coreErrorLoc
+  getLoc CoreError {..} = _coreErrorLoc

src/Juvix/Compiler/Core/Evaluator.hs

@@ -115,6 +115,7 @@ geval opts herr ctx env0 = eval' env0
       NTyp (TypeConstr i sym args) -> mkTypeConstr i sym (map' (eval' env) args)
       NPrim {} -> n
       NDyn {} -> n
+      NBot {} -> evalError "bottom" n
       Closure {} -> n
 
     branch :: Node -> Env -> [Node] -> Tag -> Maybe Node -> [CaseBranch] -> Node

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

@@ -192,6 +192,12 @@ mkDynamic i = NDyn (Dynamic i)
 mkDynamic' :: Type
 mkDynamic' = mkDynamic Info.empty
 
+mkBottom :: Info -> Type -> Node
+mkBottom _bottomInfo _bottomType = NBot Bottom {..}
+
+mkBottom' :: Node
+mkBottom' = mkBottom mempty mkDynamic'
+
 {------------------------------------------------------------------------}
 {- functions on Type -}
 
@@ -298,26 +304,6 @@ unfoldLambdas' = first length . unfoldLambdas
 lambdaTypes :: Node -> [Type]
 lambdaTypes = map (\LambdaLhs {..} -> _lambdaLhsBinder ^. binderType) . fst . unfoldLambdas
 
-isType :: Node -> Bool
-isType = \case
-  NPi {} -> True
-  NUniv {} -> True
-  NPrim {} -> True
-  NTyp {} -> True
-  NDyn {} -> True
-  NVar {} -> False
-  NIdt {} -> False
-  NCst {} -> False
-  NApp {} -> False
-  NBlt {} -> False
-  NCtr {} -> False
-  NLam {} -> False
-  NLet {} -> False
-  NRec {} -> False
-  NCase {} -> False
-  NMatch {} -> False
-  Closure {} -> False
-
 {------------------------------------------------------------------------}
 {- functions on Pattern -}
 
@@ -726,6 +712,13 @@ destruct = \case
         _nodeChildren = [],
         _nodeReassemble = noChildren $ \i' -> mkDynamic i'
       }
+  NBot (Bottom i ty) ->
+    NodeDetails
+      { _nodeInfo = i,
+        _nodeSubinfos = [],
+        _nodeChildren = [noBinders ty],
+        _nodeReassemble = oneChild mkBottom
+      }
   Closure env n ->
     NodeDetails
       { _nodeInfo = mempty,

src/Juvix/Compiler/Core/Extra/Utils.hs

@@ -28,6 +28,7 @@ import Juvix.Compiler.Core.Extra.Recursors.Utils
 import Juvix.Compiler.Core.Extra.Utils.Base
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.ExpansionInfo
+import Juvix.Compiler.Core.Info.LocationInfo qualified as Info
 import Juvix.Compiler.Core.Language
 
 substEnvInBranch :: Env -> CaseBranch -> CaseBranch
@@ -38,6 +39,9 @@ substEnvInBranch env br = over caseBranchBody (substEnv env') br
 isClosed :: Node -> Bool
 isClosed = not . has freeVars
 
+mkAxiom :: Interval -> Type -> Node
+mkAxiom loc = mkBottom (Info.setInfoLocation loc mempty)
+
 isTypeConstr :: InfoTable -> Type -> Bool
 isTypeConstr tab ty = case typeTarget ty of
   NUniv {} ->
@@ -58,6 +62,27 @@ filterOutTypeSynonyms tab = pruneInfoTable tab'
     tab' = tab {_infoIdentifiers = idents'}
     idents' = HashMap.filter (\ii -> not (isTypeConstr tab (ii ^. identifierType))) (tab ^. infoIdentifiers)
 
+isType :: Node -> Bool
+isType = \case
+  NPi {} -> True
+  NUniv {} -> True
+  NPrim {} -> True
+  NTyp {} -> True
+  NDyn {} -> True
+  NBot {} -> False
+  NVar {} -> False
+  NIdt {} -> False
+  NCst {} -> False
+  NApp {} -> False
+  NBlt {} -> False
+  NCtr {} -> False
+  NLam {} -> False
+  NLet {} -> False
+  NRec {} -> False
+  NCase {} -> False
+  NMatch {} -> False
+  Closure {} -> False
+
 -- | True for nodes whose evaluation immediately returns a value, i.e.,
 -- no reduction or memory allocation in the runtime is required.
 isImmediate :: Node -> Bool

src/Juvix/Compiler/Core/Info/TypeInfo.hs

@@ -5,7 +5,9 @@ import Juvix.Compiler.Core.Extra.Info
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Language
 
-newtype TypeInfo = TypeInfo {_infoType :: Type}
+newtype TypeInfo = TypeInfo
+  { _infoType :: Type
+  }
 
 instance IsInfo TypeInfo
 

src/Juvix/Compiler/Core/Keywords.hs

@@ -10,6 +10,7 @@ import Juvix.Data.Keyword.All
   ( kwAny,
     kwAssign,
     kwBind,
+    kwBottom,
     kwBuiltin,
     kwCase,
     kwColon,
@@ -57,6 +58,7 @@ allKeywords :: [Keyword]
 allKeywords =
   [ kwAssign,
     kwBuiltin,
+    kwBottom,
     kwLet,
     kwLetRec,
     kwIn,

src/Juvix/Compiler/Core/Language.hs

@@ -61,6 +61,8 @@ type TypePrim = TypePrim' Info
 
 type Dynamic = Dynamic' Info
 
+type Bottom = Bottom' Info Node
+
 {---------------------------------------------------------------------------------}
 
 -- | `Node` is the type of nodes in the program tree. The nodes themselves
@@ -84,6 +86,7 @@ data Node
   | NTyp {-# UNPACK #-} !TypeConstr
   | NPrim {-# UNPACK #-} !TypePrim
   | NDyn !Dynamic -- Dynamic is already a newtype, so it's unpacked.
+  | NBot {-# UNPACK #-} !Bottom
   | -- Evaluation only: `Closure env node`.
     Closure
       { _closureEnv :: !Env,
@@ -129,6 +132,7 @@ instance HasAtomicity Node where
     NTyp x -> atomicity x
     NPrim x -> atomicity x
     NDyn x -> atomicity x
+    NBot x -> atomicity x
     Closure {} -> Aggregate lambdaFixity
 
 emptyBinder :: Binder

src/Juvix/Compiler/Core/Language/Nodes.hs

@@ -219,7 +219,15 @@ data TypePrim' i = TypePrim
 -- | Dynamic type. A Node with a dynamic type has an unknown type. Useful
 -- for transformations that introduce partial type information, e.g., one can
 -- have types `* -> *` and `* -> * -> Nat` where `*` is the dynamic type.
-newtype Dynamic' i = Dynamic {_dynamicInfo :: i}
+newtype Dynamic' i = Dynamic
+  { _dynamicInfo :: i
+  }
+
+-- | A fail node.
+data Bottom' i a = Bottom
+  { _bottomInfo :: i,
+    _bottomType :: !a
+  }
 
 {-------------------------------------------------------------------}
 {- Typeclass instances -}
@@ -295,6 +303,9 @@ instance HasAtomicity (TypeConstr' i a) where
 instance HasAtomicity (Dynamic' i) where
   atomicity _ = Atom
 
+instance HasAtomicity (Bottom' i a) where
+  atomicity _ = Atom
+
 lambdaFixity :: Fixity
 lambdaFixity = Fixity (PrecNat 0) (Unary AssocPostfix)
 
@@ -378,6 +389,9 @@ instance Eq (TypePrim' i) where
 instance Eq (Dynamic' i) where
   (Dynamic _) == (Dynamic _) = True
 
+instance Eq (Bottom' i a) where
+  Bottom {} == Bottom {} = True
+
 deriving stock instance (Eq a) => Eq (Pattern' i a)
 
 instance (Eq a, Eq ty) => Eq (LetItem' a ty) where

src/Juvix/Compiler/Core/Normalizer.hs

@@ -64,6 +64,7 @@ normalize tab0 = run . evalInfoTableBuilder tab0 . runReader normEnv . normalize
       NTyp x -> goTypeConstr x
       NPrim {} -> return val
       NDyn {} -> return val
+      NBot {} -> return val
       Closure {..} -> goClosure _closureEnv _closureNode
 
     underBinder :: Norm a -> Norm a

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

@@ -309,6 +309,12 @@ instance PrettyCode Lambda where
           return $ kwLambda <> parens (n <+> kwColon <+> tty)
     return (lam <> oneLineOrNext b)
 
+instance PrettyCode Bottom where
+  ppCode :: Member (Reader Options) r => Bottom -> Sem r (Doc Ann)
+  ppCode Bottom {..} = do
+    ty' <- ppCode _bottomType
+    return (parens (kwBottom <+> kwColon <+> ty'))
+
 instance PrettyCode Node where
   ppCode :: forall r. (Member (Reader Options) r) => Node -> Sem r (Doc Ann)
   ppCode node = case node of
@@ -350,6 +356,7 @@ instance PrettyCode Node where
       n' <- ppName KNameInductive (getInfoName _typeConstrInfo)
       return $ foldl' (<+>) n' args'
     NDyn {} -> return kwDynamic
+    NBot b -> ppCode b
     Closure env n ->
       ppCode (substEnv env n)
 
@@ -737,3 +744,9 @@ kwFail = keyword Str.fail_
 
 kwDynamic :: Doc Ann
 kwDynamic = keyword Str.any
+
+kwBottomAscii :: Doc Ann
+kwBottomAscii = keyword Str.bottomAscii
+
+kwBottom :: Doc Ann
+kwBottom = keyword Str.bottom

src/Juvix/Compiler/Core/Transformation/Check/Base.hs

@@ -1,22 +1,36 @@
 module Juvix.Compiler.Core.Transformation.Check.Base where
 
 import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Data.InfoTableBuilder
 import Juvix.Compiler.Core.Data.TypeDependencyInfo (createTypeDependencyInfo)
 import Juvix.Compiler.Core.Error
 import Juvix.Compiler.Core.Extra
-import Juvix.Compiler.Core.Info.LocationInfo (getInfoLocation)
+import Juvix.Compiler.Core.Info.LocationInfo (getInfoLocation, getNodeLocation)
 import Juvix.Compiler.Core.Info.TypeInfo qualified as Info
 import Juvix.Compiler.Core.Language
+import Juvix.Compiler.Core.Transformation.Base (mapT')
+import Juvix.Data.NameKind
 import Juvix.Data.PPOutput
 
 dynamicTypeError :: Node -> Maybe Location -> CoreError
 dynamicTypeError node loc =
   CoreError
-    { _coreErrorMsg = ppOutput $ "compilation for this target requires full type information",
+    { _coreErrorMsg = ppOutput "compilation for this target requires full type information",
       _coreErrorNode = Just node,
       _coreErrorLoc = fromMaybe defaultLoc loc
     }
 
+axiomError :: Members '[Error CoreError, InfoTableBuilder] r => Symbol -> Maybe Location -> Sem r a
+axiomError sym loc = do
+  tbl <- getInfoTable
+  let nameTxt = identName tbl sym
+  throw
+    CoreError
+      { _coreErrorMsg = ppOutput ("The symbol" <+> annotate (AnnKind KNameAxiom) (pretty nameTxt) <> " is defined as an axiom and thus it cannot be compiled"),
+        _coreErrorNode = Nothing,
+        _coreErrorLoc = fromMaybe defaultLoc loc
+      }
+
 unsupportedError :: Text -> Node -> Maybe Location -> CoreError
 unsupportedError what node loc =
   CoreError
@@ -56,6 +70,17 @@ checkBuiltins allowUntypedFail = dmapRM go
           _ -> return $ Recur node
       _ -> return $ Recur node
 
+-- | Checks that the root of the node is not `Bottom`. Currently the only way we
+-- create `Bottom` is when translating axioms that are not builtin. Hence it is
+-- enought to check the root only.
+checkNoAxioms :: forall r. Member (Error CoreError) r => InfoTable -> Sem r ()
+checkNoAxioms = void . mapT' checkNodeNoAxiom
+  where
+    checkNodeNoAxiom :: Symbol -> Node -> Sem (InfoTableBuilder ': r) Node
+    checkNodeNoAxiom sym n = case n of
+      NBot {} -> axiomError sym (getNodeLocation n)
+      _ -> return n
+
 checkNoIO :: forall r. Member (Error CoreError) r => Node -> Sem r Node
 checkNoIO = dmapM go
   where

src/Juvix/Compiler/Core/Transformation/Check/Exec.hs

@@ -7,7 +7,8 @@ import Juvix.Compiler.Core.Transformation.Check.Base
 import Juvix.Data.PPOutput
 
 checkExec :: forall r. Member (Error CoreError) r => InfoTable -> Sem r InfoTable
-checkExec tab =
+checkExec tab = do
+  checkNoAxioms tab
   case tab ^. infoMain of
     Nothing ->
       throw

src/Juvix/Compiler/Core/Transformation/Check/Geb.hs

@@ -8,6 +8,7 @@ checkGeb :: forall r. Member (Error CoreError) r => InfoTable -> Sem r InfoTable
 checkGeb tab =
   checkMainExists tab
     >> checkNoRecursiveTypes tab
+    >> checkNoAxioms tab
     >> mapAllNodesM checkNoIO tab
     >> mapAllNodesM (checkBuiltins False) tab
     >> mapAllNodesM (checkTypes False tab) tab

src/Juvix/Compiler/Core/Transformation/Check/VampIR.hs

@@ -10,6 +10,7 @@ checkVampIR :: forall r. Member (Error CoreError) r => InfoTable -> Sem r InfoTa
 checkVampIR tab =
   checkMainExists tab
     >> checkMainType
+    >> checkNoAxioms tab
     >> mapAllNodesM checkNoIO tab
     >> mapAllNodesM (checkBuiltins True) tab
   where

src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs

@@ -89,6 +89,8 @@ computeNodeTypeInfo tab = umapL go
         mkUniv' 0
       NDyn Dynamic {} ->
         mkUniv' 0
+      NBot Bottom {..} ->
+        _bottomType
       Closure {} ->
         impossible