/seL4-l4v-10.1.1/HOL4/examples/computability/turing/ |
H A D | turing_machineScript.sml | 19 Each cell is either 0,1 or Blank 22 Head is said to 'scan' the cell it is currently over 23 At time 0 the cell the head is over is called the start cell 24 At time 0 every cell is Blank except 25 a finite congituous sequence from the strat cell to the right, containing only 0' and 1's 29 We can write A = {0,1,B} in the cell being scanned 65 val _ = Datatype `cell = Z | O `; 68 prog : ((num # cell) |-> (num # action)); 69 tape_l : cell lis [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
H A D | BUILTINS.sml | 51 | MemoryCellLength (* Return the length of a memory cell (heap object) *) 52 | MemoryCellFlags (* Return the flags byte of a memory cell (heap object) *) 79 (* Allocate a heap cell for byte data. The first argument is the number of words (not bytes) 81 The new cell is not initialised. *)
|
H A D | DEBUGGER_.sml | 303 (* This code will build a cons cell containing the run-time value 352 (* This code will build a cons cell containing the run-time value
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | process_env.cpp | 311 PolyObject *cell = alloc(mdTaskData, 2); local 312 cell->Set(0, at_exit_list); 313 cell->Set(1, args->Word()); 314 at_exit_list = cell; 327 PolyObject *cell = at_exit_list.AsObjPtr(); local 328 res = SAVE(cell->Get(1)); 329 at_exit_list = cell->Get(0); 680 // Return the maximum size of a cell that can be allocated on the heap.
|
H A D | polystring.cpp | 243 want to have make to make the cons cell mutable. This is only 274 ML_Cons_Cell *cell = (ML_Cons_Cell*)q.AsObjPtr(); local 275 vec[len++] = Poly_string_to_C_alloc(cell->h); 276 q = cell->t;
|
/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | KernelTypes.sml | 6 The reference cell is for uniqueness (an interactive session may
|
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | stringfindreplace.sml | 88 | ((cell as (starti, (t, bestopt)))::rest) =>
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | BackendIntermediateCodeSig.sml | 115 LoadStoreMLWord of {isImmutable: bool} (* Load/Store an ML word in an ML word cell. *) 116 | LoadStoreMLByte of {isImmutable: bool} (* Load/Store a byte, tagging and untagging as appropriate, in an ML byte cell. *)
|
H A D | BaseCodeTreeSig.sml | 35 LoadStoreMLWord of {isImmutable: bool} (* Load/Store an ML word in an ML word cell. *) 36 | LoadStoreMLByte of {isImmutable: bool} (* Load/Store a byte, tagging and untagging as appropriate, in an ML byte cell. *)
|
H A D | BackendIntermediateCode.sml | 224 LoadStoreMLWord of {isImmutable: bool} (* Load/Store an ML word in an ML word cell. *) 225 | LoadStoreMLByte of {isImmutable: bool} (* Load/Store a byte, tagging and untagging as appropriate, in an ML byte cell. *)
|
H A D | CODETREE_CODEGEN_CONSTANT_FUNCTIONS.sml | 76 mutable cell that will subsequently contain the address of the code.
|
H A D | CODETREE_FUNCTIONS.sml | 107 (* MemoryCellFlags could return a different result if a mutable cell was locked. *)
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | IntInf.sml | 123 we'll exceed the maximum size of a cell. *)
|
H A D | ForeignMemory.sml | 83 (* A weak byte cell is cleared to zero when it is read in either from the
|
H A D | Foreign.sml | 501 (* An external symbol is a memory cell containing the value in the first word 2336 allocate a memory cell big enough for a cX value. Then 2338 the argument, a pointer, to the address of the cell. *)
|
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
H A D | lalr.sml | 177 core. Each item is given a ref cell to hold the lookahead nonterminals for 200 (* findRef: state * item -> lookahead ref cell for item *)
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Literal.sml | 229 (* There are other possible literals, e.g. for word[n]. This ref cell is *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_semanticsScript.sml | 20 (* An S-expression is an atom or a dotted pair (cons-cell) *)
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | DB.sml | 102 not stored back into the reference cell, so there aren't
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Cache.sml | 189 in the same list point to the same updatable reference cell *)
|
/seL4-l4v-10.1.1/HOL4/Manual/Description/ |
H A D | holCheck.tex | 168 For this model, we need one state variable to track whose move it is, and we shall call this \(m\), which is true if the first player (call her A) is to move and false if the second player (call him B) is to move. We also need two state variables to keep track of the moves already played. The state variable \(u_{0,0}\) is true if A has claimed grid cell \((0,0)\) and false otherwise, and similarly the state variable \(v_{0,0}\) tracks B's moves. It is easy to see how this scheme can be generalised to arbitrary grids.
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | holCheck.tex | 168 For this model, we need one state variable to track whose move it is, and we shall call this \(m\), which is true if the first player (call her A) is to move and false if the second player (call him B) is to move. We also need two state variables to keep track of the moves already played. The state variable \(u_{0,0}\) is true if A has claimed grid cell \((0,0)\) and false otherwise, and similarly the state variable \(v_{0,0}\) tracks B's moves. It is easy to see how this scheme can be generalised to arbitrary grids.
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Defn.sml | 560 (* const_eq_ref is a reference cell that decides equality of literals such *)
|