- Implicit Arguments StrongCaseBranchWithVVs [[n][Γ]].
- Coercion scbwv_scb : StrongCaseBranchWithVVs >-> StrongCaseBranch.
-
- Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ) -> LeveledHaskType Γ -> Type :=
- | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev)
- | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l)
- | EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) -> Expr Γ Δ ξ (t1 @@ l)
- | ELam : ∀ Γ Δ ξ t1 t2 l ev, Γ ⊢ᴛy t1:★ ->Expr Γ Δ (update_ξ ξ ((ev,t1@@l)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l)
- | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ ((ev,tv@@l)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l)
- | EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]> @@ l) -> Expr Γ Δ ξ (t @@ (ec::l))
- | EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (t @@ (ec::l)) -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l)
- | ECast : ∀ Γ Δ ξ γ t1 t2 l, Δ ⊢ᴄᴏ γ : t1 ∼ t2 -> Expr Γ Δ ξ (t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l)
- | ENote : ∀ Γ Δ ξ t, Note -> Expr Γ Δ ξ t -> Expr Γ Δ ξ t
- | ETyApp : ∀ Γ Δ κ σ τ ξ l, Γ ⊢ᴛy τ : κ -> Expr Γ Δ ξ (HaskTAll κ σ @@ l) -> Expr Γ Δ ξ (substT σ τ @@ l)
- | ECoLam : ∀ Γ Δ κ σ σ₁ σ₂ ξ l, Γ ⊢ᴛy σ₁:κ -> Γ ⊢ᴛy σ₂:κ -> Expr Γ (σ₁∼∼∼σ₂::Δ) ξ (σ @@ l) -> Expr Γ Δ ξ (σ₁∼∼σ₂ :κ ⇒ σ @@ l)
- | ECoApp : ∀ Γ Δ κ γ σ₁ σ₂ σ ξ l, Δ ⊢ᴄᴏ γ : σ₁∼σ₂ -> Expr Γ Δ ξ (σ₁ ∼∼ σ₂ : κ ⇒ σ @@ l) -> Expr Γ Δ ξ (σ @@l)
- | ETyLam : ∀ Γ Δ ξ κ σ l,
- Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l)
-
- | ECase : forall Γ Δ ξ l n (tc:TyCon n) atypes tbranches,
- Expr Γ Δ ξ (caseType tc atypes @@ l) ->
- Tree ??{ scb : StrongCaseBranchWithVVs tc atypes
- & Expr (scb_Γ scb) (scb_Δ scb) (update_ξ (weakLT'○ξ) (scbwv_varstypes scb)) (weakLT' (tbranches@@l)) } ->
- Expr Γ Δ ξ (tbranches @@ l)
-
- | ELetRec : ∀ Γ Δ ξ l τ vars, let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ l))) (leaves vars)) in
- ELetRecBindings Γ Δ ξ' l vars ->
- Expr Γ Δ ξ' (τ@@l) ->
- Expr Γ Δ ξ (τ@@l)
+ Implicit Arguments StrongCaseBranchWithVVs [[Γ]].
+
+ Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> HaskType Γ ★ -> HaskLevel Γ -> Type :=
+
+ (* an "EGlobal" is any variable which is free in the expression which was passed to -fcoqpass (ie bound outside it) *)
+ | EGlobal: forall Γ Δ ξ (g:Global Γ) v lev, Expr Γ Δ ξ (g v) lev
+
+ | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (unlev (ξ ev)) (getlev (ξ ev))
+ | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit) l
+ | EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1) l -> Expr Γ Δ ξ t2 l -> Expr Γ Δ ξ (t1) l
+ | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_xi ξ l ((ev,t1)::nil)) t2 l -> Expr Γ Δ ξ (t1--->t2) l
+ | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ tv l ->Expr Γ Δ (update_xi ξ l ((ev,tv)::nil)) t l -> Expr Γ Δ ξ t l
+ | EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]>) l -> Expr Γ Δ ξ t (ec::l)
+ | EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ t (ec::l) -> Expr Γ Δ ξ (<[ ec |- t ]>) l
+ | ECast : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l, Expr Γ Δ ξ t1 l -> Expr Γ Δ ξ t2 l
+ | ENote : ∀ Γ Δ ξ t l, Note -> Expr Γ Δ ξ t l -> Expr Γ Δ ξ t l
+ | ETyApp : ∀ Γ Δ κ σ τ ξ l, Expr Γ Δ ξ (HaskTAll κ σ) l -> Expr Γ Δ ξ (substT σ τ) l
+ | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, Expr Γ (σ₁∼∼∼σ₂::Δ) ξ σ l -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ) l
+ | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ) l -> Expr Γ Δ ξ σ l
+ | ETyLam : ∀ Γ Δ ξ κ σ l n,
+ Expr (list_ins n κ Γ) (weakCE_ Δ) (weakLT_○ξ) (HaskTApp (weakF_ σ) (FreshHaskTyVar_ _)) (weakL_ l)-> Expr Γ Δ ξ (HaskTAll κ σ) l
+ | ECase : forall Γ Δ ξ l tc tbranches atypes,
+ Expr Γ Δ ξ (caseType tc atypes) l ->
+ Tree ??{ sac : _
+ & { scb : StrongCaseBranchWithVVs tc atypes sac
+ & Expr (sac_gamma sac Γ)
+ (sac_delta sac Γ atypes (weakCK'' Δ))
+ (scbwv_xi scb ξ l)
+ (weakT' tbranches)
+ (weakL' l) } } ->
+ Expr Γ Δ ξ tbranches l
+
+ | ELetRec : ∀ Γ Δ ξ l τ vars,
+ distinct (leaves (mapOptionTree (@fst _ _) vars)) ->
+ let ξ' := update_xi ξ l (leaves vars) in
+ ELetRecBindings Γ Δ ξ' l vars ->
+ Expr Γ Δ ξ' τ l ->
+ Expr Γ Δ ξ τ l