JuvixCore primitive types (#1521)

src/Juvix/Compiler/Core/Evaluator.hs

@@ -77,6 +77,7 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
       NPi {} -> substEnv env n
       NUniv {} -> n
       NTyp (TypeConstr i sym args) -> mkTypeConstr i sym (map' (eval' env) args)
+      NPrim {} -> n
       NDyn {} -> n
       Closure {} -> n
 

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

@@ -97,6 +97,12 @@ mkTypeConstr i sym args = NTyp (TypeConstr i sym args)
 mkTypeConstr' :: Symbol -> [Type] -> Type
 mkTypeConstr' = mkTypeConstr Info.empty
 
+mkTypePrim :: Info -> Primitive -> Type
+mkTypePrim i p = NPrim (TypePrim i p)
+
+mkTypePrim' :: Primitive -> Type
+mkTypePrim' = mkTypePrim Info.empty
+
 mkDynamic :: Info -> Type
 mkDynamic i = NDyn (Dynamic i)
 
@@ -237,6 +243,8 @@ destruct = \case
     NodeDetails i [] [] [] (\i' _ -> mkUniv i' l)
   NTyp (TypeConstr i sym args) ->
     NodeDetails i args (map (const 0) args) (map (const []) args) (`mkTypeConstr` sym)
+  NPrim (TypePrim i prim) ->
+    NodeDetails i [] [] [] (\i' _ -> mkTypePrim i' prim)
   NDyn (Dynamic i) ->
     NodeDetails i [] [] [] (\i' _ -> mkDynamic i')
   Closure env (Lambda i b) ->

src/Juvix/Compiler/Core/Language.hs

@@ -1,6 +1,5 @@
 module Juvix.Compiler.Core.Language
   ( module Juvix.Compiler.Core.Language,
-    module Juvix.Compiler.Core.Language.Base,
     module Juvix.Compiler.Core.Language.Nodes,
   )
 where
@@ -9,7 +8,6 @@ where
   This file defines the tree representation of JuvixCore (Node datatype).
 -}
 
-import Juvix.Compiler.Core.Language.Base
 import Juvix.Compiler.Core.Language.Nodes
 
 {---------------------------------------------------------------------------------}
@@ -40,6 +38,8 @@ type Univ = Univ' Info
 
 type TypeConstr = TypeConstr' Info Node
 
+type TypePrim = TypePrim' Info
+
 type Dynamic = Dynamic' Info
 
 type CaseBranch = CaseBranch' Info Node
@@ -64,6 +64,7 @@ data Node
   | NPi {-# UNPACK #-} !Pi
   | NUniv {-# UNPACK #-} !Univ
   | NTyp {-# UNPACK #-} !TypeConstr
+  | NPrim {-# UNPACK #-} !TypePrim
   | NDyn !Dynamic -- Dynamic is already a newtype, so it's unpacked.
   | -- Evaluation only: `Closure env body`.
     Closure
@@ -107,5 +108,6 @@ instance HasAtomicity Node where
     NPi x -> atomicity x
     NUniv x -> atomicity x
     NTyp x -> atomicity x
+    NPrim x -> atomicity x
     NDyn x -> atomicity x
     Closure {} -> Aggregate lambdaFixity

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

@@ -1,6 +1,12 @@
-module Juvix.Compiler.Core.Language.Nodes where
+module Juvix.Compiler.Core.Language.Nodes
+  ( module Juvix.Compiler.Core.Language.Base,
+    module Juvix.Compiler.Core.Language.Primitives,
+    module Juvix.Compiler.Core.Language.Nodes,
+  )
+where
 
 import Juvix.Compiler.Core.Language.Base
+import Juvix.Compiler.Core.Language.Primitives
 
 {-------------------------------------------------------------------}
 {- Polymorphic Node types -}
@@ -98,6 +104,11 @@ data TypeConstr' i a = TypeConstr
     _typeConstrArgs :: ![a]
   }
 
+data TypePrim' i = TypePrim
+  { _typePrimInfo :: i,
+    _typePrimPrimitive :: Primitive
+  }
+
 -- | 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.
@@ -149,6 +160,9 @@ instance HasAtomicity (Pi' i a) where
 instance HasAtomicity (Univ' i) where
   atomicity _ = Atom
 
+instance HasAtomicity (TypePrim' i) where
+  atomicity _ = Atom
+
 instance HasAtomicity (TypeConstr' i a) where
   atomicity _ = Aggregate lambdaFixity
 
@@ -203,6 +217,9 @@ instance Eq (Univ' i) where
 instance Eq a => Eq (TypeConstr' i a) where
   (TypeConstr _ sym1 args1) == (TypeConstr _ sym2 args2) = sym1 == sym2 && args1 == args2
 
+instance Eq (TypePrim' i) where
+  (TypePrim _ p1) == (TypePrim _ p2) = p1 == p2
+
 instance Eq (Dynamic' i) where
   (Dynamic _) == (Dynamic _) = True
 

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

@@ -0,0 +1,30 @@
+module Juvix.Compiler.Core.Language.Primitives where
+
+{- This module defines JuvixCore primitive types. These do not necessarily
+correspond directly to builtins, but may serve as primitive representations of
+other types. For example, any type with two zero-argument constructors may be
+represented by booleans, any type isomorphic to unary natural numbers may be
+represented by integers with minimum value 0. -}
+
+import Juvix.Compiler.Core.Language.Base
+
+-- | Primitive type representation.
+data Primitive
+  = PrimInteger PrimIntegerInfo
+  | PrimBool PrimBoolInfo
+  | PrimString
+  deriving stock (Eq)
+
+-- | Info about a type represented as an integer.
+data PrimIntegerInfo = PrimIntegerInfo
+  { _infoMinValue :: Maybe Integer,
+    _infoMaxValue :: Maybe Integer
+  }
+  deriving stock (Eq)
+
+-- | Info about a type represented as a boolean.
+data PrimBoolInfo = PrimBoolInfo
+  { _infoTrueTag :: Tag,
+    _infoFalseTag :: Tag
+  }
+  deriving stock (Eq)

src/Juvix/Compiler/Core/Language/Stripped/Type.hs

@@ -1,8 +1,9 @@
 module Juvix.Compiler.Core.Language.Stripped.Type where
 
 import Juvix.Compiler.Core.Language.Base
+import Juvix.Compiler.Core.Language.Primitives
 
-data Type = TyDynamic | TyApp TypeApp | TyFun TypeFun
+data Type = TyDynamic | TyPrim Primitive | TyApp TypeApp | TyFun TypeFun
   deriving stock (Eq)
 
 data TypeApp = TypeApp

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

@@ -66,6 +66,12 @@ instance PrettyCode Tag where
     BuiltinTag tag -> ppCode tag
     UserTag tag -> return $ kwUnnamedConstr <> pretty tag
 
+instance PrettyCode Primitive where
+  ppCode = \case
+    PrimInteger _ -> return $ annotate (AnnKind KNameInductive) (pretty ("integer" :: String))
+    PrimBool _ -> return $ annotate (AnnKind KNameInductive) (pretty ("bool" :: String))
+    PrimString -> return $ annotate (AnnKind KNameInductive) (pretty ("string" :: String))
+
 ppCodeVar' :: Member (Reader Options) r => Maybe Name -> Var' i -> Sem r (Doc Ann)
 ppCodeVar' name v =
   case name of
@@ -214,6 +220,7 @@ instance PrettyCode Node where
           return $ kwLambda <> kwQuestion <+> b
     NUniv Univ {..} ->
       return $ kwType <+> pretty _univLevel
+    NPrim TypePrim {..} -> ppCode _typePrimPrimitive
     NTyp TypeConstr {..} -> do
       args' <- mapM (ppRightExpression appFixity) _typeConstrArgs
       n' <-