# HG changeset patch # User wenzelm # Date 758985798 -3600 # Node ID 08b6e842ec161d6ceb5fed0ffb66e5ae91b5939a # Parent 6af40e3a2bcbeef66f5c04db7ee96dffd9b7b428 minor internal changes; diff -r 6af40e3a2bcb -r 08b6e842ec16 src/Pure/Syntax/ROOT.ML --- a/src/Pure/Syntax/ROOT.ML Wed Jan 19 14:22:37 1994 +0100 +++ b/src/Pure/Syntax/ROOT.ML Wed Jan 19 14:23:18 1994 +0100 @@ -6,12 +6,9 @@ *) use "pretty.ML"; - +use "lexicon.ML"; use "ast.ML"; -use "xgram.ML"; -use "lexicon.ML"; -use "extension.ML"; -use "parse_tree.ML"; +use "syn_ext.ML"; use "parser.ML"; use "earley0A.ML"; use "type_ext.ML"; @@ -20,26 +17,20 @@ use "syntax.ML"; structure Pretty = PrettyFun(); - +structure Lexicon = LexiconFun(); +structure Scanner: SCANNER = Lexicon; structure Ast = AstFun(Pretty); -structure XGram = XGramFun(Ast); -structure Lexicon = LexiconFun(); -structure Extension = ExtensionFun(structure XGram = XGram and Lexicon = Lexicon); -structure ParseTree = ParseTreeFun(structure Ast = Ast and Lexicon = Lexicon); -structure Parser = ParserFun(structure Symtab = Symtab and XGram = XGram - and ParseTree = ParseTree); -structure Earley = EarleyFun(structure Symtab = Symtab and XGram = XGram - and ParseTree = ParseTree); -structure TypeExt = TypeExtFun(structure Extension = Extension - and Lexicon = Lexicon); -structure SExtension = SExtensionFun(structure TypeExt = TypeExt - and Lexicon = Lexicon); -structure Printer = PrinterFun(structure Symtab = Symtab and Lexicon = Lexicon - and TypeExt = TypeExt and SExtension = SExtension and Pretty = Pretty); +structure SynExt = SynExtFun(structure Lexicon = Lexicon and Ast = Ast); +structure Parser = ParserFun(structure Symtab = Symtab and Lexicon = Lexicon + and SynExt = SynExt); +structure Earley = EarleyFun(structure Symtab = Symtab and Lexicon = Lexicon + and SynExt = SynExt); +structure TypeExt = TypeExtFun(structure Lexicon = Lexicon and SynExt = SynExt); +structure SExtension = SExtensionFun(Earley); +structure Printer = PrinterFun(structure Symtab = Symtab and TypeExt = TypeExt + and SExtension = SExtension); structure Syntax = SyntaxFun(structure Symtab = Symtab and TypeExt = TypeExt - and Parser = Earley and SExtension = SExtension and Printer = Printer); - -structure Scanner: SCANNER = Lexicon; + and SExtension = SExtension and Printer = Printer); (*BasicSyntax has the most important primitives, which are made pervasive*) signature BASIC_SYNTAX = sig include SEXTENSION0 include PRINTER0 end; diff -r 6af40e3a2bcb -r 08b6e842ec16 src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Wed Jan 19 14:22:37 1994 +0100 +++ b/src/Pure/Syntax/type_ext.ML Wed Jan 19 14:23:18 1994 +0100 @@ -6,7 +6,7 @@ TODO: term_of_typ: prune sorts - move "_K" (?) + move "_K", "_explode", "_implode" *) signature TYPE_EXT0 = @@ -17,19 +17,19 @@ signature TYPE_EXT = sig include TYPE_EXT0 - structure Extension: EXTENSION - local open Extension Extension.XGram.Ast in + structure SynExt: SYN_EXT + local open SynExt SynExt.Ast in val term_of_typ: bool -> typ -> term val tappl_ast_tr': ast * ast list -> ast - val type_ext: ext + val type_ext: syn_ext end end; -functor TypeExtFun(structure Extension: EXTENSION and Lexicon: LEXICON): TYPE_EXT = +functor TypeExtFun(structure Lexicon: LEXICON and SynExt: SYN_EXT): TYPE_EXT = struct -structure Extension = Extension; -open Extension Extension.XGram Extension.XGram.Ast Lexicon; +structure SynExt = SynExt; +open Lexicon SynExt SynExt.Ast; (** typ_of_term **) @@ -170,32 +170,30 @@ val classesT = Type ("classes", []); val typesT = Type ("types", []); -val type_ext = - Ext { - roots = [logic, "type"], - mfix = [ - Mfix ("_", tfreeT --> typeT, "", [], max_pri), - Mfix ("_", tvarT --> typeT, "", [], max_pri), - Mfix ("_", idT --> typeT, "", [], max_pri), - Mfix ("_::_", [tfreeT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), - Mfix ("_::_", [tvarT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), - Mfix ("_", idT --> sortT, "", [], max_pri), - Mfix ("{}", sortT, "_emptysort", [], max_pri), - Mfix ("{_}", classesT --> sortT, "_sort", [], max_pri), - Mfix ("_", idT --> classesT, "", [], max_pri), - Mfix ("_,_", [idT, classesT] ---> classesT, "_classes", [], max_pri), - Mfix ("_ _", [typeT, idT] ---> typeT, "_tapp", [max_pri, 0], max_pri), (* FIXME ambiguous *) - Mfix ("((1'(_'))_)", [typesT, idT] ---> typeT, "_tappl", [], max_pri), (* FIXME ambiguous *) - Mfix ("_", typeT --> typesT, "", [], max_pri), - Mfix ("_,/ _", [typeT, typesT] ---> typesT, "_types", [], max_pri), - Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "fun", [1, 0], 0), - Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT, "_bracket", [0, 0], 0)], - extra_consts = ["_K"], - parse_ast_translation = [("_tapp", tappl_ast_tr), ("_tappl", tappl_ast_tr), - ("_bracket", bracket_ast_tr)], - parse_translation = [], - print_translation = [], - print_ast_translation = [("fun", fun_ast_tr')]}; +val type_ext = syn_ext + [logic, "type"] + [Mfix ("_", tfreeT --> typeT, "", [], max_pri), + Mfix ("_", tvarT --> typeT, "", [], max_pri), + Mfix ("_", idT --> typeT, "", [], max_pri), + Mfix ("_::_", [tfreeT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), + Mfix ("_::_", [tvarT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri), + Mfix ("_", idT --> sortT, "", [], max_pri), + Mfix ("{}", sortT, "_emptysort", [], max_pri), + Mfix ("{_}", classesT --> sortT, "_sort", [], max_pri), + Mfix ("_", idT --> classesT, "", [], max_pri), + Mfix ("_,_", [idT, classesT] ---> classesT, "_classes", [], max_pri), + Mfix ("_ _", [typeT, idT] ---> typeT, "_tapp", [max_pri, 0], max_pri), (* FIXME ambiguous *) + Mfix ("((1'(_'))_)", [typesT, idT] ---> typeT, "_tappl", [], max_pri), (* FIXME ambiguous *) + Mfix ("_", typeT --> typesT, "", [], max_pri), + Mfix ("_,/ _", [typeT, typesT] ---> typesT, "_types", [], max_pri), + Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "fun", [1, 0], 0), + Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT, "_bracket", [0, 0], 0)] + ["_K", "_explode", "_implode"] + ([("_tapp", tappl_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)], + [], + [], + [("fun", fun_ast_tr')]) + ([], []); end;