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