Add ValueType (#2143)

- Closes #2136

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

@@ -14,7 +14,20 @@ toValue tab = \case
   NCtr c -> goConstr c
   NLam lam -> goLambda lam
   Closure {..} -> toValue tab (substEnv _closureEnv _closureNode)
-  _ -> impossible
+  NPi {} -> goType
+  NUniv {} -> goType
+  NTyp {} -> goType
+  NPrim {} -> goType
+  NVar {} -> impossible
+  NIdt {} -> impossible
+  NApp {} -> impossible
+  NBlt {} -> impossible
+  NLet {} -> impossible
+  NRec {} -> impossible
+  NCase {} -> impossible
+  NMatch {} -> impossible
+  NDyn {} -> impossible
+  NBot {} -> impossible
   where
     goConstr :: Constr -> Value
     goConstr Constr {..} =
@@ -29,6 +42,9 @@ toValue tab = \case
         ii = lookupInductiveInfo tab (ci ^. constructorInductive)
         paramsNum = length (ii ^. inductiveParams)
 
+    goType :: Value
+    goType = ValueType
+
     goLambda :: Lambda -> Value
     goLambda lam =
       let (lams, body) = unfoldLambdas (NLam lam)
@@ -40,5 +56,4 @@ toValue tab = \case
                   case body of
                     NCtr c ->
                       toValue tab (NCtr (over constrArgs (dropEnd n) c))
-                    _ ->
-                      ValueFun
+                    _ -> ValueFun

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

@@ -15,6 +15,7 @@ data Value
   | ValueConstant ConstantValue
   | ValueWildcard
   | ValueFun
+  | ValueType
 
 makeLenses ''ConstrApp
 
@@ -29,3 +30,4 @@ instance HasAtomicity Value where
     ValueConstant {} -> Atom
     ValueWildcard -> Atom
     ValueFun -> Atom
+    ValueType -> Atom

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

@@ -597,7 +597,8 @@ instance PrettyCode Value where
     ValueConstrApp x -> ppCode x
     ValueConstant c -> ppCode c
     ValueWildcard -> return "_"
-    ValueFun -> return "<fun>"
+    ValueFun -> return "<function>"
+    ValueType -> return "<type>"
 
 ppValueSequence :: Member (Reader Options) r => [Value] -> Sem r (Doc Ann)
 ppValueSequence vs = hsep <$> mapM (ppRightExpression appFixity) vs