boolean operators

include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix

@@ -7,10 +7,10 @@ trait
 type Natural A :=
   mkNatural {
     syntax operator + additive;
-    {-# isabelle-operator: {name: "+", prec: 10, assoc: left} #-}
+    {-# isabelle-operator: {name: "+", prec: 65, assoc: left} #-}
     + : A -> A -> A;
     syntax operator * multiplicative;
-    {-# isabelle-operator: {name: "*", prec: 11, assoc: left} #-}
+    {-# isabelle-operator: {name: "*", prec: 70, assoc: left} #-}
     * : A -> A -> A;
     builtin from-nat
     fromNat : Nat -> A

juvix-stdlib

@@ -1 +1 @@
-Subproject commit 5f0e487ab212c3c5bc9fc13e8f879fb514a20879
+Subproject commit b845bb0757ade52953a1b7245b0f0b5fcf11990d

src/Juvix/Compiler/Backend/Isabelle/Language.hs

@@ -242,7 +242,23 @@ letFixity =
 consFixity :: Fixity
 consFixity =
   Fixity
-    { _fixityPrecedence = PrecNat 20,
+    { _fixityPrecedence = PrecNat 80,
+      _fixityArity = OpBinary AssocRight,
+      _fixityId = Nothing
+    }
+
+andFixity :: Fixity
+andFixity =
+  Fixity
+    { _fixityPrecedence = PrecNat 35,
+      _fixityArity = OpBinary AssocRight,
+      _fixityId = Nothing
+    }
+
+orFixity :: Fixity
+orFixity =
+  Fixity
+    { _fixityPrecedence = PrecNat 30,
       _fixityArity = OpBinary AssocRight,
       _fixityId = Nothing
     }

src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs

@@ -339,6 +339,17 @@ goModule onlyTypes infoTable Internal.Module {..} =
               br1' <- goExpression br1
               br2' <- goExpression br2
               return $ ExprIf $ If val' br1' br2'
+          | Just (op, fixity, arg1, arg2) <- getBoolOperator app = do
+              arg1' <- goExpression arg1
+              arg2' <- goExpression arg2
+              return $
+                ExprBinop
+                  Binop
+                    { _binopOperator = op,
+                      _binopLeft = arg1',
+                      _binopRight = arg2',
+                      _binopFixity = fixity
+                    }
           | Just (x, y) <- getPair app = do
               x' <- goExpression x
               y' <- goExpression y
@@ -464,6 +475,24 @@ goModule onlyTypes infoTable Internal.Module {..} =
           where
             (fn, args) = Internal.unfoldApplication app
 
+        getBoolOperator :: Internal.Application -> Maybe (Name, Fixity, Internal.Expression, Internal.Expression)
+        getBoolOperator app = case fn of
+          Internal.ExpressionIden (Internal.IdenFunction name) ->
+            case HashMap.lookup name (infoTable ^. Internal.infoFunctions) of
+              Just funInfo ->
+                case funInfo ^. Internal.functionInfoBuiltin of
+                  Just Internal.BuiltinBoolAnd
+                    | (arg1 :| [arg2]) <- args ->
+                        Just (defaultName "∧", andFixity, arg1, arg2)
+                  Just Internal.BuiltinBoolOr
+                    | (arg1 :| [arg2]) <- args ->
+                        Just (defaultName "∨", orFixity, arg1, arg2)
+                  _ -> Nothing
+              Nothing -> Nothing
+          _ -> Nothing
+          where
+            (fn, args) = Internal.unfoldApplication app
+
         getPair :: Internal.Application -> Maybe (Internal.Expression, Internal.Expression)
         getPair app = case fn of
           Internal.ExpressionIden (Internal.IdenConstructor name) ->