/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | imatrix.c | 53 if ((mtx->rows=NEW(char*,size)) == NULL) 61 if ((mtx->rows[n]=NEW(char,size/8+1)) == NULL) 64 free(mtx->rows[m]); 69 memset(mtx->rows[n], 0, size/8+1); 83 free(mtx->rows[n]); 84 free(mtx->rows); 118 mtx->rows[a][b/8] |= 1<<(b%8); 124 mtx->rows[a][b/8] &= ~(1<<(b%8)); 130 return mtx->rows[a][b/8] & (1<<(b%8));
|
H A D | imatrix.h | 42 char **rows; member in struct:_imatrix
|
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
H A D | patternMatchesScript.sml | 77 (* rows of a case-expression consist of a 93 (* We defined semantics of single rows. Let's extend 157 ``!v v' rows rows' r r'. ((v = v') /\ (r v' = r' v') /\ 158 (PMATCH v' rows = PMATCH v' rows')) ==> 159 (PMATCH v (r :: rows) = PMATCH v' (r' :: rows'))``, 248 (* Changing rows and removing redundant ones *) 253 each other by modifying or dropping rows ar [all...] |
H A D | patternMatchesLib.sig | 77 (* PMATCH_CLEANUP_CONV removes rows that can't match, 78 removes all rows after the first matching row and 102 (* Remove easily detectable redundant rows *) 106 (* Remove easily detectable subsumed rows *) 111 normalise, partially evaluate rows and columns and 112 try to remove redundant and subsumed rows. *) 200 introducing wildcards reordering rows ... *) 231 (* List of all rows that are not well-formed. 235 (* List of rows that have guards *) 238 (* List of rows tha [all...] |
H A D | patternMatchesLib.sml | 227 PMATCH v rows = PMATCH v' rows' 232 It tries to get the appends in rows and rows' in 235 Then it tries to simplify appends in rows' 236 resulting in rows''. 240 l = PMATCH v' rows''. 342 The top-most split is split into the input + a list of rows. 347 (* try to collapse rows by introducing a catchall at end*) 484 val rows value 1619 val rows = List.rev rows value 3797 val rows = List.map mk_row rs value [all...] |
H A D | patternMatchesSyntax.sml | 420 fun mk_PMATCH v rows = let 426 val ty_subst = match_type rows_ty (type_of rows) 429 val t2 = mk_comb (t1, rows) 453 val (col_no, rows') = foldl split_pat (0, []) ps 471 val rows'' = foldl final_process [] rows' 474 fun get_cols acc vs rows = case vs of 477 val col = map hd rows 478 val rows' = map tl rows [all...] |
H A D | patternMatchesSyntax.sig | 80 (* [dest_PMATCH ``PMATCH v rows``] returns (``v``, ``rows``). *) 87 (* [dest_PMATCH_COLS ``PMATCH v rows``] tries to extract the columns 98 (* applies a conversion to all rows of a pmatch *)
|
H A D | parsePMATCH.sml | 274 val rows = map (mk_row recursor) (strip_casesplit arg2) value 276 list_make_comb l1 [pmatch_pt, arg1, mk_ptlist rows]
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Pmatch.sml | 107 * Goes through a list of rows and picks out the ones beginning with a * 112 fun mk_groupl literal rows = 121 itlist func rows ([],[]) 125 * Goes through a list of rows and picks out the ones beginning with a * 129 fun mk_group c rows = 138 itlist func rows ([],[]) 143 * Partition the rows among literals. Not efficient. * 146 fun partitionl _ _ (_,_,_,[]) = raise ERR"partitionl" "no rows" 148 (constructors, colty, res_ty, rows as (((prefix,_),_)::_)) = 149 let fun part {constrs = [], rows, 364 val rows = map (fn ((prefix, pL), rhs) => ((prefix, bring_to_front_list col_index pL), rhs)) rows0 value 735 val rows = zip (map (fn x => ([]:term list,[x])) pats) (map GIVEN (enumerate R)) value [all...] |
H A D | PmatchHeuristics.sig | 8 type pmatch_heuristic = {skip_rows : bool, (* skip splitting for redundant rows? *) 10 (* given a list of rows of patterns, which column to split on? *)
|
H A D | PmatchHeuristics.sml | 43 (* assumption: rowL noteq [], and all rows have same length *)
|
H A D | TypeBase.sml | 317 This is broken because it can re-order rows in the case expression in a semantically significant way
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Induction.sml | 72 fun ipartition gv (constructors,rows) = 74 fun part {constrs = [], rows = [], A} = rev A 75 | part {constrs = [], rows = _::_, A} = pfail"extra cases in defn" 76 | part {constrs = _::_, rows = [], A} = pfail"cases missing in defn" 77 | part {constrs = c::crst, rows, A} = 88 val (in_group, not_in_group) = itlist func rows ([],[]) 93 rows = not_in_group, 99 part {constrs=constructors, rows=rows, A=[]} 103 (* Partition rows wher 199 val rows = map (fn (pL, rhs) => (bring_to_front_list col_index pL, rhs)) rows0 value 306 val rows:row list = map (fn x => ([x], (th0,[]))) pats value [all...] |
/seL4-l4v-10.1.1/graph-refine/ |
H A D | stats.py | 78 rows = {} 81 rows.setdefault (wsz, []) 82 rows[wsz].append (has_nec) 84 for i in sorted (rows): 86 tr = len ([v for v in rows[i] if v]) 87 ln = len (rows[i])
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Useful.sml | 671 fun alignTab aligns rows = 673 [] => List.map (K "") rows 674 | [{leftAlign = true, padChar = #" "}] => List.map hd rows 677 val col = List.map hd rows 678 and cols = alignTab aligns (List.map tl rows) 683 fun alignTable aligns rows = 684 if List.null rows then [] else alignTab aligns rows;
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | session_build.scala | 51 rows = 24
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Useful.sml | 671 fun alignTab aligns rows = 673 [] => List.map (K "") rows 674 | [{leftAlign = true, padChar = #" "}] => List.map hd rows 677 val col = List.map hd rows 678 and cols = alignTab aligns (List.map tl rows) 683 fun alignTable aligns rows = 684 if List.null rows then [] else alignTab aligns rows;
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | session_build.scala | 51 rows = 24
|
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
H A D | sigs.sml | 390 (* SHRINK_LR_TABLE: finds unique action entry rows in the action table 395 (* Takes an action table represented as a list of action rows. 396 It returns the number of unique rows left in the action table, 398 row, and a list of unique rows *)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/GUI/ |
H A D | gui.scala | 89 if (height > 0 && split_lines(txt).length > height) text.rows = height
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/GUI/ |
H A D | gui.scala | 89 if (height > 0 && split_lines(txt).length > height) text.rows = height
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Array2.sml | 25 (* This is implemented as a vector of rows i.e. Vector.sub(v, 0)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/tupled/ |
H A D | RoundOpScript.sml | 5 (* - shifting rows *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/word8/ |
H A D | RoundOpScript.sml | 5 (* - shifting rows *)
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/AES/ |
H A D | RoundOpScript.sml | 5 (* - shifting rows *)
|