0

1 
(* Title: Pure/Thy/syntax


2 
ID: $Id$


3 
Author: Sonia Mahjoub and Tobias Nipkow and Markus Wenzel


4 
Copyright 1992 TU Muenchen


5 


6 
Definition of theory syntax together with translation to ML code.


7 
*)


8 


9 
signature THYSYN =


10 
sig


11 
val read: string list > string


12 
end;


13 


14 


15 


16 
functor ThySynFUN (Parse: PARSE): THYSYN =


17 
struct


18 


19 


20 
(* OBJECT TO STRING TRANSLATION *)


21 


22 
fun string a = "\"" ^ a ^ "\"";


23 


24 
fun parent s = "(" ^ s ^ ")";


25 


26 
fun pair(a,b) = parent(a ^ ", " ^ b);


27 


28 
fun pair_string(a,b) = pair(string a,string b);


29 


30 
fun pair_string2(a,b) = pair(a,string b);


31 


32 
fun bracket s = "[" ^ s ^ "]";


33 


34 
val comma = space_implode ", ";


35 


36 
val bracket_comma = bracket o comma;


37 


38 
val big_bracket_comma = bracket o space_implode ",\n";


39 


40 
fun big_bracket_comma_ind ind strs = bracket (space_implode (",\n" ^ ind) strs);


41 


42 
val bracket_comma_string = bracket_comma o (map string);


43 


44 


45 
(* ABSTRACT SYNTAX FUNCTIONS *)


46 


47 
datatype mixfix = Mixfix of string * string * string


48 
 Delimfix of string


49 
 Infixl of string


50 
 Infixr of string


51 
 Binder of string * string


52 
 TInfixl of string


53 
 TInfixr of string;


54 


55 


56 
datatype pfix_or_mfix = Pref of string  Mixf of string;


57 


58 
fun pm_proj(Pref s) = s


59 
 pm_proj(Mixf s) = s;


60 


61 
fun split_decls l =


62 
let val (p,m) = partition (fn Pref _ => true  _ => false) l;


63 
in (big_bracket_comma_ind " " (map pm_proj p), map pm_proj m) end;


64 


65 
fun delim_mix (s, None) = Delimfix(s)


66 
 delim_mix (s, Some(l,n)) = Mixfix(s,l,n);


67 


68 
fun mixfix (sy,c,ty,l,n) = "Mixfix(" ^ comma[string sy, c, ty, l, n] ^ ")";


69 


70 
fun infixrl(ty,c,n) = parent(comma[ty,c,n]);


71 


72 
fun binder(sy, c, ty, n) = "Binder(" ^ comma[string sy, c, ty, "0", n] ^ ")";


73 


74 
fun delimfix (sy,c,ty) = "Delimfix(" ^ comma[string sy, c, ty] ^ ")";


75 


76 
fun tinfixrl (ty, n) = "(" ^ comma[ty, ty, n] ^ ")";


77 


78 
fun mk_mfix((c,ty),mfix) =


79 
let val cs = string c and tys = string ty


80 
in case mfix of


81 
Mixfix(sy, l, n) => mixfix (sy, tys, cs, l, n)


82 
 Infixr(n) => "Infixr" ^ infixrl(cs, tys, n)


83 
 Infixl(n) => "Infixl" ^ infixrl(cs, tys, n)


84 
 Binder(sy,n) => binder(sy,tys,cs,n)


85 
 TInfixl(n) => "TInfixl" ^ tinfixrl(cs, n)


86 
 TInfixr(n) => "TInfixr" ^ tinfixrl(cs, n)


87 
 Delimfix(sy) => delimfix(sy, tys, cs)


88 
end;


89 


90 


91 
fun mk_mixfix((cs,ty), None) =


92 
[Pref(pair(bracket_comma_string cs, string ty))]


93 
 mk_mixfix((c::cs,ty), Some(mfix)) =


94 
Mixf(mk_mfix((c,ty),mfix)) :: mk_mixfix((cs,ty), Some(mfix))


95 
 mk_mixfix(([],_),_) = [];


96 


97 
fun mk_type_decl((ts, n), None) = [Pref(pair(bracket_comma_string ts, n))]


98 
 mk_type_decl((t::ts, n), Some(tinfix)) =


99 
[Pref(pair(bracket(string t), n)), Mixf(mk_mfix((t,n), tinfix))] @


100 
mk_type_decl((ts, n), Some(tinfix))


101 
 mk_type_decl(([], n), Some(tinfix)) = [];


102 


103 


104 
fun mk_extension (((((((cl, def), (ty, tinfix)), ar), (co, mfix)), tr), ax), ml) =


105 
((cl, def, ty, ar, co, ax), big_bracket_comma_ind " " tinfix,


106 
big_bracket_comma_ind " " mfix, big_bracket_comma_ind " " tr, ml);


107 


108 
fun add_val((id,_),s) = "val " ^ id ^ " = ax " ^ string id ^ "\n" ^ s;


109 


110 
fun mk_rules ps =


111 
let


112 
val axs = big_bracket_comma_ind " " (map pair_string ps);


113 
val vals = foldr add_val (ps, "")


114 
in


115 
axs ^ "\n\nval ax = get_axiom thy\n\n" ^ vals


116 
end;


117 


118 
fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend\n";


119 


120 


121 
fun mk_sext mfix trans =


122 
"Some (NewSext {\n\


123 
\ mixfix =\n " ^ mfix ^ ",\n\


124 
\ xrules =\n " ^ trans ^ ",\n\


125 
\ parse_ast_translation = parse_ast_translation,\n\


126 
\ parse_preproc = parse_preproc,\n\


127 
\ parse_postproc = parse_postproc,\n\


128 
\ parse_translation = parse_translation,\n\


129 
\ print_translation = print_translation,\n\


130 
\ print_preproc = print_preproc,\n\


131 
\ print_postproc = print_postproc,\n\


132 
\ print_ast_translation = print_ast_translation})";


133 


134 
fun mk_simple_sext mfix =


135 
"Some (Syntax.simple_sext\n " ^ mfix ^ ")";


136 


137 
fun mk_ext ((cl, def, ty, ar, co, ax), sext) =


138 
" (" ^ space_implode ",\n " [cl, def, ty, ar, co, sext] ^ ")\n " ^ ax ^ "\n";


139 


140 
fun mk_ext_thy (base, name, ext, sext) =


141 
"extend_theory (" ^ base ^ ")\n " ^ string name ^ "\n" ^ mk_ext (ext, sext);


142 


143 
val preamble =


144 
"\nlocal\n\


145 
\ val parse_ast_translation = []\n\


146 
\ val parse_preproc = None\n\


147 
\ val parse_postproc = None\n\


148 
\ val parse_translation = []\n\


149 
\ val print_translation = []\n\


150 
\ val print_preproc = None\n\


151 
\ val print_postproc = None\n\


152 
\ val print_ast_translation = []\n\


153 
\in\n\n\


154 
\(**** begin of user section ****)\n";


155 


156 
val postamble = "\n(**** end of user section ****)\n";


157 


158 
fun mk_structure ((name, base), Some (ext, tinfix, mfix, trans, ml)) =


159 
let


160 
val noext = ("[]", "[]", "[]", "[]", "[]", "[]");


161 
val basethy =


162 
if tinfix = "[]" then base


163 
else mk_ext_thy (base, name ^ "(type infix)", noext, mk_simple_sext tinfix);


164 
val sext =


165 
if mfix = "[]" andalso trans = "[]" andalso ml = "" then "None"


166 
else mk_sext mfix trans;


167 
val thy = "\nval thy = " ^ mk_ext_thy (basethy, name, ext, sext);


168 
in


169 
mk_struct (name, preamble ^ ml ^ postamble ^ thy ^ "\nend")


170 
end


171 
 mk_structure ((name, base), None) = mk_struct (name, "\nval thy = " ^ base);


172 


173 


174 
fun merge (t :: ts) =


175 
foldl (fn (base, thy) => "(merge_theories (" ^ base ^ ", " ^ thy ^ ".thy))")


176 
(t ^ ".thy", ts)


177 
 merge [] = raise Match;


178 


179 


180 


181 
(* PARSERS *)


182 


183 


184 
open Parse


185 


186 
(* VARIOUS PARSERS *)


187 


188 
val emptyl = empty >> K"[]";


189 


190 
val ids = list_of1 id >> bracket_comma_string;


191 
(* > "[id1, id2, ..., idn]" *)


192 


193 
val stgorids = list_of1 (stg  id);


194 


195 
val sort = id >> (bracket o string)


196 
 "{" $$ (ids  emptyl) $$ "}";


197 
(* > "[id]"


198 
> "[id1, ...,idn]" *)


199 


200 
val infxl = "infixl" $$ !! nat


201 
and infxr = "infixr" $$ !! nat


202 


203 


204 
(* CLASSES PARSER *)


205 


206 


207 


208 


209 
val class = (id >> string)  ( "<" $$ (!! ids)  emptyl) >> pair;


210 


211 
(* > "(id, [id1, ..., idn])"


212 



213 
> "(id, [])" *)


214 


215 


216 
val classes = "classes" $$ !!(repeat1 class) >> bracket_comma


217 
 emptyl;


218 


219 


220 
(* "[(id, [..]), ...,(id, [...])]" *)


221 


222 


223 


224 
(* DEFAULT PARSER *)


225 


226 


227 
val default = "default" $$ !!sort


228 
 emptyl;


229 


230 
(* > "[]"


231 
> "[id]"


232 
> "[id1, ...,idn]" *)


233 


234 


235 
(* TYPES PARSER *)


236 


237 


238 
val type_decl = stgorids  nat;


239 


240 
val tyinfix = infxl >> (Some o TInfixl)


241 
 infxr >> (Some o TInfixr);


242 


243 
val type_infix = "(" $$ !! (tyinfix $$ ")")


244 
 empty >> K None;


245 


246 
val types = "types" $$


247 
!! (repeat1 (type_decl  type_infix >> mk_type_decl))


248 
>> (split_decls o flat)


249 
 empty >> (K ("[]", []));


250 


251 
(* ==> ("[(id, nat), ... ]", [strg, ...]) *)


252 


253 


254 


255 
(* ARITIES PARSER *)


256 


257 


258 
val sorts = list_of sort >> bracket_comma;


259 


260 
(* > "[[id1, ...], ..., [id, ...]]" *)


261 


262 


263 
val arity = id >> (fn s => pair("[]",string s))


264 
 "(" $$ sorts $$")"  id >> (fn (l,s) => pair(l,string s));


265 


266 
(* > "([],id)"


267 
> "([[id,..], ...,[id,..]], id)" *)


268 


269 
val tys = stgorids >> bracket_comma_string;


270 


271 
val arities = "arities" $$ !! (repeat1 (tys $$ "::"  arity >> pair))


272 
>> bracket_comma


273 
 emptyl;


274 


275 
(* > "[([id,..], ([[id,...],...], id))]" *)


276 


277 


278 
(* CONSTS PARSER *)


279 


280 
val natlist = "[" $$ !!(list_of nat $$ "]") >> bracket_comma


281 
 empty >> K"[]";


282 


283 


284 
(* "[nat, ...]"  "[]" *)


285 


286 


287 
val prio_opt = natlist  nat >> Some


288 
 empty >> K None;


289 


290 
val mfix = stg  !! prio_opt >> delim_mix


291 
 infxl >> Infixl


292 
 infxr >> Infixr


293 
 "binder" $$ !!(stg  nat) >> Binder


294 


295 
val const_decl = stgorids  !! ("::" $$ stg);


296 


297 
(*("[exid, ...]", stg) *)


298 


299 


300 
val mixfix = "(" $$ !! (mfix $$ ")") >> Some


301 
 empty >> K None;


302 


303 
(* (s, e, l, n) *)


304 


305 


306 
val consts = "consts" $$


307 
!! (repeat1 (const_decl  mixfix >> mk_mixfix))


308 
>> (split_decls o flat)


309 
 empty >> K ("[]",[]);


310 


311 
(* ("[([exid, ...], stg), ....]", [strg, ..]) *)


312 


313 


314 
(* TRANSLATIONS PARSER *)


315 


316 
val xpat = "(" $$ id $$ ")"  stg >> pair_string


317 
 stg >> (fn s => pair_string ("logic", s));


318 


319 
val arrow = $$ "=>" >> K " > "


320 
 $$ "<=" >> K " < "


321 
 $$ "==" >> K " <> ";


322 


323 
val xrule = xpat  !! (arrow  xpat) >> (fn (xp1, (a, xp2)) => xp1 ^ a ^ xp2);


324 


325 
val translations = "translations" $$ !! (repeat1 xrule)


326 
 empty;


327 


328 


329 
(* RULES PARSER *)


330 


331 
val rules = "rules" $$ !! (repeat1 (id  !! stg) >> mk_rules)


332 
 emptyl;


333 


334 
(* "[(id, stg), ...]" *)


335 


336 


337 


338 
(* ML_TEXT *)


339 


340 
val mltxt = txt  empty >> K"";


341 


342 


343 
(**)


344 


345 
val extension = "+" $$ !! (classes  default  types  arities


346 
 consts  translations  rules $$ "end"  mltxt)


347 
>> (Some o mk_extension)


348 
 empty >> K None;


349 


350 


351 
val bases = id  repeat("+" $$ id) >> op:: ;


352 


353 
val theoryDef = !!(id $$ "="  (bases >> merge)  extension)


354 
>> mk_structure;


355 


356 
val read = reader theoryDef


357 


358 
end;


359 
