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 (hetmet_kappa     : WeakExprVar).
 185     Context (hetmet_kappa_app : WeakExprVar).
 186     Context (uniqueSupply     : UniqSupply).
 187
 188     Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
 189       match ut with
 190         uniqM f =>
 191          f uniqueSupply >>= fun x => OK (snd x)
 192       end.
 193
 194     Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
 195       intros.
 196       induction ln.
 197       exists O.
 198       intros.
 199       inversion H.
 200       destruct IHln as [n pf].
 201       exists (plus (S n) a).
 202       intros.
 203       destruct H.
 204       omega.
 205       fold (@In _ n' ln) in H.
 206       set (pf n' H) as q.
 207       omega.
 208       Defined.
 209
 210   Definition FreshNat : @FreshMonad nat.
 211     refine {| FMT       := fun T => nat -> prod nat T
 212             ; FMT_fresh := _
 213            |}.
 214     Focus 2.
 215     intros.
 216     refine ((S H),_).
 217     set (larger tl) as q.
 218     destruct q as [n' pf].
 219     exists n'.
 220     intros.
 221     set (pf _ H0) as qq.
 222     omega.
 223
 224     refine {| returnM := fun a (v:a) => _ |}.
 225       intro n. exact (n,v).
 226       intros.
 227       set (X H) as q.
 228       destruct q as [n' v].
 229       set (X0 v n') as q'.
 230       exact q'.
 231       Defined.
 232
 233     Definition unFresh {T} : @FreshM _ FreshNat T -> T.
 234       intros.
 235       destruct X.
 236       exact O.
 237       apply t.
 238       Defined.
 239
 240   End CoreToCore.
 241
 242   Definition coreVarToWeakExprVarOrError cv :=
 243     match addErrorMessage ("in coreVarToWeakExprVarOrError" +++ eol) (coreVarToWeakVar' cv) with
 244       | OK (WExprVar wv) => wv
 245       | Error s     => Prelude_error s
 246       | _           => Prelude_error "IMPOSSIBLE"
 247     end.
 248
 249   Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
 250     ND Rule
 251        [ Γ > Δ > Σ             |- [a ---> s  ]@lev ]
 252        [ Γ > Δ > [a @@ lev],,Σ |-       [ s ]@lev ].
 253     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 254     eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
 255     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 256     apply nd_prod.
 257     apply nd_id.
 258     apply nd_rule.
 259     apply RVar.
 260     Defined.
 261
 262   Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
 263     ND Rule [] [ Γ > Δ > [        ] |- [a ---> s  ]@lev ] ->
 264     ND Rule [] [ Γ > Δ > [a @@ lev] |-       [ s  ]@lev ].
 265     intro pf.
 266     eapply nd_comp.
 267     apply pf.
 268     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
 269     apply curry.
 270     Defined.
 271
 272   Definition fToC1' {Γ}{Δ}{a}{s}{lev} :
 273     ND Rule [] [ Γ > Δ > [        ] |- [a ---> s  ]@lev ] ->
 274     ND Rule [] [ Γ > Δ > [a @@ lev] |-       [ s  ]@lev ].
 275     intro pf.
 276     eapply nd_comp.
 277     apply pf.
 278     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
 279     apply curry.
 280     Defined.
 281
 282   Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
 283     ND Rule [] [ Γ > Δ >                       [] |- [a1 ---> (a2 ---> s)  ]@lev ] ->
 284     ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |-                  [ s  ]@lev ].
 285     intro pf.
 286     eapply nd_comp.
 287     eapply pf.
 288     clear pf.
 289     eapply nd_comp.
 290     eapply curry.
 291     eapply nd_comp.
 292     eapply nd_rule.
 293     eapply RArrange.
 294     eapply ACanR.
 295     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 296     apply curry.
 297     Defined.
 298
 299   Definition fToCx {Γ}{Δ}{a1}{a2}{a3}{l} Σ :
 300     ND Rule [] [ Γ > Δ >       [] |- [(a1 ---> a2) ---> a3  ]@l ] ->
 301     ND Rule [Γ > Δ > Σ,,[a1 @@ l] |- [a2]@l ]
 302             [Γ > Δ > Σ            |- [a3]@l ].
 303     intro pf.
 304     eapply nd_comp; [ eapply nd_rule; eapply RLam | idtac ].
 305     set (fToC1 pf) as pf'.
 306     apply boost.
 307     apply pf'.
 308     Defined.
 309
 310   Section coqPassCoreToCore.
 311     Context
 312     (do_flatten : bool)
 313     (do_skolemize : bool)
 314     (hetmet_brak  : CoreVar)
 315     (hetmet_esc   : CoreVar)
 316     (hetmet_kappa     : WeakExprVar)
 317     (hetmet_kappa_app : WeakExprVar)
 318     (uniqueSupply : UniqSupply)
 319     (lbinds:list (@CoreBind CoreVar))
 320     (hetmet_PGArrowTyCon : TyFun)
 321     (hetmet_PGArrow_unit_TyCon : TyFun)
 322     (hetmet_PGArrow_tensor_TyCon : TyFun)
 323     (hetmet_PGArrow_exponent_TyCon : TyFun)
 324     (hetmet_pga_id : CoreVar)
 325     (hetmet_pga_comp : CoreVar)
 326     (hetmet_pga_first : CoreVar)
 327     (hetmet_pga_second : CoreVar)
 328     (hetmet_pga_cancell : CoreVar)
 329     (hetmet_pga_cancelr : CoreVar)
 330     (hetmet_pga_uncancell : CoreVar)
 331     (hetmet_pga_uncancelr : CoreVar)
 332     (hetmet_pga_assoc : CoreVar)
 333     (hetmet_pga_unassoc : CoreVar)
 334     (hetmet_pga_copy : CoreVar)
 335     (hetmet_pga_drop : CoreVar)
 336     (hetmet_pga_swap : CoreVar)
 337     (hetmet_pga_applyl : CoreVar)
 338     (hetmet_pga_applyr : CoreVar)
 339     (hetmet_pga_curryl : CoreVar)
 340     (hetmet_pga_curryr : CoreVar)
 341     (hetmet_pga_loopl : CoreVar)
 342     (hetmet_pga_loopr : CoreVar)
 343     (hetmet_pga_kappa : CoreVar)
 344     .
 345
 346
 347     Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
 348       @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
 349
 350     Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★  :=
 351       (@TyFunApp TV
 352         hetmet_PGArrow_tensor_TyCon
 353         (ECKind::★ ::★ ::nil) ★
 354         (TyFunApp_cons _ _ ec
 355           (TyFunApp_cons _ _ a
 356             (TyFunApp_cons _ _ b
 357           TyFunApp_nil)))).
 358
 359     Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
 360       TApp (TApp (TApp (@TyFunApp TV
 361         hetmet_PGArrowTyCon
 362         nil _ TyFunApp_nil) a) b) c.
 363
 364     Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
 365
 366     Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
 367       fun TV ite => TApp (TApp (TApp (@TyFunApp TV
 368         hetmet_PGArrowTyCon
 369         nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
 370
 371     Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
 372       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
 373       intros.
 374       inversion X; subst.
 375       inversion X1; subst.
 376       apply f; auto.
 377       Defined.
 378
 379     Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
 380       : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ].
 381       apply nd_rule.
 382       refine (@RGlobal Γ Δ l
 383         {| glob_wv    := coreVarToWeakExprVarOrError cv
 384           ; glob_kinds := κ₁ :: κ₂ :: nil
 385           ; glob_tf    := mkGlob2'(Γ:=Γ) f
 386           |} (ICons _ _ x (ICons _ _ y INil))).
 387       Defined.
 388
 389     Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
 390       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
 391       intros.
 392       inversion X; subst.
 393       inversion X1; subst.
 394       inversion X3; subst.
 395       apply f; auto.
 396       Defined.
 397
 398     Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
 399       : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ].
 400       apply nd_rule.
 401       refine (@RGlobal Γ Δ l
 402         {| glob_wv    := coreVarToWeakExprVarOrError cv
 403           ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
 404           ; glob_tf    := mkGlob3'(Γ:=Γ) f
 405           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
 406       Defined.
 407
 408     Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
 409       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
 410       intros.
 411       inversion X; subst.
 412       inversion X1; subst.
 413       inversion X3; subst.
 414       inversion X5; subst.
 415       apply f; auto.
 416       Defined.
 417
 418     Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
 419       : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l].
 420       apply nd_rule.
 421       refine (@RGlobal Γ Δ l
 422         {| glob_wv    := coreVarToWeakExprVarOrError cv
 423           ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
 424           ; glob_tf    := mkGlob4'(Γ:=Γ) f
 425           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
 426       Defined.
 427
 428     Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★))  := @ga_mk_tree ga_unit ga_prod _ ec x.
 429
 430     Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
 431     { ga_id        := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_id        (fun ec a => ga_type' ec a a) ec (gat ec a)
 432     ; ga_cancelr   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancelr   (fun ec a => ga_type' ec _ a) ec (gat ec a)
 433     ; ga_cancell   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancell   (fun ec a => ga_type' ec _ a) ec (gat ec a)
 434     ; ga_uncancelr := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
 435     ; ga_uncancell := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
 436     ; 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)
 437     ; 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)
 438     ; 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)
 439     ; ga_drop      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_drop      (fun ec a => ga_type' ec _ _) ec (gat ec a)
 440     ; ga_copy      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_copy      (fun ec a => ga_type' ec _ _) ec (gat ec a)
 441     ; 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))
 442     ; 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))
 443     ; 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))
 444     ; 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))
 445     ; 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))
 446
 447     ; ga_curry     := fun Γ Δ ec l a     =>  Prelude_error "ga_curry"
 448
 449     ; ga_apply     := fun Γ Δ ec l a     =>  Prelude_error "ga_apply"
 450     ; ga_lit       := fun Γ Δ ec l a     => Prelude_error "ga_lit"
 451 (*  ; ga_lit       := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
 452     ; ga_kappa     := fun Γ Δ ec l a b c Σ =>
 453       fToCx Σ (mkGlob4 hetmet_pga_kappa (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec c))
 454     }.
 455
 456     Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
 457     Definition hetmet_esc'  := coreVarToWeakExprVarOrError hetmet_esc.
 458     Definition hetmet_kappa'  := coreVarToWeakExprVarOrError hetmet_kappa.
 459     Definition hetmet_kappa_app'  := coreVarToWeakExprVarOrError hetmet_kappa_app.
 460
 461     Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 462       addErrorMessage ("input CoreSyn: " +++ toString cex)
 463       (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr cex)) (
 464         coreExprToWeakExpr cex >>= fun we =>
 465           addErrorMessage ("WeakExpr: " +++ toString we)
 466             ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 467               ((weakTypeOfWeakExpr we) >>= fun t =>
 468                 (addErrorMessage ("WeakType: " +++ toString t)
 469                   ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 470
 471                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 472
 473                       (addErrorMessage ("HaskStrong...")
 474                         (if do_skolemize
 475                         then
 476                              (let haskProof := skolemize_and_flatten_proof my_ga (@expr2proof _ _ _ _ _ _ _ e)
 477                               in (* insert HaskProof-to-HaskProof manipulations here *)
 478                               OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _
 479                                 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 480                               >>= fun e' => (snd e') >>= fun e'' =>
 481                               strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
 482                                 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 483                                 (projT2 e'') INil
 484                               >>= fun q => OK (weakExprToCoreExpr q))
 485                         else (if do_flatten
 486                         then
 487                           (let haskProof := flatten_proof (@expr2proof _ _ _ _ _ _ _ e)
 488                               in (* insert HaskProof-to-HaskProof manipulations here *)
 489                               OK ((@proof2expr nat _ FreshNat _ _ τ nil _
 490                                 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 491                               >>= fun e' => (snd e') >>= fun e'' =>
 492                               strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
 493                                 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 494                                 (projT2 e'') INil
 495                               >>= fun q => OK (weakExprToCoreExpr q))
 496                         else
 497                           (let haskProof := @expr2proof _ _ _ _ _ _ _ e
 498                               in (* insert HaskProof-to-HaskProof manipulations here *)
 499                               OK ((@proof2expr nat _ FreshNat _ _ τ nil _
 500                                 (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 501                               >>= fun e' => (snd e') >>= fun e'' =>
 502                               strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
 503                                 mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 504                                 (projT2 e'') INil
 505                               >>= fun q => OK (weakExprToCoreExpr q))))
 506                   ))))))))).
 507
 508     Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
 509       match coreToCoreExpr' ce with
 510         | OK x    => x
 511         | Error s => Prelude_error s
 512       end.
 513
 514     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
 515       match binds with
 516         | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
 517
 518         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
 519                             (* FIXME: doesn't deal with the case where top level recursive binds change type *)
 520 (*
 521           match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
 522             | CoreELet (CoreRec lbe') => lbe'
 523             | x                       => Prelude_error
 524                                             ("coreToCoreExpr was given a letrec, " +++
 525                                              "but returned something that wasn't a letrec: " +++ toString x)
 526           end
 527 *)
 528       end.
 529
 530     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 531       map coreToCoreBind lbinds.
 532
 533   End coqPassCoreToCore.
 534
 535   Notation "a >>= b" := (@CoreMbind _ _ a b).
 536
 537     Definition coqPassCoreToCore
 538     (do_flatten   : bool)
 539     (do_skolemize : bool)
 540     (dsLookupVar  : string -> string -> CoreM CoreVar)
 541     (dsLookupTyc  : string -> string -> CoreM TyFun)
 542     (uniqueSupply : UniqSupply)
 543     (lbinds       : list (@CoreBind CoreVar))
 544     : CoreM (list (@CoreBind CoreVar)) :=
 545       dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_brak" >>= fun hetmet_brak =>
 546       dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_esc" >>= fun hetmet_esc =>
 547       dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa" >>= fun hetmet_kappa =>
 548       dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa_app" >>= fun hetmet_kappa_app =>
 549       dsLookupTyc "GHC.HetMet.Private" "PGArrow" >>= fun hetmet_PGArrow =>
 550       dsLookupTyc "GHC.HetMet.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit =>
 551       dsLookupTyc "GHC.HetMet.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor =>
 552       dsLookupTyc "GHC.HetMet.GArrow" "GArrowExponent" >>= fun hetmet_PGArrow_exponent =>
 553       dsLookupVar "GHC.HetMet.Private" "pga_id" >>= fun hetmet_pga_id =>
 554       dsLookupVar "GHC.HetMet.Private" "pga_comp" >>= fun hetmet_pga_comp =>
 555       dsLookupVar "GHC.HetMet.Private" "pga_first" >>= fun hetmet_pga_first =>
 556       dsLookupVar "GHC.HetMet.Private" "pga_second" >>= fun hetmet_pga_second =>
 557       dsLookupVar "GHC.HetMet.Private" "pga_cancell" >>= fun hetmet_pga_cancell =>
 558       dsLookupVar "GHC.HetMet.Private" "pga_cancelr" >>= fun hetmet_pga_cancelr =>
 559       dsLookupVar "GHC.HetMet.Private" "pga_uncancell" >>= fun hetmet_pga_uncancell =>
 560       dsLookupVar "GHC.HetMet.Private" "pga_uncancelr" >>= fun hetmet_pga_uncancelr =>
 561       dsLookupVar "GHC.HetMet.Private" "pga_assoc" >>= fun hetmet_pga_assoc =>
 562       dsLookupVar "GHC.HetMet.Private" "pga_unassoc" >>= fun hetmet_pga_unassoc =>
 563       dsLookupVar "GHC.HetMet.Private" "pga_copy" >>= fun hetmet_pga_copy =>
 564       dsLookupVar "GHC.HetMet.Private" "pga_drop" >>= fun hetmet_pga_drop =>
 565       dsLookupVar "GHC.HetMet.Private" "pga_swap" >>= fun hetmet_pga_swap =>
 566       dsLookupVar "GHC.HetMet.Private" "pga_applyl" >>= fun hetmet_pga_applyl =>
 567       dsLookupVar "GHC.HetMet.Private" "pga_applyr" >>= fun hetmet_pga_applyr =>
 568       dsLookupVar "GHC.HetMet.Private" "pga_curryl" >>= fun hetmet_pga_curryl =>
 569       dsLookupVar "GHC.HetMet.Private" "pga_curryr" >>= fun hetmet_pga_curryr =>
 570       dsLookupVar "GHC.HetMet.Private" "pga_loopl" >>= fun hetmet_pga_loopl =>
 571       dsLookupVar "GHC.HetMet.Private" "pga_loopr" >>= fun hetmet_pga_loopr =>
 572       dsLookupVar "GHC.HetMet.Private" "pga_kappa" >>= fun hetmet_pga_kappa =>
 573
 574     CoreMreturn
 575     (coqPassCoreToCore'
 576        do_flatten
 577        do_skolemize
 578        hetmet_brak
 579        hetmet_esc
 580        (*
 581        hetmet_kappa
 582        hetmet_kappa_app
 583        *)
 584        uniqueSupply
 585        hetmet_PGArrow
 586        hetmet_PGArrow_unit
 587        hetmet_PGArrow_tensor
 588 (*       hetmet_PGArrow_exponent_TyCon*)
 589        hetmet_pga_id
 590        hetmet_pga_comp
 591        hetmet_pga_first
 592        hetmet_pga_second
 593        hetmet_pga_cancell
 594        hetmet_pga_cancelr
 595        hetmet_pga_uncancell
 596        hetmet_pga_uncancelr
 597        hetmet_pga_assoc
 598        hetmet_pga_unassoc
 599        hetmet_pga_copy
 600        hetmet_pga_drop
 601        hetmet_pga_swap
 602        hetmet_pga_loopl
 603        hetmet_pga_loopr
 604        hetmet_pga_kappa
 605        lbinds
 606        (*
 607        hetmet_pga_applyl
 608        hetmet_pga_applyr
 609        hetmet_pga_curryl
 610        *)
 611        )
 612        .
 613
 614 End core2proof.