/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_LAMBDA_LIFT.sml | 20 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 D | CODETREE_OPTIMISER.sml | 136 (* 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 D | quicksort.ml | 34 % 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 D | RJBConv.sml | 27 fun failwith function = raise (ERR function "");
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | KnuthBendixOrder.sml | 24 (* 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 D | Portable.sig | 40 (* Timing function applications. *)
|
H A D | Term.sig | 17 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 D | KnuthBendixOrder.sml | 24 (* 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 D | Portable.sig | 40 (* Timing function applications. *)
|
H A D | Term.sig | 17 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 D | mlibTptp.sig | 12 (* Maintaining different relation and function names in TPTP problems *)
|
/seL4-l4v-master/HOL4/src/opentheory/compat/ |
H A D | OpenTheoryFunctionScript.sml | 3 val pkg = "function-1.55"
|
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | Intmap.sig | 50 [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 D | Binarymap.sig | 53 [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 D | lisp_extractLib.sig | 13 (* function used for code synthesis *)
|
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | compiler_proofsScript.sml | 2 Proves that the compiler in assembly form implements the compiler function.
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | AC_Sort.sig | 26 dest: destructor function for operator 28 mk: constructor function for operator 30 cmp: comparison function for performing sort. Terms identified
|
H A D | Prim_rec.sig | 27 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 D | FlagPrint.sml | 20 (* 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 D | intro.tex | 4 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 D | intro.tex | 4 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 D | funcCall.sml | 34 (* 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 D | monomorphisation.sml | 14 (* 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 D | Recftn.sml | 3 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 D | tutorial.ml | 26 (* 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...] |