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