| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
| H A D | ppc_encodeLib.sml | 48 val qs = zip y xs value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
| H A D | x86_encodeLib.sml | 37 val qs = map (fn (s,n) => (s,prod (f #"*" n))) zs value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
| H A D | codegenLib.sml | 155 val qs = map foo zs value
330 val qs = list_dest dest_star (fst_sep_disj q) value
355 val qs = filter (fn tm => mem (car tm) xs) qs value
356 val qs = map (fn tm => add_conditional(foo (cdr tm),car tm,th,l)) qs value
[all...] |
| H A D | compilerLib.sml | 264 val qs = map (fn f => (f,list_find f (!to_compile))) (rev fnames) value
|
| H A D | reg_allocLib.sml | 423 val qs = map snd (filter (fn (v,ns) => coalesced v = x) graph) value
424 val qs = map coalesced (append_lists qs) value
430 val qs = map snd (filter (fn (v,ns) => coalesced v = x) graph) value
431 val qs = map coalesced (append_lists qs) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/ |
| H A D | x64_codegenLib.sml | 137 val qs = map foo zs value
229 val qs = list_dest dest_star (fst_sep_disj q) value
254 val qs = filter (fn tm => mem (car tm) xs) qs value
255 val qs = map (fn tm => add_conditional(foo (cdr tm),car tm,th,l)) qs value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
| H A D | x64_encodeLib.sml | 37 val qs = map (fn (s,n) => (s,prod (f #"*" n))) zs value
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | Parse_support.sml | 526 val qs = map mk_bvar (#free e1) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | stack_analysisLib.sml | 31 val qs = list_dest dest_star post value
|
| H A D | graph_specsLib.sml | 140 val qs = ps |> map find_all_matches |> flatten value
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | core_decompilerLib.sml | 322 val qs = map (fn (x, y, z) => (x, y, map hd z)) zs value
324 val qs = map (fn (x, y, z) => (x, all_distinct (f x y @ f x z))) qs value
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | cacheTools.sml | 84 val ps = fromHOLstring p val qs = fromHOLstring q value
|
| H A D | lzPairRules.sml | 2495 val qs = map (subst renaming) gen_ps value
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | unix_specific.cpp | 1213 int qs = get_C_long(taskData, DEREFHANDLE(args)->Get(1)); local
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_codegenScript.sml | 1606 val qs = filter (not o can dest_sep_hide) (list_dest dest_star q) value
1608 val qs = filter (fn tm => not (car tm = pc) handle HOL_ERR _ => true) qs value
1612 val qs = sorter qs value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/coretypes/ |
| H A D | PairRules.sml | 2475 val qs = map (subst renaming) gen_ps value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
| H A D | helperLib.sml | 1134 val (qs,q) = hd (filter (fn (x,y) => mem lhs x) ys) value
1313 val qs = (list_dest dest_conj o fst o dest_imp) tm value
1314 val qs = (filter (can (dest_fun2set)) qs) value
1354 val (qs,f,df) = dest_fun2set x value
1407 val qs = (list_dest dest_conj o fst o dest_imp) tm value
1408 val qs = (filter (can (dest_fun2set)) qs) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/decompiler/ |
| H A D | decompilerLib.sml | 529 val qs = map (fn (x,y,z) => (x,y,map hd z)) zs value
531 val qs = map (fn (x,y,z) => (x,all_distinct (f x y @ f x z))) qs value
|