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)) 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_PGArrow_unit_TyCon : TyFun)
 284     (hetmet_PGArrow_tensor_TyCon : TyFun)
 285     (hetmet_PGArrow_exponent_TyCon : TyFun)
 286     (hetmet_pga_id : CoreVar)
 287     (hetmet_pga_comp : CoreVar)
 288     (hetmet_pga_first : CoreVar)
 289     (hetmet_pga_second : CoreVar)
 290     (hetmet_pga_cancell : CoreVar)
 291     (hetmet_pga_cancelr : CoreVar)
 292     (hetmet_pga_uncancell : CoreVar)
 293     (hetmet_pga_uncancelr : CoreVar)
 294     (hetmet_pga_assoc : CoreVar)
 295     (hetmet_pga_unassoc : CoreVar)
 296     (hetmet_pga_copy : CoreVar)
 297     (hetmet_pga_drop : CoreVar)
 298     (hetmet_pga_swap : CoreVar)
 299     (hetmet_pga_applyl : CoreVar)
 300     (hetmet_pga_applyr : CoreVar)
 301     (hetmet_pga_curryl : CoreVar)
 302     (hetmet_pga_curryr : CoreVar)
 303     .
 304
 305
 306     Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
 307       @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
 308     Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★  :=
 309       TApp (TApp (@TyFunApp TV hetmet_PGArrow_tensor_TyCon (ECKind::nil) _ (TyFunApp_cons _ _ ec TyFunApp_nil)) a) b.
 310     Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
 311       TApp (TApp (TApp (@TyFunApp TV
 312         hetmet_PGArrowTyCon
 313         nil _ TyFunApp_nil) a) b) c.
 314     Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
 315
 316     Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
 317       fun TV ite => TApp (TApp (TApp (@TyFunApp TV
 318         hetmet_PGArrowTyCon
 319         nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
 320
 321     Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
 322       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
 323       intros.
 324       inversion X; subst.
 325       inversion X1; subst.
 326       apply f; auto.
 327       Defined.
 328
 329     Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
 330       : ND Rule [] [ Γ > Δ > [] |- [f x y @@ l] ].
 331       apply nd_rule.
 332       refine (@RGlobal Γ Δ l
 333         {| glob_wv    := coreVarToWeakExprVarOrError cv
 334           ; glob_kinds := κ₁ :: κ₂ :: nil
 335           ; glob_tf    := mkGlob2'(Γ:=Γ) f
 336           |} (ICons _ _ x (ICons _ _ y INil))).
 337       Defined.
 338
 339     Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
 340       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
 341       intros.
 342       inversion X; subst.
 343       inversion X1; subst.
 344       inversion X3; subst.
 345       apply f; auto.
 346       Defined.
 347
 348     Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
 349       : ND Rule [] [ Γ > Δ > [] |- [f x y z @@ l] ].
 350       apply nd_rule.
 351       refine (@RGlobal Γ Δ l
 352         {| glob_wv    := coreVarToWeakExprVarOrError cv
 353           ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
 354           ; glob_tf    := mkGlob3'(Γ:=Γ) f
 355           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
 356       Defined.
 357
 358     Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
 359       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
 360       intros.
 361       inversion X; subst.
 362       inversion X1; subst.
 363       inversion X3; subst.
 364       inversion X5; subst.
 365       apply f; auto.
 366       Defined.
 367
 368     Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
 369       : ND Rule [] [ Γ > Δ > [] |- [f x y z q @@ l] ].
 370       apply nd_rule.
 371       refine (@RGlobal Γ Δ l
 372         {| glob_wv    := coreVarToWeakExprVarOrError cv
 373           ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
 374           ; glob_tf    := mkGlob4'(Γ:=Γ) f
 375           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
 376       Defined.
 377
 378     Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★))  := @ga_mk_tree ga_unit ga_prod _ ec x.
 379
 380     Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
 381     { ga_id        := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_id        (fun ec a => ga_type' ec a a) ec (gat ec a)
 382     ; ga_cancelr   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancelr   (fun ec a => ga_type' ec _ a) ec (gat ec a)
 383     ; ga_cancell   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancell   (fun ec a => ga_type' ec _ a) ec (gat ec a)
 384     ; ga_uncancelr := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
 385     ; ga_uncancell := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
 386     ; 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)
 387     ; 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)
 388     ; 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)
 389     ; ga_drop      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_drop      (fun ec a => ga_type' ec _ _) ec (gat ec a)
 390     ; ga_copy      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_copy      (fun ec a => ga_type' ec _ _) ec (gat ec a)
 391     ; 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))
 392     ; 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))
 393     ; 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))
 394 (*  ; ga_lit       := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
 395 (*  ; ga_curry     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
 396 (*  ; ga_apply     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
 397 (*  ; ga_kappa     := fun Γ Δ ec l a     => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
 398     ; ga_lit       := fun Γ Δ ec l a     => Prelude_error "ga_lit"
 399     ; ga_curry     := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
 400     ; ga_apply     := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
 401     ; ga_kappa     := fun Γ Δ ec l a     => Prelude_error "ga_kappa"
 402     }.
 403
 404     Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
 405     Definition hetmet_esc'  := coreVarToWeakExprVarOrError hetmet_esc.
 406     Definition hetmet_flatten'  := coreVarToWeakExprVarOrError hetmet_flatten.
 407     Definition hetmet_unflatten'  := coreVarToWeakExprVarOrError hetmet_unflatten.
 408     Definition hetmet_flattened_id'  := coreVarToWeakExprVarOrError hetmet_flattened_id.
 409
 410     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 411       addErrorMessage ("input CoreSyn: " +++ toString ce)
 412       (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 413         coreExprToWeakExpr ce >>= fun we =>
 414           addErrorMessage ("WeakExpr: " +++ toString we)
 415             ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 416               ((weakTypeOfWeakExpr we) >>= fun t =>
 417                 (addErrorMessage ("WeakType: " +++ toString t)
 418                   ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 419
 420                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 421
 422                       (addErrorMessage ("HaskStrong...")
 423                         (let haskProof := flatten_proof hetmet_flatten' hetmet_unflatten'
 424                                             hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e)
 425                          in (* insert HaskProof-to-HaskProof manipulations here *)
 426                          OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 427                          >>= fun e' =>
 428                            (snd e') >>= fun e'' =>
 429                          strongExprToWeakExpr hetmet_brak' hetmet_esc'
 430                            mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 431                            (projT2 e'') INil
 432                          >>= fun q =>
 433                            OK (weakExprToCoreExpr q)
 434                     )))))))))).
 435
 436     Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
 437       match coreToCoreExpr' ce with
 438         | OK x    => x
 439         | Error s => Prelude_error s
 440       end.
 441
 442     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
 443       match binds with
 444         | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
 445
 446         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
 447                             (* FIXME: doesn't deal with the case where top level recursive binds change type *)
 448 (*
 449           match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
 450             | CoreELet (CoreRec lbe') => lbe'
 451             | x                       => Prelude_error
 452                                             ("coreToCoreExpr was given a letrec, " +++
 453                                              "but returned something that wasn't a letrec: " +++ toString x)
 454           end
 455 *)
 456       end.
 457
 458     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 459       map coreToCoreBind lbinds.
 460
 461   End coqPassCoreToCore.
 462
 463     Definition coqPassCoreToCore
 464     (hetmet_brak  : CoreVar)
 465     (hetmet_esc   : CoreVar)
 466     (hetmet_flatten   : CoreVar)
 467     (hetmet_unflatten   : CoreVar)
 468     (hetmet_flattened_id   : CoreVar)
 469     (uniqueSupply : UniqSupply)
 470     (lbinds:list (@CoreBind CoreVar))
 471     (hetmet_PGArrowTyCon : TyFun)
 472     (hetmet_PGArrow_unit_TyCon : TyFun)
 473     (hetmet_PGArrow_tensor_TyCon : TyFun)
 474     (hetmet_PGArrow_exponent_TyCon : TyFun)
 475     (hetmet_pga_id : CoreVar)
 476     (hetmet_pga_comp : CoreVar)
 477     (hetmet_pga_first : CoreVar)
 478     (hetmet_pga_second : CoreVar)
 479     (hetmet_pga_cancell : CoreVar)
 480     (hetmet_pga_cancelr : CoreVar)
 481     (hetmet_pga_uncancell : CoreVar)
 482     (hetmet_pga_uncancelr : CoreVar)
 483     (hetmet_pga_assoc : CoreVar)
 484     (hetmet_pga_unassoc : CoreVar)
 485     (hetmet_pga_copy : CoreVar)
 486     (hetmet_pga_drop : CoreVar)
 487     (hetmet_pga_swap : CoreVar)
 488     (hetmet_pga_applyl : CoreVar)
 489     (hetmet_pga_applyr : CoreVar)
 490     (hetmet_pga_curryl : CoreVar)
 491     (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=
 492     coqPassCoreToCore'
 493        hetmet_brak
 494        hetmet_esc
 495        hetmet_flatten
 496        hetmet_unflatten
 497        hetmet_flattened_id
 498        uniqueSupply
 499        hetmet_PGArrowTyCon
 500        hetmet_PGArrow_unit_TyCon
 501        hetmet_PGArrow_tensor_TyCon
 502 (*       hetmet_PGArrow_exponent_TyCon*)
 503        hetmet_pga_id
 504        hetmet_pga_comp
 505        hetmet_pga_first
 506        hetmet_pga_second
 507        hetmet_pga_cancell
 508        hetmet_pga_cancelr
 509        hetmet_pga_uncancell
 510        hetmet_pga_uncancelr
 511        hetmet_pga_assoc
 512        hetmet_pga_unassoc
 513        hetmet_pga_copy
 514        hetmet_pga_drop
 515        hetmet_pga_swap
 516        lbinds
 517        (*
 518        hetmet_pga_applyl
 519        hetmet_pga_applyr
 520        hetmet_pga_curryl
 521        *)
 522        .
 523
 524 End core2proof.