1 (*********************************************************************************************************************************)
2 (* HaskStrong: a dependently-typed version of CoreSyn *)
3 (*********************************************************************************************************************************)
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.
16 (* any type with decidable equality may be used to represent value variables *)
17 Context `{EQD_VV:EqDecidable VV}.
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))
25 Implicit Arguments ExprCaseBranch [[n][Γ]].
26 Coercion cbi_sacic : ExprCaseBranch >-> StrongAltConInContext.
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)
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)
50 | ELetRec : ∀ Γ Δ ξ l τ vars, let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ l))) (leaves vars)) in
51 ELetRecBindings Γ Δ ξ' l (mapOptionTree (@snd _ _) vars) ->
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)