/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | gr_t.sml | 19 "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 D | wlogLib.sml | 132 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 D | match_goal.sig | 31 - 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 D | PrettyImpl.sml | 4 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 D | simplifier_trace.scala | 152 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 D | debugger.scala | 15 /* 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 D | simplifier_trace.scala | 152 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 D | debugger.scala | 15 /* 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 D | LEXSIG.sml | 45 { 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 D | debug.h | 26 * 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 D | intSimps.sml | 153 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 D | quantHeuristicsLib.sig | 76 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 D | simplifier_trace_dockable.scala | 42 val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results) 45 context.questions.values.toList match {
|
H A D | debugger_dockable.scala | 48 /* 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 D | simplifier_trace_dockable.scala | 42 val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results) 45 context.questions.values.toList match {
|
H A D | debugger_dockable.scala | 48 /* 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 D | boolContext.sml | 135 (* The context *)
|
/seL4-l4v-master/HOL4/examples/separationLogic/src/ |
H A D | vars_as_resourceBaseFunctor.sml | 256 (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 D | CODETREE_OPTIMISER.sml | 819 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 D | CongruenceScript.sml | 37 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 D | temporal_deep_simplificationsLib.sml | 98 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 D | elf_correlate.py | 27 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 D | file_watcher.scala | 110 case (set, event) => set + dir.toPath.resolve(event.context).toFile
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | file_watcher.scala | 110 case (set, event) => set + dir.toPath.resolve(event.context).toFile
|
/seL4-l4v-master/HOL4/src/num/arith/src/ |
H A D | numSimps.sml | 329 (* 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)),
|