Searched refs:functions (Results 1 - 25 of 723) sorted by relevance

1234567891011>>

/seL4-l4v-master/graph-refine/example/
H A Dtarget.py7 from target_objects import target_dir, structs, functions, const_globals namespace
19 syntax.check_funs (functions)
22 #pseudo_compile.compile_funcs (functions)
25 #pseudo_compile.combine_function_duplicates (functions)
28 for f in functions:
33 if f2 in functions:
34 pair = logic.mk_pairing (functions, f, f2)
/seL4-l4v-master/graph-refine/loop-example/synth/
H A Dtarget.py7 from target_objects import target_dir, structs, functions, const_globals namespace
19 syntax.check_funs (functions)
22 #pseudo_compile.compile_funcs (functions)
25 #pseudo_compile.combine_function_duplicates (functions)
28 for f in functions:
33 if f2 in functions:
34 pair = logic.mk_pairing (functions, f, f2)
/seL4-l4v-master/graph-refine/seL4-example/
H A Dtarget.py7 from target_objects import target_dir, structs, functions namespace
39 pseudo_compile.compile_funcs (functions)
44 pairs = [(s, 'Kernel_C.' + s) for s in functions
45 if ('Kernel_C.' + s) in functions]
58 syntax.check_funs (functions)
/seL4-l4v-master/graph-refine/
H A Dinst_logic.py17 from target_objects import functions, trace, pairings, pre_pairings, printout namespace
82 if l_fname in functions:
84 assert r_fname not in functions
106 functions[l_fname] = l_fun
107 functions[r_fname] = r_fun
123 if functions[fname].entry:
142 assert not functions[fname].nodes
143 functions[fname].nodes[1] = call
144 functions[fname].entry = 1
149 if functions[fnam
[all...]
/seL4-l4v-master/HOL4/src/Boolify/src/
H A DEncode.sig4 (* Basically the same as Konrad Slind's code to generate size functions *)
/seL4-l4v-master/isabelle/src/Pure/PIDE/
H A Dprotocol_handlers.scala19 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-master/l4v/isabelle/src/Pure/PIDE/
H A Dprotocol_handlers.scala19 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-master/graph-refine/loop-example/O1/
H A Dtarget.py7 from target_objects import target_dir, structs, functions, const_globals namespace
36 pseudo_compile.compile_funcs (functions)
39 syntax.check_funs (functions)
/seL4-l4v-master/graph-refine/loop-example/O2/
H A Dtarget.py7 from target_objects import target_dir, structs, functions, const_globals namespace
36 pseudo_compile.compile_funcs (functions)
39 syntax.check_funs (functions)
/seL4-l4v-master/HOL4/src/finite_maps/
H A Dalist_treeLib.sig1 (* Code to recall that some partial functions (of type 'a -> 'b option)
3 applications of those functions. *)
18 Representations of partial functions using sorted trees.
30 partial functions, initially none.
47 for functions f in the repr set.
/seL4-l4v-master/HOL4/Manual/Reference/
H A Dentries-intro.tex4 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 Dpreface.tex19 functions, such as \ML\ functions for list processing, arithmetic,
20 input/output, and interface configuration; functions for processing the types
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/
H A Dadvanced0.tex22 %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-master/l4v/isabelle/src/Doc/Tutorial/document/
H A Dadvanced0.tex22 %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-master/HOL4/examples/machine-code/compiler/
H A DcompilerLib.sig19 (* these functions expose the back-end functions *)
/seL4-l4v-master/seL4/libsel4/arch_include/x86/sel4/arch/
H A Dsyscalls.h10 #include <sel4/functions.h>
/seL4-l4v-master/HOL4/src/portableML/
H A DImplicitGraph.sig19 (* fold functions get passed distance from root as extra integer parameter.
20 the "lim" versions of the functions will drop visited nodes that have depths
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A Dacl2encodeLib.sig4 (* 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 Dtutorial.ml9 (* 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-master/HOL4/src/res_quan/Manual/
H A DMakefile31 tex: theorems functions
34 functions:
/seL4-l4v-master/HOL4/examples/miller/prob/
H A Dprob_pseudoTools.sml17 (* Simple ML functions to help find good parameters for the linear
/seL4-l4v-master/isabelle/src/Pure/Tools/
H A Dprint_operation.scala41 val functions = List(Markup.PRINT_OPERATIONS -> put _)
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/
H A Dprint_operation.scala41 val functions = List(Markup.PRINT_OPERATIONS -> put _)
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractLib.sig6 (* main functions for extraction *)
/seL4-l4v-master/graph-refine/graph-to-graph/
H A Dbench.py19 from graph_refine.target_objects import functions, functions_by_tag namespace
151 functions = target_objects.functions

Completed in 123 milliseconds

1234567891011>>