src/HaskCoreToWeak.v

   1 (*********************************************************************************************************************************)
   2 (* HaskCoreToWeak: convert HaskCore to HaskWeak                                                                                  *)
   3 (*********************************************************************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Preamble.
   7 Require Import Coq.Lists.List.
   8 Require Import General.
   9 Require Import HaskKinds.
  10 Require Import HaskLiterals.
  11 Require Import HaskTyCons.
  12 Require Import HaskCoreVars.
  13 Require Import HaskCoreTypes.
  14 Require Import HaskCore.
  15 Require Import HaskWeakVars.
  16 Require Import HaskWeakTypes.
  17 Require Import HaskWeak.
  18
  19 Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun.          Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
  20 Variable coreViewDeep : CoreType  -> CoreType.                 Extract Inlined Constant coreViewDeep => "coreViewDeep".
  21 Variable coercionKind : CoreCoercion -> (CoreType * CoreType).
  22    Extract Inlined Constant coercionKind => "(\x -> Pair.unPair (Coercion.coercionKind x))".
  23
  24 (* extracts the Name from a CoreVar *)
  25 Variable coreVarCoreName    : CoreVar -> CoreName.   Extract Inlined Constant coreVarCoreName  => "Var.varName".
  26
  27 (* the magic wired-in name for the modal type introduction/elimination forms *)
  28 Variable hetmet_brak_name   : CoreName.              Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
  29 Variable hetmet_esc_name    : CoreName.              Extract Inlined Constant hetmet_esc_name  => "PrelNames.hetmet_esc_name".
  30 Variable hetmet_csp_name    : CoreName.              Extract Inlined Constant hetmet_csp_name  => "PrelNames.hetmet_csp_name".
  31
  32 Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType :=
  33   split_list lwt (length (fst (tyFunKind tf))) >>=
  34   fun argsrest =>
  35     let (args,rest) := argsrest in
  36       OK (fold_left (fun x y => WAppTy x y) rest (WTyFunApp tf args)).
  37
  38 (* a hack to evade the guardedness check of Fixpoint *)
  39 Variable coreTypeToWeakTypeCheat' : CoreType -> ???WeakType.
  40 Extract Inlined Constant coreTypeToWeakTypeCheat' => "coreTypeToWeakType'".
  41
  42 Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
  43   match ct with
  44   | TyVarTy  cv              => match coreVarToWeakVar cv with
  45                                   | CVTWVR_EVar  ct    => Error "encountered expression variable in a type"
  46                                   | CVTWVR_TyVar k     => OK (WTyVarTy (weakTypeVar cv k))
  47                                   | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a type"
  48                                 end
  49
  50   | AppTy    t1 t2           => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2')
  51
  52   | TyConApp  tc_ lct        =>
  53       let recurse := ((fix rec tl := match tl with
  54                                   | nil => OK nil
  55                                   | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
  56                                 end) lct)
  57       in match tyConOrTyFun tc_ with
  58            | inr tf => recurse >>= fun recurse' => mkTyFunApplication tf recurse'
  59            | inl tc => if eqd_dec tc ModalBoxTyCon
  60                          then match lct with
  61                                 | ((TyVarTy ec)::tbody::nil) =>
  62                                   match coreVarToWeakVar ec with
  63                                     | CVTWVR_EVar  ct    => Error "encountered expression variable in a modal box type"
  64                                     | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a modal box type"
  65                                     | CVTWVR_TyVar k     => coreTypeToWeakType' tbody >>= fun tbody' =>
  66                                                               OK (WCodeTy (weakTypeVar ec k) tbody')
  67                                   end
  68                                 | _                      => Error ("mis-applied modal box tycon: " +++ toString ct)
  69                               end
  70                          else let tc' := if eqd_dec tc ArrowTyCon
  71                                          then WFunTyCon
  72                                          else WTyCon tc
  73                               in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc')
  74          end
  75   | FunTy (PredTy (EqPred t1 t2)) t3    => coreTypeToWeakType' t1 >>= fun t1' =>
  76                                 coreTypeToWeakType' t2 >>= fun t2' =>
  77                                 coreTypeToWeakType' t3 >>= fun t3' =>
  78                                   OK (WCoFunTy t1' t2' t3')
  79   | FunTy    t1 t2           => coreTypeToWeakType' t1 >>= fun t1' =>
  80                                 coreTypeToWeakType' t2 >>= fun t2' =>
  81                                   OK (WAppTy (WAppTy WFunTyCon t1') t2')
  82   | ForAllTy cv t            => match coreVarToWeakVar cv with
  83                                   | CVTWVR_EVar  ct    => Error "encountered expression variable in a type abstraction"
  84                                   | CVTWVR_TyVar k     => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy (weakTypeVar cv k) t')
  85                                   | CVTWVR_CoVar t1 t2 => coreTypeToWeakTypeCheat' t1 >>= fun t1' =>
  86                                                             coreTypeToWeakTypeCheat' t2 >>= fun t2' =>
  87                                                               coreTypeToWeakType' t >>= fun t3' =>
  88                                                                 OK (WCoFunTy t1' t2' t3')
  89                                 end
  90   | PredTy (ClassP  cl lct) => ((fix rec tl := match tl with
  91                                                   | nil => OK nil
  92                                                   | a::b => coreTypeToWeakType' a >>= fun a' =>
  93                                                     rec b >>= fun b' => OK (a'::b')
  94                                                 end) lct) >>= fun lct' => OK (WClassP cl lct')
  95   | PredTy (IParam ipn ct)   => coreTypeToWeakType' ct >>= fun ct' => OK (WIParam ipn ct')
  96   | PredTy (EqPred _ _)   => Error "hit a bare EqPred"
  97   end.
  98
  99 Definition coreTypeToWeakType t :=
 100   addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)).
 101
 102 Definition coreVarToWeakVar' (cv:CoreVar) : ???WeakVar :=
 103   addErrorMessage ("during coreVarToWeakVar on " +++ toString cv +++ eol)
 104   match coreVarToWeakVar cv with
 105     | CVTWVR_EVar  ct    => coreTypeToWeakType ct >>= fun t' => OK (WExprVar (weakExprVar cv t'))
 106     | CVTWVR_TyVar k     =>                                     OK (WTypeVar (weakTypeVar cv k))
 107     | CVTWVR_CoVar t1 t2 =>
 108       (* this will choke if given a coercion-between-coercions (EqPred (EqPred c1 c2) (EqPred c3 c4)) *)
 109       addErrorMessage ("with t2=" +++ toString t2 +++ eol)
 110       ((coreTypeToWeakType t2) >>= fun t2' =>
 111       addErrorMessage ("with t1=" +++ toString t1 +++ eol)
 112       (coreTypeToWeakType t1) >>= fun t1' =>
 113                                 OK (WCoerVar (weakCoerVar cv t1' t2')))
 114   end.
 115 Definition tyConTyVars (tc:CoreTyCon) :=
 116   filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (getTyConTyVars_ tc)).
 117   Opaque tyConTyVars.
 118 Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc).
 119
 120 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
 121 Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
 122 match ce with
 123   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
 124     => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
 125       match coreVarToWeakVar' ec with
 126         | OK (WTypeVar tv) => match coreVarToWeakVar' v with
 127                            | OK (WExprVar v') => Some (v',tv,tbody)
 128                            | _ => None
 129                          end
 130         | _  => None
 131       end else None
 132   | _ => None
 133 end.
 134
 135 Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
 136 match ce with
 137   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
 138     => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
 139       match coreVarToWeakVar' ec with
 140         | OK (WTypeVar tv) => match coreVarToWeakVar' v with
 141                            | OK (WExprVar v') => Some (v',tv,tbody)
 142                            | _ => None
 143                          end
 144         | _  => None
 145       end else None
 146   | _ => None
 147 end.
 148
 149 Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
 150 match ce with
 151   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
 152     => if coreName_eq hetmet_csp_name (coreVarCoreName v) then
 153       match coreVarToWeakVar' ec with
 154         | OK (WTypeVar tv) => match coreVarToWeakVar' v with
 155                            | OK (WExprVar v') => Some (v',tv,tbody)
 156                            | _ => None
 157                          end
 158         | _  => None
 159       end else None
 160   | _ => None
 161 end.
 162
 163 (* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
 164 Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list WeakType) :=
 165   match wt with
 166     | WTyCon tc        => OK (tc,acc)
 167     | WAppTy t1 t2     => expectTyConApp t1 (t2::acc)
 168     | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ toString wt)
 169     | _                => Error ("expectTyConApp encountered " +++ toString wt)
 170   end.
 171
 172 (* expects to see an EType with a coercion payload *)
 173 Definition coreExprToWeakCoercion t1 t2 (ce:@CoreExpr CoreVar) : ???WeakCoercion :=
 174   match ce with
 175     | CoreEType t => (*OK (coreCoercionToWeakCoercion t)*) OK (WCoUnsafe t1 t2)
 176     | _           => Error ("coreExprToWeakCoercion got a " +++ toString ce)
 177   end.
 178
 179 (* expects to see an EType *)
 180 Definition coreExprToWeakType (ce:@CoreExpr CoreVar) : ???WeakType :=
 181   match ce with
 182     | CoreEType t => coreTypeToWeakType t
 183     | _           => Error ("coreExprToWeakType got a " +++ toString ce)
 184   end.
 185
 186 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
 187   match ce with
 188     | CoreELit   lit   => OK (WELit lit)
 189     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
 190     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
 191     | CoreECoercion co => Error "encountered CoreECoercion in a position where an Expr should have been"
 192     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>
 193                             let (ct1,ct2) := coercionKind co
 194                              in coreTypeToWeakType ct1 >>= fun t1 =>
 195                                   coreTypeToWeakType ct2 >>= fun t2 =>
 196                                     OK (WECast e' (WCoUnsafe t1 t2))
 197
 198     | CoreEVar   v     => coreVarToWeakVar' v >>= fun v' => match v' with
 199                             | WExprVar ev => OK (WEVar ev)
 200                             | WTypeVar _  => Error "found a type variable inside an EVar!"
 201                             | WCoerVar _  => Error "found a coercion variable inside an EVar!"
 202                           end
 203
 204     | CoreEApp   e1 e2 => match isBrak e1 with
 205                             | Some (v,tv,t) =>
 206                               coreExprToWeakExpr e2 >>= fun e' =>
 207                                 coreTypeToWeakType t >>= fun t' =>
 208                                 OK (WEBrak v tv e' t')
 209                             | None    => match isEsc e1 with
 210                                            | Some (v,tv,t) =>
 211                                              coreExprToWeakExpr e2 >>= fun e' =>
 212                                                coreTypeToWeakType t >>= fun t' =>
 213                                                  OK (WEEsc v tv e' t')
 214                                            | None    => match isCSP e1 with
 215                                                           | Some (v,tv,t) =>
 216                                                             coreExprToWeakExpr e2 >>= fun e' =>
 217                                                               coreTypeToWeakType t >>= fun t' =>
 218                                                                 OK (WECSP v tv e' t')
 219                                                           | None    => coreExprToWeakExpr e1 >>= fun e1' =>
 220                                                             match e2 with
 221                                                               | CoreEType t =>
 222                                                                 coreTypeToWeakType t >>= fun t' =>
 223                                                                   OK (WETyApp e1' t')
 224                                                               | _           => coreExprToWeakExpr e2
 225                                                                 >>= fun e2' => OK (WEApp e1' e2')
 226                                                             end
 227                                                         end
 228                                          end
 229                           end
 230
 231     | CoreELam   v e => coreVarToWeakVar' v >>= fun v' => match v' with
 232                          | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam   ev e')
 233                          | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
 234                          | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
 235                        end
 236
 237     | CoreELet   (CoreNonRec v ve) e => coreVarToWeakVar' v >>= fun v' => match v' with
 238                          | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
 239                                             coreExprToWeakExpr e  >>= fun e'  => OK (WELet ev ve' e')
 240                          | WTypeVar tv => match e with
 241                                               | CoreEType t => coreExprToWeakExpr e >>= fun e'  =>
 242                                                                  coreExprToWeakType ve >>= fun ty' =>
 243                                                                    OK (WETyApp (WETyLam tv e') ty')
 244                                               | _           => Error "saw (ELet <tyvar> e) where e!=EType"
 245                                             end
 246                          | WCoerVar (weakCoerVar cv t1 t2) =>
 247                                        coreExprToWeakExpr e  >>= fun e'  =>
 248                                            coreExprToWeakCoercion t1 t2 ve >>= fun co' =>
 249                                               OK (WECoApp (WECoLam (weakCoerVar cv t1 t2) e') co')
 250                        end
 251
 252     | CoreELet   (CoreRec rb)      e =>
 253       ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
 254         match cel with
 255           | nil => OK nil
 256           | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
 257             coreVarToWeakVar' v' >>= fun v'' => match v'' with
 258               | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
 259               | WTypeVar _  => Error "found a type variable in a recursive let"
 260               | WCoerVar _  => Error "found a coercion variable in a recursive let"
 261             end
 262         end) rb) >>= fun rb' =>
 263       coreExprToWeakExpr e >>= fun e' =>
 264       OK (WELetRec (unleaves' rb') e')
 265
 266     | CoreECase  e v tbranches alts =>
 267       coreVarToWeakVar' v >>= fun v' => match v' with
 268         | WTypeVar _  => Error "found a type variable in a case"
 269         | WCoerVar _  => Error "found a coercion variable in a case"
 270         | WExprVar ev =>
 271         coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
 272           expectTyConApp te' nil >>= fun tca =>
 273             let (tc,lt) := tca:(TyCon * list WeakType) in
 274           ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
 275                 : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
 276             match branches with
 277               | nil => OK nil
 278               | (mkTriple alt vars e)::rest =>
 279                   mkBranches rest >>= fun rest' =>
 280                     coreExprToWeakExpr e >>= fun e' =>
 281                     match alt with
 282                       | DEFAULT                => OK ((WeakDEFAULT,nil,nil,nil,e')::rest')
 283                       | LitAlt lit             => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
 284                       | DataAlt dc             => let vars := map coreVarToWeakVar' vars in
 285                         OK (((WeakDataAlt dc),
 286                         (filter (map (fun x => match x with OK (WTypeVar v) => Some v | _ => None end) vars)),
 287                         (filter (map (fun x => match x with OK (WCoerVar v) => Some v | _ => None end) vars)),
 288                         (filter (map (fun x => match x with OK (WExprVar v) => Some v | _ => None end) vars)),
 289                         e')::rest')
 290                     end
 291             end) alts)
 292           >>= fun branches =>
 293             coreExprToWeakExpr e >>= fun scrutinee =>
 294               coreTypeToWeakType tbranches >>= fun tbranches' =>
 295                   OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))
 296       end
 297   end.