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 HaskCoreLiterals.
14 Require Import HaskStrongTypes.
15 Require Import HaskStrong.
16 Require Import HaskProof.
17 Require Import HaskCoreTypes.
19 (* escapifies any characters which might cause trouble for LaTeX *)
20 Variable sanitizeForLatex : string -> string. Extract Inlined Constant sanitizeForLatex => "sanitizeForLatex".
22 Open Scope string_scope.
25 Fixpoint kind2latex (k:Kind) : string :=
28 | KindTypeFunction KindType k2 => "\star\Rightarrow "+++kind2latex k2
29 | KindTypeFunction k1 k2 => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
30 | KindUnliftedType => "\text{\tt{\#}}"
31 | KindUnboxedTuple => "\text{\tt{(\#)}}"
32 | KindArgType => "\text{\tt{?}}"
33 | KindOpenType => "\text{\tt{?}}"
37 Definition var2string (n:nat) :=
50 | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++(nat2string x)+++"}"
52 Close Scope nat_scope.
54 Definition tyvar2greek (n:nat) :=
59 | S (S (S n)) => "\alpha_{"+++nat2string n+++"}"
62 Definition covar2greek (n:nat) :=
63 "{\gamma_{"+++(nat2string n)+++"}}".
65 Fixpoint count (n:nat) : vec nat n :=
68 | S n' => n':::(count n')
71 Fixpoint type2latex (needparens:bool)(n:nat)(t:RawHaskType nat) {struct t} : string :=
73 | TVar v => tyvar2greek v
74 | TCon tc => "\text{\tt{"+++sanitizeForLatex (tyConToString tc) +++"}}"
75 | TCoerc t1 t2 t => "{("+++type2latex false n t1+++"{\sim}"
76 +++type2latex false n t2+++")}\Rightarrow{"
77 +++type2latex needparens n t+++"}"
78 | (TApp (TApp TArrow t1) t2) =>
80 then "("+++(type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)+++")"
81 else (type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2))
82 | TArrow => "\text{\tt{(->)}}"
85 then "("+++(type2latex true n t1)+++" "+++(type2latex false n t2)+++")"
86 else (type2latex true n t1)+++" "+++(type2latex false n t2)
87 | TFCApp tfc lt => "{\text{\tt{"+++sanitizeForLatex (tyConToString tfc) +++"}}}"+++
88 "_{"+++(nat2string n)+++"}"+++
89 fold_left (fun x y => " \ "+++x+++y)
90 ((fix type2latex_vec (needparens:bool)(n:nat){m}(lt:vec (RawHaskType nat) m)
94 | a:::b => (type2latex needparens n a)::(type2latex_vec needparens n _ b)
97 | TAll k f => let alpha := tyvar2greek n
98 in "(\forall "+++ alpha +++ "{:}"+++ kind2latex k +++")"+++
99 type2latex false (S n) (f n)
100 | TCode ec t => "\code{"+++(type2latex true n ec)+++"}{"+++(type2latex false n t)+++"}"
103 Definition ltype2latex {Γ:TypeEnv}(t:RawHaskType nat)(lev:list nat) : string :=
105 | nil => type2latex false O t
106 | lv => "{"+++type2latex true O t+++"}^{"+++(fold_left (fun x y => x+++":"+++y) (map tyvar2greek lv) "")+++"}"
109 Fixpoint enumerate' (n:nat){T:Type}(l:list T) : list (nat * T) :=
112 | (a::b) => (n,a)::(enumerate' (S n) b)
115 Definition enumerate {T:Type}(l:list T) := enumerate' O l.
117 Definition InstantiatedTypeEnvString Γ : @InstantiatedTypeEnv nat Γ := count (length Γ).
118 Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv nat nat Γ Δ := count (length Δ).
119 Definition judgment2latex (j:Judg) : string :=
122 let Γ' := InstantiatedTypeEnvString Γ in
123 let Δ' := InstantiatedCoercionEnvString Γ Δ in
124 let lt2l := fun nt:nat*(LeveledHaskType Γ) =>
128 (var2string n)+++"{:}"+++(@ltype2latex Γ (t nat Γ') (map (fun x:HaskTyVar Γ => x nat Γ') l))
130 let lt2l' := fun lt:(LeveledHaskType Γ) =>
133 "e{:}"+++(@ltype2latex Γ (t nat Γ') (map (fun x:HaskTyVar Γ => x nat Γ') l))
135 (list2latex "" lt2l "\ ,\ " (enumerate (leaves a)))
136 +++" \ \vdash_e\ "(*+++"e{:}"*)
137 +++(list2latex "" lt2l' "\ ,\ " (leaves b))
140 Definition j2l (j2j:Judg -> Judg) jt :=
141 @judgments2latex Judg judgment2latex (mapOptionTree j2j jt).
143 Fixpoint nd_urule2latex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
145 | (RLeft _ _ c r ) => nd_urule2latex r
146 | (RRight _ _ c r ) => nd_urule2latex r
147 | (RCanL t a ) => "CanL"
148 | (RCanR t a ) => "CanR"
149 | (RuCanL t a ) => "uCanL"
150 | (RuCanR t a ) => "uCanR"
151 | (RAssoc t a b c ) => "Assoc"
152 | (RCossa t a b c ) => "Cossa"
153 | (RExch t a b ) => "Exch"
154 | (RWeak t a ) => "Weak"
155 | (RCont t a ) => "Cont"
158 Fixpoint nd_rule2latex {h}{c}(r:Rule h c) : string :=
160 | RURule _ _ _ _ r => nd_urule2latex r
161 | RNote x n z => "Note"
162 | RLit Γ _ l _ => "Lit"
163 | RVar Γ _ σ p => "Var"
164 | RLam Γ _ Σ tx te p x => "Abs"
165 | RCast Γ _ Σ σ τ γ p x => "Cast"
166 | RAbsT Γ Σ κ σ a p => "AbsT"
167 | RAppT Γ _ Σ κ σ τ p y => "AppT"
168 | RAppCo Γ _ Σ _ σ₁ σ₂ σ γ p => "AppCo"
169 | RAbsCo Γ Σ κ σ cc σ₁ σ₂ p y q => "AbsCo"
170 | RApp Γ _ Σ₁ Σ₂ tx te p => "App"
171 | RLet Γ _ Σ₁ Σ₂ σ₁ σ₂ p => "Let"
172 | REmptyGroup _ a => "REmptyGroup"
173 | RBindingGroup _ a b c d e => "RBindingGroup"
174 | RLetRec Γ _ p lri q => "LetRec"
175 | RCase Σ Γ T κlen κ ldcd τ _ => "Case"
176 | RBrak Σ _ a b c _ => "Brak"
177 | REsc Σ _ a b c _ => "Esc"
180 Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
182 | RLeft h c ctx r => nd_hideURule r
183 | RRight h c ctx r => nd_hideURule r
188 | RAssoc t a b c => true
189 | RCossa t a b c => true
190 | RExch t (T_Leaf None) b => true
191 | RExch t a (T_Leaf None) => true
192 | RWeak t (T_Leaf None) => true
193 | RCont t (T_Leaf None) => true
196 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
198 | RURule _ _ _ _ r => nd_hideURule r
199 | REmptyGroup a _ => true
200 | RBindingGroup _ _ _ _ _ _ => true
205 Definition nd_ml_toLatex {c}(pf:@ND _ Rule [] c) :=
208 (fun h c r => @nd_rule2latex h c r)
209 (fun h c r => @nd_hideRule h c r)
210 _ _ (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).