Merge pull request #944 from michaelpj/imp/post-size-removal-tidy

Post size removal tidy

language-plutus-core/README.md

@@ -104,15 +104,11 @@ echo "(program 0.1.0 [(lam x [(con integer) (con 2)] x) (con 2 ! 4)])" | plc eva
 
 #### Tests
 
-A term generation machinery sits in the [`Language.PlutusCore.Generators.Internal.Entity`](generators/Language/PlutusCore/Generators/Internal/Entity.hs) module. It allows to generate terms that contain built-ins (integers, bytestrings, sizes and booleans), constant applications and first-order functions. E.g.
-
-```
-[ (lam x_0 [ (con integer) (con 3) ] [ (lam x_1 [ (con integer) (con 3) ] [ [ { (con remainderInteger) (con 3) } [ [ { (con multiplyInteger) (con 3) } x_1 ] x_0 ] ] [ [ { (con addInteger) (con 3) } x_0 ] x_1 ] ]) [ [ { (con divideInteger) (con 3) } [ [ { (con addInteger) (con 3) } x_0 ] x_0 ] ] [ [ { (con multiplyInteger) (con 3) } x_0 ] x_0 ] ] ]) [ [ { (con divideInteger) (con 3) } [ [ { (con subtractInteger) (con 3) } [ [ { (con addInteger) (con 3) } (con 3 ! -1053) ] (con 3 ! 269) ] ] [ [ { (con divideInteger) (con 3) } (con 3 ! -1352) ] (con 3 ! -849) ] ] ] [ [ { { (con resizeInteger) (con 3) } (con 3) } (con 3) ] [ [ { { (con resizeInteger) (con 3) } (con 3) } (con 3) ] (con 3 ! 37) ] ] ] ]
-```
+A term generation machinery sits in the [`Language.PlutusCore.Generators.Internal.Entity`](generators/Language/PlutusCore/Generators/Internal/Entity.hs) module. It allows to generate terms that contain built-ins (integers, bytestrings, sizes and booleans), constant applications and first-order functions.
 
 The generator makes sure a term is well-typed and keeps track of what it's supposed to evaluate to.
 
-There is an executable that prints a term and the expected result of evaluation. Run it as `language-plutus-core-generate-evaluation-test` and you'll be shown something like
+There is an executable that prints a term and the expected result of evaluation. Run it as `language-plutus-core-generate-evaluation-test`, and you'll be shown two terms separated by a newline.
 
 ```
 (program 0.1.0 [ (lam x_0 [ (con integer) (con 2) ] [ [ { (con lessThanInteger) (con 2) } [ [ { (con divideInteger) (con 2) } x_0 ] [ [ { (con divideInteger) (con 2) } x_0 ] x_0 ] ] ] [ [ { (con remainderInteger) (con 2) } x_0 ] x_0 ] ]) [ [ { (con addInteger) (con 2) } [ [ { { (con resizeInteger) (con 2) } (con 2) } (con 2) ] [ [ { (con subtractInteger) (con 2) } (con 2 ! 26) ] (con 2 ! 63) ] ] ] [ [ { (con multiplyInteger) (con 2) } [ [ { (con divideInteger) (con 2) } (con 2 ! 61) ] (con 2 ! -7) ] ] [ [ { (con subtractInteger) (con 2) } (con 2 ! 16) ] (con 2 ! 74) ] ] ] ])

language-plutus-core/generators/Language/PlutusCore/Generators/AST.hs

@@ -41,7 +41,6 @@ genName = Name () <$> name' <*> int'
           isKw "all"        = True
           isKw "bytestring" = True
           isKw "integer"    = True
-          isKw "size"       = True
           isKw "type"       = True
           isKw "program"    = True
           isKw "con"        = True
@@ -70,7 +69,7 @@ genConstant :: MonadGen m => m (Constant ())
 genConstant = Gen.choice [genInt, genBS]
     where int' = Gen.integral_ (Range.linear (-10000000) 10000000)
           string' = BSL.fromStrict <$> Gen.utf8 (Range.linear 0 40) Gen.unicode
-          genInt = makeAutoSizedBuiltinInt <$> int'
+          genInt = makeBuiltinInt <$> int'
           genBS = BuiltinBS () <$> string'
 
 genType :: MonadGen m => m (Type TyName ())

language-plutus-core/generators/Language/PlutusCore/Generators/Interesting.hs

@@ -8,7 +8,6 @@ module Language.PlutusCore.Generators.Interesting
     ( TermGen
     , genOverapplication
     , factorial
-    , applyFactorial
     , genFactorial
     , genNaiveFib
     , genNatRoundtrip
@@ -47,8 +46,8 @@ type TermGen a = Gen (TermOf (TypedBuiltinValue a))
 -- > lessThanInteger {integer} $i1 $i2 {integer} $j1 $j2 == if i1 < i2 then j1 else j2
 genOverapplication :: TermGen Integer
 genOverapplication = do
-    let typedInt1 = TypedBuiltinSized TypedBuiltinSizedInt
-        typedInt2 = TypedBuiltinSized TypedBuiltinSizedInt
+    let typedInt1 = TypedBuiltinStatic TypedBuiltinStaticInt
+        typedInt2 = TypedBuiltinStatic TypedBuiltinStaticInt
         int2 = typedBuiltinToType typedInt2
     TermOf ti1 i1 <- genTypedBuiltinDef typedInt1
     TermOf ti2 i2 <- genTypedBuiltinDef typedInt1
@@ -73,7 +72,7 @@ factorial = runQuote $ do
     return
         . LamAbs () i int
         . mkIterApp () List.product
-        $ [ mkIterApp () List.enumFromTo [ makeDynBuiltinInt 1 , Var () i]]
+        $ [ mkIterApp () List.enumFromTo [ makeIntConstant 1 , Var () i]]
 
 -- | The naive exponential fibonacci function as a PLC term.
 --
@@ -101,33 +100,26 @@ naiveFib = runQuote $ do
               . LamAbs () i intS
               $ mkIterApp () (TyInst () ifThenElse intS)
                   [ mkIterApp () (builtinNameAsTerm LessThanEqInteger)
-                      [Var () i, makeDynBuiltinInt 1]
+                      [Var () i, makeIntConstant 1]
                   , LamAbs () u unit $ Var () i
                   , LamAbs () u unit $ mkIterApp () (builtinNameAsTerm AddInteger)
                       [ Apply () (Var () rec) $ mkIterApp () (builtinNameAsTerm SubtractInteger)
-                          [Var () i, makeDynBuiltinInt 1]
+                          [Var () i, makeIntConstant 1]
                       , Apply () (Var () rec) $ mkIterApp () (builtinNameAsTerm SubtractInteger)
-                          [Var () i, makeDynBuiltinInt 2]
+                          [Var () i, makeIntConstant 2]
                       ]
                   ]
             , Var () i0
             ]
 
--- | Apply some factorial function to its 'Integer' argument.
--- This function exist, because we have another implementation via dynamic built-ins
--- and want to compare it to the direct implementation from the above.
-applyFactorial :: Term TyName Name () -> Integer -> Term TyName Name ()
-applyFactorial fact iv = Apply () fact i where
-    i    = Constant () $ BuiltinInt () iv
-
 -- | Generate a term that computes the factorial of an @integer@ and return it
 -- along with the factorial of the corresponding 'Integer' computed on the Haskell side.
 genFactorial :: TermGen Integer
 genFactorial = do
     let m = 10
-        typedIntS = TypedBuiltinSized TypedBuiltinSizedInt
+        typedIntS = TypedBuiltinStatic TypedBuiltinStaticInt
     iv <- Gen.integral $ Range.linear 1 m
-    let term = applyFactorial factorial iv
+    let term = Apply () factorial (makeIntConstant iv)
     return . TermOf term . TypedBuiltinValue typedIntS $ Prelude.product [1..iv]
 
 -- | Generate a term that computes the ith Fibonacci number and return it
@@ -136,7 +128,7 @@ genNaiveFib :: TermGen Integer
 genNaiveFib = do
     let fibs = scanl (+) 0 $ 1 : fibs
         m = 16
-        typedIntS = TypedBuiltinSized TypedBuiltinSizedInt
+        typedIntS = TypedBuiltinStatic TypedBuiltinStaticInt
     iv <- Gen.integral $ Range.linear 0 m
     let term = Apply () naiveFib . Constant () $ BuiltinInt () iv
     return . TermOf term . TypedBuiltinValue typedIntS $ fibs `genericIndex` iv
@@ -147,7 +139,7 @@ genNaiveFib = do
 -- along with the original 'Integer'
 genNatRoundtrip :: TermGen Integer
 genNatRoundtrip = do
-    let typedIntS = TypedBuiltinSized TypedBuiltinSizedInt
+    let typedIntS = TypedBuiltinStatic TypedBuiltinStaticInt
     TermOf _ iv <- Gen.filter ((>= 0) . _termOfValue) $ genTypedBuiltinDef typedIntS
     let term = mkIterApp () natToInteger [metaIntegerToNat iv]
     return . TermOf term $ TypedBuiltinValue typedIntS iv
@@ -175,7 +167,7 @@ natSum = runQuote $ do
 -- sum elements of the list (see 'Sum') and return it along with the sum of the original list.
 genListSum :: TermGen Integer
 genListSum = do
-    let typedIntS = TypedBuiltinSized TypedBuiltinSizedInt
+    let typedIntS = TypedBuiltinStatic TypedBuiltinStaticInt
         intS = typedBuiltinToType typedIntS
     ps <- Gen.list (Range.linear 0 10) $ genTypedBuiltinDef typedIntS
     let list = metaListToList intS $ map _termOfTerm ps
@@ -187,7 +179,7 @@ genListSum = do
 -- means the same thing in Haskell and PLC. Terms are generated using 'genTermLoose'.
 genIfIntegers :: TermGen Integer
 genIfIntegers = do
-    let typedIntS = TypedBuiltinSized TypedBuiltinSizedInt
+    let typedIntS = TypedBuiltinStatic TypedBuiltinStaticInt
         intS = typedBuiltinToType typedIntS
     TermOf b bv <- genTermLoose $ TypedBuiltinDyn @Bool
     TermOf i iv <- genTermLoose typedIntS
@@ -203,7 +195,7 @@ genIfIntegers = do
 -- | Check that builtins can be partially applied.
 genApplyAdd1 :: TermGen Integer
 genApplyAdd1 = do
-    let typedIntS = TypedBuiltinSized TypedBuiltinSizedInt
+    let typedIntS = TypedBuiltinStatic TypedBuiltinStaticInt
         intS = typedBuiltinToType typedIntS
     TermOf i iv <- genTermLoose typedIntS
     TermOf j jv <- genTermLoose typedIntS
@@ -217,7 +209,7 @@ genApplyAdd1 = do
 -- | Check that builtins can be partially applied.
 genApplyAdd2 :: TermGen Integer
 genApplyAdd2 = do
-    let typedIntS = TypedBuiltinSized TypedBuiltinSizedInt
+    let typedIntS = TypedBuiltinStatic TypedBuiltinStaticInt
         intS = typedBuiltinToType typedIntS
     TermOf i iv <- genTermLoose typedIntS
     TermOf j jv <- genTermLoose typedIntS

language-plutus-core/generators/Language/PlutusCore/Generators/Internal/Denotation.hs

@@ -33,7 +33,7 @@ data Denotation object r = forall a. Denotation
     , _denotationItself :: a                              -- ^ The denotation of the object.
                                                           -- E.g. the denotation of 'AddInteger' is '(+)'.
     , _denotationScheme :: TypeScheme a r                 -- ^ The 'TypeScheme' of the object.
-                                                          -- See 'sizeIntIntInt' for example.
+                                                          -- See 'intIntInt' for example.
     }
 
 -- | A member of a 'DenotationContext'.

language-plutus-core/generators/Language/PlutusCore/Generators/Internal/Dependent.hs

@@ -22,13 +22,13 @@ liftOrdering GT = GGT
 
 -- I tried using the 'dependent-sum-template' package,
 -- but see https://stackoverflow.com/q/50048842/3237465
-instance GEq TypedBuiltinSized where
-    TypedBuiltinSizedInt  `geq` TypedBuiltinSizedInt  = Just Refl
-    TypedBuiltinSizedBS   `geq` TypedBuiltinSizedBS   = Just Refl
+instance GEq TypedBuiltinStatic where
+    TypedBuiltinStaticInt  `geq` TypedBuiltinStaticInt  = Just Refl
+    TypedBuiltinStaticBS   `geq` TypedBuiltinStaticBS   = Just Refl
     _                     `geq` _                     = Nothing
 
 instance GEq TypedBuiltin where
-    TypedBuiltinSized tbs1 `geq` TypedBuiltinSized tbs2 = tbs1 `geq` tbs2
+    TypedBuiltinStatic tbs1 `geq` TypedBuiltinStatic tbs2 = tbs1 `geq` tbs2
     dyn1@TypedBuiltinDyn         `geq` dyn2@TypedBuiltinDyn         = do
         guard $ prettyString dyn1 == prettyString dyn2
         Just $ unsafeCoerce Refl
@@ -37,15 +37,15 @@ instance GEq TypedBuiltin where
 instance GCompare TypedBuiltin where
     tb1                          `gcompare` tb2
         | Just Refl <- tb1  `geq` tb2  = GEQ
-    TypedBuiltinSized tbs1 `gcompare` TypedBuiltinSized tbs2
+    TypedBuiltinStatic tbs1 `gcompare` TypedBuiltinStatic tbs2
         | Just Refl <- tbs1 `geq` tbs2 = GEQ
         | otherwise                    = case (tbs1, tbs2) of
-            (TypedBuiltinSizedInt , _                    ) -> GLT
-            (TypedBuiltinSizedBS  , TypedBuiltinSizedInt ) -> GGT
-            (TypedBuiltinSizedBS  , _                    ) -> GLT
+            (TypedBuiltinStaticInt , _                    )  -> GLT
+            (TypedBuiltinStaticBS  , TypedBuiltinStaticInt ) -> GGT
+            (TypedBuiltinStaticBS  , _                    )  -> GLT
     dyn1@TypedBuiltinDyn         `gcompare` dyn2@TypedBuiltinDyn
         = liftOrdering $ prettyString dyn1 `compare` prettyString dyn2
-    TypedBuiltinSized _        `gcompare` TypedBuiltinDyn
+    TypedBuiltinStatic _        `gcompare` TypedBuiltinDyn
         = GLT
-    TypedBuiltinDyn              `gcompare` TypedBuiltinSized _
+    TypedBuiltinDyn              `gcompare` TypedBuiltinStatic _
         = GGT

language-plutus-core/generators/Language/PlutusCore/Generators/Internal/Entity.hs

@@ -12,7 +12,7 @@ module Language.PlutusCore.Generators.Internal.Entity
     ( PlcGenT
     , IterAppValue(..)
     , runPlcT
-    , genBuiltinSized
+    , genBuiltinStatic
     , withTypedBuiltinGen
     , withCheckedTermGen
     , genIterAppValue
@@ -89,14 +89,14 @@ revealUnique :: Name a -> Name a
 revealUnique (Name ann name uniq) =
     Name ann (name <> (prettyText $ unUnique uniq)) uniq
 
--- | Generate a 'BuiltinSized'.
-genBuiltinSized :: Monad m => GenT m BuiltinSized
-genBuiltinSized = Gen.element [BuiltinSizedInt, BuiltinSizedBS]
+-- | Generate a 'BuiltinStatic'.
+genBuiltinStatic :: Monad m => GenT m BuiltinStatic
+genBuiltinStatic = Gen.element [BuiltinStaticInt, BuiltinStaticBS]
 
 -- | Generate a 'Builtin' and supply its typed version to a continuation.
 withTypedBuiltinGen
     :: Monad m => (forall a. TypedBuiltin a -> GenT m c) -> GenT m c
-withTypedBuiltinGen k = genBuiltinSized >>= \b -> withTypedBuiltinSized b (k . TypedBuiltinSized)
+withTypedBuiltinGen k = genBuiltinStatic >>= \b -> withTypedBuiltinStatic b (k . TypedBuiltinStatic)
 
 -- | Generate a 'Term' along with the value it computes to,
 -- having a generator of terms of built-in types.

language-plutus-core/generators/Language/PlutusCore/Generators/Internal/TypedBuiltinGen.hs

@@ -85,28 +85,28 @@ updateTypedBuiltinGen tbNew genX genTb tbOld
     | Just Refl <- tbNew `geq` tbOld = attachCoercedTerm tbOld genX
     | otherwise                      = genTb tbOld
 
--- | Update a sized typed built-ins generator by overwriting the generator for a certain built-in.
-updateTypedBuiltinGenSized
+-- | Update a typed built-ins generator by overwriting the generator for a certain built-in.
+updateTypedBuiltinGenStatic
     :: (Monad m, PrettyDynamic a)
-    => TypedBuiltinSized a  -- ^ A generator of which sized built-in to overwrite.
+    => TypedBuiltinStatic a  -- ^ A generator of which sized built-in to overwrite.
     -> GenT m a             -- ^ A new generator
     -> TypedBuiltinGenT m   -- ^ An old typed built-ins generator.
     -> TypedBuiltinGenT m   -- ^ The updated typed built-ins generator.
-updateTypedBuiltinGenSized tbsNew genX genTb tbOld = case tbOld of
-    TypedBuiltinSized tbsOld | Just Refl <- tbsNew `geq` tbsOld -> attachCoercedTerm tbOld genX
-    _                                                           -> genTb tbOld
+updateTypedBuiltinGenStatic tbsNew genX genTb tbOld = case tbOld of
+    TypedBuiltinStatic tbsOld | Just Refl <- tbsNew `geq` tbsOld -> attachCoercedTerm tbOld genX
+    _                                                            -> genTb tbOld
 
 -- | Update a typed built-ins generator by overwriting the @integer@s generator.
 updateTypedBuiltinGenInt
     :: Monad m
     => GenT m Integer -> TypedBuiltinGenT m -> TypedBuiltinGenT m
-updateTypedBuiltinGenInt = updateTypedBuiltinGenSized TypedBuiltinSizedInt
+updateTypedBuiltinGenInt = updateTypedBuiltinGenStatic TypedBuiltinStaticInt
 
 -- | Update a typed built-ins generator by overwriting the @bytestring@s generator.
 updateTypedBuiltinGenBS
     :: Monad m
     => GenT m BSL.ByteString -> TypedBuiltinGenT m -> TypedBuiltinGenT m
-updateTypedBuiltinGenBS = updateTypedBuiltinGenSized TypedBuiltinSizedBS
+updateTypedBuiltinGenBS = updateTypedBuiltinGenStatic TypedBuiltinStaticBS
 
 -- | Update a typed built-ins generator by overwriting the @boolean@s generator.
 updateTypedBuiltinGenBool
@@ -121,7 +121,7 @@ genTypedBuiltinFail tb = fail $ fold
     , prettyString tb
     ]
 
--- | A default sized built-ins generator that produces values in bounds seen in the spec.
+-- | A default built-ins generator that produces values in bounds seen in the spec.
 genTypedBuiltinDef :: Monad m => TypedBuiltinGenT m
 genTypedBuiltinDef
     = updateTypedBuiltinGenInt