/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | SmtLib_Parser.sml | 28 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 D | boyer_mooreScript.sml | 32 (* 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 D | ForeignMemory.sml | 49 (* 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 D | Prim_rec.sml | 92 (* 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 D | IndDefRules.sml | 21 (* 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 D | description.tex | 63 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 D | MLY_parser2.sml | 47 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 D | parser2.sml | 17 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 D | parser2.sml | 17 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 D | CODETREE_FUNCTIONS.sml | 90 (* 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 D | logic.tex | 57 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 D | version2.tex | 41 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 D | HolSat.tex | 51 {\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 D | version2.tex | 41 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 D | tactics.tex | 78 \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 D | smlParallel.sml | 78 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 D | unwindLib.sml | 321 (* 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 D | compile.sig | 12 (* 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 D | adder-in-Model.ml | 46 % 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 D | mod.ml | 16 % 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 D | Net.sig | 55 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 D | Net.sig | 55 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 D | Boolconv.sml | 26 fun failwith function = raise (ERR function "");
|
/seL4-l4v-master/HOL4/src/pfl/examples/ |
H A D | tree.sml | 77 (* Indexed function definition *) 89 (* Domain of the function. *)
|
/seL4-l4v-master/HOL4/src/prekernel/ |
H A D | FinalNet-sig.sml | 45 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.
|