Module Unityping

Require Import Recdef Coqlib Maps Errors.

Local Open Scope nat_scope.
Local Open Scope error_monad_scope.



Module Type TYPE_ALGEBRA.

Variable t: Type.
Variable eq: forall (x y: t), {x=y} + {x<>y}.
Variable default: t.

End TYPE_ALGEBRA.


Module UniSolver (T: TYPE_ALGEBRA).


Definition constraint : Type := (positive * positive)%type.

Record typenv : Type := Typenv {
  te_typ: PTree.t T.t; (* mapping var -> typ *)
  te_equ: list constraint (* additional equality constraints *)
}.

Definition initial : typenv := {| te_typ := PTree.empty _; te_equ := nil |}.


Definition set (e: typenv) (x: positive) (ty: T.t) : res typenv :=
  match e.(te_typ)!x with
  | None =>
      OK {| te_typ := PTree.set x ty e.(te_typ);
            te_equ := e.(te_equ) |}
  | Some ty' =>
      if T.eq ty ty'
      then OK e
      else Error (MSG "bad definition/use of variable " :: POS x :: nil)
  end.

Fixpoint set_list (e: typenv) (rl: list positive) (tyl: list T.t) {struct rl}: res typenv :=
  match rl, tyl with
  | nil, nil => OK e
  | r1::rs, ty1::tys => do e1 <- set e r1 ty1; set_list e1 rs tys
  | _, _ => Error (msg "arity mismatch")
  end.


Definition move (e: typenv) (r1 r2: positive) : res (bool * typenv) :=
  if peq r1 r2 then OK (false, e) else
  match e.(te_typ)!r1, e.(te_typ)!r2 with
  | None, None =>
      OK (false, {| te_typ := e.(te_typ); te_equ := (r1, r2) :: e.(te_equ) |})
  | Some ty1, None =>
      OK (true, {| te_typ := PTree.set r2 ty1 e.(te_typ); te_equ := e.(te_equ) |})
  | None, Some ty2 =>
      OK (true, {| te_typ := PTree.set r1 ty2 e.(te_typ); te_equ := e.(te_equ) |})
  | Some ty1, Some ty2 =>
      if T.eq ty1 ty2
      then OK (false, e)
      else Error(MSG "ill-typed move from " :: POS r1 :: MSG " to " :: POS r2 :: nil)
  end.


Fixpoint solve_rec (e: typenv) (changed: bool) (q: list constraint) : res (typenv * bool) :=
  match q with
  | nil =>
      OK (e, changed)
  | (r1, r2) :: q' =>
      do (changed1, e1) <- move e r1 r2; solve_rec e1 (changed || changed1) q'
  end.


Lemma move_shape:
  forall e r1 r2 changed e',
  move e r1 r2 = OK (changed, e') ->
  (e'.(te_equ) = e.(te_equ) \/ e'.(te_equ) = (r1, r2) :: e.(te_equ))
  /\ (changed = true -> e'.(te_equ) = e.(te_equ)).

Lemma length_move:
  forall e r1 r2 changed e',
  move e r1 r2 = OK (changed, e') ->
  length e'.(te_equ) + (if changed then 1 else 0) <= S(length e.(te_equ)).

Lemma length_solve_rec:
  forall q e ch e' ch',
  solve_rec e ch q = OK (e', ch') ->
  length e'.(te_equ) + (if ch' && negb ch then 1 else 0) <= length e.(te_equ) + length q.

Definition weight_typenv (e: typenv) : nat := length e.(te_equ).



Function solve_constraints (e: typenv) {measure weight_typenv e}: res typenv :=
  match solve_rec {| te_typ := e.(te_typ); te_equ := nil |} false e.(te_equ) with
  | OK(e', false) => OK e (* no more changes, fixpoint reached *)
  | OK(e', true) => solve_constraints e' (* one more iteration *)
  | Error msg => Error msg
  end.

Definition typassign := positive -> T.t.

Definition makeassign (e: typenv) : typassign :=
  fun x => match e.(te_typ)!x with Some ty => ty | None => T.default end.

Definition solve (e: typenv) : res typassign :=
  do e' <- solve_constraints e; OK(makeassign e').


Definition satisf (te: typassign) (e: typenv) : Prop :=
   (forall x ty, e.(te_typ)!x = Some ty -> te x = ty)
/\ (forall x y, In (x, y) e.(te_equ) -> te x = te y).

Lemma satisf_initial: forall te, satisf te initial.


Lemma set_incr:
  forall te x ty e e', set e x ty = OK e' -> satisf te e' -> satisf te e.

Hint Resolve set_incr: ty.

Lemma set_sound:
  forall te x ty e e', set e x ty = OK e' -> satisf te e' -> te x = ty.

Lemma set_list_incr:
  forall te xl tyl e e', set_list e xl tyl = OK e' -> satisf te e' -> satisf te e.

Hint Resolve set_list_incr: ty.

Lemma set_list_sound:
  forall te xl tyl e e', set_list e xl tyl = OK e' -> satisf te e' -> map te xl = tyl.

Lemma move_incr:
  forall te e r1 r2 e' changed,
  move e r1 r2 = OK(changed, e') -> satisf te e' -> satisf te e.

Hint Resolve move_incr: ty.

Lemma move_sound:
  forall te e r1 r2 e' changed,
  move e r1 r2 = OK(changed, e') -> satisf te e' -> te r1 = te r2.

Lemma solve_rec_incr:
  forall te q e changed e' changed',
  solve_rec e changed q = OK(e', changed') -> satisf te e' -> satisf te e.

Lemma solve_rec_sound:
  forall te r1 r2 q e changed e' changed',
  solve_rec e changed q = OK(e', changed') -> In (r1, r2) q -> satisf te e' ->
  te r1 = te r2.

Lemma move_false:
  forall e r1 r2 e',
  move e r1 r2 = OK(false, e') ->
  te_typ e' = te_typ e /\ makeassign e r1 = makeassign e r2.

Lemma solve_rec_false:
  forall r1 r2 q e changed e',
  solve_rec e changed q = OK(e', false) ->
  changed = false /\
  (In (r1, r2) q -> makeassign e r1 = makeassign e r2).

Lemma solve_constraints_incr:
  forall te e e', solve_constraints e = OK e' -> satisf te e' -> satisf te e.

Lemma solve_constraints_sound:
  forall e e', solve_constraints e = OK e' -> satisf (makeassign e') e'.

Theorem solve_sound:
  forall e te, solve e = OK te -> satisf te e.


Lemma set_complete:
  forall te e x ty,
  satisf te e -> te x = ty -> exists e', set e x ty = OK e' /\ satisf te e'.

Lemma set_list_complete:
  forall te xl tyl e,
  satisf te e -> map te xl = tyl ->
  exists e', set_list e xl tyl = OK e' /\ satisf te e'.

Lemma move_complete:
  forall te e r1 r2,
  satisf te e -> te r1 = te r2 ->
  exists changed e', move e r1 r2 = OK(changed, e') /\ satisf te e'.

Lemma solve_rec_complete:
  forall te q e changed,
  satisf te e ->
  (forall r1 r2, In (r1, r2) q -> te r1 = te r2) ->
  exists e' changed', solve_rec e changed q = OK(e', changed') /\ satisf te e'.

Lemma solve_constraints_complete:
  forall te e, satisf te e -> exists e', solve_constraints e = OK e' /\ satisf te e'.

Lemma solve_complete:
  forall te e, satisf te e -> exists te', solve e = OK te'.

End UniSolver.