/seL4-l4v-master/isabelle/src/Pure/Thy/ |
H A D | export.scala | 123 @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = 125 case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest) 126 case '*' :: rest => make("[^:/]*" :: result, depth, rest) 127 case '?' :: rest => make("[^:/]" :: result, depth, rest) 128 case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest) 129 case '{' :: rest => make("(" :: result, depth + 1, rest) 130 case ',' :: rest if depth > 0 => make("|" :: result, depth, rest) 131 case '}' :: rest if depth > 0 => make(")" :: result, depth [all...] |
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/ |
H A D | export.scala | 123 @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = 125 case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest) 126 case '*' :: rest => make("[^:/]*" :: result, depth, rest) 127 case '?' :: rest => make("[^:/]" :: result, depth, rest) 128 case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest) 129 case '{' :: rest => make("(" :: result, depth + 1, rest) 130 case ',' :: rest if depth > 0 => make("|" :: result, depth, rest) 131 case '}' :: rest if depth > 0 => make(")" :: result, depth [all...] |
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | sptreepp.sml | 44 fun sptree_printer (tyg,tmg) backend printer ppfns (pgr,lgr,rgr) depth tm = 67 depth = decdepth depth, binderp = false} v
|
/seL4-l4v-master/HOL4/src/proofman/ |
H A D | goalStack.sig | 23 val depth : gstk -> int value
|
/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | comment.scala | 68 case Scan.Cartouche_Comment(depth) => 69 cartouche_depth(depth) ^^ { case (c, d) => (c, cartouche_context(d)) }
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | comment.scala | 68 case Scan.Cartouche_Comment(depth) => 69 cartouche_depth(depth) ^^ { case (c, d) => (c, cartouche_context(d)) }
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | type_pp.sml | 125 fun pr_ty ty grav depth = let 144 if depth = 0 then add_string "..." 216 pr_list (fn arg => pr_ty arg grav (depth - 1)) 226 pr_ty (hd realArgs) Sfx (depth - 1) >> 228 pr_ty (hd (tl realArgs)) Top (depth - 1) >> 263 pr_ty arg1 (Lfx (prec, printthis)) (depth - 1) >> 267 pr_ty arg2 (Rfx (prec, printthis)) (depth -1) 294 (fn depth => fn ty => baseprinter ty Top depth)
|
H A D | term_pp.sml | 625 pgrav lgrav rgrav depth apps = 631 depth 635 fun sysprint { gravs = (pg,lg,rg), binderp, depth} tm = 637 pg lg rg depth 643 depth tm 655 pgrav lgrav rgrav depth apps = 723 type_pp.pp_type_with_depth TyG backend (decdepth depth) ty 768 | RE TM => (pr_term (hd args) Top Top Top (decdepth depth) >> 772 pr_term (hd args) cprec lprec cprec (decdepth depth) >> 775 pr_term (hd args) cprec cprec rprec (decdepth depth) >> [all...] |
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | ImplicitGraph.sig | 22 folded into the 'result at depth 0.
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | sharedata.cpp | 70 1. From the root, recursively process all objects and calculate a "depth" 71 for each object. Mutable data and code segments have depth 0 and 73 precision values) have depth 1. Other cells have depths of 1 or greater, 74 the depth being the maximum recursion depth until a byte segment or an 75 object with depth 0 is reached. Cycles of immutable data don't arise 77 To avoid infinite recursion cycles are broken by setting the depth of an 78 object to zero before processing it. The depth of each object is stored 81 2. Vectors are created containing objects of the same depth, from 1 to the 82 maximum depth foun 245 AddToVector(POLYUNSIGNED depth, POLYUNSIGNED length, PolyObject *pt) argument 873 POLYUNSIGNED depth = 0; local [all...] |
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | Scrollbar.sml | 236 fun printFlags(put, beg, brk, nd) depth _ x = 241 fun plist [] depth = () 243 | plist [h] depth = put h 244 | plist (h::t) depth = 247 plist t (depth - 1) 252 if depth <= 0 then put "..." else plist stringFlags depth;
|
H A D | Static.sml | 177 fun printFlags(put, beg, brk, nd) depth _ x = 182 fun plist [] depth = () 184 | plist [h] depth = put h 185 | plist (h::t) depth = 188 plist t (depth - 1) 193 if depth <= 0 then put "..." else plist stringFlags depth;
|
H A D | Button.sml | 201 fun printFlags(put, beg, brk, nd) depth _ x = 206 fun plist [] depth = () 208 | plist [h] depth = put h 209 | plist (h::t) depth = 212 plist t (depth - 1) 217 if depth <= 0 then put "..." else plist stringFlags depth;
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Word8Array.sml | 105 fun pretty(depth: FixedInt.int) _ (x: vector) = 121 (if depth <= 0 then [PrettyString "...]"] 122 else #1 (foldri put_elem ([PrettyString "]"], depth - FixedInt.fromInt last) x) ) 245 fun pretty(depth: FixedInt.int) _ (x: array) = 261 (if depth <= 0 then [PrettyString "...]"] 262 else #1 (foldri put_elem ([PrettyString "]"], depth - FixedInt.fromInt last) x) ) 309 fun pretty(depth: FixedInt.int) _ (x: Word8VectorSlice.slice) = 325 (if depth <= 0 then [PrettyString "...]"] 326 else #1 (foldri put_elem ([PrettyString "]"], depth - FixedInt.fromInt last) x) ) 412 fun pretty(depth [all...] |
H A D | Array2.sml | 233 fun 'a pretty(depth: FixedInt.int) 246 fun putRowElements (row, col, tail, depth) = 249 else putRowElements(row, col-1, put_elem(sub(x, row, col), col, tail, depth), depth+1) 270 (if depth <= 0 then [PrettyString "...]"] 271 else putRow(nrows-1, depth - FixedInt.fromInt nrows + 1, [PrettyString "]"])
|
/seL4-l4v-master/seL4/src/arch/arm/object/ |
H A D | smmu.c | 26 word_t index, depth, sid; local 62 depth = getSyscallArg(2, buffer); 78 lu_ret = lookupTargetSlot(cnodeCap, index, depth); 189 word_t index, depth, cb; local 213 depth = getSyscallArg(2, buffer); 229 lu_ret = lookupTargetSlot(cnodeCap, index, depth);
|
/seL4-l4v-master/HOL4/examples/STE/ |
H A D | Conversion.sml | 59 fun add_next_upto_depth start depth term = 60 if (start = (depth-1)) then 64 ^(add_next_upto_depth (start+1) depth term)``; 92 val _ = print ("Calculating the depth of the formula...");
|
/seL4-l4v-master/HOL4/src/bool/ |
H A D | boolpp.sml | 25 fun condprinter (tyg, tmg) backend printer ppfns (pgr,lgr,rgr) depth tm = let 48 printer { gravs = gravs, depth = decdepth depth, binderp = false } t 88 fun letprinter (tyg, tmg) backend printer ppfns (pgr,lgr,rgr) depth tm = 95 printer { gravs = gravs, depth = decdepth depth, binderp = false } t 98 Simple t => printer {gravs = (Top,Top,Top), depth = decdepth depth,
|
/seL4-l4v-master/seL4/tools/hardware/ |
H A D | device.py | 24 self.depth = 0 35 self.depth = parent.depth + 1
|
/seL4-l4v-master/seL4/src/arch/x86/object/ |
H A D | interrupt.c | 72 word_t index, depth; local 101 depth = getSyscallArg(1, buffer); 121 lu_ret = lookupTargetSlot(cnodeCap, index, depth);
|
H A D | ioport.c | 115 word_t index, depth; local 136 depth = getSyscallArg(3, buffer); 153 lu_ret = lookupTargetSlot(cnodeCap, index, depth);
|
/seL4-l4v-master/seL4/src/object/ |
H A D | interrupt.c | 28 word_t index, depth, irq_w; local 42 depth = getSyscallArg(2, buffer); 57 lu_ret = lookupTargetSlot(cnodeCap, index, depth);
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | cacheTools.sml | 402 fun cache_add depth rvnm2ix env (nf,mf) mfo ce rsc rvty ithml (githms as [_,_,T_I,F_I,_,_,_,_,_,_,_,_,_,_,_,_,_,_]) 411 val cekey = if irv then mk_comb(rvtm, (fromMLstring((fromHOLstring(rand mf))^(int_to_string depth)))) else mf 412 (*mu_RV (type_of state) (fromMLstring((fromHOLstring(rand mf))^(int_to_string depth))) else mf*) 422 (* reverse scoping for RV's is more complicated, so it is quicker to just cache on name+depth (a la de Bruijn) to tell them apart *) 475 (*val _ = print_rsc rsc "RV cache_add depth"*) 650 fun mk_cache_aux ee rvnm2ix env (nf,mf) mfo ce rscope depth rvty githms state seth msp guid tysimps p_ty 660 val (pt,(ce1,rsc,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce rscope rvty [] 669 val (pt,(ce1,rsc,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce rscope rvty [] 677 | "RV" =>let val (pt,(ce1,rsc,ithm,abthm)) = cache_add depth rvnm2ix env (nf,mf) mfo ce rscope rvty [] 686 | "AP" =>let val (pt,(ce1,rsc,ithm,abthm)) = cache_add depth rvnm2i [all...] |
/seL4-l4v-master/HOL4/src/coalgebras/ |
H A D | lbtreeScript.sml | 565 of the minimum depth at which x occurs in a tree, and the minimum 566 index within the list of a tree containing x to that depth. 571 the depth number doesn't change, but the index goes down because 578 moves to the end of the list, but at a reduced depth. 586 (* depth x t n means that x occurs in tree t at depth n *) 588 (!x t1 t2. depth x (Nd x t1 t2) 0) /\ 589 (!m x a t1 t2. depth x t1 m ==> depth x (Nd a t1 t2) (SUC m)) /\ 590 (!m x a t1 t2. depth [all...] |
/seL4-l4v-master/isabelle/src/Pure/Isar/ |
H A D | line_structure.scala | 19 depth: Int = 0,
|