Require Import General.
Require Import NaturalDeduction.
-Require Import NaturalDeductionToLatex.
+Require Import NaturalDeductionContext.
Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskCoreVars.
Require Import HaskCoreTypes.
Require Import HaskCore.
Require Import HaskWeakToCore.
Require Import HaskProofToStrong.
-Require Import ProgrammingLanguage.
-
-Require Import HaskProofCategory.
-(*
-Require Import HaskStrongCategory.
-*)
-Require Import ReificationsIsomorphicToGeneralizedArrows.
+Require Import HaskFlattener.
Open Scope string_scope.
Extraction Language Haskell.
Extract Inlined Constant string_dec => "(==)".
Extract Inlined Constant ascii_dec => "(==)".
-(* adapted from ExtrOcamlString.v *)
-Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'".
+Extract Inductive ascii => "Char" [ "you_forgot_to_patch_coq" ] "you_forgot_to_patch_coq".
Extract Constant zero => "'\000'".
Extract Constant one => "'\001'".
Extract Constant shift => "shiftAscii".
Variable mkTyVar : Name -> Kind -> CoreVar.
Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
- Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))".
+ Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoType t1 t2))".
Variable mkExVar : Name -> CoreType -> CoreVar.
Extract Inlined Constant mkExVar => "Id.mkLocalId".
+Variable CoreM : Type -> Type.
+ Extract Constant CoreM "a" => "CoreMonad.CoreM".
+ Extraction Inline CoreM.
+Variable CoreMreturn : forall a, a -> CoreM a.
+ Extraction Implicit CoreMreturn [a].
+ Implicit Arguments CoreMreturn [[a]].
+ Extract Inlined Constant CoreMreturn => "Prelude.return".
+Variable CoreMbind : forall a b, CoreM a -> (a -> CoreM b) -> CoreM b.
+ Extraction Implicit CoreMbind [a b].
+ Implicit Arguments CoreMbind [[a] [b]].
+ Extract Inlined Constant CoreMbind => "(Prelude.>>=)".
+
Section core2proof.
Context (ce:@CoreExpr CoreVar).
(* We need to be able to resolve unbound exprvars, but we can be sure their types will have no
* free tyvars in them *)
Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
- match coreVarToWeakVar cv with
- | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
+ match coreVarToWeakVar' cv with
+ | OK (WExprVar wev) => match weakTypeToTypeOfKind φ wev ★ with
| Error s => Prelude_error ("Error converting weakType of top-level variable "+++
toString cv+++": " +++ s)
| OK t => t @@ nil
end
- | WTypeVar _ => Prelude_error "top-level xi got a type variable"
- | WCoerVar _ => Prelude_error "top-level xi got a coercion variable"
+ | OK (WTypeVar _) => Prelude_error "top-level xi got a type variable"
+ | OK (WCoerVar _) => Prelude_error "top-level xi got a coercion variable"
+ | Error s => Prelude_error s
end.
-
- (* core-to-string (-dcoqpass) *)
-
Definition header : string :=
- "\documentclass[9pt]{article}"+++eol+++
+ "\documentclass{article}"+++eol+++
"\usepackage{amsmath}"+++eol+++
"\usepackage{amssymb}"+++eol+++
"\usepackage{proof}"+++eol+++
- "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++
"\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
"\def\code#1#2{\Box_{#1} #2}"+++eol+++
- "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
- "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
+ "\usepackage[paperwidth=\maxdimen,paperheight=\maxdimen]{geometry}"+++eol+++
+ "\usepackage[tightpage,active]{preview}"+++eol+++
"\begin{document}"+++eol+++
- "\begin{preview}"+++eol.
+ "\setlength\PreviewBorder{5pt}"+++eol.
Definition footer : string :=
- eol+++"\end{preview}"+++
eol+++"\end{document}"+++
eol.
-
+ (* core-to-string (-dcoqpass) *)
Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
addErrorMessage ("input CoreSyn: " +++ toString ce)
(addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
addErrorMessage ("HaskType: " +++ toString τ)
((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
- OK (eol+++"$$"+++ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++"$$"+++eol)
+ OK (eol+++eol+++eol+++
+ "\begin{preview}"+++eol+++
+ "$\displaystyle "+++
+ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ _ e))+++
+ " $"+++eol+++
+ "\end{preview}"+++eol+++eol+++eol)
)))))))).
Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
- weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
+ weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) t1 t2.
Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
- Context (hetmet_brak : WeakExprVar).
- Context (hetmet_esc : WeakExprVar).
- Context (uniqueSupply : UniqSupply).
+ Context (hetmet_brak : WeakExprVar).
+ Context (hetmet_esc : WeakExprVar).
+ Context (uniqueSupply : UniqSupply).
Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
match ut with
apply t.
Defined.
- Definition env := ★::nil.
- Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
- Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
- eapply nd_comp.
- eapply nd_comp.
- eapply nd_rule.
- apply RVar.
- eapply nd_rule.
- eapply (RURule _ _ _ _ (RuCanL _ _)) .
- eapply nd_rule.
- eapply RLam.
+ End CoreToCore.
+
+ Definition coreVarToWeakExprVarOrError cv :=
+ match addErrorMessage ("in coreVarToWeakExprVarOrError" +++ eol) (coreVarToWeakVar' cv) with
+ | OK (WExprVar wv) => wv
+ | Error s => Prelude_error s
+ | _ => Prelude_error "IMPOSSIBLE"
+ end.
+
+ Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
+ ND Rule
+ [ Γ > Δ > Σ |- [a ---> s ]@lev ]
+ [ Γ > Δ > [a @@ lev],,Σ |- [ s ]@lev ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RApp ].
+ eapply nd_comp; [ apply nd_rlecnac | idtac ].
+ apply nd_prod.
+ apply nd_id.
+ apply nd_rule.
+ apply RVar.
+ Defined.
+
+ Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
+ ND Rule [] [ Γ > Δ > [ ] |- [a ---> s ]@lev ] ->
+ ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s ]@lev ].
+ intro pf.
+ eapply nd_comp.
+ apply pf.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ].
+ apply curry.
+ Defined.
+
+ Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} :
+ ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) ]@lev ] ->
+ ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s ]@lev ].
+ intro pf.
+ eapply nd_comp.
+ eapply pf.
+ clear pf.
+ eapply nd_comp.
+ eapply curry.
+ eapply nd_comp.
+ eapply nd_rule.
+ eapply RArrange.
+ eapply ACanR.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
+ apply curry.
+ Defined.
+
+ Section coqPassCoreToCore.
+ Context
+ (do_flatten : bool)
+ (do_skolemize : bool)
+ (hetmet_brak : CoreVar)
+ (hetmet_esc : CoreVar)
+ (uniqueSupply : UniqSupply)
+ (lbinds:list (@CoreBind CoreVar))
+ (hetmet_PGArrowTyCon : TyFun)
+ (hetmet_PGArrow_unit_TyCon : TyFun)
+ (hetmet_PGArrow_tensor_TyCon : TyFun)
+ (hetmet_PGArrow_exponent_TyCon : TyFun)
+ (hetmet_pga_id : CoreVar)
+ (hetmet_pga_comp : CoreVar)
+ (hetmet_pga_first : CoreVar)
+ (hetmet_pga_second : CoreVar)
+ (hetmet_pga_cancell : CoreVar)
+ (hetmet_pga_cancelr : CoreVar)
+ (hetmet_pga_uncancell : CoreVar)
+ (hetmet_pga_uncancelr : CoreVar)
+ (hetmet_pga_assoc : CoreVar)
+ (hetmet_pga_unassoc : CoreVar)
+ (hetmet_pga_copy : CoreVar)
+ (hetmet_pga_drop : CoreVar)
+ (hetmet_pga_swap : CoreVar)
+ (hetmet_pga_applyl : CoreVar)
+ (hetmet_pga_applyr : CoreVar)
+ (hetmet_pga_curryl : CoreVar)
+ (hetmet_pga_curryr : CoreVar)
+ (hetmet_pga_loopl : CoreVar)
+ (hetmet_pga_loopr : CoreVar)
+ .
+
+
+ Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
+ @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
+
+ Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
+ (@TyFunApp TV
+ hetmet_PGArrow_tensor_TyCon
+ (ECKind::★ ::★ ::nil) ★
+ (TyFunApp_cons _ _ ec
+ (TyFunApp_cons _ _ a
+ (TyFunApp_cons _ _ b
+ TyFunApp_nil)))).
+
+ Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
+ TApp (TApp (TApp (@TyFunApp TV
+ hetmet_PGArrowTyCon
+ nil _ TyFunApp_nil) a) b) c.
+
+ Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
+
+ Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
+ fun TV ite => TApp (TApp (TApp (@TyFunApp TV
+ hetmet_PGArrowTyCon
+ nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
+
+ Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) :
+ IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★.
+ intros.
+ inversion X; subst.
+ inversion X1; subst.
+ apply f; auto.
Defined.
-(*
- Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
- addErrorMessage ("input CoreSyn: " +++ toString ce)
- (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
- coreExprToWeakExpr ce >>= fun we =>
- addErrorMessage ("WeakExpr: " +++ toString we)
- ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
- ((weakTypeOfWeakExpr we) >>= fun t =>
- (addErrorMessage ("WeakType: " +++ toString t)
- ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
- addErrorMessage ("HaskType: " +++ toString τ)
- ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
- (let haskProof := @expr2proof _ _ _ _ _ _ e
- in (* insert HaskProof-to-HaskProof manipulations here *)
- (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof))
- >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e'))
-(*
- >>= fun e' =>
- Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e'))
- *)
-)
-)))))))).
-(* Error "X").*)
-(*
- strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
- (projT2 e')
- INil
- >>= fun q => Error (toString q)
- ))))))))).
-*)*)
+ Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
+ : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ].
+ apply nd_rule.
+ refine (@RGlobal Γ Δ l
+ {| glob_wv := coreVarToWeakExprVarOrError cv
+ ; glob_kinds := κ₁ :: κ₂ :: nil
+ ; glob_tf := mkGlob2'(Γ:=Γ) f
+ |} (ICons _ _ x (ICons _ _ y INil))).
+ Defined.
+ Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) :
+ IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★.
+ intros.
+ inversion X; subst.
+ inversion X1; subst.
+ inversion X3; subst.
+ apply f; auto.
+ Defined.
- Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
- addErrorMessage ("input CoreSyn: " +++ toString ce)
- (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
- coreExprToWeakExpr ce >>= fun we =>
+ Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
+ : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ].
+ apply nd_rule.
+ refine (@RGlobal Γ Δ l
+ {| glob_wv := coreVarToWeakExprVarOrError cv
+ ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil
+ ; glob_tf := mkGlob3'(Γ:=Γ) f
+ |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))).
+ Defined.
+
+ Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) :
+ IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★.
+ intros.
+ inversion X; subst.
+ inversion X1; subst.
+ inversion X3; subst.
+ inversion X5; subst.
+ apply f; auto.
+ Defined.
+
+ Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
+ : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l].
+ apply nd_rule.
+ refine (@RGlobal Γ Δ l
+ {| glob_wv := coreVarToWeakExprVarOrError cv
+ ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil
+ ; glob_tf := mkGlob4'(Γ:=Γ) f
+ |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
+ Defined.
+
+ Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ ec x.
+
+ Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
+ { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat ec a)
+ ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat ec a)
+ ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat ec a)
+ ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
+ ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
+ ; 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)
+ ; 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)
+ ; 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)
+ ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat ec a)
+ ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat ec a)
+ ; 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))
+ ; 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))
+ ; 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))
+(* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
+(* ; ga_curry := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*)
+(* ; ga_apply := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*)
+(* ; ga_kappa := fun Γ Δ ec l a => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*)
+ ; 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))
+ ; 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))
+ ; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit"
+ ; ga_curry := fun Γ Δ ec l a b c => Prelude_error "ga_curry"
+ ; ga_apply := fun Γ Δ ec l a b c => Prelude_error "ga_apply"
+ ; ga_kappa := fun Γ Δ ec l a => Prelude_error "ga_kappa"
+ }.
+
+ Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
+ Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
+
+ Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
+ addErrorMessage ("input CoreSyn: " +++ toString cex)
+ (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr cex)) (
+ coreExprToWeakExpr cex >>= fun we =>
addErrorMessage ("WeakExpr: " +++ toString we)
((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
((weakTypeOfWeakExpr we) >>= fun t =>
((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
(addErrorMessage ("HaskStrong...")
- (let haskProof := @expr2proof _ _ _ _ _ _ e
- in (* insert HaskProof-to-HaskProof manipulations here *)
- OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
- >>= fun e' =>
- (snd e') >>= fun e'' =>
- strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
- (projT2 e'') INil
- >>= fun q =>
- OK (weakExprToCoreExpr q)
- )))))))))).
+ (if do_skolemize
+ then
+ (let haskProof := skolemize_and_flatten_proof my_ga (@expr2proof _ _ _ _ _ _ _ e)
+ in (* insert HaskProof-to-HaskProof manipulations here *)
+ OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _
+ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
+ >>= fun e' => (snd e') >>= fun e'' =>
+ strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
+ (projT2 e'') INil
+ >>= fun q => OK (weakExprToCoreExpr q))
+ else (if do_flatten
+ then
+ (let haskProof := flatten_proof (@expr2proof _ _ _ _ _ _ _ e)
+ in (* insert HaskProof-to-HaskProof manipulations here *)
+ OK ((@proof2expr nat _ FreshNat _ _ τ nil _
+ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
+ >>= fun e' => (snd e') >>= fun e'' =>
+ strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
+ (projT2 e'') INil
+ >>= fun q => OK (weakExprToCoreExpr q))
+ else
+ (let haskProof := @expr2proof _ _ _ _ _ _ _ e
+ in (* insert HaskProof-to-HaskProof manipulations here *)
+ OK ((@proof2expr nat _ FreshNat _ _ τ nil _
+ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
+ >>= fun e' => (snd e') >>= fun e'' =>
+ strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
+ (projT2 e'') INil
+ >>= fun q => OK (weakExprToCoreExpr q))))
+ ))))))))).
Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
match coreToCoreExpr' ce with
| OK x => x
| Error s => Prelude_error s
end.
-
+
Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
match binds with
- | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
+ | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
+
| CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
+ (* FIXME: doesn't deal with the case where top level recursive binds change type *)
+(*
+ match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
+ | CoreELet (CoreRec lbe') => lbe'
+ | x => Prelude_error
+ ("coreToCoreExpr was given a letrec, " +++
+ "but returned something that wasn't a letrec: " +++ toString x)
+ end
+*)
end.
-
+
Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
map coreToCoreBind lbinds.
- End CoreToCore.
+ End coqPassCoreToCore.
- Definition coqPassCoreToCore
- (hetmet_brak : CoreVar)
- (hetmet_esc : CoreVar)
+ Notation "a >>= b" := (@CoreMbind _ _ a b).
+
+ Definition coqPassCoreToCore
+ (do_flatten : bool)
+ (do_skolemize : bool)
+ (dsLookupVar : string -> string -> CoreM CoreVar)
+ (dsLookupTyc : string -> string -> CoreM TyFun)
(uniqueSupply : UniqSupply)
- (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
- match coreVarToWeakVar hetmet_brak with
- | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
- | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
- | _ => Prelude_error "IMPOSSIBLE"
- end
- | _ => Prelude_error "IMPOSSIBLE"
- end.
+ (lbinds : list (@CoreBind CoreVar))
+ : CoreM (list (@CoreBind CoreVar)) :=
+ dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_brak" >>= fun hetmet_brak =>
+ dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_esc" >>= fun hetmet_esc =>
+ dsLookupTyc "GHC.HetMet.Private" "PGArrow" >>= fun hetmet_PGArrow =>
+ dsLookupTyc "GHC.HetMet.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit =>
+ dsLookupTyc "GHC.HetMet.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor =>
+ dsLookupTyc "GHC.HetMet.GArrow" "GArrowExponent" >>= fun hetmet_PGArrow_exponent =>
+ dsLookupVar "GHC.HetMet.Private" "pga_id" >>= fun hetmet_pga_id =>
+ dsLookupVar "GHC.HetMet.Private" "pga_comp" >>= fun hetmet_pga_comp =>
+ dsLookupVar "GHC.HetMet.Private" "pga_first" >>= fun hetmet_pga_first =>
+ dsLookupVar "GHC.HetMet.Private" "pga_second" >>= fun hetmet_pga_second =>
+ dsLookupVar "GHC.HetMet.Private" "pga_cancell" >>= fun hetmet_pga_cancell =>
+ dsLookupVar "GHC.HetMet.Private" "pga_cancelr" >>= fun hetmet_pga_cancelr =>
+ dsLookupVar "GHC.HetMet.Private" "pga_uncancell" >>= fun hetmet_pga_uncancell =>
+ dsLookupVar "GHC.HetMet.Private" "pga_uncancelr" >>= fun hetmet_pga_uncancelr =>
+ dsLookupVar "GHC.HetMet.Private" "pga_assoc" >>= fun hetmet_pga_assoc =>
+ dsLookupVar "GHC.HetMet.Private" "pga_unassoc" >>= fun hetmet_pga_unassoc =>
+ dsLookupVar "GHC.HetMet.Private" "pga_copy" >>= fun hetmet_pga_copy =>
+ dsLookupVar "GHC.HetMet.Private" "pga_drop" >>= fun hetmet_pga_drop =>
+ dsLookupVar "GHC.HetMet.Private" "pga_swap" >>= fun hetmet_pga_swap =>
+ dsLookupVar "GHC.HetMet.Private" "pga_applyl" >>= fun hetmet_pga_applyl =>
+ dsLookupVar "GHC.HetMet.Private" "pga_applyr" >>= fun hetmet_pga_applyr =>
+ dsLookupVar "GHC.HetMet.Private" "pga_curryl" >>= fun hetmet_pga_curryl =>
+ dsLookupVar "GHC.HetMet.Private" "pga_curryr" >>= fun hetmet_pga_curryr =>
+ dsLookupVar "GHC.HetMet.Private" "pga_loopl" >>= fun hetmet_pga_loopl =>
+ dsLookupVar "GHC.HetMet.Private" "pga_loopr" >>= fun hetmet_pga_loopr =>
+
+ CoreMreturn
+ (coqPassCoreToCore'
+ do_flatten
+ do_skolemize
+ hetmet_brak
+ hetmet_esc
+ uniqueSupply
+ hetmet_PGArrow
+ hetmet_PGArrow_unit
+ hetmet_PGArrow_tensor
+(* hetmet_PGArrow_exponent_TyCon*)
+ hetmet_pga_id
+ hetmet_pga_comp
+ hetmet_pga_first
+ hetmet_pga_second
+ hetmet_pga_cancell
+ hetmet_pga_cancelr
+ hetmet_pga_uncancell
+ hetmet_pga_uncancelr
+ hetmet_pga_assoc
+ hetmet_pga_unassoc
+ hetmet_pga_copy
+ hetmet_pga_drop
+ hetmet_pga_swap
+ hetmet_pga_loopl
+ hetmet_pga_loopr
+ lbinds
+ (*
+ hetmet_pga_applyl
+ hetmet_pga_applyr
+ hetmet_pga_curryl
+ *)
+ )
+ .
End core2proof.