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 Γ' _ ξ' t wev         => fun ite => return WEVar wev
 115     | ELam  Γ'   _ _ tv _ _ cv e    => fun ite => bind tv' = typeToWeakType tv ite
 116                                                 ; bind ev' = mkWeakExprVar tv'
 117                                                 ; bind e'  = exprToWeakExpr (update_χ χ cv ev') e ite
 118                                                 ; return WELam ev' e'
 119     | ELet  Γ' _ _ t _ _ ev e1 e2   => fun ite => bind tv' = typeToWeakType t ite
 120                                                 ; bind e1' = exprToWeakExpr χ e1 ite
 121                                                 ; bind ev' = mkWeakExprVar tv'
 122                                                 ; bind e2' = exprToWeakExpr (update_χ χ ev ev') e2 ite
 123                                                 ; return WELet ev' e1' e2'
 124     | ELit  _ _ _ lit _             => fun ite => return WELit lit
 125     | EApp  Γ' _ _ _ _ _ e1 e2      => fun ite => bind e1' = exprToWeakExpr χ e1 ite
 126                                                 ; bind e2' = exprToWeakExpr χ e2 ite
 127                                                 ; return WEApp e1' e2'
 128     | EEsc  Γ' _ _ ec t _ e         => fun ite => bind t' = typeToWeakType t ite
 129                                                 ; bind e' = exprToWeakExpr χ e ite
 130                                                 ; return WEEsc hetmet_esc (ec _ ite) e' t'
 131     | EBrak Γ' _ _ ec t _ e         => fun ite => bind t' = typeToWeakType t ite
 132                                                 ; bind e' = exprToWeakExpr χ e ite
 133                                                 ; return WEBrak hetmet_brak (ec _ ite) e' t'
 134     | ENote _ _ _ _ n e             => fun ite => bind e' = exprToWeakExpr χ e ite
 135                                                 ; return WENote n e'
 136     | ETyApp  Γ Δ κ σ τ ξ l       e => fun ite => bind t' = typeToWeakType τ ite
 137                                                 ; bind e' = exprToWeakExpr χ e ite
 138                                                 ; return WETyApp e' t'
 139     | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => fun ite => bind e' = exprToWeakExpr χ e ite
 140                                                 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
 141                                                 ; return WECoApp e' c'
 142     | ECast Γ Δ ξ t1 t2 γ l e      => fun ite  => bind e' = exprToWeakExpr χ e ite
 143                                                 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
 144                                                 ; return WECast e' c'
 145     | ETyLam _ _ _ k _ _ e          => fun ite => bind tv = mkWeakTypeVar k
 146                                                 ; bind e' = exprToWeakExpr χ e (updateITE tv ite)
 147                                                 ; return WETyLam tv e'
 148     | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => fun ite => bind t1' = typeToWeakType σ₁ ite
 149                                                 ; bind t2' = typeToWeakType σ₂ ite
 150                                                 ; bind cv  = mkWeakCoerVar κ t1' t2'
 151                                                 ; bind e'  = exprToWeakExpr χ e ite
 152                                                 ; return WECoLam cv e'
 153     | ECase Γ Δ ξ l tc tbranches atypes escrut alts =>
 154          fun ite => bind tscrut'    = typeToWeakType (caseType tc atypes) ite
 155                   ; bind vscrut'    = mkWeakExprVar tscrut'
 156                   ; bind tbranches' = @typeToWeakType Γ _ tbranches ite
 157                   ; bind escrut'    = exprToWeakExpr χ escrut ite
 158                   ; bind branches'  =
 159                       ((fix caseBranches (tree:Tree ??{scb : StrongCaseBranchWithVVs VV _ _ _ & Expr _ _ _ _  })
 160                             : UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
 161                             match tree with
 162                               | T_Leaf None           => return []
 163                               | T_Leaf (Some x)       => let (scb,e) := x in
 164                                 let varstypes := vec2list (scbwv_varstypes scb) in
 165                                       bind evars_ite = mfresh _ ite
 166                                     ; bind exprvars  = seqM (map (fun vt:VV * HaskType _ ★
 167                                                                         => bind tleaf = typeToWeakType (snd vt) (snd evars_ite)
 168                                                                          ; bind v' = mkWeakExprVar tleaf
 169                                                                          ; return ((fst vt),v'))
 170                                                                 varstypes)
 171                                     ; let χ' := update_χ' χ exprvars in
 172                                       bind e'' = exprToWeakExpr χ' e (snd evars_ite)
 173                                     ; return [(sac_altcon scb, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
 174                               | T_Branch b1 b2        => bind b1' = caseBranches b1
 175                                                        ; bind b2' = caseBranches b2
 176                                                        ; return (b1',,b2')
 177                             end) alts)
 178                   ; bind tys = seqM (ilist_to_list (@ilmap _ _
 179                                   (fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
 180                   ; return WECase vscrut' escrut' tbranches' tc tys branches'
 181
 182     | ELetRec _ _ _ _ _ vars elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
 183                                                                         => bind tleaf = typeToWeakType (snd vt) ite
 184                                                                          ; bind v' = mkWeakExprVar tleaf
 185                                                                          ; return ((fst vt),v'))
 186                                                                 (leaves vars))
 187                                                 ; let χ' := update_χ' χ vars' in
 188                                                   bind elrb' = exprLetRec2WeakExprLetRec χ' elrb ite
 189                                                 ; bind e'    = exprToWeakExpr χ' e ite
 190                                                 ; return WELetRec elrb' e'
 191     end
 192     with exprLetRec2WeakExprLetRec  {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar){vars}(elrb:@ELetRecBindings _ eqVV Γ Δ ξ τ vars)
 193       : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> UniqM (Tree ??(WeakExprVar * WeakExpr)) :=
 194     match elrb as E in ELetRecBindings G D X L V
 195        return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
 196     | ELR_nil    _ _ _ _           => fun ite => return []
 197     | ELR_leaf   _ _ ξ' cv v t e   => fun ite => bind t'  = typeToWeakType t ite
 198                                                ; bind e'  = exprToWeakExpr χ e ite
 199                                                ; bind v'  = match χ v with Error s => failM s | OK y => return y end
 200                                                ; return [(v',e')]
 201     | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => bind b1' = exprLetRec2WeakExprLetRec χ b1 ite
 202                                                ; bind b2' = exprLetRec2WeakExprLetRec χ b2 ite
 203                                                ; return b1',,b2'
 204   end.
 205
 206
 207   Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
 208     (ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
 209     : ???WeakExpr :=
 210     match exprToWeakExpr (fun v => Error ("unbound variable " +++ v)) exp ite with
 211       uniqM f => f us >>= fun x => OK (snd x)
 212       end.
 213
 214 End HaskStrongToWeak.