diff -r 000000000000 -r a5a9c433f639 src/Pure/Syntax/extension.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Syntax/extension.ML Thu Sep 16 12:20:38 1993 +0200 @@ -0,0 +1,301 @@ +(* 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; +