equal
deleted
inserted
replaced
|
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 |