-(* drops the arguments of t after the n-th *)\r
-(* FIXME! E' usato in modo improprio contando sul fatto\r
- errato che ritorna un inerte lungo esattamente n *)\r
-let inert_cut_at n t =\r
- let rec aux t =\r
- match t with\r
- | V _ as t -> 0, t\r
- | A(_,t1,_) as t ->\r
- let k', t' = aux t1 in\r
- if k' = n then n, t'\r
- else k'+1, t\r
- | _ -> assert false\r
- in snd (aux t)\r
-;;\r
-\r
-(* return the index of the first argument with a difference\r
- (the first argument is 0)\r
- precondition: p.div and t have n+1 arguments\r
- *)\r
-let find_eta_difference p t argsno =\r
- let t = inert_cut_at argsno t in\r
- let rec aux t u k = match t, u with\r
- | V _, V _ -> None\r
- | A(b1,t1,t2), A(b2,u1,u2) ->\r
- (match aux t1 u1 (k-1) with\r
- | None ->\r
- if not (eta_eq t2 u2) then begin\r
- let is_relevant = function `Some b -> !b | _ -> false in\r
- if not (is_relevant b1 || is_relevant b2) then begin\r
- print_string "WARNING! Stepping on a useless argument!";\r
-print_string (string_of_t t ^ " <==> " ^ string_of_t u);\r
- ignore(read_line())\r
- end ;\r
- Some (k-1)\r
- end\r
- else None\r
- | Some j -> Some j)\r
- | _, _ -> assert false\r
- in match aux p.div t argsno with\r
- | None -> problem_fail p "no eta difference found (div subterm of conv?)"\r
- | Some j -> j\r
-;;\r
-\r
-let compute_max_lambdas_at hd_var j =\r
- let rec aux hd = function\r
- | A(_,t1,t2) ->\r
- (if get_inert t1 = (hd, j)\r
- then max ( (*FIXME*)\r
- if is_inert t2 && let hd', j' = get_inert t2 in hd' = hd\r
- then let hd', j' = get_inert t2 in j - j'\r
- else no_leading_lambdas hd_var j t2)\r
- else id) (max (aux hd t1) (aux hd t2))\r
- | L t -> aux (hd+1) t\r
- | V _ -> 0\r
- in aux hd_var\r
-;;\r
-\r