|
Ivor.TermParser | Portability | non-portable | Stability | experimental | Maintainer | eb@dcs.st-and.ac.uk |
|
|
|
Description |
Extensible Parsec based parsing library for ViewTerms.
Briefly, the syntax is as follows:
- [x:A]y -- Lambda binding with scope y.
- (x:A) -> B -- Forall binding with scope B (-> optional).
- A -> B -- Forall binding where name bound is not used in B..
- let x:A=v in y -- Let binding, x=v in scope y.
- f a -- Function application (left associative, by juxtaposition).
- [identifier] -- names are legal Haskell identifiers.
- * -- Asterisk is type of types.
- _ -- Underscore is a placeholder.
- ?identifier -- metavariable, add a name to be defined later
Lambda/forall bindings of multiple variables are also accepted,
in the form [x,y:A;z:B]
Staging annotations have the following syntax:
- {'x} -- quoted term x
- {{A}} -- code type A (if x:A, {'x}:{{A}}
- !x -- evaluate a quoted term
- ~x -- escape a quoted term (i.e. splice into a quoted term)
Extensions for labelled types (see McBride/McKinna "The View
From The Left" for details):
- <[identifier] args : t> -- Labelled type.
- call <label> term -- Call a computation.
- return t -- Return a value from a computation.
|
|
Synopsis |
|
|
|
Documentation |
|
|
:: Maybe (Parser ViewTerm) | Extra parse rules (for example
for any primitive types or operators you might have added).
| -> Parser ViewTerm | | Basic parsec combinator for parsing terms.
|
|
|
|
Parse a term which is not an application;
use for parsing lists of terms.
|
|
|
:: Maybe (Parser ViewTerm) | Extra parse rules (for example
for any primitive types or operators you might have added).
| -> Parser Inductive | | Basic parsec combinator for parsing inductive data types
|
|
|
|
Parse a string into a ViewTerm, without mucking about with parsec
or any extra parse rules.
|
|
|
Parse a string into an Inductive, without mucking about with parsec
or any extra parse rules.
|
|
Produced by Haddock version 2.6.0 |