alc-latex.maude

in alc-system.maude

mod LATEX is 
 inc LALC-SYSTEM-FULL .
 inc CONVERSION .
 
 op latex : Concept -> String .
 op latex : Role -> String .
 
 vars A B C : Concept .
 var R : Role .
 vars L1 L2 : List{Label} .

 eq latex(CTRUE)  = "/top" .
 eq latex(CFALSE) = "/bot" .
 
 eq latex( ~ A )   = "/neg (" + latex(A) + ")" .
 eq latex( A | B ) = "(" + latex(A) + " /dlor "  + latex(B) + ")" .
 eq latex( A & B ) = "(" + latex(A) + " /dland " + latex(B) + ")" .
 eq latex( ALL(R,A) ) =   "/forall " + latex(R) + ". (" + latex(A) + ")" .
 eq latex( EXIST(R,A) ) = "/exists " + latex(R) + ". (" + latex(A) + ")" .

 op latex : List{Label} -> String .
 
 eq latex(s(R, L1) L2) = latex(R) + "(" + latex(L1) + "), " + latex(L2) .
 eq latex(R L1) = latex(R) + ", " + latex(L1) .
 eq latex(nil)  = "" .
 
 op latex : LConcept -> String .
 eq latex(< L1 | A | L2 >) = "/lf{" + latex(L1) + "}{" + latex(A) + "}{" + latex(L2) + "}" .

 op latex : FzConcept -> String .
 eq latex([ N:Nat , C:LConcept ]) = "/left[" + latex(C:LConcept) + "/right]^{" + string(N:Nat, 10) + "}" . 

 vars C1 C2 : Expression .
 vars DELTA GAMMA : Set{Expression} .

 op latex : Set{Expression} -> String .
 eq latex((C1, DELTA)) = latex(C1) + ", " + latex(DELTA) .
 eq latex(empty) = "" .

 op latex : Sequent -> String .
 eq latex((DELTA |- GAMMA)) = latex(DELTA) + " /fCenter " + latex(GAMMA) .

 op latex : Proof -> String .

 eq latex([ N0 from M by Q0 is S0 ] [ N1 from M by Q1 is S1 ] [ M from N by Q2 is S2 ] P) = 
    latex([ N0 from M by Q0 is S0 ] [ N1 from M by Q1 is S1 ] P) + 
    "\LeftLabel{" + latex(Q2) + "}" +
    "\BinaryInf{" + latex(S2) + "}" .

 eq latex([ N0 from M by Q0 is S0] [ M from N by Q1 is S1] P) = 
    latex(P) + 
    "\LeftLabel{" + latex(Q) + "}" +
    " \UnaryInf{" + latex(S) + "}" [owise] .

endm

mod LATEX-TEST is
 inc LATEX .
 inc QID .
 
 
 op conc : Qid -> AConcept .
 op role : Qid -> ARole .

 var Q : Qid .
 
 eq latex(conc(Q)) = string(Q) .
 eq latex(role(Q)) = string(Q) .
 
 ops c1 c2 : -> Concept .
 
 eq c1 =   ALL(role('R), conc('A) & CTRUE) .
 eq c2 = EXIST(role('R), conc('A) | CTRUE) .
 
 op c3 : -> FzConcept .
 eq c3 = [3, < role('R) role('S) | ALL(role('R), ~  conc('A)) | s(role('X), role('S) role('Q)) role('R) > ] .

endm