pattern_matching/main.hs

import Data.Bifunctor as Bifunctor
import Data.Maybe as Maybe
import Control.Monad as Monad

type Symb = String
infixl 4 :@:

-- %x + 3 := 12
-- addp :: BoxT Int -> Int -> Int -> ???
-- addp :: Out Int -> In Int -> In Int
-- addp :: {x: Box Int} -> {_: Int} -> {_: Int} -> ??? {x: Int}
-- addp :: Box Int -> In Int -> In Int -> Ctx
-- addp :: Box x Int -> Int -> Int -> {x: Int}
-- addp (Box x Int) 3 <- type ??? {_: Int} -> {x: Int}
-- 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

-- context is a function ?
-- matching rules:
-- Ctx Ctx -> apply in elements
-- Fls Fls, Tru Tru -> matched, []
-- Name:Type Term:Type -> matched, [name:term]
-- Union, Context, Var - should have been reduced
-- Match Term -> apply match to term, propogate result

-- 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
          | TupleT [Type]
  deriving (Read, Show, Eq)

type TermTuple = [Term]
type TypeTuple = [Type]

maybeMapToMaybe :: [Maybe a] -> Maybe [a]  -- NOTE: probably can be replaced from stdlib
maybeMapToMaybe = foldl (\res x -> case x of
                                     Just x -> (:) x <$> res
                                     Nothing -> Nothing) (Just [])

-- 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 []
          | Box Type -- encode pattern entities
          -- | Merge Term Term -- union resulting contexts -- replaced with :@:
          | Tuple TermTuple -- resulting contet as elem of context
          | Var Int -- get variable from current context
          | Match {pat :: Term, doThen :: Term, doElse :: Term} -- match context with pattern and exec body, should be applied to term=ctx
          | Term :@: Term -- apply term to term
  deriving (Read, Show)

assign :: Term -> Term -> Maybe TermTuple
assign Fls Fls = Just []
assign Tru Tru = Just []
assign (Box {}) term = Just [term]
assign (Tuple left) (Tuple right) | length left == length right = maybeMapToMaybe $ map (Tuple <$>) $ zipWith assign left right
-- assign (Var x) term -- should be reduced (?)
assign match@Match {pat, doThen, doElse} term | Tuple tuple <- whnf (match :@: term) = Just tuple
-- assign (Term :@: Term) term -- should be reduced
assign _ _ = Nothing

--------------------------------------------

-- for patterns
tupleSize :: Term -> Int
tupleSize Fls = 0
tupleSize Tru = 0
tupleSize (Box {}) = 1
tupleSize (Tuple ts) = length ts
-- tupleSize (Var x) -- should be reduced (?)
tupleSize (Match {pat, doThen, doElse}) = tupleSize doThen -- == tupleSize doElse
-- tupleSize (t :@: u) -- should be reduced

shiftFrom :: Int -> Int -> Term -> Term
shiftFrom m k Fls = Fls
shiftFrom m k Tru = Tru
shiftFrom m k (Box t) = Box t -- TODO: shift type ?? <- probaby not
shiftFrom m k (Tuple ts) = Tuple $ map (shiftFrom m k) ts
shiftFrom m k (Var n) = if n < m then Var n else Var $ n + k
shiftFrom m k (Match {pat, doThen, doElse}) = Match {
  pat = shiftFrom m k pat,
  doThen = shiftFrom (m + tupleSize pat) k doThen,
  doElse = shiftFrom m k doElse
}
shiftFrom m k (left :@: right) = shiftFrom m k left :@: shiftFrom m k right

shift :: Int -> Term -> Term
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 -- 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 {
  pat = substDB j s pat,
  doThen = substDB (j + patSize) (shift patSize s) doThen,
  doElse = substDB j s doElse
}
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
oneStep (Box {}) = Nothing
oneStep (Tuple ts) = foldl (\res t -> case res of
                                        Just t' -> Just t'
                                        Nothing -> oneStep t
                    ) 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
oneStep (Match {pat, doThen, doElse} :@: term)
  | Just assigns <- assign pat term = Just $ foldr betaReduce doThen assigns
  | otherwise = Just doElse
-- TODO
oneStep _ = Nothing

whnf :: Term -> Term
whnf u = maybe u whnf (oneStep u)

-------------------------------------------

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
infer env Fls = Just Boo
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
                                             let patVars = patternVarsT patT
                                             doThenT <- infer (patVars ++ env) doThen -- TODO: check var order
                                             doElseT <- infer env doElse
                                             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,
    isAssignableT leftTArg rightT = Just leftTRes
    -- NOTE: auto tuples from other types could be added (kind of type conversion)
infer _ _ = Nothing