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