/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/ |
H A D | return_sl.c | 9 static long return_sl(long l1, long l2) argument 11 return l1 - l2; 20 unsigned long l1, l2; local 25 values[1] = &l2; 31 l2 = 1073741824L; 34 printf("res: %ld, %ld\n", (long)res, l1 - l2);
|
/seL4-l4v-10.1.1/HOL4/src/sort/ |
H A D | permLib.sig | 12 (* Given a term of the form "PERM l1 l2" this 14 l1 and l2. It knows about APPEND and CONS. 18 PERM_ELIM_DUPLICATES_CONV ``PERM (x::l1++y::l2++l3) (y::l3++z::l2++l4)`` 20 |- PERM (x::l1 ++ y::l2 ++ l3) (y::l3 ++ z::l2 ++ l4) <=> 25 (* Given a term of the form "PERM l1 l2" this 27 l1 and l2. It uses that resorting is allowed inside permutations. 31 PERM_TAKE_DROP_CONV ``PERM (DROP n l1++l2++TAKE n l1) (l1++TAKE n l2 [all...] |
H A D | sortingScript.sml | 52 `!l1 l2. PERM l1 l2 = PERM l2 l1`, 67 `!l1 l2 x. PERM l1 l2 ==> PERM (x::l1) (x::l2)`, 73 (`PERM (x::l1) (x::l2) ==> PERM l1 l2`, 144 `!l1 l2. PERM (APPEND l1 l2) (APPEN [all...] |
H A D | mergesortScript.sml | 18 `!R l1 l2 x y. 20 SORTED R (l1 ++ l2) /\ 22 MEM y l2 31 stable R l1 l2 = 32 !p. (!x y. p x /\ p y ==> R x y) ==> FILTER p l1 = FILTER p l2`; 62 (merge R (x::l1) (y::l2) = 64 x::merge R l1 (y::l2) 66 y::merge R (x::l1) l2)`; 127 (merge_tail negate R (x::l1) (y::l2) acc = 129 merge_tail negate R l1 (y::l2) ( [all...] |
H A D | ternaryComparisonsScript.sml | 63 /\ (list_compare cmp [] l2 = LESS) 65 /\ (list_compare cmp (x::l1) (y::l2) = 68 | EQUAL => list_compare cmp l1 l2 77 !l1 l2. (list_compare cmp l1 l2 = EQUAL) = (l1 = l2)���, 86 /\ (list_merge a_lt [] l2 = l2) 87 /\ (list_merge a_lt (x:'a :: l1) (y::l2) = 89 then x::list_merge a_lt l1 (y::l2) [all...] |
H A D | permLib.sml | 42 val t = ``PERM (x1::l1 ++ (l2 ++ (x2::x3::l3) ++ x4::l4)) (x1::l1 ++ ((x2::x3::l3) ++ x4::l4 ++ l2))`` 43 val t1 = ``x1::x2::x3::(l1 ++ (x2::x3::l3 ++ x4::l4 ++ l2 ++ l4))`` 44 val t2 = ``x1::x2::x8::(x4::l4 ++ l2++l4)`` 127 val l2 = (rand o rand o rhs o concl o valOf) l_thm_opt value 129 SOME (MP (ISPECL [x,l,e,l2] PERM_FUN_CONS_11_SWAP_AT_FRONT) 136 val (l1,l2) = listSyntax.dest_append (rand t) 139 PERM_MOVE_CONS_TO_FRONT e (mk_icomb (PERM_tm, l2)) 145 SOME (MP (ISPECL [l2,l1,e,l1'] PERM_FUN_CONS_APPEND_1) 150 val l2' 174 val l2 = (rand o rhs o concl) thm1; value 211 val l2 = (rand o rand o rhs o concl o valOf) l'_thm_opt value 277 val l2 = (rand o rhs o concl) thm1; value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | temporal_deep_simplificationsLibScript.sml | 639 (!l1 l1' l2 l2'. LTL_EQUIVALENT l1 l1' ==> 640 LTL_EQUIVALENT l2 l2' ==> 641 (LTL_EQUIVALENT_INITIAL l1 l2 = 642 LTL_EQUIVALENT_INITIAL l1' l2')) /\ 654 (!l1 l2 l1' l2'. LTL_EQUIVALENT l1 l1' ==> 655 LTL_EQUIVALENT l2 l2' [all...] |
/seL4-l4v-10.1.1/HOL4/src/tfl/examples/sorting/ |
H A D | partitionScript.sml | 22 `(part P [] l1 l2 = (l1,l2)) 23 /\ (part P (h::rst) l1 l2 = 24 if P h then part P rst (h::l1) l2 25 else part P rst l1 (h::l2))`; 43 `!P L l1 l2 p q. 44 ((p,q) = part P L l1 l2) 45 ==> (LENGTH L + LENGTH l1 + LENGTH l2 = LENGTH p + LENGTH q)`, 54 `!P L l1 l2 p q. 55 ((p,q) = part P L l1 l2) [all...] |
H A D | permScript.sml | 48 `!l1 l2. PERM l1 l2 = PERM l2 l1`, 69 `!l1 l2 x. PERM l1 l2 ==> PERM (x::l1) (x::l2)`, 75 Q.prove(`PERM (x::l1) (x::l2) ==> PERM l1 l2`, 95 `!h l1 l2. APPEND (FILTER ($=h) l1) (h::l2) [all...] |
/seL4-l4v-10.1.1/l4v/tools/autocorres/tools/stats/ |
H A D | profile.zsh | 25 l1=0.0; l2=0.0; hl=0.0; wa=0.0; ts=0.0 30 if [ $stage = '(L2)' ]; then l2=$(($l2 + $time)); fi; 37 printf "L2: %10.3fs\n" "$l2"
|
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | indexedListsScript.sml | 67 ``!l1 l2 f1 f2. 68 l1 = l2 /\ (!x n. MEM x l2 ==> f1 n x = f2 n x) ==> 69 MAPi f1 l1 = MAPi f2 l2``, 74 ``l1 = l2 ==> (!x n. (x = EL n l2) ==> n < LENGTH l2 ==> f1 n x = f2 n x) ==> 75 MAPi f1 l1 = MAPi f2 l2``, 76 map_every qid_spec_tac [`f1`, `f2`, `l2`] >> Induct_on `l1` >> 96 ``!l1 l2 [all...] |
H A D | listScript.sml | 168 (!l1 l2 h. APPEND (h::l1) l2 = h::APPEND l1 l2)���}; 386 ���!l1 l2. ~(l1 = l2) ==> !h1:'a. !h2. ~(h1::l1 = h2::l2)���, 392 ���!h1:'a. !h2. ~(h1 = h2) ==> !l1 l2. ~(h1::l1 = h2::l2)���, 398 ���!h1:'a.!h2.(h1=h2) ==> !l1 l2. (l1 = l2) [all...] |
H A D | listSimps.sml | 50 val (l1, l2) = dest_append t 51 val _ = if is_list l1 andalso is_list l2 then () else raise UNCHANGED 64 val (l1, l2) = dest_append t 66 val _ = if is_list l2 andalso is_list l12 then () else raise UNCHANGED 80 (* |- x1::x2::l1 ++ (SNOC x3 (x4::l2 ++ *) 82 (* [x1; x2] ++ l1 ++ [x4] ++ l2 ++ REVERSE l5 ++ REVERSE l4 ++ *) 108 (* |- x1::x2::l1 ++ (SNOC x3 (x4::l2 ++ *) 110 (* x1::x2::(l1 ++ [x4] ++ l2 ++ REVERSE l5 ++ REVERSE l4 ++ *) 124 val t = ``[x1;x2] ++ l1 ++ l2 ++ [x3] ++ l3 = x1::x2'::l1' ++ l3`` 125 |- ([x1; x2] ++ l1 ++ l2 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/tools/ |
H A D | congToolsLibScript.sml | 9 Define `LIST_AS_SET_CONGRUENCE_RELATION R l1 l2 = 10 ((!x1. MEM x1 l1 ==> (?x2. MEM x2 l2 /\ R x1 x2)) /\ 11 (!x2. MEM x2 l2 ==> (?x1. MEM x1 l1 /\ R x1 x2)))` 24 ``!R. (!x1 x2 x3. (R x1 x2 /\ R x2 x3) ==> R x1 x3) ==> (!l1 l2 l3. LIST_AS_SET_CONGRUENCE_RELATION R l1 l2 /\ LIST_AS_SET_CONGRUENCE_RELATION R l2 l3 ==> LIST_AS_SET_CONGRUENCE_RELATION R l1 l3)``,
|
/seL4-l4v-10.1.1/HOL4/src/update/ |
H A D | updateScript.sml | 95 `!h l1 l2. 97 (FIND (\x. FST x = FST h) (l1 ++ l2) = FIND (\x. FST x = FST h) l2)`, 101 `!y l1 l2. 103 (FIND (\x. FST x = y) (l1 ++ h::l2) = 104 FIND (\x. FST x = y) (l1 ++ l2))`, 108 `!l1 l2 y. 109 ALL_DISTINCT (MAP FST l1) /\ PERM l1 l2 ==> 110 (FIND (\x. FST x = y) l1 = FIND (\x. FST x = y) l2)`, 126 `!l1 l2 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/ |
H A D | quicksort.ml | 5 let l1,l2 = partition (curry $> x) l' in 6 quicksort l1 @ [x] @ quicksort l2 30 (\l [l1;l2]. l1 @ [hd l] @ l2), 58 (\l [l1;l2]. l1 @ [hd l] @ l2),
|
H A D | mux.ml | 16 ?l1 l2 l3. 18 NAND_SPEC(l1,i2,l2) /\ 20 NAND_SPEC(l2,l3,o)");;
|
H A D | PARITY.ml | 49 ?l1 l2 l3 l4 l5. NOT(l2,l1) /\ 50 MUX(in,l1,l2,l3) /\ 51 REG(out,l2) /\ 76 THEN FILTER_ASM_REWRITE_TAC(lines`l2`)[]
|
H A D | RESET_REG.ml | 37 % | |------|l2 % 62 ?l1 l2 l3. ONE l1 /\ 63 MUX(reset,l1,in,l2) /\ 64 REG(l2,l3) /\ 65 MUX(reset,l2,l3,out)");;
|
/seL4-l4v-10.1.1/HOL4/examples/countable/ |
H A D | countableScript.sml | 9 ``���l1 l2 f f'. (l1 = l2) ��� (���x. MEM x l2 ��� (f x = f' x)) ��� (count_list_aux f l1 = count_list_aux f' l2)``,
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | SALScript.sml | 93 (Reduce (l1, ASG l1 v w l2, l2) (w,v)) (* inst *) /\ 94 (Reduce (l1, S1, l2) (v,v) /\ (* nop *) 95 Reduce (l2, S2, l3) value ==> Reduce (l1, S1 |++| S2, l3) value) /\ 96 (Reduce (l1, S1, l2) e1 /\ (* skip *) 97 Reduce (l3, S2, l4) e2 ==> Reduce (l1, S1 |++| S2, l2) e1) /\ 98 (Reduce (l1, S1, l2) (e,v) /\ (* seq *) 99 Reduce (l2, S2, l3) (f v, w) ==> Reduce (l1, S1 |++| S2, l3) 102 Reduce (l1, IFGOTO l1 c l2 l3, l2) ( [all...] |
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl-transformations/ |
H A D | ltl_translationsScript.sml | 15 (LOGIC_TO_TEMPORAL_DEEP (F_CONJ l1 l2) = (LTL_AND (LOGIC_TO_TEMPORAL_DEEP l1, LOGIC_TO_TEMPORAL_DEEP l2))) /\ 18 (LOGIC_TO_TEMPORAL_DEEP (F_U l1 l2) = (LTL_SUNTIL (LOGIC_TO_TEMPORAL_DEEP l1, LOGIC_TO_TEMPORAL_DEEP l2)))`; 75 (TEMPORAL_DEEP_TO_LOGIC (LTL_AND (l1, l2)) = (F_CONJ (TEMPORAL_DEEP_TO_LOGIC l1) (TEMPORAL_DEEP_TO_LOGIC l2))) /\ 79 (TEMPORAL_DEEP_TO_LOGIC (LTL_SUNTIL (l1, l2)) = (F_U (TEMPORAL_DEEP_TO_LOGIC l1) (TEMPORAL_DEEP_TO_LOGIC l2)))`; 150 (TEMPORAL_DEEP_TO_TEMPORAL (LTL_AND (l1, l2)) w = 152 (TEMPORAL_DEEP_TO_TEMPORAL l2 [all...] |
/seL4-l4v-10.1.1/HOL4/src/ring/src/ |
H A D | canonicalScript.sml | 52 (canonical_sum_merge (Cons_monom c1 l1 t1) (Cons_monom c2 l2 t2) = 53 compare (list_compare index_compare l1 l2) 54 (Cons_monom c1 l1 (canonical_sum_merge t1 (Cons_monom c2 l2 t2))) 56 (Cons_monom c2 l2 (canonical_sum_merge (Cons_monom c1 l1 t1) t2))) 57 /\ (canonical_sum_merge (Cons_monom c1 l1 t1) (Cons_varlist l2 t2) = 58 compare (list_compare index_compare l1 l2) 59 (Cons_monom c1 l1 (canonical_sum_merge t1 (Cons_varlist l2 t2))) 61 (Cons_varlist l2 (canonical_sum_merge (Cons_monom c1 l1 t1) t2))) 62 /\ (canonical_sum_merge (Cons_varlist l1 t1) (Cons_monom c2 l2 t2) = 63 compare (list_compare index_compare l1 l2) [all...] |
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttNumber.sml | 67 fun prefix l1 l2 = case (l1,l2) of 75 fun replace_at (l1,lrep) l2 = case l2 of 79 let val r = prefix l1 l2 in lrep @ r end
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/MISC/ |
H A D | mk_COUNT.ml | 35 "COUNT_IMP (sw,i,o) = ?l1 l2. 36 MUX (sw,i,l2,l1) /\ 38 INCR (o,l2)");;
|