Skip to content

Commit

Permalink
Make more things run in Quote to avoid shadowing
Browse files Browse the repository at this point in the history
Historically Roman's argument was that they were all fine up to
shadowing and you should just rename them when you put them in. But we
definitely weren't doing that, and it made it quite hard to debug the
actual issue due to rampant shadowing. So I just made things run in
`Quote`, which really isn't so bad.
  • Loading branch information
michaelpj committed Sep 15, 2021
1 parent f41ed1e commit c7a27c9
Show file tree
Hide file tree
Showing 17 changed files with 80 additions and 59 deletions.
10 changes: 5 additions & 5 deletions plutus-core/generators/PlutusCore/Generators/Interesting.hs
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ naiveFib iv = runQuote $ do
let
intS = mkTyBuiltin @_ @Integer ()
fib = LamAbs () i0 intS
$ mkIterApp () (mkIterInst () fix [intS, intS])
$ mkIterApp () (mkIterInst () (runQuote fix) [intS, intS])
[ LamAbs () rec (TyFun () intS intS)
. LamAbs () i intS
$ mkIterApp () (TyInst () ifThenElse intS)
Expand Down Expand Up @@ -191,7 +191,7 @@ genIfIntegers = do
TermOf b bv <- genTermLoose AsKnownType
TermOf i iv <- genTermLoose typedInt
TermOf j jv <- genTermLoose typedInt
let instConst = Apply () $ mkIterInst () Function.const [int, unit]
let instConst = Apply () $ mkIterInst () (runQuote Function.const) [int, unit]
value = if bv then iv else jv
term =
mkIterApp ()
Expand All @@ -207,7 +207,7 @@ genApplyAdd1 = do
TermOf i iv <- genTermLoose typedInt
TermOf j jv <- genTermLoose typedInt
let term =
mkIterApp () (mkIterInst () applyFun [int, int])
mkIterApp () (mkIterInst () (runQuote applyFun) [int, int])
[ Apply () (Builtin () AddInteger) i
, j
]
Expand All @@ -221,7 +221,7 @@ genApplyAdd2 = do
TermOf i iv <- genTermLoose typedInt
TermOf j jv <- genTermLoose typedInt
let term =
mkIterApp () (mkIterInst () applyFun [int, TyFun () int int])
mkIterApp () (mkIterInst () (runQuote applyFun) [int, TyFun () int int])
[ Builtin () AddInteger
, i
, j
Expand All @@ -244,7 +244,7 @@ genDivideByZeroDrop = do
int = toTypeAst typedInt
TermOf i iv <- genTermLoose typedInt
let term =
mkIterApp () (mkIterInst () Function.const [int, int])
mkIterApp () (mkIterInst () (runQuote Function.const) [int, int])
[ mkConstant @Integer () iv
, mkIterApp () (Builtin () op) [i, mkConstant @Integer () 0]
]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ ofoldrData = runQuote $ do
i <- freshName "i"
ds <- freshName "ds"
es <- freshName "es"
fixT <- fix
let listData = mkTyBuiltin @_ @[Data] ()
listR = TyApp () list r
opair a = mkIterTyApp () pair [a, a]
Expand All @@ -74,7 +75,7 @@ ofoldrData = runQuote $ do
. lamAbs () fList (TyFun () listR r)
. lamAbs () fI (TyFun () integer r)
. lamAbs () fB (TyFun () (mkTyBuiltin @_ @ByteString ()) r)
. apply () (mkIterInst () fix [dataTy, r])
. apply () (mkIterInst () fixT [dataTy, r])
. lamAbs () rec (TyFun () dataTy r)
. lamAbs () d dataTy
$ mkIterApp () (tyInst () (unwrap' () (var () d)) r)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,7 @@ foldrInterList = runQuote $ do
xs' <- freshName "xs'"
x' <- freshName "x'"
y' <- freshName "y'"
fixT <- fix
let interlistOf a' b' = mkIterTyApp () interlist [TyVar () a', TyVar () b']
fTy a' b' = mkIterTyFun () [TyVar () a', TyVar () b', TyVar () r] $ TyVar () r
fixTyArg2
Expand All @@ -127,7 +128,7 @@ foldrInterList = runQuote $ do
. TyFun () (fTy a b)
. TyFun () (interlistOf a b)
$ TyVar () r
instedFix = mkIterInst () fix [unit, fixTyArg2]
instedFix = mkIterInst () fixT [unit, fixTyArg2]
unwrappedXs = TyInst () (Unwrap () (Var () xs)) $ TyVar () r
instedRec = mkIterInst () (Apply () (Var () rec) unitval) [TyVar () b, TyVar () a]
return
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -30,12 +30,13 @@ omapList = runQuote $ do
xs <- freshName "xs"
x <- freshName "x"
xs' <- freshName "xs'"
fixT <- fix
let listA = TyApp () list $ TyVar () a
unwrap' ann = apply ann . tyInst () (mapFun Left caseList) $ TyVar () a
return
. tyAbs () a (Type ())
. lamAbs () f (TyFun () (TyVar () a) $ TyVar () a)
. apply () (mkIterInst () fix [listA, listA])
. apply () (mkIterInst () fixT [listA, listA])
. lamAbs () rec (TyFun () listA listA)
. lamAbs () xs listA
. apply () (apply () (tyInst () (unwrap' () (var () xs)) listA) $ var () xs)
Expand Down
56 changes: 29 additions & 27 deletions plutus-core/plutus-core/stdlib/PlutusCore/StdLib/Data/Function.hs
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,8 @@ import Control.Monad
-- | 'id' as a PLC term.
--
-- > /\(A :: *) -> \(x : A) -> x
idFun :: TermLike term TyName Name uni fun => term ()
idFun = runQuote $ do
idFun :: TermLike term TyName Name uni fun => Quote (term ())
idFun = do
a <- freshTyName "a"
x <- freshName "x"
return
Expand All @@ -48,8 +48,8 @@ idFun = runQuote $ do
-- | 'const' as a PLC term.
--
-- > /\(A B :: *) -> \(x : A) (y : B) -> x
const :: TermLike term TyName Name uni fun => term ()
const = runQuote $ do
const :: TermLike term TyName Name uni fun => Quote (term ())
const = do
a <- freshTyName "a"
b <- freshTyName "b"
x <- freshName "x"
Expand All @@ -64,8 +64,8 @@ const = runQuote $ do
-- | '($)' as a PLC term.
--
-- > /\(A B :: *) -> \(f : A -> B) (x : A) -> f x
applyFun :: TermLike term TyName Name uni fun => term ()
applyFun = runQuote $ do
applyFun :: TermLike term TyName Name uni fun => Quote (term ())
applyFun = do
a <- freshTyName "a"
b <- freshTyName "b"
f <- freshName "f"
Expand All @@ -79,9 +79,9 @@ applyFun = runQuote $ do

-- | @Self@ as a PLC type.
--
-- > fix \(self :: * -> *) (a :: *) -> self a -> a
selfData :: RecursiveType uni fun ()
selfData = runQuote $ do
-- > \(a ::*) -> fix \(self :: * -> *) (a :: *) -> self a -> a
selfData :: Quote (RecursiveType uni fun ())
selfData = do
self <- freshTyName "self"
a <- freshTyName "a"
makeRecursiveType () self [TyVarDecl () a $ Type ()]
Expand All @@ -91,9 +91,9 @@ selfData = runQuote $ do
-- | @unroll@ as a PLC term.
--
-- > /\(a :: *) -> \(s : self a) -> unwrap s s
unroll :: TermLike term TyName Name uni fun => term ()
unroll = runQuote $ do
let self = _recursiveType selfData
unroll :: TermLike term TyName Name uni fun => Quote (term ())
unroll = do
self <- _recursiveType <$> selfData
a <- freshTyName "a"
s <- freshName "s"
return
Expand All @@ -108,19 +108,20 @@ unroll = runQuote $ do
-- > unroll {a -> b} (iwrap selfF (a -> b) \(s : self (a -> b)) \(x : a) -> f (unroll {a -> b} s) x)
--
-- See @plutus/runQuote $ docs/fomega/z-combinator-benchmarks@ for details.
fix :: TermLike term TyName Name uni fun => term ()
fix = fst fixAndType
fix :: TermLike term TyName Name uni fun => Quote (term ())
fix = fst <$> fixAndType

fixAndType :: TermLike term TyName Name uni fun => (term (), Type TyName uni ())
fixAndType = runQuote $ do
let RecursiveType self wrapSelf = selfData
fixAndType :: TermLike term TyName Name uni fun => Quote (term (), Type TyName uni ())
fixAndType = do
RecursiveType self wrapSelf <- selfData
a <- freshTyName "a"
b <- freshTyName "b"
f <- freshName "f"
s <- freshName "s"
x <- freshName "x"
unrollT <- unroll
let funAB = TyFun () (TyVar () a) $ TyVar () b
unrollFunAB = tyInst () unroll funAB
unrollFunAB = tyInst () unrollT funAB
let selfFunAB = TyApp () self funAB
let fixTerm =
tyAbs () a (Type ())
Expand Down Expand Up @@ -167,11 +168,11 @@ natTransId f = do
-- > forall (F :: * -> *) .
-- > ((F ~> Id) -> (F ~> Id)) ->
-- > ((F ~> F) -> (F ~> Id))
fixBy :: TermLike term TyName Name uni fun => term ()
fixBy = fst fixByAndType
fixBy :: TermLike term TyName Name uni fun => Quote (term ())
fixBy = fst <$> fixByAndType

fixByAndType :: TermLike term TyName Name uni fun => (term (), Type TyName uni ())
fixByAndType = runQuote $ do
fixByAndType :: TermLike term TyName Name uni fun => Quote (term (), Type TyName uni ())
fixByAndType = do
f <- freshTyName "F"

-- by : (F ~> Id) -> (F ~> Id)
Expand All @@ -187,10 +188,11 @@ fixByAndType = runQuote $ do
pure $ TyFun () nt1 nt2

-- instantiatedFix = fix {F ~> F} {F ~> Id}
fixT <- fix
instantiatedFix <- do
nt1 <- natTrans (TyVar () f) (TyVar () f)
nt2 <- natTransId (TyVar () f)
pure $ tyInst () (tyInst () fix nt1) nt2
pure $ tyInst () (tyInst () fixT nt1) nt2

-- rec : (F ~> F) -> (F ~> Id)
recc <- freshName "rec"
Expand Down Expand Up @@ -248,11 +250,11 @@ fixByAndType = runQuote $ do
-- > (An -> Bn) ->
-- > Q) ->
-- > (forall R :: * . ((A1 -> B1) -> ... (An -> Bn) -> R) -> R)
fixN :: TermLike term TyName Name uni fun => Integer -> term () -> term ()
fixN n fixByTerm = fst (fixNAndType n fixByTerm)
fixN :: TermLike term TyName Name uni fun => Integer -> term () -> Quote (term ())
fixN n fixByTerm = fst <$> fixNAndType n fixByTerm

fixNAndType :: TermLike term TyName Name uni fun => Integer -> term () -> (term (), Type TyName uni ())
fixNAndType n fixByTerm = runQuote $ do
fixNAndType :: TermLike term TyName Name uni fun => Integer -> term () -> Quote (term (), Type TyName uni ())
fixNAndType n fixByTerm = do
-- the list of pairs of A and B types
asbs <- replicateM (fromIntegral n) $ do
a <- freshTyName "a"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -73,13 +73,14 @@ foldrList = runQuote $ do
xs' <- freshName "xs'"
let listA = TyApp () list $ TyVar () a
unwrap' ann = apply ann . tyInst () caseList $ TyVar () a
fixT <- fix
-- Copypasted verbatim from @foldrList@ over Scott-encoded lists.
return
. tyAbs () a (Type ())
. tyAbs () r (Type ())
. lamAbs () f (TyFun () (TyVar () a) . TyFun () (TyVar () r) $ TyVar () r)
. lamAbs () z (TyVar () r)
. apply () (mkIterInst () fix [listA, TyVar () r])
. apply () (mkIterInst () fixT [listA, TyVar () r])
. lamAbs () rec (TyFun () listA $ TyVar () r)
. lamAbs () xs listA
. apply () (apply () (tyInst () (unwrap' () (var () xs)) $ TyVar () r) $ var () z)
Expand Down
6 changes: 4 additions & 2 deletions plutus-core/plutus-core/stdlib/PlutusCore/StdLib/Data/Nat.hs
Original file line number Diff line number Diff line change
Expand Up @@ -92,11 +92,12 @@ foldrNat = runQuote $ do
rec <- freshName "rec"
n <- freshName "n"
n' <- freshName "n'"
fixT <- fix
return
. tyAbs () r (Type ())
. lamAbs () f (TyFun () (TyVar () r) (TyVar () r))
. lamAbs () z (TyVar () r)
. apply () (mkIterInst () fix [nat, TyVar () r])
. apply () (mkIterInst () fixT [nat, TyVar () r])
. lamAbs () rec (TyFun () nat $ TyVar () r)
. lamAbs () n nat
. apply () (apply () (tyInst () (unwrap () (var () n)) $ TyVar () r) $ var () z)
Expand All @@ -119,10 +120,11 @@ foldNat = runQuote $ do
z <- freshName "z"
n <- freshName "n"
n' <- freshName "n'"
fixT <- fix
return
. tyAbs () r (Type ())
. lamAbs () f (TyFun () (TyVar () r) (TyVar () r))
. apply () (mkIterInst () fix [TyVar () r, TyFun () nat $ TyVar () r])
. apply () (mkIterInst () fixT [TyVar () r, TyFun () nat $ TyVar () r])
. lamAbs () rec (TyFun () (TyVar () r) . TyFun () nat $ TyVar () r)
. lamAbs () z (TyVar () r)
. lamAbs () n nat
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -114,12 +114,13 @@ foldrList = runQuote $ do
x <- freshName "x"
xs' <- freshName "xs'"
let listA = TyApp () listTy (TyVar () a)
fixT <- fix
return
. tyAbs () a (Type ())
. tyAbs () r (Type ())
. lamAbs () f (TyFun () (TyVar () a) . TyFun () (TyVar () r) $ TyVar () r)
. lamAbs () z (TyVar () r)
. apply () (mkIterInst () fix [listA, TyVar () r])
. apply () (mkIterInst () fixT [listA, TyVar () r])
. lamAbs () rec (TyFun () listA $ TyVar () r)
. lamAbs () xs listA
. apply () (apply () (tyInst () (unwrap () (var () xs)) $ TyVar () r) $ var () z)
Expand Down Expand Up @@ -168,11 +169,12 @@ foldList = runQuote $ do
x <- freshName "x"
xs' <- freshName "xs'"
let listA = TyApp () listTy (TyVar () a)
fixT <- fix
return
. tyAbs () a (Type ())
. tyAbs () r (Type ())
. lamAbs () f (TyFun () (TyVar () r) . TyFun () (TyVar () a) $ TyVar () r)
. apply () (mkIterInst () fix [TyVar () r, TyFun () listA $ TyVar () r])
. apply () (mkIterInst () fixT [TyVar () r, TyFun () listA $ TyVar () r])
. lamAbs () rec (TyFun () (TyVar () r) . TyFun () listA $ TyVar () r)
. lamAbs () z (TyVar () r)
. lamAbs () xs listA
Expand Down Expand Up @@ -230,10 +232,11 @@ enumFromTo = runQuote $ do
let leqInteger = builtin () LessThanEqualsInteger
int = mkTyBuiltin @_ @Integer ()
listInt = TyApp () listTy int
fixT <- fix
return
. lamAbs () n int
. lamAbs () m int
. mkIterApp () (mkIterInst () fix [int, listInt])
. mkIterApp () (mkIterInst () fixT [int, listInt])
$ [ lamAbs () rec (TyFun () int listInt)
. lamAbs () n' int
. mkIterApp () (tyInst () ifThenElse listInt)
Expand Down
13 changes: 7 additions & 6 deletions plutus-core/plutus-core/stdlib/PlutusCore/StdLib/Everything.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ module PlutusCore.StdLib.Everything
import PlutusCore.Default
import PlutusCore.FsTree

import PlutusCore.Quote
import PlutusCore.StdLib.Data.Bool
import PlutusCore.StdLib.Data.ChurchNat
import PlutusCore.StdLib.Data.Data
Expand Down Expand Up @@ -45,12 +46,12 @@ stdLib =
, plcTermFile "ChurchSucc" churchSucc
]
, treeFolderContents "Function"
[ plcTermFile "Const" Function.const
, plcTermFile "Apply" applyFun
, plcTypeFile "Self" $ _recursiveType selfData
, plcTermFile "Unroll" unroll
, plcTermFile "Fix" fix
, plcTermFile "Fix2" $ fixN 2 fixBy
[ plcTermFile "Const" $ runQuote Function.const
, plcTermFile "Apply" $ runQuote applyFun
, plcTypeFile "Self" $ runQuote (_recursiveType <$> selfData)
, plcTermFile "Unroll" $ runQuote unroll
, plcTermFile "Fix" $ runQuote fix
, plcTermFile "Fix2" $ runQuote (fixN 2 =<< fixBy)
]
, treeFolderContents "Integer"
[ plcTypeFile "integer" integer
Expand Down
12 changes: 8 additions & 4 deletions plutus-core/plutus-ir/src/PlutusIR/Compiler/Recursion.hs
Original file line number Diff line number Diff line change
Expand Up @@ -95,17 +95,21 @@ mkFixpoint bs = do

let mkFixByDef = do
name <- liftQuote $ toProgramName fixByKey
let (fixByTerm, fixByType) = Function.fixByAndType
(fixByTerm, fixByType) <- liftQuote Function.fixByAndType
pure (PLC.Def (PLC.VarDecl noProvenance name (noProvenance <$ fixByType)) (noProvenance <$ fixByTerm, Strict), mempty)
fixBy <- lookupOrDefineTerm p0 fixByKey mkFixByDef

let mkFixNDef = do
name <- liftQuote $ toProgramName fixNKey
let ((fixNTerm, fixNType), fixNDeps) =
((fixNTerm, fixNType), fixNDeps) <-
if arity == 1
then (Function.fixAndType, mempty)
then do
ft <- liftQuote Function.fixAndType
pure (ft, mempty)
-- fixN depends on fixBy
else (Function.fixNAndType arity (void fixBy), Set.singleton fixByKey)
else do
ft <- liftQuote $ Function.fixNAndType arity (void fixBy)
pure (ft, Set.singleton fixByKey)
pure (PLC.Def (PLC.VarDecl noProvenance name (noProvenance <$ fixNType)) (noProvenance <$ fixNTerm, Strict), fixNDeps)
fixN <- lookupOrDefineTerm p0 fixNKey mkFixNDef

Expand Down
2 changes: 1 addition & 1 deletion plutus-core/plutus-ir/test/datatypes/listMatchEval.golden
Original file line number Diff line number Diff line change
@@ -1 +1 @@
(delay (lam x_138 x_138))
(delay (lam x_85 x_85))
2 changes: 1 addition & 1 deletion plutus-core/plutus-ir/test/recursion/even3Eval.golden
Original file line number Diff line number Diff line change
@@ -1 +1 @@
(delay (lam case_True_365 (lam case_False_366 case_False_366)))
(delay (lam case_True_277 (lam case_False_278 case_False_278)))
2 changes: 1 addition & 1 deletion plutus-core/plutus-ir/test/types/listMatch.golden
Original file line number Diff line number Diff line change
@@ -1 +1 @@
(fun (con integer) (all a_48 (type) (fun a_48 a_48)))
(fun (con integer) (all a_49 (type) (fun a_49 a_49)))
Original file line number Diff line number Diff line change
@@ -1 +1 @@
[ Forest_11 (all a_42 (type) (fun a_42 a_42)) ]
[ Forest_11 (all a_44 (type) (fun a_44 a_44)) ]
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ test_Const =
text = toTypeAst @_ @DefaultUni @Text Proxy
runConst con = mkIterApp () (mkIterInst () con [text, bool]) [tC, tB]
lhs = typecheckReadKnownCek defaultCekParametersExt $ runConst $ builtin () (Right Const)
rhs = typecheckReadKnownCek defaultCekParametersExt $ runConst $ mapFun Left Plc.const
rhs = typecheckReadKnownCek defaultCekParametersExt $ runConst $ mapFun Left (runQuote Plc.const)
lhs === Right (Right c)
lhs === rhs

Expand Down
Loading

0 comments on commit c7a27c9

Please sign in to comment.