(* 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;