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