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