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 Require Import HaskCoreVars.
  16
  17 Section HaskStrong.
  18
  19   (* any type with decidable equality may be used to represent value variables *)
  20   Context `{EQD_VV:EqDecidable VV}.
  21
  22   (* 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)}{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
  31   Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type :=
  32
  33   (* an "EGlobal" is any variable which is free in the expression which was passed to -fcoqpass (ie bound outside it) *)
  34   | EGlobal: forall Γ Δ ξ   (g:Global Γ) v lev,                                                      Expr Γ Δ ξ (g v @@ lev)
  35
  36   | EVar   : ∀ Γ Δ ξ ev,                                                                             Expr Γ Δ ξ (ξ ev)
  37   | ELit   : ∀ Γ Δ ξ lit   l,                                                                        Expr Γ Δ ξ (literalType lit@@l)
  38   | EApp   : ∀ Γ Δ ξ t1 t2 l,        Expr Γ Δ ξ (t2--->t1 @@ l)   -> Expr Γ Δ ξ (t2 @@ l)         -> Expr Γ Δ ξ (t1 @@ l)
  39   | ELam   : ∀ Γ Δ ξ t1 t2 l ev,              Expr Γ Δ (update_ξ ξ l ((ev,t1)::nil)) (t2@@l)      -> Expr Γ Δ ξ (t1--->t2@@l)
  40   | ELet   : ∀ Γ Δ ξ tv t  l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ l ((ev,tv)::nil))(t@@l)  -> Expr Γ Δ ξ (t@@l)
  41   | EEsc   : ∀ Γ Δ ξ ec t  l,     Expr Γ Δ ξ (<[ ec |- t ]> @@ l)                                 -> Expr Γ Δ ξ (t @@ (ec::l))
  42   | EBrak  : ∀ Γ Δ ξ ec t  l,     Expr Γ Δ ξ (t @@ (ec::l))                                       -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l)
  43   | ECast  : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l,
  44     Expr Γ Δ ξ (t1 @@ l)                        -> Expr Γ Δ ξ (t2 @@ l)
  45   | ENote  : ∀ Γ Δ ξ t, Note                      -> Expr Γ Δ ξ t                                 -> Expr Γ Δ ξ t
  46   | ETyApp : ∀ Γ Δ κ σ τ ξ l,                    Expr Γ Δ ξ (HaskTAll κ σ @@ l)                   -> Expr Γ Δ ξ (substT σ τ @@ l)
  47   | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l,
  48     Expr Γ (σ₁∼∼∼σ₂::Δ) ξ (σ @@ l)    -> Expr Γ Δ ξ (σ₁∼∼σ₂    ⇒ σ @@ l)
  49   | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l,
  50     Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ @@ l)            -> Expr Γ Δ ξ (σ        @@l)
  51   | ETyLam : ∀ Γ Δ ξ κ σ l,
  52     Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l)
  53   | ECase    : forall Γ Δ ξ l tc tbranches atypes,
  54                Expr Γ Δ ξ (caseType tc atypes @@ l) ->
  55                Tree ??{ sac : _
  56                     & { scb : StrongCaseBranchWithVVs tc atypes sac
  57                     &         Expr (sac_Γ sac Γ)
  58                                    (sac_Δ sac Γ atypes (weakCK'' Δ))
  59                                    (scbwv_ξ scb ξ l)
  60                                    (weakLT' (tbranches@@l)) } } ->
  61                Expr Γ Δ ξ (tbranches @@ l)
  62
  63   | ELetRec  : ∀ Γ Δ ξ l τ vars,
  64     distinct (leaves (mapOptionTree (@fst _ _) 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   Context {ToStringVV:ToString VV}.
  78   Context {ToLatexVV:ToLatex VV}.
  79   Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string :=
  80     match exp with
  81     | EVar  Γ' _ ξ' ev              => "var."+++ toString ev
  82     | EGlobal Γ' _ ξ'   g v _       => "global." +++ toString (g:CoreVar)
  83     | ELam  Γ'   _ _ tv _ _ cv e    => "\("+++ toString cv +++":t) -> "+++ exprToString e
  84     | ELet  Γ' _ _ t _ _ ev e1 e2   => "let "+++toString ev+++" = "+++exprToString e1+++" in "+++exprToString e2
  85     | ELit  _ _ _ lit _             => "lit."+++toString lit
  86     | EApp  Γ' _ _ _ _ _ e1 e2      => "("+++exprToString e1+++")("+++exprToString e2+++")"
  87     | EEsc  Γ' _ _ ec t _ e         => "~~("+++exprToString e+++")"
  88     | EBrak Γ' _ _ ec t _ e         => "<["+++exprToString e+++"]>"
  89     | ENote _ _ _ _ n e             => "note."+++exprToString e
  90     | ETyApp  Γ Δ κ σ τ ξ l       e => "("+++exprToString e+++")@("+++toString τ+++")"
  91     | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => "("+++exprToString e+++")~(co)"
  92     | ECast Γ Δ ξ t1 t2 γ l e       => "cast ("+++exprToString e+++"):t2"
  93     | ETyLam _ _ _ k _ _ e          => "\@_ ->"+++ exprToString e
  94     | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => "\~_ ->"+++ exprToString e
  95     | ECase Γ Δ ξ l tc branches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME"
  96     | ELetRec _ _ _ _ _ vars vu elrb e => "letrec FIXME in " +++ exprToString e
  97     end.
  98   Instance ExprToString Γ Δ ξ τ : ToString (Expr Γ Δ ξ τ) := { toString := exprToString }.
  99
 100 End HaskStrong.
 101 Implicit Arguments StrongCaseBranchWithVVs [[Γ]].