Coq source for model of voidness preservation criteria

voidness.v

Require Import Coq.Program.Basics.
Require Import List.

Inductive Name : Set := Object | A | B | Iterable | List.

Inductive DartType : Set :=
| dt_void : DartType 
| dt_dynamic : DartType
| dt_class : list (Name * list DartType) -> DartType (* Incl. all supertypes *)
| dt_function : DartType -> list DartType -> DartType
| dt_variable : Name -> DartType. (* Type parameter with no bound *)

Definition ClassType : Type := (Name * (list DartType))%type.
Definition ClassTypes : Type := list ClassType.

Inductive VoidnessType : Set :=
| vt_0 : VoidnessType
| vt_1 : VoidnessType
| vt_class : list (Name * list VoidnessType) -> VoidnessType
| vt_function : VoidnessType -> list VoidnessType -> VoidnessType.

Definition VoidnessClassType : Type := prod Name (list VoidnessType).
Definition VoidnessClassTypes : Type := list VoidnessClassType.

Fixpoint voidness (dt : DartType) : VoidnessType :=
  match dt with
  | dt_void => vt_1
  | dt_dynamic => vt_0
  | dt_class ctypes => 
    vt_class ((fix ctMap (ctypes: ClassTypes) :=
              match ctypes with
              | nil => nil
              | (name, args) :: ctypes => (name, map voidness args) :: (ctMap ctypes)
              end) ctypes)
  | dt_function ret args => vt_function (voidness ret) (map covoidness args)
  | dt_variable name => vt_1
  end

with covoidness (dt : DartType) : VoidnessType :=
  match dt with
  | dt_void => vt_1
  | dt_dynamic => vt_1
  | dt_class ctypes =>
    vt_class ((fix ctMap (ctypes: ClassTypes) :=
              match ctypes with
              | nil => nil
              | (name, args) :: ctypes => (name, map covoidness args) :: (ctMap ctypes)
              end) ctypes)
  | dt_function ret args => vt_function (covoidness ret) (map voidness args)
  | dt_variable name => vt_1
  end.

Definition annotationVoidness := covoidness.

Inductive VoidnessPreserves : VoidnessType -> VoidnessType -> Prop :=
| vp_0_any : forall vt, VoidnessPreserves vt_0 vt
| vp_any_1 : forall vt, VoidnessPreserves vt vt_1
| vp_class : forall ctypes1 ctypes2,
  VoidnessClassTypesPreserve ctypes1 ctypes2 ->
  VoidnessPreserves (vt_class ctypes1) (vt_class ctypes2)
| vp_function : forall ret1 ret2 args1 args2,
  VoidnessPreserves ret1 ret2 ->
  VoidnessPreservesPairwise args2 args1 ->
  VoidnessPreserves (vt_function ret1 args1) (vt_function ret2 args2)

with VoidnessPreservesPairwise : list VoidnessType -> list VoidnessType -> Prop :=
| vpp_nil : VoidnessPreservesPairwise nil nil
| vpp_cons : forall vt1 vt2 vts1 vts2,
  VoidnessPreserves vt1 vt2 ->
  VoidnessPreservesPairwise vts1 vts2 ->
  VoidnessPreservesPairwise (vt1 :: vts1) (vt2 :: vts2)

with VoidnessClassTypesPreserve : VoidnessClassTypes -> VoidnessClassTypes -> Prop :=
| vctsp_nil : forall ctypes,
  VoidnessClassTypesPreserve nil ctypes
| vctsp_cons : forall ctype1 ctypes1 ctypes2,
  VoidnessClassTypePreserves ctype1 ctypes2 ->
  VoidnessClassTypesPreserve ctypes1 ctypes2 ->
  VoidnessClassTypesPreserve (ctype1 :: ctypes1) ctypes2

with VoidnessClassTypePreserves : VoidnessClassType -> VoidnessClassTypes -> Prop :=
| vctp_gone : forall ctype ctypes,
  VoidnessClassTypeGone ctype ctypes ->
  VoidnessClassTypePreserves ctype ctypes
| vctp_some : forall ctype ctypes,
  VoidnessClassTypePreservesSome ctype ctypes ->
  VoidnessClassTypePreserves ctype ctypes

with VoidnessClassTypeGone : VoidnessClassType -> VoidnessClassTypes -> Prop :=
| vctg_nil : forall ctype,
  VoidnessClassTypeGone ctype nil
| vctg_cons : forall name1 args1 name2 args2 ctypes,
  name1 <> name2 ->
  VoidnessClassTypeGone (name1, args1) ctypes ->
  VoidnessClassTypeGone (name1, args1) ((name2, args2) :: ctypes)

with VoidnessClassTypePreservesSome : VoidnessClassType -> VoidnessClassTypes -> Prop :=
| vctps_first : forall name args1 args2 ctypes,
  VoidnessPreservesPairwise args1 args2 ->
  VoidnessClassTypePreservesSome (name, args1) ((name, args2) :: ctypes)
| vctps_rest : forall ctype1 ctype2 ctypes2,
  VoidnessClassTypePreservesSome ctype1 ctypes2 ->
  VoidnessClassTypePreservesSome ctype1 (ctype2 :: ctypes2).

Hint Constructors
  VoidnessPreserves VoidnessPreservesPairwise 
  VoidnessClassTypesPreserve VoidnessClassTypePreserves
  VoidnessClassTypeGone VoidnessClassTypePreservesSome.

Definition TypeVoidnessPreserves (dt1: DartType) (dt2: DartType) : Prop :=
  VoidnessPreserves (voidness dt1) (annotationVoidness dt2).

Hint Unfold TypeVoidnessPreserves.

(* ---------- Lasse's relation ---------- *)

Inductive DartSubtype : DartType -> DartType -> Prop :=
| ds_void : forall dt, DartSubtype dt dt_void
| ds_dynamic : forall dt, DartSubtype dt dt_dynamic
| ds_Object : forall dt, DartSubtype dt (dt_class ((Object, nil) :: nil))
| ds_class : forall ctypes1 ctypes2,
  DartSubtypesClassTypes ctypes1 ctypes2 ->
  DartSubtype (dt_class ctypes1) (dt_class ctypes2)
| ds_function : forall ret1 args1 ret2 args2,
  DartSubtype ret1 ret2 ->
  DartSubtypePairwise args2 args1 ->
  DartSubtype (dt_function ret1 args1) (dt_function ret2 args2)
| ds_variable : forall name,
  DartSubtype (dt_variable name) (dt_variable name)

with DartSubtypePairwise : list DartType -> list DartType -> Prop :=
| dsp_nil : DartSubtypePairwise nil nil
| dsp_cons : forall dt1 dts1 dt2 dts2,
  DartSubtype dt1 dt2 ->
  DartSubtypePairwise dts1 dts2 ->
  DartSubtypePairwise (dt1 :: dts1) (dt2 :: dts2)

with DartSubtypesClassTypes : ClassTypes -> ClassTypes -> Prop :=
| dsscts_nil : forall ctypes,
  DartSubtypesClassTypes ctypes nil
| dsscts_cons : forall ctypes1 ctype2 ctypes2,
  DartSubtypeClassTypes ctypes1 ctype2 ->
  DartSubtypesClassTypes ctypes1 ctypes2 ->
  DartSubtypesClassTypes ctypes1 (ctype2 :: ctypes2)

with DartSubtypeClassTypes : ClassTypes -> ClassType -> Prop :=
| dscts_first : forall ctype1 ctypes1 ctype2,
  DartSubtypeClassType ctype1 ctype2 ->
  DartSubtypeClassTypes (ctype1 :: ctypes1) ctype2
| dscts_rest : forall ctype1 ctypes1 ctype2,
  DartSubtypeClassTypes ctypes1 ctype2 ->
  DartSubtypeClassTypes (ctype1 :: ctypes1) ctype2

with DartSubtypeClassType : ClassType -> ClassType -> Prop :=
| dsct_args: forall name args1 args2,
  DartSubtypePairwise args1 args2 ->
  DartSubtypeClassType (name, args1) (name, args2).

Hint Constructors
  DartSubtype DartSubtypePairwise 
  DartSubtypesClassTypes DartSubtypeClassTypes DartSubtypeClassType.

Definition DartAssignable (dt1: DartType) (dt2: DartType) : Prop :=
  or (DartSubtype dt1 dt2) (DartSubtype dt2 dt1).

Hint Unfold DartAssignable.

Inductive isNotVariableNamed : Name -> DartType -> Prop :=
| invn_void : forall name,
  isNotVariableNamed name dt_void
| invn_dynamic : forall name,
  isNotVariableNamed name dt_dynamic
| invn_class : forall name ctypes,
  isNotVariableNamed name (dt_class ctypes)
| insn_variable : forall name1 name2,
  name1 <> name2 ->
  isNotVariableNamed name1 (dt_variable name2).

Hint Constructors isNotVariableNamed.

Inductive ClassTypeNamed : Name -> ClassTypes -> ClassType -> Prop :=
| ctn_first : forall name args ctypes,
  ClassTypeNamed name ((name, args) :: ctypes) (name, args)
| ctn_rest : forall name1 ctype ctypes name2 args2,
  name1 <> name2 ->
  ClassTypeNamed name1 ctypes ctype ->
  ClassTypeNamed name1 ((name2, args2) :: ctypes) ctype.

Hint Constructors ClassTypeNamed.

(* NotVoidAssignable typeOfSource typeAnnotationOfTarget: `Target x = source;` will cause a loss of voidness *)
Inductive NotVoidAssignable : DartType -> DartType -> Prop :=
| nva_base : forall T,
  T <> dt_void ->
  T <> dt_dynamic ->
  NotVoidAssignable dt_void T
| nva_class : forall ctypes1 ctypes2,
  NotVoidAssignableClassTypes ctypes1 ctypes2 ->
  NotVoidAssignable (dt_class ctypes1) (dt_class ctypes2)
| nva_function_ret : forall ret1 args1 ret2 args2,
  DartAssignable (dt_function ret1 args1) (dt_function ret2 args2) ->
  NotVoidAssignable ret1 ret2 ->
  NotVoidAssignable (dt_function ret1 args1) (dt_function ret2 args2)
| nva_function_arg : forall ret1 args1 ret2 args2,
  DartAssignable (dt_function ret1 args1) (dt_function ret2 args2) ->
  NotVoidAssignablePairwise args2 args1 ->
  NotVoidAssignable (dt_function ret1 args1) (dt_function ret2 args2)
| nva_variable : forall name dt,
  isNotVariableNamed name dt ->
  NotVoidAssignable (dt_variable name) dt

(* NotVoidAssignablePairwise types1 types2: At least one pair (type1, type2) causes a loss of voidness *)
with NotVoidAssignablePairwise : list DartType -> list DartType -> Prop :=
| nvap_cons_first : forall dt1 dts1 dt2 dts2,
  NotVoidAssignable dt1 dt2 ->
  NotVoidAssignablePairwise (dt1 :: dts1) (dt2 :: dts2)
| nvap_cons_rest : forall dt1 dts1 dt2 dts2,
  NotVoidAssignablePairwise dts1 dts2 ->
  NotVoidAssignablePairwise (dt1 :: dts1) (dt2 :: dts2)

(* NotVoidAssignableClassTypes classTypes1 classTypes2: `"dt_class classTypes2" x = "dt_class classTypes1"-expression` causes loss of voidness *)
with NotVoidAssignableClassTypes : ClassTypes -> ClassTypes -> Prop :=
| nvact_upcast : forall name args1 ctypes1 args2 ctypes2,
  DartSubtypesClassTypes ctypes1 ((name, args2) :: ctypes2) -> (* This is an upcast, to (name, args2) :: ctypes2 *)
  ClassTypeNamed name ctypes1 (name, args1) -> (* In ctypes1, the type named name is (name, args1) *)
  NotVoidAssignablePairwise args1 args2 -> (* At least one type argument is not-void-assignable *)
  NotVoidAssignableClassTypes ctypes1 ((name, args2) :: ctypes2)
| nvact_downcast : forall name args1 ctypes1 args2 ctypes2,
  DartSubtypesClassTypes ctypes2 ((name, args1) :: ctypes1) -> (* This is a downcast, to ctypes2 *)
  ClassTypeNamed name ctypes2 (name, args2) -> (* In ctypes2, the type named name is (name, args2) *)
  NotVoidAssignablePairwise args1 args2 -> (* At least one type argument is not-void-assignable *)
  NotVoidAssignableClassTypes ((name, args1) :: ctypes1) ctypes2.

Hint Constructors
  NotVoidAssignable NotVoidAssignablePairwise NotVoidAssignableClassTypes.