From 49197592f9020aa1c5f87f19f2dfce58b0ccc798 Mon Sep 17 00:00:00 2001 From: acondolu Date: Tue, 29 May 2018 11:03:53 +0200 Subject: [PATCH] get_subterm_with_head_and_args goes under lambdas --- ocaml/andrea.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml index c78dde0..0edd1b2 100644 --- a/ocaml/andrea.ml +++ b/ocaml/andrea.ml @@ -135,15 +135,16 @@ print_endline ("-- SUBST " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t ;; let get_subterm_with_head_and_args hd_var n_args = - let rec aux = function - | V _ | L _ | B | P -> None + let rec aux lev = function + | V _ | B | P -> None + | L t -> aux (lev+1) t | A(t1,t2) as t -> - if head_of_inert t1 = hd_var && n_args <= 1 + args_no t1 - then Some t - else match aux t2 with - | None -> aux t1 + if head_of_inert t1 = hd_var + lev && n_args <= 1 + args_no t1 (* why `1+' ?*) + then Some (lift ~-lev t) + else match aux lev t2 with + | None -> aux lev t1 | Some _ as res -> res - in aux + in aux 0 ;; (* let rec simple_explode p = -- 2.39.2