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
exact O.
apply t.
Defined.
-(*
- Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
- addErrorMessage ("input CoreSyn: " +++ toString ce)
- (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
- coreExprToWeakExpr ce >>= fun we =>
- addErrorMessage ("WeakExpr: " +++ toString we)
- ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
- ((weakTypeOfWeakExpr we) >>= fun t =>
- (addErrorMessage ("WeakType: " +++ toString t)
- ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
-
- ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
-
- (addErrorMessage ("HaskStrong...")
- (let haskProof := (*flatten_proof'*) (@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)
- )))))))))).
-
- Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
- match coreToCoreExpr' ce with
- | OK x => x
- | Error s => Prelude_error s
- end.
-
- Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
- match binds with
- | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
- | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
- end.
-
- Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
- map coreToCoreBind lbinds.
- *)
End CoreToCore.
Context
(hetmet_brak : CoreVar)
(hetmet_esc : CoreVar)
+ (hetmet_flatten : CoreVar)
+ (hetmet_flattened_id : CoreVar)
(uniqueSupply : UniqSupply)
(lbinds:list (@CoreBind CoreVar))
(hetmet_PGArrowTyCon : TyFun)
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_type {TV}(a b c:RawHaskType TV ★) : RawHaskType TV ★ :=
+ 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 b c:HaskType Γ ★) : HaskType Γ ★ :=
+ Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
fun TV ite => TApp (TApp (TApp (@TyFunApp TV
hetmet_PGArrowTyCon
nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).
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)
| OK x => x
| Error s => Prelude_error s
end.
-
+
Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar :=
match binds with
- | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e)
+ | CoreNonRec v e => let e' := coreToCoreExpr e in CoreNonRec (setVarType v (coreTypeOfCoreExpr e')) e'
+
| CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe)
+ (* FIXME: doesn't deal with the case where top level recursive binds change type *)
+(*
+ match coreToCoreExpr (CoreELet lbe) (CoreELit HaskMachNullAddr) with
+ | CoreELet (CoreRec lbe') => lbe'
+ | x => Prelude_error
+ ("coreToCoreExpr was given a letrec, " +++
+ "but returned something that wasn't a letrec: " +++ toString x)
+ end
+*)
end.
Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
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
projects / coq-hetmet.git / blobdiff