/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
H A D | regexp_parserScript.sml | 50 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 D | extended_emitScript.sml | 299 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 D | Q.sml | 106 [] => 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 D | ASN1.sml | 118 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 D | poly-prehol.sml | 38 fun pp_seq _ _ (_: 'a seq.seq) = PolyML.PrettyString "<seq>"
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | PEGParse.sml | 9 | 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 D | PEGParse.sig | 9 | seq of ('tok,'nt,'value)pegsym * ('tok,'nt,'value)pegsym *
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Admin/ |
H A D | isabelle_cronjob.scala | 530 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 D | isabelle_cronjob.scala | 530 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 D | trace_refute.py | 228 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 D | regScript.sml | 146 `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 D | prog_x64Script.sml | 235 !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 D | prog_x64_extraScript.sml | 308 \\ 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 D | mp_then.sml | 101 case seq.cases ps of
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | prog_ppcScript.sml | 174 !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 D | lpc_progScript.sml | 250 !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 D | pegexecScript.sml | 68 | 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 D | prog_x86Script.sml | 205 !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 D | buildcline.sml | 142 {help = "build this directory sequence", long = ["seq"], short = "",
|
H A D | buildutils.sml | 243 | ["--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 D | TermParse.sml | 258 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 D | pydot.py | 677 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 D | CooperShell.sml | 713 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 D | SALScript.sml | 98 (Reduce (l1, S1, l2) (e,v) /\ (* seq *)
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/lambek/ |
H A D | CutFreeScript.sml | 111 (head (Der seq _ _) = seq) /\ 112 (head (Unf seq) = seq)`;
|