Require Import HaskLiteralsAndTyCons.
Require Import HaskStrongTypes.
Require Import HaskWeakVars.
+Require Import HaskCoreVars.
Section HaskStrong.
(* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *)
- Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)} :=
- { scbwv_sac : @StrongAltCon tc
- ; scbwv_exprvars : vec VV (sac_numExprVars scbwv_sac)
+ Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)}{sac:@StrongAltCon tc} :=
+ { scbwv_exprvars : vec VV (sac_numExprVars sac)
; scbwv_exprvars_distinct : distinct (vec2list scbwv_exprvars)
- ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes)
+ ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types sac Γ atypes)
; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes)
}.
Implicit Arguments StrongCaseBranchWithVVs [[Γ]].
- Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon.
+ (*Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon.*)
Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type :=
Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l)
| ECase : forall Γ Δ ξ l tc tbranches atypes,
Expr Γ Δ ξ (caseType tc atypes @@ l) ->
- Tree ??{ scb : StrongCaseBranchWithVVs tc atypes
- & Expr (sac_Γ scb Γ)
- (sac_Δ scb Γ atypes (weakCK'' Δ))
+ Tree ??{ sac : _
+ & { scb : StrongCaseBranchWithVVs tc atypes sac
+ & Expr (sac_Γ sac Γ)
+ (sac_Δ sac Γ atypes (weakCK'' Δ))
(scbwv_ξ scb ξ l)
- (weakLT' (tbranches@@l)) } ->
+ (weakLT' (tbranches@@l)) } } ->
Expr Γ Δ ξ (tbranches @@ l)
| ELetRec : ∀ Γ Δ ξ l τ vars,
| ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2)
.
-
Context {ToStringVV:ToString VV}.
-
- Require Import HaskCoreVars.
-
+ Context {ToLatexVV:ToLatex VV}.
Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string :=
match exp with
- | EVar Γ' _ ξ' ev => "var."+++ev
- | EGlobal Γ' _ ξ' t wev => "global." +++(wev:CoreVar)
- | ELam Γ' _ _ tv _ _ cv e => "\("+++cv+++":t) -> "+++ exprToString e
- | ELet Γ' _ _ t _ _ ev e1 e2 => "let "+++ev+++" = "+++exprToString e1+++" in "+++exprToString e2
- | ELit _ _ _ lit _ => "lit."+++lit
+ | EVar Γ' _ ξ' ev => "var."+++ toString ev
+ | EGlobal Γ' _ ξ' t wev => "global." +++ toString (wev:CoreVar)
+ | ELam Γ' _ _ tv _ _ cv e => "\("+++ toString cv +++":t) -> "+++ exprToString e
+ | ELet Γ' _ _ t _ _ ev e1 e2 => "let "+++toString ev+++" = "+++exprToString e1+++" in "+++exprToString e2
+ | ELit _ _ _ lit _ => "lit."+++toString lit
| EApp Γ' _ _ _ _ _ e1 e2 => "("+++exprToString e1+++")("+++exprToString e2+++")"
| EEsc Γ' _ _ ec t _ e => "~~("+++exprToString e+++")"
| EBrak Γ' _ _ ec t _ e => "<["+++exprToString e+++"]>"
| ENote _ _ _ _ n e => "note."+++exprToString e
- | ETyApp Γ Δ κ σ τ ξ l e => "("+++exprToString e+++")@("+++τ+++")"
+ | ETyApp Γ Δ κ σ τ ξ l e => "("+++exprToString e+++")@("+++toString τ+++")"
| ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => "("+++exprToString e+++")~(co)"
| ECast Γ Δ ξ t1 t2 γ l e => "cast ("+++exprToString e+++"):t2"
| ETyLam _ _ _ k _ _ e => "\@_ ->"+++ exprToString e