/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | simplifier.sml | 30 rewrs = [], ac=[],filter=NONE,dprocs=[],congs=[]};
|
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | Stream.sml | 117 fun filter p NIL = NIL function 118 | filter p (CONS (x,xs)) = 119 if p x then CONS (x, fn () => filter p (xs ())) else filter p (xs ());
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibLiteralnet.sig | 23 val filter : ('a -> bool) -> 'a literalnet -> 'a literalnet value
|
H A D | mlibStream.sml | 97 fun filter p NIL = NIL function 98 | filter p (CONS (x,xs)) = 99 if p x then CONS (x, fn () => filter p (xs ())) else filter p (xs ());
|
H A D | mlibSubsume.sig | 21 val filter : ('a -> bool) -> 'a subsume -> 'a subsume value
|
H A D | mlibTermnet.sig | 22 val filter : ('a -> bool) -> 'a termnet -> 'a termnet value
|
H A D | mlibSolver.sml | 281 type sos_filter = {name : string, filter : thm -> bool}; 283 fun apply_sos_filter {name = sos, filter} (mlibSolver_node {name, solver_con}) = 293 else List.partition filter (hyps @ thms) 301 fun only_if_everything {name, filter} : sos_filter = 302 {name = "?" ^ name, filter = filter}; 304 val everything : sos_filter = {name = "everything", filter = K true}; 308 filter = (fn x => null x orelse List.exists negative x) o clause}; 312 filter = (fn x => null x orelse List.exists positive x) o clause}; 315 {name = "all negative", filter [all...] |
H A D | mlibCanon.sig | 26 (* A tautology filter for clauses *)
|
H A D | mlibClauseset.sml | 46 type filter = {subsumption : bool, simplification : int, splitting : bool} type 47 type parameters = {prefactoring : filter, postfactoring : filter} 53 fun update_subsumption f (parm : filter) : filter = 58 fun update_simplification f (parm : filter) : filter = 63 fun update_splitting f (parm : filter) : filter = 401 val d = List.filter pre [all...] |
/seL4-l4v-master/HOL4/src/tfl/src/ |
H A D | Rules.sml | 29 fun non_triv thl = filter (not o is_triv_rw o concl) thl 48 fun FILTER_DISCH_ALL P th = itlist DISCH (filter (sthat P) (Thm.hyp th)) th; 110 val veq = Lib.trye hd (filter (can dest_eq) (Thm.hyp thm)) 124 case filter (can (dest_eq o hd o strip_conj)) (Thm.hyp thm)
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_encodeLib.sml | 47 val imm = sum (map extract_int (filter (can extract_int) us)) 48 val vs = filter (not o can extract_int) us 49 val _ = if filter (fn (x,y) => not (x = "+")) vs = [] then () else fail() 51 val base = SOME ((snd o hd o filter (fn (x,y) => x = 1)) ks) handle e => NONE 136 val ys = filter (fn (x,y) => ((hd y = hd xs) handle _ => false)) instructions 141 (filter (fn x => not (x = "BYTE")) xs, 143 (filter (fn (x,y) => mem "r/m8" y) ys)) 155 val l = filter (fn (x,y) => not (x = y)) (zip xs ys) 207 | all_distinct (x::xs) = x::all_distinct (filter (fn y => not ((x:string) = y)) xs)
|
/seL4-l4v-master/HOL4/src/AI/machine_learning/ |
H A D | mlTacticData.sml | 58 val calls2 = filter (test o snd) calls1 67 val calls = filter (test o fst) (dlist (#calld tacdata)) 125 val filel = filter test (map f thyl) 128 val thyl3 = filter (fn x => not (mem x ["bool","min"])) thyl2
|
/seL4-l4v-master/HOL4/src/postkernel/ |
H A D | DB.sml | 98 newdata :: List.filter (not o dataNameEq s2) oldvalue) 126 val data' = List.filter (fn (_, (th, _)) => uptodate_thm th) 156 List.filter(not o dataNameEq bnm) datas) 251 fun subfold (k, v, acc) = List.filter data_P v @ acc 281 List.filter (fn (_, (th, _)) => matches pat th) dbdata ; 283 fun find_in s = List.filter (findpred s o dataName) 296 | selfn (SelTHY s) = List.filter (equal (norm_thyname s) o dataThy) 319 case filter (equal (norm_thyname thy,name) o fst) result of 332 val theorems = List.map thm_of o Lib.filter (is Thm) o thy 333 val definitions = List.map thm_of o Lib.filter (i [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/ |
H A D | helperLib.sml | 252 dprocs = [], filter = NONE, rewrs = [] } 609 val ws = filter (fn t => t ~~ subst i t) vs 632 val ts = alternatives (filter (not o frame_var) xs) ys 634 fun terms ([],x) = ((hd (filter frame_var xs),x) handle Empty => (list_mk_star [] (type_of (car tm1)),x)) 645 (filter (fn y => not (tmem y (redexes s))) (free_vars x)) 648 (filter (fn x => not (tmem x rs)) (filter frame_var xs)) 684 val ys = filter (fn y => not (tmem y (map (subst s) z))) xs 730 val xs = filter (fn tm => v IN FVs tm) (list_dest dest_star p) 815 List.filter [all...] |
/seL4-l4v-master/HOL4/src/1/ |
H A D | Ho_Rewrite.sml | 143 PURE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th 145 REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th 147 PURE_ONCE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th 149 ONCE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th;; 151 ASSUM_LIST (fn asl => PURE_REWRITE_TAC ((filter (f o concl) asl)@thl)) 153 ASSUM_LIST (fn asl => REWRITE_TAC ((filter (f o concl) asl) @ thl)) 155 ASSUM_LIST (fn l => PURE_ONCE_REWRITE_TAC ((filter (f o concl) l) @ L)) 157 ASSUM_LIST (fn asl => ONCE_REWRITE_TAC ((filter (f o concl) asl) @ thl));
|
H A D | Rewrite.sml | 211 PURE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th 213 REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th 215 PURE_ONCE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th 217 ONCE_REWRITE_RULE ((map ASSUME (filter f (hyp th))) @ thl) th;; 221 (fn asl => PURE_REWRITE_TAC ((filter (f o concl) asl)@thl)) 224 (fn asl => REWRITE_TAC ((filter (f o concl) asl) @ thl)) 227 (fn asl => PURE_ONCE_REWRITE_TAC ((filter (f o concl) asl) @ thl)) 230 (fn asl => ONCE_REWRITE_TAC ((filter (f o concl) asl) @ thl));
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | muTools.sml | 27 ::((List.filter (fn th => can (match_term 30 (List.filter (fn th => can (match_term
|
/seL4-l4v-master/isabelle/src/Tools/Graphview/ |
H A D | mutator.scala | 29 def filter(graph: Graph_Display.Graph): Graph_Display.Graph = pred(graph) 149 full_graph.keys.filter(node => (regex.r findFirstIn node.toString).isDefined).toList)) 176 def mutate(full_graph: Graph_Display.Graph, graph: Graph_Display.Graph) = filter(graph) 177 def filter(graph: Graph_Display.Graph): Graph_Display.Graph
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Graphview/ |
H A D | mutator.scala | 29 def filter(graph: Graph_Display.Graph): Graph_Display.Graph = pred(graph) 149 full_graph.keys.filter(node => (regex.r findFirstIn node.toString).isDefined).toList)) 176 def mutate(full_graph: Graph_Display.Graph, graph: Graph_Display.Graph) = filter(graph) 177 def filter(graph: Graph_Display.Graph): Graph_Display.Graph
|
/seL4-l4v-master/HOL4/tools/ |
H A D | holwrap.py | 40 filter=statement_ended, variable
|
H A D | unquote-init.sml | 9 treatment that the filter gives to things like `s1 ^ s2`
|
/seL4-l4v-master/HOL4/src/pred_set/src/ |
H A D | pred_setSimps.sml | 11 convs = [], rewrs = [], filter = NONE, dprocs = [], congs = [], 55 dprocs = [], filter = NONE
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_encodeLib.sml | 47 val imm = sum (map extract_int (filter (can extract_int) us)) 48 val vs = filter (not o can extract_int) us 49 val _ = if filter (fn (x,y) => not (x = "+")) vs = [] then () else fail() 51 val base = SOME ((snd o hd o filter (fn (x,y) => x = 1)) ks) handle e => NONE 184 val ys = filter (fn (x,y) => ((hd y = hd xs) handle _ => false)) instructions 195 x64_reg_size (hd (filter x64_is_reg xs)) 207 in filter (fn (x,y) => token_data_size (el 3 y) = s) ys end 209 ys |> filter (fn (x,y) => last y = "imm64") 210 |> map (fn (x,y) => (filter (fn t => not (mem t ["REX.W","+"])) x,y)) 211 val xs = filter (f [all...] |
/seL4-l4v-master/HOL4/src/tactictoe/src/ |
H A D | tttEval.sml | 105 val thyl' = filter (fn x => not (mem x ["min","bool"])) thyl 202 val ex2 = filter (fn x => term_size (fst (hd x)) < limit) ex1 247 val filel = filter (String.isPrefix "buildheap_") (listDir dir) 249 val satl = filter (fn (_,(x,_)) => x = ProofSaturated) totl 250 val timeoutl = filter (fn (_,(x,_)) => x = ProofSaturated) totl 251 val proofl = filter (fn (_,(x,_)) => is_proof x) totl 260 fun f bound = length (filter (fn x => x <= bound) timl)
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | seq.sig | 31 val filter : ('a -> bool) -> 'a seq -> 'a seq value
|