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