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 coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
  22   Extract Inlined Constant coreCoercionToWeakCoercion => "coreCoercionToWeakCoercion".
  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 Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
  33   match ct with
  34   | TyVarTy  cv              => match coreVarToWeakVar cv with
  35                                   | WExprVar _  => Error "encountered expression variable in a type"
  36                                   | WTypeVar tv => OK (WTyVarTy tv)
  37                                   | WCoerVar _  => Error "encountered coercion variable in a type"
  38                                 end
  39
  40   | AppTy    t1 t2           => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2')
  41
  42   | TyConApp  tc_ lct        =>
  43       let recurse := ((fix rec tl := match tl with
  44                                   | nil => OK nil
  45                                   | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
  46                                 end) lct)
  47       in match tyConOrTyFun tc_ with
  48            | inr tf => recurse >>= fun recurse' => OK (WTyFunApp tf recurse')
  49            | inl tc => if eqd_dec tc ModalBoxTyCon
  50                          then match lct with
  51                                 | ((TyVarTy ec)::tbody::nil) =>
  52                                   match coreVarToWeakVar ec with
  53                                     | WTypeVar ec' => coreTypeToWeakType' tbody >>= fun tbody' => OK (WCodeTy ec' tbody')
  54                                     | WExprVar _  => Error "encountered expression variable in a modal box type"
  55                                     | WCoerVar _  => Error "encountered coercion variable in a modal box type"
  56                                   end
  57                                 | _                           => Error ("mis-applied modal box tycon: " +++ toString ct)
  58                               end
  59                          else let tc' := if eqd_dec tc ArrowTyCon
  60                                          then WFunTyCon
  61                                          else WTyCon tc
  62                               in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc')
  63          end
  64   | FunTy (PredTy (EqPred t1 t2)) t3    => coreTypeToWeakType' t1 >>= fun t1' =>
  65                                 coreTypeToWeakType' t2 >>= fun t2' =>
  66                                 coreTypeToWeakType' t3 >>= fun t3' =>
  67                                   OK (WCoFunTy t1' t2' t3')
  68   | FunTy    t1 t2           => coreTypeToWeakType' t1 >>= fun t1' =>
  69                                 coreTypeToWeakType' t2 >>= fun t2' =>
  70                                   OK (WAppTy (WAppTy WFunTyCon t1') t2')
  71   | ForAllTy cv t            => match coreVarToWeakVar cv with
  72                                   | WExprVar _  => Error "encountered expression variable in a type"
  73                                   | WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t')
  74                                   | WCoerVar _  => Error "encountered coercion variable in a type"
  75                                 end
  76   | PredTy (ClassP  cl lct) => ((fix rec tl := match tl with
  77                                                   | nil => OK nil
  78                                                   | a::b => coreTypeToWeakType' a >>= fun a' =>
  79                                                     rec b >>= fun b' => OK (a'::b')
  80                                                 end) lct) >>= fun lct' => OK (WClassP cl lct')
  81   | PredTy (IParam ipn ct)   => coreTypeToWeakType' ct >>= fun ct' => OK (WIParam ipn ct')
  82   | PredTy (EqPred _ _)   => Error "hit a bare EqPred"
  83   end.
  84
  85 Fixpoint coreTypeToWeakType t := addErrorMessage "coreTypeToWeakType" (coreTypeToWeakType' (coreViewDeep t)).
  86
  87 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
  88 Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
  89 match ce with
  90   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
  91     => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
  92       match coreVarToWeakVar ec with
  93         | WExprVar _  => None
  94         | WCoerVar _  => None
  95         | WTypeVar tv => match coreVarToWeakVar v with
  96                            | WExprVar v' => Some (v',tv,tbody)
  97                            | _ => None
  98                          end
  99       end else None
 100   | _ => None
 101 end.
 102
 103 Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
 104 match ce with
 105   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
 106     => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
 107       match coreVarToWeakVar ec with
 108         | WExprVar _  => None
 109         | WTypeVar tv => match coreVarToWeakVar v with
 110                            | WExprVar v' => Some (v',tv,tbody)
 111                            | _ => None
 112                          end
 113         | WCoerVar _  => None
 114       end else None
 115   | _ => None
 116 end.
 117
 118 Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
 119 match ce with
 120   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
 121     => if coreName_eq hetmet_csp_name (coreVarCoreName v) then
 122       match coreVarToWeakVar ec with
 123         | WExprVar _  => None
 124         | WTypeVar tv => match coreVarToWeakVar v with
 125                            | WExprVar v' => Some (v',tv,tbody)
 126                            | _ => None
 127                          end
 128         | WCoerVar _  => None
 129       end else None
 130   | _ => None
 131 end.
 132
 133 (* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
 134 Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list WeakType) :=
 135   match wt with
 136     | WTyCon tc        => OK (tc,acc)
 137     | WAppTy t1 t2     => expectTyConApp t1 (t2::acc)
 138     | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ toString wt)
 139     | _                => Error ("expectTyConApp encountered " +++ toString wt)
 140   end.
 141
 142 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
 143   match ce with
 144     | CoreELit   lit   => OK (WELit lit)
 145     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
 146     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
 147     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>
 148                               OK (WECast e' (coreCoercionToWeakCoercion co))
 149
 150     | CoreEVar   v     => match coreVarToWeakVar v with
 151                             | WExprVar ev => OK (WEVar ev)
 152                             | WTypeVar _  => Error "found a type variable inside an EVar!"
 153                             | WCoerVar _  => Error "found a coercion variable inside an EVar!"
 154                           end
 155
 156     | CoreEApp   e1 e2 => match isBrak e1 with
 157                             | Some (v,tv,t) =>
 158                               coreExprToWeakExpr e2 >>= fun e' =>
 159                                 coreTypeToWeakType t >>= fun t' =>
 160                                 OK (WEBrak v tv e' t')
 161                             | None    => match isEsc e1 with
 162                                            | Some (v,tv,t) =>
 163                                              coreExprToWeakExpr e2 >>= fun e' =>
 164                                                coreTypeToWeakType t >>= fun t' =>
 165                                                  OK (WEEsc v tv e' t')
 166                                            | None    => match isCSP e1 with
 167                                                           | Some (v,tv,t) =>
 168                                                             coreExprToWeakExpr e2 >>= fun e' =>
 169                                                               coreTypeToWeakType t >>= fun t' =>
 170                                                                 OK (WECSP v tv e' t')
 171                                                           | None    => coreExprToWeakExpr e1 >>= fun e1' =>
 172                                                             match e2 with
 173                                                               | CoreEType t =>
 174                                                                 coreTypeToWeakType t >>= fun t' =>
 175                                                                   OK (WETyApp e1' t')
 176                                                               | _           => coreExprToWeakExpr e2
 177                                                                 >>= fun e2' => OK (WEApp e1' e2')
 178                                                             end
 179                                                         end
 180                                          end
 181                           end
 182
 183     | CoreELam   v e => match coreVarToWeakVar v with
 184                          | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam   ev e')
 185                          | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
 186                          | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
 187                        end
 188
 189     | CoreELet   (CoreNonRec v ve) e => match coreVarToWeakVar v with
 190                          | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
 191                                             coreExprToWeakExpr e  >>= fun e'  => OK (WELet ev ve' e')
 192                          | WTypeVar _ => match e with
 193                                               | CoreEType t => Error "saw a type-let"
 194                                               | _           => Error "saw (ELet <tyvar> e) where e!=EType"
 195                                             end
 196                          | WCoerVar _ => Error "saw an (ELet <coercionVar>)"
 197                        end
 198
 199     | CoreELet   (CoreRec rb)      e =>
 200       ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
 201         match cel with
 202           | nil => OK nil
 203           | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
 204             match coreVarToWeakVar v' with
 205               | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
 206               | WTypeVar _  => Error "found a type variable in a recursive let"
 207               | WCoerVar _  => Error "found a coercion variable in a recursive let"
 208             end
 209         end) rb) >>= fun rb' =>
 210       coreExprToWeakExpr e >>= fun e' =>
 211       OK (WELetRec (unleaves' rb') e')
 212
 213     | CoreECase  e v tbranches alts =>
 214       match coreVarToWeakVar v with
 215         | WTypeVar _  => Error "found a type variable in a case"
 216         | WCoerVar _  => Error "found a coercion variable in a case"
 217         | WExprVar ev =>
 218         coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
 219           expectTyConApp te' nil >>= fun tca =>
 220             let (tc,lt) := tca:(TyCon * list WeakType) in
 221           ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
 222                 : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
 223             match branches with
 224               | nil => OK nil
 225               | (mkTriple alt vars e)::rest =>
 226                   mkBranches rest >>= fun rest' =>
 227                     coreExprToWeakExpr e >>= fun e' =>
 228                     match alt with
 229                       | DEFAULT                => OK ((WeakDEFAULT,nil,nil,nil,e')::rest')
 230                       | LitAlt lit             => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
 231                       | DataAlt dc             => let vars := map coreVarToWeakVar vars in
 232                         OK (((WeakDataAlt dc),
 233                         (filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
 234                         (filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
 235                         (filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
 236                         e')::rest')
 237                     end
 238             end) alts)
 239           >>= fun branches =>
 240             coreExprToWeakExpr e >>= fun scrutinee =>
 241               coreTypeToWeakType tbranches >>= fun tbranches' =>
 242                   OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))
 243       end
 244   end.
 245
 246
 247
 248