Searched refs:rows (Results 1 - 25 of 34) sorted by relevance

12

/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/
H A Dimatrix.c53 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 Dimatrix.h42 char **rows; member in struct:_imatrix
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/
H A DpatternMatchesScript.sml77 (* 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 DpatternMatchesLib.sig77 (* 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 DpatternMatchesLib.sml227 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 DpatternMatchesSyntax.sml420 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 DpatternMatchesSyntax.sig80 (* [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 DparsePMATCH.sml274 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 DPmatch.sml107 * 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 DPmatchHeuristics.sig8 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 DPmatchHeuristics.sml43 (* assumption: rowL noteq [], and all rows have same length *)
H A DTypeBase.sml317 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 DInduction.sml72 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 Dstats.py78 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 DUseful.sml671 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 Dsession_build.scala51 rows = 24
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DUseful.sml671 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 Dsession_build.scala51 rows = 24
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/
H A Dsigs.sml390 (* 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 Dgui.scala89 if (height > 0 && split_lines(txt).length > height) text.rows = height
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/GUI/
H A Dgui.scala89 if (height > 0 && split_lines(txt).length > height) text.rows = height
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DArray2.sml25 (* 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 DRoundOpScript.sml5 (* - shifting rows *)
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/word8/
H A DRoundOpScript.sml5 (* - shifting rows *)
/seL4-l4v-10.1.1/HOL4/examples/Crypto/AES/
H A DRoundOpScript.sml5 (* - shifting rows *)

Completed in 364 milliseconds

12