Searched refs:right (Results 1 - 25 of 370) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/portableML/poly/
H A DIntmap.sml58 right: 'a intmap}
64 fun N(k,v,E,E) = T{key=k,value=v,cnt=1,left=E,right=E}
65 | N(k,v,E,r as T n) = T{key=k,value=v,cnt=1+(#cnt n),left=E,right=r}
66 | N(k,v,l as T n,E) = T{key=k,value=v,cnt=1+(#cnt n),left=l,right=E}
68 T{key=k,value=v,cnt=1+(#cnt n)+(#cnt n'),left=l,right=r}
70 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) =
73 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) =
76 fun double_L (a,av,w,T{key=c,value=cv,left=T{key=b,value=bv,left=x,right=y,...},right=z,...}) =
79 fun double_R (c,cv,T{key=a,value=av,left=w,right
[all...]
/seL4-l4v-10.1.1/HOL4/tools-poly/poly/
H A DBinarymap.sml59 right : ('key, 'a) tree}
67 fun N(k,v,E,E) = T{key=k,value=v,cnt=1,left=E,right=E}
68 | N(k,v,E,r as T n) = T{key=k,value=v,cnt=1+(#cnt n),left=E,right=r}
69 | N(k,v,l as T n,E) = T{key=k,value=v,cnt=1+(#cnt n),left=l,right=E}
71 T{key=k,value=v,cnt=1+(#cnt n)+(#cnt n'),left=l,right=r}
73 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) =
76 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) =
80 left=T{key=b,value=bv,left=x,right=y,...},
81 right=z,...}) =
85 right
[all...]
H A DBinaryset.sml74 right : 'item tree}
84 fun mkT(v,n,l,r) = T{elt=v,cnt=n,left=l,right=r}
92 fun single_L (a,x,T{elt=b,left=y,right=z,...}) = N(b,N(a,x,y),z)
94 fun single_R (b,T{elt=a,left=x,right=y,...},z) = N(a,x,N(b,y,z))
96 fun double_L (a,w,T{elt=c,left=T{elt=b,left=x,right=y,...},right=z,...}) =
99 fun double_R (c,T{elt=a,left=w,right=T{elt=b,left=x,right=y,...},...},z) =
110 | T' (v,E,r as T{left=E,right=E,...}) = mkT(v,2,E,r)
111 | T' (v,l as T{left=E,right
[all...]
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/
H A Dfdd.h102 inline bdd fdd_equalspp(int left, int right) argument
103 { return fdd_equals(left, right); }
127 inline bdd* fdd_add(int bitnum, bdd *left, bdd *right)
128 { return fdd_termopr(bitnum, left, right,bdd::fddAdd); }
130 inline bdd* fdd_sub(int bitnum, bdd *left, bdd *right)
131 { return fdd_termopr(bitnum, left, right,bdd::fddSub); }
139 inline bdd fdd_lth(int bitnum, bdd *left, bdd *right)
140 { return fdd_relopr(bitnum, left, right, bdd::fddLth); }
142 inline bdd fdd_lte(int bitnum, bdd *left, bdd *right)
143 { return fdd_relopr(bitnum, left, right, bd
[all...]
H A Dbvec.h93 extern BVEC bvec_add(BVEC left, BVEC right);
94 extern BVEC bvec_sub(BVEC left, BVEC right);
96 extern BVEC bvec_mul(BVEC left, BVEC right);
98 extern int bvec_div(BVEC left, BVEC right, BVEC *res, BVEC *rem);
103 extern BDD bvec_lth(BVEC left, BVEC right);
104 extern BDD bvec_lte(BVEC left, BVEC right);
105 extern BDD bvec_gth(BVEC left, BVEC right);
106 extern BDD bvec_gte(BVEC left, BVEC right);
107 extern BDD bvec_equ(BVEC left, BVEC right);
108 extern BDD bvec_neq(BVEC left, BVEC right);
229 bvec_add(const bvec &left, const bvec &right) argument
232 bvec_sub(const bvec &left, const bvec &right) argument
238 bvec_mul(const bvec &left, const bvec &right) argument
250 bvec_shl(const bvec &left, const bvec &right, const bdd &c) argument
256 bvec_shr(const bvec &left, const bvec &right, const bdd &c) argument
259 bvec_lth(const bvec &left, const bvec &right) argument
262 bvec_lte(const bvec &left, const bvec &right) argument
265 bvec_gth(const bvec &left, const bvec &right) argument
268 bvec_gte(const bvec &left, const bvec &right) argument
271 bvec_equ(const bvec &left, const bvec &right) argument
274 bvec_neq(const bvec &left, const bvec &right) argument
[all...]
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DRegion.sml15 right: SourcePos.t}
26 val right = make #right value
31 | (T {left, ...}, right) => T {left = left, right = right}
35 | T {left, right} =>
37 SourcePos.posToString left, "-", SourcePos.posToString right]
44 | (T {left, ...}, T {right, ...}) => T {left = left, right
[all...]
H A DRegion.sig21 val make: {left: SourcePos.t, right: SourcePos.t} -> t
22 val right: t -> SourcePos.t option value
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A Dint-binary-map.sml73 right : 'a map
80 fun N(k,v,E,E) = T{key=k,value=v,cnt=1,left=E,right=E}
81 | N(k,v,E,r as T n) = T{key=k,value=v,cnt=1+(#cnt n),left=E,right=r}
82 | N(k,v,l as T n,E) = T{key=k,value=v,cnt=1+(#cnt n),left=l,right=E}
84 T{key=k,value=v,cnt=1+(#cnt n)+(#cnt n'),left=l,right=r}
86 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) =
89 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) =
92 fun double_L (a,av,w,T{key=c,value=cv,left=T{key=b,value=bv,left=x,right=y,...},right=z,...}) =
95 fun double_R (c,cv,T{key=a,value=av,left=w,right
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A Dint-binary-map.sml73 right : 'a map
80 fun N(k,v,E,E) = T{key=k,value=v,cnt=1,left=E,right=E}
81 | N(k,v,E,r as T n) = T{key=k,value=v,cnt=1+(#cnt n),left=E,right=r}
82 | N(k,v,l as T n,E) = T{key=k,value=v,cnt=1+(#cnt n),left=l,right=E}
84 T{key=k,value=v,cnt=1+(#cnt n)+(#cnt n'),left=l,right=r}
86 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) =
89 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) =
92 fun double_L (a,av,w,T{key=c,value=cv,left=T{key=b,value=bv,left=x,right=y,...},right=z,...}) =
95 fun double_R (c,cv,T{key=a,value=av,left=w,right
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/
H A Dint-binary-map.sml73 right : 'a map
80 fun N(k,v,E,E) = T{key=k,value=v,cnt=1,left=E,right=E}
81 | N(k,v,E,r as T n) = T{key=k,value=v,cnt=1+(#cnt n),left=E,right=r}
82 | N(k,v,l as T n,E) = T{key=k,value=v,cnt=1+(#cnt n),left=l,right=E}
84 T{key=k,value=v,cnt=1+(#cnt n)+(#cnt n'),left=l,right=r}
86 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) =
89 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) =
92 fun double_L (a,av,w,T{key=c,value=cv,left=T{key=b,value=bv,left=x,right=y,...},right=z,...}) =
95 fun double_R (c,cv,T{key=a,value=av,left=w,right
[all...]
/seL4-l4v-10.1.1/HOL4/developers/mlton-srcs/
H A DBinarymap.sml128 right : ('key, 'a) tree}
136 fun N(k,v,E,E) = T{key=k,value=v,cnt=1,left=E,right=E}
137 | N(k,v,E,r as T n) = T{key=k,value=v,cnt=1+(#cnt n),left=E,right=r}
138 | N(k,v,l as T n,E) = T{key=k,value=v,cnt=1+(#cnt n),left=l,right=E}
140 T{key=k,value=v,cnt=1+(#cnt n)+(#cnt n'),left=l,right=r}
142 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) =
145 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) =
149 left=T{key=b,value=bv,left=x,right=y,...},
150 right=z,...}) =
154 right
[all...]
/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/examples/
H A Dheap_wrap.c20 struct thing *right; member in struct:thing
37 t->right = t->left + 1;
58 return l->p->x && t->left->right->x;
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DKeyMap.sml64 right : 'value tree};
83 | T (Node {size,left,right,...}) =>
86 and r = checkSizes right
96 | T (Node {left,key,right,...}) =>
111 checkSorted x right
119 val Node {left,right,...} = node
129 case checkPriorities right of
133 else raise Bug "right child has greater priority"
165 fun mkNode priority left key value right =
167 val size = treeSize left + 1 + treeSize right
221 and right = E value
270 val right = treeAppend right tree2 value
502 and right = treeDelete dkey right value
531 and right = treeMapPartial f right value
553 and right = treeMap f right value
584 and right = treeMerge f1 f2 fb r right value
622 and right = treeUnion f f2 r right value
658 and right = treeIntersect f r right value
691 and right = treeUnionDomain r right value
719 and right = treeIntersectDomain r right value
746 and right = treeDifferenceDomain right r value
[all...]
H A DMap.sml56 right : ('key,'value) tree};
75 | T (Node {size,left,right,...}) =>
78 and r = checkSizes right
88 | T (Node {left,key,right,...}) =>
103 checkSorted compareKey x right
111 val Node {left,right,...} = node
121 case checkPriorities compareKey right of
125 else raise Bug "right child has greater priority"
157 fun mkNode priority left key value right =
159 val size = treeSize left + 1 + treeSize right
213 and right = E value
262 val right = treeAppend right tree2 value
494 and right = treeDelete compareKey dkey right value
523 and right = treeMapPartial f right value
545 and right = treeMap f right value
576 and right = treeMerge compareKey f1 f2 fb r right value
614 and right = treeUnion compareKey f f2 r right value
650 and right = treeIntersect compareKey f r right value
683 and right = treeUnionDomain compareKey r right value
711 and right = treeIntersectDomain compareKey r right value
738 and right = treeDifferenceDomain compareKey right r value
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DKeyMap.sml64 right : 'value tree};
83 | T (Node {size,left,right,...}) =>
86 and r = checkSizes right
96 | T (Node {left,key,right,...}) =>
111 checkSorted x right
119 val Node {left,right,...} = node
129 case checkPriorities right of
133 else raise Bug "right child has greater priority"
165 fun mkNode priority left key value right =
167 val size = treeSize left + 1 + treeSize right
221 and right = E value
270 val right = treeAppend right tree2 value
502 and right = treeDelete dkey right value
531 and right = treeMapPartial f right value
553 and right = treeMap f right value
584 and right = treeMerge f1 f2 fb r right value
622 and right = treeUnion f f2 r right value
658 and right = treeIntersect f r right value
691 and right = treeUnionDomain r right value
719 and right = treeIntersectDomain r right value
746 and right = treeDifferenceDomain right r value
[all...]
H A DMap.sml56 right : ('key,'value) tree};
75 | T (Node {size,left,right,...}) =>
78 and r = checkSizes right
88 | T (Node {left,key,right,...}) =>
103 checkSorted compareKey x right
111 val Node {left,right,...} = node
121 case checkPriorities compareKey right of
125 else raise Bug "right child has greater priority"
157 fun mkNode priority left key value right =
159 val size = treeSize left + 1 + treeSize right
213 and right = E value
262 val right = treeAppend right tree2 value
494 and right = treeDelete compareKey dkey right value
523 and right = treeMapPartial f right value
545 and right = treeMap f right value
576 and right = treeMerge compareKey f1 f2 fb r right value
614 and right = treeUnion compareKey f f2 r right value
650 and right = treeIntersect compareKey f r right value
683 and right = treeUnionDomain compareKey r right value
711 and right = treeIntersectDomain compareKey r right value
738 and right = treeDifferenceDomain compareKey right r value
[all...]
/seL4-l4v-10.1.1/HOL4/src/portableML/
H A DTable.sml103 | map (Branch2 (left, (k, x), right)) =
104 Branch2 (map left, (k, f k x), map right)
105 | map (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
106 Branch3 (map left, (k1, f k1 x1), map mid, (k2, f k2 x2), map right);
112 | fold (Branch2 (left, p, right)) x =
113 fold right (f p (fold left x))
114 | fold (Branch3 (left, p1, mid, p2, right)) x =
115 fold right (f p2 (fold mid (f p1 (fold left x))));
121 | fold (Branch2 (left, p, right)) x =
122 fold left (f p (fold right
[all...]
H A DRedblackmap.sml23 let fun loopShared k x left right =
27 | GREATER => loop right
29 | loop (RED(k, x, left, right)) = loopShared k x left right
30 | loop (BLACK(k, x, left, right)) = loopShared k x left right
42 | lbalance k x left right = BLACK(k, x, left, right)
48 | rbalance k x left right = BLACK(k, x, left, right)
[all...]
H A DRedblackset.sml24 let fun memShared x left right =
28 | GREATER => mem right
30 | mem (RED(x, left, right)) = memShared x left right
31 | mem (BLACK(x, left, right)) = memShared x left right
42 | lbalance x left right = BLACK(x, left, right)
48 | rbalance x left right = BLACK(x, left, right)
[all...]
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/
H A DHeap.h28 static inline int right (int i) { return i+i + 1; } function
54 int child = right(i) < heap.size() && comp(heap[right(i)],heap[left(i)]) ? right(i) : left(i);
95 || ((parent(i) == 0 || !comp(heap[i],heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); }
/seL4-l4v-10.1.1/l4v/misc/filemerge/
H A Dfmdiff67 exec "$FM" -left "$leftfile" -right "$rightfile"
/seL4-l4v-10.1.1/HOL4/examples/elliptic/
H A DMap.sml33 right : 'c};
57 left = E, key = key, value = value, right = E};
77 | checkSizes (T {size,left,right,...}) =
80 and r = checkSizes right
87 | checkSorted cmp x (T {left,key,right,...}) =
99 checkSorted cmp (SOME key) right
103 | checkPriorities cmp (T (x as {left,right,...})) =
114 case checkPriorities cmp right of
119 | EQUAL => raise Error "right child has equal key"
120 | GREATER => raise Error "right chil
421 and right = treeMapPartial cmp f right value
440 and right = treeMap f right value
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/
H A DShape.sml24 type RECT = { top: int, left: int, bottom: int, right: int }
52 fun Chord (h,{left,top,right,bottom}: RECT,{x=x1,y=y1}: POINT,{x=x2,y=y2}: POINT) =
53 chord (h,left,top,right,bottom,x1,y1,x2,y2)
60 fun Ellipse (h,{left,top,right,bottom}: RECT) =
61 ellipse(h,left,top,right,bottom)
69 fun Pie (h,{left,top,right,bottom}: RECT,{x=x1,y=y1}: POINT,{x=x2,y=y2}: POINT) =
70 pie(h,left,top,right,bottom,x1,y1,x2,y2)
90 fun Rectangle(h,{left,top,right,bottom}: RECT) =
91 rectangle(h,left,top,right,bottom)
98 fun RoundRect(h,{left,top,right,botto
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/samplecode/Foreign/
H A DForeignTest.c39 struct _tree *left, *right; member in struct:_tree
46 else return t->nValue + SumTree(t->left) + SumTree(t->right);
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/
H A Dyacc.lex47 fn (s,left,right) =>
48 let fun f ((a,d)::b) = if a=s then d(left,right) else f b
49 | f nil = UNKNOWN(s,left,right)
92 <A>"%right" => (PREC(Hdr.RIGHT,!lineno,!lineno));

Completed in 111 milliseconds

1234567891011>>