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