1.1 --- a/src/Pure/Syntax/syntax.ML Sun Sep 05 21:41:24 2010 +0200
1.2 +++ b/src/Pure/Syntax/syntax.ML Sun Sep 05 22:15:50 2010 +0200
1.3 @@ -22,65 +22,7 @@
1.4 include SYN_TRANS1
1.5 include MIXFIX1
1.6 include PRINTER0
1.7 - type syntax
1.8 - val eq_syntax: syntax * syntax -> bool
1.9 - val is_keyword: syntax -> string -> bool
1.10 - type mode
1.11 - val mode_default: mode
1.12 - val mode_input: mode
1.13 - val merge_syntaxes: syntax -> syntax -> syntax
1.14 - val basic_syntax: syntax
1.15 - val basic_nonterms: string list
1.16 - val print_gram: syntax -> unit
1.17 - val print_trans: syntax -> unit
1.18 - val print_syntax: syntax -> unit
1.19 - val guess_infix: syntax -> string -> mixfix option
1.20 val read_token: string -> Symbol_Pos.T list * Position.T
1.21 - val ambiguity_enabled: bool Config.T
1.22 - val ambiguity_level_value: Config.value Config.T
1.23 - val ambiguity_level: int Config.T
1.24 - val ambiguity_limit: int Config.T
1.25 - val standard_parse_term: Pretty.pp -> (term -> string option) ->
1.26 - (((string * int) * sort) list -> string * int -> Term.sort) ->
1.27 - (string -> bool * string) -> (string -> string option) -> Proof.context ->
1.28 - (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
1.29 - val standard_parse_typ: Proof.context -> syntax ->
1.30 - ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
1.31 - val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
1.32 - datatype 'a trrule =
1.33 - ParseRule of 'a * 'a |
1.34 - PrintRule of 'a * 'a |
1.35 - ParsePrintRule of 'a * 'a
1.36 - val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
1.37 - val is_const: syntax -> string -> bool
1.38 - val standard_unparse_term: {structs: string list, fixes: string list} ->
1.39 - {extern_class: string -> xstring, extern_type: string -> xstring,
1.40 - extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
1.41 - val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
1.42 - Proof.context -> syntax -> typ -> Pretty.T
1.43 - val standard_unparse_sort: {extern_class: string -> xstring} ->
1.44 - Proof.context -> syntax -> sort -> Pretty.T
1.45 - val update_trfuns:
1.46 - (string * ((ast list -> ast) * stamp)) list *
1.47 - (string * ((term list -> term) * stamp)) list *
1.48 - (string * ((bool -> typ -> term list -> term) * stamp)) list *
1.49 - (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax
1.50 - val update_advanced_trfuns:
1.51 - (string * ((Proof.context -> ast list -> ast) * stamp)) list *
1.52 - (string * ((Proof.context -> term list -> term) * stamp)) list *
1.53 - (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
1.54 - (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
1.55 - val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
1.56 - syntax -> syntax
1.57 - val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
1.58 - val update_const_gram: bool -> (string -> bool) ->
1.59 - mode -> (string * typ * mixfix) list -> syntax -> syntax
1.60 - val update_trrules: Proof.context -> (string -> bool) -> syntax ->
1.61 - (string * string) trrule list -> syntax -> syntax
1.62 - val remove_trrules: Proof.context -> (string -> bool) -> syntax ->
1.63 - (string * string) trrule list -> syntax -> syntax
1.64 - val update_trrules_i: ast trrule list -> syntax -> syntax
1.65 - val remove_trrules_i: ast trrule list -> syntax -> syntax
1.66 val parse_token: Proof.context -> Markup.T -> string -> Symbol_Pos.T list * Position.T
1.67 val parse_sort: Proof.context -> string -> sort
1.68 val parse_typ: Proof.context -> string -> typ
1.69 @@ -155,306 +97,70 @@
1.70 val string_of_sort_global: theory -> sort -> string
1.71 val pp: Proof.context -> Pretty.pp
1.72 val pp_global: theory -> Pretty.pp
1.73 + type syntax
1.74 + val eq_syntax: syntax * syntax -> bool
1.75 + val is_keyword: syntax -> string -> bool
1.76 + type mode
1.77 + val mode_default: mode
1.78 + val mode_input: mode
1.79 + val merge_syntaxes: syntax -> syntax -> syntax
1.80 + val basic_syntax: syntax
1.81 + val basic_nonterms: string list
1.82 + val print_gram: syntax -> unit
1.83 + val print_trans: syntax -> unit
1.84 + val print_syntax: syntax -> unit
1.85 + val guess_infix: syntax -> string -> mixfix option
1.86 + val ambiguity_enabled: bool Config.T
1.87 + val ambiguity_level_value: Config.value Config.T
1.88 + val ambiguity_level: int Config.T
1.89 + val ambiguity_limit: int Config.T
1.90 + val standard_parse_term: Pretty.pp -> (term -> string option) ->
1.91 + (((string * int) * sort) list -> string * int -> Term.sort) ->
1.92 + (string -> bool * string) -> (string -> string option) -> Proof.context ->
1.93 + (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
1.94 + val standard_parse_typ: Proof.context -> syntax ->
1.95 + ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
1.96 + val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
1.97 + datatype 'a trrule =
1.98 + ParseRule of 'a * 'a |
1.99 + PrintRule of 'a * 'a |
1.100 + ParsePrintRule of 'a * 'a
1.101 + val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
1.102 + val is_const: syntax -> string -> bool
1.103 + val standard_unparse_term: {structs: string list, fixes: string list} ->
1.104 + {extern_class: string -> xstring, extern_type: string -> xstring,
1.105 + extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
1.106 + val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
1.107 + Proof.context -> syntax -> typ -> Pretty.T
1.108 + val standard_unparse_sort: {extern_class: string -> xstring} ->
1.109 + Proof.context -> syntax -> sort -> Pretty.T
1.110 + val update_trfuns:
1.111 + (string * ((ast list -> ast) * stamp)) list *
1.112 + (string * ((term list -> term) * stamp)) list *
1.113 + (string * ((bool -> typ -> term list -> term) * stamp)) list *
1.114 + (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax
1.115 + val update_advanced_trfuns:
1.116 + (string * ((Proof.context -> ast list -> ast) * stamp)) list *
1.117 + (string * ((Proof.context -> term list -> term) * stamp)) list *
1.118 + (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
1.119 + (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
1.120 + val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
1.121 + syntax -> syntax
1.122 + val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
1.123 + val update_const_gram: bool -> (string -> bool) ->
1.124 + mode -> (string * typ * mixfix) list -> syntax -> syntax
1.125 + val update_trrules: Proof.context -> (string -> bool) -> syntax ->
1.126 + (string * string) trrule list -> syntax -> syntax
1.127 + val remove_trrules: Proof.context -> (string -> bool) -> syntax ->
1.128 + (string * string) trrule list -> syntax -> syntax
1.129 + val update_trrules_i: ast trrule list -> syntax -> syntax
1.130 + val remove_trrules_i: ast trrule list -> syntax -> syntax
1.131 end;
1.132
1.133 structure Syntax: SYNTAX =
1.134 struct
1.135
1.136 -(** tables of translation functions **)
1.137 -
1.138 -(* parse (ast) translations *)
1.139 -
1.140 -fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
1.141 -
1.142 -fun err_dup_trfun name c =
1.143 - error ("More than one " ^ name ^ " for " ^ quote c);
1.144 -
1.145 -fun remove_trtab trfuns = fold (Symtab.remove Syn_Ext.eq_trfun) trfuns;
1.146 -
1.147 -fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
1.148 - handle Symtab.DUP c => err_dup_trfun name c;
1.149 -
1.150 -fun merge_trtabs name tab1 tab2 = Symtab.merge Syn_Ext.eq_trfun (tab1, tab2)
1.151 - handle Symtab.DUP c => err_dup_trfun name c;
1.152 -
1.153 -
1.154 -(* print (ast) translations *)
1.155 -
1.156 -fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
1.157 -fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
1.158 -fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
1.159 -fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2);
1.160 -
1.161 -
1.162 -
1.163 -(** tables of token translation functions **)
1.164 -
1.165 -fun lookup_tokentr tabs modes =
1.166 - let val trs = distinct (eq_fst (op =)) (maps (these o AList.lookup (op =) tabs) (modes @ [""]))
1.167 - in fn c => Option.map fst (AList.lookup (op =) trs c) end;
1.168 -
1.169 -fun merge_tokentrtabs tabs1 tabs2 =
1.170 - let
1.171 - fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
1.172 -
1.173 - fun name (s, _) = implode (tl (Symbol.explode s));
1.174 -
1.175 - fun merge mode =
1.176 - let
1.177 - val trs1 = these (AList.lookup (op =) tabs1 mode);
1.178 - val trs2 = these (AList.lookup (op =) tabs2 mode);
1.179 - val trs = distinct eq_tr (trs1 @ trs2);
1.180 - in
1.181 - (case duplicates (eq_fst (op =)) trs of
1.182 - [] => (mode, trs)
1.183 - | dups => error ("More than one token translation function in mode " ^
1.184 - quote mode ^ " for " ^ commas_quote (map name dups)))
1.185 - end;
1.186 - in map merge (distinct (op =) (map fst (tabs1 @ tabs2))) end;
1.187 -
1.188 -fun extend_tokentrtab tokentrs tabs =
1.189 - let
1.190 - fun ins_tokentr (m, c, f) =
1.191 - AList.default (op =) (m, [])
1.192 - #> AList.map_entry (op =) m (cons ("_" ^ c, (f, stamp ())));
1.193 - in merge_tokentrtabs tabs (fold ins_tokentr tokentrs []) end;
1.194 -
1.195 -
1.196 -
1.197 -(** tables of translation rules **)
1.198 -
1.199 -type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
1.200 -
1.201 -fun dest_ruletab tab = maps snd (Symtab.dest tab);
1.202 -
1.203 -
1.204 -(* empty, update, merge ruletabs *)
1.205 -
1.206 -val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.head_of_rule r, r));
1.207 -val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r));
1.208 -fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2);
1.209 -
1.210 -
1.211 -
1.212 -(** datatype syntax **)
1.213 -
1.214 -datatype syntax =
1.215 - Syntax of {
1.216 - input: Syn_Ext.xprod list,
1.217 - lexicon: Scan.lexicon,
1.218 - gram: Parser.gram,
1.219 - consts: string list,
1.220 - prmodes: string list,
1.221 - parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
1.222 - parse_ruletab: ruletab,
1.223 - parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table,
1.224 - print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
1.225 - print_ruletab: ruletab,
1.226 - print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
1.227 - tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list,
1.228 - prtabs: Printer.prtabs} * stamp;
1.229 -
1.230 -fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
1.231 -
1.232 -fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
1.233 -
1.234 -type mode = string * bool;
1.235 -val mode_default = ("", true);
1.236 -val mode_input = (Print_Mode.input, true);
1.237 -
1.238 -
1.239 -(* empty_syntax *)
1.240 -
1.241 -val empty_syntax = Syntax
1.242 - ({input = [],
1.243 - lexicon = Scan.empty_lexicon,
1.244 - gram = Parser.empty_gram,
1.245 - consts = [],
1.246 - prmodes = [],
1.247 - parse_ast_trtab = Symtab.empty,
1.248 - parse_ruletab = Symtab.empty,
1.249 - parse_trtab = Symtab.empty,
1.250 - print_trtab = Symtab.empty,
1.251 - print_ruletab = Symtab.empty,
1.252 - print_ast_trtab = Symtab.empty,
1.253 - tokentrtab = [],
1.254 - prtabs = Printer.empty_prtabs}, stamp ());
1.255 -
1.256 -
1.257 -(* update_syntax *)
1.258 -
1.259 -fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
1.260 - let
1.261 - val {input, lexicon, gram, consts = consts1, prmodes = prmodes1,
1.262 - parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
1.263 - print_ast_trtab, tokentrtab, prtabs} = tabs;
1.264 - val Syn_Ext.Syn_Ext {xprods, consts = consts2, prmodes = prmodes2,
1.265 - parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
1.266 - print_ast_translation, token_translation} = syn_ext;
1.267 - val new_xprods =
1.268 - if inout then distinct (op =) (filter_out (member (op =) input) xprods) else [];
1.269 - fun if_inout xs = if inout then xs else [];
1.270 - in
1.271 - Syntax
1.272 - ({input = new_xprods @ input,
1.273 - lexicon = fold Scan.extend_lexicon (Syn_Ext.delims_of new_xprods) lexicon,
1.274 - gram = Parser.extend_gram new_xprods gram,
1.275 - consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
1.276 - prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
1.277 - parse_ast_trtab =
1.278 - update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
1.279 - parse_ruletab = update_ruletab (if_inout parse_rules) parse_ruletab,
1.280 - parse_trtab = update_trtab "parse translation" (if_inout parse_translation) parse_trtab,
1.281 - print_trtab = update_tr'tab print_translation print_trtab,
1.282 - print_ruletab = update_ruletab print_rules print_ruletab,
1.283 - print_ast_trtab = update_tr'tab print_ast_translation print_ast_trtab,
1.284 - tokentrtab = extend_tokentrtab token_translation tokentrtab,
1.285 - prtabs = Printer.update_prtabs mode xprods prtabs}, stamp ())
1.286 - end;
1.287 -
1.288 -
1.289 -(* remove_syntax *)
1.290 -
1.291 -fun remove_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
1.292 - let
1.293 - val Syn_Ext.Syn_Ext {xprods, consts = _, prmodes = _,
1.294 - parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
1.295 - print_ast_translation, token_translation = _} = syn_ext;
1.296 - val {input, lexicon, gram, consts, prmodes,
1.297 - parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
1.298 - print_ast_trtab, tokentrtab, prtabs} = tabs;
1.299 - val input' = if inout then subtract (op =) xprods input else input;
1.300 - val changed = length input <> length input';
1.301 - fun if_inout xs = if inout then xs else [];
1.302 - in
1.303 - Syntax
1.304 - ({input = input',
1.305 - lexicon = if changed then Scan.make_lexicon (Syn_Ext.delims_of input') else lexicon,
1.306 - gram = if changed then Parser.make_gram input' else gram,
1.307 - consts = consts,
1.308 - prmodes = prmodes,
1.309 - parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab,
1.310 - parse_ruletab = remove_ruletab (if_inout parse_rules) parse_ruletab,
1.311 - parse_trtab = remove_trtab (if_inout parse_translation) parse_trtab,
1.312 - print_trtab = remove_tr'tab print_translation print_trtab,
1.313 - print_ruletab = remove_ruletab print_rules print_ruletab,
1.314 - print_ast_trtab = remove_tr'tab print_ast_translation print_ast_trtab,
1.315 - tokentrtab = tokentrtab,
1.316 - prtabs = Printer.remove_prtabs mode xprods prtabs}, stamp ())
1.317 - end;
1.318 -
1.319 -
1.320 -(* merge_syntaxes *)
1.321 -
1.322 -fun merge_syntaxes (Syntax (tabs1, _)) (Syntax (tabs2, _)) =
1.323 - let
1.324 - val {input = input1, lexicon = lexicon1, gram = gram1, consts = consts1,
1.325 - prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1,
1.326 - parse_ruletab = parse_ruletab1, parse_trtab = parse_trtab1,
1.327 - print_trtab = print_trtab1, print_ruletab = print_ruletab1,
1.328 - print_ast_trtab = print_ast_trtab1, tokentrtab = tokentrtab1, prtabs = prtabs1} = tabs1;
1.329 -
1.330 - val {input = input2, lexicon = lexicon2, gram = gram2, consts = consts2,
1.331 - prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2,
1.332 - parse_ruletab = parse_ruletab2, parse_trtab = parse_trtab2,
1.333 - print_trtab = print_trtab2, print_ruletab = print_ruletab2,
1.334 - print_ast_trtab = print_ast_trtab2, tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2;
1.335 - in
1.336 - Syntax
1.337 - ({input = Library.merge (op =) (input1, input2),
1.338 - lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
1.339 - gram = Parser.merge_gram (gram1, gram2),
1.340 - consts = sort_distinct string_ord (consts1 @ consts2),
1.341 - prmodes = Library.merge (op =) (prmodes1, prmodes2),
1.342 - parse_ast_trtab =
1.343 - merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
1.344 - parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,
1.345 - parse_trtab = merge_trtabs "parse translation" parse_trtab1 parse_trtab2,
1.346 - print_trtab = merge_tr'tabs print_trtab1 print_trtab2,
1.347 - print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2,
1.348 - print_ast_trtab = merge_tr'tabs print_ast_trtab1 print_ast_trtab2,
1.349 - tokentrtab = merge_tokentrtabs tokentrtab1 tokentrtab2,
1.350 - prtabs = Printer.merge_prtabs prtabs1 prtabs2}, stamp ())
1.351 - end;
1.352 -
1.353 -
1.354 -(* basic syntax *)
1.355 -
1.356 -val basic_syntax =
1.357 - empty_syntax
1.358 - |> update_syntax mode_default Type_Ext.type_ext
1.359 - |> update_syntax mode_default Syn_Ext.pure_ext;
1.360 -
1.361 -val basic_nonterms =
1.362 - (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
1.363 - Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
1.364 - "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const",
1.365 - "index", "struct"]);
1.366 -
1.367 -
1.368 -
1.369 -(** print syntax **)
1.370 -
1.371 -local
1.372 -
1.373 -fun pretty_strs_qs name strs =
1.374 - Pretty.strs (name :: map quote (sort_strings strs));
1.375 -
1.376 -fun pretty_gram (Syntax (tabs, _)) =
1.377 - let
1.378 - val {lexicon, prmodes, gram, ...} = tabs;
1.379 - val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes);
1.380 - in
1.381 - [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
1.382 - Pretty.big_list "prods:" (Parser.pretty_gram gram),
1.383 - pretty_strs_qs "print modes:" prmodes']
1.384 - end;
1.385 -
1.386 -fun pretty_trans (Syntax (tabs, _)) =
1.387 - let
1.388 - fun pretty_trtab name tab =
1.389 - pretty_strs_qs name (Symtab.keys tab);
1.390 -
1.391 - fun pretty_ruletab name tab =
1.392 - Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab));
1.393 -
1.394 - fun pretty_tokentr (mode, trs) = Pretty.strs (quote mode ^ ":" :: map fst trs);
1.395 -
1.396 - val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
1.397 - print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs;
1.398 - in
1.399 - [pretty_strs_qs "consts:" consts,
1.400 - pretty_trtab "parse_ast_translation:" parse_ast_trtab,
1.401 - pretty_ruletab "parse_rules:" parse_ruletab,
1.402 - pretty_trtab "parse_translation:" parse_trtab,
1.403 - pretty_trtab "print_translation:" print_trtab,
1.404 - pretty_ruletab "print_rules:" print_ruletab,
1.405 - pretty_trtab "print_ast_translation:" print_ast_trtab,
1.406 - Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab)]
1.407 - end;
1.408 -
1.409 -in
1.410 -
1.411 -fun print_gram syn = Pretty.writeln (Pretty.chunks (pretty_gram syn));
1.412 -fun print_trans syn = Pretty.writeln (Pretty.chunks (pretty_trans syn));
1.413 -fun print_syntax syn = Pretty.writeln (Pretty.chunks (pretty_gram syn @ pretty_trans syn));
1.414 -
1.415 -end;
1.416 -
1.417 -
1.418 -(* reconstructing infixes -- educated guessing *)
1.419 -
1.420 -fun guess_infix (Syntax ({gram, ...}, _)) c =
1.421 - (case Parser.guess_infix_lr gram c of
1.422 - SOME (s, l, r, j) => SOME
1.423 - (if l then Mixfix.Infixl (s, j)
1.424 - else if r then Mixfix.Infixr (s, j)
1.425 - else Mixfix.Infix (s, j))
1.426 - | NONE => NONE);
1.427 -
1.428 -
1.429 -
1.430 -(** read **)
1.431 +(** inner syntax operations **)
1.432
1.433 (* read token -- with optional YXML encoding of position *)
1.434
1.435 @@ -471,234 +177,6 @@
1.436 in (Symbol_Pos.explode (text, pos), pos) end;
1.437
1.438
1.439 -(* read_ast *)
1.440 -
1.441 -val ambiguity_enabled =
1.442 - Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
1.443 -
1.444 -val ambiguity_level_value = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1);
1.445 -val ambiguity_level = Config.int ambiguity_level_value;
1.446 -
1.447 -val ambiguity_limit =
1.448 - Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
1.449 -
1.450 -fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
1.451 -
1.452 -fun read_asts ctxt is_logtype (Syntax (tabs, _)) xids root (syms, pos) =
1.453 - let
1.454 - val {lexicon, gram, parse_ast_trtab, ...} = tabs;
1.455 - val toks = Lexicon.tokenize lexicon xids syms;
1.456 - val _ = List.app (Lexicon.report_token ctxt) toks;
1.457 -
1.458 - val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
1.459 - val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks);
1.460 - val len = length pts;
1.461 -
1.462 - val limit = Config.get ctxt ambiguity_limit;
1.463 - fun show_pt pt =
1.464 - Pretty.string_of (Ast.pretty_ast (hd (Syn_Trans.pts_to_asts ctxt (K NONE) [pt])));
1.465 - in
1.466 - if len <= Config.get ctxt ambiguity_level then ()
1.467 - else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
1.468 - else
1.469 - (Context_Position.if_visible ctxt warning (cat_lines
1.470 - (("Ambiguous input" ^ Position.str_of pos ^
1.471 - "\nproduces " ^ string_of_int len ^ " parse trees" ^
1.472 - (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
1.473 - map show_pt (take limit pts))));
1.474 - Syn_Trans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
1.475 - end;
1.476 -
1.477 -
1.478 -(* read *)
1.479 -
1.480 -fun read ctxt is_logtype (syn as Syntax (tabs, _)) ty inp =
1.481 - let
1.482 - val {parse_ruletab, parse_trtab, ...} = tabs;
1.483 - val asts = read_asts ctxt is_logtype syn false (Syn_Ext.typ_to_nonterm ty) inp;
1.484 - in
1.485 - Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
1.486 - (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
1.487 - end;
1.488 -
1.489 -
1.490 -(* read terms *)
1.491 -
1.492 -(*brute-force disambiguation via type-inference*)
1.493 -fun disambig _ _ _ [t] = t
1.494 - | disambig ctxt pp check ts =
1.495 - let
1.496 - val level = Config.get ctxt ambiguity_level;
1.497 - val limit = Config.get ctxt ambiguity_limit;
1.498 -
1.499 - val ambiguity = length ts;
1.500 - fun ambig_msg () =
1.501 - if ambiguity > 1 andalso ambiguity <= level then
1.502 - "Got more than one parse tree.\n\
1.503 - \Retry with smaller syntax_ambiguity_level for more information."
1.504 - else "";
1.505 -
1.506 - val errs = Par_List.map check ts;
1.507 - val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
1.508 - val len = length results;
1.509 - in
1.510 - if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
1.511 - else if len = 1 then
1.512 - (if ambiguity > level then
1.513 - Context_Position.if_visible ctxt warning
1.514 - "Fortunately, only one parse tree is type correct.\n\
1.515 - \You may still want to disambiguate your grammar or your input."
1.516 - else (); hd results)
1.517 - else cat_error (ambig_msg ()) (cat_lines
1.518 - (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
1.519 - (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
1.520 - map (Pretty.string_of_term pp) (take limit results)))
1.521 - end;
1.522 -
1.523 -fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
1.524 - read ctxt is_logtype syn ty (syms, pos)
1.525 - |> map (Type_Ext.decode_term get_sort map_const map_free)
1.526 - |> disambig ctxt (Printer.pp_show_brackets pp) check;
1.527 -
1.528 -
1.529 -(* read types *)
1.530 -
1.531 -fun standard_parse_typ ctxt syn get_sort (syms, pos) =
1.532 - (case read ctxt (K false) syn Syn_Ext.typeT (syms, pos) of
1.533 - [t] => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t
1.534 - | _ => error (ambiguity_msg pos));
1.535 -
1.536 -
1.537 -(* read sorts *)
1.538 -
1.539 -fun standard_parse_sort ctxt syn (syms, pos) =
1.540 - (case read ctxt (K false) syn Type_Ext.sortT (syms, pos) of
1.541 - [t] => Type_Ext.sort_of_term t
1.542 - | _ => error (ambiguity_msg pos));
1.543 -
1.544 -
1.545 -
1.546 -(** prepare translation rules **)
1.547 -
1.548 -datatype 'a trrule =
1.549 - ParseRule of 'a * 'a |
1.550 - PrintRule of 'a * 'a |
1.551 - ParsePrintRule of 'a * 'a;
1.552 -
1.553 -fun map_trrule f (ParseRule (x, y)) = ParseRule (f x, f y)
1.554 - | map_trrule f (PrintRule (x, y)) = PrintRule (f x, f y)
1.555 - | map_trrule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y);
1.556 -
1.557 -fun parse_rule (ParseRule pats) = SOME pats
1.558 - | parse_rule (PrintRule _) = NONE
1.559 - | parse_rule (ParsePrintRule pats) = SOME pats;
1.560 -
1.561 -fun print_rule (ParseRule _) = NONE
1.562 - | print_rule (PrintRule pats) = SOME (swap pats)
1.563 - | print_rule (ParsePrintRule pats) = SOME (swap pats);
1.564 -
1.565 -
1.566 -fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
1.567 -
1.568 -local
1.569 -
1.570 -fun check_rule (rule as (lhs, rhs)) =
1.571 - (case Ast.rule_error rule of
1.572 - SOME msg =>
1.573 - error ("Error in syntax translation rule: " ^ msg ^ "\n" ^
1.574 - Ast.str_of_ast lhs ^ " -> " ^ Ast.str_of_ast rhs)
1.575 - | NONE => rule);
1.576 -
1.577 -fun read_pattern ctxt is_logtype syn (root, str) =
1.578 - let
1.579 - fun constify (ast as Ast.Constant _) = ast
1.580 - | constify (ast as Ast.Variable x) =
1.581 - if is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
1.582 - else ast
1.583 - | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
1.584 -
1.585 - val (syms, pos) = read_token str;
1.586 - in
1.587 - (case read_asts ctxt is_logtype syn true root (syms, pos) of
1.588 - [ast] => constify ast
1.589 - | _ => error (ambiguity_msg pos))
1.590 - end;
1.591 -
1.592 -fun prep_rules rd_pat raw_rules =
1.593 - let val rules = map (map_trrule rd_pat) raw_rules in
1.594 - (map check_rule (map_filter parse_rule rules),
1.595 - map check_rule (map_filter print_rule rules))
1.596 - end
1.597 -
1.598 -in
1.599 -
1.600 -val cert_rules = prep_rules I;
1.601 -
1.602 -fun read_rules ctxt is_logtype syn =
1.603 - prep_rules (read_pattern ctxt is_logtype syn);
1.604 -
1.605 -end;
1.606 -
1.607 -
1.608 -
1.609 -(** unparse terms, typs, sorts **)
1.610 -
1.611 -local
1.612 -
1.613 -fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
1.614 - let
1.615 - val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
1.616 - val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
1.617 - in
1.618 - Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
1.619 - (lookup_tokentr tokentrtab (print_mode_value ()))
1.620 - (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast))
1.621 - end;
1.622 -
1.623 -in
1.624 -
1.625 -fun standard_unparse_term idents extern =
1.626 - unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
1.627 -
1.628 -fun standard_unparse_typ extern ctxt syn =
1.629 - unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
1.630 -
1.631 -fun standard_unparse_sort {extern_class} ctxt syn =
1.632 - unparse_t (K Printer.sort_to_ast)
1.633 - (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
1.634 - Markup.sort ctxt syn false;
1.635 -
1.636 -end;
1.637 -
1.638 -
1.639 -
1.640 -(** modify syntax **)
1.641 -
1.642 -fun ext_syntax f decls = update_syntax mode_default (f decls);
1.643 -
1.644 -val update_trfuns = ext_syntax Syn_Ext.syn_ext_trfuns;
1.645 -val update_advanced_trfuns = ext_syntax Syn_Ext.syn_ext_advanced_trfuns;
1.646 -val extend_tokentrfuns = ext_syntax Syn_Ext.syn_ext_tokentrfuns;
1.647 -
1.648 -fun update_type_gram add prmode decls =
1.649 - (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
1.650 -
1.651 -fun update_const_gram add is_logtype prmode decls =
1.652 - (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
1.653 -
1.654 -fun update_trrules ctxt is_logtype syn =
1.655 - ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
1.656 -
1.657 -fun remove_trrules ctxt is_logtype syn =
1.658 - remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
1.659 -
1.660 -val update_trrules_i = ext_syntax Syn_Ext.syn_ext_rules o cert_rules;
1.661 -val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules;
1.662 -
1.663 -
1.664 -
1.665 -(** inner syntax operations **)
1.666 -
1.667 (* (un)parsing *)
1.668
1.669 fun parse_token ctxt markup str =
1.670 @@ -914,6 +392,528 @@
1.671 fn x => pretty_arity (init_pretty_global thy) x);
1.672
1.673
1.674 +
1.675 +(** tables of translation functions **)
1.676 +
1.677 +(* parse (ast) translations *)
1.678 +
1.679 +fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
1.680 +
1.681 +fun err_dup_trfun name c =
1.682 + error ("More than one " ^ name ^ " for " ^ quote c);
1.683 +
1.684 +fun remove_trtab trfuns = fold (Symtab.remove Syn_Ext.eq_trfun) trfuns;
1.685 +
1.686 +fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
1.687 + handle Symtab.DUP c => err_dup_trfun name c;
1.688 +
1.689 +fun merge_trtabs name tab1 tab2 = Symtab.merge Syn_Ext.eq_trfun (tab1, tab2)
1.690 + handle Symtab.DUP c => err_dup_trfun name c;
1.691 +
1.692 +
1.693 +(* print (ast) translations *)
1.694 +
1.695 +fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
1.696 +fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
1.697 +fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
1.698 +fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2);
1.699 +
1.700 +
1.701 +
1.702 +(** tables of token translation functions **)
1.703 +
1.704 +fun lookup_tokentr tabs modes =
1.705 + let val trs = distinct (eq_fst (op =)) (maps (these o AList.lookup (op =) tabs) (modes @ [""]))
1.706 + in fn c => Option.map fst (AList.lookup (op =) trs c) end;
1.707 +
1.708 +fun merge_tokentrtabs tabs1 tabs2 =
1.709 + let
1.710 + fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
1.711 +
1.712 + fun name (s, _) = implode (tl (Symbol.explode s));
1.713 +
1.714 + fun merge mode =
1.715 + let
1.716 + val trs1 = these (AList.lookup (op =) tabs1 mode);
1.717 + val trs2 = these (AList.lookup (op =) tabs2 mode);
1.718 + val trs = distinct eq_tr (trs1 @ trs2);
1.719 + in
1.720 + (case duplicates (eq_fst (op =)) trs of
1.721 + [] => (mode, trs)
1.722 + | dups => error ("More than one token translation function in mode " ^
1.723 + quote mode ^ " for " ^ commas_quote (map name dups)))
1.724 + end;
1.725 + in map merge (distinct (op =) (map fst (tabs1 @ tabs2))) end;
1.726 +
1.727 +fun extend_tokentrtab tokentrs tabs =
1.728 + let
1.729 + fun ins_tokentr (m, c, f) =
1.730 + AList.default (op =) (m, [])
1.731 + #> AList.map_entry (op =) m (cons ("_" ^ c, (f, stamp ())));
1.732 + in merge_tokentrtabs tabs (fold ins_tokentr tokentrs []) end;
1.733 +
1.734 +
1.735 +
1.736 +(** tables of translation rules **)
1.737 +
1.738 +type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
1.739 +
1.740 +fun dest_ruletab tab = maps snd (Symtab.dest tab);
1.741 +
1.742 +
1.743 +(* empty, update, merge ruletabs *)
1.744 +
1.745 +val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.head_of_rule r, r));
1.746 +val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r));
1.747 +fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2);
1.748 +
1.749 +
1.750 +
1.751 +(** datatype syntax **)
1.752 +
1.753 +datatype syntax =
1.754 + Syntax of {
1.755 + input: Syn_Ext.xprod list,
1.756 + lexicon: Scan.lexicon,
1.757 + gram: Parser.gram,
1.758 + consts: string list,
1.759 + prmodes: string list,
1.760 + parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
1.761 + parse_ruletab: ruletab,
1.762 + parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table,
1.763 + print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
1.764 + print_ruletab: ruletab,
1.765 + print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
1.766 + tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list,
1.767 + prtabs: Printer.prtabs} * stamp;
1.768 +
1.769 +fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
1.770 +
1.771 +fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
1.772 +
1.773 +type mode = string * bool;
1.774 +val mode_default = ("", true);
1.775 +val mode_input = (Print_Mode.input, true);
1.776 +
1.777 +
1.778 +(* empty_syntax *)
1.779 +
1.780 +val empty_syntax = Syntax
1.781 + ({input = [],
1.782 + lexicon = Scan.empty_lexicon,
1.783 + gram = Parser.empty_gram,
1.784 + consts = [],
1.785 + prmodes = [],
1.786 + parse_ast_trtab = Symtab.empty,
1.787 + parse_ruletab = Symtab.empty,
1.788 + parse_trtab = Symtab.empty,
1.789 + print_trtab = Symtab.empty,
1.790 + print_ruletab = Symtab.empty,
1.791 + print_ast_trtab = Symtab.empty,
1.792 + tokentrtab = [],
1.793 + prtabs = Printer.empty_prtabs}, stamp ());
1.794 +
1.795 +
1.796 +(* update_syntax *)
1.797 +
1.798 +fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
1.799 + let
1.800 + val {input, lexicon, gram, consts = consts1, prmodes = prmodes1,
1.801 + parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
1.802 + print_ast_trtab, tokentrtab, prtabs} = tabs;
1.803 + val Syn_Ext.Syn_Ext {xprods, consts = consts2, prmodes = prmodes2,
1.804 + parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
1.805 + print_ast_translation, token_translation} = syn_ext;
1.806 + val new_xprods =
1.807 + if inout then distinct (op =) (filter_out (member (op =) input) xprods) else [];
1.808 + fun if_inout xs = if inout then xs else [];
1.809 + in
1.810 + Syntax
1.811 + ({input = new_xprods @ input,
1.812 + lexicon = fold Scan.extend_lexicon (Syn_Ext.delims_of new_xprods) lexicon,
1.813 + gram = Parser.extend_gram new_xprods gram,
1.814 + consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
1.815 + prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
1.816 + parse_ast_trtab =
1.817 + update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
1.818 + parse_ruletab = update_ruletab (if_inout parse_rules) parse_ruletab,
1.819 + parse_trtab = update_trtab "parse translation" (if_inout parse_translation) parse_trtab,
1.820 + print_trtab = update_tr'tab print_translation print_trtab,
1.821 + print_ruletab = update_ruletab print_rules print_ruletab,
1.822 + print_ast_trtab = update_tr'tab print_ast_translation print_ast_trtab,
1.823 + tokentrtab = extend_tokentrtab token_translation tokentrtab,
1.824 + prtabs = Printer.update_prtabs mode xprods prtabs}, stamp ())
1.825 + end;
1.826 +
1.827 +
1.828 +(* remove_syntax *)
1.829 +
1.830 +fun remove_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
1.831 + let
1.832 + val Syn_Ext.Syn_Ext {xprods, consts = _, prmodes = _,
1.833 + parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
1.834 + print_ast_translation, token_translation = _} = syn_ext;
1.835 + val {input, lexicon, gram, consts, prmodes,
1.836 + parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
1.837 + print_ast_trtab, tokentrtab, prtabs} = tabs;
1.838 + val input' = if inout then subtract (op =) xprods input else input;
1.839 + val changed = length input <> length input';
1.840 + fun if_inout xs = if inout then xs else [];
1.841 + in
1.842 + Syntax
1.843 + ({input = input',
1.844 + lexicon = if changed then Scan.make_lexicon (Syn_Ext.delims_of input') else lexicon,
1.845 + gram = if changed then Parser.make_gram input' else gram,
1.846 + consts = consts,
1.847 + prmodes = prmodes,
1.848 + parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab,
1.849 + parse_ruletab = remove_ruletab (if_inout parse_rules) parse_ruletab,
1.850 + parse_trtab = remove_trtab (if_inout parse_translation) parse_trtab,
1.851 + print_trtab = remove_tr'tab print_translation print_trtab,
1.852 + print_ruletab = remove_ruletab print_rules print_ruletab,
1.853 + print_ast_trtab = remove_tr'tab print_ast_translation print_ast_trtab,
1.854 + tokentrtab = tokentrtab,
1.855 + prtabs = Printer.remove_prtabs mode xprods prtabs}, stamp ())
1.856 + end;
1.857 +
1.858 +
1.859 +(* merge_syntaxes *)
1.860 +
1.861 +fun merge_syntaxes (Syntax (tabs1, _)) (Syntax (tabs2, _)) =
1.862 + let
1.863 + val {input = input1, lexicon = lexicon1, gram = gram1, consts = consts1,
1.864 + prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1,
1.865 + parse_ruletab = parse_ruletab1, parse_trtab = parse_trtab1,
1.866 + print_trtab = print_trtab1, print_ruletab = print_ruletab1,
1.867 + print_ast_trtab = print_ast_trtab1, tokentrtab = tokentrtab1, prtabs = prtabs1} = tabs1;
1.868 +
1.869 + val {input = input2, lexicon = lexicon2, gram = gram2, consts = consts2,
1.870 + prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2,
1.871 + parse_ruletab = parse_ruletab2, parse_trtab = parse_trtab2,
1.872 + print_trtab = print_trtab2, print_ruletab = print_ruletab2,
1.873 + print_ast_trtab = print_ast_trtab2, tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2;
1.874 + in
1.875 + Syntax
1.876 + ({input = Library.merge (op =) (input1, input2),
1.877 + lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
1.878 + gram = Parser.merge_gram (gram1, gram2),
1.879 + consts = sort_distinct string_ord (consts1 @ consts2),
1.880 + prmodes = Library.merge (op =) (prmodes1, prmodes2),
1.881 + parse_ast_trtab =
1.882 + merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
1.883 + parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,
1.884 + parse_trtab = merge_trtabs "parse translation" parse_trtab1 parse_trtab2,
1.885 + print_trtab = merge_tr'tabs print_trtab1 print_trtab2,
1.886 + print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2,
1.887 + print_ast_trtab = merge_tr'tabs print_ast_trtab1 print_ast_trtab2,
1.888 + tokentrtab = merge_tokentrtabs tokentrtab1 tokentrtab2,
1.889 + prtabs = Printer.merge_prtabs prtabs1 prtabs2}, stamp ())
1.890 + end;
1.891 +
1.892 +
1.893 +(* basic syntax *)
1.894 +
1.895 +val basic_syntax =
1.896 + empty_syntax
1.897 + |> update_syntax mode_default Type_Ext.type_ext
1.898 + |> update_syntax mode_default Syn_Ext.pure_ext;
1.899 +
1.900 +val basic_nonterms =
1.901 + (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
1.902 + Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
1.903 + "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const",
1.904 + "index", "struct"]);
1.905 +
1.906 +
1.907 +
1.908 +(** print syntax **)
1.909 +
1.910 +local
1.911 +
1.912 +fun pretty_strs_qs name strs =
1.913 + Pretty.strs (name :: map quote (sort_strings strs));
1.914 +
1.915 +fun pretty_gram (Syntax (tabs, _)) =
1.916 + let
1.917 + val {lexicon, prmodes, gram, ...} = tabs;
1.918 + val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes);
1.919 + in
1.920 + [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
1.921 + Pretty.big_list "prods:" (Parser.pretty_gram gram),
1.922 + pretty_strs_qs "print modes:" prmodes']
1.923 + end;
1.924 +
1.925 +fun pretty_trans (Syntax (tabs, _)) =
1.926 + let
1.927 + fun pretty_trtab name tab =
1.928 + pretty_strs_qs name (Symtab.keys tab);
1.929 +
1.930 + fun pretty_ruletab name tab =
1.931 + Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab));
1.932 +
1.933 + fun pretty_tokentr (mode, trs) = Pretty.strs (quote mode ^ ":" :: map fst trs);
1.934 +
1.935 + val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
1.936 + print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs;
1.937 + in
1.938 + [pretty_strs_qs "consts:" consts,
1.939 + pretty_trtab "parse_ast_translation:" parse_ast_trtab,
1.940 + pretty_ruletab "parse_rules:" parse_ruletab,
1.941 + pretty_trtab "parse_translation:" parse_trtab,
1.942 + pretty_trtab "print_translation:" print_trtab,
1.943 + pretty_ruletab "print_rules:" print_ruletab,
1.944 + pretty_trtab "print_ast_translation:" print_ast_trtab,
1.945 + Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab)]
1.946 + end;
1.947 +
1.948 +in
1.949 +
1.950 +fun print_gram syn = Pretty.writeln (Pretty.chunks (pretty_gram syn));
1.951 +fun print_trans syn = Pretty.writeln (Pretty.chunks (pretty_trans syn));
1.952 +fun print_syntax syn = Pretty.writeln (Pretty.chunks (pretty_gram syn @ pretty_trans syn));
1.953 +
1.954 +end;
1.955 +
1.956 +
1.957 +(* reconstructing infixes -- educated guessing *)
1.958 +
1.959 +fun guess_infix (Syntax ({gram, ...}, _)) c =
1.960 + (case Parser.guess_infix_lr gram c of
1.961 + SOME (s, l, r, j) => SOME
1.962 + (if l then Mixfix.Infixl (s, j)
1.963 + else if r then Mixfix.Infixr (s, j)
1.964 + else Mixfix.Infix (s, j))
1.965 + | NONE => NONE);
1.966 +
1.967 +
1.968 +
1.969 +(** read **)
1.970 +
1.971 +(* read_ast *)
1.972 +
1.973 +val ambiguity_enabled =
1.974 + Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
1.975 +
1.976 +val ambiguity_level_value = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1);
1.977 +val ambiguity_level = Config.int ambiguity_level_value;
1.978 +
1.979 +val ambiguity_limit =
1.980 + Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
1.981 +
1.982 +fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
1.983 +
1.984 +fun read_asts ctxt is_logtype (Syntax (tabs, _)) xids root (syms, pos) =
1.985 + let
1.986 + val {lexicon, gram, parse_ast_trtab, ...} = tabs;
1.987 + val toks = Lexicon.tokenize lexicon xids syms;
1.988 + val _ = List.app (Lexicon.report_token ctxt) toks;
1.989 +
1.990 + val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
1.991 + val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks);
1.992 + val len = length pts;
1.993 +
1.994 + val limit = Config.get ctxt ambiguity_limit;
1.995 + fun show_pt pt =
1.996 + Pretty.string_of (Ast.pretty_ast (hd (Syn_Trans.pts_to_asts ctxt (K NONE) [pt])));
1.997 + in
1.998 + if len <= Config.get ctxt ambiguity_level then ()
1.999 + else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
1.1000 + else
1.1001 + (Context_Position.if_visible ctxt warning (cat_lines
1.1002 + (("Ambiguous input" ^ Position.str_of pos ^
1.1003 + "\nproduces " ^ string_of_int len ^ " parse trees" ^
1.1004 + (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
1.1005 + map show_pt (take limit pts))));
1.1006 + Syn_Trans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
1.1007 + end;
1.1008 +
1.1009 +
1.1010 +(* read *)
1.1011 +
1.1012 +fun read ctxt is_logtype (syn as Syntax (tabs, _)) ty inp =
1.1013 + let
1.1014 + val {parse_ruletab, parse_trtab, ...} = tabs;
1.1015 + val asts = read_asts ctxt is_logtype syn false (Syn_Ext.typ_to_nonterm ty) inp;
1.1016 + in
1.1017 + Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
1.1018 + (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
1.1019 + end;
1.1020 +
1.1021 +
1.1022 +(* read terms *)
1.1023 +
1.1024 +(*brute-force disambiguation via type-inference*)
1.1025 +fun disambig _ _ _ [t] = t
1.1026 + | disambig ctxt pp check ts =
1.1027 + let
1.1028 + val level = Config.get ctxt ambiguity_level;
1.1029 + val limit = Config.get ctxt ambiguity_limit;
1.1030 +
1.1031 + val ambiguity = length ts;
1.1032 + fun ambig_msg () =
1.1033 + if ambiguity > 1 andalso ambiguity <= level then
1.1034 + "Got more than one parse tree.\n\
1.1035 + \Retry with smaller syntax_ambiguity_level for more information."
1.1036 + else "";
1.1037 +
1.1038 + val errs = Par_List.map check ts;
1.1039 + val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
1.1040 + val len = length results;
1.1041 + in
1.1042 + if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
1.1043 + else if len = 1 then
1.1044 + (if ambiguity > level then
1.1045 + Context_Position.if_visible ctxt warning
1.1046 + "Fortunately, only one parse tree is type correct.\n\
1.1047 + \You may still want to disambiguate your grammar or your input."
1.1048 + else (); hd results)
1.1049 + else cat_error (ambig_msg ()) (cat_lines
1.1050 + (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
1.1051 + (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
1.1052 + map (Pretty.string_of_term pp) (take limit results)))
1.1053 + end;
1.1054 +
1.1055 +fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
1.1056 + read ctxt is_logtype syn ty (syms, pos)
1.1057 + |> map (Type_Ext.decode_term get_sort map_const map_free)
1.1058 + |> disambig ctxt (Printer.pp_show_brackets pp) check;
1.1059 +
1.1060 +
1.1061 +(* read types *)
1.1062 +
1.1063 +fun standard_parse_typ ctxt syn get_sort (syms, pos) =
1.1064 + (case read ctxt (K false) syn Syn_Ext.typeT (syms, pos) of
1.1065 + [t] => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t
1.1066 + | _ => error (ambiguity_msg pos));
1.1067 +
1.1068 +
1.1069 +(* read sorts *)
1.1070 +
1.1071 +fun standard_parse_sort ctxt syn (syms, pos) =
1.1072 + (case read ctxt (K false) syn Type_Ext.sortT (syms, pos) of
1.1073 + [t] => Type_Ext.sort_of_term t
1.1074 + | _ => error (ambiguity_msg pos));
1.1075 +
1.1076 +
1.1077 +
1.1078 +(** prepare translation rules **)
1.1079 +
1.1080 +datatype 'a trrule =
1.1081 + ParseRule of 'a * 'a |
1.1082 + PrintRule of 'a * 'a |
1.1083 + ParsePrintRule of 'a * 'a;
1.1084 +
1.1085 +fun map_trrule f (ParseRule (x, y)) = ParseRule (f x, f y)
1.1086 + | map_trrule f (PrintRule (x, y)) = PrintRule (f x, f y)
1.1087 + | map_trrule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y);
1.1088 +
1.1089 +fun parse_rule (ParseRule pats) = SOME pats
1.1090 + | parse_rule (PrintRule _) = NONE
1.1091 + | parse_rule (ParsePrintRule pats) = SOME pats;
1.1092 +
1.1093 +fun print_rule (ParseRule _) = NONE
1.1094 + | print_rule (PrintRule pats) = SOME (swap pats)
1.1095 + | print_rule (ParsePrintRule pats) = SOME (swap pats);
1.1096 +
1.1097 +
1.1098 +fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
1.1099 +
1.1100 +local
1.1101 +
1.1102 +fun check_rule (rule as (lhs, rhs)) =
1.1103 + (case Ast.rule_error rule of
1.1104 + SOME msg =>
1.1105 + error ("Error in syntax translation rule: " ^ msg ^ "\n" ^
1.1106 + Ast.str_of_ast lhs ^ " -> " ^ Ast.str_of_ast rhs)
1.1107 + | NONE => rule);
1.1108 +
1.1109 +fun read_pattern ctxt is_logtype syn (root, str) =
1.1110 + let
1.1111 + fun constify (ast as Ast.Constant _) = ast
1.1112 + | constify (ast as Ast.Variable x) =
1.1113 + if is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
1.1114 + else ast
1.1115 + | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
1.1116 +
1.1117 + val (syms, pos) = read_token str;
1.1118 + in
1.1119 + (case read_asts ctxt is_logtype syn true root (syms, pos) of
1.1120 + [ast] => constify ast
1.1121 + | _ => error (ambiguity_msg pos))
1.1122 + end;
1.1123 +
1.1124 +fun prep_rules rd_pat raw_rules =
1.1125 + let val rules = map (map_trrule rd_pat) raw_rules in
1.1126 + (map check_rule (map_filter parse_rule rules),
1.1127 + map check_rule (map_filter print_rule rules))
1.1128 + end
1.1129 +
1.1130 +in
1.1131 +
1.1132 +val cert_rules = prep_rules I;
1.1133 +
1.1134 +fun read_rules ctxt is_logtype syn =
1.1135 + prep_rules (read_pattern ctxt is_logtype syn);
1.1136 +
1.1137 +end;
1.1138 +
1.1139 +
1.1140 +
1.1141 +(** unparse terms, typs, sorts **)
1.1142 +
1.1143 +local
1.1144 +
1.1145 +fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
1.1146 + let
1.1147 + val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
1.1148 + val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
1.1149 + in
1.1150 + Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
1.1151 + (lookup_tokentr tokentrtab (print_mode_value ()))
1.1152 + (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast))
1.1153 + end;
1.1154 +
1.1155 +in
1.1156 +
1.1157 +fun standard_unparse_term idents extern =
1.1158 + unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
1.1159 +
1.1160 +fun standard_unparse_typ extern ctxt syn =
1.1161 + unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
1.1162 +
1.1163 +fun standard_unparse_sort {extern_class} ctxt syn =
1.1164 + unparse_t (K Printer.sort_to_ast)
1.1165 + (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
1.1166 + Markup.sort ctxt syn false;
1.1167 +
1.1168 +end;
1.1169 +
1.1170 +
1.1171 +
1.1172 +(** modify syntax **)
1.1173 +
1.1174 +fun ext_syntax f decls = update_syntax mode_default (f decls);
1.1175 +
1.1176 +val update_trfuns = ext_syntax Syn_Ext.syn_ext_trfuns;
1.1177 +val update_advanced_trfuns = ext_syntax Syn_Ext.syn_ext_advanced_trfuns;
1.1178 +val extend_tokentrfuns = ext_syntax Syn_Ext.syn_ext_tokentrfuns;
1.1179 +
1.1180 +fun update_type_gram add prmode decls =
1.1181 + (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
1.1182 +
1.1183 +fun update_const_gram add is_logtype prmode decls =
1.1184 + (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
1.1185 +
1.1186 +fun update_trrules ctxt is_logtype syn =
1.1187 + ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
1.1188 +
1.1189 +fun remove_trrules ctxt is_logtype syn =
1.1190 + remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
1.1191 +
1.1192 +val update_trrules_i = ext_syntax Syn_Ext.syn_ext_rules o cert_rules;
1.1193 +val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules;
1.1194 +
1.1195 +
1.1196 (*export parts of internal Syntax structures*)
1.1197 open Lexicon Syn_Ext Ast Parser Type_Ext Syn_Trans Mixfix Printer;
1.1198