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 NaturalDeductionContext.
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 HaskLiterals.
16 Require Import HaskTyCons.
17 Require Import HaskStrongTypes.
18 Require Import HaskStrong.
19 Require Import HaskProof.
20 Require Import HaskCoreTypes.
24 Inductive VarNameStore :=
25 varNameStore : nat -> nat -> nat -> VarNameStore.
26 Inductive VarNameStoreM {T} :=
27 varNameStoreM : (VarNameStore -> (T * VarNameStore)) -> VarNameStoreM.
28 Implicit Arguments VarNameStoreM [ ].
31 Instance VarNameMonad : Monad VarNameStoreM :=
32 { returnM := fun _ x => varNameStoreM (fun v => (x,v))
33 ; bindM := fun _ _ x f =>
36 varNameStoreM (fun vns =>
38 (x',vns') => match f x' with
39 varNameStoreM fx' => fx' vns'
43 Definition freshTyVarName : Kind -> VarNameStoreM LatexMath :=
44 fun κ => varNameStoreM (fun vns =>
46 varNameStore n1 n2 n3 =>
47 let name := (rawLatexMath "\alpha_{")+++toLatexMath (toString n1)+++(rawLatexMath "}")
48 in (name,(varNameStore (S n1) n2 n3))
50 Definition freshCoVarName : VarNameStoreM LatexMath :=
51 varNameStoreM (fun vns =>
53 varNameStore n1 n2 n3 =>
54 let name := (rawLatexMath "\gamma_{")+++toLatexMath (toString n2)+++(rawLatexMath "}")
55 in (name,(varNameStore n1 (S n2) n3))
57 Definition freshValVarName : VarNameStoreM LatexMath :=
58 varNameStoreM (fun vns =>
60 varNameStore n1 n2 n3 =>
61 let vn := match n3 with
73 | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++toString x+++"}"
75 in let name := rawLatexMath ("x_{"+++vn+++"}")
76 in (name,(varNameStore n1 n2 (S n3)))
79 Fixpoint typeToLatexMath (needparens:bool){κ}(t:RawHaskType (fun _ => LatexMath) κ) {struct t} : VarNameStoreM LatexMath :=
80 match t return VarNameStoreM LatexMath with
81 | TVar _ v => return toLatexMath v
82 | TCon tc => return ((rawLatexMath "\text{\tt{")+++toLatexMath (toString tc)+++(rawLatexMath "}}"))
83 | TArrow => return rawLatexMath "\text{\tt{(->)}}"
84 | TCoerc _ t1 t2 t => bind t1' = typeToLatexMath false t1
85 ; bind t2' = typeToLatexMath false t2
86 ; bind t' = typeToLatexMath needparens t
87 ; return ((rawLatexMath "{(")+++t1'+++(rawLatexMath "{\sim}")+++
88 t2'+++(rawLatexMath ")}\Rightarrow{")+++t'+++(rawLatexMath "}"))
89 | TCode ec t => bind ec' = typeToLatexMath true ec
90 ; bind t' = typeToLatexMath false t
91 ; return (rawLatexMath "\code{")+++ec'+++(rawLatexMath "}{")+++t'+++(rawLatexMath "}")
92 | TAll k f => bind alpha = freshTyVarName k
93 ; bind t' = typeToLatexMath false (f alpha)
94 ; return (rawLatexMath "(\forall ")+++alpha+++(rawLatexMath "{:}")+++
95 (kindToLatexMath k)+++(rawLatexMath ")")+++t'
96 | TApp _ _ t1 t2 => match t1 return VarNameStoreM LatexMath with
97 | TApp _ _ TArrow tx => bind t1' = typeToLatexMath true tx
98 ; bind t2' = typeToLatexMath true t2
99 ; let body := t1'+++(rawLatexMath "{\rightarrow}")+++t2'
100 in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
101 | _ => bind t1' = typeToLatexMath true t1
102 ; bind t2' = typeToLatexMath true t2
103 ; let body := t1'+++(rawLatexMath " ")+++t2'
104 in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
106 | TyFunApp tfc _ _ lt => bind rest = typeListToRawLatexMath false lt
107 ; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++
108 (rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++
109 (rawLatexMath "}")+++
110 (fold_left (fun x y => (rawLatexMath " \ ")+++x+++y)
111 rest (rawLatexMath ""))
113 with typeListToRawLatexMath (needparens:bool){κ}(t:RawHaskTypeList κ) {struct t} : VarNameStoreM (list LatexMath) :=
114 match t return VarNameStoreM (list LatexMath) with
115 | TyFunApp_nil => return nil
116 | TyFunApp_cons κ kl rhk rhkl => bind r = typeToLatexMath needparens rhk
117 ; bind rl = typeListToRawLatexMath needparens rhkl
121 Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameStoreM LatexMath.
126 bind t'' = typeToLatexMath false (t' (fun _ => LatexMath) ite) ;
127 return match lev with
129 | lv => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++
130 (fold_left (fun x y => x+++(rawLatexMath ":")+++y)
131 (map (fun l:HaskTyVar Γ _ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
133 end); try apply ConcatenableLatexMath.
134 try apply VarNameMonad.
138 refine (bind tv' = freshTyVarName a ; _).
140 refine (bind IHΓ' = IHΓ ; return _).
148 Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
149 match match j return VarNameStoreM LatexMath with
150 | mkJudg Γ Δ Σ₁ Σ₂ l =>
151 bind Σ₁' = treeM (mapOptionTree ltypeToLatexMath Σ₁)
152 ; bind Σ₂' = treeM (mapOptionTree (fun t => ltypeToLatexMath (t@@l)) Σ₂)
153 ; return treeToLatexMath Σ₁' +++ (rawLatexMath "\vdash") +++ treeToLatexMath Σ₂'
155 varNameStoreM f => fst (f (varNameStore 0 0 0))
158 Instance ToLatexMathJudgment : ToLatexMath Judg :=
159 { toLatexMath := judgmentToRawLatexMath }.
161 Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
163 | ALeft _ _ _ r => nd_uruleToRawLatexMath r
164 | ARight _ _ _ r => nd_uruleToRawLatexMath r
168 | AuCanL _ => "uCanL"
169 | AuCanR _ => "uCanR"
170 | AAssoc _ _ _ => "Assoc"
171 | AuAssoc _ _ _ => "Cossa"
172 | AExch _ _ => "Exch"
175 | AComp _ _ _ _ _ => "Comp" (* FIXME: do a better job here *)
178 Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
180 | RArrange _ _ _ _ _ _ r => nd_uruleToRawLatexMath r
181 | RNote _ _ _ _ _ _ => "Note"
182 | RLit _ _ _ _ => "Lit"
183 | RVar _ _ _ _ => "Var"
184 | RGlobal _ _ _ _ _ => "Global"
185 | RLam _ _ _ _ _ _ => "Abs"
186 | RCast _ _ _ _ _ _ _ => "Cast"
187 | RAbsT _ _ _ _ _ _ _ => "AbsT"
188 | RAppT _ _ _ _ _ _ _ => "AppT"
189 | RAppCo _ _ _ _ _ _ _ _ _ => "AppCo"
190 | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
191 | RApp _ _ _ _ _ _ _ => "App"
192 | RCut _ _ _ _ _ _ _ _ => "Cut"
193 | RLeft _ _ _ _ _ _ => "Left"
194 | RRight _ _ _ _ _ _ => "Right"
195 | RLetRec _ _ _ _ _ _ => "LetRec"
196 | RCase _ _ _ _ _ _ _ _ => "Case"
197 | RBrak _ _ _ _ _ _ => "Brak"
198 | REsc _ _ _ _ _ _ => "Esc"
199 | RVoid _ _ _ => "RVoid"
202 Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
204 | ALeft _ _ _ r => nd_hideURule r
205 | ARight _ _ _ r => nd_hideURule r
210 | AAssoc _ _ _ => true
211 | AuAssoc _ _ _ => true
212 | AExch (T_Leaf None) b => true
213 | AExch a (T_Leaf None) => true
214 | AWeak (T_Leaf None) => true
215 | ACont (T_Leaf None) => true
216 | AComp _ _ _ _ _ => false (* FIXME: do better *)
219 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
221 | RArrange _ _ _ _ _ _ r => nd_hideURule r
222 | RVoid _ _ _ => true
223 | RLeft _ _ _ _ _ _ => true
224 | RRight _ _ _ _ _ _ => true
228 Instance ToLatexMathRule h c : ToLatexMath (Rule h c) :=
229 { toLatexMath := fun r => rawLatexMath (@nd_ruleToRawLatexMath h c r) }.
231 Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) :=
232 @SIND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
233 (mkSIND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).