Removed pacman

diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index 95c6a6a649178a295f524388fcfdab5271ebfc60..93d69a83d9e82bcec96c33c519a86b95f60f66df 100644 (file)
--- a/ocaml/andrea.ml
+++ b/ocaml/andrea.ml
@@ -9,7 +9,6 @@ type t =
  | A of t * t\r
  | L of t\r
  | B (* bottom *)\r
- | P (* pacman *)\r
 ;;\r
 \r
 let eta_eq =\r
@@ -46,7 +45,6 @@ let string_of_t =
     | A _\r
     | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")"\r
     | B -> "BOT"\r
-    | P -> "PAC"\r
   and string_of_term_no_pars_app level = function\r
     | A(t1,t2) -> string_of_term_no_pars_app level t1 ^ " " ^ string_of_term_w_pars level t2\r
     | _ as t -> string_of_term_w_pars level t\r
@@ -79,7 +77,7 @@ let rec is_inert =
  function\r
  | A(t,_) -> is_inert t\r
  | V _ -> true\r
- | L _ | B | P -> false\r
+ | L _ | B -> false\r
 ;;\r
 \r
 let is_var = function V _ -> true | _ -> false;;\r
@@ -100,8 +98,7 @@ let rec subst level delift sub =
   let t2 = subst level delift sub t2 in\r
   mk_app t1 t2\r
  | B -> B\r
- | P -> P\r
-and mk_app t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with\r
+and mk_app t1 t2 = match t1 with\r
  | B | _ when t2 = B -> B\r
  | L t1 -> subst 0 true (0, t2) t1\r
  | t1 -> A (t1, t2)\r
@@ -112,7 +109,6 @@ and lift n =
   | L t -> L (aux (lev+1) t)\r
   | A (t1, t2) -> A (aux lev t1, aux lev t2)\r
   | B -> B\r
-  | P -> P\r
  in aux 0\r
 ;;\r
 let subst = subst 0 false;;\r
@@ -128,7 +124,7 @@ print_endline ("-- SUBST " ^ string_of_t (V (fst sub)) ^ " |-> " ^ string_of_t (
 \r
 let get_subterm_with_head_and_args hd_var n_args =\r
  let rec aux lev = function\r
- | V _ | B | P -> None\r
+ | V _ | B -> None\r
  | L t -> aux (lev+1) t\r
  | A(t1,t2) as t ->\r
    let hd_var', n_args' = get_inert t1 in\r
@@ -140,13 +136,6 @@ let get_subterm_with_head_and_args hd_var n_args =
  in aux 0\r
 ;;\r
 \r
-(* let rec simple_explode p =\r
- match p.div with\r
- | V var ->\r
-  let subst = var, B in\r
-  sanity (subst_in_problem subst p)\r
- | _ -> p *)\r
-\r
 let sanity p =\r
  print_endline (string_of_problem p); (* non cancellare *)\r
  if p.conv = B then problem_fail p "p.conv diverged";\r
@@ -215,12 +204,6 @@ let problem_of div conv =
   let subst = Util.index_of "BOMB" var_names, L B in\r
    subst_in_problem subst p\r
   with Not_found -> p in\r
- (* activate pacmans *)\r
- let p = try\r
-  let subst = Util.index_of "PACMAN" var_names, P in\r
-   let p = subst_in_problem subst p in\r
-   (print_endline ("after subst in problem " ^ string_of_problem p); p)\r
-  with Not_found -> p in\r
  (* initial sanity check *)\r
  sanity p; p\r
 ;;\r