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