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.
21 Open Scope string_scope.
24 Fixpoint kind2latex (k:Kind) : string :=
27 | ★ ⇛ k2 => "\star\Rightarrow "+++kind2latex k2
28 | k1 ⇛ k2 => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
29 | KindUnliftedType => "\text{\tt{\#}}"
30 | KindUnboxedTuple => "\text{\tt{(\#)}}"
31 | KindArgType => "\text{\tt{??}}"
32 | KindOpenType => "\text{\tt{?}}"
36 Definition var2string (n:nat) :=
49 | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++x+++"}"
51 Close Scope nat_scope.
53 Definition tyvar2greek (n:nat) :=
58 | S (S (S n)) => "\alpha_{"+++n+++"}"
61 Definition covar2greek (n:nat) :=
62 "{\gamma_{"+++n+++"}}".
64 (* TODO: now that PHOAS tyvar-representation-types are kind-indexed, we can do some clever stuff here *)
65 Fixpoint type2latex (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
67 | TVar _ v => tyvar2greek v
68 | TCon tc => "\text{\tt{"+++sanitizeForLatex (toString tc) +++"}}"
69 | TCoerc _ t1 t2 t => "{("+++type2latex false n t1+++"{\sim}"
70 +++type2latex false n t2+++")}\Rightarrow{"
71 +++type2latex needparens n t+++"}"
74 | TApp _ _ TArrow t1 =>
76 then "("+++(type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)+++")"
77 else (type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)
80 then "("+++(type2latex true n t1)+++" "+++(type2latex false n t2)+++")"
81 else (type2latex true n t1)+++" "+++(type2latex false n t2)
83 | TArrow => "\text{\tt{(->)}}"
84 | TAll k f => let alpha := tyvar2greek n
85 in "(\forall "+++ alpha +++ "{:}"+++ kind2latex k +++")"+++
86 type2latex false (S n) (f n)
87 | TCode ec t => "\code{"+++(type2latex true n ec)+++"}{"+++(type2latex false n t)+++"}"
88 | TyFunApp tfc lt => "{\text{\tt{"+++sanitizeForLatex (toString tfc) +++"}}}"+++
90 fold_left (fun x y => " \ "+++x+++y)
91 (typeList2latex false n lt) ""
93 with typeList2latex (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
96 | TyFunApp_cons κ kl rhk rhkl => (type2latex needparens n rhk)::(typeList2latex needparens n rhkl)
99 Definition ltype2latex {Γ:TypeEnv}{κ}(t:RawHaskType (fun _ => nat) κ)(lev:list nat) : string :=
101 | nil => type2latex false O t
102 | lv => "{"+++type2latex true O t+++"}^{"+++(fold_left (fun x y => x+++":"+++y) (map tyvar2greek lv) "")+++"}"
105 Fixpoint enumerate' (n:nat){T:Type}(l:list T) : list (nat * T) :=
108 | (a::b) => (n,a)::(enumerate' (S n) b)
111 Definition enumerate {T:Type}(l:list T) := enumerate' O l.
113 Fixpoint count (n:nat) : vec nat n :=
116 | S n' => n':::(count n')
119 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
120 match lk as LK return IList _ _ LK with
122 | h::t => n::::(count' t (S n))
125 Definition InstantiatedTypeEnvString Γ : @InstantiatedTypeEnv (fun _ => nat) Γ := count' Γ O.
126 Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv (fun _ => nat) nat Γ Δ := count (length Δ).
127 Definition judgment2latex (j:Judg) : string :=
130 let Γ' := InstantiatedTypeEnvString Γ in
131 let Δ' := InstantiatedCoercionEnvString Γ Δ in
132 let lt2l := fun nt:nat*(LeveledHaskType Γ ★) =>
136 (var2string n)+++"{:}"+++(@ltype2latex Γ _ (t (fun _ => nat) Γ')
137 (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
139 let lt2l' := fun lt:(LeveledHaskType Γ ★) =>
142 "e{:}"+++(@ltype2latex Γ _ (t (fun _ => nat) Γ')
143 (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
145 (list2latex "" lt2l "\ ,\ " (enumerate (leaves a)))
146 +++" \ \vdash_e\ "(*+++"e{:}"*)
147 +++(list2latex "" lt2l' "\ ,\ " (leaves b))
150 Definition j2l (j2j:Judg -> Judg) jt :=
151 @judgments2latex Judg judgment2latex (mapOptionTree j2j jt).
153 Fixpoint nd_urule2latex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
155 | RLeft _ _ _ r => nd_urule2latex r
156 | RRight _ _ _ r => nd_urule2latex r
157 | RCanL _ _ => "CanL"
158 | RCanR _ _ => "CanR"
159 | RuCanL _ _ => "uCanL"
160 | RuCanR _ _ => "uCanR"
161 | RAssoc _ _ _ _ => "Assoc"
162 | RCossa _ _ _ _ => "Cossa"
163 | RExch _ _ _ => "Exch"
164 | RWeak _ _ => "Weak"
165 | RCont _ _ => "Cont"
168 Fixpoint nd_rule2latex {h}{c}(r:Rule h c) : string :=
170 | RURule _ _ _ _ r => nd_urule2latex r
171 | RNote _ _ _ _ _ _ => "Note"
172 | RLit _ _ _ _ => "Lit"
173 | RVar _ _ _ _ => "Var"
174 | RGlobal _ _ _ _ _ => "Global"
175 | RLam _ _ _ _ _ _ => "Abs"
176 | RCast _ _ _ _ _ _ _ => "Cast"
177 | RAbsT _ _ _ _ _ _ => "AbsT"
178 | RAppT _ _ _ _ _ _ _ => "AppT"
179 | RAppCo _ _ _ _ _ _ _ _ _ => "AppCo"
180 | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
181 | RApp _ _ _ _ _ _ _ => "App"
182 | RLet _ _ _ _ _ _ _ => "Let"
183 | RBindingGroup _ _ _ _ _ _ => "RBindingGroup"
184 | RLetRec _ _ _ _ _ _ => "LetRec"
185 | RCase _ _ _ _ _ _ _ _ => "Case"
186 | RBrak _ _ _ _ _ _ => "Brak"
187 | REsc _ _ _ _ _ _ => "Esc"
188 | REmptyGroup _ _ => "REmptyGroup"
191 Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
193 | RLeft _ _ _ r => nd_hideURule r
194 | RRight _ _ _ r => nd_hideURule r
199 | RAssoc _ _ _ _ => true
200 | RCossa _ _ _ _ => true
201 | RExch _ (T_Leaf None) b => true
202 | RExch _ a (T_Leaf None) => true
203 | RWeak _ (T_Leaf None) => true
204 | RCont _ (T_Leaf None) => true
207 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
209 | RURule _ _ _ _ r => nd_hideURule r
210 | REmptyGroup _ _ => true
211 | RBindingGroup _ _ _ _ _ _ => true
216 Definition nd_ml_toLatex {c}(pf:@ND _ Rule [] c) :=
219 (fun h c r => @nd_rule2latex h c r)
220 (fun h c r => @nd_hideRule h c r)
221 _ _ (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).