remove RJoin rule

[coq-hetmet.git] / src / HaskProofToLatex.v

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index be5cb31..b787d3e 100644 (file)
--- 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 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 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.
 
 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
-    | KindStar                     => "\star"
-    | KindArrow KindStar k2 => "\star\Rightarrow "+++kind2latex k2
-    | KindArrow 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
   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.
 
   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.
 
   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.
   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.
 
   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 [])).