1(* ===================================================================== *)
2(* FILE          : Tag.sml                                               *)
3(* DESCRIPTION   : Theorem tagging (for oracles and other stuff)         *)
4(*                                                                       *)
5(* AUTHOR        : (c) Konrad Slind, University of Cambridge             *)
6(*                 Modified by Thibault Gauthier 2015                    *)
7(* DATE          : 1998                                                  *)
8(* ===================================================================== *)
9
10structure Tag :> Tag =
11struct
12
13open Lib Feedback Dep
14
15val ERR = mk_HOL_ERR "Tag";
16
17(*---------------------------------------------------------------------------*)
18(* A tag is represented by a pair (D,O,A) where O is a list of oracles       *)
19(* (represented by strings) and A is a list of axioms (a list of references  *)
20(* to strings). The axioms are used to track the use of axioms in proofs in  *)
21(* the current theory. D represents a list of proof dependencies of the      *)
22(* theorem.                                                                  *)
23(*---------------------------------------------------------------------------*)
24
25datatype tag = TAG of dep * string list * string Nonce.t list
26
27fun dest_tag (TAG(D,O,A)) = (O, map Nonce.dest A)
28fun oracles_of (TAG(_,O,_)) = O
29fun axioms_of  (TAG(_,_,A)) = A
30fun dep_of (TAG(D,_,_)) = D
31fun set_dep d (TAG(_,O,A)) = TAG(d,O,A)
32
33val empty_tag = TAG (empty_dep,[],[])
34val disk_only_tag  = TAG (empty_dep,["DISK_THM"],[])
35fun ax_tag r = TAG (empty_dep,[],[r])
36
37fun isEmpty tg = null (oracles_of tg) andalso null (axioms_of tg)
38fun isDisk tg = oracles_of tg = ["DISK_THM"] andalso null (axioms_of tg)
39
40(*---------------------------------------------------------------------------
41   Create a tag. A tag is a string with only printable characters (as
42   defined by Char.isPrint) and without spaces.
43 ----------------------------------------------------------------------------*)
44
45fun read s =
46 let open Substring
47 in if isEmpty(dropl Char.isPrint (full s))
48     then TAG (empty_dep,[s],[])
49     else raise ERR "read"
50           (Lib.quote s^" has unprintable characters")
51 end;
52
53(*---------------------------------------------------------------------------
54   Tracks the extra information passed through the inference rules.
55   Read tags from disk.
56 ----------------------------------------------------------------------------*)
57
58local
59
60val merge_axiom = Lib.union
61
62fun merge_oracle t1 [] = t1
63  | merge_oracle [] t2 = t2
64  | merge_oracle (t as ["DISK_THM"]) ["DISK_THM"] = t
65  | merge_oracle (l0 as s0::rst0) (l1 as s1::rst1) =
66      case String.compare (s0,s1) of
67        LESS    => s0::merge_oracle rst0 l1
68      | GREATER => s1::merge_oracle l0 rst1
69      | EQUAL   => s0::merge_oracle rst0 rst1
70
71in (* in local *)
72
73fun merge (TAG(d1,o1,ax1)) (TAG(d2,o2,ax2)) =
74  TAG(merge_dep d1 d2, merge_oracle o1 o2, merge_axiom ax1 ax2)
75
76fun read_disk_tag (d,[]) = TAG (read_dep d, ["DISK_THM"], [])
77  | read_disk_tag (d,sl) = TAG (read_dep d, merge_oracle ["DISK_THM"] sl, [])
78
79end; (* end local *)
80
81
82(*---------------------------------------------------------------------------
83   In a theory file, the list of oracles gets dumped out as a list of
84   strings. The axioms are not currently dumped, since they are being used
85   only for ensuring that no out-of-date objects in the current theory
86   become persistent. Concrening dependencies, we only print the dependency
87   number inside the tag. Other informations are retrieved from the dependency
88   graph.
89 ----------------------------------------------------------------------------*)
90
91fun pp_to_disk ppstrm (TAG (d,olist,_)) =
92  let
93    open Portable OldPP
94    val {add_string,add_break,begin_block,end_block,...} = with_ppstream ppstrm
95    fun pp_sl l =
96      (
97      begin_block CONSISTENT 0;
98      add_string "[";
99      begin_block INCONSISTENT 1;
100      pr_list add_string (fn () => add_string ",")
101                         (fn () => add_break(1,0)) l;
102      end_block();
103      add_string "]";
104      end_block()
105      )
106   in
107    (
108    begin_block CONSISTENT 0;
109      add_string "(";
110      pp_dep ppstrm d;
111      add_string ",";
112      pp_sl (map Lib.mlquote olist);
113      add_string ")";
114    end_block()
115    )
116  end
117
118(*---------------------------------------------------------------------------
119     Prettyprint a tag (for interactive work).
120 ---------------------------------------------------------------------------*)
121
122local open Portable
123      fun repl ch alist = CharVector.tabulate(length alist, fn _ => ch)
124      open HOLPP
125      fun pr_list s c b [] = []
126        | pr_list s c b [e] = [PrettyString (s e)]
127        | pr_list s c b (e::es) =
128            PrettyString (s e) :: PrettyString c :: PrettyBreak b ::
129            pr_list s c b es
130      val add_string = PrettyString
131      val add_break = PrettyBreak
132in
133fun pp_tag (TAG (_,olist,axlist)) =
134  PrettyBlock(0, true, [],
135    [PrettyString "[oracles: ",
136     PrettyBlock(1, false, [],
137                 if !Globals.show_tags then pr_list I "," (1,0) olist
138                 else [PrettyString(repl #"#" olist)]),
139      add_string "]",
140      add_break(1,0),
141      add_string "[axioms: ",
142      PrettyBlock(1, false, [],
143                  if !Globals.show_axioms then
144                    pr_list Nonce.dest "," (1,0) axlist
145                  else [add_string(repl #"#" axlist)]),
146      add_string "]"
147    ])
148end;
149
150end
151