+ Definition idproof1 : ND Rule [] [nil > nil > [TInt @@ nil] |- [TInt @@ nil]].
+ apply nd_rule.
+ apply RVar.
+ Defined.
+
+ Definition idtype :=
+ HaskTAll(Γ:=nil) ★ (fun TV ite tv => (TApp (TApp TArrow (TVar tv)) (TVar tv))).
+
+ Definition idproof : ND Rule [] [nil > nil > [] |- [idtype @@ nil]].
+ eapply nd_comp; [ idtac | eapply nd_rule ; eapply RAbsT ].
+ apply idproof0.
+ Defined.
+*)
+(*
+ Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
+ addErrorMessage ("input CoreSyn: " +++ ce)
+ (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
+ coreExprToWeakExpr ce >>= fun we =>
+ addErrorMessage ("WeakExpr: " +++ we)
+ ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
+ ((weakTypeOfWeakExpr we) >>= fun t =>
+ (addErrorMessage ("WeakType: " +++ t)
+ ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
+ addErrorMessage ("HaskType: " +++ τ)
+ ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
+ (let haskProof := @expr2proof _ _ _ _ _ _ e
+ in (* insert HaskProof-to-HaskProof manipulations here *)
+ (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof))
+ >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e'))
+(*
+ >>= fun e' =>
+ Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e'))
+ *)
+)
+)))))))).
+(* Error "X").*)
+(*
+ strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
+ (projT2 e')
+ INil
+ >>= fun q => Error (toString q)
+ ))))))))).
+*)
+*)
+
+ Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
+ addErrorMessage ("input CoreSyn: " +++ ce)
+ (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
+ coreExprToWeakExpr ce >>= fun we =>
+ addErrorMessage ("WeakExpr: " +++ we)
+ ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
+ ((weakTypeOfWeakExpr we) >>= fun t =>
+ (addErrorMessage ("WeakType: " +++ t)
+ ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
+
+ ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
+
+ (addErrorMessage ("HaskStrong...")
+ (let haskProof := @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 coqPassCoreToCore
+ (hetmet_brak : CoreVar)
+ (hetmet_esc : CoreVar)
+ (uniqueSupply : UniqSupply)
+ (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) :=
+ match coreVarToWeakVar hetmet_brak with
+ | WExprVar hetmet_brak' => match coreVarToWeakVar hetmet_esc with
+ | WExprVar hetmet_esc' => coqPassCoreToCore' hetmet_brak' hetmet_esc' uniqueSupply lbinds
+ | _ => Prelude_error "IMPOSSIBLE"
+ end
+ | _ => Prelude_error "IMPOSSIBLE"
+ end.
+
+End core2proof.
+(*Set Extraction Optimize.*)
+(*Set Extraction AutoInline.*)