1.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Aug 26 14:48:48 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Fri Aug 27 09:34:06 2010 +0200
     1.3 @@ -4,13 +4,24 @@
     1.4  
     1.5  section {* Example append *}
     1.6  
     1.7 +
     1.8  inductive append
     1.9  where
    1.10    "append [] ys ys"
    1.11  | "append xs ys zs ==> append (x # xs) ys (x # zs)"
    1.12  
    1.13 +ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.14 +
    1.15 +values "{(x, y, z). append x y z}"
    1.16 +
    1.17  values 3 "{(x, y, z). append x y z}"
    1.18  
    1.19 +ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.YAP} *}
    1.20 +
    1.21 +values "{(x, y, z). append x y z}"
    1.22 +
    1.23 +ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.24 +
    1.25  
    1.26  section {* Example queens *}
    1.27  
    1.28 @@ -172,7 +183,7 @@
    1.29  where
    1.30    "y \<noteq> B \<Longrightarrow> notB y"
    1.31  
    1.32 -ML {* Code_Prolog.options := {ensure_groundness = true, limited_types = []} *}
    1.33 +ML {* Code_Prolog.options := {ensure_groundness = true, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.34  
    1.35  values 2 "{y. notB y}"
    1.36  

     2.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 26 14:48:48 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Aug 27 09:34:06 2010 +0200
     2.3 @@ -6,7 +6,9 @@
     2.4  
     2.5  signature CODE_PROLOG =
     2.6  sig
     2.7 -  type code_options = {ensure_groundness : bool, limited_types : (typ * int) list}
     2.8 +  datatype prolog_system = SWI_PROLOG | YAP
     2.9 +  type code_options =
    2.10 +    {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
    2.11    val options : code_options ref
    2.12  
    2.13    datatype arith_op = Plus | Minus
    2.14 @@ -21,10 +23,10 @@
    2.15    type clause = ((string * prol_term list) * prem);
    2.16    type logic_program = clause list;
    2.17    type constant_table = (string * string) list
    2.18 -    
    2.19 -  val generate : code_options -> Proof.context -> string -> (logic_program * constant_table)
    2.20 +
    2.21 +  val generate : bool -> Proof.context -> string -> (logic_program * constant_table)
    2.22    val write_program : logic_program -> string
    2.23 -  val run : logic_program -> string -> string list -> int option -> prol_term list list
    2.24 +  val run : prolog_system -> logic_program -> string -> string list -> int option -> prol_term list list
    2.25  
    2.26    val quickcheck : Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
    2.27  
    2.28 @@ -42,9 +44,13 @@
    2.29  
    2.30  (* code generation options *)
    2.31  
    2.32 -type code_options = {ensure_groundness : bool, limited_types : (typ * int) list}
    2.33 +datatype prolog_system = SWI_PROLOG | YAP
    2.34  
    2.35 -val options = Unsynchronized.ref {ensure_groundness = false, limited_types = []};
    2.36 +type code_options =
    2.37 +  {ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system}
    2.38 +
    2.39 +val options = Unsynchronized.ref {ensure_groundness = false, limited_types = [],
    2.40 +  prolog_system = SWI_PROLOG};
    2.41  
    2.42  (* general string functions *)
    2.43  
    2.44 @@ -190,10 +196,10 @@
    2.45  
    2.46  fun mk_groundness_prems t = map Ground (Term.add_frees t [])
    2.47    
    2.48 -fun translate_prem options ctxt constant_table t =  
    2.49 +fun translate_prem ensure_groundness ctxt constant_table t =  
    2.50      case try HOLogic.dest_not t of
    2.51        SOME t =>
    2.52 -        if #ensure_groundness options then
    2.53 +        if ensure_groundness then
    2.54            Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)])
    2.55          else
    2.56            NegRel_of (translate_literal ctxt constant_table t)
    2.57 @@ -215,7 +221,7 @@
    2.58        (Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq}))))
    2.59      (Thm.transfer thy rule)
    2.60  
    2.61 -fun translate_intros options ctxt gr const constant_table =
    2.62 +fun translate_intros ensure_groundness ctxt gr const constant_table =
    2.63    let
    2.64      val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const)
    2.65      val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
    2.66 @@ -225,7 +231,7 @@
    2.67        let
    2.68          val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro)
    2.69          val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems intro)
    2.70 -        val prems' = Conj (map (translate_prem options ctxt' constant_table') prems)
    2.71 +        val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems)
    2.72          val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems')
    2.73        in clause end
    2.74    in (map translate_intro intros', constant_table') end
    2.75 @@ -250,7 +256,7 @@
    2.76      fst (extend' key (G, []))
    2.77    end
    2.78  
    2.79 -fun generate options ctxt const =
    2.80 +fun generate ensure_groundness ctxt const =
    2.81    let 
    2.82      fun strong_conn_of gr keys =
    2.83        Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
    2.84 @@ -259,7 +265,7 @@
    2.85      val scc = strong_conn_of gr' [const]
    2.86      val constant_table = mk_constant_table (flat scc)
    2.87    in
    2.88 -    apfst flat (fold_map (translate_intros options ctxt gr) (flat scc) constant_table)
    2.89 +    apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
    2.90    end
    2.91    
    2.92  (* implementation for fully enumerating predicates and
    2.93 @@ -402,12 +408,14 @@
    2.94  
    2.95  (* query templates *)
    2.96  
    2.97 -fun query_first rel vnames =
    2.98 +(** query and prelude for swi-prolog **)
    2.99 +
   2.100 +fun swi_prolog_query_first rel vnames =
   2.101    "eval :- once("  ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
   2.102    "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
   2.103    "\\n', [" ^ space_implode ", " vnames ^ "]).\n"
   2.104    
   2.105 -fun query_firstn n rel vnames =
   2.106 +fun swi_prolog_query_firstn n rel vnames =
   2.107    "eval :- findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^
   2.108      rel ^ "(" ^ space_implode ", " vnames ^ "), Sols), writelist(Sols).\n" ^
   2.109      "writelist([]).\n" ^
   2.110 @@ -415,7 +423,7 @@
   2.111      "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
   2.112      "\\n', [" ^ space_implode ", " vnames ^ "]), writelist(T).\n"
   2.113    
   2.114 -val prelude =
   2.115 +val swi_prolog_prelude =
   2.116    "#!/usr/bin/swipl -q -t main -f\n\n" ^
   2.117    ":- use_module(library('dialect/ciao/aggregates')).\n" ^
   2.118    ":- style_check(-singleton).\n" ^
   2.119 @@ -424,6 +432,36 @@
   2.120    "main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
   2.121    "main :- halt(1).\n"
   2.122  
   2.123 +(** query and prelude for yap **)
   2.124 +
   2.125 +fun yap_query_first rel vnames =
   2.126 +  "eval :- once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
   2.127 +  "format('" ^ space_implode ";" (map (fn v => v ^ " = ~w") vnames) ^
   2.128 +  "\\n', [" ^ space_implode ", " vnames ^ "]).\n"
   2.129 +
   2.130 +val yap_prelude =
   2.131 +  "#!/usr/bin/yap -L\n\n" ^
   2.132 +  ":- initialization(eval).\n"
   2.133 +
   2.134 +(* system-dependent query, prelude and invocation *)
   2.135 +
   2.136 +fun query system nsols = 
   2.137 +  case system of
   2.138 +    SWI_PROLOG =>
   2.139 +      (case nsols of NONE => swi_prolog_query_first | SOME n => swi_prolog_query_firstn n)
   2.140 +  | YAP =>
   2.141 +      case nsols of NONE => yap_query_first | SOME n =>
   2.142 +        error "No support for querying multiple solutions in the prolog system yap"
   2.143 +
   2.144 +fun prelude system =
   2.145 +  case system of SWI_PROLOG => swi_prolog_prelude | YAP => yap_prelude
   2.146 +
   2.147 +fun invoke system file_name =
   2.148 +  let
   2.149 +    val cmd =
   2.150 +      case system of SWI_PROLOG => "/usr/local/bin/swipl -f " | YAP => "/usr/local/bin/yap -L "
   2.151 +  in bash_output (cmd ^ file_name) end
   2.152 +
   2.153  (* parsing prolog solution *)
   2.154  
   2.155  val scan_number =
   2.156 @@ -476,19 +514,18 @@
   2.157    
   2.158  (* calling external interpreter and getting results *)
   2.159  
   2.160 -fun run p query_rel vnames nsols =
   2.161 +fun run system p query_rel vnames nsols =
   2.162    let
   2.163      val cmd = Path.named_root
   2.164 -    val query = case nsols of NONE => query_first | SOME n => query_firstn n
   2.165      val p' = rename_vars_program p
   2.166      val _ = tracing "Renaming variable names..."
   2.167      val renaming = fold mk_renaming vnames [] 
   2.168      val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
   2.169 -    val prog = prelude ^ query query_rel vnames' ^ write_program p'
   2.170 +    val prog = prelude system ^ query system nsols query_rel vnames' ^ write_program p'
   2.171      val _ = tracing ("Generated prolog program:\n" ^ prog)
   2.172      val prolog_file = File.tmp_path (Path.basic "prolog_file")
   2.173      val _ = File.write prolog_file prog
   2.174 -    val (solution, _) = bash_output ("/usr/local/bin/swipl -f " ^ File.shell_path prolog_file)
   2.175 +    val (solution, _) = invoke system (File.shell_path prolog_file)
   2.176      val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
   2.177      val tss = parse_solutions solution
   2.178    in
   2.179 @@ -563,12 +600,13 @@
   2.180      val thy' = Predicate_Compile.preprocess preprocess_options t (ProofContext.theory_of ctxt')
   2.181      val ctxt'' = ProofContext.init_global thy'
   2.182      val _ = tracing "Generating prolog program..."
   2.183 -    val (p, constant_table) = generate options ctxt'' name
   2.184 +    val (p, constant_table) = generate (#ensure_groundness options) ctxt'' name
   2.185        |> (if #ensure_groundness options then
   2.186            add_ground_predicates ctxt'' (#limited_types options)
   2.187          else I)
   2.188      val _ = tracing "Running prolog program..."
   2.189 -    val tss = run p (translate_const constant_table name) (map first_upper vnames) soln
   2.190 +    val tss = run (#prolog_system options)
   2.191 +      p (translate_const constant_table name) (map first_upper vnames) soln
   2.192      val _ = tracing "Restoring terms..."
   2.193      val empty = Const("Orderings.bot_class.bot", fastype_of t_compr)
   2.194      fun mk_insert x S =
   2.195 @@ -657,11 +695,11 @@
   2.196      val thy3 = Predicate_Compile.preprocess preprocess_options const thy2
   2.197      val ctxt'' = ProofContext.init_global thy3
   2.198      val _ = tracing "Generating prolog program..."
   2.199 -    val (p, constant_table) = generate {ensure_groundness = true, limited_types = []} ctxt'' full_constname
   2.200 +    val (p, constant_table) = generate true ctxt'' full_constname
   2.201        |> add_ground_predicates ctxt'' (#limited_types (!options))
   2.202      val _ = tracing "Running prolog program..."
   2.203 -    val [ts] = run p (translate_const constant_table full_constname) (map fst vs')
   2.204 -      (SOME 1)
   2.205 +    val [ts] = run (#prolog_system (!options))
   2.206 +      p (translate_const constant_table full_constname) (map fst vs') (SOME 1)
   2.207      val _ = tracing "Restoring terms..."
   2.208      val res = SOME (map (restore_term ctxt'' constant_table) (ts ~~ Ts))
   2.209      val empty_report = ([], false)