support THF1 parsing for 'tptp_...' commands (e.g. 'tptp_isabelle') -- useful for CASC, SystemOnTPTP, ...
authorblanchet
Wed Dec 14 18:52:17 2016 +0100 (2016-12-14)
changeset 64560c48becd96398
parent 64559 abd9a9fd030b
child 64561 a7664ca9ffc5
support THF1 parsing for 'tptp_...' commands (e.g. 'tptp_isabelle') -- useful for CASC, SystemOnTPTP, ...
src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML
     1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Dec 14 09:19:50 2016 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Dec 14 18:52:17 2016 +0100
     1.3 @@ -215,7 +215,7 @@
     1.4  fun declare_constant config const_name ty thy =
     1.5    if const_exists config thy const_name then
     1.6      raise MISINTERPRET_TERM
     1.7 -     ("Const already declared", Term_Func (Uninterpreted const_name, []))
     1.8 +     ("Const already declared", Term_FuncG (Uninterpreted const_name, [], []))
     1.9    else
    1.10      Theory.specify_const ((mk_binding config const_name, ty), NoSyn) thy
    1.11  
    1.12 @@ -224,10 +224,10 @@
    1.13  
    1.14  (*Types in TFF/THF are encoded as formulas. These functions translate them to type form.*)
    1.15  
    1.16 -fun termtype_to_type (Term_Func (TypeSymbol typ, [])) =
    1.17 +fun termtype_to_type (Term_FuncG (TypeSymbol typ, [], [])) =
    1.18        Defined_type typ
    1.19 -  | termtype_to_type (Term_Func (Uninterpreted str, tms)) =
    1.20 -      Atom_type (str, map termtype_to_type tms)
    1.21 +  | termtype_to_type (Term_FuncG (Uninterpreted str, tys, tms)) =
    1.22 +      Atom_type (str, tys @ map termtype_to_type tms)
    1.23    | termtype_to_type (Term_Var str) = Var_type str
    1.24  
    1.25  (*FIXME possibly incomplete hack*)
    1.26 @@ -249,6 +249,9 @@
    1.27    | fmlatype_to_type (Quant (Dep_Prod, _, fmla)) = fmlatype_to_type fmla
    1.28    | fmlatype_to_type (Pred (Interpreted_ExtraLogic Apply, [tm])) =
    1.29        termtype_to_type tm
    1.30 +  | fmlatype_to_type (Fmla (Interpreted_ExtraLogic Apply, [tm1, tm2])) =
    1.31 +      (case fmlatype_to_type tm1 of
    1.32 +        Atom_type (str, tys) => Atom_type (str, tys @ [fmlatype_to_type tm2]))
    1.33  
    1.34  fun tfree_name_of_var_type str = "'" ^ Name.desymbolize (SOME false) str
    1.35  fun tfree_of_var_type str = TFree (tfree_name_of_var_type str, @{sort type})
    1.36 @@ -323,7 +326,7 @@
    1.37        else
    1.38          raise MISINTERPRET_TERM
    1.39              ("Could not find the interpretation of this constant in the \
    1.40 -              \mapping to Isabelle/HOL", Term_Func (Uninterpreted str, [])))
    1.41 +              \mapping to Isabelle/HOL", Term_FuncG (Uninterpreted str, [], [])))
    1.42  
    1.43  (*Eta-expands n-ary function.
    1.44   "str" is the name of an Isabelle/HOL constant*)
    1.45 @@ -448,7 +451,7 @@
    1.46          interpret_type config thy type_map (Defined_type Type_Bool)
    1.47        else ind_type
    1.48    in case tptp_atom_value of
    1.49 -      Atom_App (Term_Func (symb, tptp_ts)) =>
    1.50 +      Atom_App (Term_FuncG (symb, tptp_tys, tptp_ts)) =>
    1.51          let
    1.52            val thy' = fold (fn t =>
    1.53              type_atoms_to_thy config false type_map (Atom_App t)) tptp_ts thy
    1.54 @@ -456,7 +459,8 @@
    1.55            case symb of
    1.56               Uninterpreted const_name =>
    1.57                 perhaps (try (snd o declare_constant config const_name
    1.58 -                (mk_fun_type (replicate (length tptp_ts) ind_type) value_type I))) thy'
    1.59 +                (mk_fun_type (replicate (length tptp_tys + length tptp_ts) ind_type) value_type I)))
    1.60 +                thy'
    1.61             | _ => thy'
    1.62          end
    1.63      | Atom_App _ => thy
    1.64 @@ -499,6 +503,25 @@
    1.65       | _ => false
    1.66     end
    1.67  
    1.68 +fun strip_applies_term (Term_FuncG (Interpreted_ExtraLogic Apply, [], [tm1, tm2])) =
    1.69 +    strip_applies_term tm1 ||> (fn tms => tms @ [tm2])
    1.70 +  | strip_applies_term tm = (tm, [])
    1.71 +
    1.72 +fun termify_apply_fmla thy config (Fmla (Interpreted_ExtraLogic Apply, [fmla1, fmla2])) =
    1.73 +    (case termify_apply_fmla thy config fmla1 of
    1.74 +      SOME (Term_FuncG (symb, tys, tms)) =>
    1.75 +      let val typ_arity = type_arity_of_symbol thy config symb in
    1.76 +        (case (null tms andalso length tys < typ_arity, try fmlatype_to_type fmla2) of
    1.77 +          (true, SOME ty) => SOME (Term_FuncG (symb, tys @ [ty], []))
    1.78 +        | _ =>
    1.79 +          (case termify_apply_fmla thy config fmla2 of
    1.80 +            SOME tm2 => SOME (Term_FuncG (symb, tys, tms @ [tm2]))
    1.81 +          | NONE => NONE))
    1.82 +      end
    1.83 +    | _ => NONE)
    1.84 +  | termify_apply_fmla _ _ (Atom (THF_Atom_term tm)) = SOME tm
    1.85 +  | termify_apply_fmla _ _ _ = NONE
    1.86 +
    1.87  (*
    1.88   Information needed to be carried around:
    1.89   - constant mapping: maps constant names to Isabelle terms with fully-qualified
    1.90 @@ -508,29 +531,33 @@
    1.91      after each call of interpret_term since variables' cannot be bound across
    1.92      terms.
    1.93  *)
    1.94 -fun interpret_term formula_level config language const_map var_types type_map
    1.95 - tptp_t thy =
    1.96 +fun interpret_term formula_level config language const_map var_types type_map tptp_t thy =
    1.97    case tptp_t of
    1.98 -    Term_Func (symb, tptp_ts) =>
    1.99 +    Term_FuncG (symb, tptp_tys, tptp_ts) =>
   1.100         let
   1.101           val thy' =
   1.102             type_atoms_to_thy config formula_level type_map (Atom_App tptp_t) thy
   1.103         in
   1.104           case symb of
   1.105             Interpreted_ExtraLogic Apply =>
   1.106 +           (case strip_applies_term tptp_t of
   1.107 +             (Term_FuncG (symb, tptp_tys, tptp_ts), extra_tptp_ts) =>
   1.108 +             interpret_term formula_level config language const_map var_types type_map
   1.109 +               (Term_FuncG (symb, tptp_tys, tptp_ts @ extra_tptp_ts)) thy
   1.110 +           | _ =>
   1.111               (*apply the head of the argument list to the tail*)
   1.112               (mapply'
   1.113                 (fold_map (interpret_term false config language const_map
   1.114                  var_types type_map) (tl tptp_ts) thy')
   1.115                 (interpret_term formula_level config language const_map
   1.116 -                var_types type_map (hd tptp_ts)))
   1.117 -           | _ =>
   1.118 +                var_types type_map (hd tptp_ts))))
   1.119 +         | _ =>
   1.120                let
   1.121                  val typ_arity = type_arity_of_symbol thy' config symb
   1.122 -                val (tptp_type_args, tptp_term_args) = chop typ_arity tptp_ts
   1.123 +                val (tptp_type_args, tptp_term_args) = chop (typ_arity - length tptp_tys) tptp_ts
   1.124                  val tyargs =
   1.125 -                  map (interpret_type config thy' type_map o termtype_to_type)
   1.126 -                    tptp_type_args
   1.127 +                  map (interpret_type config thy' type_map)
   1.128 +                    (tptp_tys @ map termtype_to_type tptp_type_args)
   1.129                in
   1.130                  (*apply symb to tptp_ts*)
   1.131                  if is_prod_typed thy' config symb then
   1.132 @@ -604,38 +631,40 @@
   1.133  
   1.134  and interpret_formula config language const_map var_types type_map tptp_fmla thy =
   1.135    case tptp_fmla of
   1.136 -      Pred app =>
   1.137 +      Pred (symb, ts) =>
   1.138          interpret_term true config language const_map
   1.139 -         var_types type_map (Term_Func app) thy
   1.140 +         var_types type_map (Term_FuncG (symb, [], ts)) thy
   1.141      | Fmla (symbol, tptp_formulas) =>
   1.142         (case symbol of
   1.143            Interpreted_ExtraLogic Apply =>
   1.144 +          (case termify_apply_fmla thy config tptp_fmla of
   1.145 +            SOME tptp_t =>
   1.146 +            interpret_term true config language const_map var_types type_map tptp_t thy
   1.147 +          | NONE =>
   1.148              mapply'
   1.149                (fold_map (interpret_formula config language const_map
   1.150                 var_types type_map) (tl tptp_formulas) thy)
   1.151                (interpret_formula config language const_map
   1.152 -               var_types type_map (hd tptp_formulas))
   1.153 +               var_types type_map (hd tptp_formulas)))
   1.154          | Uninterpreted const_name =>
   1.155              let
   1.156                val (args, thy') = (fold_map (interpret_formula config language
   1.157 -               const_map var_types type_map) tptp_formulas thy)
   1.158 +                const_map var_types type_map) tptp_formulas thy)
   1.159                val thy' =
   1.160                  type_atoms_to_thy config true type_map
   1.161 -                 (Atom_Arity (const_name, length tptp_formulas)) thy'
   1.162 +                  (Atom_Arity (const_name, length tptp_formulas)) thy'
   1.163              in
   1.164                (if is_prod_typed thy' config symbol then
   1.165                   mtimes thy' args (interpret_symbol config const_map symbol [] thy')
   1.166                 else
   1.167 -                mapply args (interpret_symbol config const_map symbol [] thy'),
   1.168 +                 mapply args (interpret_symbol config const_map symbol [] thy'),
   1.169                thy')
   1.170              end
   1.171          | _ =>
   1.172              let
   1.173                val (args, thy') =
   1.174 -                fold_map
   1.175 -                 (interpret_formula config language
   1.176 -                  const_map var_types type_map)
   1.177 -                 tptp_formulas thy
   1.178 +                fold_map (interpret_formula config language const_map var_types type_map)
   1.179 +                  tptp_formulas thy
   1.180              in
   1.181                (if is_prod_typed thy' config symbol then
   1.182                   mtimes thy' args (interpret_symbol config const_map symbol [] thy')
   1.183 @@ -737,19 +766,20 @@
   1.184        | _ => ([], tptp_type)
   1.185  in
   1.186    fun typeof_typing (THF_typing (_, tptp_type)) = extract_type tptp_type
   1.187 -  fun typeof_tff_typing (Atom (TFF_Typed_Atom (_, SOME tptp_type))) =
   1.188 -    extract_type tptp_type
   1.189 +    | typeof_typing (Atom (TFF_Typed_Atom (_, SOME tptp_type))) = extract_type tptp_type
   1.190  end
   1.191  
   1.192 -fun nameof_typing
   1.193 -  (THF_typing
   1.194 -     ((Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))), _)) = str
   1.195 -fun nameof_tff_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str
   1.196 +fun nameof_typing (THF_typing
   1.197 +     ((Atom (THF_Atom_term (Term_FuncG (Uninterpreted str, [], [])))), _)) = str
   1.198 +  | nameof_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str
   1.199  
   1.200  fun strip_prod_type (Prod_type (ty1, ty2)) = ty1 :: strip_prod_type ty2
   1.201    | strip_prod_type ty = [ty]
   1.202  
   1.203 -fun dest_fn_type (Fn_type (ty1, ty2)) = (strip_prod_type ty1, ty2)
   1.204 +fun dest_fn_type (Fn_type (ty1, ty2)) =
   1.205 +    let val (tys2, ty3) = dest_fn_type ty2 in
   1.206 +      (strip_prod_type ty1 @ tys2, ty3)
   1.207 +    end
   1.208    | dest_fn_type ty = ([], ty)
   1.209  
   1.210  fun resolve_include_path path_prefixes path_suffix =
   1.211 @@ -758,11 +788,16 @@
   1.212      SOME prefix => Path.append prefix path_suffix
   1.213    | NONE => error ("Cannot find include file " ^ Path.print path_suffix)
   1.214  
   1.215 -(* Ideally, to be in sync with TFF1, we should perform full type skolemization here.
   1.216 -   But the problems originating from HOL systems are restricted to top-level
   1.217 -   universal quantification for types. *)
   1.218 +fun is_type_type (Fmla_type (Atom (THF_Atom_term (Term_FuncG (TypeSymbol Type_Type, [], []))))) =
   1.219 +    true
   1.220 +  | is_type_type (Defined_type Type_Type) = true
   1.221 +  | is_type_type _ = false;
   1.222 +
   1.223 +(* Ideally, to be in sync with TFF1/THF1, we should perform full type
   1.224 +   skolemization here. But the problems originating from HOL systems are
   1.225 +   restricted to top-level universal quantification for types. *)
   1.226  fun remove_leading_type_quantifiers (Quant (Forall, varlist, tptp_fmla)) =
   1.227 -    (case filter_out (curry (op =) (SOME (Defined_type Type_Type)) o snd) varlist of
   1.228 +    (case filter_out (fn (_, SOME ty) => is_type_type ty | _ => false) varlist of
   1.229        [] => remove_leading_type_quantifiers tptp_fmla
   1.230      | varlist' => Quant (Forall, varlist', tptp_fmla))
   1.231    | remove_leading_type_quantifiers tptp_fmla = tptp_fmla
   1.232 @@ -788,12 +823,8 @@
   1.233             Role_Type =>
   1.234               let
   1.235                 val ((tptp_type_vars, tptp_ty), name) =
   1.236 -                 if lang = THF then
   1.237 -                   (typeof_typing tptp_formula (*assuming tptp_formula is a typing*),
   1.238 -                    nameof_typing tptp_formula (*and that the LHS is a (atom) name*))
   1.239 -                 else
   1.240 -                   (typeof_tff_typing tptp_formula,
   1.241 -                    nameof_tff_typing tptp_formula)
   1.242 +                 (typeof_typing tptp_formula (*assuming tptp_formula is a typing*),
   1.243 +                  nameof_typing tptp_formula (*and that the LHS is a (atom) name*))
   1.244               in
   1.245                 case dest_fn_type tptp_ty of
   1.246                   (tptp_binders, Defined_type Type_Type) => (*add new type*)
   1.247 @@ -865,7 +896,7 @@
   1.248                 (*gather interpreted term, and the map of types occurring in that term*)
   1.249                 val (t, thy') =
   1.250                   interpret_formula config lang
   1.251 -                  const_map [] type_map (remove_leading_type_quantifiers tptp_formula) thy
   1.252 +                   const_map [] type_map (remove_leading_type_quantifiers tptp_formula) thy
   1.253                   |>> HOLogic.mk_Trueprop
   1.254                 (*type_maps grow monotonically, so return the newest value (type_mapped);
   1.255                 there's no need to unify it with the type_map parameter.*)
     2.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Dec 14 09:19:50 2016 +0100
     2.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Dec 14 18:52:17 2016 +0100
     2.3 @@ -81,7 +81,7 @@
     2.4      | General_List of general_term list
     2.5  
     2.6    and tptp_term =
     2.7 -      Term_Func of symbol * tptp_term list
     2.8 +      Term_FuncG of symbol * tptp_type list (*special hack for TPTP_Interpret*) * tptp_term list
     2.9      | Term_Var of string
    2.10      | Term_Conditional of tptp_formula * tptp_term * tptp_term
    2.11      | Term_Num of number_kind * string
    2.12 @@ -118,6 +118,8 @@
    2.13      | Fmla_type of tptp_formula
    2.14      | Subtype of symbol * symbol (*only THF*)
    2.15  
    2.16 +  val Term_Func: symbol * tptp_term list -> tptp_term (*for Yacc parser*)
    2.17 +
    2.18    type general_list = general_term list
    2.19    type parent_details = general_list
    2.20    type useful_info = general_term list
    2.21 @@ -230,7 +232,7 @@
    2.22      | General_List of general_term list
    2.23  
    2.24    and tptp_term =
    2.25 -      Term_Func of symbol * tptp_term list
    2.26 +      Term_FuncG of symbol * tptp_type list (*special hack for TPTP_Interpret*) * tptp_term list
    2.27      | Term_Var of string
    2.28      | Term_Conditional of tptp_formula * tptp_term * tptp_term
    2.29      | Term_Num of number_kind * string
    2.30 @@ -267,6 +269,8 @@
    2.31      | Fmla_type of tptp_formula
    2.32      | Subtype of symbol * symbol
    2.33  
    2.34 +fun Term_Func (symb, ts) = Term_FuncG (symb, [], ts)
    2.35 +
    2.36  type general_list = general_term list
    2.37  type parent_details = general_list
    2.38  type useful_info = general_term list
    2.39 @@ -405,9 +409,10 @@
    2.40  
    2.41  fun string_of_tptp_term x =
    2.42    case x of
    2.43 -      Term_Func (symbol, tptp_term_list) =>
    2.44 +      Term_FuncG (symbol, tptp_type_list, tptp_term_list) =>
    2.45          "(" ^ string_of_symbol symbol ^ " " ^
    2.46 -        space_implode " " (map string_of_tptp_term tptp_term_list) ^ ")"
    2.47 +        space_implode " " (map string_of_tptp_type tptp_type_list
    2.48 +          @ map string_of_tptp_term tptp_term_list) ^ ")"
    2.49      | Term_Var str => str
    2.50      | Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*)
    2.51      | Term_Num (_, str) => str
    2.52 @@ -531,22 +536,23 @@
    2.53  (*infix symbols, including \subset, \cup, \cap*)
    2.54  fun latex_of_tptp_term x =
    2.55    case x of
    2.56 -      Term_Func (Interpreted_Logic Equals, [tptp_t1, tptp_t2]) =>
    2.57 +      Term_FuncG (Interpreted_Logic Equals, [], [tptp_t1, tptp_t2]) =>
    2.58          "(" ^ latex_of_tptp_term tptp_t1 ^ " = " ^ latex_of_tptp_term tptp_t2 ^ ")"
    2.59 -    | Term_Func (Interpreted_Logic NEquals, [tptp_t1, tptp_t2]) =>
    2.60 +    | Term_FuncG (Interpreted_Logic NEquals, [], [tptp_t1, tptp_t2]) =>
    2.61          "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\neq " ^ latex_of_tptp_term tptp_t2 ^ ")"
    2.62 -    | Term_Func (Interpreted_Logic Or, [tptp_t1, tptp_t2]) =>
    2.63 +    | Term_FuncG (Interpreted_Logic Or, [], [tptp_t1, tptp_t2]) =>
    2.64          "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\vee " ^ latex_of_tptp_term tptp_t2 ^ ")"
    2.65 -    | Term_Func (Interpreted_Logic And, [tptp_t1, tptp_t2]) =>
    2.66 +    | Term_FuncG (Interpreted_Logic And, [], [tptp_t1, tptp_t2]) =>
    2.67          "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\wedge " ^ latex_of_tptp_term tptp_t2 ^ ")"
    2.68 -    | Term_Func (Interpreted_Logic Iff, [tptp_t1, tptp_t2]) =>
    2.69 +    | Term_FuncG (Interpreted_Logic Iff, [], [tptp_t1, tptp_t2]) =>
    2.70          "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")"
    2.71 -    | Term_Func (Interpreted_Logic If, [tptp_t1, tptp_t2]) =>
    2.72 +    | Term_FuncG (Interpreted_Logic If, [], [tptp_t1, tptp_t2]) =>
    2.73          "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")"
    2.74  
    2.75 -    | Term_Func (symbol, tptp_term_list) =>
    2.76 +    | Term_FuncG (symbol, tptp_type_list, tptp_term_list) =>
    2.77          (*"(" ^*) latex_of_symbol symbol ^ "\\\\, " ^
    2.78 -        space_implode "\\\\, " (map latex_of_tptp_term tptp_term_list) (*^ ")"*)
    2.79 +        space_implode "\\\\, " (map latex_of_tptp_type tptp_type_list
    2.80 +          @ map latex_of_tptp_term tptp_term_list) (*^ ")"*)
    2.81      | Term_Var str => "\\\\mathrm{" ^ str ^ "}"
    2.82      | Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*)
    2.83      | Term_Num (_, str) => str
    2.84 @@ -647,10 +653,10 @@
    2.85        latex_of_symbol symbol ^
    2.86         space_implode "\\\\, " (map latex_of_tptp_term tptp_term_list)
    2.87  
    2.88 -  | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "union", []))), tptp_f1]), tptp_f2])) =
    2.89 +  | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_FuncG (Uninterpreted "union", [], []))), tptp_f1]), tptp_f2])) =
    2.90        "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_f2 ^ ")"
    2.91  
    2.92 -  | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "subset", []))), tptp_f1]), tptp_f2])) =
    2.93 +  | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_FuncG (Uninterpreted "subset", [], []))), tptp_f1]), tptp_f2])) =
    2.94        "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_f2 ^ ")"
    2.95  
    2.96    | latex_of_tptp_formula (Fmla (Interpreted_Logic Equals, [tptp_f1, tptp_f2])) =
     3.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Wed Dec 14 09:19:50 2016 +0100
     3.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Wed Dec 14 18:52:17 2016 +0100
     3.3 @@ -96,7 +96,7 @@
     3.4    which we interpret to be the last line of the proof.*)
     3.5  fun is_last_line CNF (Pred (Interpreted_Logic False, [])) = true
     3.6    | is_last_line THF (Atom (THF_Atom_term
     3.7 -      (Term_Func (Interpreted_Logic False, [])))) = true
     3.8 +      (Term_Func (Interpreted_Logic False, [], [])))) = true
     3.9    | is_last_line _ _ = false
    3.10  
    3.11  fun tptp_dot_node with_label reverse_arrows