33 |
35 |
34 subsection {* Primitive operations *} |
36 subsection {* Primitive operations *} |
35 |
37 |
36 setup_lifting type_definition_rbt |
38 setup_lifting type_definition_rbt |
37 |
39 |
38 quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup" |
40 lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup" |
39 by simp |
41 by simp |
40 |
42 |
41 (* FIXME: quotient_definition at the moment requires that types variables match exactly, |
43 lift_definition empty :: "('a\<Colon>linorder, 'b) rbt" is RBT_Impl.Empty |
42 i.e., sort constraints must be annotated to the constant being lifted. |
44 by (simp add: empty_def) |
43 But, it should be possible to infer the necessary sort constraints, making the explicit |
|
44 sort constraints unnecessary. |
|
45 |
45 |
46 Hence this unannotated quotient_definition fails: |
46 lift_definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.insert" |
47 |
|
48 quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt" |
|
49 is "RBT_Impl.Empty" |
|
50 |
|
51 Similar issue for quotient_definition for entries, keys, map, and fold. |
|
52 *) |
|
53 |
|
54 quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt" |
|
55 is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" by (simp add: empty_def) |
|
56 |
|
57 quotient_definition insert where "insert :: 'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" |
|
58 is "RBT_Impl.insert" by simp |
|
59 |
|
60 quotient_definition delete where "delete :: 'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" |
|
61 is "RBT_Impl.delete" by simp |
|
62 |
|
63 (* FIXME: unnecessary type annotations *) |
|
64 quotient_definition "entries :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" |
|
65 is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" by simp |
|
66 |
|
67 (* FIXME: unnecessary type annotations *) |
|
68 quotient_definition "keys :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" |
|
69 is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list" by simp |
|
70 |
|
71 quotient_definition "bulkload :: ('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" |
|
72 is "RBT_Impl.bulkload" by simp |
|
73 |
|
74 quotient_definition "map_entry :: 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" |
|
75 is "RBT_Impl.map_entry" by simp |
|
76 |
|
77 (* FIXME: unnecesary type annotations *) |
|
78 quotient_definition map where "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" |
|
79 is "RBT_Impl.map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a, 'b) RBT_Impl.rbt" |
|
80 by simp |
47 by simp |
81 |
48 |
82 (* FIXME: unnecessary type annotations *) |
49 lift_definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.delete" |
83 quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" |
50 by simp |
84 is "RBT_Impl.fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'c \<Rightarrow> 'c" by simp |
51 |
|
52 lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries |
|
53 by simp |
|
54 |
|
55 lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys |
|
56 by simp |
|
57 |
|
58 lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.bulkload" |
|
59 by simp |
|
60 |
|
61 lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map_entry |
|
62 by simp |
|
63 |
|
64 lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map |
|
65 by simp |
|
66 |
|
67 lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" is RBT_Impl.fold |
|
68 by simp |
85 |
69 |
86 export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML |
70 export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML |
87 |
71 |
88 subsection {* Derived operations *} |
72 subsection {* Derived operations *} |
89 |
73 |