lookup codomain of uninterpreted function in metric_wf

[mzacho]

When checking let rec expressions with a metric that's a call to an uninterpreted function (such as "length reflects len" whose metric is len(xs)), we're currently assume that any function has as result that's int-sorted.

See the P_FunApp case in check_sort:

let rec check_sort (g : logic_env) (p : L.pred) (s : L.sort) : bool =
  match s with
  | L.S_Int -> (
      match p with
      | L.P_Int _ -> true
      (* check that both predicates are int-sorted *)
      | L.P_Op (_, p1, p2) -> check_sort g p1 s && check_sort g p2 s
      | L.P_Var x -> (
          try
            let _, s' = List.find (fun (y, _) -> String.equal y x) g in
            s' = L.S_Int
          with Not_found -> true)
      | P_FunApp (_, _) -> true (* TODO: lookup codomain of uninterpreted fun *)
      | _ -> false
  )
  | L.S_Bool -> failwith "unimplemented"
  | L.S_TyCtor _ -> failwith "unimplemented"

on the termination branch