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.
22 Section HaskProofToLatex.
24 Context {TV:Kind -> Type}.
25 Context {TVLatex:forall k, ToLatex (TV k)}.
26 Context {freshM:FreshMonad (∀ κ, TV κ)}.
27 Definition FreshM' := FMT freshM.
28 Instance FreshMon' : Monad FreshM' := FMT_Monad freshM.
30 Fixpoint typeToLatex (needparens:bool){κ}(t:RawHaskType TV κ) {struct t} : FMT freshM Latex :=
32 | TVar _ v => return toLatex v
33 | TCon tc => return (latex "\text{\tt{")+=+tc+=+(latex "}}")
34 | TArrow => return latex "\text{\tt{(->)}}"
35 | TCoerc _ t1 t2 t => bind t1' = typeToLatex false t1
36 ; bind t2' = typeToLatex false t2
37 ; bind t' = typeToLatex needparens t
38 ; return (latex "{(")+=+t1'+=+(latex "{\sim}")+=+
39 t2'+=+(latex ")}\Rightarrow{")+=+t'+=+(latex "}")
40 | TApp _ _ t1 t2 => match t1 with
41 | TApp _ _ TArrow tx => bind t1' = typeToLatex true tx
42 ; bind t2' = typeToLatex true t2
43 ; let body := t1'+=+(latex "{\rightarrow}")+=+t2'
44 in return if needparens then (latex "(")+=+body+=+(latex ")") else body
45 | _ => bind t1' = typeToLatex true t1
46 ; bind t2' = typeToLatex true t2
47 ; let body := t1'+=+(latex " ")+=+t2'
48 in return if needparens then (latex "(")+=+body+=+(latex ")") else body
50 | TCode ec t => bind ec' = typeToLatex true ec
51 ; bind t' = typeToLatex false t
52 ; return (latex "\code{")+=+ec'+=+(latex "}{")+=+t'+=+(latex "}")
53 | TyFunApp tfc lt => bind rest = typeListToLatex false lt
54 ; return (latex "{\text{\tt{")+=+(sanitizeForLatex (toString tfc))+=+(latex "}}}")+=+
55 (*(latex "_{")+=+(latex (toString (tfc:nat)))+=+(latex "}")+=+*)
56 (fold_left (fun x y => (latex " \ ")+=+x+=+y)
58 | TAll k f => (*bind alpha = next
59 ; bind t' = typeToLatex false (f (alpha k))
60 ; *)return (latex "(\forall ")(*+=+(@toLatex _ (TVLatex k) (alpha k))*)
61 +=+(latex "{:}")+=+(kindToLatex k)+=+(latex ")")(*+=+t'*)
63 with typeListToLatex (needparens:bool){κ}(t:RawHaskTypeList κ) {struct t} : FreshM' (list Latex) :=
65 | TyFunApp_nil => return nil
66 | TyFunApp_cons κ kl rhk rhkl => bind r = typeToLatex needparens rhk
67 ; bind rl = typeListToLatex needparens rhkl
71 Definition ltypeToLatex {Γ:TypeEnv}{κ}(t:RawHaskType TV κ)(lev:list nat) : FreshM' Latex :=
73 | nil => typeToLatex false t
74 | lv => bind t' = typeToLatex true t
82 (fold_left (fun x y => x+=+":"+=+y) (map tyvar2greek lv) "")+=+"}"
86 Definition var2string (n:nat) :=
99 | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++x+++"}"
101 Close Scope nat_scope.
103 Definition covar2greek (n:nat) :=
104 "{\gamma_{"+++n+++"}}".
106 Fixpoint enumerate' (n:nat){T:Type}(l:list T) : list (nat * T) :=
109 | (a::b) => (n,a)::(enumerate' (S n) b)
112 Definition enumerate {T:Type}(l:list T) := enumerate' O l.
114 Fixpoint count (n:nat) : vec nat n :=
117 | S n' => n':::(count n')
120 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
121 match lk as LK return IList _ _ LK with
123 | h::t => n::::(count' t (S n))
126 Definition InstantiatedTypeEnvString Γ : @InstantiatedTypeEnv (fun _ => nat) Γ := count' Γ O.
127 Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv (fun _ => nat) nat Γ Δ := count (length Δ).
128 Definition judgmentToLatex (j:Judg) : string :=
131 let Γ' := InstantiatedTypeEnvString Γ in
132 let Δ' := InstantiatedCoercionEnvString Γ Δ in
133 let lt2l := fun nt:nat*(LeveledHaskType Γ ★) =>
137 (var2string n)+++"{:}"+++(@ltypeToLatex Γ _ (t (fun _ => nat) Γ')
138 (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
140 let lt2l' := fun lt:(LeveledHaskType Γ ★) =>
143 (@ltypeToLatex Γ _ (t (fun _ => nat) Γ')
144 (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
146 (listToLatex "" lt2l "\ ,\ " (enumerate (leaves a)))
147 +++" \ \vdash_e\ "(*+++"e{:}"*)
148 +++(listToLatex "" lt2l' "\ ,\ " (leaves b))
151 Definition j2l (j2j:Judg -> Judg) jt :=
152 @judgmentsToLatex Judg judgmentToLatex (mapOptionTree j2j jt).
154 Fixpoint nd_uruleToLatex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
156 | RLeft _ _ _ r => nd_uruleToLatex r
157 | RRight _ _ _ r => nd_uruleToLatex r
158 | RCanL _ _ => "CanL"
159 | RCanR _ _ => "CanR"
160 | RuCanL _ _ => "uCanL"
161 | RuCanR _ _ => "uCanR"
162 | RAssoc _ _ _ _ => "Assoc"
163 | RCossa _ _ _ _ => "Cossa"
164 | RExch _ _ _ => "Exch"
165 | RWeak _ _ => "Weak"
166 | RCont _ _ => "Cont"
169 Fixpoint nd_ruleToLatex {h}{c}(r:Rule h c) : string :=
171 | RURule _ _ _ _ r => nd_uruleToLatex r
172 | RNote _ _ _ _ _ _ => "Note"
173 | RLit _ _ _ _ => "Lit"
174 | RVar _ _ _ _ => "Var"
175 | RGlobal _ _ _ _ _ => "Global"
176 | RLam _ _ _ _ _ _ => "Abs"
177 | RCast _ _ _ _ _ _ _ => "Cast"
178 | RAbsT _ _ _ _ _ _ => "AbsT"
179 | RAppT _ _ _ _ _ _ _ => "AppT"
180 | RAppCo _ _ _ _ _ _ _ _ _ => "AppCo"
181 | RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
182 | RApp _ _ _ _ _ _ _ => "App"
183 | RLet _ _ _ _ _ _ _ => "Let"
184 | RBindingGroup _ _ _ _ _ _ => "RBindingGroup"
185 | RLetRec _ _ _ _ _ _ => "LetRec"
186 | RCase _ _ _ _ _ _ _ _ => "Case"
187 | RBrak _ _ _ _ _ _ => "Brak"
188 | REsc _ _ _ _ _ _ => "Esc"
189 | REmptyGroup _ _ => "REmptyGroup"
192 Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
194 | RLeft _ _ _ r => nd_hideURule r
195 | RRight _ _ _ r => nd_hideURule r
200 | RAssoc _ _ _ _ => true
201 | RCossa _ _ _ _ => true
202 | RExch _ (T_Leaf None) b => true
203 | RExch _ a (T_Leaf None) => true
204 | RWeak _ (T_Leaf None) => true
205 | RCont _ (T_Leaf None) => true
208 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
210 | RURule _ _ _ _ r => nd_hideURule r
211 | REmptyGroup _ _ => true
212 | RBindingGroup _ _ _ _ _ _ => true
217 End HaskProofToLatex.
220 Definition nd_ml_toLatex {c}(pf:@ND _ Rule [] c) :=
223 (fun h c r => @nd_ruleToLatex h c r)
224 (fun h c r => @nd_hideRule h c r)
225 _ _ (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).