Searched refs:context (Results 51 - 75 of 285) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/examples/elliptic/
H A DellipticScript.sml56 (* The subtype context. *)
59 val context = field_context; value
60 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
673 val context = subtypeTools.add_reduction2 curve_field context; value
674 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
681 val context = subtypeTools.add_reduction2 curve_a1_carrier context; value
682 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
689 val context value
697 val context = subtypeTools.add_reduction2 curve_a3_carrier context; value
705 val context = subtypeTools.add_reduction2 curve_a4_carrier context; value
713 val context = subtypeTools.add_reduction2 curve_a6_carrier context; value
1137 val context = subtypeTools.add_reduction2 curve_zero_carrier context; value
1151 val context = subtypeTools.add_reduction2 curve_neg_carrier context; value
1182 val context = subtypeTools.add_reduction2 curve_double_carrier context; value
1217 val context = subtypeTools.add_reduction2 curve_add_carrier context; value
1229 val context = subtypeTools.add_rewrite2 curve_double_zero context; value
1241 val context = subtypeTools.add_rewrite2 curve_add_lzero context; value
1262 val context = subtypeTools.add_rewrite2 curve_add_lneg context; value
1310 val context = subtypeTools.add_rewrite2 curve_add_rzero context; value
1319 val context = subtypeTools.add_rewrite2 curve_add_rneg context; value
1418 val context = subtypeTools.add_rewrite2 example_prime_def context; value
1421 val context = subtypeTools.add_rewrite2 example_field_def context; value
1429 val context = value
1437 val context = value
1451 val context = subtypeTools.add_reduction2 example_curve context; value
[all...]
H A DsubtypeTools.sml273 datatype context = type
280 fun pp p context =
282 val Context {rewrites,conversions,reductions,judgements,...} = context
299 fun to_string context = PP.pp_to_string (!Globals.linewidth) pp context;
306 fun add_rewrite x context =
309 judgements = j, dproc_cache = m} = context
315 fun add_conversion x context =
318 judgements = j, dproc_cache = m} = context
324 fun add_reduction x context
403 val {context, solver = _, conv = _, relation = _, stack = _} = dproc_context value
[all...]
H A DgroupTools.sig31 (* Subtype context. *)
H A Delliptic_exampleScript.sml40 (* The subtype context. *)
43 val context = elliptic_context; value
44 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
95 val context = subtypeTools.add_reduction2 example1_prime context; value
96 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
102 val context = subtypeTools.add_reduction2 example1_field context; value
103 val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context;
115 val context value
[all...]
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Dtoken_markup.scala25 /* line context */
39 def context =
44 context getOrElse {
46 context getOrElse init(JEdit_Lib.buffer_mode(buffer))
53 val context: Option[Scan.Line_Context],
57 def get_context: Scan.Line_Context = context.getOrElse(Scan.Finished)
59 override def hashCode: Int = (mode, context, structure).hashCode
63 mode == other.mode && context == other.context && structure == other.structure
76 ctxt <- line_context.context
[all...]
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/
H A Dtoken_markup.scala25 /* line context */
39 def context =
44 context getOrElse {
46 context getOrElse init(JEdit_Lib.buffer_mode(buffer))
53 val context: Option[Scan.Line_Context],
57 def get_context: Scan.Line_Context = context.getOrElse(Scan.Finished)
59 override def hashCode: Int = (mode, context, structure).hashCode
63 mode == other.mode && context == other.context && structure == other.structure
76 ctxt <- line_context.context
[all...]
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dx86_dep.cpp202 virtual bool AddTimeProfileCount(SIGNALCONTEXT *context);
597 // Get the PC and SP(stack) from a signal context. This is needed for profiling.
600 bool X86TaskData::AddTimeProfileCount(SIGNALCONTEXT *context) argument
604 if (context != 0)
610 sp = (stackItem *)context->Rsp;
611 pc = (POLYCODEPTR)context->Rip;
614 sp = (stackItem *)context->Esp;
615 pc = (POLYCODEPTR)context->Eip;
621 pc = (byte*)context->uc_mcontext.gregs[REG_EIP];
622 sp = (stackItem*)context
[all...]
/seL4-l4v-master/HOL4/tools/
H A Dhol-mode.sml37 (*no context*)
41 (*user context*)
58 (*goalstack context*)
108 print_header "-" "No context:";
112 print_header "-" ("In context \"" ^ (valOf context_string_opt) ^ "\":");
116 print_header "-" ("In goalstack context:");
120 print_header "-" ("Matching subterms in context \"" ^ (valOf context_string_opt) ^ "\":");
124 print_header "-" ("Matching subterms in goalstack-context:");
/seL4-l4v-master/seL4/include/arch/arm/arch/32/mode/machine/
H A Dregisterset.h35 /* Offsets within the user context, these need to match the order in
62 * saved thread context. The values are determined
204 /* We don't use context comparisons. */
222 /* ARM user-code context: size = 72 bytes
245 void Arch_initBreakpointContext(user_context_t *context);
248 static inline void Arch_initContext(user_context_t *context) argument
250 context->registers[CPSR] = CPSR_USER;
252 Arch_initBreakpointContext(context);
/seL4-l4v-master/seL4/src/arch/x86/machine/
H A Dfpu.c16 void Arch_initFpuContext(user_context_t *context) argument
18 context->fpuState = x86KSnullFpuState;
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DCODETREE_CODEGEN_CONSTANT_FUNCTIONS.sml91 | cgFuns (context as {debugArgs, ...}) (Lambda lambda) =
93 val copied as { closure=resultClosure, ...} = cgLambda(context, lambda, EnvGenLoad LoadRecursive)
104 val repLambda = cgLambda(context, lambda, EnvGenConst(toMachineWord closure, []))
112 | cgFuns (context as { enterConstant, debugArgs, ...}) (Newenv(envBindings, envExp)) =
122 case mapCodetree (cgFuns context) value of
128 NullBinding(mapCodetree (cgFuns context) c) :: processBindings tail
141 {addr=addr, lambda=cgLambda(context, lambda, EnvGenLoad LoadRecursive), use=use}
169 cgLambda(context, lambda, EnvGenConst(closureAsMachineWord, []))
185 setter = mapCodetree (cgFuns context) setter} :: processBindings tail
190 val body = mapCodetree (cgFuns context) envEx
226 val context = value
257 val context = value
[all...]
H A DCODETREE_SIMPLIFIER.sml160 | simpGeneral context (Newenv envArgs) =
161 SOME(specialToGeneral(simpNewenv(envArgs, context, RevList [])))
163 | simpGeneral context (Lambda lambda) =
164 SOME(Lambda(#1(simpLambda(lambda, context, NONE, NONE))))
166 | simpGeneral context (Eval {function, argList, resultType}) =
167 SOME(specialToGeneral(simpFunctionCall(function, argList, resultType, context, RevList[])))
171 | simpGeneral context (Unary{oper, arg1}) =
172 SOME(specialToGeneral(simpUnary(oper, arg1, context, RevList [])))
174 | simpGeneral context (Binary{oper, arg1, arg2}) =
175 SOME(specialToGeneral(simpBinary(oper, arg1, arg2, context, RevLis
[all...]
/seL4-l4v-master/isabelle/src/Pure/Tools/
H A Ddump.scala82 /* context and session */
143 context =>
188 else List(new Session(context, session_logic, log, selected_sessions, record_proofs))
248 val context: Context,
257 if (record_proofs) context.session_options + "record_proofs=2"
258 else context.session_options
260 private def deps = context.deps
261 private def progress = context.progress
265 session_dirs = context.session_dirs,
322 if (context
[all...]
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/
H A Ddump.scala82 /* context and session */
143 context =>
188 else List(new Session(context, session_logic, log, selected_sessions, record_proofs))
248 val context: Context,
257 if (record_proofs) context.session_options + "record_proofs=2"
258 else context.session_options
260 private def deps = context.deps
261 private def progress = context.progress
265 session_dirs = context.session_dirs,
322 if (context
[all...]
/seL4-l4v-master/HOL4/src/1/
H A DConseqConv.sml542 fun CONSEQ_CONV_CONGRUENCE___asm_marker context (sys:conseq_conv_congruence_syscall) dir t =
545 val (n1, thm1) = check_sys_call sys [] context 0 dir b1;
566 fun CONSEQ_CONV_CONGRUENCE___neg context (sys:conseq_conv_congruence_syscall) dir t =
569 val (n1, thm1) = check_sys_call sys [] context 0 (CONSEQ_CONV_DIRECTION_NEGATE dir) b1;
597 fun CONSEQ_CONV_CONGRUENCE___conj context sys dir t =
601 val (n1, thm1_opt) = sys [b2] context 0 dir b1;
603 val (n2, thm2_opt) = sys [a2] context n1 dir b2;
621 fun CONSEQ_CONV_CONGRUENCE___conj_no_context context sys dir t =
625 val (n1, thm1_opt) = sys [] context 0 dir b1;
628 val (n2, thm2_opt) = if abort_cond then (n1, NONE) else sys [] context n
[all...]
H A DConseqConv.sig187 simplifier is available, which allows to use context
192 - using context information
222 3: context -> conversion
224 thm list -> (*context that might be used*)
239 context : thm list
240 A list of theorems from the context it may use.
260 new context information that may be assumed theorems are build
265 the old context theorems that can be used
293 different levels of using context information. If more
294 context i
[all...]
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/
H A DholfootLib.sml145 fun array_bound_DECIDE context t =
147 val _ = cref := SOME context;
149 val thm_opt = SOME (EQT_ELIM (SIMP_CONV arith_ss context t)) handle HOL_ERR _ => NONE;
166 fun holfoot_arith_simp_CONV context t =
167 SIMP_CONV arith_simp_ss context t
170 fun array_bound_DECIDE___HOL context t =
171 (EQT_ELIM (holfoot_arith_simp_CONV context t))
174 fun array_bound_DECIDE___YICES context t =
176 val (_, vali) = YICES_TAC (map concl context, t)
178 val xthm1 = foldl (fn (h, thm) => PROVE_HYP h thm) xthm0 context
[all...]
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DMATCH_COMPILER.sml85 (* To simplify passing the context it is wrapped up in this type.
86 This is a subset of the context used in CODEGEN_PARSETREE. *)
402 fun buildAot (Ident {value=ref ident, expType=ref expType, ... }, tree, patNo, line, context as { typeVarMap, ...} ) =
406 fun doArg a = buildAot(WildCard nullLocation, a, patNo, line, context)
421 patNo, _, context) =
424 val tlist = map (fn el => buildAot(el, wild tree, patNo, location, context)) fields
431 patNo, line, context) =
436 ListPair.mapEq (fn(t, a) => buildAot(t, a, patNo, line, context)) (fields, pl)
446 tree, patNo, _, context as { lex, ...}) =
478 buildAot(TupleTree{fields=tupleList, location=location, expType=ref expType}, tree, patNo, location, context)
[all...]
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DPretty.sml21 (* abstype context =
27 AbsPrettyBlock of int * bool * context list * pretty list
59 type context = address type
62 fun ContextLocation(p: loc): context = cast(0w0, p)
63 and ContextProperty(s1: string, s2: string): context = cast(0w1, s1, s2)
80 fun PrettyBlock(offset: FixedInt.int, consistent: bool, context: context list, items: pretty list): pretty =
81 cast(tagPrettyBlock, offset, consistent, context, items)
93 val (_: int, offset: int, consistent: bool, context: context lis
329 and context = context type
[all...]
/seL4-l4v-master/HOL4/src/simp/src/
H A DCache.sml90 context-aware, and the context as well the goal attempted is
93 If a success is stored with context C, and the context of the
97 goal, with a smaller context, then the cache's verdict can be
99 latest attempt has a larger context, and what's stored is a
103 However, if the context in the latest attempt is only larger
107 bigger context will just result in a slower failure. That is,
205 type context = hypinfo * thm list type
208 | possible_ctxts of context lis
[all...]
/seL4-l4v-master/HOL4/src/quantHeuristics/
H A DquantHeuristicsLibFunRemove.sig19 occourence of x into an context of the form "f x". *)
/seL4-l4v-master/HOL4/polyml/basis/
H A DPrettyPrinter.sml40 PrettyBlock(indent, consistent, context, entries) -
59 fun prettyMarkup (beginContext: context list -> unit, endContext: context list -> unit)
94 fun layOut(p as PrettyBlock (blockOffset, consistent, context, entries), indent, spaceLeft) =
101 beginContext context;
104 endContext context;
170 val () = beginContext context;
172 val () = endContext context
197 (* Basic pretty printer without mark-up of context. *)
/seL4-l4v-master/HOL4/examples/lambda/typing/
H A DcontextlistsScript.sml13 (* the free variables of a context *)
18 (* A context is valid if the strings
41 (* context membership "respects" permutation *)
78 (* sub-context relation, overloaded to use SUBSET *)
/seL4-l4v-master/seL4/include/arch/riscv/arch/machine/
H A Dregisterset.h119 static inline void Arch_initContext(user_context_t *context) argument
122 context->registers[SSTATUS] = SSTATUS_SPIE;
/seL4-l4v-master/isabelle/src/Pure/Isar/
H A Douter_syntax.scala112 context: Completion.Language_Context): Option[Completion.Result] =
114 completion.complete(history, unicode, explicit, start, text, caret, context)
140 /* language context */
142 def set_language_context(context: Completion.Language_Context): Outer_Syntax =
143 new Outer_Syntax(keywords, rev_abbrevs, context, has_tokens)

Completed in 361 milliseconds

1234567891011>>