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