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 HaskGeneral.
13 Require Import HaskLiterals.
14 Require Import HaskStrongTypes.
15 Require Import HaskStrong.
16 Require Import HaskProof.
18 (* escapifies any characters which might cause trouble for LaTeX *)
19 Variable sanitizeForLatex : string -> string. Extract Inlined Constant sanitizeForLatex => "sanitizeForLatex".
20 Variable nat2string : nat -> string. Extract Inlined Constant nat2string => "nat2string".
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 κ => "{\text{\tt{(+>)}}}_{"+++ kind2latex κ +++"}"
78 | TApp (TCon 2 tc) t1' =>
79 if (tyCon_eq tc ArrowTyCon)
80 then inl _ (if needparens
81 then "("+++(type2latex true n t1')+++"{\rightarrow}"+++(type2latex true n t2)+++")"
82 else (type2latex true n t1')+++"{\rightarrow}"+++(type2latex true n t2))
88 then "("+++(type2latex true n t1)+++" "+++(type2latex false n t2)+++")"
89 else (type2latex true n t1)+++" "+++(type2latex false n t2)
91 | TFCApp n tfc lt => "{\text{\tt{"+++sanitizeForLatex (tyFunToString _ tfc) +++"}}}"+++
92 "_{"+++(nat2string n)+++"}"+++
93 fold_left (fun x y => " \ "+++x+++y)
94 ((fix type2latex_vec (needparens:bool)(n:nat){m}(lt:vec (RawHaskType nat) m)
98 | a:::b => (type2latex needparens n a)::(type2latex_vec needparens n _ b)
101 | TAll k f => let alpha := tyvar2greek n
102 in "(\forall "+++ alpha +++ "{:}"+++ kind2latex k +++")"+++
103 type2latex false (S n) (f n)
104 | TCode ec t => "\code{"+++(type2latex true n ec)+++"}{"+++(type2latex false n t)+++"}"
107 Definition ltype2latex {Γ:TypeEnv}(t:RawHaskType nat)(lev:list nat) : string :=
109 | nil => type2latex false O t
110 | lv => "{"+++type2latex true O t+++"}^{"+++(fold_left (fun x y => x+++":"+++y) (map tyvar2greek lv) "")+++"}"
113 Fixpoint enumerate' (n:nat){T:Type}(l:list T) : list (nat * T) :=
116 | (a::b) => (n,a)::(enumerate' (S n) b)
119 Definition enumerate {T:Type}(l:list T) := enumerate' O l.
121 Definition InstantiatedTypeEnvString Γ : @InstantiatedTypeEnv nat Γ := count (length Γ).
122 Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv nat nat Γ Δ := count (length Δ).
123 Definition judgment2latex (j:Judg) : string :=
126 let Γ' := InstantiatedTypeEnvString Γ in
127 let Δ' := InstantiatedCoercionEnvString Γ Δ in
128 let lt2l := fun nt:nat*(LeveledHaskType Γ) =>
132 (var2string n)+++"{:}"+++(@ltype2latex Γ (t nat Γ') (map (fun x:HaskTyVar Γ => x nat Γ') l))
134 let lt2l' := fun lt:(LeveledHaskType Γ) =>
137 "e{:}"+++(@ltype2latex Γ (t nat Γ') (map (fun x:HaskTyVar Γ => x nat Γ') l))
139 (list2latex "" lt2l "\ ,\ " (enumerate (leaves a)))
140 +++" \ \vdash_e\ "(*+++"e{:}"*)
141 +++(list2latex "" lt2l' "\ ,\ " (leaves b))
144 Definition j2l (j2j:Judg -> Judg) jt :=
145 @judgments2latex Judg judgment2latex (mapOptionTree j2j jt).
147 Fixpoint nd_urule2latex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
149 | (RLeft _ _ c r ) => nd_urule2latex r
150 | (RRight _ _ c r ) => nd_urule2latex r
151 | (RCanL t a ) => "CanL"
152 | (RCanR t a ) => "CanR"
153 | (RuCanL t a ) => "uCanL"
154 | (RuCanR t a ) => "uCanR"
155 | (RAssoc t a b c ) => "Assoc"
156 | (RCossa t a b c ) => "Cossa"
157 | (RExch t a b ) => "Exch"
158 | (RWeak t a ) => "Weak"
159 | (RCont t a ) => "Cont"
162 Fixpoint nd_rule2latex {h}{c}(r:Rule h c) : string :=
164 | RURule _ _ _ _ r => nd_urule2latex r
165 | RNote x n z => "Note"
166 | RLit Γ _ l _ => "Lit"
167 | RVar Γ _ σ p => "Var"
168 | RLam Γ _ Σ tx te p x => "Abs"
169 | RCast Γ _ Σ σ τ γ p x => "Cast"
170 | RAbsT Γ Σ κ σ a p => "AbsT"
171 | RAppT Γ _ Σ κ σ τ p y => "AppT"
172 | RAppCo Γ _ Σ κ _ σ₁ σ₂ σ γ p => "AppCo"
173 | RAbsCo Γ Σ κ σ cc σ₁ σ₂ p y q => "AbsCo"
174 | RApp Γ _ Σ₁ Σ₂ tx te p => "App"
175 | RLet Γ _ Σ₁ Σ₂ σ₁ σ₂ p => "Let"
176 | REmptyGroup _ a => "REmptyGroup"
177 | RBindingGroup _ a b c d e => "RBindingGroup"
178 | RLetRec Γ _ p lri q => "LetRec"
179 | RCase Σ Γ T κlen κ ldcd τ _ _ => "Case"
180 | RBrak Σ _ a b c _ => "Brak"
181 | REsc Σ _ a b c _ => "Esc"
184 Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
186 | RLeft h c ctx r => nd_hideURule r
187 | RRight h c ctx r => nd_hideURule r
192 | RAssoc t a b c => true
193 | RCossa t a b c => true
194 | RExch t (T_Leaf None) b => true
195 | RExch t a (T_Leaf None) => true
196 | RWeak t (T_Leaf None) => true
197 | RCont t (T_Leaf None) => true
200 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
202 | RURule _ _ _ _ r => nd_hideURule r
203 | REmptyGroup a _ => true
204 | RBindingGroup _ _ _ _ _ _ => true
209 Definition nd_ml_toLatex {c}(pf:@ND _ Rule [] c) :=
212 (fun h c r => @nd_rule2latex h c r)
213 (fun h c r => @nd_hideRule h c r)
214 _ _ (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).