X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=5bfa2100133390e9e6380dc67ec92c9e4b8df7f8;hp=77326e0054370762fbe7dc90a8d4a1130ff8154d;hb=68f5bca870525f0740a4c5cb1fdbc7c7ce270306;hpb=57e387249da84dac0f1c5a9411e3900831ce2d81 diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 77326e0..5bfa210 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -13,6 +13,7 @@ Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import HaskKinds. Require Import HaskLiterals. @@ -70,10 +71,22 @@ Variable mkSystemName : Unique -> string -> nat -> Name. Variable mkTyVar : Name -> Kind -> CoreVar. Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))". Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar. - Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))". + Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoType t1 t2))". 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). @@ -91,14 +104,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 := @@ -132,7 +146,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) )))))))). @@ -227,8 +241,9 @@ Section core2proof. 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. @@ -236,7 +251,7 @@ Section core2proof. ND Rule [ Γ > Δ > Σ |- [a ---> s ]@lev ] [ Γ > Δ > [a @@ lev],,Σ |- [ s ]@lev ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + 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. @@ -251,7 +266,7 @@ Section core2proof. intro pf. eapply nd_comp. apply pf. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanR ]. apply curry. Defined. @@ -267,13 +282,15 @@ Section core2proof. eapply nd_comp. eapply nd_rule. eapply RArrange. - eapply RCanR. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + 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) @@ -302,6 +319,8 @@ Section core2proof. (hetmet_pga_applyr : CoreVar) (hetmet_pga_curryl : CoreVar) (hetmet_pga_curryr : CoreVar) + (hetmet_pga_loopl : CoreVar) + (hetmet_pga_loopr : CoreVar) . @@ -406,6 +425,8 @@ Section core2proof. (* ; 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_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" @@ -431,18 +452,41 @@ Section core2proof. ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => (addErrorMessage ("HaskStrong...") - (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) - )))))))))). + (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 @@ -471,45 +515,58 @@ Section core2proof. End coqPassCoreToCore. + Notation "a >>= b" := (@CoreMbind _ _ a b). + Definition coqPassCoreToCore - (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) : 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 => + 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 => + 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 => + + 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 @@ -524,13 +581,15 @@ Section core2proof. hetmet_pga_copy hetmet_pga_drop hetmet_pga_swap + hetmet_pga_loopl + hetmet_pga_loopr lbinds (* hetmet_pga_applyl hetmet_pga_applyr hetmet_pga_curryl *) - + ) . End core2proof.