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