0
|
1 |
(* Title: Pure/Syntax/ROOT
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
|
|
4 |
|
|
5 |
This file builds the syntax module. It assumes the standard Isabelle
|
|
6 |
environment.
|
|
7 |
*)
|
|
8 |
|
|
9 |
use "ast.ML";
|
|
10 |
use "xgram.ML";
|
|
11 |
use "extension.ML";
|
|
12 |
use "lexicon.ML";
|
|
13 |
use "parse_tree.ML";
|
|
14 |
use "earley0A.ML";
|
|
15 |
use "type_ext.ML";
|
|
16 |
use "sextension.ML";
|
|
17 |
use "pretty.ML";
|
|
18 |
use "printer.ML";
|
|
19 |
use "syntax.ML";
|
|
20 |
|
|
21 |
structure Ast = AstFun();
|
|
22 |
structure XGram = XGramFun(Ast);
|
|
23 |
structure Extension = ExtensionFun(XGram);
|
|
24 |
structure Lexicon = LexiconFun(Extension);
|
|
25 |
structure ParseTree = ParseTreeFun(structure Lexicon = Lexicon and Ast = Ast);
|
|
26 |
structure Earley = EarleyFun(structure XGram = XGram and ParseTree = ParseTree);
|
|
27 |
structure TypeExt = TypeExtFun(structure Extension = Extension
|
|
28 |
and Lexicon = Lexicon);
|
|
29 |
structure SExtension = SExtensionFun(structure TypeExt = TypeExt
|
|
30 |
and Lexicon = Lexicon);
|
|
31 |
structure Pretty = PrettyFun();
|
|
32 |
structure Printer = PrinterFun(structure Symtab = Symtab and Lexicon = Lexicon
|
|
33 |
and TypeExt = TypeExt and SExtension = SExtension and Pretty = Pretty);
|
|
34 |
structure Syntax = SyntaxFun(structure Symtab = Symtab and TypeExt = TypeExt
|
|
35 |
and Parser = Earley and SExtension = SExtension and Printer = Printer);
|
|
36 |
|
|
37 |
(*Basic_Syntax has the most important primitives, which are made pervasive*)
|
|
38 |
signature BASIC_SYNTAX = sig include SEXTENSION0 include PRINTER0 end;
|
|
39 |
structure Basic_Syntax: BASIC_SYNTAX = Syntax;
|
|
40 |
|