welcome: please sign in

Diff for "DomTool/LanguageReference"

Differences between revisions 2 and 3
Revision 2 as of 2006-12-17 16:59:10
Size: 2879
Editor: AdamChlipala
Comment: Types
Revision 3 as of 2006-12-17 17:18:17
Size: 4706
Editor: AdamChlipala
Comment: Expressions
Deletions are marked like this. Additions are marked like this.
Line 14: Line 14:
|| `Int` || Integer constant ||
|| `String` || String constant (enclosed in double quotes) ||
Line 44: Line 46:

= Expressions =

Here is the grammar of expressions `E`. As is standard in ML-family languages and Haskell, juxtaposition is used to represent function application, with application associating to the left.

|| '''Syntax''' || '''Description''' || '''Typing''' ||
|| `Int` || Integer constant || `G |- Int : int` ||
|| `String` || String constant || `G |- String : string` ||
|| `[E1, ..., EN]` || List || If `G |- Ei : T` for each `Ei`, then `G |- [E1, ..., EN] : [T]`. ||
|| `Symbol` || Variable || `G1, Symbol : T, G2 |- Symbol : T`. ||
|| `E1 E2` || Application || If `G |- E1 : T1 -> T2` and `G |- E2 : T1`, then `G |- E1 E2 : T2`. ||
|| `\ Symbol -> E` || Abstraction (inferred domain type) || If `G, Symbol : T1 |- E : T2`, then `G |- \ Symbol -> E : T1 -> T2`. ||
|| `\ Symbol : (T1) -> E` || Abstraction (explicit domain type) || If `G, Symbol : T1 |- E : T2`, then `G |- \ Symbol : (T1) -> E : T1 -> T2`. ||
|| `CSymbol = E` || Environment variable set || See subsection on actions ||
|| `Symbol <- CSymbol; E` || Environment variable get || See subsection on actions ||
|| `E1; E2` || Sequencing || See subsection on actions ||
|| `E1 where E2 end` || Local bindings || See subsection on actions ||
|| `let E1 in E2 end` || Local bindings || See subsection on actions ||
|| `E1 with E2 end` || Nested action || See subsection on actions ||
|| `E1 with end` || Empty nested action || See subsection on actions ||
|| `E1 where E2 with E3 end` || Nested action with local bindings || See subsection on actions ||
|| `E1 where E2 with end` || Empty nested action with local bindings || See subsection on actions ||
|| `\\ Symbol : P -> E` || Nested action abstraction || See subsection on actions ||

This page gives an in-depth specification of the DomTool language. Most members would probably prefer the more informal presentation in DomTool/UserGuide.

TableOfContents()

1. Source code

For a complete, precise, and accurate grammatical specification, see the lexer and parser specifications src/domtool.lex and src/domtool.grm in the DomTool source code. See src/tycheck.sml for the type-checker implementation. ["DomTool/Building"] has information on obtaining the source.

2. Token conventions

In the grammars that follow, we use these lexical token class names:

Name

Description

Int

Integer constant

String

String constant (enclosed in double quotes)

Symbol

Identifier starting with a lowercase letter

CSymbol

Identifier starting with a capital letter

3. Predicates

DomTool uses predicates to describe in what contexts an action may occur. For instance, web-related actions should only occur inside the scope of a virtual host directive. Predicates are built up following the grammar in the table below, using the letter P as the non-terminal for predicates.

Meanings are given as statements that must hold about the context where an action is found. The context is represented as a stack of context IDs which have been declared with context declarations.

Syntax

Description

Meaning

Root

Root

The stack is empty.

CSymbol

Context ID

CSymbol is on the top of the stack.

^P

Suffixes

Some (not necessarily strict) suffix of the stack matches P.

!P

Not

The stack doesn't match P.

P1 & P2

And

The stack matches both P1 and P2.

(P)

Grouping

Identical to P

4. Types

Types describe expressions. As is standard in statically-typed programming languages, they are used only for validation purposes and have no real effect on the "output" of a program. The following table gives the grammar of types T. The section on expressions will give the meanings of types in terms of which expressions have which types.

Syntax

Description

Symbol

Extern type

[T]

List of Ts

T1 -> T2

Function from T1 to T2

[P]

Action allowed only when P is satisified; requires no environment variables on input and writes none of its own

[P] {CSymbol1 : T1, ..., CSymbolN : TN}

Action that requires environment variables CSymbol1, ..., CSymbolN to have the given types when run

[P] {CSymbol1_1 : T1_1, ..., CSymbol1_N : T1_N} => {CSymbol2_1 : T2_1, ..., CSymbol2_M : T2_M}

Like the last case, but the second set of typed environment variables describes what the action will write

P => T

A nested action that requires that its nested configuration satisfy P; T should be some action type

(T)

Grouping

5. Expressions

Here is the grammar of expressions E. As is standard in ML-family languages and Haskell, juxtaposition is used to represent function application, with application associating to the left.

Syntax

Description

Typing

Int

Integer constant

G |- Int : int

String

String constant

G |- String : string

[E1, ..., EN]

List

If G |- Ei : T for each Ei, then G |- [E1, ..., EN] : [T].

Symbol

Variable

G1, Symbol : T, G2 |- Symbol : T.

E1 E2

Application

If G |- E1 : T1 -> T2 and G |- E2 : T1, then G |- E1 E2 : T2.

\ Symbol -> E

Abstraction (inferred domain type)

If G, Symbol : T1 |- E : T2, then G |- \ Symbol -> E : T1 -> T2.

\ Symbol : (T1) -> E

Abstraction (explicit domain type)

If G, Symbol : T1 |- E : T2, then G |- \ Symbol : (T1) -> E : T1 -> T2.

CSymbol = E

Environment variable set

See subsection on actions

Symbol <- CSymbol; E

Environment variable get

See subsection on actions

E1; E2

Sequencing

See subsection on actions

E1 where E2 end

Local bindings

See subsection on actions

let E1 in E2 end

Local bindings

See subsection on actions

E1 with E2 end

Nested action

See subsection on actions

E1 with end

Empty nested action

See subsection on actions

E1 where E2 with E3 end

Nested action with local bindings

See subsection on actions

E1 where E2 with end

Empty nested action with local bindings

See subsection on actions

\\ Symbol : P -> E

Nested action abstraction

See subsection on actions

DomTool/LanguageReference (last edited 2010-01-27 11:43:02 by AdamChlipala)