Searched refs:word (Results 126 - 150 of 347) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/src/emit/
H A Dbasis_emitScript.sml1131 val word_index_def = Define `word_index (w:'a word) n = w ' n`;
1132 val w2w_itself_def = Define `w2w_itself (:'a) w = (w2w w): 'a word`;
1133 val sw2sw_itself_def = Define `sw2sw_itself (:'a) w = (sw2sw w): 'a word`;
1134 val word_eq_def = Define `word_eq (v: 'a word) w = (v = w)`;
1159 `!b. $FCP (K b) = n2w (if b then 1 else 0) : 1 word`,
1219 val w = "type word" ^ x ^ " = " ^ s ^ " word"
1225 "val toWord" ^ x ^ " : NumML.num -> word" ^ x,
1231 "val toWord" ^ x ^ " : numML.num -> word" ^ x,
1233 " = o(toWord" ^ x ^ ", numML.fromString) : string -> word"
[all...]
/seL4-l4v-master/HOL4/polyml/basis/
H A DForeign.sml27 val volatileRef: SysWord.word -> volatileRef
28 val setVolatileRef: volatileRef * SysWord.word -> unit
29 val getVolatileRef: volatileRef -> SysWord.word
32 val voidStar2Sysword: voidStar -> SysWord.word
33 val sysWord2VoidStar: SysWord.word -> voidStar
36 val ++ : voidStar * word -> voidStar
37 val -- : voidStar * word -> voidStar
46 val malloc: word -> voidStar
52 val alloca: word * (voidStar -> 'a) -> 'a
54 val get8: voidStar * Word.word
[all...]
H A DExnPrinter.581.sml86 val printLimit: word ref list Universal.tag = Universal.tag()
99 val thisRef: word ref = RunCall.unsafeCast r
H A DExnPrinter.sml86 val printLimit: word ref list Universal.tag = Universal.tag()
99 val thisRef: word ref = RunCall.unsafeCast r
H A DThreadLib.sml39 val oldAttrs: Word.word = RunCall.loadWord(self(), 0w1)
H A DUnix.sml27 | W_EXITSTATUS of Word8.word
41 val exit : Word8.word -> 'a
63 val exit : Word8.word -> 'a
H A DVector.sml28 val vecAsWord: 'a vector -> word = RunCall.unsafeCast
29 and wordAsVec: word -> 'a vector = RunCall.unsafeCast
30 val intAsWord: int -> word = RunCall.unsafeCast
31 and wordAsInt: word -> int = RunCall.unsafeCast
201 local val u = unsafeSub in fun unsafeSub (v: 'a vector, i: word) = u(v, wordAsInt i) end
/seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/step/
H A Driscv_stepScript.sml96 Sub-word select operation (temporary)
100 select (p:'a word) (w: word64) =
103 (l + sz - 1 >< l) w : 'b word`
156 ``(=):'a word -> 'a word -> bool``,
157 ``(h >< l) : 'a word -> 'b word``
186 ``w2w ((63 >< 3) a : 61 word) << 3 = (63 '' 3) (a: word64)``
189 ``w2w ((63 >< 3) a + 1w: 61 word) << 3 = (63 '' 3) (a: word64) + 8w``
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/
H A DhelperLib.sml257 val sw2sw_ss = eval_term_ss "sw2sw" ``(sw2sw:'a word->'b word) (n2w n)``
258 val w2w_ss = eval_term_ss "w2w" ``(w2w:'a word->'b word) (n2w n)``
511 ``(n2w n ?? n2w m):('a word)``,``(n2w n || n2w m):('a word)``,``(n2w n && n2w m):('a word)``,
512 ``(n2w n + n2w m):('a word)``, ``(n2w n - n2w m):('a word)``, ``(n2w n * n2w m):('a word)``,
[all...]
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/step/
H A Dm0_stepScript.sml67 STM1 f (b: word32) (registers: 'a word) s m j =
80 STM_UPTO f i (registers: 'a word) (b: word32, s) =
203 \\ Cases_on `word_msb (x + y) <> word_msb (1w : 'a word)`
339 `!registers: 'a word.
346 `!r: 'a word.
460 (((31 >< 1) r : 31 word @@ (0w: word1)) = r)`,
467 (((31 >< 1) (w + 4w) : 31 word @@ (1w: word1)) = (w + 4w) !! 1w)`,
474 (((31 >< 1) (w + 4w - 2w) : 31 word @@ (1w: word1)) = (w + 2w) !! 1w)`,
488 `aligned 1 (w: 31 word @@ (0w: word1))`,
760 ((w2w w : 33 word) << im
[all...]
/seL4-l4v-master/HOL4/src/update/
H A DupdateLib.sml367 SORT_UPDATES_MAPTO_CONV ``FST : 'a word # 'b -> 'a word``
373 SORT_UPDATES_MAPTO_CONV ``FST : 'a word # 'b -> 'a word``
419 Sort sequences of updates for maps of type ``:ty word -> 'a``.
434 "Cannot compute size or word type")
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DPrint.sml111 datatype word = Word of {word : string, size : int}; type
113 fun mkWord s = Word {word = s, size = String.size s};
119 fun spacesWord i = Word {word = nSpaces i, size = i};
123 fun renderWord (Word {word = x, ...}) = x;
171 | AddWord of word
435 fn Word {word = s, size = n} =>
635 WordChunk of word
1308 fun executeAddWord lineLength word lines state =
1312 val n = sizeWord word
[all...]
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DPrint.sml111 datatype word = Word of {word : string, size : int}; type
113 fun mkWord s = Word {word = s, size = String.size s};
119 fun spacesWord i = Word {word = nSpaces i, size = i};
123 fun renderWord (Word {word = x, ...}) = x;
171 | AddWord of word
435 fn Word {word = s, size = n} =>
635 WordChunk of word
1308 fun executeAddWord lineLength word lines state =
1312 val n = sizeWord word
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/
H A Dprog_x64Script.sml1533 (w2w w && n2w n = w2w ((w:'b word) && n2w n) :'a word) /\
1534 (n2w n && w2w w = w2w (n2w n && (w:'b word)) :'a word) /\
1535 (w2w w ?? n2w n = w2w ((w:'b word) ?? n2w n) :'a word) /\
1536 (n2w n ?? w2w w = w2w (n2w n ?? (w:'b word)) :'a word) /\
1537 (w2w w || n2w n = w2w ((w:'b word) || n2w n) :'a word) /\
[all...]
/seL4-l4v-master/HOL4/tools/Holmake/
H A Dparse_glob.sml106 "space", "upper", "xdigit", "word"]
124 | ":word:]" => return POSIX.word_set
/seL4-l4v-master/HOL4/examples/logic/ltl/
H A DgbaSimplScript.sml415 (* (* (un_merged_run word aT x_old x_new init trans f switch 0 = *) *)
417 (* (* ��� (un_merged_run word aT x_old x_new init trans f s (SUC i) = *) *)
418 (* (* if ?a. (a, f (SUC i)) ��� trans (f i) ��� at word i ��� a *) *)
420 (* (* ��� (at word i ��� a2) ==> switch ((f i), a2)) *) *)
422 (* (* else let a2 = @a. (a,x_old) ��� trans (f i) ��� (at word i ��� a) *) *)
427 (* (* un_merged_run word aT x_old x_new init trans f i = *) *)
430 (* (* else (if ?a. (a,f i) ��� trans (f (i - 1)) ��� at word (i-1) ��� a *) *)
432 (* (* ��� (at word (i-1) ��� a2) ==> *) *)
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DBackendIntermediateCode.sml209 firstIndex: word
232 | BICTagTest of { test: backendIC, tag: word, maxTag: word }
251 | CaseTag of word
260 LoadStoreMLWord of {isImmutable: bool} (* Load/Store an ML word in an ML word cell. *)
262 | LoadStoreC8 (* Load/Store C values - The base address is a boxed SysWord.word value. *)
294 address if this is to/from ML memory or a (boxed) SysWord.word if it is
/seL4-l4v-master/HOL4/examples/formal-languages/regular/
H A DRegexp_Type.sig4 type w64 = Word64.word
/seL4-l4v-master/HOL4/examples/ARM/v7/
H A Darm_parserLib.sig94 ALIGN 4 ; ensures next short is in the following word
/seL4-l4v-master/HOL4/src/integer/
H A Dinteger_wordLib.sml98 else raise ERR "INT_WORD_GROUND_CONV" "not ground integer word operation"
/seL4-l4v-master/HOL4/examples/dev/sw2/
H A DNormalScript.sml139 `!w1 w2 : 'a word.
171 `!w1 w2 : 'a word.
193 `((x : 'a word < y) = (y > x)) /\
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/step/
H A Darm_stepScript.sml355 \\ Cases_on `word_msb (x + y) <> word_msb (1w : 'a word)`
509 `!r: 'a word.
628 (((31 >< 1) (w + 4w): 31 word) @@ (1w: word1) = w + 5w)`,
704 x22; x23]: word24 @@ (0w: word2)): 26 word): word32) =
725 (v2w [x24; F]: word2)): 26 word): word32) =
740 val t2 = ``(((31 >< 1) (i: word32) : 31 word) @@ (0w: word1)): word32``
743 (!i:word32. ((31 >< 2) i : 30 word) @@ (0w: word2) = align 2 i)`,
908 `!w : 'a word. fixwidth (dimindex (:'a)) (w2v w) = w2v w`,
1082 ((w2w w : 33 word) << imm) ' 32 = testbit 32 (shiftl (w2v w) imm)`,
1093 ((w << imm2, if imm2 = 0 then C else ((w2w w : 33 word) << imm
[all...]
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/
H A DWinBase.sml58 type flags = SysWord.word
119 type flags = SysWord.word
175 | SWP_OTHER of Word32.word
H A DFontBase.sml28 (DEFAULT_QUALITY, 0w0: Word8.word),
47 (ANSI_CHARSET, 0wx00: Word8.word),
127 (OUT_DEFAULT_PRECIS, 0w0: Word8.word),
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A Dtheories.tex2209 Questa teoria � usata nello sviluppo della teoria word e fornisce anche
2215 La teoria \theoryimp{words} introduce una selezione di costanti ed operazioni polimorfiche, i cui tipi possono essere istanziati a parole di qualsiasi dimensione. Per esempio, l'addizione word
2221 Tutti i teoremi circa operazioni word si applicano a word di qualsiasi lunghezza\footnote{Si noti
2222 che � impossibile introdurre word di lunghezza zero perch� tutti i tipi
2234 \holtxt{word\_len:\worda\rarr\num}.
2280 L'operazione \holtxt{word\_concat:\worda\rarr\wordb\rarr\wordc} concatena parole. Si noti che il tipo restituito non � vincolato. Questo significa che due parole di sedici bit possono essere concatenate per dare una parola di qualsiasi lunghezza -- che pu� essere pi� piccola o pi� grande del valore atteso di 32. La funzione correlata \holtxt{word\_join} restituisce una parola della lunghezza attesa, cio� di tipo fcp{\bool}{$\alpha+\beta$}; comunque, l'operazione di concatenazione � pi� utile perch� spesso vogliamo \fcp{\bool}{\ty{32}} e non il logicamente distinto \fcp{\bool}{\ty{16}+\ty{16}}.
2316 Le funzioni \holtxt{word\_lsb}, \holtxt{word\_ms
[all...]

Completed in 249 milliseconds

1234567891011>>