/seL4-l4v-10.1.1/graph-refine/example/ |
H A D | target.py | 12 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 D | target.py | 12 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 D | inst_logic.py | 9 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 D | c_rodata.py | 1 import syntax namespace 25 hyp = rep.to_smt_expr (syntax.mk_implies (pc, 26 syntax.mk_not (eq_rodata)), (n, vc))
|
H A D | stack_logic.py | 9 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 D | logic.py | 9 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 D | objdump.py | 49 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 D | target.py | 13 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 D | target.py | 14 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 D | target.py | 13 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 D | token_markup.scala | 4 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 D | isabelle_sidekick.scala | 88 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 D | token_markup.scala | 4 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 D | isabelle_sidekick.scala | 88 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 D | state_transformerSyntax.sml | 10 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 D | document_structure.scala | 34 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 D | document_structure.scala | 34 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 D | documents0.tex | 8 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 D | documents0.tex | 8 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 D | syntax_style.scala | 4 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 D | syntax_style.scala | 4 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 D | parse_glob.sig | 16 All strings generate a regular expression in this syntax. For
|
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
H A D | graph_to_graph.py | 11 import graph_refine.syntax as syntax namespace
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/bytecode/ |
H A D | lisp_bytecodeScript.sml | 11 (* abstract syntax of bytecode *)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/ |
H A D | thy_syntax.scala | 4 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...] |