# HG changeset patch # User wenzelm # Date 749745482 -3600 # Node ID e6fb60365db903fbad95a92e97d81ba2d18db852 # Parent 929ad32d63fcb337eac387386eb27fadf76f71b6 Pure/Thy/syntax.ML removed {parse,print}_{pre,post}_proc; removed 'val ax = ..'; diff -r 929ad32d63fc -r e6fb60365db9 src/Pure/Thy/syntax.ML --- a/src/Pure/Thy/syntax.ML Mon Oct 04 15:36:31 1993 +0100 +++ b/src/Pure/Thy/syntax.ML Mon Oct 04 15:38:02 1993 +0100 @@ -1,7 +1,6 @@ -(* Title: Pure/Thy/syntax +(* Title: Pure/Thy/syntax.ML ID: $Id$ - Author: Sonia Mahjoub and Tobias Nipkow and Markus Wenzel - Copyright 1992 TU Muenchen + Author: Sonia Mahjoub and Tobias Nipkow and Markus Wenzel, TU Muenchen Definition of theory syntax together with translation to ML code. *) @@ -19,15 +18,13 @@ (*-------------- OBJECT TO STRING TRANSLATION ---------------*) -fun string a = "\"" ^ a ^ "\""; - fun parent s = "(" ^ s ^ ")"; -fun pair(a,b) = parent(a ^ ", " ^ b); +fun pair(a, b) = parent(a ^ ", " ^ b); -fun pair_string(a,b) = pair(string a,string b); +fun pair_quote(a, b) = pair(quote a, quote b); -fun pair_string2(a,b) = pair(a,string b); +fun pair_quote2(a, b) = pair(a, quote b); fun bracket s = "[" ^ s ^ "]"; @@ -39,7 +36,7 @@ fun big_bracket_comma_ind ind strs = bracket (space_implode (",\n" ^ ind) strs); -val bracket_comma_string = bracket_comma o (map string); +val bracket_comma_quote = bracket_comma o (map quote); (*------------------- ABSTRACT SYNTAX FUNCTIONS ---------------------*) @@ -59,44 +56,44 @@ | pm_proj(Mixf s) = s; fun split_decls l = - let val (p,m) = partition (fn Pref _ => true | _ => false) l; + let val (p, m) = partition (fn Pref _ => true | _ => false) l; in (big_bracket_comma_ind " " (map pm_proj p), map pm_proj m) end; fun delim_mix (s, None) = Delimfix(s) - | delim_mix (s, Some(l,n)) = Mixfix(s,l,n); + | delim_mix (s, Some(l, n)) = Mixfix(s, l, n); -fun mixfix (sy,c,ty,l,n) = "Mixfix(" ^ comma[string sy, c, ty, l, n] ^ ")"; +fun mixfix (sy, c, ty, l, n) = "Mixfix(" ^ comma[quote sy, c, ty, l, n] ^ ")"; -fun infixrl(ty,c,n) = parent(comma[ty,c,n]); +fun infixrl(ty, c, n) = parent(comma[ty, c, n]); -fun binder(sy, c, ty, n) = "Binder(" ^ comma[string sy, c, ty, "0", n] ^ ")"; +fun binder(sy, c, ty, n) = "Binder(" ^ comma[quote sy, c, ty, "0", n] ^ ")"; -fun delimfix (sy,c,ty) = "Delimfix(" ^ comma[string sy, c, ty] ^ ")"; +fun delimfix (sy, c, ty) = "Delimfix(" ^ comma[quote sy, c, ty] ^ ")"; fun tinfixrl (ty, n) = "(" ^ comma[ty, ty, n] ^ ")"; -fun mk_mfix((c,ty),mfix) = - let val cs = string c and tys = string ty +fun mk_mfix((c, ty), mfix) = + let val cs = quote c and tys = quote ty in case mfix of Mixfix(sy, l, n) => mixfix (sy, tys, cs, l, n) | Infixr(n) => "Infixr" ^ infixrl(cs, tys, n) | Infixl(n) => "Infixl" ^ infixrl(cs, tys, n) - | Binder(sy,n) => binder(sy,tys,cs,n) + | Binder(sy, n) => binder(sy, tys, cs, n) | TInfixl(n) => "TInfixl" ^ tinfixrl(cs, n) | TInfixr(n) => "TInfixr" ^ tinfixrl(cs, n) | Delimfix(sy) => delimfix(sy, tys, cs) end; -fun mk_mixfix((cs,ty), None) = - [Pref(pair(bracket_comma_string cs, string ty))] - | mk_mixfix((c::cs,ty), Some(mfix)) = - Mixf(mk_mfix((c,ty),mfix)) :: mk_mixfix((cs,ty), Some(mfix)) - | mk_mixfix(([],_),_) = []; +fun mk_mixfix((cs, ty), None) = + [Pref(pair(bracket_comma_quote cs, quote ty))] + | mk_mixfix((c::cs, ty), Some(mfix)) = + Mixf(mk_mfix((c, ty), mfix)) :: mk_mixfix((cs, ty), Some(mfix)) + | mk_mixfix(([], _), _) = []; -fun mk_type_decl((ts, n), None) = [Pref(pair(bracket_comma_string ts, n))] +fun mk_type_decl((ts, n), None) = [Pref(pair(bracket_comma_quote ts, n))] | mk_type_decl((t::ts, n), Some(tinfix)) = - [Pref(pair(bracket(string t), n)), Mixf(mk_mfix((t,n), tinfix))] @ + [Pref(pair(bracket(quote t), n)), Mixf(mk_mfix((t, n), tinfix))] @ mk_type_decl((ts, n), Some(tinfix)) | mk_type_decl(([], n), Some(tinfix)) = []; @@ -105,14 +102,14 @@ ((cl, def, ty, ar, co, ax), big_bracket_comma_ind " " tinfix, big_bracket_comma_ind " " mfix, big_bracket_comma_ind " " tr, ml); -fun add_val((id,_),s) = "val " ^ id ^ " = ax " ^ string id ^ "\n" ^ s; +fun add_val((id, _), s) = "val " ^ id ^ " = get_axiom thy " ^ quote id ^ "\n" ^ s; fun mk_rules ps = let - val axs = big_bracket_comma_ind " " (map pair_string ps); + val axs = big_bracket_comma_ind " " (map pair_quote ps); val vals = foldr add_val (ps, "") in - axs ^ "\n\nval ax = get_axiom thy\n\n" ^ vals + axs ^ "\n\n" ^ vals end; fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend\n"; @@ -123,12 +120,8 @@ \ mixfix =\n " ^ mfix ^ ",\n\ \ xrules =\n " ^ trans ^ ",\n\ \ parse_ast_translation = parse_ast_translation,\n\ -\ parse_preproc = parse_preproc,\n\ -\ parse_postproc = parse_postproc,\n\ \ parse_translation = parse_translation,\n\ \ print_translation = print_translation,\n\ -\ print_preproc = print_preproc,\n\ -\ print_postproc = print_postproc,\n\ \ print_ast_translation = print_ast_translation})"; fun mk_simple_sext mfix = @@ -138,17 +131,13 @@ " (" ^ space_implode ",\n " [cl, def, ty, ar, co, sext] ^ ")\n " ^ ax ^ "\n"; fun mk_ext_thy (base, name, ext, sext) = - "extend_theory (" ^ base ^ ")\n " ^ string name ^ "\n" ^ mk_ext (ext, sext); + "extend_theory (" ^ base ^ ")\n " ^ quote name ^ "\n" ^ mk_ext (ext, sext); val preamble = "\nlocal\n\ \ val parse_ast_translation = []\n\ - \ val parse_preproc = None\n\ - \ val parse_postproc = None\n\ \ val parse_translation = []\n\ \ val print_translation = []\n\ - \ val print_preproc = None\n\ - \ val print_postproc = None\n\ \ val print_ast_translation = []\n\ \in\n\n\ \(**** begin of user section ****)\n"; @@ -185,17 +174,17 @@ (*------------------- VARIOUS PARSERS ----------------------*) -val emptyl = empty >> K"[]"; +val emptyl = empty >> K "[]"; -val ids = list_of1 id >> bracket_comma_string; +val ids = list_of1 id >> bracket_comma_quote; (* -> "[id1, id2, ..., idn]" *) val stgorids = list_of1 (stg || id); -val sort = id >> (bracket o string) +val sort = id >> (bracket o quote) || "{" $$-- (ids || emptyl) --$$ "}"; (* -> "[id]" - -> "[id1, ...,idn]" *) + -> "[id1, ..., idn]" *) val infxl = "infixl" $$-- !! nat and infxr = "infixr" $$-- !! nat @@ -206,7 +195,7 @@ -val class = (id >> string) -- ( "<" $$-- (!! ids) || emptyl) >> pair; +val class = (id >> quote) -- ( "<" $$-- (!! ids) || emptyl) >> pair; (* -> "(id, [id1, ..., idn])" || @@ -217,7 +206,7 @@ || emptyl; -(* "[(id, [..]), ...,(id, [...])]" *) +(* "[(id, [..]), ..., (id, [...])]" *) @@ -229,7 +218,7 @@ (* -> "[]" -> "[id]" - -> "[id1, ...,idn]" *) + -> "[id1, ..., idn]" *) (*-------------------- TYPES PARSER ----------------------*) @@ -260,25 +249,25 @@ (* -> "[[id1, ...], ..., [id, ...]]" *) -val arity = id >> (fn s => pair("[]",string s)) - || "(" $$-- sorts --$$")" -- id >> (fn (l,s) => pair(l,string s)); +val arity = id >> (fn s => pair("[]", quote s)) + || "(" $$-- sorts --$$")" -- id >> (fn (l, s) => pair(l, quote s)); -(* -> "([],id)" - -> "([[id,..], ...,[id,..]], id)" *) +(* -> "([], id)" + -> "([[id, ..], ..., [id, ..]], id)" *) -val tys = stgorids >> bracket_comma_string; +val tys = stgorids >> bracket_comma_quote; val arities = "arities" $$-- !! (repeat1 (tys --$$ "::" -- arity >> pair)) >> bracket_comma || emptyl; -(* -> "[([id,..], ([[id,...],...], id))]" *) +(* -> "[([id, ..], ([[id, ...], ...], id))]" *) (*--------------------- CONSTS PARSER ---------------------*) val natlist = "[" $$-- !!(list_of nat --$$ "]") >> bracket_comma - || empty >> K"[]"; + || empty >> K "[]"; (* "[nat, ...]" || "[]" *) @@ -306,15 +295,15 @@ val consts = "consts" $$-- !! (repeat1 (const_decl -- mixfix >> mk_mixfix)) >> (split_decls o flat) - || empty >> K ("[]",[]); + || empty >> K ("[]", []); (* ("[([exid, ...], stg), ....]", [strg, ..]) *) (*---------------- TRANSLATIONS PARSER --------------------*) -val xpat = "(" $$-- id --$$ ")" -- stg >> pair_string - || stg >> (fn s => pair_string ("logic", s)); +val xpat = "(" $$-- id --$$ ")" -- stg >> pair_quote + || stg >> (fn s => pair_quote ("logic", s)); val arrow = $$ "=>" >> K " |-> " || $$ "<=" >> K " <-| " @@ -337,7 +326,7 @@ (*----------------------- ML_TEXT -------------------------*) -val mltxt = txt || empty >> K""; +val mltxt = txt || empty >> K ""; (*---------------------------------------------------------*)