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