/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | ppc_encodeLib.sml | 48 val qs = zip y xs value
|
/seL4-l4v-master/HOL4/polyml/Tests/ |
H A D | RunTests.sml | 129 fun qs ([], tail) = tail function
|
/seL4-l4v-master/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-master/HOL4/examples/machine-code/compiler/ |
H A D | codegenLib.sml | 184 val qs = map foo zs value 359 val qs = list_dest dest_star (fst_sep_disj q) value 385 val qs = filter (fn tm => tmem (car tm) xs) qs value 386 val qs = map (fn tm => add_conditional(foo (cdr tm),car tm,th,l)) qs value [all...] |
H A D | compilerLib.sml | 275 val qs = map (fn f => (f,list_find f (!to_compile))) (rev fnames) value
|
H A D | reg_allocLib.sml | 430 val qs = map snd (filter (fn (v,ns) => coalesced v ~~ x) graph) value 431 val qs = map coalesced (append_lists qs) value 437 val qs = map snd (filter (fn (v,ns) => coalesced v ~~ x) graph) value 438 val qs = map coalesced (append_lists qs) value [all...] |
/seL4-l4v-master/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-master/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-master/HOL4/src/parse/ |
H A D | Parse_support.sml | 526 val qs = map mk_bvar (#free e1) value
|
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | stack_analysisLib.sml | 38 val qs = list_dest dest_star post value
|
H A D | graph_specsLib.sml | 174 val qs = ps |> map find_all_matches |> flatten value
|
/seL4-l4v-master/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-master/HOL4/examples/l3-machine-code/common/ |
H A D | core_decompilerLib.sml | 323 val qs = map (fn (x, y, z) => (x, y, map hd z)) zs value 325 val qs = map (fn (x, y, z) => (x, all_distinct (f x y @ f x z))) qs value
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | unix_specific.cpp | 1092 int qs = get_C_long(taskData, DEREFHANDLE(args)->Get(1)); local
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_codegenScript.sml | 1607 val qs = filter (not o can dest_sep_hide) (list_dest dest_star q) value 1609 val qs = filter (fn tm => (car tm !~ pc) handle HOL_ERR _ => true) qs value 1613 val qs = sorter qs value [all...] |
/seL4-l4v-master/HOL4/src/coretypes/ |
H A D | PairRules.sml | 2482 val qs = map (subst renaming) gen_ps value
|
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/ |
H A D | helperLib.sml | 1155 val (qs,q) = hd (filter (fn (x,y) => tmem lhs x) ys) value 1342 val qs = (list_dest dest_conj o fst o dest_imp) tm value 1343 val qs = (filter (can (dest_fun2set)) qs) value 1384 val (qs,f,df) = dest_fun2set x value 1437 val qs = (list_dest dest_conj o fst o dest_imp) tm value 1438 val qs = (filter (can (dest_fun2set)) qs) value [all...] |
/seL4-l4v-master/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
|