/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Sequence.sig | 18 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 D | Sequence.sml | 10 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 D | seq.sig | 1 (* 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 D | seq.sml | 5 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 D | seqmonad.sml | 2 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 D | seqmonad.sig | 4 type ('a, 'b) seqmonad = 'a -> ('a * 'b) seq.seq
|
/seL4-l4v-10.1.1/HOL4/examples/miller/prob/ |
H A D | prob_uniformTools.sml | 44 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 D | prob_trichotomyTools.sml | 30 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 D | Sequents.tex | 47 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 D | Sequents.tex | 47 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 D | bddtree.h | 45 int *seq; /* Sequence of first...last in the current order */ member in struct:s_BddTree
|
H A D | tree.c | 60 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 D | reorder.c | 573 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 D | temporal_stateScript.sml | 39 (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 D | stateScript.sml | 57 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 D | temporalScript.sml | 12 !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 D | progScript.sml | 17 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 D | TermParse.sig | 24 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 D | pegSampleScript.sml | 24 ``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 D | pegML.sml | 24 | 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 D | pegScript.sml | 19 | 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 D | simpleSexpPEGScript.sml | 35 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 D | scan.scala | 433 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 D | scan.scala | 433 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 D | mlibSolver.sml | 174 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)
|