/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | SIGNATURES.sml | 207 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 D | Pretty.sml | 291 val str = Substring.string a value 293 val fields = String.fields (fn #"\t" => true | _ => false) str
|
/seL4-l4v-master/graph-refine/ |
H A D | debug.py | 126 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 D | solver.py | 434 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 D | problem.py | 523 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 D | stats.py | 210 return (seconds, str (datetime.timedelta (seconds = int (seconds))))
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | hol_defaxioms_proofsScript.sml | 1780 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 D | translateScript.sml | 100 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 D | IR.sml | 147 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 D | pegML.sml | 122 val mk = map str o explode
|
/seL4-l4v-master/HOL4/src/n-bit/ |
H A D | bitstringSyntax.sml | 141 String.translate (fn c => if Char.isSpace c then "" else String.str c)
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Sequence.sml | 12 (*Return next sequence element as NONE or SOME(x,str) *)
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | winNT-systeml.sml | 115 fun munge s = String.translate (fn #"/" => "\\" | c => str c) s
|
/seL4-l4v-master/HOL4/examples/ARM/arm6-verification/correctness/ |
H A D | iclass_compLib.sml | 75 val classes = [`unexec`,`swp`,`mrs_msr`,`data_proc`,`reg_shift`,`ldr`,`str`,
|
/seL4-l4v-master/HOL4/examples/ARM/v7/ |
H A D | selftest.sml | 18 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 D | conflict.py | 162 #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 D | elf_correlate.py | 348 #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 D | reconstruct.py | 466 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 D | html.scala | 45 def output_string(str: String): Unit = 46 str.iterator.foreach(output_char)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/ |
H A D | html.scala | 45 def output_string(str: String): Unit = 46 str.iterator.foreach(output_char)
|
/seL4-l4v-master/HOL4/src/postkernel/ |
H A D | TheoryReader.sml | 152 fun with_stridty (str,id,tyv) =
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | term_pp.sml | 874 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 D | liteLib.sml | 206 val (str,rm) = strip r value 207 in (l::str,rm)
|
/seL4-l4v-master/HOL4/tools/mllex/ |
H A D | mllex.sml | 297 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 D | makebase.sml | 190 handle exn as OS.SysErr (str, _) => (print(str ^ "\n\n"); raise exn)
|