/seL4-l4v-master/HOL4/examples/machine-code/x64_compiler/ |
H A D | x64_codegenLib.sml | 103 fun replace_char c str = 104 String.translate (fn x => if x = c then str else implode [x]); 124 val str = implode (repeatc m #" ") value 128 val zs = map (fn (x,y) => (x, option_concat str y)) ys 295 val str = code2string code false value 296 in print ("\n" ^ str ^ "\n") end
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | kernel.c | 672 static char str[100]; local 673 sprintf(str, "BuDDy - release %d.%d", VERSION/10, VERSION%10); 674 return str;
|
/seL4-l4v-master/HOL4/src/datatype/mutrec/ |
H A D | MutRecDef.sml | 208 (fn tyname => fn str => str ^ "_" ^ tyname) 318 | get_var_info {arg_info = (being_defined str)::arg_info, 326 val rec_num_term = mk_hol_num (type_num str) 526 | (being_defined str) => 528 let val ty = mk_type{Tyop = str, Args = type_arg_vars} 569 fun get_type str = 570 (case find (fn entry => str = #type_name entry) ty_defs 990 | mk_case_aux {arg_info = (being_defined str)::arg_info, 1016 case find (fn entry => str [all...] |
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | internal_functions.sml | 278 val s = String.translate (fn c => if c = #"\r" then "" else String.str c) s 288 val str = fix_nls (TextIO.inputAll ins) value 290 if OS.Process.isSuccess (reap proc) then str else ""
|
H A D | ReadHMF.sml | 99 val (result, rest) = position (str dchar) (ss s') 100 val _ = size rest <> 0 orelse error b ("No matching "^str dchar) 113 | _ => error b ("Bad argument delimiter: "^str c) 262 String.toString (str c1) ^ "\"")
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | CommonDialog.sml | 323 fun allocAndInitialise(space: int, str: string) = 326 val space = Int.max(space, size str) + 1 329 stringToBuf(buf, 0, str); 569 | TemplateResource(hInst, IdAsString str) => 571 val s = toCstring str 780 | TemplateResource(hInst, IdAsString str) => 782 val s = toCstring str 1008 fun copyString b str = 1010 stringToBuf(b, 0, str); 1011 b ++ Word.fromInt(size str 1088 val str = (Word.toInt sizePageSD, owner, devmode, devnames, flags, value [all...] |
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | ParseDoc.sml | 38 fun fetch str = Substring.string (fetch_contents str); 299 raise ParseError ("Illegal character "^str (sub(ssb,0))^ " in "^
|
H A D | Doc2Html.sml | 34 fun encode c = Option.getOpt(txt_helper c, String.str c) 80 | del_bslash c = String.str c;
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | TypeBase.sml | 25 List [Sym tag, String str, Thm th] => 27 case simpfrag.lookup_simpfrag_conv str of 30 ("No function "^str^" registered");
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | IR.sml | 138 fun inspectVar str = 139 case H.peek (!symbolT) str of 143 tmpT := T.enter(!tmpT, i, str); 144 H.insert (!symbolT) (str, i);
|
/seL4-l4v-master/HOL4/src/TeX/ |
H A D | munger.lex | 33 else String.translate (fn #"c" => "\\," | c => "\\" ^ str c) s
|
/seL4-l4v-master/HOL4/src/prekernel/ |
H A D | stringfindreplace.sml | 40 Binarymap.foldl (fn (c,t,a) => recurse (k ^ str c) a t) acc (dictOf t)
|
/seL4-l4v-master/HOL4/tools-poly/Holmake/ |
H A D | winNT-systeml.sml | 75 fun munge s = String.translate (fn #"/" => "\\" | c => str c) s
|
/seL4-l4v-master/HOL4/developers/ |
H A D | generateBuildSummary.sml | 42 val remove_nulls = String.translate (fn #"\000" => "^@" | c => str c)
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | bddTools.sml | 46 SOME(str,_) => mk_var(str,bool) 66 SOME(str,_) => mk_var(str,bool)
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/calculator/ |
H A D | parser.y | 408 if (bdd_fnprintdot(fname->str, ((nodeData*)hd.def)->val) < 0) 409 cout << "Could not open file: " << fname->str << endl;
|
/seL4-l4v-master/HOL4/examples/formal-languages/context-free/ |
H A D | grammarLib.sml | 165 getc ("EOF while looking for "^str c^" of "^s) >- 167 else fail ("token: didn't find "^str c^" of "^s)) 310 SOME {Tyop,...} => str (String.sub(Tyop,0)) 311 | NONE => str (String.sub(dest_vartype ty,1))
|
/seL4-l4v-master/HOL4/src/opentheory/ |
H A D | OpenTheoryMap.sml | 23 val component = String.translate (fn #"." => "\\." | #"\"" => "\\\"" | #"\\" => "\\\\" | c => String.str c)
|
/seL4-l4v-master/HOL4/src/postkernel/ |
H A D | Theory.sml | 1049 fun new_theory str = 1050 if not(Lexis.ok_identifier str) then 1052 ("proposed theory name "^Lib.quote str^" is not an identifier") 1056 val tdelta = TheoryDelta.NewTheory{oldseg=thyname,newseg=str} 1057 fun mk_thy () = (HOL_MESG ("Created theory "^Lib.quote str); 1058 makeCT(fresh_segment str); 1063 if str=thyname then 1064 (HOL_MESG("Restarting theory "^Lib.quote str); 1065 zapCT str; 1067 else if mem str (ancestr [all...] |
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibTptp.sml | 66 val exact_puncts = f o map (fn c => exact (Punct, str c) >> K ()) o explode; 75 ((some symbol || some punct) >> (fn c => (Punct, str c))))) >> snd;
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | term_pp_utils.sml | 10 fun PP_ERR fname str = Feedback.mk_HOL_ERR "term_pp_utils" fname str
|
H A D | type_pp.sml | 99 else "'" ^ str (Char.chr (Char.ord #"a" + i)) 173 fun tab i = str (Char.chr (Char.ord #"e" + i))
|
/seL4-l4v-master/graph-refine/graph-to-graph/ |
H A D | imm_utils.py | 46 s_bound = str(bound)
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | elfexport.cpp | 420 unsigned long ELFExport::makeStringTableEntry(const char *str, ExportStringTable *stab) argument 422 if (str == NULL || str[0] == 0) 425 return stab->makeEntry(str);
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | fmap_encodeScript.sml | 660 (!a b c. lexorder (sym a b) (str c) = nil) /\ 663 (!a b c. lexorder (str a) (sym b c) = t)``, 736 ``equal (str x) (str y) = bool (x = y)``, 758 ``alphorder (str x) (str y) = ite (string_less_equal (str x) (str y)) t nil``, 781 ``!a b. lexorder (str a) (str [all...] |