open Interp;; let rec print_nat n = match n with O -> print_string "O" | S x -> print_string "S("; print_nat x; print_string ")";; let rec print_aexp a = match a with Loc v -> (print_string "Loc(" ; print_nat v; print_string ")") | Num n -> (print_string "Num("; print_nat n; print_string ")") | Plus (a1, a2) -> (print_string "Plus("; print_aexp a1; print_aexp a2; print_string ")") | Minus (a1, a2) -> (print_string "Minus("; print_aexp a1; print_aexp a2; print_string ")") | Mult (a1, a2) -> (print_string "Mult("; print_aexp a1; print_aexp a2; print_string ")") let rec print_bexp b = match b with IMPtrue -> print_string "True" | IMPfalse -> print_string "False" | Equal (a1, a2) -> (print_string "Equal("; print_aexp a1; print_aexp a2; print_string ")") | LessEqual (a1, a2) -> (print_string "LessEqual("; print_aexp a1; print_aexp a2; print_string ")") | Not b1 -> (print_string "Not("; print_bexp b1 ; print_string ")") | Or (b1, b2) -> (print_string "Or("; print_bexp b1; print_bexp b2; print_string ")") | AAnd (b1, b2) -> (print_string "And("; print_bexp b1; print_bexp b2; print_string ")") let rec print_com c = match c with Skip -> print_string "Skip" | Assign (v, a) -> (print_string "Assign("; print_nat v; print_aexp a; print_string ")") | Scolon (c1, c2) -> (print_string "Scolon("; print_com c1; print_com c2; print_string ")") | IfThenElse (b, c1, c2) -> (print_string "IfThenElse("; print_bexp b; print_com c1; print_com c2; print_string ")") | WhileDo (b, c0) -> (print_string "WhileDo("; print_bexp b; print_com c0; print_string ")");; let print_state s = let rec print_state_rec s = match s with No_location -> print_string "]" | One_location(n,v,e) -> (print_string "("; print_nat n; print_nat v; print_string ")"; print_state_rec e) in (print_string "["; print_state_rec s ; print_string "\n"; flush stdout);; let inst = WhileDo(LessEqual(Num(S O),Loc(O)), Scolon(Assign(O,Minus(Loc(O),Num(S(O)))), Assign(S O,Plus(Loc(O),Loc(S O)))));; let s0 = One_location(O,S(S O),One_location(S O,O,No_location));; iter2 evalcom_rec_F (S (S (S (S (S (S O)))))) (fun c s -> s) inst s0;; let rec no_bound = S no_bound;; let rec fix f = f (fun x -> (fix f x));; iter2 evalcom_rec_F no_bound (fun c s -> s) inst s0;; fix evalcom_rec_F no_bound inst s0;;