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