1.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Jul 29 17:27:54 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Jul 29 17:27:55 2010 +0200
     1.3 @@ -20,4 +20,6 @@
     1.4    Code_Prolog.run (Code_Prolog.generate @{context} [@{const_name append}]) "append" ["X", "Y", "Z"]
     1.5  *}
     1.6  
     1.7 +values "{(x, y, z). append x y z}"
     1.8 +
     1.9  end

     2.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jul 29 17:27:54 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jul 29 17:27:55 2010 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4  
     2.5    val generate : Proof.context -> string list -> logic_program
     2.6    val write_program : logic_program -> string
     2.7 -  val run : logic_program -> string -> string list -> unit
     2.8 +  val run : logic_program -> string -> string list -> term list
     2.9  
    2.10  end;
    2.11  
    2.12 @@ -29,6 +29,10 @@
    2.13  
    2.14  datatype term = Var of string * typ | Cons of string | AppF of string * term list;
    2.15  
    2.16 +fun string_of_prol_term (Var (s, T)) = "Var " ^ s
    2.17 +  | string_of_prol_term (Cons s) = "Cons " ^ s
    2.18 +  | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")" 
    2.19 +
    2.20  datatype prem = Conj of prem list | NotRel of string * term list | Rel of string * term list | Eq of term * term | NotEq of term * term;
    2.21  
    2.22  fun dest_Rel (Rel (c, ts)) = (c, ts)
    2.23 @@ -145,6 +149,36 @@
    2.24    ":- style_check(-singleton).\n\n" ^
    2.25    "main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
    2.26    "main :- halt(1).\n"
    2.27 +
    2.28 +(* parsing prolog solution *)
    2.29 +
    2.30 +val scan_atom =
    2.31 +  Scan.repeat (Scan.one (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_quasi s))
    2.32 +
    2.33 +val scan_var =
    2.34 +  Scan.repeat (Scan.one
    2.35 +    (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s))
    2.36 +
    2.37 +fun dest_Char (Symbol.Char s) = s
    2.38 +
    2.39 +val string_of = concat o map (dest_Char o Symbol.decode)
    2.40 +
    2.41 +val scan_term =
    2.42 +  scan_atom >> (Cons o string_of) || scan_var >> (Var o rpair dummyT o string_of)
    2.43 +
    2.44 +val parse_term = fst o Scan.finite Symbol.stopper
    2.45 +            (Scan.error (!! (fn _ => raise Fail "parsing prolog output failed"))
    2.46 +                            scan_term)
    2.47 +  o explode
    2.48 +  
    2.49 +fun parse_solution sol =
    2.50 +  let
    2.51 +    fun dest_eq s = (tracing s; tracing(commas (space_explode "=" s)); case space_explode "=" s of
    2.52 +        (l :: r :: []) => parse_term (unprefix " " r)
    2.53 +      | _ => raise Fail "unexpected equation in prolog output")
    2.54 +  in
    2.55 +    map dest_eq (fst (split_last (space_explode "\n" sol)))
    2.56 +  end 
    2.57    
    2.58  (* calling external interpreter and getting results *)
    2.59  
    2.60 @@ -155,8 +189,61 @@
    2.61      val prolog_file = File.tmp_path (Path.basic "prolog_file")
    2.62      val _ = File.write prolog_file prog
    2.63      val (solution, _) = bash_output ("/usr/bin/swipl -f " ^ File.shell_path prolog_file)
    2.64 +    val ts = parse_solution solution
    2.65 +    val _ = tracing (commas (map string_of_prol_term ts)) 
    2.66    in
    2.67 -    tracing ("Prolog returns result:\n" ^ solution)
    2.68 +    ts
    2.69    end
    2.70  
    2.71 +(* values command *)
    2.72 +
    2.73 +fun mk_term (Var (s, T)) = Free (s, T)
    2.74 +  | mk_term (Cons s) = Const (s, dummyT)
    2.75 +  | mk_term (AppF (f, args)) = list_comb (Const (f, dummyT), map mk_term args)
    2.76 +  
    2.77 +fun values ctxt soln t_compr =
    2.78 +  let
    2.79 +    val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
    2.80 +      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
    2.81 +    val (body, Ts, fp) = HOLogic.strip_psplits split;
    2.82 +    val output_names = Name.variant_list (Term.add_free_names body [])
    2.83 +      (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
    2.84 +    val output_frees = map2 (curry Free) output_names (rev Ts)
    2.85 +    val body = subst_bounds (output_frees, body)
    2.86 +    val (pred as Const (name, T), all_args) =
    2.87 +      case strip_comb body of
    2.88 +        (Const (name, T), all_args) => (Const (name, T), all_args)
    2.89 +      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)
    2.90 +    val vnames =
    2.91 +      case try (map (fst o dest_Free)) all_args of
    2.92 +        SOME vs => vs
    2.93 +      | NONE => error ("Not only free variables in " ^ commas (map (Syntax.string_of_term ctxt) all_args))
    2.94 +    val ts = run (generate ctxt [name]) (translate_const name) (map first_upper vnames)
    2.95 +  in
    2.96 +    HOLogic.mk_tuple (map mk_term ts)
    2.97 +  end
    2.98 +
    2.99 +fun values_cmd print_modes soln raw_t state =
   2.100 +  let
   2.101 +    val ctxt = Toplevel.context_of state
   2.102 +    val t = Syntax.read_term ctxt raw_t
   2.103 +    val t' = values ctxt soln t
   2.104 +    val ty' = Term.type_of t'
   2.105 +    val ctxt' = Variable.auto_fixes t' ctxt
   2.106 +    val p = Print_Mode.with_modes print_modes (fn () =>
   2.107 +      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
   2.108 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   2.109 +  in Pretty.writeln p end;
   2.110 +
   2.111 +
   2.112 +(* renewing the values command for Prolog queries *)
   2.113 +
   2.114 +val opt_print_modes =
   2.115 +  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
   2.116 +
   2.117 +val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
   2.118 +  (opt_print_modes -- Scan.optional Parse.nat ~1 -- Parse.term
   2.119 +   >> (fn ((print_modes, soln), t) => Toplevel.keep
   2.120 +        (values_cmd print_modes soln t)));
   2.121 +
   2.122  end;