Searched refs:filename (Results 1 - 25 of 99) sorted by relevance

1234

/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibTptp.sig15 (* Reading from a TPTP file in CNF/FOF format: pass in a filename *)
16 val read : {filename : string} -> formula
18 (* Writing to a TPTP file in CNF format: pass in a formula and filename *)
19 val write : {filename : string} -> formula -> unit
/seL4-l4v-10.1.1/l4v/misc/benchmark-isabelle/
H A Dbenchmark.py27 # Get the filename, and strip off the trailing ".thy".
28 filename = args[0]
29 if filename.endswith(".thy"):
30 filename = filename[:-4]
34 ['-r', '-q', '-f', '-e', 'use_thy \"%s\";' % filename, "Benchmark"], timeout=None)
41 header = "%s Benchmark Results" % filename
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A Dmetis.sml97 "special - filename.\n",
162 fun display_name filename =
164 else TextIO.print ("Problem: " ^ filename ^ "\n\n");
206 fun display_proof_start filename =
207 TextIO.print ("\nSZS output start CNFRefutation for " ^ filename ^ "\n");
229 val filename = "-" value
234 filename = filename}
237 fun display_proof_end filename =
238 TextIO.print ("SZS output end CNFRefutation for " ^ filename
353 val filename = mkTptpFilename inc value
[all...]
H A Dproblems2tptp.sml46 val filename = name ^ ".tptp" value
47 val filename = value
49 NONE => filename
50 | SOME dir => addSlash dir ^ filename
91 filename = filename}
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A Dmetis.sml97 "special - filename.\n",
162 fun display_name filename =
164 else TextIO.print ("Problem: " ^ filename ^ "\n\n");
206 fun display_proof_start filename =
207 TextIO.print ("\nSZS output start CNFRefutation for " ^ filename ^ "\n");
229 val filename = "-" value
234 filename = filename}
237 fun display_proof_end filename =
238 TextIO.print ("SZS output end CNFRefutation for " ^ filename
353 val filename = mkTptpFilename inc value
[all...]
H A Dproblems2tptp.sml46 val filename = name ^ ".tptp" value
47 val filename = value
49 NONE => filename
50 | SOME dir => addSlash dir ^ filename
91 filename = filename}
/seL4-l4v-10.1.1/HOL4/tools/
H A Dunquote-init.sml30 val filename = FileSys.tmpName()^".hol" value
32 if Process.isSuccess (unquote_to s filename) then
33 (Meta.use filename; FileSys.remove filename)
34 handle e => (FileSys.remove filename handle _ => (); raise e)
/seL4-l4v-10.1.1/HOL4/examples/elliptic/c_output/
H A Dc_outputLib.sig6 translate_to_c dirname filename defs rewrites main_func tests
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.
14 filename-test.c contains code for testing. It checks for the tests passed in tests automatically and afterwards provides interactive for
/seL4-l4v-10.1.1/l4v/spec/cspec/
H A Dmk_umm_types.py27 self.filename = tempfile.mkdtemp()
29 return self.filename
33 shutil.rmtree(self.filename)
41 help="output filename")
/seL4-l4v-10.1.1/HOL4/examples/real-to-float/
H A DdaisyLib.sml10 val filename = output_filename ^ ".scala" value
11 val f = TextIO.openOut filename
14 val _ = OS.Process.system("cd "^path^" && ./daisy " ^ filename ^ " > /dev/null")
/seL4-l4v-10.1.1/HOL4/src/1/
H A DScaledTests.sml20 fun test_upto {f,ntrials,max_size,filename} = let
21 val outstr = TextIO.openOut filename
/seL4-l4v-10.1.1/HOL4/examples/acl2/lisp/
H A Dpkg-alist-to-alist.lisp3 ; Evaluation of (print-kpa lisp-filename ml-filename) prints to the indicated
73 (defun print-ml-string-triples-and-known-pkgs (triples pkg-names filename ctx
77 (open-output-channel filename :character state)
81 filename))
105 (defun print-imports-alist (filename ctx state)
108 (open-output-channel filename :object state)
112 filename))
120 (defmacro print-kpa (lisp-filename ml-filename)
[all...]
/seL4-l4v-10.1.1/HOL4/help/src-sml/
H A DParsspec.sml18 fun parseSpec filename is = let
21 TextIO.output(TextIO.stdErr, filename^":"^Int.toString (i+1) ^ ": " ^ s ^ "\n")
68 val filename = OS.Path.joinDirFile {dir=dir, file = basefile} value
71 val is = TextIO.openIn filename
72 val specs = case parseSpec filename is
87 (* To parse the signature of unit `filename' and prepend the
91 fun processfile stoplist dir (filename, res) =
92 let val {base, ext} = OS.Path.splitBaseExt filename
H A DMyDatabase.sml28 fun writebase(filename, db) =
29 let val os = BasicIO.open_out_bin filename
32 fun readbase filename =
45 val is = open_in_bin filename
/seL4-l4v-10.1.1/HOL4/src/TeX/
H A Dmkmkcline.sml7 " [-o filename] [-static] [theory1 theory2 ...]\n");
/seL4-l4v-10.1.1/HOL4/tools-poly/poly/
H A DMosml.sml10 fun write filename s =
12 val os = openOut filename
14 fun read filename =
16 val is = openIn filename
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/scripts/
H A Dmlpp95 my $filename = shift @_;
99 print STDOUT "(*#line 0.0 \"$filename\"*)\n";
102 open my $INPUT, "$filename" or
103 die "mlpp: couldn't open $filename: $!\n";
112 or warn "no terminating newline in $filename\nline = '$line'\n";
173 if ($use_filename !~ /^\// && $filename =~ /^(.*)\//) {
178 print STDOUT "(*#line $line_num.0 \"$filename\"*)\n";
254 my $filename = shift @ARGV;
255 process_file $filename;
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/scripts/
H A Dmlpp95 my $filename = shift @_;
99 print STDOUT "(*#line 0.0 \"$filename\"*)\n";
102 open my $INPUT, "$filename" or
103 die "mlpp: couldn't open $filename: $!\n";
112 or warn "no terminating newline in $filename\nline = '$line'\n";
173 if ($use_filename !~ /^\// && $filename =~ /^(.*)\//) {
178 print STDOUT "(*#line $line_num.0 \"$filename\"*)\n";
254 my $filename = shift @ARGV;
255 process_file $filename;
/seL4-l4v-10.1.1/l4v/tools/autocorres/tools/
H A Drelease.py29 self.filename = tempfile.mkdtemp()
30 return self.filename
34 shutil.rmtree(self.filename)
51 for filename in fnmatch.filter(filenames, pattern):
52 results.append(os.path.join(root, filename))
55 def read_manifest(filename, base):
68 with open(filename) as f:
114 default=None, help='Output filename. Defaults to "autocorres-<VERSION>.tar.gz".')
130 # Setup output filename if the user used the default.
287 def inplace_replace_string(filename, old_strin
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A DarmLib.sig56 arm_assemble_from_file <filename>
61 print_arm_assemble_from_file <start address> <filename>
71 arm_parse_from_file <filename>
79 arm_steps_from_file <options> <filename>
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DHoldep.sml133 fun read {assumes, includes, srcext, objext, filename} = let
134 val mentions = uqfname_holdep (addExt filename srcext)
135 val curr_dir = Path.dir filename
137 val (targetname, res0) = beginentry objext (manglefilename filename)
145 end handle Holdep_Error s => raise Holdep_Error (filename ^ ": " ^ s)
148 fun processfile {assumes, includes, fname = filename, diag} =
150 val {base, ext} = Path.splitBaseExt filename
154 filename = base, includes = includes}
156 filename = base, includes = includes}
157 | _ => {tgt = filename, dep
[all...]
/seL4-l4v-10.1.1/l4v/misc/regression/
H A Dtestspec.py123 def validate_xml(doc, filename):
133 "%s does not validate against DTD:\n\n" % filename
136 def parse_testsuite_xml(filename):
139 doc = etree.parse(filename, parser=parser)
142 validate_xml(doc, filename)
145 env = TestEnv(os.path.dirname(filename))
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A Ddecompile.py9 parser.add_argument('filename', metavar='filename', type=str,
10 help='base of filename, e.g. loop for loop.elf.txt')
48 elf = os.path.abspath(args.filename)
49 output_file = os.path.abspath(args.filename + '_output.txt')
/seL4-l4v-10.1.1/seL4/tools/
H A Dumm.py116 def print_graph(filename, out_file):
117 mp = build_types(filename)
/seL4-l4v-10.1.1/HOL4/examples/elliptic/
H A DStream.sig88 val to_textfile : {filename : string} -> string stream -> unit
90 val from_textfile : {filename : string} -> string stream (* line by line *)

Completed in 215 milliseconds

1234