From a26d059aecabb05d9edce10e939b3b518e37cc82 Mon Sep 17 00:00:00 2001
From: tzlil <tzlils@protonmail.com>
Date: Sat, 8 Jul 2023 02:50:40 +0300
Subject: finish untyped

---
 Untyped.hs | 63 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 63 insertions(+)
 create mode 100644 Untyped.hs

(limited to 'Untyped.hs')

diff --git a/Untyped.hs b/Untyped.hs
new file mode 100644
index 0000000..5e48ba3
--- /dev/null
+++ b/Untyped.hs
@@ -0,0 +1,63 @@
+module Main where
+import Text.ParserCombinators.Parsec (many1, sepBy1, string, noneOf, char, digit, spaces, sepEndBy, Parser, (<|>), parse, letter, oneOf)
+--import Relude hiding ((<|>))
+import Prelude
+import Data.Foldable (foldl1) 
+import qualified Data.Set as Set
+import Control.Monad (forever, void)
+import System.IO (hFlush, stdout)
+
+data Term = Var String | App Term Term | Lam String Term deriving (Eq)
+instance Show Term where
+    show (Var x) = x
+    show (App x y) = show x ++ show y
+    show (Lam x y) = "(λ"++x++". "++show y++")"
+
+
+parens p = char '(' *> spaces *> p <* spaces <* char ')'
+var = Var <$> many1 letter
+lam = do
+  void $ char '\\'
+  spaces
+  vars <- many1 $ (many1 letter) <* spaces
+  void $ string "."
+  spaces
+  body <- term
+  return (foldr Lam body vars)
+app = foldl1 App <$> sepBy1 (var <|> parens term) spaces
+term = lam <|> app <|> var
+
+fv :: Term -> Set.Set String
+fv (Var x) = Set.singleton x
+fv (Lam x m) = x `Set.delete` (fv m)
+fv (App m1 m2) = (fv m1) `Set.union` (fv m2)
+
+pickFresh :: Set.Set String -> String -> String
+pickFresh s n | n `Set.notMember` s = n
+pickFresh s n = pickFresh s $ n <> "'"
+
+subst n x (Var e)
+    | x == e = n
+    | otherwise = Var e
+subst n x (App m1 m2) = App (subst n x m1) (subst n x m2)
+subst n x l@(Lam y m)
+    | x == y = l
+    | y `Set.notMember` (fv n) = Lam y (subst n x m)
+    | otherwise = Lam y' (subst n x (subst (Var y') y m))
+  where
+    y' = pickFresh ((fv n) `Set.union` (fv m)) y
+
+normalstep (App (Lam x m) n) = Just (subst n x m)
+normalstep (Lam x m) = normalstep m >>= return . Lam x
+normalstep (App m n) | normalstep m == Nothing = normalstep n >>= return . App m
+normalstep (App m n) = normalstep m >>= return . (`App` n)
+normalstep _ = Nothing
+
+repeatedly f x = maybe x (repeatedly f) (f x)
+eval = (repeatedly normalstep <$>) . parse term "<stdin>" 
+
+main = forever $ do 
+  putStr "Untyped> "
+  hFlush stdout
+  contents <- getLine 
+  putStrLn $ (either show show . eval) contents
-- 
cgit 1.4.1