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