1.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu Aug 16 14:07:32 2012 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu Aug 16 15:41:36 2012 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4      Timing.timing
     1.5        (TPTP_Interpret.interpret_file
     1.6         false
     1.7 -       (Path.dir tptp_probs_dir)
     1.8 +       [Path.explode "$TPTP"]
     1.9         (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
    1.10         []
    1.11         [])
    1.12 @@ -38,7 +38,7 @@
    1.13      TimeLimit.timeLimit (Time.fromSeconds (if timeout = 0 then 60 else timeout))
    1.14       (TPTP_Interpret.interpret_file
    1.15         false
    1.16 -       (Path.dir tptp_probs_dir)
    1.17 +       [Path.explode "$TPTP"]
    1.18         file
    1.19         []
    1.20         []) thy

     2.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Aug 16 14:07:32 2012 +0200
     2.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Aug 16 15:41:36 2012 +0200
     2.3 @@ -70,31 +70,32 @@
     2.4        given to force a specific mapping: this is usually done for using an
     2.5        imported TPTP problem in Isar.
     2.6      const_map = as previous, but for constants.
     2.7 -    path_prefix = path where TPTP problems etc are located (to help the "include"
     2.8 -      directive find the files.
     2.9 +    path_prefixes = paths where TPTP problems etc are located (to help the
    2.10 +      "include" directive find the files.
    2.11      line = parsed TPTP line
    2.12      thy = theory where interpreted info will be stored.
    2.13    *)
    2.14    val interpret_line : config -> string list -> type_map -> const_map ->
    2.15 -    Path.T -> TPTP_Syntax.tptp_line -> theory -> tptp_general_meaning * theory
    2.16 +    Path.T list -> TPTP_Syntax.tptp_line -> theory ->
    2.17 +    tptp_general_meaning * theory
    2.18  
    2.19    (*Like "interpret_line" above, but works over a whole parsed problem.
    2.20      Arguments:
    2.21        config = as previously
    2.22        inclusion list = as previously
    2.23 -      path_prefix = as previously
    2.24 +      path_prefixes = as previously
    2.25        lines = parsed TPTP syntax
    2.26        type_map = as previously
    2.27        const_map = as previously
    2.28        thy = as previously
    2.29    *)
    2.30 -  val interpret_problem : config -> string list -> Path.T ->
    2.31 +  val interpret_problem : config -> string list -> Path.T list ->
    2.32      TPTP_Syntax.tptp_line list -> type_map -> const_map -> theory ->
    2.33      tptp_general_meaning * theory
    2.34  
    2.35    (*Like "interpret_problem" above, but it is given a filename rather than
    2.36    a parsed problem.*)
    2.37 -  val interpret_file : bool -> Path.T -> Path.T -> type_map -> const_map ->
    2.38 +  val interpret_file : bool -> Path.T list -> Path.T -> type_map -> const_map ->
    2.39      theory -> tptp_general_meaning * theory
    2.40  
    2.41    type position = string * int * int
    2.42 @@ -104,7 +105,7 @@
    2.43    exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term
    2.44    exception MISINTERPRET_TYPE of string * TPTP_Syntax.tptp_type
    2.45  
    2.46 -  val import_file : bool -> Path.T -> Path.T -> type_map -> const_map ->
    2.47 +  val import_file : bool -> Path.T list -> Path.T -> type_map -> const_map ->
    2.48      theory -> theory
    2.49  
    2.50    (*Imported TPTP files are stored as "manifests" in the theory.*)
    2.51 @@ -322,9 +323,6 @@
    2.52    | mk_fun_type (ty :: tys) b acc =
    2.53        mk_fun_type tys b (fn ty_rest => Type ("fun", [ty, acc ty_rest]))
    2.54  
    2.55 -fun dummy_term () =
    2.56 -  HOLogic.choice_const Term.dummyT $ Term.absdummy Term.dummyT @{term "True"}
    2.57 -
    2.58  (*These arities are not part of the TPTP spec*)
    2.59  fun arity_of interpreted_symbol = case interpreted_symbol of
    2.60      UMinus => 1
    2.61 @@ -390,7 +388,7 @@
    2.62     | TypeSymbol _ =>
    2.63         raise MISINTERPRET_SYMBOL
    2.64          ("Cannot have TypeSymbol in term", symb)
    2.65 -   | System str =>
    2.66 +   | System _ =>
    2.67         raise MISINTERPRET_SYMBOL
    2.68          ("Cannot interpret system symbol", symb)
    2.69  
    2.70 @@ -445,7 +443,6 @@
    2.71          declare_const_ifnot config const_name
    2.72           (mk_fun_type (replicate n_args ind_type) value_type I) thy
    2.73          |> snd
    2.74 -    | _ => thy
    2.75    end
    2.76  
    2.77  (*FIXME only used until interpretation is implemented*)
    2.78 @@ -498,8 +495,6 @@
    2.79         let
    2.80           val thy' =
    2.81             type_atoms_to_thy config formula_level type_map (Atom_App tptp_t) thy
    2.82 -         fun typeof_const const_name = Sign.the_const_type thy'
    2.83 -             (Sign.full_name thy' (mk_binding config const_name))
    2.84         in
    2.85           case symb of
    2.86             Interpreted_ExtraLogic Apply =>
    2.87 @@ -708,18 +703,22 @@
    2.88       ((Atom (THF_Atom_term (Term_Func (Uninterpreted str, [])))), _)) = str
    2.89  fun nameof_tff_typing (Atom (TFF_Typed_Atom (Uninterpreted str, _))) = str
    2.90  
    2.91 -fun interpret_line config inc_list type_map const_map path_prefix line thy =
    2.92 +fun resolve_include_path path_prefixes path_suffix =
    2.93 +  case find_first (fn prefix => File.exists (Path.append prefix path_suffix))
    2.94 +         path_prefixes of
    2.95 +    SOME prefix => Path.append prefix path_suffix
    2.96 +  | NONE =>
    2.97 +    error ("Cannot find include file " ^ quote (Path.implode path_suffix))
    2.98 +
    2.99 +fun interpret_line config inc_list type_map const_map path_prefixes line thy =
   2.100    case line of
   2.101       Include (_, quoted_path, inc_list) =>
   2.102         interpret_file'
   2.103          config
   2.104          inc_list
   2.105 -        path_prefix
   2.106 -        (Path.append
   2.107 -          path_prefix
   2.108 -          (quoted_path
   2.109 -           |> unenclose
   2.110 -           |> Path.explode))
   2.111 +        path_prefixes
   2.112 +        (resolve_include_path path_prefixes
   2.113 +           (quoted_path |> unenclose |> Path.explode))
   2.114          type_map
   2.115          const_map
   2.116          thy
   2.117 @@ -731,7 +730,6 @@
   2.118           case role of
   2.119             Role_Type =>
   2.120               let
   2.121 -               val thy_name = Context.theory_name thy
   2.122                 val (tptp_ty, name) =
   2.123                   if lang = THF then
   2.124                     (typeof_typing tptp_formula (*assuming tptp_formula is a typing*),
   2.125 @@ -818,17 +816,15 @@
   2.126         else (*do nothing if we're not to includ this AF*)
   2.127           ((type_map, const_map, []), thy)
   2.128  
   2.129 -and interpret_problem config inc_list path_prefix lines type_map const_map thy =
   2.130 -  let
   2.131 -    val thy_name = Context.theory_name thy
   2.132 -    val thy_with_symbols = add_interp_symbols_to_thy config type_map thy
   2.133 -  in
   2.134 +and interpret_problem config inc_list path_prefixes lines type_map const_map thy =
   2.135 +  let val thy_with_symbols = add_interp_symbols_to_thy config type_map thy in
   2.136      fold (fn line =>
   2.137             fn ((type_map, const_map, lines), thy) =>
   2.138               let
   2.139                 (*process the line, ignoring the type-context for variables*)
   2.140                 val ((type_map', const_map', l'), thy') =
   2.141 -                 interpret_line config inc_list type_map const_map path_prefix line thy
   2.142 +                 interpret_line config inc_list type_map const_map path_prefixes
   2.143 +                   line thy
   2.144                   (*FIXME
   2.145                     handle
   2.146                       (*package all exceptions to include position information,
   2.147 @@ -851,32 +847,32 @@
   2.148           ((type_map, const_map, []), thy_with_symbols) (*initial values*)
   2.149    end
   2.150  
   2.151 -and interpret_file' config inc_list path_prefix file_name =
   2.152 +and interpret_file' config inc_list path_prefixes file_name =
   2.153    let
   2.154      val file_name' = Path.expand file_name
   2.155    in
   2.156      if Path.is_absolute file_name' then
   2.157        Path.implode file_name
   2.158        |> TPTP_Parser.parse_file
   2.159 -      |> interpret_problem config inc_list path_prefix
   2.160 +      |> interpret_problem config inc_list path_prefixes
   2.161      else error "Could not determine absolute path to file"
   2.162    end
   2.163  
   2.164 -and interpret_file cautious path_prefix file_name =
   2.165 +and interpret_file cautious path_prefixes file_name =
   2.166    let
   2.167      val config =
   2.168        {cautious = cautious,
   2.169         problem_name =
   2.170          SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode)
   2.171           file_name))}
   2.172 -  in interpret_file' config [] path_prefix file_name end
   2.173 +  in interpret_file' config [] path_prefixes file_name end
   2.174  
   2.175 -fun import_file cautious path_prefix file_name type_map const_map thy =
   2.176 +fun import_file cautious path_prefixes file_name type_map const_map thy =
   2.177    let
   2.178      val prob_name =
   2.179        TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name))
   2.180      val (result, thy') =
   2.181 -      interpret_file cautious path_prefix file_name type_map const_map thy
   2.182 +      interpret_file cautious path_prefixes file_name type_map const_map thy
   2.183    (*FIXME doesn't check if problem has already been interpreted*)
   2.184    in TPTP_Data.map (cons ((prob_name, result))) thy' end
   2.185  
   2.186 @@ -886,6 +882,6 @@
   2.187        Toplevel.theory (fn thy =>
   2.188         (*NOTE: assumes include files are located at $TPTP/Axioms
   2.189           (which is how TPTP is organised)*)
   2.190 -       import_file true (Path.explode "$TPTP") path [] [] thy)))
   2.191 +       import_file true [Path.dir path, Path.explode "$TPTP"] path [] [] thy)))
   2.192  
   2.193  end

     3.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Thu Aug 16 14:07:32 2012 +0200
     3.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Thu Aug 16 15:41:36 2012 +0200
     3.3 @@ -56,7 +56,8 @@
     3.4               path |> not (Path.is_absolute path)
     3.5                       ? Path.append (Path.explode "$PWD"))
     3.6      val ((_, _, problem), thy) =
     3.7 -      TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
     3.8 +      TPTP_Interpret.interpret_file true [Path.dir path, Path.explode "$TPTP"]
     3.9 +                                    path [] [] thy
    3.10      val (conjs, defs_and_nondefs) =
    3.11        problem |> List.partition (has_role TPTP_Syntax.Role_Conjecture)
    3.12                ||> List.partition (has_role TPTP_Syntax.Role_Definition)