X-Logic tools in Standard ML.
Overview
This document covers a collection of X-Logic tools in sml which are independent of the various proof tools implemented in sml.
This document covers a collection of X-Logic tools in sml which are independent of the various proof tools implemented in sml.
Two datatypes for representing XML documents (Fat and Lean) and a function for throwing away the fat.
Procedures for invoking the fxp XML parser to create a data structure (parse tree) for further processing.
Procedures for driving collections of "hooks" from fat or lean datatype representations of XML documents, primarily intended to support writing XML documents to files.
Wrappers for the Unicode decode and encode facilities provided in the fxp parser library to package these in ways which are convenient for X-Logic.
Singatures for state and exception monads, and an input stream monad, with an implementation of an input stream monad with exception handling.
Arrows which can be constructed from Monads using a Kleisli functor.
This document covers a collection of X-Logic tools in sml which are independent of the various proof tools implemented in sml.
Introduction
X-Logic X-ification Tools
This document covers a collection of X-Logic tools in sml which are independent of the various proof tools implemented in sml.
Miscellany
This is place for small bits of SML required by the rest of the tools for which I have not yet found a better home.
CM File
A CM file is provided for building the X-Logic tools as a library under SML/NJ.
XML Data
Two datatypes for representing XML documents (Fat and Lean) and a function for throwing away the fat.
Introduction
This document datatypes for representing XML parse trees using the fxp xml parser.
The Fat Datatype
A datatype of parse trees naively based on the HookData structure in fxp "Parser/Params/hookData.sml".
The Lean Datatype
The lean datatype is for use in semantic applications where details of presentation of the XML document need not be preserved.
Slimming
A function to throw away the fat.
XML Input
Procedures for invoking the fxp XML parser to create a data structure (parse tree) for further processing.
Introduction
Parser Hooks
This is a set of Hooks for constructing a full parse tree.
Parsing
This is the procedure to invoke the fxp parser with the XmlParseHooks to construct the parse tree. It is derived from the fxp "null" parser ("Apps/Null/null.sml").
XML Output
Procedures for driving collections of "hooks" from fat or lean datatype representations of XML documents, primarily intended to support writing XML documents to files.
Introduction
This document provides facilities for output of XML documents using the fxp library.
Driving Fat Hooks
The following functor provides a driver for a set of Hooks. This allows the Hooks to be driven from a parse tree as if the parser were driving the hooks when it originally parsed the file.
Full XML Output
This structure provides a function which writes to a file the XML generated from a FatTree. It is based on the fxp program "Copy" and uses the copyHooks verabatim.
Lean Hooks
The following functor provides a signature for a set of hooks which match the lean parse tree.
Driving Lean Hooks
The following functor provides a driver for a set of Hooks. This allows the Hooks to be driven from a parse tree as if the parser were driving the hooks when it originally parsed the file.
Unicode IO
Wrappers for the Unicode decode and encode facilities provided in the fxp parser library to package these in ways which are convenient for X-Logic.
Introduction
A few words on the fxp facilities and how they are adapted for X-Logic.
Input
Output
Basic Monads
Singatures for state and exception monads, and an input stream monad, with an implementation of an input stream monad with exception handling.
Introduction
Monads for conversion to arrows.
Basic Monad
The basic monad does nothing behind the scenes, no side effects or exceptions.
State Monad
A state monad represents computations with possible side effects involving reading and/or writing to a state.
Exception Monad
An exception monad provides for raising and handling exceptions.
InStream Monad
An "InStream" monad is one which reads an input stream as a side effect.
Kleisli Arrows
Arrows which can be constructed from Monads using a Kleisli functor.
Introduction
The Arrow Signatures
This tells us what arrows are.
Functors between Monads and Arrows
From any Monad we can construct an Arrow, and we ought to be able to retrieve the original Monad from that Arrow.
Full Arrows
A fuller signature for arrows is defined, with a functor constructing full arrows from primitive arrows.
Combinators
This document covers a collection of X-Logic tools in sml which are independent of the various proof tools implemented in sml.
Introduction
Parse Options
Introduction
Parse Hooks
Introduction
Tree Building
A type for a partially constructed tree representation of an XML document, together with functions which create an empty tree, add things into this tree and finally extract the completed structure.
Parse
Introduction
Strucutre XLParse
A Simple Monadic Parser
Superceeded by the InStream Monad in BasicMonads.xml.
Introduction
Input
Output

up quick index © RBJ

$Id: index.xml,v 1.1.1.1 2000/12/04 17:25:11 rbjones Exp $