Rename builtin natural to nat and boolean to bool

docs/org/language-reference/builtins.org

@@ -6,7 +6,7 @@ Juvix has support for the built-in natural type and a few functions that are com
 1. Built-in inductive definitions.
 
    #+begin_example
-   builtin natural
+   builtin nat
    inductive Nat {
      zero : Nat;
      suc : Nat → Nat;
@@ -17,7 +17,7 @@ Juvix has support for the built-in natural type and a few functions that are com
 
    #+begin_example
    inifl 6 +;
-   builtin natural-plus
+   builtin nat-plus
    + : Nat → Nat → Nat;
    + zero b := b;
    + (suc a) b := suc (a + b);
@@ -26,6 +26,6 @@ Juvix has support for the built-in natural type and a few functions that are com
 3. Builtin axiom definitions.
 
    #+begin_example
-   builtin natural-print
+   builtin nat-print
    axiom printNat : Nat → Action;
    #+end_example

docs/org/notes/builtins.org

@@ -9,7 +9,7 @@ of definitions:
 
 1. Builtin inductive definitions. For example:
    #+begin_example
-   builtin natural
+   builtin nat
    inductive Nat {
      zero : Nat;
      suc : Nat → Nat;
@@ -20,15 +20,15 @@ of definitions:
 2. Builtin function definitions. For example:
    #+begin_src text
    inifl 6 +;
-   builtin natural-plus
+   builtin nat-plus
    + : Nat → Nat → Nat;
    + zero b := b;
    + (suc a) b := suc (a + b);
    #+end_src
 
 3. Builtin axiom definitions. For example:
    #+begin_src text
-   builtin natural-print
+   builtin nat-print
    axiom printNat : Nat → Action;
    #+end_src
 
@@ -40,7 +40,7 @@ collect information about the builtins that have been included in the code and
 what are the terms that refer to them. For instance, imagine that we find this
 definitions in a juvix module:
 #+begin_src text
-builtin natural
+builtin nat
 inductive MyNat {
     z : MyNat;
     s : MyNat → MyNat;

examples/milestone/ValidityPredicates/Data/Int/Ops.juvix

@@ -21,24 +21,22 @@ foreign c {
    \}
 };
 
-infix 4 <';
-axiom <' : Int → Int → BackendBool;
-compile <' {
+infix 4 <;
+axiom < : Int → Int → Bool;
+compile < {
   c ↦ "lessThan";
 };
 
-infix 4 <;
-< : Int → Int → Bool;
-< i1 i2 := from-backend-bool (i1 <' i2);
-
-axiom eqInt : Int → Int → BackendBool;
+axiom eqInt : Int → Int → Bool;
 compile eqInt {
   c ↦ "eqInt";
 };
 
 infix 4 ==;
-== : Int → Int → Bool;
-== i1 i2 := from-backend-bool (eqInt i1 i2);
+axiom == : Int → Int → Bool;
+compile == {
+  c ↦ "eqInt";
+};
 
 infixl 6 -;
 axiom - : Int -> Int -> Int;

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

@@ -243,17 +243,17 @@ registerBuiltinInductive ::
   BuiltinInductive ->
   Sem r ()
 registerBuiltinInductive d = \case
-  BuiltinNatural -> registerNaturalDef d
-  BuiltinBoolean -> registerBoolDef d
+  BuiltinNat -> registerNatDef d
+  BuiltinBool -> registerBoolDef d
 
 registerBuiltinFunction ::
   Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r =>
   Abstract.FunctionDef ->
   BuiltinFunction ->
   Sem r ()
 registerBuiltinFunction d = \case
-  BuiltinNaturalPlus -> registerNaturalPlus d
-  BuiltinBooleanIf -> registerIf d
+  BuiltinNatPlus -> registerNatPlus d
+  BuiltinBoolIf -> registerIf d
 
 registerBuiltinAxiom ::
   Members '[InfoTableBuilder, Error ScoperError, Builtins] r =>
@@ -263,7 +263,7 @@ registerBuiltinAxiom ::
 registerBuiltinAxiom d = \case
   BuiltinIO -> registerIO d
   BuiltinIOSequence -> registerIOSequence d
-  BuiltinNaturalPrint -> registerNaturalPrint d
+  BuiltinNatPrint -> registerNatPrint d
 
 goInductive ::
   Members '[InfoTableBuilder, Builtins, Error ScoperError] r =>

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

@@ -6,26 +6,26 @@ import Juvix.Prelude
 
 builtinConstructorName :: BuiltinConstructor -> Maybe Text
 builtinConstructorName = \case
-  BuiltinNaturalZero -> Just zero
-  BuiltinNaturalSuc -> Just suc
-  BuiltinBooleanTrue -> Just true_
-  BuiltinBooleanFalse -> Just false_
+  BuiltinNatZero -> Just zero
+  BuiltinNatSuc -> Just suc
+  BuiltinBoolTrue -> Just true_
+  BuiltinBoolFalse -> Just false_
 
 builtinInductiveName :: BuiltinInductive -> Maybe Text
 builtinInductiveName = \case
-  BuiltinNatural -> Just nat
-  BuiltinBoolean -> Just bool_
+  BuiltinNat -> Just nat
+  BuiltinBool -> Just bool_
 
 builtinAxiomName :: BuiltinAxiom -> Maybe Text
 builtinAxiomName = \case
-  BuiltinNaturalPrint -> Just printNat
+  BuiltinNatPrint -> Just printNat
   BuiltinIO -> Just io
   BuiltinIOSequence -> Just ioseq
 
 builtinFunctionName :: BuiltinFunction -> Maybe Text
 builtinFunctionName = \case
-  BuiltinNaturalPlus -> Just natplus
-  BuiltinBooleanIf -> Just boolif
+  BuiltinNatPlus -> Just natplus
+  BuiltinBoolIf -> Just boolif
 
 builtinName :: BuiltinPrim -> Maybe Text
 builtinName = \case

src/Juvix/Compiler/Builtins.hs

@@ -1,12 +1,12 @@
 module Juvix.Compiler.Builtins
   ( module Juvix.Compiler.Builtins.Effect,
-    module Juvix.Compiler.Builtins.Natural,
+    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.Natural
+import Juvix.Compiler.Builtins.Nat

src/Juvix/Compiler/Builtins/Base.hs

@@ -8,11 +8,11 @@ import Juvix.Prelude
 import Juvix.Prelude.Pretty
 
 data BuiltinsEnum
-  = BuiltinsNatural
+  = BuiltinsNat
   | BuiltinsZero
   | BuiltinsSuc
-  | BuiltinsNaturalPlus
-  | BuiltinsNaturalPrint
+  | BuiltinsNatPlus
+  | BuiltinsNatPrint
   | BuiltinsIO
   | BuiltinsIOSequence
   deriving stock (Show, Eq, Generic)
@@ -21,10 +21,10 @@ instance Hashable BuiltinsEnum
 
 instance Pretty BuiltinsEnum where
   pretty = \case
-    BuiltinsNatural -> Str.natural
+    BuiltinsNat -> Str.nat
     BuiltinsZero -> "zero"
     BuiltinsSuc -> "suc"
-    BuiltinsNaturalPlus -> Str.naturalPlus
-    BuiltinsNaturalPrint -> Str.naturalPrint
+    BuiltinsNatPlus -> Str.natPlus
+    BuiltinsNatPrint -> Str.natPrint
     BuiltinsIO -> Str.io
     BuiltinsIOSequence -> Str.ioSequence

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/Builtins/Natural.hs → src/Juvix/Compiler/Builtins/Nat.hs

@@ -1,4 +1,4 @@
-module Juvix.Compiler.Builtins.Natural where
+module Juvix.Compiler.Builtins.Nat where
 
 import Data.HashSet qualified as HashSet
 import Juvix.Compiler.Abstract.Extra
@@ -7,47 +7,47 @@ import Juvix.Compiler.Builtins.Effect
 import Juvix.Data.Effect.NameIdGen
 import Juvix.Prelude
 
-registerNaturalDef :: Member Builtins r => InductiveDef -> Sem r ()
-registerNaturalDef d = do
-  unless (null (d ^. inductiveParameters)) (error "Naturals should have no type parameters")
-  unless (isSmallUniverse' (d ^. inductiveType)) (error "Naturals should be in the small universe")
-  registerBuiltin BuiltinNatural (d ^. inductiveName)
+registerNatDef :: Member Builtins r => InductiveDef -> Sem r ()
+registerNatDef d = do
+  unless (null (d ^. inductiveParameters)) (error "Nats should have no type parameters")
+  unless (isSmallUniverse' (d ^. inductiveType)) (error "Nats should be in the small universe")
+  registerBuiltin BuiltinNat (d ^. inductiveName)
   case d ^. inductiveConstructors of
     [c1, c2] -> registerZero c1 >> registerSuc c2
-    _ -> error "Natural numbers should have exactly two constructors"
+    _ -> error "Nat numbers should have exactly two constructors"
 
 registerZero :: Member Builtins r => InductiveConstructorDef -> Sem r ()
 registerZero d@InductiveConstructorDef {..} = do
   let zero = _constructorName
       ty = _constructorType
-  nat <- getBuiltinName (getLoc d) BuiltinNatural
+  nat <- getBuiltinName (getLoc d) BuiltinNat
   unless (ty === nat) (error $ "zero has the wrong type " <> ppTrace ty <> " | " <> ppTrace nat)
-  registerBuiltin BuiltinNaturalZero zero
+  registerBuiltin BuiltinNatZero zero
 
 registerSuc :: Member Builtins r => InductiveConstructorDef -> Sem r ()
 registerSuc d@InductiveConstructorDef {..} = do
   let suc = _constructorName
       ty = _constructorType
-  nat <- getBuiltinName (getLoc d) BuiltinNatural
+  nat <- getBuiltinName (getLoc d) BuiltinNat
   unless (ty === (nat --> nat)) (error "suc has the wrong type")
-  registerBuiltin BuiltinNaturalSuc suc
+  registerBuiltin BuiltinNatSuc suc
 
-registerNaturalPrint :: Members '[Builtins] r => AxiomDef -> Sem r ()
-registerNaturalPrint f = do
-  nat <- getBuiltinName (getLoc f) BuiltinNatural
+registerNatPrint :: Members '[Builtins] r => AxiomDef -> Sem r ()
+registerNatPrint f = do
+  nat <- getBuiltinName (getLoc f) BuiltinNat
   io <- getBuiltinName (getLoc f) BuiltinIO
-  unless (f ^. axiomType === (nat --> io)) (error "Natural print has the wrong type signature")
-  registerBuiltin BuiltinNaturalPrint (f ^. axiomName)
+  unless (f ^. axiomType === (nat --> io)) (error "Nat print has the wrong type signature")
+  registerBuiltin BuiltinNatPrint (f ^. axiomName)
 
-registerNaturalPlus :: Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
-registerNaturalPlus f = do
-  nat <- getBuiltinName (getLoc f) BuiltinNatural
-  zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNaturalZero
-  suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNaturalSuc
+registerNatPlus :: Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerNatPlus f = do
+  nat <- getBuiltinName (getLoc f) BuiltinNat
+  zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatZero
+  suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc
   let plus = f ^. funDefName
       ty = f ^. funDefTypeSig
-  unless (ty === (nat --> nat --> nat)) (error "Natural plus has the wrong type signature")
-  registerBuiltin BuiltinNaturalPlus plus
+  unless (ty === (nat --> nat --> nat)) (error "Nat plus has the wrong type signature")
+  registerBuiltin BuiltinNatPlus plus
   varn <- freshVar "n"
   varm <- freshVar "m"
   let n = toExpression varn
@@ -67,7 +67,7 @@ registerNaturalPlus f = do
           | c <- toList (f ^. funDefClauses)
         ]
   case zipExactMay exClauses clauses of
-    Nothing -> error "Natural plus has the wrong number of clauses"
+    Nothing -> error "Nat plus 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)