bugfixes

src/Juvix/Compiler/Core/Data/TransformationId.hs

@@ -6,5 +6,6 @@ data TransformationId
   = LambdaLifting
   | TopEtaExpand
   | RemoveTypeArgs
+  | NatToInt
   | Identity
   deriving stock (Data)

src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs

@@ -45,6 +45,7 @@ pcompletions = do
       TopEtaExpand -> strTopEtaExpand
       Identity -> strIdentity
       RemoveTypeArgs -> strRemoveTypeArgs
+      NatToInt -> strNatToInt
 
 lexeme :: MonadParsec e Text m => m a -> m a
 lexeme = L.lexeme L.hspace
@@ -61,6 +62,7 @@ transformation =
     <|> symbol strIdentity $> Identity
     <|> symbol strTopEtaExpand $> TopEtaExpand
     <|> symbol strRemoveTypeArgs $> RemoveTypeArgs
+    <|> symbol strNatToInt $> NatToInt
 
 allStrings :: [Text]
 allStrings =
@@ -81,3 +83,6 @@ strIdentity = "identity"
 
 strRemoveTypeArgs :: Text
 strRemoveTypeArgs = "remove-type-args"
+
+strNatToInt :: Text
+strNatToInt = "nat-to-int"

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -158,20 +158,32 @@ ppCodeLet' name mty lt = do
   return $ kwLet <+> n' <> tty <+> kwAssign <+> v' <+> kwIn <> line <> b'
 
 ppCodeCase' :: (PrettyCode a, Member (Reader Options) r) => [[Text]] -> [Text] -> Case' i bi a -> Sem r (Doc Ann)
-ppCodeCase' branchBinderNames branchTagNames Case {..} = do
-  let branchBodies = map (^. caseBranchBody) _caseBranches
-  bns <- mapM (mapM (ppName KNameLocal)) branchBinderNames
-  cns <- mapM (ppName KNameConstructor) branchTagNames
-  v <- ppCode _caseValue
-  bs' <- sequence $ zipWith3Exact (\cn bn br -> ppCode br >>= \br' -> return $ foldl' (<+>) cn bn <+> kwAssign <+> br') cns bns branchBodies
-  bs'' <-
-    case _caseDefault of
-      Just def -> do
-        d' <- ppCode def
-        return $ bs' ++ [kwDefault <+> kwAssign <+> d']
-      Nothing -> return bs'
-  let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs''
-  return $ kwCase <+> v <+> kwOf <+> bss
+ppCodeCase' branchBinderNames branchTagNames Case {..} =
+  case _caseBranches of
+    [CaseBranch _ (BuiltinTag TagTrue) _ _ br1, CaseBranch _ (BuiltinTag TagTrue) _ _ br2] -> do
+      br1' <- ppCode br1
+      br2' <- ppCode br2
+      v <- ppCode _caseValue
+      return $ kwIf <+> v <+> kwThen <+> br1' <+> kwElse <+> br2'
+    [CaseBranch _ (BuiltinTag TagTrue) _ _ br1] | isJust _caseDefault -> do
+      br1' <- ppCode br1
+      br2' <- ppCode (fromJust _caseDefault)
+      v <- ppCode _caseValue
+      return $ kwIf <+> v <+> kwThen <+> br1' <+> kwElse <+> br2'
+    _ -> do
+      let branchBodies = map (^. caseBranchBody) _caseBranches
+      bns <- mapM (mapM (ppName KNameLocal)) branchBinderNames
+      cns <- mapM (ppName KNameConstructor) branchTagNames
+      v <- ppCode _caseValue
+      bs' <- sequence $ zipWith3Exact (\cn bn br -> ppCode br >>= \br' -> return $ foldl' (<+>) cn bn <+> kwAssign <+> br') cns bns branchBodies
+      bs'' <-
+        case _caseDefault of
+          Just def -> do
+            d' <- ppCode def
+            return $ bs' ++ [kwDefault <+> kwAssign <+> d']
+          Nothing -> return bs'
+      let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs''
+      return $ kwCase <+> v <+> kwOf <+> bss
 
 instance PrettyCode PatternWildcard where
   ppCode _ = return kwWildcard
@@ -505,6 +517,15 @@ kwMatch = keyword Str.match_
 kwWith :: Doc Ann
 kwWith = keyword Str.with_
 
+kwIf :: Doc Ann
+kwIf = keyword Str.if_
+
+kwThen :: Doc Ann
+kwThen = keyword Str.then_
+
+kwElse :: Doc Ann
+kwElse = keyword Str.else_
+
 kwDefault :: Doc Ann
 kwDefault = keyword Str.underscore
 

src/Juvix/Compiler/Core/Transformation.hs

@@ -14,6 +14,7 @@ import Juvix.Compiler.Core.Transformation.Eta
 import Juvix.Compiler.Core.Transformation.Identity
 import Juvix.Compiler.Core.Transformation.LambdaLifting
 import Juvix.Compiler.Core.Transformation.RemoveTypeArgs
+import Juvix.Compiler.Core.Transformation.NatToInt
 import Juvix.Compiler.Core.Transformation.TopEtaExpand
 
 applyTransformations :: [TransformationId] -> InfoTable -> InfoTable
@@ -25,3 +26,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
       Identity -> identity
       TopEtaExpand -> topEtaExpand
       RemoveTypeArgs -> removeTypeArgs
+      NatToInt -> natToInt

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

@@ -1,14 +1,17 @@
 module Juvix.Compiler.Core.Transformation.NatToInt (natToInt) where
 
+import Data.List qualified as List
 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Transformation.Base
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.NameInfo
 
 convertNode :: InfoTable -> Node -> Node
 convertNode tab = convert [] 0
   where
     convert :: [Level] -> Level -> Node -> Node
-    convert levels bl = dmapCNR' (bl, go) levels
+    convert levels bl node = dmapCNR' (bl, go) levels node
 
     go :: [Level] -> Level -> Node -> Recur' [Level]
     go levels bl node = case node of
@@ -41,7 +44,7 @@ convertNode tab = convert [] 0
       NCase (Case {..}) ->
         let ii = fromJust $ HashMap.lookup _caseInductive (tab ^. infoInductives)
          in case ii ^. inductiveBuiltin of
-              Just BuiltinBool ->
+              Just BuiltinNat ->
                 case _caseBranches of
                   [br] -> makeIf br (maybeBranch _caseDefault)
                   [br1, br2] ->
@@ -65,13 +68,15 @@ convertNode tab = convert [] 0
                     Recur' (levels, mkIf _caseInfo sym (mkBuiltinApp' OpEq [_caseValue, mkConstant' (ConstInteger 0)]) _caseBranchBody br)
                   1 ->
                     End' $
-                      mkLet' (mkBuiltinApp' OpIntSub [convert levels bl _caseValue, mkConstant' (ConstInteger 1)]) $
+                      mkLet mempty (emptyBinder{_binderName = name}) (mkBuiltinApp' OpIntSub [convert levels bl _caseValue, mkConstant' (ConstInteger 1)]) $
                         mkIf
                           _caseInfo
                           sym
-                          (mkBuiltinApp' OpIntLe [mkConstant' (ConstInteger 0), mkVar' 0])
+                          (mkBuiltinApp' OpIntLe [mkConstant' (ConstInteger 0), mkVar (Info.singleton (NameInfo name)) 0])
                           (convert levels (bl + 1) _caseBranchBody)
                           (convert (bl : levels) bl br)
+                    where
+                      name = List.head _caseBranchBinders ^. binderName
                   _ -> impossible
           maybeBranch :: Maybe Node -> Node
           maybeBranch = fromMaybe (mkBuiltinApp' OpFail [mkConstant' (ConstString "no matching branch")])

src/Juvix/Compiler/Core/Translation/FromSource.hs

@@ -49,8 +49,9 @@ createBuiltinConstr ::
   Text ->
   Type ->
   Interval ->
+  Maybe BuiltinConstructor ->
   Sem r ConstructorInfo
-createBuiltinConstr sym tag nameTxt ty i = do
+createBuiltinConstr sym tag nameTxt ty i cblt = do
   return $
     ConstructorInfo
       { _constructorName = nameTxt,
@@ -59,21 +60,21 @@ createBuiltinConstr sym tag nameTxt ty i = do
         _constructorType = ty,
         _constructorArgsNum = length (typeArgs ty),
         _constructorInductive = sym,
-        _constructorBuiltin = Nothing
+        _constructorBuiltin = cblt
       }
 
 declareInductiveBuiltins ::
   Member InfoTableBuilder r =>
   Text ->
   Maybe BuiltinInductive ->
-  [(Tag, Text, Type -> Type)] ->
+  [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] ->
   ParsecS r ()
 declareInductiveBuiltins indName blt ctrs = do
   loc <- curLoc
   let i = mkInterval loc loc
   sym <- lift freshSymbol
   let ty = mkIdent' sym
-  constrs <- lift $ mapM (\(tag, name, fty) -> createBuiltinConstr sym tag name (fty ty) i) ctrs
+  constrs <- lift $ mapM (\(tag, name, fty, cblt) -> createBuiltinConstr sym tag name (fty ty) i cblt) ctrs
   lift $
     registerInductive
       indName
@@ -95,19 +96,19 @@ declareIOBuiltins =
   declareInductiveBuiltins
     "IO"
     Nothing
-    [ (BuiltinTag TagReturn, "return", mkPi' mkDynamic'),
-      (BuiltinTag TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty)),
-      (BuiltinTag TagWrite, "write", mkPi' mkDynamic'),
-      (BuiltinTag TagReadLn, "readLn", id)
+    [ (BuiltinTag TagReturn, "return", mkPi' mkDynamic', Nothing),
+      (BuiltinTag TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty), Nothing),
+      (BuiltinTag TagWrite, "write", mkPi' mkDynamic', Nothing),
+      (BuiltinTag TagReadLn, "readLn", id, Nothing)
     ]
 
 declareBoolBuiltins :: Member InfoTableBuilder r => ParsecS r ()
 declareBoolBuiltins =
   declareInductiveBuiltins
     "bool"
     (Just BuiltinBool)
-    [ (BuiltinTag TagTrue, "true", id),
-      (BuiltinTag TagFalse, "false", id)
+    [ (BuiltinTag TagTrue, "true", id, Just BuiltinBoolTrue),
+      (BuiltinTag TagFalse, "false", id, Just BuiltinBoolFalse)
     ]
 
 declareNatBuiltins :: Member InfoTableBuilder r => ParsecS r ()
@@ -117,8 +118,8 @@ declareNatBuiltins = do
   declareInductiveBuiltins
     "nat"
     (Just BuiltinNat)
-    [ (tagZero, "zero", id),
-      (tagSuc, "suc", \x -> mkPi' x x)
+    [ (tagZero, "zero", id, Just BuiltinNatZero),
+      (tagSuc, "suc", \x -> mkPi' x x, Just BuiltinNatSuc)
     ]
 
 parseToplevel ::