Document type Definition

The file $instantiation/src/DocumentTypeDefinition.prx (.prx stands for Proxima) contains the abstract datatype definitions for the Proxima instantiation. At least two types need to be defined: the document (Document) and the enriched document (EnrichedDoc). The Proxima generator generates the actual Haskell and AG data type declarations for the document and the enriched document from this definition, as well as the generic document editing code and several utility functions.

The data type definitions are similar to monomorphic Haskell data types, but can contain named fields by prefixing the field with the name and a colon. A field may be either a Proxima type, or a monomorphic Haskell type, such as Int, or Bool.

An example definition looks like this:

data SomeDataType = ConA namea:A nameb:B C C
                  | ConB

In this example, SomeDataType has two constructors (ConA and ConB), and has two explicitly named fields (namea, nameb). The other fields are implicitly named, by taking the type name with the first letter in lower case, and appending an index: c0 and c1.

Each constructor may also specify how many tokens are used in its presentation, by declaring IDP fields between braces. In a future release this may be inferred from the presentation sheet, but for now it has to be specified by hand. An example:

data Exp = PlusExp exp1:Exp exp2:Exp { idP0:IDP }
         | LetExp [Decl] Exp         { idP0:IDP, idP1:IDP }
         | IntExp Int                                    { idP0:IDP }
         | ...

Here, the PlusExp specifies that it has one token in its presentation (".. + .."), just as the IntExp (for the integer), and the LetExp has two ("let .. in .."). It is also possible to declare a list of IDP's, by using this syntax: "{ idps:[IDP] }".

Additional Haskell datatypes may be defined at the top of the generated module $instantiation/src/DocTypes_Generated.hs. These types can be used in the Proxima type declarations.

Generator adds list conslist nil, as well as hole and parseerror

Generated constructors

The genererator automatically adds two constructors to each type:

data <Type> = ...
               | Hole<Type>
               | ParseErr<Type> (ParseError Document EnrichedDoc Node ClipDoc UserToken)

The first one, Hole represents a hole in the document structure, and is used during structure editing (i.e. document-oriented editing) of the document. The second one represents a parse error, and is only used when the type appears at the root of a parsing presentation. The presentation rules for both elements are also generated automatically.

Lists

When a list is used in the document type definition, the generated generates an explicit monomorphic list datatype for it. Thus, if [Type] appears in a declaration, the following types are generated:

data List_<Type> = List_<Type>  elts : ConsList_<Type>
                | HoleList_<Type>
                | ParseErrList_<Type> (ParseError Document EnrichedDoc Node ClipDoc UserToken)

data ConsList_Thing = Cons_<Type> head : <Type> tail : ConsList_<Type>
                    | Nil_<Type>

Each list has List_ as its root. It can be used to specify a presentation rule for the list as a whole, or perform a special attribute computation at the root of the list (which can be awkward on a mere conslist). The second type is the actual conslist for .

-- Main.GerboEngels - 14/22 Feb 2008