/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
H A D | yacc-grm-sig.sml | 3 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 D | yacc-grm-sig.sml | 6 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 D | cpp | 17 llvm-gcc -Wno-invalid-pp-token -E -x c $@
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/examples/calculator/ |
H A D | parser.y | 42 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 D | parser.h | 16 struct token /* BISON token data */ struct 24 #define YYSTYPE token
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | DiskFiles.lex | 6 type ('a,'b) token = ('a,'b)Tokens.token 7 type lexresult = (svalue,pos) token
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | TheoryLexer.sml | 49 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 D | keyword.scala | 184 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 D | parse.scala | 45 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 D | keyword.scala | 184 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 D | parse.scala | 45 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 D | MLY_base-sig.sml | 75 (* 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 D | MLY_parser1.sml | 41 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 D | base.sig | 51 (* 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 D | parser1.sml | 19 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 D | base.sig | 51 (* 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 D | parser1.sml | 19 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 D | SmtLib_Parser.sml | 28 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 D | SmtLib_Theories.sml | 92 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 D | Z3_ProofParser.sml | 64 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 D | check_keywords.scala | 21 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 D | check_keywords.scala | 21 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 D | jedit_bibtex.scala | 57 /** 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 D | jedit_bibtex.scala | 57 /** 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 D | tttLexer.sml | 101 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
|