Searched refs:ok (Results 1 - 25 of 140) sorted by relevance

123456

/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/bytecode/
H A Dlisp_alt_semanticsScript.sml22 RR_ev (Const s, a,fns,io,ok) (s,fns,io,ok))
26 RR_ev (Var x,a,fns,io,ok) (a ' x,fns,io,ok))
29 RR_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
30 RR_ev (Or [],a,fns,io,ok) (s,fns1,io1,ok1))
33 RR_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ isTrue s1 ==>
34 RR_ev (Or (t::ts),a,fns,io,ok) (s1,fns1,io1,ok1))
37 RR_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~(isTrue s1) /\
39 RR_ev (Or (t::ts),a,fns,io,ok) (s
[all...]
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/spec/
H A Dlisp_semanticsScript.sml169 (!s a fns io ok.
170 R_ev (Const s, a,fns,io,ok) (s,fns,io,ok))
172 (!x (a: string |-> SExp) fns io ok.
174 R_ev (Var x,a,fns,io,ok) (a ' x,fns,io,ok))
176 (!a fns io ok s fns1 io1 ok1.
177 R_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
178 R_ev (Or [],a,fns,io,ok) (s,fns1,io1,ok1))
180 (!a fns io s1 fns1 io1 t ts ok
[all...]
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractScript.sml44 ``!x. x IN FDOM e ==> R_ev (Var x,e,fns,io,ok) (e ' x,fns,io,ok)``,
48 ``!x. T ==> R_ev (Const x,e,fns,io,ok) (x,fns,io,ok)``,
54 (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
56 R_ev (If x y z,e,fns,io,ok)
67 (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
69 R_ev (If x y z,e,fns,io,ok)
78 (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
80 R_ev (Or (x::y::xs),e,fns,io,ok)
[all...]
/seL4-l4v-master/HOL4/src/portableML/monads/
H A Dstmonad.sig7 val ok : ('a, unit) stmonad value
H A Doptmonad.sml12 fun ok env = return () env function
43 fun repeatn' 0 f = ok
49 fun repeat p env = ((p >> repeat p) ++ ok) env
H A Dstmonad.sml16 fun ok s = return () s function
H A Derrormonad.sig10 val ok : ('a, unit, 'c) t value
H A Dseqmonad.sml5 fun ok env = seq.result (env, ()) function
50 fun repeatn' 0 f = ok
56 fun repeat p env = ((p >> repeat p) ++ ok) env
H A Derrormonad.sml12 fun ok e = return () e (* eta-expanded b/c of value restriction *) function
42 fun repeatn' 0 f = ok
49 fun repeat p env = ((p >> repeat p) ++ ok) env
H A Doptmonad.sig8 val ok : ('a, unit) optmonad value
H A Dseqmonad.sig8 val ok : ('a, unit) seqmonad value
/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_execScript.sml29 (!s a fns ok.
30 MR_ev (Const s,a,ctxt:context_type,fns,ok) (s,ok))
32 (!x (a: string |-> SExp) fns ok.
34 MR_ev (Var x,a,ctxt,fns,ok) (FAPPLY a x,ok))
36 (!a fns ok s ok1.
37 MR_ev (Const (Sym "NIL"),a,ctxt,fns,ok) (s,ok1) ==>
38 MR_ev (Or [],a,ctxt,fns,ok) (s,ok1))
40 (!a fns s1 t ts ok
[all...]
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DHeap.h64 bool ok(int n) { return n >= 0 && n < (int)indices.size(); }
70 bool inHeap (int n) { assert(ok(n)); return indices[n] != 0; }
71 void increase (int n) { assert(ok(n)); assert(inHeap(n)); percolateUp(indices[n]); }
75 assert(ok(n));
/seL4-l4v-master/HOL4/tools/Holmake/
H A Dholdeptool.sml5 fun ok () = OS.Process.exit OS.Process.success function
25 | ["-h"] => usage ok
/seL4-l4v-master/isabelle/src/Pure/PIDE/
H A Ddocument_status.scala164 def ok: Boolean = failed == 0
175 JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
225 val ok, failed, pending = Value
256 if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
290 var ok = 0
296 case Overall_Node_Status.ok => ok += 1
302 "Nodes_Status(ok
[all...]
/seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/
H A Ddocument_status.scala164 def ok: Boolean = failed == 0
175 JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
225 val ok, failed, pending = Value
256 if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
290 var ok = 0
296 case Overall_Node_Status.ok => ok += 1
302 "Nodes_Status(ok
[all...]
/seL4-l4v-master/HOL4/tools/Holmake/poly/
H A Dmultibuild.sml58 fun genjob (g,ok) =
59 case (ok,find_runnable g) of
61 | (true, NONE) => NoMoreJobs (g, ok)
73 else GiveUpAndDie (g, ok)
113 fun update ((g,ok), b) =
117 val ok' = status = Succeeded orelse keep_going
119 (g',ok')
142 fun update ((g,ok), b) =
H A Dgenscriptdep.sml32 fun usage ok =
34 val strm = if ok then TextIO.stdOut else TextIO.stdErr
37 Process.exit (if ok then Process.success else Process.failure)
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_opsScript.sml54 zLISP_ALT side (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) =
61 cond (lisp_inv (a1,a2,sl,sl1,e,ex,cs,ok) (x0,x1,x2,x3,x4,x5,^VAR_REST)
66 zLISP_R (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) =
73 cond (lisp_inv (a1,a2,sl,sl1,e,ex,cs,ok) (x0,x1,x2,x3,x4,x5,^VAR_REST)
88 ``zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)``
298 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = r2) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
299 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,p+3w::qs,code,amnt,ok) * zPC r2``
308 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = r2) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
309 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,r2::qs,code,amnt,ok) * zPC (p+2w)``
318 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zP
[all...]
/seL4-l4v-master/seL4/tools/hardware/
H A Dirq.py85 ok = False
96 ok = True
106 if not ok:
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/
H A Dbddio.c384 int ok; local
389 ok = bdd_save(ofile, r);
391 return ok;
478 int ok; local
483 ok = bdd_load(ifile, root);
485 return ok;
H A Dcppext.cxx83 int ok = bdd_init(n,c); local
88 return ok;
424 int ok, first; local
460 ok=1;
462 for (i=0 ; i<binsize && ok ; i++)
464 ok = 0;
467 ok = 0;
469 if (ok)
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/
H A Dselftest.sml29 val ok = snd ((holfootLib.holfoot_interactive_verify_spec (not quiet) (not quiet) (concat [examples_dir, file]) (SOME [generate_vcs]) [])); value
31 val _ = if (not ok andalso hard_fail) then Process.exit Process.failure else ();
32 in ok end
/seL4-l4v-master/isabelle/src/Pure/Admin/
H A Dbuild_doc.scala47 if (res1.ok) {
56 if (res2.ok) {
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/
H A Dbuild_doc.scala47 if (res1.ok) {
56 if (res2.ok) {

Completed in 185 milliseconds

123456