X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=src%2FExtractionMain.v;h=9f0fc1a640b70f45a2d5c98a0f620a5fb4c55f51;hb=025c2de2effdd7177ca875998b65f51236c8c7c6;hp=5bfa2100133390e9e6380dc67ec92c9e4b8df7f8;hpb=68f5bca870525f0740a4c5cb1fdbc7c7ce270306;p=coq-hetmet.git diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 5bfa210..9f0fc1a 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -179,12 +179,11 @@ Section core2proof. 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 (hetmet_flatten : WeakExprVar). - Context (hetmet_unflatten : WeakExprVar). - Context (hetmet_flattened_id : 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 @@ -270,6 +269,16 @@ Section core2proof. 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 ]. @@ -287,15 +296,25 @@ Section core2proof. 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) + (hetmet_kappa : WeakExprVar) + (hetmet_kappa_app : WeakExprVar) (uniqueSupply : UniqSupply) (lbinds:list (@CoreBind CoreVar)) (hetmet_PGArrowTyCon : TyFun) @@ -321,6 +340,7 @@ Section core2proof. (hetmet_pga_curryr : CoreVar) (hetmet_pga_loopl : CoreVar) (hetmet_pga_loopr : CoreVar) + (hetmet_pga_kappa : CoreVar) . @@ -421,23 +441,22 @@ Section core2proof. ; 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 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) @@ -454,25 +473,23 @@ Section core2proof. (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 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)) 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) >>= 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)) @@ -482,7 +499,7 @@ Section core2proof. 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)))) @@ -527,9 +544,8 @@ Section core2proof. : 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 => + 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 => @@ -553,6 +569,7 @@ Section core2proof. 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' @@ -560,9 +577,10 @@ Section core2proof. do_skolemize hetmet_brak hetmet_esc - hetmet_flatten - hetmet_unflatten - hetmet_flattened_id + (* + hetmet_kappa + hetmet_kappa_app + *) uniqueSupply hetmet_PGArrow hetmet_PGArrow_unit @@ -583,6 +601,7 @@ Section core2proof. hetmet_pga_swap hetmet_pga_loopl hetmet_pga_loopr + hetmet_pga_kappa lbinds (* hetmet_pga_applyl