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