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

12345

/seL4-l4v-master/HOL4/src/portableML/mosml/
H A DSHA1_ML.sig4 val sha1_file : {filename:string} -> string
H A DSHA1_ML.sml4 fun sha1_file {filename} =
6 case Mosml.run "/usr/bin/shasum" [Systeml.protect filename] "" of
8 | Mosml.Failure _ => raise Fail ("Calling shasum {filename=\"" ^ filename ^ "} failed")
/seL4-l4v-master/HOL4/src/portableML/
H A DSHA1.sig6 sha1_file : {filename:string} -> string
/seL4-l4v-master/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-master/l4v/misc/benchmark-isabelle/
H A Dbenchmark.py24 # Get the filename, and strip off the trailing ".thy".
25 filename = args[0]
26 if filename.endswith(".thy"):
27 filename = filename[:-4]
31 ['-r', '-q', '-f', '-e', 'use_thy \"%s\";' % filename, "Benchmark"], timeout=None)
38 header = "%s Benchmark Results" % filename
/seL4-l4v-master/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-master/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-master/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-master/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-master/l4v/spec/cspec/
H A Dmk_umm_types.py25 self.filename = tempfile.mkdtemp()
27 return self.filename
31 shutil.rmtree(self.filename)
40 help="output filename")
/seL4-l4v-master/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-master/HOL4/src/1/
H A DScaledTests.sml20 fun test_upto {f,ntrials,max_size,filename} = let
21 val outstr = TextIO.openOut filename
/seL4-l4v-master/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
/seL4-l4v-master/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-master/HOL4/src/TeX/
H A Dmkmkcline.sml7 " [-o filename] [-static] [theory1 theory2 ...]\n");
/seL4-l4v-master/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-master/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-master/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-master/l4v/tools/autocorres/tools/
H A Drelease.py27 self.filename = tempfile.mkdtemp()
28 return self.filename
32 shutil.rmtree(self.filename)
51 for filename in fnmatch.filter(filenames, pattern):
52 results.append(os.path.join(root, filename))
56 def read_manifest(filename, base):
69 with open(filename) as f:
117 default=None, help='Output filename. Defaults to "autocorres-<VERSION>.tar.gz".')
133 # Setup output filename if the user used the default.
287 def inplace_replace_string(filename, old_strin
[all...]
/seL4-l4v-master/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-master/HOL4/src/postkernel/
H A DTheoryReader.sig9 (* [load_thydata thyname fname] loads the filename and makes the appropriate
/seL4-l4v-master/HOL4/tools/Holmake/
H A DHoldep.sml131 fun read {assumes, includes, srcext, objext, filename} = let
132 val mentions = uqfname_holdep (addExt filename srcext)
133 val curr_dir = Path.dir filename
135 val (targetname, res0) = beginentry objext (manglefilename filename)
143 end handle Holdep_Error s => raise Holdep_Error (filename ^ ": " ^ s)
146 fun processfile {assumes, includes, fname = filename, diag} =
148 val {base, ext} = Path.splitBaseExt filename
152 filename = base, includes = includes}
154 filename = base, includes = includes}
155 | _ => {tgt = filename, dep
[all...]
/seL4-l4v-master/l4v/misc/regression/
H A Dtestspec.py131 def validate_xml(doc, filename):
141 "%s does not validate against DTD:\n\n" % filename
145 def parse_testsuite_xml(filename):
148 doc = etree.parse(filename, parser=parser)
151 validate_xml(doc, filename)
154 env = TestEnv(os.path.dirname(filename))

Completed in 104 milliseconds

12345