1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 *) 10 11signature PROOF_COUNT = 12sig 13 14 datatype lemmaT = Lemma of string | Declare of string 15 16 datatype transactionT = Start | Qed | Declaration | Qed_Global | Unknown 17 18 type count_report = (((transactionT * string) * string list * (Position.range)) list Symtab.table) 19 20 val get_size_report : unit -> count_report 21 22 val compute_sizes : count_report -> (lemmaT * Position.range) Symtab.table 23 24end 25 26structure Proof_Count : PROOF_COUNT = 27struct 28 29datatype transactionT = Start | Qed | Declaration | Qed_Global | Unknown 30 31type count_report = (((transactionT * string) * string list * (Position.range)) list Symtab.table) 32 33val transactions = Synchronized.var "hooked" (Symtab.empty : ((transactionT * string) * string list * (Position.range)) list Symtab.table) 34 35fun get_transactionT k = 36 if Keyword.is_theory_goal k orelse Keyword.is_proof_goal k then Start 37 else if Keyword.is_qed k then Qed 38 else if Keyword.is_qed_global k then Qed_Global 39 else if member (op =) (Keyword.command_tags k) "thy_decl" orelse k = "lemmas" then Declaration 40 else Unknown 41 42fun needs_hook k = case get_transactionT k of Unknown => false 43 | _ => if k = "lemmas" orelse k = "by" then false else true 44 45(*We explicitly ignore the "real" fact names because this is not what's given in the dependency analysis.*) 46(*The "name" tag in the thm is what is picked up by the kernel for creating the proof_bodies*) 47fun add_new_lemmas thy thy' beg fin trans = 48let 49 val file = Position.file_of beg 50 |> the_default "" 51 val prev_facts = Global_Theory.facts_of thy; 52 val facts = Global_Theory.facts_of thy'; 53 val nms = (Facts.dest_static false [prev_facts] facts); 54 val realnms = map (fn (_,thms) => filter Thm.has_name_hint thms |> map Thm.get_name_hint) nms |> flat 55in 56 Synchronized.change transactions (Symtab.map_default (file,[]) (cons ((get_transactionT trans,trans),realnms,(beg,fin)))) end 57 58 59val _ = 60 Outer_Syntax.command @{command_keyword "by"} "terminal backward proof" 61 ((fn toks => 62 let 63 val (beg,fin) = (Token.pos_of (hd toks),Token.pos_of (List.last toks)) 64 val file = Position.file_of beg |> the_default "" 65 val _ = Synchronized.change transactions (Symtab.map_default (file,[]) (cons ((Qed,"by"),[],(beg,fin)))) 66 in 67 (Method.parse -- Scan.option Method.parse >> Isar_Cmd.terminal_proof) toks 68 end)) 69 70fun wrap_lthy' ttyp parser toks = 71 let 72 val (flthy,toks') = parser toks 73 in 74 ((fn b => fn lthy => let 75 val (beg,fin) = (Token.pos_of (hd toks),Token.pos_of (List.last toks)) 76 val lthy' = flthy b lthy 77 val _ = add_new_lemmas (Proof_Context.theory_of lthy) (Proof_Context.theory_of lthy') beg fin ttyp 78 in 79 lthy' end),toks') end 80 81fun theorems kind = 82 Parse_Spec.name_facts -- Parse.for_fixes 83 >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd kind facts fixes); 84 85val _ = 86 Outer_Syntax.local_theory' @{command_keyword "lemmas"} "define lemmas" (wrap_lthy' "lemmas" (theorems Thm.lemmaK)); 87 88fun get_size_report () = Synchronized.value transactions 89 90(* Move to library? *) 91fun bracket_list leftbr rightbr superbr l = 92let 93 fun err () = error ("Mismatched parenthesis: " ^ Position.here @{here}) 94 95 fun bracket_list_aux stack pairs extras [] = 96 if null stack then (rev pairs,rev extras) else err () 97 98 | bracket_list_aux stack pairs extras (x :: l) = 99 if leftbr x then bracket_list_aux (x :: stack) pairs extras l 100 else if rightbr x then 101 case stack of 102 (s :: stack') => bracket_list_aux stack' ((s,x) :: pairs) extras l 103 | _ => err () 104 else if superbr x then bracket_list_aux [] ((List.last stack,x) :: pairs) extras l 105 else bracket_list_aux stack pairs (x :: extras) l 106in 107 bracket_list_aux [] [] [] l 108end 109 110fun merge_duplicates ord merge = 111let 112 fun merge_duplicates_aux (a :: b :: l) = 113 (case (ord (a,b)) of 114 EQUAL => merge_duplicates_aux ((merge a b) :: l) 115 | GREATER => error "Merging duplicates requires sorted list" 116 | _ => a :: (merge_duplicates_aux (b :: l))) 117 118 | merge_duplicates_aux x = x 119in 120 merge_duplicates_aux 121end 122 123 124fun to_tuple pos = (Position.line_of pos, Position.offset_of pos) 125 126fun pos_ord (pos1,pos2) = (prod_ord (option_ord int_ord) (option_ord int_ord)) (to_tuple pos1,to_tuple pos2) 127 128datatype lemmaT = Lemma of string | Declare of string 129 130 131fun compute_sizes (transactions) = 132 let 133 134 fun trans_less (Start,Qed) = true 135 | trans_less (Start,Declaration) = true 136 | trans_less (Qed,Declaration) = true 137 | trans_less (Start,Qed_Global) = true 138 | trans_less (Qed_Global,Declaration) = true 139 | trans_less _ = false 140 141 fun do_prod (((trans,_),_,(st1,_)),((trans',_),_,(st2,_))) = ((st1,trans),(st2,trans')) 142 143 val ord = (prod_ord pos_ord (make_ord trans_less)) o do_prod 144 145 fun proc_entry (_,trans) = 146 let 147 val _ = map (fn ((Unknown,_),_,_) => 148 error "Unexpected Unknown transaction in count report" 149 | _ => ()) trans 150 151 val sorted_transactions = sort ord trans 152 |> merge_duplicates ord (fn (t,nms,s) => fn (_,nms',_) => (t,merge (op =) (nms,nms'),s)) 153 154 val (paired,singles) = bracket_list 155 (fn ((t,_),_,_) => t = Start) 156 (fn ((t,_),_,_) => t = Qed) 157 (fn ((t,_),_,_) => t = Qed_Global) 158 sorted_transactions 159 160 fun fix_range ((x,xs,(st1,_)),(_,ys,(_,fin2))) = (x,xs @ ys,(st1,fin2)) 161 in 162 (map fix_range paired) @ singles end 163 164 fun translate_trans t nm = case t of Start => Lemma nm 165 | Declaration => Declare nm 166 | _ => error "Unexpected transaction type" 167 in 168 fold (append o proc_entry) (Symtab.dest transactions) [] 169 |> map (fn (t,facts,range) => map (rpair (t,range)) facts) 170 |> flat 171 |> Symtab.make_list 172 |> Symtab.map (fn _ => fn k => find_first (fn (_,(p,p')) => Option.isSome (Position.line_of p) andalso Option.isSome (Position.line_of p')) k |> the_default (hd k)) 173 |> Symtab.delete_safe "" 174 |> Symtab.map (fn _ => fn ((t,nm),range) => (translate_trans t nm,range)) 175end 176 177(*FIXME: Redundant?*) 178val _ = Toplevel.add_hook (fn trans => fn state => fn state' => 179 if needs_hook (Toplevel.name_of trans) then 180 (let 181 val pos = Toplevel.pos_of trans 182 val name = Toplevel.name_of trans 183 184 val thy = Toplevel.theory_of state 185 val thy' = Toplevel.theory_of state' 186 187 in 188 add_new_lemmas thy thy' pos pos name end) 189 else ()) 190 191 192end 193