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 HaskCoreToWeak.
  17 Require Import HaskCoreVars.
  18
  19 Section HaskStrong.
  20
  21   (* any type with decidable equality may be used to represent value variables *)
  22   Context `{EQD_VV:EqDecidable VV}.
  23
  24   (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *)
  25   Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)}{sac:@StrongAltCon tc} :=
  26   { scbwv_exprvars          :  vec VV (sac_numExprVars sac)
  27   ; scbwv_exprvars_distinct :  distinct (vec2list scbwv_exprvars)
  28   ; scbwv_varstypes         := vec_zip scbwv_exprvars (sac_types sac Γ atypes)
  29   ; scbwv_xi                := fun ξ lev =>  update_xi (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes)
  30   }.
  31   Implicit Arguments StrongCaseBranchWithVVs [[Γ]].
  32
  33   Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> HaskType Γ ★ -> HaskLevel Γ -> Type :=
  34
  35   (* an "EGlobal" is any variable which is free in the expression which was passed to -fcoqpass (ie bound outside it) *)
  36   | EGlobal: forall Γ Δ ξ   (g:Global Γ) v lev,                                                      Expr Γ Δ ξ (g v) lev
  37
  38   | EVar   : ∀ Γ Δ ξ ev,                                                                Expr Γ Δ ξ (unlev (ξ ev)) (getlev (ξ ev))
  39   | ELit   : ∀ Γ Δ ξ lit   l,                                                                        Expr Γ Δ ξ (literalType lit) l
  40   | EApp   : ∀ Γ Δ ξ t1 t2 l,        Expr Γ Δ ξ (t2--->t1) l   -> Expr Γ Δ ξ t2 l         -> Expr Γ Δ ξ (t1) l
  41   | ELam   : ∀ Γ Δ ξ t1 t2 l ev,              Expr Γ Δ (update_xi ξ l ((ev,t1)::nil)) t2 l       -> Expr Γ Δ ξ (t1--->t2) l
  42   | ELet   : ∀ Γ Δ ξ tv t  l ev,Expr Γ Δ ξ  tv l ->Expr Γ Δ (update_xi ξ l ((ev,tv)::nil)) t l  -> Expr Γ Δ ξ t l
  43   | EEsc   : ∀ Γ Δ ξ ec t  l,     Expr Γ Δ ξ  (<[ ec |- t ]>)  l                                  -> Expr Γ Δ ξ t (ec::l)
  44   | EBrak  : ∀ Γ Δ ξ ec t  l,     Expr Γ Δ ξ t  (ec::l)                                         -> Expr Γ Δ ξ (<[ ec |- t ]>) l
  45   | ECast  : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l, Expr Γ Δ ξ t1 l             -> Expr Γ Δ ξ t2 l
  46   | ENote  : ∀ Γ Δ ξ t l, Note                      -> Expr Γ Δ ξ t l                               -> Expr Γ Δ ξ t l
  47   | ETyApp : ∀ Γ Δ κ σ τ ξ l,                    Expr Γ Δ ξ (HaskTAll κ σ) l                   -> Expr Γ Δ ξ (substT σ τ) l
  48   | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, Expr Γ (σ₁∼∼∼σ₂::Δ) ξ σ l    -> Expr Γ Δ ξ (σ₁∼∼σ₂    ⇒ σ) l
  49   | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ) l  -> Expr Γ Δ ξ σ l
  50   | ETyLam : ∀ Γ Δ ξ κ σ l n,
  51     Expr (list_ins n κ Γ) (weakCE_ Δ) (weakLT_○ξ) (HaskTApp (weakF_ σ) (FreshHaskTyVar_ _)) (weakL_ l)-> Expr Γ Δ ξ (HaskTAll κ σ) l
  52   | ECase    : forall Γ Δ ξ l tc tbranches atypes,
  53                Expr Γ Δ ξ (caseType tc atypes) l ->
  54                Tree ??{ sac : _
  55                     & { scb : StrongCaseBranchWithVVs tc atypes sac
  56                     &         Expr (sac_gamma sac Γ)
  57                                    (sac_delta sac Γ atypes (weakCK'' Δ))
  58                                    (scbwv_xi scb ξ l)
  59                                    (weakT' tbranches)
  60                                    (weakL' l) } } ->
  61                Expr Γ Δ ξ tbranches l
  62
  63   | ELetRec  : ∀ Γ Δ ξ l τ vars,
  64     distinct (leaves (mapOptionTree (@fst _ _) vars)) ->
  65     let ξ' := update_xi ξ 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 {Γ}{Δ}{ξ}{τ}{l}(exp:Expr Γ Δ ξ τ l) : 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 Γ Δ ξ τ l : ToString (Expr Γ Δ ξ τ l) := { toString := exprToString }.
  99
 100 End HaskStrong.
 101 Implicit Arguments StrongCaseBranchWithVVs [[Γ]].