Searched refs:str (Results 201 - 225 of 345) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DSIGNATURES.sml207 fun displaySigs (str, depth) =
212 case str of
452 fun sigVal(str : sigs,
695 giveError (str, locn, lex) (msg ^ " in signature.")
735 giveError (str, lno, lex)("Signature (" ^ name ^ ") has not been declared");
740 fun sigValue (str : sigs, Env env : env, _ : LEX.location, structPath) =
741 case str of
814 giveError (str, line, lex) (msg ^ " in signature.")
834 giveError (str, locn, lex))
966 errorNear (lex, true, fn n => displaySigs(str,
[all...]
H A DPretty.sml291 val str = Substring.string a value
293 val fields = String.fields (fn #"\t" => true | _ => false) str
/seL4-l4v-master/graph-refine/
H A Ddebug.py126 while rec and type (cond_def) == str and cond_def in rep.solv.defs:
427 if type (smt_xp) == str:
731 if type (sexpr) == str:
774 if 'Call' in str (intr):
798 if type (v) == str:
H A Dsolver.py434 assert val[0] == 'SplitMem' or type(val) == str
894 if type (mem_name) == str:
1177 trace (' --> new parallel solver %s' % str (k))
1401 if type (v) == str or '_' in v
1564 if [s for s in res if type (s) != str]:
1740 assert type (m) == str
2033 assert type (sexp) == str
2046 elif type (naming) == str:
2120 elif type (sexpr) == str:
H A Dproblem.py523 if type (n) == str:
534 elif type (details) != str:
535 details = '_'.join (map (str, details))
581 if type (c) != str]) for n in nodes])
H A Dstats.py210 return (seconds, str (datetime.timedelta (seconds = int (seconds))))
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A Dhol_defaxioms_proofsScript.sml1780 str s``,
1954 (str "ACL2-PKG-WITNESS"),
1960 ``|= equal (symbol_name (pkg_witness pkg_name)) (str "ACL2-PKG-WITNESS")``,
1976 (ite (stringp pkg_name) pkg_name (str ACL2)),
1995 (ite (andl[stringp pkg_name;not (equal pkg_name (str ""))])
1997 (str ACL2))``,
2042 equal (symbol_package_name y) (str "ACL2-INPUT-CHANNEL")])
2044 (str "ACL2-INPUT-CHANNEL")),
2058 equal (symbol_package_name y) (str "ACL2-INPUT-CHANNEL")])
2060 (str "ACL
[all...]
H A DtranslateScript.sml100 val fix_string_def = Define `fix_string x = if |= stringp x then x else str ""`;
111 (* Inverse to ``str : string -> sexp`` *)
142 Define `(sexp_to_string (str x) = x) /\
447 ``(sexp_to_bool o stringp) o str = K T``,
526 ``(sexp_to_string o str) = I``,
593 ``(str o sexp_to_string) = fix_string``,
1186 val STRING_EXPLODE = store_thm("STRING_EXPLODE",``list chr (EXPLODE s) = coerce (str s) (sym "COMMON-LISP" "LIST")``,
1189 val STRING_IMPLODE = store_thm("STRING_IMPLODE",``str (IMPLODE l) = coerce (list chr l) (sym "COMMON-LISP" "STRING")``,
1198 val STRING_LENGTH = store_thm("STRING_LENGTH",``nat (STRLEN s) = length (str s)``,
/seL4-l4v-master/HOL4/examples/dev/sw/
H A DIR.sml147 fun inspectVar str =
148 case H.peek (!symbolT) str of
152 tmpT := T.enter(!tmpT, i, str);
153 H.insert (!symbolT) (str, i);
/seL4-l4v-master/HOL4/examples/formal-languages/context-free/
H A DpegML.sml122 val mk = map str o explode
/seL4-l4v-master/HOL4/src/n-bit/
H A DbitstringSyntax.sml141 String.translate (fn c => if Char.isSpace c then "" else String.str c)
/seL4-l4v-master/HOL4/src/simp/src/
H A DSequence.sml12 (*Return next sequence element as NONE or SOME(x,str) *)
/seL4-l4v-master/HOL4/tools/Holmake/
H A DwinNT-systeml.sml115 fun munge s = String.translate (fn #"/" => "\\" | c => str c) s
/seL4-l4v-master/HOL4/examples/ARM/arm6-verification/correctness/
H A Diclass_compLib.sml75 val classes = [`unexec`,`swp`,`mrs_msr`,`data_proc`,`reg_shift`,`ldr`,`str`,
/seL4-l4v-master/HOL4/examples/ARM/v7/
H A Dselftest.sml18 fun test str f x = let
23 TextIO.print ("\n" ^ str ^ " ... " ^ Time.toString elapsed ^ "s" ^
675 str r1,[r2,#4]
735 str r1,[r2],#8
/seL4-l4v-master/graph-refine/graph-to-graph/
H A Dconflict.py162 #print 'fs: %s' % str(fs)
163 #print 'cs_so_far: %s' % str(cs_so_far)
176 #print ' phy_rets: %s' % str(phy_rets)
188 #print 'context: %s' % str(context)
189 #print 's: %s' % str(s)
365 print 'bbcs: %s' % str(bbCallStrings)
370 #print 'final_callee_bb: %s'% str(final_callee_bb)
552 print 'ret: %s' % str(ret)
H A Delf_correlate.py348 #print 'adding: %s' % str(p_nf)
434 print 'tags: %s'% str(p.node_tags[p_n])
465 print 'g_n %s' % str(g_n)
H A Dreconstruct.py466 print 'max_bb_addr: %x' % id_to_bb_addr[str(max_id)]
468 print_context(id_to_context[str(max_id)])
/seL4-l4v-master/isabelle/src/Pure/Thy/
H A Dhtml.scala45 def output_string(str: String): Unit =
46 str.iterator.foreach(output_char)
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/
H A Dhtml.scala45 def output_string(str: String): Unit =
46 str.iterator.foreach(output_char)
/seL4-l4v-master/HOL4/src/postkernel/
H A DTheoryReader.sml152 fun with_stridty (str,id,tyv) =
/seL4-l4v-master/HOL4/src/parse/
H A Dterm_pp.sml874 fun tm nmight_print str = let
889 NONE => Name = str
891 List.exists (mem str o term_grammar.rule_tokens G o #3) rrlist
894 fun tm might_print str =
896 COMB(Rator, Rand) => Rator might_print str orelse Rand might_print str
897 | LAMB(_,Body) => Body might_print str
898 | VAR(Name,Ty) => Name = str
899 | CONST x => tm nmight_print str
996 str
[all...]
/seL4-l4v-master/HOL4/src/lite/
H A DliteLib.sml206 val (str,rm) = strip r value
207 in (l::str,rm)
/seL4-l4v-master/HOL4/tools/mllex/
H A Dmllex.sml297 val removeTABs = String.translate (fn #"\t" => " " | c => str c)
539 String.toString (String.str ch)))
607 then get_state(prev,matched ^ String.str x)
616 getID(matched ^ String.str x)
619 in ID(getID(String.str ch))
629 then get_r(matched ^ String.str x,r1)
632 in REPS(get_r(String.str ch,~1))
676 String.toString (String.str c))))
/seL4-l4v-master/HOL4/help/src-sml/
H A Dmakebase.sml190 handle exn as OS.SysErr (str, _) => (print(str ^ "\n\n"); raise exn)

Completed in 164 milliseconds

1234567891011>>