1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
implementation module typeproperties
import StdEnv
import general, compare_types
:: TypeClassification =
{ tc_signs :: TypeSignTree
, tc_props :: TypePropTree
}
:: SignClassification =
{ sc_pos_vect :: !BITVECT
, sc_neg_vect :: !BITVECT
}
/*
IsPositive sign_class index :== sign_class.sc_pos_vect bitand (1 << index) <> 0
IsNegative sign_class index :== sign_class.sc_neg_vect bitand (1 << index) <> 0
*/
:: PropClassification :== BITVECT
TopSignClass :== { sc_pos_vect = bitnot 0, sc_neg_vect = bitnot 0 }
ArrowSignClass :== { sc_pos_vect = 2, sc_neg_vect = 1 }
PosSignClass :== { sc_pos_vect = bitnot 0, sc_neg_vect = 0 }
:: Sign =
{ pos_sign :: !Bool
, neg_sign :: !Bool
}
TopSign :== { pos_sign = True, neg_sign = True }
BottomSign :== { pos_sign = False, neg_sign = False }
PositiveSign :== { pos_sign = True, neg_sign = False }
NegativeSign :== { pos_sign = False, neg_sign = True }
:: TypeSign key =
{ ts_cons_var_signs :: !key
, ts_type_sign :: !SignClassification
}
:: TypeProp key =
{ ts_cons_var_props :: !key
, ts_type_prop :: !PropClassification
}
:: VarBind a key =
{ vb_number :: !key
, vb_value :: !a
}
:: TypeSignTree :== BinTree (TypeSign [SignClassification])
:: TypePropTree :== BinTree (TypeProp [PropClassification])
:: EnvTree a :== BinTree (VarBind a Int)
:: BinTree a = BT_Node !a !(BinTree a) !(BinTree a) | BT_Empty
class key m :: (m a) -> a
instance key TypeSign
where
key {ts_cons_var_signs} = ts_cons_var_signs
instance key TypeProp
where
key {ts_cons_var_props} = ts_cons_var_props
instance key (VarBind a)
where
key {vb_number} = vb_number
EmptyTypeClassification :: TypeClassification
EmptyTypeClassification = { tc_signs = BT_Empty, tc_props = BT_Empty }
treeInsert :: !k !(m k) !(BinTree (m k)) -> BinTree (m k) | =< k & key m
treeInsert new_key el BT_Empty
= BT_Node el BT_Empty BT_Empty
treeInsert new_key new_el tree=:(BT_Node el left right)
# cmp = new_key =< key el
| cmp == Smaller
= BT_Node el (treeInsert new_key new_el left) right
= BT_Node el left (treeInsert new_key new_el right)
treeRetrieve :: !k !(BinTree (m k)) -> Optional (m k) | =< k & key m
treeRetrieve search_key BT_Empty
= No
treeRetrieve search_key tree=:(BT_Node el left right)
# cmp = search_key =< key el
| cmp == Equal
= Yes el
| cmp == Smaller
= treeRetrieve search_key left
= treeRetrieve search_key right
signClassToSign :: !SignClassification !Int -> Sign
signClassToSign {sc_pos_vect,sc_neg_vect} index
= { pos_sign = sc_pos_vect bitand (1 << index) <> 0, neg_sign = sc_neg_vect bitand (1 << index) <> 0}
instance <<< Sign
where
(<<<) file {pos_sign,neg_sign}
| pos_sign
| neg_sign
= file <<< "T"
= file <<< "+"
| neg_sign
= file <<< "-"
= file <<< "L"
instance =< SignClassification
where
=< sc1 sc2
| sc1.sc_pos_vect == sc2.sc_pos_vect
| sc1.sc_neg_vect == sc2.sc_neg_vect
= Equal
| sc1.sc_neg_vect < sc2.sc_neg_vect
= Smaller
= Greater
| sc1.sc_pos_vect < sc2.sc_pos_vect
= Smaller
= Greater
retrieveSignClassification :: ![SignClassification] !TypeClassification -> Optional (TypeSign [SignClassification])
retrieveSignClassification cons_classes {tc_signs}
= treeRetrieve cons_classes tc_signs
addSignClassification :: ![SignClassification] !SignClassification !TypeClassification -> TypeClassification
addSignClassification hio_signs sign_class tc=:{tc_signs}
= { tc & tc_signs = treeInsert hio_signs { ts_cons_var_signs = hio_signs, ts_type_sign = sign_class } tc_signs }
retrievePropClassification :: ![PropClassification] !TypeClassification -> Optional (TypeProp [PropClassification])
retrievePropClassification cons_classes {tc_props}
= treeRetrieve cons_classes tc_props
addPropClassification :: ![PropClassification] !PropClassification !TypeClassification -> TypeClassification
addPropClassification hio_props prop_class tc=:{tc_props}
= { tc & tc_props = treeInsert hio_props { ts_cons_var_props = hio_props, ts_type_prop = prop_class } tc_props }
instance * Sign
where
(*) sign1 sign2
| sign1.pos_sign
| sign1.neg_sign
= sign1
= sign2
| sign1.neg_sign
= { pos_sign = sign2.neg_sign, neg_sign = sign2.pos_sign }
= sign1
/*
= { pos_sign = sign1.pos_sign * sign2.pos_sign || sign1.neg_sign * sign2.neg_sign,
neg_sign = sign1.pos_sign * sign2.neg_sign || sign1.neg_sign * sign2.pos_sign }
instance * Bool
where
(*) b1 b2 = b1 && b2 || not b1 && not b2
*/
|
