From d7e489dca4f184297b27e6e03fef69936abceb16 Mon Sep 17 00:00:00 2001
From: "Antoine \"Annwan\" COMBET" <annwan@annwan.me>
Date: Fri, 20 Jan 2023 11:23:29 +0100
Subject: [PATCH] some stuff

---
 .gitignore        |  5 ++++-
 src/LCalc/Term.hs | 44 ++++++++++++++++++++++++++++++++++++--------
 src/Main.hs       |  2 +-
 3 files changed, 41 insertions(+), 10 deletions(-)

diff --git a/.gitignore b/.gitignore
index 253efe1..f955806 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,5 @@
 /.stack-work
-/stack.yaml.lock
\ No newline at end of file
+/stack.yaml.lock
+*#
+*~
+.#*
\ No newline at end of file
diff --git a/src/LCalc/Term.hs b/src/LCalc/Term.hs
index 97e0cf3..d079581 100644
--- a/src/LCalc/Term.hs
+++ b/src/LCalc/Term.hs
@@ -1,14 +1,42 @@
 {-# LANGUAGE OverloadedStrings #-}
 
-module LCalc.Term where
+module LCalc.Term ( alphaReduce
+                  , betaReduce
+                  , apply
+                  , rename
+                  , Term(..)
+                  ) where
 
-data Term = Variable String
-          | Abstraction String Term
-          | Application Term Term
+data Term = Var String
+          | Lam String Term
+          | App Term Term
 
 instance Show Term where
-  show (Variable name) = name
-  show (Abstraction var term)  = "(λ" ++ var ++ "." ++ show term ++ ")"
-  show (Application t1 t2) = "(" ++ show t1 ++ " " ++ show t2 ++ ")"
+  show (Var name) = name
+  show (Lam var term)  = "(λ" ++ var ++ "." ++ show term ++ ")"
+  show (App t1 t2) = "(" ++ show t1 ++ " " ++ show t2 ++ ")"
 
-  
+rename :: String -> String -> Term -> Term
+rename old new (Lam name term) = Lam name $ rename old new term
+rename old new (App t1 t2) = App
+                             (rename old new t1)
+                             (rename old new t2)
+rename old new (Var name) = if old == name then Var new else Var name
+
+alphaReduce :: String -> Term -> Term
+alphaReduce newname (Lam name term) = Lam newname
+                                      $ rename name newname term
+alphaReduce _ t = t
+
+apply :: Term -> Term -> Term
+apply (Lam x e) a  = replace x e a
+apply x1
+
+replace :: String -> Term -> Term -> Term
+replace v l@(Lam x b) a = if x == v then l else Lam x (replace v b a)
+replace v (App x y) a = App (replace v x a) (replace v y a)
+replace v o@(Var n) a = if v == n then a else o
+
+betaReduce :: Term -> Term
+betaReduce (App t1 t2) = apply t1 t2
+betaReduce x = x
diff --git a/src/Main.hs b/src/Main.hs
index 7eb3e5a..3c99ad7 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -3,7 +3,7 @@ module Main (main) where
 import LCalc.Term
 
 t :: Term
-t = Abstraction "x" (Application (Variable "x") (Variable "x"))
+t = Lam "x" (App (Var "x") (Var "x"))
 
 main :: IO ()
 main = putStrLn $ show t