wenzelm@18: (* Title: Pure/Syntax/syntax.ML clasohm@0: ID: $Id$ clasohm@0: Author: Tobias Nipkow and Markus Wenzel, TU Muenchen wenzelm@18: wenzelm@18: Root of Isabelle's syntax module. clasohm@0: *) clasohm@0: wenzelm@260: signature BASIC_SYNTAX = wenzelm@2383: sig wenzelm@260: include AST0 wenzelm@556: include SYN_TRANS0 wenzelm@556: include MIXFIX0 wenzelm@260: include PRINTER0 wenzelm@2383: end; wenzelm@260: clasohm@0: signature SYNTAX = wenzelm@2383: sig wenzelm@6322: include TOKEN_TRANS0 wenzelm@260: include AST1 clasohm@0: include LEXICON0 wenzelm@237: include SYN_EXT0 clasohm@0: include TYPE_EXT0 wenzelm@556: include SYN_TRANS1 wenzelm@556: include MIXFIX1 clasohm@0: include PRINTER0 wenzelm@1158: datatype 'a trrule = wenzelm@3526: ParseRule of 'a * 'a | wenzelm@3526: PrintRule of 'a * 'a | wenzelm@3526: ParsePrintRule of 'a * 'a wenzelm@556: type syntax wenzelm@12073: val extend_log_types: string list -> syntax -> syntax wenzelm@12073: val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax wenzelm@12073: val extend_const_gram: string * bool -> (string * typ * mixfix) list -> syntax -> syntax wenzelm@12073: val extend_consts: string list -> syntax -> syntax wenzelm@12073: val extend_trfuns: wenzelm@556: (string * (ast list -> ast)) list * wenzelm@556: (string * (term list -> term)) list * wenzelm@556: (string * (term list -> term)) list * wenzelm@12073: (string * (ast list -> ast)) list -> syntax -> syntax wenzelm@12073: val extend_trfunsT: (string * (bool -> typ -> term list -> term)) list -> syntax -> syntax wenzelm@12073: val extend_tokentrfuns: (string * string * (string -> string * real)) list -> syntax -> syntax wenzelm@12073: val extend_trrules: (string * string) trrule list -> syntax -> syntax wenzelm@12073: val extend_trrules_i: ast trrule list -> syntax -> syntax wenzelm@4618: val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule wenzelm@556: val merge_syntaxes: syntax -> syntax -> syntax wenzelm@556: val type_syn: syntax clasohm@764: val pure_syn: syntax wenzelm@556: val print_gram: syntax -> unit wenzelm@556: val print_trans: syntax -> unit wenzelm@556: val print_syntax: syntax -> unit wenzelm@556: val test_read: syntax -> string -> string -> unit clasohm@624: val read: syntax -> typ -> string -> term list wenzelm@12316: val read_typ: syntax -> ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) -> wenzelm@12316: string -> typ wenzelm@8894: val read_sort: syntax -> string -> sort wenzelm@3779: val pretty_term: syntax -> bool -> term -> Pretty.T wenzelm@556: val pretty_typ: syntax -> typ -> Pretty.T wenzelm@3779: val pretty_sort: syntax -> sort -> Pretty.T wenzelm@3782: val simple_str_of_sort: sort -> string wenzelm@556: val simple_string_of_typ: typ -> string wenzelm@556: val simple_pprint_typ: typ -> pprint_args -> unit clasohm@882: val ambiguity_level: int ref wenzelm@2383: end; clasohm@0: wenzelm@12094: structure Syntax: SYNTAX = clasohm@0: struct clasohm@0: wenzelm@237: wenzelm@237: (** tables of translation functions **) wenzelm@237: wenzelm@5692: fun mk_trfun (c, f) = (c, (f, stamp ())); wenzelm@12292: fun eq_trfuns ((_, s1:stamp), (_, s2)) = s1 = s2; clasohm@0: clasohm@0: wenzelm@5692: (* parse (ast) translations *) wenzelm@5692: wenzelm@5692: fun lookup_tr tab c = apsome fst (Symtab.lookup (tab, c)); wenzelm@237: wenzelm@383: fun err_dup_trfuns name cs = wenzelm@383: error ("More than one " ^ name ^ " for " ^ commas_quote cs); wenzelm@237: wenzelm@237: fun extend_trtab tab trfuns name = wenzelm@5692: Symtab.extend (tab, map mk_trfun trfuns) wenzelm@383: handle Symtab.DUPS cs => err_dup_trfuns name cs; wenzelm@237: wenzelm@237: fun merge_trtabs tab1 tab2 name = wenzelm@237: Symtab.merge eq_snd (tab1, tab2) wenzelm@383: handle Symtab.DUPS cs => err_dup_trfuns name cs; wenzelm@237: wenzelm@237: wenzelm@5692: (* print (ast) translations *) wenzelm@5692: wenzelm@5692: fun lookup_tr' tab c = map fst (Symtab.lookup_multi (tab, c)); wenzelm@12292: fun extend_tr'tab tab trfuns = foldr Symtab.update_multi (map mk_trfun trfuns, tab); wenzelm@12292: fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' eq_trfuns (tab1, tab2); wenzelm@5692: wenzelm@5692: wenzelm@237: wenzelm@2700: (** tables of token translation functions **) wenzelm@2700: wenzelm@2700: fun lookup_tokentr tabs modes = wenzelm@4496: let val trs = gen_distinct eq_fst (flat (map (assocs tabs) (modes @ [""]))) wenzelm@2700: in fn c => apsome fst (assoc (trs, c)) end; wenzelm@2700: wenzelm@2700: fun merge_tokentrtabs tabs1 tabs2 = wenzelm@2700: let wenzelm@2700: fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2; wenzelm@2700: wenzelm@4703: fun name (s, _) = implode (tl (Symbol.explode s)); wenzelm@2706: wenzelm@2700: fun merge mode = wenzelm@2700: let wenzelm@2700: val trs1 = assocs tabs1 mode; wenzelm@2700: val trs2 = assocs tabs2 mode; wenzelm@2700: val trs = gen_distinct eq_tr (trs1 @ trs2); wenzelm@2700: in wenzelm@2700: (case gen_duplicates eq_fst trs of wenzelm@2700: [] => (mode, trs) wenzelm@2700: | dups => error ("More than one token translation function in mode " ^ wenzelm@2706: quote mode ^ " for " ^ commas_quote (map name dups))) wenzelm@2700: end; wenzelm@2700: in wenzelm@2700: map merge (distinct (map fst (tabs1 @ tabs2))) wenzelm@2700: end; wenzelm@2700: wenzelm@2700: fun extend_tokentrtab tabs tokentrs = wenzelm@2700: let wenzelm@2700: fun ins_tokentr (ts, (m, c, f)) = wenzelm@2700: overwrite (ts, (m, ("_" ^ c, (f, stamp ())) :: assocs ts m)); wenzelm@2700: in wenzelm@2700: merge_tokentrtabs tabs (foldl ins_tokentr ([], tokentrs)) wenzelm@2700: end; wenzelm@2700: wenzelm@2700: wenzelm@2700: wenzelm@237: (** tables of translation rules **) wenzelm@237: wenzelm@5692: type ruletab = (Ast.ast * Ast.ast) list Symtab.table; wenzelm@237: wenzelm@383: fun dest_ruletab tab = flat (map snd (Symtab.dest tab)); wenzelm@9372: fun lookup_ruletab tab a = Symtab.lookup_multi (tab, a); wenzelm@237: wenzelm@237: wenzelm@237: (* empty, extend, merge ruletabs *) wenzelm@237: wenzelm@237: fun extend_ruletab tab rules = wenzelm@12292: foldr Symtab.update_multi (map (fn r => (Ast.head_of_rule r, r)) rules, tab); wenzelm@237: wenzelm@12292: fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2); clasohm@0: clasohm@0: clasohm@0: clasohm@0: (** datatype syntax **) clasohm@0: wenzelm@237: datatype syntax = wenzelm@237: Syntax of { wenzelm@4703: lexicon: Scan.lexicon, clasohm@764: logtypes: string list, wenzelm@5692: gram: Parser.gram, wenzelm@18: consts: string list, wenzelm@2913: prmodes: string list, wenzelm@5692: parse_ast_trtab: ((Ast.ast list -> Ast.ast) * stamp) Symtab.table, wenzelm@237: parse_ruletab: ruletab, wenzelm@5692: parse_trtab: ((term list -> term) * stamp) Symtab.table, wenzelm@5692: print_trtab: ((bool -> typ -> term list -> term) * stamp) list Symtab.table, wenzelm@237: print_ruletab: ruletab, wenzelm@5692: print_ast_trtab: ((Ast.ast list -> Ast.ast) * stamp) list Symtab.table, wenzelm@6322: tokentrtab: (string * (string * ((string -> string * real) * stamp)) list) list, wenzelm@5692: prtabs: Printer.prtabs} clasohm@0: wenzelm@18: wenzelm@237: (* empty_syntax *) wenzelm@18: wenzelm@237: val empty_syntax = wenzelm@237: Syntax { wenzelm@4703: lexicon = Scan.empty_lexicon, clasohm@764: logtypes = [], wenzelm@5692: gram = Parser.empty_gram, wenzelm@167: consts = [], wenzelm@2913: prmodes = [], wenzelm@5692: parse_ast_trtab = Symtab.empty, wenzelm@5692: parse_ruletab = Symtab.empty, wenzelm@5692: parse_trtab = Symtab.empty, wenzelm@5692: print_trtab = Symtab.empty, wenzelm@5692: print_ruletab = Symtab.empty, wenzelm@5692: print_ast_trtab = Symtab.empty, wenzelm@2700: tokentrtab = [], wenzelm@5692: prtabs = Printer.empty_prtabs} wenzelm@167: wenzelm@167: wenzelm@237: (* extend_syntax *) wenzelm@167: wenzelm@2366: fun extend_syntax (mode, inout) (Syntax tabs) syn_ext = wenzelm@167: let wenzelm@2913: val {lexicon, logtypes = logtypes1, gram, consts = consts1, prmodes = prmodes1, wenzelm@2366: parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, wenzelm@2700: print_ast_trtab, tokentrtab, prtabs} = tabs; wenzelm@5692: val SynExt.SynExt {logtypes = logtypes2, xprods, consts = consts2, prmodes = prmodes2, wenzelm@2913: parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, wenzelm@2700: print_ast_translation, token_translation} = syn_ext; wenzelm@167: in wenzelm@237: Syntax { wenzelm@5692: lexicon = if inout then Scan.extend_lexicon lexicon (SynExt.delims_of xprods) else lexicon, wenzelm@12292: logtypes = merge_lists logtypes1 logtypes2, wenzelm@5692: gram = if inout then Parser.extend_gram gram xprods else gram, berghofe@11528: consts = consts2 @ consts1, wenzelm@11546: prmodes = (mode ins_string prmodes2) union_string prmodes1, wenzelm@167: parse_ast_trtab = wenzelm@167: extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation", wenzelm@167: parse_ruletab = extend_ruletab parse_ruletab parse_rules, wenzelm@167: parse_trtab = extend_trtab parse_trtab parse_translation "parse translation", wenzelm@5692: print_trtab = extend_tr'tab print_trtab print_translation, wenzelm@167: print_ruletab = extend_ruletab print_ruletab print_rules, wenzelm@5692: print_ast_trtab = extend_tr'tab print_ast_trtab print_ast_translation, wenzelm@2700: tokentrtab = extend_tokentrtab tokentrtab token_translation, wenzelm@5692: prtabs = Printer.extend_prtabs prtabs mode xprods} wenzelm@18: end; wenzelm@18: wenzelm@18: wenzelm@237: (* merge_syntaxes *) clasohm@0: wenzelm@237: fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) = clasohm@0: let wenzelm@2913: val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1, consts = consts1, wenzelm@2913: prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1, wenzelm@237: parse_trtab = parse_trtab1, print_trtab = print_trtab1, wenzelm@237: print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1, wenzelm@2700: tokentrtab = tokentrtab1, prtabs = prtabs1} = tabs1; wenzelm@237: wenzelm@2913: val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2, consts = consts2, wenzelm@2913: prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2, wenzelm@237: parse_trtab = parse_trtab2, print_trtab = print_trtab2, wenzelm@237: print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2, wenzelm@2700: tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2; clasohm@0: in wenzelm@237: Syntax { wenzelm@4703: lexicon = Scan.merge_lexicons lexicon1 lexicon2, clasohm@764: logtypes = merge_lists logtypes1 logtypes2, wenzelm@5692: gram = Parser.merge_grams gram1 gram2, berghofe@11528: consts = unique_strings (sort_strings (consts1 @ consts2)), wenzelm@2913: prmodes = merge_lists prmodes1 prmodes2, wenzelm@237: parse_ast_trtab = wenzelm@237: merge_trtabs parse_ast_trtab1 parse_ast_trtab2 "parse ast translation", wenzelm@237: parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2, wenzelm@237: parse_trtab = merge_trtabs parse_trtab1 parse_trtab2 "parse translation", wenzelm@5692: print_trtab = merge_tr'tabs print_trtab1 print_trtab2, wenzelm@237: print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2, wenzelm@5692: print_ast_trtab = merge_tr'tabs print_ast_trtab1 print_ast_trtab2, wenzelm@2700: tokentrtab = merge_tokentrtabs tokentrtab1 tokentrtab2, wenzelm@5692: prtabs = Printer.merge_prtabs prtabs1 prtabs2} clasohm@0: end; clasohm@0: clasohm@0: wenzelm@260: (* type_syn *) wenzelm@260: wenzelm@5692: val type_syn = extend_syntax ("", true) empty_syntax TypeExt.type_ext; wenzelm@5692: val pure_syn = extend_syntax ("", true) type_syn SynExt.pure_ext; wenzelm@260: clasohm@0: wenzelm@4887: wenzelm@237: (** inspect syntax **) clasohm@0: wenzelm@260: fun pretty_strs_qs name strs = wenzelm@260: Pretty.strs (name :: map quote (sort_strings strs)); clasohm@0: wenzelm@18: wenzelm@18: (* print_gram *) clasohm@0: wenzelm@237: fun print_gram (Syntax tabs) = clasohm@0: let wenzelm@2913: val {lexicon, logtypes, prmodes, gram, prtabs, ...} = tabs; wenzelm@2913: val prmodes' = sort_strings (filter_out (equal "") prmodes); clasohm@0: in wenzelm@8720: [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon), wenzelm@8720: Pretty.strs ("logtypes:" :: logtypes), wenzelm@8720: Pretty.big_list "prods:" (Parser.pretty_gram gram), wenzelm@8720: pretty_strs_qs "print modes:" prmodes'] wenzelm@8720: |> Pretty.chunks |> Pretty.writeln clasohm@0: end; clasohm@0: clasohm@0: wenzelm@18: (* print_trans *) clasohm@0: wenzelm@237: fun print_trans (Syntax tabs) = clasohm@0: let wenzelm@260: fun pretty_trtab name tab = wenzelm@5692: pretty_strs_qs name (Symtab.keys tab); clasohm@0: wenzelm@260: fun pretty_ruletab name tab = wenzelm@5692: Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab)); clasohm@0: wenzelm@4703: fun pretty_tokentr (mode, trs) = Pretty.strs (quote mode ^ ":" :: map fst trs); wenzelm@4703: wenzelm@237: val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, wenzelm@4703: print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs; clasohm@0: in wenzelm@8720: [pretty_strs_qs "consts:" consts, wenzelm@8720: pretty_trtab "parse_ast_translation:" parse_ast_trtab, wenzelm@8720: pretty_ruletab "parse_rules:" parse_ruletab, wenzelm@8720: pretty_trtab "parse_translation:" parse_trtab, wenzelm@8720: pretty_trtab "print_translation:" print_trtab, wenzelm@8720: pretty_ruletab "print_rules:" print_ruletab, wenzelm@8720: pretty_trtab "print_ast_translation:" print_ast_trtab, wenzelm@8720: Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab)] wenzelm@8720: |> Pretty.chunks |> Pretty.writeln clasohm@0: end; clasohm@0: clasohm@0: clasohm@0: (* print_syntax *) clasohm@0: wenzelm@237: fun print_syntax syn = (print_gram syn; print_trans syn); clasohm@0: clasohm@0: clasohm@0: wenzelm@237: (** read **) wenzelm@18: wenzelm@237: (* test_read *) wenzelm@18: wenzelm@237: fun test_read (Syntax tabs) root str = wenzelm@18: let wenzelm@237: val {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs; wenzelm@18: wenzelm@4703: val chars = Symbol.explode str; wenzelm@5692: val toks = Lexicon.tokenize lexicon false chars; wenzelm@5692: val _ = writeln ("tokens: " ^ space_implode " " (map Lexicon.display_token toks)); wenzelm@18: wenzelm@383: fun show_pt pt = wenzelm@383: let wenzelm@5692: val raw_ast = SynTrans.pt_to_ast (K None) pt; wenzelm@5692: val _ = writeln ("raw: " ^ Ast.str_of_ast raw_ast); wenzelm@5692: val pre_ast = SynTrans.pt_to_ast (lookup_tr parse_ast_trtab) pt; wenzelm@5692: val _ = Ast.normalize true true (lookup_ruletab parse_ruletab) pre_ast; wenzelm@383: in () end; wenzelm@5692: in seq show_pt (Parser.parse gram root toks) end; wenzelm@18: wenzelm@18: wenzelm@260: (* read_ast *) wenzelm@260: clasohm@882: val ambiguity_level = ref 1; clasohm@882: clasohm@865: fun read_asts (Syntax tabs) xids root str = wenzelm@260: let clasohm@764: val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs; wenzelm@5692: val root' = if root mem logtypes then SynExt.logic else root; wenzelm@4703: val chars = Symbol.explode str; wenzelm@5692: val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars); clasohm@330: wenzelm@12292: fun show_pt pt = wenzelm@12292: warning (Pretty.string_of (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt))); wenzelm@260: in wenzelm@888: if length pts > ! ambiguity_level then oheimb@7944: (warning ("Ambiguous input " ^ quote str); wenzelm@3526: warning "produces the following parse trees:"; clasohm@882: seq show_pt pts) clasohm@624: else (); wenzelm@5692: map (SynTrans.pt_to_ast (lookup_tr parse_ast_trtab)) pts wenzelm@260: end; wenzelm@260: wenzelm@260: wenzelm@237: (* read *) clasohm@0: wenzelm@237: fun read (syn as Syntax tabs) ty str = clasohm@0: let wenzelm@237: val {parse_ruletab, parse_trtab, ...} = tabs; wenzelm@5692: val asts = read_asts syn false (SynExt.typ_to_nonterm ty) str; clasohm@0: in wenzelm@5692: map (SynTrans.ast_to_term (lookup_tr parse_trtab)) wenzelm@5692: (map (Ast.normalize_ast (lookup_ruletab parse_ruletab)) asts) clasohm@0: end; clasohm@0: clasohm@0: wenzelm@237: (* read types *) clasohm@0: wenzelm@12316: fun read_typ syn get_sort map_sort str = wenzelm@5692: (case read syn SynExt.typeT str of wenzelm@12316: [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) map_sort t wenzelm@8894: | _ => error "read_typ: ambiguous syntax"); wenzelm@144: wenzelm@144: wenzelm@8894: (* read sorts *) wenzelm@8894: wenzelm@8894: fun read_sort syn str = wenzelm@8894: (case read syn TypeExt.sortT str of wenzelm@8894: [t] => TypeExt.sort_of_term t wenzelm@8894: | _ => error "read_sort: ambiguous syntax"); wenzelm@8894: wenzelm@8894: wenzelm@18: wenzelm@1158: (** prepare translation rules **) wenzelm@1158: wenzelm@1158: datatype 'a trrule = wenzelm@3526: ParseRule of 'a * 'a | wenzelm@3526: PrintRule of 'a * 'a | wenzelm@3526: ParsePrintRule of 'a * 'a; wenzelm@888: wenzelm@4618: fun map_trrule f (ParseRule (x, y)) = ParseRule (f x, f y) wenzelm@4618: | map_trrule f (PrintRule (x, y)) = PrintRule (f x, f y) wenzelm@4618: | map_trrule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y); wenzelm@1158: wenzelm@3526: fun parse_rule (ParseRule pats) = Some pats wenzelm@3526: | parse_rule (PrintRule _) = None wenzelm@3526: | parse_rule (ParsePrintRule pats) = Some pats; wenzelm@1158: wenzelm@3526: fun print_rule (ParseRule _) = None wenzelm@3526: | print_rule (PrintRule pats) = Some (swap pats) wenzelm@3526: | print_rule (ParsePrintRule pats) = Some (swap pats); wenzelm@1158: wenzelm@1158: wenzelm@1158: fun check_rule (rule as (lhs, rhs)) = wenzelm@5692: (case Ast.rule_error rule of wenzelm@1158: Some msg => wenzelm@1158: error ("Error in syntax translation rule: " ^ msg ^ "\n" ^ wenzelm@5692: Ast.str_of_ast lhs ^ " -> " ^ Ast.str_of_ast rhs) wenzelm@1158: | None => rule); wenzelm@888: wenzelm@888: wenzelm@888: fun read_pattern syn (root, str) = wenzelm@18: let wenzelm@237: val Syntax {consts, ...} = syn; wenzelm@18: wenzelm@5692: fun constify (ast as Ast.Constant _) = ast wenzelm@5692: | constify (ast as Ast.Variable x) = wenzelm@8720: if x mem consts orelse NameSpace.is_qualified x then Ast.Constant x wenzelm@3830: else ast wenzelm@5692: | constify (Ast.Appl asts) = Ast.Appl (map constify asts); wenzelm@18: in wenzelm@888: (case read_asts syn true root str of wenzelm@888: [ast] => constify ast wenzelm@888: | _ => error ("Syntactically ambiguous input: " ^ quote str)) wenzelm@888: end handle ERROR => wenzelm@888: error ("The error(s) above occurred in translation pattern " ^ wenzelm@888: quote str); clasohm@0: wenzelm@556: wenzelm@1158: fun prep_rules rd_pat raw_rules = wenzelm@4618: let val rules = map (map_trrule rd_pat) raw_rules in wenzelm@3526: (map check_rule (mapfilter parse_rule rules), wenzelm@3526: map check_rule (mapfilter print_rule rules)) wenzelm@1158: end wenzelm@18: wenzelm@18: wenzelm@18: wenzelm@3779: (** pretty terms, typs, sorts **) wenzelm@18: wenzelm@3779: fun pretty_t t_to_ast prt_t (syn as Syntax tabs) curried t = clasohm@0: let wenzelm@2700: val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs; wenzelm@5692: val ast = t_to_ast (lookup_tr' print_trtab) t; clasohm@0: in wenzelm@5692: prt_t curried prtabs (lookup_tr' print_ast_trtab) oheimb@6167: (lookup_tokentr tokentrtab (! print_mode)) wenzelm@5692: (Ast.normalize_ast (lookup_ruletab print_ruletab) ast) clasohm@0: end; clasohm@0: wenzelm@5692: val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast; wenzelm@5692: fun pretty_typ syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast syn false; wenzelm@5692: fun pretty_sort syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast syn false; clasohm@0: wenzelm@3782: val simple_str_of_sort = Pretty.str_of o pretty_sort type_syn; wenzelm@3779: val simple_string_of_typ = Pretty.string_of o (pretty_typ type_syn); wenzelm@260: val simple_pprint_typ = Pretty.pprint o Pretty.quote o (pretty_typ type_syn); clasohm@0: clasohm@0: clasohm@0: wenzelm@383: (** extend syntax (external interfaces) **) wenzelm@383: wenzelm@12073: fun ext_syntax mk_syn_ext prmode decls (syn as Syntax {logtypes, ...}) = wenzelm@2202: extend_syntax prmode syn (mk_syn_ext logtypes decls); wenzelm@383: wenzelm@167: wenzelm@12073: fun extend_log_types logtypes syn = wenzelm@5692: extend_syntax ("", true) syn (SynExt.syn_ext_logtypes logtypes); wenzelm@383: wenzelm@5692: val extend_type_gram = ext_syntax Mixfix.syn_ext_types ("", true); wenzelm@383: wenzelm@12073: fun extend_const_gram prmode = ext_syntax Mixfix.syn_ext_consts prmode; wenzelm@383: wenzelm@5692: val extend_consts = ext_syntax SynExt.syn_ext_const_names ("", true); wenzelm@383: wenzelm@5692: val extend_trfuns = ext_syntax SynExt.syn_ext_trfuns ("", true); wenzelm@383: wenzelm@5692: val extend_trfunsT = ext_syntax SynExt.syn_ext_trfunsT ("", true); wenzelm@2383: wenzelm@5692: val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns ("", true); wenzelm@2700: wenzelm@12073: fun extend_trrules rules syn = wenzelm@12073: ext_syntax SynExt.syn_ext_rules ("", true) (prep_rules (read_pattern syn) rules) syn; wenzelm@1158: wenzelm@12073: fun extend_trrules_i rules = ext_syntax SynExt.syn_ext_rules ("", true) (prep_rules I rules); wenzelm@5692: wenzelm@5692: wenzelm@5692: wenzelm@5692: (** export parts of internal Syntax structures **) wenzelm@5692: wenzelm@6322: open TokenTrans Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer; wenzelm@2366: wenzelm@2366: clasohm@0: end; wenzelm@5692: wenzelm@5692: wenzelm@5692: structure BasicSyntax: BASIC_SYNTAX = Syntax; wenzelm@5692: open BasicSyntax;