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