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