src/Pure/Syntax/syn_ext.ML
author wenzelm
Fri Feb 28 16:40:08 1997 +0100 (1997-02-28)
changeset 2694 b98365c6e869
parent 2382 e7c2bce815ba
child 2913 ce271fa4d8e2
permissions -rw-r--r--
added token_translation interface;
     1 (*  Title:      Pure/Syntax/syn_ext.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel and Carsten Clasohm, TU Muenchen
     4 
     5 Syntax extension (internal interface).
     6 *)
     7 
     8 signature SYN_EXT0 =
     9   sig
    10   val typeT: typ
    11   val constrainC: string
    12   end;
    13 
    14 signature SYN_EXT =
    15   sig
    16   include SYN_EXT0
    17   val logic: string
    18   val args: string
    19   val cargs: string
    20   val any: string
    21   val sprop: string
    22   val typ_to_nonterm: typ -> string
    23   datatype xsymb =
    24     Delim of string |
    25     Argument of string * int |
    26     Space of string |
    27     Bg of int | Brk of int | En
    28   datatype xprod = XProd of string * xsymb list * string * int
    29   val max_pri: int
    30   val chain_pri: int
    31   val delims_of: xprod list -> string list
    32   datatype mfix = Mfix of string * typ * string * int list * int
    33   datatype syn_ext =
    34     SynExt of {
    35       logtypes: string list,
    36       xprods: xprod list,
    37       consts: string list,
    38       parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    39       parse_rules: (Ast.ast * Ast.ast) list,
    40       parse_translation: (string * (term list -> term)) list,
    41       print_translation: (string * (typ -> term list -> term)) list,
    42       print_rules: (Ast.ast * Ast.ast) list,
    43       print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    44       token_translation: (string * string * (string -> string * int)) list}
    45   val mk_syn_ext: bool -> string list -> mfix list ->
    46     string list -> (string * (Ast.ast list -> Ast.ast)) list *
    47     (string * (term list -> term)) list *
    48     (string * (typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    49     -> (string * string * (string -> string * int)) list
    50     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    51   val syn_ext: string list -> mfix list -> string list ->
    52     (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
    53     (string * (typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    54     -> (string * string * (string -> string * int)) list
    55     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    56   val syn_ext_logtypes: string list -> syn_ext
    57   val syn_ext_const_names: string list -> string list -> syn_ext
    58   val syn_ext_rules: string list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    59   val fix_tr': (term list -> term) -> typ -> term list -> term
    60   val syn_ext_trfuns: string list ->
    61     (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
    62     (string * (term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    63     -> syn_ext
    64   val syn_ext_trfunsT: string list -> (string * (typ -> term list -> term)) list -> syn_ext
    65   val syn_ext_tokentrfuns: string list
    66     -> (string * string * (string -> string * int)) list -> syn_ext
    67   val pure_ext: syn_ext
    68   end;
    69 
    70 structure SynExt : SYN_EXT =
    71 struct
    72 
    73 open Lexicon Ast;
    74 
    75 
    76 (** misc definitions **)
    77 
    78 (* syntactic categories *)
    79 
    80 val logic = "logic";
    81 val logicT = Type (logic, []);
    82 
    83 val args = "args";
    84 val cargs = "cargs";
    85 
    86 val typeT = Type ("type", []);
    87 
    88 val sprop = "#prop";
    89 val spropT = Type (sprop, []);
    90 
    91 val any = "any";
    92 val anyT = Type (any, []);
    93 
    94 
    95 (* constants *)
    96 
    97 val constrainC = "_constrain";
    98 
    99 
   100 
   101 (** datatype xprod **)
   102 
   103 (*Delim s: delimiter s
   104   Argument (s, p): nonterminal s requiring priority >= p, or valued token
   105   Space s: some white space for printing
   106   Bg, Brk, En: blocks and breaks for pretty printing*)
   107 
   108 datatype xsymb =
   109   Delim of string |
   110   Argument of string * int |
   111   Space of string |
   112   Bg of int | Brk of int | En;
   113 
   114 
   115 (*XProd (lhs, syms, c, p):
   116     lhs: name of nonterminal on the lhs of the production
   117     syms: list of symbols on the rhs of the production
   118     c: head of parse tree
   119     p: priority of this production*)
   120 
   121 datatype xprod = XProd of string * xsymb list * string * int;
   122 
   123 val max_pri = 1000;   (*maximum legal priority*)
   124 val chain_pri = ~1;   (*dummy for chain productions*)
   125 
   126 
   127 (* delims_of *)
   128 
   129 fun delims_of xprods =
   130   let
   131     fun del_of (Delim s) = Some s
   132       | del_of _ = None;
   133 
   134     fun dels_of (XProd (_, xsymbs, _, _)) =
   135       mapfilter del_of xsymbs;
   136   in
   137     distinct (flat (map dels_of xprods))
   138   end;
   139 
   140 
   141 
   142 (** datatype mfix **)
   143 
   144 (*Mfix (sy, ty, c, ps, p):
   145     sy: rhs of production as symbolic string
   146     ty: type description of production
   147     c: head of parse tree
   148     ps: priorities of arguments in sy
   149     p: priority of production*)
   150 
   151 datatype mfix = Mfix of string * typ * string * int list * int;
   152 
   153 
   154 (* typ_to_nonterm *)
   155 
   156 fun typ_to_nt _ (Type (c, _)) = c
   157   | typ_to_nt default _ = default;
   158 
   159 (*get nonterminal for rhs*)
   160 val typ_to_nonterm = typ_to_nt any;
   161 
   162 (*get nonterminal for lhs*)
   163 val typ_to_nonterm1 = typ_to_nt logic;
   164 
   165 
   166 (* mfix_to_xprod *)
   167 
   168 fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) =
   169   let
   170     fun err msg =
   171       (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
   172         error msg);
   173     fun post_err () = error ("The error(s) above occurred in mixfix annotation " ^
   174       quote sy ^ " for " ^ quote const);
   175 
   176     fun check_pri p =
   177       if p >= 0 andalso p <= max_pri then ()
   178       else err ("precedence out of range: " ^ string_of_int p);
   179 
   180     fun blocks_ok [] 0 = true
   181       | blocks_ok [] _ = false
   182       | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
   183       | blocks_ok (En :: _) 0 = false
   184       | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
   185       | blocks_ok (_ :: syms) n = blocks_ok syms n;
   186 
   187     fun check_blocks syms =
   188       if blocks_ok syms 0 then ()
   189       else err "unbalanced block parentheses";
   190 
   191 
   192     local
   193       fun is_meta c = c mem ["(", ")", "/", "_"];
   194 
   195       fun scan_delim_char ("'" :: c :: cs) =
   196             if is_blank c then raise LEXICAL_ERROR else (c, cs)
   197         | scan_delim_char ["'"] = err "trailing escape character"
   198         | scan_delim_char (chs as c :: cs) =
   199             if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)
   200         | scan_delim_char [] = raise LEXICAL_ERROR;
   201 
   202       val scan_sym =
   203         $$ "_" >> K (Argument ("", 0)) ||
   204         $$ "(" -- scan_int >> (Bg o #2) ||
   205         $$ ")" >> K En ||
   206         $$ "/" -- $$ "/" >> K (Brk ~1) ||
   207         $$ "/" -- scan_any is_blank >> (Brk o length o #2) ||
   208         scan_any1 is_blank >> (Space o implode) ||
   209         repeat1 scan_delim_char >> (Delim o implode);
   210 
   211       val scan_symb =
   212         scan_sym >> Some ||
   213         $$ "'" -- scan_one is_blank >> K None;
   214     in
   215       val scan_symbs = mapfilter I o #1 o repeat scan_symb;
   216     end;
   217 
   218 
   219     val cons_fst = apfst o cons;
   220 
   221     fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
   222       | add_args [] _ _ = err "too many precedences"
   223       | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
   224           cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys [])
   225       | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
   226           cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps)
   227       | add_args (Argument _ :: _) _ _ =
   228           err "more arguments than in corresponding type"
   229       | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
   230 
   231 
   232     fun is_arg (Argument _) = true
   233       | is_arg _ = false;
   234 
   235     fun is_term (Delim _) = true
   236       | is_term (Argument (s, _)) = is_terminal s
   237       | is_term _ = false;
   238 
   239     fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
   240       | rem_pri sym = sym;
   241 
   242     fun is_delim (Delim _) = true
   243       | is_delim _ = false;
   244 
   245     (*replace logical types on rhs by "logic"*)
   246     fun unify_logtypes copy_prod (a as (Argument (s, p))) =
   247           if s mem logtypes then Argument (logic, p)
   248           else a
   249       | unify_logtypes _ a = a;
   250 
   251 
   252     val sy_chars =
   253       SymbolFont.read_charnames (explode sy) handle ERROR => post_err ();
   254     val raw_symbs = scan_symbs sy_chars;
   255     val (symbs, lhs) = add_args raw_symbs typ pris;
   256     val copy_prod =
   257       lhs mem ["prop", "logic"]
   258         andalso const <> ""
   259         andalso not (null symbs)
   260         andalso not (exists is_delim symbs);
   261     val lhs' =
   262       if convert andalso not copy_prod then
   263        (if lhs mem logtypes then logic
   264         else if lhs = "prop" then sprop else lhs)
   265       else lhs;
   266     val symbs' = map (unify_logtypes copy_prod) symbs;
   267     val xprod = XProd (lhs', symbs', const, pri);
   268   in
   269     seq check_pri pris;
   270     check_pri pri;
   271     check_blocks symbs';
   272 
   273     if is_terminal lhs' then err ("illegal lhs: " ^ lhs')
   274     else if const <> "" then xprod
   275     else if length (filter is_arg symbs') <> 1 then
   276       err "copy production must have exactly one argument"
   277     else if exists is_term symbs' then xprod
   278     else XProd (lhs', map rem_pri symbs', "", chain_pri)
   279   end;
   280 
   281 
   282 (** datatype syn_ext **)
   283 
   284 datatype syn_ext =
   285   SynExt of {
   286     logtypes: string list,
   287     xprods: xprod list,
   288     consts: string list,
   289     parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
   290     parse_rules: (Ast.ast * Ast.ast) list,
   291     parse_translation: (string * (term list -> term)) list,
   292     print_translation: (string * (typ -> term list -> term)) list,
   293     print_rules: (Ast.ast * Ast.ast) list,
   294     print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
   295     token_translation: (string * string * (string -> string * int)) list};
   296 
   297 
   298 (* syn_ext *)
   299 
   300 fun mk_syn_ext convert logtypes mfixes consts trfuns tokentrfuns rules =
   301   let
   302     val (parse_ast_translation, parse_translation, print_translation,
   303       print_ast_translation) = trfuns;
   304     val (parse_rules, print_rules) = rules;
   305     val logtypes' = logtypes \ "prop";
   306 
   307     val mfix_consts = distinct (map (fn (Mfix (_, _, c, _, _)) => c) mfixes);
   308     val xprods = map (mfix_to_xprod convert logtypes') mfixes;
   309   in
   310     SynExt {
   311       logtypes = logtypes',
   312       xprods = xprods,
   313       consts = filter is_xid (consts union mfix_consts),
   314       parse_ast_translation = parse_ast_translation,
   315       parse_rules = parse_rules,
   316       parse_translation = parse_translation,
   317       print_translation = print_translation,
   318       print_rules = print_rules,
   319       print_ast_translation = print_ast_translation,
   320       token_translation = tokentrfuns}
   321   end;
   322 
   323 
   324 val syn_ext = mk_syn_ext true;
   325 
   326 fun syn_ext_logtypes logtypes =
   327   syn_ext logtypes [] [] ([], [], [], []) [] ([], []);
   328 
   329 fun syn_ext_const_names logtypes cs =
   330   syn_ext logtypes [] cs ([], [], [], []) [] ([], []);
   331 
   332 fun syn_ext_rules logtypes rules =
   333   syn_ext logtypes [] [] ([], [], [], []) [] rules;
   334 
   335 fun fix_tr' f _ args = f args;
   336 
   337 fun syn_ext_trfuns logtypes (atrs, trs, tr's, atr's) =
   338   syn_ext logtypes [] [] (atrs, trs, map (apsnd fix_tr') tr's, atr's) [] ([], []);
   339 
   340 fun syn_ext_trfunsT logtypes tr's =
   341   syn_ext logtypes [] [] ([], [], tr's, []) [] ([], []);
   342 
   343 fun syn_ext_tokentrfuns logtypes tokentrfuns =
   344   syn_ext logtypes [] [] ([], [], [], []) tokentrfuns ([], []);
   345 
   346 
   347 (* pure_ext *)
   348 
   349 val pure_ext = mk_syn_ext false []
   350   [Mfix ("_", spropT --> propT, "", [0], 0),
   351    Mfix ("_", logicT --> anyT, "", [0], 0),
   352    Mfix ("_", spropT --> anyT, "", [0], 0),
   353    Mfix ("'(_')", logicT --> logicT, "", [0], max_pri),
   354    Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
   355    Mfix ("_::_",  [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
   356    Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
   357   []
   358   ([], [], [], [])
   359   []
   360   ([], []);
   361 
   362 end;