From 4f6905300c400828058afe683c0996b46ad7b624 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 30 May 2023 10:34:00 +0200
Subject: [PATCH 1/2] add ValueType

---
 src/Juvix/Compiler/Core/Extra/Value.hs    | 21 ++++++++++++++++++---
 src/Juvix/Compiler/Core/Language/Value.hs |  2 ++
 src/Juvix/Compiler/Core/Pretty/Base.hs    |  1 +
 3 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/src/Juvix/Compiler/Core/Extra/Value.hs b/src/Juvix/Compiler/Core/Extra/Value.hs
index e6303c8750..487660ad80 100644
--- a/src/Juvix/Compiler/Core/Extra/Value.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Language/Value.hs b/src/Juvix/Compiler/Core/Language/Value.hs
index bff640f42b..38fd72a2ad 100644
--- a/src/Juvix/Compiler/Core/Language/Value.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index d624cb3591..576ec85b3e 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -598,6 +598,7 @@ instance PrettyCode Value where
     ValueConstant c -> ppCode c
     ValueWildcard -> return "_"
     ValueFun -> return "<fun>"
+    ValueType -> return "<type>"
 
 ppValueSequence :: Member (Reader Options) r => [Value] -> Sem r (Doc Ann)
 ppValueSequence vs = hsep <$> mapM (ppRightExpression appFixity) vs

From 547ac4248c2fbb5079f4ee9cc6173b5540ffb798 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 30 May 2023 10:44:38 +0200
Subject: [PATCH 2/2] fun -> function

---
 src/Juvix/Compiler/Core/Pretty/Base.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 576ec85b3e..804288f43e 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -597,7 +597,7 @@ 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)