iteration

main.hs

@@ -0,0 +1,125 @@
+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)