\documentclass[11pt]{book}

%include lhs2TeX.fmt
%include polycode.fmt

\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{stmaryrd}
\usepackage{float}
\usepackage{mathpartir}
\usepackage{xcolor}
\usepackage{natbib}
\usepackage[pdftex]{graphicx}

\floatstyle{boxed}
\restylefloat{figure}

\newcommand\TinkerType{TinkerType}
\newcommand\TinkerTypeAssembler{TinkerType Assembler}


\author{Arie Middelkoop}
\title{Related Work}

\begin{document}

\chapter{Related Work}

\section{\TinkerType}

  \TinkerType{}~\cite{DBLP:journals/jfp/LevinP03} is a language for the modular description of whole families of
  formal systems, with focus on type systems and operational semantics. A type
  system is described in two ways: intensional as a set of {\it features}
  (names for some abstract properties of a type system), and intentional as a
  set of {\it clauses} (a denotation of a type rule in the form of \LaTeX{} text
  or ML code).

  \subsection{Overview}

  A \TinkerType{} description consists of a number of elements: features,
  dependencies between features, clauses, a clause refinement relation, and
  feature constraint formulas. With the latter two elements, clause
  refinement and feature constraints, a partial consistency between type systems
  can be expressed.

  Distinct type systems have different clauses. However, type systems with
  similar features tend to have similar clauses. The relation between clauses
  is exploited by \TinkerType. A \TinkerType{} description therefore contains
  a whole repository of named clauses tagged with a number of feature names. There
  can be clauses with the same name but different feature sets. A type
  system supporting a number of features is then assembled by the
  \TinkerTypeAssembler{} by selecting those
  clauses that support these features best. These are all clauses where the
  feature set is a subset of the requested feature set, and duplicates removed
  by, in case of duplicately named clauses, only selecting the clause with the
  largest feature set.

  Features are declared with a dependency relation between them. A type system
  is fully defined by the transitive closure of the dependency relation on the
  set of features of the type system. Some combinations of features give an
  unsound type system or the inference algorithm, assembled from the clauses
  belonging to these features, is incomplete. Certain combinations of features
  can be declared as deficient using feature constraint formulas: propositional
  formulas over features that must be satisfied with the features mapped to
  truth-values based on their presence in the type system. The dependency
  relation between features is one form of such a feature constraint formula,
  in the form of an implication.

  \subsection{Code Assembly}

  The code repository consists of {\it components}, which represents several
  clauses and support code. For example, here is an excerp from a simplified
  ML code component dealing with type checking conditional and boolean
  expressions:
  \begin{verbatim}
  component bool, typing {
    parsing { ... }
    ast { ... }
    core {
      typeof {
        header {# let rec typeof gam t = match t with #}
        separator {#| #}

        T-If
          {#TmIf(e1,e2,e3) ->
            if equiv gam (typeof gam e1} TyBool
            then let res = typeof gam e2 in
              if equiv res (typeof gam e3)
              then res
              else error "arms differ in type"
            else error "guard is not a boolean"#}
  } } }
  \end{verbatim}
  The level of granularity of features is actually per component instead of per
  clause. A component consists of several sections related to parsing, abstract
  syntax tree representation, and the actual typing relations with their
  clauses.

  The assembling process itself is straight-forward. The components matching the
  requested features are merged, and code is produced by outputting the @header@,
  then taking the clauses verbatim separated by the @separator@.

  Consider a component with subtyping @sub@ as additional feature:
  \begin{verbatim}
  component bool, typing, sub {
    core {
      typeof {
        T-If
          {#TmIf(e1,e2,e3) ->
            if [[subtype]] gam (typeof gam e1} TyBool
            then [[join (typeof gam e2) (typeof gam e3)]]
            else error "guard is not a boolean"#}
  } } }
  \end{verbatim}
  In another component with feature @sub@, the functions @subtype@ and @join@ are
  defined, which can thus be used in the above component.

  The refinement relation between clauses is expressed by means of double bracket
  annotations in the source code. The parts inside the double brackets are
  considered new, the part outside the double brackets must occur verbatim in the
  refined clause.

  \subsection{Discussion}

  \TinkerType{} is modular in the sense that all clauses can be written
  seperately, and the system enforces that clauses are designed with reuse of
  concepts in mind. Physical reuse of clauses is limited. A clause can only be
  reused verbatim. In many cases, additional material needs to be added to the
  clause. For example, due to extra judgments or due to extra parameters to the
  judgments when supporting extra features. This leads to code duplication in
  the clauses, with the usual engineering problems as a consequence. The static
  checks on clause refinement, however, are likely to catch errors resulting from
  incomplete code modifications, and encourage writing clauses as increments of
  each other.

  As discussed above, some forms of consistency are expressed between clauses of
  different type systems, which is enforced by means of consistency checks that point
  to errors in the code. To make these checks effective, there must be a lot
  of overlap between clauses, and thus an extensive set of features with a
  fine granularity. Consistency is not expressed between clauses of the same type
  system. There is no guarantee that the collection of clauses results in compilable
  ML code or \LaTeX{} text, nor that the ML code is in any way related to the
  \LaTeX{} text.


\section{Door Attribute Grammars}

  A Door Attribute Grammar~\cite{DBLP:conf/cc/Hedin94} provides programming model
  for remote attributes. It introduces a different kind
  of AST node, called a \emph{door node}. These nodes do not have children, and
  carry not syntactic content. Their sole purpose is to serve as interface to
  attributes of a door node defined elsewhere in the AST. Only the equations of
  a door object may deference attributes of a remote node.
  
  The door nodes restrict programmers to deal with remote attributes separately
  from conventional attributes. This makes explicit what data is exchanged
  between remote locations, and how this data is derived from local data of
  these locations.
  
  Like any mechanism for remote attributes, door nodes provides a convenient
  mechanism to deal with symbol tables. Instead of storing concrete data in
  a symbol table, only a reference to the door node is stored. Data defined
  at a declaration site can then easily be accessed at a definition site.
  
  The author gives an algorithm for Door Attribute Grammars. This algorithm
  maintains a runtime dependency graph between attributes.
  Door nodes gives rise to dependencies to other
  door nodes. During evaluation of equations of door nodes, more dependencies
  arise when remote attributes are dereferenced. Attributes are evaluated on
  demand, in such a way that dependencies are evaluated first. The behavior in
  case of cyclic dependencies is not specified.

\section{Modeling and Specifying Name Visibility and Binding Semantics}

  Visibility networks.
  

\end{document}