Searched refs:word (Results 151 - 175 of 347) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/prog/
H A Darm_progLib.sml35 val word = wordsSyntax.mk_int_word_type 32 value
114 val r15 = stateLib.gvar "pc" word
131 val pc_tm = Term.mk_var ("pc", word)
458 utilsLib.mk_cond_rand_thms [``aligned n : 'a word -> bool``]
549 [``Extend (T, w:'a word): 'b word``,
550 ``Extend (F, w:'a word): 'b word``] @
742 [word, word5, ``:RName``]
1250 val map_tys = [word, word
[all...]
/seL4-l4v-master/HOL4/polyml/basis/
H A DThread.sml297 fun attrsToWord (at: threadAttribute list): Word.word * Word.word =
326 fun getIstateBits(w: Word.word): interruptState =
350 word mutable object.
401 (* If there is a pending request the word in the thread object
413 fun getAttrWord (me: thread) : Word.word =
437 val oldValues: Word.word = getAttrWord me
474 (unit->unit) * word * int -> thread = RunCall.rtsCallFull3 "PolyThreadForkThread"
524 type mutex = Word.word ref
531 (* A mutex is implemented as a Word.word re
[all...]
H A DOS.sml54 val hash : file_id -> word
111 val hash : iodesc -> word
166 type syserror = LibrarySupport.syserror (* Implemented as a SysWord.word value. *)
849 val doIo: int*string*word -> bool
915 IODESC of word ref (* This is currently a volatile ref. We MUST use pointer equality. *)
927 fun hash (i: iodesc) : word =
974 type poll_desc = word*iodesc
975 datatype poll_info = PI of word*poll_desc
978 val doIo: int*iodesc*int -> word
984 val sysPoll:iodesc Vector.vector * word Vecto
[all...]
H A DGeneral.sml60 (* Exception packets. The first word is the code, a unique id; the second is
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/step/
H A Darm8_stepLib.sml50 ``(h >< l) : 'a word -> 'b word``] @
268 [``t <> 31w: word5``, ``w2w (s.REG t) = 0w: 'a word``],
269 [``t <> 31w: word5``, ``w2w (s.REG t) <> 0w: 'a word``]] []
273 val tm = ``word_bit (w2n (bit_pos: word6)) (w2w (^st.REG t): 'a word)``
287 `!a:'a word b c. (if b then a else a + c) = a + (if b then 0w else c)`,
/seL4-l4v-master/HOL4/examples/ARM/v4/
H A DsystemScript.sml274 MEM_WRITE_BYTE (mem:mem) addr (word:word8) =
276 (a30 =+ SET_BYTE ((1 >< 0) addr) word (mem a30)) mem`;
279 MEM_WRITE_HALF (mem:mem) addr (word:word16) =
281 (a30 =+ SET_HALF (addr ' 1) word (mem a30)) mem`;
284 MEM_WRITE_WORD (mem:mem) addr word = (addr30 addr =+ word) mem`;
/seL4-l4v-master/HOL4/examples/ARM/experimental/
H A Dlpc_uartScript.sml178 BIT_UPDATE i b (w:'a word) = (FCP j. if i = j then b else w ' j):'a word`;
183 (BIT_UPDATE i b (w:'a word) ' j = if i = j then b else w ' j)``,
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/
H A Dppc_Lib.sml85 val tm = find_term (can (match_term ``(sw2sw:'a word -> 'b word) (n2w n)``)) (concl th)
89 val tm = find_term (can (match_term ``(n2w n) && (n2w m) = (n2w k):'a word``)) (concl th)
/seL4-l4v-master/HOL4/examples/dev/Fact32/
H A Dexor32.ml53 (* an instance, using the type of ``out`` to compute the word width *)
/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/
H A DFP64.sml25 raise Fail ("fromBits: not " ^ Int.toString size ^ "-bit word")
/seL4-l4v-master/HOL4/src/n-bit/
H A DbitstringLib.sml141 ���!l n. (v2n l = n) ==> (v2w l = n2w n : 'a word)���,
156 {name = "v2w_n2w", pats = [``v2w x: 'a word``], conv = v2w_n2w_CONV}
257 ((h >< l) (v2w v : 'a word) : 'b word =
/seL4-l4v-master/isabelle/src/Pure/ML/
H A Dml_lex.scala47 val WORD = Value("word")
217 val word =
252 (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad))))
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dexport_codeLib.sml68 if ty = ``:word32`` then "\t.word\t" else fail()
/seL4-l4v-master/HOL4/examples/l3-machine-code/x64/step/
H A Dx64_stepLib.sml42 ``(h >< l) : 'a word -> 'b word``,
43 ``bit_field_insert h l : 'a word -> 'b word -> 'b word``] @
517 ``IS_SOME (x: 'a word option)`` o
519 ``IS_SOME (x: 'a word option)``)
813 (if IS_SOME x then w2w (i2w (THE x) : 'c word) else y) =
814 case x of SOME a => w2w (i2w a : 'c word) | _ => y)���,
/seL4-l4v-master/HOL4/examples/machine-code/just-in-time/
H A Dexport_codeLib.sml57 if ty = ``:word32`` then "\t.word\t" else hd []
/seL4-l4v-master/HOL4/examples/machine-code/lisp/
H A Dexport_codeLib.sml56 if ty = ``:word32`` then "\t.word\t" else fail()
/seL4-l4v-master/l4v/isabelle/src/Pure/ML/
H A Dml_lex.scala47 val WORD = Value("word")
217 val word =
252 (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad))))
/seL4-l4v-master/HOL4/examples/ARM/v7/
H A Darm_stepLib.sml115 ``(v = v + w) <=> (w = 0w:'a word)``;
117 val word_add_sub2 = wordsLib.WORD_DECIDE ``(a + b) + -a = b : 'a word``
118 val word_add_sub3 = wordsLib.WORD_DECIDE ``a + b + -b = a : 'a word``
119 val word_add_sub4 = wordsLib.WORD_DECIDE ``a + -b + b = a : 'a word``
120 val word_add_sub5 = wordsLib.WORD_DECIDE ``a + -(a + -b) = b : 'a word``
382 pats = [``arm_coretypes$aligned (n2w a:'a word,n)``]}
845 val lem3 = ``(-1w * a:'a word) << 1 = -1w * (a << 1)``
908 (((31 >< 1) w):31 word) @@ (1w:bool[unit])`,
980 pats = [``n2w w = n2w y :'a word``]}
/seL4-l4v-master/HOL4/examples/bootstrap/
H A Dautomation_lemmasScript.sml409 (* word *)
412 word w = Num (w2n w)
417 b0 ��� x < 16 ��� (env,[x1],s) ---> ([word ((n2w x):word4)],s)
424 b0 ��� x < 2 ** 64 ��� (env,[x1],s) ---> ([word ((n2w x):word64)],s)
430 (b0 ��� (env,[x1],s) ---> ([word (x:word4)],s)) ���
437 (b0 ��� (env,[x1],s) ---> ([word (x:word64)],s)) ���
707 inst (Const r1 w64) = list [Name "Const"; reg r1; word w64] ���
719 inst (Load r1 r2 i) = list [Name "Load"; reg r1; reg r2; word i] ���
720 inst (Store r1 r2 i) = list [Name "Store"; reg r1; reg r2; word i] ���
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/
H A DGdiBase.sml105 (* COLORREF - this is an RGB encoded into a 32-bit word. *)
106 abstype COLORREF = C of Word32.word
H A DMenu.sml42 | MFT_OWNERDRAW of SysWord.word
204 | MFT_OWNERDRAW of SysWord.word
222 (MFT_MENUBARBREAK, 0wx00000020: Word32.word),
391 (* If the menu opens a submenu the high order word is the number of
392 items. The low order word is the state. *)
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A Dderive_specsLib.sml152 ``CARRY_OUT (x : 'a word) y T``
158 ``OVERFLOW (x : 'a word) y T``
184 val Align_pat1 = ``arm$Align (w:'a word,n)``
185 val Align_pat2 = ``m0$Align (w:'a word,n)``
223 ``(((((31 >< 1) (w:word32)):31 word) @@ (0w:1 word)) : word32) =
226 ``(n2w n + w = if n < dimword (:'a) DIV 2 then n2w n + (w:'a word)
377 val pattern = inst [``:'a``|->aa] ``(p:'a word) + n2w n``
/seL4-l4v-master/HOL4/examples/logic/ltl/
H A DalterAScript.sml60 validity condition for runs over a given word
64 `validAARunFor aut run word =
68 ==> ?a. (a,run.E (i,q)) ��� aut.trans q /\ (at word i ��� a))
132 `runForAA aut run word =
133 validAARunFor aut run word /\ acceptingAARun aut run`;
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/prog/
H A Dm0_progLib.sml32 val word = wordsSyntax.mk_int_word_type 32 value
93 then sumSyntax.mk_inl (list_mk_concat ty16 l, word)
98 val r15 = stateLib.gvar "pc" word
551 [word, ``:RName``]
776 val map_tys = [word, ``:RName``]
/seL4-l4v-master/HOL4/src/HolSmt/
H A DSmtLib.sml40 (* returns true iff 'ty' is a word type that is not fixed-width *)
45 (* make sure that all word types in 't' are of fixed width; return 's' *)
53 "not a fixed-width word type"
139 raise ERR "<builtin_symbols.x:'a word>" "not a word literal")),

Completed in 194 milliseconds

1234567891011>>