/seL4-l4v-10.1.1/graph-refine/example/ |
H A D | target.py | 9 from target_objects import target_dir, structs, functions, const_globals namespace 21 syntax.check_funs (functions) 24 #pseudo_compile.compile_funcs (functions) 27 #pseudo_compile.combine_function_duplicates (functions) 30 for f in functions: 35 if f2 in functions: 36 pair = logic.mk_pairing (functions, f, f2)
|
/seL4-l4v-10.1.1/graph-refine/loop-example/synth/ |
H A D | target.py | 9 from target_objects import target_dir, structs, functions, const_globals namespace 21 syntax.check_funs (functions) 24 #pseudo_compile.compile_funcs (functions) 27 #pseudo_compile.combine_function_duplicates (functions) 30 for f in functions: 35 if f2 in functions: 36 pair = logic.mk_pairing (functions, f, f2)
|
/seL4-l4v-10.1.1/graph-refine/seL4-example/ |
H A D | target.py | 9 from target_objects import target_dir, structs, functions namespace 41 pseudo_compile.compile_funcs (functions) 46 pairs = [(s, 'Kernel_C.' + s) for s in functions 47 if ('Kernel_C.' + s) in functions] 60 syntax.check_funs (functions)
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | inst_logic.py | 19 from target_objects import functions, trace, pairings, pre_pairings, printout namespace 84 if l_fname in functions: 86 assert r_fname not in functions 108 functions[l_fname] = l_fun 109 functions[r_fname] = r_fun 125 if functions[fname].entry: 144 assert not functions[fname].nodes 145 functions[fname].nodes[1] = call 146 functions[fname].entry = 1 151 if functions[fnam [all...] |
/seL4-l4v-10.1.1/HOL4/src/Boolify/src/ |
H A D | Encode.sig | 4 (* Basically the same as Konrad Slind's code to generate size functions *)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
H A D | protocol_handlers.scala | 19 functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty) 32 (handlers - name, functions -- old_handler.functions.map(_._1)) 33 case None => (handlers, functions) 40 val dups = for ((a, _) <- handler.functions if functions1.isDefinedAt(a)) yield a 41 if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups)) 43 (handlers1 + (name -> handler), functions1 ++ handler.functions) 48 copy(handlers = handlers2, functions = functions2) 61 case Markup.Function(a) if functions.isDefinedAt(a) => 62 try { functions( [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
H A D | protocol_handlers.scala | 19 functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty) 32 (handlers - name, functions -- old_handler.functions.map(_._1)) 33 case None => (handlers, functions) 40 val dups = for ((a, _) <- handler.functions if functions1.isDefinedAt(a)) yield a 41 if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups)) 43 (handlers1 + (name -> handler), functions1 ++ handler.functions) 48 copy(handlers = handlers2, functions = functions2) 61 case Markup.Function(a) if functions.isDefinedAt(a) => 62 try { functions( [all...] |
/seL4-l4v-10.1.1/seL4/libsel4/arch_include/x86/sel4/arch/ |
H A D | syscalls.h | 17 #include <sel4/arch/functions.h>
|
/seL4-l4v-10.1.1/graph-refine/loop-example/O1/ |
H A D | target.py | 9 from target_objects import target_dir, structs, functions, const_globals namespace 38 pseudo_compile.compile_funcs (functions) 41 syntax.check_funs (functions)
|
/seL4-l4v-10.1.1/graph-refine/loop-example/O2/ |
H A D | target.py | 10 from target_objects import target_dir, structs, functions, const_globals namespace 39 pseudo_compile.compile_funcs (functions) 42 syntax.check_funs (functions)
|
/seL4-l4v-10.1.1/HOL4/Manual/Reference/ |
H A D | entries-intro.tex | 4 in the \HOL{} system. These include: general-purpose functions, such 5 as functions for list processing, arithmetic, input/output, and 6 interface configuration; functions for processing the types and terms
|
H A D | preface.tex | 19 functions, such as \ML\ functions for list processing, arithmetic, 20 input/output, and interface configuration; functions for processing the types
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
H A D | advanced0.tex | 22 %functions, how to define recursive functions over nested recursive datatypes 23 %and how to deal with partial functions. 26 %functions is overly complicated by the requirement of 27 %totality, you should ponder the alternatives. In a logic of partial functions, 46 %\index{functions!partial}
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | advanced0.tex | 22 %functions, how to define recursive functions over nested recursive datatypes 23 %and how to deal with partial functions. 26 %functions is overly complicated by the requirement of 27 %totality, you should ponder the alternatives. In a logic of partial functions, 46 %\index{functions!partial}
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | compilerLib.sig | 19 (* these functions expose the back-end functions *)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | acl2encodeLib.sig | 4 (* Functions are encoded using the translate_..._function functions, and *) 40 (* The translation of under-specified recursive functions (eg. SEG) is *) 69 (* This has the advantage that functions run must faster. However, ACL2 *) 84 (* However, if functions are translated using the destructors then the *) 93 (* Initialises a type so that functions over it can be translated to ACL2 *) 94 (* This generates the following functions: *) 96 (* The standard map and all functions, these can be viewed *) 99 (* These functions form the basis of the translation and may *) 118 (* These functions translate non-polymorphic definitions that do not use *) 135 (* The first of these functions shoul [all...] |
H A D | tutorial.ml | 9 (* We also load the example types and the example functions. *) 16 (* Simple functions: *) 20 (* We start by encoding simple functions, that is, functions that may be *) 22 (* only on functions that may be encoded across their entire range. *) 24 (* form, where mutually recursive functions are given as conjunctions. *) 26 (* Such functions are translated using the function: *) 30 (* functions and the second is the argument itself. *) 108 (* function creates recognition functions, suitable for export to ACL2, for *) 136 (* As rewrites for translated functions ar [all...] |
/seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/ |
H A D | Makefile | 31 tex: theorems functions 34 functions:
|
/seL4-l4v-10.1.1/HOL4/examples/miller/prob/ |
H A D | prob_pseudoTools.sml | 17 (* Simple ML functions to help find good parameters for the linear
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/ |
H A D | print_operation.scala | 41 val functions = List(Markup.PRINT_OPERATIONS -> put _)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/ |
H A D | print_operation.scala | 41 val functions = List(Markup.PRINT_OPERATIONS -> put _)
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
H A D | lisp_extractLib.sig | 6 (* main functions for extraction *)
|
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
H A D | bench.py | 21 from graph_refine.target_objects import functions, functions_by_tag namespace 153 functions = target_objects.functions
|
/seL4-l4v-10.1.1/HOL4/src/holyhammer/ |
H A D | holyHammer.sig | 38 (* Main functions *) 41 (* saving results of the next functions in goaltac_cache *) 47 (* Other functions *)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/Hahn_Banach/document/ |
H A D | root.tex | 45 normed spaces, continuous linear-forms, norm of functions and an order on 46 functions by domain extension. The second part contains some lemmas about the 47 supremum (w.r.t.\ the function order) and extension of non-maximal functions.
|