Searched refs:file (Results 251 - 275 of 645) sorted by relevance

<<11121314151617181920>>

/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A DHolQbf.tex134 \paragraph{Support for the QDIMACS file format}
136 The QDIMACS standard defines an input file format for QBF solvers.
143 \ml{QDimacs.write\_qdimacs\_file path $\phi$} creates a QDIMACS file
147 variable index (a positive integer) used in the QDIMACS file.
150 file (with name \ml{path}) and returns the encoded QBF as a \HOL{}
164 {\tt /tmp} on Unix machines. The actual file names are generated at
/seL4-l4v-master/HOL4/src/HolSat/
H A DdimacsTools.sml146 (* FIXME: if is_cnf, then assume the .cnf file is already present, and use
232 ** Refererence containing name of temporary file used
241 ** file into the temporary directory.
242 ** the name of the temporary file (without extension ".cnf") is returned,
252 (* so we don't waste time creating empty cnf file *)
279 (*Write out DIMACS file and build svm and sva*)
295 ** reads a DIMACS file called filename and returns
296 ** a term in CNF in which each number n in the DIMACS file
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DPRETTYSIG.sml24 { file: string, startLine: FixedInt.int, startPosition: FixedInt.int, endLine: FixedInt.int, endPosition: FixedInt.int } -> context
42 { file: string, startLine: int, startPosition: int, endLine: int, endPosition: int }
/seL4-l4v-master/isabelle/src/Tools/VSCode/src/
H A Dgrammar.scala149 -o FILE output file name (default """ + default_output() + """)
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dexport_codeLib.sml9 val _ = print ("Extracting machine code to file \"" ^ filename ^ "\", ")
84 (* write to text file *)
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/
H A Dpreface.tex33 annotated source file is run, typesetting the theory
34 in the form of a \LaTeX\ source file. This book is derived almost entirely
/seL4-l4v-master/HOL4/examples/machine-code/just-in-time/
H A Dexport_codeLib.sml9 val _ = print ("Extracting machine code to file \"" ^ filename ^ "\", ")
73 (* write to text file *)
/seL4-l4v-master/HOL4/examples/machine-code/lisp/
H A Dexport_codeLib.sml9 val _ = print ("Extracting machine code to file \"" ^ filename ^ "\", ")
72 (* write to text file *)
/seL4-l4v-master/l4v/isabelle/src/Tools/VSCode/src/
H A Dgrammar.scala149 -o FILE output file name (default """ + default_output() + """)
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/
H A Dpreface.tex33 annotated source file is run, typesetting the theory
34 in the form of a \LaTeX\ source file. This book is derived almost entirely
/seL4-l4v-master/HOL4/src/AI/sml_inspection/
H A DsmlParallel.sml427 write_arg = let fun f file arg = writel file [its arg] in f end,
428 read_arg = let fun f file =
429 string_to_int (singleton_of_list (readl file)) in f end,
430 write_result = let fun f file r = writel file [its r] in f end,
431 read_result = let fun f file = string_to_int (hd (readl_rm file)) in f end
/seL4-l4v-master/HOL4/examples/fun-op-sem/for/
H A Dfor_ndScript.sml7 This file defines a FOR language that's very similar to the language
31 - Getchar returns -1 to signal the end of file. *)
/seL4-l4v-master/l4v/spec/cspec/c/
H A Dkernel.mk7 # This file contains parts of the l4v C kernel build that are reused by binary verification.
101 # This step also generates a large number of files, so we create a dummy file
/seL4-l4v-master/HOL4/examples/AI_tasks/
H A DmleDiophSynt.sml98 fun write_boardl file boardl =
100 writel (file ^ "_poly") (map poly_to_string l1);
101 writel (file ^ "_graph") (map graph_to_string l2);
102 writel (file ^ "_timer") (map its l3)
105 fun read_boardl file =
107 val l1 = map string_to_poly (readl_empty (file ^ "_poly"))
108 val l2 = map string_to_graph (readl (file ^ "_graph"))
109 val l3 = map string_to_int (readl (file ^ "_timer"))
H A DmleCombinSynt.sml128 fun write_boardl file boardl =
132 export_terml (file ^ "_witness") (map combin_to_cterm l1);
133 export_terml (file ^ "_headnf") (map combin_to_cterm l2);
134 writel (file ^ "_timer") (map its l3)
137 fun read_boardl file =
139 val l1 = map cterm_to_combin (import_terml (file ^ "_witness"))
140 val l2 = map cterm_to_combin (import_terml (file ^ "_headnf"))
141 val l3 = map string_to_int (readl (file ^ "_timer"))
/seL4-l4v-master/HOL4/src/tactictoe/src/
H A DtttUnfold.sml872 fun extract_thy file =
874 val suffix = last (String.tokens (fn x => x = #"/") file)
896 fun write_sl file sl =
897 let val oc = TextIO.openOut file in
918 "(* This file was modifed by TacticToe. *)",
974 fun sketch_wrap thy file =
976 val s1 = QFRead.inputFile file
990 fun tttsml_of file = OS.Path.base file ^ "_ttt.sml"
1052 fun save_file file
[all...]
/seL4-l4v-master/HOL4/examples/elliptic/c_output/
H A Dc_outputLib.sig12 translate_to_c generates 3 files: filename.h, filename.c and filename-test.c in the directory dirname. The directory name must end with a "/". The file filename.c contains the main function definitions, filename.h the headers.
/seL4-l4v-master/HOL4/examples/hardware/hol88/
H A DStokes.ml4 % The example proof in this file comes from the paper "Traces for Hardware %
/seL4-l4v-master/HOL4/src/integer/
H A DCooperThms.sml6 (* Fix the grammar used by this file *)
/seL4-l4v-master/HOL4/src/portableML/
H A DHOLPP.sml6 * See file mosml/copyrght/copyrght.att for details.
/seL4-l4v-master/HOL4/tools/set_mtime/
H A Dset_mtime.sml14 \ Must provide file_to_change and >=1 other file to take mtime from\n"
/seL4-l4v-master/HOL4/developers/
H A Dprehol.sml114 {file = "help/Docfiles/HOL.help",
223 fun has_dq file =
225 val istrm = TextIO.openIn file
248 ("Failed to translate file: "^s^"\n"));
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/
H A Darm_evalLib.sig23 Note: the elf file must be generated with "arm-elf-as -EB ..." and
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/
H A Dimported_acl2Script.sml2 (* This file defines a type of s-expressions and various constants and *)
/seL4-l4v-master/HOL4/polyml/mlsource/
H A DBuildAll.sml22 to compile the basis and produce an object file. *)

Completed in 200 milliseconds

<<11121314151617181920>>