/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/prog/ |
H A D | arm_progLib.sml | 35 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 D | Thread.sml | 297 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 D | OS.sml | 54 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 D | General.sml | 60 (* 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 D | arm8_stepLib.sml | 50 ``(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 D | systemScript.sml | 274 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 D | lpc_uartScript.sml | 178 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 D | ppc_Lib.sml | 85 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 D | exor32.ml | 53 (* an instance, using the type of ``out`` to compute the word width *)
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/ |
H A D | FP64.sml | 25 raise Fail ("fromBits: not " ^ Int.toString size ^ "-bit word")
|
/seL4-l4v-master/HOL4/src/n-bit/ |
H A D | bitstringLib.sml | 141 ���!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 D | ml_lex.scala | 47 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 D | export_codeLib.sml | 68 if ty = ``:word32`` then "\t.word\t" else fail()
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/x64/step/ |
H A D | x64_stepLib.sml | 42 ``(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 D | export_codeLib.sml | 57 if ty = ``:word32`` then "\t.word\t" else hd []
|
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | export_codeLib.sml | 56 if ty = ``:word32`` then "\t.word\t" else fail()
|
/seL4-l4v-master/l4v/isabelle/src/Pure/ML/ |
H A D | ml_lex.scala | 47 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 D | arm_stepLib.sml | 115 ``(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 D | automation_lemmasScript.sml | 409 (* 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 D | GdiBase.sml | 105 (* COLORREF - this is an RGB encoded into a 32-bit word. *) 106 abstype COLORREF = C of Word32.word
|
H A D | Menu.sml | 42 | 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 D | derive_specsLib.sml | 152 ``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 D | alterAScript.sml | 60 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 D | m0_progLib.sml | 32 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 D | SmtLib.sml | 40 (* 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")),
|