716a9830a6358d6f1c442004bf6e61e0e4234fc9
[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 NaturalDeductionContext.
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 HaskLiterals.
16 Require Import HaskTyCons.
17 Require Import HaskStrongTypes.
18 Require Import HaskStrong.
19 Require Import HaskProof.
20 Require Import HaskCoreTypes.
21
22
23
24 Inductive VarNameStore :=
25   varNameStore : nat -> nat -> nat -> VarNameStore.
26 Inductive VarNameStoreM {T} :=
27   varNameStoreM : (VarNameStore -> (T * VarNameStore)) -> VarNameStoreM.
28 Implicit Arguments VarNameStoreM [ ].
29
30 Open Scope nat_scope.
31 Instance VarNameMonad : Monad VarNameStoreM :=
32 { returnM := fun _   x   => varNameStoreM (fun v => (x,v))
33 ; bindM   := fun _ _ x f =>
34   match x with
35     varNameStoreM xf =>
36   varNameStoreM (fun vns =>
37     match xf vns with
38       (x',vns') => match f x' with
39                      varNameStoreM fx' => fx' vns'
40                    end
41     end) end }.
42
43 Definition freshTyVarName : Kind -> VarNameStoreM LatexMath :=
44   fun κ => varNameStoreM (fun vns =>
45     match vns with
46       varNameStore n1 n2 n3 =>
47       let name := (rawLatexMath "\alpha_{")+++toLatexMath (toString n1)+++(rawLatexMath "}")
48         in (name,(varNameStore (S n1) n2 n3))
49     end).
50 Definition freshCoVarName : VarNameStoreM LatexMath :=
51   varNameStoreM (fun vns =>
52     match vns with
53       varNameStore n1 n2 n3 =>
54       let name := (rawLatexMath "\gamma_{")+++toLatexMath (toString n2)+++(rawLatexMath "}")
55         in (name,(varNameStore n1 (S n2) n3))
56     end).
57 Definition freshValVarName : VarNameStoreM LatexMath :=
58   varNameStoreM (fun vns =>
59     match vns with
60       varNameStore n1 n2 n3 =>
61       let vn := match n3 with
62                   | 0 => "x"
63                   | 1 => "y"
64                   | 2 => "z"
65                   | 3 => "a"
66                   | 4 => "b"
67                   | 5 => "c"
68                   | 6 => "d"
69                   | 7 => "e"
70                   | 8 => "f"
71                   | 9 => "g"
72                   | 10 => "h"
73                   | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++toString x+++"}"
74                 end
75       in let name := rawLatexMath ("x_{"+++vn+++"}")
76         in (name,(varNameStore n1 n2 (S n3)))
77     end).
78
79 Fixpoint typeToLatexMath (needparens:bool){κ}(t:RawHaskType (fun _ => LatexMath) κ) {struct t} : VarNameStoreM LatexMath :=
80   match t return VarNameStoreM LatexMath with
81   | TVar    _ v        => return toLatexMath v
82   | TCon    tc         => return ((rawLatexMath "\text{\tt{")+++toLatexMath (toString tc)+++(rawLatexMath "}}"))
83   | TArrow             => return rawLatexMath "\text{\tt{(->)}}"
84   | TCoerc _ t1 t2   t => bind t1' = typeToLatexMath false      t1
85                         ; bind t2' = typeToLatexMath false      t2
86                         ; bind t'  = typeToLatexMath needparens t
87                         ; return ((rawLatexMath "{(")+++t1'+++(rawLatexMath "{\sim}")+++
88                                    t2'+++(rawLatexMath ")}\Rightarrow{")+++t'+++(rawLatexMath "}"))
89   | TCode  ec t        => bind ec' = typeToLatexMath true ec
90                         ; bind t'  = typeToLatexMath false t
91                         ; return (rawLatexMath "\code{")+++ec'+++(rawLatexMath "}{")+++t'+++(rawLatexMath "}")
92   | TAll   k f         => bind alpha = freshTyVarName k
93                         ; bind t'    = typeToLatexMath false (f alpha)
94                         ; return (rawLatexMath "(\forall ")+++alpha+++(rawLatexMath "{:}")+++
95                         (kindToLatexMath k)+++(rawLatexMath ")")+++t'
96   | TApp  _ _  t1 t2   => match t1 return VarNameStoreM LatexMath with
97                 | TApp _ _ TArrow tx => bind t1' = typeToLatexMath true tx
98                                       ; bind t2' = typeToLatexMath true t2
99                                       ; let body := t1'+++(rawLatexMath "{\rightarrow}")+++t2'
100                                         in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
101                 | _                  => bind t1' = typeToLatexMath true t1
102                                       ; bind t2' = typeToLatexMath true t2
103                                       ; let body := t1'+++(rawLatexMath " ")+++t2'
104                                         in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
105                 end
106   | TyFunApp   tfc _ _ lt  => bind rest = typeListToRawLatexMath false lt
107                         ; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++
108                                  (rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++
109                                  (rawLatexMath "}")+++
110                                  (fold_left (fun x y => (rawLatexMath " \  ")+++x+++y)
111                                    rest (rawLatexMath ""))
112 end
113 with typeListToRawLatexMath (needparens:bool){κ}(t:RawHaskTypeList κ) {struct t} : VarNameStoreM (list LatexMath) :=
114 match t return VarNameStoreM (list LatexMath) with
115 | TyFunApp_nil                 => return nil
116 | TyFunApp_cons  κ kl rhk rhkl => bind r  = typeToLatexMath needparens rhk
117                                 ; bind rl = typeListToRawLatexMath needparens rhkl
118                                 ; return (r::rl)
119 end.
120
121 Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameStoreM LatexMath.
122   refine (
123   match t with
124     t' @@ lev =>
125     bind ite = _ ;
126     bind t'' = typeToLatexMath false (t' (fun _ => LatexMath) ite) ;
127     return match lev with
128     | nil => t''
129     | lv  => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++
130            (fold_left (fun x y => x+++(rawLatexMath ":")+++y)
131              (map (fun l:HaskTyVar Γ _ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
132     end
133     end); try apply ConcatenableLatexMath.
134     try apply VarNameMonad.
135     clear t t' lev κ.
136     induction Γ.
137     apply (return INil).
138     refine (bind tv' = freshTyVarName a ; _).
139     apply VarNameMonad.
140     refine (bind IHΓ' = IHΓ ; return _).
141     apply VarNameMonad.
142     apply ICons.
143     apply tv'.
144     apply IHΓ'.
145     apply VarNameMonad.
146     Defined.
147
148 Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
149   match match j return VarNameStoreM LatexMath with
150     | mkJudg Γ Δ Σ₁ Σ₂ l =>
151           bind Σ₁' = treeM (mapOptionTree ltypeToLatexMath Σ₁)
152         ; bind Σ₂' = treeM (mapOptionTree (fun t => ltypeToLatexMath (t@@l)) Σ₂)
153         ; return treeToLatexMath Σ₁' +++ (rawLatexMath "\vdash") +++ treeToLatexMath Σ₂'
154   end with
155     varNameStoreM f => fst (f (varNameStore 0 0 0))
156   end.
157
158 Instance ToLatexMathJudgment : ToLatexMath Judg :=
159   { toLatexMath := judgmentToRawLatexMath }.
160
161 Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
162   match r with
163     | ALeft   _ _ _ r => nd_uruleToRawLatexMath r
164     | ARight  _ _ _ r => nd_uruleToRawLatexMath r
165     | AId     _     => "Id"
166     | ACanL   _     => "CanL"
167     | ACanR   _     => "CanR"
168     | AuCanL  _     => "uCanL"
169     | AuCanR  _     => "uCanR"
170     | AAssoc  _ _ _ => "Assoc"
171     | AuAssoc  _ _ _ => "Cossa"
172     | AExch   _ _   => "Exch"
173     | AWeak   _     => "Weak"
174     | ACont   _     => "Cont"
175     | AComp   _ _ _ _ _  => "Comp"  (* FIXME: do a better job here *)
176   end.
177
178 Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
179   match r with
180     | RArrange      _ _ _ _ _ _ r     => nd_uruleToRawLatexMath r
181     | RNote         _ _ _ _ _ _       => "Note"
182     | RLit          _ _ _ _           => "Lit"
183     | RVar          _ _ _ _           => "Var"
184     | RGlobal       _ _ _ _ _         => "Global"
185     | RLam          _ _ _ _ _ _       => "Abs"
186     | RCast         _ _ _ _ _ _ _     => "Cast"
187     | RAbsT         _ _ _ _ _ _       => "AbsT"
188     | RAppT         _ _ _ _ _ _ _     => "AppT"
189     | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
190     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
191     | RApp          _ _ _ _ _ _ _     => "App"
192     | RCut          _ _ _ _ _ _ _ _   => "Cut"
193     | RLeft         _ _ _ _ _ _       => "Left"
194     | RRight        _ _ _ _ _ _       => "Right"
195     | RLetRec       _ _ _ _ _ _       => "LetRec"
196     | RCase         _ _ _ _ _ _ _ _   => "Case"
197     | RBrak         _ _ _ _ _ _       => "Brak"
198     | REsc          _ _ _ _ _ _       => "Esc"
199     | RVoid         _ _ _             => "RVoid"
200 end.
201
202 Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
203   match r with
204     | ALeft   _ _ _ r             => nd_hideURule r
205     | ARight  _ _ _ r             => nd_hideURule r
206     | ACanL   _                   => true
207     | ACanR   _                   => true
208     | AuCanL  _                   => true
209     | AuCanR  _                   => true
210     | AAssoc  _ _ _               => true
211     | AuAssoc  _ _ _               => true
212     | AExch      (T_Leaf None) b  => true
213     | AExch   a  (T_Leaf None)    => true
214     | AWeak      (T_Leaf None)    => true
215     | ACont      (T_Leaf None)    => true
216     | AComp   _ _ _ _ _           => false   (* FIXME: do better *)
217     | _                           => false
218   end.
219 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
220   match r with
221     | RArrange _    _ _ _ _ _ r => nd_hideURule r
222     | RVoid _  _ _         => true
223     | RLeft _ _ _ _  _ _         => true
224     | RRight _  _ _ _ _ _        => true
225     | _                         => false
226   end.
227
228 Instance ToLatexMathRule h c : ToLatexMath (Rule h c) :=
229   { toLatexMath := fun r => rawLatexMath (@nd_ruleToRawLatexMath h c r) }.
230
231 Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) :=
232 @SIND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
233   (mkSIND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).