521 | string_of_tptp_type (Sum_type (tptp_type1, tptp_type2)) = "" |
523 | string_of_tptp_type (Sum_type (tptp_type1, tptp_type2)) = "" |
522 | string_of_tptp_type (Fmla_type tptp_formula) = string_of_tptp_formula tptp_formula |
524 | string_of_tptp_type (Fmla_type tptp_formula) = string_of_tptp_formula tptp_formula |
523 | string_of_tptp_type (Subtype (symbol1, symbol2)) = |
525 | string_of_tptp_type (Subtype (symbol1, symbol2)) = |
524 string_of_symbol symbol1 ^ " << " ^ string_of_symbol symbol2 |
526 string_of_symbol symbol1 ^ " << " ^ string_of_symbol symbol2 |
525 |
527 |
|
528 |
|
529 (*Add subscripting*) |
|
530 (*infix symbols, including \subset, \cup, \cap*) |
|
531 fun latex_of_tptp_term x = |
|
532 ((*writeln ("term=" ^ PolyML.makestring x);*) |
|
533 case x of |
|
534 (* |
|
535 Term_Func (Uninterpreted "subset", [tptp_t1, tptp_t2]) => |
|
536 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
537 | Term_Func (Uninterpreted "union", [tptp_t1, tptp_t2]) => |
|
538 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
539 *) |
|
540 (* |
|
541 Term_Func (Interpreted_Logic Apply, [Term_Func (Interpreted_Logic Apply, [Uninterpreted "subset", tptp_t1]), tptp_t2]) => |
|
542 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
543 | Term_Func (Interpreted_Logic Apply, [Term_Func (Interpreted_Logic Apply, [Uninterpreted "union", tptp_t1]), tptp_t2]) => |
|
544 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
545 *) |
|
546 (* |
|
547 Term_Func (Interpreted_ExtraLogic Apply, |
|
548 [Term_Func (Interpreted_ExtraLogic Apply, |
|
549 [Term_Func (Interpreted_ExtraLogic Apply, [Term_Func (Uninterpreted "subset", []), |
|
550 tptp_t1])]), tptp_t2]) => |
|
551 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
552 | Term_Func (Interpreted_ExtraLogic Apply, |
|
553 [Term_Func (Interpreted_ExtraLogic Apply, |
|
554 [Term_Func (Interpreted_ExtraLogic Apply, [Term_Func (Uninterpreted "union", []), |
|
555 tptp_t1])]), tptp_t2]) => |
|
556 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
557 |
|
558 |*) Term_Func (Interpreted_Logic Equals, [tptp_t1, tptp_t2]) => |
|
559 "(" ^ latex_of_tptp_term tptp_t1 ^ " = " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
560 | Term_Func (Interpreted_Logic NEquals, [tptp_t1, tptp_t2]) => |
|
561 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\neq " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
562 | Term_Func (Interpreted_Logic Or, [tptp_t1, tptp_t2]) => |
|
563 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\vee " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
564 | Term_Func (Interpreted_Logic And, [tptp_t1, tptp_t2]) => |
|
565 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\wedge " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
566 | Term_Func (Interpreted_Logic Iff, [tptp_t1, tptp_t2]) => |
|
567 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
568 | Term_Func (Interpreted_Logic If, [tptp_t1, tptp_t2]) => |
|
569 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
570 |
|
571 | Term_Func (symbol, tptp_term_list) => |
|
572 (*"(" ^*) latex_of_symbol symbol ^ " " ^ |
|
573 space_implode " " (map latex_of_tptp_term tptp_term_list) (*^ ")"*) |
|
574 | Term_Var str => str |
|
575 | Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*) |
|
576 | Term_Num (_, str) => str |
|
577 | Term_Distinct_Object str => str |
|
578 ) |
|
579 and latex_of_symbol (Uninterpreted str) = |
|
580 (* if str = "union" then "\\\\cup" |
|
581 else if str = "subset" then "\\\\subset" |
|
582 else*) |
|
583 if str = "emptyset" then "\\\\emptyset" |
|
584 else str |
|
585 | latex_of_symbol (Interpreted_ExtraLogic interpreted_symbol) = latex_of_interpreted_symbol interpreted_symbol |
|
586 | latex_of_symbol (Interpreted_Logic logic_symbol) = latex_of_logic_symbol logic_symbol |
|
587 | latex_of_symbol (TypeSymbol tptp_base_type) = latex_of_tptp_base_type tptp_base_type |
|
588 | latex_of_symbol (System str) = str |
|
589 |
|
590 and latex_of_tptp_base_type Type_Ind = "\\\\iota " |
|
591 | latex_of_tptp_base_type Type_Bool = "o" |
|
592 | latex_of_tptp_base_type Type_Type = "\\\\mathcal{T} " |
|
593 | latex_of_tptp_base_type Type_Int = "\\\\mathsf{int} " |
|
594 | latex_of_tptp_base_type Type_Rat = "\\\\mathsf{rat} " |
|
595 | latex_of_tptp_base_type Type_Real = "\\\\mathsf{real} " |
|
596 |
|
597 and latex_of_interpreted_symbol x = |
|
598 case x of |
|
599 UMinus => "-" |
|
600 | Sum => "-" |
|
601 | Difference => "-" |
|
602 | Product => "*" |
|
603 | Quotient => "/" |
|
604 | Quotient_E => "" (*FIXME*) |
|
605 | Quotient_T => "" (*FIXME*) |
|
606 | Quotient_F => "" (*FIXME*) |
|
607 | Remainder_E => "" (*FIXME*) |
|
608 | Remainder_T => "" (*FIXME*) |
|
609 | Remainder_F => "" (*FIXME*) |
|
610 | Floor => "" (*FIXME*) |
|
611 | Ceiling => "" (*FIXME*) |
|
612 | Truncate => "" (*FIXME*) |
|
613 | Round => "" (*FIXME*) |
|
614 | To_Int => "" (*FIXME*) |
|
615 | To_Rat => "" (*FIXME*) |
|
616 | To_Real => "" (*FIXME*) |
|
617 | Less => "<" |
|
618 | LessEq => "\\\\leq " |
|
619 | Greater => ">" |
|
620 | GreaterEq => "\\\\geq " |
|
621 | EvalEq => "" (*FIXME*) |
|
622 | Is_Int => "" (*FIXME*) |
|
623 | Is_Rat => "" (*FIXME*) |
|
624 | Distinct => "" (*FIXME*) |
|
625 | Apply => "\\\\;" |
|
626 |
|
627 and latex_of_logic_symbol Equals = "=" |
|
628 | latex_of_logic_symbol NEquals = "\\\\neq " |
|
629 | latex_of_logic_symbol Or = "\\\\vee " |
|
630 | latex_of_logic_symbol And = "\\\\wedge " |
|
631 | latex_of_logic_symbol Iff = "\\\\longleftrightarrow " |
|
632 | latex_of_logic_symbol If = "\\\\longrightarrow " |
|
633 | latex_of_logic_symbol Fi = "\\\\longleftarrow " |
|
634 | latex_of_logic_symbol Xor = "\\\\oplus " |
|
635 | latex_of_logic_symbol Nor = "\\\\not\\\\vee " |
|
636 | latex_of_logic_symbol Nand = "\\\\not\\\\wedge " |
|
637 | latex_of_logic_symbol Not = "\\\\neg " |
|
638 | latex_of_logic_symbol Op_Forall = "\\\\forall " |
|
639 | latex_of_logic_symbol Op_Exists = "\\\\exists " |
|
640 | latex_of_logic_symbol True = "\\\\mathsf{true} " |
|
641 | latex_of_logic_symbol False = "\\\\mathsf{false} " |
|
642 |
|
643 and latex_of_quantifier Forall = "\\\\forall " |
|
644 | latex_of_quantifier Exists = "\\\\exists " |
|
645 | latex_of_quantifier Epsilon = "\\\\varepsilon " |
|
646 | latex_of_quantifier Iota = "" (*FIXME*) |
|
647 | latex_of_quantifier Lambda = "\\\\lambda " |
|
648 | latex_of_quantifier Dep_Prod = "\\\\Pi " |
|
649 | latex_of_quantifier Dep_Sum = "\\\\Sigma " |
|
650 |
|
651 and latex_of_tptp_atom (TFF_Typed_Atom (symbol, tptp_type_option)) = |
|
652 (case tptp_type_option of |
|
653 NONE => latex_of_symbol symbol |
|
654 | SOME tptp_type => |
|
655 latex_of_symbol symbol ^ " : " ^ latex_of_tptp_type tptp_type) |
|
656 | latex_of_tptp_atom (THF_Atom_term tptp_term) = latex_of_tptp_term tptp_term |
|
657 | latex_of_tptp_atom (THF_Atom_conn_term symbol) = latex_of_symbol symbol |
|
658 |
|
659 (* |
|
660 and latex_of_tptp_formula (Pred (symbol, tptp_term_list)) = |
|
661 "(" ^ latex_of_symbol symbol ^ |
|
662 space_implode " " (map latex_of_tptp_term tptp_term_list) ^ ")" |
|
663 | latex_of_tptp_formula (Fmla (symbol, tptp_formula_list)) = |
|
664 "(" ^ latex_of_symbol symbol ^ |
|
665 space_implode " " (map latex_of_tptp_formula tptp_formula_list) ^ ")" |
|
666 *) |
|
667 (* |
|
668 and latex_of_tptp_formula (Pred (Uninterpreted "subset", [tptp_t1, tptp_t2])) = |
|
669 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
670 | latex_of_tptp_formula (Pred (Uninterpreted "union", [tptp_t1, tptp_t2])) = |
|
671 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
672 *) |
|
673 and (*latex_of_tptp_formula ( |
|
674 Pred (Interpreted_ExtraLogic Apply, |
|
675 [Term_Func (Interpreted_ExtraLogic Apply, |
|
676 [Term_Func (Interpreted_ExtraLogic Apply, [Term_Func (Uninterpreted "subset", []), |
|
677 tptp_t1])]), tptp_t2])) = |
|
678 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
679 | latex_of_tptp_formula (Pred (Interpreted_ExtraLogic Apply, |
|
680 [Term_Func (Interpreted_ExtraLogic Apply, |
|
681 [Term_Func (Interpreted_ExtraLogic Apply, [Term_Func (Uninterpreted "union", []), |
|
682 tptp_t1])]), tptp_t2])) = |
|
683 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
684 |
|
685 |*) latex_of_tptp_formula (Pred (Interpreted_Logic Equals, [tptp_t1, tptp_t2])) = |
|
686 "(" ^ latex_of_tptp_term tptp_t1 ^ " = " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
687 | latex_of_tptp_formula (Pred (Interpreted_Logic NEquals, [tptp_t1, tptp_t2])) = |
|
688 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\neq " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
689 | latex_of_tptp_formula (Pred (Interpreted_Logic Or, [tptp_t1, tptp_t2])) = |
|
690 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\vee " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
691 | latex_of_tptp_formula (Pred (Interpreted_Logic And, [tptp_t1, tptp_t2])) = |
|
692 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\wedge " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
693 | latex_of_tptp_formula (Pred (Interpreted_Logic Iff, [tptp_t1, tptp_t2])) = |
|
694 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
695 | latex_of_tptp_formula (Pred (Interpreted_Logic If, [tptp_t1, tptp_t2])) = |
|
696 "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")" |
|
697 |
|
698 | latex_of_tptp_formula (x as (Pred (symbol, tptp_term_list))) = |
|
699 ((*writeln ("fmla=" ^ PolyML.makestring x);*) |
|
700 (*"(" ^*) latex_of_symbol symbol ^ |
|
701 space_implode " " (map latex_of_tptp_term tptp_term_list) (*^ ")"*) |
|
702 ) |
|
703 |
|
704 (* |
|
705 | latex_of_tptp_formula (Fmla (Uninterpreted "subset", [tptp_f1, tptp_f2])) = |
|
706 "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_f2 ^ ")" |
|
707 | latex_of_tptp_formula (Fmla (Uninterpreted "union", [tptp_f1, tptp_f2])) = |
|
708 "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_f2 ^ ")" |
|
709 *) |
|
710 |
|
711 (* |
|
712 | latex_of_tptp_formula ( |
|
713 Fmla (Interpreted_ExtraLogic Apply, |
|
714 [Fmla (Interpreted_ExtraLogic Apply, |
|
715 [Fmla (Interpreted_ExtraLogic Apply, [Fmla (Uninterpreted "subset", []), |
|
716 tptp_t1])]), tptp_t2])) = |
|
717 "(" ^ latex_of_tptp_formula tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_t2 ^ ")" |
|
718 | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, |
|
719 [Fmla (Interpreted_ExtraLogic Apply, |
|
720 [Fmla (Interpreted_ExtraLogic Apply, [Fmla (Uninterpreted "union", []), |
|
721 tptp_t1])]), tptp_t2])) = |
|
722 "(" ^ latex_of_tptp_formula tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_t2 ^ ")" |
|
723 *) |
|
724 |
|
725 | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "union", []))), tptp_f1]), tptp_f2])) = |
|
726 "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_f2 ^ ")" |
|
727 |
|
728 | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "subset", []))), tptp_f1]), tptp_f2])) = |
|
729 "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_f2 ^ ")" |
|
730 |
|
731 |
|
732 | latex_of_tptp_formula (Fmla (Interpreted_Logic Equals, [tptp_f1, tptp_f2])) = |
|
733 "(" ^ latex_of_tptp_formula tptp_f1 ^ " = " ^ latex_of_tptp_formula tptp_f2 ^ ")" |
|
734 | latex_of_tptp_formula (Fmla (Interpreted_Logic NEquals, [tptp_f1, tptp_f2])) = |
|
735 "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\neq " ^ latex_of_tptp_formula tptp_f2 ^ ")" |
|
736 | latex_of_tptp_formula (Fmla (Interpreted_Logic Or, [tptp_f1, tptp_f2])) = |
|
737 "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\vee " ^ latex_of_tptp_formula tptp_f2 ^ ")" |
|
738 | latex_of_tptp_formula (Fmla (Interpreted_Logic And, [tptp_f1, tptp_f2])) = |
|
739 "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\wedge " ^ latex_of_tptp_formula tptp_f2 ^ ")" |
|
740 | latex_of_tptp_formula (Fmla (Interpreted_Logic Iff, [tptp_f1, tptp_f2])) = |
|
741 "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_formula tptp_f2 ^ ")" |
|
742 | latex_of_tptp_formula (Fmla (Interpreted_Logic If, [tptp_f1, tptp_f2])) = |
|
743 "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\longrightarrow " ^ latex_of_tptp_formula tptp_f2 ^ ")" |
|
744 |
|
745 | latex_of_tptp_formula (x as (Fmla (symbol, tptp_formula_list))) = |
|
746 (writeln ("fmla=" ^ PolyML.makestring x); |
|
747 (*"(" ^*) latex_of_symbol symbol ^ |
|
748 space_implode " " (map latex_of_tptp_formula tptp_formula_list) (*^ ")"*) |
|
749 ) |
|
750 |
|
751 | latex_of_tptp_formula (Sequent (tptp_formula_list1, tptp_formula_list2)) = "" (*FIXME*) |
|
752 | latex_of_tptp_formula (Quant (quantifier, varlist, tptp_formula)) = |
|
753 latex_of_quantifier quantifier ^ |
|
754 space_implode ", " (map (fn (n, ty) => |
|
755 case ty of |
|
756 NONE => n |
|
757 | SOME ty => n ^ " : " ^ latex_of_tptp_type ty) varlist) ^ ". (" ^ |
|
758 latex_of_tptp_formula tptp_formula ^ ")" |
|
759 | latex_of_tptp_formula (Conditional _) = "" (*FIXME*) |
|
760 | latex_of_tptp_formula (Let _) = "" (*FIXME*) |
|
761 | latex_of_tptp_formula (Atom tptp_atom) = latex_of_tptp_atom tptp_atom |
|
762 | latex_of_tptp_formula (Type_fmla tptp_type) = latex_of_tptp_type tptp_type |
|
763 | latex_of_tptp_formula (THF_typing (tptp_formula, tptp_type)) = |
|
764 latex_of_tptp_formula tptp_formula ^ " : " ^ latex_of_tptp_type tptp_type |
|
765 |
|
766 and latex_of_tptp_type (Prod_type (tptp_type1, tptp_type2)) = |
|
767 latex_of_tptp_type tptp_type1 ^ " \\\\times " ^ latex_of_tptp_type tptp_type2 |
|
768 | latex_of_tptp_type (Fn_type (tptp_type1, tptp_type2)) = |
|
769 latex_of_tptp_type tptp_type1 ^ " \\\\to " ^ latex_of_tptp_type tptp_type2 |
|
770 | latex_of_tptp_type (Atom_type str) = str |
|
771 | latex_of_tptp_type (Defined_type tptp_base_type) = |
|
772 latex_of_tptp_base_type tptp_base_type |
|
773 | latex_of_tptp_type (Sum_type (tptp_type1, tptp_type2)) = "" |
|
774 | latex_of_tptp_type (Fmla_type tptp_formula) = latex_of_tptp_formula tptp_formula |
|
775 | latex_of_tptp_type (Subtype (symbol1, symbol2)) = "" (*FIXME*) |
|
776 |
526 end |
777 end |