Searched refs:read (Results 1 - 25 of 348) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/1/theory_tests/
H A Dreadthm1Script.sml5 val read = save_thm("read", TRUTH); value
H A Dreadthm2Script.sml7 val next_thm = save_thm("next_thm", CONJ read read)
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DHM_SimpleBuffer.sig4 val mkBuffer : unit -> {push : string -> unit, read : unit -> string,
H A DHM_SimpleBuffer.sml7 fun read () = let function
15 {push = push, read = read, reset = reset}
H A DQFRead.sml8 fun exhaust_lexer (read, close) =
11 case read () of
23 val read = QuoteFilter.makeLexer (fn n => TextIO.input instrm) qstate value
25 (read, (fn () => TextIO.closeIn instrm))
33 val read = QuoteFilter.makeLexer str_read qstate value
35 (read, (fn () => ()))
41 val read = QuoteFilter.makeLexer (fn n => TextIO.input strm) qstate value
43 (read, (fn () => ()))
50 fun mkReaderEOF (read, close) = let
55 fun pull () = (s := read(); s
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A DfunCallScript.sml299 (w2n (read st SP) <= w2n (read st FP) - (12 + m)) /\
300 locate_ge (read st FP) (12 + m)`;
320 Q.ABBREV_TAC `x = read st SP` THEN
321 Cases_on `w2n (read st FP) <= n + w2n (x:word32)` THEN
335 `!st l m k. locate_ge (read st SP) (k + LENGTH l) /\
340 (isM (w2n (read st SP) - k - PRE (LENGTH l) + i)) = st '' (EL i l))`,
347 `locate_ge (read st1 SP) (LENGTH l) /\ standard_frame st1 m /\
348 (w2n (regs ' 13) - k = w2n (read st1 SP))` by ALL_TAC THENL [
370 `!st n. i > w2n (read s
[all...]
H A DbigInstScript.sml49 (reade st (isR r) = read st (REG r)) /\
51 (reade st (isV k) = read st (MEM (fp, NEG k))) /\
70 (addr_of st (isV v) = w2n (read st FP) - v)`;
315 Q.ABBREV_TAC `y = w2n (read st FP)` THEN
394 ((run_cfl (BLK (push_one e)) st = st |# (isM (w2n (read st SP)), st '' e) |# (isR sp, st '' (isR sp) - 1w)) \/
396 st |# (isM (w2n (read st SP)), st '' e) |# (isR 9, v) |# (isR sp, st '' (isR sp) - 1w)))
422 ~(addr_in_range st e (w2n (read st SP), w2n (read st SP) - k)) /\ valid_exp_1 e`;
426 `!st h l. valid_exp_3 h /\ locate_ge (read st SP) (SUC (LENGTH l))
429 locate_ge (read st
[all...]
H A DpreARMScript.sml174 read (regs,mem) (exp:EXP) =
188 ` (read (regs,mem) (MEM (r,POS k)) = mem ' (w2n (regs ' r) + k)) /\
189 (read (regs,mem) (MEM (r,NEG k)) = mem ' (w2n (regs ' r) - k)) /\
190 (read (regs,mem) (NCONST i) = n2w i) /\
191 (read (regs,mem) (WCONST w) = w) /\
192 (read (regs,mem) (REG r) = regs ' r)`,
242 MOV -> (cpsr, write s (THE dst) (read s (HD src)))
250 (* We must read values from the original state instead of the updated state *)
251 (cpsr, FST (FOLDL (\(s1,i) reg. (write s1 reg (read s (MEM(r,POS(i+1)))), i+1)) (s,0) src))
254 (cpsr, write (FST (FOLDL (\(s1,i) reg. (write s1 reg (read
[all...]
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DGrammarAncestry.sml10 val (write, read) =
12 read = Lib.K Coding.StringData.decodel,
19 | SOME t => case read t of
/seL4-l4v-10.1.1/HOL4/src/datatype/theory_tests/
H A DmonofldBScript.sml7 val (write, read) = let
27 val msg = read()
/seL4-l4v-10.1.1/HOL4/src/Boolify/src/
H A DPreListEncode.sml28 val bool_info = Option.valOf (TypeBase.read {Thy= "min", Tyop="bool"});
37 val prod_info = Option.valOf (TypeBase.read {Thy="pair", Tyop="prod"});
47 val sum_info = Option.valOf (TypeBase.read {Thy = "sum", Tyop = "sum"});
58 Option.valOf (TypeBase.read {Thy = "option", Tyop = "option"});
68 val list_info = Option.valOf (TypeBase.read {Thy = "list", Tyop = "list"});
78 val num_info = Option.valOf (TypeBase.read {Thy = "num", Tyop = "num"});
87 val one_info = Option.valOf (TypeBase.read {Thy = "one", Tyop = "one"});
/seL4-l4v-10.1.1/HOL4/src/num/theories/
H A DbasicSize.sml18 val bool_info = Option.valOf (TypeBase.read {Thy="min", Tyop = "bool"});
32 (Option.valOf (TypeBase.read {Tyop="prod", Thy="pair"}))
40 (Option.valOf(TypeBase.read {Tyop="sum", Thy="sum"}));
46 val one_info = Option.valOf (TypeBase.read {Tyop="one",Thy="one"})
58 val option_info = Option.valOf (TypeBase.read {Tyop="option", Thy="option"})
/seL4-l4v-10.1.1/isabelle/src/Pure/System/
H A Dnuma.scala21 def read(s: String): List[Int] =
29 space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/
H A Dnuma.scala21 def read(s: String): List[Int] =
29 space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
/seL4-l4v-10.1.1/isabelle/src/Pure/Admin/
H A Dnews.scala27 HTML.source(Symbol.decode(File.read(Path.explode("~~/NEWS"))))))
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/
H A Dnews.scala27 HTML.source(Symbol.decode(File.read(Path.explode("~~/NEWS"))))))
/seL4-l4v-10.1.1/l4v/misc/filemerge/
H A Dunicode.py35 data = f.read().decode('utf-8')
H A Dxsymbol.py35 data = f.read()
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A DpreARMScript.sml182 read (regs,mem) (exp:EXP) =
196 ` (read (regs,mem) (MEM (r,POS k)) = mem ' (MEM_ADDR (regs ' (n2w r)) + (n2w k))) /\
197 (read (regs,mem) (MEM (r,NEG k)) = mem ' (MEM_ADDR (regs ' (n2w r)) - (n2w k))) /\
198 (read (regs,mem) (NCONST i) = n2w i) /\
199 (read (regs,mem) (WCONST w) = w) /\
200 (read (regs,mem) (REG r) = regs ' (n2w r)) /\
201 (read (regs,mem) (MEM (r,INR)) = ARB)`,
254 MOV => (cpsr, write s (THE dst) (read s (HD src)))
262 (* We must read values from the original state instead of the updated state *)
263 (cpsr, FST (FOLDL (\(s1,i) reg. (write s1 reg (read
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DpreARMScript.sml178 read (regs,mem) (exp:EXP) =
192 ` (read (regs,mem) (MEM (r,POS k)) = mem ' (ADDR30 (regs ' (n2w r)) + (n2w k))) /\
193 (read (regs,mem) (MEM (r,NEG k)) = mem ' (ADDR30 (regs ' (n2w r)) - (n2w k))) /\
194 (read (regs,mem) (NCONST i) = n2w i) /\
195 (read (regs,mem) (WCONST w) = w) /\
196 (read (regs,mem) (REG r) = regs ' (n2w r)) /\
197 (read (regs,mem) (MEM (r,INR)) = ARB)`,
250 MOV -> (cpsr, write s (THE dst) (read s (HD src)))
258 (* We must read values from the original state instead of the updated state *)
259 (cpsr, FST (FOLDL (\(s1,i) reg. (write s1 reg (read
[all...]
/seL4-l4v-10.1.1/HOL4/src/integer/testing/
H A Dreadproblemfile.sig9 [readterm is] attempts to read a term from the stream is. If the stream
11 SOME (SOME t) if there is a term there to be read, or SOME NONE if
12 something was read, but if failed to parse as a term. The stream must
17 v. The very first term read is combined with the initial value v0.
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A DFinalTag-sig.sml12 val read : string -> tag value
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/
H A Dupdate_header.scala14 val text0 = File.read(path)
H A Dupdate_then.scala14 val text0 = File.read(path)
H A Dupdate_theorems.scala14 val text0 = File.read(path)

Completed in 188 milliseconds

1234567891011>>