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