matita/matita/lib/turing/universal/uni_step.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_____________________________________________________________*)
  11
  12
  13 (* COMPARE BIT
  14
  15 *)
  16
  17 include "turing/universal/copy.ma".
  18
  19 (*
  20
  21 step :
  22
  23 if is_true(current) (* current state is final *)
  24    then nop
  25    else
  26    (* init_match *)
  27    mark;
  28    adv_to_grid_r;
  29    move_r;
  30    mark;
  31    move_l;
  32    adv_to_mark_l
  33    (* /init_match *)
  34    match_tuple;
  35    if is_marked(current) = false (* match ok *)
  36       then
  37            (* init_copy *)
  38            move_l;
  39            init_current;
  40            move_r;
  41            adv_to_mark_r;
  42            adv_mark_r;
  43            (* /init_copy *)
  44            copy;
  45            move_r;
  46            (* move_tape *)
  47            by cases on current:
  48              case bit false: move_tape_l
  49              case bit true: move_tape_r
  50              case null: adv_to_grid_l; move_l; adv_to_grid_l;
  51            move_r;
  52            (* /move_tape *)
  53       else sink;
  54
  55 *)