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