X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=2e51d0e410a111c5911419869953a7c98c82453e;hp=e628f268153b1602c975584a4820bb5c2be96ac1;hb=4c5c94487aa2bf5489371f112607f0a4c4f01a94;hpb=b4857a6f575dffd5c9c9d5decbc21ff63a338270 diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index e628f26..2e51d0e 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -13,9 +13,11 @@ Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import HaskKinds. -Require Import HaskLiteralsAndTyCons. +Require Import HaskLiterals. +Require Import HaskTyCons. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. @@ -90,14 +92,15 @@ Section core2proof. (* 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. Definition header : string := @@ -131,7 +134,7 @@ Section core2proof. OK (eol+++eol+++eol+++ "\begin{preview}"+++eol+++ "$\displaystyle "+++ - toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++ + toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ _ e))+++ " $"+++eol+++ "\end{preview}"+++eol+++eol+++eol) )))))))). @@ -160,13 +163,16 @@ Section core2proof. 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 (hetmet_flatten : WeakExprVar). + Context (hetmet_unflatten : WeakExprVar). + Context (hetmet_flattened_id : WeakExprVar). + Context (uniqueSupply : UniqSupply). Definition useUniqueSupply {T}(ut:UniqM T) : ???T := match ut with @@ -219,80 +225,42 @@ Section core2proof. exact O. apply t. 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 τ => - - ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => - - (addErrorMessage ("HaskStrong...") - (let haskProof := (*flatten_proof'*) (@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) - )))))))))). - - 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) - | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe) - end. - - Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) := - map coreToCoreBind lbinds. - *) End CoreToCore. Definition coreVarToWeakExprVarOrError cv := - match coreVarToWeakVar cv with - | WExprVar wv => wv + 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; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ]. + [ Γ > Δ > Σ |- [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_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 ] ]. + 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 RCanL ]. + 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 ] ]. + ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) ]@lev ] -> + ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s ]@lev ]. intro pf. eapply nd_comp. eapply pf. @@ -302,17 +270,26 @@ Section core2proof. eapply nd_comp. eapply nd_rule. eapply RArrange. - eapply RCanL. + 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) + (hetmet_flatten : CoreVar) + (hetmet_unflatten : CoreVar) + (hetmet_flattened_id : 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) @@ -332,13 +309,24 @@ Section core2proof. (hetmet_pga_curryr : CoreVar) . - Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil ★ TyFunApp_nil. - Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★ := - TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b. + + 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 Γ ★ := @@ -355,7 +343,7 @@ Section core2proof. Defined. Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y - : ND Rule [] [ Γ > Δ > [] |- [f x y @@ l] ]. + : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ]. apply nd_rule. refine (@RGlobal Γ Δ l {| glob_wv := coreVarToWeakExprVarOrError cv @@ -374,7 +362,7 @@ Section core2proof. Defined. Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z - : ND Rule [] [ Γ > Δ > [] |- [f x y z @@ l] ]. + : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ]. apply nd_rule. refine (@RGlobal Γ Δ l {| glob_wv := coreVarToWeakExprVarOrError cv @@ -394,7 +382,7 @@ Section core2proof. Defined. Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q - : ND Rule [] [ Γ > Δ > [] |- [f x y z q @@ l] ]. + : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l]. apply nd_rule. refine (@RGlobal Γ Δ l {| glob_wv := coreVarToWeakExprVarOrError cv @@ -403,22 +391,22 @@ Section core2proof. |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))). Defined. - Definition gat {Γ}(x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ x. + 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 a) - ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat a) - ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat a) - ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat a) - ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat a) - ; 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) - ; 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) - ; ga_swap := fun Γ Δ ec l a b => mkGlob3 hetmet_pga_swap (fun ec a b => ga_type' ec _ _) ec (gat a) (gat b) - ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat a) - ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat a) - ; 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)) - ; 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)) - ; 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)) + { 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))*) @@ -431,11 +419,14 @@ Section core2proof. Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak. Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc. - - Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := - addErrorMessage ("input CoreSyn: " +++ toString ce) - (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) ( - coreExprToWeakExpr ce >>= fun we => + Definition hetmet_flatten' := coreVarToWeakExprVarOrError hetmet_flatten. + Definition hetmet_unflatten' := coreVarToWeakExprVarOrError hetmet_unflatten. + Definition hetmet_flattened_id' := coreVarToWeakExprVarOrError hetmet_flattened_id. + + 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 => @@ -445,27 +436,62 @@ Section core2proof. ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => (addErrorMessage ("HaskStrong...") - (let haskProof := flatten_proof my_ga (@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 hetmet_flatten' hetmet_unflatten' + hetmet_flattened_id' 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 (*hetmet_flatten' hetmet_unflatten' + hetmet_flattened_id' my_ga*) (@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) := @@ -474,11 +500,19 @@ Section core2proof. End coqPassCoreToCore. Definition coqPassCoreToCore + (do_flatten : bool) + (do_skolemize : bool) (hetmet_brak : CoreVar) (hetmet_esc : CoreVar) + (hetmet_flatten : CoreVar) + (hetmet_unflatten : CoreVar) + (hetmet_flattened_id : 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) @@ -497,10 +531,18 @@ Section core2proof. (hetmet_pga_curryl : CoreVar) (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) := coqPassCoreToCore' + do_flatten + do_skolemize hetmet_brak hetmet_esc + hetmet_flatten + hetmet_unflatten + hetmet_flattened_id uniqueSupply hetmet_PGArrowTyCon + hetmet_PGArrow_unit_TyCon + hetmet_PGArrow_tensor_TyCon +(* hetmet_PGArrow_exponent_TyCon*) hetmet_pga_id hetmet_pga_comp hetmet_pga_first @@ -520,6 +562,7 @@ Section core2proof. hetmet_pga_applyr hetmet_pga_curryl *) + . End core2proof.