From e8d698f1d1a874bdea5d1934d2888f5285d446bb Mon Sep 17 00:00:00 2001
From: ProgramSnail <purpurebacterium@yandex.ru>
Date: Wed, 3 Sep 2025 00:28:27 +0300
Subject: [PATCH] iteration

---
 main.hs | 30 +++++++++++++++++++-----------
 1 file changed, 19 insertions(+), 11 deletions(-)

diff --git a/main.hs b/main.hs
index fc06bd1..62e5232 100644
--- a/main.hs
+++ b/main.hs
@@ -67,6 +67,8 @@ data Term = Fls -- const
 -- complex pattern:
 -- Match (Union (Context Box:Boo) (Match (Tru) (Union (Context Tru) (Context Tru)) (Union (Context Fls) (Context Fls))) ... <- match pair, match second elem with Tru. Note that context size = 3 after 
 
+-- TODO: isPatAlwaysMatch function to throw away unrequired doElse branches
+
 assign :: Term -> Term -> Maybe TermTuple
 assign Fls Fls = Just []
 assign Tru Tru = Just []
@@ -118,6 +120,9 @@ substDB j s (Match {pat, doThen, doElse}) = let patSize = tupleSize pat in Match
 }
 substDB j s (left :@: right) =  substDB j s left :@: substDB j s right
 
+betaReduce :: Term -> Term -> Term
+betaReduce val term = shift (-1) $ substDB 0 (shift 1 val) term
+
 oneStep :: Term -> Maybe Term
 oneStep Fls = Nothing
 oneStep Tru = Nothing
@@ -131,8 +136,9 @@ oneStep (Match {pat, doThen, doElse}) | Just pat' <- oneStep pat = Just $ Match
 oneStep (left :@: right) | Just left' <- oneStep left = Just $ left' :@: right
                          | Just right' <- oneStep right = Just $ left :@: right'
 oneStep ((Tuple left) :@: (Tuple right)) = Just $ Tuple $ left ++ right -- TODO: check order
--- oneStep (Match {pat, doThen, doElse} :@: term) | Just tuple <- assign pat term = -- TODO: subst context
---                                                | otherwise = Just doElse 
+oneStep (Match {pat, doThen, doElse} :@: term)
+  | Just assigns <- assign pat term = Just $ foldr betaReduce doThen assigns
+  | otherwise = Just doElse
 -- TODO
 oneStep _ = Nothing
 
@@ -153,17 +159,19 @@ infer :: TypeTuple -> Term -> Maybe Type
 infer env Tru = Just Boo
 infer env Fls = Just Boo
 infer env (Box t) = Just $ BoxT t
-infer env (Tuple terms) = TupleT <$> maybeMapToMaybe $ map (infer env) terms -- TODO
-infer (Var x) = env `elem` x -- TODO
+infer env (Tuple terms) = TupleT <$> maybeMapToMaybe (map (infer env) terms)
+infer env (Var x) = Just $ env !! x -- (!?) ??
 infer env (Match {pat, doThen, doElse}) = do patT <- infer env pat
                                          -- TODO: infer doThenT with extended context
                                              doElseT <- infer env doElse
                                         -- TODO: guard: doThenT == doElseT
-                                             return patT :-> doElseT -- TODO ??
-infer (left :@: right) | Just (Tuple leftTs) <- infer env left,
-                         Just (TupleT rightTs) <- infer env right = Just $ TupleT $ leftTs ++ rightTs
-                       | Just (leftTArg :-> leftTRes) <- infer env left,
-                         Just rightT <- infer env right = -- TODO: assign types, etc.
-                       -- TODO: auto make tuples from other types ??
--- TODO
+                                             Just $ patT :-> doElseT -- TODO ??
+infer env (left :@: right)
+  | Just (TupleT leftTs) <- infer env left,
+    Just (TupleT rightTs) <- infer env right = Just $ TupleT $ leftTs ++ rightTs
+  | Just (leftTArg :-> leftTRes) <- infer env left,
+    Just rightT <- infer env right,
+    Just assigns <- assignT leftTArg rightT = Just $ leftTRes
+    -- TODO: check (assigns are not used?), assign types, etc.
+    -- TODO: auto make tuples from other types ??
 infer _ _ = Nothing