src/Pure/Syntax/syntax.ML
author wenzelm
Mon Nov 29 12:32:42 1993 +0100 (1993-11-29)
changeset 167 128e122acc89
parent 144 0a0da273a6c5
child 168 1bf4e2cab673
permissions -rw-r--r--
added (partial) extend_tables;
improved extend;
fixed roots handling of extend and merge;
     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 TODO:
     8   fix empty_tables, extend_tables, mk_tables (requires empty_gram, extend_gram)
     9   fix extend (requires extend_tables)
    10 *)
    11 
    12 signature SYNTAX =
    13 sig
    14   include AST0
    15   include LEXICON0
    16   include EXTENSION0
    17   include TYPE_EXT0
    18   include SEXTENSION1
    19   include PRINTER0
    20   type syntax
    21   val type_syn: syntax
    22   val extend: syntax -> (string -> typ) -> string list * string list * sext -> syntax
    23   val merge: string list -> syntax -> syntax -> syntax
    24   val print_gram: syntax -> unit
    25   val print_trans: syntax -> unit
    26   val print_syntax: syntax -> unit
    27   val test_read: syntax -> string -> string -> unit
    28   val read: syntax -> typ -> string -> term
    29   val read_typ: syntax -> (indexname -> sort) -> string -> typ
    30   val pretty_term: syntax -> term -> Pretty.T
    31   val pretty_typ: syntax -> typ -> Pretty.T
    32   val string_of_term: syntax -> term -> string
    33   val string_of_typ: syntax -> typ -> string
    34 end;
    35 
    36 functor SyntaxFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT
    37   and Parser: PARSER and SExtension: SEXTENSION and Printer: PRINTER
    38   sharing TypeExt.Extension = SExtension.Extension
    39   and Parser.XGram = TypeExt.Extension.XGram = Printer.XGram
    40   and Parser.XGram.Ast = Parser.ParseTree.Ast): SYNTAX =
    41 struct
    42 
    43 structure Extension = TypeExt.Extension;
    44 structure XGram = Extension.XGram;
    45 structure Lexicon = Parser.ParseTree.Lexicon;
    46 open Lexicon Parser Parser.ParseTree Extension TypeExt SExtension Printer
    47   XGram XGram.Ast;
    48 
    49 
    50 fun lookup tab a = Symtab.lookup (tab, a);
    51 
    52 
    53 
    54 (** datatype syntax **)
    55 
    56 datatype tables =
    57   Tabs of {
    58     lexicon: lexicon,
    59     roots: string list,
    60     gram: gram,
    61     consts: string list,
    62     parse_ast_trtab: (ast list -> ast) Symtab.table,
    63     parse_ruletab: (ast * ast) list Symtab.table,
    64     parse_trtab: (term list -> term) Symtab.table,
    65     print_trtab: (term list -> term) Symtab.table,
    66     print_ruletab: (ast * ast) list Symtab.table,
    67     prtab: prtab};
    68 
    69 datatype gramgraph =
    70   EmptyGG |
    71   ExtGG of gramgraph ref * ext |
    72   MergeGG of gramgraph ref * gramgraph ref;
    73 
    74 datatype syntax = Syntax of gramgraph ref * tables;
    75 
    76 
    77 
    78 (*** compile syntax ***)
    79 
    80 (* translation funs *)
    81 
    82 fun extend_trtab tab trfuns name =
    83   Symtab.balance (Symtab.st_of_alist (trfuns, tab)) handle Symtab.DUPLICATE s
    84     => error ("More than one " ^ name ^ " for " ^ quote s);
    85 
    86 val mk_trtab = extend_trtab Symtab.null;
    87 
    88 
    89 (* translation rules *)
    90 
    91 fun mk_ruletab rules =
    92   let
    93     fun add_rule (r, tab) =
    94       let val a = head_of_rule r;
    95       in
    96         (case lookup tab a of
    97           None => Symtab.update ((a, [r]), tab)
    98         | Some rs => Symtab.update ((a, r :: rs), tab))
    99       end;
   100   in
   101     Symtab.balance (foldr add_rule (rules, Symtab.null))
   102   end;
   103 
   104 fun extend_ruletab tab rules =
   105   mk_ruletab (flat (map #2 (Symtab.alist_of tab)) @ rules);
   106 
   107 
   108 
   109 (** tables **)
   110 
   111 (* empty_tables *)
   112 
   113 val empty_tables =
   114   Tabs {
   115     lexicon = empty_lexicon,
   116     roots = [],
   117     (* gram = empty_gram, *)    (* FIXME *)
   118     gram = mk_gram [] [],       (* FIXME *)
   119     consts = [],
   120     parse_ast_trtab = Symtab.null,
   121     parse_ruletab = Symtab.null,
   122     parse_trtab = Symtab.null,
   123     print_trtab = Symtab.null,
   124     print_ruletab = Symtab.null,
   125     prtab = empty_prtab};
   126 
   127 
   128 (* extend_tables *)
   129 
   130 fun extend_tables (Tabs tabs) (XGram xgram) =
   131   let
   132     val {lexicon, roots = roots1, gram, consts = consts1, parse_ast_trtab,
   133       parse_ruletab, parse_trtab, print_trtab, print_ruletab, prtab} = tabs;
   134     val {roots = roots2, prods, consts = consts2, parse_ast_translation,
   135       parse_rules, parse_translation, print_translation, print_rules,
   136       print_ast_translation} = xgram;
   137   in
   138     (* FIXME *)
   139     if not (null prods) then
   140       error "extend_tables: called with non-empty prods"
   141     else
   142 
   143     Tabs {
   144       lexicon = extend_lexicon lexicon (literals_of prods),
   145       roots = roots2 union roots1,
   146       (* gram = extend_gram gram roots2 prods, *)  (* FIXME *)
   147       gram = gram,                                 (* FIXME *)
   148       consts = consts2 union consts1,
   149       parse_ast_trtab =
   150         extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
   151       parse_ruletab = extend_ruletab parse_ruletab parse_rules,
   152       parse_trtab = extend_trtab parse_trtab parse_translation "parse translation",
   153       print_trtab = extend_trtab print_trtab print_translation "print translation",
   154       print_ruletab = extend_ruletab print_ruletab print_rules,
   155       prtab = extend_prtab prtab prods print_ast_translation}
   156   end;
   157 
   158 
   159 (* mk_tables *)
   160 
   161 val mk_tables = extend_tables empty_tables;
   162 
   163 (* FIXME *)
   164 fun mk_tables (XGram xgram) =
   165   let
   166     val {roots, prods, consts, parse_ast_translation, parse_rules,
   167       parse_translation, print_translation, print_rules,
   168       print_ast_translation} = xgram;
   169   in
   170     Tabs {
   171       lexicon = mk_lexicon (literals_of prods),
   172       roots = roots,
   173       gram = mk_gram roots prods,
   174       consts = consts,
   175       parse_ast_trtab = mk_trtab parse_ast_translation "parse ast translation",
   176       parse_ruletab = mk_ruletab parse_rules,
   177       parse_trtab = mk_trtab parse_translation "parse translation",
   178       print_trtab = mk_trtab print_translation "print translation",
   179       print_ruletab = mk_ruletab print_rules,
   180       prtab = mk_prtab prods print_ast_translation}
   181   end;
   182 
   183 
   184 (* ggr_to_xgram *)
   185 
   186 fun ggr_to_xgram ggr =
   187   let
   188     fun flatGG ggr (xg, v) =
   189       if ggr mem v then (xg, v) else flatGG' ggr (xg, ggr :: v)
   190     and flatGG' (ref EmptyGG) xgv = xgv
   191       | flatGG' (ref (ExtGG (ggr, ext))) xgv =
   192           let
   193             val (xg', v') = flatGG ggr xgv;
   194           in
   195             (extend_xgram xg' ext, v')
   196           end
   197       | flatGG' (ref (MergeGG (ggr1, ggr2))) xgv =
   198           flatGG ggr1 (flatGG ggr2 xgv);
   199   in
   200     #1 (flatGG ggr (empty_xgram, []))
   201   end;
   202 
   203 
   204 (* mk_syntax *)
   205 
   206 fun mk_syntax ggr = Syntax (ggr, mk_tables (ggr_to_xgram ggr));
   207 
   208 
   209 
   210 (*** inspect syntax ***)
   211 
   212 fun xgram_of (Syntax (ggr, _)) = ggr_to_xgram ggr;
   213 
   214 fun string_of_big_list name prts =
   215   Pretty.string_of (Pretty.blk (2,
   216     separate Pretty.fbrk (Pretty.str name :: prts)));
   217 
   218 fun string_of_strings name strs =
   219   Pretty.string_of (Pretty.blk (2,
   220     separate (Pretty.brk 1)
   221       (map Pretty.str (name :: map quote (sort_strings strs)))));
   222 
   223 
   224 (* print_gram *)
   225 
   226 fun prt_gram (XGram {roots, prods, ...}) =
   227   let
   228     fun pretty_name name = [Pretty.str (name ^ " ="), Pretty.brk 1];
   229 
   230     fun pretty_xsymbs (Terminal s :: xs) =
   231           Pretty.str (quote s) :: Pretty.brk 1 :: pretty_xsymbs xs
   232       | pretty_xsymbs (Nonterminal (s, p) :: xs) =
   233           (if is_terminal s then Pretty.str s
   234           else Pretty.str (s ^ "[" ^ string_of_int p ^ "]"))
   235             :: Pretty.brk 1 :: pretty_xsymbs xs
   236       | pretty_xsymbs (_ :: xs) = pretty_xsymbs xs
   237       | pretty_xsymbs [] = [];
   238 
   239     fun pretty_const "" = [Pretty.brk 1]
   240       | pretty_const c = [Pretty.str (" => " ^ quote c), Pretty.brk 1];
   241 
   242     fun pretty_pri p = [Pretty.str ("(" ^ string_of_int p ^ ")")];
   243 
   244     fun pretty_prod (Prod (name, xsymbs, const, pri)) =
   245       Pretty.blk (2, pretty_name name @ pretty_xsymbs xsymbs @
   246         pretty_const const @ pretty_pri pri);
   247   in
   248     writeln (string_of_strings "lexicon:" (literals_of prods));
   249     writeln (Pretty.string_of (Pretty.blk (2,
   250       separate (Pretty.brk 1) (map Pretty.str ("roots:" :: roots)))));
   251     writeln (string_of_big_list "prods:" (map pretty_prod prods))
   252   end;
   253 
   254 val print_gram = prt_gram o xgram_of;
   255 
   256 
   257 (* print_trans *)
   258 
   259 fun prt_trans (XGram xgram) =
   260   let
   261     fun string_of_trs name trs = string_of_strings name (map fst trs);
   262 
   263     fun string_of_rules name rules =
   264       string_of_big_list name (map pretty_rule rules);
   265 
   266     val {consts, parse_ast_translation, parse_rules, parse_translation,
   267       print_translation, print_rules, print_ast_translation, ...} = xgram;
   268   in
   269     writeln (string_of_strings "consts:" consts);
   270     writeln (string_of_trs "parse_ast_translation:" parse_ast_translation);
   271     writeln (string_of_rules "parse_rules:" parse_rules);
   272     writeln (string_of_trs "parse_translation:" parse_translation);
   273     writeln (string_of_trs "print_translation:" print_translation);
   274     writeln (string_of_rules "print_rules:" print_rules);
   275     writeln (string_of_trs "print_ast_translation:" print_ast_translation)
   276   end;
   277 
   278 val print_trans = prt_trans o xgram_of;
   279 
   280 
   281 (* print_syntax *)
   282 
   283 fun print_syntax syn =
   284   let
   285     val xgram = xgram_of syn;
   286   in
   287     prt_gram xgram; prt_trans xgram
   288   end;
   289 
   290 
   291 
   292 (*** parsing and printing ***)
   293 
   294 (* mk_get_rules *)
   295 
   296 fun mk_get_rules ruletab =
   297   let
   298     fun get_rules a =
   299       (case lookup ruletab a of
   300         Some rules => rules
   301       | None => []);
   302   in
   303     if Symtab.is_null ruletab then None else Some get_rules
   304   end;
   305 
   306 
   307 (* read_ast *)
   308 
   309 fun read_ast (Syntax (_, tabs)) xids root str =
   310   let
   311     val Tabs {lexicon, gram, parse_ast_trtab, ...} = tabs;
   312   in
   313     pt_to_ast (lookup parse_ast_trtab)
   314       (parse gram root (tokenize lexicon xids str))
   315   end;
   316 
   317 
   318 
   319 (** test_read **)
   320 
   321 fun test_read (Syntax (_, tabs)) root str =
   322   let
   323     val Tabs {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs;
   324 
   325     val toks = tokenize lexicon false str;
   326     val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks));
   327 
   328     val pt = parse gram root toks;
   329     val raw_ast = pt_to_ast (K None) pt;
   330     val _ = writeln ("raw: " ^ str_of_ast raw_ast);
   331 
   332     val pre_ast = pt_to_ast (lookup parse_ast_trtab) pt;
   333     val _ = normalize true true (mk_get_rules parse_ruletab) pre_ast;
   334   in () end;
   335 
   336 
   337 
   338 (** read **)
   339 
   340 fun read (syn as Syntax (_, tabs)) ty str =
   341   let
   342     val Tabs {parse_ruletab, parse_trtab, ...} = tabs;
   343     val ast = read_ast syn false (typ_to_nonterm ty) str;
   344   in
   345     ast_to_term (lookup parse_trtab)
   346       (normalize_ast (mk_get_rules parse_ruletab) ast)
   347   end;
   348 
   349 
   350 
   351 (** read_typ **)
   352 
   353 fun read_typ syn def_sort str = typ_of_term def_sort (read syn typeT str);
   354 
   355 
   356 
   357 (** read_rule **)
   358 
   359 fun read_rule syn (xrule as ((_, lhs_src), (_, rhs_src))) =
   360   let
   361     val Syntax (_, Tabs {consts, ...}) = syn;
   362 
   363     fun constantify (ast as Constant _) = ast
   364       | constantify (ast as Variable x) =
   365           if x mem consts then Constant x else ast
   366       | constantify (Appl asts) = Appl (map constantify asts);
   367 
   368     fun read_pat (root, str) =
   369       constantify (read_ast syn true root str)
   370         handle ERROR => error ("The error above occurred in " ^ quote str);
   371 
   372     val rule as (lhs, rhs) = (pairself read_pat) xrule;
   373   in
   374     (case rule_error rule of
   375       Some msg =>
   376         error ("Error in syntax translation rule: " ^ msg ^
   377           "\nexternal: " ^ quote lhs_src ^ "  ->  " ^ quote rhs_src ^
   378           "\ninternal: " ^ str_of_ast lhs ^ "  ->  " ^ str_of_ast rhs)
   379     | None => rule)
   380   end;
   381 
   382 
   383 
   384 (** read_xrules **)
   385 
   386 fun read_xrules syn xrules =
   387   let
   388     fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2)
   389       | right_rule (xpat1 <-| xpat2) = None
   390       | right_rule (xpat1 <-> xpat2) = Some (xpat1, xpat2);
   391 
   392     fun left_rule (xpat1 |-> xpat2) = None
   393       | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1)
   394       | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1);
   395   in
   396     (map (read_rule syn) (mapfilter right_rule xrules),
   397      map (read_rule syn) (mapfilter left_rule xrules))
   398   end;
   399 
   400 
   401 
   402 (** pretty terms or typs **)
   403 
   404 fun pretty_t t_to_ast pretty_t (syn as Syntax (_, tabs)) t =
   405   let
   406     val Tabs {print_trtab, print_ruletab, prtab, ...} = tabs;
   407     val ast = t_to_ast (lookup print_trtab) t;
   408   in
   409     pretty_t prtab (normalize_ast (mk_get_rules print_ruletab) ast)
   410   end;
   411 
   412 val pretty_term = pretty_t term_to_ast pretty_term_ast;
   413 
   414 val pretty_typ = pretty_t typ_to_ast pretty_typ_ast;
   415 
   416 fun string_of_term syn t = Pretty.string_of (pretty_term syn t);
   417 
   418 fun string_of_typ syn ty = Pretty.string_of (pretty_typ syn ty);
   419 
   420 
   421 
   422 (*** build syntax ***)
   423 
   424 (* type_syn *)
   425 
   426 val type_syn = mk_syntax (ref (ExtGG (ref EmptyGG, type_ext)));
   427 
   428 
   429 (* extend *)  (* FIXME *)
   430 
   431 fun old_extend syn read_ty (roots, xconsts, sext) =
   432   let
   433     val Syntax (ggr0, Tabs {roots = roots0, ...}) = syn;
   434 
   435     val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext;
   436     val (syn1 as Syntax (ggr1, tabs1)) = mk_syntax (ref (ExtGG (ggr0, ext1)));
   437 
   438     val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext);
   439     val ext2 = ExtRules {parse_rules = parse_rules, print_rules = print_rules};
   440   in
   441     Syntax (ref (ExtGG (ggr1, ext2)), extend_tables tabs1 (mk_xgram ext2))
   442   end;
   443 
   444 
   445 fun new_extend syn read_ty (roots, xconsts, sext) =
   446   let
   447     val Syntax (ggr0, tabs0 as Tabs {roots = roots0, ...}) = syn;
   448 
   449     val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext;
   450     val (syn1 as Syntax (ggr1, tabs1)) =
   451       Syntax (ref (ExtGG (ggr0, ext1)), extend_tables tabs0 (mk_xgram ext1));
   452 
   453     val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext);
   454     val ext2 = ExtRules {parse_rules = parse_rules, print_rules = print_rules};
   455   in
   456     Syntax (ref (ExtGG (ggr1, ext2)), extend_tables tabs1 (mk_xgram ext2))
   457   end;
   458 
   459 
   460 fun extend syn read_ty (ex as (_, _, sext)) =
   461   (case sext of
   462     Sext {mixfix = [], ...} => new_extend
   463   | NewSext {mixfix = [], ...} => new_extend
   464   | _ => old_extend) syn read_ty ex;
   465 
   466 
   467 (* merge *)
   468 
   469 fun merge roots syn1 syn2 =
   470   let
   471     val Syntax (ggr1, Tabs {roots = roots1, ...}) = syn1;
   472     val Syntax (ggr2, Tabs {roots = roots2, ...}) = syn2;
   473     val mggr = ref (MergeGG (ggr1, ggr2));
   474   in
   475     (case ((distinct roots) \\ roots1) \\ roots2 of
   476       [] => mk_syntax mggr
   477     | new_roots => mk_syntax (ref (ExtGG (mggr, ExtRoots new_roots))))
   478   end;
   479 
   480 
   481 end;
   482