Searched refs:tag (Results 51 - 75 of 142) sorted by relevance

123456

/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DTheoryPP.sml118 (Tag.isEmpty (Thm.tag th) orelse Tag.isDisk (Thm.tag th))
229 val (tg, asl, w) = (Thm.tag th, Thm.hyp th, Thm.concl th)
377 fun pp_tag tag =
379 val dep = Tag.dep_of tag
380 val ocl = fst (Tag.dest_tag tag)
387 val (tag, asl, w) = (Thm.tag th, Thm.hyp th, Thm.concl th) value
393 pp_tag tag >> add_newline >>
/seL4-l4v-10.1.1/seL4/manual/parts/
H A Dipc.tex35 Every IPC message also has a tag (structure \texttt{seL4\_MessageInfo\_t}). The
36 tag consists of four fields: the label, message length, number of capabilities
57 \ipcparam{seL4\_MessageInfo\_t}{}{tag}{Message tag}
95 The situation is similar for the tag field.
98 may wish to copy the message tag from its CPU register to this field, although
147 to send is specified in the \texttt{extraCaps} field of the message tag.
171 tag. The capability itself is not transferred, so the receive slot may be used
174 If a receiver gets a message whose tag has an \texttt{extraCaps} of 2 and a
/seL4-l4v-10.1.1/HOL4/polyml/PolyPerf/
H A DPolyPerf.cpp224 unsigned tag = *ptr++; local
226 switch (tag)
293 unsigned char tag = *ptr++; local
295 switch (tag)
318 unsigned char tag = *ptr++; local
320 switch (tag)
367 // Anything else is an unknown tag; skip
/seL4-l4v-10.1.1/HOL4/polyml/modules/IntInfAsInt/
H A DROOT.sml51 fun dolookup (look, tag, kind) s =
53 SOME v => Universal.tagInject tag (s, v)
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/examples/calculator/
H A Dparser.y24 nodeData(const nodeData &d) { tag=d.tag; name=sdup(d.name); val=d.val; }
25 nodeData(int t, char *n, bdd v) { tag=t; name=n; val=v; }
27 int tag;
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DBackendIntermediateCode.sml194 | BICTagTest of { test: backendIC, tag: word, maxTag: word }
266 val tupleTag: universal list list tag = tag()
269 | splitProps tag (hd::tl) =
270 if Universal.tagIs tag hd
272 else let val (p, l) = splitProps tag tl in (p, hd :: l) end
591 | BICTagTest { test, tag, maxTag } =>
594 PrettyString (concat["TAGTEST(", Word.toString tag, ", ", Word.toString maxTag, ","]),
H A DCODETREE_STATIC_LINK_AND_CASES.sml46 (* Property tag to indicate which arguments to a function are functions
48 val closureFreeArgsTag: int list Universal.tag = Universal.tag()
453 | insert(TagTest{test, tag, maxTag}) = BICTagTest{test=insert test, tag=tag, maxTag=maxTag}
488 { tag: word, test: codetree, caseType: caseType } option;
514 then SOME{tag=toShort c1, test=arg2, caseType = CaseWord}
519 then SOME{tag=toShort c2, test=arg1, caseType = CaseWord}
526 | findCase(BICTagTest { test, tag, maxTa
[all...]
H A DBaseCodeTree.sml101 | TagTest of { test: codetree, tag: word, maxTag: word }
181 val inlineCodeTag: envSpecial tag = tag()
471 | TagTest { test, tag, maxTag } =>
474 PrettyString (concat["TAGTEST(", Word.toString tag, ", ", Word.toString maxTag, ","]),
674 | mapt (TagTest{test, tag, maxTag}) = TagTest{test = mapCodetree f test, tag = tag, maxTag = maxTag }
H A DBaseCodeTreeSig.sml111 | TagTest of { test: codetree, tag: word, maxTag: word }
183 val tupleTag: Universal.universal list list Universal.tag
184 val inlineCodeTag: envSpecial Universal.tag
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/
H A DPRETTYSIG.sml58 val printOutputTag : (pretty -> unit) Universal.tag
60 and compilerOutputTag: (pretty->unit) Universal.tag
H A DDATATYPEREPSIG.sml35 val EnumForm: { tag: word, maxTag: word } -> representations;
H A DCOPIER.sml36 type 'a tag = 'a Universal.tag
38 val univEnter: univTable * 'a tag * string * 'a -> unit;
39 val univLookup: univTable * 'a tag * string -> 'a option;
57 open Universal; (* for tag record selectors *)
H A DPretty.sml259 val printOutputTag : (pretty -> unit) tag = tag()
261 and compilerOutputTag: (pretty->unit) tag = tag()
266 fun getTag (t: (pretty -> unit) tag) (tagList: universal list) : pretty -> unit =
H A DExportTree.sml107 val rootTreeTag: navigation Universal.tag = Universal.tag()
H A DEXPORTTREESIG.sml59 val rootTreeTag: navigation Universal.tag
/seL4-l4v-10.1.1/HOL4/tools/unicode-grep/
H A Dugrep.sml78 fun line_error qp fname linenum tag line =
81 (print (fname^":"^Int.toString linenum^": " ^ tag ^ ": " ^ line);
154 fun foldthis ((_, (f, tag)), (b, tags)) =
158 (b andalso b', if not b' then inc tag tags else tags)
/seL4-l4v-10.1.1/graph-refine/
H A Dsearch.py76 tag = p.node_tags[n][0]
77 trace ('Finding split limit: %d (%s)' % (n, tag))
95 epc = rep.get_pc (('Err', restrs3), tag = tag)
113 trace ('No split limit found for %d (%s).' % (n, tag))
146 err_pc_hyps = [rep_graph.pc_false_hyp ((('Err', no_loop_restrs), tag))
147 for tag in p.pairing.tags]
174 err_pc_hyps = [rep_graph.pc_false_hyp ((('Err', no_loop_restrs), tag))
175 for tag in p.pairing.tags]
963 for (tag,
[all...]
H A Dsolver.py988 def next_hyp (self, (hyp, tag), hyp_dict):
991 hyp_dict[name] = tag
1000 raw_hyps = [(hyp2, tag) for (hyp, tag) in hyps
1151 unsat_core.extend ([tag for (_, tag) in hyps])
1870 for (i, (ass, tag)) in enumerate (asserts):
1900 return set ([tag for (_, tag) in asserts])
1904 hyps = [(smt_expr (hyp, env, self), tag) fo
[all...]
H A Dgraph-refine.py43 for (tag, fname) in pair.funs.iteritems ():
45 printout ('Skipping %s, underspecified %s' % (pair, tag))
/seL4-l4v-10.1.1/HOL4/help/src-sml/
H A DParseDoc.sml328 fun section (tag, ss) =
329 case tag of
343 if null args andalso not (mem tag empty_ok) then
344 raise ParseError ("Empty "^tag^" field")
345 else FIELD (tag, args)
H A DDoc2Html.sml114 | markout_section (FIELD (tag, ss))
116 out (if tag = "DESCRIBE" then "DESCRIPTION" else tag);
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DExnPrinter.sml86 val printLimit: word ref list Universal.tag = Universal.tag()
H A DFinalPolyML.sml683 val useFileTag: string option Universal.tag = Universal.tag()
749 type 'a tag = 'a Universal.tag;
2155 val structureTag: (string * PolyML.NameSpace.Structures.structureVal) Universal.tag = Universal.tag()
2156 val functorTag: (string * PolyML.NameSpace.Functors.functorVal) Universal.tag = Universal.tag()
2157 val signatureTag: (string * PolyML.NameSpace.Signatures.signatureVal) Universal.tag = Universal.tag()
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A DMakefile.in184 libpolyml_la_LINK = $(LIBTOOL) $(AM_V_lt) --tag=CXX $(AM_LIBTOOLFLAGS) \
215 LTCXXCOMPILE = $(LIBTOOL) $(AM_V_lt) --tag=CXX $(AM_LIBTOOLFLAGS) \
224 CXXLINK = $(LIBTOOL) $(AM_V_lt) --tag=CXX $(AM_LIBTOOLFLAGS) \
233 LTCOMPILE = $(LIBTOOL) $(AM_V_lt) --tag=CC $(AM_LIBTOOLFLAGS) \
242 LINK = $(LIBTOOL) $(AM_V_lt) --tag=CC $(AM_LIBTOOLFLAGS) \
/seL4-l4v-10.1.1/HOL4/src/1/
H A DPmatch.sml199 fun build (prefix,tag,plist) =
202 in (prefix,tag, c'::plist') end
208 fun build (prefix,tag,plist) =
210 in (prefix,tag,list_mk_comb(c,args)::plist') end
218 fun v_to_pats (v::prefix,tag, pats) = (prefix, tag, v::pats)
350 let val (tag,tm) = dest_pattern rhs value
351 in ([(prefix,tag,[])], tm)
742 fun func (_,(tag,i),[pat]) = tag (pa
[all...]

Completed in 137 milliseconds

123456