Require Import Coq.Lists.List.
Require Import HaskKinds.
Require Import HaskCoreTypes.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskStrongTypes.
Require Import HaskWeakVars.
Require Import HaskCoreVars.
Context `{EQD_VV:EqDecidable VV}.
(* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *)
-
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_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes)
}.
Implicit Arguments StrongCaseBranchWithVVs [[Γ]].
- (*Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon.*)
Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type :=
(* an "EGlobal" is any variable which is free in the expression which was passed to -fcoqpass (ie bound outside it) *)
- | EGlobal: ∀ Γ Δ ξ t, WeakExprVar -> Expr Γ Δ ξ t
+ | EGlobal: forall Γ Δ ξ (g:Global Γ) v lev, Expr Γ Δ ξ (g v @@ lev)
| EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev)
| ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l)
Expr Γ Δ ξ (tbranches @@ l)
| ELetRec : ∀ Γ Δ ξ l τ vars,
+ distinct (leaves (mapOptionTree (@fst _ _) vars)) ->
let ξ' := update_ξ ξ l (leaves vars) in
ELetRecBindings Γ Δ ξ' l vars ->
Expr Γ Δ ξ' (τ@@l) ->
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 Γ' _ ξ' g v _ => "global." +++ toString (g: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
| ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => "\~_ ->"+++ exprToString e
- | ECase Γ Δ ξ l tc tbranches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME"
- | ELetRec _ _ _ _ _ vars elrb e => "letrec FIXME in " +++ exprToString e
+ | ECase Γ Δ ξ l tc branches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME"
+ | ELetRec _ _ _ _ _ vars vu elrb e => "letrec FIXME in " +++ exprToString e
end.
Instance ExprToString Γ Δ ξ τ : ToString (Expr Γ Δ ξ τ) := { toString := exprToString }.