Add optimization cases for triage and composition

This commit is contained in:
James Eversole
2025-01-25 15:12:28 -06:00
parent 2bd388c871
commit ea128929da
3 changed files with 24 additions and 12 deletions

View File

@ -59,8 +59,21 @@ evalAST env term
elimLambda :: TricuAST -> TricuAST
elimLambda = go
where
-- η-reduction
go (SLambda [v] (SApp f (SVar x)))
| v == x && not (isFree v f) = elimLambda f
-- Triage optimization
go (SLambda [a] (SLambda [b] (SLambda [c] body)))
| body == triageBody = _TRIAGE
where
triageBody =
(SApp (SApp TLeaf (SApp (SApp TLeaf (SVar a)) (SVar b))) (SVar c))
-- Compose optimization
go (SLambda [f] (SLambda [g] (SLambda [x] body)))
| body == composeBody = _COMPOSE
where
composeBody = SApp (SVar f) (SApp (SVar g) (SVar x))
-- General elimination
go (SLambda (v:vs) body)
| null vs = toSKI v (elimLambda body)
| otherwise = elimLambda (SLambda [v] (SLambda vs body))
@ -75,10 +88,13 @@ elimLambda = go
| otherwise = SApp (SApp _S (toSKI x n)) (toSKI x u)
toSKI x t
| not (isFree x t) = SApp _K t
| otherwise = errorWithoutStackTrace "Unhandled toSKI conversion"
_S = parseSingle "t (t (t t t)) t"
_K = parseSingle "t t"
_I = parseSingle "t (t (t t)) t"
_S = parseSingle "t (t (t t t)) t"
_K = parseSingle "t t"
_I = parseSingle "t (t (t t)) t"
_TRIAGE = parseSingle "t (t (t t (t (t (t t t))))) t"
_COMPOSE = parseSingle "t (t (t t (t (t (t t t)) t))) (t t)"
isFree x = Set.member x . freeVars
freeVars (SVar v ) = Set.singleton v