Searched refs:function (Results 26 - 50 of 876) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DCODETREE_LAMBDA_LIFT.sml20 Lambda-lifting. If every call point to a function can be identified we can
24 function of a stack-closure cannot call a stack-closure with tail-recursion
25 because the closure must remain on the stack until the function returns.
26 Also we can lambda-lift a function even if it is used in a function that
28 function if the closure would be used in a full, heap closure.
70 | checkCode(Eval{function as Extract _, argList, resultType}) =
71 (* A call of a function. We don't need to mark the function as needing a closure. *)
73 Eval{function
[all...]
H A DCODETREE_OPTIMISER.sml136 (* This transforms the body of a "small" recursive function replacing any reference
142 | repEntry(Eval { function = Extract LoadRecursive, argList, resultType }) =
160 (* If we have a tail recursive function we can replace the tail calls
187 (* If we have a small recursive function where some arguments are passed
198 (* This is the argument from the outer function. It is either added
199 to the closure or passed to the inner function. *)
221 function = Extract LoadRecursive, argList = l, resultType = t
223 isInline = DontInline, (* Don't inline this function. *)
231 function = subFunction,
238 (* If the function argument
[all...]
/seL4-l4v-master/HOL4/examples/hardware/hol88/
H A Dquicksort.ml34 % The function list_fun_def_functional should satisfy:
39 function f in the list satisfies |- !x. length(f x) < length x ).
/seL4-l4v-master/HOL4/src/num/arith/src/
H A DRJBConv.sml27 fun failwith function = raise (ERR function "");
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DKnuthBendixOrder.sml24 (* one unary function with weight 0. *)
28 {weight : Term.function -> int,
29 precedence : Term.function * Term.function -> order};
33 val uniformWeight : Term.function -> int = K 1;
37 val arityPrecedence : Term.function * Term.function -> order =
49 (* Term weight-1 represented as a linear function of the weight-1 of the *)
H A DPortable.sig40 (* Timing function applications. *)
H A DTerm.sig17 type function = functionName * int type
49 val fnFunction : term -> function
78 (* A total comparison function for terms. *)
131 val hasTypeFunction : function
140 (* Special support for terms with an explicit function application operator. *)
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DKnuthBendixOrder.sml24 (* one unary function with weight 0. *)
28 {weight : Term.function -> int,
29 precedence : Term.function * Term.function -> order};
33 val uniformWeight : Term.function -> int = K 1;
37 val arityPrecedence : Term.function * Term.function -> order =
49 (* Term weight-1 represented as a linear function of the weight-1 of the *)
H A DPortable.sig40 (* Timing function applications. *)
H A DTerm.sig17 type function = functionName * int type
49 val fnFunction : term -> function
78 (* A total comparison function for terms. *)
131 val hasTypeFunction : function
140 (* Special support for terms with an explicit function application operator. *)
/seL4-l4v-master/HOL4/src/metis/
H A DmlibTptp.sig12 (* Maintaining different relation and function names in TPTP problems *)
/seL4-l4v-master/HOL4/src/opentheory/compat/
H A DOpenTheoryFunctionScript.sml3 val pkg = "function-1.55"
/seL4-l4v-master/HOL4/src/portableML/poly/
H A DIntmap.sig50 [app f m] applies function f to the entries (i, v) in m, in
53 [revapp f m] applies function f to the entries (i, v) in m, in
56 [foldl f e m] applies the folding function f to the entries (i, v)
59 [foldr f e m] applies the folding function f to the entries (i, v)
/seL4-l4v-master/HOL4/tools-poly/poly/
H A DBinarymap.sig53 [app f m] applies function f to the entries (k, v) in m, in
57 [revapp f m] applies function f to the entries (k, v) in m, in
60 [foldl f e m] applies the folding function f to the entries (k, v)
63 [foldr f e m] applies the folding function f to the entries (k, v)
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractLib.sig13 (* function used for code synthesis *)
/seL4-l4v-master/HOL4/examples/bootstrap/
H A Dcompiler_proofsScript.sml2 Proves that the compiler in assembly form implements the compiler function.
/seL4-l4v-master/HOL4/src/1/
H A DAC_Sort.sig26 dest: destructor function for operator
28 mk: constructor function for operator
30 cmp: comparison function for performing sort. Terms identified
H A DPrim_rec.sig27 once, this function returns the definitions of the case constants for
40 Similarly, this function returns a list of theorems where each theorem
52 (* A utility function *)
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/
H A DFlagPrint.sml20 (* Auxiliary function to create a function to print out bit flags.
21 The function must actually be installed by the caller because
/seL4-l4v-master/isabelle/src/Doc/Functions/document/
H A Dintro.tex4 function definitions~\cite{krauss2006} are available. They provide
6 packages. But despite all tool support, function definitions can
26 Section 3 introduces the more verbose \cmd{function} command which
37 non-recursive form, such that the function can be defined using
48 The new \cmd{function} command, and its short form \cmd{fun} have mostly
/seL4-l4v-master/l4v/isabelle/src/Doc/Functions/document/
H A Dintro.tex4 function definitions~\cite{krauss2006} are available. They provide
6 packages. But despite all tool support, function definitions can
26 Section 3 introduces the more verbose \cmd{function} command which
37 non-recursive form, such that the function can be defined using
48 The new \cmd{function} command, and its short form \cmd{fun} have mostly
/seL4-l4v-master/HOL4/examples/dev/sw2/
H A DfuncCall.sml34 (* Is an expression a function application? *)
45 (* Traverse the function body to find all modified registers and the next available memory slot *)
106 (* Convert a function body into its call-save format *)
126 val tr_f = ref (``T``); (* the name of a recursive function *)
150 if is_fun x andalso not (x = !tr_f) then (* non-recursive function application *)
160 mk_plet(v, caller_save M, caller_save N) (* not function application *)
181 for each function call; it also make the outputs of the two branches of a conditional
192 if is_fun x andalso not (x = !tr_f) then (* non-recursive function application *)
206 in (mk_plet(v, M', N'), output') end (* not function application *)
227 (* Process function call
[all...]
H A Dmonomorphisation.sml14 (* The basic idea is to duplicate a datatype declaration at each type used and a function *)
16 (* and function. *)
46 fun is_fun t = (* the term is a function? *)
59 (* Format: [function's name |-> [type |-> instantiation set] ] *)
62 (* Format: [function's name |-> a set of new defitions] *)
172 (* SOME (#1 ((strip_comb o lhs o concl o SPEC_ALL o DB.definition) (f_str ^ "_def"))) (* be a predefined function *) *)
182 if is_pabs M then (* an embedded function *)
215 else if is_fun M then (* function application *)
227 (* handle _ => M.mkDict strOrder (* not function application *) *)
255 (* format: function nam
[all...]
/seL4-l4v-master/HOL4/src/datatype/mutrec/
H A DRecftn.sml3 description of how the function should behave the values of the
7 that compute the return value of the function from the arguments
10 instantiate our recursive function with them, define the functions,
15 there must be at most one function defined for each type (there need
16 not be a function defined for every type). If a function is being
23 first term gives explictly the values of the function on all
24 constructors for each type for which a function is defined, and the
26 the constructors. The "allelse" works like this: Say a function is
34 right of the = sign is used as the value of the function o
[all...]
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A Dtutorial.ml26 (* Such functions are translated using the function: *)
29 (* The first argument relates function constants to the names of translated *)
32 (* The function EXP: *)
58 (* functionEncodeLib.rewrites, using the function *)
61 (* The function LENGTH (instantiated to operate on concrete lists of natural *)
106 (* 'listnum' is created using the function: *)
108 (* function creates recognition functions, suitable for export to ACL2, for *)
111 (* We can create a different translation using this function directly: *)
180 (* The function 'i2n' is defined as follows: *)
261 (* their entire range. In the case of SEG this is because the function *)
[all...]

Completed in 170 milliseconds

1234567891011>>