# HG changeset patch # User wenzelm # Date 758985757 -3600 # Node ID 6af40e3a2bcbeef66f5c04db7ee96dffd9b7b428 # Parent a7d3e712767a37fd2f2bcb1ab271cb72e2d31220 MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables now much leaner (eliminated gramgraph, all data except tables of old parser are shared); simplified the internal interfaces for syntax extension; added translations for _explode, _implode (experimental); diff -r a7d3e712767a -r 6af40e3a2bcb src/Pure/Syntax/sextension.ML --- a/src/Pure/Syntax/sextension.ML Wed Jan 19 14:21:26 1994 +0100 +++ b/src/Pure/Syntax/sextension.ML Wed Jan 19 14:22:37 1994 +0100 @@ -6,15 +6,15 @@ binders, translation rules / functions and the Pure syntax. TODO: - move ast_to_term (?) + move ast_to_term, pt_to_ast (?) *) infix |-> <-| <->; signature SEXTENSION0 = sig - structure Ast: AST - local open Ast in + structure Parser: PARSER + local open Parser.SynExt.Ast in datatype mixfix = Mixfix of string * string * string * int list * int | Delimfix of string * string * string | @@ -61,25 +61,22 @@ signature SEXTENSION = sig include SEXTENSION1 - structure Extension: EXTENSION - sharing Extension.XGram.Ast = Ast - local open Extension Ast in + local open Parser Parser.SynExt Parser.SynExt.Ast in val xrules_of: sext -> xrule list val abs_tr': term -> term val appl_ast_tr': ast * ast list -> ast - val ext_of_sext: string list -> string list -> (string -> typ) -> sext -> ext + val syn_ext_of_sext: string list -> string list -> (string -> typ) -> sext -> syn_ext + val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast val ast_to_term: (string -> (term list -> term) option) -> ast -> term - val constrainIdtC: string val apropC: string end end; -functor SExtensionFun(structure TypeExt: TYPE_EXT and Lexicon: LEXICON): SEXTENSION = +functor SExtensionFun(Parser: PARSER): SEXTENSION = struct -structure Extension = TypeExt.Extension; -structure Ast = Extension.XGram.Ast; -open Lexicon Extension Extension.XGram Ast; +structure Parser = Parser; +open Parser.Lexicon Parser.SynExt.Ast Parser.SynExt Parser; (** datatype sext **) @@ -214,6 +211,25 @@ | bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts; +(* explode atoms *) (* FIXME check, leading 0s (?) *) + +fun explode_tr (*"_explode"*) [consC, nilC, bit0, bit1, Free (str, _)] = + let + fun mk_list [] = nilC + | mk_list (t :: ts) = consC $ t $ mk_list ts; + + fun encode_bit 0 = bit0 + | encode_bit 1 = bit1 + | encode_bit _ = sys_error "encode_bit"; + + fun encode_char c = + mk_list (map encode_bit (radixpand (2, (ord c)))); + in + mk_list (map encode_char (explode str)) + end + | explode_tr (*"_explode"*) ts = raise_term "explode_tr" ts; + + (** print (ast) translations **) @@ -319,8 +335,31 @@ | dependent_tr' _ _ = raise Match; +(* implode atoms *) (* FIXME check *) -(** ext_of_sext **) +fun implode_ast_tr' (*"_implode"*) (asts as [Constant cons_name, nilC, + bit0, bit1, bitss]) = + let + fun fail () = raise_ast "implode_ast_tr'" asts; + + fun strip_list lst = + let val (xs, y) = unfold_ast_p cons_name lst + in if y = nilC then xs else fail () + end; + + fun decode_bit bit = + if bit = bit0 then "0" else if bit = bit1 then "1" else fail (); + + fun decode_char bits = + chr (#1 (scan_radixint (2, map decode_bit (strip_list bits)))); + in + Variable (implode (map decode_char (strip_list bitss))) + end + | implode_ast_tr' (*"_implode"*) asts = raise_ast "implode_ast_tr'" asts; + + + +(** syn_ext_of_sext **) fun strip_esc str = let @@ -335,7 +374,7 @@ fun infix_name sy = "op " ^ strip_esc sy; -fun ext_of_sext roots xconsts read_typ sext = +fun syn_ext_of_sext roots xconsts read_typ sext = let val {mixfix, parse_ast_translation, parse_translation, print_translation, print_ast_translation, ...} = sext_components sext; @@ -351,9 +390,9 @@ [Type ("idts", []), T2] ---> T3 | _ => error ("Illegal binder type " ^ quote ty)); - fun mk_infix sy T c p1 p2 p3 = - [Mfix ("op " ^ sy, T, c, [], max_pri), - Mfix ("(_ " ^ sy ^ "/ _)", T, c, [p1, p2], p3)]; + fun mk_infix sy ty c p1 p2 p3 = + [Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3), + Mfix ("op " ^ sy, ty, c, [], max_pri)]; fun mfix_of (Mixfix (sy, ty, c, ps, p)) = [Mfix (sy, read_typ ty, c, ps, p)] | mfix_of (Delimfix (sy, ty, c)) = [Mfix (sy, read_typ ty, c, [], max_pri)] @@ -371,15 +410,14 @@ val mfix = flat (map mfix_of mixfix); val binders = mapfilter binder mixfix; val bparses = map mk_binder_tr binders; - val bprints = map (mk_binder_tr' o (fn (x, y) => (y, x))) binders; + val bprints = map (mk_binder_tr' o swap) binders; in - Ext { - roots = roots, mfix = mfix, - extra_consts = distinct (filter is_xid xconsts), - parse_ast_translation = parse_ast_translation, - parse_translation = bparses @ parse_translation, - print_translation = bprints @ print_translation, - print_ast_translation = print_ast_translation} + syn_ext roots mfix (distinct (filter is_xid xconsts)) + (parse_ast_translation, + bparses @ parse_translation, + bprints @ print_translation, + print_ast_translation) + ([], []) end; @@ -400,6 +438,24 @@ +(** pt_to_ast **) + +fun pt_to_ast trf pt = + let + fun trans a args = + (case trf a of + None => mk_appl (Constant a) args + | Some f => f args handle exn + => (writeln ("Error in parse ast translation for " ^ quote a); raise exn)); + + fun ast_of (Node (a, pts)) = trans a (map ast_of pts) + | ast_of (Tip tok) = Variable (str_of_token tok); + in + ast_of pt + end; + + + (** ast_to_term **) fun ast_to_term trf ast = @@ -438,7 +494,7 @@ Mixfix ("_/ _", "[idt, idts] => idts", "_idts", [1, 0], 0), Delimfix ("_", "id => aprop", ""), Delimfix ("_", "var => aprop", ""), - Mixfix ("(1_/(1'(_')))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], 0), + Mixfix ("(1_/(1'(_')))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], max_pri), (* FIXME lhs pri: 0 vs. max_pri *) Delimfix ("PROP _", "aprop => prop", "_aprop"), Delimfix ("_", "prop => asms", ""), Delimfix ("_;/ _", "[prop, asms] => asms", "_asms"), @@ -448,18 +504,17 @@ Mixfix ("(_ ==>/ _)", "[prop, prop] => prop", "==>", [2, 1], 1), Binder ("!!", "('a::logic => prop) => prop", "all", 0, 0)], xrules = [], - parse_ast_translation = - [(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), - ("_bigimpl", bigimpl_ast_tr)], - parse_translation = [("_abs", abs_tr), ("_K", k_tr), ("_aprop", aprop_tr)], + parse_ast_translation = [(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), + ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr)], + parse_translation = [("_abs", abs_tr), ("_aprop", aprop_tr), ("_K", k_tr), + ("_explode", explode_tr)], print_translation = [], print_ast_translation = [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), - ("==>", impl_ast_tr')]}; + ("==>", impl_ast_tr'), ("_implode", implode_ast_tr')]}; -val syntax_types = [id, var, tfree, tvar, logic, "type", "types", "sort", - "classes", args, "idt", "idts", "aprop", "asms"]; +val syntax_types = terminals @ [logic, "type", "types", "sort", "classes", + args, "idt", "idts", "aprop", "asms"]; -val constrainIdtC = "_idtyp"; val constrainAbsC = "_constrainAbs"; val apropC = "_aprop";