Literal casting

src/Juvix/Compiler/Builtins/Int.hs

@@ -371,6 +371,9 @@ registerIntLt :: forall r. (Members '[Builtins, NameIdGen] r) => FunctionDef ->
 registerIntLt f = do
   int <- builtinName BuiltinInt
   bool_ <- builtinName BuiltinBool
+  ofNat <- toExpression <$> builtinName BuiltinIntOfNat
+  suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc
+  zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatZero
   intLe <- toExpression <$> builtinName BuiltinIntLe
   intPlus <- toExpression <$> builtinName BuiltinIntPlus
   let l = getLoc f
@@ -380,7 +383,7 @@ registerIntLt f = do
       (.+.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
       x .+. y = intPlus @@ x @@ y
       (.<=.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
-      lit1 = ExpressionLiteral (WithLoc (getLoc f) (LitInteger 1))
+      lit1 = ofNat @@ (suc @@ zero)
       x .<=. y = intLe @@ x @@ y
       m = toExpression varm
       n = toExpression varn
@@ -399,3 +402,7 @@ registerIntLt f = do
   where
     builtinName :: (IsBuiltin a) => a -> Sem r Name
     builtinName = getBuiltinName (getLoc f)
+
+registerFromInt :: (Members '[Builtins, NameIdGen] r) => FunctionDef -> Sem r ()
+registerFromInt f = do
+  registerBuiltin BuiltinFromInt (f ^. funDefName)

src/Juvix/Compiler/Builtins/Nat.hs

@@ -301,3 +301,7 @@ registerNatEq f = do
         _funInfoFreeVars = [varn, varm],
         _funInfoFreeTypeVars = []
       }
+
+registerFromNat :: (Members '[Builtins, NameIdGen] r) => FunctionDef -> Sem r ()
+registerFromNat f = do
+  registerBuiltin BuiltinFromNat (f ^. funDefName)

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

@@ -107,6 +107,8 @@ data BuiltinFunction
   | BuiltinIntNonNeg
   | BuiltinIntLe
   | BuiltinIntLt
+  | BuiltinFromNat
+  | BuiltinFromInt
   | BuiltinSeq
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
 
@@ -138,6 +140,8 @@ instance Pretty BuiltinFunction where
     BuiltinIntNonNeg -> Str.intNonNeg
     BuiltinIntLe -> Str.intLe
     BuiltinIntLt -> Str.intLt
+    BuiltinFromNat -> Str.fromNat
+    BuiltinFromInt -> Str.fromInt
     BuiltinSeq -> Str.builtinSeq
 
 data BuiltinAxiom
@@ -224,5 +228,11 @@ isIntBuiltin = \case
   BuiltinIntLt -> True
   _ -> False
 
+isCastBuiltin :: BuiltinFunction -> Bool
+isCastBuiltin = \case
+  BuiltinFromNat -> True
+  BuiltinFromInt -> True
+  _ -> False
+
 isIgnoredBuiltin :: BuiltinFunction -> Bool
-isIgnoredBuiltin f = not (isNatBuiltin f) && not (isIntBuiltin f)
+isIgnoredBuiltin f = not (isNatBuiltin f) && not (isIntBuiltin f) && not (isCastBuiltin f)

src/Juvix/Compiler/Concrete/Language.hs

@@ -242,7 +242,8 @@ deriving stock instance Ord (Statement 'Scoped)
 data ProjectionDef s = ProjectionDef
   { _projectionConstructor :: S.Symbol,
     _projectionField :: SymbolType s,
-    _projectionFieldIx :: Int
+    _projectionFieldIx :: Int,
+    _projectionFieldBuiltin :: Maybe (WithLoc BuiltinFunction)
   }
 
 deriving stock instance Show (ProjectionDef 'Parsed)
@@ -595,7 +596,8 @@ deriving stock instance Ord (RecordDefineField 'Scoped)
 data RecordField (s :: Stage) = RecordField
   { _fieldName :: SymbolType s,
     _fieldColon :: Irrelevant (KeywordRef),
-    _fieldType :: ExpressionType s
+    _fieldType :: ExpressionType s,
+    _fieldBuiltin :: Maybe (WithLoc BuiltinFunction)
   }
 
 deriving stock instance Show (RecordField 'Parsed)

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -1141,8 +1141,12 @@ instance (SingI s) => PrettyPrint (RhsGadt s) where
     ppCode _rhsGadtColon <+> ppExpressionType _rhsGadtType
 
 instance (SingI s) => PrettyPrint (RecordField s) where
-  ppCode RecordField {..} =
-    ppSymbolType _fieldName <+> ppCode _fieldColon <+> ppExpressionType _fieldType
+  ppCode RecordField {..} = do
+    let builtin' = (<> line) . ppCode <$> _fieldBuiltin
+    builtin'
+      ?<> ppSymbolType _fieldName
+      <+> ppCode _fieldColon
+      <+> ppExpressionType _fieldType
 
 instance (SingI s) => PrettyPrint (RhsRecord s) where
   ppCode RhsRecord {..} = do

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -146,6 +146,7 @@ checkProjectionDef p = do
     ProjectionDef
       { _projectionFieldIx = p ^. projectionFieldIx,
         _projectionConstructor = p ^. projectionConstructor,
+        _projectionFieldBuiltin = p ^. projectionFieldBuiltin,
         _projectionField
       }
 
@@ -1339,7 +1340,8 @@ checkSections sec = do
                               ProjectionDef
                                 { _projectionConstructor = headConstr,
                                   _projectionField = field ^. fieldName,
-                                  _projectionFieldIx = idx
+                                  _projectionFieldIx = idx,
+                                  _projectionFieldBuiltin = field ^. fieldBuiltin
                                 }
 
                             getFields :: Sem (Fail ': s') [RecordStatement 'Parsed]

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

@@ -495,6 +495,11 @@ builtinStatement = do
     <|> (builtinFunction >>= fmap StatementFunctionDef . builtinFunctionDef)
     <|> (builtinAxiom >>= fmap StatementAxiom . builtinAxiomDef)
 
+builtinRecordField :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (WithLoc BuiltinFunction)
+builtinRecordField = do
+  void (kw kwBuiltin)
+  builtinFunction
+
 --------------------------------------------------------------------------------
 -- Syntax declaration
 --------------------------------------------------------------------------------
@@ -1265,6 +1270,7 @@ rhsGadt = P.label "<constructor gadt>" $ do
 
 recordField :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (RecordField 'Parsed)
 recordField = do
+  _fieldBuiltin <- optional builtinRecordField
   _fieldName <- symbol
   _fieldColon <- Irrelevant <$> kw kwColon
   _fieldType <- parseExpressionAtoms

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

@@ -1056,6 +1056,7 @@ goApplication a = do
 goLiteral :: Symbol -> Symbol -> Internal.LiteralLoc -> Node
 goLiteral intToNat intToInt l = case l ^. withLocParam of
   Internal.LitString s -> mkLitConst (ConstString s)
+  Internal.LitNumeric i -> mkLitConst (ConstInteger i)
   Internal.LitInteger i -> mkApp' (mkIdent' intToInt) (mkLitConst (ConstInteger i))
   Internal.LitNatural i -> mkApp' (mkIdent' intToNat) (mkLitConst (ConstInteger i))
   where

src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs

@@ -24,6 +24,7 @@ fromCore tab =
           _infoInductives = HashMap.filter (maybe True shouldKeepType . (^. inductiveBuiltin)) (tab ^. infoInductives),
           _infoConstructors = HashMap.filter (maybe True shouldKeepConstructor . (^. constructorBuiltin)) (tab ^. infoConstructors)
         }
+
     shouldKeepFunction :: BuiltinFunction -> Bool
     shouldKeepFunction = \case
       BuiltinNatPlus -> False
@@ -51,6 +52,8 @@ fromCore tab =
       BuiltinIntLe -> False
       BuiltinIntLt -> False
       BuiltinSeq -> False
+      BuiltinFromNat -> True
+      BuiltinFromInt -> True
 
     shouldKeepConstructor :: BuiltinConstructor -> Bool
     shouldKeepConstructor = \case

src/Juvix/Compiler/Internal/Data/Cast.hs

@@ -0,0 +1,18 @@
+module Juvix.Compiler.Internal.Data.Cast where
+
+import Juvix.Compiler.Internal.Language
+import Juvix.Prelude
+
+data CastType = CastInt | CastNat
+
+data CastHole = CastHole
+  { _castHoleHole :: Hole,
+    _castHoleType :: CastType
+  }
+
+makeLenses ''CastHole
+
+isCastInt :: CastType -> Bool
+isCastInt = \case
+  CastInt -> True
+  CastNat -> False

src/Juvix/Compiler/Internal/Extra.hs

@@ -81,10 +81,11 @@ genFieldProjection ::
   forall r.
   (Members '[NameIdGen] r) =>
   FunctionName ->
+  Maybe BuiltinFunction ->
   ConstructorInfo ->
   Int ->
   Sem r FunctionDef
-genFieldProjection _funDefName info fieldIx = do
+genFieldProjection _funDefName _funDefBuiltin info fieldIx = do
   body' <- genBody
   let (inductiveParams, constrArgs) = constructorArgTypes info
       implicity = constructorImplicity info
@@ -97,12 +98,12 @@ genFieldProjection _funDefName info fieldIx = do
         _funDefTerminating = False,
         _funDefInstance = False,
         _funDefCoercion = False,
-        _funDefBuiltin = Nothing,
         _funDefArgsInfo = mempty,
         _funDefPragmas = mempty {_pragmasInline = Just InlineAlways},
         _funDefBody = body',
         _funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy,
-        ..
+        _funDefName,
+        _funDefBuiltin
       }
   where
     genBody :: Sem r Expression

src/Juvix/Compiler/Internal/Extra/Base.hs

@@ -614,9 +614,6 @@ genWildcard loc impl = do
   var <- varFromWildcard (Wildcard loc)
   return (PatternArg impl Nothing (PatternVariable var))
 
-freshWildcard :: (Members '[NameIdGen] r) => Interval -> Sem r Hole
-freshWildcard l = mkHole l <$> freshNameId
-
 freshHole :: (Members '[NameIdGen] r) => Interval -> Sem r Hole
 freshHole l = mkHole l <$> freshNameId