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 (* escapifies any characters which might cause trouble for LaTeX *)
22 Variable sanitizeForLatex : string -> string. Extract Inlined Constant sanitizeForLatex => "sanitizeForLatex".
24 Open Scope string_scope.
27 Fixpoint kind2latex (k:Kind) : string :=
30 | ★ ⇛ k2 => "\star\Rightarrow "+++kind2latex k2
31 | k1 ⇛ k2 => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
32 | KindUnliftedType => "\text{\tt{\#}}"
33 | KindUnboxedTuple => "\text{\tt{(\#)}}"
34 | KindArgType => "\text{\tt{??}}"
35 | KindOpenType => "\text{\tt{?}}"
39 Definition var2string (n:nat) :=
52 | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++x+++"}"
54 Close Scope nat_scope.
56 Definition tyvar2greek (n:nat) :=
61 | S (S (S n)) => "\alpha_{"+++n+++"}"
64 Definition covar2greek (n:nat) :=
65 "{\gamma_{"+++n+++"}}".
67 (* TODO: now that PHOAS tyvar-representation-types are kind-indexed, we can do some clever stuff here *)
68 Fixpoint type2latex (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
70 | TVar _ v => tyvar2greek v
71 | TCon tc => "\text{\tt{"+++sanitizeForLatex (toString tc) +++"}}"
72 | TCoerc _ t1 t2 t => "{("+++type2latex false n t1+++"{\sim}"
73 +++type2latex false n t2+++")}\Rightarrow{"
74 +++type2latex needparens n t+++"}"
77 | TApp _ _ TArrow t1 =>
79 then "("+++(type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)+++")"
80 else (type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)
83 then "("+++(type2latex true n t1)+++" "+++(type2latex false n t2)+++")"
84 else (type2latex true n t1)+++" "+++(type2latex false n t2)
86 | TArrow => "\text{\tt{(->)}}"
87 | TAll k f => let alpha := tyvar2greek n
88 in "(\forall "+++ alpha +++ "{:}"+++ kind2latex k +++")"+++
89 type2latex false (S n) (f n)
90 | TCode ec t => "\code{"+++(type2latex true n ec)+++"}{"+++(type2latex false n t)+++"}"
91 | TyFunApp tfc lt => "{\text{\tt{"+++sanitizeForLatex (toString tfc) +++"}}}"+++
93 fold_left (fun x y => " \ "+++x+++y)
94 (typeList2latex false n lt) ""
96 with typeList2latex (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
99 | TyFunApp_cons κ kl rhk rhkl => (type2latex needparens n rhk)::(typeList2latex needparens n rhkl)
102 Definition ltype2latex {Γ:TypeEnv}{κ}(t:RawHaskType (fun _ => nat) κ)(lev:list nat) : string :=
104 | nil => type2latex false O t
105 | lv => "{"+++type2latex true O t+++"}^{"+++(fold_left (fun x y => x+++":"+++y) (map tyvar2greek lv) "")+++"}"
108 Fixpoint enumerate' (n:nat){T:Type}(l:list T) : list (nat * T) :=
111 | (a::b) => (n,a)::(enumerate' (S n) b)
114 Definition enumerate {T:Type}(l:list T) := enumerate' O l.
116 Fixpoint count (n:nat) : vec nat n :=
119 | S n' => n':::(count n')
122 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
123 match lk as LK return IList _ _ LK with
125 | h::t => n::::(count' t (S n))
128 Definition InstantiatedTypeEnvString Γ : @InstantiatedTypeEnv (fun _ => nat) Γ := count' Γ O.
129 Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv (fun _ => nat) nat Γ Δ := count (length Δ).
130 Definition judgment2latex (j:Judg) : string :=
133 let Γ' := InstantiatedTypeEnvString Γ in
134 let Δ' := InstantiatedCoercionEnvString Γ Δ in
135 let lt2l := fun nt:nat*(LeveledHaskType Γ ★) =>
139 (var2string n)+++"{:}"+++(@ltype2latex Γ _ (t (fun _ => nat) Γ')
140 (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
142 let lt2l' := fun lt:(LeveledHaskType Γ ★) =>
145 "e{:}"+++(@ltype2latex Γ _ (t (fun _ => nat) Γ')
146 (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
148 (list2latex "" lt2l "\ ,\ " (enumerate (leaves a)))
149 +++" \ \vdash_e\ "(*+++"e{:}"*)
150 +++(list2latex "" lt2l' "\ ,\ " (leaves b))
153 Definition j2l (j2j:Judg -> Judg) jt :=
154 @judgments2latex Judg judgment2latex (mapOptionTree j2j jt).
156 Fixpoint nd_urule2latex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
158 | RLeft _ _ _ r => nd_urule2latex r
159 | RRight _ _ _ r => nd_urule2latex r
160 | RCanL _ _ => "CanL"
161 | RCanR _ _ => "CanR"
162 | RuCanL _ _ => "uCanL"
163 | RuCanR _ _ => "uCanR"
164 | RAssoc _ _ _ _ => "Assoc"
165 | RCossa _ _ _ _ => "Cossa"
166 | RExch _ _ _ => "Exch"
167 | RWeak _ _ => "Weak"
168 | RCont _ _ => "Cont"
171 Fixpoint nd_rule2latex {h}{c}(r:Rule h c) : string :=
173 | RURule _ _ _ _ r => nd_urule2latex r
174 | RNote _ _ _ => "Note"
175 | RLit _ _ _ _ => "Lit"
176 | RVar _ _ _ _ => "Var"
177 | RLam _ _ _ _ _ _ => "Abs"
178 | RCast _ _ _ _ _ _ _ => "Cast"
179 | RAbsT _ _ _ _ _ _ => "AbsT"
180 | RAppT _ _ _ _ _ _ _ => "AppT"
181 | RAppCo _ _ _ _ _ _ _ _ _ => "AppCo"
182 | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
183 | RApp _ _ _ _ _ _ _ => "App"
184 | RLet _ _ _ _ _ _ _ => "Let"
185 | RBindingGroup _ _ _ _ _ _ => "RBindingGroup"
186 | RLetRec _ _ _ _ _ => "LetRec"
187 | RCase _ _ _ _ _ _ _ _ => "Case"
188 | RBrak _ _ _ _ _ _ => "Brak"
189 | REsc _ _ _ _ _ _ => "Esc"
190 | REmptyGroup _ _ => "REmptyGroup"
193 Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
195 | RLeft _ _ _ r => nd_hideURule r
196 | RRight _ _ _ r => nd_hideURule r
201 | RAssoc _ _ _ _ => true
202 | RCossa _ _ _ _ => true
203 | RExch _ (T_Leaf None) b => true
204 | RExch _ a (T_Leaf None) => true
205 | RWeak _ (T_Leaf None) => true
206 | RCont _ (T_Leaf None) => true
209 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
211 | RURule _ _ _ _ r => nd_hideURule r
212 | REmptyGroup _ _ => true
213 | RBindingGroup _ _ _ _ _ _ => true
218 Definition nd_ml_toLatex {c}(pf:@ND _ Rule [] c) :=
221 (fun h c r => @nd_rule2latex h c r)
222 (fun h c r => @nd_hideRule h c r)
223 _ _ (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).