1(* ===================================================================== *) 2(* FILE : hhWriter.sml *) 3(* DESCRIPTION : Print objects (constants, types and theorems) and *) 4(* dependencies theorems for *) 5(* export to the holyHammer framework. *) 6(* AUTHOR : (c) Thibault Gauthier, University of Innsbruck *) 7(* DATE : 2015 *) 8(* ===================================================================== *) 9 10 11structure hhWriter :> hhWriter = 12struct 13 14open HolKernel boolLib tttTools TextIO Tag Dep 15 16val ERR = mk_HOL_ERR "hhWriter" 17 18(*---------------------------------------------------------------------------- 19 Dictionaries 20 -----------------------------------------------------------------------------*) 21 22(* reserved names *) 23val hollight_theorems = ["HL_TRUTH", "HL_FALSITY", "HL_BOOL_CASES", "HL_EXT"]; 24val conjecture_name = "conjecture" 25val reserved_names = conjecture_name :: hollight_theorems 26val reserved_names0 = map (fn x => (x,0)) reserved_names 27 28(*---------------------------------------------------------------------------- 29 Escaping 30 -----------------------------------------------------------------------------*) 31 32fun is_tptp_sq_char c = 33 let val n = Char.ord c in 34 (40 <= n andalso n <= 176) andalso 35 (c <> #".") andalso 36 (c <> #"/") andalso 37 (c <> #":") andalso 38 (c <> #"|") andalso 39 (c <> #"\"") 40 end 41 42fun hh_escape s = 43 let fun image c = 44 if is_tptp_sq_char c 45 then Char.toString c 46 else "|" ^ (int_to_string (Char.ord c)) ^ "|" 47 in 48 String.translate image s 49 end 50 51fun squotify name = "'" ^ name ^ "'" 52fun full_escape name = "'" ^ hh_escape name ^ "'" 53 54(*---------------------------------------------------------------------------- 55 Renaming 56 -----------------------------------------------------------------------------*) 57 58(* only used for variables *) 59fun variant_name_dict s used = 60 let 61 val i = dfind s used 62 fun new_name s i = 63 let val si = s ^ Int.toString i in 64 if dmem si used 65 then new_name s (i + 1) 66 else (full_escape si, dadd s (i + 1) (dadd si 0 used)) 67 end 68 in 69 new_name s i 70 end 71 handle NotFound => (full_escape s, dadd s 0 used) 72 73fun store_name state name = 74 let val dict = #used_names state in 75 if dmem name (!dict) then () else dict := dadd name 0 (!dict) 76 end 77 78(* types *) 79fun declare_perm_type state {Thy,Name} = 80 let 81 val name1 = "type." ^ Thy ^ "." ^ (hh_escape Name) 82 val name2 = squotify name1 83 val dict = #ty_names state 84 in 85 store_name state name1; (* may be deprecated *) 86 dict := dadd {Thy=Thy,Name=Name} name2 (!dict); 87 name2 88 end 89 90(* constants *) 91fun declare_perm_const state {Thy,Name} = 92 let 93 val name1 = "const." ^ Thy ^ "." ^ (hh_escape Name) 94 val name2 = squotify name1 95 val dict = #const_names state 96 in 97 store_name state name1; 98 dict := dadd {Thy=Thy,Name=Name} name2 (!dict); 99 name2 100 end 101 102(* theorems *) 103fun declare_perm_thm state (thy,n) name = 104 let 105 val name1 = "thm." ^ thy ^ "." ^ (hh_escape name) 106 val name2 = squotify name1 107 val dict = #thm_names state 108 in 109 store_name state name1; 110 dict := dadd (thy,n) name2 (!dict); 111 name2 112 end 113 114(* special constants *) 115fun declare_fixed state dict {Thy,Name} name = 116 ( 117 store_name state name; 118 dict := dadd {Thy=Thy,Name=Name} name (!dict); 119 name 120 ) 121 122(* temporary variables and type variables *) 123fun declare_temp_list state get_name dict l = 124 let 125 val olddict = !dict 126 val oldused = !(#used_names state) 127 fun fold_fun (s,sl) = 128 let 129 val useddict = #used_names state 130 val (news, newused) = variant_name_dict (get_name s) (!useddict) 131 in 132 dict := dadd s news (!dict); 133 useddict := newused; 134 news :: sl 135 end 136 val sl = foldl fold_fun [] l 137 fun undeclare () = 138 let val usedref = #used_names state in 139 dict := olddict; usedref := oldused 140 end 141 in 142 (List.rev sl, undeclare) 143 end 144 145(*--------------------------------------------------------------------------- 146 Streams. Objects and dependencies are written in different files. 147 ----------------------------------------------------------------------------*) 148 149fun os oc s = output (oc,s) 150fun oiter_aux oc sep f = 151 fn [] => () 152 | [e] => f e 153 | h :: t => (f h; output (oc,sep); oiter_aux oc sep f t) 154fun oiter_deps oc_deps sep f l = oiter_aux oc_deps sep f l 155fun oiter oc sep f l = oiter_aux oc sep f l 156 157(*--------------------------------------------------------------------------- 158 Printing objects (types, constants, theorems' conjuncts). 159 ----------------------------------------------------------------------------*) 160 161(* type *) 162fun oty state oc ty = 163 if is_vartype ty 164 then os oc (dfind_err "tyvar" ty (!(#tyvar_names state))) 165 else 166 let val {Args,Thy,Tyop} = dest_thy_type ty in 167 let val s = dfind {Thy=Thy,Name=Tyop} (!(#ty_names state)) in 168 if null Args then os oc s else 169 if (Thy ="min" andalso Tyop = "fun") 170 then (os oc "("; oty state oc (hd Args); os oc " > "; 171 oty state oc (hd (tl Args)); os oc ")") 172 else (os oc ("(" ^ s ^ " "); 173 oiter oc " " (oty state oc) Args; os oc ")") 174 end end 175 176type ('a,'b)substp = {redex : 'a, residue : 'b} 177val less_ty = fn a => (fn b => Type.compare (a,b) = LESS) 178fun less_red (a:(hol_type,'a)substp) (b:(hol_type,'b)substp) = 179 less_ty (#redex a) (#redex b) 180 181fun id_subst a = {redex = a, residue = a} 182fun full_match_type t1 t2 = 183 let 184 val (subst1,al) = raw_match_type t1 t2 ([],[]) 185 val subst2 = map id_subst al 186 in 187 sort less_red (subst1 @ subst2) 188 end 189 190(* term *) 191fun otm state oc tm = 192 if is_var tm then os oc (dfind_err "var" tm (!(#var_names state))) 193 else if is_const tm then 194 let 195 val {Thy, Name, Ty} = dest_thy_const tm 196 val mgty = type_of (prim_mk_const {Thy = Thy, Name = Name}) 197 val subst = full_match_type mgty Ty 198 val resl = map #residue subst 199 in 200 if null resl 201 then os oc (dfind {Thy=Thy,Name=Name} (!(#const_names state))) 202 else (os oc "("; 203 os oc (dfind {Thy=Thy,Name=Name} (!(#const_names state))); 204 os oc " "; 205 oiter oc " " (oty state oc) resl; 206 os oc ")") 207 end 208 else if is_eq tm then 209 (os oc "("; otm state oc (lhs tm); os oc " = "; otm state oc (rhs tm); os oc ")") 210 else if is_conj tm then 211 (os oc "("; otm state oc (lhand tm); os oc " & "; otm state oc (rand tm); os oc ")") 212 else if is_disj tm then 213 (os oc "("; otm state oc (lhand tm); os oc " | "; otm state oc (rand tm); os oc ")") 214 else if is_imp_only tm then 215 (os oc "("; otm state oc (lhand tm); os oc " => "; otm state oc (rand tm); os oc ")") 216 else if is_neg tm then (os oc "(~ "; otm state oc (rand tm); os oc ")") 217 else if is_forall tm then hh_binder state oc "!" (strip_forall tm) 218 else if is_exists tm then hh_binder state oc "?" (strip_exists tm) 219 else if is_abs tm then hh_binder state oc "^" (strip_abs tm) 220 else if is_comb tm then 221 let val (v,l) = strip_comb tm in 222 (os oc "("; otm state oc v; app (fn x => (os oc " "; otm state oc x)) l; os oc ")") 223 end 224 else raise ERR "otm" "" 225and hh_binder state oc s (l,tm) = 226 let 227 val (vl,undeclare) = 228 declare_temp_list state (fst o dest_var) (#var_names state) l 229 fun f x = 230 (os oc (dfind_err "var" x (!(#var_names state))); 231 os oc " : "; oty state oc (type_of x)) 232 in 233 os oc ("(" ^ s ^ "["); 234 oiter oc ", " f l; 235 os oc "]: "; otm state oc tm; os oc ")"; 236 undeclare () 237 end 238 239(* type definition *) 240fun hh_tydef state oc thy (s,arity) = 241 case (thy,s) of 242 ("min","bool") => 243 ignore (declare_fixed state (#ty_names state) {Thy=thy,Name=s} "$o") 244 | ("min","fun") => 245 ignore (declare_fixed state (#ty_names state) {Thy=thy,Name=s} "$fun") 246 | _ => 247 let val news = declare_perm_type state {Thy=thy,Name=s} in 248 os oc "tt("; os oc news; os oc ", ty, "; 249 let fun tyd i = case i of 250 0 => os oc "$t" 251 | n => (os oc "$t > "; tyd (n - 1)) 252 in 253 (tyd arity; os oc ").\n") 254 end 255 end 256 257fun quant_tyvarl oc l = 258 if null l then () 259 else (os oc "!["; oiter oc ", " (fn x => (os oc x; os oc " : $t")) l; os oc "]: ") 260 261(* constant definition *) 262fun hh_constdef state oc thy (s,ty) = 263 let 264 val fix = declare_fixed state (#const_names state) {Thy=thy,Name=s} 265 val news = case (thy,s) of 266 ("min","=") => fix "$equals" 267 | ("bool","!") => fix "$forall" 268 | ("bool","?") => fix "$exists" 269 | ("bool","/\\") => fix "$and" 270 | ("bool","\\/") => fix "$or" 271 | ("min","==>") => fix "$imply" 272 | ("bool","~") => fix "$not" 273 | ("bool","T") => fix "$true" 274 | ("bool","F") => fix "$false" 275 | _ => declare_perm_const state {Thy=thy,Name=s} 276 val tv = sort less_ty (type_vars ty) 277 val (newtvs, undeclare) = 278 declare_temp_list state dest_vartype (#tyvar_names state) tv 279 in 280 ( 281 os oc "tt("; os oc news; os oc ", ty, "; 282 case newtvs of [] => () | l => quant_tyvarl oc l; 283 oty state oc ty; os oc ").\n"; undeclare () 284 ) 285 end 286 287(* theorems *) 288fun othm state oc (name,role,tm) = 289 let 290 val l1 = type_varsl (map type_of (find_terms is_const tm @ all_vars tm)) 291 val (l2, undeclare) = 292 declare_temp_list state dest_vartype (#tyvar_names state) l1 293 in 294 ( 295 if uptodate_term tm 296 then (os oc "tt("; os oc name; 297 os oc (", " ^ role ^ ", "); quant_tyvarl oc l2; 298 otm state oc tm; 299 os oc ").\n") 300 else () 301 ; 302 undeclare () 303 ) 304 end 305 306fun othm_theorem state oc (name,role,thm) = 307 othm state oc (name,role,concl (GEN_ALL (DISCH_ALL thm))) 308 309(* conjecture *) 310fun othm_conjecture state oc conjecture = 311 othm state oc (conjecture_name, conjecture_name, 312 list_mk_forall (free_vars_lr conjecture,conjecture)) 313 314 315(*--------------------------------------------------------------------------- 316 Printing dependencies. 317 ----------------------------------------------------------------------------*) 318 319fun odep state oc_deps (name,dl) = 320 let 321 fun os_deps s = output (oc_deps,s) 322 fun name_did did = dfind_err "thm" did (!(#thm_names state)) 323 in 324 os_deps (name ^ " "); 325 oiter_deps oc_deps " " os_deps (mapfilter name_did dl); 326 os_deps "\n" 327 end 328 329(*--------------------------------------------------------------------------- 330 Exporting a theorem and its dependencies 331 ----------------------------------------------------------------------------*) 332 333fun export_thm state oc oc_deps ((name,thm),role) = 334 let 335 val d = (dep_of o tag) thm 336 val did = depid_of d 337 val dl = filter exists_did (depidl_of d) 338 val name' = declare_perm_thm state did name 339 in 340 othm_theorem state oc (name',role,thm); 341 odep state oc_deps (name',dl) 342 end 343 344(*--------------------------------------------------------------------------- 345 Printing theories 346 ----------------------------------------------------------------------------*) 347 348(* TODO: use OS.Path.concat *) 349fun write_thy dir filter_f state thy = 350 let 351 val oc = openOut (dir ^ "/" ^ thy ^ ".p") 352 val oc_deps = openOut (dir ^ "/" ^ thy ^ ".hd") 353 val THEORY(_,t) = dest_theory thy 354 val _ = app (hh_tydef state oc thy) (#types t) 355 val _ = app (hh_constdef state oc thy) (#consts t) 356 val axl = map (fn x => (x,"ax")) (DB.theorems thy) 357 (* TODO: why not (#theorems t) etc.? *) 358 val defl = map (fn x => (x,"def")) (DB.axioms thy @ DB.definitions thy) 359 fun local_compare (((_,th1),_),((_,th2),_)) = 360 let val f = depnumber_of o depid_of o dep_of o Thm.tag in 361 Int.compare (f th1, f th2) 362 end 363 val thml = filter (filter_f thy) (dict_sort local_compare (axl @ defl)) 364 in 365 app (export_thm state oc oc_deps) thml; 366 closeOut oc; 367 closeOut oc_deps 368 end 369 370fun write_thydep file thyl = 371 let 372 val oc = openOut file 373 fun f x = (os oc x; os oc " "; oiter oc " " (os oc) (parents x); os oc "\n") 374 in 375 app f thyl; 376 os oc namespace_tag; os oc " "; 377 oiter oc " " (os oc) [current_theory ()]; 378 os oc "\n"; 379 closeOut oc 380 end 381 382fun write_thyl dir filter_f thyl = 383 let 384 val state = 385 { 386 ty_names = ref (dempty KernelSig.name_compare), 387 const_names = ref (dempty KernelSig.name_compare), 388 var_names = ref (dempty Term.compare), 389 tyvar_names = ref (dempty Type.compare), 390 used_names = ref (dnew String.compare reserved_names0), 391 thm_names = ref (dempty depid_compare) 392 } 393 in 394 app (write_thy dir filter_f state) (sort_thyl thyl) 395 end 396 397fun write_conjecture state file conjecture = 398 if type_of conjecture = bool 399 then 400 let val oc = openOut file in 401 othm_conjecture state oc conjecture; 402 closeOut oc 403 end 404 else raise ERR "write_conjecture" "conjecture is not a boolean" 405 406(*--------------------------------------------------------------------------- 407 Writing theorems from the namespace. 408 ----------------------------------------------------------------------------*) 409 410fun write_ns state dir ns_thml = 411 let 412 val oc = openOut (dir ^ "/" ^ namespace_tag ^ ".p") 413 val oc_deps = openOut (dir ^ "/" ^ namespace_tag ^ ".hd") 414 fun new_name name = 415 let val (thy,nm1) = split_string "Theory." name in 416 squotify ("thm." ^ thy ^ "." ^ hh_escape nm1) 417 end 418 fun f (name,thm) = 419 let val name' = new_name name in 420 othm_theorem state oc (name',"ax",thm); 421 odep state oc_deps (name',[]) 422 end 423 in 424 app f ns_thml; 425 closeOut oc; 426 closeOut oc_deps 427 end 428 429fun write_problem dir filter_f ns_thml thyl cj = 430 let 431 fun sort_thyl thyl = topo_sort (map (fn x => (x, ancestry x)) thyl) 432 val state = 433 { 434 ty_names = ref (dempty KernelSig.name_compare), 435 const_names = ref (dempty KernelSig.name_compare), 436 var_names = ref (dempty Term.compare), 437 tyvar_names = ref (dempty Type.compare), 438 used_names = ref (dnew String.compare reserved_names0), 439 thm_names = ref (dempty depid_compare) 440 } 441 in 442 app (write_thy dir filter_f state) (sort_thyl thyl); 443 write_ns state dir ns_thml; 444 write_conjecture state (dir ^ "/conjecture.fof") cj (* not actually fof *) 445 end 446 447 448 449end 450