equal
deleted
inserted
replaced
4 Prototype of an code generator for logic programming languages (a.k.a. Prolog) |
4 Prototype of an code generator for logic programming languages (a.k.a. Prolog) |
5 *) |
5 *) |
6 |
6 |
7 signature CODE_PROLOG = |
7 signature CODE_PROLOG = |
8 sig |
8 sig |
9 datatype prol_term = Var of string * typ | Cons of string | AppF of string * prol_term list; |
9 datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list; |
10 datatype prem = Conj of prem list | NotRel of string * prol_term list |
10 datatype prem = Conj of prem list | NotRel of string * prol_term list |
11 | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term; |
11 | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term; |
12 type clause = ((string * prol_term list) * prem); |
12 type clause = ((string * prol_term list) * prem); |
13 type logic_program = clause list; |
13 type logic_program = clause list; |
14 type constant_table = (string * string) list |
14 type constant_table = (string * string) list |
33 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; |
33 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; |
34 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; |
34 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; |
35 |
35 |
36 (* internal program representation *) |
36 (* internal program representation *) |
37 |
37 |
38 datatype prol_term = Var of string * typ | Cons of string | AppF of string * prol_term list; |
38 datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list; |
39 |
39 |
40 fun string_of_prol_term (Var (s, T)) = "Var " ^ s |
40 fun string_of_prol_term (Var s) = "Var " ^ s |
41 | string_of_prol_term (Cons s) = "Cons " ^ s |
41 | string_of_prol_term (Cons s) = "Cons " ^ s |
42 | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")" |
42 | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")" |
43 |
43 |
44 datatype prem = Conj of prem list | NotRel of string * prol_term list |
44 datatype prem = Conj of prem list | NotRel of string * prol_term list |
45 | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term; |
45 | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term; |
80 |
80 |
81 (** translation of terms, literals, premises, and clauses **) |
81 (** translation of terms, literals, premises, and clauses **) |
82 |
82 |
83 fun translate_term ctxt constant_table t = |
83 fun translate_term ctxt constant_table t = |
84 case strip_comb t of |
84 case strip_comb t of |
85 (Free (v, T), []) => Var (v, T) |
85 (Free (v, T), []) => Var v |
86 | (Const (c, _), []) => Cons (translate_const constant_table c) |
86 | (Const (c, _), []) => Cons (translate_const constant_table c) |
87 | (Const (c, _), args) => |
87 | (Const (c, _), args) => |
88 AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args) |
88 AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args) |
89 | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t) |
89 | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t) |
90 |
90 |
140 fun string_of_typ (Type (s, Ts)) = Long_Name.base_name s |
140 fun string_of_typ (Type (s, Ts)) = Long_Name.base_name s |
141 |
141 |
142 fun mk_groundness_prems ts = |
142 fun mk_groundness_prems ts = |
143 let |
143 let |
144 val vars = fold add_vars ts [] |
144 val vars = fold add_vars ts [] |
145 fun mk_ground (v, T) = |
145 fun mk_ground v = |
146 Rel ("ground_" ^ string_of_typ T, [Var (v, T)]) |
146 Rel ("ground", [Var v]) |
147 in |
147 in |
148 map mk_ground vars |
148 map mk_ground vars |
149 end |
149 end |
150 |
150 |
151 fun ensure_groundness_prem (NotRel (c, ts)) = Conj (mk_groundness_prems ts @ [NotRel (c, ts)]) |
151 fun ensure_groundness_prem (NotRel (c, ts)) = Conj (mk_groundness_prems ts @ [NotRel (c, ts)]) |
156 fun ensure_groundness_before_negation p = |
156 fun ensure_groundness_before_negation p = |
157 map (apsnd ensure_groundness_prem) p |
157 map (apsnd ensure_groundness_prem) p |
158 |
158 |
159 (* code printer *) |
159 (* code printer *) |
160 |
160 |
161 fun write_term (Var (v, _)) = first_upper v |
161 fun write_term (Var v) = first_upper v |
162 | write_term (Cons c) = c |
162 | write_term (Cons c) = c |
163 | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")" |
163 | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")" |
164 |
164 |
165 fun write_rel (pred, args) = |
165 fun write_rel (pred, args) = |
166 pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")" |
166 pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")" |
221 forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) |
221 forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) |
222 |
222 |
223 fun scan_terms xs = (((scan_term --| $$ ",") ::: scan_terms) |
223 fun scan_terms xs = (((scan_term --| $$ ",") ::: scan_terms) |
224 || (scan_term >> single)) xs |
224 || (scan_term >> single)) xs |
225 and scan_term xs = |
225 and scan_term xs = |
226 ((scan_var >> (fn s => Var (string_of s, dummyT))) |
226 ((scan_var >> (Var o string_of)) |
227 || ((scan_atom -- ($$ "(" |-- scan_terms --| $$ ")")) |
227 || ((scan_atom -- ($$ "(" |-- scan_terms --| $$ ")")) |
228 >> (fn (f, ts) => AppF (string_of f, ts))) |
228 >> (fn (f, ts) => AppF (string_of f, ts))) |
229 || (scan_atom >> (Cons o string_of))) xs |
229 || (scan_atom >> (Cons o string_of))) xs |
230 |
230 |
231 val parse_term = fst o Scan.finite Symbol.stopper |
231 val parse_term = fst o Scan.finite Symbol.stopper |
259 tss |
259 tss |
260 end |
260 end |
261 |
261 |
262 (* values command *) |
262 (* values command *) |
263 |
263 |
264 fun restore_term ctxt constant_table (Var (s, _), T) = Free (s, T) |
264 fun restore_term ctxt constant_table (Var s, T) = Free (s, T) |
265 | restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T) |
265 | restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T) |
266 | restore_term ctxt constant_table (AppF (f, args), T) = |
266 | restore_term ctxt constant_table (AppF (f, args), T) = |
267 let |
267 let |
268 val thy = ProofContext.theory_of ctxt |
268 val thy = ProofContext.theory_of ctxt |
269 val c = restore_const constant_table f |
269 val c = restore_const constant_table f |