From: acondolu <andrea.condoluci@unibo.it>
Date: Wed, 30 May 2018 11:18:57 +0000 (+0200)
Subject: Removed pacman
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2917b01cd638d1ef0786f085fdf27cb68a183329;p=fireball-separation.git

Removed pacman
---

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