Searched refs:cell (Results 1 - 23 of 23) sorted by relevance

/seL4-l4v-10.1.1/HOL4/examples/computability/turing/
H A Dturing_machineScript.sml19 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 DBUILTINS.sml51 | 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 DDEBUGGER_.sml303 (* 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 Dprocess_env.cpp311 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 Dpolystring.cpp243 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 DKernelTypes.sml6 The reference cell is for uniqueness (an interactive session may
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A Dstringfindreplace.sml88 | ((cell as (starti, (t, bestopt)))::rest) =>
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DBackendIntermediateCodeSig.sml115 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 DBaseCodeTreeSig.sml35 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 DBackendIntermediateCode.sml224 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 DCODETREE_CODEGEN_CONSTANT_FUNCTIONS.sml76 mutable cell that will subsequently contain the address of the code.
H A DCODETREE_FUNCTIONS.sml107 (* MemoryCellFlags could return a different result if a mutable cell was locked. *)
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DIntInf.sml123 we'll exceed the maximum size of a cell. *)
H A DForeignMemory.sml83 (* A weak byte cell is cleared to zero when it is read in either from the
H A DForeign.sml501 (* 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 Dlalr.sml177 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 DLiteral.sml229 (* 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 Dlisp_semanticsScript.sml20 (* An S-expression is an atom or a dotted pair (cons-cell) *)
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DDB.sml102 not stored back into the reference cell, so there aren't
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DCache.sml189 in the same list point to the same updatable reference cell *)
/seL4-l4v-10.1.1/HOL4/Manual/Description/
H A DholCheck.tex168 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 DholCheck.tex168 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 DDefn.sml560 (* const_eq_ref is a reference cell that decides equality of literals such *)

Completed in 278 milliseconds