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 NaturalDeductionToLatex.
10 Require Import Coq.Strings.String.
11 Require Import Coq.Lists.List.
12 Require Import HaskKinds.
13 Require Import HaskWeakVars.
14 Require Import HaskWeakTypes.
15 Require Import HaskLiteralsAndTyCons.
16 Require Import HaskStrongTypes.
17 Require Import HaskStrong.
18 Require Import HaskProof.
19 Require Import HaskCoreTypes.
23 Inductive VarNameStore :=
24 varNameStore : nat -> nat -> nat -> VarNameStore.
25 Inductive VarNameStoreM {T} :=
26 varNameStoreM : (VarNameStore -> (T * VarNameStore)) -> VarNameStoreM.
27 Implicit Arguments VarNameStoreM [ ].
30 Instance VarNameMonad : Monad VarNameStoreM :=
31 { returnM := fun _ x => varNameStoreM (fun v => (x,v))
32 ; bindM := fun _ _ x f =>
35 varNameStoreM (fun vns =>
37 (x',vns') => match f x' with
38 varNameStoreM fx' => fx' vns'
42 Definition freshTyVarName : Kind -> VarNameStoreM LatexMath :=
43 fun κ => varNameStoreM (fun vns =>
45 varNameStore n1 n2 n3 =>
46 let name := (rawLatexMath "\alpha_{")+++toLatexMath (toString n1)+++(rawLatexMath "}")
47 in (name,(varNameStore (S n1) n2 n3))
49 Definition freshCoVarName : VarNameStoreM LatexMath :=
50 varNameStoreM (fun vns =>
52 varNameStore n1 n2 n3 =>
53 let name := (rawLatexMath "\gamma_{")+++toLatexMath (toString n2)+++(rawLatexMath "}")
54 in (name,(varNameStore n1 (S n2) n3))
56 Definition freshValVarName : VarNameStoreM LatexMath :=
57 varNameStoreM (fun vns =>
59 varNameStore n1 n2 n3 =>
60 let vn := match n3 with
72 | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++toString x+++"}"
74 in let name := rawLatexMath ("x_{"+++vn+++"}")
75 in (name,(varNameStore n1 n2 (S n3)))
78 Fixpoint typeToLatexMath (needparens:bool){κ}(t:RawHaskType (fun _ => LatexMath) κ) {struct t} : VarNameStoreM LatexMath :=
79 match t return VarNameStoreM LatexMath with
80 | TVar _ v => return toLatexMath v
81 | TCon tc => return ((rawLatexMath "\text{\tt{")+++toLatexMath (toString tc)+++(rawLatexMath "}}"))
82 | TArrow => return rawLatexMath "\text{\tt{(->)}}"
83 | TCoerc _ t1 t2 t => bind t1' = typeToLatexMath false t1
84 ; bind t2' = typeToLatexMath false t2
85 ; bind t' = typeToLatexMath needparens t
86 ; return ((rawLatexMath "{(")+++t1'+++(rawLatexMath "{\sim}")+++
87 t2'+++(rawLatexMath ")}\Rightarrow{")+++t'+++(rawLatexMath "}"))
88 | TCode ec t => bind ec' = typeToLatexMath true ec
89 ; bind t' = typeToLatexMath false t
90 ; return (rawLatexMath "\code{")+++ec'+++(rawLatexMath "}{")+++t'+++(rawLatexMath "}")
91 | TAll k f => bind alpha = freshTyVarName k
92 ; bind t' = typeToLatexMath false (f alpha)
93 ; return (rawLatexMath "(\forall ")+++alpha+++(rawLatexMath "{:}")+++
94 (kindToLatexMath k)+++(rawLatexMath ")")+++t'
95 | TApp _ _ t1 t2 => match t1 return VarNameStoreM LatexMath with
96 | TApp _ _ TArrow tx => bind t1' = typeToLatexMath true tx
97 ; bind t2' = typeToLatexMath true t2
98 ; let body := t1'+++(rawLatexMath "{\rightarrow}")+++t2'
99 in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
100 | _ => bind t1' = typeToLatexMath true t1
101 ; bind t2' = typeToLatexMath true t2
102 ; let body := t1'+++(rawLatexMath " ")+++t2'
103 in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
105 | TyFunApp tfc lt => bind rest = typeListToRawLatexMath false lt
106 ; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++
107 (rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++
108 (rawLatexMath "}")+++
109 (fold_left (fun x y => (rawLatexMath " \ ")+++x+++y)
110 rest (rawLatexMath ""))
112 with typeListToRawLatexMath (needparens:bool){κ}(t:RawHaskTypeList κ) {struct t} : VarNameStoreM (list LatexMath) :=
113 match t return VarNameStoreM (list LatexMath) with
114 | TyFunApp_nil => return nil
115 | TyFunApp_cons κ kl rhk rhkl => bind r = typeToLatexMath needparens rhk
116 ; bind rl = typeListToRawLatexMath needparens rhkl
120 Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameStoreM LatexMath.
125 bind t'' = typeToLatexMath false (t' (fun _ => LatexMath) ite) ;
126 return match lev with
128 | lv => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++
129 (fold_left (fun x y => x+++(rawLatexMath ":")+++y)
130 (map (fun l:HaskTyVar Γ ★ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
132 end); try apply ConcatenableLatexMath.
133 try apply VarNameMonad.
137 refine (bind tv' = freshTyVarName a ; _).
139 refine (bind IHΓ' = IHΓ ; return _).
147 Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
148 match match j return VarNameStoreM LatexMath with
149 | mkJudg Γ Δ Σ₁ Σ₂ =>
150 bind Σ₁' = treeM (mapOptionTree ltypeToLatexMath Σ₁)
151 ; bind Σ₂' = treeM (mapOptionTree ltypeToLatexMath Σ₂)
152 ; return treeToLatexMath Σ₁' +++ (rawLatexMath "\vdash") +++ treeToLatexMath Σ₂'
154 varNameStoreM f => fst (f (varNameStore 0 0 0))
157 Instance ToLatexMathJudgment : ToLatexMath Judg :=
158 { toLatexMath := judgmentToRawLatexMath }.
160 Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
162 | RLeft _ _ _ r => nd_uruleToRawLatexMath r
163 | RRight _ _ _ r => nd_uruleToRawLatexMath r
166 | RuCanL _ => "uCanL"
167 | RuCanR _ => "uCanR"
168 | RAssoc _ _ _ => "Assoc"
169 | RCossa _ _ _ => "Cossa"
170 | RExch _ _ => "Exch"
173 | RComp _ _ _ _ _ => "Comp" (* FIXME: do a better job here *)
176 Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
178 | RArrange _ _ _ _ _ r => nd_uruleToRawLatexMath r
179 | RNote _ _ _ _ _ _ => "Note"
180 | RLit _ _ _ _ => "Lit"
181 | RVar _ _ _ _ => "Var"
182 | RGlobal _ _ _ _ _ => "Global"
183 | RLam _ _ _ _ _ _ => "Abs"
184 | RCast _ _ _ _ _ _ _ => "Cast"
185 | RAbsT _ _ _ _ _ _ => "AbsT"
186 | RAppT _ _ _ _ _ _ _ => "AppT"
187 | RAppCo _ _ _ _ _ _ _ _ _ => "AppCo"
188 | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
189 | RApp _ _ _ _ _ _ _ => "App"
190 | RLet _ _ _ _ _ _ _ => "Let"
191 | RBindingGroup _ _ _ _ _ _ => "RBindingGroup"
192 | RLetRec _ _ _ _ _ _ => "LetRec"
193 | RCase _ _ _ _ _ _ _ _ => "Case"
194 | RBrak _ _ _ _ _ _ => "Brak"
195 | REsc _ _ _ _ _ _ => "Esc"
196 | REmptyGroup _ _ => "REmptyGroup"
199 Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
201 | RLeft _ _ _ r => nd_hideURule r
202 | RRight _ _ _ r => nd_hideURule r
207 | RAssoc _ _ _ => true
208 | RCossa _ _ _ => true
209 | RExch (T_Leaf None) b => true
210 | RExch a (T_Leaf None) => true
211 | RWeak (T_Leaf None) => true
212 | RCont (T_Leaf None) => true
213 | RComp _ _ _ _ _ => false (* FIXME: do better *)
216 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
218 | RArrange _ _ _ _ _ r => nd_hideURule r
219 | REmptyGroup _ _ => true
220 | RBindingGroup _ _ _ _ _ _ => true
224 Instance ToLatexMathRule h c : ToLatexMath (Rule h c) :=
225 { toLatexMath := fun r => rawLatexMath (@nd_ruleToRawLatexMath h c r) }.
227 Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) :=
228 @SCND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
229 (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).