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