-let problem_measure p =
- let l = Array.to_list (Array.init (p.freshno + 1) string_of_var) in
- let open Listx in
- (* aux |t1;t2| e' numero di step per portare la diff in testa
- INVARIANTE: t1 <eta> t2
- *)
- let rec aux t1 t2 =
- match t1, t2 with
- | `I(v1,nfs1), `I(v2,nfs2) ->
- if v1 <> v2
- then 0 else 1 + find_first_diff (to_list nfs1, to_list nfs2)
- | `Match (t1,bs_lift,bs,args), `Match (t2,bs_lift',bs',args') ->
- if bs != bs' then 0 (* TODO *)
- else if eta_eq (t1 :> nf) (t2 :> nf) then 1 + find_first_diff (args, args') else aux (t1 :> nf) (t2 :> nf) (* TODO *)
- | `Match _, _
- | _, `Match _ -> 0 (* FIXME!!! *)
- | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2
- | _ -> 0
- and find_first_diff = function
- | [], [] -> assert false
- | [], t::_
- | t::_, [] -> 1
- | t1::ts1, t2::ts2 ->
- if eta_eq (t1 :> nf) (t2 :> nf) then 1 + find_first_diff (ts1, ts2) else aux t1 t2
- (* no. di step da fare per separare t1 e t2 *)
- in let diff t1 t2 = (
- let res = if eta_eq t1 t2 then 0 else aux t1 t2 in
- if res <> 0 then prerr_endline ("diff (" ^ print ~l t1 ^ ") (" ^ print ~l t2 ^ ") = " ^ string_of_int res);
- res
- )
- (* aux calcola la somma delle differenze tra i termini in una lista (quadratico) *)
- in let rec sum = function
- | [] -> 0
- | x::xs -> List.fold_right ((+) ++ (diff (x :> nf))) (xs :> nf list) (sum xs)
- in let subterms = subterms ((all_terms p) :> nf list) p.freshno
- (* let subterms = sort_uniq ~compare:eta_compare subterms in *)
- in let a = sum subterms
- in let b = List.fold_right (fun bs -> (+) (sum (List.map ((List.nth p.ps) ++ fst) !bs))) p.deltas 0
- in let _ = prerr_endline ("Computed measure: " ^ string_of_int a ^ "," ^ string_of_int b)
- in a + b