src/Pure/Syntax/ROOT.ML
author wenzelm
Mon, 29 Nov 1993 12:25:15 +0100
changeset 163 ad90d96c2ec3
parent 47 0af9dbb93529
child 239 08b6e842ec16
permissions -rw-r--r--
added Scanner;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     1
(*  Title:      Pure/Syntax/ROOT.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     5
This file builds the syntax module.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     8
use "pretty.ML";
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     9
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
use "ast.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
use "xgram.ML";
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    12
use "lexicon.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
use "extension.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
use "parse_tree.ML";
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    15
use "parser.ML";
47
0af9dbb93529 *** empty log message ***
wenzelm
parents: 42
diff changeset
    16
use "earley0A.ML";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
use "type_ext.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
use "sextension.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
use "printer.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
use "syntax.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    22
structure Pretty = PrettyFun();
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    23
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    24
structure Ast = AstFun(Pretty);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
structure XGram = XGramFun(Ast);
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    26
structure Lexicon = LexiconFun();
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    27
structure Extension = ExtensionFun(structure XGram = XGram and Lexicon = Lexicon);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    28
structure ParseTree = ParseTreeFun(structure Ast = Ast and Lexicon = Lexicon);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    29
structure Parser = ParserFun(structure Symtab = Symtab and XGram = XGram
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    30
  and ParseTree = ParseTree);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    31
structure Earley = EarleyFun(structure Symtab = Symtab and XGram = XGram
47
0af9dbb93529 *** empty log message ***
wenzelm
parents: 42
diff changeset
    32
  and ParseTree = ParseTree);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
structure TypeExt = TypeExtFun(structure Extension = Extension
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  and Lexicon = Lexicon);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
structure SExtension = SExtensionFun(structure TypeExt = TypeExt
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  and Lexicon = Lexicon);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
structure Printer = PrinterFun(structure Symtab = Symtab and Lexicon = Lexicon
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  and TypeExt = TypeExt and SExtension = SExtension and Pretty = Pretty);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
structure Syntax = SyntaxFun(structure Symtab = Symtab and TypeExt = TypeExt
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
  and Parser = Earley and SExtension = SExtension and Printer = Printer);
47
0af9dbb93529 *** empty log message ***
wenzelm
parents: 42
diff changeset
    41
163
ad90d96c2ec3 added Scanner;
wenzelm
parents: 47
diff changeset
    42
structure Scanner: SCANNER = Lexicon;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    44
(*BasicSyntax has the most important primitives, which are made pervasive*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
signature BASIC_SYNTAX = sig include SEXTENSION0 include PRINTER0 end;
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
    46
structure BasicSyntax: BASIC_SYNTAX = Syntax;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47