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 HaskCoreLiterals.
  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 form *)
  27 Variable hetmet_brak_name   : CoreName.              Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
  28
  29 (* the magic wired-in name for the modal type elimination form *)
  30 Variable hetmet_esc_name    : CoreName.              Extract Inlined Constant hetmet_esc_name  => "PrelNames.hetmet_esc_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: " +++ 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) : ??(CoreVar * 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         | WTypeVar tv => Some (v,tv,tbody)
  95         | WCoerVar _  => None
  96       end else None
  97   | _ => None
  98 end.
  99
 100 Definition isEsc (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
 101 match ce with
 102   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
 103     => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
 104       match coreVarToWeakVar ec with
 105         | WExprVar _  => None
 106         | WTypeVar tv => Some (v,tv,tbody)
 107         | WCoerVar _  => None
 108       end else None
 109   | _ => None
 110 end.
 111
 112 (* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
 113 Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list WeakType) :=
 114   match wt with
 115     | WTyCon tc        => OK (tc,acc)
 116     | WAppTy t1 t2     => expectTyConApp t1 (t2::acc)
 117     | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ wt)
 118     | _                => Error ("expectTyConApp encountered " +++ wt)
 119   end.
 120
 121 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
 122   match ce with
 123     | CoreELit   lit   => OK (WELit lit)
 124     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
 125     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
 126     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>
 127                               OK (WECast e' (coreCoercionToWeakCoercion co))
 128
 129     | CoreEVar   v     => match coreVarToWeakVar v with
 130                             | WExprVar ev => OK (WEVar ev)
 131                             | WTypeVar _  => Error "found a type variable inside an EVar!"
 132                             | WCoerVar _  => Error "found a coercion variable inside an EVar!"
 133                           end
 134
 135     | CoreEApp   e1 e2 => match isBrak e1 with
 136                             | Some (v,tv,t) =>
 137                               coreExprToWeakExpr e2 >>= fun e' =>
 138                                 coreTypeToWeakType t >>= fun t' =>
 139                                 OK (WEBrak v tv e' t')
 140                             | None    => match isEsc e1 with
 141                                            | Some (v,tv,t) =>
 142                                              coreExprToWeakExpr e2 >>= fun e' =>
 143                                                coreTypeToWeakType t >>= fun t' =>
 144                                                  OK (WEEsc v tv e' t')
 145                                            | None    => coreExprToWeakExpr e1 >>= fun e1' =>
 146                                              match e2 with
 147                                                | CoreEType t =>
 148                                                  coreTypeToWeakType t >>= fun t' =>
 149                                                    OK (WETyApp e1' t')
 150                                                | _           => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2')
 151                                              end
 152                                          end
 153                           end
 154
 155     | CoreELam   v e => match coreVarToWeakVar v with
 156                          | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam   ev e')
 157                          | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
 158                          | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
 159                        end
 160
 161     | CoreELet   (CoreNonRec v ve) e => match coreVarToWeakVar v with
 162                          | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
 163                                             coreExprToWeakExpr e  >>= fun e'  => OK (WELet ev ve' e')
 164                          | WTypeVar _ => match e with
 165                                               | CoreEType t => Error "saw a type-let"
 166                                               | _           => Error "saw (ELet <tyvar> e) where e!=EType"
 167                                             end
 168                          | WCoerVar _ => Error "saw an (ELet <coercionVar>)"
 169                        end
 170
 171     | CoreELet   (CoreRec rb)      e =>
 172       ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
 173         match cel with
 174           | nil => OK nil
 175           | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
 176             match coreVarToWeakVar v' with
 177               | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
 178               | WTypeVar _  => Error "found a type variable in a recursive let"
 179               | WCoerVar _  => Error "found a coercion variable in a recursive let"
 180             end
 181         end) rb) >>= fun rb' =>
 182       coreExprToWeakExpr e >>= fun e' =>
 183       OK (WELetRec (unleaves' rb') e')
 184
 185     | CoreECase  e v tbranches alts =>
 186       match coreVarToWeakVar v with
 187         | WTypeVar _  => Error "found a type variable in a case"
 188         | WCoerVar _  => Error "found a coercion variable in a case"
 189         | WExprVar ev =>
 190         coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
 191         coreExprToWeakExpr e >>= fun e' =>
 192           expectTyConApp te' nil >>= fun tca =>
 193             let (tc,lt) := tca in
 194           ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
 195                 : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
 196             match branches with
 197               | nil => OK nil
 198               | (mkTriple alt vars e)::rest =>
 199                   mkBranches rest >>= fun rest' =>
 200                     coreExprToWeakExpr e >>= fun e' =>
 201                     match alt with
 202                       | DEFAULT                => OK ((DEFAULT,nil,nil,nil,e')::rest')
 203                       | LitAlt lit             => OK ((LitAlt lit,nil,nil,nil,e')::rest')
 204                       | DataAlt dc             => let vars := map coreVarToWeakVar vars in
 205                         OK (((DataAlt dc),
 206                         (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
 207                         (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
 208                         (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
 209                         e')::rest')
 210                     end
 211             end) alts)
 212           >>= fun branches =>
 213             coreExprToWeakExpr e >>= fun scrutinee =>
 214               coreTypeToWeakType tbranches >>= fun tbranches' =>
 215                   OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))
 216       end
 217   end.
 218
 219
 220
 221