mirror of
https://codeberg.org/ProgramSnail/pattern_matching.git
synced 2025-12-05 22:48:43 +00:00
125 lines
4.7 KiB
Haskell
125 lines
4.7 KiB
Haskell
import Data.Map.Strict as Map
|
|
|
|
type Symb = String
|
|
infixl 4 :@:
|
|
|
|
-- data Type = Boo
|
|
-- | Type :-> Type
|
|
-- | BoxT Symb Type -- is type required ??
|
|
-- deriving (Read,Show,Eq)
|
|
|
|
-- -- TODO: integrate into match
|
|
-- data SymbType = SymbIn -- simple 'argument'
|
|
-- | SymbOut -- exported from inside function to outer context by export
|
|
-- | SymbRef -- In + Out
|
|
|
|
-- data CtxType = PreviousCtx
|
|
-- | NewCtx
|
|
|
|
-- data Term = Fls
|
|
-- | Tru
|
|
-- | Var Symb
|
|
-- | Box SymbType Symb Type
|
|
-- | Export Symb Type
|
|
-- | Term :@: Term
|
|
-- | Match Term Term Term -- match _ : T then _ else _
|
|
-- -- Box s t (variable place) = Match SymbIn
|
|
-- deriving (Read,Show)
|
|
|
|
-- type Ctx = Map Symb Term
|
|
|
|
-- assign :: Term -> Term -> Maybe Ctx
|
|
|
|
-- assign Fls Fls = Just []
|
|
-- assign Tru Tru = Just []
|
|
-- assign (Idx i) (Idx j) | i == j = Just []
|
|
-- assign (Box x _) t = Just [t] -- TODO: remember name
|
|
-- assign (left :@: right) (left' :@: right') = do ctxLeft <- assign left left' -- TODO: ??
|
|
-- ctxRight <- assign right right'
|
|
-- Just $ ctxLeft ++ ctxRight
|
|
-- -- assign (Match pattern t doThen deElse) term = case assign pattern term of -- TODO: ??
|
|
-- -- Just ctx -> doThen
|
|
-- -- Nothing -> doElse
|
|
-- assign _ _ = Nothing
|
|
|
|
-- -- need to extend context in some way
|
|
-- -- context effect ??
|
|
|
|
-- -- TODO
|
|
-- subst :: Ctx -> Term -> Term
|
|
|
|
-- -- TODO
|
|
-- oneStep :: Term -> Maybe Term
|
|
-- oneStep _ = Nothing
|
|
|
|
-- -- TODO
|
|
-- whnf :: Term -> Term
|
|
-- whnf u = maybe u whnf (oneStep u)
|
|
|
|
-------------------------------------------------------------------------
|
|
|
|
-- %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
|
|
|
|
-- TODO: proper types for all nodes
|
|
data Type = Boo
|
|
| Type :-> Type
|
|
| BoxT Symb Type
|
|
|
|
type Ctx = Map Symb Term
|
|
|
|
data Term = Fls
|
|
| Tru
|
|
| OpenContext {ctx :: Term, term :: Term}
|
|
| GetFromContext {x :: Symb, ctx :: Term}
|
|
| Context Ctx
|
|
| Var Symb
|
|
| Box Symb Type
|
|
| Term :@: Term
|
|
| Match {pattern :: Term, doThen :: Term, doElse :: Term}
|
|
|
|
assign :: Term -> Term -> Maybe Ctx
|
|
assign Fls Fls = Just Map.empty
|
|
assign Tru Tru = Just Map.empty
|
|
-- assign (OpenContext ctx term) term = Just Map.empty -- TODO ?? no meaning, should have been evaluated
|
|
-- assign (GetFromContext x ctx) term = Just Map.empty -- TODO ?? no meaning, should have biie evaluated
|
|
-- assign (Context ctx) term = Just Map.empty -- TODO ?? can't assign term, no meaning ??
|
|
assign (Var x) (Var y) | x == y = Just Map.empty
|
|
assign (Box x t) term = Just $ Map.singleton x term
|
|
-- assign (left :@: right) (left' :@: right') = do ctxLeft <- assign left left' -- TODO: ?? probably should hav been evaluated first
|
|
-- ctxRight <- assign right right'
|
|
-- Just $ Map.union ctxLeft ctxRight
|
|
assign match@(Match {}) term = case whnf (match :@: term) of
|
|
Context ctx -> Just ctx
|
|
_ -> Nothing
|
|
assign _ _ = Nothing
|
|
|
|
-- TODO: check
|
|
-- TODO: choose eval trategy
|
|
-- TODO: separate unsuccessful assignment and camputation error during assignment ??
|
|
oneStep :: Term -> Maybe Term
|
|
oneStep Fls = Nothing
|
|
oneStep Tru = Nothing
|
|
oneStep (OpenContext {ctx, term}) = error "not implemented yet"
|
|
oneStep (GetFromContext {x, ctx}) | Just ctx' <- oneStep ctx = Just $ GetFromContext {x, ctx = ctx'}
|
|
| Context c <- ctx = Map.lookup x c
|
|
oneStep (Context {}) = Nothing
|
|
oneStep (Var {}) = Nothing
|
|
oneStep (Box {}) = Nothing
|
|
oneStep (left :@: right) | Just left' <- oneStep left = Just left'
|
|
| Just right' <- oneStep right = Just right'
|
|
oneStep (Match {pattern, doThen, doElse}) | Just pattern' <- oneStep pattern = Just pattern'
|
|
| Just doThen' <- oneStep doThen = Just doThen'
|
|
| Just doElse' <- oneStep doElse = Just doElse'
|
|
oneStep (Match {pattern, doThen, doElse} :@: term) | Just c <- assign pattern term = Just doThen
|
|
| otherwise = Just doElse
|
|
oneStep _ = Nothing
|
|
|
|
whnf :: Term -> Term
|
|
whnf u = maybe u whnf (oneStep u)
|