|
Last change
on this file since 950 was
746,
checked in by mulligan, 10 years ago
|
|
Changes to bitvectortrieset: equality on sets. Added new file for translation of variable set functor. other small changes.
|
|
File size:
1.2 KB
|
| Line | |
|---|
| 1 | include "ERTL/ERTL.ma". |
|---|
| 2 | include "utilities/BitVectorTrieSet.ma". |
|---|
| 3 | |
|---|
| 4 | definition VariableSet ≝ (BitVectorTrieSet 16) × (BitVectorTrieSet 16). |
|---|
| 5 | |
|---|
| 6 | definition VariableProperty ≝ (BitVectorTrieSet 16) × (BitVectorTrieSet 16). |
|---|
| 7 | |
|---|
| 8 | definition vs_bottom ≝ 〈set_empty 16, set_empty 16〉. |
|---|
| 9 | |
|---|
| 10 | definition vs_p_singleton ≝ |
|---|
| 11 | λar: AbstractRegister. |
|---|
| 12 | match ar with [ |
|---|
| 13 | mkAbstractRegister r ⇒ 〈set_singleton ? r, set_empty 16〉 |
|---|
| 14 | ]. |
|---|
| 15 | |
|---|
| 16 | definition vs_h_singleton ≝ |
|---|
| 17 | λr: Register. |
|---|
| 18 | let index ≝ word_of_register r in |
|---|
| 19 | 〈set_empty 16, set_singleton ? index〉. |
|---|
| 20 | |
|---|
| 21 | definition join: VariableSet → VariableSet → VariableSet ≝ |
|---|
| 22 | λvs1: VariableSet. |
|---|
| 23 | λvs2: VariableSet. |
|---|
| 24 | 〈set_union ? (\fst vs1) (\fst vs2), set_union ? (\snd vs1) (\snd vs2)〉. |
|---|
| 25 | |
|---|
| 26 | definition vs_is_maximal ≝ λA: Type[0]. λa: A. false. |
|---|
| 27 | |
|---|
| 28 | definition vs_eq: VariableSet → VariableSet → bool ≝ |
|---|
| 29 | λvs1: VariableSet. |
|---|
| 30 | λvs2: VariableSet. |
|---|
| 31 | andb (set_eq ? (\fst vs1) (\fst vs2)) (set_eq ? (\snd vs1) (\snd vs2)). |
|---|
| 32 | |
|---|
| 33 | definition vs_diff: VariableSet → VariableSet → VariableSet ≝ |
|---|
| 34 | λvs1: VariableSet. |
|---|
| 35 | λvs2: VariableSet. |
|---|
| 36 | 〈set_diff ? (\fst vs1) (\fst vs2), set_diff ? (\snd vs1) (\snd vs2)〉. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
