+Section HaskProofToLatex.
+
+ Context {TV:Kind -> Type}.
+ Context {TVLatex:forall k, ToLatex (TV k)}.
+ Context {freshM:FreshMonad (∀ κ, TV κ)}.
+ Definition FreshM' := FMT freshM.
+ Instance FreshMon' : Monad FreshM' := FMT_Monad freshM.
+
+ Instance ToLatexTyCon : ToLatex TyCon.
+ admit.
+ Defined.
+
+ Fixpoint typeToLatex (needparens:bool){κ}(t:RawHaskType TV κ) {struct t} : FMT freshM Latex :=
+ match t with
+ | TVar _ v => return toLatex v
+ | TCon tc => return (latex "\text{\tt{")+=+tc+=+(latex "}}")
+ | TArrow => return latex "\text{\tt{(->)}}"
+ | TCoerc _ t1 t2 t => bind t1' = typeToLatex false t1
+ ; bind t2' = typeToLatex false t2
+ ; bind t' = typeToLatex needparens t
+ ; return (latex "{(")+=+t1'+=+(latex "{\sim}")+=+
+ t2'+=+(latex ")}\Rightarrow{")+=+t'+=+(latex "}")
+ | TApp _ _ t1 t2 => match t1 with
+ | TApp _ _ TArrow tx => bind t1' = typeToLatex true tx
+ ; bind t2' = typeToLatex true t2
+ ; let body := t1'+=+(latex "{\rightarrow}")+=+t2'
+ in return if needparens then (latex "(")+=+body+=+(latex ")") else body
+ | _ => bind t1' = typeToLatex true t1
+ ; bind t2' = typeToLatex true t2
+ ; let body := t1'+=+(latex " ")+=+t2'
+ in return if needparens then (latex "(")+=+body+=+(latex ")") else body
+ end
+ | TCode ec t => bind ec' = typeToLatex true ec
+ ; bind t' = typeToLatex false t
+ ; return (latex "\code{")+=+ec'+=+(latex "}{")+=+t'+=+(latex "}")
+ | TyFunApp tfc lt => bind rest = typeListToLatex false lt
+ ; return (latex "{\text{\tt{")+=+(sanitizeForLatex (toString tfc))+=+(latex "}}}")+=+
+ (*(latex "_{")+=+(latex (toString (tfc:nat)))+=+(latex "}")+=+*)
+ (fold_left (fun x y => (latex " \ ")+=+x+=+y)
+ rest (latex ""))
+ | TAll k f => (*bind alpha = next
+ ; bind t' = typeToLatex false (f (alpha k))
+ ; *)return (latex "(\forall ")(*+=+(@toLatex _ (TVLatex k) (alpha k))*)
+ +=+(latex "{:}")+=+(kindToLatex k)+=+(latex ")")(*+=+t'*)
+ end
+ with typeListToLatex (needparens:bool){κ}(t:RawHaskTypeList κ) {struct t} : FreshM' (list Latex) :=
+ match t with
+ | TyFunApp_nil => return nil
+ | TyFunApp_cons κ kl rhk rhkl => bind r = typeToLatex needparens rhk
+ ; bind rl = typeListToLatex needparens rhkl
+ ; return (r::rl)
+ end.
+(*
+ Definition ltypeToLatex {Γ:TypeEnv}{κ}(t:RawHaskType TV κ)(lev:list nat) : FreshM' Latex :=
+ match lev with
+ | nil => typeToLatex false t
+ | lv => bind t' = typeToLatex true t
+ ;
+ (latex "{")
+ +=+
+
+ +=+
+ (latex "}^{")
+ +=+
+ (fold_left (fun x y => x+=+":"+=+y) (map tyvar2greek lv) "")+=+"}"