caml-urm

A OCaml module for manipulating unlimited register machines

Diffstat

4 files changed, 111 insertions, 0 deletions

diff --git a/Makefile b/Makefile
@@ -0,0 +1,5 @@
+docs.pdf: urm.mli
+	ocamldoc -latex -o docs.tex urm.mli
+	latexmk -pdflatex docs.tex
+	texclear docs.tex
+	rm  docs.tex ocamldoc.sty

diff --git a/docs.pdf b/docs.pdf
Binary files differ.

diff --git a/urm.ml b/urm.ml
@@ -0,0 +1,68 @@
+open Array
+
+type instruction = 
+  | T of int * int
+  | Z of int
+  | S of int
+  | J of int * int * int
+
+type machine = 
+  { instruction_pointer : int;
+    registers : nat -> nat;
+  }
+
+let from_registers (f : int -> int) : machine =
+  { intruction_pointer = 0;
+    registers = f
+  }
+
+let zero : machines = from_registers (fun _ -> 0)
+
+let register (m : machine) (i : int) : int = m.registers i
+
+(** Executes the next instruction. Returns [Some _] is the instruction pointer
+ points to a valid adress and [None] otherwise. *)
+let step (program : instruction array) (m : machine) : machine option =
+  if m.instruction_pointer >= length program || m.instruction_pointer < 0
+  then None
+  else
+    let updated =
+      match program.(m.instruction_pointer) with
+      | T (r1, r2) -> 
+        { registers = 
+            (fun n -> if n == r2 then m.registers r1 else m.registers n);
+          instruction_pointer = m.instruction_pointer + 1;
+        }
+      | Z r -> 
+        { registers = (fun n -> if n == r then 0 else m.registers n);
+          instruction_pointer = m.instruction_pointer + 1;
+        }
+      | S r -> 
+        { registers = 
+            (fun n -> if n == r then 1 + (m.registers n) else m.registers n);
+          instruction_pointer = m.instruction_pointer + 1;
+        }
+      | J (r1, r2, i) when m.registers r1 == m.registers r2 -> 
+        { m with instruction_pointer = i }
+      | J _ -> 
+        { m with instruction_pointer = m.instruction_pointer + 1 } 
+    in Some updated
+
+let rec exec (program : instruction array) (m : machine) : machine =
+  match step program m with
+  | None -> { m with instruction_pointer = 0 }
+  | Some n -> exec program n
+
+let exec_safe program (m : machine) (max : int) : machine option =
+  if max <= 0 
+  then raise (Invalid_argument "the number of clock-cycles must be positive ")
+  else
+    let rec exec_safe_tail m clock_cycles =
+      if clock_cycles <= max
+      then 
+        match step program m with
+        | None -> Some { m with instruction_pointer = 0 }
+        | Some n -> exec_safe_tail n (clock_cycles + 1)
+      else None
+    in exec_safe_tail m 0
+

diff --git a/urm.mli b/urm.mli
@@ -0,0 +1,38 @@
+(** Functions and types for manipulation unlimited register machines. *)
+
+(** The type of instructions. *)
+type instruction = 
+  | T of int * int (** Transfers values between registers. *)
+  | Z of int (** Sets a register to zero. *)
+  | S of int (** Increments a register *)
+  | J of int * int * int 
+    (** Jumps to a given point if the values of two registers coincide. *)
+
+(** The type of all possible states of a URM. *)
+type machine
+
+(** Returns a machine whose value of the [n]-th register is given by [f n]. *)
+val from_registers : f:(int -> int) -> machine
+
+(** Returns the value of the [i]-th register of [m]. *)
+val register : m:machine -> i:int -> int
+
+(** A machine whose registers are all zeros. *)
+val zeros : machine
+
+(** Returns a machine whose register values are given by the register values of
+    [m] with updates corresponding to the execution of [program]. 
+
+    This function only returns when [program] actually halts. Please use {!
+    exec_safe } if you don't trust the [program]. *)
+val exec : program:instruction array -> m:machine -> machine
+
+(** A safe version of {! exec }, where the max number of clock-cycles
+    allowed is controlled by [max]. Each instruction takes a single clock-cycle
+    to execute.
+
+    Returns [Some _] if [program] halts in at most [max] clock-cycles and
+    [None] otherwise. Throws [Invalid_argument] if [max] is not a positive
+    integer. *)
+val exec_safe : program: instruction array -> 
+  machine -> max:int -> machine option