From 9adc9f5cc334b016b4dd3338ed3b727514c76a6d Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Wed, 3 Sep 2025 12:54:31 +0300 Subject: [PATCH] fixes, cases impl --- main.hs | 70 +++++++++++++++++++++++++++++++-------------------------- 1 file changed, 38 insertions(+), 32 deletions(-) diff --git a/main.hs b/main.hs index 62e5232..26bf1aa 100644 --- a/main.hs +++ b/main.hs @@ -15,7 +15,7 @@ infixl 4 :@: -- Match ((+') (Box x Int) 3) 12 -------------------------------- --- + -- idea: every function returns context (list/map of named terms instead of expr) -- Branch - split current entity on two subcontexts -- Name - name current branch @@ -30,6 +30,20 @@ infixl 4 :@: -- context -> tuple +-------------------------------- + +-- \x:Boo -> if x then Fls else Sru +-- ~same to (?): +-- Match (Box:Boo) ((Match Tru Fls Tru) (Var 0)) Empty +-- +-- pattern matching (use contexts as tuples / lists): +-- Match (Union (Context Box:Boo) (Context Box:Boo)) ... <- pattern match pair +-- +-- 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 + +-------------------------------- + data Type = Boo | BoxT Type | Type :-> Type @@ -44,8 +58,7 @@ maybeMapToMaybe = foldl (\res x -> case x of Just x -> (:) x <$> res Nothing -> Nothing) (Just []) --- TODO: put something into empty branches / replace branching with another solution --- TODO: how to return names from context <- return indexed list +-- put something into empty branches / replace branching with another solution -> TODO: bottom type or lazy type eval (check for alwys matching patterns, isPatAlwaysMatch) data Term = Fls -- const | Tru -- const -- | Empty -- empty context -- replaced with Tuple [] @@ -57,18 +70,6 @@ data Term = Fls -- const | Term :@: Term -- apply term to term deriving (Read, Show) --- \x:Boo -> if x then Fls else Sru --- ~same to (?): --- Match (Box:Boo) ((Match Tru Fls Tru) (Var 0)) Empty --- --- pattern matching (use contexts as tuples / lists): --- Match (Union (Context Box:Boo) (Context Box:Boo)) ... <- pattern match pair --- --- 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 [] @@ -110,10 +111,10 @@ shift = shiftFrom 0 substDB :: Int -> Term -> Term -> Term substDB j s Fls = Fls substDB j s Tru = Tru -substDB j s (Box t) = Box t -- TODO: subst in type ?? <- probaby not +substDB j s (Box t) = Box t -- NOTE: no type vars => no subst in type substDB j s (Tuple ts) = Tuple $ map (substDB j s) ts substDB j s (Var n) = if n == j then s else Var n -substDB j s (Match {pat, doThen, doElse}) = let patSize = tupleSize pat in Match { -- TODO +substDB j s (Match {pat, doThen, doElse}) = let patSize = tupleSize pat in Match { pat = substDB j s pat, doThen = substDB (j + patSize) (shift patSize s) doThen, doElse = substDB j s doElse @@ -130,12 +131,12 @@ oneStep (Box {}) = Nothing oneStep (Tuple ts) = foldl (\res t -> case res of Just t' -> Just t' Nothing -> oneStep t - ) Nothing ts -- or foldr ? -- TODO: step in first possible. foldl ?? + ) Nothing ts -- TODO or foldr ? (step in first possible) oneStep (Var {}) = Nothing oneStep (Match {pat, doThen, doElse}) | Just pat' <- oneStep pat = Just $ Match {pat=pat', doThen, doElse} 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 ((Tuple left) :@: (Tuple right)) = Just $ Tuple $ left ++ right oneStep (Match {pat, doThen, doElse} :@: term) | Just assigns <- assign pat term = Just $ foldr betaReduce doThen assigns | otherwise = Just doElse @@ -147,13 +148,18 @@ whnf u = maybe u whnf (oneStep u) ------------------------------------------- --- returned 'Maybe' has another meaning: is typecheck possible -assignT :: Type -> Type -> Maybe TypeTuple -assignT Boo Boo = Just [] -assignT (BoxT t) u = Just [u] -assignT (t :-> u) w | t == w = Just [u] -- TODO: redifine Eq ?? -assignT (TupleT ts) (TupleT us) | length ts == length us = maybeMapToMaybe $ map (TupleT <$>) $ zipWith assignT ts us -assignT _ _ = Nothing +patternVarsT :: Type -> TypeTuple +patternVarsT Boo = [] +patternVarsT (BoxT t) = [t] +patternVarsT (t :-> u) = [u] +patternVarsT (TupleT ts) = map (TupleT . patternVarsT) ts + +isAssignableT :: Type -> Type -> Bool +isAssignableT Boo Boo = True +isAssignableT (BoxT t) u = t == u -- proper types eq ? +isAssignableT (t :-> u) w = isAssignableT t w +isAssignableT (TupleT ts) (TupleT us) | length ts == length us = and $ zipWith isAssignableT ts us +isAssignableT _ _ = False infer :: TypeTuple -> Term -> Maybe Type infer env Tru = Just Boo @@ -162,16 +168,16 @@ infer env (Box t) = Just $ BoxT t 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 + let patVars = patternVarsT patT + doThenT <- infer (patVars ++ env) doThen -- TODO: check var order doElseT <- infer env doElse - -- TODO: guard: doThenT == doElseT - Just $ patT :-> doElseT -- TODO ?? + guard $ doThenT == doElseT + Just $ patT :-> doElseT 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 ?? + isAssignableT leftTArg rightT = Just leftTRes + -- NOTE: auto tuples from other types could be added (kind of type conversion) infer _ _ = Nothing