diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,46 @@
+Copyright (c) 2015 Takayuki Muranushi
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+
+
+
+The code of parser and pretty-printer for Formura is based on codes of
+`syntax`, `semi-iso` and their derived packages by Paweł Nowak under following license.
+
+Copyright (c) 2014 Paweł Nowak
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/exe-src/formura-eval.hs b/exe-src/formura-eval.hs
new file mode 100644
--- /dev/null
+++ b/exe-src/formura-eval.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE DataKinds #-}
+module Main where
+
+import           Control.Lens
+import           Data.Monoid
+import           System.Environment
+import           System.IO
+import qualified Text.PrettyPrint.ANSI.Leijen as Ppr
+import qualified Text.Trifecta as P
+
+import           Formura.Interpreter.Eval
+import qualified Formura.Parser as P
+import           Formura.Syntax
+
+main :: IO ()
+main = do
+  argv <- getArgs
+  mapM_ process argv
+
+process :: FilePath -> IO ()
+process fn = do
+  mprog <- P.parseFromFileEx (P.runP $ P.program <* P.eof) fn
+  case mprog of
+      P.Failure doc -> Ppr.displayIO stdout $ Ppr.renderPretty 0.8 80 $ doc <> Ppr.linebreak
+      P.Success prog -> do
+        let BindingF stmts = prog ^. programBinding
+        mapM_ evalStmt stmts
+
+evalStmt :: StatementF RExpr -> IO ()
+evalStmt (TypeDecl _ _) = return ()
+evalStmt (Subst l r) = do
+  putStrLn $ show l ++ " = " ++ show r
+  rv <- runIM $ eval r
+  case rv of
+    Left doc -> Ppr.displayIO stdout $ Ppr.renderPretty 0.8 80 $ doc <> Ppr.linebreak
+    Right vt -> print vt
+  putStrLn ""
diff --git a/exe-src/formura-gen.hs b/exe-src/formura-gen.hs
new file mode 100644
--- /dev/null
+++ b/exe-src/formura-gen.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE DataKinds #-}
+module Main where
+
+import           Control.Lens
+import           Control.Monad
+import qualified Data.IntMap as G
+import           Data.Monoid
+import qualified Data.Text as T
+import qualified Data.Text.IO as T
+import           System.Environment
+import           System.IO
+import qualified Text.PrettyPrint.ANSI.Leijen as Ppr
+import qualified Text.Trifecta as P
+
+import qualified Formura.Annotation as A
+import           Formura.Annotation.Representation
+import           Formura.OrthotopeMachine.Graph
+import           Formura.OrthotopeMachine.Translate
+import qualified Formura.Parser as P
+import           Formura.Compiler
+import           Formura.Syntax
+import qualified Formura.Cxx.Translate as C
+
+main :: IO ()
+main = do
+  argv <- getArgs
+  mapM_ process argv
+
+process :: FilePath -> IO ()
+process fn = do
+  mprog <- P.parseFromFileEx (P.runP $ P.program <* P.eof) fn
+  case mprog of
+      P.Failure doc -> Ppr.displayIO stdout $ Ppr.renderPretty 0.8 80 $ doc <> Ppr.linebreak
+      P.Success prog -> do
+        let BindingF stmts = prog ^. programBinding
+        mapM_ genStmt stmts
+
+genStmt :: StatementF RExpr -> IO ()
+genStmt (TypeDecl _ _) = return ()
+genStmt (Subst l r) = do
+  putStrLn $ show l ++ " = " ++ show r
+  (ret, s, _) <- runCompiler (genMainFunction r) defaultCodegenRead defaultCodegenState
+  case ret of
+    Left doc -> Ppr.displayIO stdout $ Ppr.renderPretty 0.8 80 $ doc <> Ppr.linebreak
+    Right () -> return ()
+  mapM_ pprNode $ G.toList (s ^. theGraph)
+  putStrLn ""
+
+  (ret, s, cxxCode) <- runCompiler C.translate () C.defaultTranState{C._theGraph = s ^. theGraph}
+  case ret of
+    Left doc -> Ppr.displayIO stdout $ Ppr.renderPretty 0.8 80 $ doc <> Ppr.linebreak
+    Right () -> return ()
+  T.putStrLn cxxCode    
+  T.writeFile "output.cpp" cxxCode
+
+pprNode :: (Int, Node) -> IO ()
+pprNode (i,n) = do
+  let r = case A.toMaybe (n ^. A.annotation) of
+        Just Manifest -> "M"
+        _             -> " "
+      varName = case A.toMaybe (n ^. A.annotation) of
+        Just (SourceName n) -> n
+        _                   -> ""
+  putStrLn $ unwords [r , take 4 $ varName ++ repeat ' ', show (i,n)]
diff --git a/exe-src/formura-parser.hs b/exe-src/formura-parser.hs
new file mode 100644
--- /dev/null
+++ b/exe-src/formura-parser.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE DataKinds #-}
+module Main where
+
+import           Data.Monoid
+import           System.Environment
+import           System.IO
+import qualified Text.PrettyPrint.ANSI.Leijen as Ppr
+import qualified Text.Trifecta as P
+
+import qualified Formura.Parser as P
+
+main :: IO ()
+main = do
+  argv <- getArgs
+  mapM_ process argv
+
+process :: FilePath -> IO ()
+process fn = do
+  mprog <- P.parseFromFileEx (P.runP $ P.program <* P.eof) fn
+  case mprog of
+      P.Success prog -> print $ prog
+      P.Failure doc -> Ppr.displayIO stdout $ Ppr.renderPretty 0.8 80 $ doc <> Ppr.linebreak
diff --git a/formura.cabal b/formura.cabal
new file mode 100644
--- /dev/null
+++ b/formura.cabal
@@ -0,0 +1,139 @@
+-- Initial formura.cabal generated by cabal init.  For further
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                formura
+version:             1.0
+synopsis:            Formura is a simple language to describe stencil computation.
+-- description:
+homepage:            http://nushio3.github.io
+license:             MIT
+license-file:        LICENSE
+author:              Takayuki Muranushi
+maintainer:          muranushi@gmail.com
+-- copyright:
+category:            Language
+build-type:          Simple
+-- extra-source-files:
+cabal-version:       >=1.10
+
+source-repository head
+  type: git
+  location: git://github.com/nushio3/formura.git
+
+
+library
+  exposed-modules:
+                  Formura.Language.Combinator
+                  Formura.Annotation
+                  Formura.Annotation.Representation
+                  Formura.Compiler
+                  Formura.Parser
+                  Formura.Syntax
+                  Formura.Type
+                  Formura.Vec
+                  Formura.Interpreter.Value
+                  Formura.Interpreter.Eval
+                  Formura.OrthotopeMachine.Graph
+                  Formura.OrthotopeMachine.Translate
+                  Formura.Cxx.Translate
+
+
+  -- other-modules:
+  -- other-extensions:
+  build-depends:
+                base == 4.*
+              , ansi-wl-pprint
+              , containers
+              , either
+              , lattices
+              , lens
+              , mmorph
+              , mtl
+              , parsers
+              , QuickCheck
+              , text
+              , trifecta
+              , vector
+
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  ghc-options:         -O2 -Wall  -fno-warn-unused-do-bind -threaded -rtsopts -with-rtsopts=-N
+
+
+
+executable formura-parser
+  hs-source-dirs: exe-src
+  main-is: formura-parser.hs
+  default-language:    Haskell2010
+  ghc-options:         -O2 -Wall -fno-warn-unused-do-bind -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+                base == 4.*
+              , ansi-wl-pprint
+              , formura
+              , trifecta
+
+executable formura-eval
+  hs-source-dirs: exe-src
+  main-is: formura-eval.hs
+  default-language:    Haskell2010
+  ghc-options:         -O2 -Wall -fno-warn-unused-do-bind -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+                base == 4.*
+              , ansi-wl-pprint
+              , lens
+              , formura
+              , trifecta
+
+executable formura-gen
+  hs-source-dirs: exe-src
+  main-is: formura-gen.hs
+  default-language:    Haskell2010
+  ghc-options:         -O2 -Wall -fno-warn-unused-do-bind -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+                base == 4.*
+              , ansi-wl-pprint
+              , containers
+              , lens
+              , formura
+              , text
+              , trifecta
+
+
+
+
+-- executable test-parser
+--   buildable: False
+--   hs-source-dirs: exe-src
+--   main-is: test-parser.hs
+--   Other-Modules: CommandLineOption
+--   ghc-options:         -O2 -Wall -fno-warn-unused-do-bind
+--   build-depends:
+--                 base == 4.*
+--               , ansi-wl-pprint
+--               , bytestring
+--               , containers
+--               , formura
+--               , lens
+--               , text
+--               , trifecta
+--               , vector
+--
+-- executable test-generator
+--   buildable: False
+--   hs-source-dirs: exe-src
+--   main-is: test-generator.hs
+--   ghc-options:         -O2 -Wall  -fno-warn-unused-do-bind
+--   build-depends:
+--                 base == 4.*
+--               , formura
+--               , hoopl
+--
+--
+-- executable formura-list-reserved-char
+--   hs-source-dirs: exe-src
+--   main-is: formura-list-reserved-char.hs
+--   ghc-options:         -O2 -Wall -fno-warn-unused-do-bind
+--   build-depends:
+--                 base == 4.*
+--               , formura
+--
diff --git a/src/Formura/Annotation.hs b/src/Formura/Annotation.hs
new file mode 100644
--- /dev/null
+++ b/src/Formura/Annotation.hs
@@ -0,0 +1,68 @@
+{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
+module Formura.Annotation where
+
+import Control.Lens
+import Control.Monad
+import Data.Maybe
+import Data.Dynamic
+import Prelude hiding (map)
+import qualified Prelude as P (map)
+
+-- | A dynamically-typed list of annotations.
+type Annotation = [Dynamic]
+
+class Annotated a where
+  annotation :: Lens' a Annotation
+instance Annotated Annotation where
+  annotation = simple
+
+-- | An empty collection.
+empty :: Annotation
+empty = []
+
+-- | An annotation from a single value
+singleton :: Typeable a => a -> Annotation
+singleton x = [toDyn x]
+
+-- | Add an annotation to a collection.
+insert :: (Typeable a) => a -> Annotation -> Annotation
+insert x ys = toDyn x : ys
+
+-- | Remove all elements of type @a@ from the collection, and
+--   set @x@ as the only member of the type in the collection.
+set :: (Typeable a) => a -> Annotation -> Annotation
+set x ys = toDyn x : filter ((/= typeOf x) . dynTypeRep) ys
+
+-- | set @x@ as the only member of the type in the collection,
+-- only if no annotation of the same type pre-exists.
+weakSet :: (Typeable a) => a -> Annotation -> Annotation
+weakSet x ys
+  | any ((== typeOf x) . dynTypeRep) ys = ys
+  | otherwise                           = toDyn x : ys
+
+-- | Extract all annotations of type @a@ from
+-- the collection.
+toList :: (Typeable a) => Annotation -> [a]
+toList =  catMaybes . P.map fromDynamic
+
+-- | Extract the first annotation of the given type,
+-- if it exists.
+toMaybe :: (Typeable a) => Annotation -> Maybe a
+toMaybe = msum . P.map fromDynamic
+
+-- | Extract the first annotation of the given type,
+-- if it exists.
+viewMaybe :: (Typeable a, Annotated b) => b -> Maybe a
+viewMaybe = toMaybe . (^. annotation)
+
+
+-- | Map all annotations of type @a@ to type @b@,
+-- while leaving the others untouched.
+map :: (Typeable a, Typeable b) => (a->b) -> Annotation -> Annotation
+map f = P.map (maybeApply f)
+
+maybeApply :: (Typeable a, Typeable b) => (a->b) -> Dynamic -> Dynamic
+maybeApply f x =
+    case dynApply (toDyn f) x of
+      Just y  -> y
+      Nothing -> x
diff --git a/src/Formura/Annotation/Representation.hs b/src/Formura/Annotation/Representation.hs
new file mode 100644
--- /dev/null
+++ b/src/Formura/Annotation/Representation.hs
@@ -0,0 +1,9 @@
+module Formura.Annotation.Representation where
+
+import Formura.Syntax
+
+data Representation = Manifest | Delay
+                    deriving (Eq, Ord, Show, Read)
+
+data SourceName = SourceName IdentName
+                    deriving (Eq, Ord, Show, Read)
diff --git a/src/Formura/Compiler.hs b/src/Formura/Compiler.hs
new file mode 100644
--- /dev/null
+++ b/src/Formura/Compiler.hs
@@ -0,0 +1,99 @@
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, StandaloneDeriving, TemplateHaskell #-}
+
+module Formura.Compiler where
+
+import           Control.Applicative
+import           Control.Lens
+import           Control.Monad.Trans.Either
+import           Control.Monad.Morph
+import           Control.Monad.RWS
+import qualified Data.Set as S
+import qualified Text.Trifecta as P
+import qualified Text.PrettyPrint.ANSI.Leijen as Ppr
+
+import Formura.Language.Combinator
+
+type CompilerError = Ppr.Doc
+
+-- | The state of the compiler.
+data CompilerSyntacticState =
+  CompilerSyntacticState
+  { _compilerFocus :: Maybe Metadata
+  , _compilerStage :: String }
+
+makeClassy ''CompilerSyntacticState
+
+defaultCompilerSyntacticState :: CompilerSyntacticState
+defaultCompilerSyntacticState = CompilerSyntacticState Nothing ""
+
+-- | The formura compiler monad.
+newtype CompilerMonad r w s a = CompilerMonad
+  { runCompilerMonad :: EitherT CompilerError (RWST r w s IO) a}
+              deriving (Functor, Applicative, Monad, MonadIO,
+                        MonadReader r, MonadState s, MonadWriter w)
+
+compileErrMsg :: (HasCompilerSyntacticState s, MonadState s m) => P.Err -> m Ppr.Doc
+compileErrMsg errMsg = do
+    stg <- use compilerStage
+    foc <- use compilerFocus
+    let errMsg2
+          | stg == "" = errMsg
+          | otherwise = errMsg & P.footnotes %~ (++ [Ppr.text ("when " ++ stg)])
+    case foc of
+      Nothing -> return $ P.explain P.emptyRendering $ errMsg2
+      Just (Metadata r b e) -> return $
+        P.explain (P.addSpan b e $ r) $ errMsg2
+
+
+-- | Throw an error, possibly with user-friendly diagnostics of the current compiler state.
+instance (HasCompilerSyntacticState s, Monoid w) => P.Errable (CompilerMonad r w s) where
+  raiseErr errMsg = do
+    msg2 <- compileErrMsg errMsg
+    CompilerMonad $ left $ msg2
+
+-- | Run the compiler and get the result.
+evalCompiler :: CompilerMonad r w s a -> r -> s -> IO (Either CompilerError a)
+evalCompiler m r s = fmap fst $ evalRWST (runEitherT $ runCompilerMonad m) r s
+
+-- | Run the compiler and get the state and written results.
+--   Note that you get some partial results even when the compilation aborts.
+runCompiler :: CompilerMonad r w s a -> r -> s -> IO (Either CompilerError a,s,w)
+runCompiler m r s = runRWST (runEitherT $ runCompilerMonad m) r s
+
+-- | Run compiler, changing the reader and the state.
+withCompiler :: Monoid w => (r' -> s -> (r,s)) -> CompilerMonad r w s a -> CompilerMonad r' w s a
+withCompiler f = CompilerMonad . (hoist $ withRWST f) . runCompilerMonad
+
+-- | Raise doc as an error
+raiseDoc :: P.Errable m => Ppr.Doc ->  m a
+raiseDoc doc = P.raiseErr $ P.Err (Just doc) [] S.empty
+
+-- | The monadic algebra, specialized to the compiler monad.
+type CompilerAlgebra r w s f a = f a -> CompilerMonad r w s a
+
+-- | The compiler-monad-specific fold, that takes track of the syntax tree traversed.
+compilerMFold :: (Monoid w, Traversable f, HasCompilerSyntacticState s) =>
+           CompilerAlgebra r w s f (Lang g) -> Fix f -> CompilerMonad r w s (Lang g)
+compilerMFold k (In meta x) = do
+  r1 <- traverse (compilerMFold k) x
+  compilerFocus %= (meta <|>)
+  r2 <- k r1
+  return $ propagateMetadata meta r2
+
+-- | The compiler-monad-specific fold, that takes track of the syntax tree traversed and produces non-language results.
+compilerMFoldout :: (Monoid w, Traversable f, HasCompilerSyntacticState s) =>
+           CompilerAlgebra r w s f g -> Fix f -> CompilerMonad r w s g
+compilerMFoldout k (In meta x) = do
+  r1 <- traverse (compilerMFoldout k) x
+  compilerFocus %= (meta <|>)
+  r2 <- k r1
+  return $ r2
+
+-- | The compiler-monad-specific pure foldout, that takes track of the syntax tree traversed.
+compilerFoldout :: (Monoid w, Traversable f, HasCompilerSyntacticState s) =>
+           Algebra f (CompilerMonad r w s a) -> Fix f -> CompilerMonad r w s a
+compilerFoldout k (In meta x) = do
+  -- TODO: in order for this compilerFocus to work properly, the compiler state
+  -- needs to be a reader monad rather than state monad.
+  compilerFocus %= (meta <|>)
+  k $ fmap (compilerFoldout k) x
diff --git a/src/Formura/Cxx/Translate.hs b/src/Formura/Cxx/Translate.hs
new file mode 100644
--- /dev/null
+++ b/src/Formura/Cxx/Translate.hs
@@ -0,0 +1,171 @@
+{-# LANGUAGE OverloadedStrings, TemplateHaskell #-}
+
+module Formura.Cxx.Translate where
+
+import           Control.Applicative
+import           Control.Lens
+import           Control.Monad
+import           Control.Monad.RWS
+import           Data.Foldable (toList)
+import qualified Data.IntMap as G
+import           Data.Monoid
+import qualified Data.Text as T
+import           Text.Trifecta (failed, raiseErr)
+
+
+import qualified Formura.Annotation as A
+import           Formura.Annotation.Representation
+import           Formura.Compiler
+import           Formura.Syntax
+import           Formura.OrthotopeMachine.Graph
+import           Formura.Vec
+
+showt :: Show a => a -> T.Text
+showt = T.pack . show
+
+parens :: T.Text -> T.Text
+parens x = "(" <> x <> ")"
+
+brackets :: T.Text -> T.Text
+brackets x = "[" <> x <> "]"
+
+newtype VariableName = VariableName T.Text
+
+data TranState = TranState
+  { _tranSyntacticState :: CompilerSyntacticState
+  , _extent :: Vec Int
+  , _indexVariables :: Vec T.Text
+  , _theGraph :: Graph
+  }
+makeClassy ''TranState
+
+instance HasCompilerSyntacticState TranState where
+  compilerSyntacticState = tranSyntacticState
+
+defaultTranState :: TranState
+defaultTranState = TranState
+  { _tranSyntacticState = defaultCompilerSyntacticState{ _compilerStage = "C++ code generation"}
+  , _extent = Vec [128]
+  , _indexVariables = Vec ["i"]
+  , _theGraph = G.empty
+  }
+
+
+type TranM = CompilerMonad () T.Text TranState
+
+lookupNode :: NodeID -> TranM Node
+lookupNode i = do
+  g <- use theGraph
+  case G.lookup i g of
+   Nothing -> raiseErr $ failed $ "out-of-bound node reference: #" ++ show i
+   Just n -> do
+     case A.viewMaybe n of
+        Just meta -> compilerFocus %= (meta <|>)
+        Nothing -> return ()
+     return n
+
+
+-- cursorToCode :: Vec Int -> TranM T.Text
+-- cursorToCode cursor = do
+--   ivs <- use indexVariables
+--   return $ brackets (T.intercalate "," $ toList $
+--                      (\i c -> i <> "+" <> showt c) <$> ivs <*> cursor)
+
+cursorToCode :: T.Text -> Vec Int -> TranM T.Text
+cursorToCode vn (PureVec 0) = return $ vn <> "[i]"
+cursorToCode vn (Vec [0]) = return $ vn <> "[i]"
+cursorToCode vn (Vec [1]) = return $ parens $
+  "i == NX_AVX-1 ? _mm256_permutevar8x32_ps(" <> vn <> "[0],permute_fwd)" <>":" <> vn <> "[i+1]"
+cursorToCode vn (Vec [-1]) = return $ parens $
+  "i == 0 ? _mm256_permutevar8x32_ps(" <> vn <> "[NX_AVX-1],permute_bwd)" <>":" <> vn <> "[i-1]"
+cursorToCode _ c = raiseErr $ failed $ "unsupported cursor position: " ++ show c
+
+rhsCodeAt :: Vec Int -> NodeID -> TranM T.Text
+rhsCodeAt cursor nid = do
+  nd <- lookupNode nid
+  case A.viewMaybe nd of
+     Just Manifest -> do
+       Just (VariableName vn) <- return $ A.viewMaybe nd
+       cursorToCode vn cursor
+     _  -> rhsDelayedCodeAt cursor nd
+
+rhsDelayedCodeAt :: Vec Int -> Node -> TranM T.Text
+rhsDelayedCodeAt cursor (Node inst0 typ0 ann0) = do
+  case inst0 of
+     Imm r -> return $ showt (realToFrac r :: Double)
+     Uniop op a -> do
+       a_code <- rhsCodeAt cursor a
+       return $ parens $ T.pack op <> a_code
+     Binop op a b -> do
+       a_code <- rhsCodeAt cursor a
+       b_code <- rhsCodeAt cursor b
+       return $ parens $ a_code <> T.pack op <> b_code
+     Shift vi a -> rhsCodeAt (cursor + vi) a
+     LoadExtent i -> do
+       ext <- use extent
+       return $ showt (ext ^?! ix i :: Int)
+     x -> raiseErr $ failed $ "cxx codegen unimplemented for keyword: " ++ show x
+
+manifestNodes :: Graph -> [NodeID]
+manifestNodes g =
+  map fst $
+  filter f $
+  G.toList g
+  where
+    f :: (NodeID, Node) -> Bool
+    f (_, nd) = case A.viewMaybe nd of
+      Just Manifest -> True
+      _             -> False
+
+nameManifestVariables :: TranM ()
+nameManifestVariables = do
+  theGraph %= G.mapWithKey nameIt
+  where
+    nameIt :: NodeID -> Node -> Node
+    nameIt i n =
+      let newName = case A.viewMaybe n of
+                      Just (SourceName n) -> T.pack n
+                      _    -> "a_" <> showt i
+      in n & A.annotation %~ A.set (VariableName newName)
+
+translate :: TranM ()
+translate = censor makeCxxBody $ do
+  nameManifestVariables
+  g <- use theGraph
+  let ms = manifestNodes g
+  forM_ ms $ \ mnid -> do
+    n <- lookupNode mnid
+    case n ^. nodeInst of
+      Load _ -> return ()
+      _ -> do
+        Just (VariableName newName) <- return $ A.viewMaybe n
+        rhsCode <- rhsDelayedCodeAt 0 n
+        lhsCursor <- cursorToCode newName $ Vec [0]
+        tell $ lhsCursor <> " = " <> rhsCode <> ";\n"
+
+cxxHeader :: T.Text
+cxxHeader = T.unlines
+ [ "#include <iostream>"
+ , "#include <immintrin.h>"
+ , "#include <x86intrin.h>"
+ , ""
+ , "using namespace std;"
+ , ""
+ , "const __m256i permute_fwd =  _mm256_set_epi32(0,7,6,5,4,3,2,1);"
+ , "const __m256i permute_bwd =  _mm256_set_epi32(6,5,4,3,2,1,0,7);"
+ , ""
+ , "void inspect(__m256 a) {"
+ , "  float dest[8];"
+ , "  _mm256_storeu_ps(&dest[0], a);"
+ , "  for (int i = 0; i < 8; ++i)"
+ , "    cout << dest[i] << \"\\t\";"
+ , "  cout << endl;"
+ , "}"]
+
+makeCxxBody :: T.Text -> T.Text
+makeCxxBody core = T.unlines
+  [ "for (int i = 0; i < NX_AVX; ++i) {" 
+  , core
+  , "}"
+  , "SWAP;"
+  ]
diff --git a/src/Formura/Interpreter/Eval.hs b/src/Formura/Interpreter/Eval.hs
new file mode 100644
--- /dev/null
+++ b/src/Formura/Interpreter/Eval.hs
@@ -0,0 +1,119 @@
+{-# LANGUAGE FlexibleContexts, FlexibleInstances,  RankNTypes, TemplateHaskell #-}
+module Formura.Interpreter.Eval where
+
+import           Control.Applicative
+import           Control.Lens
+import           Control.Monad.RWS hiding (fix)
+import qualified Data.Map as M
+import qualified Data.Vector as V
+import           Text.Trifecta (failed, raiseErr)
+
+import           Formura.Interpreter.Value
+import           Formura.Compiler
+import           Formura.Language.Combinator
+import           Formura.Syntax
+
+
+type Binding = M.Map IdentName TypedValue
+
+data Environment =
+  Environment
+  { _envDimension :: Int
+  , _envExtent :: [Int]
+  , _envCS :: CompilerSyntacticState
+  }
+
+makeLenses ''Environment
+
+defaultEnvironment :: Environment
+defaultEnvironment = Environment 0 [] defaultCompilerSyntacticState{ _compilerStage = "interpretation" }
+
+instance HasCompilerSyntacticState Environment where
+  compilerSyntacticState = envCS
+
+type IM = CompilerMonad Binding () Environment
+type IAlgebra f a = f a -> IM a
+
+runIM :: IM a -> IO (Either CompilerError a)
+runIM m = evalCompiler m M.empty defaultEnvironment
+
+-- | Monadic 'fold' for twin language.
+mfold2 :: Traversable f => AlgebraM IM f (Lang g, Lang h) -> Fix f -> IM (Lang g, Lang h)
+mfold2 k (In meta x) = do
+  r1 <- traverse (mfold2 k) x
+  compilerFocus %= (meta <|>)
+  (g2, h2) <- k r1
+  return $ (propagateMetadata meta g2, propagateMetadata meta h2)
+
+
+class Evalable a where
+  eval :: a -> IM TypedValue
+
+instance Evalable (ImmF x) where
+  eval (ImmF r) = return $ (ElemValue $ fromRational r, ElemType "double")
+
+instance Evalable (IdentF x) where
+  eval (IdentF nam) = do
+    binding <- ask
+    case M.lookup nam (binding :: Binding) of
+      Just x  -> return x
+      Nothing -> raiseErr $ failed $ "undefined variable: " ++ nam
+
+instance Evalable (OperatorF TypedValue) where
+  eval (UniopF "+" x) = return x
+  eval (UniopF "-" x) = evalUniop negate x
+  eval (BinopF "+" x y) = evalBinop (+) x y
+  eval (BinopF "-" x y) = evalBinop (-) x y
+  eval (BinopF "*" x y) = evalBinop (*) x y
+  eval (BinopF "/" x y) = evalBinop (/) x y
+  eval (BinopF str _ _) = raiseErr $ failed $ "unimplemented binary operator: (" ++ str ++ ")"
+  eval _ = raiseErr $ failed "unimplemented operator in eval"
+
+evalUniop :: (forall a. Num a => a -> a) -> TypedValue -> IM TypedValue
+evalUniop f (ElemValue r, t) = return $ (ElemValue (f r), t)
+
+evalBinop :: (forall a. Fractional a => a -> a -> a) -> TypedValue -> TypedValue -> IM TypedValue
+evalBinop f (ElemValue x, tx ) (ElemValue y, ty) = return $ (ElemValue (f x y), tx)
+
+instance Evalable (TupleF TypedValue) where
+  eval (Tuple xts) = return $ (Tuple $ map fst xts, Tuple $ map snd xts)
+
+instance Evalable (GridF x) where
+  eval _ = raiseErr $ failed "eval of grid unimplemented."
+
+instance Evalable (ApplyF x) where
+  eval _ = raiseErr $ failed "eval of apply unimplemented."
+
+instance Evalable (LambdaF x) where
+  eval _ = raiseErr $ failed "eval of lambda unimplemented."
+
+instance Evalable (LetF x) where
+  eval _ = raiseErr $ failed "eval of let unimplemented."
+
+voidEval :: a -> IM TypedValue
+voidEval _ = raiseErr $ failed "eval of void unimplemented."
+
+instance Evalable RExpr where
+  eval = mfold2 (eval +:: eval +:: eval +:: eval +:: eval +:: eval +:: eval +:: eval +:: voidEval
+                  :: RExprF TypedValue -> IM TypedValue)
+
+
+ret :: Iso' [Int] Int
+ret = iso enc dec
+  where
+    enc = product
+    dec = const []
+
+makeGridValueF :: [Rational] -> ([Rational] -> IM x) -> IM (GridValueF x)
+makeGridValueF offset fun = do
+  exts <- use envExtent
+  let idxs = map (zipWith (+) offset . map toRational) $ spanExts exts
+      spanExts []  = [[]]
+      spanExts (n:ns) = [i:js| i <- [0..n-1], js <- spanExts ns]
+  content <- mapM fun idxs
+  return $ GridValueF offset $ V.fromList content
+
+accessGridF :: GridValueF x -> [Rational] -> IM x
+accessGridF g addr = do
+  let iaddr = zipWith (-) addr (g ^.gridOffset)
+  return undefined
diff --git a/src/Formura/Interpreter/Value.hs b/src/Formura/Interpreter/Value.hs
new file mode 100644
--- /dev/null
+++ b/src/Formura/Interpreter/Value.hs
@@ -0,0 +1,53 @@
+{-|
+Module      : Formura.Interpreter.Value
+Description : Haskell interpreter's value semantics
+Copyright   : (c) Takayuki Muranushi, 2015
+License     : MIT
+Maintainer  : muranushi@gmail.com
+Stability   : experimental
+
+Grid object with rational offset, to interpret Formura semantics in Haskell.
+-}
+
+
+{-# LANGUAGE DataKinds, DeriveFunctor, DeriveFoldable,
+DeriveTraversable, PatternSynonyms, TemplateHaskell, ViewPatterns #-}
+
+module Formura.Interpreter.Value where
+
+import           Control.Lens
+import qualified Data.Vector as V
+
+import           Formura.Language.Combinator
+import           Formura.Syntax
+
+newtype ElemValueF x = ElemValueF Double
+                 deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
+
+pattern ElemValue x <- ((^? match) -> Just (ElemValueF x)) where ElemValue x = match # ElemValueF x
+
+
+data FunValueF x = FunValueF LExpr RExpr
+                 deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
+pattern FunValue l r <- ((^? match) -> Just (FunValueF l r)) where FunValue l r = match # FunValueF l r
+
+
+
+data VectorValueF x =
+  VectorValueF
+  { _vectorContent :: V.Vector x
+  }
+                 deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
+
+data GridValueF x =
+  GridValueF
+  { _gridOffset  :: [Rational]
+  , _gridContent :: V.Vector x
+  }
+                 deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
+
+makeLenses ''GridValueF
+
+type ValueExpr = Lang '[ GridValueF, TupleF, VectorValueF,  FunValueF, ElemValueF ]
+
+type TypedValue = (ValueExpr, TypeExpr)
diff --git a/src/Formura/Language/Combinator.hs b/src/Formura/Language/Combinator.hs
new file mode 100644
--- /dev/null
+++ b/src/Formura/Language/Combinator.hs
@@ -0,0 +1,307 @@
+{- |
+Copyright   : (c) Takayuki Muranushi, 2015
+License     : MIT
+Maintainer  : muranushi@gmail.com
+Stability   : experimental
+
+Combinators for creating a customized language based on Modular Reifiable Matching.
+-}
+
+{-# LANGUAGE ConstraintKinds, DataKinds, DeriveFoldable, DeriveFunctor,
+DeriveTraversable, FlexibleContexts, FlexibleInstances,
+FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses,
+PatternSynonyms, RankNTypes, ScopedTypeVariables, StandaloneDeriving,
+TemplateHaskell, TupleSections, TypeFamilies, TypeOperators,
+UndecidableInstances, ViewPatterns #-}
+
+module Formura.Language.Combinator where
+
+import           Control.Lens
+import           Control.Monad
+import           Data.Traversable
+import qualified Test.QuickCheck     as Q
+import qualified Text.Trifecta       as P hiding (string)
+import qualified Text.Trifecta.Delta as P
+
+-- * Sum of functors
+
+-- | The datatype for the sum of functors.
+data Sum (fs :: [* -> *]) x where
+  Void :: Sum '[] x
+  Here :: Traversable f => f x -> Sum (f ': fs) x
+  There :: Sum fs x -> Sum (f ': fs) x
+
+instance Eq (Sum '[] x) where
+  _ == _ = True
+instance (Eq (f x), Eq (Sum fs x)) => Eq (Sum (f ': fs) x) where
+   (Here a)   == (Here b)  = a == b
+   (Here _ )  == (There _) = False
+   (There _ ) == (Here _)  = False
+   (There a)  == (There b) = a == b
+
+instance Ord (Sum '[] x) where
+  compare Void Void = EQ
+instance (Ord (f x), Ord (Sum fs x)) => Ord (Sum (f ': fs) x) where
+  compare (Here a) (Here b) = compare a b
+  compare (Here _ ) (There _) = LT
+  compare (There _ ) (Here _) = GT
+  compare (There a) (There b) = compare a b
+
+
+instance Show x => Show (Sum '[] x) where
+  show Void = "∅"
+
+instance (Show (f x), Show (Sum fs x)) => Show (Sum (f ': fs) x) where
+  showsPrec n (Here x) = showsPrec n x
+  showsPrec n (There x) = showsPrec n x
+
+instance Functor (Sum fs) where
+  fmap _ Void      = Void
+  fmap f (Here t)  = Here $ fmap f t
+  fmap f (There t) = There $ fmap f t
+
+instance Foldable (Sum fs) where
+  foldMap = foldMapDefault
+
+instance Traversable (Sum fs) where
+  traverse _   Void      = pure Void
+  traverse afb (Here x)  = Here  <$> traverse afb x
+  traverse afb (There x) = There <$> traverse afb x
+
+instance Elem f fs => Matches f (Sum fs x) where
+  type Content f (Sum fs x) = x
+  match = constructor
+
+instance Q.Arbitrary (Sum '[] x) where
+  arbitrary = return Void
+  shrink _ = []
+
+instance (Traversable f, Q.Arbitrary (f x)) => Q.Arbitrary (Sum (f ': '[]) x) where
+  arbitrary = Here <$> Q.arbitrary
+  shrink (Here x)  = map Here  $ Q.shrink x
+  shrink (There x) = map There $ Q.shrink x
+
+instance (Traversable f, Q.Arbitrary (f x), Q.Arbitrary (Sum (g ': fs) x)) => Q.Arbitrary (Sum (f ': g ': fs) x) where
+  arbitrary = Q.oneof [Here <$> Q.arbitrary, There <$> Q.arbitrary]
+  shrink (Here x)  = map Here  $ Q.shrink x
+  shrink (There x) = map There $ Q.shrink x
+
+
+
+-- | The prisms for accessing the first functor in the Sum
+_Here :: Traversable f => Prism' (Sum (f ': fs) x) (f x)
+_Here = let a :: Sum (f ': fs) x -> Maybe (f x)
+            a (Here x) = Just x
+            a _        = Nothing
+    in prism' Here a
+
+-- | The prisms for accessing the rest of functors in the Sum
+_There :: Traversable f => Prism' (Sum (f ': fs) x) (Sum fs x)
+_There = let a :: Sum (f ': fs) x -> Maybe (Sum fs x)
+             a (There x) = Just x
+             a _         = Nothing
+    in prism' There a
+
+
+
+-- | The constraint that functor f is an element of 'Sum' fs
+class Elem f fs where
+  constructor :: Prism' (Sum fs x) (f x)
+
+-- | Unicode type synonym for 'Elem'
+type f ∈ fs = Elem f fs
+
+instance {-# OVERLAPPING #-} Traversable f => Elem f (f ': fs) where
+  constructor = _Here
+instance {-# OVERLAPPABLE #-} (Traversable f, Traversable g, Elem f fs) => Elem f (g ': fs) where
+  constructor = _There . constructor
+
+-- | The constraint that set of functors @fs@ is a subset of @gs@
+class Subset fs gs where
+  subrep :: Prism' (Sum gs x) (Sum fs x)
+
+-- | Unicode type synonym for 'Subset'
+type fs ⊆ gs = Subset fs gs
+
+instance {-# OVERLAPPING #-} Subset '[] '[] where
+  subrep = simple
+
+instance {-# OVERLAPPING #-} Subset '[] fs => Subset '[] (f ': fs) where
+  subrep = prism' There (const Nothing) . subrep
+
+instance {-# OVERLAPPABLE #-} (Traversable f, Elem f gs, Subset fs gs) => Subset (f ': fs) gs where
+  subrep = let fwd :: Sum (f ': fs) x -> Sum gs x
+               fwd (Here x)  = review constructor x
+               fwd (There x) = review subrep x
+
+               bwd :: Sum gs x -> Maybe (Sum (f ': fs) x)
+               bwd ((^? constructor ) -> Just x) = Just (Here x)
+               bwd ((^? subrep) -> Just x) = Just (There x)
+               bwd _                     = Nothing
+           in prism' fwd bwd
+
+
+-- * Tools for matching
+
+-- | The constraint that object @x@ can somehow be matched to functor @f@, that is, there is a 'Prism'' from type @x@
+--   to type @f (Content f x)@.
+class Matches f x where
+  type Content f x :: *
+  match :: Prism' x (f (Content f x))
+
+-- | The type of the  'Prism'' that matches any @x@ such that @Matches f x@.
+type MatchPrism (f :: * -> *) = forall x. Matches f x => Prism' x (f (Content f x))
+
+
+instance Matches f (f x) where
+  type Content f (f x) = x
+  match = simple
+
+-- * Syntax tree
+
+-- | The compiler metadata.
+data Metadata = Metadata {_metadataRendering :: P.Rendering, _metadataBegin :: P.Delta,  _metadataEnd :: P.Delta}
+makeLenses ''Metadata
+
+instance Show Metadata where
+  show = const ""
+instance P.HasRendering Metadata where
+  rendering = metadataRendering
+
+-- | The fix point of F-algebra, with compiler metadata information. This is the datatype we use to represent any AST.
+data Fix f where
+  In :: Functor f => {_metadata :: Maybe Metadata, _out :: f (Fix f)} -> Fix f
+
+instance (Eq (f (Fix f))) => Eq (Fix f) where
+  (In _ a) == (In _ b) = a == b
+instance (Ord (f (Fix f))) => Ord (Fix f) where
+  compare (In _ a) (In _ b) = compare a b
+
+instance (Show (f (Fix f))) => Show (Fix f) where
+  showsPrec n (In _ x) = showsPrec n x
+
+instance (f ∈ fs) => Matches f (Fix (Sum fs)) where
+  type Content f (Fix (Sum fs)) = Fix (Sum fs)
+  match = fix . constructor
+
+instance (Functor f, Q.Arbitrary (f (Fix f))) => Q.Arbitrary (Fix f) where
+  arbitrary       = In Nothing <$> Q.arbitrary
+  shrink (In h x) = map (In h) $ Q.shrink x
+
+
+-- | The lens that accesses the compiler metadata of the syntax tree
+metadata :: Functor f => Lens' (Fix f) (Maybe Metadata)
+metadata fun (In p o) = fmap (\p' -> In p' o) (fun p)
+
+-- | The lens to convert to/from 'Fix' and its content.
+
+fix :: forall f. Functor f => Iso' (Fix f) (f (Fix f))
+fix = iso _out go
+  where
+    go :: f (Fix f) -> Fix f
+    go ffixf = In Nothing ffixf
+
+-- * Syntax tree utility
+
+
+
+-- | Languages are 'Fix' over 'Sum' of functors
+type Lang (fs :: [ * -> * ]) = Fix (Sum fs)
+
+
+-- | An F-algebra.
+type Algebra f a = f a -> a
+
+-- | A monadic F-algebra.
+type AlgebraM m f a = f a -> m a
+
+-- | A precursor for an 'Algebra' .
+type Algebrogen f a b = f a -> b
+
+
+-- | The catamorphism that is specialized to 'Lang' . It copies the metadata from @Lang f@ to @Lang g@.
+
+fold :: Algebra f (Lang g) -> Fix f -> (Lang g)
+fold k (In meta x) = propagateMetadata meta $ k $ fmap (fold k) x
+
+-- | Monadic 'fold' .
+
+mfold :: (Monad m, Traversable f) => AlgebraM m f (Lang g) -> Fix f -> m (Lang g)
+mfold k (In meta x) = do
+  r1 <- traverse (mfold k) x
+  r2 <- k r1
+  return $ propagateMetadata meta r2
+
+-- | Propagate Metadata from the top of the syntax tree, in case the algebra had added more than one constructors.
+
+propagateMetadata :: Maybe Metadata -> Lang f -> Lang f
+propagateMetadata Nothing x = x
+propagateMetadata (Just meta) x = go x
+  where
+    go (In Nothing y) = In (Just meta) $ fmap go y
+    go y = y
+
+
+-- | Lift an 'Algebrogen' to monad.
+
+mlift :: (Monad m, Traversable fs) => Algebrogen fs a b -> Algebrogen fs (m a) (m b)
+mlift fsa2b fsma = liftM fsa2b $ sequence fsma
+
+-- | A generic catamorphism, where the compiler metadata is lost.
+
+foldout :: Algebra f a -> Fix f -> a
+foldout k (In _ x) = k $ fmap (foldout k) x
+
+-- | Monadic 'foldout' .
+
+mfoldout :: Monad m => (Sum fs a -> m a) -> Lang fs -> m a
+mfoldout k x = foldout (join . mlift k) x
+
+-- | Promote a @Lang fs@ to @Lang gs@, when @gs@ has more constructors than @fs@.
+
+subFix :: (fs ⊆ gs) => Lang fs -> Lang gs
+subFix = fold (review (fix . subrep))
+
+-- | Restrict a function from @Lang gs@ to that from @Lang fs@, where @fs@ has less constructors than @gs@.
+
+subOp :: (fs ⊆ gs) => (Lang gs -> c) -> Lang fs -> c
+subOp g = g . subFix
+
+-- | An algebra that just copies what found in @Lang fs@ to @Lang gs@.
+
+transAlg :: (fs ⊆ gs) => Algebra (Sum fs) (Lang gs)
+transAlg = review (fix . subrep)
+
+-- | A monadic 'transAlg' .
+
+mTransAlg :: (Monad m, fs ⊆ gs) => AlgebraM m (Sum fs) (Lang gs)
+mTransAlg = return . transAlg
+
+-- | Cons an algebra to a 'Sum' of an algebra, to create a larger algebra.
+
+(+::) :: Algebrogen f a b -> Algebrogen (Sum fs) a b -> Algebrogen (Sum (f ': fs)) a b
+af +:: afs = affs
+  where
+    affs (Here x)  = af  x
+    affs (There x) = afs x
+
+-- | Override a specific algebra @f@ in an algebra over @fs@.
+
+(>::) :: (f ∈ fs) => Algebrogen f a b -> Algebrogen (Sum fs) a b -> Algebrogen (Sum fs) a b
+af >:: afs= affs
+  where
+    affs ((^? constructor) -> Just fa) = af  fa
+    affs x                             = afs x
+
+-- | Override a subset algebra @fs@ within wider algebra @gs@.
+
+(>>::) :: (fs ⊆ gs) => Algebrogen (Sum fs) a b -> Algebrogen (Sum gs) a b -> Algebrogen (Sum gs) a b
+af >>:: afs= affs
+  where
+    affs ((^? subrep) -> Just fa) = af  fa
+    affs x                        = afs x
+
+
+
+
+infixr 5 +::, >::, >>::
diff --git a/src/Formura/OrthotopeMachine/Graph.hs b/src/Formura/OrthotopeMachine/Graph.hs
new file mode 100644
--- /dev/null
+++ b/src/Formura/OrthotopeMachine/Graph.hs
@@ -0,0 +1,101 @@
+{- |
+Copyright   : (c) Takayuki Muranushi, 2015
+License     : MIT
+Maintainer  : muranushi@gmail.com
+Stability   : experimental
+
+A virtual machine with multidimensional vector instructions that operates on structured lattices, as described
+in http://arxiv.org/abs/1204.4779 .
+-}
+
+{-# LANGUAGE DataKinds, DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances, PatternSynonyms,TemplateHaskell, TypeSynonymInstances, ViewPatterns #-}
+
+module Formura.OrthotopeMachine.Graph where
+
+import           Algebra.Lattice
+import           Control.Lens
+import qualified Data.IntMap as G
+
+import qualified Formura.Annotation as A
+import           Formura.Language.Combinator
+import           Formura.Syntax
+import           Formura.Type
+import           Formura.Vec
+
+-- | The functor for orthotope machine-specific instructions. Note that arithmetic operations are outsourced.
+
+data DataflowInstF x
+  = LoadF IdentName
+  | StoreF IdentName x
+  | LoadIndexF Int
+  | LoadExtentF Int
+  | ShiftF (Vec Int) x
+  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
+
+
+-- | smart patterns
+pattern Load n <- ((^? match) -> Just (LoadF n)) where
+  Load n = match # LoadF n
+pattern Store n x <- ((^? match) -> Just (StoreF n x)) where
+  Store n x = match # StoreF n x
+pattern LoadIndex n <- ((^? match) -> Just (LoadIndexF n)) where
+  LoadIndex n = match # LoadIndexF n
+pattern LoadExtent n <- ((^? match) -> Just (LoadExtentF n)) where
+  LoadExtent n = match # LoadExtentF n
+pattern Shift v x <- ((^? match) -> Just (ShiftF v x)) where
+  Shift v x = match # ShiftF v x
+
+type OMInstF = Sum '[DataflowInstF, OperatorF, ImmF]
+type OMInst  = Fix OMInstF
+
+type NodeTypeF = Sum '[ TopTypeF, GridTypeF, ElemTypeF ]
+type NodeType  = Fix NodeTypeF
+
+instance MeetSemiLattice NodeType where
+  (/\) = semiLatticeOfNodeType
+
+semiLatticeOfNodeType :: NodeType -> NodeType -> NodeType
+semiLatticeOfNodeType a b = case go a b of
+  TopType -> go b a
+  c       -> c
+  where
+    go :: NodeType -> NodeType -> NodeType
+    go a b | a == b = a
+    go (ElemType ea) (ElemType eb) = subFix (ElemType ea /\ ElemType eb :: ElementalType)
+    go a@(ElemType _) b@(GridType v c) = let d = a /\ c in
+           if d==TopType then TopType else GridType v d
+    go (GridType v1 c1) (GridType v2 c2) = (if v1 == v2 then GridType v1 (c1 /\ c2) else TopType)
+    go _ _          = TopType
+
+
+type NodeID  = G.Key
+data Node = Node {_nodeInst :: OMInstF NodeID, _nodeType :: NodeType, _nodeAnnot :: A.Annotation}
+instance Show Node where
+  show (Node i t _) = show i ++ " :: " ++ show t
+
+
+makeLenses ''Node
+instance A.Annotated Node where
+  annotation = nodeAnnot
+
+type Graph = G.IntMap Node
+
+data NodeValueF x = NodeValueF NodeID NodeType
+                 deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
+
+pattern NodeValue n t <- ((^? match) -> Just (NodeValueF n t)) where NodeValue n t = match # NodeValueF n t
+pattern n :. t <- ((^? match) -> Just (NodeValueF n t)) where n :. t = match # NodeValueF n t
+
+
+data FunValueF x = FunValueF LExpr RXExpr
+                 deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
+pattern FunValue l r <- ((^? match) -> Just (FunValueF l r)) where FunValue l r = match # FunValueF l r
+
+
+-- | RXExpr is RExpr extended with NodeValue constructors
+type RXExprF = Sum '[ LetF, LambdaF, ApplyF, GridF, TupleF, OperatorF, IdentF, FunValueF, NodeValueF, ImmF ]
+type RXExpr  = Fix RXExprF
+type ValueExprF = Sum '[TupleF, FunValueF, NodeValueF, ImmF]
+type ValueExpr = Fix ValueExprF
+type ValueLexExprF = Sum '[TupleF, FunValueF, NodeValueF, IdentF, ImmF]
+type ValueLexExpr = Fix ValueLexExprF
diff --git a/src/Formura/OrthotopeMachine/Translate.hs b/src/Formura/OrthotopeMachine/Translate.hs
new file mode 100644
--- /dev/null
+++ b/src/Formura/OrthotopeMachine/Translate.hs
@@ -0,0 +1,288 @@
+{-# LANGUAGE DataKinds, DeriveFunctor, DeriveFoldable,
+DeriveTraversable, FlexibleContexts, FlexibleInstances, PatternSynonyms,
+TemplateHaskell, TypeOperators, ViewPatterns #-}
+module Formura.OrthotopeMachine.Translate where
+
+import           Algebra.Lattice
+import           Control.Applicative
+import           Control.Lens hiding (op)
+import           Control.Monad
+import           Control.Monad.Reader
+import qualified Data.IntMap as G
+import qualified Data.Map as M
+import qualified Data.Set as S
+import           Data.Ratio
+import           Text.Trifecta (failed, raiseErr)
+
+import           Formura.Language.Combinator
+import qualified Formura.Annotation as A
+import           Formura.Annotation.Representation
+import           Formura.Compiler
+import           Formura.Syntax
+import           Formura.Type
+import           Formura.Vec
+import           Formura.OrthotopeMachine.Graph
+
+
+type Binding = M.Map IdentName ValueExpr
+type LexBinding = M.Map IdentName ValueLexExpr
+
+class HasBinding s where
+  binding :: Lens' s Binding
+
+instance HasBinding Binding where
+  binding = simple
+
+data CodegenState = CodegenState
+  { _codegenSyntacticState :: CompilerSyntacticState
+  , _theGraph :: Graph
+  }
+makeClassy ''CodegenState
+
+defaultCodegenState :: CodegenState
+defaultCodegenState = CodegenState
+  { _codegenSyntacticState = defaultCompilerSyntacticState{ _compilerStage = "codegen"}
+  , _theGraph = G.empty
+  }
+
+defaultCodegenRead :: Binding
+defaultCodegenRead = M.empty
+
+instance HasCompilerSyntacticState CodegenState where
+  compilerSyntacticState = codegenSyntacticState
+
+
+-- | the code generator monad.
+type GenM = CompilerMonad Binding () CodegenState
+type LexGenM = CompilerMonad LexBinding () CodegenState
+
+
+class Generatable f where
+  gen :: f (GenM ValueExpr) -> GenM ValueExpr
+
+freeNodeID :: GenM NodeID
+freeNodeID = do
+  g <- use theGraph
+  return $ G.size g
+
+insert :: OMInstF NodeID -> NodeType -> GenM ValueExpr
+insert inst typ = do
+  n0 <- freeNodeID
+  foc <- use compilerFocus
+  let a = case foc of
+        Just meta -> A.singleton meta
+        Nothing   -> A.empty
+  theGraph %= G.insert n0 (Node inst typ a)
+  mmeta <- use compilerFocus
+  case mmeta of
+       Just meta -> theGraph . ix n0 . A.annotation %= A.set meta
+       _         -> return ()
+
+  return $ NodeValue n0 typ
+
+
+-- | Find the type of a 'ValueExpr' .
+typeOfVal :: ValueExpr -> TypeExpr
+typeOfVal (Imm _)         = ElemType "Rational"
+typeOfVal (NodeValue _ t) = subFix t
+typeOfVal (FunValue _ _)  = FunType
+typeOfVal (Tuple xs)      = Tuple $ map typeOfVal xs
+
+
+-- | convert a value to other value, so that the result may have the given type
+castVal :: TypeExpr -> ValueExpr -> GenM ValueExpr
+castVal t1 vx = let t0 = typeOfVal vx in case (t1, t0, vx) of
+  _ | t1 == t0 -> return vx
+  (ElemType _, ElemType _, _) -> return vx
+  (GridType vec (ElemType te), ElemType _, n :. _) -> return (n :. (GridType vec (ElemType te)))
+  (GridType vec0 _, GridType vec1 _, _) | vec0 == vec1 ->  return vx
+  _ -> raiseErr $ failed $ "cannot convert type " ++ show t0 ++ " to " ++ show t1
+
+
+
+instance Generatable ImmF where
+  gen (Imm r) = do
+    insert (Imm r) (ElemType "Rational")
+
+instance Generatable OperatorF where
+  gen (Uniop op gA)       = do a <- gA                  ; goUniop op a
+  gen (Binop op gA gB)    = do a <- gA; b <- gB         ; goBinop op a b
+  gen (Triop op gA gB gC) = do a <- gA; b <- gB; c <- gC; goTriop op a b c
+
+goUniop :: IdentName -> ValueExpr -> GenM ValueExpr
+goUniop op (av :. at) = insert (Uniop op av) at
+goUniop _ _  = raiseErr $ failed $ "unimplemented path in unary operator"
+
+goBinop :: IdentName -> ValueExpr -> ValueExpr -> GenM ValueExpr
+goBinop op ax@(av :. at) bx@(bv :. bt) = case at /\ bt of
+  TopType -> raiseErr $ failed $ unwords
+             ["there is no common type that can accomodate both hand side:", show at, op , show bt]
+  ct -> do
+    (av2 :. _) <- castVal (subFix ct) ax
+    (bv2 :. _) <- castVal (subFix ct) bx
+    insert (Binop op av2 bv2) ct
+
+goBinop _ _ _  = raiseErr $ failed $ "unimplemented path in binary operator"
+
+goTriop :: IdentName -> ValueExpr -> ValueExpr -> ValueExpr -> GenM ValueExpr
+goTriop op (av :. at) (bv :. bt) (cv :. ct)
+  | op == "ite" && at == ElemType "bool" && bt == ct = insert (Triop op av bv cv) bt
+goTriop _ _ _ _ = raiseErr $ failed $ "unimplemented path in trinary operator"
+
+instance Generatable IdentF where
+  -- you should not generate this!
+  gen (Ident n) = do
+    b <- view binding
+    case M.lookup n b of
+      Nothing -> do
+        raiseErr $ failed $ "undefined variable: " ++ n ++ "\n Bindings:\n" ++ show b
+      Just x  -> return $ subFix x
+
+
+instance Generatable TupleF where
+  gen (Tuple xsGen) = do
+    xs <- sequence xsGen
+    return $ Tuple xs
+
+instance Generatable GridF where
+  gen (Grid npks gen0) = do
+    vt0@(val0 :. typ0) <- gen0
+    case typ0 of
+      ElemType _   -> return vt0
+      GridType offs0 etyp0 -> do
+        let
+            patK   = fmap (^. _2) (npks :: Vec NPlusK)
+            newPos = offs0 - patK
+            intOff = fmap floor newPos
+            newOff = liftA2 (\r n -> r - fromIntegral n) newPos intOff
+            typ1 = GridType newOff etyp0
+        if intOff == 0
+                then return (val0 :. typ1)
+                else insert (Shift intOff val0) typ1
+
+  gen _ = raiseErr $ failed "unexpected happened in gen of grid"
+
+instance Generatable ApplyF where
+  gen (Apply fgen agen) = do
+    f0 <- fgen
+    a0 <- agen
+    goApply f0 a0
+
+goApply :: ValueExpr -> ValueExpr -> GenM ValueExpr
+goApply (Tuple xs) (Imm r) = do
+  when (denominator r /= 1) $ raiseErr $ failed "non-integer indexing in tuple access"
+  let n = fromInteger $  numerator r
+      l = length xs
+  when (n < 0 || n >= l) $ raiseErr $ failed "tuple access out of bounds"
+  return $ xs!!n
+goApply (Tuple xs) _ = raiseErr $ failed "tuple applied to non-constant integer"
+goApply (FunValue l r) x = do
+  local (M.insert (nameOfLhs l) x) $ genRhs r
+goApply  _ _ = raiseErr $ failed "unexpected combination of application"
+
+instance Generatable LambdaF where
+  -- Expand all but bound variables, in order to implement lexical scope
+  gen (Lambda l r) = do
+    let conv :: Binding -> CodegenState -> (LexBinding, CodegenState)
+        conv b s = (M.insert (nameOfLhs l) (Ident $ nameOfLhs l) $ M.map subFix b, s)
+    r' <- withCompiler conv $ resolveLex $ subFix r
+    return $ FunValue l r'
+
+resolveLex :: RXExpr -> LexGenM RXExpr
+resolveLex r = compilerMFold resolveLexAlg r
+
+resolveLexAlg :: RXExprF RXExpr -> LexGenM RXExpr
+resolveLexAlg (Ident n) = do
+  b <- ask
+  case M.lookup n b of
+    Nothing -> raiseErr $ failed $ "undefined variable: " ++ n
+    Just x  -> return $ subFix x
+resolveLexAlg (Lambda l r) = do
+  r' <- local (M.insert (nameOfLhs l) (Ident $ nameOfLhs l)) $ resolveLex $ subFix r
+  return $ FunValue l r'
+resolveLexAlg (FunValue l r) = do
+  r' <- local (M.insert (nameOfLhs l) (Ident $ nameOfLhs l)) $ resolveLex r
+  return $ FunValue l r'
+resolveLexAlg fx = mTransAlg fx
+
+instance Generatable LetF where
+  gen (Let b genX) = withBindings b genX
+
+nameOfLhs :: LExpr -> IdentName
+nameOfLhs (Ident n) = n
+nameOfLhs (Grid _ x) = nameOfLhs x
+nameOfLhs (Vector _ x) = nameOfLhs x
+nameOfLhs _ = error "tuple unsupported in type decl"
+
+withBindings :: BindingF (GenM ValueExpr) -> GenM ValueExpr -> GenM ValueExpr
+withBindings b1 genX = do
+  b0 <- view binding
+  let
+      BindingF stmts0 = b1
+      typeDecls0 :: [(LExpr, TypeExpr)]
+      typeDecls0 = concat $ flip map stmts0 $ \x -> case x of
+        TypeDeclF t l -> [(l, t)]
+        _             -> []
+
+      substs0 :: [(LExpr, GenM ValueExpr)]
+      substs0 = concat $ flip map stmts0 $ \x -> case x of
+        SubstF l r -> [(l, r)]
+        _             -> []
+
+      typeDict :: M.Map IdentName TypeExpr
+      typeDict = M.fromList [(nameOfLhs l, t) | (l,t)<- typeDecls0]
+
+  let
+    -- Let bindings enter scope one by one, not simultaneously
+    graduallyBind :: [(LExpr, GenM ValueExpr)] -> GenM [(IdentName, ValueExpr)]
+    graduallyBind [] = return []
+    graduallyBind ((l,genV): restOfBinds) = do
+      v0 <- genV
+      v <- case M.lookup (nameOfLhs l) typeDict of
+        Nothing -> return v0
+        Just t  -> castVal t v0
+      case v of
+       (n :. _) -> do
+         theGraph . ix n . A.annotation %= A.set (SourceName $ nameOfLhs l)
+         theGraph . ix n . A.annotation %= A.set Manifest
+       _        -> return ()
+
+      -- TODO: LHS grid pattern must be taken care of.
+
+      b2s <- local (binding %~ M.insert (nameOfLhs l) v) $ graduallyBind restOfBinds
+      return ((nameOfLhs l, v) : b2s)
+  substs1 <- graduallyBind substs0
+
+
+  --  M.union prefers left-hand-side when duplicate keys are encountered
+  local (binding %~ M.union (M.fromList substs1)) genX
+
+
+
+
+instance Generatable (Sum '[]) where
+  gen _ =  raiseErr $ failed "impossible happened: gen of Void"
+
+instance Generatable NodeValueF where
+  gen (NodeValue t v) = return (NodeValue t v)
+
+instance Generatable FunValueF where
+  gen (FunValue l r) = return (FunValue l r)
+
+instance (Generatable f, Generatable (Sum fs)) => Generatable (Sum (f ': fs)) where
+  gen =  gen +:: gen
+
+genRhs :: RXExpr -> GenM ValueExpr
+genRhs r = compilerFoldout gen r
+
+genMainFunction :: RExpr -> GenM ()
+genMainFunction (Lambda l r) = do
+  v <- insert (Load "input_value") (GridType (Vec [0]) (ElemType "double"))
+  let (n :. _ ) = v
+  theGraph . ix n . A.annotation %= A.set Manifest
+
+  (n99 :. t99) <- genRhs $ Apply (FunValue l (subFix r)) (subFix v)
+
+  theGraph . ix n99 . A.annotation %= A.set Manifest
+  return ()
+genMainFunction _ = raiseErr $ failed "Please specify a function for generation"
diff --git a/src/Formura/Parser.hs b/src/Formura/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/Formura/Parser.hs
@@ -0,0 +1,426 @@
+{-|
+Module      : Formura.Parser
+Description : parser combinator
+Copyright   : (c) Takayuki Muranushi, 2015
+License     : MIT
+Maintainer  : muranushi@gmail.com
+Stability   : experimental
+
+This module contains combinator for writing Formura parser, and also the parsers for Formura syntax.
+-}
+
+{-# LANGUAGE FlexibleContexts, GeneralizedNewtypeDeriving, TypeOperators #-}
+module Formura.Parser where
+
+import Control.Applicative
+import Control.Lens
+import Control.Monad
+import Data.Char (isSpace, isLetter, isAlphaNum, isPrint)
+import Data.Either (partitionEithers)
+import Data.Maybe
+import Data.Monoid
+import qualified Data.Set as S
+import Text.Trifecta hiding (ident)
+import Text.Trifecta.Delta
+import qualified Text.Parser.Expression as X
+import qualified Text.PrettyPrint.ANSI.Leijen as Ppr
+
+import Text.Parser.LookAhead
+
+import Formura.Language.Combinator
+import Formura.Vec
+import Formura.Syntax
+
+-- * The parser comibnator
+
+-- | The parser monad.
+newtype P a = P { runP :: Parser a }
+            deriving (Alternative, Monad, Functor, MonadPlus, Applicative, CharParsing, LookAheadParsing, Parsing, DeltaParsing, MarkParsing Delta)
+
+instance Errable P where
+  raiseErr = P . raiseErr
+
+instance TokenParsing P where
+  someSpace =
+    let  f '\n' = False
+         f '\r' = False
+         f x | isSpace x = True
+             | otherwise = False
+
+    in "whitespace" ?> some ((satisfy f >> return ())
+             <|> comment
+             <|> lineContinuation)
+       >> return ()
+
+-- | Document the parser.
+(?>) :: String -> P a -> P a
+s ?> p = p <?> s
+
+infixr 0 ?>
+
+-- | Parse a string as a keyword. Check if the keyword is indeed in a keyword list.
+keyword :: IdentName -> P IdentName
+keyword k = "keyword " ++ k ?> do
+  when (k `S.notMember` keywordSet) $
+    raiseErr $ failed $
+    "Please report the compiler developer: \"" ++ k ++ "\" is not in a keyword list!"
+  symbol k
+
+-- | The set of keywords. The string is not parsed as a identifier if it's in the keyword list.
+keywordSet :: S.Set IdentName
+keywordSet = S.fromList
+             ["begin", "end", "function", "returns", "let", "in", "lambda", "for", "dimension", "axes",
+              "+","-","*","/",".","::","=", ","]
+
+
+comment :: P ()
+comment = "comment" ?> do
+  char '#'
+  manyTill anyChar (lookAhead newline)
+  return ()
+
+lineContinuation :: P ()
+lineContinuation = "line continuation" ?> do
+  char '\\'
+  whiteSpace
+  newline
+  return ()
+
+-- | Run parser, and record the metadata for the parsed syntax component
+parseIn :: Functor f => P (Fix f) -> P (Fix f)
+parseIn p = do
+  r1 <- rend
+  (In m x)  <- p
+  r2 <- rend
+  let m2 = Just $ Metadata r1 (delta r1) (delta r2)
+  return $ In (m <|> m2) x
+
+
+-- * The parser for Formura syntax
+
+isIdentifierAlphabet0 :: Char -> Bool
+isIdentifierAlphabet0 = isLetter
+isIdentifierAlphabet1 :: Char -> Bool
+isIdentifierAlphabet1 c = isAlphaNum c || c == '_'  || c == '\''
+isIdentifierSymbol :: Char -> Bool
+isIdentifierSymbol c = isPrint c &&
+  not (isIdentifierAlphabet1 c || isSpace c ||
+      c `elem` "\"#();[\\]{}")
+
+identName :: P IdentName
+identName = "identifier" ?> try $ do
+  let s :: P String
+      s = some $ "symbolic character" ?> satisfy isIdentifierSymbol
+      a0 :: P Char
+      a0 = "identifier alphabet character" ?> satisfy isIdentifierAlphabet0
+      a1 :: P Char
+      a1 = "identifier alphabet character" ?> satisfy isIdentifierAlphabet1
+      a :: P String
+      a = (:) <$> a0 <*> many a1
+  str <- s <|> a
+  guard $  str `S.notMember` keywordSet
+  whiteSpace
+  return str
+
+
+
+ident :: (IdentF ∈ fs) => P (Lang fs)
+ident = "identifier" ?> parseIn $ Ident <$> identName
+
+elemType :: (ElemTypeF ∈ fs) => P (Lang fs)
+elemType = "element type" ?> parseIn $ do
+  str <- identName
+  guard $ str `S.member` elemTypeNames
+  return $ ElemType str
+    where
+      elemTypeNames = S.fromList ["int","rational","float","double","real"]
+
+funType :: (FunTypeF ∈ fs) => P (Lang fs)
+funType = "function type" ?> parseIn $ keyword "function" *> pure FunType
+
+
+tupleOf :: (TupleF ∈ fs) => P (Lang fs) -> P (Lang fs)
+tupleOf p = "tuple" ?> {- don't parseIn here ... -} do
+  r1 <- rend
+  "tuple opening" ?> try $ symbolic '('
+  xs <- p `sepBy` symbolic ','
+  symbolic ')'
+  r2 <- rend
+  case xs of
+    -- ... because we treat one-element tuple as parenthesized expression.
+    [x] -> return x
+    _   -> return $ In (Just $ Metadata r1 (delta r1) (delta r2)) $ Tuple xs
+
+gridIndicesOf :: P a -> P (Vec a)
+gridIndicesOf parseIdx = "grid index" ?> do
+  "grid opening" ?> try $ symbolic '['
+  xs <- parseIdx `sepBy` symbolic ','
+  symbolic ']'
+  return $ Vec xs
+
+nPlusK :: P NPlusK
+nPlusK = "n+k pattern" ?> do
+  x <-  identName
+  mn <- optional $ do
+    s <- symbolic '+' <|> symbolic '-'
+    n <- constRationalExpr
+    if s == '+' then return n else return (negate n)
+  return $ NPlusK x (maybe 0 id mn)
+
+
+
+imm :: (ImmF ∈ fs) => P (Lang fs)
+imm = "rational literal" ?> parseIn $ do
+  Imm <$> constRational
+
+exprOf :: (OperatorF ∈ fs, ApplyF  ∈ fs) => P (Lang fs) -> P (Lang fs)
+exprOf termParser = X.buildExpressionParser tbl termParser
+  where
+    tbl = [[binary "." Apply X.AssocRight],
+           [binary "**" (Binop "**") X.AssocLeft],
+           [binary "*" (Binop "*") X.AssocLeft, binary "/" (Binop "/") X.AssocLeft],
+           [unary "+" (Uniop "+") , unary "-" (Uniop "-") ],
+           [binary "+" (Binop "+") X.AssocLeft, binary "-" (Binop "-") X.AssocLeft]
+          ]
+    unary  name fun = X.Prefix (pUni name fun)
+    binary name fun assoc = X.Infix (pBin name fun) assoc
+
+    pUni name fun = "unary operator " ++ name ?> do
+      r1 <- rend
+      f <- fun <$ keyword name
+      r2 <- rend
+      return $ \a -> f a & metadata .~ (Just $ joinMeta r1 r2 a a)
+
+    pBin name fun = "binary operator " ++ name ?> do
+      r1 <- rend
+      f <- fun <$ keyword name
+      r2 <- rend
+      return $ \a b -> f a b & metadata .~ (Just $ joinMeta r1 r2 a b)
+
+    joinMeta r1 r2 a b = let
+      da = case a ^. metadata of
+        Nothing -> delta r1
+        Just ma -> min (ma ^. metadataBegin) (delta r1)
+      db = case b ^. metadata of
+        Nothing -> delta r2
+        Just mb -> max (mb ^. metadataEnd) (delta r2)
+      in Metadata r1 da db
+
+expr10 :: P RExpr
+expr10 = fexpr
+
+fexpr :: P RExpr
+fexpr = "function application chain" ?> do
+  f <- aexpr
+  findArgument f
+  where
+    findArgument :: RExpr -> P RExpr
+    findArgument f = parseIn $ do
+      mx' <- optional $ gridIndicesOf nPlusK
+      case mx' of
+        Just x -> findArgument $ Grid x f
+        Nothing ->do
+          mx <- optional $ aexpr
+          case mx of
+            Just x -> findArgument $ Apply f x
+            Nothing ->  return f
+
+
+aexpr :: P RExpr
+aexpr = tupleOf rExpr <|> letExpr <|> lambdaExpr <|> ident <|> imm
+
+
+letExpr :: P RExpr
+letExpr = "let expression" ?> parseIn $ do
+  "keyword let" ?> try $ keyword "let"
+  xs <- binding
+  keyword "in"
+  x <- rExpr
+  return $ Let xs x
+
+lambdaExpr :: P RExpr
+lambdaExpr = "lambda expression" ?> parseIn $ do
+  "keyword for" ?> try $ keyword "for"
+  x <- tupleOf lExpr
+  y <- rExpr
+  return $ Lambda x y
+
+binding :: P (BindingF RExpr)
+binding = "statements" ?> do
+  stmts <- statementCompound `sepEndBy` statementDelimiter
+  return $ Binding $ concat stmts
+
+statementDelimiter :: P ()
+statementDelimiter = "statement delimiter" ?> some d >> return ()
+  where
+    d = (symbolic ';' >> return ()) <|> (newline >> whiteSpace)
+
+statementCompound :: P [StatementF RExpr]
+statementCompound = functionSyntaxSugar <|> typeValueStatements
+
+functionSyntaxSugar :: P [StatementF RExpr]
+functionSyntaxSugar = "function definition" ?> do
+  keyword "begin"
+  keyword "function"
+  (funName, inExpr, outExpr) <-
+    ("returns-form" ?> try returnsForm) <|>
+    ("equal-form" ?> try equalForm) <|>
+    raiseErr (Err (Just $ Ppr.text "Malformed Function Syntax" <> Ppr.line)
+              [Ppr.text "Please check if you are using one of the following forms:",
+               Ppr.text "・  begin function f(x) returns y",
+               Ppr.text "・  begin function y = f(x)"]
+              S.empty)
+  statementDelimiter
+  b <- binding
+  keyword "end"
+  keyword "function"
+  return [Subst funName $ Lambda inExpr $ Let b outExpr]
+  where
+    returnsForm :: P (LExpr, LExpr, RExpr)
+    returnsForm = do
+      fn <- ident
+      inx <- tupleOf lExpr
+      keyword "returns"
+      outx <- rExpr
+      return (fn, inx, outx)
+
+    equalForm :: P (LExpr, LExpr, RExpr)
+    equalForm = do
+      outx <- rExpr
+      keyword "="
+      fn <- ident
+      inx <- tupleOf lExpr
+      return (fn, inx, outx)
+
+
+typeValueStatements :: P [StatementF RExpr]
+typeValueStatements = "type-decl and/or substitiution statement" ?> do
+  maybeType <- optional $ "statement start by type decl" ?> try $ typeExpr <* keyword "::"
+
+  let lhsAndMaybeRhs :: P (LExpr, Maybe RExpr)
+      lhsAndMaybeRhs = do
+        lhs   <- lExpr
+        mRhs  <- optional (keyword "=" >> rExpr)
+        return (lhs, mRhs)
+  lamrs <- case maybeType of
+    -- When there is type, we allow multiple substitutions, and lhs-only terms.
+    Just _ -> lhsAndMaybeRhs `sepBy1` symbol ","
+    -- When there is no type, we allow only one substitution.
+    Nothing -> do
+      lhs <- lExpr
+      keyword "="
+      rhs <- rExpr
+      return [(lhs, Just rhs)]
+
+  let typePart = [ TypeDecl typ lhs
+                 | typ <- maybeToList maybeType,
+                   lhs <- map fst lamrs
+                   ]
+      substPart = [Subst lhs rhs
+                   | (lhs, Just rhs) <- lamrs]
+  -- Type definitions always come before the values.
+  return $ typePart ++ substPart
+
+
+
+
+lAexpr :: P LExpr
+lAexpr = "atomic l-expr" ?> tupleOf lExpr <|> ident
+
+vectorIndexOf :: P a -> P a
+vectorIndexOf content = do
+  "vector index access" ?> try $ symbolic '('
+  r <- content
+  symbolic ')'
+  return r
+
+lFexpr :: P LExpr
+lFexpr = "applied l-expr" ?> do
+  f <- lAexpr
+  go f
+  where
+    go :: LExpr -> P LExpr
+    go f = parseIn $ do
+      mx <- "grid option" ?> optional $ gridIndicesOf nPlusK
+      case mx of
+        Just x -> go $ Grid x f
+        Nothing -> do
+          mx' <- "grid option" ?>  optional (vectorIndexOf identName)
+          case mx' of
+            Just x -> go $ Vector x f
+            Nothing -> return f
+
+lExpr :: P LExpr
+lExpr = "l-expr" ?> lFexpr
+
+typeExpr :: P TypeExpr
+typeExpr = typeFexpr
+
+typeAexpr :: P TypeExpr
+typeAexpr = "atomic type-expression" ?> tupleOf typeExpr <|> elemType <|> funType
+
+typeFexpr :: P TypeExpr
+typeFexpr = "applied type-expression" ?> do
+  f <- typeAexpr
+  go f
+  where
+    go :: TypeExpr -> P TypeExpr
+    go f = parseIn $ do
+      mx <- optional (gridIndicesOf constRationalExpr)
+      case mx of
+        Just x -> go $ GridType x f
+        Nothing -> do
+          mx' <- optional (vectorIndexOf constIntExpr)
+          case mx' of
+            Just x -> go $ VectorType x f
+            Nothing -> return f
+
+
+rExpr :: P RExpr
+rExpr = "r-expr" ?> exprOf expr10
+
+constRationalExpr :: P Rational
+constRationalExpr = "const rational expression" ?> do
+  cre <- exprOf imm
+  mfoldout evalCRE cre
+
+evalCRE :: ConstRationalExprF Rational -> P Rational
+evalCRE (Imm x) = return x
+evalCRE (Uniop "+" x) = return x
+evalCRE (Uniop "-" x) = return $ negate x
+evalCRE (Binop "+" a b) = return $ a + b
+evalCRE (Binop "-" a b) = return $ a - b
+evalCRE (Binop "*" a b) = return $ a * b
+evalCRE (Binop "/" a b) = return $ a / b
+evalCRE _ = raiseErr $ failed "unsupported operator in const rational expression"
+
+constRational :: P Rational
+constRational = "const rational expression" ?> do
+  nos <- naturalOrScientific
+  return $ either toRational toRational  nos
+
+
+constIntExpr :: P Int
+constIntExpr = fromInteger <$> natural
+
+
+specialDeclaration :: P SpecialDeclaration
+specialDeclaration = dd  <|> ad
+  where
+    dd = do
+      "dimension declaration" ?> try $ keyword "dimension"
+      keyword "::"
+      n <- natural
+      return $ DimensionDeclaration $ fromInteger n
+    ad = do
+      "axes declaration" ?> try $ keyword "axes"
+      keyword "::"
+      xs <- identName `sepBy` symbolic ','
+      return $ AxesDeclaration xs
+
+program :: P Program
+program = do
+  ps <- choice [Left <$> specialDeclaration, Right <$> statementCompound]
+        `sepEndBy` statementDelimiter
+  let (decls, stmts) = partitionEithers ps
+  return $ Program decls (BindingF $ concat stmts)
diff --git a/src/Formura/Syntax.hs b/src/Formura/Syntax.hs
new file mode 100644
--- /dev/null
+++ b/src/Formura/Syntax.hs
@@ -0,0 +1,261 @@
+{-|
+Module      : Language.Formura.Syntax
+Description : formura syntax elements
+Copyright   : (c) Takayuki Muranushi, 2015
+License     : MIT
+Maintainer  : muranushi@gmail.com
+Stability   : experimental
+
+Components for syntatic elements of formura.
+-}
+
+{-# LANGUAGE DataKinds, DeriveDataTypeable, DeriveFunctor, DeriveFoldable, DeriveGeneric,
+DeriveTraversable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses,
+PatternSynonyms, TemplateHaskell, ViewPatterns #-}
+
+module Formura.Syntax where
+
+import Algebra.Lattice
+import Control.Lens hiding (op)
+import Data.List (intercalate)
+import Data.Typeable
+import GHC.Generics
+import qualified Test.QuickCheck as Q
+
+import Formura.Language.Combinator
+import Formura.Vec
+
+-- * Syntactical Elements
+
+-- ** Elemental types
+
+data ElemTypeF x = ElemTypeF IdentName
+                 deriving (Eq, Ord, Functor, Foldable, Traversable, Typeable)
+instance Show (ElemTypeF x) where
+  show (ElemTypeF n) = n
+
+pattern ElemType x <- ((^? match) -> Just (ElemTypeF x)) where ElemType x = match # ElemTypeF x
+
+
+
+data FunTypeF x = FunTypeF
+                deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable)
+
+pattern FunType <- ((^? match) -> Just FunTypeF) where FunType = match # FunTypeF
+
+
+data TopTypeF x = TopTypeF
+                deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable)
+
+pattern TopType <- ((^? match) -> Just TopTypeF) where TopType = match # TopTypeF
+
+
+-- ** Identifier terms
+type IdentName = String
+
+data IdentF x = IdentF IdentName
+             deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable)
+
+-- | smart pattern
+pattern Ident xs <- ((^? match) -> Just (IdentF xs)) where
+  Ident xs = match # IdentF xs
+
+
+
+-- ** Tuple
+
+-- | The functor for tuple.
+data TupleF x = TupleF [x]
+             deriving (Eq, Ord, Functor, Foldable, Traversable, Typeable)
+instance Show x => Show (TupleF x) where
+  show (TupleF xs) = "(" ++ (intercalate ", " $ map show xs) ++ ")"
+
+instance Q.Arbitrary x => Q.Arbitrary (TupleF x) where
+  arbitrary = Q.sized $ \n -> do
+    k <- Q.choose (2,n)
+    xs <- Q.scale (`div` (1+k)) $ Q.vector k
+    return $ TupleF xs
+  shrink (TupleF xs) = map TupleF $ Q.shrink xs
+
+-- | smart pattern
+pattern Tuple xs <- ((^? match) -> Just (TupleF xs)) where
+  Tuple xs = match # TupleF xs
+
+
+
+-- ** Arithmetic elements
+
+-- | Rational Literal
+data ImmF x = ImmF Rational
+            deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable)
+
+pattern Imm r <- ((^? match) -> Just (ImmF r)) where
+  Imm r = match # ImmF r
+
+instance Q.Arbitrary x => Q.Arbitrary (ImmF x) where
+  arbitrary = ImmF <$> Q.arbitrary
+  shrink (ImmF x) = map ImmF $ Q.shrink x
+
+-- | Boolean Literal
+data ImmBoolF x = ImmBoolF Bool
+                deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable)
+
+pattern ImmBool r <- ((^? match) -> Just (ImmBoolF r)) where
+  ImmBool r = match # ImmBoolF r
+
+
+-- | Infix and Postfix operators
+data OperatorF x
+  = UniopF IdentName x
+  | BinopF IdentName x x
+  | TriopF IdentName x x x
+             deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable, Generic)
+
+instance Q.Arbitrary x => Q.Arbitrary (OperatorF x) where
+  arbitrary =
+    let compounds =
+          [ UniopF "+" <$> Q.arbitrary
+          , UniopF "-" <$> Q.arbitrary
+          , BinopF "+" <$> Q.arbitrary <*> Q.arbitrary
+          , BinopF "-" <$> Q.arbitrary <*> Q.arbitrary
+          , BinopF "*" <$> Q.arbitrary <*> Q.arbitrary
+          , BinopF "/" <$> Q.arbitrary <*> Q.arbitrary
+          ]
+        go n
+          | n <= 1 = UniopF "+" <$> Q.arbitrary
+          | otherwise = Q.oneof compounds
+    in Q.sized go
+  shrink = Q.genericShrink
+
+-- | smart patterns
+pattern Uniop op a <- ((^? match) -> Just (UniopF op a)) where
+  Uniop op a = match # UniopF op a
+pattern Binop op a b <- ((^? match) -> Just (BinopF op a b)) where
+  Binop op a b = match # BinopF op a b
+pattern Triop op a b c <- ((^? match) -> Just (TriopF op a b c)) where
+  Triop op a b c = match # TriopF op a b c
+
+-- ** Structures and Element Access
+
+data GridF x = GridF (Vec NPlusK) x
+             deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable)
+
+pattern Grid args x <- ((^? match) -> Just (GridF args x )) where
+  Grid args x = match # GridF args x
+
+data GridTypeF x = GridTypeF (Vec Rational) x
+             deriving (Eq, Ord, Functor, Foldable, Traversable, Typeable)
+instance Show x => Show (GridTypeF x) where
+  show (GridTypeF v x) = show x ++ show v
+
+pattern GridType args x <- ((^? match) -> Just (GridTypeF args x )) where
+  GridType args x = match # GridTypeF args x
+
+
+data VectorF x = VectorF IdentName x
+                   deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable)
+
+pattern Vector args x <- ((^? match) -> Just (VectorF args x )) where
+  Vector args x = match # VectorF args x
+
+data VectorTypeF x = VectorTypeF Int x
+                   deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable)
+
+pattern VectorType args x <- ((^? match) -> Just (VectorTypeF args x )) where
+  VectorType args x = match # VectorTypeF args x
+
+-- ** Functional Program Constituent
+
+-- | Function application
+data ApplyF x = ApplyF x x
+             deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable)
+
+pattern Apply f x <- ((^? match) -> Just (ApplyF f x)) where
+  Apply f x = match # ApplyF f x
+
+-- | Let clause
+data LetF x = LetF (BindingF x) x
+             deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable)
+
+pattern Let binds x <- ((^? match) -> Just (LetF binds x)) where
+  Let binds x = match # LetF binds x
+
+-- | Lambda expression. Lambda expression is not to recurse into its RExpr.
+data LambdaF x = LambdaF LExpr RExpr
+             deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable)
+
+pattern Lambda args x <- ((^? match) -> Just (LambdaF args x )) where
+  Lambda args x = match # LambdaF args x
+
+-- | Bunch of bindings
+data BindingF x = BindingF [StatementF x]
+             deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable)
+
+pattern Binding xs <- ((^? match) -> Just (BindingF xs )) where
+  Binding xs = match # BindingF xs
+
+-- | Statement
+data StatementF x
+  = SubstF LExpr x
+  -- ^ substitution
+  | TypeDeclF TypeExpr LExpr
+  -- ^ type declaration
+             deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Typeable)
+pattern Subst l r <- ((^? match) -> Just (SubstF l r)) where
+  Subst l r = match # SubstF l r
+pattern TypeDecl t x <- ((^? match) -> Just (TypeDeclF t x)) where
+  TypeDecl t x = match # TypeDeclF t x
+
+-- * Program Components
+
+type ConstRationalExprF = Sum '[ ApplyF, OperatorF, ImmF ]
+type ConstRationalExpr  = Lang '[ ApplyF, OperatorF, ImmF ]
+
+data NPlusK = NPlusK IdentName Rational
+             deriving (Eq, Ord, Show)
+instance Num NPlusK where
+  fromInteger n = NPlusK "" $ fromInteger n
+  (+)    = error "instance Num NPlusK is only partially defined"
+  (*)    = error "instance Num NPlusK is only partially defined"
+  (-)    = error "instance Num NPlusK is only partially defined"
+  abs    = error "instance Num NPlusK is only partially defined"
+  signum = error "instance Num NPlusK is only partially defined"
+-- TODO: correctly deal with NPlusK pattern with identifier abbreviation.
+
+instance Field1 NPlusK NPlusK IdentName IdentName where
+  _1 = lens (\(NPlusK x _) -> x) (\(NPlusK _ y) x -> NPlusK x y)
+instance Field2 NPlusK NPlusK Rational Rational where
+  _2 = lens (\(NPlusK _ y) -> y) (\(NPlusK x _) y -> NPlusK x y)
+
+type TypeExprF = Sum '[ TopTypeF, GridTypeF, TupleF, VectorTypeF, FunTypeF , ElemTypeF ]
+type TypeExpr  = Fix TypeExprF
+
+type LExprF = Sum '[ GridF, TupleF, VectorF, IdentF ]
+type LExpr  = Fix LExprF
+
+type RExprF = Sum '[ LetF, LambdaF, ApplyF, GridF, TupleF, OperatorF, IdentF, ImmF ]
+type RExpr  = Fix RExprF
+
+data SpecialDeclaration = DimensionDeclaration Int
+                        | AxesDeclaration [IdentName]
+             deriving (Eq, Ord, Show)
+
+data Program = Program
+               { _programSpecialDeclarations :: [SpecialDeclaration]
+               , _programBinding :: BindingF RExpr}
+             deriving (Eq, Ord, Show)
+makeLenses ''Program
+
+instance MeetSemiLattice TypeExpr where
+  (/\) = semiLatticeOfTypeExpr
+
+semiLatticeOfTypeExpr :: TypeExpr -> TypeExpr -> TypeExpr
+semiLatticeOfTypeExpr a b = case go a b of
+  TopType -> go b a
+  c       -> c
+  where
+    go :: TypeExpr -> TypeExpr -> TypeExpr
+    go a b | a == b = a
+    go a@(ElemType _) b@(GridType v c) = let d = a/\c in if d==TopType then TopType else GridType v d
+    go (GridType v1 c1) (GridType v2 c2) = if v1 == v2 then GridType v1 (c1 /\ c2) else TopType
+    go _ _          = TopType
diff --git a/src/Formura/Type.hs b/src/Formura/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Formura/Type.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE DataKinds, FlexibleInstances, TypeSynonymInstances #-}
+module Formura.Type where
+
+import Algebra.Lattice
+import Data.Tuple(swap)
+
+import Formura.Language.Combinator
+import Formura.Syntax
+
+
+type ElementalType = Lang '[TopTypeF, ElemTypeF]
+
+instance MeetSemiLattice ElementalType where
+  (ElemType ea) /\ (ElemType eb) =
+    case elementTypenameDecode(max (elementTypenameEncode ea) (elementTypenameEncode eb)) of
+     "top" -> TopType
+     str   -> ElemType str
+  _ /\ _ = TopType
+
+elementTypenameTable :: [(String,Int)]
+elementTypenameTable =
+      [("Rational", 0)
+      ,("float", 1)
+      ,("double", 2)
+      ,("real", 3)
+      ,("Real", 4)]
+
+
+elementTypenameEncode :: String -> Int
+elementTypenameEncode str = case lookup str elementTypenameTable of
+  Just i -> i
+  Nothing -> maxBound
+
+
+
+elementTypenameDecode :: Int -> String
+elementTypenameDecode i = case lookup i (map swap elementTypenameTable) of
+  Just n -> n
+  Nothing -> "top"
diff --git a/src/Formura/Vec.hs b/src/Formura/Vec.hs
new file mode 100644
--- /dev/null
+++ b/src/Formura/Vec.hs
@@ -0,0 +1,70 @@
+{- |
+Copyright   : (c) Takayuki Muranushi, 2015
+License     : MIT
+Maintainer  : muranushi@gmail.com
+Stability   : experimental
+
+ZipList treated as mathematical vectors, to deal with multidimensionality in stencil computation.
+-}
+
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, TypeFamilies #-}
+
+module Formura.Vec where
+
+import Control.Applicative
+import Control.Lens
+import Data.Monoid
+
+data Vec a = Vec { getVec :: [a] } | PureVec a
+           deriving (Functor, Foldable, Traversable)
+
+
+type instance Index (Vec a) = Int
+type instance IxValue (Vec a) = a
+instance Ixed (Vec a) where
+  ix i =
+       let myIso :: Iso' (Vec a) [a]
+           myIso = iso back Vec
+
+           back (PureVec x) = repeat x
+           back (Vec xs) = xs
+       in myIso . ix i
+
+instance Show a => Show (Vec a) where
+  show (Vec xs) = show xs
+  show (PureVec x) = "[" ++ show x ++ "..]"
+
+-- | Equality of vector requires the knowledge of how to zero-fill
+instance (Num a, Eq a) => Eq (Vec a) where
+  a == b = and $ liftVec2 (==) a b
+
+instance (Num a, Ord a) => Ord (Vec a) where
+  compare a b = foldr (<>) EQ $ liftVec2 compare a b
+
+instance Applicative Vec where
+    pure x = PureVec x
+    PureVec f <*> PureVec x = PureVec $ f x
+    PureVec f <*> Vec xs    = Vec $ fmap f xs
+    Vec fs <*> PureVec x    = Vec $ fmap ($x) fs
+    Vec fs <*> Vec xs = Vec (zipWith id fs xs)
+
+instance Num a => Num (Vec a) where
+  (+) = liftVec2 (+)
+  (-) = liftVec2 (-)
+  (*) = liftVec2 (*)
+  abs   = fmap abs
+  signum = fmap signum
+  negate = fmap negate
+  fromInteger = pure . fromInteger
+
+instance Fractional a => Fractional (Vec a) where
+  (/) = liftVec2 (/)
+  recip = fmap recip
+  fromRational = pure .fromRational
+
+liftVec2 :: (Num a, Num b) => (a -> b -> c) -> Vec a -> Vec b -> Vec c
+liftVec2 f (PureVec x) (PureVec y) = PureVec $ f x y
+liftVec2 f (PureVec x) (Vec ys   ) = Vec $ fmap (f x) ys
+liftVec2 f (Vec xs   ) (PureVec y) = Vec $ fmap (flip f y) xs
+liftVec2 f (Vec xs   ) (Vec ys   ) = let n = max (length xs) (length ys) in
+  Vec $ take n $ zipWith f (xs ++ repeat 0) (ys ++ repeat 0)