Searched refs:syntax (Results 1 - 25 of 283) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/graph-refine/example/
H A Dtarget.py12 import syntax namespace
17 syntax.parse_and_install_all (f, None)
21 syntax.check_funs (functions)
/seL4-l4v-10.1.1/graph-refine/loop-example/synth/
H A Dtarget.py12 import syntax namespace
17 syntax.parse_and_install_all (f, None)
21 syntax.check_funs (functions)
/seL4-l4v-10.1.1/graph-refine/
H A Dinst_logic.py9 import syntax namespace
17 from syntax import mk_var
51 bin_globs = [('mem', syntax.builtinTs['Mem'])]
52 asm_globs = [('Mem', syntax.builtinTs['Mem'])]
55 """wrapper for making a syntax.Function with standard args/rets."""
56 return syntax.Function (nm,
57 [(nm, syntax.word32T) for nm in word_args] + ex_args + globs,
58 [(nm, syntax.word32T) for nm in word_rets] + ex_rets + globs)
88 ident_v = ("inst_ident", syntax.builtinTs['Token'])
99 (syntax
[all...]
H A Dc_rodata.py1 import syntax namespace
25 hyp = rep.to_smt_expr (syntax.mk_implies (pc,
26 syntax.mk_not (eq_rodata)), (n, vc))
H A Dstack_logic.py9 import syntax namespace
22 from syntax import mk_var, word32T, builtinTs, mk_eq, mk_less_eq
94 syntax.boolT)
95 (mk_nimp, mk_not) = (syntax.mk_n_implies, syntax.mk_not)
107 bool_hyps = bool_hyps + [syntax.mk_not (cond_exp)])
116 cache = None, typ = syntax.word32T):
266 sp = mk_var ('r13', syntax.word32T)
291 sp = syntax.rename_expr (mk_var ('r13', syntax
[all...]
H A Dlogic.py9 import syntax namespace
10 from syntax import word32T, word8T, boolT, builtinTs, Expr, Node
11 from syntax import true_term, false_term, mk_num
12 from syntax import foldr1
17 mk_if, mk_meta_typ, mk_pvalid) = syntax.mks
19 from syntax import structs
37 ghost_assertion_type = syntax.Type ('WordArray', 64, 32)
111 return [syntax.mk_var (v, typ) for v in vs]
288 return syntax.do_subst (var_exp, substor)
295 return syntax
[all...]
H A Dobjdump.py49 from syntax import structs, fresh_name, Struct, mk_word32
50 import syntax namespace
98 typ = syntax.get_global_wrapper (struct.typ)
/seL4-l4v-10.1.1/graph-refine/loop-example/O1/
H A Dtarget.py13 import syntax namespace
26 syntax.parse_and_install_all (f, 'C')
30 (astructs, afunctions, aconst_gs) = syntax.parse_and_install_all (f, 'ASM')
41 syntax.check_funs (functions)
/seL4-l4v-10.1.1/graph-refine/loop-example/O2/
H A Dtarget.py14 import syntax namespace
27 syntax.parse_and_install_all (f, 'C')
31 (astructs, afunctions, aconst_gs) = syntax.parse_and_install_all (f, 'ASM')
42 syntax.check_funs (functions)
/seL4-l4v-10.1.1/graph-refine/seL4-example/
H A Dtarget.py13 import syntax namespace
24 syntax.parse_and_install_all (f, 'C')
28 (astructs, afunctions, aconst_globals) = syntax.parse_and_install_all (f, 'ASM',skip_functions= ['fastpath_call', 'fastpath_reply_recv','c_handle_syscall'])
60 syntax.check_funs (functions)
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/
H A Dtoken_markup.scala4 Outer syntax token markup.
17 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
71 private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int)
78 } yield Token.explode_line(syntax.keywords, text, ctxt)._1
82 syntax: Outer_Syntax,
88 tokens <- try_line_tokens(syntax, buffer, line).iterator
96 syntax: Outer_Syntax,
102 tokens <- try_line_tokens(syntax, buffer, line).iterator
112 def token_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset):
115 line_token_iterator(syntax, buffe
[all...]
H A Disabelle_sidekick.scala88 def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
96 val syntax = Isabelle.buffer_syntax(buffer)
98 if (syntax.isDefined) {
99 val ok = parser(buffer, syntax.get, data)
117 override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
141 make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer)))
178 override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
222 override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/
H A Dtoken_markup.scala4 Outer syntax token markup.
17 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
71 private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int)
78 } yield Token.explode_line(syntax.keywords, text, ctxt)._1
82 syntax: Outer_Syntax,
88 tokens <- try_line_tokens(syntax, buffer, line).iterator
96 syntax: Outer_Syntax,
102 tokens <- try_line_tokens(syntax, buffer, line).iterator
112 def token_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset):
115 line_token_iterator(syntax, buffe
[all...]
H A Disabelle_sidekick.scala88 def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
96 val syntax = Isabelle.buffer_syntax(buffer)
98 if (syntax.isDefined) {
99 val ok = parser(buffer, syntax.get, data)
117 override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
141 make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer)))
178 override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
222 override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
/seL4-l4v-10.1.1/HOL4/src/monad/more_monads/
H A Dstate_transformerSyntax.sml10 fun syntax n d m = function
13 val s1 = syntax 2 HolKernel.dest_monop HolKernel.mk_monop
14 val s2 = syntax 3 HolKernel.dest_binop HolKernel.mk_binop
34 syntax 2
45 syntax 2
71 syntax 2
86 syntax 2
/seL4-l4v-10.1.1/isabelle/src/Pure/Isar/
H A Ddocument_structure.scala34 syntax: Outer_Syntax,
39 is_theory_command(syntax.keywords, command.span.name) &&
81 val spans = syntax.parse_spans(text)
136 /* outer syntax sections */
158 syntax: Outer_Syntax,
162 val sections = new Sections(syntax.keywords)
164 for { span <- syntax.parse_spans(text) } {
166 new Command_Item(syntax.keywords,
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Isar/
H A Ddocument_structure.scala34 syntax: Outer_Syntax,
39 is_theory_command(syntax.keywords, command.span.name) &&
81 val spans = syntax.parse_spans(text)
136 /* outer syntax sections */
158 syntax: Outer_Syntax,
162 val sections = new Sections(syntax.keywords)
164 for { span <- syntax.parse_spans(text) } {
166 new Command_Item(syntax.keywords,
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/
H A Ddocuments0.tex8 pleasing manner. Isabelle provides a rich infrastructure for concrete syntax
10 {\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/
H A Ddocuments0.tex8 pleasing manner. Isabelle provides a rich infrastructure for concrete syntax
10 {\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src-base/
H A Dsyntax_style.scala4 Extended syntax styles: dummy version.
13 import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src-base/
H A Dsyntax_style.scala4 Extended syntax styles: dummy version.
13 import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A Dparse_glob.sig16 All strings generate a regular expression in this syntax. For
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/
H A Dgraph_to_graph.py11 import graph_refine.syntax as syntax namespace
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/bytecode/
H A Dlisp_bytecodeScript.sml11 (* abstract syntax of bytecode *)
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/
H A Dthy_syntax.scala4 Superficial theory syntax: tokens and spans.
66 /** header edits: graph structure and outer syntax **/
99 val syntax =
111 nodes += (name -> node.update_syntax(syntax))
168 syntax: Outer_Syntax,
177 syntax.parse_spans(cmds0.iterator.map(_.source).mkString).map(span =>
178 (Command.blobs_info(resources, syntax, get_blob, can_import, node_name, span), span))
214 syntax: Outer_Syntax,
239 reparse_spans(resources, syntax, get_blob, can_import, name, cmds, first, last))
282 reparse_spans(resources, syntax, get_blo
[all...]

Completed in 142 milliseconds

1234567891011>>