src/ExtractionMain.v

   1 (*********************************************************************************************************************************)
   2 (* ExtractionMain:                                                                                                               *)
   3 (*                                                                                                                               *)
   4 (*    This module is the "top level" for extraction                                                                              *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Require Import Coq.Strings.Ascii.
   9 Require Import Coq.Strings.String.
  10 Require Import Coq.Lists.List.
  11
  12 Require Import Preamble.
  13 Require Import General.
  14
  15 Require Import NaturalDeduction.
  16
  17 Require Import HaskKinds.
  18 Require Import HaskLiteralsAndTyCons.
  19 Require Import HaskCoreVars.
  20 Require Import HaskCoreTypes.
  21 Require Import HaskCore.
  22 Require Import HaskWeakVars.
  23 Require Import HaskWeakTypes.
  24 Require Import HaskWeak.
  25 Require Import HaskStrongTypes.
  26 Require Import HaskStrong.
  27 Require Import HaskProof.
  28 Require Import HaskCoreToWeak.
  29 Require Import HaskWeakToStrong.
  30 Require Import HaskStrongToProof.
  31 Require Import HaskProofToLatex.
  32 Require Import HaskStrongToWeak.
  33 Require Import HaskWeakToCore.
  34 Require Import HaskProofToStrong.
  35
  36 Require Import HaskFlattener.
  37
  38 Open Scope string_scope.
  39 Extraction Language Haskell.
  40
  41 (*Extract Inductive vec    => "([])" [ "([])" "(:)" ].*)
  42 (*Extract Inductive Tree   => "([])" [ "([])" "(:)" ].*)
  43 (*Extract Inlined Constant map => "Prelude.map".*)
  44
  45 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
  46 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
  47 Extract Inductive list   => "([])" [ "([])" "(:)" ].
  48 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
  49 Extract Inductive prod   => "(,)" [ "(,)" ].
  50 Extract Inductive sum    => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
  51 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
  52 Extract Inductive bool    => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
  53 Extract Inductive unit    => "()" [ "()" ].
  54 Extract Inlined Constant string_dec => "(==)".
  55 Extract Inlined Constant ascii_dec => "(==)".
  56
  57 Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
  58 Extract Constant zero   => "'\000'".
  59 Extract Constant one    => "'\001'".
  60 Extract Constant shift  => "shiftAscii".
  61
  62 Unset Extraction Optimize.
  63 Unset Extraction AutoInline.
  64
  65 Variable Name : Type.  Extract Inlined Constant Name => "Name.Name".
  66 Variable mkSystemName : Unique -> string -> nat -> Name.
  67   Extract Inlined Constant mkSystemName =>
  68     "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
  69 Variable mkTyVar : Name -> Kind -> CoreVar.
  70   Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
  71 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
  72   Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
  73 Variable mkExVar : Name -> CoreType -> CoreVar.
  74   Extract Inlined Constant mkExVar => "Id.mkLocalId".
  75
  76 Section core2proof.
  77   Context (ce:@CoreExpr CoreVar).
  78
  79   Definition Γ : TypeEnv := nil.
  80
  81   Definition Δ : CoercionEnv Γ := nil.
  82
  83   Definition φ : TyVarResolver Γ :=
  84     fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
  85     (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
  86
  87   Definition ψ : CoVarResolver Γ Δ :=
  88     fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
  89
  90   (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
  91    * free tyvars in them *)
  92   Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
  93     match coreVarToWeakVar cv with
  94       | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
  95                           | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
  96                                                          toString cv+++": " +++ s)
  97                           | OK    t => t @@ nil
  98                         end
  99       | WTypeVar _   => Prelude_error "top-level xi got a type variable"
 100       | WCoerVar _   => Prelude_error "top-level xi got a coercion variable"
 101     end.
 102
 103   Definition header : string :=
 104     "\documentclass{article}"+++eol+++
 105     "\usepackage{amsmath}"+++eol+++
 106     "\usepackage{amssymb}"+++eol+++
 107     "\usepackage{proof}"+++eol+++
 108     "\usepackage{trfrac}       % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
 109     "\def\code#1#2{\Box_{#1} #2}"+++eol+++
 110     "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
 111     "\usepackage[tightpage,active]{preview}"+++eol+++
 112     "\begin{document}"+++eol+++
 113     "\setlength\PreviewBorder{5pt}"+++eol.
 114
 115   Definition footer : string :=
 116     eol+++"\end{document}"+++
 117     eol.
 118
 119   (* core-to-string (-dcoqpass) *)
 120   Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
 121     addErrorMessage ("input CoreSyn: " +++ toString ce)
 122     (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 123       coreExprToWeakExpr ce >>= fun we =>
 124         addErrorMessage ("WeakExpr: " +++ toString we)
 125           ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 126             ((weakTypeOfWeakExpr we) >>= fun t =>
 127               (addErrorMessage ("WeakType: " +++ toString t)
 128                 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 129                   addErrorMessage ("HaskType: " +++ toString τ)
 130                   ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
 131                     OK (eol+++eol+++eol+++
 132                         "\begin{preview}"+++eol+++
 133                         "$\displaystyle "+++
 134                         toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
 135                         " $"+++eol+++
 136                         "\end{preview}"+++eol+++eol+++eol)
 137                   )))))))).
 138
 139   Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
 140     match coreToStringExpr' ce with
 141       | OK x => x
 142       | Error s => Prelude_error s
 143     end.
 144
 145   Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
 146     match binds with
 147       | CoreNonRec _ e => coreToStringExpr e
 148       | CoreRec    lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
 149     end.
 150
 151   Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
 152     header +++
 153     (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
 154     +++ footer.
 155
 156
 157   (* core-to-core (-fcoqpass) *)
 158   Section CoreToCore.
 159
 160     Definition mkWeakTypeVar (u:Unique)(k:Kind)                 : WeakTypeVar :=
 161       weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
 162     Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
 163       weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
 164     Definition mkWeakExprVar (u:Unique)(t:WeakType)             : WeakExprVar :=
 165       weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
 166
 167     Context (hetmet_brak  : WeakExprVar).
 168     Context (hetmet_esc   : WeakExprVar).
 169     Context (uniqueSupply : UniqSupply).
 170
 171     Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
 172       match ut with
 173         uniqM f =>
 174          f uniqueSupply >>= fun x => OK (snd x)
 175       end.
 176
 177     Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
 178       intros.
 179       induction ln.
 180       exists O.
 181       intros.
 182       inversion H.
 183       destruct IHln as [n pf].
 184       exists (plus (S n) a).
 185       intros.
 186       destruct H.
 187       omega.
 188       fold (@In _ n' ln) in H.
 189       set (pf n' H) as q.
 190       omega.
 191       Defined.
 192
 193   Definition FreshNat : @FreshMonad nat.
 194     refine {| FMT       := fun T => nat -> prod nat T
 195             ; FMT_fresh := _
 196            |}.
 197     Focus 2.
 198     intros.
 199     refine ((S H),_).
 200     set (larger tl) as q.
 201     destruct q as [n' pf].
 202     exists n'.
 203     intros.
 204     set (pf _ H0) as qq.
 205     omega.
 206
 207     refine {| returnM := fun a (v:a) => _ |}.
 208       intro n. exact (n,v).
 209       intros.
 210       set (X H) as q.
 211       destruct q as [n' v].
 212       set (X0 v n') as q'.
 213       exact q'.
 214       Defined.
 215
 216     Definition unFresh {T} : @FreshM _ FreshNat T -> T.
 217       intros.
 218       destruct X.
 219       exact O.
 220       apply t.
 221       Defined.
 222
 223   End CoreToCore.
 224
 225   Definition coreVarToWeakExprVarOrError cv :=
 226     match coreVarToWeakVar cv with
 227       | WExprVar wv => wv
 228       | _           => Prelude_error "IMPOSSIBLE"
 229     end.
 230
 231   Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
 232     ND Rule
 233        [ Γ > Δ > Σ             |- [a ---> s @@ lev ] ]
 234        [ Γ > Δ > Σ,,[a @@ lev] |-       [ s @@ lev ] ].
 235     eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ].
 236     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 237     apply nd_prod.
 238     apply nd_id.
 239     apply nd_rule.
 240     apply RVar.
 241     Defined.
 242
 243   Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
 244     ND Rule [] [ Γ > Δ > [        ] |- [a ---> s @@ lev ] ] ->
 245     ND Rule [] [ Γ > Δ > [a @@ lev] |-       [ s @@ lev ] ].
 246     intro pf.
 247     eapply nd_comp.
 248     apply pf.
 249     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
 250     apply curry.
 251     Defined.
 252
 253   Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
 254     ND Rule [] [ Γ > Δ >                       [] |- [a1 ---> (a2 ---> s) @@ lev ] ] ->
 255     ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |-                 [ s @@ lev ] ].
 256     intro pf.
 257     eapply nd_comp.
 258     eapply pf.
 259     clear pf.
 260     eapply nd_comp.
 261     eapply curry.
 262     eapply nd_comp.
 263     eapply nd_rule.
 264     eapply RArrange.
 265     eapply RCanL.
 266     apply curry.
 267     Defined.
 268
 269   Section coqPassCoreToCore.
 270     Context
 271     (hetmet_brak  : CoreVar)
 272     (hetmet_esc   : CoreVar)
 273     (uniqueSupply : UniqSupply)
 274     (lbinds:list (@CoreBind CoreVar))
 275     (hetmet_PGArrowTyCon : TyFun)
 276     (hetmet_pga_id : CoreVar)
 277     (hetmet_pga_comp : CoreVar)
 278     (hetmet_pga_first : CoreVar)
 279     (hetmet_pga_second : CoreVar)
 280     (hetmet_pga_cancell : CoreVar)
 281     (hetmet_pga_cancelr : CoreVar)
 282     (hetmet_pga_uncancell : CoreVar)
 283     (hetmet_pga_uncancelr : CoreVar)
 284     (hetmet_pga_assoc : CoreVar)
 285     (hetmet_pga_unassoc : CoreVar)
 286     (hetmet_pga_copy : CoreVar)
 287     (hetmet_pga_drop : CoreVar)
 288     (hetmet_pga_swap : CoreVar)
 289     (hetmet_pga_applyl : CoreVar)
 290     (hetmet_pga_applyr : CoreVar)
 291     (hetmet_pga_curryl : CoreVar)
 292     (hetmet_pga_curryr : CoreVar)
 293     .
 294
 295     Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil         ★ TyFunApp_nil.
 296     Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★  :=
 297       TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b.
 298     Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
 299       TApp (TApp (TApp (@TyFunApp TV
 300         hetmet_PGArrowTyCon
 301         nil _ TyFunApp_nil) a) b) c.
 302     Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
 303
 304     Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
 305       fun TV ite => TApp (TApp (TApp (@TyFunApp TV
 306         hetmet_PGArrowTyCon
 307         nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
 308
 309     Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
 310       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
 311       intros.
 312       inversion X; subst.
 313       inversion X1; subst.
 314       apply f; auto.
 315       Defined.
 316
 317     Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
 318       : ND Rule [] [ Γ > Δ > [] |- [f x y @@ l] ].
 319       apply nd_rule.
 320       refine (@RGlobal Γ Δ l
 321         {| glob_wv    := coreVarToWeakExprVarOrError cv
 322           ; glob_kinds := κ₁ :: κ₂ :: nil
 323           ; glob_tf    := mkGlob2'(Γ:=Γ) f
 324           |} (ICons _ _ x (ICons _ _ y INil))).
 325       Defined.
 326
 327     Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
 328       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
 329       intros.
 330       inversion X; subst.
 331       inversion X1; subst.
 332       inversion X3; subst.
 333       apply f; auto.
 334       Defined.
 335
 336     Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
 337       : ND Rule [] [ Γ > Δ > [] |- [f x y z @@ l] ].
 338       apply nd_rule.
 339       refine (@RGlobal Γ Δ l
 340         {| glob_wv    := coreVarToWeakExprVarOrError cv
 341           ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
 342           ; glob_tf    := mkGlob3'(Γ:=Γ) f
 343           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
 344       Defined.
 345
 346     Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
 347       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
 348       intros.
 349       inversion X; subst.
 350       inversion X1; subst.
 351       inversion X3; subst.
 352       inversion X5; subst.
 353       apply f; auto.
 354       Defined.
 355
 356     Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
 357       : ND Rule [] [ Γ > Δ > [] |- [f x y z q @@ l] ].
 358       apply nd_rule.
 359       refine (@RGlobal Γ Δ l
 360         {| glob_wv    := coreVarToWeakExprVarOrError cv
 361           ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
 362           ; glob_tf    := mkGlob4'(Γ:=Γ) f
 363           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
 364       Defined.
 365
 366     Definition gat {Γ}(x:Tree ??(HaskType Γ ★))  := @ga_mk_tree ga_unit ga_prod _ x.
 367
 368     Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
 369     { ga_id        := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_id        (fun ec a => ga_type' ec a a) ec (gat a)
 370     ; ga_cancelr   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancelr   (fun ec a => ga_type' ec _ a) ec (gat a)
 371     ; ga_cancell   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancell   (fun ec a => ga_type' ec _ a) ec (gat a)
 372     ; ga_uncancelr := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat a)
 373     ; ga_uncancell := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat a)
 374     ; ga_assoc     := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc     (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
 375     ; ga_unassoc   := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc   (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
 376     ; ga_swap      := fun Γ Δ ec l a b   => mkGlob3 hetmet_pga_swap      (fun ec a b => ga_type' ec _ _) ec (gat a) (gat b)
 377     ; ga_drop      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_drop      (fun ec a => ga_type' ec _ _) ec (gat a)
 378     ; ga_copy      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_copy      (fun ec a => ga_type' ec _ _) ec (gat a)
 379     ; ga_first     := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat a) (gat b) (gat x))
 380     ; ga_second    := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat a) (gat b) (gat x))
 381     ; ga_comp      := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat a) (gat b) (gat c))
 382 (*  ; ga_lit       := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
 383 (*  ; ga_curry     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
 384 (*  ; ga_apply     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
 385 (*  ; ga_kappa     := fun Γ Δ ec l a     => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
 386     ; ga_lit       := fun Γ Δ ec l a     => Prelude_error "ga_lit"
 387     ; ga_curry     := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
 388     ; ga_apply     := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
 389     ; ga_kappa     := fun Γ Δ ec l a     => Prelude_error "ga_kappa"
 390     }.
 391
 392     Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
 393     Definition hetmet_esc'  := coreVarToWeakExprVarOrError hetmet_esc.
 394
 395     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 396       addErrorMessage ("input CoreSyn: " +++ toString ce)
 397       (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 398         coreExprToWeakExpr ce >>= fun we =>
 399           addErrorMessage ("WeakExpr: " +++ toString we)
 400             ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 401               ((weakTypeOfWeakExpr we) >>= fun t =>
 402                 (addErrorMessage ("WeakType: " +++ toString t)
 403                   ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 404
 405                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 406
 407                       (addErrorMessage ("HaskStrong...")
 408                         (let haskProof := flatten_proof my_ga (@expr2proof _ _ _ _ _ _ e)
 409                          in (* insert HaskProof-to-HaskProof manipulations here *)
 410                          OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 411                          >>= fun e' =>
 412                            (snd e') >>= fun e'' =>
 413                          strongExprToWeakExpr hetmet_brak' hetmet_esc' mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 414                            (projT2 e'') INil
 415                          >>= fun q =>
 416                            OK (weakExprToCoreExpr q)
 417                     )))))))))).
 418
 419     Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
 420       match coreToCoreExpr' ce with
 421         | OK x    => x
 422         | Error s => Prelude_error s
 423       end.
 424
 425     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
 426       match binds with
 427         | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
 428
 429         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
 430                             (* FIXME: doesn't deal with the case where top level recursive binds change type *)
 431 (*
 432           match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
 433             | CoreELet (CoreRec lbe') => lbe'
 434             | x                       => Prelude_error
 435                                             ("coreToCoreExpr was given a letrec, " +++
 436                                              "but returned something that wasn't a letrec: " +++ toString x)
 437           end
 438 *)
 439       end.
 440
 441     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 442       map coreToCoreBind lbinds.
 443
 444   End coqPassCoreToCore.
 445
 446     Definition coqPassCoreToCore
 447     (hetmet_brak  : CoreVar)
 448     (hetmet_esc   : CoreVar)
 449     (uniqueSupply : UniqSupply)
 450     (lbinds:list (@CoreBind CoreVar))
 451     (hetmet_PGArrowTyCon : TyFun)
 452     (hetmet_pga_id : CoreVar)
 453     (hetmet_pga_comp : CoreVar)
 454     (hetmet_pga_first : CoreVar)
 455     (hetmet_pga_second : CoreVar)
 456     (hetmet_pga_cancell : CoreVar)
 457     (hetmet_pga_cancelr : CoreVar)
 458     (hetmet_pga_uncancell : CoreVar)
 459     (hetmet_pga_uncancelr : CoreVar)
 460     (hetmet_pga_assoc : CoreVar)
 461     (hetmet_pga_unassoc : CoreVar)
 462     (hetmet_pga_copy : CoreVar)
 463     (hetmet_pga_drop : CoreVar)
 464     (hetmet_pga_swap : CoreVar)
 465     (hetmet_pga_applyl : CoreVar)
 466     (hetmet_pga_applyr : CoreVar)
 467     (hetmet_pga_curryl : CoreVar)
 468     (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=
 469     coqPassCoreToCore'
 470        hetmet_brak
 471        hetmet_esc
 472        uniqueSupply
 473        hetmet_PGArrowTyCon
 474        hetmet_pga_id
 475        hetmet_pga_comp
 476        hetmet_pga_first
 477        hetmet_pga_second
 478        hetmet_pga_cancell
 479        hetmet_pga_cancelr
 480        hetmet_pga_uncancell
 481        hetmet_pga_uncancelr
 482        hetmet_pga_assoc
 483        hetmet_pga_unassoc
 484        hetmet_pga_copy
 485        hetmet_pga_drop
 486        hetmet_pga_swap
 487        lbinds
 488        (*
 489        hetmet_pga_applyl
 490        hetmet_pga_applyr
 491        hetmet_pga_curryl
 492        *)
 493        .
 494
 495 End core2proof.