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 HaskLiterals.
  13 Require Import HaskTyCons.
  14 Require Import HaskStrongTypes.
  15 Require Import HaskWeakVars.
  16 Require Import HaskCoreVars.
  17
  18 Section HaskStrong.
  19
  20   (* any type with decidable equality may be used to represent value variables *)
  21   Context `{EQD_VV:EqDecidable VV}.
  22
  23   (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *)
  24   Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)}{sac:@StrongAltCon tc} :=
  25   { scbwv_exprvars          :  vec VV (sac_numExprVars sac)
  26   ; scbwv_exprvars_distinct :  distinct (vec2list scbwv_exprvars)
  27   ; scbwv_varstypes         := vec_zip scbwv_exprvars (sac_types sac Γ atypes)
  28   ; scbwv_xi                := fun ξ lev =>  update_xi (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes)
  29   }.
  30   Implicit Arguments StrongCaseBranchWithVVs [[Γ]].
  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: forall Γ Δ ξ   (g:Global Γ) v lev,                                                      Expr Γ Δ ξ (g v @@ lev)
  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_xi ξ l ((ev,t1)::nil)) (t2@@l)      -> Expr Γ Δ ξ (t1--->t2@@l)
  41   | ELet   : ∀ Γ Δ ξ tv t  l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_xi ξ 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_gamma sac Γ)
  59                                    (sac_delta sac Γ atypes (weakCK'' Δ))
  60                                    (scbwv_xi scb ξ l)
  61                                    (weakLT' (tbranches@@l)) } } ->
  62                Expr Γ Δ ξ (tbranches @@ l)
  63
  64   | ELetRec  : ∀ Γ Δ ξ l τ vars,
  65     distinct (leaves (mapOptionTree (@fst _ _) vars)) ->
  66     let ξ' := update_xi ξ l (leaves vars) in
  67     ELetRecBindings Γ Δ ξ'     l vars ->
  68     Expr            Γ Δ ξ' (τ@@l) ->
  69     Expr            Γ Δ ξ  (τ@@l)
  70
  71   (* 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 *)
  72   with ELetRecBindings : ∀ Γ, CoercionEnv Γ -> (VV -> LeveledHaskType Γ ★) -> HaskLevel Γ -> Tree ??(VV*HaskType Γ ★) -> Type :=
  73   | ELR_nil    : ∀ Γ Δ ξ l  ,                                                                 ELetRecBindings Γ Δ ξ l []
  74   | ELR_leaf   : ∀ Γ Δ ξ l v t,                                        Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [(v,t)]
  75   | ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2)
  76   .
  77
  78   Context {ToStringVV:ToString VV}.
  79   Context {ToLatexVV:ToLatex VV}.
  80   Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string :=
  81     match exp with
  82     | EVar  Γ' _ ξ' ev              => "var."+++ toString ev
  83     | EGlobal Γ' _ ξ'   g v _       => "global." +++ toString (g:CoreVar)
  84     | ELam  Γ'   _ _ tv _ _ cv e    => "\("+++ toString cv +++":t) -> "+++ exprToString e
  85     | ELet  Γ' _ _ t _ _ ev e1 e2   => "let "+++toString ev+++" = "+++exprToString e1+++" in "+++exprToString e2
  86     | ELit  _ _ _ lit _             => "lit."+++toString lit
  87     | EApp  Γ' _ _ _ _ _ e1 e2      => "("+++exprToString e1+++")("+++exprToString e2+++")"
  88     | EEsc  Γ' _ _ ec t _ e         => "~~("+++exprToString e+++")"
  89     | EBrak Γ' _ _ ec t _ e         => "<["+++exprToString e+++"]>"
  90     | ENote _ _ _ _ n e             => "note."+++exprToString e
  91     | ETyApp  Γ Δ κ σ τ ξ l       e => "("+++exprToString e+++")@("+++toString τ+++")"
  92     | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => "("+++exprToString e+++")~(co)"
  93     | ECast Γ Δ ξ t1 t2 γ l e       => "cast ("+++exprToString e+++"):t2"
  94     | ETyLam _ _ _ k _ _ e          => "\@_ ->"+++ exprToString e
  95     | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => "\~_ ->"+++ exprToString e
  96     | ECase Γ Δ ξ l tc branches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME"
  97     | ELetRec _ _ _ _ _ vars vu elrb e => "letrec FIXME in " +++ exprToString e
  98     end.
  99   Instance ExprToString Γ Δ ξ τ : ToString (Expr Γ Δ ξ τ) := { toString := exprToString }.
 100
 101 End HaskStrong.
 102 Implicit Arguments StrongCaseBranchWithVVs [[Γ]].