src/HaskCoreToWeak.v

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