--- NOTE: IS NOT COMPLETED ---

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)