Fix Nat builtins

c-runtime/builtins/nat.h

@@ -21,6 +21,8 @@ prim_nat prim_natsub(prim_nat a, prim_nat b) { return a - b; }
 
 prim_nat prim_natmul(prim_nat a, prim_nat b) { return a * b; }
 
+prim_nat prim_natudiv(prim_nat a, prim_nat b) { return (a + b - 1) / b; }
+
 prim_nat prim_natdiv(prim_nat a, prim_nat b) { return a / b; }
 
 prim_nat prim_natmod(prim_nat a, prim_nat b) { return a % b; }

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

@@ -250,6 +250,7 @@ registerBuiltinFunction d = \case
   BuiltinNatPlus -> registerNatPlus d
   BuiltinNatSub -> registerNatSub d
   BuiltinNatMul -> registerNatMul d
+  BuiltinNatUDiv -> registerNatUDiv d
   BuiltinNatDiv -> registerNatDiv d
   BuiltinNatMod -> registerNatMod d
   BuiltinNatLe -> registerNatLe d

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

@@ -30,6 +30,7 @@ builtinFunctionName = \case
   BuiltinNatPlus -> Just natplus
   BuiltinNatSub -> Just natsub
   BuiltinNatMul -> Just natmul
+  BuiltinNatUDiv -> Just natudiv
   BuiltinNatDiv -> Just natdiv
   BuiltinNatMod -> Just natmod
   BuiltinNatLe -> Just natle

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

@@ -53,6 +53,9 @@ natsub = primPrefix "natsub"
 natmul :: Text
 natmul = primPrefix "natmul"
 
+natudiv :: Text
+natudiv = primPrefix "natudiv"
+
 natdiv :: Text
 natdiv = primPrefix "natdiv"
 

src/Juvix/Compiler/Builtins/Nat.hs

@@ -126,8 +126,8 @@ registerNatSub f = do
         ]
   registerNatFun f BuiltinNatSub (nat --> nat --> nat) exClauses [varn, varm]
 
-registerNatDiv :: Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
-registerNatDiv f = do
+registerNatUDiv :: Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerNatUDiv f = do
   nat <- getBuiltinName (getLoc f) BuiltinNat
   zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatZero
   suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc
@@ -145,6 +145,25 @@ registerNatDiv f = do
         [ (zero ./. h, zero),
           (n ./. m, suc @@ ((sub @@ n @@ m) ./. m))
         ]
+  registerNatFun f BuiltinNatUDiv (nat --> nat --> nat) exClauses [varn, varm]
+
+registerNatDiv :: Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
+registerNatDiv f = do
+  nat <- getBuiltinName (getLoc f) BuiltinNat
+  suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc
+  udiv <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatUDiv
+  sub <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSub
+  let divop = f ^. funDefName
+  varn <- freshVar "n"
+  varm <- freshVar "m"
+  let n = toExpression varn
+      m = toExpression varm
+      (./.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
+      x ./. y = divop @@ x @@ y
+      exClauses :: [(Expression, Expression)]
+      exClauses =
+        [ (n ./. m, udiv @@ (sub @@ (suc @@ n) @@ m) @@ m)
+        ]
   registerNatFun f BuiltinNatDiv (nat --> nat --> nat) exClauses [varn, varm]
 
 registerNatMod :: Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()

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

@@ -65,6 +65,7 @@ data BuiltinFunction
   = BuiltinNatPlus
   | BuiltinNatSub
   | BuiltinNatMul
+  | BuiltinNatUDiv
   | BuiltinNatDiv
   | BuiltinNatMod
   | BuiltinNatLe
@@ -80,6 +81,7 @@ instance Pretty BuiltinFunction where
     BuiltinNatPlus -> Str.natPlus
     BuiltinNatSub -> Str.natSub
     BuiltinNatMul -> Str.natMul
+    BuiltinNatUDiv -> Str.natUDiv
     BuiltinNatDiv -> Str.natDiv
     BuiltinNatMod -> Str.natMod
     BuiltinNatLe -> Str.natLe

src/Juvix/Compiler/Core/Transformation/NatToInt.hs

@@ -22,19 +22,18 @@ convertNode tab = convert [] 0
         | Just _identSymbol == tab ^. infoIntToNat ->
             End' (convert levels bl l)
       NApp (App _ (NApp (App _ (NIdt (Ident {..})) l)) r) ->
-        Recur' (levels, convertIdentApp node (\op g -> g $ mkBuiltinApp _identInfo op [l, r]) _identSymbol)
+        Recur' (levels, convertIdentApp node (\g -> g _identInfo l r) _identSymbol)
       NApp (App _ (NIdt (Ident {..})) l) ->
-        Recur' (levels, convertIdentApp node (\op g -> mkLet' l $ mkLambdaTy mkTypeInteger' $ g $ mkBuiltinApp _identInfo op [mkVar' 1, mkVar' 0]) _identSymbol)
+        Recur' (levels, convertIdentApp node (\g -> mkLet' l $ mkLambdaTy mkTypeInteger' $ g _identInfo (mkVar' 1) (mkVar' 0)) _identSymbol)
       NIdt (Ident {..}) ->
         Recur'
           ( levels,
             convertIdentApp
               node
-              ( \op g ->
+              ( \g ->
                   mkLambdaTy mkTypeInteger' $
                     mkLambdaTy mkTypeInteger' $
-                      g $
-                        mkBuiltinApp _identInfo op [mkVar' 1, mkVar' 0]
+                      g _identInfo (mkVar' 1) (mkVar' 0)
               )
               _identSymbol
           )
@@ -87,16 +86,15 @@ convertNode tab = convert [] 0
           maybeBranch = fromMaybe (mkBuiltinApp' OpFail [mkConstant' (ConstString "no matching branch")])
       _ -> Recur' (levels, node)
 
-    convertIdentApp :: Node -> (BuiltinOp -> (Node -> Node) -> Node) -> Symbol -> Node
+    convertIdentApp :: Node -> ((Info -> Node -> Node -> Node) -> Node) -> Symbol -> Node
     convertIdentApp node f sym =
       let ii = fromJust $ HashMap.lookup sym (tab ^. infoIdentifiers)
        in case ii ^. identifierBuiltin of
-            Just BuiltinNatPlus -> f OpIntAdd id
+            Just BuiltinNatPlus -> f (\info x y -> mkBuiltinApp info OpIntAdd [x, y])
             Just BuiltinNatSub ->
               f
-                OpIntSub
-                ( \node' ->
-                    mkLet' node' $
+                ( \info x y ->
+                    mkLet' (mkBuiltinApp info OpIntSub [x, y]) $
                       mkIf'
                         boolSymbol
                         (mkBuiltinApp' OpIntLe [mkConstant' (ConstInteger 0), mkVar' 0])
@@ -106,12 +104,17 @@ convertNode tab = convert [] 0
               where
                 boolSymbol =
                   fromJust (HashMap.lookup (BuiltinTag TagTrue) (tab ^. infoConstructors)) ^. constructorInductive
-            Just BuiltinNatMul -> f OpIntMul id
-            Just BuiltinNatDiv -> f OpIntDiv id
-            Just BuiltinNatMod -> f OpIntMod id
-            Just BuiltinNatLe -> f OpIntLe id
-            Just BuiltinNatLt -> f OpIntLt id
-            Just BuiltinNatEq -> f OpEq id
+            Just BuiltinNatMul -> f (\info x y -> mkBuiltinApp info OpIntAdd [x, y])
+            Just BuiltinNatUDiv ->
+              f
+                ( \info x y ->
+                    mkBuiltinApp info OpIntDiv [mkBuiltinApp' OpIntAdd [x, mkBuiltinApp' OpIntSub [y, mkConstant' (ConstInteger 1)]], y]
+                )
+            Just BuiltinNatDiv -> f (\info x y -> mkBuiltinApp info OpIntAdd [x, y])
+            Just BuiltinNatMod -> f (\info x y -> mkBuiltinApp info OpIntAdd [x, y])
+            Just BuiltinNatLe -> f (\info x y -> mkBuiltinApp info OpIntAdd [x, y])
+            Just BuiltinNatLt -> f (\info x y -> mkBuiltinApp info OpIntAdd [x, y])
+            Just BuiltinNatEq -> f (\info x y -> mkBuiltinApp info OpIntAdd [x, y])
             _ -> node
 
 natToInt :: InfoTable -> InfoTable

src/Juvix/Extra/Strings.hs

@@ -122,6 +122,9 @@ natSub = "nat-sub"
 natMul :: IsString s => s
 natMul = "nat-mul"
 
+natUDiv :: IsString s => s
+natUDiv = "nat-udiv"
+
 natDiv :: IsString s => s
 natDiv = "nat-div"