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