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"
  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) : ??(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 v with
  83         | WExprVar _  => None
  84         | WTypeVar tv => Some (tv,tbody)
  85         | WCoerVar _  => None
  86       end else None
  87   | _ => None
  88 end.
  89 Definition isEsc (ce:@CoreExpr 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 v with
  94         | WExprVar _  => None
  95         | WTypeVar tv => Some (tv,tbody)
  96         | WCoerVar _  => None
  97       end else None
  98   | _ => None
  99 end.
 100
 101 Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : ???WeakCoercion :=
 102   let (t1,t2) := coreCoercionKind cc
 103   in  coreTypeToWeakType t1 >>= fun t1' =>
 104     coreTypeToWeakType t2 >>= fun t2' =>
 105     OK (weakCoercion t1' t2' cc).
 106
 107 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
 108   match ce with
 109     | CoreELit   lit   => OK (WELit lit)
 110     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
 111     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
 112     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>
 113                             coreCoercionToWeakCoercion co >>= fun co' =>
 114                               OK (WECast e' co')
 115
 116     | CoreEVar   v     => match coreVarToWeakVar v with
 117                             | WExprVar ev => OK (WEVar ev)
 118                             | WTypeVar _  => Error "found a type variable inside an EVar!"
 119                             | WCoerVar _  => Error "found a coercion variable inside an EVar!"
 120                           end
 121
 122     | CoreEApp   e1 e2 => match isBrak e1 with
 123                             | Some (tv,t) =>
 124                               coreExprToWeakExpr e2 >>= fun e' =>
 125                                 coreTypeToWeakType t >>= fun t' =>
 126                                 OK (WEBrak tv e' t')
 127                             | None    => match isEsc e1 with
 128                                            | Some (tv,t) =>
 129                                              coreExprToWeakExpr e2 >>= fun e' =>
 130                                                coreTypeToWeakType t >>= fun t' =>
 131                                                  OK (WEEsc tv e' t')
 132                                            | None    => coreExprToWeakExpr e1 >>= fun e1' =>
 133                                              match e2 with
 134                                                | CoreEType t =>
 135                                                  coreTypeToWeakType t >>= fun t' =>
 136                                                    OK (WETyApp e1' t')
 137                                                | _           => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2')
 138                                              end
 139                                          end
 140                           end
 141
 142     | CoreELam   v e => match coreVarToWeakVar v with
 143                          | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam   ev e')
 144                          | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
 145                          | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
 146                        end
 147
 148     | CoreELet   (CoreNonRec v ve) e => match coreVarToWeakVar v with
 149                          | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
 150                                             coreExprToWeakExpr e  >>= fun e'  => OK (WELet ev ve' e')
 151                          | WTypeVar _ => match e with
 152                                               | CoreEType t => Error "saw a type-let"
 153                                               | _           => Error "saw (ELet <tyvar> e) where e!=EType"
 154                                             end
 155                          | WCoerVar _ => Error "saw an (ELet <coercionVar>)"
 156                        end
 157
 158     | CoreELet   (CoreRec rb)      e =>
 159       ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
 160         match cel with
 161           | nil => OK nil
 162           | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
 163             match coreVarToWeakVar v' with
 164               | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
 165               | WTypeVar _  => Error "found a type variable in a recursive let"
 166               | WCoerVar _  => Error "found a coercion variable in a recursive let"
 167             end
 168         end) rb) >>= fun rb' =>
 169       coreExprToWeakExpr e >>= fun e' =>
 170       OK (WELetRec (unleaves' rb') e')
 171
 172     | CoreECase  e v tbranches alts =>
 173       match coreVarToWeakVar v with
 174         | WTypeVar _  => Error "found a type variable in a case"
 175         | WCoerVar _  => Error "found a coercion variable in a case"
 176         | WExprVar ev =>
 177       coreExprToWeakExpr e >>= fun e' =>
 178         weakTypeOfWeakExpr e' >>= fun te' =>
 179           (match isTyConApp te' nil with None => Error "expectTyConApp encountered strange type" | Some x => OK x end)
 180              >>= fun tca =>
 181             let (tc,lt) := tca in
 182           ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
 183                 : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
 184             match branches with
 185               | nil => OK nil
 186               | (mkTriple alt vars e)::rest =>
 187                   mkBranches rest >>= fun rest' =>
 188                     coreExprToWeakExpr e >>= fun e' =>
 189                     match alt with
 190                       | DEFAULT                => OK ((DEFAULT,nil,nil,nil,e')::rest')
 191                       | LitAlt lit             => OK ((LitAlt lit,nil,nil,nil,e')::rest')
 192                       | DataAlt dc             => let vars := map coreVarToWeakVar vars in
 193                         OK (((DataAlt dc),
 194                         (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
 195                         (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
 196                         (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
 197                         e')::rest')
 198                     end
 199             end) alts)
 200           >>= fun branches =>
 201             coreExprToWeakExpr e >>= fun scrutinee =>
 202               coreTypeToWeakType tbranches >>= fun tbranches' =>
 203                   OK (WELet ev scrutinee (WECase (WEVar ev) tbranches' tc lt (unleaves branches)))
 204       end
 205   end.
 206