From 97552c1a6dfb32098d4491951929ab1d4aca96a0 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 15:09:55 -0700 Subject: [PATCH] add Concatenable, LatexMath, and fix HaskProofToLatex --- src/ExtractionMain.v | 67 +++---- src/General.v | 85 ++++++--- src/HaskCoreToWeak.v | 6 +- src/HaskKinds.v | 18 +- src/HaskLiteralsAndTyCons.v | 4 +- src/HaskProofToLatex.v | 393 +++++++++++++++++++++-------------------- src/HaskProofToStrong.v | 7 - src/HaskStrong.v | 12 +- src/HaskStrongToWeak.v | 2 +- src/HaskStrongTypes.v | 9 +- src/HaskWeakToStrong.v | 32 ++-- src/NaturalDeductionToLatex.v | 125 ++++++------- 12 files changed, 380 insertions(+), 380 deletions(-) diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 59183c9..2b65a18 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -88,7 +88,7 @@ Section core2proof. 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 Γ Δ := @@ -128,20 +128,19 @@ Section core2proof. 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 @@ -239,38 +238,18 @@ Section core2proof. 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 *) @@ -289,17 +268,17 @@ Section core2proof. 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 => diff --git a/src/General.v b/src/General.v index f2e451f..6cb18be 100644 --- a/src/General.v +++ b/src/General.v @@ -24,7 +24,15 @@ Coercion eqd_type : EqDecidable >-> Sortclass. 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 *) @@ -145,11 +153,10 @@ Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (for 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 }. @@ -725,10 +732,6 @@ Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3), -CoInductive Fresh A T := -{ next : forall a:A, (T a * Fresh A T) -; split : Fresh A T * Fresh A T -}. @@ -763,7 +766,6 @@ Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) := 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) @@ -912,23 +914,58 @@ Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_z 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. diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 6e1b58f..abcd6b8 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -53,7 +53,7 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := | 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 @@ -134,8 +134,8 @@ Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list Weak 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 := diff --git a/src/HaskKinds.v b/src/HaskKinds.v index 0357780..b61ed07 100644 --- a/src/HaskKinds.v +++ b/src/HaskKinds.v @@ -38,17 +38,17 @@ Instance KindToString : ToString Kind := { toString := kindToString }. 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. diff --git a/src/HaskLiteralsAndTyCons.v b/src/HaskLiteralsAndTyCons.v index a0695d2..1b8494f 100644 --- a/src/HaskLiteralsAndTyCons.v +++ b/src/HaskLiteralsAndTyCons.v @@ -86,8 +86,8 @@ Variable tyConToString : TyCon -> string. Extract Inlined Constant tyCon 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". diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index d99469c..39dd8ba 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -18,209 +18,210 @@ 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. - - 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 [])). diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index f907514..3dee0fe 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -507,13 +507,6 @@ Section HaskProofToStrong. 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}) diff --git a/src/HaskStrong.v b/src/HaskStrong.v index 6539c89..d688c2f 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -79,16 +79,16 @@ Section HaskStrong. 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 diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index ad1dee7..1761b83 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -209,7 +209,7 @@ Section HaskStrongToWeak. 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. diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 85d6f24..2ee78b2 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -547,7 +547,7 @@ Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ). (* 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+++")=>" @@ -564,11 +564,12 @@ Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) 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 diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index bbc9cc7..b2521e3 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -97,7 +97,7 @@ Notation " ` x " := (@fixkind _ x) (at level 100). 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. @@ -118,7 +118,7 @@ Definition mkTAll {κ}{Γ} : HaskType (κ :: Γ) ★ -> HaskType Γ ★. 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 _ @@ -149,6 +149,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) end ) (fst (tyFunKind tc)) lt) >>= fun lt' => let case_WTyFunApp := tt in _ end ); clear weakTypeToType. + apply ConcatenableString. destruct case_WTyVarTy. apply (addErrorMessage "case_WTyVarTy"). @@ -159,7 +160,8 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) 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)))); @@ -354,7 +356,7 @@ Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAlt 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 *. @@ -401,13 +403,13 @@ Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Ex 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. @@ -534,14 +536,14 @@ Definition weakExprToStrongExpr : forall (τ: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 => @@ -596,7 +598,7 @@ Definition weakExprToStrongExpr : forall 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 => @@ -612,7 +614,7 @@ Definition weakExprToStrongExpr : forall 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 @@ -680,8 +682,8 @@ Definition weakExprToStrongExpr : forall 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. diff --git a/src/NaturalDeductionToLatex.v b/src/NaturalDeductionToLatex.v index 2d6fb55..ddf6e8c 100644 --- a/src/NaturalDeductionToLatex.v +++ b/src/NaturalDeductionToLatex.v @@ -13,43 +13,14 @@ Section ToLatex. 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. @@ -57,46 +28,62 @@ Section 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. -- 1.7.10.4