src/Pure/Syntax/extension.ML

tuned Interrupt msgs;

(*  Title:      Pure/Syntax/extension.ML
    ID:         $Id$
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen

External grammar definition (internal interface).
*)

signature EXTENSION0 =
sig
  val typeT: typ
  val constrainC: string
end;

signature EXTENSION =
sig
  include EXTENSION0
  structure XGram: XGRAM
  local open XGram XGram.Ast in
    datatype mfix = Mfix of string * typ * string * int list * int
    datatype ext =
      Ext of {
        roots: string list,
        mfix: mfix list,
        extra_consts: string list,
        parse_ast_translation: (string * (ast list -> ast)) list,
        parse_translation: (string * (term list -> term)) list,
        print_translation: (string * (term list -> term)) list,
        print_ast_translation: (string * (ast list -> ast)) list} |
      ExtRules of {
        parse_rules: (ast * ast) list,
        print_rules: (ast * ast) list} |
      ExtRoots of string list
    val logic: string
    val args: string
    val idT: typ
    val varT: typ
    val tfreeT: typ
    val tvarT: typ
    val typ_to_nonterm: typ -> string
    val applC: string
    val empty_xgram: xgram
    val extend_xgram: xgram -> ext -> xgram
    val mk_xgram: ext -> xgram
  end
end;

functor ExtensionFun(structure XGram: XGRAM and Lexicon: LEXICON): EXTENSION =
struct

structure XGram = XGram;
open XGram XGram.Ast Lexicon;


(** datatype ext **)

(*Mfix (sy, ty, c, ps, p):
    sy: rhs of production as symbolic string
    ty: type description of production
    c: head of parse tree
    ps: priorities of arguments in sy
    p: priority of production*)

datatype mfix = Mfix of string * typ * string * int list * int;

datatype ext =
  Ext of {
    roots: string list,
    mfix: mfix list,
    extra_consts: string list,
    parse_ast_translation: (string * (ast list -> ast)) list,
    parse_translation: (string * (term list -> term)) list,
    print_translation: (string * (term list -> term)) list,
    print_ast_translation: (string * (ast list -> ast)) list} |
  ExtRules of {
    parse_rules: (ast * ast) list,
    print_rules: (ast * ast) list} |
  ExtRoots of string list;


(* ext_components *)

fun ext_components (Ext ext) = {
      roots = #roots ext,
      mfix = #mfix ext,
      extra_consts = #extra_consts ext,
      parse_ast_translation = #parse_ast_translation ext,
      parse_rules = [],
      parse_translation = #parse_translation ext,
      print_translation = #print_translation ext,
      print_rules = [],
      print_ast_translation = #print_ast_translation ext}
  | ext_components (ExtRules {parse_rules, print_rules}) = {
      roots = [],
      mfix = [],
      extra_consts = [],
      parse_ast_translation = [],
      parse_rules = parse_rules,
      parse_translation = [],
      print_translation = [],
      print_rules = print_rules,
      print_ast_translation = []}
  | ext_components (ExtRoots roots) = {
      roots = roots,
      mfix = [],
      extra_consts = [],
      parse_ast_translation = [],
      parse_rules = [],
      parse_translation = [],
      print_translation = [],
      print_rules = [],
      print_ast_translation = []};


(* empty_xgram *)

val empty_xgram =
  XGram {
    roots = [], prods = [], consts = [],
    parse_ast_translation = [],
    parse_rules = [],
    parse_translation = [],
    print_translation = [],
    print_rules = [],
    print_ast_translation = []};


(* syntactic categories *)

val logic = "logic";
val logicT = Type (logic, []);

val logic1 = "logic1";
val logic1T = Type (logic1, []);

val args = "args";
val argsT = Type (args, []);

val funT = Type ("fun", []);

val typeT = Type ("type", []);


(* terminals *)

val idT = Type (id, []);
val varT = Type (var, []);
val tfreeT = Type (tfree, []);
val tvarT = Type (tvar, []);


(* constants *)

val applC = "_appl";
val constrainC = "_constrain";


(* typ_to_nonterm *)

fun typ_to_nonterm (Type (c, _)) = c
  | typ_to_nonterm _ = logic;

fun typ_to_nonterm1 (Type (c, _)) = c
  | typ_to_nonterm1 _ = logic1;



(** mfix_to_prod **)

fun mfix_to_prod (Mfix (sy, typ, const, pris, pri)) =
  let
    fun err msg =
      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
        error msg);

    fun check_pri p =
      if p >= 0 andalso p <= max_pri then ()
      else err ("precedence out of range: " ^ string_of_int p);

    fun blocks_ok [] 0 = true
      | blocks_ok [] _ = false
      | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
      | blocks_ok (En :: _) 0 = false
      | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
      | blocks_ok (_ :: syms) n = blocks_ok syms n;

    fun check_blocks syms =
      if blocks_ok syms 0 then ()
      else err "unbalanced block parentheses";


    fun is_meta c = c mem ["(", ")", "/", "_"];

    fun scan_delim_char ("'" :: c :: cs) =
          if is_blank c then err "illegal spaces in delimiter" else (c, cs)
      | scan_delim_char ["'"] = err "trailing escape character"
      | scan_delim_char (chs as c :: cs) =
          if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)
      | scan_delim_char [] = raise LEXICAL_ERROR;

    val scan_symb =
      $$ "_" >> K (Nonterminal ("", 0)) ||
      $$ "(" -- scan_int >> (Bg o #2) ||
      $$ ")" >> K En ||
      $$ "/" -- $$ "/" >> K (Brk ~1) ||
      $$ "/" -- scan_any is_blank >> (Brk o length o #2) ||
      scan_any1 is_blank >> (Space o implode) ||
      repeat1 scan_delim_char >> (Terminal o implode);


    val cons_fst = apfst o cons;

    fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
      | add_args [] _ _ = err "too many precedences"
      | add_args (Nonterminal _ :: syms) (Type ("fun", [ty, tys])) [] =
          cons_fst (Nonterminal (typ_to_nonterm ty, 0)) (add_args syms tys [])
      | add_args (Nonterminal _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
          cons_fst (Nonterminal (typ_to_nonterm ty, p)) (add_args syms tys ps)
      | add_args (Nonterminal _ :: _) _ _ =
          err "more arguments than in corresponding type"
      | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);


    fun is_arg (Nonterminal _) = true
      | is_arg _ = false;

    fun is_term (Terminal _) = true
      | is_term (Nonterminal (s, _)) = is_terminal s
      | is_term _ = false;

    fun rem_pri (Nonterminal (s, _)) = Nonterminal (s, chain_pri)
      | rem_pri sym = sym;


    val (raw_symbs, _) = repeat scan_symb (explode sy);
    val (symbs, lhs) = add_args raw_symbs typ pris;
    val prod = Prod (lhs, symbs, const, pri);
  in
    seq check_pri pris;
    check_pri pri;
    check_blocks symbs;

    if is_terminal lhs then err ("illegal lhs: " ^ lhs)
    else if const <> "" then prod
    else if length (filter is_arg symbs) <> 1 then
      err "copy production must have exactly one argument"
    else if exists is_term symbs then prod
    else Prod (lhs, map rem_pri symbs, "", chain_pri)
  end;



(** extend_xgram **)

fun extend_xgram (XGram xgram) ext =
  let
    fun descend (from, to) = Mfix ("_", to --> from, "", [0], 0);

    fun parents T = Mfix ("'(_')", T --> T, "", [0], max_pri);

    fun mkappl T =
      Mfix ("(1_/(1'(_')))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri);

    fun mkid T = Mfix ("_", idT --> T, "", [], max_pri);

    fun mkvar T = Mfix ("_", varT --> T, "", [], max_pri);

    fun constrain T =
      Mfix ("_::_", [T, typeT] ---> T, constrainC, [max_pri, 0], max_pri - 1);


    val {roots = roots1, prods, consts,
      parse_ast_translation = parse_ast_translation1,
      parse_rules = parse_rules1,
      parse_translation = parse_translation1,
      print_translation = print_translation1,
      print_rules = print_rules1,
      print_ast_translation = print_ast_translation1} = xgram;

    val {roots = roots2, mfix, extra_consts,
      parse_ast_translation = parse_ast_translation2,
      parse_rules = parse_rules2,
      parse_translation = parse_translation2,
      print_translation = print_translation2,
      print_rules = print_rules2,
      print_ast_translation = print_ast_translation2} = ext_components ext;

    val Troots = map (apr (Type, [])) (roots2 \\ roots1);
    val Troots' = Troots \\ [typeT, propT, logicT];
    val mfix' = mfix @ map parents (Troots \ logicT) @ map mkappl Troots' @
      map mkid Troots' @ map mkvar Troots' @ map constrain Troots' @
      map (apl (logicT, descend)) (Troots \\ [typeT, logicT]) @
      map (apr (descend, logic1T)) Troots';
    val mfix_consts =
      distinct (filter is_xid (map (fn (Mfix (_, _, c, _, _)) => c) mfix'));
  in
    XGram {
      roots = distinct (roots1 @ roots2),
      prods = prods @ map mfix_to_prod mfix',
      consts = extra_consts union (mfix_consts union consts),
      parse_ast_translation = parse_ast_translation1 @ parse_ast_translation2,
      parse_rules = parse_rules1 @ parse_rules2,
      parse_translation = parse_translation1 @ parse_translation2,
      print_translation = print_translation1 @ print_translation2,
      print_rules = print_rules1 @ print_rules2,
      print_ast_translation = print_ast_translation1 @ print_ast_translation2}
  end;


(* mk_xgram *)

val mk_xgram = extend_xgram empty_xgram;


end;