src/HOL/Tools/Predicate_Compile/code_prolog.ML
changeset 39462 3a86194d1534
parent 39461 0ed0f015d140
child 39464 13493d3c28d0
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Sep 16 13:49:04 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Sep 16 13:49:06 2010 +0200
     1.3 @@ -104,8 +104,11 @@
     1.4  
     1.5  datatype prolog_system = SWI_PROLOG | YAP
     1.6  
     1.7 +fun string_of_system SWI_PROLOG = "swiprolog"
     1.8 +  | string_of_system YAP = "yap"
     1.9 +
    1.10  type system_configuration = {timeout : Time.time, prolog_system : prolog_system}
    1.11 -
    1.12 +                                                
    1.13  structure System_Config = Generic_Data
    1.14  (
    1.15    type T = system_configuration
    1.16 @@ -638,6 +641,7 @@
    1.17    in
    1.18      fst (fold_map reorder' p [])
    1.19    end
    1.20 +
    1.21  (* rename variables to prolog-friendly names *)
    1.22  
    1.23  fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v))
    1.24 @@ -739,9 +743,16 @@
    1.25  
    1.26  fun invoke system file_name =
    1.27    let
    1.28 +    val env_var =
    1.29 +      (case system of SWI_PROLOG => "EXEC_SWIPL"| YAP => "EXEC_YAP")
    1.30 +    val prog = getenv env_var
    1.31      val cmd =
    1.32 -      case system of SWI_PROLOG => "/usr/local/bin/swipl -f " | YAP => "/usr/local/bin/yap -L "
    1.33 -  in fst (bash_output (cmd ^ file_name)) end
    1.34 +      case system of SWI_PROLOG => prog ^ " -f " | YAP => prog ^ " -L "
    1.35 +  in
    1.36 +    if prog = "" then
    1.37 +      (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
    1.38 +    else fst (bash_output (cmd ^ file_name))
    1.39 +  end
    1.40  
    1.41  (* parsing prolog solution *)
    1.42