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@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@556: val extend_log_types: syntax -> string list -> syntax wenzelm@556: val extend_type_gram: syntax -> (string * int * mixfix) list -> syntax wenzelm@2366: val extend_const_gram: syntax -> string * bool -> (string * typ * mixfix) list -> syntax wenzelm@556: val extend_consts: syntax -> string list -> syntax wenzelm@556: val extend_trfuns: syntax -> wenzelm@556: (string * (ast list -> ast)) list * wenzelm@556: (string * (term list -> term)) list * wenzelm@556: (string * (term list -> term)) list * wenzelm@556: (string * (ast list -> ast)) list -> syntax wenzelm@4145: val extend_trfunsT: syntax -> (string * (bool -> typ -> term list -> term)) list -> syntax wenzelm@2700: val extend_tokentrfuns: syntax -> (string * string * (string -> string * int)) list -> syntax wenzelm@1158: val extend_trrules: syntax -> (string * string) trrule list -> syntax wenzelm@1158: val extend_trrules_i: syntax -> ast trrule list -> 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@3779: val read_typ: syntax -> ((indexname * sort) list -> indexname -> sort) -> string -> typ wenzelm@556: val simple_read_typ: string -> typ 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: paulson@1511: 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@5692: fun eq_trfuns ((c1:string, (_, s1:stamp)), (c2, (_, s2))) = c1 = c2 andalso 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@5692: wenzelm@5692: fun extend_tr'tab tab trfuns = wenzelm@5692: generic_extend eq_trfuns Symtab.dest_multi Symtab.make_multi tab (map mk_trfun trfuns); wenzelm@5692: wenzelm@5692: val merge_tr'tabs = generic_merge eq_trfuns Symtab.dest_multi Symtab.make_multi; 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@237: wenzelm@237: wenzelm@237: (* lookup_ruletab *) wenzelm@237: wenzelm@237: fun lookup_ruletab tab = wenzelm@4487: if Symtab.is_empty tab then None wenzelm@237: else Some (fn 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@237: generic_extend (op =) Symtab.dest_multi Symtab.make_multi tab wenzelm@5692: (map (fn r => (Ast.head_of_rule r, r)) (distinct rules)); wenzelm@237: wenzelm@237: fun merge_ruletabs tab1 tab2 = wenzelm@237: generic_merge (op =) Symtab.dest_multi Symtab.make_multi 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@2700: tokentrtab: (string * (string * ((string -> string * int) * 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, clasohm@764: logtypes = extend_list logtypes1 logtypes2, wenzelm@5692: gram = if inout then Parser.extend_gram gram xprods else gram, wenzelm@167: consts = consts2 union consts1, wenzelm@2913: prmodes = (mode ins prmodes2) union 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, wenzelm@237: consts = merge_lists 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@4703: Pretty.writeln (pretty_strs_qs "lexicon:" (map implode (Scan.dest_lexicon lexicon))); clasohm@764: Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes)); wenzelm@5692: Pretty.writeln (Pretty.big_list "prods:" (Parser.pretty_gram gram)); wenzelm@2913: Pretty.writeln (pretty_strs_qs "print modes:" prmodes') 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@260: Pretty.writeln (pretty_strs_qs "consts:" consts); wenzelm@260: Pretty.writeln (pretty_trtab "parse_ast_translation:" parse_ast_trtab); wenzelm@260: Pretty.writeln (pretty_ruletab "parse_rules:" parse_ruletab); wenzelm@260: Pretty.writeln (pretty_trtab "parse_translation:" parse_trtab); wenzelm@260: Pretty.writeln (pretty_trtab "print_translation:" print_trtab); wenzelm@260: Pretty.writeln (pretty_ruletab "print_rules:" print_ruletab); wenzelm@4703: Pretty.writeln (pretty_trtab "print_ast_translation:" print_ast_trtab); wenzelm@4703: Pretty.writeln (Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab)) 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@3739: fun show_pt pt = wenzelm@5692: 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 berghofe@1580: (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@3779: fun read_typ syn get_sort str = wenzelm@5692: (case read syn SynExt.typeT str of wenzelm@5692: [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) t wenzelm@2585: | _ => error "read_typ: ambiguous type syntax"); wenzelm@144: wenzelm@2585: fun simple_read_typ str = wenzelm@2585: let fun get_sort env xi = if_none (assoc (env, xi)) [] in wenzelm@3779: read_typ type_syn get_sort str wenzelm@2585: end; wenzelm@144: wenzelm@144: 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@5692: if x mem consts orelse NameSpace.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) wenzelm@5692: (lookup_tokentr tokentrtab (! Printer.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@2202: fun ext_syntax mk_syn_ext prmode (syn as Syntax {logtypes, ...}) decls = wenzelm@2202: extend_syntax prmode syn (mk_syn_ext logtypes decls); wenzelm@383: wenzelm@167: clasohm@764: fun extend_log_types syn logtypes = 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@5692: fun extend_const_gram syn prmode = ext_syntax Mixfix.syn_ext_consts prmode syn; 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@1158: fun extend_trrules syn rules = wenzelm@5692: ext_syntax SynExt.syn_ext_rules ("", true) syn (prep_rules (read_pattern syn) rules); wenzelm@1158: wenzelm@1158: fun extend_trrules_i syn rules = wenzelm@5692: ext_syntax SynExt.syn_ext_rules ("", true) syn (prep_rules I rules); wenzelm@5692: wenzelm@5692: wenzelm@5692: wenzelm@5692: (** export parts of internal Syntax structures **) wenzelm@5692: wenzelm@5692: open 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;