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 HaskGeneral.
   9 Require Import HaskLiterals.
  10 Require Import HaskCoreVars.
  11 Require Import HaskCoreTypes.
  12 Require Import HaskCore.
  13 Require Import HaskWeak.
  14
  15 Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr :=
  16   match ce with
  17     | CoreELit   lit   => OK (WELit lit)
  18     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
  19     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
  20     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' => OK (WECast e' co)
  21
  22     | CoreEVar   v     => match coreVarSort v with
  23                             | CoreExprVar _ => OK (WEVar v)
  24                             | CoreTypeVar _ => Error "found a type variable inside an EVar!"
  25                             | CoreCoerVar _ => Error "found a coercion variable inside an EVar!"
  26                           end
  27
  28     | CoreEApp   e1 e2 => match isBrak e1 with
  29                             | Some tv => coreExprToWeakExpr e2 >>= fun e' => OK (WEBrak tv e')
  30                             | None    => match isEsc e1 with
  31                                            | Some tv => coreExprToWeakExpr e2 >>= fun e' => OK (WEEsc tv e')
  32                                            | None    => coreExprToWeakExpr e1 >>= fun e1' =>
  33                                              match e2 with
  34                                                | CoreEType t => OK (WETyApp e1' t)
  35                                                | _           => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2')
  36                                              end
  37                                          end
  38                           end
  39
  40     | CoreELam   v e => match coreVarSort v with
  41                          | CoreExprVar _ => coreExprToWeakExpr e >>= fun e' => OK (WELam   v e')
  42                          | CoreTypeVar _ => coreExprToWeakExpr e >>= fun e' => OK (WETyLam v e')
  43                          | CoreCoerVar _ => coreExprToWeakExpr e >>= fun e' => OK (WECoLam v e')
  44                        end
  45
  46     | CoreELet   (CoreNonRec v ve) e => match coreVarSort v with
  47                          | CoreExprVar _ => coreExprToWeakExpr ve >>= fun ve' =>
  48                                             coreExprToWeakExpr e  >>= fun e'  => OK (WELet v ve' e')
  49                          | CoreTypeVar _ => match e with
  50                                               | CoreEType t => Error "saw a type-let"
  51                                               | _           => Error "saw (ELet <tyvar> e) where e!=EType"
  52                                             end
  53                          | CoreCoerVar _ => Error "saw an (ELet <coercionVar>)"
  54                        end
  55
  56     | CoreELet   (CoreRec rb)      e =>
  57       ((fix coreExprToWeakExprList (cel:list (CoreVar * (CoreExpr CoreVar))) : ???(list (CoreVar * WeakExpr)) :=
  58         match cel with
  59           | nil => OK nil
  60           | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
  61             match coreVarSort v' with
  62               | CoreExprVar _ => coreExprToWeakExpr e' >>= fun e' => OK ((v',e')::t')
  63               | CoreTypeVar _ => Error "found a type variable in a recursive let"
  64               | CoreCoerVar _ => Error "found a coercion variable in a recursive let"
  65             end
  66         end) rb) >>= fun rb' =>
  67       coreExprToWeakExpr e >>= fun e' =>
  68       OK (WELetRec (unleaves' rb') e')
  69
  70     | CoreECase  e v tbranches alts =>
  71       coreExprToWeakExpr e
  72       >>= fun e' => coreTypeOfWeakExpr e' >>= fun te' =>
  73       match te' with
  74         | TyConApp _ tc lt =>
  75           ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (CoreExpr CoreVar)))
  76                 : ???(list (AltCon*list CoreVar*WeakExpr)) :=
  77             match branches with
  78               | nil => OK nil
  79               | (mkTriple alt vars e)::rest =>
  80                   mkBranches rest
  81                   >>= fun rest' =>
  82                     coreExprToWeakExpr e >>= fun e' =>
  83                     match alt with
  84                       | DEFAULT                => OK ((DEFAULT,nil,e')::rest')
  85                       | LitAlt lit             => OK ((LitAlt lit,nil,e')::rest')
  86                       | DataAlt _ _ _ _ tc' dc => OK (((DataAlt _ dc),vars,e')::rest')
  87                     end
  88             end) alts)
  89           >>= fun branches => coreExprToWeakExpr e
  90             >>= fun scrutinee =>
  91               list2vecOrError lt _ >>= fun lt' =>
  92                 OK (WELet v scrutinee (WECase (WEVar v) tbranches tc lt' (unleaves branches)))
  93         | _ => Error "found a case whose scrutinee's type wasn't a TyConApp"
  94       end
  95   end.
  96