diff -r b35851cafd3e -r c9ec452ff08f src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Fri Oct 01 13:26:22 1993 +0100 +++ b/src/Pure/Syntax/syntax.ML Mon Oct 04 15:30:49 1993 +0100 @@ -1,47 +1,53 @@ -(* Title: Pure/Syntax/syntax +(* Title: Pure/Syntax/syntax.ML ID: $Id$ Author: Tobias Nipkow and Markus Wenzel, TU Muenchen + +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: read_typ (incl check) as arg, remove def_sort + extend: use extend_tables *) signature SYNTAX = sig - (* FIXME include AST0 (?) *) + include AST0 include LEXICON0 include EXTENSION0 include TYPE_EXT0 include SEXTENSION1 include PRINTER0 - structure Extension: EXTENSION - structure Pretty: PRETTY - local open Extension.XGram Extension.XGram.Ast in - type syntax - val print_gram: syntax -> unit - val print_trans: syntax -> unit - val print_syntax: syntax -> unit - val read_ast: syntax -> string * string -> ast - val read: syntax -> typ -> string -> term - val pretty_term: syntax -> term -> Pretty.T - val pretty_typ: syntax -> typ -> Pretty.T - val string_of_term: syntax -> term -> string - val string_of_typ: syntax -> typ -> string - val type_syn: syntax - val extend: syntax * (indexname -> sort) -> string list * string list * sext - -> syntax - val merge: syntax * syntax -> syntax - end + type syntax + val type_syn: syntax + val extend: syntax * (indexname -> sort) -> string list * string list * sext + -> syntax + val merge: syntax * syntax -> syntax + val print_gram: syntax -> unit + val print_trans: syntax -> unit + val print_syntax: syntax -> unit + val test_read: syntax -> string -> string -> unit + val read: syntax -> typ -> string -> term + val pretty_term: syntax -> term -> Pretty.T + val pretty_typ: syntax -> typ -> Pretty.T + val string_of_term: syntax -> term -> string + val string_of_typ: syntax -> typ -> string end; functor SyntaxFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT and Parser: PARSER and SExtension: SEXTENSION and Printer: PRINTER - sharing TypeExt.Extension.XGram = Parser.XGram = Printer.XGram - and TypeExt.Extension = SExtension.Extension - and Parser.ParseTree.Ast = Parser.XGram.Ast)(*: SYNTAX *) = (* FIXME *) + sharing TypeExt.Extension = SExtension.Extension + and Parser.XGram = TypeExt.Extension.XGram = Printer.XGram + and Parser.XGram.Ast = Parser.ParseTree.Ast)(*: SYNTAX *) = (* FIXME *) struct structure Extension = TypeExt.Extension; structure XGram = Extension.XGram; structure Lexicon = Parser.ParseTree.Lexicon; -open Lexicon Extension TypeExt SExtension Printer XGram XGram.Ast; +open Lexicon Parser Parser.ParseTree Extension TypeExt SExtension Printer + XGram XGram.Ast; fun lookup tab a = Symtab.lookup (tab, a); @@ -51,20 +57,17 @@ (** datatype syntax **) datatype tables = - Tab of { - gram: Parser.Gram, - lexicon: Lexicon, - const_tab: unit Symtab.table, + Tabs of { + lexicon: lexicon, + roots: string list, + gram: gram, + consts: string list, parse_ast_trtab: (ast list -> ast) Symtab.table, - parse_preproc: ast -> ast, parse_ruletab: (ast * ast) list Symtab.table, - parse_postproc: ast -> ast, parse_trtab: (term list -> term) Symtab.table, print_trtab: (term list -> term) Symtab.table, - print_preproc: ast -> ast, print_ruletab: (ast * ast) list Symtab.table, - print_postproc: ast -> ast, - print_tab: Printer.tab}; + prtab: prtab}; datatype gramgraph = EmptyGG | @@ -77,6 +80,75 @@ (*** compile syntax ***) +(* translation funs *) + +fun extend_trtab tab trfuns name = + Symtab.balance (Symtab.st_of_alist (trfuns, tab)) handle Symtab.DUPLICATE s + => error ("More than one " ^ name ^ " for " ^ quote s); + +val mk_trtab = extend_trtab Symtab.null; + + +(* translation rules *) + +fun mk_ruletab rules = + let + fun add_rule (r, tab) = + let val a = head_of_rule r; + in + (case lookup tab a of + None => Symtab.update ((a, [r]), tab) + | Some rs => Symtab.update ((a, r :: rs), tab)) + end; + in + Symtab.balance (foldr add_rule (rules, Symtab.null)) + end; + +fun extend_ruletab tab rules = + mk_ruletab (flat (map #2 (Symtab.alist_of tab)) @ rules); + + +(* mk_tables *) + +fun mk_tables (XGram xgram) = + let + val {roots, prods, consts, parse_ast_translation, parse_rules, + parse_translation, print_translation, print_rules, + print_ast_translation} = xgram; + in + Tabs { + lexicon = mk_lexicon (literals_of prods), + roots = roots, + gram = mk_gram roots prods, + consts = consts, + parse_ast_trtab = mk_trtab parse_ast_translation "parse ast translation", + parse_ruletab = mk_ruletab parse_rules, + parse_trtab = mk_trtab parse_translation "parse translation", + print_trtab = mk_trtab print_translation "print translation", + print_ruletab = mk_ruletab print_rules, + prtab = mk_prtab prods print_ast_translation} + 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 = @@ -86,130 +158,38 @@ and flatGG' (ref EmptyGG) xgv = xgv | flatGG' (ref (ExtGG (ggr, ext))) xgv = let - val (xg', v') = flatGG ggr xgv + val (xg', v') = flatGG ggr xgv; in - (Extension.extend xg' ext, v') + (extend_xgram xg' ext, v') end | flatGG' (ref (MergeGG (ggr1, ggr2))) xgv = flatGG ggr1 (flatGG ggr2 xgv); in - fst (flatGG ggr (Extension.empty, [])) - end; - - -(* mk_ruletab *) - -fun mk_ruletab rules = - let - fun add_rule (r, tab) = - let - val a = head_of_rule r - in - case lookup tab a of - None => Symtab.update ((a, [r]), tab) - | Some rs => Symtab.update ((a, r :: rs), tab) - end; - in - Symtab.balance (foldr add_rule (rules, Symtab.null)) + #1 (flatGG ggr (empty_xgram, [])) end; (* make_syntax *) -fun make_syntax ggr = - let - fun mk_const_tab cs = - Symtab.balance - (Symtab.st_of_alist ((map (fn c => (c, ())) cs), Symtab.null)); - - fun mk_trtab alst name = - Symtab.balance (Symtab.st_of_alist (alst, Symtab.null)) - handle Symtab.DUPLICATE s => error ("More than one " ^ name ^ " for " ^ quote s); - - fun mk_proc (Some f) = f - | mk_proc None = I; - - fun all_strings (opl: string prod list): string list = - flat (map (fn Prod (_, syn, _, _) => terminals syn) opl); - - fun str_to_tok (opl: string prod list, lex: Lexicon): Token prod list = - map - (fn Prod (t, syn, s, pa) => - Prod (t, translate (hd o tokenize lex) syn, s, pa)) - opl; - - fun xgram_to_tables (XGram xgram) = - let - val {roots, prods, consts, parse_ast_translation, parse_preproc, parse_rules, - parse_postproc, parse_translation, print_translation, print_preproc, - print_rules, print_postproc, print_ast_translation} = xgram; - val lexicon = mk_lexicon (all_strings prods); - in - Tab { - gram = Parser.compile_xgram (roots, str_to_tok (prods, lexicon)), - lexicon = lexicon, - const_tab = mk_const_tab consts, - parse_ast_trtab = mk_trtab parse_ast_translation "parse ast translation", - parse_preproc = mk_proc parse_preproc, - parse_ruletab = mk_ruletab parse_rules, - parse_postproc = mk_proc parse_postproc, - parse_trtab = mk_trtab parse_translation "parse translation", - print_trtab = mk_trtab print_translation "print translation", - print_preproc = mk_proc print_preproc, - print_ruletab = mk_ruletab print_rules, - print_postproc = mk_proc print_postproc, - print_tab = mk_print_tab prods - (mk_trtab print_ast_translation "print ast translation")} - end; - in - Syntax (ggr, xgram_to_tables (ggr_to_xgram ggr)) - end; - - -(* add_synrules *) - -fun add_synrules (Tab tabs) (SynRules rules) = - let - val {gram, lexicon, const_tab, parse_ast_trtab, parse_preproc, parse_ruletab, - parse_postproc, parse_trtab, print_trtab, print_preproc, print_ruletab, - print_postproc, print_tab} = tabs; - val {parse_rules, print_rules} = rules; - val parse_rs = flat (map snd (Symtab.alist_of parse_ruletab)) @ parse_rules; - val print_rs = flat (map snd (Symtab.alist_of print_ruletab)) @ print_rules; - in - Tab { - gram = gram, lexicon = lexicon, const_tab = const_tab, - parse_ast_trtab = parse_ast_trtab, - parse_preproc = parse_preproc, - parse_ruletab = mk_ruletab parse_rs, - parse_postproc = parse_postproc, - parse_trtab = parse_trtab, - print_trtab = print_trtab, - print_preproc = print_preproc, - print_ruletab = mk_ruletab print_rs, - print_postproc = print_postproc, - print_tab = print_tab} - end; +fun make_syntax ggr = Syntax (ggr, mk_tables (ggr_to_xgram ggr)); (*** inspect syntax ***) -(* print_syntax_old *) (* FIXME remove *) - -fun print_syntax_old (Syntax (_, Tab {gram, lexicon, ...})) = - Parser.print_gram (gram, lexicon); - - - fun xgram_of (Syntax (ggr, _)) = ggr_to_xgram ggr; fun string_of_big_list name prts = Pretty.string_of (Pretty.blk (2, separate Pretty.fbrk (Pretty.str name :: prts))); +fun string_of_strings name strs = + Pretty.string_of (Pretty.blk (2, + separate (Pretty.brk 1) + (map Pretty.str (name :: map quote (sort_strings strs))))); -(* print_gram *) (* FIXME check *) + +(* print_gram *) fun prt_gram (XGram {roots, prods, ...}) = let @@ -233,51 +213,36 @@ Pretty.blk (2, pretty_name name @ pretty_xsymbs xsymbs @ pretty_const const @ pretty_pri pri); in + writeln (string_of_strings "lexicon:" (literals_of prods)); writeln (Pretty.string_of (Pretty.blk (2, separate (Pretty.brk 1) (map Pretty.str ("roots:" :: roots))))); writeln (string_of_big_list "prods:" (map pretty_prod prods)) end; - val print_gram = prt_gram o xgram_of; -(* print_trans *) (* FIXME check *) +(* print_trans *) fun prt_trans (XGram xgram) = let - fun string_of_strings name strs = - Pretty.string_of (Pretty.blk (2, - separate (Pretty.brk 1) (map Pretty.str (name :: map quote strs)))); - fun string_of_trs name trs = string_of_strings name (map fst trs); - fun string_of_proc name proc = - Pretty.string_of (Pretty.blk (2, [Pretty.str name, Pretty.brk 1, - Pretty.str (if is_none proc then "None" else "Some fn")])); - fun string_of_rules name rules = string_of_big_list name (map pretty_rule rules); - - val {consts, parse_ast_translation, parse_preproc, parse_rules, - parse_postproc, parse_translation, print_translation, print_preproc, - print_rules, print_postproc, print_ast_translation, ...} = xgram; + val {consts, parse_ast_translation, parse_rules, parse_translation, + print_translation, print_rules, print_ast_translation, ...} = xgram; in writeln (string_of_strings "consts:" consts); writeln (string_of_trs "parse_ast_translation:" parse_ast_translation); - writeln (string_of_proc "parse_preproc:" parse_preproc); writeln (string_of_rules "parse_rules:" parse_rules); - writeln (string_of_proc "parse_postproc:" parse_postproc); writeln (string_of_trs "parse_translation:" parse_translation); writeln (string_of_trs "print_translation:" print_translation); - writeln (string_of_proc "print_preproc:" print_preproc); writeln (string_of_rules "print_rules:" print_rules); - writeln (string_of_proc "print_postproc:" print_postproc); writeln (string_of_trs "print_ast_translation:" print_ast_translation) end; - val print_trans = prt_trans o xgram_of; @@ -294,63 +259,116 @@ (*** parsing and printing ***) -(* read_ast *) +(* mk_get_rules *) -fun read_ast syn (root, s) = - let - val Syntax (_, Tab {gram, lexicon, parse_ast_trtab, ...}) = syn; - val root = if Parser.parsable (gram, root) then root else error ("Unparsable root " ^ root) (* Extension.logic *); (* FIXME *) - fun syn_err toks = - error ("Syntax error at\n" ^ space_implode " " (map token_to_string toks)); - in - Parser.ParseTree.pt_to_ast (lookup parse_ast_trtab) - (Parser.parse (gram, root, tokenize lexicon s)) - handle Parser.SYNTAX_ERR toks => syn_err toks - end; - - -(* norm_ast *) - -fun norm_ast ruletab ast = +fun mk_get_rules ruletab = let fun get_rules a = (case lookup ruletab a of Some rules => rules | None => []); in - normalize (if Symtab.is_null ruletab then None else Some get_rules) ast + if Symtab.is_null ruletab then None else Some get_rules + end; + + +(* read_ast *) + +fun read_ast (Syntax (_, tabs)) xids root str = + let + val Tabs {lexicon, gram, parse_ast_trtab, ...} = tabs; + in + pt_to_ast (lookup parse_ast_trtab) + (parse gram root (tokenize lexicon xids str)) end; +(** test_read **) + +fun test_read (Syntax (_, tabs)) root str = + let + val Tabs {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs; + + val toks = tokenize lexicon false str; + val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks)); + + val pt = parse gram root toks; + val raw_ast = pt_to_ast (K None) pt; + val _ = writeln ("raw: " ^ str_of_ast raw_ast); + + val pre_ast = pt_to_ast (lookup parse_ast_trtab) pt; + val _ = normalize true true (mk_get_rules parse_ruletab) pre_ast; + in () end; + + + (** read **) -fun read (syn as Syntax (_, Tab tabs)) ty s = +fun read (syn as Syntax (_, tabs)) ty str = let - val {parse_preproc, parse_ruletab, parse_postproc, parse_trtab, ...} = tabs; - val ast = read_ast syn (typ_to_nt ty, s); + val Tabs {parse_ruletab, parse_trtab, ...} = tabs; + val ast = read_ast syn false (typ_to_nonterm ty) str; in ast_to_term (lookup parse_trtab) - (parse_postproc (norm_ast parse_ruletab (parse_preproc ast))) + (normalize_ast (mk_get_rules parse_ruletab) ast) end; -(** pprint_ast **) +(** read_rule **) + +fun read_rule syn (xrule as ((_, lhs_src), (_, rhs_src))) = + let + val Syntax (_, Tabs {consts, ...}) = syn; + + fun constantify (ast as Constant _) = ast + | constantify (ast as Variable x) = + if x mem consts then Constant x else ast + | constantify (Appl asts) = Appl (map constantify asts); -val pprint_ast = Pretty.pprint o pretty_ast; + fun read_pat (root, str) = + constantify (read_ast syn true root str) + handle ERROR => error ("The error above occurred in " ^ quote str); + + val rule as (lhs, rhs) = (pairself read_pat) xrule; + in + (case rule_error rule of + Some msg => + error ("Error in syntax translation rule: " ^ msg ^ + "\nexternal: " ^ quote lhs_src ^ " -> " ^ quote rhs_src ^ + "\ninternal: " ^ str_of_ast lhs ^ " -> " ^ str_of_ast rhs) + | None => rule) + end; -(** pretty term, typ **) +(** read_xrules **) + +fun read_xrules syn xrules = + let + fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2) + | right_rule (xpat1 <-| xpat2) = None + | right_rule (xpat1 <-> xpat2) = Some (xpat1, xpat2); -fun pretty_t t_to_ast pretty_t (syn as Syntax (_, Tab tabs)) t = + fun left_rule (xpat1 |-> xpat2) = None + | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1) + | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1); + in + (map (read_rule syn) (mapfilter right_rule xrules), + map (read_rule syn) (mapfilter left_rule xrules)) + end; + + + +(** pretty terms or typs **) + +fun pretty_t t_to_ast pretty_t (syn as Syntax (_, tabs)) t = let - val {print_trtab, print_preproc, print_ruletab, print_postproc, print_tab, ...} = tabs; + val Tabs {print_trtab, print_ruletab, prtab, ...} = tabs; val ast = t_to_ast (lookup print_trtab) t; in - pretty_t print_tab - (print_postproc (norm_ast print_ruletab (print_preproc ast))) + pretty_t prtab (normalize_ast (mk_get_rules print_ruletab) ast) end; val pretty_term = pretty_t term_to_ast pretty_term_ast; @@ -370,53 +388,23 @@ val type_syn = make_syntax (ref (ExtGG (ref EmptyGG, (type_ext, empty_synrules)))); -(* extend *) (* FIXME check *) +(** extend **) fun extend (old_syn as Syntax (ggr, _), def_sort) (roots, xconsts, sext) = let fun read_typ s = typ_of_term def_sort (read old_syn typeT s); val ext = ext_of_sext roots xconsts read_typ sext; - fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2) - | right_rule (xpat1 <-| xpat2) = None - | right_rule (xpat1 <-> xpat2) = Some (xpat1, xpat2); - - fun left_rule (xpat1 |-> xpat2) = None - | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1) - | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1); - val (tmp_syn as Syntax (_, tmp_tabs)) = make_syntax (ref (ExtGG (ggr, (ext, empty_synrules)))); - val Syntax (_, Tab {const_tab, ...}) = tmp_syn; - fun constantify (ast as (Constant _)) = ast - | constantify (ast as (Variable x)) = - if is_some (lookup const_tab x) then Constant x else ast - | constantify (Appl asts) = Appl (map constantify asts); - - fun read_pat (r_s as (root, s)) = - constantify ((read_ast tmp_syn r_s) - handle ERROR => error ("The error above occurred in " ^ quote s)); - - fun read_rule (xrule as ((_, lhs_src), (_, rhs_src))) = - let - val rule as (lhs, rhs) = (pairself read_pat) xrule; - in - case rule_error rule of - Some msg => - error ("Error in syntax translation rule: " ^ msg ^ - "\nexternal: " ^ quote lhs_src ^ " -> " ^ quote rhs_src ^ - "\ninternal: " ^ str_of_ast lhs ^ " -> " ^ str_of_ast rhs) - | None => rule - end; - - val xrules = xrules_of sext; - val new_rules = + val (parse_rules, print_rules) = read_xrules tmp_syn (xrules_of sext); + val rules = SynRules { - parse_rules = map read_rule (mapfilter right_rule xrules), - print_rules = map read_rule (mapfilter left_rule xrules)}; + parse_rules = parse_rules, + print_rules = print_rules}; in - Syntax (ref (ExtGG (ggr, (ext, new_rules))), add_synrules tmp_tabs new_rules) + Syntax (ref (ExtGG (ggr, (ext, rules))), add_synrules tmp_tabs rules) end;