iteration

This commit is contained in:
ProgramSnail 2025-09-03 00:28:27 +03:00
parent c9fa374008
commit e8d698f1d1

24
main.hs
View file

@ -67,6 +67,8 @@ data Term = Fls -- const
-- complex pattern: -- 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 -- 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 :: Term -> Term -> Maybe TermTuple
assign Fls Fls = Just [] assign Fls Fls = Just []
assign Tru Tru = 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 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 :: Term -> Maybe Term
oneStep Fls = Nothing oneStep Fls = Nothing
oneStep Tru = 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 oneStep (left :@: right) | Just left' <- oneStep left = Just $ left' :@: right
| Just right' <- oneStep right = 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 -- TODO: check order
-- oneStep (Match {pat, doThen, doElse} :@: term) | Just tuple <- assign pat term = -- TODO: subst context oneStep (Match {pat, doThen, doElse} :@: term)
-- | otherwise = Just doElse | Just assigns <- assign pat term = Just $ foldr betaReduce doThen assigns
| otherwise = Just doElse
-- TODO -- TODO
oneStep _ = Nothing oneStep _ = Nothing
@ -153,17 +159,19 @@ infer :: TypeTuple -> Term -> Maybe Type
infer env Tru = Just Boo infer env Tru = Just Boo
infer env Fls = Just Boo infer env Fls = Just Boo
infer env (Box t) = Just $ BoxT t infer env (Box t) = Just $ BoxT t
infer env (Tuple terms) = TupleT <$> maybeMapToMaybe $ map (infer env) terms -- TODO infer env (Tuple terms) = TupleT <$> maybeMapToMaybe (map (infer env) terms)
infer (Var x) = env `elem` x -- TODO infer env (Var x) = Just $ env !! x -- (!?) ??
infer env (Match {pat, doThen, doElse}) = do patT <- infer env pat infer env (Match {pat, doThen, doElse}) = do patT <- infer env pat
-- TODO: infer doThenT with extended context -- TODO: infer doThenT with extended context
doElseT <- infer env doElse doElseT <- infer env doElse
-- TODO: guard: doThenT == doElseT -- TODO: guard: doThenT == doElseT
return patT :-> doElseT -- TODO ?? Just $ patT :-> doElseT -- TODO ??
infer (left :@: right) | Just (Tuple leftTs) <- infer env left, infer env (left :@: right)
| Just (TupleT leftTs) <- infer env left,
Just (TupleT rightTs) <- infer env right = Just $ TupleT $ leftTs ++ rightTs Just (TupleT rightTs) <- infer env right = Just $ TupleT $ leftTs ++ rightTs
| Just (leftTArg :-> leftTRes) <- infer env left, | Just (leftTArg :-> leftTRes) <- infer env left,
Just rightT <- infer env right = -- TODO: assign types, etc. 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 ?? -- TODO: auto make tuples from other types ??
-- TODO
infer _ _ = Nothing infer _ _ = Nothing