# HG changeset patch # User wenzelm # Date 1120050823 -7200 # Node ID 76e57e08dcb5f463029c2db4f512f58e08842ec0 # Parent 48be8ef738df6c5ed16ec8a447db83d2120eaaf1 proper treatment of advanced trfuns: pass thy argument; tuned warning; diff -r 48be8ef738df -r 76e57e08dcb5 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Wed Jun 29 15:13:42 2005 +0200 +++ b/src/Pure/Syntax/syntax.ML Wed Jun 29 15:13:43 2005 +0200 @@ -46,9 +46,14 @@ (string * ((term list -> term) * stamp)) list * (string * ((bool -> typ -> term list -> term) * stamp)) list * (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax + val extend_advanced_trfuns: + (string * ((theory -> ast list -> ast) * stamp)) list * + (string * ((theory -> term list -> term) * stamp)) list * + (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list * + (string * ((theory -> ast list -> ast) * stamp)) list -> syntax -> syntax val extend_tokentrfuns: (string * string * (string -> string * real)) list -> syntax -> syntax val extend_trrules_i: ast trrule list -> syntax -> syntax - val extend_trrules: (string -> bool) -> syntax -> + val extend_trrules: theory -> (string -> bool) -> syntax -> (string * string) trrule list -> syntax -> syntax val remove_const_gram: (string -> bool) -> string * bool -> (string * typ * mixfix) list -> syntax -> syntax @@ -59,14 +64,13 @@ val print_gram: syntax -> unit val print_trans: syntax -> unit val print_syntax: syntax -> unit - val read: (string -> bool) -> syntax -> typ -> string -> term list - val read_typ: syntax -> ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) -> - string -> typ - val read_sort: syntax -> string -> sort - val pretty_term: syntax -> bool -> term -> Pretty.T - val pretty_typ: syntax -> typ -> Pretty.T - val pretty_sort: syntax -> sort -> Pretty.T - val simple_pprint_typ: typ -> pprint_args -> unit + val read: theory -> (string -> bool) -> syntax -> typ -> string -> term list + val read_typ: theory -> syntax -> ((indexname * sort) list -> indexname -> sort) -> + (sort -> sort) -> string -> typ + val read_sort: theory -> syntax -> string -> sort + val pretty_term: theory -> syntax -> bool -> term -> Pretty.T + val pretty_typ: theory -> syntax -> typ -> Pretty.T + val pretty_sort: theory -> syntax -> sort -> Pretty.T val ambiguity_level: int ref val ambiguity_is_error: bool ref end; @@ -164,12 +168,12 @@ gram: Parser.gram, consts: string list, prmodes: string list, - parse_ast_trtab: ((Ast.ast list -> Ast.ast) * stamp) Symtab.table, + parse_ast_trtab: ((theory -> Ast.ast list -> Ast.ast) * stamp) Symtab.table, parse_ruletab: ruletab, - parse_trtab: ((term list -> term) * stamp) Symtab.table, - print_trtab: ((bool -> typ -> term list -> term) * stamp) list Symtab.table, + parse_trtab: ((theory -> term list -> term) * stamp) Symtab.table, + print_trtab: ((theory -> bool -> typ -> term list -> term) * stamp) list Symtab.table, print_ruletab: ruletab, - print_ast_trtab: ((Ast.ast list -> Ast.ast) * stamp) list Symtab.table, + print_ast_trtab: ((theory -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table, tokentrtab: (string * (string * ((string -> string * real) * stamp)) list) list, prtabs: Printer.prtabs} @@ -353,7 +357,7 @@ val ambiguity_level = ref 1; val ambiguity_is_error = ref false -fun read_asts is_logtype (Syntax tabs) xids root str = +fun read_asts thy is_logtype (Syntax tabs) xids root str = let val {lexicon, gram, parse_ast_trtab, ...} = tabs; val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root; @@ -361,44 +365,40 @@ val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars); fun show_pt pt = - warning (Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts (K NONE) [pt])))); + Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts thy (K NONE) [pt]))); in - if length pts > ! ambiguity_level then - if ! ambiguity_is_error then - error ("Ambiguous input " ^ quote str) - else - (warning ("Ambiguous input " ^ quote str); - warning "produces the following parse trees:"; - List.app show_pt pts) - else (); - SynTrans.pts_to_asts (lookup_tr parse_ast_trtab) pts + conditional (length pts > ! ambiguity_level) (fn () => + if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str) + else warning (cat_lines ("Ambiguous input " ^ quote str :: + "produces the following parse trees:" :: map show_pt pts))); + SynTrans.pts_to_asts thy (lookup_tr parse_ast_trtab) pts end; (* read *) -fun read is_logtype (syn as Syntax tabs) ty str = +fun read thy is_logtype (syn as Syntax tabs) ty str = let val {parse_ruletab, parse_trtab, ...} = tabs; - val asts = read_asts is_logtype syn false (SynExt.typ_to_nonterm ty) str; + val asts = read_asts thy is_logtype syn false (SynExt.typ_to_nonterm ty) str; in - SynTrans.asts_to_terms (lookup_tr parse_trtab) + SynTrans.asts_to_terms thy (lookup_tr parse_trtab) (map (Ast.normalize_ast (lookup_ruletab parse_ruletab)) asts) end; (* read types *) -fun read_typ syn get_sort map_sort str = - (case read (K false) syn SynExt.typeT str of +fun read_typ thy syn get_sort map_sort str = + (case read thy (K false) syn SynExt.typeT str of [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) map_sort t | _ => error "read_typ: ambiguous syntax"); (* read sorts *) -fun read_sort syn str = - (case read (K false) syn TypeExt.sortT str of +fun read_sort thy syn str = + (case read thy (K false) syn TypeExt.sortT str of [t] => TypeExt.sort_of_term t | _ => error "read_sort: ambiguous syntax"); @@ -432,7 +432,7 @@ | NONE => rule); -fun read_pattern is_logtype syn (root, str) = +fun read_pattern thy is_logtype syn (root, str) = let val Syntax {consts, ...} = syn; @@ -442,7 +442,7 @@ else ast | constify (Ast.Appl asts) = Ast.Appl (map constify asts); in - (case read_asts is_logtype syn true root str of + (case read_asts thy is_logtype syn true root str of [ast] => constify ast | _ => error ("Syntactically ambiguous input: " ^ quote str)) end handle ERROR => @@ -460,21 +460,19 @@ (** pretty terms, typs, sorts **) -fun pretty_t t_to_ast prt_t (syn as Syntax tabs) curried t = +fun pretty_t t_to_ast prt_t thy (syn as Syntax tabs) curried t = let val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs; - val ast = t_to_ast (lookup_tr' print_trtab) t; + val ast = t_to_ast thy (lookup_tr' print_trtab) t; in - prt_t curried prtabs (lookup_tr' print_ast_trtab) + prt_t thy curried prtabs (lookup_tr' print_ast_trtab) (lookup_tokentr tokentrtab (! print_mode)) (Ast.normalize_ast (lookup_ruletab print_ruletab) ast) end; val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast; -fun pretty_typ syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast syn false; -fun pretty_sort syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast syn false; - -val simple_pprint_typ = Pretty.pprint o Pretty.quote o (pretty_typ type_syn); +fun pretty_typ thy syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast thy syn false; +fun pretty_sort thy syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast thy syn false; @@ -483,16 +481,17 @@ fun ext_syntax' f is_logtype prmode decls = extend_syntax prmode (f is_logtype decls); fun ext_syntax f = ext_syntax' (K f) (K false) default_mode; -val extend_type_gram = ext_syntax Mixfix.syn_ext_types; -val extend_const_gram = ext_syntax' Mixfix.syn_ext_consts; -val extend_consts = ext_syntax SynExt.syn_ext_const_names; -val extend_trfuns = ext_syntax SynExt.syn_ext_trfuns; -val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns; -val extend_trrules_i = ext_syntax SynExt.syn_ext_rules o prep_rules I; +val extend_type_gram = ext_syntax Mixfix.syn_ext_types; +val extend_const_gram = ext_syntax' Mixfix.syn_ext_consts; +val extend_consts = ext_syntax SynExt.syn_ext_const_names; +val extend_trfuns = ext_syntax SynExt.syn_ext_trfuns; +val extend_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns; +val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns; +val extend_trrules_i = ext_syntax SynExt.syn_ext_rules o prep_rules I; -fun extend_trrules is_logtype syn rules = +fun extend_trrules thy is_logtype syn rules = ext_syntax' (K SynExt.syn_ext_rules) (K false) default_mode - (prep_rules (read_pattern is_logtype syn) rules); + (prep_rules (read_pattern thy is_logtype syn) rules); fun remove_const_gram is_logtype prmode decls = remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);