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