(*********************************************************************************************************************************)
(* HaskCoreToWeak: convert HaskCore to HaskWeak                                                                                  *)
(*********************************************************************************************************************************)

Generalizable All Variables.
Require Import Preamble.
Require Import General.
Require Import HaskGeneral.
Require Import HaskLiterals.
Require Import HaskCoreVars.
Require Import HaskCoreTypes.
Require Import HaskCore.
Require Import HaskWeak.

Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr :=
  match ce with
    | CoreELit   lit   => OK (WELit lit)
    | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
    | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
    | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' => OK (WECast e' co)

    | CoreEVar   v     => match coreVarSort v with
                            | CoreExprVar _ => OK (WEVar v)
                            | CoreTypeVar _ => Error "found a type variable inside an EVar!"
                            | CoreCoerVar _ => Error "found a coercion variable inside an EVar!"
                          end

    | CoreEApp   e1 e2 => match isBrak e1 with
                            | Some tv => coreExprToWeakExpr e2 >>= fun e' => OK (WEBrak tv e')
                            | None    => match isEsc e1 with
                                           | Some tv => coreExprToWeakExpr e2 >>= fun e' => OK (WEEsc tv e')
                                           | None    => coreExprToWeakExpr e1 >>= fun e1' =>
                                             match e2 with
                                               | CoreEType t => OK (WETyApp e1' t)
                                               | _           => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2')
                                             end
                                         end
                          end

    | CoreELam   v e => match coreVarSort v with
                         | CoreExprVar _ => coreExprToWeakExpr e >>= fun e' => OK (WELam   v e')
                         | CoreTypeVar _ => coreExprToWeakExpr e >>= fun e' => OK (WETyLam v e')
                         | CoreCoerVar _ => coreExprToWeakExpr e >>= fun e' => OK (WECoLam v e')
                       end

    | CoreELet   (CoreNonRec v ve) e => match coreVarSort v with
                         | CoreExprVar _ => coreExprToWeakExpr ve >>= fun ve' =>
                                            coreExprToWeakExpr e  >>= fun e'  => OK (WELet v ve' e')
                         | CoreTypeVar _ => match e with
                                              | CoreEType t => Error "saw a type-let"
                                              | _           => Error "saw (ELet <tyvar> e) where e!=EType"
                                            end
                         | CoreCoerVar _ => Error "saw an (ELet <coercionVar>)"
                       end

    | CoreELet   (CoreRec rb)      e =>
      ((fix coreExprToWeakExprList (cel:list (CoreVar * (CoreExpr CoreVar))) : ???(list (CoreVar * WeakExpr)) :=
        match cel with
          | nil => OK nil
          | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
            match coreVarSort v' with
              | CoreExprVar _ => coreExprToWeakExpr e' >>= fun e' => OK ((v',e')::t')
              | CoreTypeVar _ => Error "found a type variable in a recursive let"
              | CoreCoerVar _ => Error "found a coercion variable in a recursive let"
            end
        end) rb) >>= fun rb' =>
      coreExprToWeakExpr e >>= fun e' =>
      OK (WELetRec (unleaves' rb') e')

    | CoreECase  e v tbranches alts => 
      coreExprToWeakExpr e
      >>= fun e' => coreTypeOfWeakExpr e' >>= fun te' =>
      match te' with
        | TyConApp _ tc lt =>
          ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (CoreExpr CoreVar)))
                : ???(list (AltCon*list CoreVar*WeakExpr)) :=
            match branches with
              | nil => OK nil
              | (mkTriple alt vars e)::rest =>
                  mkBranches rest
                  >>= fun rest' => 
                    coreExprToWeakExpr e >>= fun e' => 
                    match alt with
                      | DEFAULT                => OK ((DEFAULT,nil,e')::rest')
                      | LitAlt lit             => OK ((LitAlt lit,nil,e')::rest')
                      | DataAlt _ _ _ _ tc' dc => OK (((DataAlt _ dc),vars,e')::rest')
                    end
            end) alts)
          >>= fun branches => coreExprToWeakExpr e
            >>= fun scrutinee =>
              list2vecOrError lt _ >>= fun lt' => 
                OK (WELet v scrutinee (WECase (WEVar v) tbranches tc lt' (unleaves branches)))
        | _ => Error "found a case whose scrutinee's type wasn't a TyConApp"
      end
  end.