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