/seL4-l4v-master/HOL4/src/datatype/mutrec/ |
H A D | ConsThms.sml | 42 (* This function divides up a list of applied constructors into a list 64 (* This function proves that constructors are distinct, ie, for each TY 121 (* the following function takes the constructor first in the list, (say 139 (* this function makes all the conjuncts for one type *) 222 We apply the appropriate distinctness function, getting 262 (* This function proves that constructors are one-to-one, ie, for each TY 353 extraction function will be called CON_arg.) *) 442 a pair consisting of the definition of the function and the name of 443 the function defined. *) 524 (* This function prove [all...] |
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | DEBUGGER_.sml | 66 (* Global function entries. These could be in storage allocated by the RTS. *) 67 (* Specialised option type here. Because a function is always boxed this 215 return a function because we will use applyToInstanceType to apply it to the 253 because the next reference could be inside an inner function. 405 (* Add debugging calls on entry and exit to a function. *) 436 (* At the start of the function: 440 4. Call the global onEntry function if it's set 441 5. Call the local onEntry function if it's set *) 454 to be passed to the body of the function so that it is included in the 486 (* Restore the state. Used both if the function return [all...] |
/seL4-l4v-master/HOL4/examples/dev/ |
H A D | vsynth.sml | 46 (* Error reporting function *) 156 print "\nis not a function type\n"; 157 raise ERR "dest_unop_type" "not a function type") 172 print "\nis not a function type\n"; 173 raise ERR "dest_binop_type" "not a function type") 468 (* ClockvInst out n "clk" prints, using function out, an instance of Clock *) 517 handle e => (print "ML function associated in vsynth_lib with:\n";
|
/seL4-l4v-master/HOL4/examples/elliptic/c_output/ |
H A D | c_outputLib.sml | 200 ) ("Unknown function '"^f_name^"'!") 242 ("Unknown boolean function '"^(term_to_string exp)^"'!"); 251 (syntax_error true ("Unknown boolean function '"^(term_to_string exp)^"'!"); (false, "")); 436 ("The function '"^fun_name^"' is not a function on 32-bit words!"); 612 (print "The main function is not in the list of definitions!\n";fail()) else (); 619 val _ = print "The following constants are unkown to the C-export function. Please add additional definitions or rewrites:\n";
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | OmegaSymbolic.sml | 106 This function attempts to prove |- EVERY fst_nzero ^t 140 This function attempts to prove |- EVERY fst1 ^t 166 This function attempts to prove |- EVERY (\p. FST p <= ^m) ^t 198 defining the corresponding row function (conjuncts of 358 This function expands it into an equation of the form 408 Every ci is a valid Omega leaf. This function converts the body 569 fully normalised leaves. This function picks one of the quantifiers
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | Portable.sml | 527 * A hash function used for various tasks in the system. It works fairly * 529 * argument should be a prime. The function then takes a string and * 682 * Invoking a function with a flag temporarily assigned to the given value. * 741 A function that strips leading (nested) comments and whitespace 780 * pfun = item printing function 781 * dfun = delimiter printing function 782 * bfun = break printer function
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | LibraryIOSupport.sml | 18 (* This function provides wrappers for the RTS file descriptors to construct 173 (* If evaluating the function raises EAGAIN or EWOULDBLOCK we return NONE 277 (* Unlike the other functions "avail" is a function returning 278 an option, not an optional function. *) 389 (* Unlike the other functions "avail" is a function returning 390 an option, not an optional function. *) 462 This applies a function while a mutex is being held. *)
|
H A D | BoolArray.sml | 56 The equality function we're using tests all the bytes so we need to initialise them. *) 126 (* Internal function which subscripts the vector assuming that 234 apply the function beyond the last bit. *) 261 apply the function beyond the last bit. *) 363 (* Internal function for updating a bit assuming the bounds 399 (* Exported update function. *)
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | mechReasoning.sml | 290 (* the characteristic function *) 293 val f_c = mk_pabs (initV, subst rules (calculate_outs post_st outs)); (* the charateristic function *) 299 (* the stack function *) 317 (* Given an basic block, the charateristic function on inputs and outputs are derived by symbolic simulation *) 415 (* the characteristic function of SC *) 515 (* Given a TR, the charateristic function on inputs and outputs are derived by the TR_RULE *) 550 val cj_cond = subst rules instance1 (* the condition function *) 555 fun mk_cond_f cond_t ins = (* the condition function *) 616 (* the characteristic function *) 686 (* the characteristic function *) [all...] |
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | conv.tex | 22 is an \ML\ function of type \ml{conv} (\ie\ a conversion) that 149 this exception appropriately. The standard function \ml{QCONV} is 319 subterm of a term, the function \ml{DEPTH\_CONV} can be applied to $c$: 363 \noindent The function \ml{TOP\_DEPTH\_CONV} 386 Finally, the simpler function \ml{ONCE\_DEPTH\_CONV} is provided: 507 The function \ml{FIRST\_CONV} 545 The function \ml{EVERY\_CONV} applies a list of conversions in sequence. 625 \noindent The function \ml{SUB\_CONV} 821 and the successor function \ml{SUC}, then: 916 done component-wise, and function application [all...] |
H A D | HolBdd.tex | 110 In Version~1 there was a function, called 269 Initialisation is done with the ML function 309 The function 320 The function 333 using the function \t{stats} 393 The function \t{toBool} returns \t{true} on TRUE and \t{false} on FALSE. 421 dynamically. The function 430 The function 478 \Muddy{} provides a function for general purpose simultaneous 504 Variables can be renamed using the function \ [all...] |
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/binomial/ |
H A D | binomial.tex | 136 $\obj{CHOOSE}\,n\,k$, where $\obj{CHOOSE}$ is a function defined by 192 says that any base case and inductive case identifies a unique function, 202 Given the theorem \verb@prim_rec@, the builtin function 203 \verb@prove_rec_fn_exists@ can prove that there is a function that satisfies 218 easy to prove there is a function which satisfies the original three 359 which can be coded as the \ML{} function \verb@SPEC_EQ@: 471 Hilbert's $\epsilon$-operator to specify a function \verb@Id@ such that 474 is unique. The first step is to prove that there exists a function \verb@Id@ 554 a function \verb@Inv@ so that, if \verb@Group plus@ holds, then the 555 element \verb@Inv plus a@ is an inverse of \verb@a@. The function [all...] |
/seL4-l4v-master/HOL4/Manual/Tutorial/binomial/ |
H A D | binomial.tex | 136 $\obj{CHOOSE}\,n\,k$, where $\obj{CHOOSE}$ is a function defined by 192 says that any base case and inductive case identifies a unique function, 202 Given the theorem \verb@prim_rec@, the builtin function 203 \verb@prove_rec_fn_exists@ can prove that there is a function that satisfies 218 easy to prove there is a function which satisfies the original three 359 which can be coded as the \ML{} function \verb@SPEC_EQ@: 471 Hilbert's $\epsilon$-operator to specify a function \verb@Id@ such that 474 is unique. The first step is to prove that there exists a function \verb@Id@ 554 a function \verb@Inv@ so that, if \verb@Group plus@ holds, then the 555 element \verb@Inv plus a@ is an inverse of \verb@a@. The function [all...] |
/seL4-l4v-master/HOL4/src/meson/test/ |
H A D | selftest.sml | 1682 (!Xf. function(Xf) ==> subclass(Xf,cross_product(universal_class,universal_class))) /\ 1683 (!Xf. function(Xf) ==> subclass(compose(Xf,inverse(Xf)),identity_relation)) /\ 1684 (!Xf. subclass(Xf,cross_product(universal_class,universal_class)) /\ subclass(compose(Xf,inverse(Xf)),identity_relation) ==> function(Xf)) /\ 1685 (!Xf X. function(Xf) /\ member(X,universal_class) ==> member(image(Xf,X),universal_class)) /\ 1689 (function(choice)) /\ 1691 (!Xf. one_to_one(Xf) ==> function(Xf)) /\ 1692 (!Xf. one_to_one(Xf) ==> function(inverse(Xf))) /\ 1693 (!Xf. function(inverse(Xf)) /\ function(Xf) ==> one_to_one(Xf)) /\ 1698 (!Xf. operation(Xf) ==> function(X [all...] |
/seL4-l4v-master/HOL4/Manual/Description/ |
H A D | HolBdd.tex | 110 In Version~1 there was a function, called 269 Initialisation is done with the ML function 309 The function 320 The function 333 using the function \t{stats} 393 The function \t{toBool} returns \t{true} on TRUE and \t{false} on FALSE. 421 dynamically. The function 430 The function 478 \Muddy{} provides a function for general purpose simultaneous 504 Variables can be renamed using the function \ [all...] |
/seL4-l4v-master/HOL4/src/1/ |
H A D | dep_rewrite.sml | 118 (* These take as argument a thm_tactic, a function which takes a *) 183 fun TACTIC_ERR{function,message} = 185 origin_function = function, 188 fun failwith function = 190 print_string ("Failure in dep_rewrite: "^function^"\n") 192 raise TACTIC_ERR{function = function,message = "Failure in dep_rewrite"}); 303 (* APPLY_IMP_THEN ttac th is a dependent rewriting function, *) 395 (* TAC_DEP turns a tactic into a dependent rewriting function. *) 405 (* DEP_TAC turns a dependent rewriting function int [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/ |
H A D | arm_compiler_demoScript.sml | 23 arm_progLib can be used. The compiler's top-level function is 53 The compiler expects def to be a function where variables have names 62 memory locations (m0,m1,m2,etc), f over function names, 80 restrictions regarding varaible names in function calls.) 155 the definition of the function, i.e. 340 (* TEST: function in-lining *) 423 Use the option "PushProcedure ([],0)" when the function to be compiled contains 450 Example: the function c1 (below) uses registers 11 and 12 as temporaries and 451 function c2 (also below) depends on the fact that the values in registers 11 474 (* So far we have required that procedure/function call [all...] |
/seL4-l4v-master/isabelle/src/Doc/Logics/document/ |
H A D | HOL.tex | 120 function types, is overloaded with arity {\tt(term,\thinspace 176 Where function types are involved, Isabelle's unification code does not 456 & range of a function \\[1ex] 570 avoid complications involving function types in unification. The isomorphisms 751 %definition, $f$ is the abstraction function and $A$ is the set of valid 864 \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function 882 rules. Reasoning about function composition (the operator~\sdx{o}) and the 955 {Chap.\ts\ref{chap:simplification}}), there is a special infix function 1150 \cdx{Suc} & $nat \To nat$ & & successor function\\ 1240 %define a higher-order function, w [all...] |
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/ |
H A D | HOL.tex | 120 function types, is overloaded with arity {\tt(term,\thinspace 176 Where function types are involved, Isabelle's unification code does not 456 & range of a function \\[1ex] 570 avoid complications involving function types in unification. The isomorphisms 751 %definition, $f$ is the abstraction function and $A$ is the set of valid 864 \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function 882 rules. Reasoning about function composition (the operator~\sdx{o}) and the 955 {Chap.\ts\ref{chap:simplification}}), there is a special infix function 1150 \cdx{Suc} & $nat \To nat$ & & successor function\\ 1240 %define a higher-order function, w [all...] |
/seL4-l4v-master/HOL4/Manual/Quick/ |
H A D | quick.tex | 29 \hol{TotalDefn}{Define} \var{term} & function definition \\ 219 \hol{Conv}{SKOLEM_CONV} & proves the existence of a Skolem function \\[4pt] 295 \hol{Lib}{time} \var{function} & measure how long a function application takes \\ 298 \hol{Count}{apply} \var{function} & returns the theorem count for a function application \\
|
/seL4-l4v-master/HOL4/examples/Crypto/TWOFISH/ |
H A D | twofishScript.sml | 6 bijective F function made up of four key-dependent 8-by-8-bit S-boxes, 235 (* function works in k stages. In each stage, the four bytes are each *) 287 (* The words of the expanded key are defined using the h function. For Ai *) 399 (* The function FF is a key-dependent permutation on 64-bit values *) 411 (*-------------Forward round used by the encrypting function-----------------*) 436 (*-------------Backward round used by the decrypting function----------------*)
|
/seL4-l4v-master/HOL4/examples/lambda/basics/ |
H A D | binderLib.sml | 57 to prove that such a function actually exists. The RHS of any 59 attempt a recursion that is not be justified. This function 458 ("Couldn't prove function with swap over range - \n\ 466 ("Couldn't prove function with swap over range - \n\ 492 ("Couldn't prove function with swap over range - \n\ 504 ("Couldn't prove function with swap over range - \n\
|
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | SmtLib.sml | 26 (* (HOL type, a function that maps the type to its SMT-LIB sort name) *) 58 (* (HOL term, a function that maps a pair (rator, rands) to an 319 (* SMT-LIB type and function names are uniformly generated as "tN" 359 arguments of base type, but not to arguments of function type; 364 offending function type to a fresh base type, and by abstracting 366 correct (abstracted) type. Note that the same function/operator
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | BackendIntermediateCode.sml | 184 | BICEval of (* Evaluate a function with an argument list. *) 186 function: backendIC, 212 | BICBeginLoop of (* Start of tail-recursive inline function. *) 215 | BICLoop of (backendIC * argumentType) list (* Jump back to start of tail-recursive function. *) 399 BICEval {function, argList, resultType} => 409 [ pretty function, PrettyBreak(1, 0), prettyArgType resultType, PrettyBreak(1, 0), prettyArgs ]
|
/seL4-l4v-master/HOL4/src/HolQbf/ |
H A D | QDimacs.sml | 80 (* auxiliary function to strip off quantifiers over Boolean variables *) 145 (* into a function that can be passed to 'read_qdimacs_file' as its *) 167 (* a function (i.e., the result only depends on its argument), and *)
|