Searched refs:gs (Results 1 - 25 of 36) sorted by relevance

12

/seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/
H A Dtypes.h30 seL4_Word tls_base, fs, gs; member in struct:seL4_UserContext_
/seL4-l4v-10.1.1/HOL4/examples/computability/
H A DrecursivefnsScript.sml20 recCn (f:num list -> num option) gs l =
21 let results = MAP (��g : num list -> num option. g l) gs
41 (���f gs m. recfn f (LENGTH gs) ��� EVERY (��g. recfn g m) gs ���
42 recfn (recCn f gs) m) ���
55 `SOME o Cn f gs = recCn (SOME o f) (MAP (��g. SOME o g) gs)`
137 Induct_on ���recfn��� >> rw[] >> rename [���gs ��� []���] >>
138 Cases_on ���gs��� >> f
[all...]
H A DprimrecfnsScript.sml54 Cn (f:num list -> num) (gs:(num list -> num) list) (l:num list) =
55 f (MAP (��g. g l) gs)
87 (���f gs m. primrec f (LENGTH gs) ��� EVERY (��g. primrec g m) gs ���
88 primrec (Cn f gs) m) ���
161 Induct_on `gs` THEN SRW_TAC [][],
186 Induct_on `gs` THEN SRW_TAC [][],
728 ``EVERY (��g. primrec g k ��� ���J. ���l. (LENGTH l = k) ==> g l < H J (SUM l)) gs
730 ���J. ���l. (LENGTH l = k) ==> SUM (MAP (��g. g l) gs) <
[all...]
/seL4-l4v-10.1.1/HOL4/src/meson/src/
H A DjrhTactics.sml32 | rotate_p1 ((g::gs), just) =
33 let val newgs = gs @ [g]
38 | rotate_n1 (gs, just) =
39 let val (newg, newgs) = (last gs, butlast gs)
75 let val (gs, jf) = T (map ASSUME asl, g) value
76 val newgs = map (fn (asl, g) => (map concl asl, g)) gs
H A DmesonLib.sml517 (fn (gs,(newinsts,newoffset,newsize)) =>
520 val g' = Subgoal(g,gs,apprule,offset,locin)
522 if (globin = insts) andalso null(gs) then
533 | g::gs =>
555 exp_goals depth (gs,stup)
556 (cacheconts (fn (gs',ftup) => cont(g'::gs',ftup)))))
722 fun meson_to_hol insts cpos_cache cvdb (Subgoal(g,gs,(n,th),offset,locin)) =
727 val ths = map (meson_to_hol newins cpos_cache cvdb) gs
/seL4-l4v-10.1.1/HOL4/src/num/termination/
H A Dselftest.sml37 val gs_def = DefineSchema`(gs 0 y = x + y) /\ (gs x y = x)`;
/seL4-l4v-10.1.1/seL4/src/arch/x86/32/
H A Dmachine_asm.S24 movw %ax, %gs
54 movw %ax, %gs
H A Dtraps.S25 pushl %gs; \
426 popl %gs
515 pushl %gs # save GS
/seL4-l4v-10.1.1/HOL4/examples/computability/lambda/
H A DprtermScript.sml1506 LAM "f" (LAM "gs" (LAM "x" (
1507 VAR "gs"
1533 ``���i f gs x.
1534 MEM i gs ��� (Phi i x = NONE) ���
1535 (bnf_of (crecCn @@ f @@ cvlist (MAP church gs) @@ church x) = NONE)``,
1538 ���i f gs x. MEM i gs ��� (Phi i x = NONE) ���
1539 (bnf_of (LL gs @@ NN f @@ CC x @@ cnil) = NONE)
1542 ���i f gs k x. MEM i gs ��� (Ph
[all...]
/seL4-l4v-10.1.1/seL4/src/arch/x86/64/
H A Dmachine_asm.S89 movw %ax, %gs
H A Dtraps.S60 /* If using multicore our gs base is set to point to a nodeInfo_t structure.
66 #define LOAD_USER_CONTEXT movq %gs:16, %rsp
68 #define LOAD_KERNEL_STACK movq %gs:0, %rsp
69 #define LOAD_IRQ_STACK(x) movq %gs:8, %x
/seL4-l4v-10.1.1/HOL4/src/proofman/
H A DgoalStack.sml174 val gs = return(GSTK{prop=prop,final=final, value
176 in expand_msg dpth gs ; gs end
192 fun expand tac gs = expandf (Tactical.VALID tac) gs;
193 fun expand_list ltac gs = expand_listf (Tactical.VALID_LT ltac) gs;
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/
H A DhelperLib.sml533 fun AUTO_EXISTS_TAC (gs,goal) = EXISTS_TAC (fst (dest_exists goal)) (gs,goal)
1128 fun aux (hs,gs) = let
1129 val (v,n) = dest_exists gs
1138 THEN SIMP_TAC (std_ss++star_ss) []) (hs,gs) end
1143 fun prepare_tac (hs,gs) = let
1144 val (x,y) = pred_setSyntax.dest_in gs
1151 val thi = auto_prove "SEP_READ_TAC" (mk_imp(mk_conj(tm,gs),gs),REPEAT STRIP_TAC)
1152 in MATCH_MP_TAC thi (hs,gs) en
[all...]
/seL4-l4v-10.1.1/HOL4/examples/zipper/
H A DzipperScript.sml245 ``zpure (o) <*> fs <*> gs <*> xs = fs <*> (gs <*> xs)``,
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibSolver.sml69 | contr th gs = map (C CONTR th) gs;
73 fn gs => S.CONS (SOME (contr th gs), K S.NIL));
H A DmlibMeson.sml452 | mp env th (g :: gs) (th1 :: p) =
453 mp env (RESOLVE (formula_subst env g) (INST env th1) th) gs p
456 fun modus_ponens th gs (state as {env, ...}) =
457 update_proof (mp env (INST env th) (rev gs)) state;
H A DmetisTools.sml400 fun order_cl (cl,gs,_,_,_) [] = (cl,gs)
/seL4-l4v-10.1.1/HOL4/src/patricia/
H A DsptreeSyntax.sml201 fun sys gs d = syspr {gravs = gs, depth = d, binderp = false}
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/concurrent/
H A DTask_Queue.sml215 fun group_tasks (Queue {groups, ...}) gs =
218 gs Tasks.empty
/seL4-l4v-10.1.1/HOL4/examples/logic/
H A DfoltypesScript.sml334 ``GFVl [] = {} ��� GFVl (g::gs) = GFV g ��� GFVl gs``,
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/
H A DcompilerLib.sml274 val gs = (map strip_forall o list_dest dest_conj o fst o dest_imp o concl) imp value
275 val xs = zip (rev fnames) gs
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A DexportLib.sml70 val gs = tm |> rator |> rand |> dest_graph value
73 in (xs,ys,gs,ep) end
H A Dderive_specsLib.sml119 in mk_TRACE_SPLIT (map (fn (th,gs,nexts) =>
120 TRACE_STEP (p, gs, th, mk_TRACE_SPLIT (map
121 (fn n => aux (n:int) (p::seen) (gs:term)) nexts))) ys) end)
/seL4-l4v-10.1.1/HOL4/src/holyhammer/legacy/
H A Dhh_tac.ml171 let fOL_TAC2 ((ps,gl) as gs) =
174 rULE_ASSUM_TAC (cONV_RULE (fOL_CONV mindata))) gs;;
/seL4-l4v-10.1.1/HOL4/src/parse/
H A Dtype_grammar.sml365 fun merge_acc acc (gs as (g1, g2)) =
366 case gs of

Completed in 233 milliseconds

12