Plutonomicon / plutarch-plutus

Typed eDSL for writing UPLC /ˈpluː.tɑːk/
MIT License
124 stars 63 forks source link

Preevaluate constant terms, even the ones under abstraction #667

Open SeungheonOh opened 3 months ago

SeungheonOh commented 3 months ago

evalTerms pre-evaluates a given terms, but anything that is behind a lambda abstraction will not get evaluated. So, for example,

> l = plam $ \_-> plength # (pconstant $ [1, 2,3:: Integer] :: Term s (PBuiltinList PInteger))

> (Right (Right es, _, _)) = evalTerm def l

> (Right esc) = compile def es

> esc
Script {unScript = Program {_progAnn = (), _progVer = Version () 1 0 0, _progTerm = LamAbs () (DeBruijn {dbnIndex = 0}) (Apply () (Apply () (Apply () (LamAbs () (DeBruijn {dbnIndex = 0}) (Apply () (LamAbs () (DeBruijn {dbnIndex = 0}) (Apply () (Var () (DeBruijn {dbnIndex = 2})) (LamAbs () (DeBruijn {dbnIndex = 0}) (Apply () (Apply () (Var () (DeBruijn {dbnIndex = 2})) (Var () (DeBruijn {dbnIndex = 2}))) (Var () (DeBruijn {dbnIndex = 1})))))) (LamAbs () (DeBruijn {dbnIndex = 0}) (Apply () (Var () (DeBruijn {dbnIndex = 2})) (LamAbs () (DeBruijn {dbnIndex = 0}) (Apply () (Apply () (Var () (DeBruijn {dbnIndex = 2})) (Var () (DeBruijn {dbnIndex = 2}))) (Var () (DeBruijn {dbnIndex = 1})))))))) (LamAbs () (DeBruijn {dbnIndex = 0}) (LamAbs () (DeBruijn {dbnIndex = 0}) (LamAbs () (DeBruijn {dbnIndex = 0}) (Force () (Apply () (Apply () (Apply () (Force () (Force () (Builtin () ChooseList))) (Var () (DeBruijn {dbnIndex = 1}))) (Delay () (Var () (DeBruijn {dbnIndex = 2})))) (Delay () (Apply () (Apply () (Var () (DeBruijn {dbnIndex = 3})) (Apply () (Apply () (Builtin () AddInteger) (Var () (DeBruijn {dbnIndex = 2}))) (Constant () (Some (ValueOf DefaultUniInteger 1))))) (Apply () (Force () (Builtin () TailList)) (Var () (DeBruijn {dbnIndex = 1}))))))))))) (Constant () (Some (ValueOf DefaultUniInteger 0)))) (Constant () (Some (ValueOf (DefaultUniApply DefaultUniProtoList DefaultUniInteger) [1,2,3]))))}}

Need either some function that can evaluate constant terms behind lambda abstractions or some mechanism to keep constant terms always evaluated structurally

SeungheonOh commented 3 months ago

Some idea:

Add plamEval that will evaluate body before constructing actual abstraction.

L-as commented 3 months ago

You want to make this issue on the Plutus repository.

SeungheonOh commented 3 months ago

Ideally, they make some option in CEK machine so that it can evaluate UPLC with some unbound variables