src/ExtractionMain.v

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