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.
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).
| 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) :=