src/Pure/Syntax/syn_ext.ML
author skalberg
Thu Mar 03 12:43:01 2005 +0100 (2005-03-03)
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15754 f867c48de2e1
permissions -rw-r--r--
Move towards standard functions.
     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 dddot_indexname: indexname
    11   val constrainC: string
    12   val typeT: typ
    13   val max_pri: int
    14 end;
    15 
    16 signature SYN_EXT =
    17 sig
    18   include SYN_EXT0
    19   val logic: string
    20   val args: string
    21   val cargs: string
    22   val any: string
    23   val sprop: string
    24   val typ_to_nonterm: typ -> string
    25   datatype xsymb =
    26     Delim of string |
    27     Argument of string * int |
    28     Space of string |
    29     Bg of int | Brk of int | En
    30   datatype xprod = XProd of string * xsymb list * string * int
    31   val chain_pri: int
    32   val delims_of: xprod list -> string list list
    33   datatype mfix = Mfix of string * typ * string * int list * int
    34   datatype syn_ext =
    35     SynExt of {
    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 * real)) list}
    46   val mfix_args: string -> int
    47   val escape_mfix: string -> string
    48   val syn_ext': bool -> (string -> bool) -> mfix list ->
    49     string list -> (string * (Ast.ast list -> Ast.ast)) list *
    50     (string * (term list -> term)) list *
    51     (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    52     -> (string * string * (string -> string * real)) list
    53     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    54   val syn_ext: mfix list -> string list ->
    55     (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
    56     (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    57     -> (string * string * (string -> string * real)) list
    58     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    59   val syn_ext_const_names: string list -> syn_ext
    60   val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    61   val syn_ext_trfuns:
    62     (string * (Ast.ast list -> Ast.ast)) list *
    63     (string * (term list -> term)) list *
    64     (string * (bool -> typ -> term list -> term)) list *
    65     (string * (Ast.ast list -> Ast.ast)) list -> syn_ext
    66   val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext
    67   val pure_ext: syn_ext
    68 end;
    69 
    70 structure SynExt : SYN_EXT =
    71 struct
    72 
    73 
    74 (** misc definitions **)
    75 
    76 val dddot_indexname = ("dddot", 0);
    77 val constrainC = "_constrain";
    78 
    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 
    98 (** datatype xprod **)
    99 
   100 (*Delim s: delimiter s
   101   Argument (s, p): nonterminal s requiring priority >= p, or valued token
   102   Space s: some white space for printing
   103   Bg, Brk, En: blocks and breaks for pretty printing*)
   104 
   105 datatype xsymb =
   106   Delim of string |
   107   Argument of string * int |
   108   Space of string |
   109   Bg of int | Brk of int | En;
   110 
   111 fun is_delim (Delim _) = true
   112   | is_delim _ = false;
   113 
   114 fun is_terminal (Delim _) = true
   115   | is_terminal (Argument (s, _)) = Lexicon.is_terminal s
   116   | is_terminal _ = false;
   117 
   118 fun is_argument (Argument _) = true
   119   | is_argument _ = false;
   120 
   121 fun is_index (Argument ("index", _)) = true
   122   | is_index _ = false;
   123 
   124 val index = Argument ("index", 1000);
   125 
   126 
   127 (*XProd (lhs, syms, c, p):
   128     lhs: name of nonterminal on the lhs of the production
   129     syms: list of symbols on the rhs of the production
   130     c: head of parse tree
   131     p: priority of this production*)
   132 
   133 datatype xprod = XProd of string * xsymb list * string * int;
   134 
   135 val max_pri = 1000;   (*maximum legal priority*)
   136 val chain_pri = ~1;   (*dummy for chain productions*)
   137 
   138 
   139 (* delims_of *)
   140 
   141 fun delims_of xprods =
   142   let
   143     fun del_of (Delim s) = SOME s
   144       | del_of _ = NONE;
   145 
   146     fun dels_of (XProd (_, xsymbs, _, _)) =
   147       List.mapPartial del_of xsymbs;
   148   in
   149     map Symbol.explode (distinct (List.concat (map dels_of xprods)))
   150   end;
   151 
   152 
   153 
   154 (** datatype mfix **)
   155 
   156 (*Mfix (sy, ty, c, ps, p):
   157     sy: rhs of production as symbolic string
   158     ty: type description of production
   159     c: head of parse tree
   160     ps: priorities of arguments in sy
   161     p: priority of production*)
   162 
   163 datatype mfix = Mfix of string * typ * string * int list * int;
   164 
   165 fun err_in_mfix msg (Mfix (sy, _, const, _, _)) =
   166   error ((if msg = "" then "" else msg ^ "\n") ^
   167     "in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
   168 
   169 
   170 (* typ_to_nonterm *)
   171 
   172 fun typ_to_nt _ (Type (c, _)) = c
   173   | typ_to_nt default _ = default;
   174 
   175 (*get nonterminal for rhs*)
   176 val typ_to_nonterm = typ_to_nt any;
   177 
   178 (*get nonterminal for lhs*)
   179 val typ_to_nonterm1 = typ_to_nt logic;
   180 
   181 
   182 (* read_mixfix *)
   183 
   184 local
   185   fun is_meta c = c mem ["(", ")", "/", "_", "\\<index>"];
   186 
   187   val scan_delim_char =
   188     $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
   189     Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
   190 
   191   fun read_int ["0", "0"] = ~1
   192     | read_int cs = #1 (Library.read_int cs);
   193 
   194   val scan_sym =
   195     $$ "_" >> K (Argument ("", 0)) ||
   196     $$ "\\<index>" >> K index ||
   197     $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o read_int) ||
   198     $$ ")" >> K En ||
   199     $$ "/" -- $$ "/" >> K (Brk ~1) ||
   200     $$ "/" |-- Scan.any Symbol.is_blank >> (Brk o length) ||
   201     Scan.any1 Symbol.is_blank >> (Space o implode) ||
   202     Scan.repeat1 scan_delim_char >> (Delim o implode);
   203 
   204   val scan_symb =
   205     scan_sym >> SOME ||
   206     $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
   207 
   208   val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
   209   val read_symbs = List.mapPartial I o valOf o Scan.read Symbol.stopper scan_symbs;
   210 
   211   fun unique_index xsymbs =
   212     if length (List.filter is_index xsymbs) <= 1 then xsymbs
   213     else error "Duplicate index arguments (\\<index>)";
   214 in
   215   val read_mixfix = unique_index o read_symbs o Symbol.explode;
   216   val mfix_args = length o List.filter is_argument o read_mixfix;
   217   val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
   218 end;
   219 
   220 
   221 (* mfix_to_xprod *)
   222 
   223 fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
   224   let
   225     fun check_pri p =
   226       if p >= 0 andalso p <= max_pri then ()
   227       else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
   228 
   229     fun blocks_ok [] 0 = true
   230       | blocks_ok [] _ = false
   231       | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
   232       | blocks_ok (En :: _) 0 = false
   233       | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
   234       | blocks_ok (_ :: syms) n = blocks_ok syms n;
   235 
   236     fun check_blocks syms =
   237       if blocks_ok syms 0 then ()
   238       else err_in_mfix "Unbalanced block parentheses" mfix;
   239 
   240 
   241     val cons_fst = apfst o cons;
   242 
   243     fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
   244       | add_args [] _ _ = err_in_mfix "Too many precedences" mfix
   245       | add_args ((arg as Argument ("index", _)) :: syms) ty ps =
   246           cons_fst arg (add_args syms ty ps)
   247       | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
   248           cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys [])
   249       | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
   250           cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps)
   251       | add_args (Argument _ :: _) _ _ =
   252           err_in_mfix "More arguments than in corresponding type" mfix
   253       | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
   254 
   255     fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
   256       | rem_pri sym = sym;
   257 
   258     fun logify_types copy_prod (a as (Argument (s, p))) =
   259           if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
   260       | logify_types _ a = a;
   261 
   262 
   263     val raw_symbs = read_mixfix sy handle ERROR => err_in_mfix "" mfix;
   264     val args = List.filter (fn Argument _ => true | _ => false) raw_symbs;
   265     val (const', typ', parse_rules) =
   266       if not (exists is_index args) then (const, typ, [])
   267       else
   268         let
   269           val indexed_const = if const <> "" then "_indexed_" ^ const
   270             else err_in_mfix "Missing constant name for indexed syntax" mfix;
   271           val rangeT = Term.range_type typ handle Match =>
   272             err_in_mfix "Missing structure argument for indexed syntax" mfix;
   273 
   274           val xs = map Ast.Variable (Term.invent_names [] "xa" (length args - 1));
   275           val (xs1, xs2) = Library.splitAt (Library.find_index is_index args, xs);
   276           val i = Ast.Variable "i";
   277           val lhs = Ast.mk_appl (Ast.Constant indexed_const)
   278             (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
   279           val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs);
   280         in (indexed_const, rangeT, [(lhs, rhs)]) end;
   281 
   282     val (symbs, lhs) = add_args raw_symbs typ' pris;
   283 
   284     val copy_prod =
   285       lhs mem ["prop", "logic"]
   286         andalso const <> ""
   287         andalso not (null symbs)
   288         andalso not (exists is_delim symbs);
   289     val lhs' =
   290       if convert andalso not copy_prod then
   291        (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
   292       else lhs;
   293     val symbs' = map (logify_types copy_prod) symbs;
   294     val xprod = XProd (lhs', symbs', const', pri);
   295 
   296     val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');
   297     val xprod' =
   298       if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix
   299       else if const <> "" then xprod
   300       else if length (List.filter is_argument symbs') <> 1 then
   301         err_in_mfix "Copy production must have exactly one argument" mfix
   302       else if exists is_terminal symbs' then xprod
   303       else XProd (lhs', map rem_pri symbs', "", chain_pri);
   304 
   305   in (xprod', parse_rules) end;
   306 
   307 
   308 
   309 (** datatype syn_ext **)
   310 
   311 datatype syn_ext =
   312   SynExt of {
   313     xprods: xprod list,
   314     consts: string list,
   315     prmodes: string list,
   316     parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
   317     parse_rules: (Ast.ast * Ast.ast) list,
   318     parse_translation: (string * (term list -> term)) list,
   319     print_translation: (string * (bool -> typ -> term list -> term)) list,
   320     print_rules: (Ast.ast * Ast.ast) list,
   321     print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
   322     token_translation: (string * string * (string -> string * real)) list}
   323 
   324 
   325 (* syn_ext *)
   326 
   327 fun syn_ext' convert is_logtype mfixes consts trfuns tokentrfuns (parse_rules, print_rules) =
   328   let
   329     val (parse_ast_translation, parse_translation, print_translation,
   330       print_ast_translation) = trfuns;
   331 
   332     val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
   333       |> split_list |> apsnd (rev o List.concat);
   334     val mfix_consts = distinct (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
   335   in
   336     SynExt {
   337       xprods = xprods,
   338       consts = consts union_string mfix_consts,
   339       prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
   340       parse_ast_translation = parse_ast_translation,
   341       parse_rules = parse_rules' @ parse_rules,
   342       parse_translation = parse_translation,
   343       print_translation = print_translation,
   344       print_rules = map swap parse_rules' @ print_rules,
   345       print_ast_translation = print_ast_translation,
   346       token_translation = tokentrfuns}
   347   end;
   348 
   349 
   350 val syn_ext = syn_ext' true (K false);
   351 
   352 fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) [] ([], []);
   353 fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) [] rules;
   354 fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns [] ([], []);
   355 fun syn_ext_tokentrfuns trfuns = syn_ext [] [] ([], [], [], []) trfuns ([], []);
   356 
   357 
   358 (* pure_ext *)
   359 
   360 val pure_ext = syn_ext' false (K false)
   361   [Mfix ("_", spropT --> propT, "", [0], 0),
   362    Mfix ("_", logicT --> anyT, "", [0], 0),
   363    Mfix ("_", spropT --> anyT, "", [0], 0),
   364    Mfix ("'(_')", logicT --> logicT, "", [0], max_pri),
   365    Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
   366    Mfix ("_::_",  [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
   367    Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
   368   []
   369   ([], [], [], [])
   370   []
   371   ([], []);
   372 
   373 end;