From 0416bd8de0e028ee39608a4d94e0a22b456a5dc6 Mon Sep 17 00:00:00 2001
From: Lars Hupel <lars.hupel@mytum.de>
Date: Thu, 31 Mar 2016 17:05:37 +0200
Subject: [PATCH] print types for function definitions in theory dump
---
src/main/isabelle/stateful_ops.ML | 25 ++++++++++++++++++++-----
1 file changed, 20 insertions(+), 5 deletions(-)
diff --git a/src/main/isabelle/stateful_ops.ML b/src/main/isabelle/stateful_ops.ML
index 18f0d6400..88ee8478f 100644
--- a/src/main/isabelle/stateful_ops.ML
+++ b/src/main/isabelle/stateful_ops.ML
@@ -33,12 +33,13 @@ fun err_timeout msg f x =
| Exn.Exn exn => reraise exn
datatype report =
- Function of {names: string list, raws: string list, specs: string list, inducts: (string * string) list} |
+ Function of {heads: (string * string) list, raws: string list, specs: string list, inducts: (string * string) list} |
Datatype of string |
Theory of {import: string, scripts: (string * string) list} |
Equivalence of string |
Lemma of {name: string, prop: string} |
- Oracle
+ Oracle |
+ End
structure Reports = Theory_Data
(
@@ -363,6 +364,12 @@ fun functions raw_funs =
Exn.Res (thms, lthy) =>
let
val names = map #1 raw_funs
+ val get_typ =
+ Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst
+ #> strip_comb #> fst
+ #> fastype_of
+ #> print_typ lthy
+ val typs = map get_typ thms
val lthy' = Local_Theory.restore lthy
val thms = Proof_Context.export lthy lthy' thms
val simpss = thms
@@ -375,7 +382,7 @@ fun functions raw_funs =
val binding = Binding.qualified true "spec" (Binding.make (hd names, @{here}))
val report =
Function
- {names = names,
+ {heads = names ~~ typs,
inducts = map_filter print_induct specs,
specs = map (print_thm lthy') simps,
raws = map (print_thm lthy') thms}
@@ -547,11 +554,19 @@ fun dump () =
| print_report (Lemma {prop, ...}) = ([], "lemma [simp]: " ^ quote prop ^ "\nsorry")
| print_report (Datatype spec) = ([], spec)
| print_report Oracle = ([], "")
- | print_report (Function {names, specs, ...}) =
- ([], "fun " ^ space_implode " and " names ^ " where\n" ^ space_implode "|\n" (map quote specs))
+ | print_report End = ([], "\nend\n")
+ | print_report (Function {heads, specs, ...}) =
+ let
+ fun mk_head (name, typ) = quote name ^ " :: " ^ quote typ
+ val head = "fun " ^ space_implode " and " (map mk_head heads) ^ " where\n"
+ val body = space_implode "|\n" (map quote specs)
+ in
+ ([], head ^ body)
+ end
in
Proof_Context.theory_of lthy
|> Reports.get
+ |> cons End
|> rev
|> map print_report
|> split_list
--
GitLab