Searched refs:src (Results 176 - 200 of 331) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/test/
H A DregexTest.sml27 (* /opt/hol_bir/src/tfl/examples/regexp.{naive/deriv} - in the end *)
/seL4-l4v-10.1.1/HOL4/src/Boolify/src/
H A DPreListEncode.sml7 val () = loadPath := ["../../list/src"] @ !loadPath;
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DUnwind.sig65 * use "3/simplifier/src/UNWIND.sml";
/seL4-l4v-10.1.1/HOL4/tools/
H A Dwin-config.sml53 val _ = FileSys.mkDir (fullPath [holdir, "src", "0"]) handle _ => ()
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/tools/
H A DcongToolsLib.sml8 loadPath := (concat home_dir "src/tools") :: !loadPath;
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DByte.sml51 Word8ArraySlice.copyVec{src=slice, dst=array, di=i}
H A DArray2.sml129 fun copy {src as {base, row, col, ...}, dst, dst_row, dst_col} =
132 val (nrows, ncols) = getRegion src
159 else (* We have to be careful if dst = src and the regions
H A DBoolArray.sml145 fun move_bits(src: Bootstrap.byteVector, dest: Bootstrap.byteVector, dest_off, len, last_bits) =
154 val newbyte = last orb (RunCall.loadByteFromImmutable(src, byte) << dest_bit)
167 val nextsrc = RunCall.loadByteFromImmutable(src, byte);
418 fun copy {src=Array (slen, s), dst=Array (dlen, d), di: int} =
433 (* fun copy {src as Array (slen, s), dst as Array (dlen, d), di: int} =
464 fun copyVec {src=Vector(slen, s), dst=Array (dlen, d), di: int} =
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/
H A Dbvec.c89 PROTO {* bvec bvec_copy(bvec src) *}
90 DESCR {* Returns a copy of {\tt src}. The result is reference counted. *}
93 bvec bvec_copy(bvec src) argument
98 if (src.bitnum == 0)
104 dst = bvec_build(src.bitnum,0);
106 for (n=0 ; n<src.bitnum ; n++)
107 dst.bitvec[n] = bdd_addref( src.bitvec[n] );
108 dst.bitnum = src.bitnum;
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/examples/
H A Dltl2omega.sml5 loadPath := (concat home_dir "src/deep_embeddings") ::
6 (concat home_dir "src/translations") ::
7 (concat home_dir "src/tools") ::
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibArbnum.sml9 fun copyVec' {di,dst,len,src,si} = let
10 val v = VectorSlice.vector(VectorSlice.slice(src,si,len));
12 Array.copyVec {di = di, dst = dst, src = v}
298 val _ = copyVec' {di=j, dst=u, len=NONE, src=newu_v, si=0}
312 copyVec' {di = j, dst = u, len = NONE, src = newu_v, si = 0}
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/
H A DHolSat.tex117 For details, see the source file \t{src/taut/tautLib.sml} which contains comprehensive comments. Note however that the extra functionality in {{\tt tautLib}} was not engineered for very large problems and can become a performance bottleneck.
121 The ZChaff SAT solver has a proof production mode and is supported by {\tt{HolSatLib}}. However, the ZChaff end user license is not compatible with the \HOL{} license, so we are unable to distribute it with \HOL{}. If you wish to use ZChaff, download and unpack it in the directory {\tt src/HolSat/sat\_solvers/} under the main \HOL{} directory, and compile it with proof production mode enabled (which is not the default). This should create a binary {\tt zchaff} in the directory {\tt src/HolSat/sat\_solvers/zchaff/}. ZChaff can now be used as the external proof engine instead of MiniSat, by using the HolSatLib functions described above, prefixed with a ``{\tt Z}'', e.g., {\tt ZSAT\_PROVE}.
143 The name of a proof trace file. Overrides \texttt{solver} if set. The file must be in the native format of {\tt{HolSatLib}}, and must correspond to a proof for \texttt{infile}, which must also be set. The included version of MiniSat has been modified to produce proofs in the native format, and ZChaff proofs are translated to this format using the included proof translator \texttt{src/HolSat/sat\_solvers/zc2hs} (type \texttt{zc2hs -h} for usage help). \texttt{zc2hs} is used internally by \texttt{ZSAT\_PROVE} etc.
152 A special value \texttt{base\_config~:~sat\_config} is provided for which the term is \texttt{T}, the solver is MiniSat, the options are unset, the CNF flag is false and the proof flag is true. This value can be inspected and modified using getter and setter functions provided in \texttt{src/HolSat/satConfig.sig}. For example, to invoke ZChaff (assuming it is installed), on a file \texttt{unsat.cnf} containing an unsatisfiable problem, we do:
/seL4-l4v-10.1.1/HOL4/src/Boolify/test/
H A Ddatatypes.sml9 ["../../../../ptr/hol/src/datatype/", "../../../../ptr/hol/src/list/src",
10 "../../../../ptr/hol/src/tfl/src", "../../../../ptr/hol/src/Boolify/src"] @
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A DannotatedIR.sml233 fun extract (Assem.OPER {oper = (Assem.BL,_,_), dst = dList, src = sList, jump = jp}) = (dList, sList, jp);
246 | Assem.OPER {oper = (Assem.BL,_,_), dst = dList, src = sList, jump = jp} =>
285 val (Assem.OPER {src = rec_argL,...}) = #instr ((#3(G.context(bal_node,cfg))):CFG.node);
286 val rec_args_pass_ir = STM (List.map (fn (dexp,sexp) => {oper = mmov, src = [sexp], dst = [dexp]})
314 fun is_dummy_inst ({oper = mmov, src = sList, dst = dList}) =
316 | is_dummy_inst (stm as {oper = op', src = sList, dst = dList}) =
431 fun one_stm_modified_regs ({oper = op1, dst = dlist, src = slist}) =
659 val defs = List.map (fn (name, (flag,src,anf,cps)) => src) env;
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttInfix.sml90 Infixity from src/thm/Overlay.sml.
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/
H A Dpreface.tex53 Isabelle (see the directory \texttt{src}). They are also available for
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/
H A Dpreface.tex53 Isabelle (see the directory \texttt{src}). They are also available for
/seL4-l4v-10.1.1/HOL4/examples/computability/
H A DgoedelCodeScript.sml3 (* numpairTheory in src/num/extra_theories. *)
155 (* src/num/extra_theories/numpairScript. *)
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DannotatedIR.sml229 | Assem.OPER {oper = (Assem.BL,_,_), dst = dList, src = sList, jump = jp} =>
268 val (Assem.OPER {src = rec_argL,...}) = #instr ((#3(G.context(bal_node,cfg))):CFG.node);
269 val rec_args_pass_ir = STM (List.map (fn (dexp,sexp) => {oper = mmov, src = [sexp], dst = [dexp]})
297 fun is_dummy_inst ({oper = mmov, src = sList, dst = dList}) =
299 | is_dummy_inst (stm as {oper = op', src = sList, dst = dList}) =
414 fun one_stm_modified_regs ({oper = op1, dst = dlist, src = slist}) =
602 val defs = List.map (fn (name, (flag,src,anf,cps)) => src) env;
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A DannotatedIR.sml229 | Assem.OPER {oper = (Assem.BL,_,_), dst = dList, src = sList, jump = jp} =>
268 val (Assem.OPER {src = rec_argL,...}) = #instr ((#3(G.context(bal_node,cfg))):CFG.node);
269 val rec_args_pass_ir = STM (List.map (fn (dexp,sexp) => {oper = mmov, src = [sexp], dst = [dexp]})
297 fun is_dummy_inst ({oper = mmov, src = sList, dst = dList}) =
299 | is_dummy_inst (stm as {oper = op', src = sList, dst = dList}) =
414 fun one_stm_modified_regs ({oper = op1, dst = dlist, src = slist}) =
602 val defs = List.map (fn (name, (flag,src,anf,cps)) => src) env;
/seL4-l4v-10.1.1/HOL4/src/pfl/examples/
H A Dzero.sml8 use (HOLDIR^"/src/pfl/defchoose");
9 use (HOLDIR^"/src/pfl/tactics.sml");
/seL4-l4v-10.1.1/HOL4/tools/unicode-grep/
H A Dugrep.sml309 echo "If no directories given, run in HOL's src directory"
318 LC_ALL=C eval $cmd $(dirname $0)/../src/
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dx86_decoderScript.sml144 decode_Xdest_src g dest src =
145 if MEM src ["r32";"r8"] then
146 Xrm_r (decode_Xrm32 g dest) (decode_Xr32 g src)
147 else if MEM src ["r/m32";"r/m8"] then
148 Xr_rm (decode_Xr32 g dest) (decode_Xrm32 g src)
149 else if src = "m" then
150 Xr_rm (decode_Xr32 g dest) (decode_Xrm32 g src)
152 Xrm_i (decode_Xrm32 g dest) (decode_Xconst src g)`;
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/
H A Dx64_decoderScript.sml183 decode_Zdest_src g dest src =
184 if MEM src ["r64";"r32";"r16";"r8"] then
185 Zrm_r (decode_Zrm32 g dest) (decode_Zr32 g src)
186 else if MEM src ["r/m64";"r/m32";"r/m16";"r/m8"] then
187 Zr_rm (decode_Zr32 g dest) (decode_Zrm32 g src)
188 else if src = "m" then
189 Zr_rm (decode_Zr32 g dest) (decode_Zrm32 g src)
191 Zrm_i (decode_Zrm32 g dest) (decode_Zconst src g)`;
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/
H A DholfootSyntax.sml6 loadPath := (Globals.HOLDIR ^ "/examples/separationLogic/src") ::
7 (Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot") ::

Completed in 141 milliseconds

1234567891011>>