Searched refs:token (Results 1 - 25 of 114) sorted by relevance

12345

/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/
H A Dyacc-grm-sig.sml3 type ('a,'b) token
5 val BOGUS_VALUE: 'a * 'a -> (svalue,'a) token
6 val UNKNOWN: (string) * 'a * 'a -> (svalue,'a) token
7 val VALUE: 'a * 'a -> (svalue,'a) token
8 val VERBOSE: 'a * 'a -> (svalue,'a) token
9 val TYVAR: (string) * 'a * 'a -> (svalue,'a) token
10 val TERM: 'a * 'a -> (svalue,'a) token
11 val START: 'a * 'a -> (svalue,'a) token
12 val SUBST: 'a * 'a -> (svalue,'a) token
13 val RPAREN: 'a * 'a -> (svalue,'a) token
[all...]
/seL4-l4v-10.1.1/l4v/tools/c-parser/tools/mlyacc/src/
H A Dyacc-grm-sig.sml6 type ('a,'b) token
8 val BOGUS_VALUE: 'a * 'a -> (svalue,'a) token
9 val UNKNOWN: (string) * 'a * 'a -> (svalue,'a) token
10 val VALUE: 'a * 'a -> (svalue,'a) token
11 val VERBOSE: 'a * 'a -> (svalue,'a) token
12 val TYVAR: (string) * 'a * 'a -> (svalue,'a) token
13 val TERM: 'a * 'a -> (svalue,'a) token
14 val START: 'a * 'a -> (svalue,'a) token
15 val SUBST: 'a * 'a -> (svalue,'a) token
16 val RPAREN: 'a * 'a -> (svalue,'a) token
[all...]
/seL4-l4v-10.1.1/l4v/misc/scripts/
H A Dcpp17 llvm-gcc -Wno-invalid-pp-token -E -x c $@
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/examples/calculator/
H A Dparser.y42 void actInit(token *nodes, token *cache);
44 void actAddInput(token *id);
45 void actAssign(token *id, token *expr);
46 void actOpr2(token *res, token *left, token *right, int opr);
47 void actNot(token *res, token *righ
[all...]
H A Dparser.h16 struct token /* BISON token data */ struct
24 #define YYSTYPE token
/seL4-l4v-10.1.1/HOL4/src/1/
H A DDiskFiles.lex6 type ('a,'b) token = ('a,'b)Tokens.token
7 type lexresult = (svalue,pos) token
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DTheoryLexer.sml49 let val (token, cont) = wait_endquote [#"\""] m in value
50 lex_helper (token :: acc) cont
60 let val (token, cont) = wait_char (not o is_alphanum) [] charl in value
61 lex_helper (token :: acc) cont
/seL4-l4v-10.1.1/isabelle/src/Pure/Isar/
H A Dkeyword.scala184 def is_command(token: Token, check_kind: String => Boolean): Boolean =
185 token.is_command &&
186 (kinds.get(token.source) match { case Some(k) => check_kind(k) case None => false })
188 def is_before_command(token: Token): Boolean =
189 token.is_keyword && kinds.get(token.source) == Some(BEFORE_COMMAND)
191 def is_quasi_command(token: Token): Boolean =
192 token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND)
194 def is_indent_command(token
[all...]
H A Dparse.scala45 def token(s: String, pred: Elem => Boolean): Parser[Elem] =
52 val token = in.first
53 if (pred(token)) Success(token, proper(in.rest))
54 else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in)
60 token(s, pred) ^^ (_.content)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Isar/
H A Dkeyword.scala184 def is_command(token: Token, check_kind: String => Boolean): Boolean =
185 token.is_command &&
186 (kinds.get(token.source) match { case Some(k) => check_kind(k) case None => false })
188 def is_before_command(token: Token): Boolean =
189 token.is_keyword && kinds.get(token.source) == Some(BEFORE_COMMAND)
191 def is_quasi_command(token: Token): Boolean =
192 token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND)
194 def is_indent_command(token
[all...]
H A Dparse.scala45 def token(s: String, pred: Elem => Boolean): Parser[Elem] =
52 val token = in.first
53 if (pred(token)) Success(token, proper(in.rest))
54 else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in)
60 token(s, pred) ^^ (_.content)
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/mlyacclib/
H A DMLY_base-sig.sml75 (* TOKEN: signature revealing the internal structure of a token. This signature
80 The representation of token was very carefully chosen here to allow the
86 type 'a token which functions to construct tokens would create. A
87 constructor function for a integer token might be
89 INT: int * 'a * 'a -> 'a token.
96 INT: int * 'a * 'a -> (svalue,'a) token
106 datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
107 val sameToken : ('a,'b) token * ('a,'b) token -> bool
123 lexer : ('_b,'_c) Token.token Strea
[all...]
H A DMLY_parser1.sml41 datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
68 lexer : ('_b,'_c) token Stream.stream,
98 ('_b,'_c) token * ('_b,'_c) token Stream.stream,
113 val (token,restLexer) = next value
114 in (topvalue,Stream.cons(token,lexer))
/seL4-l4v-10.1.1/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/
H A Dbase.sig51 (* TOKEN: signature revealing the internal structure of a token. This signature
56 The representation of token was very carefully chosen here to allow the
62 type 'a token which functions to construct tokens would create. A
63 constructor function for a integer token might be
65 INT: int * 'a * 'a -> 'a token.
72 INT: int * 'a * 'a -> (svalue,'a) token
82 datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
83 val sameToken : ('a,'b) token * ('a,'b) token -> bool
99 lexer : ('_b,'_c) Token.token Strea
[all...]
H A Dparser1.sml19 datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
46 lexer : ('_b,'_c) token Stream.stream,
76 ('_b,'_c) token * ('_b,'_c) token Stream.stream,
91 val (token,restLexer) = next value
92 in (topvalue,Stream.cons(token,lexer))
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/
H A Dbase.sig51 (* TOKEN: signature revealing the internal structure of a token. This signature
56 The representation of token was very carefully chosen here to allow the
62 type 'a token which functions to construct tokens would create. A
63 constructor function for a integer token might be
65 INT: int * 'a * 'a -> 'a token.
72 INT: int * 'a * 'a -> (svalue,'a) token
82 datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
83 val sameToken : ('a,'b) token * ('a,'b) token -> bool
99 lexer : ('_b,'_c) Token.token Strea
[all...]
H A Dparser1.sml19 datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
46 lexer : ('_b,'_c) token Stream.stream,
76 ('_b,'_c) token * ('_b,'_c) token Stream.stream,
91 val (token,restLexer) = next value
92 in (topvalue,Stream.cons(token,lexer))
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DSmtLib_Parser.sml28 token. 4. Parsing a function symbol in some cases requires that
31 indexed identifiers, i.e., "(_ token m n ...)". 6. Parsing must
42 results from applying the (function corresponding to the) token
54 dictionary entry for a token (or every parsing function in its
58 indexed identifiers (which are instead keyed by the first token
60 catch-all entry. The token itself is passed verbatim.
76 fun t_with_args dict (token : string) (nums : Arbnum.num list)
78 Lib.tryfind (fn f => f token nums args) (Redblackmap.find (dict, token)
82 Lib.tryfind (fn f => f token num
94 val token = get_token () value
113 val token = get_token () value
137 val token = get_token () value
178 val token = get_token () value
221 val token = get_token () value
265 val token = get_token () value
281 val token = get_token () value
306 val token = get_token () value
[all...]
H A DSmtLib_Theories.sml92 fun is_numeral token =
94 val cs = String.explode token
101 (* A <decimal> is a token of the form <numeral>.0*<numeral>. *)
102 fun real_of_decimal token =
104 val (left, right) = Lib.pair_of_list (String.fields (Lib.equal #".") token)
161 ("_", zero_zero (fn token =>
162 if String.isPrefix "#b" token then
164 val binary = String.extract (token, 2, NONE)
170 else if String.isPrefix "#x" token then
172 val hex = String.extract (token,
[all...]
H A DZ3_ProofParser.sml64 parentheses; then the parser would find a ")" token once it has
125 ("_", SmtLib_Theories.zero_zero (fn token =>
126 if String.isPrefix "bv" token then
128 val args = String.extract (token, 2, NONE)
143 ("_", SmtLib_Theories.zero_one (fn token =>
144 if String.isPrefix "extract[" token then
146 val args = String.extract (token, 8, NONE)
162 ("_", SmtLib_Theories.one_one (fn token => fn n =>
163 if String.isPrefix "extract" token then
165 val m = Library.parse_arbnum (String.extract (token,
[all...]
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/
H A Dcheck_keywords.scala21 position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
22 private val other = token("token", _ => true)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/
H A Dcheck_keywords.scala21 position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
22 private val other = token("token", _ => true)
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/
H A Djedit_bibtex.scala57 /** token markup **/
59 /* token style */
61 private def token_style(context: String, token: Bibtex.Token): Byte =
62 token.kind match {
70 if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
73 case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
74 case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
99 /* token marker */
136 for ((style, token) <- styled_tokens) {
137 val length = token
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/
H A Djedit_bibtex.scala57 /** token markup **/
59 /* token style */
61 private def token_style(context: String, token: Bibtex.Token): Byte =
62 token.kind match {
70 if (Bibtex.is_month(token.source)) JEditToken.LITERAL3
73 case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3
74 case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4
99 /* token marker */
136 for ((style, token) <- styled_tokens) {
137 val length = token
[all...]
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttLexer.sml101 let val (token, cont) = wait_endquote [#"\""] m in value
102 lex_helper (token :: acc) cont
112 let val (token, cont) = wait_char (not o is_sml_id) [] charl in value
113 lex_helper (token :: acc) cont
117 let val (token, cont) = wait_char (not o is_sml_symbol) [] charl in value
118 lex_helper (token :: acc) cont

Completed in 253 milliseconds

12345