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       | OK (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       | OK (WTypeVar _)   => Prelude_error "top-level xi got a type variable"
 102       | OK (WCoerVar _)   => Prelude_error "top-level xi got a coercion variable"
 103       | Error s           => Prelude_error s
 104     end.
 105
 106   Definition header : string :=
 107     "\documentclass{article}"+++eol+++
 108     "\usepackage{amsmath}"+++eol+++
 109     "\usepackage{amssymb}"+++eol+++
 110     "\usepackage{proof}"+++eol+++
 111     "\usepackage{trfrac}       % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
 112     "\def\code#1#2{\Box_{#1} #2}"+++eol+++
 113     "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
 114     "\usepackage[tightpage,active]{preview}"+++eol+++
 115     "\begin{document}"+++eol+++
 116     "\setlength\PreviewBorder{5pt}"+++eol.
 117
 118   Definition footer : string :=
 119     eol+++"\end{document}"+++
 120     eol.
 121
 122   (* core-to-string (-dcoqpass) *)
 123   Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
 124     addErrorMessage ("input CoreSyn: " +++ toString ce)
 125     (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 126       coreExprToWeakExpr ce >>= fun we =>
 127         addErrorMessage ("WeakExpr: " +++ toString we)
 128           ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 129             ((weakTypeOfWeakExpr we) >>= fun t =>
 130               (addErrorMessage ("WeakType: " +++ toString t)
 131                 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 132                   addErrorMessage ("HaskType: " +++ toString τ)
 133                   ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
 134                     OK (eol+++eol+++eol+++
 135                         "\begin{preview}"+++eol+++
 136                         "$\displaystyle "+++
 137                         toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ _ e))+++
 138                         " $"+++eol+++
 139                         "\end{preview}"+++eol+++eol+++eol)
 140                   )))))))).
 141
 142   Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
 143     match coreToStringExpr' ce with
 144       | OK x => x
 145       | Error s => Prelude_error s
 146     end.
 147
 148   Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
 149     match binds with
 150       | CoreNonRec _ e => coreToStringExpr e
 151       | CoreRec    lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
 152     end.
 153
 154   Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
 155     header +++
 156     (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
 157     +++ footer.
 158
 159
 160   (* core-to-core (-fcoqpass) *)
 161   Section CoreToCore.
 162
 163     Definition mkWeakTypeVar (u:Unique)(k:Kind)                 : WeakTypeVar :=
 164       weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
 165     Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
 166       weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) t1 t2.
 167     Definition mkWeakExprVar (u:Unique)(t:WeakType)             : WeakExprVar :=
 168       weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
 169
 170     Context (hetmet_brak    : WeakExprVar).
 171     Context (hetmet_esc     : WeakExprVar).
 172     Context (hetmet_flatten : WeakExprVar).
 173     Context (hetmet_unflatten : WeakExprVar).
 174     Context (hetmet_flattened_id : WeakExprVar).
 175     Context (uniqueSupply   : UniqSupply).
 176
 177     Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
 178       match ut with
 179         uniqM f =>
 180          f uniqueSupply >>= fun x => OK (snd x)
 181       end.
 182
 183     Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
 184       intros.
 185       induction ln.
 186       exists O.
 187       intros.
 188       inversion H.
 189       destruct IHln as [n pf].
 190       exists (plus (S n) a).
 191       intros.
 192       destruct H.
 193       omega.
 194       fold (@In _ n' ln) in H.
 195       set (pf n' H) as q.
 196       omega.
 197       Defined.
 198
 199   Definition FreshNat : @FreshMonad nat.
 200     refine {| FMT       := fun T => nat -> prod nat T
 201             ; FMT_fresh := _
 202            |}.
 203     Focus 2.
 204     intros.
 205     refine ((S H),_).
 206     set (larger tl) as q.
 207     destruct q as [n' pf].
 208     exists n'.
 209     intros.
 210     set (pf _ H0) as qq.
 211     omega.
 212
 213     refine {| returnM := fun a (v:a) => _ |}.
 214       intro n. exact (n,v).
 215       intros.
 216       set (X H) as q.
 217       destruct q as [n' v].
 218       set (X0 v n') as q'.
 219       exact q'.
 220       Defined.
 221
 222     Definition unFresh {T} : @FreshM _ FreshNat T -> T.
 223       intros.
 224       destruct X.
 225       exact O.
 226       apply t.
 227       Defined.
 228
 229   End CoreToCore.
 230
 231   Definition coreVarToWeakExprVarOrError cv :=
 232     match addErrorMessage ("in coreVarToWeakExprVarOrError" +++ eol) (coreVarToWeakVar' cv) with
 233       | OK (WExprVar wv) => wv
 234       | Error s     => Prelude_error s
 235       | _           => Prelude_error "IMPOSSIBLE"
 236     end.
 237
 238   Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
 239     ND Rule
 240        [ Γ > Δ > Σ             |- [a ---> s  ]@lev ]
 241        [ Γ > Δ > [a @@ lev],,Σ |-       [ s ]@lev ].
 242     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 243     eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
 244     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 245     apply nd_prod.
 246     apply nd_id.
 247     apply nd_rule.
 248     apply RVar.
 249     Defined.
 250
 251   Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
 252     ND Rule [] [ Γ > Δ > [        ] |- [a ---> s  ]@lev ] ->
 253     ND Rule [] [ Γ > Δ > [a @@ lev] |-       [ s  ]@lev ].
 254     intro pf.
 255     eapply nd_comp.
 256     apply pf.
 257     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
 258     apply curry.
 259     Defined.
 260
 261   Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
 262     ND Rule [] [ Γ > Δ >                       [] |- [a1 ---> (a2 ---> s)  ]@lev ] ->
 263     ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |-                  [ s  ]@lev ].
 264     intro pf.
 265     eapply nd_comp.
 266     eapply pf.
 267     clear pf.
 268     eapply nd_comp.
 269     eapply curry.
 270     eapply nd_comp.
 271     eapply nd_rule.
 272     eapply RArrange.
 273     eapply ACanR.
 274     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 275     apply curry.
 276     Defined.
 277
 278   Section coqPassCoreToCore.
 279     Context
 280     (do_flatten : bool)
 281     (do_skolemize : bool)
 282     (hetmet_brak  : CoreVar)
 283     (hetmet_esc   : CoreVar)
 284     (hetmet_flatten : CoreVar)
 285     (hetmet_unflatten : CoreVar)
 286     (hetmet_flattened_id : CoreVar)
 287     (uniqueSupply : UniqSupply)
 288     (lbinds:list (@CoreBind CoreVar))
 289     (hetmet_PGArrowTyCon : TyFun)
 290     (hetmet_PGArrow_unit_TyCon : TyFun)
 291     (hetmet_PGArrow_tensor_TyCon : TyFun)
 292     (hetmet_PGArrow_exponent_TyCon : TyFun)
 293     (hetmet_pga_id : CoreVar)
 294     (hetmet_pga_comp : CoreVar)
 295     (hetmet_pga_first : CoreVar)
 296     (hetmet_pga_second : CoreVar)
 297     (hetmet_pga_cancell : CoreVar)
 298     (hetmet_pga_cancelr : CoreVar)
 299     (hetmet_pga_uncancell : CoreVar)
 300     (hetmet_pga_uncancelr : CoreVar)
 301     (hetmet_pga_assoc : CoreVar)
 302     (hetmet_pga_unassoc : CoreVar)
 303     (hetmet_pga_copy : CoreVar)
 304     (hetmet_pga_drop : CoreVar)
 305     (hetmet_pga_swap : CoreVar)
 306     (hetmet_pga_applyl : CoreVar)
 307     (hetmet_pga_applyr : CoreVar)
 308     (hetmet_pga_curryl : CoreVar)
 309     (hetmet_pga_curryr : CoreVar)
 310     .
 311
 312
 313     Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
 314       @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
 315
 316     Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★  :=
 317       (@TyFunApp TV
 318         hetmet_PGArrow_tensor_TyCon
 319         (ECKind::★ ::★ ::nil) ★
 320         (TyFunApp_cons _ _ ec
 321           (TyFunApp_cons _ _ a
 322             (TyFunApp_cons _ _ b
 323           TyFunApp_nil)))).
 324
 325     Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
 326       TApp (TApp (TApp (@TyFunApp TV
 327         hetmet_PGArrowTyCon
 328         nil _ TyFunApp_nil) a) b) c.
 329
 330     Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
 331
 332     Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
 333       fun TV ite => TApp (TApp (TApp (@TyFunApp TV
 334         hetmet_PGArrowTyCon
 335         nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
 336
 337     Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
 338       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
 339       intros.
 340       inversion X; subst.
 341       inversion X1; subst.
 342       apply f; auto.
 343       Defined.
 344
 345     Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
 346       : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ].
 347       apply nd_rule.
 348       refine (@RGlobal Γ Δ l
 349         {| glob_wv    := coreVarToWeakExprVarOrError cv
 350           ; glob_kinds := κ₁ :: κ₂ :: nil
 351           ; glob_tf    := mkGlob2'(Γ:=Γ) f
 352           |} (ICons _ _ x (ICons _ _ y INil))).
 353       Defined.
 354
 355     Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
 356       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
 357       intros.
 358       inversion X; subst.
 359       inversion X1; subst.
 360       inversion X3; subst.
 361       apply f; auto.
 362       Defined.
 363
 364     Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
 365       : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ].
 366       apply nd_rule.
 367       refine (@RGlobal Γ Δ l
 368         {| glob_wv    := coreVarToWeakExprVarOrError cv
 369           ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
 370           ; glob_tf    := mkGlob3'(Γ:=Γ) f
 371           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
 372       Defined.
 373
 374     Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
 375       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
 376       intros.
 377       inversion X; subst.
 378       inversion X1; subst.
 379       inversion X3; subst.
 380       inversion X5; subst.
 381       apply f; auto.
 382       Defined.
 383
 384     Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
 385       : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l].
 386       apply nd_rule.
 387       refine (@RGlobal Γ Δ l
 388         {| glob_wv    := coreVarToWeakExprVarOrError cv
 389           ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
 390           ; glob_tf    := mkGlob4'(Γ:=Γ) f
 391           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
 392       Defined.
 393
 394     Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★))  := @ga_mk_tree ga_unit ga_prod _ ec x.
 395
 396     Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
 397     { ga_id        := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_id        (fun ec a => ga_type' ec a a) ec (gat ec a)
 398     ; ga_cancelr   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancelr   (fun ec a => ga_type' ec _ a) ec (gat ec a)
 399     ; ga_cancell   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancell   (fun ec a => ga_type' ec _ a) ec (gat ec a)
 400     ; ga_uncancelr := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
 401     ; ga_uncancell := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
 402     ; 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)
 403     ; 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)
 404     ; 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)
 405     ; ga_drop      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_drop      (fun ec a => ga_type' ec _ _) ec (gat ec a)
 406     ; ga_copy      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_copy      (fun ec a => ga_type' ec _ _) ec (gat ec a)
 407     ; 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))
 408     ; 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))
 409     ; 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))
 410 (*  ; ga_lit       := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
 411 (*  ; ga_curry     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
 412 (*  ; ga_apply     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
 413 (*  ; ga_kappa     := fun Γ Δ ec l a     => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
 414     ; ga_lit       := fun Γ Δ ec l a     => Prelude_error "ga_lit"
 415     ; ga_curry     := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
 416     ; ga_apply     := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
 417     ; ga_kappa     := fun Γ Δ ec l a     => Prelude_error "ga_kappa"
 418     }.
 419
 420     Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
 421     Definition hetmet_esc'  := coreVarToWeakExprVarOrError hetmet_esc.
 422     Definition hetmet_flatten'  := coreVarToWeakExprVarOrError hetmet_flatten.
 423     Definition hetmet_unflatten'  := coreVarToWeakExprVarOrError hetmet_unflatten.
 424     Definition hetmet_flattened_id'  := coreVarToWeakExprVarOrError hetmet_flattened_id.
 425
 426     Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 427       addErrorMessage ("input CoreSyn: " +++ toString cex)
 428       (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr cex)) (
 429         coreExprToWeakExpr cex >>= fun we =>
 430           addErrorMessage ("WeakExpr: " +++ toString we)
 431             ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 432               ((weakTypeOfWeakExpr we) >>= fun t =>
 433                 (addErrorMessage ("WeakType: " +++ toString t)
 434                   ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 435
 436                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 437
 438                       (addErrorMessage ("HaskStrong...")
 439                         (if do_skolemize
 440                         then
 441                              (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
 442                                                  hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e)
 443                               in (* insert HaskProof-to-HaskProof manipulations here *)
 444                               OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _
 445                                 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 446                               >>= fun e' => (snd e') >>= fun e'' =>
 447                               strongExprToWeakExpr hetmet_brak' hetmet_esc'
 448                                 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 449                                 (projT2 e'') INil
 450                               >>= fun q => OK (weakExprToCoreExpr q))
 451                         else (if do_flatten
 452                         then
 453                           (let haskProof := flatten_proof (*hetmet_flatten' hetmet_unflatten'
 454                                                  hetmet_flattened_id' my_ga*) (@expr2proof _ _ _ _ _ _ _ e)
 455                               in (* insert HaskProof-to-HaskProof manipulations here *)
 456                               OK ((@proof2expr nat _ FreshNat _ _ τ nil _
 457                                 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 458                               >>= fun e' => (snd e') >>= fun e'' =>
 459                               strongExprToWeakExpr hetmet_brak' hetmet_esc'
 460                                 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 461                                 (projT2 e'') INil
 462                               >>= fun q => OK (weakExprToCoreExpr q))
 463                         else
 464                           (let haskProof := @expr2proof _ _ _ _ _ _ _ e
 465                               in (* insert HaskProof-to-HaskProof manipulations here *)
 466                               OK ((@proof2expr nat _ FreshNat _ _ τ nil _
 467                                 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 468                               >>= fun e' => (snd e') >>= fun e'' =>
 469                               strongExprToWeakExpr hetmet_brak' hetmet_esc'
 470                                 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 471                                 (projT2 e'') INil
 472                               >>= fun q => OK (weakExprToCoreExpr q))))
 473                   ))))))))).
 474
 475     Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
 476       match coreToCoreExpr' ce with
 477         | OK x    => x
 478         | Error s => Prelude_error s
 479       end.
 480
 481     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
 482       match binds with
 483         | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
 484
 485         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
 486                             (* FIXME: doesn't deal with the case where top level recursive binds change type *)
 487 (*
 488           match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
 489             | CoreELet (CoreRec lbe') => lbe'
 490             | x                       => Prelude_error
 491                                             ("coreToCoreExpr was given a letrec, " +++
 492                                              "but returned something that wasn't a letrec: " +++ toString x)
 493           end
 494 *)
 495       end.
 496
 497     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 498       map coreToCoreBind lbinds.
 499
 500   End coqPassCoreToCore.
 501
 502     Definition coqPassCoreToCore
 503     (do_flatten  : bool)
 504     (do_skolemize  : bool)
 505     (hetmet_brak  : CoreVar)
 506     (hetmet_esc   : CoreVar)
 507     (hetmet_flatten   : CoreVar)
 508     (hetmet_unflatten   : CoreVar)
 509     (hetmet_flattened_id   : CoreVar)
 510     (uniqueSupply : UniqSupply)
 511     (lbinds:list (@CoreBind CoreVar))
 512     (hetmet_PGArrowTyCon : TyFun)
 513     (hetmet_PGArrow_unit_TyCon : TyFun)
 514     (hetmet_PGArrow_tensor_TyCon : TyFun)
 515     (hetmet_PGArrow_exponent_TyCon : TyFun)
 516     (hetmet_pga_id : CoreVar)
 517     (hetmet_pga_comp : CoreVar)
 518     (hetmet_pga_first : CoreVar)
 519     (hetmet_pga_second : CoreVar)
 520     (hetmet_pga_cancell : CoreVar)
 521     (hetmet_pga_cancelr : CoreVar)
 522     (hetmet_pga_uncancell : CoreVar)
 523     (hetmet_pga_uncancelr : CoreVar)
 524     (hetmet_pga_assoc : CoreVar)
 525     (hetmet_pga_unassoc : CoreVar)
 526     (hetmet_pga_copy : CoreVar)
 527     (hetmet_pga_drop : CoreVar)
 528     (hetmet_pga_swap : CoreVar)
 529     (hetmet_pga_applyl : CoreVar)
 530     (hetmet_pga_applyr : CoreVar)
 531     (hetmet_pga_curryl : CoreVar)
 532     (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=
 533     coqPassCoreToCore'
 534        do_flatten
 535        do_skolemize
 536        hetmet_brak
 537        hetmet_esc
 538        hetmet_flatten
 539        hetmet_unflatten
 540        hetmet_flattened_id
 541        uniqueSupply
 542        hetmet_PGArrowTyCon
 543        hetmet_PGArrow_unit_TyCon
 544        hetmet_PGArrow_tensor_TyCon
 545 (*       hetmet_PGArrow_exponent_TyCon*)
 546        hetmet_pga_id
 547        hetmet_pga_comp
 548        hetmet_pga_first
 549        hetmet_pga_second
 550        hetmet_pga_cancell
 551        hetmet_pga_cancelr
 552        hetmet_pga_uncancell
 553        hetmet_pga_uncancelr
 554        hetmet_pga_assoc
 555        hetmet_pga_unassoc
 556        hetmet_pga_copy
 557        hetmet_pga_drop
 558        hetmet_pga_swap
 559        lbinds
 560        (*
 561        hetmet_pga_applyl
 562        hetmet_pga_applyr
 563        hetmet_pga_curryl
 564        *)
 565
 566        .
 567
 568 End core2proof.