]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
get_subterm_with_head_and_args goes under lambdas
authoracondolu <andrea.condoluci@unibo.it>
Tue, 29 May 2018 09:03:53 +0000 (11:03 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Tue, 29 May 2018 14:33:37 +0000 (16:33 +0200)
ocaml/andrea.ml

index 85c385e1fc923ef7e0655278837cbff9d9e898aa..c8710f4a7192092f50433d332963625f055247e1 100644 (file)
@@ -135,15 +135,16 @@ print_endline ("-- SUBST " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t
 ;;\r
 \r
 let get_subterm_with_head_and_args hd_var n_args =\r
- let rec aux = function\r
- | V _ | L _ | B | P -> None\r
+ let rec aux lev = function\r
+ | V _ | B | P -> None\r
+ | L t -> aux (lev+1) t\r
  | A(t1,t2) as t ->\r
-   if head_of_inert t1 = hd_var && n_args <= 1 + args_no t1\r
-    then Some t\r
-    else match aux t2 with\r
-    | None -> aux t1\r
+   if head_of_inert t1 = hd_var + lev && n_args <= 1 + args_no t1 (* why `1+' ?*)\r
+    then Some (lift ~-lev t)\r
+    else match aux lev t2 with\r
+    | None -> aux lev t1\r
     | Some _ as res -> res\r
- in aux\r
+ in aux 0\r
 ;;\r
 \r
 (* let rec simple_explode p =\r