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
  17 Require Import HaskKinds.
  18 Require Import HaskLiteralsAndTyCons.
  19 Require Import HaskCoreVars.
  20 Require Import HaskCoreTypes.
  21 Require Import HaskCore.
  22 Require Import HaskWeakVars.
  23 Require Import HaskWeakTypes.
  24 Require Import HaskWeak.
  25 Require Import HaskStrongTypes.
  26 Require Import HaskStrong.
  27 Require Import HaskProof.
  28 Require Import HaskCoreToWeak.
  29 Require Import HaskWeakToStrong.
  30 Require Import HaskStrongToProof.
  31 Require Import HaskProofToLatex.
  32 Require Import HaskStrongToWeak.
  33 Require Import HaskWeakToCore.
  34 Require Import HaskProofToStrong.
  35
  36 Require Import HaskFlattener.
  37
  38 Open Scope string_scope.
  39 Extraction Language Haskell.
  40
  41 (*Extract Inductive vec    => "([])" [ "([])" "(:)" ].*)
  42 (*Extract Inductive Tree   => "([])" [ "([])" "(:)" ].*)
  43 (*Extract Inlined Constant map => "Prelude.map".*)
  44
  45 (* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
  46 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
  47 Extract Inductive list   => "([])" [ "([])" "(:)" ].
  48 Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
  49 Extract Inductive prod   => "(,)" [ "(,)" ].
  50 Extract Inductive sum    => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
  51 Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
  52 Extract Inductive bool    => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
  53 Extract Inductive unit    => "()" [ "()" ].
  54 Extract Inlined Constant string_dec => "(==)".
  55 Extract Inlined Constant ascii_dec => "(==)".
  56
  57 Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
  58 Extract Constant zero   => "'\000'".
  59 Extract Constant one    => "'\001'".
  60 Extract Constant shift  => "shiftAscii".
  61
  62 Unset Extraction Optimize.
  63 Unset Extraction AutoInline.
  64
  65 Variable Name : Type.  Extract Inlined Constant Name => "Name.Name".
  66 Variable mkSystemName : Unique -> string -> nat -> Name.
  67   Extract Inlined Constant mkSystemName =>
  68     "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
  69 Variable mkTyVar : Name -> Kind -> CoreVar.
  70   Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
  71 Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
  72   Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
  73 Variable mkExVar : Name -> CoreType -> CoreVar.
  74   Extract Inlined Constant mkExVar => "Id.mkLocalId".
  75
  76 Section core2proof.
  77   Context (ce:@CoreExpr CoreVar).
  78
  79   Definition Γ : TypeEnv := nil.
  80
  81   Definition Δ : CoercionEnv Γ := nil.
  82
  83   Definition φ : TyVarResolver Γ :=
  84     fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
  85     (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
  86
  87   Definition ψ : CoVarResolver Γ Δ :=
  88     fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
  89
  90   (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
  91    * free tyvars in them *)
  92   Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
  93     match coreVarToWeakVar cv with
  94       | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
  95                           | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
  96                                                          toString cv+++": " +++ s)
  97                           | OK    t => t @@ nil
  98                         end
  99       | WTypeVar _   => Prelude_error "top-level xi got a type variable"
 100       | WCoerVar _   => Prelude_error "top-level xi got a coercion variable"
 101     end.
 102
 103   Definition header : string :=
 104     "\documentclass{article}"+++eol+++
 105     "\usepackage{amsmath}"+++eol+++
 106     "\usepackage{amssymb}"+++eol+++
 107     "\usepackage{proof}"+++eol+++
 108     "\usepackage{trfrac}       % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
 109     "\def\code#1#2{\Box_{#1} #2}"+++eol+++
 110     "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
 111     "\usepackage[tightpage,active]{preview}"+++eol+++
 112     "\begin{document}"+++eol+++
 113     "\setlength\PreviewBorder{5pt}"+++eol.
 114
 115   Definition footer : string :=
 116     eol+++"\end{document}"+++
 117     eol.
 118
 119   (* core-to-string (-dcoqpass) *)
 120   Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
 121     addErrorMessage ("input CoreSyn: " +++ toString ce)
 122     (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 123       coreExprToWeakExpr ce >>= fun we =>
 124         addErrorMessage ("WeakExpr: " +++ toString we)
 125           ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 126             ((weakTypeOfWeakExpr we) >>= fun t =>
 127               (addErrorMessage ("WeakType: " +++ toString t)
 128                 ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 129                   addErrorMessage ("HaskType: " +++ toString τ)
 130                   ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
 131                     OK (eol+++eol+++eol+++
 132                         "\begin{preview}"+++eol+++
 133                         "$\displaystyle "+++
 134                         toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++
 135                         " $"+++eol+++
 136                         "\end{preview}"+++eol+++eol+++eol)
 137                   )))))))).
 138
 139   Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
 140     match coreToStringExpr' ce with
 141       | OK x => x
 142       | Error s => Prelude_error s
 143     end.
 144
 145   Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
 146     match binds with
 147       | CoreNonRec _ e => coreToStringExpr e
 148       | CoreRec    lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
 149     end.
 150
 151   Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
 152     header +++
 153     (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
 154     +++ footer.
 155
 156
 157   (* core-to-core (-fcoqpass) *)
 158   Section CoreToCore.
 159
 160     Definition mkWeakTypeVar (u:Unique)(k:Kind)                 : WeakTypeVar :=
 161       weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
 162     Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
 163       weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
 164     Definition mkWeakExprVar (u:Unique)(t:WeakType)             : WeakExprVar :=
 165       weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
 166
 167     Context (hetmet_brak  : WeakExprVar).
 168     Context (hetmet_esc   : WeakExprVar).
 169     Context (uniqueSupply : UniqSupply).
 170
 171     Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
 172       match ut with
 173         uniqM f =>
 174          f uniqueSupply >>= fun x => OK (snd x)
 175       end.
 176
 177     Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
 178       intros.
 179       induction ln.
 180       exists O.
 181       intros.
 182       inversion H.
 183       destruct IHln as [n pf].
 184       exists (plus (S n) a).
 185       intros.
 186       destruct H.
 187       omega.
 188       fold (@In _ n' ln) in H.
 189       set (pf n' H) as q.
 190       omega.
 191       Defined.
 192
 193   Definition FreshNat : @FreshMonad nat.
 194     refine {| FMT       := fun T => nat -> prod nat T
 195             ; FMT_fresh := _
 196            |}.
 197     Focus 2.
 198     intros.
 199     refine ((S H),_).
 200     set (larger tl) as q.
 201     destruct q as [n' pf].
 202     exists n'.
 203     intros.
 204     set (pf _ H0) as qq.
 205     omega.
 206
 207     refine {| returnM := fun a (v:a) => _ |}.
 208       intro n. exact (n,v).
 209       intros.
 210       set (X H) as q.
 211       destruct q as [n' v].
 212       set (X0 v n') as q'.
 213       exact q'.
 214       Defined.
 215
 216     Definition unFresh {T} : @FreshM _ FreshNat T -> T.
 217       intros.
 218       destruct X.
 219       exact O.
 220       apply t.
 221       Defined.
 222 (*
 223     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 224       addErrorMessage ("input CoreSyn: " +++ toString ce)
 225       (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 226         coreExprToWeakExpr ce >>= fun we =>
 227           addErrorMessage ("WeakExpr: " +++ toString we)
 228             ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 229               ((weakTypeOfWeakExpr we) >>= fun t =>
 230                 (addErrorMessage ("WeakType: " +++ toString t)
 231                   ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 232
 233                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 234
 235                       (addErrorMessage ("HaskStrong...")
 236                         (let haskProof := (*flatten_proof'*) (@expr2proof _ _ _ _ _ _ e)
 237                          in (* insert HaskProof-to-HaskProof manipulations here *)
 238                          OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 239                          >>= fun e' =>
 240                            (snd e') >>= fun e'' =>
 241                          strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 242                            (projT2 e'') INil
 243                          >>= fun q =>
 244                            OK (weakExprToCoreExpr q)
 245                     )))))))))).
 246
 247     Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
 248       match coreToCoreExpr' ce with
 249         | OK x    => x
 250         | Error s => Prelude_error s
 251       end.
 252
 253     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
 254       match binds with
 255         | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
 256         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
 257       end.
 258
 259     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 260       map coreToCoreBind lbinds.
 261   *)
 262
 263   End CoreToCore.
 264
 265   Definition coreVarToWeakExprVarOrError cv :=
 266     match coreVarToWeakVar cv with
 267       | WExprVar wv => wv
 268       | _           => Prelude_error "IMPOSSIBLE"
 269     end.
 270
 271   Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
 272     ND Rule
 273        [ Γ > Δ > Σ             |- [a ---> s @@ lev ] ]
 274        [ Γ > Δ > Σ,,[a @@ lev] |-       [ s @@ lev ] ].
 275     eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ].
 276     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 277     apply nd_prod.
 278     apply nd_id.
 279     apply nd_rule.
 280     apply RVar.
 281     Defined.
 282
 283   Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
 284     ND Rule [] [ Γ > Δ > [        ] |- [a ---> s @@ lev ] ] ->
 285     ND Rule [] [ Γ > Δ > [a @@ lev] |-       [ s @@ lev ] ].
 286     intro pf.
 287     eapply nd_comp.
 288     apply pf.
 289     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
 290     apply curry.
 291     Defined.
 292
 293   Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
 294     ND Rule [] [ Γ > Δ >                       [] |- [a1 ---> (a2 ---> s) @@ lev ] ] ->
 295     ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |-                 [ s @@ lev ] ].
 296     intro pf.
 297     eapply nd_comp.
 298     eapply pf.
 299     clear pf.
 300     eapply nd_comp.
 301     eapply curry.
 302     eapply nd_comp.
 303     eapply nd_rule.
 304     eapply RArrange.
 305     eapply RCanL.
 306     apply curry.
 307     Defined.
 308
 309   Section coqPassCoreToCore.
 310     Context
 311     (hetmet_brak  : CoreVar)
 312     (hetmet_esc   : CoreVar)
 313     (uniqueSupply : UniqSupply)
 314     (lbinds:list (@CoreBind CoreVar))
 315     (hetmet_PGArrowTyCon : TyFun)
 316     (hetmet_pga_id : CoreVar)
 317     (hetmet_pga_comp : CoreVar)
 318     (hetmet_pga_first : CoreVar)
 319     (hetmet_pga_second : CoreVar)
 320     (hetmet_pga_cancell : CoreVar)
 321     (hetmet_pga_cancelr : CoreVar)
 322     (hetmet_pga_uncancell : CoreVar)
 323     (hetmet_pga_uncancelr : CoreVar)
 324     (hetmet_pga_assoc : CoreVar)
 325     (hetmet_pga_unassoc : CoreVar)
 326     (hetmet_pga_copy : CoreVar)
 327     (hetmet_pga_drop : CoreVar)
 328     (hetmet_pga_swap : CoreVar)
 329     (hetmet_pga_applyl : CoreVar)
 330     (hetmet_pga_applyr : CoreVar)
 331     (hetmet_pga_curryl : CoreVar)
 332     (hetmet_pga_curryr : CoreVar)
 333     .
 334
 335     Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil         ★ TyFunApp_nil.
 336     Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★  :=
 337       TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b.
 338     Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
 339       TApp (TApp (TApp (@TyFunApp TV
 340         hetmet_PGArrowTyCon
 341         nil _ TyFunApp_nil) a) b) c.
 342     Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
 343
 344     Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
 345       fun TV ite => TApp (TApp (TApp (@TyFunApp TV
 346         hetmet_PGArrowTyCon
 347         nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
 348
 349     Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
 350       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
 351       intros.
 352       inversion X; subst.
 353       inversion X1; subst.
 354       apply f; auto.
 355       Defined.
 356
 357     Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
 358       : ND Rule [] [ Γ > Δ > [] |- [f x y @@ l] ].
 359       apply nd_rule.
 360       refine (@RGlobal Γ Δ l
 361         {| glob_wv    := coreVarToWeakExprVarOrError cv
 362           ; glob_kinds := κ₁ :: κ₂ :: nil
 363           ; glob_tf    := mkGlob2'(Γ:=Γ) f
 364           |} (ICons _ _ x (ICons _ _ y INil))).
 365       Defined.
 366
 367     Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
 368       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
 369       intros.
 370       inversion X; subst.
 371       inversion X1; subst.
 372       inversion X3; subst.
 373       apply f; auto.
 374       Defined.
 375
 376     Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
 377       : ND Rule [] [ Γ > Δ > [] |- [f x y z @@ l] ].
 378       apply nd_rule.
 379       refine (@RGlobal Γ Δ l
 380         {| glob_wv    := coreVarToWeakExprVarOrError cv
 381           ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
 382           ; glob_tf    := mkGlob3'(Γ:=Γ) f
 383           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
 384       Defined.
 385
 386     Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
 387       IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
 388       intros.
 389       inversion X; subst.
 390       inversion X1; subst.
 391       inversion X3; subst.
 392       inversion X5; subst.
 393       apply f; auto.
 394       Defined.
 395
 396     Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
 397       : ND Rule [] [ Γ > Δ > [] |- [f x y z q @@ l] ].
 398       apply nd_rule.
 399       refine (@RGlobal Γ Δ l
 400         {| glob_wv    := coreVarToWeakExprVarOrError cv
 401           ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
 402           ; glob_tf    := mkGlob4'(Γ:=Γ) f
 403           |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
 404       Defined.
 405
 406     Definition gat {Γ}(x:Tree ??(HaskType Γ ★))  := @ga_mk_tree ga_unit ga_prod _ x.
 407
 408     Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
 409     { ga_id        := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_id        (fun ec a => ga_type' ec a a) ec (gat a)
 410     ; ga_cancelr   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancelr   (fun ec a => ga_type' ec _ a) ec (gat a)
 411     ; ga_cancell   := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_cancell   (fun ec a => ga_type' ec _ a) ec (gat a)
 412     ; ga_uncancelr := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat a)
 413     ; ga_uncancell := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat a)
 414     ; ga_assoc     := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc     (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
 415     ; ga_unassoc   := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc   (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
 416     ; ga_swap      := fun Γ Δ ec l a b   => mkGlob3 hetmet_pga_swap      (fun ec a b => ga_type' ec _ _) ec (gat a) (gat b)
 417     ; ga_drop      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_drop      (fun ec a => ga_type' ec _ _) ec (gat a)
 418     ; ga_copy      := fun Γ Δ ec l a     => mkGlob2 hetmet_pga_copy      (fun ec a => ga_type' ec _ _) ec (gat a)
 419     ; ga_first     := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat a) (gat b) (gat x))
 420     ; ga_second    := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat a) (gat b) (gat x))
 421     ; ga_comp      := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat a) (gat b) (gat c))
 422 (*  ; ga_lit       := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
 423 (*  ; ga_curry     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
 424 (*  ; ga_apply     := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
 425 (*  ; ga_kappa     := fun Γ Δ ec l a     => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
 426     ; ga_lit       := fun Γ Δ ec l a     => Prelude_error "ga_lit"
 427     ; ga_curry     := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
 428     ; ga_apply     := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
 429     ; ga_kappa     := fun Γ Δ ec l a     => Prelude_error "ga_kappa"
 430     }.
 431
 432     Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
 433     Definition hetmet_esc'  := coreVarToWeakExprVarOrError hetmet_esc.
 434
 435     Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
 436       addErrorMessage ("input CoreSyn: " +++ toString ce)
 437       (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
 438         coreExprToWeakExpr ce >>= fun we =>
 439           addErrorMessage ("WeakExpr: " +++ toString we)
 440             ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
 441               ((weakTypeOfWeakExpr we) >>= fun t =>
 442                 (addErrorMessage ("WeakType: " +++ toString t)
 443                   ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
 444
 445                     ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
 446
 447                       (addErrorMessage ("HaskStrong...")
 448                         (let haskProof := flatten_proof my_ga (@expr2proof _ _ _ _ _ _ e)
 449                          in (* insert HaskProof-to-HaskProof manipulations here *)
 450                          OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
 451                          >>= fun e' =>
 452                            (snd e') >>= fun e'' =>
 453                          strongExprToWeakExpr hetmet_brak' hetmet_esc' mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
 454                            (projT2 e'') INil
 455                          >>= fun q =>
 456                            OK (weakExprToCoreExpr q)
 457                     )))))))))).
 458
 459     Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
 460       match coreToCoreExpr' ce with
 461         | OK x    => x
 462         | Error s => Prelude_error s
 463       end.
 464
 465     Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
 466       match binds with
 467         | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
 468         | CoreRec    lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
 469       end.
 470
 471     Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
 472       map coreToCoreBind lbinds.
 473
 474   End coqPassCoreToCore.
 475
 476     Definition coqPassCoreToCore
 477     (hetmet_brak  : CoreVar)
 478     (hetmet_esc   : CoreVar)
 479     (uniqueSupply : UniqSupply)
 480     (lbinds:list (@CoreBind CoreVar))
 481     (hetmet_PGArrowTyCon : TyFun)
 482     (hetmet_pga_id : CoreVar)
 483     (hetmet_pga_comp : CoreVar)
 484     (hetmet_pga_first : CoreVar)
 485     (hetmet_pga_second : CoreVar)
 486     (hetmet_pga_cancell : CoreVar)
 487     (hetmet_pga_cancelr : CoreVar)
 488     (hetmet_pga_uncancell : CoreVar)
 489     (hetmet_pga_uncancelr : CoreVar)
 490     (hetmet_pga_assoc : CoreVar)
 491     (hetmet_pga_unassoc : CoreVar)
 492     (hetmet_pga_copy : CoreVar)
 493     (hetmet_pga_drop : CoreVar)
 494     (hetmet_pga_swap : CoreVar)
 495     (hetmet_pga_applyl : CoreVar)
 496     (hetmet_pga_applyr : CoreVar)
 497     (hetmet_pga_curryl : CoreVar)
 498     (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=
 499     coqPassCoreToCore'
 500        hetmet_brak
 501        hetmet_esc
 502        uniqueSupply
 503        hetmet_PGArrowTyCon
 504        hetmet_pga_id
 505        hetmet_pga_comp
 506        hetmet_pga_first
 507        hetmet_pga_second
 508        hetmet_pga_cancell
 509        hetmet_pga_cancelr
 510        hetmet_pga_uncancell
 511        hetmet_pga_uncancelr
 512        hetmet_pga_assoc
 513        hetmet_pga_unassoc
 514        hetmet_pga_copy
 515        hetmet_pga_drop
 516        hetmet_pga_swap
 517        lbinds
 518        (*
 519        hetmet_pga_applyl
 520        hetmet_pga_applyr
 521        hetmet_pga_curryl
 522        *)
 523        .
 524
 525 End core2proof.