[#135] add custom Indigo fromInteger

Problem: type signatures or annotations always need to be specified for
numeric values in Indigo code, because they are otherwise ambiguous.
However, Indigo uses `RebindableSyntax` that allows to define a
`fromInteger` function used to resolve numeric literals, and this can
be used to implement (some) custom resolution logic.

Solution: implement a `fromInteger` that takes an additional value
(beside the Integer) that provides disambiguation for the resulting
value type, with function constructors for this type that match the
target Michelson type.
Additionally, because of this, the 'int' expression has been renamed
'toInt'.
parent 29dd1ed2
Pipeline #144852190 passed with stages
in 4 minutes and 15 seconds
......@@ -12,7 +12,7 @@ import Indigo.Frontend as Exports
import Indigo.Internal as Exports hiding (return, (=<<), (>>), (>>=))
import Indigo.Lib as Exports
import Indigo.Lorentz as Exports
import Indigo.Prelude as Exports
import Indigo.Prelude as Exports hiding (fromInteger)
import Indigo.Print as Exports
import Indigo.Rebinded as Exports
import Prelude (return, (=<<), (>>), (>>=))
......@@ -16,7 +16,7 @@ module Indigo.Internal.Expr
-- ** Comparison
, (==.), (/=.), (<=.), (>=.), (<.), (>.)
-- ** Conversion
, isNat, int
, isNat, toInt
-- * Bits and boolean
, (<<.), (>>.), (&&.), (||.), (^.), not
......@@ -236,10 +236,10 @@ isNat :: (ex :~> Integer)
-> Expr (Maybe Natural)
isNat = IsNat
int :: (ex :~> Natural)
toInt :: (ex :~> Natural)
=> ex
-> Expr Integer
int = Int'
toInt = Int'
-- Bits and boolean
----------------------------------------------------------------------------
......
......@@ -11,8 +11,7 @@ During its execution Lorentz code is being generated.
-}
module Indigo.Internal.State
(
-- * Indigo State
( -- * Indigo State
IndigoState (..)
, usingIndigoState
, (>>=)
......@@ -101,7 +100,7 @@ iput gc = IndigoState $ \_ -> gc
-- | Reference id to a stack cell
newtype RefId = RefId Word
deriving stock (Show, Generic)
deriving newtype (Eq, Ord, Real, Num)
deriving newtype (Eq, Ord, Real, Num)
-- | Constraint for `StkEl`, required for comparison in constraint checking
type TypeValue a = (Typeable a, Typeable (ToT a))
......
......@@ -22,7 +22,7 @@ import Indigo.Frontend
import Indigo.Internal.Expr
import Indigo.Internal.State (TypeValue)
import Indigo.Lorentz
import Indigo.Prelude
import Indigo.Prelude hiding (fromInteger)
import Indigo.Rebinded
----------------------------------------------------------------------------
......@@ -126,7 +126,7 @@ subGt0 minuend subtrahend onNegative = do
diff = minuend -. subtrahend
zero :: Expr Integer
zero = C 0
zero = C $ 0 int
when (diff <. zero) onNegative
......
......@@ -8,11 +8,22 @@
-- @
module Indigo.Rebinded
( ifThenElse
( -- * @if/then/[email protected] construct
ifThenElse
-- * Numerical literals resolution
, fromInteger
, nat
, int
, mutez
-- * Re-exports
, IsLabel (..)
) where
import qualified Prelude as P
import qualified Data.Kind as Kind
import Indigo.Internal
import Indigo.Frontend
import Indigo.Backend.Scope
......@@ -20,6 +31,10 @@ import Indigo.Backend.Conditional (IfConstraint)
import Indigo.Lorentz
import Util.Label (IsLabel(..))
----------------------------------------------------------------------------
-- @if/then/[email protected] construct
----------------------------------------------------------------------------
-- | Defines semantics of @if ... then ... else [email protected] construction for Indigo
-- where the predicate is a generic @[email protected] for which @IsExpr exa [email protected] holds
ifThenElse
......@@ -29,3 +44,40 @@ ifThenElse
-> IndigoM b
-> IndigoM (RetVars a)
ifThenElse cond = if_ (toExpr cond)
----------------------------------------------------------------------------
-- Numerical literals resolution
----------------------------------------------------------------------------
-- | Kind used for 'NumType' as part of the disambiguation machinery.
data NumKind = Nat | Int | Mtz
-- | Disambiguation type used in 'fromInteger' that links a single 'NumKind' to
-- the numeric type to resolve to.
data NumType (n :: NumKind) (t :: Kind.Type) where
NNat :: NumType 'Nat Natural
NInt :: NumType 'Int Integer
NMtz :: NumType 'Mtz Mutez
-- | Numerical literal disambiguation value for a 'Natural', see 'fromInteger'.
nat :: NumType 'Nat Natural
nat = NNat
-- | Numerical literal disambiguation value for an 'Integer', see 'fromInteger'.
int :: NumType 'Int Integer
int = NInt
-- | Numerical literal disambiguation value for a 'Mutez', see 'fromInteger'.
mutez :: NumType 'Mtz Mutez
mutez = NMtz
-- | Defines numerical literals resolution for Indigo.
--
-- It is implemented with an additional 'NumType' argument that disambiguates
-- the resulting type.
-- This allows, for example, @1 [email protected] to be resolved to @1 :: [email protected]
fromInteger :: Integer -> NumType n t -> t
fromInteger val = \case
NNat -> P.fromInteger val
NInt -> val
NMtz -> toMutez (P.fromInteger val)
......@@ -5,7 +5,8 @@ module Test.Decomposition
import Test.QuickCheck (Arbitrary(..), oneof)
import Test.Tasty (TestTree)
import Indigo
import Indigo hiding (fromInteger)
import Indigo.Prelude (fromInteger)
import Lorentz.TypeAnns (HasTypeAnn)
import Michelson.Interpret (MichelsonFailed(..))
import Test.Util
......
......@@ -52,9 +52,9 @@ test_Examples =
whileCheck :: Integer -> Integer -> Either MichelsonFailed Integer
whileCheck param st
| st <= 0 = Right 0
| param == 0 = Left zeroDivFail
| otherwise = Right . sum $ filter ((== 0) . (`mod` param)) [0..(st - 1)]
| st <= (0 int) = Right (0 int)
| param == (0 int) = Left zeroDivFail
| otherwise = Right . sum $ filter ((== (0 int)) . (`mod` param)) [(0 int)..(st - (1 int))]
forEachCheck :: [Integer] -> Integer -> Either MichelsonFailed Integer
forEachCheck param _st = Right $ sum param
......@@ -69,12 +69,12 @@ opsCheck param _st = Right [crConOp, setDelOp]
where
setDelOp = T.OpSetDelegate $ T.SetDelegate param
crConOp = T.OpCreateContract $
T.CreateContract genesisAddress param (toMutez 0) (T.VInt 0)
T.CreateContract genesisAddress param (0 mutez) (T.VInt $ 0 int)
(compileLorentz contractIfLorentz)
assertCheck :: Integer -> Integer -> Either MichelsonFailed Integer
assertCheck param st
| sm <= 0 = Left negativeResFail
| sm <= (0 int) = Left negativeResFail
| otherwise = Right sm
where sm = st + param
......@@ -84,8 +84,8 @@ assertCheck param st
contractVarLorentz :: ContractCode Integer Integer
contractVarLorentz = compileIndigoContract $ \_param ->
when ((5 :: Integer) <. (10 :: Integer)) $ do
_a <- newVar $ (10 :: Integer)
when (5 int <. 10 int) $ do
_a <- newVar $ 10 int
return ()
ifTest
......@@ -93,7 +93,7 @@ ifTest
=> Var Integer
-> IndigoM ()
ifTest param = do
a <- newVar $ (7 :: Integer) +. param
a <- newVar $ 7 int +. param
when (param <. a) $ do
_c <- newVar (storageVar @Integer)
return ()
......@@ -105,7 +105,7 @@ contractIfLorentz = compileIndigoContract ifTest
contractIfValueLorentz :: ContractCode Integer Integer
contractIfValueLorentz = compileIndigoContract $ \param -> do
a <- newVar $ (7 :: Integer) +. param
a <- newVar $ 7 int +. param
when (param <. a) $ do
_c <- newVar (storageVar @Integer)
return ()
......@@ -114,17 +114,17 @@ contractIfValueLorentz = compileIndigoContract $ \param -> do
contractWhileLorentz :: ContractCode Integer Integer
contractWhileLorentz = compileIndigoContract $ \param -> do
i <- newVar @Integer 0
s <- newVar @Integer 0
i <- newVar $ 0 int
s <- newVar $ 0 int
while (i <. storageVar @Integer) $ do
when (i %. param ==. (0 :: Natural)) $
when (i %. param ==. 0 nat) $
s += i
i += (1 :: Integer)
i += 1 int
setVar storageVar s
contractForEachLorentz :: ContractCode [Integer] Integer
contractForEachLorentz = compileIndigoContract $ \param -> do
s <- newVar @Integer 0
s <- newVar $ 0 int
forEach param $ \it -> do
setVar s (s +. it)
setVar storageVar s
......@@ -137,7 +137,7 @@ contractCaseLorentz = compileIndigoContract $ \param -> scope $ do
-- 2. branches can return not exactly the same types
--- it's useful when you have case bodies in-place, like
-- caseT param $
-- ( #cSomething1 //-> const $ return (5 :: Integer)
-- ( #cSomething1 //-> const $ return (5 int)
-- , #cSomething2 //-> (\var -> return (10 +. var))
-- , #cSomething3 //-> return var)
-- Pay attention, that all three branches have different return types
......@@ -180,29 +180,29 @@ contractDocLorentz :: ContractCode Integer Integer
contractDocLorentz = compileIndigoContract $ \param -> do
doc (DDescription "x")
contractName "aaa" (doc $ DDescription "a")
i <- newVar @Integer 10
i <- newVar $ 10 int
docGroup (SomeDocItem . DName "bbb") (doc $ DDescription "b")
setVar storageVar (param +. i)
contractOpsLorentz :: ContractCode (Maybe KeyHash) Address
contractOpsLorentz = compileIndigoContract $ \param -> do
setDelegate param
m <- newVar (toMutez 0)
is <- newVar @Integer 0
m <- newVar $ 0 mutez
is <- newVar $ 0 int
addr <- createContract ifTest param m is
setVar storageVar addr
contractAssertLorentz :: ContractCode Integer Integer
contractAssertLorentz = compileIndigoContract $ \param -> do
s <- newVar (param +. storageVar @Integer)
z <- newVar @Integer 0
z <- newVar $ 0 int
assert negativeResM (s >. z)
setVar storageVar s
contractCommentLorentz :: ContractCode Integer Integer
contractCommentLorentz = compileIndigoContract $ \param -> do
s <- commentAroundStmt "param plus storage" $ newVar (param +. storageVar @Integer)
_z <- newVar @Integer 0
_z <- newVar $ 0 int
justComment "just comment"
setVar storageVar s
......@@ -224,8 +224,8 @@ expectedDocContract =
L.doc (DDescription "x") #
-- contractName "aaa" (doc $ DDescription "a")
L.contractName "aaa" (L.doc $ DDescription "a") #
-- i <- newVar @Integer 10
L.push @Integer 10 #
-- i <- newVar $ 10 int
L.push (10 int) #
-- docGroup (SomeDocItem . DName "bbb") (doc $ DDescription "b")
L.docGroup (SomeDocItem . DName "bbb") (L.doc $ DDescription "b") #
-- duplicate `i`
......
......@@ -14,7 +14,8 @@ import Test.QuickCheck (Arbitrary(..))
import Test.Tasty (TestTree)
import Util.Test.Arbitrary ()
import Indigo
import Indigo hiding (fromInteger)
import Indigo.Prelude (fromInteger)
import Michelson.Interpret (MichelsonFailed(..), runUnpack)
import Michelson.Interpret.Pack
import Michelson.Runtime.GState (genesisAddress)
......
......@@ -7,7 +7,8 @@ import Test.Tasty (TestTree)
import Test.Hspec.Expectations (shouldThrow, errorCall)
import Test.Tasty.HUnit (testCase)
import Indigo
import Indigo hiding (fromInteger)
import Indigo.Prelude (fromInteger)
import Lorentz.TypeAnns (HasTypeAnn)
import Michelson.Interpret (MichelsonFailed(..))
import Michelson.Runtime.GState
......
......@@ -13,7 +13,8 @@ import Test.Tasty (TestTree, testGroup)
import Test.Tasty.HUnit (testCase)
import Util.Test.Arbitrary ()
import Indigo
import Indigo hiding (fromInteger)
import Indigo.Prelude (fromInteger)
import qualified Lorentz.Instr as L
import qualified Lorentz.Macro as L
import Util.Peano
......
......@@ -22,7 +22,6 @@ As a reminder, for informations on types you can instead consult
[Appendix A: types](AA.md).
<!--
TODO #135: remember to also update the examples in this document
TODO #169: remember to also update the examples in this document
-->
......@@ -55,12 +54,12 @@ before them (e.g. `1 +. 2`, `True ||. False`, etc.)
3. do not return an expression, but a complete statement
For example:
```haskell
1 += 2 -- is invalid, this will not compile
1 int += 2 int -- is invalid, this will not compile
a <- newVar 1
a += 2 -- "a" will have value of "3" after this expression
a <- newVar (1 int)
a += 2 int -- "a" will have value of "3" after this expression
b <- newVar (a += 1) -- is also invalid, because "(a += b)" is not an expression
b <- newVar (a += 1 int) -- is also invalid, because "(a += b)" is not an expression
```
*Type variables* are used in the types of these tables as well, you can recognize
......@@ -201,7 +200,7 @@ TODO #175: remember to update the table above
| Operator | Input type I | Result type | Description |
|-----------|---------------|-------------------|---------------------------------------------------------------------------|
| `isNat` | `Integer` | `Maybe Natural` | Converts an `Integer` to `some` `Natural` if possible, `none` otherwise |
| `int` | `Natural` | `Integer` | Converts a `Natural` to an `Integer` |
| `toInt` | `Natural` | `Integer` | Converts a `Natural` to an `Integer` |
## Bytes and String
......@@ -403,7 +402,7 @@ For example, let's say we have a contract that takes a `View Integer Bool`
greaterThan0 :: Var Integer -> IndigoFunction Bool
greaterThan0 val = defFunction $ do
return (val >. 0)
return (val >. 0 int)
```
As you can see we only need the function to take an `Integer` as parameter and
return a `Bool` to satisfy the `View Integer Bool` requirement.
......@@ -414,7 +413,7 @@ function in place, so the previous example could be written as:
```haskell
-- previous contract code to select the entrypoint
project param $ \val ->
return (val >. 0)
return (val >. 0 int)
```
This is more compact and does not require the definition of a specific function.
......@@ -431,18 +430,18 @@ Note that the branches can return a value, in which case this can be captured as
a variable, but both branches need to return the same type.
For example, these are valid statements:
```haskell
if (1 <= 2)
if 1 int <= 2 int
then do
setVar storage 1 -- this will be executed
setVar storage (1 int) -- this will be executed
return ()
else do
return () -- this will not
resVal <- if (1 == 2)
resVal <- if 1 int ==. 2 int
then do
return False
else do
a <- newVar (1 ==. 1)
a <- newVar (1 int ==. 1 int)
return a
-- we can now use the `resVal` `Bool` variable
```
......@@ -453,8 +452,8 @@ called `when` that only takes the `Bool` condition and a single branch, that wil
be executed only if the condition is `True`.
The first statement above could so be rewritten as:
```haskell
when (1 <= 2) $ do
setVar storage 1
when (1 int <= 2 int) $ do
setVar storage (1 int)
```
In other cases we might want to do exactly the opposite and execute some code
......@@ -462,8 +461,8 @@ only when a `Bool` condition is `False`.
Indigo has a convenience statement for this too, called `unless`.
The previous example for instance could also be written as:
```haskell
unless (1 > 2) $ do
setVar storage 1
unless (1 int > 2 int) $ do
setVar storage (1 int)
```
When we have to deal with `Maybe a`s we often want to know if they are `some a`
......@@ -493,12 +492,12 @@ We also two have statements similar to `when` for convenience:
`while` is the statement that will execute a piece of code as long as a `Bool`
condition holds. For example, this loop would execute twice:
```haskell
i <- newVar 0
while (i < 2) $ do
i <- newVar (0 int)
while (i int < 2 int) $ do
-- more code can be here
i += 1
i += 1 int
-- the code following will get executed after the loop
setVar i 0
setVar i (0 int)
```
`forEach` is instead a way to execute a piece of code over each of the elements
......@@ -506,7 +505,7 @@ of a container (a list, set or map).
For example, given a `numList` variable of type `[Integer]` this will compute
the sum of all its elements:
```haskell
sum <- newVar 0
sum <- newVar (0 int)
forEach numList $ \number -> do
sum += number
```
......
......@@ -6,5 +6,5 @@ import Indigo
exampleContract :: IndigoContract Integer Integer
exampleContract param = defContract $ do
a <- newVar @Integer 1
a <- newVar (1 int)
setVar storageVar (param +. a)
......@@ -7,7 +7,7 @@ import Indigo
exampleContract :: IndigoContract Integer Integer
exampleContract param = defContract $ do
a <- newVar @Integer 1
a <- newVar (1 int)
setVar storageVar (param +. a)
textKeeper :: IndigoContract MText MText
......
......@@ -50,12 +50,12 @@ parameter variable (in case we want to use something other than `param`).
The indented lines that follow are the actual contract code.
In this case:
```haskell
a <- newVar @Integer 1
a <- newVar (1 int)
setVar storageVar (param +. a)
```
these lines show both methods of direct variable manipulation:
- we can create a new variable by using `newVar`, on its right we put the
expression we want to assign to the new variable (`1`) and on the left of the
expression we want to assign to the new variable (`1 int`) and on the left of the
arrow `<-` the name we'll be referring to with (`a`)
- we can set an existing variable to a new value by using `setVar`, immediately
followed by the variable we want to set (`storageVar`) and the expression whose
......@@ -63,10 +63,11 @@ these lines show both methods of direct variable manipulation:
You may have noticed that we never defined `storageVar`; we don't need to because
`storageVar` is a special variable that is always available in contracts.
You may have also noticed that we had to tell `newVar` what was the type of the
new variable `a`; this is not always necessary, but we need to do so when the
type of the value (`1`) is ambiguous (in this case, for example, it could have
been a `Natural`).
You may have also noticed that we had to specify `int` after `1`, this is always
necessary because numeric types are otherwise ambiguous; a numeric literal, like
`1`, needs to be followed by either `int`, `nat` or `mutez` to clarify that its
type is `Integer`, `Natural` or `Mutez`, respectively.
### Making a new contract
......
......@@ -6,11 +6,11 @@ import Indigo
mathContract :: IndigoContract Integer Integer
mathContract param = defContract $ do
zero <- newVar @Integer 0
zero <- newVar (0 int)
_z <- newVar zero
five <- newVar (zero +. (6 :: Integer))
five -= (1 :: Integer)
storage += abs ((param *. five) -. (10 :: Integer))
five <- newVar (zero +. 6 int)
five -= 1 int
storage += abs ((param *. five) -. 10 int)
storage :: HasStorage Integer => Var Integer
storage = storageVar
......@@ -29,9 +29,9 @@ with the explanation. Remember: you can always bring it into the REPL by using
We can see in the first line of the code that it creates a variable starting from
the simplest expression, a constant: `0`.
It uses this to create a new variable `zero` with `newVar`, all variables are
expressions too, so we can see in the next line how it creates another variable
from it.
Here this constant is used to create a new variable `zero` with `newVar`, all
variables are expressions too, so we can see in the next line how it creates
another variable from it.
Note on syntax: the second variable is also an example of an unused one, you can
see how its name starts with an underscore: `_z`.
......
......@@ -15,21 +15,21 @@ instance ParameterHasEntryPoints IncrementIf where
controlContract :: IndigoContract IncrementIf Natural
controlContract param = defContract $ do
base <- newVar @Natural 10
base <- newVar (10 nat)
result <- caseT param $
( #cIsZero //-> \val -> do
return (val ==. (0 :: Integer))
return (val ==. 0 int)
, #cHasDigitOne //-> \val -> do
checkRes <- newVar False
while (val >. base &&. checkRes ==. False) $ do
setVar val (val /. base)
remainder <- newVar (val %. base)
setVar checkRes (remainder ==. (1 :: Natural))
setVar checkRes (remainder ==. 1 nat)
return checkRes
)
if result ==. False
then setVar storage (0 :: Natural)
else storage += (1 :: Natural)
then setVar storage (0 nat)
else storage += 1 nat
storage :: HasStorage Natural => Var Natural
storage = storageVar
......@@ -53,13 +53,13 @@ the `//->` for `#cIsZero`. Here we take the `Integer` parameter of `IsZero`,
call it `val`, and start a code block with `do`, the isolated code is:
```haskell
\val -> do
return (val ==. (0 :: Integer))
return (val ==. 0 int)
```
that just returns `True` if `val` is `0` and `False` otherwise.
This is indeed so simple it could have been defined without the code-block (and
so the `do`) in a single line as:
```haskell
\val -> return (val ==. (0 :: Integer))
\val -> return (val ==. 0 int)
```
Let's look instead at the isolated code for the second branch, the one for
......@@ -70,7 +70,7 @@ Let's look instead at the isolated code for the second branch, the one for
while (val >. base &&. checkRes ==. False) $ do
setVar val (val /. base)
remainder <- newVar (val %. base)
setVar checkRes (remainder ==. (1 :: Natural))
setVar checkRes (remainder ==. 1 nat)
return checkRes
```
here we take the `Natural` parameter of `HasDigitOne` and we call it `val`, then
......@@ -98,8 +98,8 @@ Going back to the contract as a whole for just a second we can see, after
Please note the indentation for it, which is:
```haskell
if result ==. False
then setVar storage (0 :: Natural)
else storage += (1 :: Natural)
then setVar storage (0 nat)
else storage += 1 nat
```
this is because `if/then/else` is not a code-block, but a single statement, so
we could have written it in a single line.
......
......@@ -23,25 +23,25 @@ functionsContract param = defContract $ do
checkZero :: Var Integer -> IndigoFunction Bool
checkZero val = defFunction $ do