- }
-
-
-(* let heads = Util.sort_uniq (List.map hd_of_i_var p.ps) in
-for all head
- List.map (fun (_, bs) -> List.map (fun (x,_) -> List.nth p.ps x) !bs) p.deltas *)
-
-(* let ($) f x = f x;; *)
-
-(* let subterms tms freshno =
- let apply_var =
- let no = ref freshno in
- function t -> incr no; mk_app t (`Var !no) in
- let applicative hd args = snd (
- List.fold_left (fun (hd, acc) t -> let hd = mk_app hd t in hd, hd::acc) (hd, []) args) in
- let rec aux t = match t with
- | `Var _ -> []
- | `I(v,ts) ->
- (* applicative (`Var v) (Listx.to_list ts) @ *)
- Util.concat_map aux (Listx.to_list ts) @ List.map apply_var (Listx.to_list ts)
- | `Lam(_,_,t) -> aux (lift ~-1 t)
- | `Match(u,_,bs_lift,bs,args) ->
- aux (u :> nf) @
- (* applicative (`Match(u,bs_lift,bs,[])) args @ *)
- Util.concat_map aux args @ List.map apply_var args
- (* @ Util.concat_map (aux ++ (lift bs_lift) ++ snd) !bs *)
- | `N _ -> []
- in let tms' = (* Util.sort_uniq ~compare:eta_compare*) (Util.concat_map aux tms) in
- tms @ tms'
- (* List.map (fun (t, v) -> match t with `N _ -> t | _ -> mk_app t v) (List.combine tms (List.mapi (fun i _ -> `Var(freshno+i)) tms)) *)
-;; *)