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