X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskWeakToCore.v;h=1194251c394191dc201ebc3063d8cc3388021dec;hb=8efffc7368b5e54c42461f45a9708ff2828409a4;hp=cfaf65e21f9cc4652e1004241069a37e9c50d873;hpb=1f411b48dd607e76a65903e8506d0ae5e7470321;p=coq-hetmet.git

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index cfaf65e..1194251 100644
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -15,13 +15,12 @@ Require Import HaskCore.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.
-Require Import HaskCoreToWeak.
 
 Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar.
   Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet".
 
 Variable sortAlts  : forall {a}{b}, list (@triple AltCon a b) -> list (@triple AltCon a b).
-  Extract Inlined Constant mkCoreLet => "sortAlts".
+  Extract Inlined Constant sortAlts => "sortAlts".
   Implicit Arguments sortAlts [[a][b]].
 
 Variable trustMeCoercion           : CoreCoercion.
@@ -31,35 +30,38 @@ Variable trustMeCoercion           : CoreCoercion.
 Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType.
   Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)".
 
-Section HaskWeakToCore.
+Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
+   fun _ => trustMeCoercion.
 
-  (* the CoreVar for the "magic" bracket/escape identifiers must be created from within one of the monads *)
-  Context (hetmet_brak_var : CoreVar).
-  Context (hetmet_esc_var  : CoreVar).
 
-  Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion :=
-    fun _ => trustMeCoercion.
-
-  Fixpoint weakExprToCoreExpr (f:Fresh unit (fun _ => WeakExprVar)) (me:WeakExpr) : @CoreExpr CoreVar :=
+  Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   match me with
   | WEVar   (weakExprVar v _)            => CoreEVar  v
   | WELit   lit                          => CoreELit  lit
-  | WEApp   e1 e2                        => CoreEApp     (weakExprToCoreExpr f e1) (weakExprToCoreExpr f e2)
-  | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr f e ) (CoreEType (weakTypeToCoreType t))
-  | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr f e )
+  | WEApp   e1 e2                        => CoreEApp     (weakExprToCoreExpr e1) (weakExprToCoreExpr e2)
+  | WETyApp e t                          => CoreEApp     (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t))
+  | WECoApp e co                         => CoreEApp     (weakExprToCoreExpr e )
                                                            (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co)))
-  | WENote  n e                          => CoreENote n  (weakExprToCoreExpr f e )
-  | WELam   (weakExprVar ev _  ) e       => CoreELam  ev (weakExprToCoreExpr f e )
-  | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr f e )
-  | WECoLam (weakCoerVar cv _ _ _) e     => CoreELam  cv (weakExprToCoreExpr f e )
-  | WECast  e co                         => CoreECast    (weakExprToCoreExpr f e ) (weakCoercionToCoreCoercion co)
-  | WEBrak  (weakTypeVar ec _) e t       => CoreEApp  (CoreEApp (CoreEVar hetmet_brak_var)
-                                                           (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
-  | WEEsc   (weakTypeVar ec _) e t       => CoreEApp  (CoreEApp (CoreEVar hetmet_esc_var)
-                                                           (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
-  | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr f ve))  (weakExprToCoreExpr f e)
-  | WECase  e tbranches tc types alts    => let (v,f') := next _ _ f tt  in
-                                            CoreECase (weakExprToCoreExpr f' e) v (weakTypeToCoreType tbranches)
+  | WENote  n e                          => CoreENote n  (weakExprToCoreExpr e )
+  | WELam   (weakExprVar ev _  ) e       => CoreELam  ev (weakExprToCoreExpr e )
+  | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr e )
+  | WECoLam (weakCoerVar cv _ _ _) e     => CoreELam  cv (weakExprToCoreExpr e )
+  | WECast  e co                         => CoreECast    (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
+  | WEBrak  v (weakTypeVar ec _) e t     => fold_left CoreEApp
+                                                   ((CoreEType (TyVarTy ec))::
+                                                     (CoreEType (weakTypeToCoreType t))::
+                                                     (weakExprToCoreExpr e)::
+                                                     nil)
+                                                   (CoreEVar v)
+  | WEEsc   v (weakTypeVar ec _) e t     => fold_left CoreEApp
+                                                   ((CoreEType (TyVarTy ec))::
+                                                     (CoreEType (weakTypeToCoreType t))::
+                                                     (weakExprToCoreExpr e)::
+                                                     nil)
+                                                   (CoreEVar v)
+  | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr ve))  (weakExprToCoreExpr e)
+  | WECase  vscrut e tbranches tc types alts  =>
+                                            CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches)
                                               (sortAlts ((
                                                 fix mkCaseBranches (alts:Tree 
                                                   ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
@@ -72,19 +74,19 @@ Section HaskWeakToCore.
                                                         (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars)
                                                         (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars))
                                                       (map (fun v:WeakExprVar => weakVarToCoreVar v) evars))
-                                                      (weakExprToCoreExpr f' e))::nil
+                                                      (weakExprToCoreExpr e))::nil
                                                 end
                                               ) alts))
   | WELetRec mlr e                       => CoreELet (CoreRec
                                                ((fix mkLetBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) :=
                                                  match mlr with
                                                    | T_Leaf None                        => nil
-                                                   | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr f e))::nil
+                                                   | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr e))::nil
                                                    | T_Branch b1 b2                     => app (mkLetBindings b1) (mkLetBindings b2)
                                                  end) mlr))
-                                               (weakExprToCoreExpr f e)
+                                               (weakExprToCoreExpr e)
   end.
 
-End HaskWeakToCore.
+