reshuffle definitions in an attempt to iron out inter-file dependenceies
[coq-hetmet.git] / src / HaskProofToLatex.v
1 (*********************************************************************************************************************************)
2 (* HaskProofToLatex: render HaskProof's as LaTeX code using trfrac.sty                                                           *)
3 (*********************************************************************************************************************************)
4
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.
20
21 (* escapifies any characters which might cause trouble for LaTeX *)
22 Variable sanitizeForLatex    : string      -> string.        Extract Inlined Constant sanitizeForLatex      => "sanitizeForLatex".
23
24 Open Scope string_scope.
25 Section ToLatex.
26
27   Fixpoint kind2latex (k:Kind) : string :=
28     match k with
29     | KindType                     => "\star"
30     | KindTypeFunction KindType k2 => "\star\Rightarrow "+++kind2latex k2
31     | KindTypeFunction k1 k2       => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
32     | KindUnliftedType             => "\text{\tt{\#}}"
33     | KindUnboxedTuple             => "\text{\tt{(\#)}}"
34     | KindArgType                  => "\text{\tt{??}}"
35     | KindOpenType                 => "\text{\tt{?}}"
36     end.
37
38   Open Scope nat_scope.
39   Definition var2string (n:nat) :=
40     match n with
41       | 0 => "x"
42       | 1 => "y"
43       | 2 => "z"
44       | 3 => "a"
45       | 4 => "b"
46       | 5 => "c"
47       | 6 => "d"
48       | 7 => "e"
49       | 8 => "f"
50       | 9 => "g"
51       | 10 => "h"
52       | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++x+++"}"
53     end.
54   Close Scope nat_scope.
55
56   Definition tyvar2greek (n:nat) :=
57     match n with
58       | O => "\alpha"
59       | S O => "\beta"
60       | S (S O) => "\xi"
61       | S (S (S n)) => "\alpha_{"+++n+++"}"
62     end.
63
64   Definition covar2greek (n:nat) :=
65     "{\gamma_{"+++n+++"}}".
66
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 :=
69     match t with
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+++"}"
75     | TApp  _ _  t1 t2     =>
76       match t1 with
77         | TApp _ _ TArrow t1 =>
78                      if needparens
79                      then "("+++(type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)+++")"
80                      else (type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)
81         | _ =>
82                      if needparens
83                      then "("+++(type2latex true n t1)+++" "+++(type2latex false n t2)+++")"
84                      else (type2latex true n t1)+++" "+++(type2latex false n t2)
85       end
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) +++"}}}"+++
92                               "_{"+++n+++"}"+++
93                               fold_left (fun x y => " \  "+++x+++y)
94                               (typeList2latex false n lt) ""
95   end
96   with typeList2latex (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
97   match t with
98   | TyFunApp_nil                 => nil
99   | TyFunApp_cons  κ kl rhk rhkl => (type2latex needparens n rhk)::(typeList2latex needparens n rhkl)
100   end.
101
102   Definition ltype2latex {Γ:TypeEnv}{κ}(t:RawHaskType (fun _ => nat) κ)(lev:list nat) : string :=
103     match lev with
104       | nil => type2latex false O t
105       | lv  => "{"+++type2latex true O t+++"}^{"+++(fold_left (fun x y => x+++":"+++y) (map tyvar2greek lv) "")+++"}"
106     end.
107
108   Fixpoint enumerate' (n:nat){T:Type}(l:list T) : list (nat * T) :=
109     match l with
110       | nil    => nil
111       | (a::b) => (n,a)::(enumerate' (S n) b)
112     end.
113
114   Definition enumerate {T:Type}(l:list T) := enumerate' O l.
115
116   Fixpoint count (n:nat) : vec nat n :=
117   match n with
118     | O    => vec_nil
119     | S n' => n':::(count n')
120   end.
121
122   Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
123   match lk as LK return IList _ _ LK with
124     | nil    => INil
125     | h::t   => n::::(count' t (S n))
126   end.
127
128   Definition InstantiatedTypeEnvString     Γ   : @InstantiatedTypeEnv     (fun _ => nat) Γ := count' Γ O.
129   Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv (fun _ => nat) nat Γ Δ  := count (length Δ).
130   Definition judgment2latex (j:Judg) : string :=
131       match j with
132         | mkJudg Γ Δ  a b =>
133           let Γ' := InstantiatedTypeEnvString Γ in
134           let Δ' := InstantiatedCoercionEnvString Γ Δ in
135           let lt2l := fun nt:nat*(LeveledHaskType Γ ★) => 
136             let (n,lt) := nt in
137               match lt with
138                 t @@ l =>
139                 (var2string n)+++"{:}"+++(@ltype2latex Γ _ (t (fun _ => nat) Γ')
140                   (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
141               end in
142           let lt2l' := fun lt:(LeveledHaskType Γ ★) => 
143               match lt with
144                 t @@ l =>
145                 "e{:}"+++(@ltype2latex Γ _ (t (fun _ => nat) Γ')
146                   (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
147               end in
148           (list2latex "" lt2l "\ ,\ " (enumerate (leaves a)))
149           +++" \ \vdash_e\  "(*+++"e{:}"*)
150           +++(list2latex "" lt2l' "\ ,\ " (leaves b))
151       end.
152
153   Definition j2l (j2j:Judg -> Judg) jt :=
154     @judgments2latex Judg judgment2latex (mapOptionTree j2j jt).
155
156   Fixpoint nd_urule2latex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
157     match r with
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"
169     end.
170
171   Fixpoint nd_rule2latex {h}{c}(r:Rule h c) : string :=
172     match r with
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"
191   end.
192
193   Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
194     match r with
195       | RLeft   _ _ _ r               => nd_hideURule r
196       | RRight  _ _ _ r               => nd_hideURule r
197       | RCanL   _ _                   => true
198       | RCanR   _ _                   => true
199       | RuCanL  _ _                   => true
200       | RuCanR  _ _                   => true
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
207       | _                             => false
208     end.
209   Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
210     match r with
211       | RURule        _ _ _ _ r   => nd_hideURule r
212       | REmptyGroup   _ _         => true
213       | RBindingGroup _ _ _ _ _ _ => true
214       | _                         => false
215     end.
216 End ToLatex.
217
218 Definition nd_ml_toLatex {c}(pf:@ND _ Rule [] c) :=
219   @SCND_toLatex _ _
220       judgment2latex
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 [])).