/seL4-l4v-master/HOL4/src/emit/ |
H A D | basis_emitScript.sml | 1131 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 D | Foreign.sml | 27 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 D | ExnPrinter.581.sml | 86 val printLimit: word ref list Universal.tag = Universal.tag() 99 val thisRef: word ref = RunCall.unsafeCast r
|
H A D | ExnPrinter.sml | 86 val printLimit: word ref list Universal.tag = Universal.tag() 99 val thisRef: word ref = RunCall.unsafeCast r
|
H A D | ThreadLib.sml | 39 val oldAttrs: Word.word = RunCall.loadWord(self(), 0w1)
|
H A D | Unix.sml | 27 | W_EXITSTATUS of Word8.word 41 val exit : Word8.word -> 'a 63 val exit : Word8.word -> 'a
|
H A D | Vector.sml | 28 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 D | riscv_stepScript.sml | 96 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 D | helperLib.sml | 257 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 D | m0_stepScript.sml | 67 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 D | updateLib.sml | 367 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 D | Print.sml | 111 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 D | Print.sml | 111 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 D | prog_x64Script.sml | 1533 (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 D | parse_glob.sml | 106 "space", "upper", "xdigit", "word"] 124 | ":word:]" => return POSIX.word_set
|
/seL4-l4v-master/HOL4/examples/logic/ltl/ |
H A D | gbaSimplScript.sml | 415 (* (* (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 D | BackendIntermediateCode.sml | 209 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 D | Regexp_Type.sig | 4 type w64 = Word64.word
|
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | arm_parserLib.sig | 94 ALIGN 4 ; ensures next short is in the following word
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | integer_wordLib.sml | 98 else raise ERR "INT_WORD_GROUND_CONV" "not ground integer word operation"
|
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | NormalScript.sml | 139 `!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 D | arm_stepScript.sml | 355 \\ 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 D | WinBase.sml | 58 type flags = SysWord.word 119 type flags = SysWord.word 175 | SWP_OTHER of Word32.word
|
H A D | FontBase.sml | 28 (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 D | theories.tex | 2209 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...] |