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