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