148 val shrink_proof: proof -> proof |
148 val shrink_proof: proof -> proof |
149 |
149 |
150 (*rewriting on proof terms*) |
150 (*rewriting on proof terms*) |
151 val add_prf_rrule: proof * proof -> theory -> theory |
151 val add_prf_rrule: proof * proof -> theory -> theory |
152 val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory |
152 val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory |
|
153 val set_preproc: (theory -> proof -> proof) -> theory -> theory |
153 val no_skel: proof |
154 val no_skel: proof |
154 val normal_skel: proof |
155 val normal_skel: proof |
155 val rewrite_proof: theory -> (proof * proof) list * |
156 val rewrite_proof: theory -> (proof * proof) list * |
156 (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof |
157 (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof |
157 val rewrite_proof_notypes: (proof * proof) list * |
158 val rewrite_proof_notypes: (proof * proof) list * |
1584 (* theory data *) |
1585 (* theory data *) |
1585 |
1586 |
1586 structure Data = Theory_Data |
1587 structure Data = Theory_Data |
1587 ( |
1588 ( |
1588 type T = |
1589 type T = |
1589 (stamp * (proof * proof)) list * |
1590 ((stamp * (proof * proof)) list * |
1590 (stamp * (typ list -> term option list -> proof -> (proof * proof) option)) list; |
1591 (stamp * (typ list -> term option list -> proof -> (proof * proof) option)) list) * |
1591 |
1592 (theory -> proof -> proof) option; |
1592 val empty = ([], []); |
1593 |
|
1594 val empty = (([], []), NONE); |
1593 val extend = I; |
1595 val extend = I; |
1594 fun merge ((rules1, procs1), (rules2, procs2)) : T = |
1596 fun merge (((rules1, procs1), preproc1), ((rules2, procs2), preproc2)) : T = |
1595 (AList.merge (op =) (K true) (rules1, rules2), |
1597 ((AList.merge (op =) (K true) (rules1, rules2), |
1596 AList.merge (op =) (K true) (procs1, procs2)); |
1598 AList.merge (op =) (K true) (procs1, procs2)), |
|
1599 merge_options (preproc1, preproc2)); |
1597 ); |
1600 ); |
1598 |
1601 |
1599 fun get_data thy = let val (rules, procs) = Data.get thy in (map #2 rules, map #2 procs) end; |
1602 fun get_rew_data thy = |
1600 fun rew_proof thy = rewrite_prf fst (get_data thy); |
1603 let val (rules, procs) = #1 (Data.get thy) |
1601 |
1604 in (map #2 rules, map #2 procs) end; |
1602 fun add_prf_rrule r = (Data.map o apfst) (cons (stamp (), r)); |
1605 |
1603 fun add_prf_rproc p = (Data.map o apsnd) (cons (stamp (), p)); |
1606 fun rew_proof thy = rewrite_prf fst (get_rew_data thy); |
|
1607 |
|
1608 fun add_prf_rrule r = (Data.map o apfst o apfst) (cons (stamp (), r)); |
|
1609 fun add_prf_rproc p = (Data.map o apfst o apsnd) (cons (stamp (), p)); |
|
1610 |
|
1611 fun set_preproc f = (Data.map o apsnd) (K (SOME f)); |
|
1612 fun apply_preproc thy = (case #2 (Data.get thy) of NONE => I | SOME f => f thy); |
1604 |
1613 |
1605 |
1614 |
1606 |
1615 |
1607 (** reconstruction of partial proof terms **) |
1616 (** reconstruction of partial proof terms **) |
1608 |
1617 |
2140 executable = false, |
2149 executable = false, |
2141 compress = true, |
2150 compress = true, |
2142 strict = false} |
2151 strict = false} |
2143 end; |
2152 end; |
2144 |
2153 |
2145 fun export_proof_boxes proof = |
2154 fun force_export_boxes proof = |
2146 let |
2155 let |
2147 fun export_boxes (AbsP (_, _, prf)) = export_boxes prf |
2156 fun export_boxes (AbsP (_, _, prf)) = export_boxes prf |
2148 | export_boxes (Abst (_, _, prf)) = export_boxes prf |
2157 | export_boxes (Abst (_, _, prf)) = export_boxes prf |
2149 | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2 |
2158 | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2 |
2150 | export_boxes (prf % _) = export_boxes prf |
2159 | export_boxes (prf % _) = export_boxes prf |
2158 in export_boxes prf boxes' end) |
2167 in export_boxes prf boxes' end) |
2159 | export_boxes _ = I; |
2168 | export_boxes _ = I; |
2160 val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest; |
2169 val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest; |
2161 in List.app (Lazy.force o #2) boxes end; |
2170 in List.app (Lazy.force o #2) boxes end; |
2162 |
2171 |
2163 fun export thy i prop prf = |
2172 fun export thy i prop prf0 = |
2164 if export_enabled () then (export_proof_boxes prf; export_proof thy i prop prf) else (); |
2173 if export_enabled () then |
|
2174 let |
|
2175 val prf = apply_preproc thy prf0; |
|
2176 val _ = force_export_boxes prf; |
|
2177 val _ = export_proof thy i prop prf; |
|
2178 in () end |
|
2179 else (); |
2165 |
2180 |
2166 fun prune proof = |
2181 fun prune proof = |
2167 if Options.default_bool "prune_proofs" then MinProof |
2182 if Options.default_bool "prune_proofs" then MinProof |
2168 else proof; |
2183 else proof; |
2169 |
2184 |