Searched refs:seq (Results 26 - 50 of 63) sorted by relevance

123

/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/
H A Dregexp_parserScript.sml50 pegf sym f = seq sym (empty NONE) (��l1 l2. OPTION_MAP f l1)
60 igLeft s1 s2 = seq s1 s2 (��l1 l2. l2)
65 igRight s1 s2 = seq s1 s2 (��l1 l2. l1)
131 seq (pnt Atom) (try (tok ((=) #"*") (K (SOME (Chset charset_empty)))))
138 seq (pnt Star) (try (pnt Concat))
145 seq (pnt Concat) (rpt (igtok ((=) #"|") *> pnt Concat) OrM)
/seL4-l4v-10.1.1/HOL4/src/emit/
H A Dextended_emitScript.sml299 MLSTRUCT "type 'a llist = 'a seq.seq" ::
300 MLSTRUCT "fun llcases n c seq = seq.fcases seq (n,c)" ::
301 MLSTRUCT "fun LLCONS h t = seq.cons h (seq.delay t)"::
302 MLSTRUCT "fun LCONS h t = seq.cons h t"::
303 MLSTRUCT "val LNIL = seq.empty"::
305 MLSTRUCT "fun LUNFOLD f x = seq
[all...]
/seL4-l4v-10.1.1/HOL4/src/q/
H A DQ.sml106 [] => seq.result []
107 | x::xs => seq.bind (mf x)
109 seq.bind (seq_mmap mf xs)
110 (fn xs' => seq.result (x'::xs')))
119 case seq.cases tl_s of
126 case seq.cases (seq.mapPartial f tl_s) of
387 case PQ seq.cases patseq of
444 case PQ seq.cases patseq of
467 {ERR = ERR, pats = seq
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DASN1.sml118 fun decode (acc, seq) =
119 case getNext seq of
120 SOME(code, seq') =>
127 then SOME(tag', seq')
128 else decode(tag', seq')
/seL4-l4v-10.1.1/HOL4/developers/
H A Dpoly-prehol.sml38 fun pp_seq _ _ (_: 'a seq.seq) = PolyML.PrettyString "<seq>"
/seL4-l4v-10.1.1/HOL4/src/portableML/
H A DPEGParse.sml9 | seq of ('tok,'nt,'value)pegsym * ('tok,'nt,'value)pegsym * ('value -> 'value -> 'value)
52 | seq(e1,e2,f) => pe e1 inp stk (ksym(e2,appf2(f,k),returnTo(inp,stk,fk))) fk
H A DPEGParse.sig9 | seq of ('tok,'nt,'value)pegsym * ('tok,'nt,'value)pegsym *
/seL4-l4v-10.1.1/isabelle/src/Pure/Admin/
H A Disabelle_cronjob.scala530 PAR(remote_builds.map(_.filter(_.active)).map(seq =>
533 (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/
H A Disabelle_cronjob.scala530 PAR(remote_builds.map(_.filter(_.active)).map(seq =>
533 (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
/seL4-l4v-10.1.1/graph-refine/
H A Dtrace_refute.py228 def adj (seq):
229 (x_stack, y_stack) = seq[stack_idx]
230 xsub = dict ([(v, xv) for (v, (xv, _)) in azip (inps, seq)])
231 ysub = dict ([(v, yv) for (v, (_, yv)) in azip (inps, seq)])
236 return seq[:stack_idx] + seq[stack_idx + 1:] + stk_eqs
/seL4-l4v-10.1.1/HOL4/examples/computability/register/
H A DregScript.sml146 `haltsAt (prog:num |-> instr) (seq:num -> config) =
147 if (?n. haltedConfig prog (seq n))
148 then SOME (LEAST n. haltedConfig prog (seq n))
153 ``!prog pc args seq m.
154 isExecution prog pc args seq /\
155 haltedConfig prog (seq m) ==>
156 !q. m <= q ==> haltedConfig prog (seq q)``,
161 Q.SPEC_THEN `seq (m + k)` FULL_STRUCT_CASES_TAC
182 let seq = execOf prog 1 (0::args)
183 in case haltsAt prog seq o
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/
H A Dprog_x64Script.sml235 !y s t1 seq.
236 p (x64_2set' y t1) /\ X64_ICACHE t1 s /\ rel_sequence X64_NEXT_REL seq s /\
238 ?k t2. q (x64_2set' y t2) /\ X64_ICACHE t2 (seq k) /\
239 (x64_2set'' y t1 = x64_2set'' y t2) \/ X64_STACK_FULL (seq k)``,
246 \\ Q.PAT_X_ASSUM `!y.bbb` (MP_TAC o Q.SPECL [`y`,`state`,`s`,`seq`])
256 `t1`,`seq`,`y`]) \\ FULL_SIMP_TAC std_ss []
264 !y s t1 seq.
265 p (x64_2set' y t1) /\ X64_ICACHE t1 s /\ rel_sequence X64_NEXT_REL seq s /\
267 ?k t2. q (x64_2set' y t2) /\ X64_ICACHE t2 (seq (k + 1)) /\
268 (x64_2set'' y t1 = x64_2set'' y t2) \/ X64_STACK_FULL (seq
[all...]
H A Dprog_x64_extraScript.sml308 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`y`,`s`,`t1`,`seq`])
315 \\ `?r e s m i. seq k = (r,e,s,m,i)` by METIS_TAC [PAIR]
341 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`y`,`s`,`t1`,`seq`])
343 \\ Cases_on `X64_STACK_FULL (seq (k+1))` THEN1 METIS_TAC []
344 \\ Cases_on `X64_STACK_FULL (seq k)` THEN1 METIS_TAC []
350 \\ `?r e s m i. seq (k+1) = (r,e,s,m,i)` by METIS_TAC [PAIR]
/seL4-l4v-10.1.1/HOL4/src/1/
H A Dmp_then.sml101 case seq.cases ps of
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/
H A Dprog_ppcScript.sml174 !y s seq. p (ppc2set' y s) /\ rel_sequence PPC_NEXT_REL seq s ==>
175 ?k. q (ppc2set' y (seq k)) /\ (ppc2set'' y s = ppc2set'' y (seq k))``,
/seL4-l4v-10.1.1/HOL4/examples/ARM/experimental/
H A Dlpc_progScript.sml250 !y s seq. p (lpc2set' y s) /\ rel_sequence LPC_NEXT seq s ==>
251 ?k. q (lpc2set' y (seq k)) /\ (lpc2set'' y s = lpc2set'' y (seq k))``,
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/
H A DpegexecScript.sml68 | EV (seq e1 e2 f) i r k fk =>
141 ([`e` |-> `seq e1 e2 sf`], []),
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dprog_x86Script.sml205 !y s t1 seq.
206 p (x86_2set' y t1) /\ X86_ICACHE t1 s /\ rel_sequence X86_NEXT_REL seq s ==>
207 ?k t2. q (x86_2set' y t2) /\ X86_ICACHE t2 (seq k) /\ (x86_2set'' y t1 = x86_2set'' y t2)``,
396 \\ `X86_NEXT_REL (seq 0) (seq (SUC 0))` by
397 (`?x. X86_NEXT_REL (seq 0) x` by
400 \\ Q.EXISTS_TAC `seq 0` \\ ASM_SIMP_TAC std_ss []
404 \\ `seq 0 = s` by FULL_SIMP_TAC std_ss [rel_sequence_def]
/seL4-l4v-10.1.1/HOL4/tools/
H A Dbuildcline.sml142 {help = "build this directory sequence", long = ["seq"], short = "",
H A Dbuildutils.sml243 | ["--seq"] => (warn "Trailing --seq option in last build info ignored";
245 | "--seq"::fname::t => let
357 write_options ("--"^knlspec::"--seq"::seqspec::joption::bgoption)
862 fun add kspec seq s =
863 Binaryset.addList(s,read_buildsequence {kernelname = kspec} seq)
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DTermParse.sml258 seq.map #2 (M Pretype.Env.empty)
351 seq.map #2 ((pt_S >- Preterm.typecheckS) Pretype.Env.empty)
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/
H A Dpydot.py677 def set_sequence(self, seq):
679 self.obj_dict['sequence'] = seq
1255 seq = self.obj_dict['current_child_sequence']
1259 return seq
/seL4-l4v-10.1.1/HOL4/src/integer/
H A DCooperShell.sml713 fun rule f th = (seq.result (f th, ())) handle HOL_ERR _ => seq.empty
716 seq.result(EQF_INTRO (NOT_INTRO (DISCH tm th)),())
717 else seq.empty
729 case seq.cases (spec 5 (ASSUME tm)) of
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A DSALScript.sml98 (Reduce (l1, S1, l2) (e,v) /\ (* seq *)
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/lambek/
H A DCutFreeScript.sml111 (head (Der seq _ _) = seq) /\
112 (head (Unf seq) = seq)`;

Completed in 199 milliseconds

123