src/HaskStrong.v

   1 (*********************************************************************************************************************************)
   2 (* HaskStrong: a dependently-typed version of CoreSyn                                                                            *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import Coq.Strings.String.
   9 Require Import Coq.Lists.List.
  10 Require Import HaskGeneral.
  11 Require Import HaskLiterals.
  12 Require Import HaskStrongTypes.
  13
  14 Section HaskStrong.
  15
  16   (* any type with decidable equality may be used to represent value variables *)
  17   Context `{EQD_VV:EqDecidable VV}.
  18
  19   (* a ExprCaseBranch contains all the data found in a case branch except the expression itself *)
  20   Record ExprCaseBranch {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} :=
  21   { cbi_sacic     :  @StrongAltConInContext n tc Γ atypes
  22   ; cbi_vars      :  vec VV (tagNumValVars (cbi_tag cbi_sacic))
  23   ; cbi_varstypes := vec2list (vec_zip cbi_vars (cbi_types cbi_sacic))
  24   }.
  25   Implicit Arguments ExprCaseBranch [[n][Γ]].
  26   Coercion cbi_sacic : ExprCaseBranch >-> StrongAltConInContext.
  27
  28   Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ) -> LeveledHaskType Γ -> Type :=
  29   | EVar   : ∀ Γ Δ ξ ev,                                                                             Expr Γ Δ ξ (ξ ev)
  30   | ELit   : ∀ Γ Δ ξ lit   l,                                                                        Expr Γ Δ ξ (literalType lit@@l)
  31   | EApp   : ∀ Γ Δ ξ t1 t2 l,        Expr Γ Δ ξ (t2--->t1 @@ l)   -> Expr Γ Δ ξ (t2 @@ l)         -> Expr Γ Δ ξ (t1 @@ l)
  32   | ELam   : ∀ Γ Δ ξ t1 t2 l ev, Γ ⊢ᴛy t1:★ ->Expr Γ Δ (update_ξ ξ ((ev,t1@@l)::nil)) (t2@@l)     -> Expr Γ Δ ξ (t1--->t2@@l)
  33   | ELet   : ∀ Γ Δ ξ tv t  l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ ((ev,tv@@l)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l)
  34   | EEsc   : ∀ Γ Δ ξ ec t  l,     Expr Γ Δ ξ (<[ ec |- t ]> @@ l)                                 -> Expr Γ Δ ξ (t @@ (ec::l))
  35   | EBrak  : ∀ Γ Δ ξ ec t  l,     Expr Γ Δ ξ (t @@ (ec::l))                                       -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l)
  36   | ECast  : ∀ Γ Δ ξ γ t1 t2 l, Δ ⊢ᴄᴏ γ : t1 ∼ t2 ->  Expr Γ Δ ξ (t1 @@ l)                        -> Expr Γ Δ ξ (t2 @@ l)
  37   | ENote  : ∀ Γ Δ ξ t, Note                      -> Expr Γ Δ ξ t                                 -> Expr Γ Δ ξ t
  38   | ETyApp : ∀ Γ Δ κ σ τ ξ l,     Γ ⊢ᴛy τ : κ -> Expr Γ Δ ξ (HaskTAll κ σ @@ l)                   -> Expr Γ Δ ξ (substT σ τ @@ l)
  39   | ECoLam : ∀ Γ Δ κ σ σ₁ σ₂ ξ l,   Γ ⊢ᴛy σ₁:κ -> Γ ⊢ᴛy σ₂:κ -> Expr Γ (σ₁∼∼∼σ₂::Δ) ξ (σ @@ l)    -> Expr Γ Δ ξ (σ₁∼∼σ₂ :κ ⇒ σ @@ l)
  40   | ECoApp : ∀ Γ Δ κ γ σ₁ σ₂ σ ξ l, Δ ⊢ᴄᴏ γ  : σ₁∼σ₂ -> Expr Γ Δ ξ (σ₁ ∼∼ σ₂ : κ ⇒ σ @@ l)        -> Expr Γ Δ ξ (σ        @@l)
  41   | ETyLam : ∀ Γ Δ ξ κ σ l,
  42     Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l)
  43
  44   | ECase    : forall Γ Δ ξ l n (tc:TyCon n) atypes tbranches,
  45                Expr Γ Δ ξ (caseType tc atypes @@ l) ->
  46                Tree ??{ scb : ExprCaseBranch tc atypes
  47                             & Expr (cbi_Γ scb) (cbi_Δ scb) (update_ξ (weakLT'○ξ) (cbi_varstypes scb)) (weakLT' (tbranches@@l)) } ->
  48                Expr Γ Δ ξ (tbranches @@ l)
  49
  50   | ELetRec  : ∀ Γ Δ ξ l τ vars, let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ l))) (leaves vars)) in
  51     ELetRecBindings Γ Δ ξ'     l (mapOptionTree (@snd _ _) vars) ->
  52     Expr            Γ Δ ξ' (τ@@l) ->
  53     Expr            Γ Δ ξ  (τ@@l)
  54
  55   (* can't avoid having an additional inductive: it is a tree of Expr's, each of whose ξ depends on the type of the entire tree *)
  56   with ELetRecBindings : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ) -> HaskLevel Γ -> Tree ??(HaskType Γ) -> Type :=
  57   | ELR_nil    : ∀ Γ Δ ξ l  ,                                                                 ELetRecBindings Γ Δ ξ l []
  58   | ELR_leaf   : ∀ Γ Δ ξ t l,                                          Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [t]
  59   | ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2)
  60   .
  61
  62 End HaskStrong.