/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | HolQbf.tex | 134 \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 D | dimacsTools.sml | 146 (* 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 D | PRETTYSIG.sml | 24 { 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 D | grammar.scala | 149 -o FILE output file name (default """ + default_output() + """)
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | export_codeLib.sml | 9 val _ = print ("Extracting machine code to file \"" ^ filename ^ "\", ") 84 (* write to text file *)
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | preface.tex | 33 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 D | export_codeLib.sml | 9 val _ = print ("Extracting machine code to file \"" ^ filename ^ "\", ") 73 (* write to text file *)
|
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | export_codeLib.sml | 9 val _ = print ("Extracting machine code to file \"" ^ filename ^ "\", ") 72 (* write to text file *)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/VSCode/src/ |
H A D | grammar.scala | 149 -o FILE output file name (default """ + default_output() + """)
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | preface.tex | 33 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 D | smlParallel.sml | 427 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 D | for_ndScript.sml | 7 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 D | kernel.mk | 7 # 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 D | mleDiophSynt.sml | 98 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 D | mleCombinSynt.sml | 128 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 D | tttUnfold.sml | 872 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 D | c_outputLib.sig | 12 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 D | Stokes.ml | 4 % The example proof in this file comes from the paper "Traces for Hardware %
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | CooperThms.sml | 6 (* Fix the grammar used by this file *)
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | HOLPP.sml | 6 * See file mosml/copyrght/copyrght.att for details.
|
/seL4-l4v-master/HOL4/tools/set_mtime/ |
H A D | set_mtime.sml | 14 \ Must provide file_to_change and >=1 other file to take mtime from\n"
|
/seL4-l4v-master/HOL4/developers/ |
H A D | prehol.sml | 114 {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 D | arm_evalLib.sig | 23 Note: the elf file must be generated with "arm-elf-as -EB ..." and
|
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/ |
H A D | imported_acl2Script.sml | 2 (* This file defines a type of s-expressions and various constants and *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/ |
H A D | BuildAll.sml | 22 to compile the basis and produce an object file. *)
|