From stdpp Require Import binders strings stringmap.
From iris.base_logic Require Import lib.iprop.
Set Implicit Arguments.
(* Nicer error messages. Instead of being asked to prove `False`,
    you are asked to prove `error (hopefully useful message)`.
*)
Module Type errorT.
    Parameter error : ∀ {T : Type}, T -> Prop.
    Axiom error_elim : ∀ {msgType} {msg : msgType} {T}, error msg -> T.
End errorT.
Module Export error : errorT.
    Definition error {T} (msg : T) := False.
    Theorem error_elim {msgType} (msg : msgType) T : error msg -> T. Proof. elim. Qed.
End error.
Inductive context Σ : Type :=
    | CEmpty
    | CVar of string & iProp Σ
    | CAnd of context Σ & context Σ
    | CSep of context Σ & context Σ
.
Definition c_sep {Σ} (c1 c2 : context Σ) := 
    if c1 is CEmpty _ then c2 else if c2 is CEmpty _ then c1 else CSep c1 c2.
Definition c_and {Σ} (c1 c2 : context Σ) := 
    if c1 is CEmpty _ then c2 else if c2 is CEmpty _ then c1 else CAnd c1 c2.
    
Fixpoint bind {Σ} (var : string) (c : context Σ) : context Σ 
:= match c with
    | CEmpty _ => CEmpty _
    | CVar var' P => if decide (var = var') then CEmpty _ else CVar var' P
    | CAnd c1 c2 => c_and (bind var c1) (bind var c2)
    | CSep c1 c2 => c_sep (bind var c1) (bind var c2)
end.
Fixpoint prop_of_ctx {Σ} (c : context Σ) : iProp Σ := match c with
    | CEmpty _ => True
    | CVar _ P => P
    | CAnd c1 c2 => prop_of_ctx c1 ∧ prop_of_ctx c2
    | CSep c1 c2 => prop_of_ctx c1 ∗ prop_of_ctx c2
end.
Lemma c_sep_spec {Σ} (c1 c2 : context Σ) 
    : prop_of_ctx (c_sep c1 c2) ⊣⊢ prop_of_ctx (CSep c1 c2).
Proof.
    by case c1; case c2; intros; simpl; 
        try rewrite bi.emp_sep; try rewrite bi.sep_emp.
Qed.
Lemma c_and_spec {Σ} (c1 c2 : context Σ) 
    : prop_of_ctx (c_and c1 c2) ⊣⊢ prop_of_ctx (CAnd c1 c2).
Proof.
    by case c1; case c2; intros; simpl;
        try rewrite bi.True_and; try rewrite bi.and_True.
Qed.
(* Purpose of ctx_uses:
    - Only used in constraint generation
    - Generates equality constraints, if variable is repeated
    - Decides whether the variable needs to be persistent.
    - No, it is also used in bind_spec.
    - MUST determine whether variable needs to be persistent.
    - MUST allow generation of equality constraints.
    - SHOULD allow easy definition of bind_spec.
    option (constraints * iProp * uses)
*)
Inductive uses := One | Many.
(* Returns:
    - Whether the variable must be persistent.
    - The type of the variable.
    - The generated equality constraints.
*)
Fixpoint ctx_uses {Σ} (var : string) (c : context Σ)
    : option (uses * iProp Σ * Prop)
    := match c with
        | CEmpty _ => None
        | CVar var' P =>
            if decide (var = var') 
            then Some (One, P, True)
            else None
        | CAnd c1 c2 =>
            union_with
                (λ '(u1, P1, constraints1) '(u2, P2, constraints2), Some
                    ( match u1, u2 with One, One => One | _, _ => Many end
                    , P1
                    , constraints1 ∧ constraints2 ∧ P1 = P2
                    )
                )
                (ctx_uses var c1)
                (ctx_uses var c2)
        | CSep c1 c2 =>
            union_with
                (λ '(u1, P1, constraints1) '(u2, P2, constraints2), Some
                    ( Many
                    , P1
                    , constraints1 ∧ constraints2 ∧ P1 = P2
                    )
                )
                (ctx_uses var c1)
                (ctx_uses var c2)
    end.
Lemma bind_spec {Σ} var (c : context Σ)
    : match ctx_uses var c with
        | None => prop_of_ctx (bind var c) ⊢ prop_of_ctx c
        | Some (uses, P, constraints) => 
            constraints -> 
            prop_of_ctx (bind var c) ∗ 
            (match uses with One => P | Many => □P end) ⊢ 
            prop_of_ctx c
    end.
Proof.
    have: ∀ u (P : iProp Σ), □ P ⊢ match u with One => P | Many => □ P end.
    { case. apply: bi.intuitionistically_elim. done. }
    move=> lemma1.
    have: ∀ u (P : iProp Σ), match u with One => P | Many => □ P end ⊢ P.
    { case. done. apply: bi.intuitionistically_elim. }
    move=> lemma2.
    elim c; simpl.
    - done.
    - move=> var' P.
        case: (decide (var = var')).
        + by rewrite bi.emp_sep.
        + done.
    - move=> c1; case: (ctx_uses var c1) => [[[u1 P1] constraints1]|] H1;
        move=> c2; case: (ctx_uses var c2) => [[[u2 P2] constraints2]|] H2;
        simpl; rewrite c_and_spec; simpl;
        [ move=>[/H1 w1 [/H2 w2 eq]] 
        | move: H2 => w2 /H1 w1 
        | move: H1 => w1 /H2 w2 
        | move: H1 H2 => w1 w2
        ];
        (apply: transitivity; last (apply: bi.and_mono; [apply: w1 | apply: w2])).
        + rewrite eq.
            apply: transitivity; first apply: bi.sep_and_r.
            apply: bi.and_mono; apply: bi.sep_mono_r.
            * case u1; last done.
                apply: transitivity; last apply: (lemma2 u2).
                by case u2.
            * case u2; last by case u1.
                apply: transitivity; last apply: (lemma2 u1).
                by case u1.
            + apply: transitivity; first apply: bi.sep_and_r.
            apply: bi.and_mono; first done.
            rewrite -{2}[prop_of_ctx _]bi.sep_emp.
            apply: bi.sep_mono; first done.
            apply: bi.True_intro.
        + apply: transitivity; first apply: bi.sep_and_r.
            apply: bi.and_mono; last done.
            rewrite -{2}[prop_of_ctx _]bi.sep_emp.
            apply: bi.sep_mono; first done.
            apply: bi.True_intro.
        + done.
    - move=> c1; case: (ctx_uses var c1) => [[[u1 P1] constraints1]|] H1;
        move=> c2; case: (ctx_uses var c2) => [[[u2 P2] constraints2]|] H2;
        simpl; rewrite c_sep_spec; simpl;
        [ move=>[/H1 w1 [/H2 w2 eq]] 
        | move: H2 => w2 /H1 w1 
        | move: H1 => w1 /H2 w2 
        | move: H1 H2 => w1 w2
        ];
        (apply: transitivity; last (apply: bi.sep_mono; [apply: w1 | apply: w2])).
        + apply: transitivity; 
            last (apply: bi.sep_mono; apply: bi.sep_mono_r; apply: lemma1).
            rewrite eq {1}bi.intuitionistically_sep_dup.
            rewrite bi.sep_assoc bi.sep_assoc; apply: bi.sep_mono_l.
            rewrite -bi.sep_assoc -bi.sep_assoc; apply: bi.sep_mono_r.
            by rewrite bi.sep_comm.
        + by rewrite 
            -bi.sep_assoc 
            [(prop_of_ctx (bind var c2) ∗ _)%I]bi.sep_comm
            bi.sep_assoc.
        + by rewrite bi.sep_assoc.
        + done.
Qed.
    
Inductive expr {Σ : gFunctors} : context Σ -> iProp Σ -> Type :=
    | Pair {c1 c2 T1 T2} : expr c1 T1 -> expr c2 T2 -> expr (c_sep c1 c2) (T1 ∗ T2)
    | Var {T} : ∀ var, expr (CVar var T) T
    | Lam {ctx T1 T2} 
        : ∀ var {constraints : match ctx_uses var ctx with
            | None => True
            | Some (uses, type, constraints) =>
                constraints ∧ type = T1 ∧ match uses with 
                    | Many => error 
                        ( "A linear variable was used multiple times.", var )
                    | One => True
                end
        end },
        expr ctx T2 ->
        expr (bind var ctx) (T1 -∗ T2)
.
Lemma check_expr {Σ ctx} (type : iProp Σ) : 
    expr ctx type -> prop_of_ctx ctx ⊢ type.
Proof.
    elim.
    - move=> ctx1 ctx2 type1 type2 e1 fact1 e2 fact2.
        rewrite c_sep_spec.
        by apply: bi.sep_mono.
    - done.
    - move=> ctx1 type1 type2 var w e fact1.
        move: (bind_spec var ctx1) w.
        case: (ctx_uses var ctx1) => [[[uses P] constraint]|].
        + case uses; last (move=> _ [_ [_ err]]; apply: (error_elim err)).
            move=> H2 [/H2 fact2 [<- []]].
            apply: bi.wand_intro_r.
            apply: transitivity.
            * apply: fact2.
            * apply: fact1.
        + move=> fact2 [].
            apply: bi.wand_intro_r.
            rewrite -[type2]bi.sep_emp.
            apply: bi.sep_mono.
            * apply: transitivity; [apply: fact2 | apply: fact1].
            * apply: bi.True_intro.
Qed.
Theorem check_program {Σ} (type : iProp Σ) : 
    expr (CEmpty _) type -> ⊢ type.
Proof.
    exact: check_expr.
Qed.
(* Example Proof. *)
Goal forall {Σ} (P Q : iProp Σ), ⊢ P -∗ Q -∗ Q ∗ P.
    move=> Σ P Q.
    by apply: (check_program (Lam "x" (Lam "y" (Pair (Var "y") (Var "x"))))).
Qed.

# My TODO list
## Short term
- Expand the language.
    - Import theorems from outside.
    - Pattern matching.
    - Update monad.
- Add notations.
- Generalize the language to work for an arbitrary BI, rather than specifically iProp.
    - This would require changing it from an *affine* language to a *linear* one.
## Long term
- Explore the idea of combining this with a normal programming language.
    - As in, combine the analysis language with the language it's analyzing.

This project is an exploration of that idea.

This project is an exploration of that idea.
## Versioning
Developed using:
- Coq 8.13.2
- Iris dev.2021-12-17.0.72485828