open Syntax

type ev = Evidence.TypeEvidence.t

(** Given two evidences, ev1 is more precise than ev2 when the set of static
    types represented by ev1 is contained in the set of static types represented
    by ev2 *)
let is_more_precise (ev1 : ev) (ev2 : ev) : bool =
  ev1 = Evidence.TypeEvidence.meet ev1 ev2

(** An evidence ev is fully precise when the set of static types it representes
    corresponds to a singleton *)
let rec is_fully_precise (ev : ev) : bool =
  match ev with
  | Type.Any -> false
  | Type.Int | Type.Bool | Type.Float | Type.Rec (_, _) | Type.Variant _ -> true
  | Type.Arrow (tys, ty) ->
      List.for_all is_fully_precise tys && is_fully_precise ty
  | Type.Product tys -> List.for_all is_fully_precise tys
  | Type.Vec ty -> is_fully_precise ty
  | Type.Var _ -> failwith "should be impossible"

(** Assuming that a term is know to be at least as precise as ev1 is being
    ascribed with an evidence exactly ev2, we can remove the ascription when ev1
    is more precise than ev2. *)
let can_remove_static_ascription ev1 ev2 = is_more_precise ev1 ev2

(** Assuming that a term is known to be at least as precise as ev1 and it is
    being ascribed with an evidence that we know to be at least as precise as
    ev2, we can only remove the annotation when ev1 is fully precise and ev2 is
    equal to ev1. *)
let can_remove_runtime_ascription ev1 ev2 = is_fully_precise ev1 && ev1 = ev2
