Searched refs:str (Results 176 - 200 of 345) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/examples/machine-code/x64_compiler/
H A Dx64_codegenLib.sml103 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 Dkernel.c672 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 DMutRecDef.sml208 (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 Dinternal_functions.sml278 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 DReadHMF.sml99 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 DCommonDialog.sml323 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 DParseDoc.sml38 fun fetch str = Substring.string (fetch_contents str);
299 raise ParseError ("Illegal character "^str (sub(ssb,0))^ " in "^
H A DDoc2Html.sml34 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 DTypeBase.sml25 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 DIR.sml138 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 Dmunger.lex33 else String.translate (fn #"c" => "\\," | c => "\\" ^ str c) s
/seL4-l4v-master/HOL4/src/prekernel/
H A Dstringfindreplace.sml40 Binarymap.foldl (fn (c,t,a) => recurse (k ^ str c) a t) acc (dictOf t)
/seL4-l4v-master/HOL4/tools-poly/Holmake/
H A DwinNT-systeml.sml75 fun munge s = String.translate (fn #"/" => "\\" | c => str c) s
/seL4-l4v-master/HOL4/developers/
H A DgenerateBuildSummary.sml42 val remove_nulls = String.translate (fn #"\000" => "^@" | c => str c)
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DbddTools.sml46 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 Dparser.y408 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 DgrammarLib.sml165 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 DOpenTheoryMap.sml23 val component = String.translate (fn #"." => "\\." | #"\"" => "\\\"" | #"\\" => "\\\\" | c => String.str c)
/seL4-l4v-master/HOL4/src/postkernel/
H A DTheory.sml1049 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 DmlibTptp.sml66 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 Dterm_pp_utils.sml10 fun PP_ERR fname str = Feedback.mk_HOL_ERR "term_pp_utils" fname str
H A Dtype_pp.sml99 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 Dimm_utils.py46 s_bound = str(bound)
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Delfexport.cpp420 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 Dfmap_encodeScript.sml660 (!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...]

Completed in 170 milliseconds

1234567891011>>