Module Annot.IAnnot

An intermediate derivation, still containing undecided choices.

type res = (Rid.t * Mlsem_types.Ty.t) option

The result type a branch of an intersection was explored for, tagged with the node that produced it. None is the default branch, which assumes nothing.

type coverage = res * Mlsem_common.REnv.t

What a branch of an intersection covers: the result it was explored for, and the refinement of the environment under which it was explored. Used to skip branches subsumed by those already explored (cf. Domain).

type branch =
  1. | BMaybe of t
  2. | BType of t
  3. | BSkip
    (*

    A branch of a typecase: BMaybe before it has been decided whether the branch is reachable, BType / BSkip afterwards.

    *)
and inter_branch = {
  1. coverage : coverage option;
  2. ann : t option;
}

One branch of an intersection; ann = None once the branch has been found untypeable.

and inter = inter_branch list
and part = (Mlsem_types.Ty.t * LazyIAnnot.t option) list
and a =
  1. | Untyp
    (*

    Known untypeable; fails immediately.

    *)
  2. | AVar of Mlsem_types.MVarSet.t -> Mlsem_types.Subst.t
  3. | AConstruct of t list
  4. | ALet of t * part
  5. | ALet' of t * t
  6. | AApp of t * t * Mlsem_types.Ty.t
  7. | AOp of Mlsem_types.MVarSet.t -> Mlsem_types.Subst.t * t * Mlsem_types.Ty.t
  8. | AProj of t * Mlsem_types.Ty.t
  9. | ACast of Mlsem_types.GTy.t * t
  10. | ACoerce of Mlsem_types.GTy.t * t
  11. | AIte of t * Mlsem_types.GTy.t * branch * branch
  12. | ALambda of Mlsem_types.GTy.t * t
  13. | ALambdaRec of (Mlsem_types.GTy.t * t) list
  14. | AAlt of bool * t option list
  15. | AInter of inter
and t =
  1. | A of Annot.t
    (*

    An already completed sub-derivation.

    *)
  2. | I of {
    1. rid : Rid.t;
    2. ann : a;
    3. refinement : Mlsem_common.REnv.t;
    }
val substitute : Mlsem_types.Subst.t -> t -> t
val pp : Stdlib.Format.formatter -> t -> unit
val pp_a : Stdlib.Format.formatter -> a -> unit
val pp_coverage : Stdlib.Format.formatter -> coverage -> unit
val pp_res : Stdlib.Format.formatter -> res -> unit