source: src/ERTL/VariableSet.ma @ 752

Last change on this file since 752 was 746, checked in by mulligan, 9 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 
1include "ERTL/ERTL.ma".
2include "utilities/BitVectorTrieSet.ma".
3
4definition VariableSet ≝ (BitVectorTrieSet 16) × (BitVectorTrieSet 16).
5
6definition VariableProperty ≝ (BitVectorTrieSet 16) × (BitVectorTrieSet 16).
7
8definition vs_bottom ≝ 〈set_empty 16, set_empty 16〉.
9
10definition vs_p_singleton ≝
11  λar: AbstractRegister.
12  match ar with [
13  mkAbstractRegister r ⇒ 〈set_singleton ? r, set_empty 16〉
14  ].
15 
16definition vs_h_singleton ≝
17  λr: Register.
18  let index ≝ word_of_register r in
19    〈set_empty 16, set_singleton ? index〉.
20   
21definition join: VariableSet → VariableSet → VariableSet ≝
22  λvs1: VariableSet.
23  λvs2: VariableSet.
24    〈set_union ? (\fst vs1) (\fst vs2), set_union ? (\snd vs1) (\snd vs2)〉.
25   
26definition vs_is_maximal ≝ λA: Type[0]. λa: A. false.
27
28definition 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   
33definition 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.