- 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.
-
- 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) :=
+
+Inductive VarNameStore :=
+ varNameStore : nat -> nat -> nat -> VarNameStore.
+Inductive VarNameStoreM {T} :=
+ varNameStoreM : (VarNameStore -> (T * VarNameStore)) -> VarNameStoreM.
+Implicit Arguments VarNameStoreM [ ].
+
+Open Scope nat_scope.
+Instance VarNameMonad : Monad VarNameStoreM :=
+{ returnM := fun _ x => varNameStoreM (fun v => (x,v))
+; bindM := fun _ _ x f =>
+ match x with
+ varNameStoreM xf =>
+ varNameStoreM (fun vns =>
+ match xf vns with
+ (x',vns') => match f x' with
+ varNameStoreM fx' => fx' vns'
+ end
+ end) end }.
+
+Definition freshTyVarName : Kind -> VarNameStoreM LatexMath :=
+ fun κ => varNameStoreM (fun vns =>
+ match vns with
+ varNameStore n1 n2 n3 =>
+ let name := (rawLatexMath "\alpha_{")+++toLatexMath (toString n1)+++(rawLatexMath "}")
+ in (name,(varNameStore (S n1) n2 n3))
+ end).
+Definition freshCoVarName : VarNameStoreM LatexMath :=
+ varNameStoreM (fun vns =>
+ match vns with
+ varNameStore n1 n2 n3 =>
+ let name := (rawLatexMath "\gamma_{")+++toLatexMath (toString n2)+++(rawLatexMath "}")
+ in (name,(varNameStore n1 (S n2) n3))
+ end).
+Definition freshValVarName : VarNameStoreM LatexMath :=
+ varNameStoreM (fun vns =>
+ match vns with
+ varNameStore n1 n2 n3 =>
+ let vn := match n3 with
+ | 0 => "x"
+ | 1 => "y"
+ | 2 => "z"
+ | 3 => "a"
+ | 4 => "b"
+ | 5 => "c"
+ | 6 => "d"
+ | 7 => "e"
+ | 8 => "f"
+ | 9 => "g"
+ | 10 => "h"
+ | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++toString x+++"}"
+ end
+ in let name := rawLatexMath ("x_{"+++vn+++"}")
+ in (name,(varNameStore n1 n2 (S n3)))
+ end).
+
+Fixpoint typeToLatexMath (needparens:bool){κ}(t:RawHaskType (fun _ => LatexMath) κ) {struct t} : VarNameStoreM LatexMath :=
+ match t return VarNameStoreM LatexMath with
+ | TVar _ v => return toLatexMath v
+ | TCon tc => return ((rawLatexMath "\text{\tt{")+++toLatexMath (toString tc)+++(rawLatexMath "}}"))
+ | TArrow => return rawLatexMath "\text{\tt{(->)}}"
+ | TCoerc _ t1 t2 t => bind t1' = typeToLatexMath false t1
+ ; bind t2' = typeToLatexMath false t2
+ ; bind t' = typeToLatexMath needparens t
+ ; return ((rawLatexMath "{(")+++t1'+++(rawLatexMath "{\sim}")+++
+ t2'+++(rawLatexMath ")}\Rightarrow{")+++t'+++(rawLatexMath "}"))
+ | TCode ec t => bind ec' = typeToLatexMath true ec
+ ; bind t' = typeToLatexMath false t
+ ; return (rawLatexMath "\code{")+++ec'+++(rawLatexMath "}{")+++t'+++(rawLatexMath "}")
+ | TAll k f => bind alpha = freshTyVarName k
+ ; bind t' = typeToLatexMath false (f alpha)
+ ; return (rawLatexMath "(\forall ")+++alpha+++(rawLatexMath "{:}")+++
+ (kindToLatexMath k)+++(rawLatexMath ")")+++t'
+ | TApp _ _ t1 t2 => match t1 return VarNameStoreM LatexMath with
+ | TApp _ _ TArrow tx => bind t1' = typeToLatexMath true tx
+ ; bind t2' = typeToLatexMath true t2
+ ; let body := t1'+++(rawLatexMath "{\rightarrow}")+++t2'
+ in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
+ | _ => bind t1' = typeToLatexMath true t1
+ ; bind t2' = typeToLatexMath true t2
+ ; let body := t1'+++(rawLatexMath " ")+++t2'
+ in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
+ end
+ | TyFunApp tfc lt => bind rest = typeListToRawLatexMath false lt
+ ; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++
+ (rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++
+ (rawLatexMath "}")+++
+ (fold_left (fun x y => (rawLatexMath " \ ")+++x+++y)
+ rest (rawLatexMath ""))
+end
+with typeListToRawLatexMath (needparens:bool){κ}(t:RawHaskTypeList κ) {struct t} : VarNameStoreM (list LatexMath) :=
+match t return VarNameStoreM (list LatexMath) with
+| TyFunApp_nil => return nil
+| TyFunApp_cons κ kl rhk rhkl => bind r = typeToLatexMath needparens rhk
+ ; bind rl = typeListToRawLatexMath needparens rhkl
+ ; return (r::rl)
+end.
+
+Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameStoreM LatexMath.
+ refine (