Searched refs:swap (Results 1 - 25 of 82) sorted by relevance

1234

/seL4-l4v-master/l4v/tools/c-parser/testfiles/errors/
H A Daddrlocal.c7 void swap(int *i1, int *i2) function
20 swap(&i, &j);
/seL4-l4v-master/l4v/tools/c-parser/testfiles/
H A Dptr_umm.c7 int swap(int *i, int *j) function
H A Dswap.c10 PROC swap(\<acute>p,\<acute>q)
14 void swap(unsigned int *p, unsigned int *q) function
33 swap(a,b);
34 swap(c,a);
/seL4-l4v-master/l4v/tools/autocorres/doc/quickstart/
H A Dswap.c11 void swap(unsigned *a, unsigned *b) function
/seL4-l4v-master/l4v/tools/autocorres/tests/examples/
H A Dswap.c7 void swap(unsigned *a, unsigned *b) function
/seL4-l4v-master/HOL4/examples/lambda/other-models/
H A DswapScript.sml5 val _ = new_theory "swap"
112 val swap_def = new_specification("swap_def", ["swap"], thm1);
116 ``!t. swap x x t = t``,
123 ``!t. swap x y t = swap y x t``,
131 ``!t. ~(v IN FV t) ==> ([VAR v/u] t = swap v u t)``,
156 ``!t u v. FV (swap u v t) = swapset u v (FV t)``,
168 ``!t x y. size (swap x y t) = size t``,
187 ``!t u v x y. swap u v ([VAR x/y] t) =
188 [VAR (swapstr u v x)/swapstr u v y] (swap
[all...]
/seL4-l4v-master/HOL4/examples/pgcl/src/
H A DposrealTools.sml188 fun bubble is_op swap inv tm =
200 else REWR_CONV swap THENC RAND_CONV (bubble is_op swap inv)
203 fun sort is_op swap inv tm =
205 else RAND_CONV (sort is_op swap inv) THENC bubble is_op swap inv) tm;
207 fun permute is_op assoc rid swap inv =
210 THENC sort is_op swap inv;
212 fun permute_conv is_op assoc rid swap inv tm =
213 (if is_op tm then permute is_op assoc rid swap in
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw/
H A DUTuple.sml16 fun swap (x,y) = (y,x) function
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DUTuple.sml16 fun swap (x,y) = (y,x) function
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/
H A DUTuple.sml16 fun swap (x,y) = (y,x) function
/seL4-l4v-master/l4v/tools/c-parser/standalone-parser/
H A Dbasics.sml117 fun swap (x,y) = (y,x) function
131 (subset eq (xs,ys) andalso subset (eq o swap) (ys,xs))
/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/
H A DL3.sig45 val swap : 'a * 'b -> 'b * 'a value
H A DL3.sml109 fun swap (n, l) = (l, n) function
/seL4-l4v-master/HOL4/examples/fsub/
H A DfsubtypesScript.sml17 This theory establishes the type, along with swap functions for the type
158 (* definition of swap *)
160 fswap x y ty = term2fsubty (swap x y (fsubty2term ty))
165 ``!t. fsubrep t ==> !x y. fsubrep (swap x y t)``,
200 (* define swap over contexts *)
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/
H A Dcheney_allocScript.sml46 ``!i j. bijection (swap i j)``,
468 (apply (swap i j) s = s)``,
584 \\ Q.EXISTS_TAC `b' o swap i' (k (fresh h))`
587 \\ ASM_SIMP_TAC bool_ss [METIS_PROVE [swap_def] ``!i k. swap i k i = k``]
596 \\ `(MAP b' (MAP (swap i' (k (fresh h))) t) = t2::ts)` by
652 \\ `swap i' (k (fresh h)) o swap i' (k (fresh h)) = I` by METIS_TAC [swap_swap]
654 \\ (ASSUME_TAC o UNDISCH_ALL o Q.SPECL [`swap i' (k (fresh h))`,`swap i' (k (fresh h))`]) apply_INSERT
656 \\ `swap
[all...]
H A Dcheney_gcScript.sml188 swap i j = \k. if k = i then j else if k = j then i else k`;
191 ``!i:'a j. swap i j o swap i j = I``,
197 ``!i:'a j x. swap i j (swap i j x) = x``,
203 ``!i j k. ~(i = k) /\ ~(j = k) ==> (swap i j k = k)``,
235 (ADDR k (swap j x t) (((x =+ REF j) ((j =+ (DATA (n',n'',d'))) m)) k) =
285 (((x =+ REF j) ((j =+ DATA (n',n'',d')) m) (swap j x a) = DATA (k,k',v)) =
296 (apply (swap j x) (abs((x =+ REF j) ((j =+ m x) m))) = abs m)``,
310 ``!i j s t. (apply (swap
[all...]
/seL4-l4v-master/HOL4/examples/lambda/basics/
H A Dnomdatatype.sml15 fun list_mk_icomb(f, args) = List.foldl (mk_icomb o swap) f args
70 val union = List.foldl (mk_union o swap) (hd sets) (tl sets)
120 val list_mk_icomb = uncurry (List.foldl (mk_icomb o swap))
H A DbinderLib.sml458 ("Couldn't prove function with swap over range - \n\
466 ("Couldn't prove function with swap over range - \n\
492 ("Couldn't prove function with swap over range - \n\
504 ("Couldn't prove function with swap over range - \n\
/seL4-l4v-master/HOL4/examples/imperative/
H A Dnecec2010.sml290 A useful function on state spaces is the swap command which is defined as:
311 val _ = tprint ("swap is possible with introduction of temporary variable: " );
388 In the special case where both variables are numbers, an algebraic method can be used to swap the values without the use of a temporary variable.
397 val _ = tprint ("swap is possible for num type without need for temporary variable: " );
/seL4-l4v-master/HOL4/examples/AI_TNN/
H A DmleArithData.sml157 let val d = dregroup Int.compare (map swap (map_assoc f tml)) in
/seL4-l4v-master/HOL4/examples/machine-code/lisp/
H A Dlisp_opsScript.sml377 val swap = swap_thm i value
378 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc))
379 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap))
412 val swap = swap_thm i value
413 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc))
414 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap))
445 val swap = swap_thm i value
446 val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc))
447 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap))
484 val swap value
511 val swap = swap_thm i value
538 val swap = swap_thm i value
[all...]
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DUseful.sig57 val swap : 'a * 'b -> 'b * 'a value
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DUseful.sig57 val swap : 'a * 'b -> 'b * 'a value
/seL4-l4v-master/HOL4/src/AI/proof_search/
H A DpsBigSteps.sml53 dnew (#board_compare game) (map swap (map_snd #board (dlist tree)))
/seL4-l4v-master/HOL4/src/metis/
H A DmlibRewrite.sml188 fun redex_residue lr th = (if lr then I else swap) (dest_unit_eq th);
265 else foldl (fst o rewr_lit neqs o swap) th rest

Completed in 226 milliseconds

1234