/seL4-l4v-master/HOL4/src/portableML/mosml/ |
H A D | SHA1_ML.sig | 4 val sha1_file : {filename:string} -> string
|
H A D | SHA1_ML.sml | 4 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 D | SHA1.sig | 6 sha1_file : {filename:string} -> string
|
/seL4-l4v-master/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-master/l4v/misc/benchmark-isabelle/ |
H A D | benchmark.py | 24 # 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 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-master/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-master/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-master/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-master/l4v/spec/cspec/ |
H A D | mk_umm_types.py | 25 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 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-master/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-master/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
|
/seL4-l4v-master/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-master/HOL4/src/TeX/ |
H A D | mkmkcline.sml | 7 " [-o filename] [-static] [theory1 theory2 ...]\n");
|
/seL4-l4v-master/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-master/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-master/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-master/l4v/tools/autocorres/tools/ |
H A D | release.py | 27 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 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-master/HOL4/src/postkernel/ |
H A D | TheoryReader.sig | 9 (* [load_thydata thyname fname] loads the filename and makes the appropriate
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Holdep.sml | 131 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 D | testspec.py | 131 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))
|