Searched refs:str (Results 76 - 100 of 332) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DBool.sml38 fun scan (getc: (char, 'a) StringCvt.reader) (str: 'a) : (bool * 'a) option =
41 val strm = StringCvt.skipWS getc str
H A DByte.sml48 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 DEncode.sml50 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 DDataSize.sml29 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 DdaisyScript.sml38 (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 Douter_syntax.scala24 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 Douter_syntax.scala24 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 Dhyp_traps.S103 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 Dlhs_pars.py517 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 Dgraph-refine.py117 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 Dsyntax.py306 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 DBackendIntermediateCode.sml401 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 Drelease.py106 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 DARM_proverLib.sml78 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 Dregexp2dfa.sml12 | 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 Dgraph_specsLib.sml51 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 DHtmlsigs.sml75 | 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 "&nbsp;&nbsp;"))
376 app out ["\n</ul>\n\n<a name=\"", str c1, "\">"];
377 subheader (str c1);
H A DDoc2Tex.sml13 fun out(str,s) = TextIO.output(str, s)
76 | c => str c)
/seL4-l4v-10.1.1/HOL4/src/portableML/
H A DUTF8.sml12 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 DHoldep.sml21 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 Dreals.cpp117 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 Dscan.scala331 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 Dscan.scala331 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 DHelp.sml57 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 Da2ml.lisp155 (defun set-cbd-fn-state (str state)
157 (set-cbd-fn str state)
162 str))

Completed in 313 milliseconds

1234567891011>>