Lines Matching defs:cond
102 {sflag : term, cond : term, qual : qualifier,
155 read_instruction >>= (fn i => return (#cond (valOf i)));
185 SOME { sflag = #sflag i, cond = c, qual = #qual i,
1085 (let val cond = condition_to_word4 s
1086 val cond' = if m = B andalso not outside orelse
1091 cond
1097 itcond = cond
1099 opposite_condition (itcond,cond))
1103 (write_token r >>- return cond')
1167 (SOME {sflag = F, cond = mk_word4 14,
1172 arm_parse_condition M >>= (fn cond =>
1174 let val i = {sflag = sflag, cond = cond,
1782 read_cond >>= (fn cond =>
1785 if is_var cond orelse is_AL cond then
1789 val wide_okay = if is_var cond orelse is_AL cond then
1899 read_cond >>= (fn cond =>
1900 assertT (is_AL cond)
1989 fun mk_it_mask (cond,l) =
1990 let val cond0 = wordsSyntax.mk_index (cond,numSyntax.zero_tm) |> eval
2027 val cond = condition_to_word4 c
2028 val mask = mk_it_mask (cond,t)
2029 val cond = if b then
2030 cond
2032 wordsSyntax.mk_word_xor (mk_word4 1,cond)
2034 eval (wordsSyntax.mk_word_concat (cond,mask))
2055 let val cond = condition_to_word4 c in
2057 assertT (not (is_AL cond) orelse Lib.all I l)
2060 (write_itcond cond >>-
2068 (cond,mk_it_mask (cond,tl l))))))
4212 read_cond >>= (fn cond =>
4216 return (Instruction1 (line,enc,cond,tm))))));
4448 | Instruction1 (i,enc,cond,tm) =>
4455 else Encoding_Thumb2_tm,cond,tm)
4464 if is_AL cond then
4477 if is_AL cond then
4559 | recurse ((x,Instruction1 (i,enc,cond,tm))::t) code =
4561 recurse t ((x,Instruction (enc,cond,tm))::code)
4570 if is_var cond orelse is_AL cond then
4576 if is_var cond orelse is_AL cond then
4804 recurse t ((x,Instruction (enc,cond,tm'))::code)