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