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 (uniqueSupply : UniqSupply).
+ Context (hetmet_brak : WeakExprVar).
+ Context (hetmet_esc : WeakExprVar).
+ Context (hetmet_flatten : WeakExprVar).
+ Context (hetmet_flattened_id : WeakExprVar).
+ Context (uniqueSupply : UniqSupply).
Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
match ut with
Context
(hetmet_brak : CoreVar)
(hetmet_esc : CoreVar)
+ (hetmet_flatten : CoreVar)
+ (hetmet_flattened_id : CoreVar)
(uniqueSupply : UniqSupply)
(lbinds:list (@CoreBind CoreVar))
(hetmet_PGArrowTyCon : TyFun)
Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
+ Definition hetmet_flatten' := coreVarToWeakExprVarOrError hetmet_flatten.
+ Definition hetmet_flattened_id' := coreVarToWeakExprVarOrError hetmet_flattened_id.
Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
addErrorMessage ("input CoreSyn: " +++ toString ce)
((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
(addErrorMessage ("HaskStrong...")
- (let haskProof := flatten_proof my_ga (@expr2proof _ _ _ _ _ _ e)
+ (let haskProof := flatten_proof hetmet_flatten' 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
+ strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
(projT2 e'') INil
>>= fun q =>
OK (weakExprToCoreExpr q)
Definition coqPassCoreToCore
(hetmet_brak : CoreVar)
(hetmet_esc : CoreVar)
+ (hetmet_flatten : CoreVar)
+ (hetmet_flattened_id : CoreVar)
(uniqueSupply : UniqSupply)
(lbinds:list (@CoreBind CoreVar))
(hetmet_PGArrowTyCon : TyFun)
coqPassCoreToCore'
hetmet_brak
hetmet_esc
+ hetmet_flatten
+ hetmet_flattened_id
uniqueSupply
hetmet_PGArrowTyCon
hetmet_pga_id
Require Import HaskKinds.
Require Import HaskCoreTypes.
+Require Import HaskCoreVars.
+Require Import HaskWeakTypes.
+Require Import HaskWeakVars.
Require Import HaskLiteralsAndTyCons.
Require Import HaskStrongTypes.
Require Import HaskProof.
Require Import HaskProof.
Require Import HaskStrongToProof.
Require Import HaskProofToStrong.
+Require Import HaskWeakToStrong.
Open Scope nd_scope.
Set Printing Width 130.
+ Context (hetmet_flatten : WeakExprVar).
+ Context (hetmet_id : WeakExprVar).
Context {unitTy : forall TV, RawHaskType TV ★ }.
Context {prodTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
simpl.
rename l into g.
rename σ into l.
- destruct l as [|ec lev]; simpl; [ apply nd_rule; rewrite globals_do_not_have_code_types; apply RGlobal; auto | idtac ].
+ destruct l as [|ec lev]; simpl.
+ destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
+ set (garrowfy_code_types (g wev)) as t.
+ set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
+ simpl in q.
+ apply nd_rule.
+ apply q.
+ apply INil.
+ apply nd_rule; rewrite globals_do_not_have_code_types.
+ apply RGlobal.
apply (Prelude_error "found RGlobal at depth >0").
destruct case_RLam.