Skip to content

Commit

Permalink
WIP try to restore a unary special case
Browse files Browse the repository at this point in the history
  • Loading branch information
michaelpj committed Nov 28, 2022
1 parent 9e45815 commit a2572df
Showing 1 changed file with 42 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -559,6 +559,8 @@ we can match on context and the top frame in a single, strict pattern match.
data Context uni fun s
= FrameEvalApp !(CekValEnv uni fun) {-# UNPACK #-} !(Accumulator (Term NamedDeBruijn uni fun ()) (CekValue uni fun) s) !(Context uni fun s) -- ^ @[_ N]@
| FrameApplyArgs !(NEV.NonEmptyVector (CekValue uni fun)) !(Context uni fun s) -- ^ @[_ V ...]@
| FrameApplyFun !(CekValue uni fun) !(Context uni fun s) -- ^ @[V _]@
| FrameApplyArg !(CekValEnv uni fun) !(Term NamedDeBruijn uni fun ()) !(Context uni fun s) -- ^ @[_ V]@
| FrameForce !(Context uni fun s) -- ^ @(force _)@
| FrameConstr !(CekValEnv uni fun) {-# UNPACK #-} !Int {-# UNPACK #-} !(Accumulator (Term NamedDeBruijn uni fun ()) (CekValue uni fun) s) !(Context uni fun s)
| FrameCases !(CekValEnv uni fun) ![Term NamedDeBruijn uni fun ()] !(Context uni fun s)
Expand Down Expand Up @@ -670,6 +672,9 @@ enterComputeCek = computeCek (toWordArray 0) where
!unbudgetedSteps' <- stepAndMaybeSpend BForce unbudgetedSteps
computeCek unbudgetedSteps' (FrameForce ctx) env body
-- s ; ρ ▻ [L M] ↦ s , [_ (M,ρ)] ; ρ ▻ L
computeCek !unbudgetedSteps !ctx !env (Apply _ fun (arg :| [])) = do
!unbudgetedSteps' <- stepAndMaybeSpend BApply unbudgetedSteps
computeCek unbudgetedSteps' (FrameApplyArg env arg ctx) env fun
computeCek !unbudgetedSteps !ctx !env (Apply _ fun args) = do
!unbudgetedSteps' <- stepAndMaybeSpend BApply unbudgetedSteps
(t, acc) <- CekM $ newNEAccumulator (NE.cons fun args)
Expand Down Expand Up @@ -716,6 +721,7 @@ enterComputeCek = computeCek (toWordArray 0) where
pure $ dischargeCekValue val
-- s , {_ A} ◅ abs α M ↦ s ; ρ ▻ M [ α / A ]*
returnCek !unbudgetedSteps (FrameForce ctx) fun = forceEvaluate unbudgetedSteps ctx fun

-- s , [_ (M,ρ)] ◅ V ↦ s , [V _] ; ρ ▻ M
returnCek !unbudgetedSteps (FrameEvalApp env acc ctx) arg = do
r <- CekM $ stepAccumulator acc arg
Expand All @@ -729,9 +735,14 @@ enterComputeCek = computeCek (toWordArray 0) where
-- Or I guesss make an error for it, but it genuinely is impossible
_ -> error "impossible"
-- s , [(lam x (M,ρ)) _] ◅ V ↦ s ; ρ [ x ↦ V ] ▻ M
-- FIXME: add rule for VBuiltin once it's in the specification.
returnCek !unbudgetedSteps (FrameApplyArgs args ctx) fun =
applyEvaluate unbudgetedSteps ctx fun args

returnCek !unbudgetedSteps (FrameApplyArg argVarEnv arg ctx) fun =
computeCek unbudgetedSteps (FrameApplyFun fun ctx) argVarEnv arg
returnCek !unbudgetedSteps (FrameApplyFun fun ctx) arg =
applyEvaluate1 unbudgetedSteps ctx fun arg

returnCek !unbudgetedSteps (FrameConstr env i acc ctx) e = do
r <- CekM $ stepAccumulator acc e
case r of
Expand Down Expand Up @@ -824,6 +835,36 @@ enterComputeCek = computeCek (toWordArray 0) where
applyEvaluate !_ !_ val !_ =
throwingDischarged _MachineError NonFunctionalApplicationMachineError val

applyEvaluate1
:: WordArray
-> Context uni fun s
-> CekValue uni fun -- lhs of application
-> CekValue uni fun -- rhs of application
-> CekM uni fun s (Term NamedDeBruijn uni fun ())
applyEvaluate1 !unbudgetedSteps !ctx (VLam arity vars env body) !arg =
let
remainingArity = arity-1
extended = Env.cons arg env
-- TODO: slab env
in if remainingArity > 0
then returnCek unbudgetedSteps ctx (VLam remainingArity vars extended body)
else computeCek unbudgetedSteps ctx extended body
applyEvaluate1 !unbudgetedSteps !ctx (VBuiltin fun term runtime) !arg = do
let argTerms = pure $ dischargeCekValue arg
-- @term@ and @argTerm@ are fully discharged, and so @term'@ is, hence we can put it
-- in a 'VBuiltin'.
term' = Apply () term argTerms
case runtime of
-- It's only possible to apply a builtin application if the builtin expects a term
-- argument next.
BuiltinExpectArgument f -> do
res <- evalBuiltinApp fun term' $ f arg
returnCek unbudgetedSteps ctx res
_ ->
throwingWithCause _MachineError UnexpectedBuiltinTermArgumentMachineError (Just term')
applyEvaluate1 !_ !_ val !_ =
throwingDischarged _MachineError NonFunctionalApplicationMachineError val

-- | Spend the budget that has been accumulated for a number of machine steps.
spendAccumulatedBudget :: WordArray -> CekM uni fun s ()
spendAccumulatedBudget !unbudgetedSteps = iforWordArray unbudgetedSteps spend
Expand Down

0 comments on commit a2572df

Please sign in to comment.