/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | ellipticScript.sml | 56 (* 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 D | subtypeTools.sml | 273 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 D | groupTools.sig | 31 (* Subtype context. *)
|
H A D | elliptic_exampleScript.sml | 40 (* 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 D | token_markup.scala | 25 /* 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 D | token_markup.scala | 25 /* 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 D | x86_dep.cpp | 202 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 D | hol-mode.sml | 37 (*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 D | registerset.h | 35 /* 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 D | fpu.c | 16 void Arch_initFpuContext(user_context_t *context) argument 18 context->fpuState = x86KSnullFpuState;
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_CODEGEN_CONSTANT_FUNCTIONS.sml | 91 | 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 D | CODETREE_SIMPLIFIER.sml | 160 | 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 D | dump.scala | 82 /* 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 D | dump.scala | 82 /* 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 D | ConseqConv.sml | 542 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 D | ConseqConv.sig | 187 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 D | holfootLib.sml | 145 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 D | MATCH_COMPILER.sml | 85 (* 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 D | Pretty.sml | 21 (* 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 D | Cache.sml | 90 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 D | quantHeuristicsLibFunRemove.sig | 19 occourence of x into an context of the form "f x". *)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | PrettyPrinter.sml | 40 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 D | contextlistsScript.sml | 13 (* 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 D | registerset.h | 119 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 D | outer_syntax.scala | 112 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)
|