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