diff -r 000000000000 -r a5a9c433f639 src/Pure/Thy/syntax.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/syntax.ML Thu Sep 16 12:20:38 1993 +0200 @@ -0,0 +1,359 @@ +(* Title: Pure/Thy/syntax + ID: $Id$ + Author: Sonia Mahjoub and Tobias Nipkow and Markus Wenzel + Copyright 1992 TU Muenchen + +Definition of theory syntax together with translation to ML code. +*) + +signature THYSYN = + sig + val read: string list -> string + end; + + + +functor ThySynFUN (Parse: PARSE): THYSYN = +struct + + +(*-------------- OBJECT TO STRING TRANSLATION ---------------*) + +fun string a = "\"" ^ a ^ "\""; + +fun parent s = "(" ^ s ^ ")"; + +fun pair(a,b) = parent(a ^ ", " ^ b); + +fun pair_string(a,b) = pair(string a,string b); + +fun pair_string2(a,b) = pair(a,string b); + +fun bracket s = "[" ^ s ^ "]"; + +val comma = space_implode ", "; + +val bracket_comma = bracket o comma; + +val big_bracket_comma = bracket o space_implode ",\n"; + +fun big_bracket_comma_ind ind strs = bracket (space_implode (",\n" ^ ind) strs); + +val bracket_comma_string = bracket_comma o (map string); + + +(*------------------- ABSTRACT SYNTAX FUNCTIONS ---------------------*) + +datatype mixfix = Mixfix of string * string * string + | Delimfix of string + | Infixl of string + | Infixr of string + | Binder of string * string + | TInfixl of string + | TInfixr of string; + + +datatype pfix_or_mfix = Pref of string | Mixf of string; + +fun pm_proj(Pref s) = s + | pm_proj(Mixf s) = s; + +fun split_decls 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); + +fun mixfix (sy,c,ty,l,n) = "Mixfix(" ^ comma[string sy, c, ty, l, 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 delimfix (sy,c,ty) = "Delimfix(" ^ comma[string 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 + 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) + | 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_type_decl((ts, n), None) = [Pref(pair(bracket_comma_string ts, n))] + | mk_type_decl((t::ts, n), Some(tinfix)) = + [Pref(pair(bracket(string t), n)), Mixf(mk_mfix((t,n), tinfix))] @ + mk_type_decl((ts, n), Some(tinfix)) + | mk_type_decl(([], n), Some(tinfix)) = []; + + +fun mk_extension (((((((cl, def), (ty, tinfix)), ar), (co, mfix)), tr), ax), ml) = + ((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 mk_rules ps = + let + val axs = big_bracket_comma_ind " " (map pair_string ps); + val vals = foldr add_val (ps, "") + in + axs ^ "\n\nval ax = get_axiom thy\n\n" ^ vals + end; + +fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend\n"; + + +fun mk_sext mfix trans = + "Some (NewSext {\n\ +\ 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 = + "Some (Syntax.simple_sext\n " ^ mfix ^ ")"; + +fun mk_ext ((cl, def, ty, ar, co, ax), sext) = + " (" ^ 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); + +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"; + +val postamble = "\n(**** end of user section ****)\n"; + +fun mk_structure ((name, base), Some (ext, tinfix, mfix, trans, ml)) = + let + val noext = ("[]", "[]", "[]", "[]", "[]", "[]"); + val basethy = + if tinfix = "[]" then base + else mk_ext_thy (base, name ^ "(type infix)", noext, mk_simple_sext tinfix); + val sext = + if mfix = "[]" andalso trans = "[]" andalso ml = "" then "None" + else mk_sext mfix trans; + val thy = "\nval thy = " ^ mk_ext_thy (basethy, name, ext, sext); + in + mk_struct (name, preamble ^ ml ^ postamble ^ thy ^ "\nend") + end + | mk_structure ((name, base), None) = mk_struct (name, "\nval thy = " ^ base); + + +fun merge (t :: ts) = + foldl (fn (base, thy) => "(merge_theories (" ^ base ^ ", " ^ thy ^ ".thy))") + (t ^ ".thy", ts) + | merge [] = raise Match; + + + +(*------------------------ PARSERS -------------------------*) + + +open Parse + +(*------------------- VARIOUS PARSERS ----------------------*) + +val emptyl = empty >> K"[]"; + +val ids = list_of1 id >> bracket_comma_string; +(* -> "[id1, id2, ..., idn]" *) + +val stgorids = list_of1 (stg || id); + +val sort = id >> (bracket o string) + || "{" $$-- (ids || emptyl) --$$ "}"; +(* -> "[id]" + -> "[id1, ...,idn]" *) + +val infxl = "infixl" $$-- !! nat +and infxr = "infixr" $$-- !! nat + + +(*------------------- CLASSES PARSER ----------------------*) + + + + +val class = (id >> string) -- ( "<" $$-- (!! ids) || emptyl) >> pair; + +(* -> "(id, [id1, ..., idn])" + || + -> "(id, [])" *) + + +val classes = "classes" $$-- !!(repeat1 class) >> bracket_comma + || emptyl; + + +(* "[(id, [..]), ...,(id, [...])]" *) + + + +(*------------------- DEFAULT PARSER ---------------------*) + + +val default = "default" $$-- !!sort + || emptyl; + +(* -> "[]" + -> "[id]" + -> "[id1, ...,idn]" *) + + +(*-------------------- TYPES PARSER ----------------------*) + + +val type_decl = stgorids -- nat; + +val tyinfix = infxl >> (Some o TInfixl) + || infxr >> (Some o TInfixr); + +val type_infix = "(" $$-- !! (tyinfix --$$ ")") + || empty >> K None; + +val types = "types" $$-- + !! (repeat1 (type_decl -- type_infix >> mk_type_decl)) + >> (split_decls o flat) + || empty >> (K ("[]", [])); + + (* ==> ("[(id, nat), ... ]", [strg, ...]) *) + + + +(*-------------------- ARITIES PARSER ----------------------*) + + +val sorts = list_of sort >> bracket_comma; + +(* -> "[[id1, ...], ..., [id, ...]]" *) + + +val arity = id >> (fn s => pair("[]",string s)) + || "(" $$-- sorts --$$")" -- id >> (fn (l,s) => pair(l,string s)); + +(* -> "([],id)" + -> "([[id,..], ...,[id,..]], id)" *) + +val tys = stgorids >> bracket_comma_string; + +val arities = "arities" $$-- !! (repeat1 (tys --$$ "::" -- arity >> pair)) + >> bracket_comma + || emptyl; + +(* -> "[([id,..], ([[id,...],...], id))]" *) + + +(*--------------------- CONSTS PARSER ---------------------*) + +val natlist = "[" $$-- !!(list_of nat --$$ "]") >> bracket_comma + || empty >> K"[]"; + + + (* "[nat, ...]" || "[]" *) + + +val prio_opt = natlist -- nat >> Some + || empty >> K None; + +val mfix = stg -- !! prio_opt >> delim_mix + || infxl >> Infixl + || infxr >> Infixr + || "binder" $$-- !!(stg -- nat) >> Binder + +val const_decl = stgorids -- !! ("::" $$-- stg); + +(*("[exid, ...]", stg) *) + + +val mixfix = "(" $$-- !! (mfix --$$ ")") >> Some + || empty >> K None; + +(* (s, e, l, n) *) + + +val consts = "consts" $$-- + !! (repeat1 (const_decl -- mixfix >> mk_mixfix)) + >> (split_decls o flat) + || empty >> K ("[]",[]); + +(* ("[([exid, ...], stg), ....]", [strg, ..]) *) + + +(*---------------- TRANSLATIONS PARSER --------------------*) + +val xpat = "(" $$-- id --$$ ")" -- stg >> pair_string + || stg >> (fn s => pair_string ("logic", s)); + +val arrow = $$ "=>" >> K " |-> " + || $$ "<=" >> K " <-| " + || $$ "==" >> K " <-> "; + +val xrule = xpat -- !! (arrow -- xpat) >> (fn (xp1, (a, xp2)) => xp1 ^ a ^ xp2); + +val translations = "translations" $$-- !! (repeat1 xrule) + || empty; + + +(*------------------- RULES PARSER -----------------------*) + +val rules = "rules" $$-- !! (repeat1 (id -- !! stg) >> mk_rules) + || emptyl; + +(* "[(id, stg), ...]" *) + + + +(*----------------------- ML_TEXT -------------------------*) + +val mltxt = txt || empty >> K""; + + +(*---------------------------------------------------------*) + +val extension = "+" $$-- !! (classes -- default -- types -- arities + -- consts -- translations -- rules --$$ "end" -- mltxt) + >> (Some o mk_extension) + || empty >> K None; + + +val bases = id -- repeat("+" $$-- id) >> op:: ; + +val theoryDef = !!(id --$$ "=" -- (bases >> merge) -- extension) + >> mk_structure; + +val read = reader theoryDef + +end; +