Make non-negative literals default to `Nat` rather than `Int`.

Nats are far more common that Ints, and lets you write `num_iters = 100` as a top-level decl instead of `num_iters : Nat = 100`. To deliberately default to `Int`, you can write `+4`, which is analogous to the way we write `4.`, where we add the redundant decimal point to indicate a float.
author: Dougal <d.maclaurin@gmail.com> 2022-05-25 19:36:12 -0400
committer: Dougal <d.maclaurin@gmail.com> 2022-05-25 21:47:05 -0400
commit: a2cb8216876ee5ed04ba41a46ce332210bd42d6f (patch)
tree: b5d7b27664a281195d7d945abbd847c9d6f0d29a
parent: da51f864135430a90d3173d2618a6103633f601c (diff)
25 files changed, 146 insertions, 86 deletions
diff --git a/examples/fluidsim.dx b/examples/fluidsim.dx
index e704c813..48106534 100644
--- a/examples/fluidsim.dx
+++ b/examples/fluidsim.dx
@@ -128,7 +128,7 @@ init_color = for i:N j:M.
   [r, g, b]
 
 -- Run fluid sim and plot it.
-num_steps = 5 : Nat
+num_steps = 5
 :html imseqshow $ fluidsim num_steps init_color init_velocity
 > <html output>
 
diff --git a/examples/mcmc.dx b/examples/mcmc.dx
index 950a1eb1..1d70e5b6 100644
--- a/examples/mcmc.dx
+++ b/examples/mcmc.dx
@@ -103,7 +103,7 @@ mhSamples  = runChain randn_vec (mhStep  mhParams  myLogProb) numSamples k0
   slice (map head mhSamples) 0 (Fin 1000)
 > <html output>
 
-hmcParams = (10 : Nat, 0.1)
+hmcParams = (10, 0.1)
 hmcSamples = runChain randn_vec (hmcStep hmcParams myLogProb) numSamples k0
 
 :p meanAndCovariance hmcSamples
diff --git a/examples/particle-filter.dx b/examples/particle-filter.dx
index 68f38c6c..a48635ad 100644
--- a/examples/particle-filter.dx
+++ b/examples/particle-filter.dx
@@ -56,8 +56,8 @@ gaussModel : Model Float Float =
   , \s. normalDistn s 1.0
   )
 
-timesteps = 10 : Nat
-num_particles = 10000 : Nat
+timesteps = 10
+num_particles = 10000
 
 truth = for i:(Fin timesteps).
   s = n_to_f (ordinal i)
diff --git a/examples/pi.dx b/examples/pi.dx
index 1a151b84..c38bf6f5 100644
--- a/examples/pi.dx
+++ b/examples/pi.dx
@@ -27,7 +27,7 @@ def meanAndStdDev (n:Nat) (f: Key -> Float) (key:Key) : (Float & Float) =
   samps = for i:(Fin n). many f key i
   (mean samps, std samps)
 
-numSamps = 1000000 : Nat
+numSamps = 1000000
 
 :p meanAndStdDev numSamps estimatePiArea (new_key 0)
 > (3.143452, 1.640889)
diff --git a/examples/raytrace.dx b/examples/raytrace.dx
index 3c1c0966..5e52aa80 100644
--- a/examples/raytrace.dx
+++ b/examples/raytrace.dx
@@ -301,12 +301,12 @@ theScene = MkScene $
   ]
 
 defaultParams = {
-    numSamples = 50 : Nat
-  , maxBounces = 10 : Nat
+    numSamples = 50
+  , maxBounces = 10
   , shareSeed  = True }
 
 defaultCamera = {
-    numPix     = 250 : Nat
+    numPix     = 250
   , pos        = 10.0 .* zHat
   , halfWidth  = 0.3
   , sensorDist = 1.0 }
diff --git a/examples/rejection-sampler.dx b/examples/rejection-sampler.dx
index d6487133..a78d4db4 100644
--- a/examples/rejection-sampler.dx
+++ b/examples/rejection-sampler.dx
@@ -36,9 +36,9 @@ def trySampleBinomial (n:Nat) (p:Prob) (k:Key) : Maybe Nat =
 'We test the implementation by sampling from a Binomial distribution with 10 trials and success probability 0.4.
 
 -- parameters
-n = 10 : Nat
+n = 10
 p = 0.4
-numSamples = 5000 : Nat
+numSamples = 5000
 k0 = new_key 0
 
 rejectionSamples = rand_vec numSamples (rejectionSample $ trySampleBinomial n p) k0
diff --git a/examples/schrodinger.dx b/examples/schrodinger.dx
index aa54d6a6..55e25841 100644
--- a/examples/schrodinger.dx
+++ b/examples/schrodinger.dx
@@ -19,7 +19,7 @@ import png
 '## Parameters
 
 -- The number of points on the grid in each dimension e.g. (41x41 for the 2d case)
-gridSize = 41 : Nat
+gridSize = 41
 D = Fin gridSize
 
 -- Space discretization
@@ -32,7 +32,7 @@ dt = 0.000001
 Steps = Fin 155000
 
 -- The number of frames to output in each GIF animation
-gifFrames = 100 : Nat
+gifFrames = 100
 
 '## Helpers
 
diff --git a/examples/sgd.dx b/examples/sgd.dx
index 82235e86..01d26e9d 100644
--- a/examples/sgd.dx
+++ b/examples/sgd.dx
@@ -29,7 +29,7 @@ def gradfunc (x:D=>Float) (iter:Nat) : D=>Float = grad objective x
 x_init = for i:D. 0.0
 stepsize = 0.01
 decay = 0.9
-num_iters = 1000 : Nat
+num_iters = 1000
 :p sgd stepsize decay num_iters gradfunc x_init
 > [1.1, 1.1, 1.1, 1.1]
 
diff --git a/examples/tutorial.dx b/examples/tutorial.dx
index 10957624..e65b4c9e 100644
--- a/examples/tutorial.dx
+++ b/examples/tutorial.dx
@@ -458,7 +458,7 @@ tableMean [0.0, 1.0, 0.5]
   constructor in this case).
 
 :t \ x. x + 10
-> (Int32 -> Int32)
+> (Nat32 -> Nat32)
 
 (\ x. x + 10) 20
 > 30
diff --git a/lib/prelude.dx b/lib/prelude.dx
index f4d48ff8..394ac63e 100644
--- a/lib/prelude.dx
+++ b/lib/prelude.dx
@@ -72,29 +72,42 @@ def f_to_n (x:Float) : Nat = internal_cast _ x
 def n_to_f (x : Nat) : Float = internal_cast _ x
 def n_to_w8 (x : Nat) : Word8   = internal_cast _ x
 
+interface FromNatural a
+  from_natural : Nat64 -> a
+
+instance FromNatural Float32
+  from_natural = \x. internal_cast _ x
+
+instance FromNatural Float64
+  from_natural = \x. internal_cast _ x
+
+instance FromNatural Int32
+  from_natural = \x. internal_cast _ x
+
+instance FromNatural Int64
+  from_natural = \x. internal_cast _ x
+
+instance FromNatural Nat32
+  from_natural = \x. internal_cast _ x
+
+instance FromNatural Nat64
+  from_natural = \x. x
+
 interface FromInteger a
   from_integer : Int64 -> a
 
 instance FromInteger Float32
-  from_integer = \x. i_to_f $ i64_to_i x
+  from_integer = \x. internal_cast _ x
 
 instance FromInteger Int32
-  from_integer = \x. i64_to_i x
+  from_integer = \x. internal_cast _ x
 
 instance FromInteger Float64
-  from_integer = \x. f_to_f64 $ i_to_f $ i64_to_i x
+  from_integer = \x. internal_cast _ x
 
 instance FromInteger Int64
   from_integer = \x. x
 
-instance FromInteger Nat64
-  -- TODO: figure out how we're going to handle negative literals. Maybe have a
-  -- separate `FromNat` class?
-  from_integer = \x. i64_to_n64 x
-
-instance FromInteger Nat32
-  from_integer = \x. i64_to_n32 x
-
 '## Bitwise operations
 
 interface Bits a
@@ -538,7 +551,7 @@ def n_to_i (x:Nat) : Int =
   internal_cast _ x
 
 def i_to_n (x:Int) : Maybe Nat =
-  if w8_to_b $ %ilt x 0
+  if w8_to_b $ %ilt x (0:Int)
     then Nothing
     else Just $ unsafe_i_to_n x
 
@@ -2153,7 +2166,7 @@ def is_power_of_2 (x:Nat) : Bool =
     else 0 == %and x (unsafe_nat_diff x 1)
 
 def natlog2 (x:Nat) : Nat =
-  yield_state (-1) \ansRef.
+  tmp = yield_state 0 \ansRef.
     run_state 1 \cmpRef.
       while do
         if x >= (get cmpRef)
@@ -2163,6 +2176,7 @@ def natlog2 (x:Nat) : Nat =
             True
           else
             False
+  unsafe_nat_diff tmp 1  -- TODO: something less horrible
 
 def general_integer_power {a} (times:a->a->a) (one:a) (base:a) (power:Nat) : a =
   -- Implements exponentiation by squaring.
diff --git a/src/lib/CheapReduction.hs b/src/lib/CheapReduction.hs
index a07fda19..16e154e5 100644
--- a/src/lib/CheapReduction.hs
+++ b/src/lib/CheapReduction.hs
@@ -273,7 +273,7 @@ instance CheaplyReducibleE Expr Atom where
         BaseTy (Scalar Nat32Type) -> do
           val <- cheapReduceE val'
           case val of
-            Con (Lit (Int64Lit v)) -> return $ Con $ Lit $ Nat32Lit $ fromIntegral v
+            Con (Lit (Nat64Lit v)) -> return $ Con $ Lit $ Nat32Lit $ fromIntegral v
             _ -> empty
         _ -> empty
     Op (ProjMethod dict i) -> do
diff --git a/src/lib/Inference.hs b/src/lib/Inference.hs
index da980e8e..bfb16302 100644
--- a/src/lib/Inference.hs
+++ b/src/lib/Inference.hs
@@ -194,13 +194,17 @@ class (SubstReader Name m, InfBuilder2 m, Solver2 m)
   liftSolverMInf :: EmitsInf o => SolverM o a -> m i o a
   gatherUnsolvedInterfaces :: m i o a -> m i o (a, IfaceTypeSet o)
   reportUnsolvedInterface  :: Type o  -> m i o ()
-  addIntDefault :: AtomName o -> m i o ()
+  addDefault :: AtomName o -> DefaultType -> m i o ()
   getDefaults :: m i o (Defaults o)
 
 applyDefaults :: EmitsInf o => InfererM i o ()
 applyDefaults = do
-  Defaults defaults <- getDefaults
-  forM_ (nameSetToList defaults) \v -> tryConstrainEq (Var v) $ BaseTy $ Scalar Int32Type
+  defaults <- getDefaults
+  applyDefault (intDefaults defaults) (BaseTy $ Scalar Int32Type)
+  applyDefault (natDefaults defaults) (BaseTy $ Scalar Nat32Type)
+  where
+    applyDefault ds ty =
+      forM_ (nameSetToList ds) \v -> tryConstrainEq (Var v) ty
 
 withApplyDefaults :: EmitsInf o => InfererM i o a -> InfererM i o a
 withApplyDefaults cont = cont <* applyDefaults
@@ -218,24 +222,36 @@ data InfOutMap (n::S) =
     -- we zonk bindings)
     (UnsolvedEnv n)
 
--- Set of names that should be defaulted to Int32
-newtype Defaults (n::S) = Defaults (NameSet n)
-        deriving (Semigroup, Monoid)
+data DefaultType = IntDefault | NatDefault -- | StrDefault ??
+
+data Defaults (n::S) = Defaults
+  { intDefaults :: NameSet n   -- Set of names that should be defaulted to Int32
+  , natDefaults :: NameSet n } -- Set of names that should be defaulted to Nat32
+
+instance Semigroup (Defaults n) where
+  Defaults d1 d2 <> Defaults d1' d2' = Defaults (d1 <> d1') (d2 <> d2')
+
+instance Monoid (Defaults n) where
+  mempty = Defaults mempty mempty
 
 instance SinkableE Defaults where
   sinkingProofE _ _ = todoSinkableProof
 instance HoistableE Defaults where
-  freeVarsE (Defaults fvs) = fvs
+  freeVarsE (Defaults d1 d2) = d1 <> d2
 instance SubstE Name Defaults where
-  substE env (Defaults ds) = Defaults $ freeVarsE $ substE env $ ListE $ nameSetToList @AtomNameC ds
+  substE env (Defaults d1 d2) = Defaults (substDefaultSet d1) (substDefaultSet d2)
+    where
+      substDefaultSet d = freeVarsE $ substE env $ ListE $ nameSetToList @AtomNameC d
 
 zonkDefaults :: SolverSubst n -> Defaults n -> Defaults n
-zonkDefaults s (Defaults ds) =
-  Defaults $ flip foldMap (nameSetToList @AtomNameC ds) \v ->
-    case lookupSolverSubst s v of
-      Rename   v'       -> freeVarsE v'
-      SubstVal (Var v') -> freeVarsE v'
-      _ -> mempty
+zonkDefaults s (Defaults d1 d2) =
+  Defaults (zonkDefaultSet d1) (zonkDefaultSet d2)
+  where
+    zonkDefaultSet d = flip foldMap (nameSetToList @AtomNameC d) \v ->
+      case lookupSolverSubst s v of
+        Rename   v'       -> freeVarsE v'
+        SubstVal (Var v') -> freeVarsE v'
+        _ -> mempty
 
 data InfOutFrag (n::S) (l::S) = InfOutFrag (InfEmissions n l) (Defaults l) (SolverSubst l)
 
@@ -466,9 +482,13 @@ instance Inferer InfererM where
       runSolverM' m
   {-# INLINE liftSolverMInf #-}
 
-  addIntDefault v = InfererM $ SubstReaderT $ lift $ lift11 $
-    extendTrivialInplaceT $ InfOutFrag REmpty defaults emptySolverSubst
-    where defaults = Defaults $ freeVarsE v
+  addDefault v defaultType =
+    InfererM $ SubstReaderT $ lift $ lift11 $
+      extendTrivialInplaceT $ InfOutFrag REmpty defaults emptySolverSubst
+    where
+      defaults = case defaultType of
+        IntDefault -> Defaults (freeVarsE v) mempty
+        NatDefault -> Defaults mempty (freeVarsE v)
 
   getDefaults = InfererM $ SubstReaderT $ lift $ lift11 do
     InfOutMap _ _ defaults _ <- getOutMapInplaceT
@@ -711,7 +731,8 @@ hoistRequiredIfaces bs = \case
     HoistFailure _  -> Nothing
 
 hoistDefaults :: BindsNames b => b n l -> Defaults l -> Defaults n
-hoistDefaults b (Defaults defaults) = Defaults $ hoistFilterNameSet b defaults
+hoistDefaults b (Defaults d1 d2) = Defaults (hoistFilterNameSet b d1)
+                                            (hoistFilterNameSet b d2)
 
 infNamesToEmissions :: InferenceNameBinders n l -> InfEmissions n l
 infNamesToEmissions = go REmpty
@@ -992,6 +1013,19 @@ checkOrInferRho (WithSrcE pos expr) reqTy = do
     value' <- zonk =<< (checkRho value $ VariantTy $ Ext NoLabeledItems $ Just row)
     prev <- mapM (\() -> freshType TyKind) labels
     matchRequirement =<< emitOp (VariantLift prev value')
+  UNatLit x -> do
+    lookupSourceMap "from_natural" >>= \case
+      Nothing ->
+        -- fallback for missing protolude
+        matchRequirement $ Con $ Lit $ Nat32Lit $ fromIntegral x
+      Just (UMethodVar fromNatMethod) -> do
+        ~(MethodBinding _ _ fromNat) <- lookupEnv fromNatMethod
+        (fromNatInst, (Var resTyVar:_)) <- instantiateSigmaWithArgs fromNat
+        addDefault resTyVar NatDefault
+        let i64Atom = Con $ Lit $ Nat64Lit $ fromIntegral x
+        result <- matchRequirement =<< app fromNatInst i64Atom
+        return result
+      Just _ -> error "not a method"
   UIntLit x  -> do
     lookupSourceMap "from_integer" >>= \case
       Nothing ->
@@ -1000,7 +1034,7 @@ checkOrInferRho (WithSrcE pos expr) reqTy = do
       Just (UMethodVar fromIntMethod) -> do
         ~(MethodBinding _ _ fromInt) <- lookupEnv fromIntMethod
         (fromIntInst, (Var resTyVar:_)) <- instantiateSigmaWithArgs fromInt
-        addIntDefault resTyVar
+        addDefault resTyVar IntDefault
         let i64Atom = Con $ Lit $ Int64Lit $ fromIntegral x
         result <- matchRequirement =<< app fromIntInst i64Atom
         return result
diff --git a/src/lib/Interpreter.hs b/src/lib/Interpreter.hs
index 89ba2a2b..1ac78b8f 100644
--- a/src/lib/Interpreter.hs
+++ b/src/lib/Interpreter.hs
@@ -222,8 +222,8 @@ evalOp expr = mapM evalAtom expr >>= \case
         (Int64Type, Int32Type) -> do
           let Con (Lit (Int64Lit v)) = x
           return $ Con $ Lit $ Int32Lit $ fromIntegral v
-        (Int64Type, Nat32Type) -> do
-          let Con (Lit (Int64Lit v)) = x
+        (Nat64Type, Nat32Type) -> do
+          let Con (Lit (Nat64Lit v)) = x
           return $ Con $ Lit $ Nat32Lit $ fromIntegral v
         _ -> failedCast
       _ -> failedCast
diff --git a/src/lib/PPrint.hs b/src/lib/PPrint.hs
index ff810bf6..73af5fc6 100644
--- a/src/lib/PPrint.hs
+++ b/src/lib/PPrint.hs
@@ -647,6 +647,7 @@ instance PrettyPrec (UExpr' n) where
     UVariant labels label value -> prettyVariant labels label value
     UVariantTy items -> prettyExtLabeledItems items Nothing (line <> "|") ":"
     UVariantLift labels value -> prettyVariantLift labels value
+    UNatLit   v -> atPrec ArgPrec $ p v
     UIntLit   v -> atPrec ArgPrec $ p v
     UFloatLit v -> atPrec ArgPrec $ p v
 
diff --git a/src/lib/Parser.hs b/src/lib/Parser.hs
index 51a3f2ea..e83d9be2 100644
--- a/src/lib/Parser.hs
+++ b/src/lib/Parser.hs
@@ -28,6 +28,7 @@ import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.Scientific as Scientific
 import Data.Maybe (fromMaybe)
 import Data.Void
+import Data.Word
 import qualified Data.Set as S
 import Data.String (IsString, fromString)
 import qualified Text.Megaparsec.Char.Lexer as L
@@ -225,7 +226,8 @@ leafExpr = uVarOcc <|> lookaheadExprs <?> "expression"
         '%'  -> uPrim
         '#'  -> uLabel <|> uIsoSugar
         '{'  -> (uLabeledExprs `fallBackTo` uVariantExpr)
-        _ | isDigit next -> withSrc (UIntLit <$> intLit <|> UFloatLit <$> doubleLit)
+        _ | isDigit next -> withSrc (    UNatLit   <$> natLit
+                                     <|> UFloatLit <$> doubleLit)
         -- Here we can't commit to a single option yet
         'v'  -> uViewExpr <|> uPiType
         'f'  -> uForExpr  <|> uPiType
@@ -963,7 +965,7 @@ ops :: [[Operator Parser (UExpr VoidS)]]
 ops =
   [ [InfixL $ sym "." $> mkTabApp , symOp "!"]
   , [InfixL $ sc $> mkApp]
-  , [prefixNegOp]
+  , [prefixNegOp, prefixPosOp]
   , [anySymOp] -- other ops with default fixity
   , [symOp "+", symOp "-", symOp "||", symOp "&&",
      InfixR $ sym "=>" $> mkTabType,
@@ -1009,14 +1011,26 @@ pairingSymOpP s = opWithSrc $ do
 prefixNegOp :: Operator Parser (UExpr VoidS)
 prefixNegOp = Prefix $ label "negation" $ do
   ((), pos) <- withPos $ sym "-"
-  let f = WithSrcE (Just pos) "neg"
-  return \case
-    -- Special case: negate literals directly
-    WithSrcE litpos (IntLitExpr i)
-      -> WithSrcE (joinPos (Just pos) litpos) (IntLitExpr (-i))
-    WithSrcE litpos (FloatLitExpr i)
-      -> WithSrcE (joinPos (Just pos) litpos) (FloatLitExpr (-i))
-    x -> mkApp f x
+  return \(WithSrcE litpos e) -> do
+    let pos' = joinPos (Just pos) litpos
+    case e of
+      UNatLit   i -> WithSrcE pos' $ UIntLit   (-(fromIntegral i))
+      UIntLit   i -> WithSrcE pos' $ UIntLit   (-i)
+      UFloatLit i -> WithSrcE pos' $ UFloatLit (-i)
+      _ -> do
+        let f = WithSrcE (Just pos) "neg"
+        mkApp f $ WithSrcE litpos e
+
+prefixPosOp :: Operator Parser (UExpr VoidS)
+prefixPosOp = Prefix $ label "positive" $ do
+  ((), pos) <- withPos $ sym "+"
+  return \(WithSrcE litpos e) -> do
+    let pos' = joinPos (Just pos) litpos
+    WithSrcE pos' case e of
+      UNatLit   i -> UIntLit   (fromIntegral i)
+      UIntLit   i -> UIntLit   i
+      UFloatLit i -> UFloatLit i
+      _ -> e
 
 binApp :: SourceName -> SrcPos -> UExpr VoidS -> UExpr VoidS -> UExpr VoidS
 binApp f pos x y = (f' `mkApp` x) `mkApp` y
@@ -1179,8 +1193,8 @@ charLit = lexeme $ char '\'' >> L.charLiteral <* char '\''
 strLit :: Lexer String
 strLit = lexeme $ char '"' >> manyTill L.charLiteral (char '"')
 
-intLit :: Lexer Int
-intLit = lexeme $ try $ L.decimal <* notFollowedBy (char '.')
+natLit :: Lexer Word64
+natLit = lexeme $ try $ L.decimal <* notFollowedBy (char '.')
 
 doubleLit :: Lexer Double
 doubleLit = lexeme $
diff --git a/src/lib/Simplify.hs b/src/lib/Simplify.hs
index 08fe50f5..014bed84 100644
--- a/src/lib/Simplify.hs
+++ b/src/lib/Simplify.hs
@@ -535,7 +535,7 @@ simplifyOp op = case op of
     _ -> error "Not a variant type"
   CastOp (BaseTy (Scalar Int32Type)) (Con (Lit (Int64Lit val))) ->
     return $ Con $ Lit $ Int32Lit $ fromIntegral val
-  CastOp (BaseTy (Scalar Nat32Type)) (Con (Lit (Int64Lit val))) ->
+  CastOp (BaseTy (Scalar Nat32Type)) (Con (Lit (Nat64Lit val))) ->
     return $ Con $ Lit $ Nat32Lit $ fromIntegral val
   -- Those are not no-ops! Builder methods do algebraic simplification!
   BinOp ISub x y -> isub x y
diff --git a/src/lib/SourceRename.hs b/src/lib/SourceRename.hs
index df785a03..2db37d21 100644
--- a/src/lib/SourceRename.hs
+++ b/src/lib/SourceRename.hs
@@ -211,6 +211,7 @@ instance SourceRenamableE UExpr' where
     URecordTy elems -> URecordTy <$> mapM sourceRenameE elems
     UVariantTy (Ext tys ext) -> UVariantTy <$>
       (Ext <$> mapM sourceRenameE tys <*> mapM sourceRenameE ext)
+    UNatLit   x -> return $ UNatLit x
     UIntLit   x -> return $ UIntLit x
     UFloatLit x -> return $ UFloatLit x
 
diff --git a/src/lib/Syntax.hs b/src/lib/Syntax.hs
index 140cbc46..4fa16dc9 100644
--- a/src/lib/Syntax.hs
+++ b/src/lib/Syntax.hs
@@ -108,7 +108,7 @@ module Syntax (
     pattern BaseTy, pattern PtrTy, pattern UnitVal,
     pattern PairVal, pattern TyKind, pattern TabTy, pattern TabVal,
     pattern Pure, pattern LabeledRowKind, pattern EffKind, pattern UPatIgnore,
-    pattern IntLitExpr, pattern FloatLitExpr, pattern ProdTy, pattern ProdVal,
+    pattern ProdTy, pattern ProdVal,
     pattern SumTy, pattern SumVal, pattern MaybeTy, pattern BinaryFunTy,
     pattern BinaryLamExpr,
     pattern NothingAtom, pattern JustAtom, pattern AtomicBlock,
diff --git a/src/lib/Types/Source.hs b/src/lib/Types/Source.hs
index 7d2847c7..14664231 100644
--- a/src/lib/Types/Source.hs
+++ b/src/lib/Types/Source.hs
@@ -26,6 +26,7 @@ import qualified Data.Map.Strict       as M
 import Data.String (IsString, fromString)
 import Data.Text (Text)
 import Data.Text.Prettyprint.Doc (Pretty (..), hardline, (<+>))
+import Data.Word
 
 import GHC.Generics (Generic (..))
 import Data.Store (Store (..))
@@ -95,16 +96,11 @@ data UExpr' (n::S) =
  | ULabeledRow (UFieldRowElems n)                    -- {@v:X ? a:Y ? b:Z ? ...rest}
  | URecordTy (UFieldRowElems n)                      -- {@v:X & a:Y & b:Z & ...rest}
  | UVariantTy (ExtLabeledItems (UExpr n) (UExpr n))  -- {a:X | b:Y | ...rest}
- | UIntLit  Int
+ | UNatLit   Word64
+ | UIntLit   Int
  | UFloatLit Double
   deriving (Show, Generic)
 
-pattern IntLitExpr :: Int -> UExpr' n
-pattern IntLitExpr x = UIntLit x
-
-pattern FloatLitExpr :: Double -> UExpr' n
-pattern FloatLitExpr x = UFloatLit x
-
 type UFieldRowElems (n::S) = [UFieldRowElem n]
 data UFieldRowElem (n::S)
   = UStaticField String                (UExpr n)
diff --git a/tests/adt-tests.dx b/tests/adt-tests.dx
index e3988316..a0addf66 100644
--- a/tests/adt-tests.dx
+++ b/tests/adt-tests.dx
@@ -10,7 +10,7 @@ data IntFloat =
 data MyPair a:Type b:Type =
    MkMyPair a b
 
-z = MkMyPair 1 2.3
+z = MkMyPair (+1) 2.3
 
 :p z
 > (MkMyPair 1 2.3)
@@ -74,7 +74,7 @@ x : MyEither Int Float = MyLeft 1
 > 1
 
 -- %passes imp
-myTab = [MyLeft 1, MyRight 3.5, MyLeft 123, MyLeft 456]
+myTab = [MyLeft (+1), MyRight 3.5, MyLeft 123, MyLeft 456]
 
 :p myTab
 > [(MyLeft 1), (MyRight 3.5), (MyLeft 123), (MyLeft 456)]
diff --git a/tests/eval-tests.dx b/tests/eval-tests.dx
index 9be03d43..a73f04f8 100644
--- a/tests/eval-tests.dx
+++ b/tests/eval-tests.dx
@@ -685,7 +685,7 @@ for i:(Fin 5). for j:(..i).
 :p 1 + 2
 > 3
 
-:p [1,2] - [2,10]
+:p [+1,2] - [2,10]
 > [-1, -8]
 
 :p 2.0 .* [[1.0, 2.0], [3.0, 4.0]]
diff --git a/tests/fft-tests.dx b/tests/fft-tests.dx
index 5e3650b4..c6c50498 100644
--- a/tests/fft-tests.dx
+++ b/tests/fft-tests.dx
@@ -1,7 +1,7 @@
 import fft
 
-:p map nextpow2 [-1, 0, 1, 2, 3, 4, 7, 8, 9, 1023, 1024, 1025]
-> [0, 0, 0, 1, 2, 2, 3, 3, 4, 10, 10, 11]
+:p map nextpow2 [0, 1, 2, 3, 4, 7, 8, 9, 1023, 1024, 1025]
+> [0, 0, 1, 2, 2, 3, 3, 4, 10, 10, 11]
 
 a : (Fin 4)=>Complex = arb $ new_key 0
 :p a ~~ (ifft $ fft a)
diff --git a/tests/record-variant-tests.dx b/tests/record-variant-tests.dx
index b61055d7..b100cd2c 100644
--- a/tests/record-variant-tests.dx
+++ b/tests/record-variant-tests.dx
@@ -32,17 +32,17 @@ Syntax for records, variants, and their types.
 :p {a=3, b=4}
 > {a = 3, b = 4}
 :t {a=3, b=4}
-> {a: Int32 & b: Int32}
+> {a: Nat32 & b: Nat32}
 
 :p {a=3, b=4,}
 > {a = 3, b = 4}
 :t {a=3, b=4,}
-> {a: Int32 & b: Int32}
+> {a: Nat32 & b: Nat32}
 
 :p {a=3, a=4}
 > {a = 3, a = 4}
 :t {a=3, a=4}
-> {a: Int32 & a: Int32}
+> {a: Nat32 & a: Nat32}
 
 :p
   x = {a=5.0, b=2}
@@ -398,7 +398,7 @@ q = {@abc=1, y=2}
 q
 > {abc = 1, y = 2}
 :t q
-> {abc: Int32 & y: Int32}
+> {abc: Nat32 & y: Nat32}
 
 :p
   {@abc=xv, y=yv} = q
diff --git a/tests/test_module_B.dx b/tests/test_module_B.dx
index 868a3220..ce899d8a 100644
--- a/tests/test_module_B.dx
+++ b/tests/test_module_B.dx
@@ -7,7 +7,7 @@ test_module_B_val = 10
 
 test_module_B_val_from_C = test_module_C_val
 
-instance FooClass Int
+instance FooClass Nat
   fooMethod = \x. x + x
 
 arrayVal = [1,2,3]
diff --git a/tests/type-tests.dx b/tests/type-tests.dx
index e1b95269..98985fc2 100644
--- a/tests/type-tests.dx
+++ b/tests/type-tests.dx
@@ -53,7 +53,7 @@ help make the errors more local.
 :t
    myid : a:Type ?-> a -> a = \x. x
    myid (myid) (myid 1)
-> Int32
+> Nat32
 
 :t
    x = iota (Fin 10)
@@ -96,16 +96,16 @@ xr = map n_to_f arr
 > Float32
 
 :t [1, 2, 3]
-> ((Fin 3) => Int32)
+> ((Fin 3) => Nat32)
 
 :t [1, [2]]
-> Type error:Couldn't synthesize a class dictionary for: (FromInteger ((Fin 1) => Int32))
+> Type error:Couldn't synthesize a class dictionary for: (FromNatural ((Fin 1) => Nat32))
 >
 > :t [1, [2]]
 >     ^
 
 :t [[1, 2], [3, 4]]
-> ((Fin 2) => (Fin 2) => Int32)
+> ((Fin 2) => (Fin 2) => Nat32)
 
 :t [[1, 2], [3]]
 > Type error:Literal has 1 element, but required type has 2.
@@ -373,7 +373,7 @@ def weakerInferenceReduction {n} (l : i:n=>(..i)=>Float) (j:n): Unit =
 val = for i:(Fin 2). \(x:Float). for j:(..i). 1
 
 :t val
-> ((v#0:(Fin 2)) => Float32 -> (..v#0) => Int32)
+> ((v#0:(Fin 2)) => Float32 -> (..v#0) => Nat32)
 
 -- Tests for table
 
@@ -421,7 +421,7 @@ def uncurryTable {a} (x : ((Fin 2) & (Fin 2))=>a) : (Fin 2)=>(Fin 2)=>a =
 :t uncurryTable [0.0, 1.0, 2.0, 3.0]  -- We should be able to infer the tuple type here
 > ((Fin 2) => (Fin 2) => Float32)
 :t uncurryTable [0, 1, 2, 3]          -- Extra difficulty: need to default the integer type
-> ((Fin 2) => (Fin 2) => Int32)
+> ((Fin 2) => (Fin 2) => Nat32)
 
 
 -- Make sure that the local type alias is unifiable with Int
author	Dougal <d.maclaurin@gmail.com>	2022-05-25 19:36:12 -0400
committer	Dougal <d.maclaurin@gmail.com>	2022-05-25 21:47:05 -0400
commit	a2cb8216876ee5ed04ba41a46ce332210bd42d6f (patch)
tree	b5d7b27664a281195d7d945abbd847c9d6f0d29a
parent	da51f864135430a90d3173d2618a6103633f601c (diff)