# HG changeset patch # User wenzelm # Date 754572762 -3600 # Node ID 128e122acc89e1e582257406d62986530da0e895 # Parent 79e61c182b22c1844be4dc1624ce877580b44a1a added (partial) extend_tables; improved extend; fixed roots handling of extend and merge; diff -r 79e61c182b22 -r 128e122acc89 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Mon Nov 29 12:29:41 1993 +0100 +++ b/src/Pure/Syntax/syntax.ML Mon Nov 29 12:32:42 1993 +0100 @@ -5,10 +5,8 @@ Root of Isabelle's syntax module. TODO: - extend_tables (requires extend_gram) (roots!) - replace add_synrules by extend_tables - extend, merge: make roots handling more robust - extend: use extend_tables + fix empty_tables, extend_tables, mk_tables (requires empty_gram, extend_gram) + fix extend (requires extend_tables) *) signature SYNTAX = @@ -22,7 +20,7 @@ type syntax val type_syn: syntax val extend: syntax -> (string -> typ) -> string list * string list * sext -> syntax - val merge: syntax * syntax -> syntax + val merge: string list -> syntax -> syntax -> syntax val print_gram: syntax -> unit val print_trans: syntax -> unit val print_syntax: syntax -> unit @@ -70,7 +68,7 @@ datatype gramgraph = EmptyGG | - ExtGG of gramgraph ref * (ext * synrules) | + ExtGG of gramgraph ref * ext | MergeGG of gramgraph ref * gramgraph ref; datatype syntax = Syntax of gramgraph ref * tables; @@ -107,8 +105,62 @@ mk_ruletab (flat (map #2 (Symtab.alist_of tab)) @ rules); + +(** tables **) + +(* empty_tables *) + +val empty_tables = + Tabs { + lexicon = empty_lexicon, + roots = [], + (* gram = empty_gram, *) (* FIXME *) + gram = mk_gram [] [], (* FIXME *) + consts = [], + parse_ast_trtab = Symtab.null, + parse_ruletab = Symtab.null, + parse_trtab = Symtab.null, + print_trtab = Symtab.null, + print_ruletab = Symtab.null, + prtab = empty_prtab}; + + +(* extend_tables *) + +fun extend_tables (Tabs tabs) (XGram xgram) = + let + val {lexicon, roots = roots1, gram, consts = consts1, parse_ast_trtab, + parse_ruletab, parse_trtab, print_trtab, print_ruletab, prtab} = tabs; + val {roots = roots2, prods, consts = consts2, parse_ast_translation, + parse_rules, parse_translation, print_translation, print_rules, + print_ast_translation} = xgram; + in + (* FIXME *) + if not (null prods) then + error "extend_tables: called with non-empty prods" + else + + Tabs { + lexicon = extend_lexicon lexicon (literals_of prods), + roots = roots2 union roots1, + (* gram = extend_gram gram roots2 prods, *) (* FIXME *) + gram = gram, (* FIXME *) + consts = consts2 union consts1, + parse_ast_trtab = + extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation", + parse_ruletab = extend_ruletab parse_ruletab parse_rules, + parse_trtab = extend_trtab parse_trtab parse_translation "parse translation", + print_trtab = extend_trtab print_trtab print_translation "print translation", + print_ruletab = extend_ruletab print_ruletab print_rules, + prtab = extend_prtab prtab prods print_ast_translation} + end; + + (* mk_tables *) +val mk_tables = extend_tables empty_tables; + +(* FIXME *) fun mk_tables (XGram xgram) = let val {roots, prods, consts, parse_ast_translation, parse_rules, @@ -129,25 +181,6 @@ end; -(* add_synrules *) - -fun add_synrules (Tabs tabs) (SynRules rules) = - let - val {lexicon, roots, gram, consts, parse_ast_trtab, parse_ruletab, - parse_trtab, print_trtab, print_ruletab, prtab} = tabs; - val {parse_rules, print_rules} = rules; - in - Tabs { - lexicon = lexicon, roots = roots, gram = gram, consts = consts, - parse_ast_trtab = parse_ast_trtab, - parse_ruletab = extend_ruletab parse_ruletab parse_rules, - parse_trtab = parse_trtab, - print_trtab = print_trtab, - print_ruletab = extend_ruletab print_ruletab print_rules, - prtab = prtab} - end; - - (* ggr_to_xgram *) fun ggr_to_xgram ggr = @@ -168,9 +201,9 @@ end; -(* make_syntax *) +(* mk_syntax *) -fun make_syntax ggr = Syntax (ggr, mk_tables (ggr_to_xgram ggr)); +fun mk_syntax ggr = Syntax (ggr, mk_tables (ggr_to_xgram ggr)); @@ -390,32 +423,59 @@ (* type_syn *) -val type_syn = make_syntax (ref (ExtGG (ref EmptyGG, (type_ext, empty_synrules)))); +val type_syn = mk_syntax (ref (ExtGG (ref EmptyGG, type_ext))); + + +(* extend *) (* FIXME *) + +fun old_extend syn read_ty (roots, xconsts, sext) = + let + val Syntax (ggr0, Tabs {roots = roots0, ...}) = syn; + + val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext; + val (syn1 as Syntax (ggr1, tabs1)) = mk_syntax (ref (ExtGG (ggr0, ext1))); + + val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext); + val ext2 = ExtRules {parse_rules = parse_rules, print_rules = print_rules}; + in + Syntax (ref (ExtGG (ggr1, ext2)), extend_tables tabs1 (mk_xgram ext2)) + end; -(** extend **) - -fun extend (old_syn as Syntax (ggr, _)) read_ty (roots, xconsts, sext) = +fun new_extend syn read_ty (roots, xconsts, sext) = let - val ext = ext_of_sext roots xconsts read_ty sext; + val Syntax (ggr0, tabs0 as Tabs {roots = roots0, ...}) = syn; - val (tmp_syn as Syntax (_, tmp_tabs)) = - make_syntax (ref (ExtGG (ggr, (ext, empty_synrules)))); + val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext; + val (syn1 as Syntax (ggr1, tabs1)) = + Syntax (ref (ExtGG (ggr0, ext1)), extend_tables tabs0 (mk_xgram ext1)); - val (parse_rules, print_rules) = read_xrules tmp_syn (xrules_of sext); - val rules = - SynRules { - parse_rules = parse_rules, - print_rules = print_rules}; + val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext); + val ext2 = ExtRules {parse_rules = parse_rules, print_rules = print_rules}; in - Syntax (ref (ExtGG (ggr, (ext, rules))), add_synrules tmp_tabs rules) + Syntax (ref (ExtGG (ggr1, ext2)), extend_tables tabs1 (mk_xgram ext2)) end; +fun extend syn read_ty (ex as (_, _, sext)) = + (case sext of + Sext {mixfix = [], ...} => new_extend + | NewSext {mixfix = [], ...} => new_extend + | _ => old_extend) syn read_ty ex; + + (* merge *) -fun merge (Syntax (ggr1, _), Syntax (ggr2, _)) = - make_syntax (ref (MergeGG (ggr1, ggr2))); +fun merge roots syn1 syn2 = + let + val Syntax (ggr1, Tabs {roots = roots1, ...}) = syn1; + val Syntax (ggr2, Tabs {roots = roots2, ...}) = syn2; + val mggr = ref (MergeGG (ggr1, ggr2)); + in + (case ((distinct roots) \\ roots1) \\ roots2 of + [] => mk_syntax mggr + | new_roots => mk_syntax (ref (ExtGG (mggr, ExtRoots new_roots)))) + end; end;