delete old type system. everything has been ported to the new one.

_CoqProject

@@ -24,8 +24,6 @@ theories/lang/races.v
 theories/lang/tactics.v
 theories/lang/wp_tactics.v
 theories/typing/type.v
-theories/typing/perm.v
-theories/typing/typing.v
 theories/typing/lft_contexts.v
 theories/typing/type_context.v
 theories/typing/cont_context.v

theories/typing/borrow.v

@@ -3,7 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lifetime Require Import reborrow frac_borrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export uniq_bor shr_bor own.
-From lrust.typing Require Import lft_contexts type_context perm typing programs.
+From lrust.typing Require Import lft_contexts type_context programs.
 
 (** The rules for borrowing and derferencing borrowed non-Copy pointers are in
   a separate file so make sure that own.v and uniq_bor.v can be compiled

theories/typing/perm.v

-From iris.proofmode Require Import tactics.
-From lrust.typing Require Export type.
-From lrust.lang Require Export proofmode notation.
-From lrust.lifetime Require Import borrow frac_borrow.
-
-(* TODO: This is all still using the outdated type system. *)
-
-Section perm.
-  Context `{typeG Σ}.
-
-  Definition perm {Σ} := na_inv_pool_name → iProp Σ.
-
-  Fixpoint eval_expr (ν : expr) : option val :=
-    match ν with
-    | BinOp OffsetOp e (Lit (LitInt n)) =>
-      match eval_expr e with
-      | Some (#(LitLoc l)) => Some (#(shift_loc l n))
-      | _ => None
-      end
-    | e => to_val e
-    end.
-
-  Definition has_type (ν : expr) (ty : type) : perm := λ tid,
-    from_option (λ v, ty.(ty_own) tid [v]) False%I (eval_expr ν).
-
-  Definition extract (κ : lft) (ρ : perm) : perm :=
-    λ tid, ([†κ] ={↑lftN}=∗ ρ tid)%I.
-
-  Definition tok (κ : lft) (q : Qp) : perm :=
-    λ _, q.[κ]%I.
-
-
-  Definition killable (κ : lft) : perm :=
-    λ _, (□ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]))%I.
-
-  Definition incl (κ κ' : lft) : perm :=
-    λ _, (κ ⊑ κ')%I.
-
-  Definition exist {A : Type} (P : A -> perm) : @perm Σ :=
-    λ tid, (∃ x, P x tid)%I.
-
-  Definition sep (ρ1 ρ2 : perm) : @perm Σ :=
-    λ tid, (ρ1 tid ∗ ρ2 tid)%I.
-
-  Global Instance top : Top (@perm Σ) :=
-    λ _, True%I.
-(*
-  Definition perm_incl (ρ1 ρ2 : perm) :=
-    ∀ tid, lft_ctx -∗ ρ1 tid ={⊤}=∗ ρ2 tid.
-
-  Global Instance perm_equiv : Equiv perm :=
-    λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1. *)
-End perm.
-
-Delimit Scope perm_scope with P.
-Bind Scope perm_scope with perm.
-
-Notation "ν ◁ ty" := (has_type ν%E ty)
-  (at level 75, right associativity) : perm_scope.
-
-Notation "κ ∋ ρ" := (extract κ ρ)
-  (at level 75, right associativity) : perm_scope.
-
-Notation "q .[ κ ]" := (tok κ q) (format "q .[ κ ]", at level 0) : perm_scope.
-
-Notation "† κ" := (killable κ) (format "† κ", at level 75).
-
-Infix "⊑" := incl (at level 70) : perm_scope.
-
-Notation "∃ x .. y , P" :=
-  (exist (λ x, .. (exist (λ y, P)) ..)) : perm_scope.
-
-Infix "∗" := sep (at level 80, right associativity) : perm_scope.
-(*
-Infix "⇒" := perm_incl (at level 95, no associativity) : C_scope.
-Notation "(⇒)" := perm_incl (only parsing) : C_scope.
-
-Notation "ρ1 ⇔ ρ2" := (equiv (A:=perm) ρ1%P ρ2%P)
-   (at level 95, no associativity) : C_scope.
-Notation "(⇔)" := (equiv (A:=perm)) (only parsing) : C_scope.
-*)
-Section has_type.
-  Context `{typeG Σ}.
-
-  Lemma has_type_value (v : val) ty tid :
-    (v ◁ ty)%P tid ⊣⊢ ty.(ty_own) tid [v].
-  Proof.
-    destruct v as [|f xl e ?]. done.
-    unfold has_type, eval_expr, of_val.
-    assert (Rec f xl e = RecV f xl e) as -> by done. by rewrite to_of_val.
-  Qed.
-
-  Lemma has_type_wp E (ν : expr) ty tid (Φ : val -> iProp _) :
-    (ν ◁ ty)%P tid -∗
-    (∀ (v : val), ⌜eval_expr ν = Some v⌝ -∗ (v ◁ ty)%P tid ={E}=∗ Φ v) -∗
-    WP ν @ E {{ Φ }}.
-  Proof.
-    iIntros "H◁ HΦ". setoid_rewrite has_type_value. unfold has_type.
-    destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]".
-    iMod ("HΦ" $! v with "[] H◁") as "HΦ". done.
-    iInduction ν as [| | |[] e ? [|[]| | | | | | | | | |] _| | | | | | | |] "IH"
-      forall (Φ v EQν); try done.
-    - inversion EQν. subst. wp_value. auto.
-    - wp_value. auto.
-    - wp_bind e. simpl in EQν. destruct (eval_expr e) as [[[|l|]|]|]; try done.
-      iApply ("IH" with "[] [HΦ]"). done. simpl. wp_op. inversion EQν. eauto.
-  Qed.
-End has_type.

theories/typing/typing.v

-From iris.program_logic Require Import hoare.
-From iris.base_logic Require Import big_op.
-From lrust.lang Require Export notation memcpy.
-From lrust.typing Require Export type.
-From lrust.typing Require Import perm lft_contexts type_context cont_context.
-From lrust.lang Require Import proofmode.
-From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
-
-(* TODO: This is all still using the outdated type system. *)
-
-Section typing.
-  Context `{typeG Σ}.
-
-  (* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
-  Definition typed_step (ρ : perm) e (θ : val → perm) :=
-    ∀ tid, {{ heap_ctx ∗ lft_ctx ∗ ρ tid ∗ na_own tid ⊤ }} e
-           {{ v, θ v tid ∗ na_own tid ⊤ }}.
-
-  Definition typed_step_ty (ρ : perm) e ty :=
-    typed_step ρ e (λ ν, ν ◁ ty)%P.
-
-End typing.