Searched refs:assoc (Results 1 - 25 of 109) sorted by relevance

12345

/seL4-l4v-master/seL4/src/arch/arm/armv/armv8-a/64/
H A Dcache.c64 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 DGenPolyCanon.sml11 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 DGenPolyCanon.sig11 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 DNumRelNorms.sml40 assoc = ADD_ASSOC,
55 assoc = ADD_ASSOC,
101 assoc = MULT_ASSOC,
/seL4-l4v-master/seL4/src/arch/arm/armv/armv7-a/
H A Dcache.c58 /* 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 Dcache.c58 /* 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 DAC_Sort.sml22 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 DAC_Sort.sig5 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 DAC.sml128 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 DrecordEnumSimpsBScript.sml28 ^(#accessor (Lib.assoc "fld2" (TypeBase.fields_of ���:'a Record���)))
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DPrint.sig156 datatype assoc = type
165 assoc : assoc} list
169 val layerInfixes : infixes -> {tokens : StringSet.set, assoc : assoc} list
H A DTerm.sml371 {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 DPrint.sml472 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 DPrint.sig156 datatype assoc = type
165 assoc : assoc} list
169 val layerInfixes : infixes -> {tokens : StringSet.set, assoc : assoc} list
H A DTerm.sml371 {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 DPrint.sml472 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 Dhol_defaxioms_thmsScript.sml117 ``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 Dhol88Lib.sml42 fun assoc i alist = function
44 of NONE => raise HOL88_ERR {function = "assoc", message = ""}
H A Dhol88Lib.sig17 val assoc : ''a -> (''a * 'b) list -> ''a * 'b value
/seL4-l4v-master/HOL4/tools/
H A Dholscript-mode.el790 '((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 DintSimps.sml17 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 DProvideUnicode.sml98 | 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 Dbasics.sml14 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 DsatCommonTools.sml54 (* Like CONJUNCTS but assumes the conjunct is bracketed right-assoc. *)
/seL4-l4v-master/HOL4/examples/pgcl/src/
H A DposrealTools.sml207 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;

Completed in 232 milliseconds

12345