+Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
+Variable mkSystemName : Unique -> string -> nat -> Name.
+ Extract Inlined Constant mkSystemName =>
+ "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
+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))".
+Variable mkExVar : Name -> CoreType -> CoreVar.
+ Extract Inlined Constant mkExVar => "Id.mkLocalId".
+
+Section core2proof.
+ Context (ce:@CoreExpr CoreVar).
+
+ Definition Γ : TypeEnv := nil.
+
+ Definition Δ : CoercionEnv Γ := nil.
+
+ Definition φ : TyVarResolver Γ :=
+ fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)).
+ (*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
+
+ Definition ψ : CoVarResolver Γ Δ :=
+ fun cv => Error ("tried to get the representative of an unbound covar!" (*+++ (getTypeVarOccString cv)*)).
+
+ (* 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
+ | Error s => Prelude_error ("Error in top-level xi: " +++ 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"
+ end.
+
+
+ (* core-to-string (-dcoqpass) *)
+
+ Definition header : string :=
+ "\documentclass[9pt]{article}"+++eol+++
+ "\usepackage{amsmath}"+++eol+++
+ "\usepackage{amssymb}"+++eol+++
+ "\usepackage{proof}"+++eol+++
+ "\usepackage{mathpartir} % http://cristal.inria.fr/~remy/latex/"+++eol+++
+ "\usepackage{trfrac} % http://www.utdallas.edu/~hamlen/trfrac.sty"+++eol+++
+ "\def\code#1#2{\Box_{#1} #2}"+++eol+++
+ "\usepackage[paperwidth=200in,centering]{geometry}"+++eol+++
+ "\usepackage[displaymath,tightpage,active]{preview}"+++eol+++
+ "\begin{document}"+++eol+++
+ "\begin{preview}"+++eol.
+
+ Definition footer : string :=
+ eol+++"\end{preview}"+++
+ eol+++"\end{document}"+++
+ eol.
+
+
+ Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
+ 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 =>
+ OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)
+ )))))))).
+
+ Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
+ match coreToStringExpr' ce with
+ | OK x => x
+ | Error s => Prelude_error s
+ end.
+
+ Definition coreToStringBind (binds:@CoreBind CoreVar) : string :=
+ match binds with
+ | CoreNonRec _ e => coreToStringExpr e
+ | CoreRec lbe => fold_left (fun x y => x+++eol+++eol+++y) (map (fun x => coreToStringExpr (snd x)) lbe) ""
+ end.
+
+ Definition coqPassCoreToString (lbinds:list (@CoreBind CoreVar)) : string :=
+ header +++
+ (fold_left (fun x y => x+++eol+++eol+++y) (map coreToStringBind lbinds) "")
+ +++ footer.
+
+
+ (* core-to-core (-fcoqpass) *)
+ Section CoreToCore.
+
+ 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.
+ 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).
+
+ Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
+ match ut with
+ uniqM f =>
+ f uniqueSupply >>= fun x => OK (snd x)
+ end.
+
+ Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
+ intros.
+ induction ln.
+ exists O.
+ intros.
+ inversion H.
+ destruct IHln as [n pf].
+ exists (plus (S n) a).
+ intros.
+ destruct H.
+ omega.
+ fold (@In _ n' ln) in H.
+ set (pf n' H) as q.
+ omega.
+ Defined.
+
+ Definition FreshNat : @FreshMonad nat.
+ refine {| FMT := fun T => nat -> prod nat T
+ ; FMT_fresh := _
+ |}.
+ Focus 2.
+ intros.
+ refine ((S H),_).
+ set (larger tl) as q.
+ destruct q as [n' pf].
+ exists n'.
+ intros.
+ set (pf _ H0) as qq.
+ omega.
+
+ refine {| returnM := fun a (v:a) => _ |}.
+ intro n. exact (n,v).
+ intros.
+ set (X H) as q.
+ destruct q as [n' v].
+ set (X0 v n') as q'.
+ exact q'.
+ Defined.
+
+ Definition unFresh {T} : @FreshM _ FreshNat T -> T.
+ intros.
+ destruct X.
+ exact O.
+ apply t.
+ Defined.
+
+ Definition env := ★::nil.
+ Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
+ Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
+ eapply nd_comp.
+ eapply nd_comp.
+ eapply nd_rule.
+ apply RVar.
+ eapply nd_rule.
+ eapply (RURule _ _ _ _ (RuCanL _ _)) .
+ eapply nd_rule.
+ eapply RLam.
+ Defined.