Searched refs:function (Results 201 - 225 of 876) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/src/HolSmt/
H A DSmtLib_Parser.sml28 token. 4. Parsing a function symbol in some cases requires that
29 the function arguments have been parsed (e.g., to instantiate
40 functions. 4. Each parsing function maps a (possibly empty) list
41 of function arguments (parsed as HOL terms) to the HOL term that
42 results from applying the (function corresponding to the) token
44 valid. 'parse_term' uses the result of the first parsing function
45 that does not raise 'HOL_ERR'. 5. Each parsing function
54 dictionary entry for a token (or every parsing function in its
56 of the first parsing function in the entry for "_" that does not
443 declared function symbol
[all...]
/seL4-l4v-master/HOL4/examples/boyer_moore/
H A Dboyer_mooreScript.sml32 (* Relationship between checkDeltaC function
66 (* Intermediate lemmas to reason about recursive function bounds *)
156 (* Relationship between cmVal function and valid_cha_shift specification *)
172 (* Proving bounds on cmVal function with valid input *)
203 (* Relationship between checkDeltaS function
272 (* Intermediate lemmas to reason about recursive function bounds *)
369 (* Relationship between smVal function and valid_suf_shift specification *)
390 (* Proving bounds on smVal function with valid input *)
680 (* Final proof that the bmSearch function correctly searches
825 (* Final proof that the bmSearchString function correctl
[all...]
/seL4-l4v-master/HOL4/polyml/basis/
H A DForeignMemory.sml49 (* alloca: allocate temporary memory on the C-stack and call the function.
50 The memory is deallocated when the function returns or raises and exception. *)
80 (* Internal utility function. *)
129 (* Initialise to zero. That means the function won't be
134 We need to execute the function and set it. *)
/seL4-l4v-master/HOL4/src/1/
H A DPrim_rec.sml92 (* last arguments in the pattern will be instances of a function symbol
257 (* Version that defines function(s). *)
346 Make a new recursive function definition.
473 (* Internal function: *)
495 (* Internal function: GTAC *)
515 (* Internal function: TACF *)
544 (* TACF is a strictly local function, used only to define TACS, below. *)
566 (* Internal function: TACS *)
580 (* TACS is a strictly local function, used only in INDUCT_THEN. *)
590 (* Internal function
[all...]
/seL4-l4v-master/HOL4/src/IndDef/
H A DIndDefRules.sml21 (* This function takes an axiom of the form *)
52 if its the argument of a higher-order function like EVERY. *)
175 (* Internal function: TACF *)
221 (* TACF is a strictly local function, used only to define TACS, below. *)
259 (* Internal function: TACS *)
273 (* TACS is a strictly local function, used only in INDUCT_THEN. *)
287 (* Internal function RED_WHERE. *)
289 (* Given the arguments "f" and "tm[f]", this function produces a *)
485 (* The function returns the reduced list of theorems, paired with a list *)
/seL4-l4v-master/HOL4/src/res_quan/Manual/
H A Ddescription.tex63 with the function:
208 The ML function \ml{COND\_REWR\_CANON} transforms a theorem
246 search function \ml{search\_top\_down}. This function determines how to
248 search function, other conditional rewriting strategy can be
347 This function only transforms the restricted existential quantifier to
350 The function \ml{RESQ\_MATCH\_MP} eliminates a restricted universal
368 The ML function
370 function \ml{LIST\_RESQ\_FORALL\_CONV} is an iterative version of
/seL4-l4v-master/HOL4/tools/mlyacc/mlyacclib/
H A DMLY_parser2.sml47 action should produce a function from unit -> value instead of producing the
50 and apply the unit -> value function in it to get the answer.
214 steady-state. It takes a table, showTerminal function, saction
215 function, and fixError function. It parses until an ACCEPT is
263 error are encountered. Takes a table, showTerminal function, and
264 semantic action function. Returns a parser which takes a lexPair
304 (* mkFixError: function to create fixError function which adjusts parser state
/seL4-l4v-master/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/
H A Dparser2.sml17 action should produce a function from unit -> value instead of producing the
20 and apply the unit -> value function in it to get the answer.
186 steady-state. It takes a table, showTerminal function, saction
187 function, and fixError function. It parses until an ACCEPT is
235 error are encountered. Takes a table, showTerminal function, and
236 semantic action function. Returns a parser which takes a lexPair
276 (* mkFixError: function to create fixError function which adjusts parser state
/seL4-l4v-master/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/
H A Dparser2.sml17 action should produce a function from unit -> value instead of producing the
20 and apply the unit -> value function in it to get the answer.
186 steady-state. It takes a table, showTerminal function, saction
187 function, and fixError function. It parses until an ACCEPT is
235 error are encountered. Takes a table, showTerminal function, and
236 semantic action function. Returns a parser which takes a lexPair
276 (* mkFixError: function to create fixError function which adjusts parser state
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DCODETREE_FUNCTIONS.sml90 (* A built-in function may be side-effect free. This can
93 inside an inline function and some of the arguments to the
94 function are constants. This then gets converted to
161 a function call. It should never have a side-effect so it might
492 fun evaluateInlining(function, numArgs, maxInlineSize) =
494 (* This checks for the possibility of inlining a function. It sees if it is
496 for recursive uses of the function.
497 Typically if the function is small enough to inline there will be only
518 fun checkUse _ (_, 0, _) = 0 (* The function is too big to inline. *)
539 (* For the moment, any recursive use in an inner function prevent
[all...]
/seL4-l4v-master/HOL4/Manual/Tutorial/
H A Dlogic.tex57 For example, the \ML{} function \ml{dest\_imp} with \ML{} type \ml{term -> term * term} splits an implication into a pair of terms consisting of its antecedent and consequent, and the \ML\ function \ml{dest\_conj} of type \ml{term -> term * term} splits a conjunction into its two conjuncts.%
85 The built-in function \ml{type_of} has \ML{} type \ml{term->hol_type} and returns the logical type of a term.
118 The function \ml{mk_var} constructs a variable from a string and a type.
145 There are actually only four different kinds of term in \HOL: variables, constants, function applications (\ml{``$t_1$ $t_2$``}), and lambda abstractions (\ml{``\bs$x$.$t$``}).
201 An application $(t_1\ t_2)$ is well-typed if $t_1$ is a function with type $\tau_1 \to \tau_2$ and $t_2$ has type $\tau_1$.
202 Contrarily, an application $(t_1\ t_2)$ is badly typed if $t_1$ is not a function:
222 \noindent or if it is a function, but $t_2$ is not in its domain:
261 Functions have types of the form \ml{$\sigma_1$->$\sigma_2$}, where $\sigma_1$ and $\sigma_2$ are the types of the domain and range of the function, respectively.
295 For example, {\small\verb|``\x. x+1``|} is a term that denotes the function
[all...]
/seL4-l4v-master/HOL4/Manual/Description/
H A Dversion2.tex41 The type definition package (i.e.\ the \ML\ function
163 The \ml{install} function now sets the search path to:
173 The function
191 \ml{library\_pathname} can be changed by users only via the \ml{install} function.
216 displaying help files. This default can be changed with the \ML\ function:
223 \noindent This installs a new user-supplied help function, and returns the
231 into the current help function,
261 and these two function are analogous to the \ML\ functions
318 with the function:
481 the infixed function \m
[all...]
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A DHolSat.tex51 {\tt{HolSatLib}} provides a function {\tt SAT\_PROVE} \index{HolSatLib!SAT\_PROVE@\ml{SAT\_PROVE}} for propositional satisfiability testing and for proving propositional tautologies. It uses an external SAT solver (currently MiniSat 1.14p) to find an unsatisfiability proof or satisfying assignment, and then reconstructs the proof or checks the assignment deductively in \HOL.
53 Alternatively, the function {\tt SAT\_ORACLE} \index{HolSatLib!SAT\_ORACLE@\ml{SAT\_ORACLE}} has the same behaviour as {\tt SAT\_PROVE} but asserts the result of the solver without proof. The theorem thus asserted is tagged with ``{\tt{HolSatLib}}'' to indicate that it is unchecked. Since proof reconstruction can be expensive, the oracle facility can be useful during prototyping, or if proof is not required.
129 The functions described above are wrappers for the function \texttt{GEN\_SAT}, which is the single entry point for {\tt{HolSatLib}}. \texttt{GEN\_SAT} can be used directly if more flexibility is required. \texttt{GEN\_SAT} takes a single argument, of type \texttt{sat\_config}, defined in \texttt{satConfig.sml}. This is an opaque record type, currently containing the following fields:
176 Temporary files are generated using the Moscow ML function \t{FileSys.tmpName}. This usually writes to the standard temporary file space on the operating system. If that file space is full, or if it is inaccessible for some other reason, {\tt{HolSatLib}} calls may fail mysteriously.
178 The function {\tt dimacsTools.readDimacs}~{\it file} reads a DIMACS format file and returns
179 a CNF \HOL{} term corresponding to the SAT problem in the file named by {\it file}. Since DIMACS uses numbers to denote variables, and numbers are not legal identifiers in \HOL{}, each variable number is prefixed with the string ``{\tt v}''. This string is defined in the reference variable {\tt dimacsTools.prefix} and can be changed if required. This function can be used independently of {\tt{HolSatLib}} to read in DIMACS format files.
H A Dversion2.tex41 The type definition package (i.e. the \ML\ function
163 The \ml{install} function now sets the search path to:
173 The function
191 \ml{library\_pathname} can be changed by users only via the \ml{install} function.
216 displaying help files. This default can be changed with the \ML\ function:
223 \noindent This installs a new user-supplied help function, and returns the
231 into the current help function,
261 and these two function are analogous to the \ML\ functions
318 with the function:
481 the infixed function \m
[all...]
H A Dtactics.tex78 \index{proof steps, as ML function applications@proof steps, as \ML{} function applications}
79 is an \ML{} function that when applied to a \emph{goal}
85 function mapping a list of theorems to a theorem. The idea is that
86 the function justifies the decomposition of the goal.
110 \index{proofs, in HOL logic@proofs, in \HOL{} logic!as ML function applications@as \ML{} function applications}
113 an \ML{} function
114 from a theorem list to a theorem. The \ML{} `proof' function
119 evaluate the \ML{} function correspondin
[all...]
/seL4-l4v-master/HOL4/src/AI/sml_inspection/
H A DsmlParallel.sml78 The function parmap_gen start n threads, and generate a parmap function
79 relying on this threads and a function to close this threads.
216 function : 'a -> 'b -> 'c,
372 val r = (#function es) param arg
424 function = let fun f _ (x:int) = x in f end,
/seL4-l4v-master/HOL4/src/unwind/
H A DunwindLib.sml321 (* The function p:term->bool is a predicate which will be *)
354 (* fnn = a function which, when applied to a rewriting conversion *)
359 (* pf = a function which maps |- tm to [|- t1;...;|- tj] where each *)
454 (* function decides which equations to use by performing a loop analysis on *)
459 (* The algorithms used for loop analysis in this function are extremely *)
463 (* Amongst other things, the internal function "graph_of_term' rearranges the*)
465 (* gives them priority over the internal lines when the function is *)
648 (* function decides which equations to use by performing a loop analysis on *)
692 (* x1 and x2 do not appear free in t but x3 does, the function will fail; it *)
957 (* possible the function wil
[all...]
/seL4-l4v-master/HOL4/examples/dev/
H A Dcompile.sig12 (* Error reporting function *)
119 (* function of the form f(x) = if f1(x) then f2(x) else f (f3(x)) *)
204 (* Allows measure function to be indicated in same quotation as definition, *)
209 (* will use f as the measure function and attempt automatic termination *)
212 (* parse errors result. Also, the name of the defined function must be *)
215 (* One can also omit the measure function, as in Define: *)
292 (* A refinement function is an ML function that maps a term ``DEV f`` to *)
/seL4-l4v-master/HOL4/examples/hardware/hol88/
H A Dadder-in-Model.ml46 % The higher-order function ITERATE has type: %
60 % To define ITERATE we first define another function ITER by primitive %
/seL4-l4v-master/HOL4/examples/hardware/hol88/tamarack2/
H A Dmod.ml16 % DESCRIPTION : Defines MOD function for natural numbers and proves %
17 % some useful theorems about this function, including %
/seL4-l4v-master/HOL4/src/0/
H A DNet.sig55 that a matching function would have to make, say when rewriting
83 [itnet f net b] folds function f through net, with base value b.
/seL4-l4v-master/HOL4/src/experimental-kernel/
H A DNet.sig55 that a matching function would have to make, say when rewriting
83 [itnet f net b] folds function f through net, with base value b.
/seL4-l4v-master/HOL4/src/num/reduce/src/
H A DBoolconv.sml26 fun failwith function = raise (ERR function "");
/seL4-l4v-master/HOL4/src/pfl/examples/
H A Dtree.sml77 (* Indexed function definition *)
89 (* Domain of the function. *)
/seL4-l4v-master/HOL4/src/prekernel/
H A DFinalNet-sig.sml45 that a matching function would have to make, say when rewriting
73 [itnet f net b] folds function f through net, with base value b.

Completed in 400 milliseconds

1234567891011>>