From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Mon, 7 Mar 2011 13:41:17 +0000 (-0800)
Subject: added HaskCoreToWeak
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=95d220bc417942c682bffa4adcd89513711486ae

added HaskCoreToWeak
---

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
new file mode 100644
index 0000000..1b3ffcf
--- /dev/null
+++ b/src/HaskCoreToWeak.v
@@ -0,0 +1,96 @@
+(*********************************************************************************************************************************)
+(* 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.
+
diff --git a/src/Main.v b/src/Main.v
index 99c6734..300dfb8 100644
--- a/src/Main.v
+++ b/src/Main.v
@@ -10,10 +10,10 @@ Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskWeak.
-(*Require Import HaskCoreToWeak.*)
+Require Import HaskCoreToWeak.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 (*Require Import HaskStrongToProof.*)
 Require Import HaskProof.
 (*Require Import HaskWeakToStrong.*)
-(*Require Import HaskProofToLatex.*)
+Require Import HaskProofToLatex.