Require Import General.
Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
Require Import HaskKinds.
Require Import HaskLiterals.
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".
(* 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 :=
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)
)))))))).
Definition mkWeakTypeVar (u:Unique)(k:Kind) : WeakTypeVar :=
weakTypeVar (mkTyVar (mkSystemName u "tv" O) k) k.
Definition mkWeakCoerVar (u:Unique)(k:Kind)(t1 t2:WeakType) : WeakCoerVar :=
- weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) k t1 t2.
+ weakCoerVar (mkCoVar (mkSystemName u "cv" O) (weakTypeToCoreType t1) (weakTypeToCoreType t2)) t1 t2.
Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
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.
Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} :
ND Rule
- [ Γ > Δ > Σ |- [a ---> s @@ lev ] ]
- [ Γ > Δ > Σ,,[a @@ lev] |- [ s @@ lev ] ].
- eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ].
+ [ Γ > Δ > Σ |- [a ---> s ]@lev ]
+ [ Γ > Δ > [a @@ lev],,Σ |- [ s ]@lev ].
+ 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.
+ apply nd_prod.
apply nd_id.
apply nd_rule.
apply RVar.
Defined.
Definition fToC1 {Γ}{Δ}{a}{s}{lev} :
- ND Rule [] [ Γ > Δ > [ ] |- [a ---> s @@ lev ] ] ->
- ND Rule [] [ Γ > Δ > [a @@ lev] |- [ 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 RCanL ].
+ 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 ] ].
+ ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) ]@lev ] ->
+ ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s ]@lev ].
intro pf.
eapply nd_comp.
eapply pf.
eapply nd_comp.
eapply nd_rule.
eapply RArrange.
- eapply RCanL.
+ 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)
(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_curryr : CoreVar)
.
- Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil ★ TyFunApp_nil.
- Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
- TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b.
+
+ Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ :=
+ @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil).
+
+ Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★ :=
+ (@TyFunApp TV
+ hetmet_PGArrow_tensor_TyCon
+ (ECKind::★ ::★ ::nil) ★
+ (TyFunApp_cons _ _ ec
+ (TyFunApp_cons _ _ a
+ (TyFunApp_cons _ _ b
+ TyFunApp_nil)))).
+
Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
TApp (TApp (TApp (@TyFunApp TV
hetmet_PGArrowTyCon
nil _ TyFunApp_nil) a) b) c.
+
Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
Defined.
Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y
- : ND Rule [] [ Γ > Δ > [] |- [f x y @@ l] ].
+ : ND Rule [] [ Γ > Δ > [] |- [f x y ]@l ].
apply nd_rule.
refine (@RGlobal Γ Δ l
{| glob_wv := coreVarToWeakExprVarOrError cv
Defined.
Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z
- : ND Rule [] [ Γ > Δ > [] |- [f x y z @@ l] ].
+ : ND Rule [] [ Γ > Δ > [] |- [f x y z ]@l ].
apply nd_rule.
refine (@RGlobal Γ Δ l
{| glob_wv := coreVarToWeakExprVarOrError cv
Defined.
Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q
- : ND Rule [] [ Γ > Δ > [] |- [f x y z q @@ l] ].
+ : ND Rule [] [ Γ > Δ > [] |- [f x y z q ] @l].
apply nd_rule.
refine (@RGlobal Γ Δ l
{| glob_wv := coreVarToWeakExprVarOrError cv
|} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))).
Defined.
- Definition gat {Γ}(x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ x.
+ Definition gat {Γ} ec (x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ ec x.
Instance my_ga : garrow ga_unit ga_prod (@ga_type) :=
- { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat a)
- ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat a)
- ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat a)
- ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat a)
- ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat a)
- ; ga_assoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
- ; ga_unassoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c)
- ; ga_swap := fun Γ Δ ec l a b => mkGlob3 hetmet_pga_swap (fun ec a b => ga_type' ec _ _) ec (gat a) (gat b)
- ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat a)
- ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat a)
- ; ga_first := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat a) (gat b) (gat x))
- ; ga_second := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat a) (gat b) (gat x))
- ; ga_comp := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat a) (gat b) (gat c))
+ { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat ec a)
+ ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat ec a)
+ ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat ec a)
+ ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat ec a)
+ ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat ec a)
+ ; ga_assoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc (fun ec a b c => ga_type' ec _ _) ec (gat ec a) (gat ec b) (gat ec c)
+ ; ga_unassoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc (fun ec a b c => ga_type' ec _ _) ec (gat ec a) (gat ec b) (gat ec c)
+ ; ga_swap := fun Γ Δ ec l a b => mkGlob3 hetmet_pga_swap (fun ec a b => ga_type' ec _ _) ec (gat ec a) (gat ec b)
+ ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat ec a)
+ ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat ec a)
+ ; 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))*)
Definition hetmet_unflatten' := coreVarToWeakExprVarOrError hetmet_unflatten.
Definition hetmet_flattened_id' := coreVarToWeakExprVarOrError hetmet_flattened_id.
- Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
- addErrorMessage ("input CoreSyn: " +++ toString ce)
- (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
- coreExprToWeakExpr ce >>= fun we =>
+ Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
+ addErrorMessage ("input CoreSyn: " +++ toString cex)
+ (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr cex)) (
+ coreExprToWeakExpr cex >>= fun we =>
addErrorMessage ("WeakExpr: " +++ toString we)
((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
((weakTypeOfWeakExpr we) >>= fun t =>
((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
(addErrorMessage ("HaskStrong...")
- (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 _ _ _ _ (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
End coqPassCoreToCore.
Definition coqPassCoreToCore
+ (do_flatten : bool)
+ (do_skolemize : bool)
(hetmet_brak : CoreVar)
(hetmet_esc : CoreVar)
(hetmet_flatten : CoreVar)
(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_curryl : CoreVar)
(hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=
coqPassCoreToCore'
+ do_flatten
+ do_skolemize
hetmet_brak
hetmet_esc
hetmet_flatten
hetmet_flattened_id
uniqueSupply
hetmet_PGArrowTyCon
+ hetmet_PGArrow_unit_TyCon
+ hetmet_PGArrow_tensor_TyCon
+(* hetmet_PGArrow_exponent_TyCon*)
hetmet_pga_id
hetmet_pga_comp
hetmet_pga_first
hetmet_pga_applyr
hetmet_pga_curryl
*)
+
.
End core2proof.
projects / coq-hetmet.git / blobdiff