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_kappa : WeakExprVar).
+ Context (hetmet_kappa_app : WeakExprVar).
+ Context (uniqueSupply : UniqSupply).
Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
match ut with
apply curry.
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 ].
apply curry.
Defined.
+ Definition fToCx {Γ}{Δ}{a1}{a2}{a3}{l} Σ :
+ ND Rule [] [ Γ > Δ > [] |- [(a1 ---> a2) ---> a3 ]@l ] ->
+ ND Rule [Γ > Δ > Σ,,[a1 @@ l] |- [a2]@l ]
+ [Γ > Δ > Σ |- [a3]@l ].
+ intro pf.
+ eapply nd_comp; [ eapply nd_rule; eapply RLam | idtac ].
+ set (fToC1 pf) as pf'.
+ apply boost.
+ apply pf'.
+ Defined.
+
Section coqPassCoreToCore.
Context
(do_flatten : bool)
(do_skolemize : bool)
(hetmet_brak : CoreVar)
(hetmet_esc : CoreVar)
+ (hetmet_kappa : WeakExprVar)
+ (hetmet_kappa_app : WeakExprVar)
(uniqueSupply : UniqSupply)
(lbinds:list (@CoreBind CoreVar))
(hetmet_PGArrowTyCon : TyFun)
(hetmet_pga_curryr : CoreVar)
(hetmet_pga_loopl : CoreVar)
(hetmet_pga_loopr : CoreVar)
+ (hetmet_pga_kappa : CoreVar)
.
; 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_curry := fun Γ Δ ec l a => Prelude_error "ga_curry"
+
+ ; ga_apply := fun Γ Δ ec l a => Prelude_error "ga_apply"
; 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"
+(* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*)
+ ; ga_kappa := fun Γ Δ ec l a b c Σ =>
+ fToCx Σ (mkGlob4 hetmet_pga_kappa (fun ec a b c => _) ec (gat ec a) (gat ec b) (gat ec c))
}.
Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
+ Definition hetmet_kappa' := coreVarToWeakExprVarOrError hetmet_kappa.
+ Definition hetmet_kappa_app' := coreVarToWeakExprVarOrError hetmet_kappa_app.
Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
addErrorMessage ("input CoreSyn: " +++ toString cex)
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'
+ strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
(projT2 e'') INil
>>= fun q => OK (weakExprToCoreExpr q))
OK ((@proof2expr nat _ FreshNat _ _ τ nil _
(fun _ => Prelude_error "unbound unique") _ haskProof) O)
>>= fun e' => (snd e') >>= fun e'' =>
- strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
(projT2 e'') INil
>>= fun q => OK (weakExprToCoreExpr q))
OK ((@proof2expr nat _ FreshNat _ _ τ nil _
(fun _ => Prelude_error "unbound unique") _ haskProof) O)
>>= fun e' => (snd e') >>= fun e'' =>
- strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
(projT2 e'') INil
>>= fun q => OK (weakExprToCoreExpr q))))
: CoreM (list (@CoreBind CoreVar)) :=
dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_brak" >>= fun hetmet_brak =>
dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_esc" >>= fun hetmet_esc =>
+ dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa" >>= fun hetmet_kappa =>
+ dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa_app" >>= fun hetmet_kappa_app =>
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 =>
+ dsLookupTyc "Control.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit =>
+ dsLookupTyc "Control.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor =>
+ dsLookupTyc "Control.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_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 =>
+ dsLookupVar "GHC.HetMet.Private" "pga_kappa" >>= fun hetmet_pga_kappa =>
CoreMreturn
(coqPassCoreToCore'
do_skolemize
hetmet_brak
hetmet_esc
+ (*
+ hetmet_kappa
+ hetmet_kappa_app
+ *)
uniqueSupply
hetmet_PGArrow
hetmet_PGArrow_unit
hetmet_pga_swap
hetmet_pga_loopl
hetmet_pga_loopr
+ hetmet_pga_kappa
lbinds
(*
hetmet_pga_applyl