bulwahn@38319
|
1 |
(* Title: HOL/Tools/Predicate_Compile/code_prolog.ML
|
bulwahn@38319
|
2 |
Author: Lukas Bulwahn, TU Muenchen
|
bulwahn@38319
|
3 |
|
bulwahn@38319
|
4 |
Prototype of an code generator for logic programming languages (a.k.a. Prolog)
|
bulwahn@38319
|
5 |
*)
|
bulwahn@38319
|
6 |
|
bulwahn@38319
|
7 |
signature CODE_PROLOG =
|
bulwahn@38319
|
8 |
sig
|
bulwahn@38319
|
9 |
datatype term = Var of string * typ | Cons of string | AppF of string * term list;
|
bulwahn@38319
|
10 |
datatype prem = Conj of prem list | NotRel of string * term list | Rel of string * term list | Eq of term * term | NotEq of term * term;
|
bulwahn@38319
|
11 |
type clause = ((string * term list) * prem);
|
bulwahn@38319
|
12 |
type logic_program = clause list;
|
bulwahn@38319
|
13 |
|
bulwahn@38319
|
14 |
val generate : Proof.context -> string list -> logic_program
|
bulwahn@38319
|
15 |
val write_program : logic_program -> string
|
bulwahn@38319
|
16 |
val run : logic_program -> string -> string list -> unit
|
bulwahn@38319
|
17 |
|
bulwahn@38319
|
18 |
end;
|
bulwahn@38319
|
19 |
|
bulwahn@38319
|
20 |
structure Code_Prolog : CODE_PROLOG =
|
bulwahn@38319
|
21 |
struct
|
bulwahn@38319
|
22 |
|
bulwahn@38319
|
23 |
(* general string functions *)
|
bulwahn@38319
|
24 |
|
bulwahn@38319
|
25 |
val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
|
bulwahn@38319
|
26 |
val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
|
bulwahn@38319
|
27 |
|
bulwahn@38319
|
28 |
(* internal program representation *)
|
bulwahn@38319
|
29 |
|
bulwahn@38319
|
30 |
datatype term = Var of string * typ | Cons of string | AppF of string * term list;
|
bulwahn@38319
|
31 |
|
bulwahn@38319
|
32 |
datatype prem = Conj of prem list | NotRel of string * term list | Rel of string * term list | Eq of term * term | NotEq of term * term;
|
bulwahn@38319
|
33 |
|
bulwahn@38319
|
34 |
fun dest_Rel (Rel (c, ts)) = (c, ts)
|
bulwahn@38319
|
35 |
|
bulwahn@38319
|
36 |
type clause = ((string * term list) * prem);
|
bulwahn@38319
|
37 |
|
bulwahn@38319
|
38 |
type logic_program = clause list;
|
bulwahn@38319
|
39 |
|
bulwahn@38319
|
40 |
(* translation from introduction rules to internal representation *)
|
bulwahn@38319
|
41 |
|
bulwahn@38319
|
42 |
(* assuming no clashing *)
|
bulwahn@38319
|
43 |
fun translate_const c = Long_Name.base_name c
|
bulwahn@38319
|
44 |
|
bulwahn@38319
|
45 |
fun translate_term ctxt t =
|
bulwahn@38319
|
46 |
case strip_comb t of
|
bulwahn@38319
|
47 |
(Free (v, T), []) => Var (v, T)
|
bulwahn@38319
|
48 |
| (Const (c, _), []) => Cons (translate_const c)
|
bulwahn@38319
|
49 |
| (Const (c, _), args) => AppF (translate_const c, map (translate_term ctxt) args)
|
bulwahn@38319
|
50 |
| _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t)
|
bulwahn@38319
|
51 |
|
bulwahn@38319
|
52 |
|
bulwahn@38319
|
53 |
fun translate_literal ctxt t =
|
bulwahn@38319
|
54 |
case strip_comb t of
|
bulwahn@38319
|
55 |
(Const (@{const_name "op ="}, _), [l, r]) => Eq (pairself (translate_term ctxt) (l, r))
|
bulwahn@38319
|
56 |
| (Const (c, _), args) => Rel (translate_const c, map (translate_term ctxt) args)
|
bulwahn@38319
|
57 |
| _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t)
|
bulwahn@38319
|
58 |
|
bulwahn@38319
|
59 |
fun NegRel_of (Rel lit) = NotRel lit
|
bulwahn@38319
|
60 |
| NegRel_of (Eq eq) = NotEq eq
|
bulwahn@38319
|
61 |
|
bulwahn@38319
|
62 |
fun translate_prem ctxt t =
|
bulwahn@38319
|
63 |
case try HOLogic.dest_not t of
|
bulwahn@38319
|
64 |
SOME t => NegRel_of (translate_literal ctxt t)
|
bulwahn@38319
|
65 |
| NONE => translate_literal ctxt t
|
bulwahn@38319
|
66 |
|
bulwahn@38319
|
67 |
fun translate_intros ctxt gr const =
|
bulwahn@38319
|
68 |
let
|
bulwahn@38319
|
69 |
val intros = Graph.get_node gr const
|
bulwahn@38319
|
70 |
val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt
|
bulwahn@38319
|
71 |
fun translate_intro intro =
|
bulwahn@38319
|
72 |
let
|
bulwahn@38319
|
73 |
val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro)
|
bulwahn@38319
|
74 |
val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems intro)
|
bulwahn@38319
|
75 |
val prems' = Conj (map (translate_prem ctxt') prems)
|
bulwahn@38319
|
76 |
val clause = (dest_Rel (translate_literal ctxt' head), prems')
|
bulwahn@38319
|
77 |
in clause end
|
bulwahn@38319
|
78 |
in map translate_intro intros' end
|
bulwahn@38319
|
79 |
|
bulwahn@38319
|
80 |
fun generate ctxt const =
|
bulwahn@38319
|
81 |
let
|
bulwahn@38319
|
82 |
fun strong_conn_of gr keys =
|
bulwahn@38319
|
83 |
Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
|
bulwahn@38319
|
84 |
val gr = Predicate_Compile_Core.intros_graph_of ctxt
|
bulwahn@38319
|
85 |
val scc = strong_conn_of gr const
|
bulwahn@38319
|
86 |
val _ = tracing (commas (flat scc))
|
bulwahn@38319
|
87 |
in
|
bulwahn@38319
|
88 |
maps (translate_intros ctxt gr) (flat scc)
|
bulwahn@38319
|
89 |
end
|
bulwahn@38319
|
90 |
|
bulwahn@38319
|
91 |
(* transform logic program *)
|
bulwahn@38319
|
92 |
|
bulwahn@38319
|
93 |
(** ensure groundness of terms before negation **)
|
bulwahn@38319
|
94 |
|
bulwahn@38319
|
95 |
fun add_vars (Var x) vs = insert (op =) x vs
|
bulwahn@38319
|
96 |
| add_vars (Cons c) vs = vs
|
bulwahn@38319
|
97 |
| add_vars (AppF (f, args)) vs = fold add_vars args vs
|
bulwahn@38319
|
98 |
|
bulwahn@38319
|
99 |
fun string_of_typ (Type (s, Ts)) = Long_Name.base_name s
|
bulwahn@38319
|
100 |
|
bulwahn@38319
|
101 |
fun mk_groundness_prems ts =
|
bulwahn@38319
|
102 |
let
|
bulwahn@38319
|
103 |
val vars = fold add_vars ts []
|
bulwahn@38319
|
104 |
fun mk_ground (v, T) =
|
bulwahn@38319
|
105 |
Rel ("ground_" ^ string_of_typ T, [Var (v, T)])
|
bulwahn@38319
|
106 |
in
|
bulwahn@38319
|
107 |
map mk_ground vars
|
bulwahn@38319
|
108 |
end
|
bulwahn@38319
|
109 |
|
bulwahn@38319
|
110 |
fun ensure_groundness_prem (NotRel (c, ts)) = Conj (mk_groundness_prems ts @ [NotRel (c, ts)])
|
bulwahn@38319
|
111 |
| ensure_groundness_prem (NotEq (l, r)) = Conj (mk_groundness_prems [l, r] @ [NotEq (l, r)])
|
bulwahn@38319
|
112 |
| ensure_groundness_prem (Conj ps) = Conj (map ensure_groundness_prem ps)
|
bulwahn@38319
|
113 |
| ensure_groundness_prem p = p
|
bulwahn@38319
|
114 |
|
bulwahn@38319
|
115 |
fun ensure_groundness_before_negation p =
|
bulwahn@38319
|
116 |
map (apsnd ensure_groundness_prem) p
|
bulwahn@38319
|
117 |
|
bulwahn@38319
|
118 |
(* code printer *)
|
bulwahn@38319
|
119 |
|
bulwahn@38319
|
120 |
fun write_term (Var (v, _)) = first_upper v
|
bulwahn@38319
|
121 |
| write_term (Cons c) = first_lower c
|
bulwahn@38319
|
122 |
| write_term (AppF (f, args)) = first_lower f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
|
bulwahn@38319
|
123 |
|
bulwahn@38319
|
124 |
fun write_rel (pred, args) =
|
bulwahn@38319
|
125 |
pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
|
bulwahn@38319
|
126 |
|
bulwahn@38319
|
127 |
fun write_prem (Conj prems) = space_implode ", " (map write_prem prems)
|
bulwahn@38319
|
128 |
| write_prem (Rel p) = write_rel p
|
bulwahn@38319
|
129 |
| write_prem (NotRel p) = "not(" ^ write_rel p ^ ")"
|
bulwahn@38319
|
130 |
| write_prem (Eq (l, r)) = write_term l ^ " = " ^ write_term r
|
bulwahn@38319
|
131 |
| write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r
|
bulwahn@38319
|
132 |
|
bulwahn@38319
|
133 |
fun write_clause (head, prem) =
|
bulwahn@38319
|
134 |
write_rel head ^ (if prem = Conj [] then "." else " :- " ^ write_prem prem ^ ".")
|
bulwahn@38319
|
135 |
|
bulwahn@38319
|
136 |
fun write_program p =
|
bulwahn@38319
|
137 |
cat_lines (map write_clause p)
|
bulwahn@38319
|
138 |
|
bulwahn@38319
|
139 |
fun query_first rel vnames =
|
bulwahn@38319
|
140 |
"eval :- once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
|
bulwahn@38319
|
141 |
"writef('" ^ implode (map (fn v => v ^ " = %w\\n") vnames) ^"', [" ^ space_implode ", " vnames ^ "]).\n"
|
bulwahn@38319
|
142 |
|
bulwahn@38319
|
143 |
val prelude =
|
bulwahn@38319
|
144 |
"#!/usr/bin/swipl -q -t main -f\n\n" ^
|
bulwahn@38319
|
145 |
":- style_check(-singleton).\n\n" ^
|
bulwahn@38319
|
146 |
"main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
|
bulwahn@38319
|
147 |
"main :- halt(1).\n"
|
bulwahn@38319
|
148 |
|
bulwahn@38319
|
149 |
(* calling external interpreter and getting results *)
|
bulwahn@38319
|
150 |
|
bulwahn@38319
|
151 |
fun run p query_rel vnames =
|
bulwahn@38319
|
152 |
let
|
bulwahn@38319
|
153 |
val cmd = Path.named_root
|
bulwahn@38319
|
154 |
val prog = prelude ^ query_first query_rel vnames ^ write_program p
|
bulwahn@38319
|
155 |
val prolog_file = File.tmp_path (Path.basic "prolog_file")
|
bulwahn@38319
|
156 |
val _ = File.write prolog_file prog
|
bulwahn@38319
|
157 |
val (solution, _) = bash_output ("/usr/bin/swipl -f " ^ File.shell_path prolog_file)
|
bulwahn@38319
|
158 |
in
|
bulwahn@38319
|
159 |
tracing ("Prolog returns result:\n" ^ solution)
|
bulwahn@38319
|
160 |
end
|
bulwahn@38319
|
161 |
|
bulwahn@38319
|
162 |
end;
|