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