1 (*********************************************************************************************************************************)
2 (* HaskProofToLatex: render HaskProof's as LaTeX code using trfrac.sty *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import NaturalDeduction.
9 Require Import Coq.Strings.String.
10 Require Import Coq.Lists.List.
11 Require Import HaskKinds.
12 Require Import HaskWeakVars.
13 Require Import HaskWeakTypes.
14 Require Import HaskLiteralsAndTyCons.
15 Require Import HaskStrongTypes.
16 Require Import HaskStrong.
17 Require Import HaskProof.
18 Require Import HaskCoreTypes.
22 Inductive VarNameStore :=
23 varNameStore : nat -> nat -> nat -> VarNameStore.
24 Inductive VarNameStoreM {T} :=
25 varNameStoreM : (VarNameStore -> (T * VarNameStore)) -> VarNameStoreM.
26 Implicit Arguments VarNameStoreM [ ].
29 Instance VarNameMonad : Monad VarNameStoreM :=
30 { returnM := fun _ x => varNameStoreM (fun v => (x,v))
31 ; bindM := fun _ _ x f =>
34 varNameStoreM (fun vns =>
36 (x',vns') => match f x' with
37 varNameStoreM fx' => fx' vns'
41 Definition freshTyVarName : Kind -> VarNameStoreM LatexMath :=
42 fun κ => varNameStoreM (fun vns =>
44 varNameStore n1 n2 n3 =>
45 let name := (rawLatexMath "\alpha_{")+++toLatexMath (toString n1)+++(rawLatexMath "}")
46 in (name,(varNameStore (S n1) n2 n3))
48 Definition freshCoVarName : VarNameStoreM LatexMath :=
49 varNameStoreM (fun vns =>
51 varNameStore n1 n2 n3 =>
52 let name := (rawLatexMath "\gamma_{")+++toLatexMath (toString n2)+++(rawLatexMath "}")
53 in (name,(varNameStore n1 (S n2) n3))
55 Definition freshValVarName : VarNameStoreM LatexMath :=
56 varNameStoreM (fun vns =>
58 varNameStore n1 n2 n3 =>
59 let vn := match n3 with
71 | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++toString x+++"}"
73 in let name := rawLatexMath ("x_{"+++vn+++"}")
74 in (name,(varNameStore n1 n2 (S n3)))
77 Fixpoint typeToLatexMath (needparens:bool){κ}(t:RawHaskType (fun _ => LatexMath) κ) {struct t} : VarNameStoreM LatexMath :=
78 match t return VarNameStoreM LatexMath with
79 | TVar _ v => return toLatexMath v
80 | TCon tc => return ((rawLatexMath "\text{\tt{")+++toLatexMath (toString tc)+++(rawLatexMath "}}"))
81 | TArrow => return rawLatexMath "\text{\tt{(->)}}"
82 | TCoerc _ t1 t2 t => bind t1' = typeToLatexMath false t1
83 ; bind t2' = typeToLatexMath false t2
84 ; bind t' = typeToLatexMath needparens t
85 ; return ((rawLatexMath "{(")+++t1'+++(rawLatexMath "{\sim}")+++
86 t2'+++(rawLatexMath ")}\Rightarrow{")+++t'+++(rawLatexMath "}"))
87 | TCode ec t => bind ec' = typeToLatexMath true ec
88 ; bind t' = typeToLatexMath false t
89 ; return (rawLatexMath "\code{")+++ec'+++(rawLatexMath "}{")+++t'+++(rawLatexMath "}")
90 | TAll k f => bind alpha = freshTyVarName k
91 ; bind t' = typeToLatexMath false (f alpha)
92 ; return (rawLatexMath "(\forall ")+++alpha+++(rawLatexMath "{:}")+++
93 (kindToLatexMath k)+++(rawLatexMath ")")+++t'
94 | TApp _ _ t1 t2 => match t1 return VarNameStoreM LatexMath with
95 | TApp _ _ TArrow tx => bind t1' = typeToLatexMath true tx
96 ; bind t2' = typeToLatexMath true t2
97 ; let body := t1'+++(rawLatexMath "{\rightarrow}")+++t2'
98 in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
99 | _ => bind t1' = typeToLatexMath true t1
100 ; bind t2' = typeToLatexMath true t2
101 ; let body := t1'+++(rawLatexMath " ")+++t2'
102 in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
104 | TyFunApp tfc lt => bind rest = typeListToRawLatexMath false lt
105 ; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++
106 (rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++
107 (rawLatexMath "}")+++
108 (fold_left (fun x y => (rawLatexMath " \ ")+++x+++y)
109 rest (rawLatexMath ""))
111 with typeListToRawLatexMath (needparens:bool){κ}(t:RawHaskTypeList κ) {struct t} : VarNameStoreM (list LatexMath) :=
112 match t return VarNameStoreM (list LatexMath) with
113 | TyFunApp_nil => return nil
114 | TyFunApp_cons κ kl rhk rhkl => bind r = typeToLatexMath needparens rhk
115 ; bind rl = typeListToRawLatexMath needparens rhkl
119 Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameStoreM LatexMath.
124 bind t'' = typeToLatexMath false (t' (fun _ => LatexMath) ite) ;
125 return match lev with
127 | lv => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++
128 (fold_left (fun x y => x+++(rawLatexMath ":")+++y)
129 (map (fun l:HaskTyVar Γ ★ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
131 end); try apply ConcatenableLatexMath.
132 try apply VarNameMonad.
136 refine (bind tv' = freshTyVarName a ; _).
138 refine (bind IHΓ' = IHΓ ; return _).
146 Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
147 match match j return VarNameStoreM LatexMath with
148 | mkJudg Γ Δ Σ₁ Σ₂ =>
149 bind Σ₁' = treeM (mapOptionTree ltypeToLatexMath Σ₁)
150 ; bind Σ₂' = treeM (mapOptionTree ltypeToLatexMath Σ₂)
151 ; return treeToLatexMath Σ₁' +++ (rawLatexMath "\vdash") +++ treeToLatexMath Σ₂'
153 varNameStoreM f => fst (f (varNameStore 0 0 0))
156 Instance ToLatexMathJudgment : ToLatexMath Judg :=
157 { toLatexMath := judgmentToRawLatexMath }.
159 Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
161 | RLeft _ _ _ r => nd_uruleToRawLatexMath r
162 | RRight _ _ _ r => nd_uruleToRawLatexMath r
165 | RuCanL _ => "uCanL"
166 | RuCanR _ => "uCanR"
167 | RAssoc _ _ _ => "Assoc"
168 | RCossa _ _ _ => "Cossa"
169 | RExch _ _ => "Exch"
172 | RComp _ _ _ _ _ => "Comp" (* FIXME: do a better job here *)
175 Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
177 | RArrange _ _ _ _ _ r => nd_uruleToRawLatexMath r
178 | RNote _ _ _ _ _ _ => "Note"
179 | RLit _ _ _ _ => "Lit"
180 | RVar _ _ _ _ => "Var"
181 | RGlobal _ _ _ _ _ => "Global"
182 | RLam _ _ _ _ _ _ => "Abs"
183 | RCast _ _ _ _ _ _ _ => "Cast"
184 | RAbsT _ _ _ _ _ _ => "AbsT"
185 | RAppT _ _ _ _ _ _ _ => "AppT"
186 | RAppCo _ _ _ _ _ _ _ _ _ => "AppCo"
187 | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
188 | RApp _ _ _ _ _ _ _ => "App"
189 | RLet _ _ _ _ _ _ _ => "Let"
190 | RJoin _ _ _ _ _ _ => "RJoin"
191 | RLetRec _ _ _ _ _ _ => "LetRec"
192 | RCase _ _ _ _ _ _ _ _ => "Case"
193 | RBrak _ _ _ _ _ _ => "Brak"
194 | REsc _ _ _ _ _ _ => "Esc"
195 | RVoid _ _ => "RVoid"
198 Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
200 | RLeft _ _ _ r => nd_hideURule r
201 | RRight _ _ _ r => nd_hideURule r
206 | RAssoc _ _ _ => true
207 | RCossa _ _ _ => true
208 | RExch (T_Leaf None) b => true
209 | RExch a (T_Leaf None) => true
210 | RWeak (T_Leaf None) => true
211 | RCont (T_Leaf None) => true
212 | RComp _ _ _ _ _ => false (* FIXME: do better *)
215 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
217 | RArrange _ _ _ _ _ r => nd_hideURule r
219 | RJoin _ _ _ _ _ _ => true
223 Instance ToLatexMathRule h c : ToLatexMath (Rule h c) :=
224 { toLatexMath := fun r => rawLatexMath (@nd_ruleToRawLatexMath h c r) }.
226 Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) :=
227 @SIND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
228 (mkSIND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).