Rename builtin boolean to bool

src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs

@@ -244,7 +244,7 @@ registerBuiltinInductive ::
   Sem r ()
 registerBuiltinInductive d = \case
   BuiltinNat -> registerNatDef d
-  BuiltinBoolean -> registerBoolDef d
+  BuiltinBool -> registerBoolDef d
 
 registerBuiltinFunction ::
   Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r =>
@@ -253,7 +253,7 @@ registerBuiltinFunction ::
   Sem r ()
 registerBuiltinFunction d = \case
   BuiltinNatPlus -> registerNatPlus d
-  BuiltinBooleanIf -> registerIf d
+  BuiltinBoolIf -> registerIf d
 
 registerBuiltinAxiom ::
   Members '[InfoTableBuilder, Error ScoperError, Builtins] r =>

src/Juvix/Compiler/Backend/C/Data/BuiltinTable.hs

@@ -8,13 +8,13 @@ builtinConstructorName :: BuiltinConstructor -> Maybe Text
 builtinConstructorName = \case
   BuiltinNatZero -> Just zero
   BuiltinNatSuc -> Just suc
-  BuiltinBooleanTrue -> Just true_
-  BuiltinBooleanFalse -> Just false_
+  BuiltinBoolTrue -> Just true_
+  BuiltinBoolFalse -> Just false_
 
 builtinInductiveName :: BuiltinInductive -> Maybe Text
 builtinInductiveName = \case
   BuiltinNat -> Just nat
-  BuiltinBoolean -> Just bool_
+  BuiltinBool -> Just bool_
 
 builtinAxiomName :: BuiltinAxiom -> Maybe Text
 builtinAxiomName = \case
@@ -25,7 +25,7 @@ builtinAxiomName = \case
 builtinFunctionName :: BuiltinFunction -> Maybe Text
 builtinFunctionName = \case
   BuiltinNatPlus -> Just natplus
-  BuiltinBooleanIf -> Just boolif
+  BuiltinBoolIf -> Just boolif
 
 builtinName :: BuiltinPrim -> Maybe Text
 builtinName = \case

src/Juvix/Compiler/Builtins.hs

@@ -2,11 +2,11 @@ module Juvix.Compiler.Builtins
   ( module Juvix.Compiler.Builtins.Effect,
     module Juvix.Compiler.Builtins.Nat,
     module Juvix.Compiler.Builtins.IO,
-    module Juvix.Compiler.Builtins.Boolean,
+    module Juvix.Compiler.Builtins.Bool,
   )
 where
 
-import Juvix.Compiler.Builtins.Boolean
+import Juvix.Compiler.Builtins.Bool
 import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Builtins.IO
 import Juvix.Compiler.Builtins.Nat

src/Juvix/Compiler/Builtins/Boolean.hs → src/Juvix/Compiler/Builtins/Bool.hs

@@ -1,4 +1,4 @@
-module Juvix.Compiler.Builtins.Boolean where
+module Juvix.Compiler.Builtins.Bool where
 
 import Data.HashSet qualified as HashSet
 import Juvix.Compiler.Abstract.Extra
@@ -10,7 +10,7 @@ registerBoolDef :: Member Builtins r => InductiveDef -> Sem r ()
 registerBoolDef d = do
   unless (null (d ^. inductiveParameters)) (error "Bool should have no type parameters")
   unless (isSmallUniverse' (d ^. inductiveType)) (error "Bool should be in the small universe")
-  registerBuiltin BuiltinBoolean (d ^. inductiveName)
+  registerBuiltin BuiltinBool (d ^. inductiveName)
   case d ^. inductiveConstructors of
     [c1, c2] -> registerTrue c1 >> registerFalse c2
     _ -> error "Bool should have exactly two constructors"
@@ -19,30 +19,30 @@ registerTrue :: Member Builtins r => InductiveConstructorDef -> Sem r ()
 registerTrue d@InductiveConstructorDef {..} = do
   let ctorTrue = _constructorName
       ctorTy = _constructorType
-  boolTy <- getBuiltinName (getLoc d) BuiltinBoolean
+  boolTy <- getBuiltinName (getLoc d) BuiltinBool
   unless (ctorTy === boolTy) (error $ "true has the wrong type " <> ppTrace ctorTy <> " | " <> ppTrace boolTy)
-  registerBuiltin BuiltinBooleanTrue ctorTrue
+  registerBuiltin BuiltinBoolTrue ctorTrue
 
 registerFalse :: Member Builtins r => InductiveConstructorDef -> Sem r ()
 registerFalse d@InductiveConstructorDef {..} = do
   let ctorFalse = _constructorName
       ctorTy = _constructorType
-  boolTy <- getBuiltinName (getLoc d) BuiltinBoolean
+  boolTy <- getBuiltinName (getLoc d) BuiltinBool
   unless (ctorTy === boolTy) (error $ "false has the wrong type " <> ppTrace ctorTy <> " | " <> ppTrace boolTy)
-  registerBuiltin BuiltinBooleanFalse ctorFalse
+  registerBuiltin BuiltinBoolFalse ctorFalse
 
 registerIf :: Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
 registerIf f = do
-  boolean <- getBuiltinName (getLoc f) BuiltinBoolean
-  true_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBooleanTrue
-  false_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBooleanFalse
+  bool <- getBuiltinName (getLoc f) BuiltinBool
+  true_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolTrue
+  false_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse
   vart <- freshVar "t"
   let if_ = f ^. funDefName
       ty = f ^. funDefTypeSig
       freeTVars = HashSet.fromList [vart]
       u = ExpressionUniverse (Universe {_universeLevel = Nothing, _universeLoc = error "Universe with no location"})
-  unless (((u <>--> boolean --> vart --> vart --> vart) ==% ty) freeTVars) (error "Boolean if has the wrong type signature")
-  registerBuiltin BuiltinBooleanIf if_
+  unless (((u <>--> bool --> vart --> vart --> vart) ==% ty) freeTVars) (error "Bool if has the wrong type signature")
+  registerBuiltin BuiltinBoolIf if_
   vare <- freshVar "e"
   hole <- freshHole
   let e = toExpression vare
@@ -60,7 +60,7 @@ registerIf f = do
           | c <- toList (f ^. funDefClauses)
         ]
   case zipExactMay exClauses clauses of
-    Nothing -> error "Boolean if has the wrong number of clauses"
+    Nothing -> error "Bool if has the wrong number of clauses"
     Just z -> forM_ z $ \((exLhs, exBody), (lhs, body)) -> do
       unless (exLhs =% lhs) (error "clause lhs does not match")
       unless (exBody =% body) (error $ "clause body does not match " <> ppTrace exBody <> " | " <> ppTrace body)

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -38,40 +38,40 @@ instance Pretty BuiltinPrim where
 builtinConstructors :: BuiltinInductive -> [BuiltinConstructor]
 builtinConstructors = \case
   BuiltinNat -> [BuiltinNatZero, BuiltinNatSuc]
-  BuiltinBoolean -> [BuiltinBooleanTrue, BuiltinBooleanFalse]
+  BuiltinBool -> [BuiltinBoolTrue, BuiltinBoolFalse]
 
 data BuiltinInductive
   = BuiltinNat
-  | BuiltinBoolean
+  | BuiltinBool
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic)
 
 instance Hashable BuiltinInductive
 
 instance Pretty BuiltinInductive where
   pretty = \case
     BuiltinNat -> Str.nat
-    BuiltinBoolean -> Str.boolean_
+    BuiltinBool -> Str.bool_
 
 data BuiltinConstructor
   = BuiltinNatZero
   | BuiltinNatSuc
-  | BuiltinBooleanTrue
-  | BuiltinBooleanFalse
+  | BuiltinBoolTrue
+  | BuiltinBoolFalse
   deriving stock (Show, Eq, Ord, Generic)
 
 instance Hashable BuiltinConstructor
 
 data BuiltinFunction
   = BuiltinNatPlus
-  | BuiltinBooleanIf
+  | BuiltinBoolIf
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic)
 
 instance Hashable BuiltinFunction
 
 instance Pretty BuiltinFunction where
   pretty = \case
     BuiltinNatPlus -> Str.natPlus
-    BuiltinBooleanIf -> Str.booleanIf
+    BuiltinBoolIf -> Str.boolIf
 
 data BuiltinAxiom
   = BuiltinNatPrint

src/Juvix/Extra/Strings.hs

@@ -92,8 +92,8 @@ string = "string"
 nat :: IsString s => s
 nat = "nat"
 
-boolean_ :: IsString s => s
-boolean_ = "boolean"
+bool_ :: IsString s => s
+bool_ = "bool"
 
 io :: IsString s => s
 io = "IO"
@@ -107,8 +107,8 @@ natPrint = "nat-print"
 natPlus :: IsString s => s
 natPlus = "nat-plus"
 
-booleanIf :: IsString s => s
-booleanIf = "boolean-if"
+boolIf :: IsString s => s
+boolIf = "bool-if"
 
 builtin :: IsString s => s
 builtin = "builtin"

test/Scope/Positive.hs

@@ -205,7 +205,7 @@ tests =
       StdlibInclude
       "Symbols.juvix",
     PosTest
-      "Builtin boolean"
+      "Builtin bool"
       "."
       StdlibExclude
       "BuiltinsBool.juvix"

tests/positive/BuiltinsBool.juvix

@@ -1,12 +1,12 @@
 module BuiltinsBool;
 
-builtin boolean
+builtin bool
 inductive Bool {
   true : Bool;
   false : Bool;
 };
 
-builtin boolean-if
+builtin bool-if
 if : {A : Type} → Bool → A → A → A;
 if true t _ := t;
 if false _ e := e;

tests/positive/MiniC/Builtins/Input.juvix

@@ -1,12 +1,12 @@
 module Input;
 
-builtin boolean
+builtin bool
 inductive Bool {
   true : Bool;
   false : Bool;
 };
 
-builtin boolean-if
+builtin bool-if
 if : {A : Type} → Bool → A → A → A;
 if true t _ := t;
 if false _ e := e;