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