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