/seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
H A D | Intmap.sml | 58 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 D | Binarymap.sml | 59 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 D | Binaryset.sml | 74 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 D | fdd.h | 102 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 D | bvec.h | 93 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 D | Region.sml | 15 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 D | Region.sig | 21 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 D | int-binary-map.sml | 73 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 D | int-binary-map.sml | 73 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 D | int-binary-map.sml | 73 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 D | Binarymap.sml | 128 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 D | heap_wrap.c | 20 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 D | KeyMap.sml | 64 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 D | Map.sml | 56 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 D | KeyMap.sml | 64 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 D | Map.sml | 56 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 D | Table.sml | 103 | 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 D | Redblackmap.sml | 23 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 D | Redblackset.sml | 24 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 D | Heap.h | 28 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 D | fmdiff | 67 exec "$FM" -left "$leftfile" -right "$rightfile"
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
H A D | Map.sml | 33 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 D | Shape.sml | 24 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 D | ForeignTest.c | 39 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 D | yacc.lex | 47 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));
|