From 16b6a64353790f5a507c91df612cb30d0fec1abd Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Fri, 14 Oct 2022 12:54:56 +0100 Subject: [PATCH] Rename builtin boolean to bool --- juvix-stdlib | 2 +- .../Abstract/Translation/FromConcrete.hs | 4 ++-- .../Compiler/Backend/C/Data/BuiltinTable.hs | 8 +++---- src/Juvix/Compiler/Builtins.hs | 4 ++-- .../Compiler/Builtins/{Boolean.hs => Bool.hs} | 24 +++++++++---------- src/Juvix/Compiler/Concrete/Data/Builtins.hs | 14 +++++------ src/Juvix/Extra/Strings.hs | 8 +++---- test/Scope/Positive.hs | 2 +- tests/positive/BuiltinsBool.juvix | 4 ++-- tests/positive/MiniC/Builtins/Input.juvix | 4 ++-- 10 files changed, 37 insertions(+), 37 deletions(-) rename src/Juvix/Compiler/Builtins/{Boolean.hs => Bool.hs} (80%) diff --git a/juvix-stdlib b/juvix-stdlib index 2b86d05f18..b0109d1dd9 160000 --- a/juvix-stdlib +++ b/juvix-stdlib @@ -1 +1 @@ -Subproject commit 2b86d05f1874d51b9677d90c634366a57dd36c9b +Subproject commit b0109d1dd9bc477906e93d240800c5c31195c972 diff --git a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs index d17fce1ef1..2cae90b16f 100644 --- a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs +++ b/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 => diff --git a/src/Juvix/Compiler/Backend/C/Data/BuiltinTable.hs b/src/Juvix/Compiler/Backend/C/Data/BuiltinTable.hs index 07b003732a..4e20ad1598 100644 --- a/src/Juvix/Compiler/Backend/C/Data/BuiltinTable.hs +++ b/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 diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs index 2b5a64e8d6..cf36a50d6d 100644 --- a/src/Juvix/Compiler/Builtins.hs +++ b/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 diff --git a/src/Juvix/Compiler/Builtins/Boolean.hs b/src/Juvix/Compiler/Builtins/Bool.hs similarity index 80% rename from src/Juvix/Compiler/Builtins/Boolean.hs rename to src/Juvix/Compiler/Builtins/Bool.hs index 47342cf74e..a725fcb1e3 100644 --- a/src/Juvix/Compiler/Builtins/Boolean.hs +++ b/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) diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs index 0c0275f449..e124c1ac84 100644 --- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs +++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs @@ -38,11 +38,11 @@ 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 @@ -50,20 +50,20 @@ 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 @@ -71,7 +71,7 @@ instance Hashable BuiltinFunction instance Pretty BuiltinFunction where pretty = \case BuiltinNatPlus -> Str.natPlus - BuiltinBooleanIf -> Str.booleanIf + BuiltinBoolIf -> Str.boolIf data BuiltinAxiom = BuiltinNatPrint diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index a860349162..4b53f174a6 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/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" diff --git a/test/Scope/Positive.hs b/test/Scope/Positive.hs index 5ac18959d4..099cffbcad 100644 --- a/test/Scope/Positive.hs +++ b/test/Scope/Positive.hs @@ -205,7 +205,7 @@ tests = StdlibInclude "Symbols.juvix", PosTest - "Builtin boolean" + "Builtin bool" "." StdlibExclude "BuiltinsBool.juvix" diff --git a/tests/positive/BuiltinsBool.juvix b/tests/positive/BuiltinsBool.juvix index 8f85525c09..cca3ffb994 100644 --- a/tests/positive/BuiltinsBool.juvix +++ b/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; diff --git a/tests/positive/MiniC/Builtins/Input.juvix b/tests/positive/MiniC/Builtins/Input.juvix index 1fd7156851..c03c779700 100644 --- a/tests/positive/MiniC/Builtins/Input.juvix +++ b/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;