From 4c6386fd250e8447e76ec9dfb6e8f5a266a050e2 Mon Sep 17 00:00:00 2001
From: Marvin Borner
Date: Thu, 29 Feb 2024 11:35:25 +0100
Subject: Added higher order reducer

---
 src/Reducer/HigherOrder.hs | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 src/Reducer/HigherOrder.hs

(limited to 'src/Reducer/HigherOrder.hs')

diff --git a/src/Reducer/HigherOrder.hs b/src/Reducer/HigherOrder.hs
new file mode 100644
index 0000000..91378b7
--- /dev/null
+++ b/src/Reducer/HigherOrder.hs
@@ -0,0 +1,40 @@
+-- MIT License, Copyright (c) 2024 Marvin Borner
+-- Slightly modified version of Tromp's AIT/Lambda.lhs reducer implementation
+module Reducer.HigherOrder
+  ( reduce
+  ) where
+
+import           Helper
+
+data HigherOrder = HigherOrderBruijn Int | HigherOrderAbstraction (HigherOrder -> HigherOrder) | HigherOrderApplication HigherOrder HigherOrder
+data NamedTerm = NamedVariable Int | NamedAbstraction Int NamedTerm | NamedApplication NamedTerm NamedTerm
+
+app :: HigherOrder -> HigherOrder -> HigherOrder
+app (HigherOrderAbstraction f) = f
+app f                          = HigherOrderApplication f
+
+eval :: Expression -> HigherOrder
+eval = go []
+ where
+  go env (Bruijn      x    ) = env !! x
+  go env (Abstraction e    ) = HigherOrderAbstraction $ \x -> go (x : env) e
+  go env (Application e1 e2) = app (go env e1) (go env e2)
+  go _   _                   = invalidProgramState
+
+toNamedTerm :: HigherOrder -> NamedTerm
+toNamedTerm = go 0
+ where
+  go _ (HigherOrderBruijn i) = NamedVariable i
+  go d (HigherOrderAbstraction f) =
+    NamedAbstraction d $ go (d + 1) (f (HigherOrderBruijn d))
+  go d (HigherOrderApplication e1 e2) = NamedApplication (go d e1) (go d e2)
+
+resolveExpression :: NamedTerm -> Expression
+resolveExpression = resolve []
+ where
+  resolve vs (NamedVariable i     ) = Bruijn $ vs !! i
+  resolve vs (NamedAbstraction v t) = Abstraction $ resolve (v : vs) t
+  resolve vs (NamedApplication l r) = Application (resolve vs l) (resolve vs r)
+
+reduce :: Expression -> Expression
+reduce = resolveExpression . toNamedTerm . eval
-- 
cgit v1.2.3