Definition Δ : CoercionEnv Γ := nil.
Definition φ : TyVarResolver Γ :=
- fun cv => Error ("unbound tyvar: " +++ (cv:CoreVar)).
+ fun cv => Error ("unbound tyvar: " +++ toString (cv:CoreVar)).
(*fun tv => error ("tried to get the representative of an unbound tyvar:" +++ (getCoreVarOccString tv)).*)
Definition ψ : CoVarResolver Γ Δ :=
eol.
- Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string := Error "Temporarily Disabled".
-(*
- addErrorMessage ("input CoreSyn: " +++ ce)
- (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
+ Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
+ addErrorMessage ("input CoreSyn: " +++ toString ce)
+ (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
coreExprToWeakExpr ce >>= fun we =>
- addErrorMessage ("WeakExpr: " +++ we)
- ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
+ addErrorMessage ("WeakExpr: " +++ toString we)
+ ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
((weakTypeOfWeakExpr we) >>= fun t =>
- (addErrorMessage ("WeakType: " +++ t)
+ (addErrorMessage ("WeakType: " +++ toString t)
((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
- addErrorMessage ("HaskType: " +++ τ)
+ addErrorMessage ("HaskType: " +++ toString τ)
((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => false) τ nil we) >>= fun e =>
- OK (eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e)+++"$$"+++eol)
- )))))))).*)
+ OK (eol+++"$$"+++ toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++"$$"+++eol)
+ )))))))).
Definition coreToStringExpr (ce:@CoreExpr CoreVar) : string :=
match coreToStringExpr' ce with
eapply nd_rule.
eapply RLam.
Defined.
-(*
- Definition TInt : HaskType nil ★.
- assert (tyConKind' intPrimTyCon = ★).
- rewrite <- H.
- unfold HaskType; intros.
- apply TCon.
- Defined.
-
- Definition idproof1 : ND Rule [] [nil > nil > [TInt @@ nil] |- [TInt @@ nil]].
- apply nd_rule.
- apply RVar.
- Defined.
-
- Definition idtype :=
- HaskTAll(Γ:=nil) ★ (fun TV ite tv => (TApp (TApp TArrow (TVar tv)) (TVar tv))).
- Definition idproof : ND Rule [] [nil > nil > [] |- [idtype @@ nil]].
- eapply nd_comp; [ idtac | eapply nd_rule ; eapply RAbsT ].
- apply idproof0.
- Defined.
-*)
(*
Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
- addErrorMessage ("input CoreSyn: " +++ ce)
- (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
+ addErrorMessage ("input CoreSyn: " +++ toString ce)
+ (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
coreExprToWeakExpr ce >>= fun we =>
- addErrorMessage ("WeakExpr: " +++ we)
- ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
+ addErrorMessage ("WeakExpr: " +++ toString we)
+ ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
((weakTypeOfWeakExpr we) >>= fun t =>
- (addErrorMessage ("WeakType: " +++ t)
+ (addErrorMessage ("WeakType: " +++ toString t)
((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
- addErrorMessage ("HaskType: " +++ τ)
+ addErrorMessage ("HaskType: " +++ toString τ)
((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
(let haskProof := @expr2proof _ _ _ _ _ _ e
in (* insert HaskProof-to-HaskProof manipulations here *)
INil
>>= fun q => Error (toString q)
))))))))).
-*)
-*)
+*)*)
+
Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
- addErrorMessage ("input CoreSyn: " +++ ce)
- (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
+ addErrorMessage ("input CoreSyn: " +++ toString ce)
+ (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) (
coreExprToWeakExpr ce >>= fun we =>
- addErrorMessage ("WeakExpr: " +++ we)
- ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
+ addErrorMessage ("WeakExpr: " +++ toString we)
+ ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we)))
((weakTypeOfWeakExpr we) >>= fun t =>
- (addErrorMessage ("WeakType: " +++ t)
+ (addErrorMessage ("WeakType: " +++ toString t)
((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
Class ToString (T:Type) := { toString : T -> string }.
Instance StringToString : ToString string := { toString := fun x => x }.
-Notation "a +++ b" := (append (toString a) (toString b)) (at level 100).
+Class Concatenable {T:Type} :=
+ { concatenate : T -> T -> T }.
+ Implicit Arguments Concatenable [ ].
+Open Scope string_scope.
+Open Scope type_scope.
+Close Scope list_scope.
+Notation "a +++ b" := (@concatenate _ _ a b) (at level 99).
+Instance ConcatenableString : Concatenable string := { concatenate := append }.
+
(*******************************************************************************)
(* Trees *)
simpl; rewrite IHt1; rewrite IHt2; auto.
Qed.
-Open Scope string_scope.
Fixpoint treeToString {T}{TT:ToString T}(t:Tree ??T) : string :=
match t with
| T_Leaf None => "[]"
- | T_Leaf (Some s) => "["+++s+++"]"
+ | T_Leaf (Some s) => "["+++toString s+++"]"
| T_Branch b1 b2 => treeToString b1 +++ ",," +++ treeToString b2
end.
Instance TreeToString {T}{TT:ToString T} : ToString (Tree ??T) := { toString := treeToString }.
-CoInductive Fresh A T :=
-{ next : forall a:A, (T a * Fresh A T)
-; split : Fresh A T * Fresh A T
-}.
end.
Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
-Open Scope string_scope.
Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg :=
match oe with
| Error s => Error (err_msg +++ eol +++ " " +++ s)
admit.
Defined.
+
+Fixpoint mapM {M}{mon:Monad M}{T}(ml:list (M T)) : M (list T) :=
+ match ml with
+ | nil => return nil
+ | a::b => bind a' = a ; bind b' = mapM b ; return a'::b'
+ end.
+
+Fixpoint list_to_ilist {T}{F}(f:forall t:T, F t) (l:list T) : IList T F l :=
+ match l as L return IList T F L with
+ | nil => INil
+ | a::b => ICons a b (f a) (list_to_ilist f b)
+ end.
+
+Fixpoint treeM {T}{M}{MT:Monad M}(t:Tree ??(M T)) : M (Tree ??T) :=
+ match t with
+ | T_Leaf None => return []
+ | T_Leaf (Some x) => bind x' = x ; return [x']
+ | T_Branch b1 b2 => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
+ end.
+
+
(* escapifies any characters which might cause trouble for LaTeX *)
Variable sanitizeForLatex : string -> string.
Extract Inlined Constant sanitizeForLatex => "sanitizeForLatex".
-Inductive Latex : Type := latex : string -> Latex.
-Instance LatexToString : ToString Latex := { toString := fun x => match x with latex s => s end }.
-Class ToLatex (T:Type) := { toLatex : T -> Latex }.
-Instance StringToLatex : ToLatex string := { toLatex := fun x => latex (sanitizeForLatex x) }.
-Instance LatexToLatex : ToLatex Latex := { toLatex := fun x => x }.
-Definition concatLatex {T1}{T2}(l1:T1)(l2:T2){L1:ToLatex T1}{L2:ToLatex T2} : Latex :=
- match toLatex l1 with
- latex s1 =>
- match toLatex l2 with
- latex s2 =>
- latex (s1 +++ s2)
- end
- end.
-Notation "a +=+ b" := (concatLatex a b) (at level 60, right associativity).
-
-
+Inductive Latex : Type := rawLatex : string -> Latex.
+Inductive LatexMath : Type := rawLatexMath : string -> LatexMath.
+Class ToLatex (T:Type) := { toLatex : T -> Latex }.
+Instance ConcatenableLatex : Concatenable Latex :=
+ { concatenate := fun l1 l2 => match l1 with rawLatex l1' => match l2 with rawLatex l2' => rawLatex (l1'+++l2') end end }.
+Instance LatexToString : ToString Latex := { toString := fun x => match x with rawLatex s => s end }.
+
+Class ToLatexMath (T:Type) := { toLatexMath : T -> LatexMath }.
+Instance ConcatenableLatexMath : Concatenable LatexMath :=
+ { concatenate := fun l1 l2 =>
+ match l1 with rawLatexMath l1' =>
+ match l2 with rawLatexMath l2' => rawLatexMath (l1'+++l2')
+ end end }.
+Instance LatexMathToString : ToString LatexMath := { toString := fun x => match x with rawLatexMath s => s end }.
+
+Instance ToLatexLatexMath : ToLatex LatexMath := { toLatex := fun l => rawLatex ("$"+++toString l+++"$") }.
+Instance ToLatexMathLatex : ToLatexMath Latex := { toLatexMath := fun l => rawLatexMath ("\text{"+++toString l+++"}") }.
+
+Instance StringToLatex : ToLatex string := { toLatex := fun x => rawLatex (sanitizeForLatex x) }.
+Instance StringToLatexMath : ToLatexMath string := { toLatexMath := fun x => toLatexMath (toLatex x) }.
+Instance LatexToLatex : ToLatex Latex := { toLatex := fun x => x }.
+Instance LatexMathToLatexMath : ToLatexMath LatexMath := { toLatexMath := fun x => x }.
+
+Fixpoint treeToLatexMath {V}{ToLatexV:ToLatexMath V}(t:Tree ??V) : LatexMath :=
+ match t with
+ | T_Leaf None => rawLatexMath "\langle\rangle"
+ | T_Leaf (Some x) => (rawLatexMath "\langle")+++toLatexMath x+++(rawLatexMath "\rangle")
+ | T_Branch b1 b2 => (rawLatexMath "\langle")+++treeToLatexMath b1+++(rawLatexMath " , ")
+ +++treeToLatexMath b2+++(rawLatexMath "\rangle")
+ end.
| WExprVar _ => Error "encountered expression variable in a modal box type"
| WCoerVar _ => Error "encountered coercion variable in a modal box type"
end
- | _ => Error ("mis-applied modal box tycon: " +++ ct)
+ | _ => Error ("mis-applied modal box tycon: " +++ toString ct)
end
else let tc' := if eqd_dec tc ArrowTyCon
then WFunTyCon
match wt with
| WTyCon tc => OK (tc,acc)
| WAppTy t1 t2 => expectTyConApp t1 (t2::acc)
- | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ wt)
- | _ => Error ("expectTyConApp encountered " +++ wt)
+ | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ toString wt)
+ | _ => Error ("expectTyConApp encountered " +++ toString wt)
end.
Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
Notation "'★'" := KindStar.
Notation "a ⇛ b" := (KindArrow a b).
-Fixpoint kindToLatex (k:Kind) : Latex :=
+Fixpoint kindToLatexMath (k:Kind) : LatexMath :=
match k with
- | ★ => latex "\star"
- | ★ ⇛ k2 => (latex "\star\Rightarrow ")+=+kindToLatex k2
- | k1 ⇛ k2 => (latex "(")+=+kindToLatex k1+=+(latex ")\Rightarrow ")+=+kindToLatex k2
- | KindUnliftedType => latex "\text{\tt{\#}}"
- | KindUnboxedTuple => latex "\text{\tt{(\#)}}"
- | KindArgType => latex "\text{\tt{??}}"
- | KindOpenType => latex "\text{\tt{?}}"
+ | ★ => rawLatexMath "\star"
+ | ★ ⇛ k2 => (rawLatexMath "\star\Rightarrow ")+++kindToLatexMath k2
+ | k1 ⇛ k2 => (rawLatexMath "(")+++kindToLatexMath k1+++(rawLatexMath ")\Rightarrow ")+++kindToLatexMath k2
+ | KindUnliftedType => rawLatexMath "\text{\tt{\#}}"
+ | KindUnboxedTuple => rawLatexMath "\text{\tt{(\#)}}"
+ | KindArgType => rawLatexMath "\text{\tt{??}}"
+ | KindOpenType => rawLatexMath "\text{\tt{?}}"
end.
-Instance KindToLatex : ToLatex Kind := { toLatex := kindToLatex }.
+Instance KindToLatexMath : ToLatexMath Kind := { toLatexMath := kindToLatexMath }.
Instance KindEqDecidable : EqDecidable Kind.
apply Build_EqDecidable.
Variable tyFunToString : TyFun -> string. Extract Inlined Constant tyFunToString => "outputableToString".
Instance TyConToString : ToString TyCon := { toString := tyConToString }.
Instance TyFunToString : ToString TyFun := { toString := tyFunToString }.
-Instance TyConToLatex : ToLatex TyCon := { toLatex := fun x => latex (sanitizeForLatex (toString x)) }.
-Instance TyFunToLatex : ToLatex TyCon := { toLatex := fun x => latex (sanitizeForLatex (toString x)) }.
+Instance TyConToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }.
+Instance TyFunToLatex : ToLatex TyCon := { toLatex := fun x => toLatex (toString x) }.
Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".
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.
-
- 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)
+ 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 Γ Δ Σ₁ Σ₂ =>
+ bind Σ₁' = treeM (mapOptionTree ltypeToLatexMath Σ₁)
+ ; bind Σ₂' = treeM (mapOptionTree ltypeToLatexMath Σ₂)
+ ; return treeToLatexMath Σ₁' +++ (rawLatexMath "\vdash") +++ treeToLatexMath Σ₂'
+ end with
+ varNameStoreM f => fst (f (varNameStore 0 0 0))
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.
- 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 {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
+ match r with
+ | RLeft _ _ _ r => nd_uruleToRawLatexMath r
+ | RRight _ _ _ r => nd_uruleToRawLatexMath r
+ | RCanL _ _ => "CanL"
+ | RCanR _ _ => "CanR"
+ | RuCanL _ _ => "uCanL"
+ | RuCanR _ _ => "uCanR"
+ | RAssoc _ _ _ _ => "Assoc"
+ | RCossa _ _ _ _ => "Cossa"
+ | RExch _ _ _ => "Exch"
+ | RWeak _ _ => "Weak"
+ | RCont _ _ => "Cont"
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
+ | RURule _ _ _ _ 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"
+ | RBindingGroup _ _ _ _ _ _ => "RBindingGroup"
+ | RLetRec _ _ _ _ _ _ => "LetRec"
+ | RCase _ _ _ _ _ _ _ _ => "Case"
+ | RBrak _ _ _ _ _ _ => "Brak"
+ | REsc _ _ _ _ _ _ => "Esc"
+ | REmptyGroup _ _ => "REmptyGroup"
+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.
-
- 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_hideRule {h}{c}(r:Rule h c) : bool :=
+ match r with
+ | RURule _ _ _ _ r => nd_hideURule r
+ | REmptyGroup _ _ => true
+ | RBindingGroup _ _ _ _ _ _ => 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) :=
+@SCND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
+ (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).
admit.
Defined.
- Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) :=
- match t with
- | T_Leaf None => return []
- | T_Leaf (Some x) => bind x' = x ; return [x']
- | T_Branch b1 b2 => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
- end.
-
Definition gather_branch_variables
Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
ProofCaseBranch tc Γ Δ lev tbranches avars sac})
Context {ToLatexVV:ToLatex VV}.
Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string :=
match exp with
- | EVar Γ' _ ξ' ev => "var."+++ev
- | EGlobal Γ' _ ξ' t wev => "global." +++(wev:CoreVar)
- | ELam Γ' _ _ tv _ _ cv e => "\("+++cv+++":t) -> "+++ exprToString e
- | ELet Γ' _ _ t _ _ ev e1 e2 => "let "+++ev+++" = "+++exprToString e1+++" in "+++exprToString e2
- | ELit _ _ _ lit _ => "lit."+++lit
+ | EVar Γ' _ ξ' ev => "var."+++ toString ev
+ | EGlobal Γ' _ ξ' t wev => "global." +++ toString (wev:CoreVar)
+ | ELam Γ' _ _ tv _ _ cv e => "\("+++ toString cv +++":t) -> "+++ exprToString e
+ | ELet Γ' _ _ t _ _ ev e1 e2 => "let "+++toString ev+++" = "+++exprToString e1+++" in "+++exprToString e2
+ | ELit _ _ _ lit _ => "lit."+++toString lit
| EApp Γ' _ _ _ _ _ e1 e2 => "("+++exprToString e1+++")("+++exprToString e2+++")"
| EEsc Γ' _ _ ec t _ e => "~~("+++exprToString e+++")"
| EBrak Γ' _ _ ec t _ e => "<["+++exprToString e+++"]>"
| ENote _ _ _ _ n e => "note."+++exprToString e
- | ETyApp Γ Δ κ σ τ ξ l e => "("+++exprToString e+++")@("+++τ+++")"
+ | ETyApp Γ Δ κ σ τ ξ l e => "("+++exprToString e+++")@("+++toString τ+++")"
| ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => "("+++exprToString e+++")~(co)"
| ECast Γ Δ ξ t1 t2 γ l e => "cast ("+++exprToString e+++"):t2"
| ETyLam _ _ _ k _ _ e => "\@_ ->"+++ exprToString e
Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
(ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
: ???WeakExpr :=
- match exprToWeakExpr (fun v => Error ("unbound variable " +++ v)) exp ite with
+ match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with
uniqM f => f us >>= fun x => OK (snd x)
end.
(* ToString instance for PHOAS types *)
Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
match t with
- | TVar _ v => "tv" +++ v
+ | TVar _ v => "tv" +++ toString v
| TCon tc => toString tc
| TCoerc _ t1 t2 t => "("+++typeToString' false n t1+++"~"
+++typeToString' false n t2+++")=>"
else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
end
| TArrow => "(->)"
- | TAll k f => let alpha := "tv"+++n
- in "(forall "+++ alpha +++ ":"+++ k +++")"+++
+ | TAll k f => let alpha := "tv"+++ toString n
+ in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++
typeToString' false (S n) (f n)
| TCode ec t => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
- | TyFunApp tfc lt => tfc+++"_"+++n+++" ["+++(fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]"
+ | TyFunApp tfc lt => toString tfc+++ "_" +++ toString n+++" ["+++
+ (fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]"
end
with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
match t with
Ltac matchThings T1 T2 S :=
destruct (eqd_dec T1 T2) as [matchTypeVars_pf|];
- [ idtac | apply (Error (S +++ T1 +++ " " +++ T2)) ].
+ [ idtac | apply (Error (S +++ toString T1 +++ " " +++ toString T2)) ].
Definition mkTAll' {κ}{Γ} : HaskType (κ :: Γ) ★ -> (forall TV (ite:InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★).
intros.
Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType), ???(HaskTypeOfSomeKind Γ).
refine (fix weakTypeToType {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) {struct t} : ???(HaskTypeOfSomeKind Γ) :=
- addErrorMessage ("weakTypeToType " +++ t)
+ addErrorMessage ("weakTypeToType " +++ toString t)
match t with
| WFunTyCon => let case_WFunTyCon := tt in OK (haskTypeOfSomeKind (fun TV ite => TArrow))
| WTyCon tc => let case_WTyCon := tt in _
end
) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _
end ); clear weakTypeToType.
+ apply ConcatenableString.
destruct case_WTyVarTy.
apply (addErrorMessage "case_WTyVarTy").
apply (addErrorMessage "case_WAppTy").
destruct t1' as [k1' t1'].
destruct t2' as [k2' t2'].
- set ("tried to apply type "+++t1'+++" of kind "+++k1'+++" to type "+++t2'+++" of kind "+++k2') as err.
+ set ("tried to apply type "+++toString t1'+++" of kind "+++toString k1'+++" to type "+++
+ toString t2'+++" of kind "+++toString k2') as err.
destruct k1';
try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
set ((dataConTyCon c):TyCon) as tc' in *.
set (eqd_dec tc tc') as eqpf; destruct eqpf;
[ idtac
- | apply (Error ("in a case of tycon "+++tc+++", found a branch with datacon "+++(dc:CoreDataCon))) ]; subst.
+ | apply (Error ("in a case of tycon "+++toString tc+++", found a branch with datacon "+++toString (dc:CoreDataCon))) ]; subst.
apply OK.
eapply mkStrongAltConPlusJunk.
simpl in *.
destruct τ' as [τ' l'].
destruct (eqd_dec l l'); [ idtac
| apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++
- " got: " +++(fold_left (fun x y => y+++","+++y) (map haskTyVarToType l) "")+++eol+++
- " wanted: "+++(fold_left (fun x y => x+++","+++y) (map haskTyVarToType l') "")
+ " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++
+ " wanted: "+++(fold_left (fun x y => x+++","+++y) (map (toString ○ haskTyVarToType) l') "")
)) ].
destruct (eqd_dec τ τ'); [ idtac
| apply (Error ("type mismatch in castExpr, invoked by "+++err_msg+++eol+++
- " got: " +++τ+++eol+++
- " wanted: "+++τ'
+ " got: " +++toString τ+++eol+++
+ " wanted: "+++toString τ'
)) ].
subst.
apply OK.
(τ:HaskType Γ ★)
(lev:HaskLevel Γ)
(we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) :=
- addErrorMessage ("in weakExprToStrongExpr " +++ we)
+ addErrorMessage ("in weakExprToStrongExpr " +++ toString we)
match we with
| WEVar v => if ig v
then OK (EGlobal Γ Δ ξ (τ@@lev) v)
- else castExpr we ("WEVar "+++(v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
+ else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
- | WELit lit => castExpr we ("WELit "+++lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
+ | WELit lit => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
| WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv =>
weakTypeOfWeakExpr ebody >>= fun tbody =>
weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' =>
weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' =>
castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e')
- | _ => Error ("weakTypeToType: WETyApp body with type "+++te)
+ | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te)
end
| WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
OK (ECoApp Γ Δ κ t1'' t2''
(weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
end
- | _ => Error ("weakTypeToType: WECoApp body with type "+++te)
+ | _ => Error ("weakTypeToType: WECoApp body with type "+++toString te)
end
| WECoLam cv e => let (_,_,t1,t2) := cv in
weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' =>
castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree)
- end)); try clear binds.
-
+ end)); try clear binds; try apply ConcatenableString.
+
destruct case_some.
apply (addErrorMessage "case_some").
simpl.
Context {Judgment : Type}.
Context {Rule : forall (hypotheses:Tree ??Judgment)(conclusion:Tree ??Judgment), Type}.
-
- (* the "user" must supply functions for latexifying judgments and rules *)
- Context (judgment2latex : Judgment -> string).
- Context (rule2latex : forall h c, Rule h c -> string).
+ Context {JudgmentToLatexMath : ToLatexMath Judgment}.
+ Context {RuleToLatexMath : forall h c, ToLatexMath (Rule h c)}.
Open Scope string_scope.
- Notation "a +++ b" := (append a b) (at level 100).
- Section TreeToLatex.
- Context (emptyleaf:string).
- Context {T:Type}.
- Context (leaf:T -> string).
- Fixpoint tree2latex' (j:Tree ??T) : string :=
- match j with
- | T_Leaf None => emptyleaf
- | T_Leaf (Some j') => leaf j'
- | T_Branch b1 b2 => "\left["+++tree2latex' b1+++
- "\text{\tt{,}}"+++
- tree2latex' b2+++"\right]"
- end.
- Definition tree2latex (j:Tree ??T) : string :=
- match j with
- | T_Leaf None => emptyleaf
- | T_Leaf (Some j') => leaf j'
- | T_Branch b1 b2 => tree2latex' b1+++
- "\text{\tt{,}}"+++
- tree2latex' b2
- end.
- Fixpoint list2latex (sep:string)(l:list T) : string :=
- match l with
- | nil => emptyleaf
- | (a::nil) => leaf a
- | (a::b) => (leaf a)+++sep+++(list2latex sep b)
- end.
- End TreeToLatex.
- Definition judgments2latex (j:Tree ??Judgment) :=
- list2latex " " judgment2latex " \\ " (leaves j).
+ Definition judgments2latex (j:Tree ??Judgment) := treeToLatexMath (mapOptionTree toLatexMath j).
+
+ Definition eolL : LatexMath := rawLatexMath eol.
(* invariant: each proof shall emit its hypotheses visibly, except nd_id0 *)
Section SCND_toLatex.
(* indicates which rules should be hidden (omitted) from the rendered proof; useful for structural operations *)
Context (hideRule : forall h c (r:Rule h c), bool).
- Fixpoint SCND_toLatex {h}{c}(pns:SCND h c) : string :=
+ Fixpoint SCND_toLatexMath {h}{c}(pns:SCND(Rule:=Rule) h c) : LatexMath :=
match pns with
- | scnd_leaf ht c pn => SCND_toLatex pn
- | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatex pns1 +++ " \hspace{1cm} " +++ SCND_toLatex pns2
- | scnd_weak c => ""
- | scnd_comp ht ct c pns rule => if hideRule _ _ rule
- then SCND_toLatex pns
- else "\trfrac["+++rule2latex _ _ rule +++ "]{" +++ eol +++
- SCND_toLatex pns +++ "}{" +++ eol +++
- judgment2latex c +++ "}" +++ eol
+ | scnd_leaf ht c pn => SCND_toLatexMath pn
+ | scnd_branch ht c1 c2 pns1 pns2 => SCND_toLatexMath pns1 +++ rawLatexMath " \hspace{1cm} " +++ SCND_toLatexMath pns2
+ | scnd_weak c => rawLatexMath ""
+ | scnd_comp ht ct c pns rule => if hideRule _ _ rule
+ then SCND_toLatexMath pns
+ else rawLatexMath "\trfrac["+++ toLatexMath rule +++ rawLatexMath "]{" +++ eolL +++
+ SCND_toLatexMath pns +++ rawLatexMath "}{" +++ eolL +++
+ toLatexMath c +++ rawLatexMath "}" +++ eolL
end.
End SCND_toLatex.
- (* this is a work-in-progress; please use SCND_toLatex for now *)
- Fixpoint nd_toLatex {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
+ (* this is a work-in-progress; please use SCND_toLatexMath for now *)
+ Fixpoint nd_toLatexMath {h}{c}(nd:@ND _ Rule h c)(indent:string) :=
match nd with
- | nd_id0 => indent +++ "% nd_id0 " +++ eol
- | nd_id1 h' => indent +++ "% nd_id1 "+++ judgments2latex h +++ eol
- | nd_weak h' => indent +++ "\inferrule*[Left=ndWeak]{" +++ judgment2latex h' +++ "}{ }" +++ eol
- | nd_copy h' => indent +++ "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
- "}{"+++judgments2latex c+++"}" +++ eol
- | nd_prod h1 h2 c1 c2 pf1 pf2 => indent +++ "% prod " +++ eol +++
- indent +++ "\begin{array}{c c}" +++ eol +++
- (nd_toLatex pf1 (" "+++indent)) +++
- indent +++ " & " +++ eol +++
- (nd_toLatex pf2 (" "+++indent)) +++
- indent +++ "\end{array}"
- | nd_comp h m c pf1 pf2 => indent +++ "% comp " +++ eol +++
- indent +++ "\begin{array}{c}" +++ eol +++
- (nd_toLatex pf1 (" "+++indent)) +++
- indent +++ " \\ " +++ eol +++
- (nd_toLatex pf2 (" "+++indent)) +++
- indent +++ "\end{array}"
- | nd_cancell a => indent +++ "% nd-cancell " +++ (judgments2latex a) +++ eol
- | nd_cancelr a => indent +++ "% nd-cancelr " +++ (judgments2latex a) +++ eol
- | nd_llecnac a => indent +++ "% nd-llecnac " +++ (judgments2latex a) +++ eol
- | nd_rlecnac a => indent +++ "% nd-rlecnac " +++ (judgments2latex a) +++ eol
- | nd_assoc a b c => ""
- | nd_cossa a b c => ""
- | nd_rule h c r => rule2latex h c r
+ | nd_id0 => rawLatexMath indent +++
+ rawLatexMath "% nd_id0 " +++ eolL
+ | nd_id1 h' => rawLatexMath indent +++
+ rawLatexMath "% nd_id1 "+++ judgments2latex h +++ eolL
+ | nd_weak h' => rawLatexMath indent +++
+ rawLatexMath "\inferrule*[Left=ndWeak]{" +++ toLatexMath h' +++ rawLatexMath "}{ }" +++ eolL
+ | nd_copy h' => rawLatexMath indent +++
+ rawLatexMath "\inferrule*[Left=ndCopy]{"+++judgments2latex h+++
+ rawLatexMath "}{"+++judgments2latex c+++rawLatexMath "}" +++ eolL
+ | nd_prod h1 h2 c1 c2 pf1 pf2 => rawLatexMath indent +++
+ rawLatexMath "% prod " +++ eolL +++
+ rawLatexMath indent +++
+ rawLatexMath "\begin{array}{c c}" +++ eolL +++
+ (nd_toLatexMath pf1 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath " & " +++ eolL +++
+ (nd_toLatexMath pf2 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath "\end{array}"
+ | nd_comp h m c pf1 pf2 => rawLatexMath indent +++
+ rawLatexMath "% comp " +++ eolL +++
+ rawLatexMath indent +++
+ rawLatexMath "\begin{array}{c}" +++ eolL +++
+ (nd_toLatexMath pf1 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath " \\ " +++ eolL +++
+ (nd_toLatexMath pf2 (" "+++indent)) +++
+ rawLatexMath indent +++
+ rawLatexMath "\end{array}"
+ | nd_cancell a => rawLatexMath indent +++
+ rawLatexMath "% nd-cancell " +++ (judgments2latex a) +++ eolL
+ | nd_cancelr a => rawLatexMath indent +++
+ rawLatexMath "% nd-cancelr " +++ (judgments2latex a) +++ eolL
+ | nd_llecnac a => rawLatexMath indent +++
+ rawLatexMath "% nd-llecnac " +++ (judgments2latex a) +++ eolL
+ | nd_rlecnac a => rawLatexMath indent +++
+ rawLatexMath "% nd-rlecnac " +++ (judgments2latex a) +++ eolL
+ | nd_assoc a b c => rawLatexMath ""
+ | nd_cossa a b c => rawLatexMath ""
+ | nd_rule h c r => toLatexMath r
end.
End ToLatex.
projects / coq-hetmet.git / commitdiff