/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Bool.sml | 38 fun scan (getc: (char, 'a) StringCvt.reader) (str: 'a) : (bool * 'a) option = 41 val strm = StringCvt.skipWS getc str
|
H A D | Byte.sml | 48 val (str, offset, size) = Substring.base s value 49 val slice = Word8VectorSlice.slice(stringToBytes str, offset, SOME size)
|
/seL4-l4v-10.1.1/HOL4/src/Boolify/src/ |
H A D | Encode.sml | 50 fun pass str = 51 if mem str names 53 else str 165 fun gamma str = 166 case assoc1 str tyop_map 167 of NONE => type_encode_env str
|
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | DataSize.sml | 29 fun pass str = 30 if mem str names 32 else str 127 fun gamma str = 128 case assoc1 str tyop_map 129 of NONE => type_size_env str
|
/seL4-l4v-10.1.1/HOL4/examples/real-to-float/ |
H A D | daisyScript.sml | 38 (eval_X c env (Const str) = c.parse str)` 187 (x_str (Var str) = str) /\ (x_str (Const str) = str) `
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Isar/ |
H A D | outer_syntax.scala | 24 def quote_string(str: String): String = 26 val result = new StringBuilder(str.length + 10) 28 for (s <- Symbol.iterator(str)) {
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Isar/ |
H A D | outer_syntax.scala | 24 def quote_string(str: String): String = 26 val result = new StringBuilder(str.length + 10) 28 for (s <- Symbol.iterator(str)) {
|
/seL4-l4v-10.1.1/seL4/src/arch/arm/32/ |
H A D | hyp_traps.S | 103 str lr, [sp, #4] 106 str lr, [sp, #8] 115 str lr, [sp, #(PT_FaultInstruction - PT_SP)]
|
/seL4-l4v-10.1.1/l4v/tools/haskell-translator/ |
H A D | lhs_pars.py | 517 bstring = braces.str(string, '(', ')') 528 s = str(bit).strip() 532 bit2 = braces.str(s[1:-1], '(', ')') 535 if str(bits[0]) == 'PPtr': 540 arg = ' '.join([str(bit) for bit in bits[1:]])[1:-1] 542 return ' '.join([arg, 'list', str(type_conv(bits[0]))]) 546 strs = [str(bit) for bit in bits] 587 elif str(string) in type_conv_table: 588 result = type_conv_table[str(string)] 600 type_conv_table[str(strin [all...] |
/seL4-l4v-10.1.1/graph-refine/ |
H A D | graph-refine.py | 117 return str (result) 129 word_pairs = [p for p in pairs if s in word_re.findall (str (p))] 132 print 'Possibilities for %r: %s' % (s, [str (p) for p in pairs]) 265 return [v for v in vs if type (v) == str] + [v2 266 for v in vs if type (v) != str for v2 in get_strs (v)]
|
H A D | syntax.py | 306 return hash(str(self)) 355 xs.append (str (self.num)) 358 xs.extend ([str (n) for n in self.nums]) 364 xs.append (str (self.num)) 443 if type (nm) == str: 533 xs.append (str (len (self.vals))) 537 xs.append (str (self.val)) 732 xs.extend ([str (c) for c in self.get_conts ()]) 734 xs.append (str (len (self.upds))) 743 xs.append (str (le [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | BackendIntermediateCode.sml | 401 val str : string = value 404 PrettyString str 409 val str : string = value 412 PrettyString str 417 val str : string = value 420 PrettyString str 425 val str : string = value 428 PrettyString str 433 val str = "INDIRECT(" ^ Int.toString offset ^ ", "; value 436 [ PrettyString str, prett [all...] |
/seL4-l4v-10.1.1/l4v/tools/autocorres/tools/ |
H A D | release.py | 106 type=str, help='Version number of the release, such as "0.95-beta1".') 108 type=str, help='Tarball to the C parser release.') 110 type=str, help='Tarball to the official Isabelle release') 122 type=str, help='Path to the L4.verified repository base.', default=None) 124 type=str, default='ARM,ARM_HYP,X64',
|
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
H A D | ARM_proverLib.sml | 78 let val (str , fst , snd) = value 80 (str , [fst , snd]) => (str , fst , snd) 82 val (str , tp_type, b) = value 84 (str , [tp_type, b]) => (str , tp_type, b) 266 val (c,str) = 268 COMB(c,str) => (c,str) 278 str,uf_fu 364 val str = valOf (TextIO.inputLine TextIO.stdIn) value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
H A D | regexp2dfa.sml | 12 | dest_string str = 13 let val c = String.sub(str,0) 14 val t = String.substring(str,1,String.size str - 1) 18 fun Upper str = 20 val (c,t) = dest_string str 21 in if isUpper c then str
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | graph_specsLib.sml | 51 val str = tm |> rator |> rand |> stringSyntax.fromHOLstring value 53 in mk_var(str,ty) |-> tm end) 68 val str = tm |> rator |> rand |> stringSyntax.fromHOLstring value 70 in mk_var(str,ty) |-> tm end) 416 val str = ("Graph spec failed in " ^ sec_name ^ " for pos " ^ value 418 in (write_line str; print (str ^ "\n")) end 440 val str = name ^ "_" ^ int_to_string i value 441 in if mem str (!r) then get_index_name name (i+1) 442 else(r := str [all...] |
/seL4-l4v-10.1.1/HOL4/help/src-sml/ |
H A D | Htmlsigs.sml | 75 | Str => "str" 158 | encode c = str c 263 dec "str" 347 handle exn as OS.SysErr (str, _) => (print(str ^ "\n\n"); raise exn) 363 (fn c => (href (str c) ("#" ^ str c); out " ")) 376 app out ["\n</ul>\n\n<a name=\"", str c1, "\">"]; 377 subheader (str c1);
|
H A D | Doc2Tex.sml | 13 fun out(str,s) = TextIO.output(str, s) 76 | c => str c)
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | UTF8.sml | 12 else if i < 128 then str (Char.chr i) 86 if i < 128 then SOME((str c, i), string ss') 90 if cnt = 1 then raise BadUTF8 (str c) 136 if pos < 0 then raise BadUTF8 (str (sub(ss,0))) 154 if Char.ord c < 128 then SOME(str c, Char.ord c)
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | Holdep.sml | 21 fun errMsg str = TextIO.output(TextIO.stdErr, str ^ "\n\n") 113 else str c 170 handle e as OS.SysErr (str, _) => (errMsg str; raise e)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | reals.cpp | 117 POLYEXTERNALSYMBOL POLYUNSIGNED PolyRealBoxedFromString(PolyObject *threadId, PolyWord str); 143 static Handle Real_convc(TaskData *mdTaskData, Handle str); 328 Handle Real_convc(TaskData *mdTaskData, Handle str) /* string to real */ argument 333 TempCString string_buffer(Poly_string_to_C_alloc(str->Word())); 355 POLYUNSIGNED PolyRealBoxedFromString(PolyObject *threadId, PolyWord str) argument 361 Handle pushedString = taskData->saveVec.push(str);
|
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | scan.scala | 331 private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] = 333 val len = str.length 337 tree.branches.get(str.charAt(i)) match { 347 def completions(str: CharSequence): List[String] = 348 lookup(str) match { 349 case Some((true, tree)) => dest(tree, List(str.toString))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | scan.scala | 331 private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] = 333 val len = str.length 337 tree.branches.get(str.charAt(i)) match { 347 def completions(str: CharSequence): List[String] = 348 lookup(str) match { 349 case Some((true, tree)) => dest(tree, List(str.toString))
|
/seL4-l4v-10.1.1/HOL4/tools-poly/poly/ |
H A D | Help.sml | 57 dir ^ str slash ^ file 111 fun instr s str = 115 String.sub (s, j) = Char.toLower (String.sub (str, k)) andalso eq (j+1) (k+1) 116 val stop = String.size str - len 119 fun occurshere str = 122 | SOME s => instr s str
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/lisp/ |
H A D | a2ml.lisp | 155 (defun set-cbd-fn-state (str state) 157 (set-cbd-fn str state) 162 str))
|