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