src/Pure/Syntax/syntax.ML
author wenzelm
Tue Nov 30 11:04:07 1993 +0100 (1993-11-30)
changeset 171 ab0f93a291b5
parent 168 1bf4e2cab673
child 174 319ff2d6760b
permissions -rw-r--r--
*** empty log message ***
     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 (*(* FIXME *)
   114 val empty_tables =
   115   Tabs {
   116     lexicon = empty_lexicon,
   117     roots = [],
   118     gram = empty_gram,
   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 
   129 (* extend_tables *)
   130 
   131 fun extend_tables (Tabs tabs) (XGram xgram) =
   132   let
   133     val {lexicon, roots = roots1, gram, consts = consts1, parse_ast_trtab,
   134       parse_ruletab, parse_trtab, print_trtab, print_ruletab, prtab} = tabs;
   135     val {roots = roots2, prods, consts = consts2, parse_ast_translation,
   136       parse_rules, parse_translation, print_translation, print_rules,
   137       print_ast_translation} = xgram;
   138   in
   139     (* FIXME *)
   140     if not (null prods) then
   141       error "extend_tables: called with non-empty prods"
   142     else
   143 
   144     Tabs {
   145       lexicon = extend_lexicon lexicon (literals_of prods),
   146       roots = roots2 union roots1,
   147       (* gram = extend_gram gram roots2 prods, *)  (* FIXME *)
   148       gram = gram,                                 (* FIXME *)
   149       consts = consts2 union consts1,
   150       parse_ast_trtab =
   151         extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
   152       parse_ruletab = extend_ruletab parse_ruletab parse_rules,
   153       parse_trtab = extend_trtab parse_trtab parse_translation "parse translation",
   154       print_trtab = extend_trtab print_trtab print_translation "print translation",
   155       print_ruletab = extend_ruletab print_ruletab print_rules,
   156       prtab = extend_prtab prtab prods print_ast_translation}
   157   end;
   158 
   159 
   160 (* mk_tables *)
   161 
   162 (* FIXME *)
   163 (* val mk_tables = extend_tables empty_tables; *)
   164 
   165 (* FIXME *)
   166 fun mk_tables (XGram xgram) =
   167   let
   168     val {roots, prods, consts, parse_ast_translation, parse_rules,
   169       parse_translation, print_translation, print_rules,
   170       print_ast_translation} = xgram;
   171   in
   172     Tabs {
   173       lexicon = mk_lexicon (literals_of prods),
   174       roots = roots,
   175       gram = mk_gram roots prods,
   176       consts = consts,
   177       parse_ast_trtab = mk_trtab parse_ast_translation "parse ast translation",
   178       parse_ruletab = mk_ruletab parse_rules,
   179       parse_trtab = mk_trtab parse_translation "parse translation",
   180       print_trtab = mk_trtab print_translation "print translation",
   181       print_ruletab = mk_ruletab print_rules,
   182       prtab = mk_prtab prods print_ast_translation}
   183   end;
   184 
   185 
   186 (* ggr_to_xgram *)
   187 
   188 fun ggr_to_xgram ggr =
   189   let
   190     fun flatGG ggr (xg, v) =
   191       if ggr mem v then (xg, v) else flatGG' ggr (xg, ggr :: v)
   192     and flatGG' (ref EmptyGG) xgv = xgv
   193       | flatGG' (ref (ExtGG (ggr, ext))) xgv =
   194           let
   195             val (xg', v') = flatGG ggr xgv;
   196           in
   197             (extend_xgram xg' ext, v')
   198           end
   199       | flatGG' (ref (MergeGG (ggr1, ggr2))) xgv =
   200           flatGG ggr1 (flatGG ggr2 xgv);
   201   in
   202     #1 (flatGG ggr (empty_xgram, []))
   203   end;
   204 
   205 
   206 (* mk_syntax *)
   207 
   208 fun mk_syntax ggr = Syntax (ggr, mk_tables (ggr_to_xgram ggr));
   209 
   210 
   211 
   212 (*** inspect syntax ***)
   213 
   214 fun xgram_of (Syntax (ggr, _)) = ggr_to_xgram ggr;
   215 
   216 fun string_of_big_list name prts =
   217   Pretty.string_of (Pretty.blk (2,
   218     separate Pretty.fbrk (Pretty.str name :: prts)));
   219 
   220 fun string_of_strings name strs =
   221   Pretty.string_of (Pretty.blk (2,
   222     separate (Pretty.brk 1)
   223       (map Pretty.str (name :: map quote (sort_strings strs)))));
   224 
   225 
   226 (* print_gram *)
   227 
   228 fun prt_gram (XGram {roots, prods, ...}) =
   229   let
   230     fun pretty_name name = [Pretty.str (name ^ " ="), Pretty.brk 1];
   231 
   232     fun pretty_xsymbs (Terminal s :: xs) =
   233           Pretty.str (quote s) :: Pretty.brk 1 :: pretty_xsymbs xs
   234       | pretty_xsymbs (Nonterminal (s, p) :: xs) =
   235           (if is_terminal s then Pretty.str s
   236           else Pretty.str (s ^ "[" ^ string_of_int p ^ "]"))
   237             :: Pretty.brk 1 :: pretty_xsymbs xs
   238       | pretty_xsymbs (_ :: xs) = pretty_xsymbs xs
   239       | pretty_xsymbs [] = [];
   240 
   241     fun pretty_const "" = [Pretty.brk 1]
   242       | pretty_const c = [Pretty.str (" => " ^ quote c), Pretty.brk 1];
   243 
   244     fun pretty_pri p = [Pretty.str ("(" ^ string_of_int p ^ ")")];
   245 
   246     fun pretty_prod (Prod (name, xsymbs, const, pri)) =
   247       Pretty.blk (2, pretty_name name @ pretty_xsymbs xsymbs @
   248         pretty_const const @ pretty_pri pri);
   249   in
   250     writeln (string_of_strings "lexicon:" (literals_of prods));
   251     writeln (Pretty.string_of (Pretty.blk (2,
   252       separate (Pretty.brk 1) (map Pretty.str ("roots:" :: roots)))));
   253     writeln (string_of_big_list "prods:" (map pretty_prod prods))
   254   end;
   255 
   256 val print_gram = prt_gram o xgram_of;
   257 
   258 
   259 (* print_trans *)
   260 
   261 fun prt_trans (XGram xgram) =
   262   let
   263     fun string_of_trs name trs = string_of_strings name (map fst trs);
   264 
   265     fun string_of_rules name rules =
   266       string_of_big_list name (map pretty_rule rules);
   267 
   268     val {consts, parse_ast_translation, parse_rules, parse_translation,
   269       print_translation, print_rules, print_ast_translation, ...} = xgram;
   270   in
   271     writeln (string_of_strings "consts:" consts);
   272     writeln (string_of_trs "parse_ast_translation:" parse_ast_translation);
   273     writeln (string_of_rules "parse_rules:" parse_rules);
   274     writeln (string_of_trs "parse_translation:" parse_translation);
   275     writeln (string_of_trs "print_translation:" print_translation);
   276     writeln (string_of_rules "print_rules:" print_rules);
   277     writeln (string_of_trs "print_ast_translation:" print_ast_translation)
   278   end;
   279 
   280 val print_trans = prt_trans o xgram_of;
   281 
   282 
   283 (* print_syntax *)
   284 
   285 fun print_syntax syn =
   286   let
   287     val xgram = xgram_of syn;
   288   in
   289     prt_gram xgram; prt_trans xgram
   290   end;
   291 
   292 
   293 
   294 (*** parsing and printing ***)
   295 
   296 (* mk_get_rules *)
   297 
   298 fun mk_get_rules ruletab =
   299   let
   300     fun get_rules a =
   301       (case lookup ruletab a of
   302         Some rules => rules
   303       | None => []);
   304   in
   305     if Symtab.is_null ruletab then None else Some get_rules
   306   end;
   307 
   308 
   309 (* read_ast *)
   310 
   311 fun read_ast (Syntax (_, tabs)) xids root str =
   312   let
   313     val Tabs {lexicon, gram, parse_ast_trtab, ...} = tabs;
   314   in
   315     pt_to_ast (lookup parse_ast_trtab)
   316       (parse gram root (tokenize lexicon xids str))
   317   end;
   318 
   319 
   320 
   321 (** test_read **)
   322 
   323 fun test_read (Syntax (_, tabs)) root str =
   324   let
   325     val Tabs {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs;
   326 
   327     val toks = tokenize lexicon false str;
   328     val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks));
   329 
   330     val pt = parse gram root toks;
   331     val raw_ast = pt_to_ast (K None) pt;
   332     val _ = writeln ("raw: " ^ str_of_ast raw_ast);
   333 
   334     val pre_ast = pt_to_ast (lookup parse_ast_trtab) pt;
   335     val _ = normalize true true (mk_get_rules parse_ruletab) pre_ast;
   336   in () end;
   337 
   338 
   339 
   340 (** read **)
   341 
   342 fun read (syn as Syntax (_, tabs)) ty str =
   343   let
   344     val Tabs {parse_ruletab, parse_trtab, ...} = tabs;
   345     val ast = read_ast syn false (typ_to_nonterm ty) str;
   346   in
   347     ast_to_term (lookup parse_trtab)
   348       (normalize_ast (mk_get_rules parse_ruletab) ast)
   349   end;
   350 
   351 
   352 
   353 (** read_typ **)
   354 
   355 fun read_typ syn def_sort str = typ_of_term def_sort (read syn typeT str);
   356 
   357 
   358 
   359 (** read_rule **)
   360 
   361 fun read_rule syn (xrule as ((_, lhs_src), (_, rhs_src))) =
   362   let
   363     val Syntax (_, Tabs {consts, ...}) = syn;
   364 
   365     fun constantify (ast as Constant _) = ast
   366       | constantify (ast as Variable x) =
   367           if x mem consts then Constant x else ast
   368       | constantify (Appl asts) = Appl (map constantify asts);
   369 
   370     fun read_pat (root, str) =
   371       constantify (read_ast syn true root str)
   372         handle ERROR => error ("The error above occurred in " ^ quote str);
   373 
   374     val rule as (lhs, rhs) = (pairself read_pat) xrule;
   375   in
   376     (case rule_error rule of
   377       Some msg =>
   378         error ("Error in syntax translation rule: " ^ msg ^
   379           "\nexternal: " ^ quote lhs_src ^ "  ->  " ^ quote rhs_src ^
   380           "\ninternal: " ^ str_of_ast lhs ^ "  ->  " ^ str_of_ast rhs)
   381     | None => rule)
   382   end;
   383 
   384 
   385 
   386 (** read_xrules **)
   387 
   388 fun read_xrules syn xrules =
   389   let
   390     fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2)
   391       | right_rule (xpat1 <-| xpat2) = None
   392       | right_rule (xpat1 <-> xpat2) = Some (xpat1, xpat2);
   393 
   394     fun left_rule (xpat1 |-> xpat2) = None
   395       | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1)
   396       | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1);
   397   in
   398     (map (read_rule syn) (mapfilter right_rule xrules),
   399      map (read_rule syn) (mapfilter left_rule xrules))
   400   end;
   401 
   402 
   403 
   404 (** pretty terms or typs **)
   405 
   406 fun pretty_t t_to_ast pretty_t (syn as Syntax (_, tabs)) t =
   407   let
   408     val Tabs {print_trtab, print_ruletab, prtab, ...} = tabs;
   409     val ast = t_to_ast (lookup print_trtab) t;
   410   in
   411     pretty_t prtab (normalize_ast (mk_get_rules print_ruletab) ast)
   412   end;
   413 
   414 val pretty_term = pretty_t term_to_ast pretty_term_ast;
   415 
   416 val pretty_typ = pretty_t typ_to_ast pretty_typ_ast;
   417 
   418 fun string_of_term syn t = Pretty.string_of (pretty_term syn t);
   419 
   420 fun string_of_typ syn ty = Pretty.string_of (pretty_typ syn ty);
   421 
   422 
   423 
   424 (*** build syntax ***)
   425 
   426 (* type_syn *)
   427 
   428 val type_syn = mk_syntax (ref (ExtGG (ref EmptyGG, type_ext)));
   429 
   430 
   431 (* extend *)  (* FIXME *)
   432 
   433 fun old_extend syn read_ty (roots, xconsts, sext) =
   434   let
   435     val Syntax (ggr0, Tabs {roots = roots0, ...}) = syn;
   436 
   437     val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext;
   438     val (syn1 as Syntax (ggr1, tabs1)) = mk_syntax (ref (ExtGG (ggr0, ext1)));
   439 
   440     val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext);
   441     val ext2 = ExtRules {parse_rules = parse_rules, print_rules = print_rules};
   442   in
   443     Syntax (ref (ExtGG (ggr1, ext2)), extend_tables tabs1 (mk_xgram ext2))
   444   end;
   445 
   446 
   447 fun new_extend syn read_ty (roots, xconsts, sext) =
   448   let
   449     val Syntax (ggr0, tabs0 as Tabs {roots = roots0, ...}) = syn;
   450 
   451     val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext;
   452     val (syn1 as Syntax (ggr1, tabs1)) =
   453       Syntax (ref (ExtGG (ggr0, ext1)), extend_tables tabs0 (mk_xgram ext1));
   454 
   455     val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext);
   456     val ext2 = ExtRules {parse_rules = parse_rules, print_rules = print_rules};
   457   in
   458     Syntax (ref (ExtGG (ggr1, ext2)), extend_tables tabs1 (mk_xgram ext2))
   459   end;
   460 
   461 
   462 fun extend syn read_ty (ex as (roots, _, sext)) =
   463   (case (roots, sext) of
   464     ([], Sext {mixfix = [], ...}) => new_extend
   465   | ([], NewSext {mixfix = [], ...}) => new_extend
   466   | _ => old_extend) syn read_ty ex;
   467 
   468 
   469 (* merge *)
   470 
   471 fun merge roots syn1 syn2 =
   472   let
   473     val Syntax (ggr1, Tabs {roots = roots1, ...}) = syn1;
   474     val Syntax (ggr2, Tabs {roots = roots2, ...}) = syn2;
   475     val mggr = ref (MergeGG (ggr1, ggr2));
   476   in
   477     (case ((distinct roots) \\ roots1) \\ roots2 of
   478       [] => mk_syntax mggr
   479     | new_roots => mk_syntax (ref (ExtGG (mggr, ExtRoots new_roots))))
   480   end;
   481 
   482 
   483 end;
   484