src/Pure/Syntax/syntax.ML
author wenzelm
Mon Sep 29 14:11:18 1997 +0200 (1997-09-29)
changeset 3739 13f7107676a0
parent 3526 df4d0dad2b4e
child 3779 ce8594f7e0c6
permissions -rw-r--r--
improved warning;
     1 (*  Title:      Pure/Syntax/syntax.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     5 Root of Isabelle's syntax module.
     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   datatype 'a trrule =
    26     ParseRule of 'a * 'a |
    27     PrintRule of 'a * 'a |
    28     ParsePrintRule of 'a * 'a
    29   type syntax
    30   val extend_log_types: syntax -> string list -> syntax
    31   val extend_type_gram: syntax -> (string * int * mixfix) list -> syntax
    32   val extend_const_gram: syntax -> string * bool -> (string * typ * mixfix) list -> syntax
    33   val extend_consts: syntax -> string list -> syntax
    34   val extend_trfuns: syntax ->
    35     (string * (ast list -> ast)) list *
    36     (string * (term list -> term)) list *
    37     (string * (term list -> term)) list *
    38     (string * (ast list -> ast)) list -> syntax
    39   val extend_trfunsT: syntax -> (string * (typ -> term list -> term)) list -> syntax
    40   val extend_tokentrfuns: syntax -> (string * string * (string -> string * int)) list -> syntax
    41   val extend_trrules: syntax -> (string * string) trrule list -> syntax
    42   val extend_trrules_i: syntax -> ast trrule list -> syntax
    43   val merge_syntaxes: syntax -> syntax -> syntax
    44   val type_syn: syntax
    45   val pure_syn: syntax
    46   val print_gram: syntax -> unit
    47   val print_trans: syntax -> unit
    48   val print_syntax: syntax -> unit
    49   val test_read: syntax -> string -> string -> unit
    50   val read: syntax -> typ -> string -> term list
    51   val read_typ: syntax -> (sort * sort -> bool)
    52     -> ((indexname * sort) list -> indexname -> sort) -> string -> typ
    53   val simple_read_typ: string -> typ
    54   val pretty_term: bool -> syntax -> term -> Pretty.T
    55   val pretty_typ: syntax -> typ -> Pretty.T
    56   val string_of_term: bool -> syntax -> term -> string
    57   val string_of_typ: syntax -> typ -> string
    58   val simple_string_of_typ: typ -> string
    59   val simple_pprint_typ: typ -> pprint_args -> unit
    60   val ambiguity_level: int ref
    61 end;
    62 
    63 structure Syntax : SYNTAX =
    64 struct
    65 
    66 open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
    67 
    68 
    69 (** tables of translation functions **)
    70 
    71 (*does not subsume typed print translations*)
    72 type 'a trtab = (('a list -> 'a) * stamp) Symtab.table;
    73 
    74 val dest_trtab = Symtab.dest;
    75 
    76 fun lookup_trtab tab c =
    77   apsome fst (Symtab.lookup (tab, c));
    78 
    79 
    80 (* empty, extend, merge trtabs *)
    81 
    82 fun err_dup_trfuns name cs =
    83   error ("More than one " ^ name ^ " for " ^ commas_quote cs);
    84 
    85 val empty_trtab = Symtab.null;
    86 
    87 fun extend_trtab tab trfuns name =
    88   Symtab.extend_new (tab, map (fn (c, f) => (c, (f, stamp ()))) trfuns)
    89     handle Symtab.DUPS cs => err_dup_trfuns name cs;
    90 
    91 fun merge_trtabs tab1 tab2 name =
    92   Symtab.merge eq_snd (tab1, tab2)
    93     handle Symtab.DUPS cs => err_dup_trfuns name cs;
    94 
    95 
    96 
    97 (** tables of token translation functions **)
    98 
    99 fun lookup_tokentr tabs modes =
   100   let val trs = gen_distinct eq_fst (flat (map (assocs tabs) (modes @ [""])))
   101   in fn c => apsome fst (assoc (trs, c)) end;
   102 
   103 fun merge_tokentrtabs tabs1 tabs2 =
   104   let
   105     fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
   106 
   107     fun name (s, _) = implode (tl (explode s));
   108 
   109     fun merge mode =
   110       let
   111         val trs1 = assocs tabs1 mode;
   112         val trs2 = assocs tabs2 mode;
   113         val trs = gen_distinct eq_tr (trs1 @ trs2);
   114       in
   115         (case gen_duplicates eq_fst trs of
   116           [] => (mode, trs)
   117         | dups => error ("More than one token translation function in mode " ^
   118             quote mode ^ " for " ^ commas_quote (map name dups)))
   119       end;
   120   in
   121     map merge (distinct (map fst (tabs1 @ tabs2)))
   122   end;
   123 
   124 fun extend_tokentrtab tabs tokentrs =
   125   let
   126     fun ins_tokentr (ts, (m, c, f)) =
   127       overwrite (ts, (m, ("_" ^ c, (f, stamp ())) :: assocs ts m));
   128   in
   129     merge_tokentrtabs tabs (foldl ins_tokentr ([], tokentrs))
   130   end;
   131 
   132 
   133 
   134 (** tables of translation rules **)
   135 
   136 type ruletab = (ast * ast) list Symtab.table;
   137 
   138 fun dest_ruletab tab = flat (map snd (Symtab.dest tab));
   139 
   140 
   141 (* lookup_ruletab *)
   142 
   143 fun lookup_ruletab tab =
   144   if Symtab.is_null tab then None
   145   else Some (fn a => Symtab.lookup_multi (tab, a));
   146 
   147 
   148 (* empty, extend, merge ruletabs *)
   149 
   150 val empty_ruletab = Symtab.null;
   151 
   152 fun extend_ruletab tab rules =
   153   generic_extend (op =) Symtab.dest_multi Symtab.make_multi tab
   154     (map (fn r => (head_of_rule r, r)) (distinct rules));
   155 
   156 fun merge_ruletabs tab1 tab2 =
   157   generic_merge (op =) Symtab.dest_multi Symtab.make_multi tab1 tab2;
   158 
   159 
   160 
   161 (** datatype syntax **)
   162 
   163 datatype syntax =
   164   Syntax of {
   165     lexicon: lexicon,
   166     logtypes: string list,
   167     gram: gram,
   168     consts: string list,
   169     prmodes: string list,
   170     parse_ast_trtab: ast trtab,
   171     parse_ruletab: ruletab,
   172     parse_trtab: term trtab,
   173     print_trtab: ((typ -> term list -> term) * stamp) Symtab.table,
   174     print_ruletab: ruletab,
   175     print_ast_trtab: ast trtab,
   176     tokentrtab: (string * (string * ((string -> string * int) * stamp)) list) list,
   177     prtabs: prtabs}
   178 
   179 
   180 (* empty_syntax *)
   181 
   182 val empty_syntax =
   183   Syntax {
   184     lexicon = empty_lexicon,
   185     logtypes = [],
   186     gram = empty_gram,
   187     consts = [],
   188     prmodes = [],
   189     parse_ast_trtab = empty_trtab,
   190     parse_ruletab = empty_ruletab,
   191     parse_trtab = empty_trtab,
   192     print_trtab = empty_trtab,
   193     print_ruletab = empty_ruletab,
   194     print_ast_trtab = empty_trtab,
   195     tokentrtab = [],
   196     prtabs = empty_prtabs}
   197 
   198 
   199 (* extend_syntax *)
   200 
   201 fun extend_syntax (mode, inout) (Syntax tabs) syn_ext =
   202   let
   203     val {lexicon, logtypes = logtypes1, gram, consts = consts1, prmodes = prmodes1,
   204       parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
   205       print_ast_trtab, tokentrtab, prtabs} = tabs;
   206     val SynExt {logtypes = logtypes2, xprods, consts = consts2, prmodes = prmodes2,
   207       parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
   208       print_ast_translation, token_translation} = syn_ext;
   209   in
   210     Syntax {
   211       lexicon = if inout then extend_lexicon lexicon (delims_of xprods) else lexicon,
   212       logtypes = extend_list logtypes1 logtypes2,
   213       gram = if inout then extend_gram gram xprods else gram,
   214       consts = consts2 union consts1,
   215       prmodes = (mode ins prmodes2) union prmodes1,
   216       parse_ast_trtab =
   217         extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
   218       parse_ruletab = extend_ruletab parse_ruletab parse_rules,
   219       parse_trtab = extend_trtab parse_trtab parse_translation "parse translation",
   220       print_trtab = extend_trtab print_trtab print_translation "print translation",
   221       print_ruletab = extend_ruletab print_ruletab print_rules,
   222       print_ast_trtab =
   223         extend_trtab print_ast_trtab print_ast_translation "print ast translation",
   224       tokentrtab = extend_tokentrtab tokentrtab token_translation,
   225       prtabs = extend_prtabs prtabs mode xprods}
   226   end;
   227 
   228 
   229 (* merge_syntaxes *)
   230 
   231 fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) =
   232   let
   233     val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1, consts = consts1,
   234       prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
   235       parse_trtab = parse_trtab1, print_trtab = print_trtab1,
   236       print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1,
   237       tokentrtab = tokentrtab1, prtabs = prtabs1} = tabs1;
   238 
   239     val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2, consts = consts2,
   240       prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
   241       parse_trtab = parse_trtab2, print_trtab = print_trtab2,
   242       print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2,
   243       tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2;
   244   in
   245     Syntax {
   246       lexicon = merge_lexicons lexicon1 lexicon2,
   247       logtypes = merge_lists logtypes1 logtypes2,
   248       gram = merge_grams gram1 gram2,
   249       consts = merge_lists consts1 consts2,
   250       prmodes = merge_lists prmodes1 prmodes2,
   251       parse_ast_trtab =
   252         merge_trtabs parse_ast_trtab1 parse_ast_trtab2 "parse ast translation",
   253       parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,
   254       parse_trtab = merge_trtabs parse_trtab1 parse_trtab2 "parse translation",
   255       print_trtab = merge_trtabs print_trtab1 print_trtab2 "print translation",
   256       print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2,
   257       print_ast_trtab =
   258         merge_trtabs print_ast_trtab1 print_ast_trtab2 "print ast translation",
   259       tokentrtab = merge_tokentrtabs tokentrtab1 tokentrtab2,
   260       prtabs = merge_prtabs prtabs1 prtabs2}
   261   end;
   262 
   263 
   264 (* type_syn *)
   265 
   266 val type_syn =
   267   extend_syntax ("", true) empty_syntax type_ext;
   268 
   269 val pure_syn = extend_syntax ("", true) type_syn pure_ext;
   270 
   271 
   272 (** inspect syntax **)
   273 
   274 fun pretty_strs_qs name strs =
   275   Pretty.strs (name :: map quote (sort_strings strs));
   276 
   277 
   278 (* print_gram *)
   279 
   280 fun print_gram (Syntax tabs) =
   281   let
   282     val {lexicon, logtypes, prmodes, gram, prtabs, ...} = tabs;
   283     val prmodes' = sort_strings (filter_out (equal "") prmodes);
   284   in
   285     Pretty.writeln (pretty_strs_qs "lexicon:" (dest_lexicon lexicon));
   286     Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
   287     Pretty.writeln (Pretty.big_list "prods:" (pretty_gram gram));
   288     Pretty.writeln (pretty_strs_qs "print modes:" prmodes')
   289   end;
   290 
   291 
   292 (* print_trans *)
   293 
   294 fun print_trans (Syntax tabs) =
   295   let
   296     fun pretty_trtab name tab =
   297       pretty_strs_qs name (map fst (dest_trtab tab));
   298 
   299     fun pretty_ruletab name tab =
   300       Pretty.big_list name (map pretty_rule (dest_ruletab tab));
   301 
   302     val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
   303       print_ruletab, print_ast_trtab, ...} = tabs;
   304   in
   305     Pretty.writeln (pretty_strs_qs "consts:" consts);
   306     Pretty.writeln (pretty_trtab "parse_ast_translation:" parse_ast_trtab);
   307     Pretty.writeln (pretty_ruletab "parse_rules:" parse_ruletab);
   308     Pretty.writeln (pretty_trtab "parse_translation:" parse_trtab);
   309     Pretty.writeln (pretty_trtab "print_translation:" print_trtab);
   310     Pretty.writeln (pretty_ruletab "print_rules:" print_ruletab);
   311     Pretty.writeln (pretty_trtab "print_ast_translation:" print_ast_trtab)
   312   end;
   313 
   314 
   315 (* print_syntax *)
   316 
   317 fun print_syntax syn = (print_gram syn; print_trans syn);
   318 
   319 
   320 
   321 (** read **)
   322 
   323 (* test_read *)
   324 
   325 fun test_read (Syntax tabs) root str =
   326   let
   327     val {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs;
   328 
   329     val chars = SymbolFont.read_charnames (explode str);
   330     val toks = tokenize lexicon false chars;
   331     val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks));
   332 
   333     fun show_pt pt =
   334       let
   335         val raw_ast = pt_to_ast (K None) pt;
   336         val _ = writeln ("raw: " ^ str_of_ast raw_ast);
   337         val pre_ast = pt_to_ast (lookup_trtab parse_ast_trtab) pt;
   338         val _ = normalize true true (lookup_ruletab parse_ruletab) pre_ast;
   339       in () end;
   340   in
   341     seq show_pt (parse gram root toks)
   342   end;
   343 
   344 
   345 (* read_ast *)
   346 
   347 val ambiguity_level = ref 1;
   348 
   349 fun read_asts (Syntax tabs) xids root str =
   350   let
   351     val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs;
   352     val root' = if root mem logtypes then logic else root;
   353     val chars = SymbolFont.read_charnames (explode str);
   354     val pts = parse gram root' (tokenize lexicon xids chars);
   355 
   356     fun show_pt pt =
   357       warning (Pretty.string_of (pretty_ast (pt_to_ast (K None) pt)));
   358   in
   359     if length pts > ! ambiguity_level then
   360       (warning ("Ambiguous input " ^ quote str);
   361        warning "produces the following parse trees:";
   362        seq show_pt pts)
   363     else ();
   364     map (pt_to_ast (lookup_trtab parse_ast_trtab)) pts
   365   end;
   366 
   367 
   368 (* read *)
   369 
   370 fun read (syn as Syntax tabs) ty str =
   371   let
   372     val {parse_ruletab, parse_trtab, ...} = tabs;
   373     val asts = read_asts syn false (typ_to_nonterm ty) str;
   374   in
   375     map (ast_to_term (lookup_trtab parse_trtab))
   376       (map (normalize_ast (lookup_ruletab parse_ruletab)) asts)
   377   end;
   378 
   379 
   380 (* read types *)
   381 
   382 fun read_typ syn eq_sort get_sort str =
   383   (case read syn typeT str of
   384     [t] => typ_of_term (get_sort (raw_term_sorts eq_sort t)) t
   385   | _ => error "read_typ: ambiguous type syntax");
   386 
   387 fun simple_read_typ str =
   388   let fun get_sort env xi = if_none (assoc (env, xi)) [] in
   389     read_typ type_syn eq_set_string get_sort str
   390   end;
   391 
   392 
   393 
   394 (** prepare translation rules **)
   395 
   396 datatype 'a trrule =
   397   ParseRule of 'a * 'a |
   398   PrintRule of 'a * 'a |
   399   ParsePrintRule of 'a * 'a;
   400 
   401 fun map_rule f (ParseRule (x, y)) = ParseRule (f x, f y)
   402   | map_rule f (PrintRule (x, y)) = PrintRule (f x, f y)
   403   | map_rule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y);
   404 
   405 fun parse_rule (ParseRule pats) = Some pats
   406   | parse_rule (PrintRule _) = None
   407   | parse_rule (ParsePrintRule pats) = Some pats;
   408 
   409 fun print_rule (ParseRule _) = None
   410   | print_rule (PrintRule pats) = Some (swap pats)
   411   | print_rule (ParsePrintRule pats) = Some (swap pats);
   412 
   413 
   414 fun check_rule (rule as (lhs, rhs)) =
   415   (case rule_error rule of
   416     Some msg =>
   417       error ("Error in syntax translation rule: " ^ msg ^ "\n" ^
   418         str_of_ast lhs ^ "  ->  " ^ str_of_ast rhs)
   419   | None => rule);
   420 
   421 
   422 fun read_pattern syn (root, str) =
   423   let
   424     val Syntax {consts, ...} = syn;
   425 
   426     fun constify (ast as Constant _) = ast
   427       | constify (ast as Variable x) =
   428           if x mem consts then Constant x else ast
   429       | constify (Appl asts) = Appl (map constify asts);
   430   in
   431     (case read_asts syn true root str of
   432       [ast] => constify ast
   433     | _ => error ("Syntactically ambiguous input: " ^ quote str))
   434   end handle ERROR =>
   435     error ("The error(s) above occurred in translation pattern " ^
   436       quote str);
   437 
   438 
   439 fun prep_rules rd_pat raw_rules =
   440   let val rules = map (map_rule rd_pat) raw_rules in
   441     (map check_rule (mapfilter parse_rule rules),
   442       map check_rule (mapfilter print_rule rules))
   443   end
   444 
   445 
   446 
   447 (** pretty terms or typs **)
   448 
   449 fun pretty_t t_to_ast prt_t curried (syn as Syntax tabs) t =
   450   let
   451     val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
   452     val ast = t_to_ast (lookup_trtab print_trtab) t;
   453   in
   454     prt_t curried prtabs (lookup_trtab print_ast_trtab)
   455       (lookup_tokentr tokentrtab (! print_mode))
   456       (normalize_ast (lookup_ruletab print_ruletab) ast)
   457   end;
   458 
   459 val pretty_term = pretty_t term_to_ast pretty_term_ast;
   460 val pretty_typ = pretty_t typ_to_ast pretty_typ_ast false;
   461 
   462 fun string_of_term curried syn t =
   463   Pretty.string_of (pretty_term curried syn t);
   464 fun string_of_typ syn ty = Pretty.string_of (pretty_typ syn ty);
   465 
   466 val simple_string_of_typ = string_of_typ type_syn;
   467 val simple_pprint_typ = Pretty.pprint o Pretty.quote o (pretty_typ type_syn);
   468 
   469 
   470 
   471 (** extend syntax (external interfaces) **)
   472 
   473 fun ext_syntax mk_syn_ext prmode (syn as Syntax {logtypes, ...}) decls =
   474   extend_syntax prmode syn (mk_syn_ext logtypes decls);
   475 
   476 
   477 fun extend_log_types syn logtypes =
   478   extend_syntax ("", true) syn (syn_ext_logtypes logtypes);
   479 
   480 val extend_type_gram = ext_syntax syn_ext_types ("", true);
   481 
   482 fun extend_const_gram syn prmode = ext_syntax syn_ext_consts prmode syn;
   483 
   484 val extend_consts = ext_syntax syn_ext_const_names ("", true);
   485 
   486 val extend_trfuns = ext_syntax syn_ext_trfuns ("", true);
   487 
   488 val extend_trfunsT = ext_syntax syn_ext_trfunsT ("", true);
   489 
   490 val extend_tokentrfuns = ext_syntax syn_ext_tokentrfuns ("", true);
   491 
   492 fun extend_trrules syn rules =
   493   ext_syntax syn_ext_rules ("", true) syn (prep_rules (read_pattern syn) rules);
   494 
   495 fun extend_trrules_i syn rules =
   496   ext_syntax syn_ext_rules ("", true) syn (prep_rules I rules);
   497 
   498 
   499 end;