From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Mon, 9 May 2011 06:29:31 +0000 (-0700)
Subject: allow -fcoqpass to change the type of top-level bindings
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=4ad68fe2894b35c21f2feb7b176d2b0f146ff6d3

allow -fcoqpass to change the type of top-level bindings
---

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index e628f26..350506e 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -219,46 +219,6 @@ Section core2proof.
       exact O.
       apply t.
       Defined.
-(*
-    Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
-      addErrorMessage ("input CoreSyn: " +++ toString ce)
-      (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
-        coreExprToWeakExpr ce >>= fun we =>
-          addErrorMessage ("WeakExpr: " +++ toString we)
-            ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
-              ((weakTypeOfWeakExpr we) >>= fun t =>
-                (addErrorMessage ("WeakType: " +++ toString t)
-                  ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
-
-                    ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
-
-                      (addErrorMessage ("HaskStrong...")
-                        (let haskProof := (*flatten_proof'*) (@expr2proof _ _ _ _ _ _ e)
-                         in (* insert HaskProof-to-HaskProof manipulations here *)
-                         OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
-                         >>= fun e' =>
-                           (snd e') >>= fun e'' =>
-                         strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
-                           (projT2 e'') INil
-                         >>= fun q =>
-                           OK (weakExprToCoreExpr q)
-                    )))))))))).
-
-    Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
-      match coreToCoreExpr' ce with
-        | OK x    => x
-        | Error s => Prelude_error s
-      end.
-  
-    Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
-      match binds with
-        | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
-        | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
-      end.
-
-    Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
-      map coreToCoreBind lbinds.
-  *)
 
   End CoreToCore.
 
@@ -461,11 +421,21 @@ Section core2proof.
         | OK x    => x
         | Error s => Prelude_error s
       end.
-  
+
     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
       match binds with
-        | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
+        | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
+
         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
+                            (* FIXME: doesn't deal with the case where top level recursive binds change type *)
+(*
+          match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
+            | CoreELet (CoreRec lbe') => lbe'
+            | x                       => Prelude_error
+                                            ("coreToCoreExpr was given a letrec, " +++
+                                             "but returned something that wasn't a letrec: " +++ toString x)
+          end
+*)
       end.
 
     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v
index 8aa81ee..0fbaeb5 100644
--- a/src/HaskCoreTypes.v
+++ b/src/HaskCoreTypes.v
@@ -38,6 +38,7 @@ Variable coreCoercionToString  : CoreCoercion -> string.    Extract Inlined Cons
 Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind".
 Variable kindOfCoreType   : CoreType -> Kind.   Extract Inlined Constant kindOfCoreType   => "(coreKindToKind . Coercion.typeKind)".
 Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)".
+Variable setVarType       : CoreVar -> CoreType -> CoreVar. Extract Inlined Constant setVarType       => "Var.setVarType".
 
 (* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
 Variable coreTyCon_eq         : EqDecider CoreTyCon.       Extract Inlined Constant coreTyCon_eq          => "(==)".