/seL4-l4v-master/seL4/src/arch/arm/armv/armv8-a/64/ |
H A D | cache.c | 64 int assoc = ASSOC(lsize); local 65 int assoc_bits = wordBits - clzl(assoc - 1); 67 for (int w = 0; w < assoc; w++) { 81 int assoc = ASSOC(lsize); local 82 int assoc_bits = wordBits - clzl(assoc - 1); 85 for (int w = 0; w < assoc; w++) {
|
/seL4-l4v-master/HOL4/src/num/arith/src/ |
H A D | GenPolyCanon.sml | 11 assoc : thm (* right to left *), 24 fun update_mode m (GCI {dest,is_literal,assoc,symassoc,comm,assoc_mode, 27 GCI {dest = dest, is_literal = is_literal, comm = comm, assoc = assoc, 34 val {dest,non_coeff,comm,assoc,symassoc,merge,postnorm,is_literal,...} = g 41 (l', (fn c => REWR_CONV assoc THENC LAND_CONV c), LAND_CONV, 99 REWR_CONV assoc THENC la_recurse 112 REWR_CONV assoc THENC LAND_CONV REDUCE_CONV 137 val assoc = SPEC_ALL assoc0 value 141 REWR_CONV assoc)) asso 144 val assoc = SPEC_ALL assoc0 value [all...] |
H A D | GenPolyCanon.sig | 11 assoc : thm, 47 assoc : associativity theorem (e.g., |- x + (y + z) = (x + y) + z) 83 [derive_l_asscomm ass comm] derives an l_asscomm theorem from assoc and comm 86 [derive_r_asscomm ass comm] derives an r_asscomm theorem from assoc and comm
|
H A D | NumRelNorms.sml | 40 assoc = ADD_ASSOC, 55 assoc = ADD_ASSOC, 101 assoc = MULT_ASSOC,
|
/seL4-l4v-master/seL4/src/arch/arm/armv/armv7-a/ |
H A D | cache.c | 58 /* Associativity, field is assoc - 1. */ 74 int assoc = ASSOC(s); local 75 int assoc_bits = wordBits - clzl(assoc - 1); 79 for (w = 0; w < assoc; w++) { 95 int assoc = ASSOC(s); local 96 int assoc_bits = wordBits - clzl(assoc - 1); 100 for (w = 0; w < assoc; w++) {
|
/seL4-l4v-master/seL4/src/arch/arm/armv/armv8-a/32/ |
H A D | cache.c | 58 /* Associativity, field is assoc - 1. */ 74 int assoc = ASSOC(s); local 75 int assoc_bits = wordBits - clzl(assoc - 1); 79 for (w = 0; w < assoc; w++) { 95 int assoc = ASSOC(s); local 96 int assoc_bits = wordBits - clzl(assoc - 1); 100 for (w = 0; w < assoc; w++) {
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | AC_Sort.sml | 22 fun balance (dest,mk) assoc t = let 34 val btree_norm = QCONV (PURE_REWRITE_CONV [assoc]) (recurse ts) 35 val t_norm = QCONV (PURE_REWRITE_CONV [assoc]) t 42 fun sort {cmp, combine, dest, mk, assoc, comm, preprocess} = let 43 val wassoc = REWR_CONV assoc 44 val wassoc' = REWR_CONV (GSYM assoc) 77 balance (dest, mk) assoc THENC recurse 104 assoc = DISJ_ASSOC, 141 assoc = integerTheory.INT_MUL_ASSOC, combine = intcombine,
|
H A D | AC_Sort.sig | 5 val sort : {assoc : thm, comm : thm, 14 [sort {assoc,comm,dest,mk,cmp,combine,preprocess}] is a conversion for 20 assoc: associativity theorem in standard r-to-l format:
|
/seL4-l4v-master/HOL4/src/refute/ |
H A D | AC.sml | 128 let fun MK_ASSOC_CONV oper assoc t1 t2 t3 = 136 val ppth = INST [t1 |-> l,t2 |-> r, t3 |-> rtm] assoc 148 (INST [t1|->l, t2|->r, t3|->rand(rator(concl ath))] assoc) rth 154 let val assoc = SYM(SPEC_ALL rassoc) value 155 val (opt1,t23) = dest_comb(rand(concl(assoc))) 160 then MK_ASSOC_CONV oper assoc t1 t2 t3 166 val assoc' = Thm.INST_TYPE tyin assoc 171 MK_ASSOC_CONV xop assoc' t1' t2' t3' tm
|
/seL4-l4v-master/HOL4/src/datatype/theory_tests/ |
H A D | recordEnumSimpsBScript.sml | 28 ^(#accessor (Lib.assoc "fld2" (TypeBase.fields_of ���:'a Record���)))
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Print.sig | 156 datatype assoc = type 165 assoc : assoc} list 169 val layerInfixes : infixes -> {tokens : StringSet.set, assoc : assoc} list
|
H A D | Term.sml | 371 {token = "/", precedence = 7, assoc = Print.LeftAssoc}, 372 {token = "div", precedence = 7, assoc = Print.LeftAssoc}, 373 {token = "mod", precedence = 7, assoc = Print.LeftAssoc}, 374 {token = "*", precedence = 7, assoc = Print.LeftAssoc}, 375 {token = "+", precedence = 6, assoc = Print.LeftAssoc}, 376 {token = "-", precedence = 6, assoc = Print.LeftAssoc}, 377 {token = "^", precedence = 6, assoc = Print.LeftAssoc}, 378 {token = "@", precedence = 5, assoc = Print.RightAssoc}, 379 {token = "::", precedence = 5, assoc = Print.RightAssoc}, 380 {token = "=", precedence = 4, assoc [all...] |
H A D | Print.sml | 472 datatype assoc = type 481 assoc : assoc} list; 486 val {token = _, precedence = p1, assoc = _} = io1 487 and {token = _, precedence = p2, assoc = _} = io2 498 fun new t a acc = {tokens = StringSet.singleton t, assoc = a} :: acc; 503 | {tokens = ts, assoc = a} :: acc => 504 if equalAssoc a a' then {tokens = StringSet.add ts t, assoc = a} :: acc 507 fun layer ({token = t, precedence = p, assoc = a}, (acc,p')) = 517 | {token = t, precedence = p, assoc [all...] |
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Print.sig | 156 datatype assoc = type 165 assoc : assoc} list 169 val layerInfixes : infixes -> {tokens : StringSet.set, assoc : assoc} list
|
H A D | Term.sml | 371 {token = "/", precedence = 7, assoc = Print.LeftAssoc}, 372 {token = "div", precedence = 7, assoc = Print.LeftAssoc}, 373 {token = "mod", precedence = 7, assoc = Print.LeftAssoc}, 374 {token = "*", precedence = 7, assoc = Print.LeftAssoc}, 375 {token = "+", precedence = 6, assoc = Print.LeftAssoc}, 376 {token = "-", precedence = 6, assoc = Print.LeftAssoc}, 377 {token = "^", precedence = 6, assoc = Print.LeftAssoc}, 378 {token = "@", precedence = 5, assoc = Print.RightAssoc}, 379 {token = "::", precedence = 5, assoc = Print.RightAssoc}, 380 {token = "=", precedence = 4, assoc [all...] |
H A D | Print.sml | 472 datatype assoc = type 481 assoc : assoc} list; 486 val {token = _, precedence = p1, assoc = _} = io1 487 and {token = _, precedence = p2, assoc = _} = io2 498 fun new t a acc = {tokens = StringSet.singleton t, assoc = a} :: acc; 503 | {tokens = ts, assoc = a} :: acc => 504 if equalAssoc a a' then {tokens = StringSet.add ts t, assoc = a} :: acc 507 fun layer ({token = t, precedence = p, assoc = a}, (acc,p')) = 517 | {token = t, precedence = p, assoc [all...] |
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | hol_defaxioms_thmsScript.sml | 117 ``assoc x nil = nil``, 124 ``assoc x (cons (cons x' y) l) = 125 if |= equal x x' then cons x' y else assoc x l``,
|
/seL4-l4v-master/HOL4/src/hol88/ |
H A D | hol88Lib.sml | 42 fun assoc i alist = function 44 of NONE => raise HOL88_ERR {function = "assoc", message = ""}
|
H A D | hol88Lib.sig | 17 val assoc : ''a -> (''a * 'b) list -> ''a * 'b value
|
/seL4-l4v-master/HOL4/tools/ |
H A D | holscript-mode.el | 790 '((assoc ",")) '((assoc ";")) 791 '((assoc "^Proof") 793 (assoc "by" "suffices_by")) 794 '((assoc "ENDQ." "QFIER." "in" "of") 795 (assoc "|") 796 (assoc "=>") 797 (assoc "else") 798 (assoc "<=>" "���" "<-") 799 (assoc " [all...] |
/seL4-l4v-master/HOL4/src/integer/ |
H A D | intSimps.sml | 17 val assoc = INT_ADD_ASSOC value 46 assoc = assoc, 47 symassoc = GSYM assoc, 49 l_asscomm = derive_l_asscomm assoc comm, 50 r_asscomm = derive_r_asscomm assoc comm,
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | ProvideUnicode.sml | 98 | INFIX (STD_infix (rrlist, assoc)) => 99 search_rrlist (Infix(assoc, valOf fixopt)) tf_opt
|
/seL4-l4v-master/l4v/tools/c-parser/standalone-parser/ |
H A D | basics.sml | 14 fun assoc (l, x) = function 17 | (k,v) :: rest => if k = x then SOME v else assoc(rest, x)
|
/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | satCommonTools.sml | 54 (* Like CONJUNCTS but assumes the conjunct is bracketed right-assoc. *)
|
/seL4-l4v-master/HOL4/examples/pgcl/src/ |
H A D | posrealTools.sml | 207 fun permute is_op assoc rid swap inv = 208 SIMP_CONV boolSimps.bool_ss [assoc] 212 fun permute_conv is_op assoc rid swap inv tm = 213 (if is_op tm then permute is_op assoc rid swap inv else NO_CONV) tm;
|