registering code_prolog as component; using environment variable; adding settings file for prolog code generation
authorbulwahn
Thu Sep 16 13:49:06 2010 +0200 (2010-09-16)
changeset 394623a86194d1534
parent 39461 0ed0f015d140
child 39463 7ce0ed8dc4d6
registering code_prolog as component; using environment variable; adding settings file for prolog code generation
etc/components
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/etc/settings
     1.1 --- a/etc/components	Thu Sep 16 13:49:04 2010 +0200
     1.2 +++ b/etc/components	Thu Sep 16 13:49:06 2010 +0200
     1.3 @@ -17,3 +17,4 @@
     1.4  src/HOL/Mirabelle
     1.5  src/HOL/Library/Sum_Of_Squares
     1.6  src/HOL/Tools/SMT
     1.7 +src/HOL/Tools/Predicate_Compile
     2.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Sep 16 13:49:04 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Sep 16 13:49:06 2010 +0200
     2.3 @@ -104,8 +104,11 @@
     2.4  
     2.5  datatype prolog_system = SWI_PROLOG | YAP
     2.6  
     2.7 +fun string_of_system SWI_PROLOG = "swiprolog"
     2.8 +  | string_of_system YAP = "yap"
     2.9 +
    2.10  type system_configuration = {timeout : Time.time, prolog_system : prolog_system}
    2.11 -
    2.12 +                                                
    2.13  structure System_Config = Generic_Data
    2.14  (
    2.15    type T = system_configuration
    2.16 @@ -638,6 +641,7 @@
    2.17    in
    2.18      fst (fold_map reorder' p [])
    2.19    end
    2.20 +
    2.21  (* rename variables to prolog-friendly names *)
    2.22  
    2.23  fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v))
    2.24 @@ -739,9 +743,16 @@
    2.25  
    2.26  fun invoke system file_name =
    2.27    let
    2.28 +    val env_var =
    2.29 +      (case system of SWI_PROLOG => "EXEC_SWIPL"| YAP => "EXEC_YAP")
    2.30 +    val prog = getenv env_var
    2.31      val cmd =
    2.32 -      case system of SWI_PROLOG => "/usr/local/bin/swipl -f " | YAP => "/usr/local/bin/yap -L "
    2.33 -  in fst (bash_output (cmd ^ file_name)) end
    2.34 +      case system of SWI_PROLOG => prog ^ " -f " | YAP => prog ^ " -L "
    2.35 +  in
    2.36 +    if prog = "" then
    2.37 +      (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
    2.38 +    else fst (bash_output (cmd ^ file_name))
    2.39 +  end
    2.40  
    2.41  (* parsing prolog solution *)
    2.42  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/etc/settings	Thu Sep 16 13:49:06 2010 +0200
     3.3 @@ -0,0 +1,13 @@
     3.4 +
     3.5 +EXEC_SWIPL=$(choosefrom \
     3.6 +  "$ISABELLE_HOME/contrib/swipl/bin/swipl" \
     3.7 +  "$ISABELLE_HOME/contrib_devel/swipl/bin/swipl" \
     3.8 +  "$ISABELLE_HOME/../swipl" \
     3.9 +  $(type -p swipl) \
    3.10 +  "")
    3.11 +
    3.12 +EXEC_YAP=$(choosefrom \
    3.13 +  "$ISABELLE_HOME/contrib/yap" \
    3.14 +  "$ISABELLE_HOME/../yap" \
    3.15 +  $(type -p yap) \
    3.16 +  "")