From 02c43751c4d37a489efc62a3d47ef5abaa6200e6 Mon Sep 17 00:00:00 2001
From: sebastian <sebastian.selander@gmail.com>
Date: Wed, 17 May 2023 18:53:05 +0200
Subject: [PATCH] STLC type checker in CHURF :)

---
 sample-programs/working/STLC.crf | 113 +++++++++++++++++++++++++++++++
 1 file changed, 113 insertions(+)
 create mode 100644 sample-programs/working/STLC.crf

diff --git a/sample-programs/working/STLC.crf b/sample-programs/working/STLC.crf
new file mode 100644
index 0000000..d5fcdac
--- /dev/null
+++ b/sample-programs/working/STLC.crf
@@ -0,0 +1,113 @@
+data Exp where
+    EVar : Char -> Exp
+    EAbs : Pair Char Type -> Exp -> Exp
+    EApp : Exp -> Exp -> Exp
+    EInt : Int -> Exp
+    EAdd : Exp -> Exp -> Exp
+
+data Type where
+    TLit : Char -> Type
+    TArr : Type -> Type -> Type
+
+data Maybe a where
+  Nothing : Maybe a 
+  Just : a -> Maybe a 
+
+data Ctx where
+    Ctx : List (Pair Char Type) -> Ctx
+
+data Tri a b c where
+  Tri : a -> b -> c -> Tri a b c
+
+lookupVar : Char -> Ctx -> Maybe Type
+lookupVar c ctx = case ctx of
+    Ctx ls => case ls of
+        Nil => Nothing
+        Cons a as => case a of
+            Pair name type => case (asciiCode name) == (asciiCode c) of
+                True => Just type
+                _ => lookupVar c (Ctx as)
+
+insertVar : Char -> Type -> Ctx -> Ctx
+insertVar c t ctx = case ctx of
+        Ctx ls => Ctx (Cons (Pair c t) ls)
+
+infer : Ctx -> Exp -> Maybe (Pair Type Ctx)
+infer ctx e = case ctx of
+    Ctx ls => case e of
+        EVar c => case lookupVar c ctx of
+            Nothing => Nothing
+            Just t => Just (Pair t ctx)
+        EAbs pair e => case pair of
+             Pair name targ => 
+                 let newCtx = insertVar name targ ctx
+                  in case infer newCtx e of
+                       Nothing => Nothing
+                       Just p => case p of
+                            Pair tret newCtx => Just (Pair (TArr targ tret) newCtx)
+        EApp e1 e2 => case infer ctx e1 of
+            Just p => case p of
+                Pair t ctx => case t of
+                    TArr t1 t2 => case infer ctx e2 of
+                        Just p => case p of
+                            Pair t ctx => case eq t1 t of
+                                True => Just (Pair t2 ctx)
+                                _ => Nothing
+                        Nothing => Nothing
+                    _ => Nothing
+            Nothing => Nothing
+        EInt i => Just (Pair (TLit 'i') ctx)
+        EAdd e1 e2 =>
+            case infer ctx e1 of
+                Just p => case p of
+                    Pair t ctx => case eq t (TLit 'i') of
+                        True => case infer ctx e2 of
+                            Just p => case p of
+                                Pair t ctx => case eq t (TLit 'i') of
+                                    True => Just (Pair (TLit 'i') ctx)
+                                    _ => Nothing
+                            _ => Nothing
+                        _ => Nothing
+                _ => Nothing
+
+eq : Type -> Type -> Bool
+eq t1 t2 = case t1 of
+    TArr left1 right1 => case t2 of
+        TArr left2 right2 => (eq left1 left2) && (eq right1 right2)
+        _ => False
+    TLit l1 => case t2 of
+        TLit l2 => (asciiCode l1) == (asciiCode l2)
+    _ => False
+
+
+
+.&& l r = case l of
+    True => r
+    _ => False
+
+.++ xs ys = case xs of
+    Nil => ys
+    Cons a as => Cons a (as ++ ys)
+
+emptyCtx = Ctx Nil
+
+expression = (EApp
+                (EAbs (Pair 'a' (TLit 'i'))
+                      (EAbs (Pair 'x' (TArr (TLit 'a') (TLit 'b')))
+                            (EVar 'x')))
+                (EInt 100))
+
+-- (\a : int . (\x : (a -> b) . x)) 100
+-- should infer the type (a -> b) -> (a -> b), which it does
+
+pretty : Type -> List Char
+pretty t = case t of
+    TLit t => Cons t Nil
+    TArr t1 t2 => Cons '(' ((pretty t1) ++ (" -> ") ++ (pretty t2) ++ (Cons ')' Nil))
+
+getType c e = case infer c e of
+        Nothing => printStr "fail"
+        Just p => case p of
+            Pair t _ => printStr (pretty t)
+
+main = getType emptyCtx expression