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 HaskKinds.
11 Require Import HaskCoreTypes.
12 Require Import HaskLiteralsAndTyCons.
13 Require Import HaskStrongTypes.
14 Require Import HaskWeakVars.
18 (* any type with decidable equality may be used to represent value variables *)
19 Context `{EQD_VV:EqDecidable VV}.
21 (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *)
23 Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)} :=
24 { scbwv_sac : @StrongAltCon tc
25 ; scbwv_exprvars : vec VV (sac_numExprVars scbwv_sac)
26 ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes)
27 ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (vec2list
28 (vec_map (fun x => ((fst x),(snd x @@ weakL' lev))) scbwv_varstypes))
30 Implicit Arguments StrongCaseBranchWithVVs [[Γ]].
31 Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon.
33 Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type :=
35 (* an "EGlobal" is any variable which is free in the expression which was passed to -fcoqpass (ie bound outside it) *)
36 | EGlobal: ∀ Γ Δ ξ t, WeakExprVar -> Expr Γ Δ ξ t
38 | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev)
39 | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l)
40 | EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) -> Expr Γ Δ ξ (t1 @@ l)
41 | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_ξ ξ ((ev,t1@@l)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l)
42 | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ ((ev,tv@@l)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l)
43 | EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]> @@ l) -> Expr Γ Δ ξ (t @@ (ec::l))
44 | EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (t @@ (ec::l)) -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l)
45 | ECast : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l,
46 Expr Γ Δ ξ (t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l)
47 | ENote : ∀ Γ Δ ξ t, Note -> Expr Γ Δ ξ t -> Expr Γ Δ ξ t
48 | ETyApp : ∀ Γ Δ κ σ τ ξ l, Expr Γ Δ ξ (HaskTAll κ σ @@ l) -> Expr Γ Δ ξ (substT σ τ @@ l)
49 | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l,
50 Expr Γ (σ₁∼∼∼σ₂::Δ) ξ (σ @@ l) -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ @@ l)
51 | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l,
52 Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ @@ l) -> Expr Γ Δ ξ (σ @@l)
53 | ETyLam : ∀ Γ Δ ξ κ σ l,
54 Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l)
55 | ECase : forall Γ Δ ξ l tc tbranches atypes,
56 Expr Γ Δ ξ (caseType tc atypes @@ l) ->
57 Tree ??{ scb : StrongCaseBranchWithVVs tc atypes
59 (sac_Δ scb Γ atypes (weakCK'' Δ))
61 (weakLT' (tbranches@@l)) } ->
62 Expr Γ Δ ξ (tbranches @@ l)
64 | ELetRec : ∀ Γ Δ ξ l τ vars, let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ l))) (leaves vars)) in
65 ELetRecBindings Γ Δ ξ' l vars ->
69 (* 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 *)
70 with ELetRecBindings : ∀ Γ, CoercionEnv Γ -> (VV -> LeveledHaskType Γ ★) -> HaskLevel Γ -> Tree ??(VV*HaskType Γ ★) -> Type :=
71 | ELR_nil : ∀ Γ Δ ξ l , ELetRecBindings Γ Δ ξ l []
72 | ELR_leaf : ∀ Γ Δ ξ l v, Expr Γ Δ ξ (unlev (ξ v) @@ l) -> ELetRecBindings Γ Δ ξ l [(v,unlev (ξ v))]
73 | ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2)
77 Implicit Arguments StrongCaseBranchWithVVs [[Γ]].