1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Jan 19 14:27:46 1994 +0100
     1.3 @@ -0,0 +1,314 @@
     1.4 +(*  Title:      Pure/Syntax/syn_ext.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Syntax extension (internal interface).
     1.9 +*)
    1.10 +
    1.11 +signature SYN_EXT0 =
    1.12 +sig
    1.13 +  val typeT: typ
    1.14 +  val constrainC: string
    1.15 +end;
    1.16 +
    1.17 +signature SYN_EXT =
    1.18 +sig
    1.19 +  include SYN_EXT0
    1.20 +  structure Ast: AST
    1.21 +  local open Ast in
    1.22 +    val logic: string
    1.23 +    val args: string
    1.24 +    val idT: typ
    1.25 +    val varT: typ
    1.26 +    val tfreeT: typ
    1.27 +    val tvarT: typ
    1.28 +    val applC: string
    1.29 +    val typ_to_nonterm: typ -> string
    1.30 +    datatype xsymb =
    1.31 +      Delim of string |
    1.32 +      Argument of string * int |
    1.33 +      Space of string |
    1.34 +      Bg of int | Brk of int | En
    1.35 +    datatype xprod = XProd of string * xsymb list * string * int
    1.36 +    val max_pri: int
    1.37 +    val chain_pri: int
    1.38 +    val delims_of: xprod list -> string list
    1.39 +    datatype mfix = Mfix of string * typ * string * int list * int
    1.40 +    datatype syn_ext =
    1.41 +      SynExt of {
    1.42 +        roots: string list,
    1.43 +        xprods: xprod list,
    1.44 +        consts: string list,
    1.45 +        parse_ast_translation: (string * (ast list -> ast)) list,
    1.46 +        parse_rules: (ast * ast) list,
    1.47 +        parse_translation: (string * (term list -> term)) list,
    1.48 +        print_translation: (string * (term list -> term)) list,
    1.49 +        print_rules: (ast * ast) list,
    1.50 +        print_ast_translation: (string * (ast list -> ast)) list}
    1.51 +    val syn_ext: string list -> mfix list -> string list ->
    1.52 +      (string * (ast list -> ast)) list * (string * (term list -> term)) list *
    1.53 +      (string * (term list -> term)) list * (string * (ast list -> ast)) list
    1.54 +      -> (ast * ast) list * (ast * ast) list -> syn_ext
    1.55 +    val syn_ext_rules: (ast * ast) list * (ast * ast) list -> syn_ext
    1.56 +    val syn_ext_roots: string list -> syn_ext
    1.57 +  end
    1.58 +end;
    1.59 +
    1.60 +functor SynExtFun(structure Lexicon: LEXICON and Ast: AST): SYN_EXT =
    1.61 +struct
    1.62 +
    1.63 +structure Ast = Ast;
    1.64 +open Lexicon Ast;
    1.65 +
    1.66 +
    1.67 +(** misc definitions **)
    1.68 +
    1.69 +(* syntactic categories *)
    1.70 +
    1.71 +val logic = "logic";
    1.72 +val logicT = Type (logic, []);
    1.73 +
    1.74 +val logic1 = "logic1";
    1.75 +val logic1T = Type (logic1, []);
    1.76 +
    1.77 +val args = "args";
    1.78 +val argsT = Type (args, []);
    1.79 +
    1.80 +val funT = Type ("fun", []);
    1.81 +
    1.82 +val typeT = Type ("type", []);
    1.83 +
    1.84 +
    1.85 +(* terminals *)
    1.86 +
    1.87 +val idT = Type (id, []);
    1.88 +val varT = Type (var, []);
    1.89 +val tfreeT = Type (tfree, []);
    1.90 +val tvarT = Type (tvar, []);
    1.91 +
    1.92 +
    1.93 +(* constants *)
    1.94 +
    1.95 +val applC = "_appl";
    1.96 +val constrainC = "_constrain";
    1.97 +
    1.98 +
    1.99 +
   1.100 +(** datatype xprod **)
   1.101 +
   1.102 +(*Delim s: delimiter s
   1.103 +  Argument (s, p): nonterminal s requiring priority >= p, or valued token
   1.104 +  Space s: some white space for printing
   1.105 +  Bg, Brk, En: blocks and breaks for pretty printing*)
   1.106 +
   1.107 +datatype xsymb =
   1.108 +  Delim of string |
   1.109 +  Argument of string * int |
   1.110 +  Space of string |
   1.111 +  Bg of int | Brk of int | En;
   1.112 +
   1.113 +
   1.114 +(*XProd (lhs, syms, c, p):
   1.115 +    lhs: name of nonterminal on the lhs of the production
   1.116 +    syms: list of symbols on the rhs of the production
   1.117 +    c: head of parse tree
   1.118 +    p: priority of this production*)
   1.119 +
   1.120 +datatype xprod = XProd of string * xsymb list * string * int;
   1.121 +
   1.122 +val max_pri = 1000;   (*maximum legal priority*)
   1.123 +val chain_pri = ~1;   (*dummy for chain productions*)
   1.124 +
   1.125 +
   1.126 +(* delims_of *)
   1.127 +
   1.128 +fun delims_of xprods =
   1.129 +  let
   1.130 +    fun del_of (Delim s) = Some s
   1.131 +      | del_of _ = None;
   1.132 +
   1.133 +    fun dels_of (XProd (_, xsymbs, _, _)) =
   1.134 +      mapfilter del_of xsymbs;
   1.135 +  in
   1.136 +    distinct (flat (map dels_of xprods))
   1.137 +  end;
   1.138 +
   1.139 +
   1.140 +
   1.141 +(** datatype mfix **)
   1.142 +
   1.143 +(*Mfix (sy, ty, c, ps, p):
   1.144 +    sy: rhs of production as symbolic string
   1.145 +    ty: type description of production
   1.146 +    c: head of parse tree
   1.147 +    ps: priorities of arguments in sy
   1.148 +    p: priority of production*)
   1.149 +
   1.150 +datatype mfix = Mfix of string * typ * string * int list * int;
   1.151 +
   1.152 +
   1.153 +(* typ_to_nonterm *)
   1.154 +
   1.155 +fun typ_to_nonterm (Type (c, _)) = c
   1.156 +  | typ_to_nonterm _ = logic;
   1.157 +
   1.158 +fun typ_to_nonterm1 (Type (c, _)) = c
   1.159 +  | typ_to_nonterm1 _ = logic1;
   1.160 +
   1.161 +
   1.162 +(* mfix_to_xprod *)
   1.163 +
   1.164 +fun mfix_to_xprod (Mfix (sy, typ, const, pris, pri)) =
   1.165 +  let
   1.166 +    fun err msg =
   1.167 +      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
   1.168 +        error msg);
   1.169 +
   1.170 +    fun check_pri p =
   1.171 +      if p >= 0 andalso p <= max_pri then ()
   1.172 +      else err ("precedence out of range: " ^ string_of_int p);
   1.173 +
   1.174 +    fun blocks_ok [] 0 = true
   1.175 +      | blocks_ok [] _ = false
   1.176 +      | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
   1.177 +      | blocks_ok (En :: _) 0 = false
   1.178 +      | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
   1.179 +      | blocks_ok (_ :: syms) n = blocks_ok syms n;
   1.180 +
   1.181 +    fun check_blocks syms =
   1.182 +      if blocks_ok syms 0 then ()
   1.183 +      else err "unbalanced block parentheses";
   1.184 +
   1.185 +
   1.186 +    fun is_meta c = c mem ["(", ")", "/", "_"];
   1.187 +
   1.188 +    fun scan_delim_char ("'" :: c :: cs) =
   1.189 +          if is_blank c then err "illegal spaces in delimiter" else (c, cs)
   1.190 +      | scan_delim_char ["'"] = err "trailing escape character"
   1.191 +      | scan_delim_char (chs as c :: cs) =
   1.192 +          if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)
   1.193 +      | scan_delim_char [] = raise LEXICAL_ERROR;
   1.194 +
   1.195 +    val scan_symb =
   1.196 +      $$ "_" >> K (Argument ("", 0)) ||
   1.197 +      $$ "(" -- scan_int >> (Bg o #2) ||
   1.198 +      $$ ")" >> K En ||
   1.199 +      $$ "/" -- $$ "/" >> K (Brk ~1) ||
   1.200 +      $$ "/" -- scan_any is_blank >> (Brk o length o #2) ||
   1.201 +      scan_any1 is_blank >> (Space o implode) ||
   1.202 +      repeat1 scan_delim_char >> (Delim o implode);
   1.203 +
   1.204 +
   1.205 +    val cons_fst = apfst o cons;
   1.206 +
   1.207 +    fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
   1.208 +      | add_args [] _ _ = err "too many precedences"
   1.209 +      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
   1.210 +          cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys [])
   1.211 +      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
   1.212 +          cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps)
   1.213 +      | add_args (Argument _ :: _) _ _ =
   1.214 +          err "more arguments than in corresponding type"
   1.215 +      | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
   1.216 +
   1.217 +
   1.218 +    fun is_arg (Argument _) = true
   1.219 +      | is_arg _ = false;
   1.220 +
   1.221 +    fun is_term (Delim _) = true
   1.222 +      | is_term (Argument (s, _)) = is_terminal s
   1.223 +      | is_term _ = false;
   1.224 +
   1.225 +    fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
   1.226 +      | rem_pri sym = sym;
   1.227 +
   1.228 +
   1.229 +    val (raw_symbs, _) = repeat scan_symb (explode sy);
   1.230 +    val (symbs, lhs) = add_args raw_symbs typ pris;
   1.231 +    val xprod = XProd (lhs, symbs, const, pri);
   1.232 +  in
   1.233 +    seq check_pri pris;
   1.234 +    check_pri pri;
   1.235 +    check_blocks symbs;
   1.236 +
   1.237 +    if is_terminal lhs then err ("illegal lhs: " ^ lhs)
   1.238 +    else if const <> "" then xprod
   1.239 +    else if length (filter is_arg symbs) <> 1 then
   1.240 +      err "copy production must have exactly one argument"
   1.241 +    else if exists is_term symbs then xprod
   1.242 +    else XProd (lhs, map rem_pri symbs, "", chain_pri)
   1.243 +  end;
   1.244 +
   1.245 +
   1.246 +
   1.247 +(** datatype syn_ext **)
   1.248 +
   1.249 +datatype syn_ext =
   1.250 +  SynExt of {
   1.251 +    roots: string list,
   1.252 +    xprods: xprod list,
   1.253 +    consts: string list,
   1.254 +    parse_ast_translation: (string * (ast list -> ast)) list,
   1.255 +    parse_rules: (ast * ast) list,
   1.256 +    parse_translation: (string * (term list -> term)) list,
   1.257 +    print_translation: (string * (term list -> term)) list,
   1.258 +    print_rules: (ast * ast) list,
   1.259 +    print_ast_translation: (string * (ast list -> ast)) list};
   1.260 +
   1.261 +
   1.262 +(* syn_ext *)
   1.263 +
   1.264 +fun syn_ext roots mfixes consts trfuns rules =
   1.265 +  let
   1.266 +    fun descend (from, to) = Mfix ("_", to --> from, "", [0], 0);
   1.267 +
   1.268 +    fun parents T = Mfix ("'(_')", T --> T, "", [0], max_pri);
   1.269 +
   1.270 +    fun mkappl T =
   1.271 +      Mfix ("(1_/(1'(_')))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri);
   1.272 +
   1.273 +    fun mkid T = Mfix ("_", idT --> T, "", [], max_pri);
   1.274 +
   1.275 +    fun mkvar T = Mfix ("_", varT --> T, "", [], max_pri);
   1.276 +
   1.277 +    fun constrain T =
   1.278 +      Mfix ("_::_", [T, typeT] ---> T, constrainC, [max_pri, 0], max_pri - 1);
   1.279 +
   1.280 +
   1.281 +    val (parse_ast_translation, parse_translation, print_translation,
   1.282 +      print_ast_translation) = trfuns;
   1.283 +    val (parse_rules, print_rules) = rules;
   1.284 +
   1.285 +    val Troots = map (apr (Type, [])) roots;
   1.286 +    val Troots' = Troots \\ [typeT, propT, logicT];
   1.287 +    val mfixes' = mfixes @ map parents (Troots \ logicT) @ map mkappl Troots' @
   1.288 +      map mkid Troots' @ map mkvar Troots' @ map constrain Troots' @
   1.289 +      map (apl (logicT, descend)) (Troots \\ [typeT, logicT]) @
   1.290 +      map (apr (descend, logic1T)) Troots';
   1.291 +    val mfix_consts =
   1.292 +      distinct (filter is_xid (map (fn (Mfix (_, _, c, _, _)) => c) mfixes'));
   1.293 +  in
   1.294 +    SynExt {
   1.295 +      roots = roots,
   1.296 +      xprods = map mfix_to_xprod mfixes',
   1.297 +      consts = consts union mfix_consts,
   1.298 +      parse_ast_translation = parse_ast_translation,
   1.299 +      parse_rules = parse_rules,
   1.300 +      parse_translation = parse_translation,
   1.301 +      print_translation = print_translation,
   1.302 +      print_rules = print_rules,
   1.303 +      print_ast_translation = print_ast_translation}
   1.304 +  end;
   1.305 +
   1.306 +
   1.307 +(* syn_ext_rules, syn_ext_roots *)
   1.308 +
   1.309 +fun syn_ext_rules rules =
   1.310 +  syn_ext [] [] [] ([], [], [], []) rules;
   1.311 +
   1.312 +fun syn_ext_roots roots =
   1.313 +  syn_ext roots [] [] ([], [], [], []) ([], []);
   1.314 +
   1.315 +
   1.316 +end;
   1.317 +