src/HaskStrong.v

   1 (*********************************************************************************************************************************)
   2 (* HaskStrong: a dependently-typed version of CoreSyn                                                                            *)
   3 (*********************************************************************************************************************************)
   4
   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.
  15
  16 Section HaskStrong.
  17
  18   (* any type with decidable equality may be used to represent value variables *)
  19   Context `{EQD_VV:EqDecidable VV}.
  20
  21   (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *)
  22
  23   Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)}{sac:@StrongAltCon tc} :=
  24   { scbwv_exprvars          :  vec VV (sac_numExprVars sac)
  25   ; scbwv_exprvars_distinct :  distinct (vec2list scbwv_exprvars)
  26   ; scbwv_varstypes         := vec_zip scbwv_exprvars (sac_types sac Γ atypes)
  27   ; scbwv_ξ                 := fun ξ lev =>  update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes)
  28   }.
  29   Implicit Arguments StrongCaseBranchWithVVs [[Γ]].
  30   (*Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon.*)
  31
  32   Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type :=
  33
  34   (* an "EGlobal" is any variable which is free in the expression which was passed to -fcoqpass (ie bound outside it) *)
  35   | EGlobal: ∀ Γ Δ ξ t,       WeakExprVar ->                                                         Expr Γ Δ ξ t
  36
  37   | EVar   : ∀ Γ Δ ξ ev,                                                                             Expr Γ Δ ξ (ξ ev)
  38   | ELit   : ∀ Γ Δ ξ lit   l,                                                                        Expr Γ Δ ξ (literalType lit@@l)
  39   | EApp   : ∀ Γ Δ ξ t1 t2 l,        Expr Γ Δ ξ (t2--->t1 @@ l)   -> Expr Γ Δ ξ (t2 @@ l)         -> Expr Γ Δ ξ (t1 @@ l)
  40   | ELam   : ∀ Γ Δ ξ t1 t2 l ev,              Expr Γ Δ (update_ξ ξ l ((ev,t1)::nil)) (t2@@l)      -> Expr Γ Δ ξ (t1--->t2@@l)
  41   | ELet   : ∀ Γ Δ ξ tv t  l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ l ((ev,tv)::nil))(t@@l)  -> Expr Γ Δ ξ (t@@l)
  42   | EEsc   : ∀ Γ Δ ξ ec t  l,     Expr Γ Δ ξ (<[ ec |- t ]> @@ l)                                 -> Expr Γ Δ ξ (t @@ (ec::l))
  43   | EBrak  : ∀ Γ Δ ξ ec t  l,     Expr Γ Δ ξ (t @@ (ec::l))                                       -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l)
  44   | ECast  : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l,
  45     Expr Γ Δ ξ (t1 @@ l)                        -> Expr Γ Δ ξ (t2 @@ l)
  46   | ENote  : ∀ Γ Δ ξ t, Note                      -> Expr Γ Δ ξ t                                 -> Expr Γ Δ ξ t
  47   | ETyApp : ∀ Γ Δ κ σ τ ξ l,                    Expr Γ Δ ξ (HaskTAll κ σ @@ l)                   -> Expr Γ Δ ξ (substT σ τ @@ l)
  48   | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l,
  49     Expr Γ (σ₁∼∼∼σ₂::Δ) ξ (σ @@ l)    -> Expr Γ Δ ξ (σ₁∼∼σ₂    ⇒ σ @@ l)
  50   | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l,
  51     Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ @@ l)            -> Expr Γ Δ ξ (σ        @@l)
  52   | ETyLam : ∀ Γ Δ ξ κ σ l,
  53     Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l)
  54   | ECase    : forall Γ Δ ξ l tc tbranches atypes,
  55                Expr Γ Δ ξ (caseType tc atypes @@ l) ->
  56                Tree ??{ sac : _
  57                     & { scb : StrongCaseBranchWithVVs tc atypes sac
  58                     &         Expr (sac_Γ sac Γ)
  59                                    (sac_Δ sac Γ atypes (weakCK'' Δ))
  60                                    (scbwv_ξ scb ξ l)
  61                                    (weakLT' (tbranches@@l)) } } ->
  62                Expr Γ Δ ξ (tbranches @@ l)
  63
  64   | ELetRec  : ∀ Γ Δ ξ l τ vars,
  65     let ξ' := update_ξ ξ l (leaves vars) in
  66     ELetRecBindings Γ Δ ξ'     l vars ->
  67     Expr            Γ Δ ξ' (τ@@l) ->
  68     Expr            Γ Δ ξ  (τ@@l)
  69
  70   (* 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 *)
  71   with ELetRecBindings : ∀ Γ, CoercionEnv Γ -> (VV -> LeveledHaskType Γ ★) -> HaskLevel Γ -> Tree ??(VV*HaskType Γ ★) -> Type :=
  72   | ELR_nil    : ∀ Γ Δ ξ l  ,                                                                 ELetRecBindings Γ Δ ξ l []
  73   | ELR_leaf   : ∀ Γ Δ ξ l v t,                                        Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [(v,t)]
  74   | ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2)
  75   .
  76
  77
  78   Context {ToStringVV:ToString VV}.
  79
  80   Require Import HaskCoreVars.
  81
  82   Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string :=
  83     match exp with
  84     | EVar  Γ' _ ξ' ev              => "var."+++ev
  85     | EGlobal Γ' _ ξ' t wev         => "global." +++(wev:CoreVar)
  86     | ELam  Γ'   _ _ tv _ _ cv e    => "\("+++cv+++":t) -> "+++ exprToString e
  87     | ELet  Γ' _ _ t _ _ ev e1 e2   => "let "+++ev+++" = "+++exprToString e1+++" in "+++exprToString e2
  88     | ELit  _ _ _ lit _             => "lit."+++lit
  89     | EApp  Γ' _ _ _ _ _ e1 e2      => "("+++exprToString e1+++")("+++exprToString e2+++")"
  90     | EEsc  Γ' _ _ ec t _ e         => "~~("+++exprToString e+++")"
  91     | EBrak Γ' _ _ ec t _ e         => "<["+++exprToString e+++"]>"
  92     | ENote _ _ _ _ n e             => "note."+++exprToString e
  93     | ETyApp  Γ Δ κ σ τ ξ l       e => "("+++exprToString e+++")@("+++τ+++")"
  94     | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => "("+++exprToString e+++")~(co)"
  95     | ECast Γ Δ ξ t1 t2 γ l e       => "cast ("+++exprToString e+++"):t2"
  96     | ETyLam _ _ _ k _ _ e          => "\@_ ->"+++ exprToString e
  97     | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => "\~_ ->"+++ exprToString e
  98     | ECase Γ Δ ξ l tc tbranches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME"
  99     | ELetRec _ _ _ _ _ vars elrb e => "letrec FIXME in " +++ exprToString e
 100     end.
 101   Instance ExprToString Γ Δ ξ τ : ToString (Expr Γ Δ ξ τ) := { toString := exprToString }.
 102
 103 End HaskStrong.
 104 Implicit Arguments StrongCaseBranchWithVVs [[Γ]].