X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=b787d3eaca3e2c70771f09e33b51dc45c30aa442;hp=7624c3153c444d1414b1223eb1429d2f7a36c5dd;hb=171beb27508a340b24ab14837e72451d0b500805;hpb=2ec43bc871b579bac89707988c4855ee1d6c8eda

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 7624c31..b787d3e 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -6,218 +6,230 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
-Require Import NaturalDeductionToLatex.
+Require Import NaturalDeductionContext.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskProof.
 Require Import HaskCoreTypes.
 
-(* escapifies any characters which might cause trouble for LaTeX *)
-Variable sanitizeForLatex    : string      -> string.        Extract Inlined Constant sanitizeForLatex      => "sanitizeForLatex".
 
-Open Scope string_scope.
-Section ToLatex.
 
-  Fixpoint kind2latex (k:Kind) : string :=
-    match k with
-    | KindType                     => "\star"
-    | KindTypeFunction KindType k2 => "\star\Rightarrow "+++kind2latex k2
-    | KindTypeFunction k1 k2       => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
-    | KindUnliftedType             => "\text{\tt{\#}}"
-    | KindUnboxedTuple             => "\text{\tt{(\#)}}"
-    | KindArgType                  => "\text{\tt{??}}"
-    | KindOpenType                 => "\text{\tt{?}}"
-    end.
-
-  Open Scope nat_scope.
-  Definition var2string (n:nat) :=
-    match n with
-      | 0 => "x"
-      | 1 => "y"
-      | 2 => "z"
-      | 3 => "a"
-      | 4 => "b"
-      | 5 => "c"
-      | 6 => "d"
-      | 7 => "e"
-      | 8 => "f"
-      | 9 => "g"
-      | 10 => "h"
-      | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++x+++"}"
-    end.
-  Close Scope nat_scope.
-
-  Definition tyvar2greek (n:nat) :=
-    match n with
-      | O => "\alpha"
-      | S O => "\beta"
-      | S (S O) => "\xi"
-      | S (S (S n)) => "\alpha_{"+++n+++"}"
-    end.
-
-  Definition covar2greek (n:nat) :=
-    "{\gamma_{"+++n+++"}}".
-
-  (* TODO: now that PHOAS tyvar-representation-types are kind-indexed, we can do some clever stuff here *)
-  Fixpoint type2latex (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
-    match t with
-    | TVar    _ v          => tyvar2greek v
-    | TCon    tc           => "\text{\tt{"+++sanitizeForLatex (toString tc) +++"}}"
-    | TCoerc _ t1 t2   t   => "{("+++type2latex false n t1+++"{\sim}"
-                                  +++type2latex false n t2+++")}\Rightarrow{"
-                                  +++type2latex needparens n t+++"}"
-    | TApp  _ _  t1 t2     =>
-      match t1 with
-        | TApp _ _ TArrow t1 =>
-                     if needparens
-                     then "("+++(type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)+++")"
-                     else (type2latex true n t1)+++"{\rightarrow}"+++(type2latex true n t2)
-        | _ =>
-                     if needparens
-                     then "("+++(type2latex true n t1)+++" "+++(type2latex false n t2)+++")"
-                     else (type2latex true n t1)+++" "+++(type2latex false n t2)
-      end
-    | TArrow => "\text{\tt{(->)}}"
-    | TAll   k f           => let alpha := tyvar2greek n
-                              in "(\forall "+++ alpha +++ "{:}"+++ kind2latex k +++")"+++
-                                   type2latex false (S n) (f n)
-    | TCode  ec t          => "\code{"+++(type2latex true n ec)+++"}{"+++(type2latex false n t)+++"}"
-    | TyFunApp   tfc lt    => "{\text{\tt{"+++sanitizeForLatex (toString tfc) +++"}}}"+++
-                              "_{"+++n+++"}"+++
-                              fold_left (fun x y => " \  "+++x+++y)
-                              (typeList2latex false n lt) ""
-  end
-  with typeList2latex (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
+Inductive VarNameStore :=
+  varNameStore : nat -> nat -> nat -> VarNameStore.
+Inductive VarNameStoreM {T} :=
+  varNameStoreM : (VarNameStore -> (T * VarNameStore)) -> VarNameStoreM.
+Implicit Arguments VarNameStoreM [ ].
+
+Open Scope nat_scope.
+Instance VarNameMonad : Monad VarNameStoreM :=
+{ returnM := fun _   x   => varNameStoreM (fun v => (x,v))
+; bindM   := fun _ _ x f =>
+  match x with
+    varNameStoreM xf =>
+  varNameStoreM (fun vns =>
+    match xf vns with
+      (x',vns') => match f x' with
+                     varNameStoreM fx' => fx' vns'
+                   end
+    end) end }.
+
+Definition freshTyVarName : Kind -> VarNameStoreM LatexMath :=
+  fun κ => varNameStoreM (fun vns =>
+    match vns with
+      varNameStore n1 n2 n3 =>
+      let name := (rawLatexMath "\alpha_{")+++toLatexMath (toString n1)+++(rawLatexMath "}")
+        in (name,(varNameStore (S n1) n2 n3))
+    end).
+Definition freshCoVarName : VarNameStoreM LatexMath :=
+  varNameStoreM (fun vns =>
+    match vns with
+      varNameStore n1 n2 n3 =>
+      let name := (rawLatexMath "\gamma_{")+++toLatexMath (toString n2)+++(rawLatexMath "}")
+        in (name,(varNameStore n1 (S n2) n3))
+    end).
+Definition freshValVarName : VarNameStoreM LatexMath :=
+  varNameStoreM (fun vns =>
+    match vns with
+      varNameStore n1 n2 n3 =>
+      let vn := match n3 with
+                  | 0 => "x"
+                  | 1 => "y"
+                  | 2 => "z"
+                  | 3 => "a"
+                  | 4 => "b"
+                  | 5 => "c"
+                  | 6 => "d"
+                  | 7 => "e"
+                  | 8 => "f"
+                  | 9 => "g"
+                  | 10 => "h"
+                  | S (S (S (S (S (S (S (S (S (S (S x)))))))))) => "z_{"+++toString x+++"}"
+                end
+      in let name := rawLatexMath ("x_{"+++vn+++"}")
+        in (name,(varNameStore n1 n2 (S n3)))
+    end).
+
+Fixpoint typeToLatexMath (needparens:bool){κ}(t:RawHaskType (fun _ => LatexMath) κ) {struct t} : VarNameStoreM LatexMath :=
+  match t return VarNameStoreM LatexMath with
+  | TVar    _ v        => return toLatexMath v
+  | TCon    tc         => return ((rawLatexMath "\text{\tt{")+++toLatexMath (toString tc)+++(rawLatexMath "}}"))
+  | TArrow             => return rawLatexMath "\text{\tt{(->)}}"
+  | TCoerc _ t1 t2   t => bind t1' = typeToLatexMath false      t1
+                        ; bind t2' = typeToLatexMath false      t2
+                        ; bind t'  = typeToLatexMath needparens t
+                        ; return ((rawLatexMath "{(")+++t1'+++(rawLatexMath "{\sim}")+++
+                                   t2'+++(rawLatexMath ")}\Rightarrow{")+++t'+++(rawLatexMath "}"))
+  | TCode  ec t        => bind ec' = typeToLatexMath true ec
+                        ; bind t'  = typeToLatexMath false t
+                        ; return (rawLatexMath "\code{")+++ec'+++(rawLatexMath "}{")+++t'+++(rawLatexMath "}")
+  | TAll   k f         => bind alpha = freshTyVarName k
+                        ; bind t'    = typeToLatexMath false (f alpha)
+                        ; return (rawLatexMath "(\forall ")+++alpha+++(rawLatexMath "{:}")+++
+                        (kindToLatexMath k)+++(rawLatexMath ")")+++t'
+  | TApp  _ _  t1 t2   => match t1 return VarNameStoreM LatexMath with
+                | TApp _ _ TArrow tx => bind t1' = typeToLatexMath true tx
+                                      ; bind t2' = typeToLatexMath true t2
+                                      ; let body := t1'+++(rawLatexMath "{\rightarrow}")+++t2'
+                                        in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
+                | _                  => bind t1' = typeToLatexMath true t1
+                                      ; bind t2' = typeToLatexMath true t2
+                                      ; let body := t1'+++(rawLatexMath " ")+++t2'
+                                        in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
+                end
+  | TyFunApp   tfc _ _ lt  => bind rest = typeListToRawLatexMath false lt
+                        ; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++
+                                 (rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++
+                                 (rawLatexMath "}")+++
+                                 (fold_left (fun x y => (rawLatexMath " \  ")+++x+++y)
+                                   rest (rawLatexMath ""))
+end
+with typeListToRawLatexMath (needparens:bool){κ}(t:RawHaskTypeList κ) {struct t} : VarNameStoreM (list LatexMath) :=
+match t return VarNameStoreM (list LatexMath) with
+| TyFunApp_nil                 => return nil
+| TyFunApp_cons  κ kl rhk rhkl => bind r  = typeToLatexMath needparens rhk
+                                ; bind rl = typeListToRawLatexMath needparens rhkl
+                                ; return (r::rl)
+end.
+
+Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameStoreM LatexMath.
+  refine (
   match t with
-  | TyFunApp_nil                 => nil
-  | TyFunApp_cons  κ kl rhk rhkl => (type2latex needparens n rhk)::(typeList2latex needparens n rhkl)
+    t' @@ lev =>
+    bind ite = _ ;
+    bind t'' = typeToLatexMath false (t' (fun _ => LatexMath) ite) ;
+    return match lev with
+    | nil => t''
+    | lv  => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++
+           (fold_left (fun x y => x+++(rawLatexMath ":")+++y)
+             (map (fun l:HaskTyVar Γ _ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
+    end
+    end); try apply ConcatenableLatexMath.
+    try apply VarNameMonad.
+    clear t t' lev κ.
+    induction Γ.
+    apply (return INil).
+    refine (bind tv' = freshTyVarName a ; _).
+    apply VarNameMonad.
+    refine (bind IHΓ' = IHΓ ; return _).
+    apply VarNameMonad.
+    apply ICons.
+    apply tv'.
+    apply IHΓ'.
+    apply VarNameMonad.
+    Defined.
+
+Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
+  match match j return VarNameStoreM LatexMath with
+    | mkJudg Γ Δ Σ₁ Σ₂ l =>
+          bind Σ₁' = treeM (mapOptionTree ltypeToLatexMath Σ₁)
+        ; bind Σ₂' = treeM (mapOptionTree (fun t => ltypeToLatexMath (t@@l)) Σ₂)
+        ; return treeToLatexMath Σ₁' +++ (rawLatexMath "\vdash") +++ treeToLatexMath Σ₂'
+  end with
+    varNameStoreM f => fst (f (varNameStore 0 0 0))
   end.
 
-  Definition ltype2latex {Γ:TypeEnv}{κ}(t:RawHaskType (fun _ => nat) κ)(lev:list nat) : string :=
-    match lev with
-      | nil => type2latex false O t
-      | lv  => "{"+++type2latex true O t+++"}^{"+++(fold_left (fun x y => x+++":"+++y) (map tyvar2greek lv) "")+++"}"
-    end.
-
-  Fixpoint enumerate' (n:nat){T:Type}(l:list T) : list (nat * T) :=
-    match l with
-      | nil    => nil
-      | (a::b) => (n,a)::(enumerate' (S n) b)
-    end.
-
-  Definition enumerate {T:Type}(l:list T) := enumerate' O l.
-
-  Fixpoint count (n:nat) : vec nat n :=
-  match n with
-    | O    => vec_nil
-    | S n' => n':::(count n')
+Instance ToLatexMathJudgment : ToLatexMath Judg :=
+  { toLatexMath := judgmentToRawLatexMath }.
+
+Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
+  match r with
+    | ALeft   _ _ _ r => nd_uruleToRawLatexMath r
+    | ARight  _ _ _ r => nd_uruleToRawLatexMath r
+    | AId     _     => "Id"
+    | ACanL   _     => "CanL"
+    | ACanR   _     => "CanR"
+    | AuCanL  _     => "uCanL"
+    | AuCanR  _     => "uCanR"
+    | AAssoc  _ _ _ => "Assoc"
+    | AuAssoc  _ _ _ => "Cossa"
+    | AExch   _ _   => "Exch"
+    | AWeak   _     => "Weak"
+    | ACont   _     => "Cont"
+    | AComp   _ _ _ _ _  => "Comp"  (* FIXME: do a better job here *)
   end.
 
-  Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
-  match lk as LK return IList _ _ LK with
-    | nil    => INil
-    | h::t   => n::::(count' t (S n))
+Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
+  match r with
+    | RArrange      _ _ _ _ _ _ r     => nd_uruleToRawLatexMath r
+    | RNote         _ _ _ _ _ _       => "Note"
+    | RLit          _ _ _ _           => "Lit"
+    | RVar          _ _ _ _           => "Var"
+    | RGlobal       _ _ _ _ _         => "Global"
+    | RLam          _ _ _ _ _ _       => "Abs"
+    | RCast         _ _ _ _ _ _ _     => "Cast"
+    | RAbsT         _ _ _ _ _ _       => "AbsT"
+    | RAppT         _ _ _ _ _ _ _     => "AppT"
+    | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
+    | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
+    | RApp          _ _ _ _ _ _ _     => "App"
+    | RLet          _ _ _ _ _ _ _     => "Let"
+    | RCut          _ _ _ _ _ _ _     => "Cut"
+    | RLeft         _ _ _ _ _ _       => "Left"
+    | RRight        _ _ _ _ _ _       => "Right"
+    | RWhere        _ _ _ _ _ _ _ _   => "Where"
+    | RLetRec       _ _ _ _ _ _       => "LetRec"
+    | RCase         _ _ _ _ _ _ _ _   => "Case"
+    | RBrak         _ _ _ _ _ _       => "Brak"
+    | REsc          _ _ _ _ _ _       => "Esc"
+    | RVoid         _ _ _             => "RVoid"
+end.
+
+Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
+  match r with
+    | ALeft   _ _ _ r             => nd_hideURule r
+    | ARight  _ _ _ r             => nd_hideURule r
+    | ACanL   _                   => true
+    | ACanR   _                   => true
+    | AuCanL  _                   => true
+    | AuCanR  _                   => true
+    | AAssoc  _ _ _               => true
+    | AuAssoc  _ _ _               => true
+    | AExch      (T_Leaf None) b  => true
+    | AExch   a  (T_Leaf None)    => true
+    | AWeak      (T_Leaf None)    => true
+    | ACont      (T_Leaf None)    => true
+    | AComp   _ _ _ _ _           => false   (* FIXME: do better *)
+    | _                           => false
   end.
-
-  Definition InstantiatedTypeEnvString     Γ   : @InstantiatedTypeEnv     (fun _ => nat) Γ := count' Γ O.
-  Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv (fun _ => nat) nat Γ Δ  := count (length Δ).
-  Definition judgment2latex (j:Judg) : string :=
-      match j with
-        | mkJudg Γ Δ  a b =>
-          let Γ' := InstantiatedTypeEnvString Γ in
-          let Δ' := InstantiatedCoercionEnvString Γ Δ in
-          let lt2l := fun nt:nat*(LeveledHaskType Γ ★) => 
-            let (n,lt) := nt in
-              match lt with
-                t @@ l =>
-                (var2string n)+++"{:}"+++(@ltype2latex Γ _ (t (fun _ => nat) Γ')
-                  (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
-              end in
-          let lt2l' := fun lt:(LeveledHaskType Γ ★) => 
-              match lt with
-                t @@ l =>
-                "e{:}"+++(@ltype2latex Γ _ (t (fun _ => nat) Γ')
-                  (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
-              end in
-          (list2latex "" lt2l "\ ,\ " (enumerate (leaves a)))
-          +++" \ \vdash_e\  "(*+++"e{:}"*)
-          +++(list2latex "" lt2l' "\ ,\ " (leaves b))
-      end.
-
-  Definition j2l (j2j:Judg -> Judg) jt :=
-    @judgments2latex Judg judgment2latex (mapOptionTree j2j jt).
-
-  Fixpoint nd_urule2latex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
-    match r with
-      | RLeft   _ _ _ r => nd_urule2latex r
-      | RRight  _ _ _ r => nd_urule2latex r
-      | RCanL   _ _     => "CanL"
-      | RCanR   _ _     => "CanR"
-      | RuCanL  _ _     => "uCanL"
-      | RuCanR  _ _     => "uCanR"
-      | RAssoc  _ _ _ _ => "Assoc"
-      | RCossa  _ _ _ _ => "Cossa"
-      | RExch   _ _ _   => "Exch"
-      | RWeak   _ _     => "Weak"
-      | RCont   _ _     => "Cont"
-    end.
-
-  Fixpoint nd_rule2latex {h}{c}(r:Rule h c) : string :=
-    match r with
-      | RURule        _ _ _ _ r         => nd_urule2latex r
-      | RNote         _ _ _             => "Note"
-      | RLit          _ _ _ _           => "Lit"
-      | RVar          _ _ _ _           => "Var"
-      | RLam          _ _ _ _ _ _       => "Abs"
-      | RCast         _ _ _ _ _ _ _     => "Cast"
-      | RAbsT         _ _ _ _ _ _       => "AbsT"
-      | RAppT         _ _ _ _ _ _ _     => "AppT"
-      | RAppCo        _ _ _ _ _ _ _ _ _ => "AppCo"
-      | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
-      | RApp          _ _ _ _ _ _ _     => "App"
-      | RLet          _ _ _ _ _ _ _     => "Let"
-      | RBindingGroup _ _ _ _ _ _       => "RBindingGroup"
-      | RLetRec       _ _ _ _ _         => "LetRec"
-      | RCase         _ _ _ _ _ _ _ _   => "Case"
-      | RBrak         _ _ _ _ _ _       => "Brak"
-      | REsc          _ _ _ _ _ _       => "Esc"
-      | REmptyGroup   _ _               => "REmptyGroup"
+Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
+  match r with
+    | RArrange _    _ _ _ _ _ r => nd_hideURule r
+    | RVoid _  _ _         => true
+    | RLeft _ _ _ _  _ _         => true
+    | RRight _  _ _ _ _ _        => true
+    | _                         => false
   end.
 
-  Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
-    match r with
-      | RLeft   _ _ _ r               => nd_hideURule r
-      | RRight  _ _ _ r               => nd_hideURule r
-      | RCanL   _ _                   => true
-      | RCanR   _ _                   => true
-      | RuCanL  _ _                   => true
-      | RuCanR  _ _                   => true
-      | RAssoc  _ _ _ _               => true
-      | RCossa  _ _ _ _               => true
-      | RExch   _    (T_Leaf None) b  => true
-      | RExch   _ a  (T_Leaf None)    => true
-      | RWeak   _    (T_Leaf None)    => true
-      | RCont   _    (T_Leaf None)    => true
-      | _                             => false
-    end.
-  Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
-    match r with
-      | RURule        _ _ _ _ r   => nd_hideURule r
-      | REmptyGroup   _ _         => true
-      | RBindingGroup _ _ _ _ _ _ => true
-      | _                         => false
-    end.
-End ToLatex.
+Instance ToLatexMathRule h c : ToLatexMath (Rule h c) :=
+  { toLatexMath := fun r => rawLatexMath (@nd_ruleToRawLatexMath h c r) }.
 
-Definition nd_ml_toLatex {c}(pf:@ND _ Rule [] c) :=
-  @SCND_toLatex _ _
-      judgment2latex
-      (fun h c r => @nd_rule2latex h c r)
-      (fun h c r => @nd_hideRule h c r)
-      _ _ (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).
+Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) :=
+@SIND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
+  (mkSIND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).