author | blanchet |
Tue, 28 Sep 2010 08:35:00 +0200 | |
changeset 39748 | a727e1dab162 |
parent 39483 | 9f0e5684f04b |
permissions | -rw-r--r-- |
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Datatype/datatype_selectors.ML |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
3 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
4 |
Selector functions for datatype constructor arguments. |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
5 |
*) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
6 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
7 |
signature DATATYPE_SELECTORS = |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
8 |
sig |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
9 |
val add_selector: ((string * typ) * int) * (string * typ) -> |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
10 |
Context.generic -> Context.generic |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
11 |
val lookup_selector: Proof.context -> string * int -> string option |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
12 |
val setup: theory -> theory |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
13 |
end |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
14 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
15 |
structure Datatype_Selectors: DATATYPE_SELECTORS = |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
16 |
struct |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
17 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
18 |
structure Stringinttab = Table |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
19 |
( |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
20 |
type key = string * int |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
21 |
val ord = prod_ord fast_string_ord int_ord |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
22 |
) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
23 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
24 |
structure Data = Generic_Data |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
25 |
( |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
26 |
type T = string Stringinttab.table |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
27 |
val empty = Stringinttab.empty |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
28 |
val extend = I |
39748 | 29 |
fun merge data : T = Stringinttab.merge (K true) data |
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
30 |
) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
31 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
32 |
fun pretty_term context = Syntax.pretty_term (Context.proof_of context) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
33 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
34 |
fun sanity_check context (((con as (n, _), i), sel as (m, _))) = |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
35 |
let |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
36 |
val thy = Context.theory_of context |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
37 |
val varify_const = |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
38 |
Const #> Type.varify_global [] #> snd #> Term.dest_Const #> |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
39 |
snd #> Term.strip_type |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
40 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
41 |
val (Ts, T) = varify_const con |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
42 |
val (Us, U) = varify_const sel |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
43 |
val _ = (0 < i andalso i <= length Ts) orelse |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
44 |
error (Pretty.string_of (Pretty.block [ |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
45 |
Pretty.str "The constructor ", |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
46 |
Pretty.quote (pretty_term context (Const con)), |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
47 |
Pretty.str " has no argument position ", |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
48 |
Pretty.str (string_of_int i), |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
49 |
Pretty.str "."])) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
50 |
val _ = length Us = 1 orelse |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
51 |
error (Pretty.string_of (Pretty.block [ |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
52 |
Pretty.str "The term ", Pretty.quote (pretty_term context (Const sel)), |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
53 |
Pretty.str " might not be a selector ", |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
54 |
Pretty.str "(it accepts more than one argument)."])) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
55 |
val _ = |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
56 |
(Sign.typ_equiv thy (T, hd Us) andalso |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
57 |
Sign.typ_equiv thy (nth Ts (i-1), U)) orelse |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
58 |
error (Pretty.string_of (Pretty.block [ |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
59 |
Pretty.str "The types of the constructor ", |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
60 |
Pretty.quote (pretty_term context (Const con)), |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
61 |
Pretty.str " and of the selector ", |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
62 |
Pretty.quote (pretty_term context (Const sel)), |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
63 |
Pretty.str " do not fit to each other."])) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
64 |
in ((n, i), m) end |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
65 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
66 |
fun add_selector (entry as ((con as (n, _), i), (_, T))) context = |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
67 |
(case Stringinttab.lookup (Data.get context) (n, i) of |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
68 |
NONE => Data.map (Stringinttab.update (sanity_check context entry)) context |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
69 |
| SOME c => error (Pretty.string_of (Pretty.block [ |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
70 |
Pretty.str "There is already a selector assigned to constructor ", |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
71 |
Pretty.quote (pretty_term context (Const con)), Pretty.str ", namely ", |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
72 |
Pretty.quote (pretty_term context (Const (c, T))), Pretty.str "."]))) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
73 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
74 |
fun lookup_selector ctxt = Stringinttab.lookup (Data.get (Context.Proof ctxt)) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
75 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
76 |
val setup = |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
77 |
Attrib.setup @{binding selector} |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
78 |
((Args.term >> Term.dest_Const) -- Scan.lift (Parse.nat) --| |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
79 |
Scan.lift (Parse.$$$ "=") -- (Args.term >> Term.dest_Const) >> |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
80 |
(Thm.declaration_attribute o K o add_selector)) |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
81 |
"assign a selector function to a datatype constructor argument" |
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
82 |
|
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
diff
changeset
|
83 |
end |