/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/bytecode/ |
H A D | lisp_alt_semanticsScript.sml | 22 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 D | lisp_semanticsScript.sml | 169 (!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 D | lisp_extractScript.sml | 44 ``!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 D | stmonad.sig | 7 val ok : ('a, unit) stmonad value
|
H A D | optmonad.sml | 12 fun ok env = return () env function 43 fun repeatn' 0 f = ok 49 fun repeat p env = ((p >> repeat p) ++ ok) env
|
H A D | stmonad.sml | 16 fun ok s = return () s function
|
H A D | errormonad.sig | 10 val ok : ('a, unit, 'c) t value
|
H A D | seqmonad.sml | 5 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 D | errormonad.sml | 12 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 D | optmonad.sig | 8 val ok : ('a, unit) optmonad value
|
H A D | seqmonad.sig | 8 val ok : ('a, unit) seqmonad value
|
/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/ |
H A D | milawa_execScript.sml | 29 (!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 D | Heap.h | 64 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 D | holdeptool.sml | 5 fun ok () = OS.Process.exit OS.Process.success function 25 | ["-h"] => usage ok
|
/seL4-l4v-master/isabelle/src/Pure/PIDE/ |
H A D | document_status.scala | 164 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 D | document_status.scala | 164 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 D | multibuild.sml | 58 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 D | genscriptdep.sml | 32 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 D | lisp_opsScript.sml | 54 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 D | irq.py | 85 ok = False 96 ok = True 106 if not ok:
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | bddio.c | 384 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 D | cppext.cxx | 83 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 D | selftest.sml | 29 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 D | build_doc.scala | 47 if (res1.ok) { 56 if (res2.ok) {
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/ |
H A D | build_doc.scala | 47 if (res1.ok) { 56 if (res2.ok) {
|