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