Searched refs:context (Results 101 - 125 of 285) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/
H A Dgr_t.sml19 "suc" and "anySuc" that do not access the full context
38 MapUtil utilities for (node->context) maps
48 updAdj (t,l,f) repeatedly updates the context entries for
86 mkContext rearranges map entry to a context value
131 fun context _ = raise NotImplemented function
193 fun context (n,(t,_)) = mkContext (n,valOf (M.find (t,n))) function
269 fun context (n,(t,_)) = mkContext (n,valOf (M.find (t,n))) function
/seL4-l4v-master/HOL4/src/1/
H A DwlogLib.sml132 val context = HOLset.listItems (FVL [c] lconst) value
133 val p = typed_parse_in_context bool context q
134 val extra_vars = map (parse_in_context context) vars_q
H A Dmatch_goal.sig31 - otherwise, match any subterm (i.e., like Coq's context patterns)
47 1. Parse quotation in context of goal (and check no free vars ending with _)
/seL4-l4v-master/HOL4/src/portableML/mosml/
H A DPrettyImpl.sml4 type context = unit type
6 PrettyBlock of int * bool * context list * pretty list
41 fun layOut(p as PrettyBlock (blockOffset, consistent, context, entries),
/seL4-l4v-master/isabelle/src/Pure/Tools/
H A Dsimplifier_trace.scala152 case (id, context) if context.questions contains serial =>
153 (id, context.questions(serial))
160 // its context, its last_serial counter will start at 0 again, and we'll think the
H A Ddebugger.scala15 /* thread context */
275 def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String)
279 SML.toString, Symbol.encode(context), Symbol.encode(expression))
285 def print_vals(c: Debugger.Context, SML: Boolean, context: String)
291 SML.toString, Symbol.encode(context))
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/
H A Dsimplifier_trace.scala152 case (id, context) if context.questions contains serial =>
153 (id, context.questions(serial))
160 // its context, its last_serial counter will start at 0 again, and we'll think the
H A Ddebugger.scala15 /* thread context */
275 def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String)
279 SML.toString, Symbol.encode(context), Symbol.encode(expression))
285 def print_vals(c: Debugger.Context, SML: Boolean, context: String)
291 SML.toString, Symbol.encode(context))
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DLEXSIG.sml45 { location: location, hard: bool, message: pretty, context: pretty option } -> unit
65 ({ location: location, hard: bool, message: pretty, context: pretty option } -> unit) Universal.tag
/seL4-l4v-master/seL4/include/arch/x86/arch/machine/
H A Ddebug.h26 * the hardware registers into the TCB context.
28 * @param context TCB breakpoint context for the thread being initialized.
30 void Arch_initBreakpointContext(user_breakpoint_state_t *context);
70 * try to pop all the context from a block of memory, but just unset all the
108 * the CS and SS in the context are set to anything sensible, so
/seL4-l4v-master/HOL4/src/integer/
H A DintSimps.sml153 val context = map concl thms value
155 val gl' = list_mk_imp(context,gl)
257 that we have accumulated a contradictory context. *)
272 apply = fn args => CDP (get_ctxt (#context args)),
/seL4-l4v-master/HOL4/src/quantHeuristics/
H A DquantHeuristicsLib.sig76 val direct_context_qp : quant_param; (* use the context, but don't recurse *)
77 val context_qp : quant_param; (* use the context *)
115 val no_ctxt_std_qp : quantHeuristicsLibBase.quant_param (* ignore context *);
116 val direct_ctxt_std_qp : quantHeuristicsLibBase.quant_param (* don't use context for weaken / strengthen *);
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Dsimplifier_trace_dockable.scala42 val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
45 context.questions.values.toList match {
H A Ddebugger_dockable.scala48 /* context menu */
52 val context = jEdit.getActionContext()
54 List(new EnhancedMenuItem(context.getAction(name).getLabel, name, context))
230 tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic"
233 new Completion_Popup.History_Text_Field("isabelle-debugger-context")
265 tooltip = "Evaluate ML expression within optional context"
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/
H A Dsimplifier_trace_dockable.scala42 val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
45 context.questions.values.toList match {
H A Ddebugger_dockable.scala48 /* context menu */
52 val context = jEdit.getActionContext()
54 List(new EnhancedMenuItem(context.getAction(name).getLabel, name, context))
230 tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic"
233 new Completion_Popup.History_Text_Field("isabelle-debugger-context")
265 tooltip = "Evaluate ML expression within optional context"
/seL4-l4v-master/HOL4/examples/miller/formalize/
H A DboolContext.sml135 (* The context *)
/seL4-l4v-master/HOL4/examples/separationLogic/src/
H A Dvars_as_resourceBaseFunctor.sml256 (false, SOME 1, fn context => REWRITE_CONV (rewrites@context))]
783 fun VAR_RES_PROP_REWRITE_CONV (do_something, ss) context =
785 SIMP_CONV (ss_final++ss++simpLib.rewrites (prepare_context [] context)) []
965 (K (fn context => (STRENGTHEN_CONSEQ_CONV (conv context)))):var_res_inference
971 (fn p => (fn context => (STRENGTHEN_CONSEQ_CONV
972 (conv (#do_prop_simps p, #prop_simp_ss p) context)))):var_res_inference
975 (fn p => (fn context => (STRENGTHEN_CONSEQ_CONV
976 (conv (#expands_level p) (#do_prop_simps p, #prop_simp_ss p) context))))
[all...]
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DCODETREE_OPTIMISER.sml819 fun optimise (context, use) (Lambda lambda) =
820 SOME(mapLambdaResult(optLambda(context, use, lambda, LCNormal)))
822 | optimise (context, use) (Newenv(envDecs, envExp)) =
824 fun mapExp mapUse = mapCodetree (optimise(context, mapUse))
830 case optLambda(context, use, lambda, LCRecursive) of
848 | optimise (context, use) (Eval {function = Lambda lambda, argList, resultType}) =
850 val args = map (fn (c, t) => (optGeneral context c, t)) argList
852 val (bindings, newLambda) = optLambda(context, [UseApply(use, argTuples)], lambda, LCImmediateCall)
858 | optimise (context as { reprocess, ...}, use) (Eval {function = Cond(i, t, e), argList, resultType}) =
865 mapCodetree (optimise(context, us
[all...]
/seL4-l4v-master/HOL4/examples/CCS/
H A DCongruenceScript.sml37 val _ = type_abbrev_pp ("context", ``:('a, 'b) CCS -> ('a, 'b) CCS``);
40 IS_CONST (e :('a, 'b) context) <=> !t1 t2. e t1 = e t2
356 (* Multi-hole context with guarded sums (GCONTEXT) *)
783 MP_TAC (Q.SPECL [`a`, `(\x. (c :('a, 'b) context) (e x))`] WG3) \\
786 MP_TAC (Q.SPECL [`(\x. (c :('a, 'b) context) (e x))`,
787 `(\x. (c' :('a, 'b) context) (e x))`] WG4) \\
790 MP_TAC (Q.SPECL [`(\x. (c :('a, 'b) context) (e x))`,
791 `(\x. (c' :('a, 'b) context) (e x))`] WG5) \\
794 MP_TAC (Q.SPECL [`L`, `(\x. (c :('a, 'b) context) (e x))`] WG6) \\
797 MP_TAC (Q.SPECL [`rf`, `(\x. (c :('a, 'b) context) (
[all...]
/seL4-l4v-master/HOL4/examples/temporal_deep/src/deep_embeddings/
H A Dtemporal_deep_simplificationsLib.sml98 fun addcontext (context,thms) = reducer_empty_context
99 fun apply {solver,conv, context,stack,relation} tm = conv' tm;
/seL4-l4v-master/graph-refine/graph-to-graph/
H A Delf_correlate.py27 context = {}
28 execfile('%s/loop_counts.py' % dir_name,context)
31 assert 'loops_by_fs' in context
32 lbfs = context['loops_by_fs']
/seL4-l4v-master/isabelle/src/Pure/General/
H A Dfile_watcher.scala110 case (set, event) => set + dir.toPath.resolve(event.context).toFile
/seL4-l4v-master/l4v/isabelle/src/Pure/General/
H A Dfile_watcher.scala110 case (set, event) => set + dir.toPath.resolve(event.context).toFile
/seL4-l4v-master/HOL4/src/num/arith/src/
H A DnumSimps.sml329 (* This function determines whether or not to add something as context to
334 into negative ones in the context of the wider goal, and thus cause
356 val context = map concl thms value
358 val gl' = list_mk_imp(context,gl)
384 val context = map concl thms value
385 val gl = list_mk_imp(context,mk_eq(tm,reduction))
473 that we have accumulated a contradictory context. *)
488 apply = fn args => CACHED_ARITH (get_ctxt (#context args)),

Completed in 285 milliseconds

1234567891011>>