Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
--- a/src/Pure/Syntax/ROOT.ML Fri Feb 16 13:55:29 1996 +0100
+++ b/src/Pure/Syntax/ROOT.ML Fri Feb 16 14:06:09 1996 +0100
@@ -16,39 +16,8 @@
use "printer.ML";
use "syntax.ML";
-structure PrivateSyntax =
-struct
- structure Pretty = PrettyFun();
- structure Lexicon = LexiconFun();
- structure Scanner: SCANNER = Lexicon;
- structure Ast = AstFun(Pretty);
- structure SynExt = SynExtFun(structure Lexicon = Lexicon and Ast = Ast);
- structure Parser = ParserFun(structure Symtab = Symtab and Lexicon = Lexicon
- and SynExt = SynExt);
- structure TypeExt = TypeExtFun(structure Lexicon = Lexicon and SynExt = SynExt);
- structure SynTrans = SynTransFun(structure TypeExt = TypeExt and Parser = Parser);
- structure Mixfix = MixfixFun(structure Lexicon = Lexicon and SynExt = SynExt and
- SynTrans = SynTrans);
- structure Printer = PrinterFun(structure Symtab = Symtab and TypeExt = TypeExt
- and SynTrans = SynTrans);
- structure Syntax = SyntaxFun(structure Symtab = Symtab and TypeExt = TypeExt
- and SynTrans = SynTrans and Mixfix = Mixfix and Printer = Printer);
- structure BasicSyntax: BASIC_SYNTAX = Syntax;
-end;
+(*Hiding: only the most basic features are opened*)
+structure BasicSyntax: BASIC_SYNTAX = Syntax;
+open BasicSyntax;
-structure Pretty = PrivateSyntax.Pretty;
-structure Scanner = PrivateSyntax.Scanner;
-structure Syntax = PrivateSyntax.Syntax;
-structure BasicSyntax = PrivateSyntax.BasicSyntax;
-
-(* hide functors; saves space in PolyML *)
-functor PrettyFun() = struct end;
-functor LexiconFun() = struct end;
-functor AstFun() = struct end;
-functor SynExtFun() = struct end;
-functor ParserFun() = struct end;
-functor TypeExtFun() = struct end;
-functor SynTransFun() = struct end;
-functor MixfixFun() = struct end;
-functor PrinterFun() = struct end;
-functor SyntaxFun() = struct end;
+structure Scanner: SCANNER = Lexicon;
--- a/src/Pure/Syntax/ast.ML Fri Feb 16 13:55:29 1996 +0100
+++ b/src/Pure/Syntax/ast.ML Fri Feb 16 14:06:09 1996 +0100
@@ -6,18 +6,17 @@
*)
signature AST0 =
-sig
+ sig
datatype ast =
Constant of string |
Variable of string |
Appl of ast list
exception AST of string * ast list
-end;
+ end;
signature AST1 =
-sig
+ sig
include AST0
- structure Pretty: PRETTY
val mk_appl: ast -> ast list -> ast
val str_of_ast: ast -> string
val pretty_ast: ast -> Pretty.T
@@ -25,10 +24,10 @@
val pprint_ast: ast -> pprint_args -> unit
val trace_norm_ast: bool ref
val stat_norm_ast: bool ref
-end;
+ end;
signature AST =
-sig
+ sig
include AST1
val raise_ast: string -> ast list -> 'a
val head_of_rule: ast * ast -> string
@@ -39,14 +38,11 @@
val unfold_ast_p: string -> ast -> ast list * ast
val normalize: bool -> bool -> (string -> (ast * ast) list) option -> ast -> ast
val normalize_ast: (string -> (ast * ast) list) option -> ast -> ast
-end;
+ end;
-functor AstFun(Pretty: PRETTY): AST =
+structure Ast : AST =
struct
-structure Pretty = Pretty;
-
-
(** abstract syntax trees **)
(*asts come in two flavours:
@@ -293,5 +289,5 @@
fun normalize_ast get_rules ast =
normalize (! trace_norm_ast) (! stat_norm_ast) get_rules ast;
+end;
-end;