X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=88714c73e6c8b71546086e28a384eb80aa0825fd;hp=e0226d83692efb89610f38647a562e3e68b62ffb;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=3282a2b78028238987a5a49e59d8e8d495aea0e1 diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index e0226d8..88714c7 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -75,6 +75,18 @@ Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar. 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). @@ -169,9 +181,6 @@ Section core2proof. 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 := @@ -258,6 +267,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 ]. @@ -275,15 +294,23 @@ 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) (uniqueSupply : UniqSupply) (lbinds:list (@CoreBind CoreVar)) (hetmet_PGArrowTyCon : TyFun) @@ -309,6 +336,7 @@ Section core2proof. (hetmet_pga_curryr : CoreVar) (hetmet_pga_loopl : CoreVar) (hetmet_pga_loopr : CoreVar) + (hetmet_pga_kappa : CoreVar) . @@ -409,23 +437,20 @@ 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 coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := addErrorMessage ("input CoreSyn: " +++ toString cex) @@ -442,8 +467,7 @@ 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) @@ -454,8 +478,7 @@ Section core2proof. >>= 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) @@ -503,52 +526,53 @@ Section core2proof. End coqPassCoreToCore. + Notation "a >>= b" := (@CoreMbind _ _ a b). + Definition coqPassCoreToCore - (do_flatten : bool) - (do_skolemize : bool) - (hetmet_brak : CoreVar) - (hetmet_esc : CoreVar) - (hetmet_flatten : CoreVar) - (hetmet_unflatten : CoreVar) - (hetmet_flattened_id : CoreVar) + (do_flatten : bool) + (do_skolemize : bool) + (dsLookupVar : string -> string -> CoreM CoreVar) + (dsLookupTyc : string -> string -> CoreM TyFun) (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) - : list (@CoreBind CoreVar) := - coqPassCoreToCore' + (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 => + dsLookupVar "GHC.HetMet.Private" "pga_kappa" >>= fun hetmet_pga_kappa => + + CoreMreturn + (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 + hetmet_PGArrow_unit + hetmet_PGArrow_tensor (* hetmet_PGArrow_exponent_TyCon*) hetmet_pga_id hetmet_pga_comp @@ -565,13 +589,14 @@ Section core2proof. hetmet_pga_swap hetmet_pga_loopl hetmet_pga_loopr + hetmet_pga_kappa lbinds (* hetmet_pga_applyl hetmet_pga_applyr hetmet_pga_curryl *) - + ) . End core2proof.