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