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

1234567891011>>

/seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/HOL4/src/TeX/
H A Dmunger.lex33 else String.translate (fn #"c" => "\\," | c => "\\" ^ str c) s
/seL4-l4v-10.1.1/HOL4/src/opentheory/
H A DOpenTheoryMap.sml23 val component = String.translate (fn #"." => "\\." | #"\"" => "\\\"" | #"\\" => "\\\\" | c => String.str c)
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A Dstringfindreplace.sml40 Binarymap.foldl (fn (c,t,a) => recurse (k ^ str c) a t) acc (dictOf t)
/seL4-l4v-10.1.1/HOL4/tools-poly/Holmake/
H A DwinNT-systeml.sml75 fun munge s = String.translate (fn #"/" => "\\" | c => str c) s
/seL4-l4v-10.1.1/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-10.1.1/HOL4/developers/
H A DgenerateBuildSummary.sml42 val remove_nulls = String.translate (fn #"\000" => "^@" | c => str c)
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/correctness/
H A Diclass_compLib.sml73 val classes = [`unexec`,`swp`,`mrs_msr`,`data_proc`,`reg_shift`,`ldr`,`str`,
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DbddTools.sml46 SOME(str,_) => mk_var(str,bool)
66 SOME(str,_) => mk_var(str,bool)
/seL4-l4v-10.1.1/HOL4/src/holyhammer/legacy/
H A Dhh_write.ml48 let string_list_of_string str sep =
49 let rec slos_aux str ans =
50 if str = "" then ans else
52 let first_space = String.index str sep in
54 slos_aux (String.sub str 1 (String.length str - 1)) ans
57 (String.sub str (first_space + 1)(String.length str - 1 - first_space))
58 ((String.sub str 0 (first_space)) :: ans)
61 List.rev (str
[all...]
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DTheory.sml994 fun new_theory str =
995 if not(Lexis.ok_identifier str) then
997 ("proposed theory name "^Lib.quote str^" is not an identifier")
1001 val tdelta = TheoryDelta.NewTheory{oldseg=thyname,newseg=str}
1002 fun mk_thy () = (HOL_MESG ("Created theory "^Lib.quote str);
1003 makeCT(fresh_segment str);
1008 if str=thyname then
1009 (HOL_MESG("Restarting theory "^Lib.quote str);
1010 zapCT str;
1012 else if mem str (ancestr
[all...]
/seL4-l4v-10.1.1/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-10.1.1/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))
171 fun tab i = str (Char.chr (Char.ord #"e" + i))
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/
H A Dimm_utils.py48 s_bound = str(bound)
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A Dfunc_decompileLib.sml123 val str = "Section " ^ sec_name ^ " (" ^ value
125 in write_section str end
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/aarch64/
H A Dsysv.S278 str x8, [x21, #64]
/seL4-l4v-10.1.1/HOL4/help/src-sml/
H A DDoc2Html.sml34 fun encode c = Option.getOpt(txt_helper c, String.str c)
80 | del_bslash c = String.str c;
/seL4-l4v-10.1.1/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...]
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-10.1.1/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...]
/seL4-l4v-10.1.1/graph-refine/
H A Ddebug.py128 while rec and type (cond_def) == str and cond_def in rep.solv.defs:
429 if type (smt_xp) == str:
733 if type (sexpr) == str:
776 if 'Call' in str (intr):
800 if type (v) == str:
H A Dsolver.py436 assert val[0] == 'SplitMem' or type(val) == str
896 if type (mem_name) == str:
1179 trace (' --> new parallel solver %s' % str (k))
1403 if type (v) == str or '_' in v
1566 if [s for s in res if type (s) != str]:
1742 assert type (m) == str
2035 assert type (sexp) == str
2048 elif type (naming) == str:
2122 elif type (sexpr) == str:

Completed in 209 milliseconds

1234567891011>>