src/Pure/Syntax/syntax_ext.ML
author wenzelm
Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499 f496b2b7bafb
parent 44470 6c6c31ef6bb2
child 52143 36ffe23b25f8
permissions -rw-r--r--
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
     1 (*  Title:      Pure/Syntax/syntax_ext.ML
     2     Author:     Markus Wenzel and Carsten Clasohm, TU Muenchen
     3 
     4 Syntax extension.
     5 *)
     6 
     7 signature SYNTAX_EXT =
     8 sig
     9   val dddot_indexname: indexname
    10   datatype mfix = Mfix of string * typ * string * int list * int
    11   val err_in_mfix: string -> mfix -> 'a
    12   val typ_to_nonterm: typ -> string
    13   datatype xsymb =
    14     Delim of string |
    15     Argument of string * int |
    16     Space of string |
    17     Bg of int | Brk of int | En
    18   datatype xprod = XProd of string * xsymb list * string * int
    19   val chain_pri: int
    20   val delims_of: xprod list -> string list list
    21   datatype syn_ext =
    22     Syn_Ext of {
    23       xprods: xprod list,
    24       consts: (string * string) list,
    25       parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    26       parse_rules: (Ast.ast * Ast.ast) list,
    27       parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
    28       print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
    29       print_rules: (Ast.ast * Ast.ast) list,
    30       print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list}
    31   val mfix_delims: string -> string list
    32   val mfix_args: string -> int
    33   val escape: string -> string
    34   val syn_ext': (string -> bool) -> mfix list ->
    35     (string * string) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    36     (string * ((Proof.context -> term list -> term) * stamp)) list *
    37     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
    38     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
    39     (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    40   val syn_ext: mfix list -> (string * string) list ->
    41     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    42     (string * ((Proof.context -> term list -> term) * stamp)) list *
    43     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
    44     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
    45     (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    46   val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    47   val syn_ext_trfuns:
    48     (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
    49     (string * ((term list -> term) * stamp)) list *
    50     (string * ((typ -> term list -> term) * stamp)) list *
    51     (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    52   val syn_ext_advanced_trfuns:
    53     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    54     (string * ((Proof.context -> term list -> term) * stamp)) list *
    55     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
    56     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    57   val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
    58   val mk_trfun: string * 'a -> string * ('a * stamp)
    59   val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
    60 end;
    61 
    62 structure Syntax_Ext: SYNTAX_EXT =
    63 struct
    64 
    65 
    66 (** misc definitions **)
    67 
    68 val dddot_indexname = ("dddot", 0);
    69 
    70 
    71 (** datatype xprod **)
    72 
    73 (*Delim s: delimiter s
    74   Argument (s, p): nonterminal s requiring priority >= p, or valued token
    75   Space s: some white space for printing
    76   Bg, Brk, En: blocks and breaks for pretty printing*)
    77 
    78 datatype xsymb =
    79   Delim of string |
    80   Argument of string * int |
    81   Space of string |
    82   Bg of int | Brk of int | En;
    83 
    84 fun is_delim (Delim _) = true
    85   | is_delim _ = false;
    86 
    87 fun is_terminal (Delim _) = true
    88   | is_terminal (Argument (s, _)) = Lexicon.is_terminal s
    89   | is_terminal _ = false;
    90 
    91 fun is_argument (Argument _) = true
    92   | is_argument _ = false;
    93 
    94 fun is_index (Argument ("index", _)) = true
    95   | is_index _ = false;
    96 
    97 val index = Argument ("index", 1000);
    98 
    99 
   100 (*XProd (lhs, syms, c, p):
   101     lhs: name of nonterminal on the lhs of the production
   102     syms: list of symbols on the rhs of the production
   103     c: head of parse tree
   104     p: priority of this production*)
   105 
   106 datatype xprod = XProd of string * xsymb list * string * int;
   107 
   108 val chain_pri = ~1;   (*dummy for chain productions*)
   109 
   110 fun delims_of xprods =
   111   fold (fn XProd (_, xsymbs, _, _) =>
   112     fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods []
   113   |> map Symbol.explode;
   114 
   115 
   116 
   117 (** datatype mfix **)
   118 
   119 (*Mfix (sy, ty, c, ps, p):
   120     sy: rhs of production as symbolic string
   121     ty: type description of production
   122     c: head of parse tree
   123     ps: priorities of arguments in sy
   124     p: priority of production*)
   125 
   126 datatype mfix = Mfix of string * typ * string * int list * int;
   127 
   128 fun err_in_mfix msg (Mfix (sy, _, const, _, _)) =
   129   cat_error msg ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
   130 
   131 
   132 (* typ_to_nonterm *)
   133 
   134 fun typ_to_nt _ (Type (c, _)) = c
   135   | typ_to_nt default _ = default;
   136 
   137 (*get nonterminal for rhs*)
   138 val typ_to_nonterm = typ_to_nt "any";
   139 
   140 (*get nonterminal for lhs*)
   141 val typ_to_nonterm1 = typ_to_nt "logic";
   142 
   143 
   144 (* read mixfix annotations *)
   145 
   146 local
   147 
   148 val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
   149 
   150 val scan_delim_char =
   151   $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) ||
   152   Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular);
   153 
   154 fun read_int ["0", "0"] = ~1
   155   | read_int cs = #1 (Library.read_int cs);
   156 
   157 val scan_sym =
   158   $$ "_" >> K (Argument ("", 0)) ||
   159   $$ "\\<index>" >> K index ||
   160   $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
   161   $$ ")" >> K En ||
   162   $$ "/" -- $$ "/" >> K (Brk ~1) ||
   163   $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) ||
   164   Scan.many1 Symbol.is_blank >> (Space o implode) ||
   165   Scan.repeat1 scan_delim_char >> (Delim o implode);
   166 
   167 val scan_symb =
   168   scan_sym >> SOME ||
   169   $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
   170 
   171 val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'");
   172 val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs;
   173 
   174 fun unique_index xsymbs =
   175   if length (filter is_index xsymbs) <= 1 then xsymbs
   176   else error "Duplicate index arguments (\\<index>)";
   177 
   178 in
   179 
   180 val read_mfix = unique_index o read_symbs o Symbol.explode;
   181 
   182 fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) [];
   183 val mfix_args = length o filter is_argument o read_mfix;
   184 
   185 val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
   186 
   187 end;
   188 
   189 
   190 (* mfix_to_xprod *)
   191 
   192 fun mfix_to_xprod is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
   193   let
   194     fun check_pri p =
   195       if p >= 0 andalso p <= 1000 then ()
   196       else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
   197 
   198     fun blocks_ok [] 0 = true
   199       | blocks_ok [] _ = false
   200       | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
   201       | blocks_ok (En :: _) 0 = false
   202       | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
   203       | blocks_ok (_ :: syms) n = blocks_ok syms n;
   204 
   205     fun check_blocks syms =
   206       if blocks_ok syms 0 then ()
   207       else err_in_mfix "Unbalanced block parentheses" mfix;
   208 
   209 
   210     val cons_fst = apfst o cons;
   211 
   212     fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
   213       | add_args [] _ _ = err_in_mfix "Too many precedences" mfix
   214       | add_args ((arg as Argument ("index", _)) :: syms) ty ps =
   215           cons_fst arg (add_args syms ty ps)
   216       | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
   217           cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys [])
   218       | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
   219           cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps)
   220       | add_args (Argument _ :: _) _ _ =
   221           err_in_mfix "More arguments than in corresponding type" mfix
   222       | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
   223 
   224     fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
   225       | rem_pri sym = sym;
   226 
   227     fun logify_types (a as (Argument (s, p))) =
   228           if s <> "prop" andalso is_logtype s then Argument ("logic", p) else a
   229       | logify_types a = a;
   230 
   231 
   232     val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
   233     val args = filter (fn Argument _ => true | _ => false) raw_symbs;
   234     val (const', typ', syntax_consts, parse_rules) =
   235       if not (exists is_index args) then (const, typ, NONE, NONE)
   236       else
   237         let
   238           val indexed_const =
   239             if const <> "" then const ^ "_indexed"
   240             else err_in_mfix "Missing constant name for indexed syntax" mfix;
   241           val rangeT = Term.range_type typ handle Match =>
   242             err_in_mfix "Missing structure argument for indexed syntax" mfix;
   243 
   244           val xs = map Ast.Variable (Name.invent Name.context "xa" (length args - 1));
   245           val (xs1, xs2) = chop (find_index is_index args) xs;
   246           val i = Ast.Variable "i";
   247           val lhs = Ast.mk_appl (Ast.Constant indexed_const)
   248             (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
   249           val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs);
   250         in (indexed_const, rangeT, SOME (indexed_const, const), SOME (lhs, rhs)) end;
   251 
   252     val (symbs, lhs) = add_args raw_symbs typ' pris;
   253 
   254     val copy_prod =
   255       (lhs = "prop" orelse lhs = "logic")
   256         andalso const <> ""
   257         andalso not (null symbs)
   258         andalso not (exists is_delim symbs);
   259     val lhs' =
   260       if copy_prod orelse lhs = "prop" andalso symbs = [Argument ("prop'", 0)] then lhs
   261       else if lhs = "prop" then "prop'"
   262       else if is_logtype lhs then "logic"
   263       else lhs;
   264     val symbs' = map logify_types symbs;
   265     val xprod = XProd (lhs', symbs', const', pri);
   266 
   267     val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');
   268     val xprod' =
   269       if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix
   270       else if const <> "" then xprod
   271       else if length (filter is_argument symbs') <> 1 then
   272         err_in_mfix "Copy production must have exactly one argument" mfix
   273       else if exists is_terminal symbs' then xprod
   274       else XProd (lhs', map rem_pri symbs', "", chain_pri);
   275 
   276   in (xprod', syntax_consts, parse_rules) end;
   277 
   278 
   279 
   280 (** datatype syn_ext **)
   281 
   282 datatype syn_ext =
   283   Syn_Ext of {
   284     xprods: xprod list,
   285     consts: (string * string) list,
   286     parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
   287     parse_rules: (Ast.ast * Ast.ast) list,
   288     parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
   289     print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
   290     print_rules: (Ast.ast * Ast.ast) list,
   291     print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list};
   292 
   293 
   294 (* syn_ext *)
   295 
   296 fun syn_ext' is_logtype mfixes consts trfuns (parse_rules, print_rules) =
   297   let
   298     val (parse_ast_translation, parse_translation, print_translation,
   299       print_ast_translation) = trfuns;
   300 
   301     val xprod_results = map (mfix_to_xprod is_logtype) mfixes;
   302     val xprods = map #1 xprod_results;
   303     val consts' = map_filter #2 xprod_results;
   304     val parse_rules' = rev (map_filter #3 xprod_results);
   305     val mfix_consts = map (fn Mfix x => (#3 x, "")) mfixes @ map (fn XProd x => (#3 x, "")) xprods;
   306   in
   307     Syn_Ext {
   308       xprods = xprods,
   309       consts = mfix_consts @ consts' @ consts,
   310       parse_ast_translation = parse_ast_translation,
   311       parse_rules = parse_rules' @ parse_rules,
   312       parse_translation = parse_translation,
   313       print_translation = print_translation,
   314       print_rules = map swap parse_rules' @ print_rules,
   315       print_ast_translation = print_ast_translation}
   316   end;
   317 
   318 
   319 val syn_ext = syn_ext' (K false);
   320 
   321 fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
   322 fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns ([], []);
   323 
   324 fun syn_ext_trfuns (atrs, trs, tr's, atr's) =
   325   let fun simple (name, (f, s)) = (name, (K f, s)) in
   326     syn_ext_advanced_trfuns (map simple atrs, map simple trs, map simple tr's, map simple atr's)
   327   end;
   328 
   329 fun stamp_trfun s (c, f) = (c, (f, s));
   330 fun mk_trfun tr = stamp_trfun (stamp ()) tr;
   331 fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2;
   332 
   333 end;