1(*---------------------------------------------------------------------------*
2 *                                                                           *
3 *            HOL theories interpreted by SML structures.                    *
4 *                                                                           *
5 *---------------------------------------------------------------------------*)
6
7structure TheoryPP :> TheoryPP =
8struct
9
10type thm      = Thm.thm;
11type term     = Term.term
12type hol_type = Type.hol_type
13type shared_writemaps = {strings : string -> int, terms : Term.term -> string}
14type shared_readmaps = {strings : int -> string, terms : string -> Term.term}
15type struct_info_record = {
16   theory      : string*Arbnum.num*Arbnum.num,
17   parents     : (string*Arbnum.num*Arbnum.num) list,
18   types       : (string*int) list,
19   constants   : (string*hol_type) list,
20   axioms      : (string * thm) list,
21   definitions : (string * thm) list,
22   theorems    : (string * thm) list,
23   struct_ps   : (unit -> PP.pretty) option list,
24   struct_pcps : (unit -> PP.pretty) list,
25   mldeps      : string list,
26   thydata     : string list * Term.term list *
27                 (string,shared_writemaps -> HOLsexp.t)Binarymap.dict
28 }
29
30open Feedback Lib Portable Dep;
31
32val ERR = mk_HOL_ERR "TheoryPP";
33
34val temp_binding_pfx = "@temp"
35val is_temp_binding = String.isPrefix temp_binding_pfx
36fun temp_binding s = temp_binding_pfx ^ s
37fun dest_temp_binding s =
38  if is_temp_binding s then
39    String.extract(s, size temp_binding_pfx, NONE)
40  else raise ERR "dest_temp_binding" "String not a temp-binding"
41
42
43val pp_sig_hook = ref (fn () => ());
44
45val concat = String.concat;
46val sort = Lib.sort (fn s1:string => fn s2 => s1<=s2);
47val psort = Lib.sort (fn (s1:string,_:Thm.thm) => fn (s2,_:Thm.thm) => s1<=s2);
48fun Thry s = s^"Theory";
49fun ThrySig s = Thry s
50
51fun with_parens pfn x =
52  let open Portable PP
53  in [add_string "(", pfn x, add_string ")"]
54  end
55
56fun pp_type mvartype mtype ty =
57 let open Portable Type PP
58     val pp_type = pp_type mvartype mtype
59 in
60  if is_vartype ty
61  then case dest_vartype ty
62        of "'a" => add_string "alpha"
63         | "'b" => add_string "beta"
64         | "'c" => add_string "gamma"
65         | "'d" => add_string "delta"
66         |  s   => add_string (mvartype^quote s)
67  else
68  case dest_thy_type ty
69   of {Tyop="bool",Thy="min", Args=[]} => add_string "bool"
70    | {Tyop="ind", Thy="min", Args=[]} => add_string "ind"
71    | {Tyop="fun", Thy="min", Args=[d,r]} =>
72          block INCONSISTENT 1 [
73            add_string "(",
74            pp_type d,
75            add_string " -->",
76            add_break (1,0),
77            pp_type r,
78            add_string ")"
79          ]
80   | {Tyop,Thy,Args} =>
81          block INCONSISTENT (size mtype) [
82            add_string mtype,
83            add_string (quote Tyop),
84            add_break (1,0),
85            add_string (quote Thy),
86            add_break (1,0),
87            add_string "[",
88            block INCONSISTENT 1 (
89              pr_list pp_type [add_string ",", add_break (1,0)] Args
90            ),
91            add_string "]"
92          ]
93 end
94
95val include_docs = ref true
96val _ = Feedback.register_btrace ("TheoryPP.include_docs", include_docs)
97
98fun pp_sig pp_thm info_record = let
99  open PP
100  val {name,parents,axioms,definitions,theorems,sig_ps} = info_record
101  val parents'     = sort parents
102  val rm_temp      = List.filter (fn (s, _) => not (is_temp_binding s))
103  val axioms'      = psort axioms |> rm_temp
104  val definitions' = psort definitions |> rm_temp
105  val theorems'    = psort theorems |> rm_temp
106  val thml         = axioms@definitions@theorems
107  fun vblock(header, ob_pr, obs) =
108    block CONSISTENT 2 [
109      add_string ("(*  "^header^ "  *)"), NL,
110      block CONSISTENT 0 (pr_list ob_pr [NL] obs)
111    ]
112  fun pparent s = String.concat ["structure ",Thry s," : ",ThrySig s]
113  val parentstring = "Parent theory of "^Lib.quote name
114  fun pr_parent s = block CONSISTENT 0 [
115                     add_string (String.concat ["[", s, "]"]),
116                     add_break(1,0),
117                     add_string parentstring]
118  fun pr_parents [] = []
119    | pr_parents slist =
120        [block CONSISTENT 0 (pr_list pr_parent [NL, NL] slist), NL, NL]
121
122  fun pr_thm class (s,th) =
123    block CONSISTENT 3 [
124      add_string (String.concat ["[", s, "]"]),
125      add_string ("  "^class), NL, NL,
126      if null (Thm.hyp th) andalso
127         (Tag.isEmpty (Thm.tag th) orelse Tag.isDisk (Thm.tag th))
128      then pp_thm th
129      else
130        with_flag(Globals.show_tags,true)
131                 (with_flag(Globals.show_assums, true) pp_thm) th
132    ]
133      handle e => (print ("Failed to print theorem in theory export: "^s^"\n");
134                   print (General.exnMessage e ^ "\n");
135                   raise e)
136  fun pr_thms _ [] = []
137    | pr_thms heading plist =
138       [block CONSISTENT 0 (pr_list (pr_thm heading) [NL,NL] plist), NL, NL]
139  fun pr_sig_ps NONE = []  (* won't be fired because of filtering below *)
140    | pr_sig_ps (SOME pp) = [pp()]
141  fun pr_sig_psl [] = []
142    | pr_sig_psl l =
143       [NL, NL,
144        block CONSISTENT 0
145              (pr_list (block CONSISTENT 0 o pr_sig_ps) [NL, NL] l)]
146
147  fun pr_docs() =
148      if !include_docs then
149        (!pp_sig_hook();
150         [block CONSISTENT 3 (
151             [add_string "(*", NL] @
152             pr_parents parents' @
153             pr_thms "Axiom" axioms' @
154             pr_thms "Definition" definitions' @
155             pr_thms "Theorem" theorems'
156           ), NL,
157          add_string "*)", NL])
158      else []
159  fun pthms (heading, ths) =
160    vblock(heading,
161           (fn (s,th) => block CONSISTENT 0
162                               (if is_temp_binding s then []
163                                else
164                                  [add_string("val "^ s ^ " : thm")])),
165           ths)
166in
167  block CONSISTENT 0 (
168    [add_string ("signature "^ThrySig name^" ="), NL,
169     block CONSISTENT 2 [
170       add_string "sig", NL,
171       block CONSISTENT 0 (
172         [add_string"type thm = Thm.thm"] @
173         (if null axioms' then []
174          else [NL, NL, pthms ("Axioms",axioms')]) @
175         (if null definitions' then []
176          else [NL, NL, pthms("Definitions", definitions')]) @
177         (if null theorems' then []
178          else [NL, NL, pthms ("Theorems", theorems')]) @
179         pr_sig_psl (filter (fn NONE => false | _ => true) sig_ps)
180       )
181     ], NL
182    ] @
183    pr_docs() @
184    [add_string"end", NL]
185  )
186end;
187
188(*---------------------------------------------------------------------------
189 *  Print a theory as a module.
190 *---------------------------------------------------------------------------*)
191
192val stringify = Lib.mlquote
193
194fun is_atom t = Term.is_var t orelse Term.is_const t
195fun strip_comb t = let
196  fun recurse acc t = let
197    val (f, x) = Term.dest_comb t
198  in
199    recurse (x::acc) f
200  end handle HOL_ERR _ => (t, List.rev acc)
201in
202  recurse [] t
203end
204
205infix >>
206open smpp
207
208fun mlower s m =
209  case m ((), []) of
210      NONE => raise Fail ("Couldn't print Theory" ^ s)
211    | SOME(_, (_, ps)) => PP.block PP.CONSISTENT 0 ps
212
213fun pp_struct (info_record : struct_info_record) = let
214  open Term Thm
215  val {theory as (name,i1,i2), parents=parents0, thydata, mldeps, axioms,
216       definitions,theorems,types,constants,struct_ps,
217       struct_pcps} = info_record
218  val parents1 =
219    List.mapPartial (fn (s,_,_) => if "min"=s then NONE else SOME (Thry s))
220                    parents0
221  val thml = axioms@definitions@theorems
222  val jump = add_newline >> add_newline
223  fun pblock(ob_pr, obs) =
224      case obs of
225        [] => nothing
226      |  _ =>
227         block CONSISTENT 0
228           (
229           add_string "local open " >>
230           block INCONSISTENT 0 (pr_list ob_pr (add_break (1,0)) obs) >>
231           add_break(1,0) >>
232           add_string "in end;"
233           )
234
235  fun pparent (s,i,j) = Thry s
236
237  fun pr_bind(s, th) = let
238    val (tg, asl, w) = (Thm.tag th, Thm.hyp th, Thm.concl th)
239    val addsbl = pr_list add_string (add_break(1,2))
240  in
241    if is_temp_binding s then nothing
242    else
243      (* this rigmarole is necessary to allow ML bindings where the name is
244         a datatype constructor or an infix, or both *)
245      block CONSISTENT 0
246        (block INCONSISTENT 0 (addsbl ["fun","op",s,"_","=","()"]) >>
247         add_break(1,0) >>
248         block INCONSISTENT 0 (addsbl ["val","op",s,"=","TDB.find",mlquote s]))
249  end
250
251  val bind_theorems =
252     block CONSISTENT 0 (
253       if null thml then nothing
254       else
255         block CONSISTENT 0 (pr_list pr_bind add_newline thml) >>
256         add_newline
257     )
258
259  fun pr_ps NONE = nothing
260    | pr_ps (SOME pp) = block CONSISTENT 0 (lift pp ())
261
262  fun pr_psl l =
263       block CONSISTENT 0
264         (pr_list pr_ps (add_newline >> add_newline) l)
265  fun pr_pcl l =
266      block CONSISTENT 0 (
267        pr_list (fn pf => block CONSISTENT 0 (lift pf ()))
268                (add_newline >> add_newline)
269                l
270      )
271  val datfile =
272      mlquote (
273        holpathdb.reverse_lookup {
274          path = OS.Path.concat(OS.FileSys.getDir(), name ^ "Theory.dat")
275        }
276      )
277  val m =
278      block CONSISTENT 0 (
279       add_string (String.concatWith " "
280                       ["structure",Thry name,":>", ThrySig name,"="]) >>
281       add_newline >>
282       block CONSISTENT 2 (
283          add_string "struct" >> jump >>
284          block CONSISTENT 0 (
285            block CONSISTENT 0 (
286             add_string ("val _ = if !Globals.print_thy_loads") >>
287             add_break (1,2) >>
288             add_string
289               ("then TextIO.print \"Loading "^ Thry name ^ " ... \"") >>
290             add_break (1,2) >>
291             add_string "else ()") >> jump >>
292             add_string "open Type Term Thm"  >> add_newline >>
293             pblock (add_string,
294               Listsort.sort String.compare parents1 @ mldeps) >>
295             add_newline >> add_newline >>
296             block CONSISTENT 0 (
297              add_string "structure TDB = struct" >> add_break(1,2) >>
298              add_string "val thydata = " >> add_break(1,4) >>
299              block INCONSISTENT 0 (
300                add_string "TheoryReader.load_thydata" >> add_break (1,2) >>
301                add_string (mlquote name) >> add_break (1,2) >>
302                add_string ("(holpathdb.subst_pathvars "^datfile^")")
303              ) >> add_break(1,2) >>
304              add_string ("fun find s = Redblackmap.find (thydata,s)") >>
305              add_break(1,0) >> add_string "end"
306            ) >> jump >>
307            bind_theorems >>
308            add_newline >>
309            pr_psl struct_ps
310          )
311        ) >> add_break(0,0) >>
312        add_string "val _ = if !Globals.print_thy_loads then TextIO.print \
313                   \\"done\\n\" else ()" >> add_newline >>
314        add_string ("val _ = Theory.load_complete "^ stringify name) >>
315        jump >>
316        pr_pcl struct_pcps >>
317        add_string "end" >> add_newline)
318in
319  mlower ": struct" m
320end
321
322(*---------------------------------------------------------------------------
323 *  Print theory data separately.
324 *---------------------------------------------------------------------------*)
325
326
327fun pp_thydata (info_record : struct_info_record) = let
328  open Term Thm
329  val {theory as (name,i1,i2), parents=parents0,
330       thydata = (thydata_strings,thydata_tms, thydata), mldeps,
331       axioms,definitions,theorems,types,constants,...} = info_record
332  val parents1 =
333      List.mapPartial (fn (s,_,_) => if "min"=s then NONE else SOME (Thry s))
334                      parents0
335  val thml = axioms@definitions@theorems
336  open SharingTables
337
338  val share_data = build_sharing_data {
339        named_terms = [], named_types = [], unnamed_terms = [],
340        unnamed_types = [], theorems = thml
341      }
342  val share_data = add_strings thydata_strings share_data
343  val share_data = add_terms thydata_tms share_data
344
345  local open HOLsexp in
346  fun enc_thid(s,i,j) =
347    List[String s, String (Arbnum.toString i), String (Arbnum.toString j)]
348  val enc_thid_and_parents =
349      curry (pair_encode(enc_thid, list_encode enc_thid))
350  end (* local *)
351
352  fun enc_incorporate_types types =
353      let open HOLsexp
354      in
355        tagged_encode "incorporate-types"
356                      (list_encode (pair_encode(String,Integer))) types
357      end
358
359  fun enc_incorporate_constants constants =
360      let open HOLsexp
361      in
362        tagged_encode "incorporate-consts"
363                      (list_encode
364                         (pair_encode(String, Integer o write_type share_data)))
365                      constants
366      end
367
368  val enc_dblist =
369     let
370       open HOLsexp
371       val enc_db = Integer o write_string share_data
372       val enc_dbl = list_encode enc_db
373       val check =
374           List.mapPartial (fn (nm, _) => if is_temp_binding nm then NONE
375                                          else SOME nm)
376       val axl  = check axioms
377       val defl = check definitions
378       val thml = check theorems
379     in
380       tagged_encode "thm-classes"
381                     (pair3_encode (enc_dbl, enc_dbl, enc_dbl)) (axl,defl,thml)
382     end
383
384  fun chunks w s =
385    if String.size s <= w then [s]
386    else String.substring(s, 0, w) :: chunks w (String.extract(s, w, NONE))
387
388  val enc_cpl = HOLsexp.pair_encode(HOLsexp.String, fn x => x)
389
390  fun list_loadable shared_writers thydata_map =
391    Binarymap.foldl
392      (fn (k, data, rest) => (k, data shared_writers) :: rest)
393      []
394      thydata_map
395  fun enc_loadable shared_writers thydata_map =
396      let open HOLsexp in
397        tagged_encode "loadable-thydata" (list_encode enc_cpl)
398                      (list_loadable shared_writers thydata_map)
399      end
400  val thysexp =
401      let open HOLsexp
402      in
403        List [
404          Symbol "theory",
405          enc_thid_and_parents theory parents0,
406          enc_sdata share_data,
407          tagged_encode "incorporate" (
408            pair_encode(enc_incorporate_types, enc_incorporate_constants)
409          ) (types, constants),
410          enc_dblist,
411          enc_loadable {terms = write_term share_data,
412                        strings = write_string share_data}
413                       thydata
414        ]
415      end
416in
417  mlower ": dat" (lift HOLsexp.printer thysexp)
418end handle e as Interrupt => raise e
419         | e => raise ERR "pp_thydata"
420                      ("Caught exception: " ^ General.exnMessage e)
421
422
423
424end;  (* TheoryPP *)
425