ivor-0.1.9: Theorem proving library based on dependent type theorySource codeContentsIndex
Ivor.TermParser
Portabilitynon-portable
Stabilityexperimental
Maintainereb@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
pTerm :: Maybe (Parser ViewTerm) -> Parser ViewTerm
pNoApp :: Maybe (Parser ViewTerm) -> Parser ViewTerm
pInductive :: Maybe (Parser ViewTerm) -> Parser Inductive
parseTermString :: Monad m => String -> m ViewTerm
parseDataString :: Monad m => String -> m Inductive
Documentation
pTermSource
:: 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.
pNoApp :: Maybe (Parser ViewTerm) -> Parser ViewTermSource
Parse a term which is not an application; use for parsing lists of terms.
pInductiveSource
:: 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
parseTermString :: Monad m => String -> m ViewTermSource
Parse a string into a ViewTerm, without mucking about with parsec or any extra parse rules.
parseDataString :: Monad m => String -> m InductiveSource
Parse a string into an Inductive, without mucking about with parsec or any extra parse rules.
Produced by Haddock version 2.4.2