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 HaskGeneral.
  10 Require Import HaskLiterals.
  11 Require Import HaskCoreVars.
  12 Require Import HaskCoreTypes.
  13 Require Import HaskCore.
  14 Require Import HaskWeakVars.
  15 Require Import HaskWeak.
  16
  17 Variable coreVarToWeakVar      : CoreVar  -> WeakVar.   Extract Inlined Constant coreVarToWeakVar    => "coreVarToWeakVar".
  18
  19 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
  20 Definition isBrak (ce:CoreExpr CoreVar) : ??WeakTypeVar :=
  21 match ce with
  22   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
  23     => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
  24       match coreVarToWeakVar v with
  25         | WExprVar _  => None
  26         | WTypeVar tv => Some tv
  27         | WCoerVar _  => None
  28       end else None
  29   | _ => None
  30 end.
  31 Definition isEsc (ce:CoreExpr CoreVar) : ??WeakTypeVar :=
  32 match ce with
  33   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
  34     => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
  35       match coreVarToWeakVar v with
  36         | WExprVar _  => None
  37         | WTypeVar tv => Some tv
  38         | WCoerVar _  => None
  39       end else None
  40   | _ => None
  41 end.
  42
  43 Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : WeakCoercion :=
  44   let (t1,t2) := coreCoercionKind cc
  45   in  weakCoercion t1 t2 cc.
  46
  47 Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr :=
  48   match ce with
  49     | CoreELit   lit   => OK (WELit lit)
  50     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
  51     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
  52     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>
  53                             OK (WECast e' (coreCoercionToWeakCoercion co))
  54
  55     | CoreEVar   v     => match coreVarToWeakVar v with
  56                             | WExprVar ev => OK (WEVar ev)
  57                             | WTypeVar _  => Error "found a type variable inside an EVar!"
  58                             | WCoerVar _  => Error "found a coercion variable inside an EVar!"
  59                           end
  60
  61     | CoreEApp   e1 e2 => match isBrak e1 with
  62                             | Some tv => coreExprToWeakExpr e2 >>= fun e' => OK (WEBrak tv e')
  63                             | None    => match isEsc e1 with
  64                                            | Some tv => coreExprToWeakExpr e2 >>= fun e' => OK (WEEsc tv e')
  65                                            | None    => coreExprToWeakExpr e1 >>= fun e1' =>
  66                                              match e2 with
  67                                                | CoreEType t => OK (WETyApp e1' t)
  68                                                | _           => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2')
  69                                              end
  70                                          end
  71                           end
  72
  73     | CoreELam   v e => match coreVarToWeakVar v with
  74                          | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam   ev e')
  75                          | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
  76                          | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
  77                        end
  78
  79     | CoreELet   (CoreNonRec v ve) e => match coreVarToWeakVar v with
  80                          | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
  81                                             coreExprToWeakExpr e  >>= fun e'  => OK (WELet ev ve' e')
  82                          | WTypeVar _ => match e with
  83                                               | CoreEType t => Error "saw a type-let"
  84                                               | _           => Error "saw (ELet <tyvar> e) where e!=EType"
  85                                             end
  86                          | WCoerVar _ => Error "saw an (ELet <coercionVar>)"
  87                        end
  88
  89     | CoreELet   (CoreRec rb)      e =>
  90       ((fix coreExprToWeakExprList (cel:list (CoreVar * (CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
  91         match cel with
  92           | nil => OK nil
  93           | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
  94             match coreVarToWeakVar v' with
  95               | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
  96               | WTypeVar _  => Error "found a type variable in a recursive let"
  97               | WCoerVar _  => Error "found a coercion variable in a recursive let"
  98             end
  99         end) rb) >>= fun rb' =>
 100       coreExprToWeakExpr e >>= fun e' =>
 101       OK (WELetRec (unleaves' rb') e')
 102
 103     | CoreECase  e v tbranches alts =>
 104       match coreVarToWeakVar v with
 105         | WTypeVar _  => Error "found a type variable in a case"
 106         | WCoerVar _  => Error "found a coercion variable in a case"
 107         | WExprVar ev =>
 108       coreExprToWeakExpr e
 109       >>= fun e' => coreTypeOfWeakExpr e' >>= fun te' =>
 110       match te' with
 111         | TyConApp _ tc lt =>
 112           ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (CoreExpr CoreVar)))
 113                 : ???(list (AltCon*list WeakVar*WeakExpr)) :=
 114             match branches with
 115               | nil => OK nil
 116               | (mkTriple alt vars e)::rest =>
 117                   mkBranches rest >>= fun rest' =>
 118                     coreExprToWeakExpr e >>= fun e' =>
 119                     match alt with
 120                       | DEFAULT                => OK ((DEFAULT,nil,e')::rest')
 121                       | LitAlt lit             => OK ((LitAlt lit,nil,e')::rest')
 122                       | DataAlt _ _ _ _ tc' dc => OK (((DataAlt _ dc),(map coreVarToWeakVar vars),e')::rest')
 123                     end
 124             end) alts)
 125           >>= fun branches => coreExprToWeakExpr e
 126             >>= fun scrutinee =>
 127               list2vecOrError lt _ >>= fun lt' =>
 128                   OK (WELet ev scrutinee (WECase (WEVar ev) tbranches tc lt' (unleaves branches)))
 129         | _ => Error "found a case whose scrutinee's type wasn't a TyConApp"
 130       end
 131       end
 132   end.
 133