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 HaskCoreLiterals.
  14 Require Import HaskCoreVars.
  15 Require Import HaskCoreTypes.
  16 Require Import HaskCore.
  17 Require Import HaskWeakTypes.
  18 Require Import HaskWeakVars.
  19 Require Import HaskWeak.
  20 Require Import HaskStrongTypes.
  21 Require Import HaskStrong.
  22
  23 Fixpoint mfresh (f:Fresh Kind (fun _ => WeakTypeVar))(lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ)
  24   : (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ))) :=
  25   match lk as LK return (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length LK)) *
  26                           (IList _ (fun _ => WeakTypeVar) (app LK Γ))) with
  27   | nil    => (f,(vec_nil,ite))
  28   | k::lk' =>
  29     let (f',varsite') := mfresh f lk' ite
  30     in  let (vars,ite') := varsite'
  31     in  let (v,f'') := next _ _ f' k
  32     in (f'',((v:::vars),v::::ite'))
  33   end.
  34
  35 Fixpoint rawHaskTypeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskType (fun _ => WeakTypeVar) κ)
  36  {struct rht} : WeakType :=
  37 match rht with
  38   | TVar  _  v                 => WTyVarTy v
  39   | TCon      tc              => WTyCon tc
  40   | TCoerc _ t1 t2 t3          => WCoFunTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2) (rawHaskTypeToWeakType f t3)
  41   | TArrow                    => WFunTyCon
  42   | TApp  _ _  t1 t2             => WAppTy (rawHaskTypeToWeakType f t1) (rawHaskTypeToWeakType f t2)
  43   | TAll    k rht'            => let (tv,f') := next _ _ f k in WForAllTy tv (rawHaskTypeToWeakType f' (rht' tv))
  44   | TCode   t1 t2             =>
  45     match (rawHaskTypeToWeakType f t1) with
  46       | WTyVarTy ec => WCodeTy ec (rawHaskTypeToWeakType f t2)
  47       | impossible  => impossible  (* TODO: find a way to convince Coq this can't happen *)
  48     end
  49   | TyFunApp    tfc tls         => WTyFunApp tfc (rawHaskTypeListToWeakType f tls)
  50 end
  51 with rawHaskTypeListToWeakType (f:Fresh Kind (fun _ => WeakTypeVar)){κ}(rht:RawHaskTypeList κ) :=
  52 match rht with
  53   | TyFunApp_nil   => nil
  54   | TyFunApp_cons  κ kl rht' rhtl' => (rawHaskTypeToWeakType f rht')::(rawHaskTypeListToWeakType f rhtl')
  55 end.
  56
  57 Definition typeToWeakType (f:Fresh Kind (fun _ => WeakTypeVar))
  58   {Γ}{κ}(τ:HaskType Γ κ)(φ:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : WeakType :=
  59   rawHaskTypeToWeakType f (τ _ φ).
  60
  61 (* This can be used to turn HaskStrong's with arbitrary expression variables into HaskStrong's which use WeakExprVar's
  62  * for their variables; those can subsequently be passed to the following function (strongExprToWeakExpr) *)
  63 (*
  64 Definition reindexStrongExpr {VV}{HH}{eqVV:EqDecidable VV}{eqHH:EqDecidable HH}
  65   {Γ}{Δ}{ξ}{lev}(exp:@Expr VV eqVV Γ Δ ξ lev) : { ξ' : HH -> LeveledHaskType Γ & @Expr HH eqHH Γ Δ ξ' lev }.
  66   Defined.
  67   *)
  68
  69 Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
  70   := tv::::ite.
  71
  72 Section strongExprToWeakExpr.
  73
  74   Context (hetmet_brak : CoreVar).
  75   Context (hetmet_esc  : CoreVar).
  76 Axiom FIXME : forall {t}, t.
  77
  78 Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ}
  79   (ftv:Fresh Kind                (fun _ => WeakTypeVar))
  80   (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
  81   (exp:@Expr _ CoreVarEqDecidable Γ Δ ξ τ)
  82   : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> WeakExpr :=
  83 match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> WeakExpr with
  84 | EVar  Γ' _ ξ' ev              => fun ite => WEVar (weakExprVar ev (@typeToWeakType ftv Γ' ★  (unlev (ξ' ev)) ite))
  85 | ELit  _ _ _ lit _             => fun ite => WELit lit
  86 | EApp  Γ' _ _ _ _ _ e1 e2      => fun ite => WEApp (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
  87 | ELam  Γ'   _ _ _ t _ cv e     => fun ite => WELam (weakExprVar cv (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e ite)
  88 | ELet  Γ' _ _ t _ _ ev e1 e2   => fun ite => WELet (weakExprVar ev (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite)
  89 | EEsc  Γ' _ _ ec t _ e         => fun ite => WEEsc  hetmet_esc (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
  90 | EBrak Γ' _ _ ec t _ e         => fun ite => WEBrak hetmet_brak (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite)
  91 | ENote _ _ _ _ n e             => fun ite => WENote n (strongExprToWeakExpr ftv fcv e ite)
  92 | ETyApp  Γ Δ κ σ τ ξ l       e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv τ ite)
  93 | ELetRec _ _ _ _ _ vars elrb e =>fun ite=>WELetRec (exprLetRec2WeakExprLetRec ftv fcv elrb ite)(strongExprToWeakExpr ftv fcv e ite)
  94 | ECast Γ Δ ξ t1 t2 γ l e       => fun ite => FIXME
  95 (* WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)*)
  96
  97 | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => fun ite => FIXME
  98 (* WECoApp (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)*)
  99 | ECase Γ Δ ξ l tc tbranches atypes e alts =>
 100   fun ite => WECase
 101     FIXME
 102     (strongExprToWeakExpr ftv fcv e ite)
 103     (@typeToWeakType ftv Γ _ tbranches ite)
 104     tc
 105     (ilist_to_list (@ilmap _ _ (fun _ => WeakType) _ (fun _ t => typeToWeakType ftv t ite) atypes))
 106     ((fix caseBranches
 107       (tree:Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
 108                             & Expr (sac_Γ scb Γ)
 109                                    (sac_Δ scb Γ atypes (weakCK'' Δ))
 110                                    (update_ξ (weakLT'○ξ) (vec2list (vec_map
 111                                      (fun x => ((fst x),(snd x @@ weakL' l))) (scbwv_varstypes scb))))
 112                                    (weakLT' (tbranches@@l)) })
 113       : Tree ??(AltCon * list WeakTypeVar * list WeakCoerVar * list WeakExprVar * WeakExpr) :=
 114       match tree with
 115         | T_Leaf None     => []
 116         | T_Leaf (Some x) => let (scb,e) := x in
 117           let (ftv',evarsite') := mfresh ftv _ ite in
 118           let fcv' :=  fcv in
 119             let (evars,ite') := evarsite' in
 120             [(sac_altcon scb,
 121               vec2list evars,
 122               nil (*FIXME*),
 123               map (fun vt => weakExprVar (fst vt) (typeToWeakType ftv' (snd vt) ite')) (vec2list (scbwv_varstypes scb)),
 124               strongExprToWeakExpr ftv' fcv' e ite'
 125             )]
 126         | T_Branch b1 b2  => (caseBranches b1),,(caseBranches b2)
 127       end
 128     ) alts)
 129 | ETyLam _ _ _ k _ _ e          => fun ite =>
 130   let (tv,ftv') := next _ _ ftv k in WETyLam tv (strongExprToWeakExpr ftv' fcv e (updateITE tv ite))
 131 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => fun ite =>
 132   let t1' := typeToWeakType ftv σ₁ ite in
 133   let t2' := typeToWeakType ftv σ₂ ite in
 134   let (cv,fcv') := next _ _ fcv (t1',t2') in WECoLam cv (strongExprToWeakExpr ftv fcv' e ite)
 135 end
 136 with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{τ}{vars}
 137   (ftv:Fresh Kind                (fun _ => WeakTypeVar))
 138   (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar))
 139   (elrb:@ELetRecBindings _ CoreVarEqDecidable Γ Δ ξ τ vars)
 140   : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> Tree ??(WeakExprVar * WeakExpr) :=
 141 match elrb as E in ELetRecBindings G D X L V
 142    return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> Tree ??(WeakExprVar * WeakExpr) with
 143 | ELR_nil    _ _ _ _           => fun ite => []
 144 | ELR_leaf   _ _ ξ' cv v e    => fun ite => [((weakExprVar v (typeToWeakType ftv (unlev (ξ' v)) ite)),(strongExprToWeakExpr ftv fcv e ite))]
 145 | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv b2 ite)
 146 end.
 147 End strongExprToWeakExpr.