add exprIsType

anoma · Jan 29, 2025 · 559c2e7 · 559c2e7
1 parent 5801acb
commit 559c2e7
Showing 1 changed file with 18 additions and 1 deletion.
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@@ -278,7 +278,24 @@ goMutualBlock (Internal.MutualBlock m) = preMutual m >>= goMutual
         isTypDef = \case
           Internal.StatementInductive {} -> True
           Internal.StatementFunction {} -> False
-          Internal.StatementAxiom a -> isJust (builtinInductive a)
+          Internal.StatementAxiom a
+            | isJust (builtinInductive a) -> True
+            | exprIsType (a ^. Internal.axiomType) -> True
+            | otherwise -> False
+            where
+                exprIsType :: Internal.Expression -> Bool
+                exprIsType = \case
+                  Internal.ExpressionUniverse {} -> True
+                  Internal.ExpressionFunction (Internal.Function l r) -> exprIsType (l ^. Internal.paramType) && exprIsType r
+                  Internal.ExpressionIden {} -> False
+                  Internal.ExpressionApplication {} -> False
+                  Internal.ExpressionLiteral {} -> False
+                  Internal.ExpressionHole {} -> False
+                  Internal.ExpressionInstanceHole {} -> False
+                  Internal.ExpressionLet {} -> False
+                  Internal.ExpressionSimpleLambda {} -> False
+                  Internal.ExpressionLambda {} -> False
+                  Internal.ExpressionCase {} -> False
 
         step :: Internal.MutualStatement -> Sem (State PreMutual ': r) ()
         step = \case