/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Active.sig | 10 (* A type of active clause sets. *) 23 type active type 31 val size : active -> int 33 val saturation : active -> Clause.clause list 36 (* Create a new active clause set and initialize clauses. *) 41 active * {axioms : Clause.clause list, conjecture : Clause.clause list} 44 (* Add a clause into the active set and deduce all consequences. *) 47 val add : active -> Clause.clause -> active * Clause.clause list 53 val pp : active Prin [all...] |
H A D | Resolution.sml | 16 {active : Active.parameters, 22 active : Active.active, 30 {active = Active.default, 35 val {active = activeParm, waiting = waitingParm} = parameters value 37 val (active,cls) = Active.new activeParm ths (* cls = factored ths *) value 41 Resolution {parameters = parameters, active = active, waiting = waiting} 52 fun active (Resolution {active function 99 val (active,cls) = Active.add active cl value [all...] |
H A D | Resolution.sig | 14 {active : Active.parameters, 29 val active : resolution -> Active.active value
|
H A D | Active.sml | 208 (* A type of active clause sets. *) 218 datatype active = type 236 fun setRewrite active rewrite = 240 subterms,allSubterms,...} = active 285 fun saturation active = 295 val cls = clauses active 300 val Active {parameters,...} = active 315 fun toStr active = "Active{" ^ Int.toString (size active) ^ "}" 432 fun simplifyActive simp active 771 val active = setRewrite active rewrite value 824 val active = addFactorClause active cl value 846 val (active,_,acc) = List.foldl factor1 (active,subsume,acc) cls value 847 val (active,cls) = extract_rewritables active value 878 val active = empty parameters value 879 val (active,axioms) = factor active (List.map mk_clause axioms) value 880 val (active,conjecture) = factor active (List.map mk_clause conjecture) value 900 val active = addClause active cl value 903 val (active,cls) = factor active cls value [all...] |
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Active.sig | 10 (* A type of active clause sets. *) 23 type active type 31 val size : active -> int 33 val saturation : active -> Clause.clause list 36 (* Create a new active clause set and initialize clauses. *) 41 active * {axioms : Clause.clause list, conjecture : Clause.clause list} 44 (* Add a clause into the active set and deduce all consequences. *) 47 val add : active -> Clause.clause -> active * Clause.clause list 53 val pp : active Prin [all...] |
H A D | Resolution.sml | 16 {active : Active.parameters, 22 active : Active.active, 30 {active = Active.default, 35 val {active = activeParm, waiting = waitingParm} = parameters value 37 val (active,cls) = Active.new activeParm ths (* cls = factored ths *) value 41 Resolution {parameters = parameters, active = active, waiting = waiting} 52 fun active (Resolution {active function 99 val (active,cls) = Active.add active cl value [all...] |
H A D | Resolution.sig | 14 {active : Active.parameters, 29 val active : resolution -> Active.active value
|
H A D | Active.sml | 208 (* A type of active clause sets. *) 218 datatype active = type 236 fun setRewrite active rewrite = 240 subterms,allSubterms,...} = active 285 fun saturation active = 295 val cls = clauses active 300 val Active {parameters,...} = active 315 fun toStr active = "Active{" ^ Int.toString (size active) ^ "}" 432 fun simplifyActive simp active 771 val active = setRewrite active rewrite value 824 val active = addFactorClause active cl value 846 val (active,_,acc) = List.foldl factor1 (active,subsume,acc) cls value 847 val (active,cls) = extract_rewritables active value 878 val active = empty parameters value 879 val (active,axioms) = factor active (List.map mk_clause axioms) value 880 val (active,conjecture) = factor active (List.map mk_clause conjecture) value 900 val active = addClause active cl value 903 val (active,cls) = factor active cls value [all...] |
/seL4-l4v-master/HOL4/examples/RL_Environment/ |
H A D | RL_Socket.sig | 2 val sendStr : ('a, Socket.active Socket.stream) Socket.sock * string -> int 3 val receive : ('a, Socket.active Socket.stream) Socket.sock -> string
|
/seL4-l4v-master/isabelle/src/Pure/Concurrent/ |
H A D | consumer_thread.scala | 47 private var active = true 51 def is_active: Boolean = active && thread.isAlive 81 else error("Consumer thread not active: " + quote(thread.getName)) 121 synchronized { if (is_active) { active = false; mailbox.send(None) } }
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Concurrent/ |
H A D | consumer_thread.scala | 47 private var active = true 51 def is_active: Boolean = active && thread.isAlive 81 else error("Consumer thread not active: " + quote(thread.getName)) 121 synchronized { if (is_active) { active = false; mailbox.send(None) } }
|
/seL4-l4v-master/l4v/spec/haskell/include/ |
H A D | gic.h | 21 uint32_t active[32]; /* [0x300, 0x380) */ member in struct:gic_dist_map_t
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | gc_mark_phase.cpp | 148 bool active; member in class:MTGCProcessMarkPointers 181 MTGCProcessMarkPointers::MTGCProcessMarkPointers(): msp(0), active(false), locPtr(0) 237 if (! markStacks[i].active) 244 marker->active = true; 293 marker->active = false; // It's finished 600 marker->active = true; 618 marker->active = false; 678 marker->active = true; 696 marker->active = false;
|
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | debugger.scala | 54 active: Int = 0, // active views 63 def is_active: Boolean = active > 0 64 def inc_active: State = copy(active = active + 1) 65 def dec_active: State = copy(active = active - 1)
|
H A D | server.scala | 351 def active(): Boolean = 396 list(db).find(server_info => server_info.name == name && server_info.active) 409 list(db).filterNot(_.active).foreach(server_info => 445 while(server_info.active) { Thread.sleep(50) } 495 if server_info.active
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | debugger.scala | 54 active: Int = 0, // active views 63 def is_active: Boolean = active > 0 64 def inc_active: State = copy(active = active + 1) 65 def dec_active: State = copy(active = active - 1)
|
H A D | server.scala | 351 def active(): Boolean = 396 list(db).find(server_info => server_info.name == name && server_info.active) 409 list(db).filterNot(_.active).foreach(server_info => 445 while(server_info.active) { Thread.sleep(50) } 495 if server_info.active
|
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/ |
H A D | pretty_tooltip.scala | 74 /* pending event and active state */ // owned by GUI thread 77 private var active = true 89 if (active) { 103 active = true 109 active = false
|
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | pretty_tooltip.scala | 74 /* pending event and active state */ // owned by GUI thread 77 private var active = true 89 if (active) { 103 active = true 109 active = false
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Socket.sml | 27 type active type 72 val getATMARK : ('af, active stream) sock -> bool 81 -> ('af, active stream) sock * 'af sock_addr 83 -> (('af, active stream) sock * 'af sock_addr) option 109 val sendVec : ('af, active stream) sock * Word8VectorSlice.slice -> int 110 val sendArr : ('af, active stream) sock * Word8ArraySlice.slice -> int 111 val sendVec' : ('af, active stream) sock * Word8VectorSlice.slice 113 val sendArr' : ('af, active stream) sock * Word8ArraySlice.slice 115 val sendVecNB : ('af, active stream) sock * Word8VectorSlice.slice -> int option 116 val sendArrNB : ('af, active strea 179 and active = ACTIVE type [all...] |
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | MATCH_COMPILER.sml | 619 fun pattDepth (Aot {patts=TupleField pl, ...}, active) = 620 List.foldl (fn (t, d) => Int.max(pattDepth(t, active), d)) 0 pl 622 | pattDepth (Aot {patts, defaults,...}, active) = 624 val activeDefaults = defaults intersect active 641 fun bestColumn(colsToDo, noOfCols, asTuples, active) = 649 val thisDepth = pattDepth (List.nth(asTuples, column), active) 697 fun pattCode(Aot {patts, defaults, vars, ...}, active: patSet, nextMatch: patSet * int -> pattCode, tupleNo) = 699 (* Get the set of defaults which are active. *) 700 val activeDefaults = defaults intersect active 746 (* If the active se [all...] |
/seL4-l4v-master/isabelle/src/Doc/Eisbach/document/ |
H A D | root.tex | 49 % This sort of command for each active author can be convenient
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Eisbach/document/ |
H A D | root.tex | 49 % This sort of command for each active author can be convenient
|
/seL4-l4v-master/l4v/camkes/adl-spec/document/ |
H A D | intro.tex | 23 \item \emph{Distinction between active and passive components.} Components
|
/seL4-l4v-master/seL4/src/arch/arm/object/ |
H A D | vcpu.c | 32 static void vcpu_save(vcpu_t *vcpu, bool_t active) argument 39 /* If we aren't active then this state already got stored when 41 if (active) { 54 armv_vcpu_save(vcpu, active); 130 /* Current VCPU being active should indicate that the current thread 145 /* We shouldn't get a VGICMaintenance interrupt while a VCPU isn't active, 152 printf("Received VGIC maintenance without active VCPU!\n"); 204 /* Current VCPU being active should indicate that the current thread
|