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 :=
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_flatten : CoreVar)
- (hetmet_unflatten : CoreVar)
- (hetmet_flattened_id : CoreVar)
(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_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 ("HaskStrong...")
(if do_skolemize
then
- (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
- hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e)
+ (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 q => OK (weakExprToCoreExpr q))
else (if do_flatten
then
- (let haskProof := flatten_proof (*hetmet_flatten' hetmet_unflatten'
- hetmet_flattened_id' my_ga*) (@expr2proof _ _ _ _ _ _ _ e)
+ (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)
: 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_flatten" >>= fun hetmet_flatten =>
- dsLookupVar "GHC.HetMet.CodeTypes" "pga_unflatten" >>= fun hetmet_unflatten =>
- dsLookupVar "GHC.HetMet.CodeTypes" "pga_flattened_id" >>= fun hetmet_flattened_id =>
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 =>
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_flatten
- hetmet_unflatten
- hetmet_flattened_id
uniqueSupply
hetmet_PGArrow
hetmet_PGArrow_unit
hetmet_pga_swap
hetmet_pga_loopl
hetmet_pga_loopr
+ hetmet_pga_kappa
lbinds
(*
hetmet_pga_applyl
projects / coq-hetmet.git / blobdiff