From 2917b01cd638d1ef0786f085fdf27cb68a183329 Mon Sep 17 00:00:00 2001 From: acondolu Date: Wed, 30 May 2018 13:18:57 +0200 Subject: [PATCH] Removed pacman --- ocaml/andrea.ml | 23 +++-------------------- 1 file changed, 3 insertions(+), 20 deletions(-) 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 ;; -- 2.39.2