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