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 (hetmet_flatten : WeakExprVar).
 170     Context (hetmet_unflatten : WeakExprVar).
 171     Context (hetmet_flattened_id : WeakExprVar).
 172     Context (uniqueSupply   : UniqSupply).
 173
 174     Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
 175       match ut with
 176         uniqM f =>
 177          f uniqueSupply >>= fun x => OK (snd x)
 178       end.
 179
 180     Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
 181       intros.
 182       induction ln.
 183       exists O.
 184       intros.
 185       inversion H.
 186       destruct IHln as [n pf].
 187       exists (plus (S n) a).
 188       intros.
 189       destruct H.
 190       omega.
 191       fold (@In _ n' ln) in H.
 192       set (pf n' H) as q.
 193       omega.
 194       Defined.
 195
 196   Definition FreshNat : @FreshMonad nat.
 197     refine {| FMT       := fun T => nat -> prod nat T
 198             ; FMT_fresh := _
 199            |}.
 200     Focus 2.
 201     intros.
 202     refine ((S H),_).
 203     set (larger tl) as q.
 204     destruct q as [n' pf].
 205     exists n'.
 206     intros.
 207     set (pf _ H0) as qq.
 208     omega.
 209
 210     refine {| returnM := fun a (v:a) => _ |}.
 211       intro n. exact (n,v).
 212       intros.
 213       set (X H) as q.
 214       destruct q as [n' v].
 215       set (X0 v n') as q'.
 216       exact q'.
 217       Defined.
 218
 219     Definition unFresh {T} : @FreshM _ FreshNat T -> T.
 220       intros.
 221       destruct X.
 222       exact O.
 223       apply t.
 224       Defined.
 225
 226   End CoreToCore.
 227
 228   Definition coreVarToWeakExprVarOrError cv :=
 229     match coreVarToWeakVar cv with
 230       | WExprVar wv => wv
 231       | _           => Prelude_error "IMPOSSIBLE"
 232     end.
 233
 234   Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
 235     ND Rule
 236        [ Γ > Δ > Σ             |- [a ---> s @@ lev ] ]
 237        [ Γ > Δ > Σ,,[a @@ lev] |-       [ s @@ lev ] ].
 238     eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ].
 239     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 240     apply nd_prod.
 241     apply nd_id.
 242     apply nd_rule.
 243     apply RVar.
 244     Defined.
 245
 246   Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
 247     ND Rule [] [ Γ > Δ > [        ] |- [a ---> s @@ lev ] ] ->
 248     ND Rule [] [ Γ > Δ > [a @@ lev] |-       [ s @@ lev ] ].
 249     intro pf.
 250     eapply nd_comp.
 251     apply pf.
 252     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
 253     apply curry.
 254     Defined.
 255
 256   Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
 257     ND Rule [] [ Γ > Δ >                       [] |- [a1 ---> (a2 ---> s) @@ lev ] ] ->
 258     ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |-                 [ s @@ lev ] ].
 259     intro pf.
 260     eapply nd_comp.
 261     eapply pf.
 262     clear pf.
 263     eapply nd_comp.
 264     eapply curry.
 265     eapply nd_comp.
 266     eapply nd_rule.
 267     eapply RArrange.
 268     eapply RCanL.
 269     apply curry.
 270     Defined.
 271
 272   Section coqPassCoreToCore.
 273     Context
 274     (hetmet_brak  : CoreVar)
 275     (hetmet_esc   : CoreVar)
 276     (hetmet_flatten : CoreVar)
 277     (hetmet_unflatten : CoreVar)
 278     (hetmet_flattened_id : CoreVar)
 279     (uniqueSupply : UniqSupply)
 280     (lbinds:list (@CoreBind CoreVar))
 281     (hetmet_PGArrowTyCon : TyFun)
 282     (hetmet_pga_id : CoreVar)
 283     (hetmet_pga_comp : CoreVar)
 284     (hetmet_pga_first : CoreVar)
 285     (hetmet_pga_second : CoreVar)
 286     (hetmet_pga_cancell : CoreVar)
 287     (hetmet_pga_cancelr : CoreVar)
 288     (hetmet_pga_uncancell : CoreVar)
 289     (hetmet_pga_uncancelr : CoreVar)
 290     (hetmet_pga_assoc : CoreVar)
 291     (hetmet_pga_unassoc : CoreVar)
 292     (hetmet_pga_copy : CoreVar)
 293     (hetmet_pga_drop : CoreVar)
 294     (hetmet_pga_swap : CoreVar)
 295     (hetmet_pga_applyl : CoreVar)
 296     (hetmet_pga_applyr : CoreVar)
 297     (hetmet_pga_curryl : CoreVar)
 298     (hetmet_pga_curryr : CoreVar)
 299     .
 300
 301     Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil         ★ TyFunApp_nil.
 302     Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★  :=
 303       TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b.
 304     Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
 305       TApp (TApp (TApp (@TyFunApp TV
 306         hetmet_PGArrowTyCon
 307         nil _ TyFunApp_nil) a) b) c.
 308     Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
 309
 310     Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
 311       fun TV ite => TApp (TApp (TApp (@TyFunApp TV
 312         hetmet_PGArrowTyCon
 313         nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
 314
 315     Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
 316       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
 317       intros.
 318       inversion X; subst.
 319       inversion X1; subst.
 320       apply f; auto.
 321       Defined.
 322
 323     Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
 324       : ND Rule [] [ Γ > Δ > [] |- [f x y @@ l] ].
 325       apply nd_rule.
 326       refine (@RGlobal Γ Δ l
 327         {| glob_wv    := coreVarToWeakExprVarOrError cv
 328           ; glob_kinds := κ₁ :: κ₂ :: nil
 329           ; glob_tf    := mkGlob2'(Γ:=Γ) f
 330           |} (ICons _ _ x (ICons _ _ y INil))).
 331       Defined.
 332
 333     Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
 334       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
 335       intros.
 336       inversion X; subst.
 337       inversion X1; subst.
 338       inversion X3; subst.
 339       apply f; auto.
 340       Defined.
 341
 342     Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
 343       : ND Rule [] [ Γ > Δ > [] |- [f x y z @@ l] ].
 344       apply nd_rule.
 345       refine (@RGlobal Γ Δ l
 346         {| glob_wv    := coreVarToWeakExprVarOrError cv
 347           ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
 348           ; glob_tf    := mkGlob3'(Γ:=Γ) f
 349           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
 350       Defined.
 351
 352     Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
 353       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
 354       intros.
 355       inversion X; subst.
 356       inversion X1; subst.
 357       inversion X3; subst.
 358       inversion X5; subst.
 359       apply f; auto.
 360       Defined.
 361
 362     Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
 363       : ND Rule [] [ Γ > Δ > [] |- [f x y z q @@ l] ].
 364       apply nd_rule.
 365       refine (@RGlobal Γ Δ l
 366         {| glob_wv    := coreVarToWeakExprVarOrError cv
 367           ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
 368           ; glob_tf    := mkGlob4'(Γ:=Γ) f
 369           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
 370       Defined.
 371
 372     Definition gat {Γ}(x:Tree ??(HaskType Γ ★))  := @ga_mk_tree ga_unit ga_prod _ x.
 373
 374     Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
 375     { ga_id        := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_id        (fun ec a => ga_type' ec a a) ec (gat a)
 376     ; ga_cancelr   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancelr   (fun ec a => ga_type' ec _ a) ec (gat a)
 377     ; ga_cancell   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancell   (fun ec a => ga_type' ec _ a) ec (gat a)
 378     ; ga_uncancelr := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat a)
 379     ; ga_uncancell := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat a)
 380     ; 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)
 381     ; 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)
 382     ; ga_swap      := fun Γ Δ ec l a b   => mkGlob3 hetmet_pga_swap      (fun ec a b => ga_type' ec _ _) ec (gat a) (gat b)
 383     ; ga_drop      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_drop      (fun ec a => ga_type' ec _ _) ec (gat a)
 384     ; ga_copy      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_copy      (fun ec a => ga_type' ec _ _) ec (gat a)
 385     ; 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))
 386     ; 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))
 387     ; 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))
 388 (*  ; ga_lit       := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
 389 (*  ; ga_curry     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
 390 (*  ; ga_apply     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
 391 (*  ; ga_kappa     := fun Γ Δ ec l a     => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
 392     ; ga_lit       := fun Γ Δ ec l a     => Prelude_error "ga_lit"
 393     ; ga_curry     := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
 394     ; ga_apply     := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
 395     ; ga_kappa     := fun Γ Δ ec l a     => Prelude_error "ga_kappa"
 396     }.
 397
 398     Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
 399     Definition hetmet_esc'  := coreVarToWeakExprVarOrError hetmet_esc.
 400     Definition hetmet_flatten'  := coreVarToWeakExprVarOrError hetmet_flatten.
 401     Definition hetmet_unflatten'  := coreVarToWeakExprVarOrError hetmet_unflatten.
 402     Definition hetmet_flattened_id'  := coreVarToWeakExprVarOrError hetmet_flattened_id.
 403
 404     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 405       addErrorMessage ("input CoreSyn: " +++ toString ce)
 406       (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 407         coreExprToWeakExpr ce >>= fun we =>
 408           addErrorMessage ("WeakExpr: " +++ toString we)
 409             ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 410               ((weakTypeOfWeakExpr we) >>= fun t =>
 411                 (addErrorMessage ("WeakType: " +++ toString t)
 412                   ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 413
 414                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 415
 416                       (addErrorMessage ("HaskStrong...")
 417                         (let haskProof := flatten_proof hetmet_flatten' hetmet_unflatten'
 418                                             hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e)
 419                          in (* insert HaskProof-to-HaskProof manipulations here *)
 420                          OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 421                          >>= fun e' =>
 422                            (snd e') >>= fun e'' =>
 423                          strongExprToWeakExpr hetmet_brak' hetmet_esc'
 424                            mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 425                            (projT2 e'') INil
 426                          >>= fun q =>
 427                            OK (weakExprToCoreExpr q)
 428                     )))))))))).
 429
 430     Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
 431       match coreToCoreExpr' ce with
 432         | OK x    => x
 433         | Error s => Prelude_error s
 434       end.
 435
 436     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
 437       match binds with
 438         | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
 439
 440         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
 441                             (* FIXME: doesn't deal with the case where top level recursive binds change type *)
 442 (*
 443           match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
 444             | CoreELet (CoreRec lbe') => lbe'
 445             | x                       => Prelude_error
 446                                             ("coreToCoreExpr was given a letrec, " +++
 447                                              "but returned something that wasn't a letrec: " +++ toString x)
 448           end
 449 *)
 450       end.
 451
 452     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 453       map coreToCoreBind lbinds.
 454
 455   End coqPassCoreToCore.
 456
 457     Definition coqPassCoreToCore
 458     (hetmet_brak  : CoreVar)
 459     (hetmet_esc   : CoreVar)
 460     (hetmet_flatten   : CoreVar)
 461     (hetmet_unflatten   : CoreVar)
 462     (hetmet_flattened_id   : CoreVar)
 463     (uniqueSupply : UniqSupply)
 464     (lbinds:list (@CoreBind CoreVar))
 465     (hetmet_PGArrowTyCon : TyFun)
 466     (hetmet_pga_id : CoreVar)
 467     (hetmet_pga_comp : CoreVar)
 468     (hetmet_pga_first : CoreVar)
 469     (hetmet_pga_second : CoreVar)
 470     (hetmet_pga_cancell : CoreVar)
 471     (hetmet_pga_cancelr : CoreVar)
 472     (hetmet_pga_uncancell : CoreVar)
 473     (hetmet_pga_uncancelr : CoreVar)
 474     (hetmet_pga_assoc : CoreVar)
 475     (hetmet_pga_unassoc : CoreVar)
 476     (hetmet_pga_copy : CoreVar)
 477     (hetmet_pga_drop : CoreVar)
 478     (hetmet_pga_swap : CoreVar)
 479     (hetmet_pga_applyl : CoreVar)
 480     (hetmet_pga_applyr : CoreVar)
 481     (hetmet_pga_curryl : CoreVar)
 482     (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=
 483     coqPassCoreToCore'
 484        hetmet_brak
 485        hetmet_esc
 486        hetmet_flatten
 487        hetmet_unflatten
 488        hetmet_flattened_id
 489        uniqueSupply
 490        hetmet_PGArrowTyCon
 491        hetmet_pga_id
 492        hetmet_pga_comp
 493        hetmet_pga_first
 494        hetmet_pga_second
 495        hetmet_pga_cancell
 496        hetmet_pga_cancelr
 497        hetmet_pga_uncancell
 498        hetmet_pga_uncancelr
 499        hetmet_pga_assoc
 500        hetmet_pga_unassoc
 501        hetmet_pga_copy
 502        hetmet_pga_drop
 503        hetmet_pga_swap
 504        lbinds
 505        (*
 506        hetmet_pga_applyl
 507        hetmet_pga_applyr
 508        hetmet_pga_curryl
 509        *)
 510        .
 511
 512 End core2proof.