src/Pure/Syntax/extension.ML

Initial revision

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

Syntax 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_preproc: (ast -> ast) option,
        parse_postproc: (ast -> ast) option,
        parse_translation: (string * (term list -> term)) list,
        print_translation: (string * (term list -> term)) list,
        print_preproc: (ast -> ast) option,
        print_postproc: (ast -> ast) option,
        print_ast_translation: (string * (ast list -> ast)) list}
    datatype synrules =
      SynRules of {
        parse_rules: (ast * ast) list,
        print_rules: (ast * ast) list}
    val max_pri: int
    val logic: string
    val id: string
    val idT: typ
    val var: string
    val varT: typ
    val tfree: string
    val tfreeT: typ
    val tvar: string
    val tvarT: typ
    val typ_to_nt: typ -> string
    val applC: string
    val args: string
    val empty_synrules: synrules
    val empty: string xgram
    val extend: string xgram -> (ext * synrules) -> string xgram
  end
end;

functor ExtensionFun(XGram: XGRAM): EXTENSION =
struct

structure XGram = XGram;
open XGram XGram.Ast;


(** datatype ext **)

(* Mfix (sy, ty, c, pl, p):
    sy: production as symbolic string
    ty: type description of production
    c: corresponding Isabelle Const
    pl: priorities of nonterminals 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_preproc: (ast -> ast) option,
    parse_postproc: (ast -> ast) option,
    parse_translation: (string * (term list -> term)) list,
    print_translation: (string * (term list -> term)) list,
    print_preproc: (ast -> ast) option,
    print_postproc: (ast -> ast) option,
    print_ast_translation: (string * (ast list -> ast)) list};

datatype synrules =
  SynRules of {
    parse_rules: (ast * ast) list,
    print_rules: (ast * ast) list};


(* empty_synrules *)

val empty_synrules = SynRules {parse_rules = [], print_rules = []};


(* empty xgram *)

val empty =
  XGram {
    roots = [], prods = [], consts = [],
    parse_ast_translation = [],
    parse_preproc = None,
    parse_rules = [],
    parse_postproc = None,
    parse_translation = [],
    print_translation = [],
    print_preproc = None,
    print_rules = [],
    print_postproc = None,
    print_ast_translation = []};



(** syntactic constants etc. **)

val max_pri = 1000;   (*maximum legal priority*)

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

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

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


(* terminals *)

val id = "id";
val idT = Type (id, []);

val var = "var";
val varT = Type (var, []);

val tfree = "tfree";
val tfreeT = Type (tfree, []);

val tvar = "tvar";
val tvarT = Type (tvar, []);

val terminalTs = [idT, varT, tfreeT, tvarT];


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

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

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


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



(** extend xgram **)    (* FIXME clean *)

fun nonts syn = foldl (fn (i, "_") => i + 1 | (i, _) => i) (0, explode syn);

val meta_chs = ["(", ")", "/", "_"];

fun mk_term(pref, []) = (pref, [])
  | mk_term(pref, "'"::c::cl) = mk_term(pref^c, cl)
  | mk_term(pref, l as c::cl) = if is_blank(c) orelse c mem meta_chs
        then (pref, l) else mk_term(pref^c, cl);

fun mk_space(sp, []) = (sp, []) |
    mk_space(sp, cl as c::cl') =
      if is_blank(c) then mk_space(sp^c, cl') else (sp, cl);

exception ARG_EXN;
exception BLOCK_EXN;

fun mk_syntax([], ar, _, b, sy) = if b=0 then (sy, ar) else raise BLOCK_EXN
  | mk_syntax("_"::cs, Type("fun", [ar, ar']), [], b, sy) =
        mk_syntax(cs, ar', [], b, sy@[Nonterminal(typ_to_nt ar, 0)])
  | mk_syntax("_"::cs, Type("fun", [ar, ar']), p::pl, b, sy) =
        mk_syntax(cs, ar', pl, b, sy@[Nonterminal(typ_to_nt ar, p)])
  | mk_syntax("_"::cs, _, _, _, _) = raise ARG_EXN
  | mk_syntax("("::cs, ar, pl, b, sy) = let val (i, cs') = scan_int cs
        in mk_syntax(cs', ar, pl, b+1, sy@[Bg(i)]) end
  | mk_syntax(")"::cs, ar, pl, b, sy) =
        if b>0 then mk_syntax(cs, ar, pl, b-1, sy@[En]) else raise BLOCK_EXN
  | mk_syntax("/"::cs, ar, pl, b, sy) = let val (sp, cs') = take_prefix is_blank cs
        in mk_syntax(cs', ar, pl, b, sy@[Brk(length sp)]) end
  | mk_syntax(c::cs, ar, pl, b, sy) =
        let val (term, rest) =
           if is_blank(c)
           then let val (sp, cs') = mk_space(c, cs) in (Space(sp), cs') end
           else let val (tk, cs') = mk_term("", c::cs) in(Terminal(tk), cs') end
        in mk_syntax(rest, ar, pl, b, sy@[term]) end;

fun pri_test1 p = if 0 <= p andalso p <= max_pri then ()
        else error("Priority out of range: " ^ string_of_int p)
fun pri_test(pl, p) = (pri_test1 p; seq pri_test1 pl);

fun mk_prod2(sy, T, opn, pl, p) =
let val (syn, T') = mk_syntax(explode sy, T, pl, 0, []) handle
        ARG_EXN =>
        error("More arguments in "^sy^" than in corresponding type") |
        BLOCK_EXN => error("Unbalanced block parantheses in "^sy);
    val nt = case T' of Type(c, _) => c | _ => logic1;
in Prod(nt, syn, opn, p) end;

fun mk_prod1(sy, T, opn, pl, p) = (pri_test(pl, p); mk_prod2(sy, T, opn, pl, p));


fun terminal1(T as Type("fun", _)) = hd(binder_types T) mem terminalTs
  | terminal1 _ = false;

fun mk_prod(Mfix(sy, T, "", pl, p)) = if nonts sy <> 1
        then error"Copy op must have exactly one argument" else
        if filter_out is_blank (explode sy) = ["_"] andalso
           not(terminal1 T)
        then mk_prod2(sy, T, "", [copy_pri], copy_pri)
        else mk_prod1(sy, T, "", pl, p)
  | mk_prod(Mfix(sy, T, const, pl, p)) = mk_prod1(sy, T, const, pl, p)



fun extend (XGram xgram) (Ext ext, SynRules rules) =
  let
    infix oo;

    fun None oo None = None
      | (Some f) oo None = Some f
      | None oo (Some g) = Some g
      | (Some f) oo (Some g) = Some (f o g);

    fun descend (from, to) = Mfix ("_", to --> from, "", [0], 0);

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

    fun mkappl T =
      Mfix ("_(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_preproc = parse_preproc1,
      parse_rules = parse_rules1,
      parse_postproc = parse_postproc1,
      parse_translation = parse_translation1,
      print_translation = print_translation1,
      print_preproc = print_preproc1,
      print_rules = print_rules1,
      print_postproc = print_postproc1,
      print_ast_translation = print_ast_translation1} = xgram;

    val {roots = roots2, mfix, extra_consts,
      parse_ast_translation = parse_ast_translation2,
      parse_preproc = parse_preproc2,
      parse_postproc = parse_postproc2,
      parse_translation = parse_translation2,
      print_translation = print_translation2,
      print_preproc = print_preproc2,
      print_postproc = print_postproc2,
      print_ast_translation = print_ast_translation2} = ext;

    val {parse_rules = parse_rules2, print_rules = print_rules2} = rules;

    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';
  in
    XGram {
      roots = distinct (roots1 @ roots2),
(*      roots = roots1 union roots2,  *)    (* FIXME remove *)
      prods = prods @ map mk_prod mfix',
      consts = consts union extra_consts,
      parse_ast_translation = parse_ast_translation1 @ parse_ast_translation2,
      parse_preproc = parse_preproc1 oo parse_preproc2,
      parse_rules = parse_rules1 @ parse_rules2,
      parse_postproc = parse_postproc2 oo parse_postproc1,
      parse_translation = parse_translation1 @ parse_translation2,
      print_translation = print_translation1 @ print_translation2,
      print_preproc = print_preproc1 oo print_preproc2,
      print_rules = print_rules1 @ print_rules2,
      print_postproc = print_postproc2 oo print_postproc1,
      print_ast_translation = print_ast_translation1 @ print_ast_translation2}
  end;


end;