Searched refs:seq (Results 1 - 25 of 63) sorted by relevance

123

/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DSequence.sig18 type 'a seq
19 val seq_append : 'a seq * 'a seq -> 'a seq
20 val seq_chop : int * 'a seq -> 'a list * 'a seq
21 val seq_cons : 'a * 'a seq -> 'a seq
22 val seq_filter : ('a -> bool) -> 'a seq -> 'a seq
[all...]
H A DSequence.sml10 datatype 'a seq = Seq of unit -> ('a * 'a seq)option;
34 fun seq_chop (n:int, s: 'a seq): 'a list * 'a seq =
42 fun list_of_seq (s: 'a seq) : 'a list = case seq_pull(s) of
54 fun seq_print (prelem: int -> 'a -> unit) count (s: 'a seq) : unit =
96 fun seq_iterate (f: 'a * 'b seq -> 'b seq) (s: 'a seq, bstr: 'b seq)
[all...]
/seL4-l4v-10.1.1/HOL4/src/portableML/
H A Dseq.sig1 (* FILE: seq.sig
13 signature seq = sig signature
14 type 'a seq
16 val cases : 'a seq -> ('a * 'a seq) option
17 val fcases : 'a seq -> ('b * (('a * 'a seq) -> 'b)) -> 'b
19 val append : 'a seq -> 'a seq -> 'a seq
[all...]
H A Dseq.sml5 structure seq :> seq = struct structure
6 datatype 'a seq =
8 LCONS of ('a * 'a seq) |
9 LDELAYREF of 'a seq ref |
10 LDELAYED of (unit -> 'a seq)
28 | null (LDELAYED _) = raise Fail "seq - shouldn't happen"
33 | cases (LDELAYED f) = raise Fail "seq - shouldn't happen"
38 | fcases (LDELAYED f) _ = raise Fail "seq - shouldn't happen"
43 | append (LDELAYED f) x = raise Fail "seq
[all...]
/seL4-l4v-10.1.1/HOL4/src/portableML/monads/
H A Dseqmonad.sml2 type ('a,'b) seqmonad = 'a -> ('a * 'b) seq.seq
3 fun fail env = seq.empty
4 fun return x env = seq.result (env, x)
5 fun ok env = seq.result (env, ())
9 seq.delay (fn () => let val res0 = m1 env
11 seq.flatten (seq.map (fn (e, v) => f v e) res0)
15 seq.append (seq
[all...]
H A Dseqmonad.sig4 type ('a, 'b) seqmonad = 'a -> ('a * 'b) seq.seq
/seL4-l4v-10.1.1/HOL4/examples/miller/prob/
H A Dprob_uniformTools.sml44 fun UNIFORM t n seq
45 = UNIFORM_CONV (list_mk_comb (``uniform``, [t, n, seq]));
48 | UNIFORML m t n seq
49 = let val th = UNIFORM t n seq
50 val seq' = (snd o dest_comb o snd o dest_eq o concl) th
51 in th::UNIFORML (m - 1) t n seq'
62 fun UNIFORM t n seq
63 = EVAL (list_mk_comb (``uniform``, [t, n, seq]));
66 | UNIFORML m t n seq
67 = let val th = UNIFORM t n seq
[all...]
H A Dprob_trichotomyTools.sml30 fun chain f seq 0 = []
31 | chain f seq n =
33 val th = PROB_TRICHOTOMY_CONV (mk_comb (f, seq))
34 val (_, seq) = (dest_pair o snd o dest_eq o concl) th
36 th :: chain f seq (n - 1)
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/
H A DSequents.tex47 is given the name {\tt seq}.
48 A {\tt seq} is created either by the empty space, a {\tt seqobj} or a
49 {\tt seqobj} followed by a {\tt seq}, with a comma between them. A
53 Isabelle type \verb|[seq, seq] => prop|.
71 \verb|Seq0'| with type \verb|[o,seq']=>seq'|, and translating a
89 internally} as functions of type \verb|seq'=>seq'|.
122 two_seqi = [seq'
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/
H A DSequents.tex47 is given the name {\tt seq}.
48 A {\tt seq} is created either by the empty space, a {\tt seqobj} or a
49 {\tt seqobj} followed by a {\tt seq}, with a comma between them. A
53 Isabelle type \verb|[seq, seq] => prop|.
71 \verb|Seq0'| with type \verb|[o,seq']=>seq'|, and translating a
89 internally} as functions of type \verb|seq'=>seq'|.
122 two_seqi = [seq'
[all...]
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/
H A Dbddtree.h45 int *seq; /* Sequence of first...last in the current order */ member in struct:s_BddTree
H A Dtree.c60 t->seq[bddvar2level[n]-bddvar2level[low]] = n;
73 t->seq = NULL;
86 if (t->seq != NULL)
87 free(t->seq);
105 t->seq = NEW(int,last-first+1);
125 tnew->seq = NEW(int,last-first+1);
168 tnew->seq = NEW(int,last-first+1);
H A Dreorder.c573 static BddTree *reorder_sift_seq(BddTree *t, BddTree **seq, int num) argument
589 reorder_filehandler(stdout, seq[n]->id);
591 printf("%d", seq[n]->id);
595 reorder_sift_bestpos(seq[n], num/2);
632 BddTree *this, **seq; local
641 if ((seq=NEW(BddTree*,num)) == NULL)
664 seq[n] = p[n].block;
667 t = reorder_sift_seq(t, seq, num);
669 free(seq);
706 BddTree **seq; local
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A Dtemporal_stateScript.sml39 (qspecl_then [`state`, `seq`, `r * r'`] imp_res_tac)
71 !state y seq.
72 p (SELECT_STATE m y (seq 0)) /\ rel_sequence next seq state ==>
73 q (SELECT_STATE m y (seq 1)) /\
74 (FRAME_STATE m y (seq 0) = FRAME_STATE m y (seq 1))`,
98 \\ `NEXT_REL (=) next (seq 0) (seq (SUC 0))`
100 `?x. NEXT_REL (=) next (seq
[all...]
H A DstateScript.sml57 seq_relation (NEXT_REL (=) next) seq s
61 seq 0 = s,
62 seq 1 = THE (next s),
63 seq 2 = THE (next (THE (next s))), ...
65 If ``next (seq n) = NONE`` for some "n" then this final state is repeated
220 !y s t1 seq.
221 p (SELECT_STATE m y t1) /\ r t1 s /\ rel_sequence next seq s ==>
222 ?k t2. q (SELECT_STATE m y t2) /\ r t2 (seq k) /\
243 !y s seq.
244 p (SELECT_STATE m y s) /\ rel_sequence next seq
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/
H A DtemporalScript.sml12 !state seq r.
13 rel_sequence next seq state ==>
16 exp f seq`
19 val seq = ``seq: num -> 'b`` value
21 val NOW_def = Define `NOW p ^f seq = f p (seq 0)`
22 val NEXT_def = Define `NEXT p ^f seq = p f (\n. seq (n + 1:num))`
23 val EVENTUALLY_def = Define `EVENTUALLY p ^f seq
[all...]
H A DprogScript.sml17 rel_sequence R seq state =
18 (seq 0 = state) /\
19 !n. if (?x. R (seq n) x) then R (seq n) (seq (SUC n)) else (seq (SUC n) = seq n)`;
27 !seq. rel_sequence next seq state ==>
28 ?i. SEP_REFINE (q * r) less to_set (seq
[all...]
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DTermParse.sig24 val termS : grammar -> tygrammar -> term quotation -> term seq.seq
32 term quotation -> term seq.seq
34 term quotation -> term seq.seq
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/
H A DpegSampleScript.sml24 ``seq (tok ((=) LParen) (K (XN 0)))
25 (seq (nt (INL "expr") I) (tok ((=) RParen) (K (XN 0))) K)
38 seq (rpt (seq (nt (INL "term") I)
46 seq (rpt (seq (nt (INL "factor") I)
H A DpegML.sml24 | seq of ('tok,'value) pegsym * ('tok,'value)pegsym * ('value * 'value -> 'value)
71 | seq(e1,e2,f) =>
108 "E" => seq(rpt (seq(nt("F", I), tok("+", XN 0), #1), PTL),
111 | "F" => seq(rpt (seq(nt("T", I), tok("*", XN 0), #1), PTL),
114 | "T" => choice(seq(seq(tok("(", XN 0), nt("E", I), #2), tok(")", XN 0),
H A DpegScript.sml19 | seq of pegsym => pegsym => ('c -> 'c -> 'c)
45 (���e1 e2 s f. peg_eval G (s, e1) NONE ��� peg_eval G (s, seq e1 e2 f) NONE) ���
48 peg_eval G (s0, seq e1 e2 f) NONE) ���
52 peg_eval G (s0, seq e1 e2 f) (SOME(s2, f c1 c2))) ���
135 (* seq rules *)
138 pegfail G (seq e1 e2 f)) ���
141 peggt0 G (seq e1 e2 f)) ���
142 (���e1 e2 f. peg0 G e1 ��� peg0 G e2 ��� peg0 G (seq e1 e2 f)) ���
215 wfpeg G (seq e1 e2 f)) ���
226 (subexprs (seq e
[all...]
H A DsimpleSexpPEGScript.sml35 val pegf_def = Define`pegf sym f = seq sym (empty arb_sexp) (��l1 l2. f l1)`;
79 seq (grabWS (pnt sxnt_sexp0))
80 (seq (rpt (grabWS (pnt sxnt_sexp0))
94 seq (pnt sxnt_digit)
102 seq (tok valid_first_symchar (��(c,l). SX_SYM [c]))
142 [`seq e1 e2 f`, `choice e1 e2 f`, `tok P f`,
161 [`tok P f`, `choice e1 e2 f`, `seq e1 e2 f`,
/seL4-l4v-10.1.1/isabelle/src/Pure/General/
H A Dscan.scala433 private class Restricted_Seq(seq: IndexedSeq[Char], start: Int, end: Int)
437 if (0 <= i && i < length) seq(start + i)
440 def length: Int = end - start // avoid expensive seq.length
443 if (0 <= i && i <= j && j <= length) new Restricted_Seq(seq, start + i, start + j)
449 for (offset <- start until end) buf.append(seq(offset))
459 val seq = new PagedSeq(
472 val restricted_seq = new Restricted_Seq(seq, 0, stream_length)
477 def first: Char = if (seq.isDefinedAt(offset)) seq(offset) else '\u001a'
478 def rest: Paged_Reader = if (seq
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Dscan.scala433 private class Restricted_Seq(seq: IndexedSeq[Char], start: Int, end: Int)
437 if (0 <= i && i < length) seq(start + i)
440 def length: Int = end - start // avoid expensive seq.length
443 if (0 <= i && i <= j && j <= length) new Restricted_Seq(seq, start + i, start + j)
449 for (offset <- start until end) buf.append(seq(offset))
459 val seq = new PagedSeq(
472 val restricted_seq = new Restricted_Seq(seq, 0, stream_length)
477 def first: Char = if (seq.isDefinedAt(offset)) seq(offset) else '\u001a'
478 def rest: Paged_Reader = if (seq
[all...]
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibSolver.sml174 fun seq f [] = "" function
175 | seq f (h :: t) = foldl (fn (n, s) => s ^ "," ^ f n) (f h) t;
177 fun combine_names csolvers = "[" ^ seq (name o snd) csolvers ^ "]";
211 fun seq f [] = "" function
212 | seq f (h :: t) = foldl (fn (n, s) => s ^ "--" ^ f n) (f h) t;
215 "[" ^ seq (subnode_info verbose) subnodes ^ "]--u=" ^ U.info units ^ "--";
232 val seq = (Option.valOf solns) () value
238 case seq of S.NIL => (NONE, NONE) | S.CONS (a, r) => (a, SOME r)

Completed in 145 milliseconds

123