src/Pure/Syntax/syntax.ML
author wenzelm
Sun Apr 03 21:59:33 2011 +0200 (2011-04-03)
changeset 42204 b3277168c1e7
parent 42134 4bc55652c685
child 42205 22f5cc06c419
permissions -rw-r--r--
added Position.reports convenience;
modernized Syntax.trrule constructors;
modernized Sign.add_trrules/del_trrules: internal arguments;
modernized Isar_Cmd.translations/no_translations: external arguments;
explicit syntax categories class_name/type_name, with reports via type_context;
eliminated former class_name/type_name ast translations;
tuned signatures;
     1 (*  Title:      Pure/Syntax/syntax.ML
     2     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     3 
     4 Standard Isabelle syntax, based on arbitrary context-free grammars
     5 (specified by mixfix declarations).
     6 *)
     7 
     8 signature BASIC_SYNTAX =
     9 sig
    10   include AST0
    11   include SYN_TRANS0
    12   include MIXFIX0
    13   include PRINTER0
    14 end;
    15 
    16 signature SYNTAX =
    17 sig
    18   include AST1
    19   include LEXICON0
    20   include SYN_EXT0
    21   include TYPE_EXT0
    22   include SYN_TRANS1
    23   include MIXFIX1
    24   include PRINTER0
    25   val read_token: string -> Symbol_Pos.T list * Position.T
    26   val parse_token: Proof.context -> Markup.T -> string -> Symbol_Pos.T list * Position.T
    27   val parse_sort: Proof.context -> string -> sort
    28   val parse_typ: Proof.context -> string -> typ
    29   val parse_term: Proof.context -> string -> term
    30   val parse_prop: Proof.context -> string -> term
    31   val unparse_sort: Proof.context -> sort -> Pretty.T
    32   val unparse_classrel: Proof.context -> class list -> Pretty.T
    33   val unparse_arity: Proof.context -> arity -> Pretty.T
    34   val unparse_typ: Proof.context -> typ -> Pretty.T
    35   val unparse_term: Proof.context -> term -> Pretty.T
    36   val install_operations:
    37    {parse_sort: Proof.context -> string -> sort,
    38     parse_typ: Proof.context -> string -> typ,
    39     parse_term: Proof.context -> string -> term,
    40     parse_prop: Proof.context -> string -> term,
    41     unparse_sort: Proof.context -> sort -> Pretty.T,
    42     unparse_typ: Proof.context -> typ -> Pretty.T,
    43     unparse_term: Proof.context -> term -> Pretty.T} -> unit
    44   val print_checks: Proof.context -> unit
    45   val add_typ_check: int -> string ->
    46     (typ list -> Proof.context -> (typ list * Proof.context) option) ->
    47     Context.generic -> Context.generic
    48   val add_term_check: int -> string ->
    49     (term list -> Proof.context -> (term list * Proof.context) option) ->
    50     Context.generic -> Context.generic
    51   val add_typ_uncheck: int -> string ->
    52     (typ list -> Proof.context -> (typ list * Proof.context) option) ->
    53     Context.generic -> Context.generic
    54   val add_term_uncheck: int -> string ->
    55     (term list -> Proof.context -> (term list * Proof.context) option) ->
    56     Context.generic -> Context.generic
    57   val check_sort: Proof.context -> sort -> sort
    58   val check_typ: Proof.context -> typ -> typ
    59   val check_term: Proof.context -> term -> term
    60   val check_prop: Proof.context -> term -> term
    61   val check_typs: Proof.context -> typ list -> typ list
    62   val check_terms: Proof.context -> term list -> term list
    63   val check_props: Proof.context -> term list -> term list
    64   val uncheck_sort: Proof.context -> sort -> sort
    65   val uncheck_arity: Proof.context -> arity -> arity
    66   val uncheck_classrel: Proof.context -> class list -> class list
    67   val uncheck_typs: Proof.context -> typ list -> typ list
    68   val uncheck_terms: Proof.context -> term list -> term list
    69   val read_sort: Proof.context -> string -> sort
    70   val read_typ: Proof.context -> string -> typ
    71   val read_term: Proof.context -> string -> term
    72   val read_prop: Proof.context -> string -> term
    73   val read_terms: Proof.context -> string list -> term list
    74   val read_props: Proof.context -> string list -> term list
    75   val read_sort_global: theory -> string -> sort
    76   val read_typ_global: theory -> string -> typ
    77   val read_term_global: theory -> string -> term
    78   val read_prop_global: theory -> string -> term
    79   val pretty_term: Proof.context -> term -> Pretty.T
    80   val pretty_typ: Proof.context -> typ -> Pretty.T
    81   val pretty_sort: Proof.context -> sort -> Pretty.T
    82   val pretty_classrel: Proof.context -> class list -> Pretty.T
    83   val pretty_arity: Proof.context -> arity -> Pretty.T
    84   val string_of_term: Proof.context -> term -> string
    85   val string_of_typ: Proof.context -> typ -> string
    86   val string_of_sort: Proof.context -> sort -> string
    87   val string_of_classrel: Proof.context -> class list -> string
    88   val string_of_arity: Proof.context -> arity -> string
    89   val is_pretty_global: Proof.context -> bool
    90   val set_pretty_global: bool -> Proof.context -> Proof.context
    91   val init_pretty_global: theory -> Proof.context
    92   val pretty_term_global: theory -> term -> Pretty.T
    93   val pretty_typ_global: theory -> typ -> Pretty.T
    94   val pretty_sort_global: theory -> sort -> Pretty.T
    95   val string_of_term_global: theory -> term -> string
    96   val string_of_typ_global: theory -> typ -> string
    97   val string_of_sort_global: theory -> sort -> string
    98   val pp: Proof.context -> Pretty.pp
    99   val pp_global: theory -> Pretty.pp
   100   type syntax
   101   val eq_syntax: syntax * syntax -> bool
   102   val is_keyword: syntax -> string -> bool
   103   type mode
   104   val mode_default: mode
   105   val mode_input: mode
   106   val merge_syntaxes: syntax -> syntax -> syntax
   107   val basic_syntax: syntax
   108   val basic_nonterms: string list
   109   val print_gram: syntax -> unit
   110   val print_trans: syntax -> unit
   111   val print_syntax: syntax -> unit
   112   val guess_infix: syntax -> string -> mixfix option
   113   val positions_raw: Config.raw
   114   val positions: bool Config.T
   115   val ambiguity_enabled: bool Config.T
   116   val ambiguity_level_raw: Config.raw
   117   val ambiguity_level: int Config.T
   118   val ambiguity_limit: int Config.T
   119   val standard_parse_term: (term -> string option) ->
   120     Proof.context -> type_context -> term_context -> syntax ->
   121     string -> Symbol_Pos.T list * Position.T -> term
   122   val standard_parse_typ: Proof.context -> type_context -> syntax ->
   123     ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
   124   val standard_parse_sort: Proof.context -> type_context -> syntax ->
   125     Symbol_Pos.T list * Position.T -> sort
   126   datatype 'a trrule =
   127     Parse_Rule of 'a * 'a |
   128     Print_Rule of 'a * 'a |
   129     Parse_Print_Rule of 'a * 'a
   130   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   131   val is_const: syntax -> string -> bool
   132   val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> ast
   133   val standard_unparse_term: {structs: string list, fixes: string list} ->
   134     {extern_class: string -> xstring, extern_type: string -> xstring,
   135       extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
   136   val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
   137     Proof.context -> syntax -> typ -> Pretty.T
   138   val standard_unparse_sort: {extern_class: string -> xstring} ->
   139     Proof.context -> syntax -> sort -> Pretty.T
   140   val update_trfuns:
   141     (string * ((ast list -> ast) * stamp)) list *
   142     (string * ((term list -> term) * stamp)) list *
   143     (string * ((bool -> typ -> term list -> term) * stamp)) list *
   144     (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax
   145   val update_advanced_trfuns:
   146     (string * ((Proof.context -> ast list -> ast) * stamp)) list *
   147     (string * ((Proof.context -> term list -> term) * stamp)) list *
   148     (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
   149     (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
   150   val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
   151     syntax -> syntax
   152   val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
   153   val update_const_gram: bool -> (string -> bool) ->
   154     mode -> (string * typ * mixfix) list -> syntax -> syntax
   155   val update_trrules: ast trrule list -> syntax -> syntax
   156   val remove_trrules: ast trrule list -> syntax -> syntax
   157 end;
   158 
   159 structure Syntax: SYNTAX =
   160 struct
   161 
   162 (** inner syntax operations **)
   163 
   164 (* read token -- with optional YXML encoding of position *)
   165 
   166 fun read_token str =
   167   let
   168     val tree = YXML.parse str handle Fail msg => error msg;
   169     val text = XML.content_of [tree];
   170     val pos =
   171       (case tree of
   172         XML.Elem ((name, props), _) =>
   173           if name = Markup.tokenN then Position.of_properties props
   174           else Position.none
   175       | XML.Text _ => Position.none);
   176   in (Symbol_Pos.explode (text, pos), pos) end;
   177 
   178 
   179 (* (un)parsing *)
   180 
   181 fun parse_token ctxt markup str =
   182   let
   183     val (syms, pos) = read_token str;
   184     val _ = Context_Position.report ctxt pos markup;
   185   in (syms, pos) end;
   186 
   187 local
   188 
   189 type operations =
   190  {parse_sort: Proof.context -> string -> sort,
   191   parse_typ: Proof.context -> string -> typ,
   192   parse_term: Proof.context -> string -> term,
   193   parse_prop: Proof.context -> string -> term,
   194   unparse_sort: Proof.context -> sort -> Pretty.T,
   195   unparse_typ: Proof.context -> typ -> Pretty.T,
   196   unparse_term: Proof.context -> term -> Pretty.T};
   197 
   198 val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
   199 
   200 fun operation which ctxt x =
   201   (case Single_Assignment.peek operations of
   202     NONE => raise Fail "Inner syntax operations not installed"
   203   | SOME ops => which ops ctxt x);
   204 
   205 in
   206 
   207 val parse_sort = operation #parse_sort;
   208 val parse_typ = operation #parse_typ;
   209 val parse_term = operation #parse_term;
   210 val parse_prop = operation #parse_prop;
   211 val unparse_sort = operation #unparse_sort;
   212 val unparse_typ = operation #unparse_typ;
   213 val unparse_term = operation #unparse_term;
   214 
   215 fun install_operations ops = Single_Assignment.assign operations ops;
   216 
   217 end;
   218 
   219 
   220 (* context-sensitive (un)checking *)
   221 
   222 local
   223 
   224 type key = int * bool;
   225 type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
   226 
   227 structure Checks = Generic_Data
   228 (
   229   type T =
   230     ((key * ((string * typ check) * stamp) list) list *
   231      (key * ((string * term check) * stamp) list) list);
   232   val empty = ([], []);
   233   val extend = I;
   234   fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
   235     (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
   236      AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
   237 );
   238 
   239 fun gen_add which (key: key) name f =
   240   Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
   241 
   242 fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
   243 
   244 fun gen_check which uncheck ctxt0 xs0 =
   245   let
   246     val funs = which (Checks.get (Context.Proof ctxt0))
   247       |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
   248       |> Library.sort (int_ord o pairself fst) |> map snd
   249       |> not uncheck ? map rev;
   250     val check_all = perhaps_apply (map check_stage funs);
   251   in #1 (perhaps check_all (xs0, ctxt0)) end;
   252 
   253 fun map_sort f S =
   254   (case f (TFree ("", S)) of
   255     TFree ("", S') => S'
   256   | _ => raise TYPE ("map_sort", [TFree ("", S)], []));
   257 
   258 in
   259 
   260 fun print_checks ctxt =
   261   let
   262     fun split_checks checks =
   263       List.partition (fn ((_, un), _) => not un) checks
   264       |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
   265           #> sort (int_ord o pairself fst));
   266     fun pretty_checks kind checks =
   267       checks |> map (fn (i, names) => Pretty.block
   268         [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
   269           Pretty.brk 1, Pretty.strs names]);
   270 
   271     val (typs, terms) = Checks.get (Context.Proof ctxt);
   272     val (typ_checks, typ_unchecks) = split_checks typs;
   273     val (term_checks, term_unchecks) = split_checks terms;
   274   in
   275     pretty_checks "typ_checks" typ_checks @
   276     pretty_checks "term_checks" term_checks @
   277     pretty_checks "typ_unchecks" typ_unchecks @
   278     pretty_checks "term_unchecks" term_unchecks
   279   end |> Pretty.chunks |> Pretty.writeln;
   280 
   281 fun add_typ_check stage = gen_add apfst (stage, false);
   282 fun add_term_check stage = gen_add apsnd (stage, false);
   283 fun add_typ_uncheck stage = gen_add apfst (stage, true);
   284 fun add_term_uncheck stage = gen_add apsnd (stage, true);
   285 
   286 val check_typs = gen_check fst false;
   287 val check_terms = gen_check snd false;
   288 fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
   289 
   290 val check_typ = singleton o check_typs;
   291 val check_term = singleton o check_terms;
   292 val check_prop = singleton o check_props;
   293 val check_sort = map_sort o check_typ;
   294 
   295 val uncheck_typs = gen_check fst true;
   296 val uncheck_terms = gen_check snd true;
   297 val uncheck_sort = map_sort o singleton o uncheck_typs;
   298 
   299 end;
   300 
   301 
   302 (* derived operations for classrel and arity *)
   303 
   304 val uncheck_classrel = map o singleton o uncheck_sort;
   305 
   306 fun unparse_classrel ctxt cs = Pretty.block (flat
   307   (separate [Pretty.str " <", Pretty.brk 1] (map (single o unparse_sort ctxt o single) cs)));
   308 
   309 fun uncheck_arity ctxt (a, Ss, S) =
   310   let
   311     val T = Type (a, replicate (length Ss) dummyT);
   312     val a' =
   313       (case singleton (uncheck_typs ctxt) T of
   314         Type (a', _) => a'
   315       | T => raise TYPE ("uncheck_arity", [T], []));
   316     val Ss' = map (uncheck_sort ctxt) Ss;
   317     val S' = uncheck_sort ctxt S;
   318   in (a', Ss', S') end;
   319 
   320 fun unparse_arity ctxt (a, Ss, S) =
   321   let
   322     val prtT = unparse_typ ctxt (Type (a, []));
   323     val dom =
   324       if null Ss then []
   325       else [Pretty.list "(" ")" (map (unparse_sort ctxt) Ss), Pretty.brk 1];
   326   in Pretty.block ([prtT, Pretty.str " ::", Pretty.brk 1] @ dom @ [unparse_sort ctxt S]) end;
   327 
   328 
   329 (* read = parse + check *)
   330 
   331 fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
   332 fun read_typ ctxt = parse_typ ctxt #> singleton (check_typs ctxt);
   333 
   334 fun read_terms ctxt = map (parse_term ctxt) #> check_terms ctxt;
   335 fun read_props ctxt = map (parse_prop ctxt) #> check_props ctxt;
   336 
   337 val read_term = singleton o read_terms;
   338 val read_prop = singleton o read_props;
   339 
   340 val read_sort_global = read_sort o ProofContext.init_global;
   341 val read_typ_global = read_typ o ProofContext.init_global;
   342 val read_term_global = read_term o ProofContext.init_global;
   343 val read_prop_global = read_prop o ProofContext.init_global;
   344 
   345 
   346 (* pretty = uncheck + unparse *)
   347 
   348 fun pretty_term ctxt = singleton (uncheck_terms ctxt) #> unparse_term ctxt;
   349 fun pretty_typ ctxt = singleton (uncheck_typs ctxt) #> unparse_typ ctxt;
   350 fun pretty_sort ctxt = uncheck_sort ctxt #> unparse_sort ctxt;
   351 fun pretty_classrel ctxt = uncheck_classrel ctxt #> unparse_classrel ctxt;
   352 fun pretty_arity ctxt = uncheck_arity ctxt #> unparse_arity ctxt;
   353 
   354 val string_of_term = Pretty.string_of oo pretty_term;
   355 val string_of_typ = Pretty.string_of oo pretty_typ;
   356 val string_of_sort = Pretty.string_of oo pretty_sort;
   357 val string_of_classrel = Pretty.string_of oo pretty_classrel;
   358 val string_of_arity = Pretty.string_of oo pretty_arity;
   359 
   360 
   361 (* global pretty printing *)
   362 
   363 val pretty_global = Config.bool (Config.declare "Syntax.pretty_global" (K (Config.Bool false)));
   364 fun is_pretty_global ctxt = Config.get ctxt pretty_global;
   365 val set_pretty_global = Config.put pretty_global;
   366 val init_pretty_global = set_pretty_global true o ProofContext.init_global;
   367 
   368 val pretty_term_global = pretty_term o init_pretty_global;
   369 val pretty_typ_global = pretty_typ o init_pretty_global;
   370 val pretty_sort_global = pretty_sort o init_pretty_global;
   371 
   372 val string_of_term_global = string_of_term o init_pretty_global;
   373 val string_of_typ_global = string_of_typ o init_pretty_global;
   374 val string_of_sort_global = string_of_sort o init_pretty_global;
   375 
   376 
   377 (* pp operations -- deferred evaluation *)
   378 
   379 fun pp ctxt = Pretty.pp
   380  (fn x => pretty_term ctxt x,
   381   fn x => pretty_typ ctxt x,
   382   fn x => pretty_sort ctxt x,
   383   fn x => pretty_classrel ctxt x,
   384   fn x => pretty_arity ctxt x);
   385 
   386 fun pp_global thy = Pretty.pp
   387  (fn x => pretty_term_global thy x,
   388   fn x => pretty_typ_global thy x,
   389   fn x => pretty_sort_global thy x,
   390   fn x => pretty_classrel (init_pretty_global thy) x,
   391   fn x => pretty_arity (init_pretty_global thy) x);
   392 
   393 
   394 
   395 (** tables of translation functions **)
   396 
   397 (* parse (ast) translations *)
   398 
   399 fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
   400 
   401 fun err_dup_trfun name c =
   402   error ("More than one " ^ name ^ " for " ^ quote c);
   403 
   404 fun remove_trtab trfuns = fold (Symtab.remove Syn_Ext.eq_trfun) trfuns;
   405 
   406 fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
   407   handle Symtab.DUP c => err_dup_trfun name c;
   408 
   409 fun merge_trtabs name tab1 tab2 = Symtab.merge Syn_Ext.eq_trfun (tab1, tab2)
   410   handle Symtab.DUP c => err_dup_trfun name c;
   411 
   412 
   413 (* print (ast) translations *)
   414 
   415 fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
   416 fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
   417 fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
   418 fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2);
   419 
   420 
   421 
   422 (** tables of token translation functions **)
   423 
   424 fun lookup_tokentr tabs modes =
   425   let val trs = distinct (eq_fst (op =)) (maps (these o AList.lookup (op =) tabs) (modes @ [""]))
   426   in fn c => Option.map fst (AList.lookup (op =) trs c) end;
   427 
   428 fun merge_tokentrtabs tabs1 tabs2 =
   429   let
   430     fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
   431 
   432     fun name (s, _) = implode (tl (Symbol.explode s));
   433 
   434     fun merge mode =
   435       let
   436         val trs1 = these (AList.lookup (op =) tabs1 mode);
   437         val trs2 = these (AList.lookup (op =) tabs2 mode);
   438         val trs = distinct eq_tr (trs1 @ trs2);
   439       in
   440         (case duplicates (eq_fst (op =)) trs of
   441           [] => (mode, trs)
   442         | dups => error ("More than one token translation function in mode " ^
   443             quote mode ^ " for " ^ commas_quote (map name dups)))
   444       end;
   445   in map merge (distinct (op =) (map fst (tabs1 @ tabs2))) end;
   446 
   447 fun extend_tokentrtab tokentrs tabs =
   448   let
   449     fun ins_tokentr (m, c, f) =
   450       AList.default (op =) (m, [])
   451       #> AList.map_entry (op =) m (cons ("_" ^ c, (f, stamp ())));
   452   in merge_tokentrtabs tabs (fold ins_tokentr tokentrs []) end;
   453 
   454 
   455 
   456 (** tables of translation rules **)
   457 
   458 type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
   459 
   460 fun dest_ruletab tab = maps snd (Symtab.dest tab);
   461 
   462 
   463 (* empty, update, merge ruletabs *)
   464 
   465 val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.head_of_rule r, r));
   466 val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r));
   467 fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2);
   468 
   469 
   470 
   471 (** datatype syntax **)
   472 
   473 datatype syntax =
   474   Syntax of {
   475     input: Syn_Ext.xprod list,
   476     lexicon: Scan.lexicon,
   477     gram: Parser.gram,
   478     consts: string list,
   479     prmodes: string list,
   480     parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
   481     parse_ruletab: ruletab,
   482     parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table,
   483     print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
   484     print_ruletab: ruletab,
   485     print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
   486     tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list,
   487     prtabs: Printer.prtabs} * stamp;
   488 
   489 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
   490 
   491 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
   492 
   493 type mode = string * bool;
   494 val mode_default = ("", true);
   495 val mode_input = (Print_Mode.input, true);
   496 
   497 
   498 (* empty_syntax *)
   499 
   500 val empty_syntax = Syntax
   501   ({input = [],
   502     lexicon = Scan.empty_lexicon,
   503     gram = Parser.empty_gram,
   504     consts = [],
   505     prmodes = [],
   506     parse_ast_trtab = Symtab.empty,
   507     parse_ruletab = Symtab.empty,
   508     parse_trtab = Symtab.empty,
   509     print_trtab = Symtab.empty,
   510     print_ruletab = Symtab.empty,
   511     print_ast_trtab = Symtab.empty,
   512     tokentrtab = [],
   513     prtabs = Printer.empty_prtabs}, stamp ());
   514 
   515 
   516 (* update_syntax *)
   517 
   518 fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
   519   let
   520     val {input, lexicon, gram, consts = consts1, prmodes = prmodes1,
   521       parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
   522       print_ast_trtab, tokentrtab, prtabs} = tabs;
   523     val Syn_Ext.Syn_Ext {xprods, consts = consts2, prmodes = prmodes2,
   524       parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
   525       print_ast_translation, token_translation} = syn_ext;
   526     val new_xprods =
   527       if inout then distinct (op =) (filter_out (member (op =) input) xprods) else [];
   528     fun if_inout xs = if inout then xs else [];
   529   in
   530     Syntax
   531     ({input = new_xprods @ input,
   532       lexicon = fold Scan.extend_lexicon (Syn_Ext.delims_of new_xprods) lexicon,
   533       gram = Parser.extend_gram new_xprods gram,
   534       consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
   535       prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
   536       parse_ast_trtab =
   537         update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
   538       parse_ruletab = update_ruletab (if_inout parse_rules) parse_ruletab,
   539       parse_trtab = update_trtab "parse translation" (if_inout parse_translation) parse_trtab,
   540       print_trtab = update_tr'tab print_translation print_trtab,
   541       print_ruletab = update_ruletab print_rules print_ruletab,
   542       print_ast_trtab = update_tr'tab print_ast_translation print_ast_trtab,
   543       tokentrtab = extend_tokentrtab token_translation tokentrtab,
   544       prtabs = Printer.update_prtabs mode xprods prtabs}, stamp ())
   545   end;
   546 
   547 
   548 (* remove_syntax *)
   549 
   550 fun remove_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
   551   let
   552     val Syn_Ext.Syn_Ext {xprods, consts = _, prmodes = _,
   553       parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
   554       print_ast_translation, token_translation = _} = syn_ext;
   555     val {input, lexicon, gram, consts, prmodes,
   556       parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
   557       print_ast_trtab, tokentrtab, prtabs} = tabs;
   558     val input' = if inout then subtract (op =) xprods input else input;
   559     val changed = length input <> length input';
   560     fun if_inout xs = if inout then xs else [];
   561   in
   562     Syntax
   563     ({input = input',
   564       lexicon = if changed then Scan.make_lexicon (Syn_Ext.delims_of input') else lexicon,
   565       gram = if changed then Parser.make_gram input' else gram,
   566       consts = consts,
   567       prmodes = prmodes,
   568       parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab,
   569       parse_ruletab = remove_ruletab (if_inout parse_rules) parse_ruletab,
   570       parse_trtab = remove_trtab (if_inout parse_translation) parse_trtab,
   571       print_trtab = remove_tr'tab print_translation print_trtab,
   572       print_ruletab = remove_ruletab print_rules print_ruletab,
   573       print_ast_trtab = remove_tr'tab print_ast_translation print_ast_trtab,
   574       tokentrtab = tokentrtab,
   575       prtabs = Printer.remove_prtabs mode xprods prtabs}, stamp ())
   576   end;
   577 
   578 
   579 (* merge_syntaxes *)
   580 
   581 fun merge_syntaxes (Syntax (tabs1, _)) (Syntax (tabs2, _)) =
   582   let
   583     val {input = input1, lexicon = lexicon1, gram = gram1, consts = consts1,
   584       prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1,
   585       parse_ruletab = parse_ruletab1, parse_trtab = parse_trtab1,
   586       print_trtab = print_trtab1, print_ruletab = print_ruletab1,
   587       print_ast_trtab = print_ast_trtab1, tokentrtab = tokentrtab1, prtabs = prtabs1} = tabs1;
   588 
   589     val {input = input2, lexicon = lexicon2, gram = gram2, consts = consts2,
   590       prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2,
   591       parse_ruletab = parse_ruletab2, parse_trtab = parse_trtab2,
   592       print_trtab = print_trtab2, print_ruletab = print_ruletab2,
   593       print_ast_trtab = print_ast_trtab2, tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2;
   594   in
   595     Syntax
   596     ({input = Library.merge (op =) (input1, input2),
   597       lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
   598       gram = Parser.merge_gram (gram1, gram2),
   599       consts = sort_distinct string_ord (consts1 @ consts2),
   600       prmodes = Library.merge (op =) (prmodes1, prmodes2),
   601       parse_ast_trtab =
   602         merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
   603       parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,
   604       parse_trtab = merge_trtabs "parse translation" parse_trtab1 parse_trtab2,
   605       print_trtab = merge_tr'tabs print_trtab1 print_trtab2,
   606       print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2,
   607       print_ast_trtab = merge_tr'tabs print_ast_trtab1 print_ast_trtab2,
   608       tokentrtab = merge_tokentrtabs tokentrtab1 tokentrtab2,
   609       prtabs = Printer.merge_prtabs prtabs1 prtabs2}, stamp ())
   610   end;
   611 
   612 
   613 (* basic syntax *)
   614 
   615 val basic_syntax =
   616   empty_syntax
   617   |> update_syntax mode_default Type_Ext.type_ext
   618   |> update_syntax mode_default Syn_Ext.pure_ext;
   619 
   620 val basic_nonterms =
   621   (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
   622     Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
   623     "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const", "index",
   624     "struct", "id_position", "longid_position", "type_name", "class_name"]);
   625 
   626 
   627 
   628 (** print syntax **)
   629 
   630 local
   631 
   632 fun pretty_strs_qs name strs =
   633   Pretty.strs (name :: map quote (sort_strings strs));
   634 
   635 fun pretty_gram (Syntax (tabs, _)) =
   636   let
   637     val {lexicon, prmodes, gram, ...} = tabs;
   638     val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes);
   639   in
   640     [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
   641       Pretty.big_list "prods:" (Parser.pretty_gram gram),
   642       pretty_strs_qs "print modes:" prmodes']
   643   end;
   644 
   645 fun pretty_trans (Syntax (tabs, _)) =
   646   let
   647     fun pretty_trtab name tab =
   648       pretty_strs_qs name (Symtab.keys tab);
   649 
   650     fun pretty_ruletab name tab =
   651       Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab));
   652 
   653     fun pretty_tokentr (mode, trs) = Pretty.strs (quote mode ^ ":" :: map fst trs);
   654 
   655     val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
   656       print_ruletab, print_ast_trtab, tokentrtab, ...} = tabs;
   657   in
   658     [pretty_strs_qs "consts:" consts,
   659       pretty_trtab "parse_ast_translation:" parse_ast_trtab,
   660       pretty_ruletab "parse_rules:" parse_ruletab,
   661       pretty_trtab "parse_translation:" parse_trtab,
   662       pretty_trtab "print_translation:" print_trtab,
   663       pretty_ruletab "print_rules:" print_ruletab,
   664       pretty_trtab "print_ast_translation:" print_ast_trtab,
   665       Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab)]
   666   end;
   667 
   668 in
   669 
   670 fun print_gram syn = Pretty.writeln (Pretty.chunks (pretty_gram syn));
   671 fun print_trans syn = Pretty.writeln (Pretty.chunks (pretty_trans syn));
   672 fun print_syntax syn = Pretty.writeln (Pretty.chunks (pretty_gram syn @ pretty_trans syn));
   673 
   674 end;
   675 
   676 
   677 (* reconstructing infixes -- educated guessing *)
   678 
   679 fun guess_infix (Syntax ({gram, ...}, _)) c =
   680   (case Parser.guess_infix_lr gram c of
   681     SOME (s, l, r, j) => SOME
   682      (if l then Mixfix.Infixl (s, j)
   683       else if r then Mixfix.Infixr (s, j)
   684       else Mixfix.Infix (s, j))
   685   | NONE => NONE);
   686 
   687 
   688 
   689 (** read **)
   690 
   691 fun some_results f xs =
   692   let
   693     val exn_results = map (Exn.interruptible_capture f) xs;
   694     val exns = map_filter Exn.get_exn exn_results;
   695     val results = map_filter Exn.get_result exn_results;
   696   in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
   697 
   698 
   699 (* read_ast *)
   700 
   701 val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true);
   702 val positions = Config.bool positions_raw;
   703 
   704 val ambiguity_enabled =
   705   Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
   706 
   707 val ambiguity_level_raw = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1);
   708 val ambiguity_level = Config.int ambiguity_level_raw;
   709 
   710 val ambiguity_limit =
   711   Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
   712 
   713 fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
   714 
   715 fun read_asts ctxt type_ctxt (Syntax (tabs, _)) raw root (syms, pos) =
   716   let
   717     val {lexicon, gram, parse_ast_trtab, ...} = tabs;
   718     val toks = Lexicon.tokenize lexicon raw syms;
   719     val _ = List.app (Lexicon.report_token ctxt) toks;
   720 
   721     val pts = Parser.parse ctxt gram root (filter Lexicon.is_proper toks)
   722       handle ERROR msg =>
   723         error (msg ^
   724           implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
   725     val len = length pts;
   726 
   727     val limit = Config.get ctxt ambiguity_limit;
   728     fun show_pt pt =
   729       Pretty.string_of
   730         (Ast.pretty_ast (#2 (Syn_Trans.parsetree_to_ast ctxt type_ctxt false (K NONE) pt)));
   731     val _ =
   732       if len <= Config.get ctxt ambiguity_level then ()
   733       else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
   734       else
   735         (Context_Position.if_visible ctxt warning (cat_lines
   736           (("Ambiguous input" ^ Position.str_of pos ^
   737             "\nproduces " ^ string_of_int len ^ " parse trees" ^
   738             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   739             map show_pt (take limit pts))));
   740 
   741     val constrain_pos = not raw andalso Config.get ctxt positions;
   742   in
   743     some_results
   744       (Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts
   745   end;
   746 
   747 
   748 (* read *)
   749 
   750 fun read ctxt type_ctxt (syn as Syntax (tabs, _)) root inp =
   751   let val {parse_ruletab, parse_trtab, ...} = tabs in
   752     read_asts ctxt type_ctxt syn false root inp
   753     |> map (apsnd (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)))
   754     |> some_results (apsnd (Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab)))
   755   end;
   756 
   757 
   758 (* read terms *)
   759 
   760 fun report_result ctxt (reports, res) =
   761   (List.app (fn (pos, m) => Context_Position.report ctxt pos m) reports; res);
   762 
   763 (*brute-force disambiguation via type-inference*)
   764 fun disambig ctxt _ [arg] = report_result ctxt arg
   765   | disambig ctxt check args =
   766       let
   767         val level = Config.get ctxt ambiguity_level;
   768         val limit = Config.get ctxt ambiguity_limit;
   769 
   770         val ambiguity = length args;
   771         fun ambig_msg () =
   772           if ambiguity > 1 andalso ambiguity <= level then
   773             "Got more than one parse tree.\n\
   774             \Retry with smaller syntax_ambiguity_level for more information."
   775           else "";
   776 
   777         val errs = Par_List.map_name "Syntax.disambig" (check o snd) args;
   778         val results = map_filter (fn (arg, NONE) => SOME arg | _ => NONE) (args ~~ errs);
   779         val len = length results;
   780 
   781         val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
   782       in
   783         if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
   784         else if len = 1 then
   785           (if ambiguity > level then
   786             Context_Position.if_visible ctxt warning
   787               "Fortunately, only one parse tree is type correct.\n\
   788               \You may still want to disambiguate your grammar or your input."
   789           else (); report_result ctxt (hd results))
   790         else cat_error (ambig_msg ()) (cat_lines
   791           (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
   792             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   793             map (show_term o snd) (take limit results)))
   794       end;
   795 
   796 fun standard_parse_term check ctxt type_ctxt term_ctxt syn root (syms, pos) =
   797   read ctxt type_ctxt syn root (syms, pos)
   798   |> map (Type_Ext.decode_term term_ctxt)
   799   |> disambig ctxt check;
   800 
   801 
   802 (* read types *)
   803 
   804 fun standard_parse_typ ctxt type_ctxt syn get_sort (syms, pos) =
   805   (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of
   806     [res] =>
   807       let val t = report_result ctxt res
   808       in Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t end
   809   | _ => error (ambiguity_msg pos));
   810 
   811 
   812 (* read sorts *)
   813 
   814 fun standard_parse_sort ctxt type_ctxt syn (syms, pos) =
   815   (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of
   816     [res] =>
   817       let val t = report_result ctxt res
   818       in Type_Ext.sort_of_term t end
   819   | _ => error (ambiguity_msg pos));
   820 
   821 
   822 
   823 (** prepare translation rules **)
   824 
   825 (* rules *)
   826 
   827 datatype 'a trrule =
   828   Parse_Rule of 'a * 'a |
   829   Print_Rule of 'a * 'a |
   830   Parse_Print_Rule of 'a * 'a;
   831 
   832 fun map_trrule f (Parse_Rule (x, y)) = Parse_Rule (f x, f y)
   833   | map_trrule f (Print_Rule (x, y)) = Print_Rule (f x, f y)
   834   | map_trrule f (Parse_Print_Rule (x, y)) = Parse_Print_Rule (f x, f y);
   835 
   836 fun parse_rule (Parse_Rule pats) = SOME pats
   837   | parse_rule (Print_Rule _) = NONE
   838   | parse_rule (Parse_Print_Rule pats) = SOME pats;
   839 
   840 fun print_rule (Parse_Rule _) = NONE
   841   | print_rule (Print_Rule pats) = SOME (swap pats)
   842   | print_rule (Parse_Print_Rule pats) = SOME (swap pats);
   843 
   844 
   845 fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
   846 
   847 
   848 (* check_rules *)
   849 
   850 local
   851 
   852 fun check_rule rule =
   853   (case Ast.rule_error rule of
   854     SOME msg =>
   855       error ("Error in syntax translation rule: " ^ msg ^ "\n" ^
   856         Pretty.string_of (Ast.pretty_rule rule))
   857   | NONE => rule);
   858 
   859 in
   860 
   861 fun check_rules rules =
   862  (map check_rule (map_filter parse_rule rules),
   863   map check_rule (map_filter print_rule rules));
   864 
   865 end;
   866 
   867 
   868 (* read_rule_pattern *)
   869 
   870 fun read_rule_pattern ctxt type_ctxt syn (root, str) =
   871   let
   872     fun constify (ast as Ast.Constant _) = ast
   873       | constify (ast as Ast.Variable x) =
   874           if is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
   875           else ast
   876       | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   877 
   878     val (syms, pos) = read_token str;
   879   in
   880     (case read_asts ctxt type_ctxt syn true root (syms, pos) of
   881       [res] =>
   882         let val ast = report_result ctxt res
   883         in constify ast end
   884     | _ => error (ambiguity_msg pos))
   885   end;
   886 
   887 
   888 
   889 (** unparse terms, typs, sorts **)
   890 
   891 local
   892 
   893 fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
   894   let
   895     val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
   896     val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
   897   in
   898     Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
   899       (lookup_tokentr tokentrtab (print_mode_value ()))
   900       (Ast.normalize ctxt (Symtab.lookup_list print_ruletab) ast))
   901   end;
   902 
   903 in
   904 
   905 fun standard_unparse_term idents extern =
   906   unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
   907 
   908 fun standard_unparse_typ extern ctxt syn =
   909   unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
   910 
   911 fun standard_unparse_sort {extern_class} ctxt syn =
   912   unparse_t (K Printer.sort_to_ast)
   913     (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
   914     Markup.sort ctxt syn false;
   915 
   916 end;
   917 
   918 
   919 
   920 (** modify syntax **)
   921 
   922 fun ext_syntax f decls = update_syntax mode_default (f decls);
   923 
   924 val update_trfuns = ext_syntax Syn_Ext.syn_ext_trfuns;
   925 val update_advanced_trfuns = ext_syntax Syn_Ext.syn_ext_advanced_trfuns;
   926 val extend_tokentrfuns = ext_syntax Syn_Ext.syn_ext_tokentrfuns;
   927 
   928 fun update_type_gram add prmode decls =
   929   (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
   930 
   931 fun update_const_gram add is_logtype prmode decls =
   932   (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
   933 
   934 val update_trrules = ext_syntax Syn_Ext.syn_ext_rules o check_rules;
   935 val remove_trrules = remove_syntax mode_default o Syn_Ext.syn_ext_rules o check_rules;
   936 
   937 
   938 (*export parts of internal Syntax structures*)
   939 open Lexicon Syn_Ext Ast Parser Type_Ext Syn_Trans Mixfix Printer;
   940 
   941 end;
   942 
   943 structure Basic_Syntax: BASIC_SYNTAX = Syntax;
   944 open Basic_Syntax;
   945 
   946 forget_structure "Ast";
   947 forget_structure "Syn_Ext";
   948 forget_structure "Parser";
   949 forget_structure "Type_Ext";
   950 forget_structure "Syn_Trans";
   951 forget_structure "Mixfix";
   952 forget_structure "Printer";