clean up demo code

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

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index fab70fe..716a983 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -6,225 +6,228 @@ 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.
 

-Open Scope string_scope.
-Section HaskProofToLatex.

 
 

-  Context {TV:Kind -> Type}.
-  Context {TVLatex:forall k, ToLatex (TV k)}.
-  Context {freshM:FreshMonad (∀ κ, TV κ)}.
-  Definition FreshM' := FMT freshM.
-  Instance FreshMon' : Monad FreshM' := FMT_Monad freshM.
-  
-  Instance ToLatexTyCon : ToLatex TyCon.
-    admit.
-    Defined.

 
 

-  Fixpoint typeToLatex (needparens:bool){κ}(t:RawHaskType TV κ) {struct t} : FMT freshM Latex :=
-    match t with
-    | TVar    _ v        => return toLatex v
-    | TCon    tc         => return (latex "\text{\tt{")+=+tc+=+(latex "}}")
-    | TArrow             => return latex "\text{\tt{(->)}}"
-    | TCoerc _ t1 t2   t => bind t1' = typeToLatex false      t1
-                          ; bind t2' = typeToLatex false      t2
-                          ; bind t'  = typeToLatex needparens t
-                          ; return (latex "{(")+=+t1'+=+(latex "{\sim}")+=+
-                                     t2'+=+(latex ")}\Rightarrow{")+=+t'+=+(latex "}")
-    | TApp  _ _  t1 t2   => match t1 with
-                            | TApp _ _ TArrow tx => bind t1' = typeToLatex true tx
-                                                  ; bind t2' = typeToLatex true t2
-                                                  ; let body := t1'+=+(latex "{\rightarrow}")+=+t2'
-                                                    in return if needparens then (latex "(")+=+body+=+(latex ")") else body
-                            | _                  => bind t1' = typeToLatex true t1
-                                                  ; bind t2' = typeToLatex true t2
-                                                  ; let body := t1'+=+(latex " ")+=+t2'
-                                                    in return if needparens then (latex "(")+=+body+=+(latex ")") else body
-                         end
-    | TCode  ec t        => bind ec' = typeToLatex true ec
-                          ; bind t'  = typeToLatex false t
-                          ; return (latex "\code{")+=+ec'+=+(latex "}{")+=+t'+=+(latex "}")
-    | TyFunApp   tfc lt  => bind rest = typeListToLatex false lt
-                          ; return (latex "{\text{\tt{")+=+(sanitizeForLatex (toString tfc))+=+(latex "}}}")+=+
-                                   (*(latex "_{")+=+(latex (toString (tfc:nat)))+=+(latex "}")+=+*)
-                                   (fold_left (fun x y => (latex " \  ")+=+x+=+y)
-                                     rest (latex ""))
-    | TAll   k f         => (*bind alpha = next
-                          ; bind t'    = typeToLatex false (f (alpha k))
-                          ; *)return (latex "(\forall ")(*+=+(@toLatex _ (TVLatex k) (alpha k))*)
-                          +=+(latex "{:}")+=+(kindToLatex k)+=+(latex ")")(*+=+t'*)
-  end
-  with typeListToLatex (needparens:bool){κ}(t:RawHaskTypeList κ) {struct t} : FreshM' (list Latex) :=
+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                 => return nil
-  | TyFunApp_cons  κ kl rhk rhkl => bind r  = typeToLatex needparens rhk
-                                  ; bind rl = typeListToLatex needparens rhkl
-                                  ; return (r::rl)
-  end.
-(*
-  Definition ltypeToLatex {Γ:TypeEnv}{κ}(t:RawHaskType TV κ)(lev:list nat) : FreshM' Latex :=
-    match lev with
-      | nil => typeToLatex false t
-      | lv  => bind t' = typeToLatex true t
-             ; 
-        (latex "{")
-        +=+
-        
-        +=+
-        (latex "}^{")
-        +=+
-        (fold_left (fun x y => x+=+":"+=+y) (map tyvar2greek lv) "")+=+"}"
-    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 covar2greek (n:nat) :=
-    "{\gamma_{"+++n+++"}}".
-
-  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.
+    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.

 
 

-  Fixpoint count (n:nat) : vec nat n :=
-  match n with
-    | O    => vec_nil
-    | S n' => n':::(count n')
+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.
 

-  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))
+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.
 

-  Definition InstantiatedTypeEnvString     Γ   : @InstantiatedTypeEnv     (fun _ => nat) Γ := count' Γ O.
-  Definition InstantiatedCoercionEnvString Γ Δ : @InstantiatedCoercionEnv (fun _ => nat) nat Γ Δ  := count (length Δ).
-  Definition judgmentToLatex (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)+++"{:}"+++(@ltypeToLatex Γ _ (t (fun _ => nat) Γ')
-                  (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
-              end in
-          let lt2l' := fun lt:(LeveledHaskType Γ ★) => 
-              match lt with
-                t @@ l =>
-                (@ltypeToLatex Γ _ (t (fun _ => nat) Γ')
-                  (map (fun x:HaskTyVar Γ _ => x (fun _ => nat) Γ') l))
-              end in
-          (listToLatex "" lt2l "\ ,\ " (enumerate (leaves a)))
-          +++" \ \vdash_e\  "(*+++"e{:}"*)
-          +++(listToLatex "" lt2l' "\ ,\ " (leaves b))
-      end.
-
-  Definition j2l (j2j:Judg -> Judg) jt :=
-    @judgmentsToLatex Judg judgmentToLatex (mapOptionTree j2j jt).
-
-  Fixpoint nd_uruleToLatex {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
-    match r with
-      | RLeft   _ _ _ r => nd_uruleToLatex r
-      | RRight  _ _ _ r => nd_uruleToLatex r
-      | RCanL   _ _     => "CanL"
-      | RCanR   _ _     => "CanR"
-      | RuCanL  _ _     => "uCanL"
-      | RuCanR  _ _     => "uCanR"
-      | RAssoc  _ _ _ _ => "Assoc"
-      | RCossa  _ _ _ _ => "Cossa"
-      | RExch   _ _ _   => "Exch"
-      | RWeak   _ _     => "Weak"
-      | RCont   _ _     => "Cont"
-    end.
-
-  Fixpoint nd_ruleToLatex {h}{c}(r:Rule h c) : string :=
-    match r with
-      | RURule        _ _ _ _ r         => nd_uruleToLatex 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"
-      | RBindingGroup _ _ _ _ _ _       => "RBindingGroup"
-      | RLetRec       _ _ _ _ _ _       => "LetRec"
-      | RCase         _ _ _ _ _ _ _ _   => "Case"
-      | RBrak         _ _ _ _ _ _       => "Brak"
-      | REsc          _ _ _ _ _ _       => "Esc"
-      | REmptyGroup   _ _               => "REmptyGroup"
+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"
+    | RCut          _ _ _ _ _ _ _ _   => "Cut"
+    | RLeft         _ _ _ _ _ _       => "Left"
+    | RRight        _ _ _ _ _ _       => "Right"
+    | 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.
+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 HaskProofToLatex.
+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 _ _
-      judgmentToLatex
-      (fun h c r => @nd_ruleToLatex h c r)
-      (fun h c r => @nd_hideRule h c r)
-      _ _ (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).
-*)
\ No newline at end of file
+Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) :=
+@SIND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
+  (mkSIND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).