/seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/HOL4/src/TeX/ |
H A D | munger.lex | 33 else String.translate (fn #"c" => "\\," | c => "\\" ^ str c) s
|
/seL4-l4v-10.1.1/HOL4/src/opentheory/ |
H A D | OpenTheoryMap.sml | 23 val component = String.translate (fn #"." => "\\." | #"\"" => "\\\"" | #"\\" => "\\\\" | c => String.str c)
|
/seL4-l4v-10.1.1/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-10.1.1/HOL4/tools-poly/Holmake/ |
H A D | winNT-systeml.sml | 75 fun munge s = String.translate (fn #"/" => "\\" | c => str c) s
|
/seL4-l4v-10.1.1/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-10.1.1/HOL4/developers/ |
H A D | generateBuildSummary.sml | 42 val remove_nulls = String.translate (fn #"\000" => "^@" | c => str c)
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/correctness/ |
H A D | iclass_compLib.sml | 73 val classes = [`unexec`,`swp`,`mrs_msr`,`data_proc`,`reg_shift`,`ldr`,`str`,
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | bddTools.sml | 46 SOME(str,_) => mk_var(str,bool) 66 SOME(str,_) => mk_var(str,bool)
|
/seL4-l4v-10.1.1/HOL4/src/holyhammer/legacy/ |
H A D | hh_write.ml | 48 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 D | Theory.sml | 994 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 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-10.1.1/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)) 171 fun tab i = str (Char.chr (Char.ord #"e" + i))
|
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
H A D | imm_utils.py | 48 s_bound = str(bound)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | func_decompileLib.sml | 123 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 D | sysv.S | 278 str x8, [x21, #64]
|
/seL4-l4v-10.1.1/HOL4/help/src-sml/ |
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-10.1.1/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...] |
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-10.1.1/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...] |
/seL4-l4v-10.1.1/graph-refine/ |
H A D | debug.py | 128 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 D | solver.py | 436 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:
|