/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibTptp.sig | 15 (* 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 D | benchmark.py | 27 # 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 D | metis.sml | 97 "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 D | problems2tptp.sml | 46 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 D | metis.sml | 97 "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 D | problems2tptp.sml | 46 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 D | unquote-init.sml | 30 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 D | c_outputLib.sig | 6 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 D | mk_umm_types.py | 27 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 D | daisyLib.sml | 10 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 D | ScaledTests.sml | 20 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 D | pkg-alist-to-alist.lisp | 3 ; 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 D | Parsspec.sml | 18 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 D | MyDatabase.sml | 28 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 D | mkmkcline.sml | 7 " [-o filename] [-static] [theory1 theory2 ...]\n");
|
/seL4-l4v-10.1.1/HOL4/tools-poly/poly/ |
H A D | Mosml.sml | 10 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 D | mlpp | 95 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 D | mlpp | 95 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 D | release.py | 29 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 D | armLib.sig | 56 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 D | Holdep.sml | 133 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 D | testspec.py | 123 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 D | decompile.py | 9 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 D | umm.py | 116 def print_graph(filename, out_file): 117 mp = build_types(filename)
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
H A D | Stream.sig | 88 val to_textfile : {filename : string} -> string stream -> unit 90 val from_textfile : {filename : string} -> string stream (* line by line *)
|