Skip to content

Instantly share code, notes, and snippets.

@brendanzab

brendanzab/arith.hs

Created Mar 15, 2014
Embed
What would you like to do?
evalBigStep :: Tm -> Maybe Tm
evalBigStep (TmIf t1 t2 t3) =
evalBigStep t1 >>= \b1 -> case b1 of
TmTrue -> evalBigStep t2 -- (B-IfTrue)
TmFalse -> evalBigStep t3 -- (B-IfFalse)
_ -> Nothing
evalBigStep (TmSucc t1) =
evalBigStep t1 >>= \t1' -> case t1' of
nv1 | isNumerical nv1 -> Just (TmSucc nv1) -- (B-Succ)
_ -> Nothing
evalBigStep (TmPred t1) =
evalBigStep t1 >>= \t1' -> case t1' of
TmZero -> Just TmZero -- (B-PredZero)
(TmSucc nv1) | isNumerical nv1 -> Just nv1 -- (B-PredSucc)
_ -> Nothing
evalBigStep (TmIsZero t1) =
evalBigStep t1 >>= \t1' -> case t1' of
TmZero -> Just TmTrue -- (B-IsZeroZero)
(TmSucc _) -> Just TmFalse -- (B-IsZeroZero)
_ -> Nothing
evalBigStep v = Just v
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment