src/HOL/TPTP/TPTP_Parser/tptp_problem_name.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46844 5d9aab0c609c
child 47520 ef2d04520337
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     1
(*  Title:      HOL/TPTP/TPTP_Parser/tptp_problem_name.ML
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     2
    Author:     Nik Sultana, Cambridge University Computer Laboratory
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     3
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     4
Scans a TPTP problem name. Naming convention is described
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     5
http://www.cs.miami.edu/~tptp/TPTP/TR/TPTPTR.shtml#Problem and Axiomatization Naming
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     6
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     7
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     8
signature TPTP_PROBLEM_NAME =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     9
sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    10
  datatype suffix =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    11
      Problem of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    12
        ((*version*)int *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    13
        (*size parameter*)int option) *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    14
        (*extension*)string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    15
    | Axiom of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    16
        (*specialisation*)int *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    17
        (*extension*)string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    18
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    19
  type tptp_problem_name =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    20
    {prob_domain : string,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    21
     prob_number : int,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    22
     prob_form : TPTP_Syntax.language,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    23
     suffix : suffix}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    24
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    25
  datatype problem_name =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    26
      Standard of tptp_problem_name
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    27
    | Nonstandard of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    28
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    29
  exception TPTP_PROBLEM_NAME of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    30
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    31
  val parse_problem_name : string -> problem_name
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    32
  val mangle_problem_name : problem_name -> string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    33
end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    34
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    35
structure TPTP_Problem_Name: TPTP_PROBLEM_NAME =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    36
struct
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    37
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    38
(*some basic tokens*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    39
val numerics = map Char.chr (48 upto 57) (*0..9*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    40
val alphabetics =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    41
  map Char.chr (65 upto 90) @ (*A..Z*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    42
  map Char.chr (97 upto 122)  (*a..z*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    43
(*TPTP formula forms*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    44
val forms = [#"^", #"_", #"=", #"+", #"-"]
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    45
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    46
(*lift a list of characters into a scanner combinator matching any one of the
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    47
characters in that list.*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    48
fun lift l =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    49
  (map (Char.toString #> ($$)) l, Scan.fail)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    50
  |-> fold (fn x => fn y => x || y)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    51
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    52
(*combinators for parsing letters and numbers*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    53
val alpha = lift alphabetics
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    54
val numer = lift numerics
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    55
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    56
datatype suffix =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    57
    Problem of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    58
      ((*version*)int *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    59
      (*size parameter*)int option) *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    60
      (*extension*)string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    61
  | Axiom of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    62
      (*specialisation*)int *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    63
      (*extension*)string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    64
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    65
val to_int = Int.fromString #> the
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    66
val rm_ending = Scan.this_string "rm"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    67
val ax_ending =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    68
  ((numer >> to_int) --|
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    69
   $$ "." -- (Scan.this_string "eq" || Scan.this_string "ax" || rm_ending))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    70
  >> Axiom
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    71
val prob_ending = $$ "p" || $$ "g" || rm_ending
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    72
val prob_suffix =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    73
  ((numer >> to_int) --
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    74
   Scan.option ($$ "." |-- numer ^^ numer ^^ numer >> to_int) --| $$ "."
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    75
   -- prob_ending)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    76
  >> Problem
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    77
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    78
type tptp_problem_name =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    79
  {prob_domain : string,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    80
   prob_number : int,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    81
   prob_form : TPTP_Syntax.language,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    82
   suffix : suffix}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    83
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    84
datatype problem_name =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    85
    Standard of tptp_problem_name
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    86
  | Nonstandard of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    87
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    88
exception TPTP_PROBLEM_NAME of string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    89
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    90
(*FIXME add graceful handling on non-wellformed TPTP filenames*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    91
fun parse_problem_name str' : problem_name =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    92
  let
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    93
    val str = Symbol.explode str'
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    94
    (*NOTE there's an ambiguity in the spec: there's no way of knowing if a
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    95
    file ending in "rm" used to be "ax" or "p". Here we default to "p".*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    96
    val ((((prob_domain, prob_number), prob_form), suffix), rest) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    97
     Scan.finite Symbol.stopper
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    98
     ((alpha ^^ alpha ^^ alpha) --
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    99
     (numer ^^ numer ^^ numer >> to_int) --
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   100
     lift forms -- (prob_suffix || ax_ending)) str
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   101
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   102
    fun parse_form str =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   103
      case str of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   104
        "^" => TPTP_Syntax.THF
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   105
      | "_" => TPTP_Syntax.TFF
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   106
      | "=" => TPTP_Syntax.TFF_with_arithmetic
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   107
      | "+" => TPTP_Syntax.FOF
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   108
      | "-" => TPTP_Syntax.CNF
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   109
      | _ => raise TPTP_PROBLEM_NAME ("Unknown TPTP form: " ^ str)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   110
  in
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   111
    if null rest (*check if the whole name was parsed*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   112
    then
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   113
      Standard
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   114
        {prob_domain = prob_domain,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   115
         prob_number = prob_number,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   116
         prob_form = parse_form prob_form,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   117
         suffix = suffix}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   118
      handle _ => Nonstandard str'
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   119
    else raise TPTP_PROBLEM_NAME ("Parse error")
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   120
  end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   121
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   122
(*Produces an ASCII encoding of a TPTP problem-file name.*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   123
fun mangle_problem_name (prob : problem_name) : string =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   124
  case prob of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   125
     Standard tptp_prob =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   126
       let
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   127
         val prob_form =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   128
           case #prob_form tptp_prob of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   129
             TPTP_Syntax.THF => "_thf_"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   130
           | TPTP_Syntax.TFF => "_tff_"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   131
           | TPTP_Syntax.TFF_with_arithmetic => "_thfwa_"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   132
           | TPTP_Syntax.FOF => "_fof_"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   133
           | TPTP_Syntax.CNF => "_cnf_"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   134
         val suffix =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   135
           case #suffix tptp_prob of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   136
             Problem ((version, size), extension) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   137
               Int.toString version ^ "_" ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   138
               (if is_some size then Int.toString (the size) ^ "_" else "") ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   139
               extension
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   140
           | Axiom (specialisation, extension) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   141
               Int.toString specialisation ^ "_" ^ extension
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   142
       in
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   143
         #prob_domain tptp_prob ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   144
         Int.toString (#prob_number tptp_prob) ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   145
         prob_form ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   146
         suffix
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   147
       end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   148
   | Nonstandard str => str
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   149
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   150
end