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.
-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
- | 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.
- 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.
- 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"
+ | 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.
+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 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 [])).
projects / coq-hetmet.git / blobdiff