src/Pure/Syntax/syntax.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 18 c9ec452ff08f
permissions -rw-r--r--
Initial revision
     1 (*  Title:      Pure/Syntax/syntax
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 signature SYNTAX =
     7 sig
     8   (* FIXME include AST0 (?) *)
     9   include LEXICON0
    10   include EXTENSION0
    11   include TYPE_EXT0
    12   include SEXTENSION1
    13   include PRINTER0
    14   structure Extension: EXTENSION
    15   structure Pretty: PRETTY
    16   local open Extension.XGram Extension.XGram.Ast in
    17     type syntax
    18     val print_gram: syntax -> unit
    19     val print_trans: syntax -> unit
    20     val print_syntax: syntax -> unit
    21     val read_ast: syntax -> string * string -> ast
    22     val read: syntax -> typ -> string -> term
    23     val pretty_term: syntax -> term -> Pretty.T
    24     val pretty_typ: syntax -> typ -> Pretty.T
    25     val string_of_term: syntax -> term -> string
    26     val string_of_typ: syntax -> typ -> string
    27     val type_syn: syntax
    28     val extend: syntax * (indexname -> sort) -> string list * string list * sext
    29       -> syntax
    30     val merge: syntax * syntax -> syntax
    31   end
    32 end;
    33 
    34 functor SyntaxFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT
    35   and Parser: PARSER and SExtension: SEXTENSION and Printer: PRINTER
    36   sharing TypeExt.Extension.XGram = Parser.XGram = Printer.XGram
    37   and TypeExt.Extension = SExtension.Extension
    38   and Parser.ParseTree.Ast = Parser.XGram.Ast)(*: SYNTAX *) = (* FIXME *)
    39 struct
    40 
    41 structure Extension = TypeExt.Extension;
    42 structure XGram = Extension.XGram;
    43 structure Lexicon = Parser.ParseTree.Lexicon;
    44 open Lexicon Extension TypeExt SExtension Printer XGram XGram.Ast;
    45 
    46 
    47 fun lookup tab a = Symtab.lookup (tab, a);
    48 
    49 
    50 
    51 (** datatype syntax **)
    52 
    53 datatype tables =
    54   Tab of {
    55     gram: Parser.Gram,
    56     lexicon: Lexicon,
    57     const_tab: unit Symtab.table,
    58     parse_ast_trtab: (ast list -> ast) Symtab.table,
    59     parse_preproc: ast -> ast,
    60     parse_ruletab: (ast * ast) list Symtab.table,
    61     parse_postproc: ast -> ast,
    62     parse_trtab: (term list -> term) Symtab.table,
    63     print_trtab: (term list -> term) Symtab.table,
    64     print_preproc: ast -> ast,
    65     print_ruletab: (ast * ast) list Symtab.table,
    66     print_postproc: ast -> ast,
    67     print_tab: Printer.tab};
    68 
    69 datatype gramgraph =
    70   EmptyGG |
    71   ExtGG of gramgraph ref * (ext * synrules) |
    72   MergeGG of gramgraph ref * gramgraph ref;
    73 
    74 datatype syntax = Syntax of gramgraph ref * tables;
    75 
    76 
    77 
    78 (*** compile syntax ***)
    79 
    80 (* ggr_to_xgram *)
    81 
    82 fun ggr_to_xgram ggr =
    83   let
    84     fun flatGG ggr (xg, v) =
    85       if ggr mem v then (xg, v) else flatGG' ggr (xg, ggr :: v)
    86     and flatGG' (ref EmptyGG) xgv = xgv
    87       | flatGG' (ref (ExtGG (ggr, ext))) xgv =
    88           let
    89             val (xg', v') = flatGG ggr xgv
    90           in
    91             (Extension.extend xg' ext, v')
    92           end
    93       | flatGG' (ref (MergeGG (ggr1, ggr2))) xgv =
    94           flatGG ggr1 (flatGG ggr2 xgv);
    95   in
    96     fst (flatGG ggr (Extension.empty, []))
    97   end;
    98 
    99 
   100 (* mk_ruletab *)
   101 
   102 fun mk_ruletab rules =
   103   let
   104     fun add_rule (r, tab) =
   105       let
   106         val a = head_of_rule r
   107       in
   108         case lookup tab a of
   109           None => Symtab.update ((a, [r]), tab)
   110         | Some rs => Symtab.update ((a, r :: rs), tab)
   111       end;
   112   in
   113     Symtab.balance (foldr add_rule (rules, Symtab.null))
   114   end;
   115 
   116 
   117 (* make_syntax *)
   118 
   119 fun make_syntax ggr =
   120   let
   121     fun mk_const_tab cs =
   122       Symtab.balance
   123         (Symtab.st_of_alist ((map (fn c => (c, ())) cs), Symtab.null));
   124 
   125     fun mk_trtab alst name =
   126       Symtab.balance (Symtab.st_of_alist (alst, Symtab.null))
   127         handle Symtab.DUPLICATE s => error ("More than one " ^ name ^ " for " ^ quote s);
   128 
   129     fun mk_proc (Some f) = f
   130       | mk_proc None = I;
   131 
   132     fun all_strings (opl: string prod list): string list =
   133         flat (map (fn Prod (_, syn, _, _) => terminals syn) opl);
   134 
   135     fun str_to_tok (opl: string prod list, lex: Lexicon): Token prod list =
   136       map
   137         (fn Prod (t, syn, s, pa) =>
   138           Prod (t, translate (hd o tokenize lex) syn, s, pa))
   139         opl;
   140 
   141     fun xgram_to_tables (XGram xgram) =
   142       let
   143         val {roots, prods, consts, parse_ast_translation, parse_preproc, parse_rules,
   144           parse_postproc, parse_translation, print_translation, print_preproc,
   145           print_rules, print_postproc, print_ast_translation} = xgram;
   146         val lexicon = mk_lexicon (all_strings prods);
   147       in
   148         Tab {
   149           gram = Parser.compile_xgram (roots, str_to_tok (prods, lexicon)),
   150           lexicon = lexicon,
   151           const_tab = mk_const_tab consts,
   152           parse_ast_trtab = mk_trtab parse_ast_translation "parse ast translation",
   153           parse_preproc = mk_proc parse_preproc,
   154           parse_ruletab = mk_ruletab parse_rules,
   155           parse_postproc = mk_proc parse_postproc,
   156           parse_trtab = mk_trtab parse_translation "parse translation",
   157           print_trtab = mk_trtab print_translation "print translation",
   158           print_preproc = mk_proc print_preproc,
   159           print_ruletab = mk_ruletab print_rules,
   160           print_postproc = mk_proc print_postproc,
   161           print_tab = mk_print_tab prods
   162             (mk_trtab print_ast_translation "print ast translation")}
   163       end;
   164   in
   165     Syntax (ggr, xgram_to_tables (ggr_to_xgram ggr))
   166   end;
   167 
   168 
   169 (* add_synrules *)
   170 
   171 fun add_synrules (Tab tabs) (SynRules rules) =
   172   let
   173     val {gram, lexicon, const_tab, parse_ast_trtab, parse_preproc, parse_ruletab,
   174       parse_postproc, parse_trtab, print_trtab, print_preproc, print_ruletab,
   175       print_postproc, print_tab} = tabs;
   176     val {parse_rules, print_rules} = rules;
   177     val parse_rs = flat (map snd (Symtab.alist_of parse_ruletab)) @ parse_rules;
   178     val print_rs = flat (map snd (Symtab.alist_of print_ruletab)) @ print_rules;
   179   in
   180     Tab {
   181       gram = gram, lexicon = lexicon, const_tab = const_tab,
   182       parse_ast_trtab = parse_ast_trtab,
   183       parse_preproc = parse_preproc,
   184       parse_ruletab = mk_ruletab parse_rs,
   185       parse_postproc = parse_postproc,
   186       parse_trtab = parse_trtab,
   187       print_trtab = print_trtab,
   188       print_preproc = print_preproc,
   189       print_ruletab = mk_ruletab print_rs,
   190       print_postproc = print_postproc,
   191       print_tab = print_tab}
   192   end;
   193 
   194 
   195 
   196 (*** inspect syntax ***)
   197 
   198 (* print_syntax_old *) (* FIXME remove *)
   199 
   200 fun print_syntax_old (Syntax (_, Tab {gram, lexicon, ...})) =
   201   Parser.print_gram (gram, lexicon);
   202 
   203 
   204 
   205 fun xgram_of (Syntax (ggr, _)) = ggr_to_xgram ggr;
   206 
   207 fun string_of_big_list name prts =
   208   Pretty.string_of (Pretty.blk (2,
   209     separate Pretty.fbrk (Pretty.str name :: prts)));
   210 
   211 
   212 (* print_gram *)    (* FIXME check *)
   213 
   214 fun prt_gram (XGram {roots, prods, ...}) =
   215   let
   216     fun pretty_name name = [Pretty.str (name ^ " ="), Pretty.brk 1];
   217 
   218     fun pretty_xsymbs (Terminal s :: xs) =
   219           Pretty.str (quote s) :: Pretty.brk 1 :: pretty_xsymbs xs
   220       | pretty_xsymbs (Nonterminal (s, p) :: xs) =
   221           (if is_terminal s then Pretty.str s
   222           else Pretty.str (s ^ "[" ^ string_of_int p ^ "]"))
   223             :: Pretty.brk 1 :: pretty_xsymbs xs
   224       | pretty_xsymbs (_ :: xs) = pretty_xsymbs xs
   225       | pretty_xsymbs [] = [];
   226 
   227     fun pretty_const "" = [Pretty.brk 1]
   228       | pretty_const c = [Pretty.str (" => " ^ quote c), Pretty.brk 1];
   229 
   230     fun pretty_pri p = [Pretty.str ("(" ^ string_of_int p ^ ")")];
   231 
   232     fun pretty_prod (Prod (name, xsymbs, const, pri)) =
   233       Pretty.blk (2, pretty_name name @ pretty_xsymbs xsymbs @
   234         pretty_const const @ pretty_pri pri);
   235   in
   236     writeln (Pretty.string_of (Pretty.blk (2,
   237       separate (Pretty.brk 1) (map Pretty.str ("roots:" :: roots)))));
   238     writeln (string_of_big_list "prods:" (map pretty_prod prods))
   239   end;
   240 
   241 
   242 val print_gram = prt_gram o xgram_of;
   243 
   244 
   245 (* print_trans *)   (* FIXME check *)
   246 
   247 fun prt_trans (XGram xgram) =
   248   let
   249     fun string_of_strings name strs =
   250       Pretty.string_of (Pretty.blk (2,
   251         separate (Pretty.brk 1) (map Pretty.str (name :: map quote strs))));
   252 
   253     fun string_of_trs name trs = string_of_strings name (map fst trs);
   254 
   255     fun string_of_proc name proc =
   256       Pretty.string_of (Pretty.blk (2, [Pretty.str name, Pretty.brk 1,
   257         Pretty.str (if is_none proc then "None" else "Some fn")]));
   258 
   259     fun string_of_rules name rules =
   260       string_of_big_list name (map pretty_rule rules);
   261 
   262 
   263     val {consts, parse_ast_translation, parse_preproc, parse_rules,
   264       parse_postproc, parse_translation, print_translation, print_preproc,
   265       print_rules, print_postproc, print_ast_translation, ...} = xgram;
   266   in
   267     writeln (string_of_strings "consts:" consts);
   268     writeln (string_of_trs "parse_ast_translation:" parse_ast_translation);
   269     writeln (string_of_proc "parse_preproc:" parse_preproc);
   270     writeln (string_of_rules "parse_rules:" parse_rules);
   271     writeln (string_of_proc "parse_postproc:" parse_postproc);
   272     writeln (string_of_trs "parse_translation:" parse_translation);
   273     writeln (string_of_trs "print_translation:" print_translation);
   274     writeln (string_of_proc "print_preproc:" print_preproc);
   275     writeln (string_of_rules "print_rules:" print_rules);
   276     writeln (string_of_proc "print_postproc:" print_postproc);
   277     writeln (string_of_trs "print_ast_translation:" print_ast_translation)
   278   end;
   279 
   280 
   281 val print_trans = prt_trans o xgram_of;
   282 
   283 
   284 (* print_syntax *)
   285 
   286 fun print_syntax syn =
   287   let
   288     val xgram = xgram_of syn;
   289   in
   290     prt_gram xgram; prt_trans xgram
   291   end;
   292 
   293 
   294 
   295 (*** parsing and printing ***)
   296 
   297 (* read_ast *)
   298 
   299 fun read_ast syn (root, s) =
   300   let
   301     val Syntax (_, Tab {gram, lexicon, parse_ast_trtab, ...}) = syn;
   302     val root = if Parser.parsable (gram, root) then root else error ("Unparsable root " ^ root) (* Extension.logic *);    (* FIXME *)
   303     fun syn_err toks =
   304       error ("Syntax error at\n" ^ space_implode " " (map token_to_string toks));
   305   in
   306     Parser.ParseTree.pt_to_ast (lookup parse_ast_trtab)
   307       (Parser.parse (gram, root, tokenize lexicon s))
   308         handle Parser.SYNTAX_ERR toks => syn_err toks
   309   end;
   310 
   311 
   312 (* norm_ast *)
   313 
   314 fun norm_ast ruletab ast =
   315   let
   316     fun get_rules a =
   317       (case lookup ruletab a of
   318         Some rules => rules
   319       | None => []);
   320   in
   321     normalize (if Symtab.is_null ruletab then None else Some get_rules) ast
   322   end;
   323 
   324 
   325 
   326 (** read **)
   327 
   328 fun read (syn as Syntax (_, Tab tabs)) ty s =
   329   let
   330     val {parse_preproc, parse_ruletab, parse_postproc, parse_trtab, ...} = tabs;
   331     val ast = read_ast syn (typ_to_nt ty, s);
   332   in
   333     ast_to_term (lookup parse_trtab)
   334       (parse_postproc (norm_ast parse_ruletab (parse_preproc ast)))
   335   end;
   336 
   337 
   338 
   339 (** pprint_ast **)
   340 
   341 val pprint_ast = Pretty.pprint o pretty_ast;
   342 
   343 
   344 
   345 (** pretty term, typ **)
   346 
   347 fun pretty_t t_to_ast pretty_t (syn as Syntax (_, Tab tabs)) t =
   348   let
   349     val {print_trtab, print_preproc, print_ruletab, print_postproc, print_tab, ...} = tabs;
   350     val ast = t_to_ast (lookup print_trtab) t;
   351   in
   352     pretty_t print_tab
   353       (print_postproc (norm_ast print_ruletab (print_preproc ast)))
   354   end;
   355 
   356 val pretty_term = pretty_t term_to_ast pretty_term_ast;
   357 
   358 val pretty_typ = pretty_t typ_to_ast pretty_typ_ast;
   359 
   360 fun string_of_term syn t = Pretty.string_of (pretty_term syn t);
   361 
   362 fun string_of_typ syn ty = Pretty.string_of (pretty_typ syn ty);
   363 
   364 
   365 
   366 (*** build syntax ***)
   367 
   368 (* type_syn *)
   369 
   370 val type_syn = make_syntax (ref (ExtGG (ref EmptyGG, (type_ext, empty_synrules))));
   371 
   372 
   373 (* extend *)  (* FIXME check *)
   374 
   375 fun extend (old_syn as Syntax (ggr, _), def_sort) (roots, xconsts, sext) =
   376   let
   377     fun read_typ s = typ_of_term def_sort (read old_syn typeT s);
   378     val ext = ext_of_sext roots xconsts read_typ sext;
   379 
   380     fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2)
   381       | right_rule (xpat1 <-| xpat2) = None
   382       | right_rule (xpat1 <-> xpat2) = Some (xpat1, xpat2);
   383 
   384     fun left_rule (xpat1 |-> xpat2) = None
   385       | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1)
   386       | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1);
   387 
   388     val (tmp_syn as Syntax (_, tmp_tabs)) =
   389       make_syntax (ref (ExtGG (ggr, (ext, empty_synrules))));
   390     val Syntax (_, Tab {const_tab, ...}) = tmp_syn;
   391 
   392     fun constantify (ast as (Constant _)) = ast
   393       | constantify (ast as (Variable x)) =
   394           if is_some (lookup const_tab x) then Constant x else ast
   395       | constantify (Appl asts) = Appl (map constantify asts);
   396 
   397     fun read_pat (r_s as (root, s)) =
   398       constantify ((read_ast tmp_syn r_s)
   399         handle ERROR => error ("The error above occurred in " ^ quote s));
   400 
   401     fun read_rule (xrule as ((_, lhs_src), (_, rhs_src))) =
   402       let
   403         val rule as (lhs, rhs) = (pairself read_pat) xrule;
   404       in
   405         case rule_error rule of
   406           Some msg =>
   407             error ("Error in syntax translation rule: " ^ msg ^
   408               "\nexternal: " ^ quote lhs_src ^ "  ->  " ^ quote rhs_src ^
   409               "\ninternal: " ^ str_of_ast lhs ^ "  ->  " ^ str_of_ast rhs)
   410         | None => rule
   411       end;
   412 
   413     val xrules = xrules_of sext;
   414     val new_rules =
   415       SynRules {
   416         parse_rules = map read_rule (mapfilter right_rule xrules),
   417         print_rules = map read_rule (mapfilter left_rule xrules)};
   418   in
   419     Syntax (ref (ExtGG (ggr, (ext, new_rules))), add_synrules tmp_tabs new_rules)
   420   end;
   421 
   422 
   423 (* merge *)
   424 
   425 fun merge (Syntax (ggr1, _), Syntax (ggr2, _)) =
   426   make_syntax (ref (MergeGG (ggr1, ggr2)));
   427 
   428 
   429 end;
   430