src/HaskStrongToWeak.v

   1 (*********************************************************************************************************************************)
   2 (* HaskStrongToWeak: convert HaskStrong to HaskWeak                                                                              *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import General.
   8 Require Import NaturalDeduction.
   9 Require Import Coq.Strings.String.
  10 Require Import Coq.Lists.List.
  11 Require Import Coq.Init.Specif.
  12 Require Import HaskKinds.
  13 Require Import HaskLiteralsAndTyCons.
  14 Require Import HaskWeakTypes.
  15 Require Import HaskWeakVars.
  16 Require Import HaskWeak.
  17 Require Import HaskWeakToCore.
  18 Require Import HaskStrongTypes.
  19 Require Import HaskStrong.
  20
  21 Section HaskStrongToWeak.
  22
  23   Context (hetmet_brak : WeakExprVar).
  24   Context (hetmet_esc  : WeakExprVar).
  25
  26   Context (mkWeakTypeVar_ : Unique -> Kind                         -> WeakTypeVar).
  27   Context (mkWeakCoerVar_ : Unique -> Kind -> WeakType -> WeakType -> WeakCoerVar).
  28   Context (mkWeakExprVar_ : Unique ->         WeakType             -> WeakExprVar).
  29
  30   Definition mkWeakTypeVar (k:Kind)                 : UniqM WeakTypeVar := bind u = getU ; return mkWeakTypeVar_ u k.
  31   Definition mkWeakCoerVar (k:Kind)(t1 t2:WeakType) : UniqM WeakCoerVar := bind u = getU ; return mkWeakCoerVar_ u k t1 t2.
  32   Definition mkWeakExprVar (t:WeakType)             : UniqM WeakExprVar := bind u = getU ; return mkWeakExprVar_ u t.
  33
  34   Fixpoint mfresh (lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ)
  35     : UniqM (((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ)))) :=
  36     match lk as LK return UniqM ((vec WeakTypeVar (length LK)) * (IList _ (fun _ => WeakTypeVar) (app LK Γ))) with
  37     | nil    => return (vec_nil,ite)
  38     | k::lk' => bind v = mkWeakTypeVar k
  39               ; bind vars_ite' = mfresh lk' ite
  40               ; return ((v:::(fst vars_ite')),v::::(snd vars_ite'))
  41     end.
  42
  43   Fixpoint rawHaskTypeToWeakType {κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ) {struct rht} : UniqM WeakType :=
  44   match rht with
  45     | TVar  _  v                => return WTyVarTy v
  46     | TCon      tc              => return WTyCon tc
  47     | TCoerc _ t1 t2 t3         => bind t1' = rawHaskTypeToWeakType t1
  48                                  ; bind t2' = rawHaskTypeToWeakType t2
  49                                  ; bind t3' = rawHaskTypeToWeakType t3
  50                                  ; return WCoFunTy t1' t2' t3'
  51     | TArrow                    => return WFunTyCon
  52     | TApp  _ _  t1 t2          => bind t1' = rawHaskTypeToWeakType t1
  53                                  ; bind t2' = rawHaskTypeToWeakType t2
  54                                  ; return WAppTy t1' t2'
  55     | TAll    k rht'            => bind tv = mkWeakTypeVar k
  56                                  ; bind t' = rawHaskTypeToWeakType (rht' tv)
  57                                  ; return WForAllTy tv t'
  58     | TCode   t1 t2             => bind t1' = rawHaskTypeToWeakType t1
  59                                  ; bind t2' = rawHaskTypeToWeakType t2
  60                                  ; match t1' with
  61                                      | WTyVarTy ec => return WCodeTy ec t2'
  62                                      | _           => failM  "impossible"
  63                                    end
  64     | TyFunApp    tfc _ _ tls       => bind tls' = rawHaskTypeListToWeakType tls
  65                                  ; return WTyFunApp tfc tls'
  66   end
  67   with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) :=
  68   match rht with
  69     | TyFunApp_nil                   => return nil
  70     | TyFunApp_cons  κ kl rht' rhtl' => bind t  = rawHaskTypeToWeakType rht'
  71                                       ; bind tl = rawHaskTypeListToWeakType rhtl'
  72                                       ; return t::tl
  73   end.
  74
  75   Definition typeToWeakType {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : UniqM WeakType :=
  76     rawHaskTypeToWeakType (τ _ φ).
  77
  78   Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
  79     := tv::::ite.
  80
  81   Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2))
  82     : UniqM WeakCoercion
  83     := bind t1' = @typeToWeakType Γ κ t1 ite
  84      ; bind t2' = @typeToWeakType Γ κ t2 ite
  85      ; return WCoUnsafe t1' t2'.
  86
  87   Fixpoint seqM {a}(l:list (UniqM a)) : UniqM (list a) :=
  88     match l with
  89       | nil  => return nil
  90       | x::y => bind x' = x
  91               ; bind y' = seqM y
  92               ; return x'::y'
  93     end.
  94
  95   Context {VV}{eqVV:EqDecidable VV}{toStringVV:ToString VV}.
  96
  97   Definition update_χ (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar :=
  98     fun vv' =>
  99       if eqd_dec vv vv'
 100       then OK ev'
 101       else χ vv'.
 102
 103   Fixpoint update_χ' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar :=
 104     match varsexprs with
 105       | nil => χ
 106       | (vv,wev)::rest => update_χ (update_χ' χ rest) vv wev
 107     end.
 108
 109   Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ)
 110     : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ
 111     -> UniqM WeakExpr :=
 112     match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
 113     | EVar  Γ' _ ξ' ev              => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end
 114     | EGlobal Γ' _ ξ'   g v lev     => fun ite => bind tv' = mapM (ilist_to_list (ilmap (fun κ x => typeToWeakType x ite) v))
 115                                                 ; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g))
 116     | ELam  Γ'   _ _ tv _ _ cv e    => fun ite => bind tv' = typeToWeakType tv ite
 117                                                 ; bind ev' = mkWeakExprVar tv'
 118                                                 ; bind e'  = exprToWeakExpr (update_χ χ cv ev') e ite
 119                                                 ; return WELam ev' e'
 120     | ELet  Γ' _ _ t _ _ ev e1 e2   => fun ite => bind tv' = typeToWeakType t ite
 121                                                 ; bind e1' = exprToWeakExpr χ e1 ite
 122                                                 ; bind ev' = mkWeakExprVar tv'
 123                                                 ; bind e2' = exprToWeakExpr (update_χ χ ev ev') e2 ite
 124                                                 ; return WELet ev' e1' e2'
 125     | ELit  _ _ _ lit _             => fun ite => return WELit lit
 126     | EApp  Γ' _ _ _ _ _ e1 e2      => fun ite => bind e1' = exprToWeakExpr χ e1 ite
 127                                                 ; bind e2' = exprToWeakExpr χ e2 ite
 128                                                 ; return WEApp e1' e2'
 129     | EEsc  Γ' _ _ ec t _ e         => fun ite => bind t' = typeToWeakType t ite
 130                                                 ; bind e' = exprToWeakExpr χ e ite
 131                                                 ; return WEEsc hetmet_esc (ec _ ite) e' t'
 132     | EBrak Γ' _ _ ec t _ e         => fun ite => bind t' = typeToWeakType t ite
 133                                                 ; bind e' = exprToWeakExpr χ e ite
 134                                                 ; return WEBrak hetmet_brak (ec _ ite) e' t'
 135     | ENote _ _ _ _ n e             => fun ite => bind e' = exprToWeakExpr χ e ite
 136                                                 ; return WENote n e'
 137     | ETyApp  Γ Δ κ σ τ ξ l       e => fun ite => bind t' = typeToWeakType τ ite
 138                                                 ; bind e' = exprToWeakExpr χ e ite
 139                                                 ; return WETyApp e' t'
 140     | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => fun ite => bind e' = exprToWeakExpr χ e ite
 141                                                 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
 142                                                 ; return WECoApp e' c'
 143     | ECast Γ Δ ξ t1 t2 γ l e      => fun ite  => bind e' = exprToWeakExpr χ e ite
 144                                                 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
 145                                                 ; return WECast e' c'
 146     | ETyLam _ _ _ k _ _ e          => fun ite => bind tv = mkWeakTypeVar k
 147                                                 ; bind e' = exprToWeakExpr χ e (updateITE tv ite)
 148                                                 ; return WETyLam tv e'
 149     | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => fun ite => bind t1' = typeToWeakType σ₁ ite
 150                                                 ; bind t2' = typeToWeakType σ₂ ite
 151                                                 ; bind cv  = mkWeakCoerVar κ t1' t2'
 152                                                 ; bind e'  = exprToWeakExpr χ e ite
 153                                                 ; return WECoLam cv e'
 154     | ECase Γ Δ ξ l tc tbranches atypes escrut alts =>
 155          fun ite => bind tscrut'    = typeToWeakType (caseType tc atypes) ite
 156                   ; bind vscrut'    = mkWeakExprVar tscrut'
 157                   ; bind tbranches' = @typeToWeakType Γ _ tbranches ite
 158                   ; bind escrut'    = exprToWeakExpr χ escrut ite
 159                   ; bind branches'  =
 160                       ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ } })
 161                             : UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
 162                             match tree with
 163                               | T_Leaf None           => return []
 164                               | T_Leaf (Some x)       =>
 165                                 let (sac,scb_e) := x in
 166                                 let (scb,e) := scb_e in
 167                                 let varstypes := vec2list (scbwv_varstypes scb) in
 168                                       bind evars_ite = mfresh _ ite
 169                                     ; bind exprvars  = seqM (map (fun vt:VV * HaskType _ ★
 170                                                                         => bind tleaf = typeToWeakType (snd vt) (snd evars_ite)
 171                                                                          ; bind v' = mkWeakExprVar tleaf
 172                                                                          ; return ((fst vt),v'))
 173                                                                 varstypes)
 174                                     ; let χ' := update_χ' χ exprvars in
 175                                       bind e'' = exprToWeakExpr χ' e (snd evars_ite)
 176                                     ; return [(sac_altcon sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
 177                               | T_Branch b1 b2        => bind b1' = caseBranches b1
 178                                                        ; bind b2' = caseBranches b2
 179                                                        ; return (b1',,b2')
 180                             end) alts)
 181                   ; bind tys = seqM (ilist_to_list (@ilmap _ _
 182                                   (fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
 183                   ; return WECase vscrut' escrut' tbranches' tc tys branches'
 184
 185     | ELetRec _ _ _ _ _ vars disti elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
 186                                                                         => bind tleaf = typeToWeakType (snd vt) ite
 187                                                                          ; bind v' = mkWeakExprVar tleaf
 188                                                                          ; return ((fst vt),v'))
 189                                                                 (leaves vars))
 190                                                 ; let χ' := update_χ' χ vars' in
 191                                                   bind elrb' = exprLetRec2WeakExprLetRec χ' elrb ite
 192                                                 ; bind e'    = exprToWeakExpr χ' e ite
 193                                                 ; return WELetRec elrb' e'
 194     end
 195     with exprLetRec2WeakExprLetRec  {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar){vars}(elrb:@ELetRecBindings _ eqVV Γ Δ ξ τ vars)
 196       : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> UniqM (Tree ??(WeakExprVar * WeakExpr)) :=
 197     match elrb as E in ELetRecBindings G D X L V
 198        return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
 199     | ELR_nil    _ _ _ _           => fun ite => return []
 200     | ELR_leaf   _ _ ξ' cv v t e   => fun ite => bind t'  = typeToWeakType t ite
 201                                                ; bind e'  = exprToWeakExpr χ e ite
 202                                                ; bind v'  = match χ v with Error s => failM s | OK y => return y end
 203                                                ; return [(v',e')]
 204     | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => bind b1' = exprLetRec2WeakExprLetRec χ b1 ite
 205                                                ; bind b2' = exprLetRec2WeakExprLetRec χ b2 ite
 206                                                ; return b1',,b2'
 207   end.
 208
 209
 210   Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
 211     (ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
 212     : ???WeakExpr :=
 213     match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with
 214       uniqM f => f us >>= fun x => OK (snd x)
 215       end.
 216
 217 End HaskStrongToWeak.