From c0e626fb979562114f436e2f2173a1062d8bbc31 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 85c385e..c8710f4 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